clib+crefine+asmrefine: Simpl update

Signed-off-by: Gerwin Klein <[email protected]>

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:
             \<And>s t. f (ret1 s t) = ret2 (f s) (f t);
             \<And>s t. exec_statefn_simulates f UNIV T (save1 s t) (save2 (f s) (f t)) \<rbrakk>
       \<Longrightarrow> 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

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)
 

tools/asmrefine/GraphRefine.thy

@@ -1126,7 +1126,7 @@ lemma simpl_to_graph_call_next_step:
         (add_cont (call initf proc ret (\<lambda>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'="\<lambda>gst _. eqs gst sst \<and> sst \<in> I" in simpl_to_graph_step_general)
    apply (simp add: init[THEN eq_implD] numeral_3_eq_3 eq_OO)

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