Make union types consistent in the AST

Previously union types could have no-argument constructors, for
example the option type was previously:

union option ('a : Type) = {
  Some : 'a,
  None
}

Now every union constructor must have a type, so option becomes:

union option ('a : Type) = {
  Some : 'a,
  None : unit
}

The reason for this is because previously these two different types of
constructors where very different in the AST, constructors with
arguments were used the E_app AST node, and no-argument constructors
used the E_id node. This was particularly awkward, because it meant
that E_id nodes could have polymorphic types, i.e. every E_id node
that was also a union constructor had to be annotated with a type
quantifier, in constrast with all other identifiers that have
unquantified types. This became an issue when monomorphising types,
because the machinery for figuring out function instantiations can't
be applied to identifier nodes. The same story occurs in patterns,
where previously unions were split across P_id and P_app nodes - now
the P_app node alone is used solely for unions.

This is a breaking change because it changes the syntax for union
constructors - where as previously option was matched as:

function is_none opt = match opt {
  Some(_) => false,
  None    => true
}

it is now matched as

function is_none opt = match opt {
  Some(_) => false,
  None()  => true
}

note that constructor() is syntactic sugar for constructor(()), i.e. a
one argument constructor with unit as it's value. This is exactly the
same as for functions where a unit-function can be called as f() and
not as f(()). (This commit also makes exit() work consistently in the
same way) An attempt to pattern match a variable with the same name as
a union-constructor now gives an error as a way to guard against
mistakes made because of this change.

There is probably an argument for supporting the old syntax via some
syntactic sugar, as it is slightly prettier that way, but for now I
have chosen to keep the implementation as simple as possible.

The RISCV spec, ARM spec, and tests have been updated to account for
this change. Furthermore the option type can now be included from
$SAIL_DIR/lib/ using

$include <option.sail>

5 files changed, 62 insertions, 61 deletions

diff --git a/riscv/main.sail b/riscv/main.sail
index 0cc34061..8e0b0440 100644
--- a/riscv/main.sail
+++ b/riscv/main.sail
@@ -27,7 +27,7 @@ function fetch_and_execute () =
       nextPC = PC + instr_sz;
       match instr_ast {
         Some(ast) => execute(ast),
-        None      => {print("Decode failed"); exit (())}
+	None()    => {print("Decode failed"); exit()}
       }
     };
     let tohost_val = __RISCV_read(tohost, 4);
@@ -60,9 +60,9 @@ function main () = {
     fetch_and_execute()
   } catch {
     Error_not_implemented(s) => print_string("Error: Not implemented: ", s),
-    Error_misaligned_access  => print("Error: misaligned_access"),
-    Error_EBREAK => print("EBREAK"),
-    Error_internal_error => print("Error: internal error")
+    Error_misaligned_access() => print("Error: misaligned_access"),
+    Error_EBREAK() => print("EBREAK"),
+    Error_internal_error() => print("Error: internal error")
   };
   dump_state ()
 }
diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 89221596..b58ebc52 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -1,7 +1,7 @@
 default Order dec
 
 type bits ('n : Int) = vector('n, dec, bit)
-union option ('a : Type) = {None, Some : 'a}
+union option ('a : Type) = {None : unit, Some : 'a}
 
 val eq_atom = {ocaml: "eq_int", lem: "eq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
 val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
@@ -330,9 +330,9 @@ val print_string = "print_string" : (string, string) -> unit
 
 union exception = {
   Error_not_implemented : string,
-  Error_misaligned_access,
-  Error_EBREAK,
-  Error_internal_error
+  Error_misaligned_access : unit,
+  Error_EBREAK : unit,
+  Error_internal_error : unit
 }
 
 val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index 004621c7..21c6fd64 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -353,40 +353,40 @@ function clause execute (FENCE(pred, succ)) = {
 }
 
 /* ****************************************************************** */
-union clause ast = FENCEI
+union clause ast = FENCEI : unit
 
-function clause decode 0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111 = Some(FENCEI)
+function clause decode 0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111 = Some(FENCEI())
 
-function clause execute FENCEI = MEM_fence_i()
+function clause execute FENCEI() = MEM_fence_i()
 
 /* ****************************************************************** */
-union clause ast = ECALL
+union clause ast = ECALL : unit
 
-function clause decode 0b000000000000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(ECALL)
+function clause decode 0b000000000000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(ECALL())
 
-function clause execute ECALL =
+function clause execute ECALL() =
   let t : sync_exception =
     struct { trap = match (cur_privilege) {
                       USER => User_ECall,
 		      MACHINE => Machine_ECall
 		    },
-             excinfo = (None : option(xlenbits)) } in
+	     excinfo = (None() : option(xlenbits)) } in
   nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
 
 /* ****************************************************************** */
-union clause ast = MRET
+union clause ast = MRET : unit
 
-function clause decode 0b0011000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(MRET)
+function clause decode 0b0011000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(MRET())
 
-function clause execute MRET =
-  nextPC = handle_exception_ctl(cur_privilege, CTL_MRET, PC)
+function clause execute MRET() =
+  nextPC = handle_exception_ctl(cur_privilege, CTL_MRET(), PC)
 
 /* ****************************************************************** */
-union clause ast = EBREAK
+union clause ast = EBREAK : unit
 
-function clause decode 0b000000000001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(EBREAK)
+function clause decode 0b000000000001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(EBREAK())
 
-function clause execute EBREAK = { throw(Error_EBREAK) }
+function clause execute EBREAK() = { throw Error_EBREAK() }
 
 /* ****************************************************************** */
 union clause ast = LOADRES : (bool, bool, regbits, word_width, regbits)
@@ -591,22 +591,22 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) =
 
 /* ****************************************************************** */
 
-union clause ast = NOP
+union clause ast = NOP : unit
 
 function clause decodeCompressed (0b000 @ nzi1 : bits(1) @ 0b00000 @ (nzi0 : bits(5)) @ 0b01) : bits(16) = {
-  if (nzi1 == 0b0) & (nzi0 == 0b00000) then Some(NOP)
-  else None
+  if (nzi1 == 0b0) & (nzi0 == 0b00000) then Some(NOP())
+  else None()
 }
 
-function clause execute (NOP) = ()
+function clause execute NOP() = ()
 
 /* ****************************************************************** */
 
-union clause ast = ILLEGAL
+union clause ast = ILLEGAL : unit
 
-function clause decodeCompressed (0b0000 @ 0b00000 @ 0b00000 @ 0b00) : bits(16) = Some(ILLEGAL)
+function clause decodeCompressed (0b0000 @ 0b00000 @ 0b00000 @ 0b00) : bits(16) = Some(ILLEGAL())
 
-function clause execute (ILLEGAL) = {
+function clause execute ILLEGAL() = {
   let t : sync_exception =
   struct { trap = Illegal_Instr,
            excinfo = Some (EXTZ(0b0)) } in
@@ -619,7 +619,7 @@ union clause ast = C_ADDI4SPN : (cregbits, bits(8))
 
 function clause decodeCompressed (0b000 @ nz54 : bits(2) @ nz96 : bits(4) @ nz2 : bits(1) @ nz3 : bits(1) @ rd : cregbits @ 0b00) : bits(16) = {
   let nzimm = (nz96 @ nz54 @ nz3 @ nz2) : bits(8) in
-  if nzimm == 0b00000000 then None
+  if nzimm == 0b00000000 then None()
   else Some(C_ADDI4SPN(rd, nzimm))
 }
 
@@ -699,7 +699,7 @@ union clause ast = C_ADDI : (bits(6), regbits)
 
 function clause decodeCompressed (0b000 @ nzi5 : bits(1) @ rsd : regbits @ nzi40 : bits(5) @ 0b01) : bits(16) = {
   let nzi = (nzi5 @ nzi40) : bits(6) in
-  if (nzi == 0b000000) | (rsd == zreg) then None
+  if (nzi == 0b000000) | (rsd == zreg) then None()
   else Some(C_ADDI(nzi, rsd))
 }
 
@@ -735,7 +735,7 @@ function clause execute (C_ADDIW(imm, rsd)) = {
 union clause ast = C_LI : (bits(6), regbits)
 
 function clause decodeCompressed (0b010 @ imm5 : bits(1) @ rd : regbits @ imm40 : bits(5) @ 0b01) = {
-  if (rd == zreg) then None
+  if (rd == zreg) then None()
   else Some(C_LI(imm5 @ imm40, rd))
 }
 
@@ -750,7 +750,7 @@ union clause ast = C_ADDI16SP : (bits(6))
 
 function clause decodeCompressed (0b011 @ nzi9 : bits(1) @ /* x2 */ 0b00010 @ nzi4 : bits(1) @ nzi6 : bits(1) @ nzi87 : bits(2) @ nzi5 : bits(1) @ 0b01) = {
   let nzimm = nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4 in
-  if (nzimm == 0b000000) then None
+  if (nzimm == 0b000000) then None()
   else Some(C_ADDI16SP(nzimm))
 }
 
@@ -764,7 +764,7 @@ function clause execute (C_ADDI16SP(imm)) = {
 union clause ast = C_LUI : (bits(6), regbits)
 
 function clause decodeCompressed (0b011 @ imm17 : bits(1) @ rd : regbits @ imm1612 : bits(5) @ 0b01) = {
-  if (rd == zreg) | (rd == sp) then None
+  if (rd == zreg) | (rd == sp) then None()
   else Some(C_LUI(imm17 @ imm1612, rd))
 }
 
@@ -780,7 +780,7 @@ union clause ast = C_SRLI : (bits(6), cregbits)
 function clause decodeCompressed (0b100 @ nzui5 : bits(1) @ 0b00 @ rsd : cregbits @ nzui40 : bits(5) @ 0b01) = {
   let shamt : bits(6) = nzui5 @ nzui40 in
   if shamt == 0b000000 /* TODO: On RV32, also need shamt[5] == 0 */
-  then None
+  then None()
   else Some(C_SRLI(shamt, rsd))
 }
 
@@ -796,7 +796,7 @@ union clause ast = C_SRAI : (bits(6), cregbits)
 function clause decodeCompressed (0b100 @ nzui5 : bits(1) @ 0b01 @ rsd : cregbits @ nzui40 : bits(5) @ 0b01) = {
   let shamt : bits(6) = nzui5 @ nzui40 in
   if shamt == 0b000000 /* TODO: On RV32, also need shamt[5] == 0 */
-  then None
+  then None()
   else Some(C_SRAI(shamt, rsd))
 }
 
@@ -927,7 +927,7 @@ union clause ast = C_SLLI : (bits(6), regbits)
 function clause decodeCompressed (0b000 @ nzui5 : bits(1) @ rsd : regbits @ nzui40 : bits(5) @ 0b10) = {
   let shamt : bits(6) = nzui5 @ nzui40 in
   if shamt == 0b000000 | rsd == zreg /* TODO: On RV32, also need shamt[5] == 0 */
-  then None
+  then None()
   else Some(C_SLLI(shamt, rsd))
 }
 
@@ -941,7 +941,7 @@ union clause ast = C_LWSP : (bits(6), regbits)
 function clause decodeCompressed (0b010 @ ui5 : bits(1) @ rd : regbits @ ui42 : bits(3) @ ui76 : bits(2) @ 0b10) = {
   let uimm : bits(6) = ui76 @ ui5 @ ui42 in
   if  rd == zreg
-  then None
+  then None()
   else Some(C_LWSP(uimm, rd))
 }
 
@@ -957,7 +957,7 @@ union clause ast = C_LDSP : (bits(6), regbits)
 function clause decodeCompressed (0b011 @ ui5 : bits(1) @ rd : regbits @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10) = {
   let uimm : bits(6) = ui86 @ ui5 @ ui43 in
   if  rd == zreg
-  then None
+  then None()
   else Some(C_LDSP(uimm, rd))
 }
 
@@ -1000,7 +1000,7 @@ union clause ast = C_JR : (regbits)
 
 function clause decodeCompressed (0b100 @ 0b0 @ rs1 : regbits @ 0b00000 @ 0b10) = {
   if rs1 == zreg
-  then None
+  then None()
   else Some(C_JR(rs1))
 }
 
@@ -1013,7 +1013,7 @@ union clause ast = C_JALR : (regbits)
 
 function clause decodeCompressed (0b100 @ 0b1 @ rs1 : regbits @ 0b00000 @ 0b10) = {
   if rs1 == zreg
-  then None
+  then None()
   else Some(C_JALR(rs1))
 }
 
@@ -1026,7 +1026,7 @@ union clause ast = C_MV : (regbits, regbits)
 
 function clause decodeCompressed (0b100 @ 0b0 @ rd : regbits @ rs2 : regbits @ 0b10) = {
   if rs2 == zreg | rd == zreg
-  then None
+  then None()
   else Some(C_MV(rd, rs2))
 }
 
@@ -1039,7 +1039,7 @@ union clause ast = C_ADD : (regbits, regbits)
 
 function clause decodeCompressed (0b100 @ 0b1 @ rsd : regbits @ rs2 : regbits @ 0b10) = {
   if rsd == zreg | rs2 == zreg
-  then None
+  then None()
   else Some(C_ADD(rsd, rs2))
 }
 
@@ -1048,8 +1048,8 @@ function clause execute (C_ADD(rsd, rs2)) =
 
 /* ****************************************************************** */
 
-function clause decode _ = None
-function clause decodeCompressed _ = None
+function clause decode _ = None()
+function clause decodeCompressed _ = None()
 
 end ast
 end decode
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index 2956caae..4a80bf3a 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -221,15 +221,16 @@ union ctl_result = {
   CTL_URET,
   CTL_SRET,
 */
-  CTL_MRET
+  CTL_MRET : unit
 }
 
 /* privilege level */
 
-union privilege = {
+enum privilege = {
   MACHINE,
   USER
 }
+
 register cur_privilege : privilege
 
 function priv_to_bits(p : privilege) -> bits(2) =
@@ -262,19 +263,19 @@ function handle_exception_ctl(cur_priv : privilege, ctl : ctl_result,
         Misaligned_Fetch => {
           match (e.excinfo) {
             Some(a) => mtval = a,
-            None    => throw(Error_internal_error)
+	    None()  => throw Error_internal_error()
           }
         },
         Fetch_Access => {
           match (e.excinfo) {
             Some(a) => mtval = a,
-            None    => throw(Error_internal_error)
+	    None()  => throw Error_internal_error()
           }
         },
         Illegal_Instr => {
           match (e.excinfo) {
             Some(a) => mtval = a,
-            None    => throw(Error_internal_error)
+	    None()  => throw Error_internal_error()
           }
         },
 
@@ -283,25 +284,25 @@ function handle_exception_ctl(cur_priv : privilege, ctl : ctl_result,
         Misaligned_Load => {
           match (e.excinfo) {
             Some(a) => mtval = a,
-            None    => throw(Error_internal_error)
+	    None()  => throw Error_internal_error()
           }
         },
         Load_Access => {
           match (e.excinfo) {
             Some(a) => mtval = a,
-            None    => throw(Error_internal_error)
+	    None()  => throw Error_internal_error()
           }
         },
         Misaligned_Store => {
           match (e.excinfo) {
             Some(a) => mtval = a,
-            None    => throw(Error_internal_error)
+	    None()  => throw Error_internal_error()
           }
         },
         Store_Access => {
           match (e.excinfo) {
             Some(a) => mtval = a,
-            None    => throw(Error_internal_error)
+	    None()  => throw Error_internal_error()
           }
         },
 
@@ -318,27 +319,27 @@ function handle_exception_ctl(cur_priv : privilege, ctl : ctl_result,
         Fetch_PageFault => {
           match (e.excinfo) {
             Some(a) => mtval = a,
-            None    => throw(Error_internal_error)
+	    None()  => throw Error_internal_error()
           }
         },
         Load_PageFault => {
           match (e.excinfo) {
             Some(a) => mtval = a,
-            None    => throw(Error_internal_error)
+	    None()  => throw Error_internal_error()
           }
         },
         Store_PageFault => {
           match (e.excinfo) {
             Some(a) => mtval = a,
-            None    => throw(Error_internal_error)
+	    None()  => throw Error_internal_error()
           }
         },
-        _ => throw(Error_internal_error) /* Don't expect ReservedExc0 etc. here */
+        _ => throw Error_internal_error() /* Don't expect ReservedExc0 etc. here */
       };
       /* TODO: make register read explicit */
       mtvec
     },
-    (_, CTL_MRET) => {
+    (_, CTL_MRET()) => {
       mstatus->MIE()  = mstatus.MPIE();
       mstatus->MPIE() = true;
       cur_privilege   = bits_to_priv(mstatus.MPP());
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index 944c7455..8799f580 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -5,7 +5,7 @@ function not_implemented message = throw(Error_not_implemented(message))
 val internal_error : forall ('a : Type). string -> 'a effect {escape}
 function internal_error(s) = {
     assert (false, s);
-    throw (Error_internal_error)
+    throw Error_internal_error()
 }
 
 let xlen = 64
@@ -51,7 +51,7 @@ function wX (r, v) =
 overload X = {rX, wX}
 
 function check_alignment (addr : xlenbits, width : atom('n)) -> forall 'n. unit =
-  if unsigned(addr) % width != 0 then throw(Error_misaligned_access) else ()
+  if unsigned(addr) % width != 0 then throw Error_misaligned_access() else ()
 
 val MEMr                         : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
 val MEMr_acquire                 : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}