Merge pull request #1066 from CakeML/remove-old-datatype

Remove old Datatype` syntax

Author: myreen

basis/fsFFIScript.sml

@@ -11,11 +11,15 @@ val _ = option_monadsyntax.temp_add_option_monadsyntax();
 (* Logical model of filesystem and I/O streams *)
 
 (* regular files and unnamed streams *)
-val _ = Datatype` inode = UStream mlstring | File mlstring`
+Datatype:
+  inode = UStream mlstring | File mlstring
+End
 
 Overload isFile = ``λinode. ∃fnm. inode = File fnm``
 
-val _ = Datatype` mode = ReadMode | WriteMode`;
+Datatype:
+  mode = ReadMode | WriteMode
+End
 
 (* files: a list of file names and their content.
 *  infds: descriptor * (filename * mode * position)
@@ -27,13 +31,14 @@ val _ = Datatype` mode = ReadMode | WriteMode`;
 *  ulimit -n has a usual value of 1024
 *)
 
-val _ = Datatype`
+Datatype:
   IO_fs = <| inode_tbl : (inode # char list) list ;
              files : (mlstring # mlstring) list;
              infds : (num # (inode # mode # num)) list;
              numchars : num llist;
              maxFD : num
-           |>`
+           |>
+End
 
 val IO_fs_component_equality = theorem"IO_fs_component_equality";
 

basis/pure/mloptionScript.sml

@@ -5,8 +5,6 @@ open preamble
 
 val _ = new_theory"mloption"
 
-(*val _ = Datatype `option = *)
-
 Definition getOpt_def:
   (getOpt (SOME v) a = v) /\
   (getOpt NONE a = a)

basis/pure/mlstringScript.sml

@@ -14,7 +14,9 @@ val cpn_nchotomy = TypeBase.nchotomy_of ``:ordering``
 (* Defines strings as a separate type from char list. This theory should be
    moved into HOL, either as its own theory, or as an addendum to stringTheory *)
 
-val _ = Datatype`mlstring = strlit string`
+Datatype:
+  mlstring = strlit string
+End
 val _ = add_strliteral_form{inj=``strlit``, ldelim = "«"};
 
 Definition implode_def:

characteristic/cfFFITypeScript.sml

@@ -29,15 +29,17 @@ important injectivity (suffix: "_11") are here.
 
 *)
 
-val _ = Datatype `
+Datatype:
   ffi_inner = iStr string
             | iNum num
             | iCons ffi_inner ffi_inner
             | iList (ffi_inner list)
-            | iStream (num llist)`
+            | iStream (num llist)
+End
 
-val _ = Datatype `
-  ffi = FFI_TYPE (ffi_inner -> ffi_inner)`
+Datatype:
+  ffi = FFI_TYPE (ffi_inner -> ffi_inner)
+End
 
 Definition ffi_app_def:
   ffi_app x n = case x of FFI_TYPE f => f n

characteristic/cfHeapsBaseScript.sml

@@ -11,12 +11,13 @@ val _ = new_theory "cfHeapsBase"
 (** Heaps *)
 
 (* the following is now defined in cfFFITypeTheory
-val _ = Datatype `
+Datatype:
   ffi = Str string
       | Num num
       | Cons ffi ffi
       | List (ffi list)
-      | Stream (num llist)`
+      | Stream (num llist)
+End
 *)
 
 Definition encode_pair_def:
@@ -68,8 +69,9 @@ Proof
   Cases \\ Cases \\ rw[encode_int_def]
 QED
 
-val _ = Datatype `
-  ffi_result = FFIreturn (word8 list) 'ffi | FFIdiverge`
+Datatype:
+  ffi_result = FFIreturn (word8 list) 'ffi | FFIdiverge
+End
 
 (* make an ffi_next function from base functions and encode/decode *)
 Definition mk_ffi_next_def:
@@ -86,20 +88,22 @@ Type loc = ``:num``
 
 Type ffi_next = ``:string -> word8 list -> word8 list -> ffi -> ffi ffi_result option``
 
-val _ = Datatype `
+Datatype:
   heap_part = Mem loc (v semanticPrimitives$store_v)
             | FFI_split
             | FFI_part ffi ffi_next (string list) (io_event list)
-            | FFI_full (io_event list)`
+            | FFI_full (io_event list)
+End
 
 Type heap = ``:heap_part set``
 Type hprop = ``:heap -> bool``
 
-val _ = Datatype `
+Datatype:
   res = Val v
       | Exn v
       | FFIDiv string (word8 list) (word8 list)
-      | Div (io_event llist)`
+      | Div (io_event llist)
+End
 
 Type ffi_proj = ``: ('ffi -> (string |-> ffi)) #
                     ((string list # ffi_next) list)``

compiler/backend/ag32/proofs/ag32_progScript.sml

@@ -22,10 +22,11 @@ QED
 
 (* basic definitions *)
 
-val _ = Datatype `
+Datatype:
   ag32_el = aState ag32_state
           | aMem word32 word8
-          | aPc word32`;
+          | aPc word32
+End
 
 val ag32_el_11 = DB.fetch "-" "ag32_el_11";
 val ag32_el_distinct = DB.fetch "-" "ag32_el_distinct";

compiler/backend/backendScript.sml

@@ -21,7 +21,8 @@ open jsonLangTheory presLangTheory
 
 val _ = new_theory"backend";
 
-val _ = Datatype`config =
+Datatype:
+  config =
   <| source_conf : source_to_flat$config
    ; clos_conf : clos_to_bvl$config
    ; bvl_conf : bvl_to_bvi$config
@@ -33,7 +34,8 @@ val _ = Datatype`config =
    ; symbols : (mlstring # num # num) list
    ; tap_conf : tap_config
    ; exported : mlstring list (* field for Pancake entry points - empty for CakeML *)
-   |>`;
+   |>
+End
 
 val config_component_equality = theorem"config_component_equality";
 

compiler/backend/backend_commonScript.sml

@@ -66,12 +66,13 @@ Definition clos_tag_shift_def:
 End
 
 (* Trace of an expression through the compiler, for exploring transformations *)
-val _ = Datatype`
+Datatype:
   tra =
     | SourceLoc num (* start-row *) num (* start-col *) num (* end-row *) num (* end-col *)
     | Cons tra num
     | Union tra tra
-    | None (* Dead trace, do not make traces at all *)`
+    | None (* Dead trace, do not make traces at all *)
+End
 
 (* The code below replaces "Cons" in hol output with the chosen symbol *)
 val _ = set_fixity "▷" (Infixl 480);

compiler/backend/bviScript.sml

@@ -38,13 +38,14 @@ val _ = set_grammar_ancestry ["closLang" (* for op *)]
 
 (* --- Syntax of BVI --- *)
 
-val _ = Datatype `
+Datatype:
   exp = Var num
       | If exp exp exp
       | Let (exp list) exp
       | Raise exp
       | Tick exp
       | Call num (num option) (exp list) (exp option)
-      | Op op (exp list) `
+      | Op op (exp list)
+End
 
 val _ = export_theory();

compiler/backend/bvi_tailrecScript.sml

@@ -64,13 +64,16 @@ QED
 
 val _ = export_rewrites ["is_const_def"];
 
-val _ = Datatype `
+Datatype:
   assoc_op = Plus
            | Times
            | Append
-           | Noop`;
+           | Noop
+End
 
-val _ = Datatype `v_ty = Int | List | Any`;
+Datatype:
+  v_ty = Int | List | Any
+End
 
 Definition op_type_def:
   op_type Append = List /\

compiler/backend/bvlScript.sml

@@ -26,15 +26,16 @@ val _ = set_grammar_ancestry [
    "closLang", (* for op *) "backend_common" (* for tags *)
 ]
 
-val _ = Datatype `
+Datatype:
   exp = Var num
       | If exp exp exp
       | Let (exp list) exp
       | Raise exp
       | Handle exp exp
       | Tick exp
       | Call num (num option) (exp list)
-      | Op closLang$op (exp list) `
+      | Op closLang$op (exp list)
+End
 
 Definition Bool_def:
   Bool b = Op (Cons (bool_to_tag b)) []

compiler/backend/clos_knownScript.sml

@@ -274,14 +274,15 @@ End
 
    ----------------------------------------------------------------- *)
 
-val _ = Datatype `
+Datatype:
   val_approx =
     ClosNoInline num num        (* location in code table, arity *)
   | Clos num num exp num        (* loc, arity, body, body size *)
   | Tuple num (val_approx list) (* conses or tuples *)
   | Int int                     (* used to index tuples *)
   | Other                       (* unknown *)
-  | Impossible`                 (* value 'returned' by Raise *)
+  | Impossible                  (* value 'returned' by Raise *)
+End
 val val_approx_size_def = definition "val_approx_size_def"
 
 Definition merge_def[nocompute]:
@@ -446,7 +447,9 @@ Definition clos_gen_noinline_def:
     ClosNoInline (n+2*i) a::clos_gen_noinline n (i+1) xs)
 End
 
-val _ = Datatype `globalOpt = gO_Int int | gO_NullTuple num | gO_None`
+Datatype:
+  globalOpt = gO_Int int | gO_NullTuple num | gO_None
+End
 
 Definition isGlobal_def:
   (isGlobal (Global _) ⇔ T) ∧
@@ -479,18 +482,19 @@ Termination
   wf_rel_tac `measure (FST o SND o SND)`
 End
 
-val _ = Datatype `
+Datatype:
   inliningDecision = inlD_Nothing
                    | inlD_Annotate num
                    | inlD_LetInline exp
-`;
+End
 
-val _ = Datatype`
+Datatype:
   config = <| inline_max_body_size : num
             ; inline_factor : num (* As in 'Inline expansion: when and how?' by Manuel Serrano *)
             ; initial_inline_factor : num
             ; val_approx_spt : val_approx spt (* TODO: this could replace the explicit g argument in known_def *)
-            |>`;
+            |>
+End
 
 Definition default_inline_factor_def:
   default_inline_factor = 8n

compiler/backend/clos_to_bvlScript.sml

@@ -676,15 +676,16 @@ Proof
   \\ CONV_TAC (DEPTH_CONV PairRules.PBETA_CONV) \\ fs []
 QED
 
-val _ = Datatype`
+Datatype:
   config = <| next_loc : num
             ; start : num
             ; do_mti : bool
             ; known_conf : clos_known$config option
             ; do_call : bool
             ; call_state : num_set # (num, num # closLang$exp) alist
             ; max_app : num
-            |>`;
+            |>
+End
 
 Definition default_config_def:
   default_config = <|

compiler/backend/data_to_wordScript.sml

@@ -13,14 +13,15 @@ val _ = new_theory "data_to_word";
 
 val _ = patternMatchesLib.ENABLE_PMATCH_CASES();
 
-val _ = Datatype `
+Datatype:
   (* this configuration is used in data_to_wordProof and stack_alloc *)
   gc_kind =
     None
   | Simple
-  | Generational (num list) (* sizes of generations, smallest first *)`
+  | Generational (num list) (* sizes of generations, smallest first *)
+End
 
-val _ = Datatype `
+Datatype:
   config = <| tag_bits : num (* in each pointer *)
             ; len_bits : num (* in each pointer *)
             ; pad_bits : num (* in each pointer *)
@@ -31,7 +32,8 @@ val _ = Datatype `
             ; has_fp_tern : bool (* can compile FMA *)
             ; be : bool (* bigendian *)
             ; call_empty_ffi : bool (* emit (T) / omit (F) calls to FFI "" *)
-            ; gc_kind : gc_kind (* GC settings *) |>`
+            ; gc_kind : gc_kind (* GC settings *) |>
+End
 
 Definition adjust_var_def:
   adjust_var n = 2 * n + 2:num
@@ -150,8 +152,9 @@ Definition real_byte_offset_def:
             Shift Lsr (Var r) 2]
 End
 
-val _ = Datatype`
-  word_op_type = Bitwise binop | Carried binop`;
+Datatype:
+  word_op_type = Bitwise binop | Carried binop
+End
 
 Definition lookup_word_op_def:
   (lookup_word_op Andw = Bitwise And) ∧

compiler/backend/db_varsScript.sml

@@ -6,11 +6,12 @@ open preamble;
 
 val _ = new_theory "db_vars";
 
-val _ = Datatype `
+Datatype:
   db_var_set = Empty
              | Var num
              | Shift num db_var_set
-             | Union db_var_set db_var_set`;
+             | Union db_var_set db_var_set
+End
 
 Definition mk_Union_def:
   mk_Union t1 t2 =

compiler/backend/flat_patternScript.sml

@@ -15,8 +15,10 @@ val _ = new_theory "flat_pattern";
 val _ = set_grammar_ancestry ["misc","flatLang","sptree",
     "pattern_semantics"];
 
-val _ = Datatype `config =
-  <| pat_heuristic : (* pattern_matching$branch list *) (* unit -> *) num |>`;
+Datatype:
+  config =
+  <| pat_heuristic : (* pattern_matching$branch list *) (* unit -> *) num |>
+End
 
 Definition init_config_def:
   init_config ph = <| pat_heuristic := ph |>

compiler/backend/gc/gc_combinedScript.sml

@@ -6,8 +6,9 @@ open data_to_wordTheory;
 
 val _ = new_theory "gc_combined";
 
-val _ = Datatype `
-  gen_state = GenState num (num list)`;
+Datatype:
+  gen_state = GenState num (num list)
+End
 
 Definition make_partial_conf_def:
   make_partial_conf (conf:'a gen_gc_conf) (GenState _ gen_starts) rs =