Merge pull request #1065 from CakeML/remove-zdefine

Remove zDefine usages

Author: IlmariReissumies

basis/fsFFIScript.sml

@@ -318,7 +318,7 @@ Definition encode_files_def:
   encode_files fs = encode_list (encode_pair (Str o explode) (Str o explode)) fs
 End
 
-val encode_def = zDefine`
+Definition encode_def[nocompute]:
   encode fs = Cons
                (Cons
                  (cfFFIType$Cons
@@ -327,7 +327,8 @@ val encode_def = zDefine`
                     (encode_fds fs.infds))
                   (Stream fs.numchars))
                  (encode_files fs.files))
-               (Num fs.maxFD)`
+               (Num fs.maxFD)
+End
 
 Theorem encode_inode_11[simp]:
    !x y. encode_inode x = encode_inode y <=> x = y

candle/overloading/monadic/holKernelProofScript.sml

@@ -2184,8 +2184,9 @@ Proof
   \\ match_mp_tac ALL_DISTINCT_DISJOINT \\ fs []
 QED
 
-val STRCAT_SHADOW_def = zDefine`
-  STRCAT_SHADOW = STRCAT`
+Definition STRCAT_SHADOW_def[nocompute]:
+  STRCAT_SHADOW = STRCAT
+End
 
 val first_dup_thm = Q.prove(
   `∀ls acc. (first_dup ls acc = NONE) ⇒ ALL_DISTINCT ls ∧ (∀x. MEM x ls ⇒ ¬MEM x acc)`,

candle/standard/monadic/holKernelProofScript.sml

@@ -2176,8 +2176,9 @@ Proof
   \\ match_mp_tac ALL_DISTINCT_DISJOINT \\ fs []
 QED
 
-val STRCAT_SHADOW_def = zDefine`
-  STRCAT_SHADOW = STRCAT`
+Definition STRCAT_SHADOW_def[nocompute]:
+  STRCAT_SHADOW = STRCAT
+End
 
 val first_dup_thm = Q.prove(
   `∀ls acc. (first_dup ls acc = NONE) ⇒ ALL_DISTINCT ls ∧ (∀x. MEM x ls ⇒ ¬MEM x acc)`,

characteristic/cfFFITypeScript.sml

@@ -45,44 +45,51 @@ End
 
 (* constructors *)
 
-val Num_def = zDefine `
+Definition Num_def[nocompute]:
   ((Num i):ffi) =
-    FFI_TYPE (\n. if n = iNum 0 then iNum 0 else iNum i)`
+    FFI_TYPE (\n. if n = iNum 0 then iNum 0 else iNum i)
+End
 
-val Str_def = zDefine `
+Definition Str_def[nocompute]:
   ((Str i):ffi) =
-    FFI_TYPE (\n. if n = iNum 0 then iNum 1 else iStr i)`
+    FFI_TYPE (\n. if n = iNum 0 then iNum 1 else iStr i)
+End
 
-val Cons_def = zDefine `
+Definition Cons_def[nocompute]:
   ((Cons (x:ffi) (y:ffi)):ffi) =
     FFI_TYPE (\n. if n = iNum 0 then iNum 2 else
                     case n of
                     | iCons (iNum 0) m => ffi_app x m
                     | iCons (iNum 1) m => ffi_app y m
-                    | _ => iNum 0)`
+                    | _ => iNum 0)
+End
 
-val List_def = zDefine `
+Definition List_def[nocompute]:
   ((List (xs:ffi list)):ffi) =
     FFI_TYPE (\n. if n = iNum 0 then iNum 3 else
                   if n = iNum 1 then iNum (LENGTH xs) else
                     case n of
                     | iCons (iNum k) m => ffi_app (EL k xs) m
-                    | _ => iNum 0)`
+                    | _ => iNum 0)
+End
 
-val Stream_def = zDefine `
+Definition Stream_def[nocompute]:
   ((Stream i):ffi) =
-    FFI_TYPE (\n. if n = iNum 0 then iNum 4 else iStream i)`
+    FFI_TYPE (\n. if n = iNum 0 then iNum 4 else iStream i)
+End
 
-val Fun_def = zDefine `
+Definition Fun_def[nocompute]:
   ((Fun (f:ffi_inner -> ffi)):ffi) =
     FFI_TYPE (\n. if n = iNum 0 then iNum 5 else
                     case n of
                     | iCons x y => ffi_app (f x) y
-                    | _ => iNum 0)`;
+                    | _ => iNum 0)
+End
 
-val Inner_def = zDefine `
+Definition Inner_def[nocompute]:
   ((Inner i):ffi) =
-    FFI_TYPE (\n. if n = iNum 0 then iNum 6 else i)`;
+    FFI_TYPE (\n. if n = iNum 0 then iNum 6 else i)
+End
 
 (* injectivity *)
 

compiler/backend/semantics/wordSemScript.sml

@@ -787,14 +787,15 @@ val fix_clock_IMP_LESS_EQ = Q.prove(
   `!x. fix_clock ^s x = (res,s1) ==> s1.clock <= s.clock /\ s1.termdep = s.termdep`,
   full_simp_tac(srw_ss())[fix_clock_def,FORALL_PROD] \\ srw_tac[][] \\ full_simp_tac(srw_ss())[] \\ decide_tac);
 
-val MustTerminate_limit_def = zDefine `
+Definition MustTerminate_limit_def[nocompute]:
   MustTerminate_limit (:'a) =
     (* This is just a number that's large enough for our purposes.
        It stated in a way that makes proofs easy. *)
     2 * dimword (:'a) +
     dimword (:'a) * dimword (:'a) +
     dimword (:'a) ** dimword (:'a) +
-    dimword (:'a) ** dimword (:'a) ** dimword (:'a)`;
+    dimword (:'a) ** dimword (:'a) ** dimword (:'a)
+End
 
 Definition const_addresses_def:
   const_addresses a [] d = T ∧

compiler/encoders/arm7/arm7_targetScript.sml

@@ -44,8 +44,9 @@ val () = List.app Parse.temp_overload_on
        "HI", "LS", "GE", "LT", "GT", "LE", "AL"],
       List.tabulate (15, fn i => wordsSyntax.mk_wordii (i, 4))))
 
-val arm7_encode_fail_def = zDefine`
-  arm7_encode_fail = [0w; 0w; 0w; 0w] : word8 list`
+Definition arm7_encode_fail_def[nocompute]:
+  arm7_encode_fail = [0w; 0w; 0w; 0w] : word8 list
+End
 
 Definition arm7_encode1_def:
   arm7_encode1 c i =

compiler/encoders/arm8/arm8_targetScript.sml

@@ -26,8 +26,9 @@ End
 
 (* --- Encode ASM instructions to ARM bytes. --- *)
 
-val arm8_encode_fail_def = zDefine`
-  arm8_encode_fail = [NoOperation]`
+Definition arm8_encode_fail_def[nocompute]:
+  arm8_encode_fail = [NoOperation]
+End
 
 Definition arm8_encode_def:
    arm8_encode i =
@@ -253,8 +254,9 @@ Definition arm8_ast_def:
         ])
 End
 
-val arm8_enc_def = zDefine
-  `arm8_enc = combin$C LIST_BIND arm8_encode o arm8_ast`
+Definition arm8_enc_def[nocompute]:
+  arm8_enc = combin$C LIST_BIND arm8_encode o arm8_ast
+End
 
 (* --- Configuration for ARMv8 --- *)
 

compiler/encoders/asm/asmPropsScript.sml

@@ -98,16 +98,18 @@ Proof
   \\ Cases_on`i` \\ fs[ADD1,LEFT_ADD_DISTRIB,RIGHT_ADD_DISTRIB]
 QED
 
-val asserts_def = zDefine `
+Definition asserts_def[nocompute]:
   (asserts 0 next ms _ Q <=> Q (next 0 ms)) /\
   (asserts (SUC n) next ms P Q <=>
-     let ms' = next (SUC n) ms in P ms' /\ asserts n next ms' P Q)`
+     let ms' = next (SUC n) ms in P ms' /\ asserts n next ms' P Q)
+End
 
-val asserts2_def = zDefine`
+Definition asserts2_def[nocompute]:
   (asserts2 n fi fc ms P =
    if n = 0n then T else
      P ms (fc ms) ∧
-     asserts2 (n-1) fi fc (fi n (fc ms)) P)`;
+     asserts2 (n-1) fi fc (fi n (fc ms)) P)
+End
 
 Definition encoder_correct_def:
   encoder_correct t <=>

compiler/encoders/mips/mips_targetScript.sml

@@ -285,8 +285,9 @@ Definition mips_ast_def:
            ArithI (ORI (temp_reg, 31w, 0w))])
 End        (* LR := tmp    *)
 
-val mips_enc_def = zDefine`
-  mips_enc = combin$C LIST_BIND mips_encode o mips_ast`
+Definition mips_enc_def[nocompute]:
+  mips_enc = combin$C LIST_BIND mips_encode o mips_ast
+End
 
 (* --- Configuration for MIPS --- *)
 

compiler/encoders/riscv/riscv_targetScript.sml

@@ -249,8 +249,9 @@ Definition riscv_ast_def:
        ArithI (ADDI (n2w r, n2w r, imm12))])
 End
 
-val riscv_enc_def = zDefine`
-  riscv_enc = combin$C LIST_BIND riscv_encode o riscv_ast`
+Definition riscv_enc_def[nocompute]:
+  riscv_enc = combin$C LIST_BIND riscv_encode o riscv_ast
+End
 
 (* --- Configuration for RISC-V --- *)
 

compiler/encoders/x64/x64_targetScript.sml

@@ -198,7 +198,9 @@ Definition x64_encode_def:
   (x64_encode i = x64$encode i)
 End
 
-val x64_dec_fail_def = zDefine `x64_dec_fail = [0w] : word8 list`
+Definition x64_dec_fail_def[nocompute]:
+  x64_dec_fail = [0w] : word8 list
+End
 
 Definition x64_enc_def:
   x64_enc i =

compiler/inference/unifyScript.sml

@@ -2090,8 +2090,9 @@ fs [t_wfs_def] >|
      rw [encode_infer_t_def, decode_infer_t_def, decode_left_inverse]]
 QED
 
-val t_walk_def = zDefine `
-t_walk s t = decode_infer_t (walk (encode_infer_t o_f s) (encode_infer_t t))`;
+Definition t_walk_def[nocompute]:
+t_walk s t = decode_infer_t (walk (encode_infer_t o_f s) (encode_infer_t t))
+End
 
 Theorem t_walk_eqn:
  (!s v. t_walk s (Infer_Tuvar v) = t_vwalk s v) ∧
@@ -2102,8 +2103,9 @@ rw [t_walk_def, walk_def, t_vwalk_def, encode_infer_t_def,
     decode_infer_t_def, decode_left_inverse]
 QED
 
-val t_oc_def = zDefine `
-t_oc s t v = oc (encode_infer_t o_f s) (encode_infer_t t) v`;
+Definition t_oc_def[nocompute]:
+t_oc s t v = oc (encode_infer_t o_f s) (encode_infer_t t) v
+End
 
 (*
 val t_oc_ind' = Q.prove (
@@ -2174,11 +2176,12 @@ cases_on `t_vwalk s n` >>
 rw [encode_infer_t_def, t_oc_eqn_help]
 QED
 
-val t_ext_s_check_def = zDefine `
+Definition t_ext_s_check_def[nocompute]:
 t_ext_s_check s v t =
   OPTION_MAP
     ((o_f) decode_infer_t)
-    (ext_s_check (encode_infer_t o_f s) v (encode_infer_t t))`;
+    (ext_s_check (encode_infer_t o_f s) v (encode_infer_t t))
+End
 
 Theorem t_ext_s_check_eqn:
  !s v t.
@@ -2189,11 +2192,12 @@ rw [t_ext_s_check_def, t_oc_def, decode_left_inverse_I,
 metis_tac [FUPDATE_PURGE]
 QED
 
-val t_unify_def = zDefine `
+Definition t_unify_def[nocompute]:
 t_unify s t1 t2 =
   OPTION_MAP
     ((o_f) decode_infer_t)
-    (unify (encode_infer_t o_f s) (encode_infer_t t1) (encode_infer_t t2))`;
+    (unify (encode_infer_t o_f s) (encode_infer_t t1) (encode_infer_t t2))
+End
 
 Definition ts_unify_def:
 (ts_unify s [] [] = SOME s) ∧
@@ -2600,8 +2604,9 @@ Proof
   fs[t_wfs_def]
 QED
 
-val apply_subst_t_def = zDefine `
-apply_subst_t s t = decode_infer_t (subst_APPLY (encode_infer_t o_f s) (encode_infer_t t))`;
+Definition apply_subst_t_def[nocompute]:
+apply_subst_t s t = decode_infer_t (subst_APPLY (encode_infer_t o_f s) (encode_infer_t t))
+End
 
 Theorem apply_subst_t_eqn:
  (!s n.
@@ -2624,9 +2629,10 @@ induct_on `ts` >>
 rw [apply_subst_t_def, encode_infer_t_def, decode_infer_t_def]
 QED
 
-val t_walkstar_def = zDefine `
+Definition t_walkstar_def[nocompute]:
 t_walkstar s t =
-  decode_infer_t (walkstar (encode_infer_t o_f s) (encode_infer_t t))`;
+  decode_infer_t (walkstar (encode_infer_t o_f s) (encode_infer_t t))
+End
 
 Theorem t_walkstar_cwalkstar:
   t_walkstar s t = cwalkstar (fm2sp s) t
@@ -2692,9 +2698,10 @@ Proof
   metis_tac[]
 QED
 
-val t_collapse_def = zDefine `
+Definition t_collapse_def[nocompute]:
 t_collapse s =
-  decode_infer_t o_f collapse (encode_infer_t o_f s)`;
+  decode_infer_t o_f collapse (encode_infer_t o_f s)
+End
 
 Theorem t_collapse_eqn:
  !s. t_collapse s = FUN_FMAP (\v. t_walkstar s (Infer_Tuvar v)) (FDOM s)

examples/eval/compile_code_to_evalScript.sml

@@ -117,8 +117,12 @@ Triviality to_flat_inc_thm0 = eval ``to_flat_inc
   ^config ^env_id ^p``
 
 val (c, ps) = to_flat_inc_thm0 |> rconc |> dest_pair
-val flat_conf_inc_def = zDefine`flat_conf_inc = ^c`;
-val flat_prog_def = zDefine`flat_prog = ^ps`;
+Definition flat_conf_inc_def[nocompute]:
+  flat_conf_inc = ^c
+End
+Definition flat_prog_def[nocompute]:
+  flat_prog = ^ps
+End
 val to_flat_inc_thm =
   to_flat_inc_thm0 |> CONV_RULE(RAND_CONV(
     FORK_CONV(REWR_CONV(SYM flat_conf_inc_def),
@@ -141,7 +145,9 @@ Triviality to_clos_inc_thm0 =
       REWR_CONV LET_THM THENC eval)
 
 val ps = to_clos_inc_thm0 |> rconc |> dest_pair |> #2
-val clos_prog_def = zDefine`clos_prog = ^ps`;
+Definition clos_prog_def[nocompute]:
+  clos_prog = ^ps
+End
 val to_clos_inc_thm =
   to_clos_inc_thm0 |> CONV_RULE(RAND_CONV(
     RAND_CONV(REWR_CONV(SYM clos_prog_def))))
@@ -181,8 +187,12 @@ Triviality to_bvl_inc_thm0 =
   |> CONV_RULE(RAND_CONV eval)
 
 val (c,ps) = to_bvl_inc_thm0 |> rconc |> dest_pair
-val bvl_conf_inc_def = zDefine`bvl_conf_inc = ^c`;
-val bvl_prog_def = zDefine`bvl_prog = ^ps`;
+Definition bvl_conf_inc_def[nocompute]:
+  bvl_conf_inc = ^c
+End
+Definition bvl_prog_def[nocompute]:
+  bvl_prog = ^ps
+End
 val to_bvl_inc_thm =
   to_bvl_inc_thm0 |> CONV_RULE(RAND_CONV(
     FORK_CONV(REWR_CONV(SYM bvl_conf_inc_def),
@@ -215,8 +225,12 @@ Triviality to_bvi_inc_thm0 =
   |> CONV_RULE (RAND_CONV eval)
 
 val (c,ps) = to_bvi_inc_thm0 |> rconc |> dest_pair
-val bvi_conf_inc_def = zDefine`bvi_conf_inc = ^c`;
-val bvi_prog_def = zDefine`bvi_prog = ^ps`;
+Definition bvi_conf_inc_def[nocompute]:
+  bvi_conf_inc = ^c
+End
+Definition bvi_prog_def[nocompute]:
+  bvi_prog = ^ps
+End
 val to_bvi_inc_thm =
   to_bvi_inc_thm0 |> CONV_RULE(RAND_CONV(
     FORK_CONV(REWR_CONV(SYM bvi_conf_inc_def),
@@ -251,7 +265,9 @@ val to_data_inc_thm0 =
   |> CONV_RULE(RAND_CONV eval)
 
 val (_,ps) = to_data_inc_thm0 |> rconc |> dest_pair
-val data_prog_def = zDefine`data_prog = ^ps`;
+Definition data_prog_def[nocompute]:
+  data_prog = ^ps
+End
 val to_data_inc_thm =
   to_data_inc_thm0 |> CONV_RULE(RAND_CONV(
   (RAND_CONV(REWR_CONV(SYM data_prog_def)))));
@@ -360,7 +376,9 @@ val to_word_inc_thm1 =
        REWR_CONV_BETA LET_THM))
 
 val (_,ps) = to_word_inc_thm1 |> rconc |> dest_pair
-val word_prog_def = zDefine`word_prog = ^ps`;
+Definition word_prog_def[nocompute]:
+  word_prog = ^ps
+End
 val () = computeLib.extend_compset
   [computeLib.Defs [word_prog_def]] cs;
 val to_word_inc_thm =