From 64cd17eb616d68a37179855402bb3ff8806d661b Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Sat, 17 Dec 2022 22:46:43 +0100 Subject: [PATCH] Fix/avoid some breakage --- pancake/README.md | 6 +++--- pancake/proofs/README.md | 4 ++-- pancake/proofs/crep_to_loopProofScript.sml | 12 ++++++++---- pancake/proofs/loop_liveProofScript.sml | 4 ++++ pancake/proofs/loop_to_wordProofScript.sml | 5 +++++ pancake/semantics/pan_commonPropsScript.sml | 14 ++++---------- 6 files changed, 26 insertions(+), 19 deletions(-) diff --git a/pancake/README.md b/pancake/README.md index 80e278904b..4b4389534c 100644 --- 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 index 4451290862..21411b13e3 100644 --- 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 index 7c2cf9ca45..0da3316552 100644 --- 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 index f3e9aa688e..8b555588da 100644 --- 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 index 6ad3a2cd52..372c9ea21f 100644 --- 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 index df6cec3d9c..006f60bee9 100644 --- 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: