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}