Fix/avoid some breakage

CakeML · Dec 17, 2022 · 64cd17e · 64cd17e
1 parent b1e4ecf
commit 64cd17e
Show file tree

Hide file tree

Showing 6 changed files with 26 additions and 19 deletions.
diff --git a/pancake/README.md b/pancake/README.md
@@ -50,6 +50,9 @@ Compiler from Pancake to machine code
 [pan_to_wordScript.sml](pan_to_wordScript.sml):
 Compiler from pan to word
 
+[parser](parser):
+The Pancake parser.
+
 [proofs](proofs):
 Proofs files for compiling Pancake.
 
@@ -59,9 +62,6 @@ Semantics for Pancake and its intermediate languages.
 [taParserScript.sml](taParserScript.sml):
 Parser for compactDSL programs
 
-[ta_comp_exampleScript.sml](ta_comp_exampleScript.sml):
-This is an example compilation of a TA program
-
 [ta_progs](ta_progs):
 Some sample timed automata (TA) programs.
 

diff --git a/pancake/proofs/README.md b/pancake/proofs/README.md
@@ -24,5 +24,5 @@ Correctness proof for --
 [pan_to_wordProofScript.sml](pan_to_wordProofScript.sml):
 Correctness proof for --
 
-[time_to_panProofScript.sml](time_to_panProofScript.sml):
-Correctness proof for timeLang to panLang
+[time](time):
+Proof files for compiling TimeLang.
diff --git a/pancake/proofs/crep_to_loopProofScript.sml b/pancake/proofs/crep_to_loopProofScript.sml
@@ -16,6 +16,10 @@ val _ = set_grammar_ancestry
          "loopProps", "pan_commonProps",
          "loop_liveProof", "crep_to_loop"];
 
+val _ = temp_delsimps ["fromAList_def", "domain_union",
+                       "domain_inter", "domain_difference",
+                       "domain_map", "sptree.map_def", "sptree.lookup_rwts",
+                       "sptree.insert_notEmpty", "sptree.isEmpty_union"];
 
 Theorem evaluate_nested_seq_append_first =
 evaluate_nested_seq_cases |> CONJUNCT1
@@ -2778,7 +2782,7 @@ val tail_case_tac =
    ‘st.clock = 0’ by fs [state_rel_def] >>
    fs [] >> strip_tac >> rveq >> fs [] >>
    fs [crepSemTheory.empty_locals_def] >>
-   fs [state_rel_def]
+   fs [state_rel_def];
 
 val timed_out_before_call_tac =
    drule code_rel_intro >>
@@ -2861,7 +2865,7 @@ val timed_out_before_call_tac =
    ‘st.clock = 0’ by fs [state_rel_def] >>
    fs [] >> strip_tac >> rveq >> fs [] >>
    fs [crepSemTheory.empty_locals_def] >>
-   fs [state_rel_def]
+   fs [state_rel_def];
 
 
 val fcalled_timed_out_tac =
@@ -2970,7 +2974,7 @@ val fcalled_timed_out_tac =
     first_x_assum (qspec_then ‘ad’ assume_tac) >>
     TRY (cases_on ‘v’) >>
     rfs [wlab_wloc_def]) >>
-   fs [code_rel_def, ctxt_fc_def]
+   fs [code_rel_def, ctxt_fc_def];
 
 
 val fcalled_ffi_case_tac =
@@ -3074,7 +3078,7 @@ val fcalled_ffi_case_tac =
    first_x_assum (qspec_then ‘ad’ assume_tac) >>
    TRY (cases_on ‘v’) >>
    rfs [wlab_wloc_def]) >>
-  fs [code_rel_def, ctxt_fc_def]
+  fs [code_rel_def, ctxt_fc_def];
 
 
 Theorem compile_Call:

diff --git a/pancake/proofs/loop_liveProofScript.sml b/pancake/proofs/loop_liveProofScript.sml
@@ -10,6 +10,10 @@ local open wordSemTheory in end
 
 val _ = new_theory "loop_liveProof";
 
+val _ = temp_delsimps ["fromAList_def", "domain_union",
+                       "domain_inter", "domain_difference",
+                       "domain_map", "sptree.map_def", "sptree.lookup_rwts",
+                       "sptree.insert_notEmpty", "sptree.isEmpty_union"];
 
 val goal =
   “λ(prog, s). ∀res s1 p l0 locals prog1 l1.

diff --git a/pancake/proofs/loop_to_wordProofScript.sml b/pancake/proofs/loop_to_wordProofScript.sml
@@ -12,6 +12,11 @@ val _ = new_theory "loop_to_wordProof";
 
 val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"];
 
+val _ = temp_delsimps ["fromAList_def", "domain_union",
+                       "domain_inter", "domain_difference",
+                       "domain_map", "sptree.map_def", "sptree.lookup_rwts",
+                       "sptree.insert_notEmpty", "sptree.isEmpty_union"];
+
 Definition locals_rel_def:
   locals_rel ctxt l1 l2 ⇔
     INJ (find_var ctxt) (domain ctxt) UNIV ∧

diff --git a/pancake/semantics/pan_commonPropsScript.sml b/pancake/semantics/pan_commonPropsScript.sml
@@ -736,16 +736,10 @@ Theorem lookup_some_el:
   ∀xs n x. lookup n (fromAList xs) = SOME x ==>
    ∃m. m < LENGTH xs ∧ EL m xs = (n,x)
 Proof
-  Induct >> rw []
-  >- fs [fromAList_def, lookup_def] >>
-  cases_on ‘h’ >> fs [] >>
-  fs [fromAList_def] >>
-  fs [lookup_insert] >>
-  every_case_tac >> fs [] >> rveq >> gs []
-  >- (
-  qexists_tac ‘0’ >> fs []) >>
-  res_tac >> fs [] >> rveq >> gs [] >>
-  qexists_tac ‘SUC m’ >> fs []
+  rw [lookup_fromAList]
+  \\ imp_res_tac ALOOKUP_MEM
+  \\ gvs [MEM_EL]
+  \\ first_x_assum $ irule_at Any \\ fs []
 QED
 
 Theorem max_foldr_lt: