From 36c4a437a0faa029a40f15d320609f71770c7e6a Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sun, 18 Feb 2024 16:10:05 +1100 Subject: [PATCH] clib+crefine+asmrefine: Simpl update Signed-off-by: Gerwin Klein --- lib/clib/SimplRewrite.thy | 6 +++--- proof/crefine/lib/ctac-method.ML | 4 ++-- tools/asmrefine/GraphRefine.thy | 2 +- tools/asmrefine/SimplExport.thy | 12 ++++++------ 4 files changed, 12 insertions(+), 12 deletions(-) diff --git a/lib/clib/SimplRewrite.thy b/lib/clib/SimplRewrite.thy index 952c8a1116..92e0df1a90 100644 --- a/lib/clib/SimplRewrite.thy +++ b/lib/clib/SimplRewrite.thy @@ -246,7 +246,7 @@ lemma com_initial_guards_extra_simps[simp]: "com_initial_guards (cbreak exn_upd) = UNIV" "com_initial_guards (ccatchbrk exn) = UNIV" by (simp_all add: whileAnno_def creturn_def creturn_void_def - call_def block_def cbreak_def ccatchbrk_def) + call_def block_def block_exn_def cbreak_def ccatchbrk_def) lemmas com_initial_guards_all_simps = com_initial_guards.simps com_initial_guards_extra_simps @@ -274,7 +274,7 @@ lemma com_final_guards_extra_simps[simp]: "com_final_guards S (cbreak exn_upd) = UNIV" "com_final_guards S (ccatchbrk exn) = UNIV" by (simp_all add: whileAnno_def creturn_def creturn_void_def - call_def block_def cbreak_def ccatchbrk_def) + call_def block_def block_exn_def cbreak_def ccatchbrk_def) lemmas com_final_guards_all_simps = com_final_guards.simps com_final_guards_extra_simps @@ -501,7 +501,7 @@ lemma exec_statefn_simulates_call: \s t. f (ret1 s t) = ret2 (f s) (f t); \s t. exec_statefn_simulates f UNIV T (save1 s t) (save2 (f s) (f t)) \ \ exec_statefn_simulates f S T (call init1 c ret1 save1) (call init2 c ret2 save2)" - apply (simp add: call_def block_def) + apply (simp add: call_def block_def block_exn_def) apply (intro exec_statefn_simulates_Seq exec_statefn_simulates_Catch exec_statefn_simulates_DynCom exec_statefn_simulates_Basic exec_statefn_simulates_Call diff --git a/proof/crefine/lib/ctac-method.ML b/proof/crefine/lib/ctac-method.ML index eca4ad1ab4..f2c65eee11 100644 --- a/proof/crefine/lib/ctac-method.ML +++ b/proof/crefine/lib/ctac-method.ML @@ -425,8 +425,8 @@ fun ceqv_restore_args_tac ctxt = SUBGOAL (fn (t, n) => case val proc = dest_Const i |> fst |> Long_Name.base_name val pinfo = Hoare.get_data ctxt |> #proc_info val params = Symtab.lookup pinfo proc |> the |> #params - |> filter (fn (v, _) => v = HoarePackage.In) - val new_upds = map (snd #> suffix Record.updateN #> Syntax.read_term ctxt + |> filter (fn (v, _, _) => v = HoarePackage.In) + val new_upds = map (#2 #> suffix Record.updateN #> Syntax.read_term ctxt #> dest_Const #> fst) params |> filter_out (member (op =) cnames) diff --git a/tools/asmrefine/GraphRefine.thy b/tools/asmrefine/GraphRefine.thy index f0da597f8b..e0907659fc 100644 --- a/tools/asmrefine/GraphRefine.thy +++ b/tools/asmrefine/GraphRefine.thy @@ -1126,7 +1126,7 @@ lemma simpl_to_graph_call_next_step: (add_cont (call initf proc ret (\x y. com.Basic (f' x y))) con) n tS P I eqs out_eqs" apply (rule simpl_to_graph_name_simpl_state) - apply (clarsimp simp: call_def block_def graph) + apply (clarsimp simp: call_def block_def block_exn_def graph) apply (rule_tac i=0 and j=3 and P'="{initf sst}" and inp_eqs'="\gst _. eqs gst sst \ sst \ I" in simpl_to_graph_step_general) apply (simp add: init[THEN eq_implD] numeral_3_eq_3 eq_OO) diff --git a/tools/asmrefine/SimplExport.thy b/tools/asmrefine/SimplExport.thy index 819acec43e..d75921d8b9 100644 --- a/tools/asmrefine/SimplExport.thy +++ b/tools/asmrefine/SimplExport.thy @@ -889,7 +889,7 @@ fun has_reads_globals (params : export_params) body = exists_Const (fn (s, T) => fun get_reads_calls ctxt params globals name = let val thm = Proof_Context.get_thm ctxt (name ^ "_body_def") - |> simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms call_def block_def}) + |> simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms call_def block_def block_exn_def}) fun calls (Const (@{const_name com.Call}, _) $ proc) = [proc] | calls (f $ x) = calls f @ calls x | calls (Abs (_, _, t)) = calls t @@ -1023,10 +1023,10 @@ fun emit_body ctxt outfile params (Const (@{const_name Seq}, _) $ a $ b) n c e = val proc_info = Hoare.get_data ctxt |> #proc_info val ret_vals = Symtab.lookup proc_info (Long_Name.base_name p) |> the |> #params - |> filter (fn (v, _) => v = HoarePackage.Out) - |> maps (snd #> read_const ctxt (#pfx params) + |> filter (fn (v, _, _) => v = HoarePackage.Out) + |> maps (#2 #> read_const ctxt (#pfx params) #> synthetic_updates ctxt params "rv#space#") - |> map fst + |> map #1 val p_short = unsuffix "_'proc" (Long_Name.base_name p) val no_read = mk_safe is_no_read_globals ctxt params p_short @@ -1069,10 +1069,10 @@ fun emit_body ctxt outfile params (Const (@{const_name Seq}, _) $ a $ b) n c e = fun emit_func_body ctxt outfile eparams name = let val proc_info = Hoare.get_data ctxt |> #proc_info val params = Symtab.lookup proc_info (name ^ "_'proc") - |> the |> #params + |> the |> #params |> map (fn (a, b, _) => (a, b)) |> map (apsnd (read_const ctxt (#pfx eparams) #> synthetic_updates ctxt eparams "" - #> map fst)) + #> map #1)) val no_read = mk_safe is_no_read_globals ctxt eparams name val no_write = mk_safe (K o is_no_write) ctxt eparams name