Update for improved HOL syntax for Datatypes

Summary:
HOL now lets us omit quotations on Datatypes and make them look more
like the other new-style HOL definitions.

Reviewed By: jberdine

Differential Revision: D16983934

fbshipit-source-id: f8ef3abb5

sledge/semantics/llairScript.sml

@@ -16,22 +16,25 @@ numLib.prefer_num ();
 
 (* ----- Abstract syntax ----- *)
 
-Datatype `
+Datatype:
   typ =
   | FunctionT typ (typ list)
   | IntegerT num
   | PointerT typ
   | ArrayT typ num
-  | TupleT (typ list)`;
+  | TupleT (typ list)
+End
 
-Datatype `
-  var = Var_name string`;
+Datatype:
+  var = Var_name string
+End
 
-Datatype `
-  label = Lab_name string string`;
+Datatype:
+  label = Lab_name string string
+End
 
 (* Based on the constructor functions in exp.mli rather than the type definition *)
-Datatype `
+Datatype:
   exp =
   | Var var
   | Nondet
@@ -52,9 +55,10 @@ Datatype `
   (* Args: Record, index *)
   | Select exp exp
   (* Args: Record, index, value *)
-  | Update exp exp exp`;
+  | Update exp exp exp
+End
 
-Datatype `
+Datatype:
   inst =
   (* Args: the list of variable, expression assignments to do *)
   | Move ((var # exp) list)
@@ -74,9 +78,10 @@ Datatype `
   | Free exp
   (* Args: result reg *)
   | NondetI var
-  | Abort`;
+  | Abort
+End
 
-Datatype `
+Datatype:
   term =
   (* Args: key, branch table, default exp *)
   | Switch exp ((num # label) list) label
@@ -87,53 +92,62 @@ Datatype `
   | Call var label (exp list) typ label label
   | Return exp
   | Throw exp
-  | Unreachable`;
+  | Unreachable
+End
 
-Datatype `
-  block = <| cmnd : inst list; term : term |>`;
+Datatype:
+  block = <| cmnd : inst list; term : term |>
+End
 
 (* The llair code doesn't have params here yet, but it will need to *)
-Datatype `
+Datatype:
   func = <| params : var list;
             locals : var set;
             entry : label;
             cfg : (label, block) alist;
             freturn : var;
-            fthrow : var |>`;
+            fthrow : var |>
+End
 
 (* The int is how much space the global needs *)
-Datatype `
-  global = <| var : var; init : (exp # int) option; typ: typ |>`;
+Datatype:
+  global = <| var : var; init : (exp # int) option; typ: typ |>
+End
 
-Datatype `
-  llair = <| globals : global list; functions : (label, func) alist |>`;
+Datatype:
+  llair = <| globals : global list; functions : (label, func) alist |>
+End
 
 (* ----- Semantic states ----- *)
 
 (* TODO Given the similarities with LLVM, consider moving some definitions into
  * a common predecessor theory *)
 
-Datatype `
-  addr = A num`;
+Datatype:
+  addr = A num
+End
 
 (* These are the values that can be stored in registers. The implementation uses
  * integers with a bit-width to represent numbers, and keeps locations and sizes
  * separate.
  *)
-Datatype `
+Datatype:
   v =
   | LocV num
   | SizeV num
   | IntV int num
-  | AggV (v list)`;
+  | AggV (v list)
+End
 
-Datatype `
-  pc = <| l : label; i : num |>`;
+Datatype:
+  pc = <| l : label; i : num |>
+End
 
-Datatype `
-  frame = <| ret : pc; exn_ret : pc; ret_var : var; saved_locals : var |-> v; |>`;
+Datatype:
+  frame = <| ret : pc; exn_ret : pc; ret_var : var; saved_locals : var |-> v; |>
+End
 
-Datatype `
+Datatype:
   state =
     <| ip : pc;
        globals : var |-> word64;
@@ -147,7 +161,8 @@ Datatype `
         * semantics. *)
        allocations : (num # num) set;
        (* A byte addressed heap *)
-       heap : addr |-> word8 |>`;
+       heap : addr |-> word8 |>
+End
 
 (* ----- Semantic transitions ----- *)
 

sledge/semantics/llvmScript.sml

@@ -18,47 +18,56 @@ numLib.prefer_num ();
 (* ----- Abstract syntax ----- *)
 
 (* Only support 1, 8, 32, and 64 bit words for now *)
-Datatype `
-  size = W1 | W8 | W32 | W64`;
+Datatype:
+  size = W1 | W8 | W32 | W64
+End
 
-Datatype `
+Datatype:
   ty =
   | FunT ty (ty list)
   | IntT size
   | PtrT ty
   | ArrT num ty
-  | StrT (ty list)`;
+  | StrT (ty list)
+End
 
-Datatype `
-  label = Lab string`;
+Datatype:
+  label = Lab string
+End
 
-Datatype `
-  reg = Reg string`;
+Datatype:
+  reg = Reg string
+End
 
-Datatype `
-  glob_var = Glob_var string`;
+Datatype:
+  glob_var = Glob_var string
+End
 
-Datatype `
-  fun_name = Fn string`;
+Datatype:
+  fun_name = Fn string
+End
 
-Datatype `
+Datatype:
   const =
   | IntC size int
   | StrC ((ty # const) list)
   | ArrC ((ty # const) list)
   | GepC ty const (ty # const) ((ty # const) list)
   | GlobalC glob_var
-  | UndefC`;
+  | UndefC
+End
 
-Datatype `
-  arg = Constant const | Variable reg`;
+Datatype:
+  arg = Constant const | Variable reg
+End
 
-type_abbrev ("targ", ``:ty # arg``);
+Type targ = ``:ty # arg``
 
-Datatype `
-  cond = Eq | Ult | Slt`;
+Datatype:
+  cond = Eq | Ult | Slt
+End
 
-Datatype `
+Datatype:
   instr =
   (* Terminators *)
   | Ret targ
@@ -82,33 +91,40 @@ Datatype `
   | Cxa_throw arg arg arg
   | Cxa_begin_catch reg arg
   | Cxa_end_catch
-  | Cxa_get_exception_ptr reg arg`;
+  | Cxa_get_exception_ptr reg arg
+End
 
-Datatype `
-  phi = Phi reg ty ((label option, arg) alist)`;
+Datatype:
+  phi = Phi reg ty ((label option, arg) alist)
+End
 
-Datatype `
-  clause = Catch targ`;
+Datatype:
+  clause = Catch targ
+End
 
-Datatype `
-  landingpad = Landingpad ty bool (clause list)`;
+Datatype:
+  landingpad = Landingpad ty bool (clause list)
+End
 
-Datatype `
+Datatype:
   blockHeader =
   | Entry
-  | Head (phi list) (landingpad option)`;
+  | Head (phi list) (landingpad option)
+End
 
-Datatype `
-  block = <| h : blockHeader; body : instr list |>`;
+Datatype:
+  block = <| h : blockHeader; body : instr list |>
+End
 
-Datatype `
+Datatype:
   def =
     <| r : ty;
        params : reg list;
        (* None -> entry block, and Some name -> non-entry block *)
-       blocks : (label option, block) alist |>`;
+       blocks : (label option, block) alist |>
+End
 
-type_abbrev ("prog", ``:(fun_name, def) alist``);
+Type prog = ``:(fun_name, def) alist``
 
 Definition terminator_def:
   (terminator (Ret _) ⇔ T) ∧
@@ -120,10 +136,11 @@ End
 
 (* ----- Semantic states ----- *)
 
-Datatype `
-  addr = A num`;
+Datatype:
+  addr = A num
+End
 
-Datatype `
+Datatype:
   v =
   | W1V word1
   | W8V word8
@@ -131,18 +148,22 @@ Datatype `
   | W64V word64
   | AggV (v list)
   | PtrV word64
-  | UndefV`;
+  | UndefV
+End
 
-Datatype `
-  pv = <| poison : bool; value : v |>`;
+Datatype:
+  pv = <| poison : bool; value : v |>
+End
 
-Datatype `
-  pc = <| f : fun_name; b : label option; i : num |>`;
+Datatype:
+  pc = <| f : fun_name; b : label option; i : num |>
+End
 
-Datatype `
-  frame = <| ret : pc; saved_locals : reg |-> pv; result_var : reg; stack_allocs : addr list |>`;
+Datatype:
+  frame = <| ret : pc; saved_locals : reg |-> pv; result_var : reg; stack_allocs : addr list |>
+End
 
-Datatype `
+Datatype:
   state =
     <| ip : pc;
        (* Keep the size of the global with its memory address *)
@@ -153,7 +174,8 @@ Datatype `
         * free-able or not *)
        allocations : (bool # num # num) set;
        (* A byte addressed heap, with a poison tag *)
-       heap : addr |-> bool # word8 |>`;
+       heap : addr |-> bool # word8 |>
+End
 
 (* ----- Things about types ----- *)
 

sledge/semantics/llvm_to_llairScript.sml

@@ -180,12 +180,13 @@ Definition translate_instr_to_term_def:
     Iswitch (translate_arg emap a) [translate_label f l2; translate_label f l1]
 End
 
-Datatype `
+Datatype:
   instr_class =
   | Exp reg
   | Non_exp
   | Term
-  | Call`;
+  | Call
+End
 
 Definition classify_instr_def:
   (classify_instr (Call _ _ _ _) = Call) ∧