Permalink
Browse files

Merge pull request #595 from CakeML/local

Local blocks in ml_progLib
  • Loading branch information...
xrchz committed Jan 8, 2019
2 parents 371799e + 1e78b6f commit f298b174c42f4722ed5df729fe78cd3d18371471
@@ -4,6 +4,7 @@
open preamble
ml_translatorTheory ml_translatorLib ml_progLib basisFunctionsLib
CommandLineProgTheory MarshallingProgTheory
semanticPrimitivesSyntax

val _ = new_theory"TextIOProg";

@@ -38,14 +39,11 @@ val EndOfFile_exn_def = Define `

val iobuff_e = ``(App Aw8alloc [Lit (IntLit 2052); Lit (Word8 0w)])``
val eval_thm = let
val th = get_ml_prog_state () |> get_thm
val th = MATCH_MP ml_progTheory.ML_code_Dlet_var th
|> REWRITE_RULE [ml_progTheory.ML_code_env_def]
val th = th |> CONV_RULE(RESORT_FORALL_CONV(sort_vars["e","s3"]))
|> SPEC iobuff_e
val st = th |> SPEC_ALL |> concl |> dest_imp |> #1 |> strip_comb |> #2 |> el 1
val env = get_ml_prog_state () |> ml_progLib.get_env
val st = get_ml_prog_state () |> ml_progLib.get_state
val new_st = ``^st with refs := ^st.refs ++ [W8array (REPLICATE 2052 0w)]``
val goal = th |> SPEC new_st |> SPEC_ALL |> concl |> dest_imp |> fst
val goal = list_mk_icomb (prim_mk_const {Thy="ml_prog", Name="eval_rel"},
[st, env, iobuff_e, new_st, mk_var ("x", semanticPrimitivesSyntax.v_ty)])
val lemma = goal |> (EVAL THENC SIMP_CONV(srw_ss())[semanticPrimitivesTheory.state_component_equality])
val v_thm = prove(mk_imp(lemma |> concl |> rand, goal),
rpt strip_tac \\ rveq \\ match_mp_tac(#2(EQ_IMP_RULE lemma))
@@ -11,10 +11,9 @@ open preamble
library instead *)

fun get_module_prefix () = let
val mod_tm = ml_progLib.get_thm (get_ml_prog_state ())
|> concl |> rator |> rator |> rand
in if optionSyntax.is_none mod_tm then "" else
stringSyntax.fromHOLstring (mod_tm |> rand |> rator |> rand) ^ "_"
val mods = ml_progLib.get_open_modules (get_ml_prog_state ())
in case mods of [] => ""
| (m :: ms) => m ^ "_"
end

fun trans ml_name rhs = let
@@ -10,13 +10,10 @@ val _ = translation_extends"PrettyPrinterProg";

val print_e = ``Var(Long"TextIO"(Short"print"))``
val eval_thm = let
val th = get_ml_prog_state () |> get_thm
val th = MATCH_MP ml_progTheory.ML_code_Dlet_var th
|> REWRITE_RULE [ml_progTheory.ML_code_env_def]
val th = th |> CONV_RULE(RESORT_FORALL_CONV(sort_vars["e","s3"]))
|> SPEC print_e
val st = th |> SPEC_ALL |> concl |> dest_imp |> #1 |> strip_comb |> #2 |> el 1
val goal = th |> SPEC st |> SPEC_ALL |> concl |> dest_imp |> fst
val env = get_ml_prog_state () |> ml_progLib.get_env
val state = get_ml_prog_state () |> ml_progLib.get_state
val goal = list_mk_icomb (prim_mk_const {Thy="ml_prog", Name="eval_rel"},
[state, env, print_e, state, mk_var ("x", v_ty)])
val lemma = goal |> (EVAL THENC SIMP_CONV(srw_ss())[])
val v_thm = prove(mk_imp(lemma |> concl |> rand, goal),
rpt strip_tac \\ rveq \\ match_mp_tac(#2(EQ_IMP_RULE lemma))
@@ -78,8 +75,7 @@ val basis_st = get_ml_prog_state ();
val basis_prog_state = save_thm("basis_prog_state",
ml_progLib.pack_ml_prog_state basis_st);

val basis_prog = basis_st |> remove_snocs
|> get_thm |> concl |> rator |> rator |> rator |> rand
val basis_prog = basis_st |> remove_snocs |> ml_progLib.get_prog;

val basis_def = Define `basis = ^basis_prog`;

@@ -119,12 +119,13 @@ fun whole_prog_thm st name spec =
else raise(call_ERR "Conclusion must be a whole_prog_spec or whole_prog_ffidiv_spec")
val th =
whole_prog_spec_thm
|> C MATCH_MP (st |> get_thm |> GEN_ALL |> ISPEC basis_ffi_tm)
|> C MATCH_MP (st |> get_Decls_thm |> GEN_ALL |> ISPEC basis_ffi_tm)
|> SPEC(stringSyntax.fromMLstring name)
|> CONV_RULE(QUANT_CONV(LAND_CONV(LAND_CONV EVAL THENC SIMP_CONV std_ss [])))
|> CONV_RULE(HO_REWR_CONV UNWIND_FORALL_THM1)
|> C HO_MATCH_MP spec
|> SIMP_RULE bool_ss [option_case_def, set_sepTheory.SEP_CLAUSES]
(* TS: what is this doing? why not call remove_snocs? *)
val prog_with_snoc = th |> concl |> find_term listSyntax.is_snoc
val prog_rewrite = EVAL prog_with_snoc
val th = PURE_REWRITE_RULE[prog_rewrite] th
@@ -443,7 +443,7 @@ val whole_prog_ffidiv_spec_def = Define`

Theorem whole_prog_spec_semantics_prog
`∀fname fv.
ML_code env1 (init_state (basis_ffi cl fs)) prog NONE env2 st2 ==>
Decls env1 (init_state (basis_ffi cl fs)) prog env2 st2 ==>
lookup_var fname env2 = SOME fv ==>
whole_prog_spec fv cl fs sprop Q ==>
(?h1 h2. SPLIT (st2heap (basis_proj1, basis_proj2) st2) (h1,h2) /\
@@ -492,7 +492,7 @@ Theorem whole_prog_spec_semantics_prog

Theorem whole_prog_spec_semantics_prog_ffidiv
`∀fname fv.
ML_code env1 (init_state (basis_ffi cl fs)) prog NONE env2 st2 ==>
Decls env1 (init_state (basis_ffi cl fs)) prog env2 st2 ==>
lookup_var fname env2 = SOME fv ==>
whole_prog_ffidiv_spec fv cl fs Q ==>
(?h1 h2. SPLIT (st2heap (basis_proj1, basis_proj2) st2) (h1,h2) /\
@@ -618,8 +618,13 @@ Theorem oracle_parts_div
\\ disj2_tac
\\ CCONTR_TAC \\ fs[] \\ rfs[]);

val _ = translation_extends "TextIOProg";
val st_f = get_ml_prog_state () |> get_state |> strip_comb |> fst;
val st = mk_icomb (st_f, ``basis_ffi cls fs``);
val _ = reset_translation ()

Theorem parts_ok_basis_st
`parts_ok (auto_state_1 (basis_ffi cls fs)).ffi (basis_proj1, basis_proj2)`
`parts_ok (^st).ffi (basis_proj1, basis_proj2)`
(qmatch_goalsub_abbrev_tac`st.ffi`
\\ `st.ffi.oracle = basis_ffi_oracle`
by( simp[Abbr`st`] \\ EVAL_TAC \\ NO_TAC)
@@ -326,8 +326,7 @@ fun define_abbrev_conv name tm = let
in GSYM def |> SPEC_ALL end

val candle_prog_thm =
get_thm (get_ml_prog_state()) (* (get_curr_prog_state ()) *)
|> REWRITE_RULE [ML_code_def]
get_Decls_thm (get_ml_prog_state()) (* (get_curr_prog_state ()) *)
|> CONV_RULE ((RATOR_CONV o RATOR_CONV o RAND_CONV)
(EVAL THENC define_abbrev_conv "candle_code"))
|> CONV_RULE ((RATOR_CONV o RAND_CONV)
@@ -22,14 +22,14 @@ val fname = mk_var("fname",``:string``);
val main_call = mk_main_call fname;

Theorem call_main_thm1
`ML_code env1 st1 prog NONE env2 st2 ==> (* get this from the current ML prog state *)
`Decls env1 st1 prog env2 st2 ==> (* get this from the current ML prog state *)
lookup_var fname env2 = SOME fv ==> (* get this by EVAL *)
app p fv [Conv NONE []] P (POSTv uv. &UNIT_TYPE () uv * Q) ==> (* this should be the CF spec you prove for the "main" function *)
SPLIT (st2heap p st2) (h1,h2) /\ P h1 ==> (* this might need simplification, but some of it may need to stay on the final theorem *)
∃st3.
Decls env1 st1 (SNOC ^main_call prog) env2 st3 /\
(?h3 h4. SPLIT3 (st2heap p st3) (h3,h2,h4) /\ Q h3)`
(rw[ml_progTheory.ML_code_def,SNOC_APPEND,ml_progTheory.Decls_APPEND,PULL_EXISTS]
(rw[SNOC_APPEND,ml_progTheory.Decls_APPEND,PULL_EXISTS]
\\ simp[ml_progTheory.Decls_def]
\\ fs [terminationTheory.evaluate_decs_def,PULL_EXISTS,
EVAL ``(pat_bindings (Pcon NONE []) [])``,pair_case_eq,result_case_eq]
@@ -143,7 +143,7 @@ Theorem FFI_part_hprop_SEP_EXISTS
(rw[FFI_part_hprop_def,SEP_EXISTS_THM] \\ res_tac);

Theorem call_main_thm2
`ML_code env1 st1 prog NONE env2 st2 ==>
`Decls env1 st1 prog env2 st2 ==>
lookup_var fname env2 = SOME fv ==>
app (proj1, proj2) fv [Conv NONE []] P (POSTv uv. &UNIT_TYPE () uv * Q) ==>
FFI_part_hprop Q ==>
@@ -160,7 +160,7 @@ Theorem call_main_thm2
suffices_by metis_tac[prog_to_semantics_prog]
\\ reverse (sg `?st3. Decls env1 st1 (SNOC ^main_call prog) env2 st3 ∧ B st3`)
THEN1 (asm_exists_tac \\ fs [Abbr`C`]
\\ fs [ml_progTheory.ML_code_def,ml_progTheory.Decls_def]
\\ fs [ml_progTheory.Decls_def]
\\ imp_res_tac evaluate_decs_call_FFI_rel_imp \\ fs [])
\\ simp[Abbr`A`,Abbr`B`]
\\ drule (GEN_ALL call_main_thm1)
@@ -169,7 +169,7 @@ Theorem call_main_thm2
\\ asm_exists_tac \\ simp[]);

Theorem call_main_thm2_ffidiv
`ML_code env1 st1 prog NONE env2 st2 ==>
`Decls env1 st1 prog env2 st2 ==>
lookup_var fname env2 = SOME fv ==>
app (proj1, proj2) fv [Conv NONE []] P (POSTf n. λ c b. Q n c b) ==>
SPLIT (st2heap (proj1, proj2) st2) (h1,h2) /\ P h1
@@ -187,7 +187,7 @@ Theorem call_main_thm2_ffidiv
st4.ffi.io_events)
/\ B st4 n c b /\ C st1 st4`
suffices_by metis_tac[prog_SNOC_semantics_prog]
\\ fs[ml_progTheory.ML_code_def]
\\ fs[]
\\ asm_exists_tac \\ fs[app_def,app_basic_def]
\\ first_x_assum drule \\ impl_tac >- simp[]
\\ rpt strip_tac
@@ -44,6 +44,9 @@ val () = ml_progComputeLib.add_env_compset cs
val () = cfComputeLib.add_cf_aux_compset cs
val () = computeLib.extend_compset [
computeLib.Defs [
(* TS: it's quite unclear to me why CF does this, when ml_progScript is so
careful to ensure that these definitions aren't in the compset. I've tried
adjusting it, but it results in far too much work. *)
ml_progTheory.merge_env_def,
ml_progTheory.write_def,
ml_progTheory.write_mod_def,
@@ -364,12 +364,10 @@ misc code to generate the unverified register allocator in SML
open ml_progLib astPP
val ML_code_prog =
val prog =
get_ml_prog_state ()
|> clean_state |> remove_snocs
|> get_thm
val prog = ML_code_prog |> concl |> strip_comb |> #2 |> el 3
|> ml_progLib.get_prog
val _ = enable_astPP()
val _ = trace("pp_avoids_symbol_merges",0)
@@ -34,6 +34,8 @@ fun mk_alist_reprs R_thm conv dest cmp
fun peek_functions_in_rs (AList_Reprs inn_rs)
= Redblackmap.listItems (! (#dict inn_rs)) |> map fst

fun peek_repr (AList_Reprs inn_rs) tm = Redblackmap.peek (! (#dict inn_rs), tm)

(* constructing is_insert thms *)

fun find_key_rec is_last [] = raise Empty
@@ -168,9 +170,6 @@ fun prove_insert R conv dest cmp k x al = let

(* making repr theorems *)

fun is_short_list xs = listSyntax.is_nil xs
orelse total (listSyntax.is_nil o snd o listSyntax.dest_cons) xs = SOME true

fun mk_insert_repr (AList_Reprs rs) prev_repr k_x = let
val (k, x) = pairSyntax.dest_pair k_x
val (R, al) = case strip_comb (concl prev_repr)
@@ -179,56 +178,62 @@ fun mk_insert_repr (AList_Reprs rs) prev_repr k_x = let
val insert = prove_insert R (#conv rs) (#dest rs) (#cmp rs) k x al
in MATCH_MP repr_insert (CONJ prev_repr insert) end

fun dest_alookup_single tm = let
val (f, xs) = strip_comb tm
in if not (length xs = 1 andalso same_const f alookup_tm)
then NONE
else if listSyntax.is_nil (hd xs) then SOME NONE
else case total listSyntax.dest_cons (hd xs) of
SOME (y, ys) => if listSyntax.is_nil ys then SOME (SOME y) else NONE
| NONE => NONE
end

fun mk_repr_step rs tm = let
val (AList_Reprs inn_rs) = rs
val (f, xs) = strip_comb tm
val is_empty = total (optionSyntax.is_none o snd o dest_abs) tm = SOME true
val is_alookup = same_const alookup_tm f
val is_short = is_alookup andalso total (is_short_list o hd) xs = SOME true
val merge_lhs = if same_const option_choice_tm f then [hd xs] else []
val merge_unknown = exists ((fn t => not (same_const t alookup_tm
orelse same_const t option_choice_tm)) o fst o strip_comb) merge_lhs
val merge_alookup_xs = map strip_comb merge_lhs
|> filter (same_const alookup_tm o fst) |> map (hd o snd)
val is_insert = exists (fn xs => not (listSyntax.is_nil xs)
andalso is_short_list xs) merge_alookup_xs
in if is_empty
then MATCH_MP (MATCH_MP repr_empty (#R_thm inn_rs)) (REFL tm)
else if is_short
val is_short = dest_alookup_single tm <> NONE
val is_merge = same_const option_choice_tm f
val is_repr_merge = is_merge andalso (case peek_repr rs (hd xs) of
SOME _ => true | NONE => false)
val (is_insert, insert_tm) = if not is_merge then (false, T)
else case dest_alookup_single (hd xs) of
SOME (SOME t) => (true, t) | _ => (false, T)
in if is_short
then MATCH_MP (ISPEC (hd xs) alist_repr_refl) (#R_thm inn_rs)
|> prove_assum_by_conv (SIMP_CONV list_ss [sortingTheory.SORTED_DEF])
else if is_insert
then mk_insert_repr rs (mk_repr rs (rand tm))
(fst (listSyntax.dest_cons (hd merge_alookup_xs)))
else if merge_unknown
then mk_insert_repr rs (mk_repr rs (rand tm)) insert_tm
else if is_repr_merge
then let
val l_repr_thm = mk_repr rs (hd xs)
val l_repr_al = rand (rator (concl l_repr_thm))
val look = mk_icomb (alookup_tm, l_repr_al)
val half_repr = list_mk_icomb (option_choice_tm, [look, List.last xs])
val next_repr = mk_repr rs half_repr
in MATCH_MP alist_repr_choice_trans_left (CONJ l_repr_thm next_repr) end
else if not (null merge_lhs) orelse is_alookup
then CHANGED_CONV (SIMP_CONV bool_ss [alookup_to_option_choice,
option_choice_f_assoc, alookup_empty_option_choice_f]) tm
else raise err "mk_repr_step" ("no step for: " ^ Parse.term_to_string f)
else CHANGED_CONV (SIMP_CONV bool_ss [alookup_to_option_choice,
option_choice_f_assoc, alookup_empty_option_choice_f,
count_append_def, alookup_append_option_choice_f,
empty_is_ALOOKUP]) tm
handle HOL_ERR _ => raise err "mk_repr_step"
("no progress from SIMP_CONV: " ^ Parse.term_to_string tm)
end
and mk_repr_known_step (AList_Reprs inn_rs) tm =
case Redblackmap.peek (! (#dict inn_rs), tm) of
and mk_repr_known_step rs tm =
case peek_repr rs tm of
SOME thm => thm
| NONE => mk_repr_step (AList_Reprs inn_rs) tm
| NONE => mk_repr_step rs tm
and mk_repr rs tm = let
val thm = mk_repr_known_step rs tm
in if is_eq (concl thm)
then mk_repr_known_step rs (rhs (concl thm))
then mk_repr rs (rhs (concl thm))
|> CONV_RULE (RAND_CONV (REWR_CONV (SYM thm)))
else thm
end

fun add_alist_repr rs thm = let
val AList_Reprs inn_rs = rs
val (f, rhs) = dest_eq (concl thm)
val repr_thm = case Redblackmap.peek (! (#dict inn_rs), rhs) of
val repr_thm = case peek_repr rs rhs of
SOME rhs_thm => if is_eq (concl rhs_thm)
then TRANS thm rhs_thm
else thm
@@ -325,7 +330,7 @@ fun repr_prove_lookup conv dest cmp repr_thm k = let
fun reprs_conv rs tm = let
val AList_Reprs inn_rs = rs
val (f, x) = dest_comb tm handle HOL_ERR _ => raise UNCHANGED
val repr_thm = case Redblackmap.peek (! (#dict inn_rs), f) of
val repr_thm = case peek_repr rs f of
NONE => raise UNCHANGED | SOME thm => thm
in if is_eq (concl repr_thm)
then (RATOR_CONV (REWR_CONV repr_thm) THENC reprs_conv rs) tm
@@ -207,10 +207,9 @@ Theorem option_choice_f_assoc
(fs [option_choice_f_def, FUN_EQ_THM]
\\ Cases_on `f x` \\ fs []);

Theorem repr_empty
`irreflexive R /\ transitive R ==>
(f = (\x. NONE)) ==> sorted_alist_repr R [] f`
(fs [FUN_EQ_THM, sorted_alist_repr_def]);
Theorem empty_is_ALOOKUP
`(\x. NONE) = ALOOKUP []`
(fs [FUN_EQ_THM]);

Theorem repr_insert
`sorted_alist_repr R al f /\ is_insert fl fr R k x al al' ==>
@@ -875,7 +875,9 @@ Theorem is_clock_io_mono_set_clock
\\ rpt (FIRST (map CHANGED_TAC [fs [], strip_tac]))
\\ metis_tac []);

val evaluate_set_clock_lemmas = BODY_CONJUNCTS is_clock_io_mono_evaluate
val evaluate_set_clock_lemmas
= (BODY_CONJUNCTS is_clock_io_mono_evaluate
@ BODY_CONJUNCTS is_clock_io_mono_evaluate_decs)
|> map (BETA_RULE o MATCH_MP is_clock_io_mono_set_clock);

Theorem evaluate_set_clock
@@ -886,6 +888,14 @@ Theorem evaluate_set_clock
(s1 with clock := ck,res)`
(metis_tac evaluate_set_clock_lemmas);

Theorem evaluate_decs_set_clock
`!s env decs s1 res.
evaluate_decs s env decs = (s1,res) /\
res <> Rerr (Rabort Rtimeout_error) ==>
!ck. ?ck1. evaluate_decs (s with clock := ck1) env decs =
(s1 with clock := ck,res)`
(metis_tac evaluate_set_clock_lemmas);

Theorem is_clock_io_mono_minimal
`is_clock_io_mono f s
==> f s = (s', r) /\ s'.clock = 0 /\ r <> Rerr (Rabort Rtimeout_error)
@@ -16,6 +16,17 @@ sig
val close_module : term option (* optional signature *) ->
ml_prog_state -> ml_prog_state

(* names of (nested) opened modules, outermost first *)
val get_open_modules : ml_prog_state -> string list

(* use of local/in/end blocks, by calling these three functions in order *)
val open_local_block : ml_prog_state -> ml_prog_state
val open_local_in_block : ml_prog_state -> ml_prog_state
val close_local_block : ml_prog_state -> ml_prog_state

(* close all local blocks up to the module/global scope *)
val close_local_blocks : ml_prog_state -> ml_prog_state

val add_Dtype : term (* loc *) -> term (* tds *) ->
ml_prog_state -> ml_prog_state

@@ -48,6 +59,7 @@ sig
ml_prog_state -> ml_prog_state

val nsLookup_conv : conv
val nsLookup_pf_conv : conv

val remove_snocs : ml_prog_state -> ml_prog_state
val clean_state : ml_prog_state -> ml_prog_state
@@ -57,6 +69,9 @@ sig
val get_state : ml_prog_state -> term (* state in ML_code thm *)
val get_v_defs : ml_prog_state -> thm list (* v abbrev defs *)

val get_Decls_thm : ml_prog_state -> thm (* Decls thm at top level *)
val get_prog : ml_prog_state -> term (* program at top level *)

val get_next_exn_stamp : ml_prog_state -> int
val get_next_type_stamp : ml_prog_state -> int

Oops, something went wrong.

0 comments on commit f298b17

Please sign in to comment.