Skip to content

Commit

Permalink
change interface to add_persistent_funs (#73) and fix more calls
Browse files Browse the repository at this point in the history 
The new interface takes a list of strings naming theorems.
(The old interface took a list of (string * thm) pairs.)
The new way better ensures consistency of theory development and theory
load behaviour: you can no longer pass a name with a theorem that isn't
actually saved under it.

Theorems are looked up with DB.theorem, or failing that, DB.definition
or DB.axiom.

Alas, I found more examples using add_persistent_funs to add theorems in
ancestor theories. Rather than modify the ancestor theories, I have
opted to make the offending theories save the theorems they want to add
to computeLib themselves so they have a name in the current theory to
pass to add_persistent_funs.

If this behavior was appropriate for patricia too (da47401) change it.
Alternatively, if the ancestor theories should have exported those
things for computeLib anyway, search this commit for new instances of
"save_thm" to see what needs fixing.
  • Loading branch information
@xrchz
xrchz committed Jul 30, 2012
1 parent da47401 commit 0fc7587
Show file tree
Hide file tree
Showing 37 changed files with 258 additions and 259 deletions.
10 changes: 6 additions & 4 deletions examples/ARM/v4/armScript.sml
View file
Expand Up @@ -919,11 +919,13 @@ val ARM_SPEC_def = Define`

(* ------------------------------------------------------------------------- *)

val _ = let open pred_setTheory in
val _ = let open pred_setTheory
val _ = save_thm("pred_setTheory_IN_INSERT",IN_INSERT)
val _ = save_thm("pred_setTheory_NOT_IN_EMPTY",NOT_IN_EMPTY)
in
computeLib.add_persistent_funs
([("pred_setTheory.IN_INSERT", IN_INSERT),
("pred_setTheory.NOT_IN_EMPTY", NOT_IN_EMPTY)] @
map (fn s => (s, theorem s))
(["pred_setTheory_IN_INSERT",
"pred_setTheory_NOT_IN_EMPTY"] @
["register_EQ_register","num2register_thm","register2num_thm", "mode_EQ_mode",
"mode2num_thm", "psr_EQ_psr", "psr2num_thm", "iclass_EQ_iclass",
"iclass2num_thm", "num2condition_thm", "condition2num_thm",
Expand Down
72 changes: 39 additions & 33 deletions examples/ARM/v7/arm_coretypesScript.sml
View file
Expand Up @@ -482,40 +482,46 @@ val encode_psr_bits = Q.store_thm("encode_psr_bits",

(* ------------------------------------------------------------------------ *)

val _ = app save_thm
[("pairTheory_UNCURRY",pairTheory.UNCURRY)
("pairTheory_LEX_DEF",pairTheory.LEX_DEF)
("pred_setTheory_IN_CROSS",pred_setTheory.IN_CROSS)
("pred_setTheory_IN_DELETE",pred_setTheory.IN_DELETE)
("wordsTheory_BIT_UPDATE",wordsTheory.BIT_UPDATE)]
val _ = computeLib.add_persistent_funs
[("pairTheory.UNCURRY", pairTheory.UNCURRY),
("pairTheory.LEX_DEF", pairTheory.LEX_DEF),
("pred_setTheory.IN_CROSS", pred_setTheory.IN_CROSS),
("pred_setTheory.IN_DELETE", pred_setTheory.IN_DELETE),
("wordsTheory.BIT_UPDATE", wordsTheory.BIT_UPDATE),
("NOT_IN_EMPTY_SPECIFICATION", NOT_IN_EMPTY_SPECIFICATION),
("NUMERIC_LSL_C", NUMERIC_LSL_C),
("NUMERIC_LSR_C", NUMERIC_LSR_C),
("NUMERIC_ASR_C", NUMERIC_ASR_C),
("NUMERIC_ROR_C", NUMERIC_ROR_C),
("align_n2w", align_n2w),
("aligned_n2w", aligned_n2w),
("align_id_248", align_id_248),
("lowest_set_bit_compute", lowest_set_bit_compute),
("ITAdvance_n2w", ITAdvance_n2w),
("RName_EQ_RName", theorem "RName_EQ_RName"),
("RName2num_thm", theorem "RName2num_thm"),
("num2RName_thm", theorem "num2RName_thm"),
("PSRName_EQ_PSRName", theorem "PSRName_EQ_PSRName"),
("PSRName2num_thm", theorem "PSRName2num_thm"),
("num2PSRName_thm", theorem "num2PSRName_thm"),
("ARMarch_EQ_ARMarch", theorem "ARMarch_EQ_ARMarch"),
("ARMarch2num_thm", theorem "ARMarch2num_thm"),
("num2ARMarch_thm", theorem "num2ARMarch_thm"),
("SRType_EQ_SRType", theorem "SRType_EQ_SRType"),
("SRType2num_thm", theorem "SRType2num_thm"),
("num2SRType_thm", theorem "num2SRType_thm"),
("InstrSet_EQ_InstrSet", theorem "InstrSet_EQ_InstrSet"),
("InstrSet2num_thm", theorem "InstrSet2num_thm"),
("num2InstrSet_thm", theorem "num2InstrSet_thm"),
("Encoding_EQ_Encoding", theorem "Encoding_EQ_Encoding"),
("Encoding2num_thm", theorem "Encoding2num_thm"),
("num2Encoding_thm", theorem "num2Encoding_thm")];
["pairTheory_UNCURRY",
"pairTheory_LEX_DEF",
"pred_setTheory_IN_CROSS",
"pred_setTheory_IN_DELETE",
"wordsTheory_BIT_UPDATE",
"NOT_IN_EMPTY_SPECIFICATION",
"NUMERIC_LSL_C",
"NUMERIC_LSR_C",
"NUMERIC_ASR_C",
"NUMERIC_ROR_C",
"align_n2w",
"aligned_n2w",
"align_id_248",
"lowest_set_bit_compute",
"ITAdvance_n2w",
"RName_EQ_RName",
"RName2num_thm",
"num2RName_thm",
"PSRName_EQ_PSRName",
"PSRName2num_thm",
"num2PSRName_thm",
"ARMarch_EQ_ARMarch",
"ARMarch2num_thm",
"num2ARMarch_thm",
"SRType_EQ_SRType",
"SRType2num_thm",
"num2SRType_thm",
"InstrSet_EQ_InstrSet",
"InstrSet2num_thm",
"num2InstrSet_thm",
"Encoding_EQ_Encoding",
"Encoding2num_thm",
"num2Encoding_thm"];

(* ------------------------------------------------------------------------ *)

Expand Down
28 changes: 14 additions & 14 deletions examples/ARM/v7/arm_decoderScript.sml
View file
Expand Up @@ -1555,20 +1555,20 @@ val thumb2_decode = save_thm("thumb2_decode",
rule [`arch`,`n2w it`, `n2w m`, `n2w n`] thumb2_decode_def);

val _ = computeLib.add_persistent_funs
[("arm_decode_v4", arm_decode_v4),
("arm_decode_not_v4", arm_decode_not_v4),
("thumb_decode", thumb_decode),
("thumbee_decode", thumbee_decode),
("thumb2_decode_aux1", thumb2_decode_aux1),
("thumb2_decode_aux2", thumb2_decode_aux2),
("thumb2_decode_aux3", thumb2_decode_aux3),
("thumb2_decode_aux4", thumb2_decode_aux4),
("thumb2_decode_aux5", thumb2_decode_aux5),
("thumb2_decode_aux6", thumb2_decode_aux6),
("thumb2_decode_aux7", thumb2_decode_aux7),
("thumb2_decode_aux8", thumb2_decode_aux8),
("thumb2_decode_aux9", thumb2_decode_aux9),
("thumb2_decode", thumb2_decode)];
["arm_decode_v4",
"arm_decode_not_v4",
"thumb_decode",
"thumbee_decode",
"thumb2_decode_aux1",
"thumb2_decode_aux2",
"thumb2_decode_aux3",
"thumb2_decode_aux4",
"thumb2_decode_aux5",
"thumb2_decode_aux6",
"thumb2_decode_aux7",
"thumb2_decode_aux8",
"thumb2_decode_aux9",
"thumb2_decode"];

(* ------------------------------------------------------------------------ *)

Expand Down
2 changes: 1 addition & 1 deletion examples/ARM/v7/arm_opsemScript.sml
View file
Expand Up @@ -3872,7 +3872,7 @@ val instructions =
map (I ## instruction_rule) (!instructions);

val _ = map save_thm instructions;
val _ = computeLib.add_persistent_funs instructions;
val _ = computeLib.add_persistent_funs (map fst instructions);

val instructions = map fst (List.drop (instructions,2));

Expand Down
6 changes: 3 additions & 3 deletions examples/ARM/v7/arm_seq_monadScript.sml
View file
Expand Up @@ -855,8 +855,8 @@ val coproc_get_two_words_def = Define`
constT data)`;

val _ = computeLib.add_persistent_funs
[("have_security_ext", have_security_ext),
("have_thumbEE", have_thumbEE),
("have_jazelle", have_jazelle)];
["have_security_ext",
"have_thumbEE",
"have_jazelle"];

val _ = export_theory ();
2 changes: 1 addition & 1 deletion examples/ARM/v7/arm_stepScript.sml
View file
Expand Up @@ -786,7 +786,7 @@ let val thm = aligned_bx_def |> Q.SPEC `n2w a` |> GEN_ALL in
|> SIMP_RULE (srw_ss()) [bitTheory.BITS_ZERO3, word_extract_n2w]
end);

val _ = computeLib.add_persistent_funs [("aligned_bx_n2w", aligned_bx_n2w)];
val _ = computeLib.add_persistent_funs ["aligned_bx_n2w"];

val aligned_bx_0w = EVAL ``aligned_bx (0w:word32)``;
val aligned_bx_1w = EVAL ``aligned_bx (1w:word32)``;
Expand Down
5 changes: 3 additions & 2 deletions examples/ARM/v7/eval/arm_evalScript.sml
View file
Expand Up @@ -176,9 +176,10 @@ end;

val proc = Q.store_thm("proc", `proc n f (n,x) = f x`, SRW_TAC [] [proc_def]);

val _ = save_thm("combinTheory_o_THM",combinTheory.o_THM)
val _ = computeLib.add_persistent_funs
[("combinTheory.o_THM", combinTheory.o_THM), ("proc", proc),
("register_update", register_update), ("psr_update", psr_update)];
["combinTheory_o_THM", "proc",
"register_update", "psr_update"];

(* ------------------------------------------------------------------------ *)

Expand Down
4 changes: 2 additions & 2 deletions examples/Crypto/AES/MultScript.sml
View file
Expand Up @@ -47,7 +47,7 @@ val ConstMult_def =
then b2 ?? ((b1 >>> 1) ** xtime b2)
else ((b1 >>> 1) ** xtime b2)`;

val _ = computeLib.add_persistent_funs [("ConstMult_def",ConstMult_def)];
val _ = computeLib.add_persistent_funs ["ConstMult_def"];

val ConstMultDistrib = Q.store_thm
("ConstMultDistrib",
Expand All @@ -68,7 +68,7 @@ val IterConstMult_def =
else IterConstMult (b1 >>> 1, xtime b2,
if word_lsb b1 then (b2 ?? acc) else acc)`;

val _ = computeLib.add_persistent_funs [("IterConstMult_def",IterConstMult_def)];
val _ = computeLib.add_persistent_funs ["IterConstMult_def"];

(*---------------------------------------------------------------------------*)
(* Equivalence between recursive and iterative forms. *)
Expand Down
2 changes: 1 addition & 1 deletion examples/Crypto/AES/aesScript.sml
View file
Expand Up @@ -183,7 +183,7 @@ Defn.tprove

val _ = save_thm ("expand_def", expand_def);
val _ = save_thm ("expand_ind", expand_ind);
val _ = computeLib.add_persistent_funs [("expand_def", expand_def)];
val _ = computeLib.add_persistent_funs ["expand_def"];

val mk_keysched_def = Define
`mk_keysched ((b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11,b12,b13,b14,b15):key)
Expand Down
2 changes: 1 addition & 1 deletion examples/Crypto/AES/tablesScript.sml
View file
Expand Up @@ -86,7 +86,7 @@ val InvSbox = save_thm("InvSbox",
LIST_CONJ (map (REWRITE_CONV [InvSbox_def] THENC EVAL) (for 0 255
(fn i => ``InvSbox (n2w ^(numSyntax.term_of_int i))``))));

val _ = computeLib.add_persistent_funs [("Sbox", Sbox), ("InvSbox", InvSbox)];
val _ = computeLib.add_persistent_funs ["Sbox", "InvSbox"];

val Sbox_Inversion = Q.store_thm
("Sbox_Inversion",
Expand Down
8 changes: 4 additions & 4 deletions examples/Crypto/SHA-1/SHA1Script.sml
View file
Expand Up @@ -236,7 +236,7 @@ val (expand_def, expand_ind) = Defn.tprove

val _ = save_thm("expand_def",expand_def);

val _ = computeLib.add_persistent_funs [("expand_def", expand_def)];
val _ = computeLib.add_persistent_funs ["expand_def"];

(*---------------------------------------------------------------------------*)
(* Digest a block *)
Expand Down Expand Up @@ -308,9 +308,9 @@ val stringMD_def =
(*---------------------------------------------------------------------------*)

val _ = computeLib.add_persistent_funs
[("TAKE_def",TAKE_def),
("pBits_def",pBits_def),
("digest_def",digest_def)];
["TAKE_def",
"pBits_def",
"digest_def"];

val _ = type_pp.pp_num_types := false;
val _ = type_pp.pp_array_types := false;
Expand Down
66 changes: 31 additions & 35 deletions examples/acl2/examples/fmapExample.sml
View file
Expand Up @@ -1211,10 +1211,10 @@ val SOME_EQ_ELIM =
RW_TAC (srw_ss()) []);

val _ = computeLib.add_persistent_funs
[("IS_SOME_if", IS_SOME_if),
("THE_if", THE_if),
("if_SOME", if_SOME),
("SOME_EQ_ELIM", SOME_EQ_ELIM)];
["IS_SOME_if",
"THE_if",
"if_SOME",
"SOME_EQ_ELIM"];

(* Technical theorem to make EVAL work with output from SYMBOLIC_EVAL_PROVE *)
val ScalarOf_if =
Expand Down Expand Up @@ -1251,10 +1251,10 @@ val EqRightIf =
METIS_TAC[]);

val _ = computeLib.add_persistent_funs
[("ScalarOfIf", ScalarOfIf),
("ScalarIf", ScalarIf),
("EqLeftIf", EqLeftIf),
("EqRightIf", EqRightIf)];
["ScalarOfIf",
"ScalarIf",
"EqLeftIf",
"EqRightIf"];

val int_opLeftIf =
store_thm
Expand All @@ -1280,25 +1280,21 @@ val int_relRightIf =
``!(r:int->int->bool). r (if b then x else y) n = if b then r x n else r y n``,
METIS_TAC[]);

val _ =
(map
(fn con =>
(save_thm ((fst(dest_const con) ^ "LeftIf"), SPEC con int_opLeftIf);
save_thm ((fst(dest_const con) ^ "RightIf"), SPEC con int_opRightIf);
computeLib.add_persistent_funs
[((fst(dest_const con) ^ "LeftIf"), SPEC con int_opLeftIf),
((fst(dest_const con) ^ "RightIf"), SPEC con int_opRightIf)]))
[``$int_add``,``$int_sub``]);

val _ =
(map
(fn con =>
(save_thm ((fst(dest_const con) ^ "LeftIf"), SPEC con int_relLeftIf);
save_thm ((fst(dest_const con) ^ "RightIf"), SPEC con int_relRightIf);
computeLib.add_persistent_funs
[((fst(dest_const con) ^ "LeftIf"), SPEC con int_relLeftIf),
((fst(dest_const con) ^ "RightIf"), SPEC con int_relRightIf)]))
[``$int_lt``,``$int_le``,``$int_gt``,``$int_ge``]);
local
fun f thl thr =
(app
(fn con => let
val nl = (fst(dest_const con) ^ "LeftIf")
val nr = (fst(dest_const con) ^ "RightIf")
val _ = save_thm (nl, SPEC con thl)
val _ = save_thm (nr, SPEC con thr)
in computeLib.add_persistent_funs [nl,nr] end))
in
val _ = f int_opLeftIf int_opRightIf
[``$int_add``,``$int_sub``];
val _ = f int_relLeftIf int_relRightIf
[``$int_lt``,``$int_le``,``$int_gt``,``$int_ge``]
end


(* Monad binding operation *)
Expand Down Expand Up @@ -1344,7 +1340,7 @@ val RUN_BIND_RUN_RETURN =
RW_TAC std_ss [RUN_BIND_RUN_RETURN_def,RUN_BIND_def,RUN_RETURN_def]);

(* Add to EVAL compset *)
val _ = computeLib.add_persistent_funs[("CONS_if",CONS_if)];
val _ = computeLib.add_persistent_funs["CONS_if"];

(* Technical theorems to make ML EVAL work with outcomes *)

Expand Down Expand Up @@ -1378,9 +1374,9 @@ val pair_case_if =

(* Add to EVAL compset *)
val _ = computeLib.add_persistent_funs
[("outcome_case_def",outcome_case_def),
("outcome_case_if",outcome_case_if),
("pair_case_if",pair_case_if)
["outcome_case_def",
"outcome_case_if",
"pair_case_if"
];

(*===========================================================================*)
Expand Down Expand Up @@ -1545,7 +1541,7 @@ val RUN =

(* Tell EVAL about RUN and various properties of finite maps *)

val _ = computeLib.add_persistent_funs[("RUN",RUN)];
val _ = computeLib.add_persistent_funs["RUN"];

(*===========================================================================*)
(* Small step next-state function *)
Expand Down Expand Up @@ -1608,7 +1604,7 @@ val STEP1 =
THEN RW_TAC list_ss [STEP1_def]);

(* Add to EVAL compset *)
val _ = computeLib.add_persistent_funs [("STEP1",STEP1)];
val _ = computeLib.add_persistent_funs ["STEP1"];

(* Various lemmas follow -- I'm not sure they are all needed *)
val SMALL_EVAL_IMP_STEP1 =
Expand Down Expand Up @@ -2350,7 +2346,7 @@ val ACC_STEP =
THEN RW_TAC std_ss [ACC_STEP_def,ACC_STEP_BIND_def]);

(* Add to EVAL compset *)
val _ = computeLib.add_persistent_funs [("ACC_STEP",ACC_STEP)];
val _ = computeLib.add_persistent_funs ["ACC_STEP"];

val ACC_STEP_STEP =
store_thm
Expand Down Expand Up @@ -3482,7 +3478,7 @@ val EVAL_FUN =

val _ =
computeLib.add_persistent_funs
[("EVAL_FUN", EVAL_FUN)];
["EVAL_FUN"];


(* ============================================================================
Expand Down
4 changes: 2 additions & 2 deletions examples/dev/AES/curried/MultScript.sml
View file
Expand Up @@ -71,7 +71,7 @@ val (ConstMult_def,ConstMult_ind) =

val _ = save_thm("ConstMult_def",ConstMult_def);
val _ = save_thm("ConstMult_ind",ConstMult_ind);
val _ = computeLib.add_persistent_funs [("ConstMult_def",ConstMult_def)];
val _ = computeLib.add_persistent_funs ["ConstMult_def"];

val ConstMultDistrib = Q.store_thm
("ConstMultDistrib",
Expand Down Expand Up @@ -103,7 +103,7 @@ val (IterConstMult_def,IterConstMult_ind) =

val _ = save_thm("IterConstMult_def",IterConstMult_def);
val _ = save_thm("IterConstMult_ind",IterConstMult_ind);
val _ = computeLib.add_persistent_funs [("IterConstMult_def",IterConstMult_def)];
val _ = computeLib.add_persistent_funs ["IterConstMult_def"];

(*---------------------------------------------------------------------------*)
(* Equivalence between recursive and iterative forms. *)
Expand Down
2 changes: 1 addition & 1 deletion examples/dev/AES/curried/aesScript.sml
View file
Expand Up @@ -172,7 +172,7 @@ Defn.tprove

val _ = save_thm ("expand_def", expand_def);
val _ = save_thm ("expand_ind", expand_ind);
val _ = computeLib.add_persistent_funs [("expand_def", expand_def)];
val _ = computeLib.add_persistent_funs ["expand_def"];

val mk_keysched_def = Define
`mk_keysched ((b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11,b12,b13,b14,b15):key)
Expand Down

0 comments on commit 0fc7587

Please sign in to comment.