Skip to content

Commit 8373608

Browse files
myreenmyreen
authored
Merge pull request #1158 from CakeML/remove-set-skip
2 parents 8ea3640 + a52198d commit 8373608

26 files changed

+51
-65
lines changed

‎basis/RatProgScript.sml

+3-1
Original file line numberDiff line numberDiff line change
@@ -991,7 +991,9 @@ val RATIONAL_TYPE_def = fetch "-" "RATIONAL_TYPE_def"
991991
Theorem EqualityType_RAT_TYPE = Q.prove(`
992992
EqualityType RAT_TYPE`,
993993
rw [EqualityType_def]
994-
\\ fs [RAT_TYPE_def,RATIONAL_TYPE_def,INT_def,NUM_def] \\ EVAL_TAC
994+
\\ fs [RAT_TYPE_def,RATIONAL_TYPE_def,INT_def,NUM_def]
995+
>~ [‘no_closures’] >- EVAL_TAC
996+
>~ [‘types_match’] >- EVAL_TAC
995997
\\ rveq \\ fs []
996998
\\ EQ_TAC \\ strip_tac \\ fs []
997999
\\ fs [GSYM rat_of_int_def]

‎basis/Word64ProgScript.sml

+2-2
Original file line numberDiff line numberDiff line change
@@ -98,8 +98,8 @@ Theorem var_word_asr_thm[simp]:
9898
var_word_asr w n = word_asr w n
9999
Proof
100100
ntac 32 (
101-
Cases_on `n` \\ fs [ADD1] THEN1 (EVAL_TAC \\ fs [ASR_ADD])
102-
\\ Cases_on `n'` \\ fs [ADD1] THEN1 (EVAL_TAC \\ fs [ASR_ADD]))
101+
Cases_on `n` \\ fs [ADD1] THEN1 (rw [] \\ EVAL_TAC \\ fs [ASR_ADD])
102+
\\ Cases_on `n'` \\ fs [ADD1] THEN1 (rw [] \\ EVAL_TAC \\ fs [ASR_ADD]))
103103
\\ ntac 9 (once_rewrite_tac [var_word_asr_def] \\ fs [])
104104
QED
105105

‎basis/Word8ProgScript.sml

+2-2
Original file line numberDiff line numberDiff line change
@@ -101,8 +101,8 @@ Theorem var_word_asr_thm[simp]:
101101
var_word_asr w n = word_asr w n
102102
Proof
103103
ntac 32 (
104-
Cases_on `n` \\ fs [ADD1] THEN1 (EVAL_TAC \\ fs [ASR_ADD])
105-
\\ Cases_on `n'` \\ fs [ADD1] THEN1 (EVAL_TAC \\ fs [ASR_ADD]))
104+
Cases_on `n` \\ fs [ADD1] THEN1 (rw [] \\ EVAL_TAC \\ fs [ASR_ADD])
105+
\\ Cases_on `n'` \\ fs [ADD1] THEN1 (rw [] \\ EVAL_TAC \\ fs [ASR_ADD]))
106106
\\ ntac 9 (once_rewrite_tac [var_word_asr_def] \\ fs [])
107107
QED
108108

‎basis/basis_ffiLib.sml

+4-2
Original file line numberDiff line numberDiff line change
@@ -24,8 +24,10 @@ val prove_parts_ok_st =
2424
\\ `st.ffi.oracle = basis_ffi_oracle`
2525
by( simp[Abbr`st`] \\ EVAL_TAC \\ NO_TAC)
2626
\\ rw[cfStoreTheory.parts_ok_def]
27-
\\ TRY ( simp[Abbr`st`] \\ EVAL_TAC \\ NO_TAC )
28-
\\ TRY ( imp_res_tac oracle_parts \\ rfs[] \\ NO_TAC)
27+
>- EVAL_TAC
28+
>- (simp[Abbr`st`] \\ EVAL_TAC)
29+
>~ [‘_ |++ _’] >- (imp_res_tac oracle_parts \\ gvs [])
30+
>~ [‘SOME FFIdiverge’] >- (imp_res_tac oracle_parts_div \\ rfs[])
2931
\\ qpat_x_assum`MEM _ basis_proj2`mp_tac
3032
\\ simp[basis_proj2_def,basis_ffi_part_defs,cfHeapsBaseTheory.mk_proj2_def]
3133
\\ TRY (qpat_x_assum`_ = SOME _`mp_tac)

‎basis/basis_ffiScript.sml

+4-3
Original file line numberDiff line numberDiff line change
@@ -720,9 +720,10 @@ Proof
720720
\\ `st.ffi.oracle = basis_ffi_oracle`
721721
by( simp[Abbr`st`] \\ EVAL_TAC \\ NO_TAC)
722722
\\ rw[cfStoreTheory.parts_ok_def]
723-
\\ TRY ( simp[Abbr`st`] \\ EVAL_TAC \\ NO_TAC )
724-
\\ TRY ( imp_res_tac oracle_parts \\ rfs[] \\ NO_TAC)
725-
\\ TRY ( imp_res_tac oracle_parts_div \\ rfs[] \\ NO_TAC)
723+
>- EVAL_TAC
724+
>- (simp[Abbr`st`] \\ EVAL_TAC)
725+
>~ [‘_ |++ _’] >- (imp_res_tac oracle_parts \\ gvs [])
726+
>~ [‘SOME FFIdiverge’] >- (imp_res_tac oracle_parts_div \\ rfs[])
726727
\\ qpat_x_assum`MEM _ basis_proj2`mp_tac
727728
\\ simp[basis_proj2_def,basis_ffi_part_defs,cfHeapsBaseTheory.mk_proj2_def]
728729
\\ TRY (qpat_x_assum`_ = SOME _`mp_tac)

‎characteristic/cfHeapsBaseSyntax.sml

+1-1
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ local
1414
structure Parse = struct
1515
open Parse
1616
val (Type,Term) =
17-
parse_from_grammars cfHeapsBaseTheory.cfHeapsBase_grammars
17+
parse_from_grammars $ valOf $ grammarDB {thyname = "cfHeapsBase"}
1818
end
1919
open Parse
2020
in

‎characteristic/cfTacticsLib.sml

+1-1
Original file line numberDiff line numberDiff line change
@@ -625,7 +625,7 @@ in if Teq (rhs (concl th)) then th else fail () end
625625

626626
val validate_pat_all_conv =
627627
REPEATC (
628-
RAND_CONV validate_pat_conv THENC RW.RW_CONV [boolTheory.AND_CLAUSES]
628+
RAND_CONV validate_pat_conv THENC PURE_REWRITE_CONV [boolTheory.AND_CLAUSES]
629629
)
630630

631631
local

‎compiler/bootstrap/translation/arm8ProgScript.sml

+2
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,8 @@ val _ = set_grammar_ancestry ["arm8_target", "arm8"];
1414

1515
val _ = new_theory "arm8Prog"
1616

17+
val () = computeLib.set_skip computeLib.the_compset “COND” (SOME 1);
18+
1719
val _ = translation_extends "x64Prog";
1820
val _ = ml_translatorLib.use_string_type true;
1921
val _ = ml_translatorLib.use_sub_check true;

‎compiler/bootstrap/translation/to_target32ProgScript.sml

+2
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,8 @@ val _ = translation_extends "to_word32Prog";
1414
val _ = ml_translatorLib.use_string_type true;
1515
val _ = ml_translatorLib.use_sub_check true;
1616

17+
val () = computeLib.set_skip computeLib.the_compset “COND” (SOME 1);
18+
1719
val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "to_target32Prog");
1820

1921
val RW = REWRITE_RULE

‎compiler/bootstrap/translation/to_target64ProgScript.sml

+2
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,8 @@ val _ = translation_extends "to_word64Prog";
1414
val _ = ml_translatorLib.use_string_type true;
1515
val _ = ml_translatorLib.use_sub_check true;
1616

17+
val () = computeLib.set_skip computeLib.the_compset “COND” (SOME 1);
18+
1719
val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "to_target64Prog");
1820

1921
val RW = REWRITE_RULE

‎compiler/bootstrap/translation/to_word32ProgScript.sml

+4-4
Original file line numberDiff line numberDiff line change
@@ -519,7 +519,7 @@ val word_inst_three_to_two_reg_side = Q.prove(`
519519
>> fs[]
520520
>> rw[Once(fetch "-" "word_inst_three_to_two_reg_side_def")]
521521
>> fs[]
522-
>> POP_ASSUM(ASSUME_TAC o RW.PURE_ONCE_RW_RULE[fetch"-" "word_inst_three_to_two_reg_side_def"])
522+
>> POP_ASSUM(ASSUME_TAC o PURE_ONCE_REWRITE_RULE[fetch"-" "word_inst_three_to_two_reg_side_def"])
523523
>> fs[]
524524
>> metis_tac[pair_CASES,option_CASES]) |> update_precondition
525525

@@ -561,7 +561,7 @@ val word_remove_remove_must_terminate_side = Q.prove(`
561561
>> fs[]
562562
>> rw[Once(fetch "-" "word_remove_remove_must_terminate_side_def")]
563563
>> fs[]
564-
>> POP_ASSUM(ASSUME_TAC o RW.PURE_ONCE_RW_RULE[fetch"-" "word_remove_remove_must_terminate_side_def"])
564+
>> POP_ASSUM(ASSUME_TAC o PURE_ONCE_REWRITE_RULE[fetch"-" "word_remove_remove_must_terminate_side_def"])
565565
>> fs[]
566566
>> metis_tac[pair_CASES,option_CASES]) |> update_precondition;
567567

@@ -583,7 +583,7 @@ val word_simp_const_fp_loop_side = Q.prove(`
583583
>> fs[]
584584
>> rw[Once(fetch "-" "word_simp_const_fp_loop_side_def")]
585585
>> fs[]
586-
>> POP_ASSUM(ASSUME_TAC o RW.PURE_ONCE_RW_RULE[fetch"-" "word_simp_const_fp_loop_side_def"])
586+
>> POP_ASSUM(ASSUME_TAC o PURE_ONCE_REWRITE_RULE[fetch"-" "word_simp_const_fp_loop_side_def"])
587587
>> fs[]
588588
>> metis_tac[pair_CASES,option_CASES]) |> update_precondition
589589
@@ -614,7 +614,7 @@ val word_inst_inst_select_side = Q.prove(`
614614
>> fs[]
615615
>> rw[Once(fetch "-" "word_inst_inst_select_side_def")]
616616
>> fs[]
617-
>> POP_ASSUM(ASSUME_TAC o RW.PURE_ONCE_RW_RULE[fetch"-" "word_inst_inst_select_side_def"])
617+
>> POP_ASSUM(ASSUME_TAC o PURE_ONCE_REWRITE_RULE[fetch"-" "word_inst_inst_select_side_def"])
618618
>> fs[]
619619
>> metis_tac[pair_CASES,option_CASES,fetch "asm" "reg_imm_nchotomy"]) |> update_precondition
620620
*)

‎compiler/bootstrap/translation/to_word64ProgScript.sml

+4-4
Original file line numberDiff line numberDiff line change
@@ -512,7 +512,7 @@ val word_inst_three_to_two_reg_side = Q.prove(`
512512
>> fs[]
513513
>> rw[Once(fetch "-" "word_inst_three_to_two_reg_side_def")]
514514
>> fs[]
515-
>> POP_ASSUM(ASSUME_TAC o RW.PURE_ONCE_RW_RULE[fetch"-" "word_inst_three_to_two_reg_side_def"])
515+
>> POP_ASSUM(ASSUME_TAC o PURE_ONCE_REWRITE_RULE[fetch"-" "word_inst_three_to_two_reg_side_def"])
516516
>> fs[]
517517
>> metis_tac[pair_CASES,option_CASES]) |> update_precondition
518518

@@ -554,7 +554,7 @@ val word_remove_remove_must_terminate_side = Q.prove(`
554554
>> fs[]
555555
>> rw[Once(fetch "-" "word_remove_remove_must_terminate_side_def")]
556556
>> fs[]
557-
>> POP_ASSUM(ASSUME_TAC o RW.PURE_ONCE_RW_RULE[fetch"-" "word_remove_remove_must_terminate_side_def"])
557+
>> POP_ASSUM(ASSUME_TAC o PURE_ONCE_REWRITE_RULE[fetch"-" "word_remove_remove_must_terminate_side_def"])
558558
>> fs[]
559559
>> metis_tac[pair_CASES,option_CASES]) |> update_precondition;
560560

@@ -576,7 +576,7 @@ val word_simp_const_fp_loop_side = Q.prove(`
576576
>> fs[]
577577
>> rw[Once(fetch "-" "word_simp_const_fp_loop_side_def")]
578578
>> fs[]
579-
>> POP_ASSUM(ASSUME_TAC o RW.PURE_ONCE_RW_RULE[fetch"-" "word_simp_const_fp_loop_side_def"])
579+
>> POP_ASSUM(ASSUME_TAC o PURE_ONCE_REWRITE_RULE[fetch"-" "word_simp_const_fp_loop_side_def"])
580580
>> fs[]
581581
>> metis_tac[pair_CASES,option_CASES]) |> update_precondition
582582
@@ -607,7 +607,7 @@ val word_inst_inst_select_side = Q.prove(`
607607
>> fs[]
608608
>> rw[Once(fetch "-" "word_inst_inst_select_side_def")]
609609
>> fs[]
610-
>> POP_ASSUM(ASSUME_TAC o RW.PURE_ONCE_RW_RULE[fetch"-" "word_inst_inst_select_side_def"])
610+
>> POP_ASSUM(ASSUME_TAC o PURE_ONCE_REWRITE_RULE[fetch"-" "word_inst_inst_select_side_def"])
611611
>> fs[]
612612
>> metis_tac[pair_CASES,option_CASES,fetch "asm" "reg_imm_nchotomy"]) |> update_precondition
613613
*)

‎compiler/encoders/ag32/ag32_targetLib.sml

+1-1
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ open optionLib
1111
structure Parse = struct
1212
open Parse
1313
val (Type, Term) =
14-
parse_from_grammars ag32_targetTheory.ag32_target_grammars
14+
parse_from_grammars $ valOf $ grammarDB {thyname = "ag32_target"}
1515
end
1616
open Parse
1717

‎compiler/encoders/ag32/proofs/ag32_targetProofScript.sml

+2-2
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
Prove `encoder_correct` for ag32, i.e. Silver ISA
33
*)
44
open HolKernel Parse boolLib bossLib
5-
open asmLib ag32_targetTheory;
5+
open asmLib ag32_targetTheory Import;
66

77
val () = new_theory "ag32_targetProof"
88

@@ -274,7 +274,7 @@ local
274274
val thms =
275275
List.map (DB.fetch "ag32")
276276
(List.filter (fn s => not (Lib.mem s ["Next_def", "Encode_def"]))
277-
(#C (ag32Theory.inventory)))
277+
(#C (Import.gen_inventory {thyname="ag32"})))
278278
val is_ag32_next = #4 (HolKernel.syntax_fns1 "ag32" "Next")
279279
in
280280
fun next_state_tac (asl, g) =

‎compiler/encoders/arm7/arm7_targetLib.sml

+1-1
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ open optionLib
1111
structure Parse = struct
1212
open Parse
1313
val (Type, Term) =
14-
parse_from_grammars arm7_eval_encodeTheory.arm7_eval_encode_grammars
14+
parse_from_grammars $ valOf $ grammarDB {thyname = "arm7_eval_encode"}
1515
end
1616
open Parse
1717

‎compiler/encoders/asm/asmLib.sml

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ open asmTheory asmSemTheory asmPropsTheory utilsLib
99

1010
structure Parse = struct
1111
open Parse
12-
val (Type,Term) = parse_from_grammars asmPropsTheory.asmProps_grammars
12+
val (Type,Term) = parse_from_grammars $ valOf $ grammarDB {thyname="asmProps"}
1313
end
1414

1515
open Parse

‎compiler/encoders/x64/x64_targetLib.sml

+1-1
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ open optionLib
1111
structure Parse = struct
1212
open Parse
1313
val (Type, Term) =
14-
parse_from_grammars x64_eval_encodeTheory.x64_eval_encode_grammars
14+
parse_from_grammars $ valOf $ grammarDB {thyname="x64_eval_encode"}
1515
end
1616
open Parse
1717

‎examples/README.md

-3
Original file line numberDiff line numberDiff line change
@@ -60,9 +60,6 @@ An LPR checker built on CakeML
6060
[md5ProgScript.sml](md5ProgScript.sml):
6161
Translate md5 function
6262

63-
[md5Script.sml](md5Script.sml):
64-
Functional definition of md5 hash based on HOL/src/portableML/poly/MD5.sml
65-
6663
[opentheory](opentheory):
6764
Implementation of an OpenTheory reader based on the Candle kernel.
6865

‎examples/pseudo_bool/array/npbc_parseProgScript.sml

+2
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,8 @@ val _ = new_theory "npbc_parseProg"
77

88
val _ = translation_extends"npbc_arrayProg";
99

10+
val () = computeLib.set_skip computeLib.the_compset “COND” (SOME 1);
11+
1012
val xlet_autop = xlet_auto >- (TRY( xcon) >> xsimpl)
1113

1214
val r = translate strip_numbers_def;

‎icing/examples/exampleLib.sml

+2-5
Original file line numberDiff line numberDiff line change
@@ -673,11 +673,8 @@ end;
673673
|> map (#2 o #1)
674674
|> dedup
675675
|> List.foldl (fn (elem, acc) => acc ^ " " ^ elem ^ " ;") "Used rewrites:"
676-
val _ = adjoin_to_theory
677-
{ sig_ps =
678-
SOME (fn _ => PP.add_string
679-
("(* "^hotRewrites^" *)")),
680-
struct_ps = NONE };
676+
(* REMOVED: this Lib used to print hotRewrites to the theory signature
677+
using adjoin_to_theory. That feature has now been removed. *)
681678
(** The code below stores in theorem theAST_opt the optimized version of the AST
682679
from above and in errorbounds_AST the inferred FloVer roundoff error bounds
683680
**)

‎pancake/README.md

+5-2
Original file line numberDiff line numberDiff line change
@@ -39,8 +39,8 @@ instructions for conditionals, While loop,
3939
memory load and store, functions,
4040
and foreign function calls.
4141

42-
[panScopeScript.sml](panScopeScript.sml):
43-
Scope checking for Pancake.
42+
[panStaticScript.sml](panStaticScript.sml):
43+
Static checking for Pancake.
4444

4545
[pan_commonScript.sml](pan_commonScript.sml):
4646
Common definitions for Pancake compiler
@@ -70,6 +70,9 @@ Proofs files for compiling Pancake.
7070
[semantics](semantics):
7171
Semantics for Pancake and its intermediate languages.
7272

73+
[static_checker](static_checker):
74+
Support files for Pancake static checker
75+
7376
[taParserScript.sml](taParserScript.sml):
7477
Parser for compactDSL programs
7578

‎translator/ml_translatorLib.sml

+1-24
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ local
2727
structure Parse = struct
2828
open Parse
2929
val (Type,Term) =
30-
parse_from_grammars ml_translatorTheory.ml_translator_grammars
30+
parse_from_grammars $ valOf $ grammarDB {thyname="ml_translator"}
3131
end
3232
open Parse
3333
val prim_exn_list = let
@@ -1592,29 +1592,6 @@ val (ml_ty_name,x::xs,ty,lhs,input) = hd ys
15921592
fun domain ty = ty |> dest_fun_type |> fst
15931593
fun codomain ty = ty |> dest_fun_type |> snd
15941594

1595-
fun persistent_skip_case_const const = let
1596-
val ty = (domain (type_of const))
1597-
fun thy_name_to_string thy name =
1598-
if thy = current_theory() then name else thy ^ "Theory." ^ name
1599-
val thm_name = if ty = bool then "COND_DEF" else
1600-
DB.match [] (concl (TypeBase.case_def_of ty))
1601-
|> map (fn ((thy,name),_) => thy_name_to_string thy name) |> hd
1602-
val str = thm_name
1603-
val str = "(Drule.CONJUNCTS " ^ str ^ ")"
1604-
val str = "(List.hd " ^ str ^ ")"
1605-
val str = "(Drule.SPEC_ALL " ^ str ^ ")"
1606-
val str = "(Thm.concl " ^ str ^ ")"
1607-
val str = "(boolSyntax.dest_eq " ^ str ^ ")"
1608-
val str = "(Lib.fst " ^ str ^ ")"
1609-
val str = "(Lib.repeat Term.rator " ^ str ^ ")"
1610-
val str = "val () = computeLib.set_skip computeLib.the_compset" ^
1611-
" " ^ str ^ " (SOME 1);\n"
1612-
val _ = adjoin_to_theory
1613-
{sig_ps = NONE, struct_ps = SOME(fn _ => PP.add_string str)}
1614-
in computeLib.set_skip computeLib.the_compset const (SOME 1) end
1615-
1616-
val _ = persistent_skip_case_const (get_term "COND");
1617-
16181595
val (FILTER_ASSUM_TAC : (term -> bool) -> tactic) = let
16191596
fun sing f [x] = f x
16201597
| sing f _ = raise ERR "sing" "Bind Error"

‎translator/monadic/cfMonadLib.sml

+1-1
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ local
1111
structure Parse = struct
1212
open Parse
1313
val (Type,Term) =
14-
parse_from_grammars cfMonadTheory.cfMonad_grammars
14+
parse_from_grammars $ valOf $ grammarDB {thyname = "cfMonad"}
1515
end
1616
open Parse
1717
in

‎translator/monadic/ml_monadStoreLib.sml

+1-1
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ local
4646
structure Parse = struct
4747
open Parse
4848
val (Type,Term) =
49-
parse_from_grammars ml_monadStoreTheory.ml_monadStore_grammars
49+
parse_from_grammars $ valOf $ grammarDB {thyname="ml_monadStore"}
5050
end
5151
open Parse
5252
(* Information about the subscript exceptions *)

‎translator/monadic/ml_monad_translatorLib.sml

+1-2
Original file line numberDiff line numberDiff line change
@@ -54,8 +54,7 @@ local
5454
structure Parse = struct
5555
open Parse
5656
val (Type,Term) =
57-
parse_from_grammars
58-
ml_monad_translatorTheory.ml_monad_translator_grammars
57+
parse_from_grammars $ valOf $ grammarDB {thyname="ml_monad_translator"}
5958
end
6059
open Parse
6160

‎translator/monadic/monad_base/ml_monadBaseLib.sml

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ local
1212
structure Parse = struct
1313
open Parse
1414
val (Type,Term) =
15-
parse_from_grammars ml_monadBaseTheory.ml_monadBase_grammars
15+
parse_from_grammars (valOf (grammarDB {thyname="ml_monadBase"}))
1616
end
1717
open Parse
1818

0 commit comments

Comments
 (0)