diff --git a/compiler/backend/passes/proofs/state_to_cakeProofScript.sml b/compiler/backend/passes/proofs/state_to_cakeProofScript.sml index e8b3ab67..23817622 100644 --- a/compiler/backend/passes/proofs/state_to_cakeProofScript.sml +++ b/compiler/backend/passes/proofs/state_to_cakeProofScript.sml @@ -637,7 +637,7 @@ Inductive dstep_rel: (step_rel (seve, SOME sst, sk) (Estep (cenv,dst.refs,dst.fp_state,ceve,ck)) ∧ ¬is_halt (seve, SOME sst, sk) ⇒ dstep_rel (seve, SOME sst, sk) - (Dstep dst (ExpVal cenv ceve ck locs (Pvar "prog")) [CdlocalG lenv genv []])) ∧ + (Dstep dst (ExpVal cenv ceve ck locs (Pvar "prog")) [CdlocalG lenv genv (final_gc flag)])) ∧ dstep_rel (Val sv, SOME sst, []) Ddone ∧ @@ -648,7 +648,7 @@ Inductive dstep_rel: (Effi ch ws1 ws2 0 cenv' dst.refs ck) ⇒ dstep_rel (Action ch conf, SOME sst, sk) (Dffi dst (ch,ws1,ws2,0,cenv',ck) - locs (Pvar "prog") [CdlocalG lenv genv []])) + locs (Pvar "prog") [CdlocalG lenv genv (final_gc flag)])) End Inductive next_res_rel: @@ -2290,37 +2290,44 @@ Theorem dstep1_rel: ⇒ dget_ffi_array d = SOME ws Proof reverse $ rw[Once dstep_rel_cases] >> gvs[] - >- simp[dstep_rel_cases, sstep, SF SFY_ss] - >- simp[dstep_rel_cases, sstep, SF SFY_ss] - >- simp[dstep_rel_cases, sstep, SF SFY_ss] >> + >- (simp[dstep_rel_cases, sstep, SF SFY_ss] >> irule_at Any EQ_REFL) + >- (simp[dstep_rel_cases, sstep, SF SFY_ss] >> irule_at Any EQ_REFL) + >- (simp[dstep_rel_cases, sstep, SF SFY_ss] >> irule_at Any EQ_REFL) >> drule step1_rel >> simp[] >> strip_tac >> gvs[] >> `cstep_n (SUC n) (Estep (cenv,dst.refs,dst.fp_state,ceve,ck)) ≠ Edone` by ( CCONTR_TAC >> gvs[step_rel_cases]) >> qrefine `m + n` >> simp[SUC_ADD_SYM, itree_semanticsPropsTheory.step_n_add] >> drule $ SRULE [] cstep_n_to_dstep_n >> disch_then $ qspecl_then - [`benv`,`locs`,`Pvar "prog"`,`[CdlocalG lenv genv []]`] assume_tac >> gvs[] >> - pop_assum kall_tac >> + [`benv`,`locs`,`Pvar "prog"`,`[CdlocalG lenv genv (final_gc flag)]`] assume_tac >> + gvs[] >> pop_assum kall_tac >> reverse $ Cases_on `cstep_n (SUC n) (Estep (cenv,dst.refs,dst.fp_state,ceve,ck))` >> gvs[] >- fs[Once step_rel_cases] >- ( qpat_x_assum `step_rel _ _` mp_tac >> - simp[step_rel_cases, dstep_rel_cases] >> strip_tac >> gvs[SF SFY_ss] + simp[step_rel_cases, dstep_rel_cases] >> strip_tac >> gvs[SF SFY_ss] >> + irule_at Any EQ_REFL ) >> PairCases_on `p` >> gvs[] >> drule $ iffLR step_rel_cases >> simp[] >> strip_tac >> gvs[] - >- (qexists0 >> simp[dstep, dstep_rel_cases]) + >- (qexists0 >> simp[dstep, dstep_rel_cases] >> irule_at Any EQ_REFL) >- ( reverse $ Cases_on `sk'` >> gvs[] - >- (qexists0 >> simp[dstep, dstep_rel_cases]) >> + >- (qexists0 >> simp[dstep, dstep_rel_cases] >> irule_at Any EQ_REFL) >> gvs[Once cont_rel_cases] >> qrefine `SUC m` >> simp[dstep] >> simp[astTheory.pat_bindings_def, pmatch_def] >> + reverse $ rw[final_gc_def] + >- (ntac 2 (qrefine `SUC m` >> simp[dstep]) >> simp[dstep_rel_cases]) >> + ntac 2 (qrefine `SUC m` >> simp[dstep]) >> + simp[dstep, astTheory.pat_bindings_def, smallStepTheory.collapse_env_def] >> + ntac 6 (qrefine `SUC m` >> simp[cstep, dstep, do_app_def]) >> + simp[astTheory.pat_bindings_def, pmatch_def] >> ntac 2 (qrefine `SUC m` >> simp[dstep]) >> simp[dstep_rel_cases] ) >- ( reverse $ Cases_on `sk'` >> gvs[] - >- (qexists0 >> simp[dstep, dstep_rel_cases]) >> + >- (qexists0 >> simp[dstep, dstep_rel_cases] >> irule_at Any EQ_REFL) >> gvs[Once cont_rel_cases] >> qrefine `SUC m` >> simp[dstep, dstep_rel_cases, SF SFY_ss] ) @@ -2338,9 +2345,9 @@ Proof qrefine `SUC (m + k)` >> simp[SUC_ADD_SYM] >> once_rewrite_tac[ADD_COMM] >> simp[itree_semanticsPropsTheory.step_n_add] >> drule $ iffLR dstep_rel_cases >> reverse strip_tac >> gvs[step_n_alt] - >- simp[dstep_rel_cases, sstep, SF SFY_ss] - >- simp[dstep_rel_cases, sstep, SF SFY_ss] - >- simp[dstep_rel_cases, sstep, SF SFY_ss] >> + >- (simp[dstep_rel_cases, sstep, SF SFY_ss] >> irule_at Any EQ_REFL) + >- (simp[dstep_rel_cases, sstep, SF SFY_ss] >> irule_at Any EQ_REFL) + >- (simp[dstep_rel_cases, sstep, SF SFY_ss] >> irule_at Any EQ_REFL) >> drule dstep1_rel >> disch_then $ qspec_then `benv` mp_tac >> impl_tac >- (rw[] >> last_x_assum $ qspec_then `n' + n` mp_tac >> simp[step_n_add]) >> strip_tac >> gvs[] >> goal_assum drule >> simp[] @@ -2446,12 +2453,17 @@ Proof >- ( qrefine `SUC m` >> simp[dstep] >> simp[astTheory.pat_bindings_def, pmatch_def] >> - ntac 2 (qrefine `SUC m` >> simp[dstep]) >> - simp[dstep_rel_cases] >> gvs[Once cont_rel_cases] + reverse $ rw[final_gc_def] >> ntac 2 (qrefine `SUC m` >> simp[dstep]) >> + simp[dstep_rel_cases] >> gvs[Once cont_rel_cases] >> + simp[astTheory.pat_bindings_def] >> + ntac 6 (qrefine `SUC m` >> simp[cstep, dstep, do_app_def]) >> + simp[astTheory.pat_bindings_def, pmatch_def] >> + ntac 2 (qrefine `SUC m` >> simp[dstep]) ) >> qexists0 >> simp[dstep, store_lookup_def] >> simp[dstep_rel_cases, step_rel_cases, PULL_EXISTS] >> - goal_assum drule >> gvs[state_rel] >> gvs[Once cont_rel_cases] + irule_at Any EQ_REFL >> goal_assum drule >> gvs[state_rel] >> + qpat_x_assum `cont_rel _ _ _` mp_tac >> rw[Once cont_rel_cases] QED Theorem compile_safe_itree: @@ -2459,74 +2471,17 @@ Theorem compile_safe_itree: dstep_rel (sr,st,sk) (step_n benv n dr) ⇒ safe_itree ffi_convention (interp benv dr) Proof - qsuff_tac - `∀d. - (∃s sr st sk benv n dr. - s = sinterp sr st sk ∧ d = interp benv dr ∧ - safe_itree (sinterp sr st sk) ∧ - dstep_rel (sr,st,sk) (step_n benv n dr) - ) ∨ - (∃out k. d = Ret (FinalFFI out k)) - ⇒ safe_itree ffi_convention d` - >- ( - rw[] >> first_x_assum irule >> disj1_tac >> - rpt $ goal_assum $ drule_at Any >> simp[] - ) >> - ho_match_mp_tac safe_itree_coind >> rw[] >> - `interp benv dr = interp benv (step_n benv n dr)` by simp[interp_take_steps] >> - pop_assum SUBST_ALL_TAC >> qmatch_goalsub_abbrev_tac `interp benv d'` >> - `step_until_halt (sr,st,sk) ≠ Err` by ( - gvs[Once sinterp] >> FULL_CASE_TAC >> gvs[] >> - gvs[Once pure_semanticsTheory.safe_itree_cases]) >> - drule_all step_until_halt_rel >> disch_then $ qspec_then `benv` assume_tac >> - gvs[next_res_rel_cases] - >- (once_rewrite_tac[sinterp, interp] >> simp[]) - >- (once_rewrite_tac[sinterp, interp] >> simp[]) >> - ntac 3 disj2_tac >> simp[Once sinterp, Once interp] >> - drule $ iffLR dstep_rel_cases >> rw[] >> gvs[] >> - drule $ iffLR step_rel_cases >> strip_tac >> gvs[] >> - qmatch_goalsub_abbrev_tac `ExpVal _ _ ffi_exp` >> - `LENGTH ws = max_FFI_return_size + 2` by gvs[state_rel, store_lookup_def] >> - Cases >> rw[Once ffi_convention_def] >> gvs[compile_input_rel_def] >> - disj1_tac >> irule_at Any EQ_REFL >> - qexistsl [`SOME sst`,`Val $ Atom $ Str s`,`sk'`] >> rw[GSYM PULL_EXISTS] + rw[] >> dxrule_all compile_itree_rel >> rename1 `itree_rel a b` >> + qsuff_tac `∀b. (∃a. itree_rel a b) ⇒ safe_itree ffi_convention b` + >- (rw[PULL_EXISTS] >> res_tac) >> + ho_match_mp_tac safe_itree_coind >> rw[] >> gvs[Once itree_rel_cases] >> + rw[ffi_convention_def] >> Cases_on `s` >> gvs[] >- ( - last_x_assum mp_tac >> simp[Once sinterp] >> - simp[Once pure_semanticsTheory.safe_itree_cases] >> - disch_then $ qspec_then `INR s` mp_tac >> simp[Once sinterp] - ) >> - unabbrev_all_tac >> - ntac 7 (qrefine `SUC m` >> simp[dstep, cstep]) >> - simp[namespaceTheory.nsOptBind_def] >> - `nsLookup cenv.v (Short "ffi_array") = SOME (Loc 0)` by gvs[env_ok_def] >> - simp[] >> qrefine `SUC m` >> simp[dstep, cstep, do_app_def] >> - Cases_on `dst.refs` >> gvs[store_lookup_def, LUPDATE_DEF] >> - ntac 9 (qrefine `SUC m` >> simp[dstep, cstep, do_app_def]) >> - simp[store_lookup_def] >> - ntac 21 (qrefine `SUC m` >> simp[dstep, cstep, do_app_def]) >> - simp[opb_lookup_def, opn_lookup_def, do_if_def] >> - `&(256 * (STRLEN s DIV 256) MOD dimword (:8)) + &(STRLEN s MOD dimword (:8)) = - &(STRLEN s) : int` by ( - simp[wordsTheory.dimword_def, wordsTheory.dimindex_8] >> - gvs[max_FFI_return_size_def] >> ARITH_TAC) >> - pop_assum SUBST_ALL_TAC >> simp[] >> - ntac 9 (qrefine `SUC m` >> simp[dstep, cstep, do_app_def]) >> - simp[store_lookup_def, copy_array_def, integerTheory.INT_ADD_CALCULATE] >> - qmatch_goalsub_abbrev_tac `StrLit str1` >> - `str1 = s` by ( - unabbrev_all_tac >> simp[TAKE_APPEND, GSYM MAP_TAKE] >> - simp[ws_to_chars_def, MAP_MAP_o, combinTheory.o_DEF, IMPLODE_EXPLODE_I]) >> - pop_assum SUBST_ALL_TAC >> - Cases_on `ck'` >> gvs[] - >- ( - qrefine `SUC m` >> simp[dstep] >> - simp[astTheory.pat_bindings_def, pmatch_def] >> - ntac 2 (qrefine `SUC m` >> simp[dstep]) >> - simp[dstep_rel_cases] >> gvs[Once cont_rel_cases] - ) >> - qexists0 >> simp[dstep, store_lookup_def] >> - simp[dstep_rel_cases, step_rel_cases, PULL_EXISTS] >> - goal_assum drule >> gvs[state_rel] >> gvs[Once cont_rel_cases] + pop_assum $ qspec_then + `case x of FFI_failed => FFI_failure | _ => FFI_divergence` mp_tac >> + CASE_TAC >> simp[compile_final_ffi_def] >> disch_then $ irule_at Any + ) + >- (first_x_assum $ irule_at Any >> simp[SF SFY_ss]) QED @@ -3597,18 +3552,20 @@ Theorem compile_correct: namespace_init_ok ns ∧ safe_itree (itree_of (exp_of e)) ⇒ itree_rel (itree_of (exp_of e)) - (itree_semantics (compile_with_preamble ns e)) ∧ - safe_itree ffi_convention (itree_semantics (compile_with_preamble ns e)) + (itree_semantics (compile_with_preamble c ns e)) ∧ + safe_itree ffi_convention (itree_semantics (compile_with_preamble c ns e)) Proof simp[itree_of_def, semantics_def, itree_semantics_def, cns_ok_def] >> strip_tac >> irule_at Any compile_itree_rel >> irule_at Any compile_safe_itree >> goal_assum drule >> qrefinel [`n`,`n`] >> simp[] >> simp[dstep_rel_cases, step_rel_cases, PULL_EXISTS] >> + qrefinel [`_`,`_`,`_`,`_`,`c.do_final_gc`] >> simp[Once cont_rel_cases, env_rel_def, state_rel] >> gvs[namespace_init_ok_def] >> simp[compile_with_preamble_def, initial_namespace_def, preamble_def] >> qmatch_goalsub_abbrev_tac `[ffi_array;strle_dec;char_list_dec]` >> - once_rewrite_tac[GSYM APPEND_ASSOC] >> qmatch_goalsub_abbrev_tac `_ ++ prog` >> + ntac 2 $ once_rewrite_tac[GSYM APPEND_ASSOC] >> + qmatch_goalsub_abbrev_tac `compile_namespace _ ++ prog` >> qspecl_then [`ns'`,`start_env`,`start_dstate`,`[]`,`HD prog`,`TL prog`] mp_tac step_over_compile_namespace >> impl_tac @@ -3621,7 +3578,7 @@ Proof PairCases_on `tdef` >> first_x_assum drule >> gvs[] ) >> strip_tac >> gvs[Abbr `prog`] >> - once_rewrite_tac[GSYM APPEND_ASSOC] >> rewrite_tac[APPEND] >> simp[] >> + ntac 2 (once_rewrite_tac[GSYM APPEND_ASSOC] >> rewrite_tac[APPEND]) >> simp[] >> qrefine `m + n` >> simp[itree_semanticsPropsTheory.step_n_add] >> pop_assum kall_tac >> qmatch_goalsub_abbrev_tac `Dstep dst'` >> qpat_abbrev_tac `cml_ns = nsAppend _ _` >> diff --git a/compiler/backend/passes/pure_comp_confScript.sml b/compiler/backend/passes/pure_comp_confScript.sml index 682df5d0..d065f6ef 100644 --- a/compiler/backend/passes/pure_comp_confScript.sml +++ b/compiler/backend/passes/pure_comp_confScript.sml @@ -14,7 +14,8 @@ Datatype: do_mk_delay : bool ; (* thunk-to-thunk smart mk_delay constructor *) do_let_force : bool ; (* thunk-to-thunk simplify let force *) do_split_dlam : bool ; (* thunk-to-thunk split delayed lambdas *) - do_app_unit : bool (* state-to-state *) + do_app_unit : bool ; (* state-to-state *) + do_final_gc : bool ; (* invoke GC at end of CakeML program *) |> End @@ -25,6 +26,7 @@ Overload mk_delay_flag[local] = “strlit "-mk_delay"” Overload let_force_flag[local] = “strlit "-let_force"” Overload dlam_flag[local] = “strlit "-dlam"” Overload unit_flag[local] = “strlit "-unit"” +Overload final_gc_flag[local] = “strlit "-final_gc"” Definition all_flags_def: all_flags = [pure_sort_flag; @@ -33,7 +35,8 @@ Definition all_flags_def: mk_delay_flag; let_force_flag; dlam_flag; - unit_flag] + unit_flag; + final_gc_flag] End Definition read_cline_args_def: @@ -46,7 +49,8 @@ Definition read_cline_args_def: do_mk_delay := ¬ MEM mk_delay_flag cl ; do_let_force := ¬ MEM let_force_flag cl ; do_split_dlam := ¬ MEM dlam_flag cl ; - do_app_unit := ¬ MEM unit_flag cl |> + do_app_unit := ¬ MEM unit_flag cl ; + do_final_gc := MEM final_gc_flag cl |> (* NB final GC only if flag is present *) End val default = EVAL “read_cline_args []” |> concl |> rand |> rand diff --git a/compiler/backend/passes/pure_to_cakeScript.sml b/compiler/backend/passes/pure_to_cakeScript.sml index 1991ccd9..79f4c1fc 100644 --- a/compiler/backend/passes/pure_to_cakeScript.sml +++ b/compiler/backend/passes/pure_to_cakeScript.sml @@ -32,7 +32,7 @@ End Definition pure_to_cake_def: pure_to_cake c ns e = let state_prog = pure_to_state c e in - let cake_prog = compile_with_preamble ((I ## K ns) initial_namespace) state_prog in + let cake_prog = compile_with_preamble c ((I ## K ns) initial_namespace) state_prog in let _ = empty_ffi (strlit "to_cake") in cake_prog End diff --git a/compiler/backend/passes/state_to_cakeScript.sml b/compiler/backend/passes/state_to_cakeScript.sml index 16f12a75..0eb66d33 100644 --- a/compiler/backend/passes/state_to_cakeScript.sml +++ b/compiler/backend/passes/state_to_cakeScript.sml @@ -6,10 +6,11 @@ open stringTheory optionTheory sumTheory pairTheory listTheory alistTheory rich_listTheory arithmeticTheory; open semanticPrimitivesTheory; open pure_miscTheory pure_configTheory pure_typingTheory state_cexpTheory; +open pure_comp_confTheory val _ = new_theory "state_to_cake"; -val _ = set_grammar_ancestry ["pure_typing", "state_cexp", "semanticPrimitives"] +val _ = set_grammar_ancestry ["pure_typing", "state_cexp", "semanticPrimitives", "pure_comp_conf"] (********** Primitives operation implementations **********) @@ -341,10 +342,17 @@ Termination WF_REL_TAC `measure cexp_size` End +Definition final_gc_def: + final_gc flag = + if flag then [Dlet unknown_loc (Pvar "gc") $ (App ConfigGC [int 0; int 0])] else [] +End + (* Remove initial built-in datatypes from ns *) Definition compile_with_preamble_def: - compile_with_preamble ns e = - preamble ((TL ## TL) ns) ++ [Dlet unknown_loc (Pvar "prog") $ compile e] + compile_with_preamble c ns e = + preamble ((TL ## TL) ns) ++ + [Dlet unknown_loc (Pvar "prog") $ compile e] ++ + final_gc c.do_final_gc End diff --git a/compiler/binary/pure_backendProgScript.sml b/compiler/binary/pure_backendProgScript.sml index 28e305d4..b23bbc52 100644 --- a/compiler/binary/pure_backendProgScript.sml +++ b/compiler/binary/pure_backendProgScript.sml @@ -137,6 +137,7 @@ val r = translate state_to_cakeTheory.failure_def; val r = translate state_to_cakeTheory.list_to_exp_def; val r = translate state_to_cakeTheory.cexp_pat_row_def; val r = translate state_to_cakeTheory.compile_def; +val r = translate state_to_cakeTheory.final_gc_def; val r = translate compile_with_preamble_def; (* compositions *)