Fixes for rebind change in HOL

CakeML · Oct 16, 2023 · 1da1b2d · 1da1b2d
1 parent 67dfc72
commit 1da1b2d
Show file tree

Hide file tree

Showing 6 changed files with 12 additions and 12 deletions.
diff --git a/basis/basis_ffiScript.sml b/basis/basis_ffiScript.sml
@@ -422,7 +422,7 @@ Theorem STDIO_precond = Q.prove(`
   rw[STDIO_def,IOFS_precond,SEP_EXISTS_THM,SEP_CLAUSES] >>
   qexists_tac`fs.numchars` >>
   mp_tac (IOFS_precond |> DISCH_ALL |> GEN ``fs : IO_fs``)>>
-  cases_on`fs` >> fs[recordtype_IO_fs_seldef_numchars_fupd_def]) |> UNDISCH_ALL |> curry save_thm "STDIO_precond";
+  cases_on`fs` >> fs[recordtype_IO_fs_seldef_numchars_fupd_def]) |> UNDISCH_ALL;
 
 Theorem RUNTIME_precond:
    RUNTIME {FFI_part (encode ()) (mk_ffi_next runtime_ffi_part)

diff --git a/icing/flover/semantics/CommandsScript.sml b/icing/flover/semantics/CommandsScript.sml
@@ -44,7 +44,7 @@ End
 (**
   Generate a better case lemma
 **)
-Theorem bstep_cases =
+Theorem bstep_cases[allow_rebind] =
   map (GEN_ALL o SIMP_CONV (srw_ss()) [Once bstep_cases])
     [``bstep (Let m x e s) E defVars vR m'``,
      ``bstep (Ret e) E defVars vR m``] |> LIST_CONJ

diff --git a/icing/flover/semantics/ExpressionSemanticsScript.sml b/icing/flover/semantics/ExpressionSemanticsScript.sml
@@ -88,7 +88,7 @@ Theorem eval_expr_cases_old = eval_expr_cases
 (**
   Generate a better case lemma
 **)
-Theorem eval_expr_cases =
+Theorem eval_expr_cases[allow_rebind] =
   map (GEN_ALL o SIMP_CONV (srw_ss()) [Once eval_expr_cases])
     [``eval_expr E Gamma (Var v) res m``,
      ``eval_expr E Gamma (Const m1 n) res m2``,

diff --git a/icing/flover/ssaPrgsScript.sml b/icing/flover/ssaPrgsScript.sml
@@ -42,7 +42,7 @@ End
 (*
   As usual
 *)
-Theorem ssa_cases =
+Theorem ssa_cases[allow_rebind] =
   map (GEN_ALL o SIMP_CONV (srw_ss()) [Once ssa_cases])
     [``ssa (Let m x e s) inVars Vterm``,
      ``ssa (Ret e) inVars Vterm``] |> LIST_CONJ;

diff --git a/translator/ml_translatorLib.sml b/translator/ml_translatorLib.sml
@@ -3927,7 +3927,7 @@ fun reset_translation () =
 fun abbrev_code (fname,ml_fname,def,th,v) = let
   val th = th |> UNDISCH_ALL
   val exp = th |> concl |> rator |> rand
-  val n = Theory.temp_binding ("[[" ^ fname ^ "_code]]")
+  val n = Theory.temp_binding ("____" ^ fname ^ "_code____")
   val code_def = Definition.new_definition(n,mk_eq(mk_var(n,type_of exp),exp))
   val th = CONV_RULE ((RATOR_CONV o RAND_CONV) (K (GSYM code_def))) th
   in (code_def,(fname,ml_fname,def,th,v)) end

diff --git a/translator/okasaki-examples/benchmarkScript.sml b/translator/okasaki-examples/benchmarkScript.sml
@@ -12,6 +12,8 @@ open listTheory arithmeticTheory ml_translatorLib ListProgTheory;
 
 val _ = translation_extends "ListProg";
 
+val _ = Globals.interactive := false;
+
 (* copied from ImplicitQueueScript *)
 
 Datatype:
@@ -81,11 +83,11 @@ val is_heap_ordered_def = Define `
   BAG_EVERY (\y. leq (get_key x) (get_key y)) (heap_to_bag h2))`;
 
 val _ = mlDefine `
-empty = Empty`;
+empty' = Empty`;
 
-val is_empty_def = mlDefine `
-(is_empty Empty = T) ∧
-(is_empty _ = F)`;
+val is_empty'_def = mlDefine `
+(is_empty' Empty = T) ∧
+(is_empty' _ = F)`;
 
 val partition_def = mlDefine `
 (partition get_key leq pivot Empty = (Empty, Empty)) ∧
@@ -170,8 +172,6 @@ val use_heap_def = mlDefine `
   use_heap n (insert (\x.x) ((\x y. x < y) :num->num->bool) n (delete_min (insert (\x.x) ((\x y. x < y) :num->num->bool) (n + 400000) h))))`
 
 val run_heap = mlDefine `
-run_heap ⇔ find_min (use_heap 1000 empty)`;
-
-
+run_heap ⇔ find_min (use_heap 1000 empty')`;
 
 val _ = export_theory ();