Permalink
Browse files

Many compatibility fiddles for ML_code changes.

Lots of adventures in hunting down slight incompatibilities between
the translator and the basis. The basis theories now all build.

In particular:
  - ensure that 'env' objects are abbreviated without being normalised.
    + the definitions of write/write_cons/merge_env etc will eventually be
      added to the global compute set.
  - ensure that auto-names of _v constants are exactly as before.
    + basisFunctionsLib.trans uses part of a _v constant name to guess
      a v_thm name and overwrite the translator thm with a rewritten version.
  - delete chunks of various scripts that reimplement parts of ml_progLib
    e.g. doing ml_progLib.get_state by hand via rator/rator/rand.
  - add some more queries to ml_progLib/ml_translatorLib to delete yet more
    hand interventions from other theories.
  • Loading branch information...
Thomas Sewell
Thomas Sewell committed Jan 3, 2019
1 parent 2898801 commit 9344b77d74e32ff055a85f1a9a098b45492b2489
@@ -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)
@@ -69,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

@@ -140,14 +140,14 @@ val reduce_conv =

fun prove_assum_by_conv conv th = let
val (x,y) = dest_imp (concl th)
val lemma = conv x
val lemma = CONV_RULE ((RATOR_CONV o RAND_CONV) (REWR_CONV lemma)) th
val lemma1 = conv x
val lemma = CONV_RULE ((RATOR_CONV o RAND_CONV) (REWR_CONV lemma1)) th
in MP lemma TRUTH
handle HOL_ERR e => let
val _ = print "Failed to convert:\n\n"
val _ = print_term x
val _ = print "\n\nto T. It only reduced to:\n\n"
val _ = print_term (lemma |> concl |> dest_eq |> snd)
val _ = print_term (lemma1 |> concl |> dest_eq |> snd)
val _ = print "\n\n"
in failwith "prove_assum_by_conv: unable to reduce term to T"
end
@@ -225,7 +225,7 @@ fun cond_let_abbrev cond for_eval name conv op_nm th = let
in if cond andalso is_const f andalso all is_var xs
then (CONV_RULE let_conv th, [])
else let
val def = define_abbrev for_eval (find_name name) tm |> SPEC_ALL
val def = define_abbrev for_eval name tm |> SPEC_ALL
in (CONV_RULE (RAND_CONV (REWR_CONV (GSYM def))
THENC let_conv) th, [def])
end
@@ -324,7 +324,7 @@ fun open_module mn_str = open_block "open_module"
(mk_comment ("Module", mn_str))

fun close_module sig_opt = ML_code_upd "close_module"
ML_code_close_module [let_env_abbrev reduce_conv]
ML_code_close_module [let_env_abbrev ALL_CONV]

val open_local_block = open_block "open_local_block"
(mk_comment ("Local", "local"))
@@ -347,8 +347,7 @@ fun add_Dtype loc tds_tm = ML_code_upd "add_Dtype"
[write_tdefs_def,MAP,FLAT,FOLDR,REVERSE_DEF,
write_conses_def,LENGTH,
semanticPrimitivesTheory.build_constrs_def,
APPEND,namespaceTheory.mk_id_def]
THENC reduce_conv)]
APPEND,namespaceTheory.mk_id_def])]

(*
val loc = unknown_loc
@@ -361,8 +360,7 @@ fun add_Dexn loc n_tm l_tm = ML_code_upd "add_Dexn"
[let_conv_ML_upd EVAL, let_st_abbrev reduce_conv,
let_env_abbrev (SIMP_CONV std_ss [MAP,
FLAT,FOLDR,REVERSE_DEF,
APPEND,namespaceTheory.mk_id_def]
THENC reduce_conv)]
APPEND,namespaceTheory.mk_id_def])]

fun add_Dtabbrev loc l1_tm l2_tm l3_tm = ML_code_upd "add_Dtabbrev"
(SPECL [l1_tm,l2_tm,l3_tm,loc] ML_code_Dtabbrev) []
@@ -375,7 +373,7 @@ fun add_Dlet eval_thm var_str v_thms = let
[solve_ml_imp_mp eval_thm,
solve_ml_imp_conv (SIMP_CONV bool_ss []
THENC SIMP_CONV bool_ss [ML_code_env_def]),
let_env_abbrev reduce_conv, let_st_abbrev reduce_conv]
let_env_abbrev ALL_CONV, let_st_abbrev reduce_conv]
end

(*
@@ -386,7 +384,7 @@ val (n,v,exp) = (v_tm,w,body)
fun add_Dlet_Fun loc n v exp v_name = ML_code_upd "add_Dlet_Fun"
(SPECL [n, v, exp, loc] ML_code_Dlet_Fun)
[let_conv_ML_upd (REWRITE_CONV [ML_code_env_def]),
let_v_abbrev v_name ALL_CONV, let_env_abbrev reduce_conv]
let_v_abbrev v_name ALL_CONV, let_env_abbrev ALL_CONV]

val Recclosure_pat =
semanticPrimitivesTheory.v_nchotomy
@@ -404,7 +402,7 @@ fun add_Dletrec loc funs v_names = let
val xs = zip v_names tms
val v_defs = map (fn (x,y) => define_abbrev false x y) xs
val th = CONV_RULE (RAND_CONV (REWRITE_CONV (map GSYM v_defs))) th
in let_env_abbrev reduce_conv nm
in let_env_abbrev ALL_CONV nm
(th, ML_code (ss,envs,v_defs @ vs,mlth)) end
in ML_code_upd "add_Dletrec"
(SPECL [funs, loc] ML_code_Dletrec)
@@ -491,6 +489,13 @@ fun remove_snocs (ML_code (ss,envs,vs,th)) = let
fun get_thm (ML_code (ss,envs,vs,th)) = th
fun get_v_defs (ML_code (ss,envs,vs,th)) = vs

fun get_prog (ML_code (ss,envs,vs,th)) = case ML_code_blocks (concl th) of
[comm :: st :: prog :: _] => prog
| _ => failwith ("get_prog: couldn't get toplevel declarations")
fun get_Decls_thm code = let
val _ = get_prog code
in MATCH_MP ML_code_Decls (get_thm code) end

val merge_env_tm = prim_mk_const {Name = "merge_env", Thy = "ml_prog"}
val ML_code_env_tm = prim_mk_const {Name = "ML_code_env", Thy = "ml_prog"}

@@ -481,6 +481,12 @@ val ML_code_def = Define `(ML_code env [] res_st <=> T)
res_st <=> (ML_code env bls st
/\ Decls (ML_code_env env bls) st decls res_env res_st))`;

(* retreive the Decls from a toplevel ML_code *)
Theorem ML_code_Decls
`ML_code env1 [(comm, st1, prog, env2)] st2 ==>
Decls env1 st1 prog env2 st2`
(fs [ML_code_def, ML_code_env_def]);

(* an empty program *)
local open primSemEnvTheory in

0 comments on commit 9344b77

Please sign in to comment.