Permalink
Browse files

Fix manual eval_rel proof in monad translator.

Fix another instance where an 'eval_rel' goal is constructed by
repeat manipulation of an ML_code thm (whose form has changed)
rather than just fetching the state and env component.

The monad translator seems to be working now.
  • Loading branch information...
Thomas Sewell
Thomas Sewell committed Jan 4, 2019
1 parent 9344b77 commit 1e78b6f2c23f0458b33ff988bcbdfca5a06f24b6
Showing with 7 additions and 5 deletions.
  1. +7 −5 translator/monadic/ml_monadStoreLib.sml
@@ -14,11 +14,13 @@ open ml_monadBaseTheory ml_monad_translatorBaseTheory ml_monad_translatorTheory
open Redblackmap AC_Sort Satisfy
open ml_translatorLib

(* COPY/PASTE from basisFunctionsLib *)
(* COPY/PASTE from other manual eval_rel proofs *)
fun derive_eval_thm for_eval v_name e = let
val th = get_ml_prog_state () |> get_thm
val th = MATCH_MP ml_progTheory.ML_code_Dlet_var th
val goal = th |> SPEC e |> SPEC_ALL |> concl |> dest_imp |> fst
val env = get_ml_prog_state () |> get_env
val st = get_ml_prog_state () |> get_state
val st2 = mk_var ("st2", type_of st)
val goal = list_mk_icomb (prim_mk_const {Thy="ml_prog", Name="eval_rel"},
[st, env, e, st2, mk_var ("x", semanticPrimitivesSyntax.v_ty)])
val lemma = goal
|> (NCONV 50 (SIMP_CONV (srw_ss()) [evaluate_def,ml_progTheory.eval_rel_alt,
PULL_EXISTS,do_app_def,store_alloc_def,LET_THM]) THENC EVAL)
@@ -34,7 +36,7 @@ fun derive_eval_thm for_eval v_name e = let
val v_tm = v_thm |> concl |> rand
val v_def = define_abbrev for_eval v_name v_tm
in v_thm |> REWRITE_RULE [GSYM v_def] end
(* end of COPY/PASTE from basisFunctionsLib *)
(* end of COPY/PASTE *)

fun ERR fname msg = mk_HOL_ERR "ml_monadStoreLib" fname msg;

0 comments on commit 1e78b6f

Please sign in to comment.