Fix costLib

CakeML · May 20, 2021 · 799b7eb · 799b7eb
1 parent ef53531
commit 799b7eb
Showing 1 changed file with 12 additions and 6 deletions.
diff --git a/examples/cost/costLib.sml b/examples/cost/costLib.sml
@@ -97,12 +97,18 @@ fun mk_frame_lookup frame_tm frame_def = EVERY_lookup
   |> CONV_RULE (RAND_CONV EVAL)
   |> SIMP_RULE (srw_ss()) []
 
+val locals_fupd_pat = let
+  val locals_fupd =
+    TypeBase.updates_of ``:('a,'ffi) dataSem$state``
+    |> hd |> SPEC_ALL |> concl |> rator |> rand |> rator |> rator;
+  in ``^locals_fupd _ _`` end
+
 (* remove makespace bindings *)
 val strip_makespace =
   qmatch_goalsub_abbrev_tac `bind _ rest_mkspc _`
   \\ REWRITE_TAC [ bind_def, makespace_def, add_space_def]
   \\ eval_goalsub_tac ``dataSem$cut_env _ _`` \\ simp []
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac locals_fupd_pat
   \\ Q.UNABBREV_TAC `rest_mkspc`
 
 fun mk_strip_assign code_lookup frame_lookup =
@@ -135,7 +141,7 @@ fun mk_strip_assign code_lookup frame_lookup =
         val simps = map (PATH_CONV "lr" EVAL) terms
       in ONCE_REWRITE_TAC simps (asm,goal) end)
   \\ simp [frame_lookup]
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac locals_fupd_pat
   \\ Q.UNABBREV_TAC `rest_ass`
 
 fun mk_open_tailcall code_lookup frame_lookup =
@@ -152,7 +158,7 @@ fun mk_open_tailcall code_lookup frame_lookup =
                  , to_shallow_thm , to_shallow_def
                  , flush_state_def ]
   \\ simp []
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac locals_fupd_pat
 
 val close_tailcall =
   ho_match_mp_tac data_safe_res
@@ -177,10 +183,10 @@ fun mk_open_call code_lookup frame_lookup =
                      \\ EVAL_TAC)
   \\ REWRITE_TAC [ push_env_def   , to_shallow_def
                  , to_shallow_thm , flush_state_def]
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac locals_fupd_pat
 
 val close_call =
-  qmatch_goalsub_abbrev_tac `f (dataSem$state_locals_fupd _ _)`
+  qmatch_goalsub_abbrev_tac `f (^locals_fupd_pat)`
   \\ qmatch_goalsub_abbrev_tac `f s`
   \\ `data_safe (f s)` suffices_by
      (EVERY_CASE_TAC \\ rw [data_safe_def]
@@ -220,7 +226,7 @@ val make_if =
                  , backend_commonTheory.true_tag_def
                  , backend_commonTheory.false_tag_def]
   \\ simp [pop_env_def]
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac locals_fupd_pat
 
 (* functions for making Call, lookup etc use function names *)