Got riscv spec to typecheck with sail2

Fix a typechecking bug involving constraints attached to type synonyms
within existentials.

4 files changed, 272 insertions, 243 deletions

diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index b4e36507..ff11cf7e 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -276,9 +276,11 @@ val cast ex_int : int -> {'n, true. atom('n)}
 
 function ex_int 'n = n
 
+/*
 val cast ex_range : forall 'n 'm. range('n, 'm) -> {'o, 'n <= 'o <= 'm. atom('o)}
 
 function ex_range (n as 'N) = n
+*/
 
 val coerce_int_nat : int -> nat effect {escape}
 
@@ -297,6 +299,7 @@ val print_int = "print_int" : (string, int) -> unit
 union exception = {
   Error_not_implemented : string,
   Error_misaligned_access,
+  Error_EBREAK,
 }
 
 val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
@@ -313,4 +316,16 @@ function operator <_u  (x : bits('n), y : bits('n)) -> forall 'n. bool = unsigne
 function operator >=_u (x : bits('n), y : bits('n)) -> forall 'n. bool = unsigned(x) >= unsigned(y)
 
 val cast bool_to_bits : bool -> bits(1)
-function bool_to_bits x = if x then 0b1 else 0b0
\ No newline at end of file
+function bool_to_bits x = if x then 0b1 else 0b0
+
+val cast bit_to_bool : bit -> bool
+function bit_to_bool bitone  = true
+and      bit_to_bool bitzero = false
+
+infix 7 >>
+infix 7 <<
+
+val operator >> : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
+val operator << : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
+
+val vector64 : int -> bits(64)
\ No newline at end of file
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index 00dbb190..f05bb2be 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -3,10 +3,10 @@ scattered union ast
 val decode : bits(32) -> option(ast) effect pure
 scattered function decode
 
-val execute : ast -> unit effect {escape, wreg, rreg}
+val execute : ast -> unit effect {escape, wreg, rreg, wmv, eamem, rmem, barr, exmem}
 scattered function execute
 
-/* *******************************************************************/
+/* ****************************************************************** */
 
 union clause ast = UTYPE : (bits(20), regbits, uop)
 
@@ -21,7 +21,7 @@ function clause execute UTYPE(imm, rd, op) =
     } in
     wGPR(rd, ret)
 
-/* *******************************************************************/
+/* ****************************************************************** */
 
 union clause ast = RISCV_JAL : (bits(21), regbits)
 
@@ -34,7 +34,7 @@ function clause execute (RISCV_JAL(imm, rd)) = {
     nextPC = pc + offset;
 }
 
-/* *******************************************************************/
+/* ****************************************************************** */
 union clause ast = RISCV_JALR : (bits(12), regbits, regbits)
 
 function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b1100111 =
@@ -47,7 +47,7 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = {
     nextPC = newPC[63..1] @ 0b0;
 }
 
-/* *******************************************************************/
+/* ****************************************************************** */
 union clause ast = BTYPE : (bits(13), regbits, regbits, bop)
 
 function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b000 @ imm5 : bits(5) @ 0b1100011 = Some(BTYPE(imm7[6] @ imm5[0] @ imm7[5..0] @ imm5[4..1] @ 0b0, rs2, rs1, RISCV_BEQ))
@@ -71,7 +71,7 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) =
   if taken then
     nextPC = PC + EXTS(imm)
 
-/* *******************************************************************/
+/* ****************************************************************** */
 union clause ast = ITYPE : (bits(12), regbits, regbits, iop)
 
 function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0010011 = Some(ITYPE(imm, rs1, rd, RISCV_ADDI))
@@ -93,312 +93,299 @@ function clause execute (ITYPE (imm, rs1, rd, op)) =
     RISCV_ANDI  => rs1_val & imm64
   } in
   wGPR(rd, result)
-/*
-(********************************************************************)
-union ast member ((bits(6)), regbits, regbits, sop) SHIFTIOP
 
-function clause decode (0b000000 @ (bits(6)) shamt @ (regbits) rs1 @ 0b001 @ (regbits) rd @ 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SLLI))
-function clause decode (0b000000 @ (bits(6)) shamt @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SRLI))
-function clause decode (0b010000 @ (bits(6)) shamt @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SRAI))
+/* ****************************************************************** */
+union clause ast = SHIFTIOP : (bits(6), regbits, regbits, sop)
+
+function clause decode 0b000000 @ shamt : bits(6) @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0010011 = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SLLI))
+function clause decode 0b000000 @ shamt : bits(6) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0010011 = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SRLI))
+function clause decode 0b010000 @ shamt : bits(6) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0010011 = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SRAI))
 
 function clause execute (SHIFTIOP(shamt, rs1, rd, op)) = 
     let rs1_val = rGPR(rs1) in
-    let result = switch(op) {
-      case RISCV_SLLI -> rs1_val >> shamt
-      case RISCV_SRLI -> rs1_val << shamt
-      case RISCV_SRAI -> shift_right_arith64(rs1_val, shamt)
+    let result : bits(64) = match op {
+      RISCV_SLLI => rs1_val >> shamt,
+      RISCV_SRLI => rs1_val << shamt,
+      RISCV_SRAI => shift_right_arith64(rs1_val, shamt)
     } in
     wGPR(rd, result)
 
-(********************************************************************)
-union ast member (regbits, regbits, regbits, rop) RTYPE
 
-function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b000 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_ADD))
-function clause decode (0b0100000 @ (regbits) rs2 @ (regbits) rs1 @ 0b000 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SUB))
-function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b001 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SLL))
-function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SLT))
-function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SLTU))
-function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b100 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_XOR))
-function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SRL))
-function clause decode (0b0100000 @ (regbits) rs2 @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SRA))
-function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b110 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_OR))
-function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b111 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_AND))
+/* ****************************************************************** */
+union clause ast = RTYPE : (regbits, regbits, regbits, rop)
+
+function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_ADD))
+function clause decode 0b0100000 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SUB))
+function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SLL))
+function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SLT))
+function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SLTU))
+function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b100 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_XOR))
+function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SRL))
+function clause decode 0b0100000 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SRA))
+function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_OR))
+function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b111 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_AND))
+
 
 function clause execute (RTYPE(rs2, rs1, rd, op)) =
   let rs1_val = rGPR(rs1) in
   let rs2_val = rGPR(rs2) in
-  let (bits(64)) result = switch(op) {
-    case RISCV_ADD  -> rs1_val + rs2_val
-    case RISCV_SUB  -> rs1_val - rs2_val
-    case RISCV_SLL  -> rs1_val << (rs2_val[5..0])
-    case RISCV_SLT  -> EXTZ(rs1_val <_s rs2_val)
-    case RISCV_SLTU -> EXTZ(rs1_val <_u rs2_val)
-    case RISCV_XOR  -> rs1_val ^ rs2_val
-    case RISCV_SRL  -> rs1_val >> (rs2_val[5..0])
-    case RISCV_SRA  -> shift_right_arith64(rs1_val, rs2_val[5..0])
-    case RISCV_OR   -> rs1_val | rs2_val
-    case RISCV_AND  -> rs1_val & rs2_val
+  let result : bits(64) = match op {
+    RISCV_ADD  => rs1_val + rs2_val,
+    RISCV_SUB  => rs1_val - rs2_val,
+    RISCV_SLL  => rs1_val << (rs2_val[5..0]),
+    RISCV_SLT  => EXTZ(rs1_val <_s rs2_val),
+    RISCV_SLTU => EXTZ(rs1_val <_u rs2_val),
+    RISCV_XOR  => rs1_val ^ rs2_val,
+    RISCV_SRL  => rs1_val >> (rs2_val[5..0]),
+    RISCV_SRA  => shift_right_arith64(rs1_val, rs2_val[5..0]),
+    RISCV_OR   => rs1_val | rs2_val,
+    RISCV_AND  => rs1_val & rs2_val
   } in
   wGPR(rd, result)
 
-(********************************************************************)
-union ast member ((bits(12)), regbits, regbits, bool, word_width, bool, bool) LOAD
+/* ****************************************************************** */
+union clause ast = LOAD : (bits(12), regbits, regbits, bool, word_width, bool, bool)
+
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, false, BYTE,   false, false))
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, false, HALF,   false, false))
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, false, WORD,   false, false))
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, false, DOUBLE, false, false))
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b100 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, true,  BYTE,   false, false))
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, true,  HALF,   false, false))
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, true,  WORD,   false, false))
 
-function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b000 @ (regbits) rd @ 0b0000011) = Some(LOAD(imm, rs1, rd, false, BYTE,   false, false))
-function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b001 @ (regbits) rd @ 0b0000011) = Some(LOAD(imm, rs1, rd, false, HALF,   false, false))
-function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0000011) = Some(LOAD(imm, rs1, rd, false, WORD,   false, false))
-function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0000011) = Some(LOAD(imm, rs1, rd, false, DOUBLE, false, false))
-function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b100 @ (regbits) rd @ 0b0000011) = Some(LOAD(imm, rs1, rd, true,  BYTE,   false, false))
-function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0000011) = Some(LOAD(imm, rs1, rd, true,  HALF,   false, false))
-function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b110 @ (regbits) rd @ 0b0000011) = Some(LOAD(imm, rs1, rd, true,  WORD,   false, false))
 
 function clause execute(LOAD(imm, rs1, rd, unsigned, width, aq, rl)) =
-    let (bits(64)) addr = rGPR(rs1) + EXTS(imm) in
-    let (bits(64)) result = if unsigned then 
-        switch (width) {
-          case BYTE   -> EXTZ(mem_read(addr, 1, aq, rl, false))
-          case HALF   -> EXTZ(mem_read(addr, 2, aq, rl, false))
-          case WORD   -> EXTZ(mem_read(addr, 4, aq, rl, false))
-          case DOUBLE -> mem_read(addr, 8, aq, rl, false)
+    let addr : bits(64) = rGPR(rs1) + EXTS(imm) in
+    let result : bits(64) = if unsigned then
+        match width {
+	  BYTE   => EXTZ(mem_read(addr, 1, aq, rl, false)),
+	  HALF   => EXTZ(mem_read(addr, 2, aq, rl, false)),
+	  WORD   => EXTZ(mem_read(addr, 4, aq, rl, false)),
+	  DOUBLE => mem_read(addr, 8, aq, rl, false)
         }
       else
-        switch (width) {
-          case BYTE   -> EXTS(mem_read(addr, 1, aq, rl, false))
-          case HALF   -> EXTS(mem_read(addr, 2, aq, rl, false))
-          case WORD   -> EXTS(mem_read(addr, 4, aq, rl, false))
-          case DOUBLE -> mem_read(addr, 8, aq, rl, false)
+        match width {
+	  BYTE   => EXTS(mem_read(addr, 1, aq, rl, false)),
+	  HALF   => EXTS(mem_read(addr, 2, aq, rl, false)),
+	  WORD   => EXTS(mem_read(addr, 4, aq, rl, false)),
+	  DOUBLE => mem_read(addr, 8, aq, rl, false)
         } in
     wGPR(rd, result)
 
-(********************************************************************)
-union ast member ((bits(12)), regbits, regbits, word_width, bool, bool) STORE
+/* ****************************************************************** */
+union clause ast = STORE : (bits(12), regbits, regbits, word_width, bool, bool)
 
-function clause decode ((bits(7)) imm7 @ (regbits) rs2 @ (regbits) rs1 @ 0b000 @ (bits(5)) imm5 @ 0b0100011) =
-  Some(STORE(imm7 @ imm5, rs2, rs1, BYTE, false, false))
-function clause decode ((bits(7)) imm7 @ (regbits) rs2 @ (regbits) rs1 @ 0b001 @ (bits(5)) imm5 @ 0b0100011) =
-  Some(STORE(imm7 @ imm5, rs2, rs1, HALF, false, false))
-function clause decode ((bits(7)) imm7 @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (bits(5)) imm5 @ 0b0100011) =
-  Some(STORE(imm7 @ imm5, rs2, rs1, WORD, false, false))
-function clause decode ((bits(7)) imm7 @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (bits(5)) imm5 @ 0b0100011) =
-  Some(STORE(imm7 @ imm5, rs2, rs1, DOUBLE, false, false))
+function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b000 @ imm5 : bits(5) @ 0b0100011 = Some(STORE(imm7 @ imm5, rs2, rs1, BYTE, false, false))
+function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b001 @ imm5 : bits(5) @ 0b0100011 = Some(STORE(imm7 @ imm5, rs2, rs1, HALF, false, false))
+function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b010 @ imm5 : bits(5) @ 0b0100011 = Some(STORE(imm7 @ imm5, rs2, rs1, WORD, false, false))
+function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b011 @ imm5 : bits(5) @ 0b0100011 = Some(STORE(imm7 @ imm5, rs2, rs1, DOUBLE, false, false))
 
 function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) =
-    let (bits(64)) addr = rGPR(rs1) + EXTS(imm) in {
-      switch (width) {
-        case BYTE   -> mem_write_ea(addr, 1, aq, rl, false)
-        case HALF   -> mem_write_ea(addr, 2, aq, rl, false)
-        case WORD   -> mem_write_ea(addr, 4, aq, rl, false)
-        case DOUBLE -> mem_write_ea(addr, 8, aq, rl, false)
+    let addr : bits(64) = rGPR(rs1) + EXTS(imm) in {
+      match width {
+	BYTE   => mem_write_ea(addr, 1, aq, rl, false),
+	HALF   => mem_write_ea(addr, 2, aq, rl, false),
+	WORD   => mem_write_ea(addr, 4, aq, rl, false),
+	DOUBLE => mem_write_ea(addr, 8, aq, rl, false)
       };
       let rs2_val = rGPR(rs2) in
-      switch (width) {
-        case BYTE   -> mem_write_value(addr, 1, rs2_val[7..0],  aq, rl, false)
-        case HALF   -> mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false)
-        case WORD   -> mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false)
-        case DOUBLE -> mem_write_value(addr, 8, rs2_val,        aq, rl, false)
+      match width {
+	BYTE   => mem_write_value(addr, 1, rs2_val[7..0],  aq, rl, false),
+	HALF   => mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false),
+	WORD   => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false),
+	DOUBLE => mem_write_value(addr, 8, rs2_val,        aq, rl, false)
       }
     }
 
-(********************************************************************)
-union ast member ((bits(12)), regbits, regbits) ADDIW
 
-function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b000 @ (regbits) rd @ 0b0011011) =
-  Some(ADDIW(imm, rs1, rd))
+/* ****************************************************************** */
+union clause ast = ADDIW : (bits(12), regbits, regbits)
+
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0011011 = Some(ADDIW(imm, rs1, rd))
 
 function clause execute (ADDIW(imm, rs1, rd)) =
-  let (bits(64)) imm64 = EXTS(imm) in
-  let (bits(64)) result64 = imm64 + rGPR(rs1) in
-  let (bits(64)) result32 = EXTS(result64[31..0]) in
+  let imm64 : bits(64) = EXTS(imm) in
+  let result64 : bits(64) = imm64 + rGPR(rs1) in
+  let result32 : bits(64) = EXTS(result64[31..0]) in
   wGPR(rd, result32)
 
-(********************************************************************)
-union ast member ((bits(5)), regbits, regbits, sop) SHIFTW
+/* ****************************************************************** */
+union clause ast = SHIFTW : (bits(5), regbits, regbits, sop)
 
-function clause decode (0b0000000 @ (bits(5)) shamt @ (regbits) rs1 @ 0b001 @ (regbits) rd @ 0b0011011) = Some(SHIFTW(shamt, rs1, rd, RISCV_SLLI))
-function clause decode (0b0000000 @ (bits(5)) shamt @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0011011) = Some(SHIFTW(shamt, rs1, rd, RISCV_SRLI))
-function clause decode (0b0100000 @ (bits(5)) shamt @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0011011) = Some(SHIFTW(shamt, rs1, rd, RISCV_SRAI))
+function clause decode 0b0000000 @ shamt : bits(5) @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0011011 = Some(SHIFTW(shamt, rs1, rd, RISCV_SLLI))
+function clause decode 0b0000000 @ shamt : bits(5) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0011011 = Some(SHIFTW(shamt, rs1, rd, RISCV_SRLI))
+function clause decode 0b0100000 @ shamt : bits(5) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0011011 = Some(SHIFTW(shamt, rs1, rd, RISCV_SRAI))
 
-function clause execute (SHIFTW(shamt, rs1, rd, op)) = 
+function clause execute (SHIFTW(shamt, rs1, rd, op)) =
     let rs1_val = (rGPR(rs1))[31..0] in
-    let result = switch(op) {
-      case RISCV_SLLI -> rs1_val >> shamt
-      case RISCV_SRLI -> rs1_val << shamt
-      case RISCV_SRAI -> shift_right_arith32(rs1_val, shamt)
+    let result : bits(32) = match op {
+      RISCV_SLLI => rs1_val >> shamt,
+      RISCV_SRLI => rs1_val << shamt,
+      RISCV_SRAI => shift_right_arith32(rs1_val, shamt)
     } in
     wGPR(rd, EXTS(result))
 
-(********************************************************************)
-union ast member (regbits, regbits, regbits, ropw) RTYPEW
+/* ****************************************************************** */
+union clause ast = RTYPEW : (regbits, regbits, regbits, ropw)
 
-function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b000 @ (regbits) rd @ 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_ADDW))
-function clause decode (0b0100000 @ (regbits) rs2 @ (regbits) rs1 @ 0b000 @ (regbits) rd @ 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_SUBW))
-function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b001 @ (regbits) rd @ 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_SLLW))
-function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_SRLW))
-function clause decode (0b0100000 @ (regbits) rs2 @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_SRAW))
+function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0111011 = Some(RTYPEW(rs2, rs1, rd, RISCV_ADDW))
+function clause decode 0b0100000 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0111011 = Some(RTYPEW(rs2, rs1, rd, RISCV_SUBW))
+function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0111011 = Some(RTYPEW(rs2, rs1, rd, RISCV_SLLW))
+function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0111011 = Some(RTYPEW(rs2, rs1, rd, RISCV_SRLW))
+function clause decode 0b0100000 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0111011 = Some(RTYPEW(rs2, rs1, rd, RISCV_SRAW))
 
 function clause execute (RTYPEW(rs2, rs1, rd, op)) =
   let rs1_val = (rGPR(rs1))[31..0] in
   let rs2_val = (rGPR(rs2))[31..0] in
-  let (bits(32)) result = switch(op) {
-    case RISCV_ADDW -> rs1_val + rs2_val
-    case RISCV_SUBW -> rs1_val - rs2_val
-    case RISCV_SLLW -> rs1_val << (rs2_val[4..0])
-    case RISCV_SRLW -> rs1_val >> (rs2_val[4..0])
-    case RISCV_SRAW -> shift_right_arith32(rs1_val, rs2_val[4..0])
+  let result : bits(32) = match op {
+    RISCV_ADDW => rs1_val + rs2_val,
+    RISCV_SUBW => rs1_val - rs2_val,
+    RISCV_SLLW => rs1_val << (rs2_val[4..0]),
+    RISCV_SRLW => rs1_val >> (rs2_val[4..0]),
+    RISCV_SRAW => shift_right_arith32(rs1_val, rs2_val[4..0])
   } in
   wGPR(rd, EXTS(result))
 
-(********************************************************************)
-union ast member (bits(4), bits(4)) FENCE
+/* ****************************************************************** */
+union clause ast = FENCE : (bits(4), bits(4))
 
-function clause decode (0b0000 @ (bits(4)) pred @ (bits(4)) succ @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111) = Some(FENCE (pred, succ))
+function clause decode 0b0000 @ pred : bits(4) @ succ : bits(4) @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111 = Some(FENCE(pred, succ))
 
 function clause execute (FENCE(pred, succ)) = {
-  switch(pred, succ) {
-    case (0b0011, 0b0011) -> MEM_fence_rw_rw()
-    case (0b0010, 0b0011) -> MEM_fence_r_rw()
-    case (0b0010, 0b0010) -> MEM_fence_r_r()
-    case (0b0011, 0b0001) -> MEM_fence_rw_w()
-    case (0b0001, 0b0001) -> MEM_fence_w_w()
-    case _ -> not_implemented("unsupported fence")
+  match (pred, succ) {
+    (0b0011, 0b0011) => MEM_fence_rw_rw(),
+    (0b0010, 0b0011) => MEM_fence_r_rw(),
+    (0b0010, 0b0010) => MEM_fence_r_r(),
+    (0b0011, 0b0001) => MEM_fence_rw_w(),
+    (0b0001, 0b0001) => MEM_fence_w_w(),
+    _ => not_implemented("unsupported fence")
   }
 }
 
-(********************************************************************)
-union ast member unit FENCEI
-function clause decode (0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111) = Some(FENCEI)
+/* ****************************************************************** */
+union clause ast = FENCEI
+
+function clause decode 0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111 = Some(FENCEI)
+
 function clause execute FENCEI = MEM_fence_i()
 
-(********************************************************************)
-union ast member unit ECALL
-function clause decode (0b000000000000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011) = Some(ECALL ())
+/* ****************************************************************** */
+union clause ast = ECALL
+
+function clause decode 0b000000000000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(ECALL)
+
 function clause execute ECALL = not_implemented("ECALL is not implemented")
 
-(********************************************************************)
-union ast member unit EBREAK
-function clause decode (0b000000000001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011) = Some(EBREAK ())
-function clause execute EBREAK = { exit () }
+/* ****************************************************************** */
+union clause ast = EBREAK
+
+function clause decode 0b000000000001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(EBREAK)
 
-(********************************************************************)
-union ast member (bool, bool, regbits, word_width, regbits) LOADRES
+function clause execute EBREAK = { throw(Error_EBREAK) }
+
+/* ****************************************************************** */
+union clause ast = LOADRES : (bool, bool, regbits, word_width, regbits)
+
+function clause decode 0b00010 @ [aq] @ [rl] @ 0b00000 @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(LOADRES(aq, rl, rs1, WORD, rd))
+function clause decode 0b00010 @ [aq] @ [rl] @ 0b00000 @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(LOADRES(aq, rl, rs1, DOUBLE, rd))
 
-function clause decode (0b00010 @ [aq] @ [rl] @ 0b00000 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) = Some(LOADRES(aq, rl, rs1, WORD, rd))
-function clause decode (0b00010 @ [aq] @ [rl] @ 0b00000 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) = Some(LOADRES(aq, rl, rs1, DOUBLE, rd))
 function clause execute(LOADRES(aq, rl, rs1, width, rd)) =
-  let (bits(64)) addr = rGPR(rs1) in
-  let (bits(64)) result =
-      switch width {
-        case WORD   -> EXTS(mem_read(addr, 4, aq, rl, true))
-        case DOUBLE -> mem_read(addr, 8, aq, rl, true)
+  let addr : bits(64) = rGPR(rs1) in
+  let result : bits(64) =
+      match width {
+	WORD   => EXTS(mem_read(addr, 4, aq, rl, true)),
+	DOUBLE => mem_read(addr, 8, aq, rl, true)
       } in
   wGPR(rd, result)
 
-(********************************************************************)
-union ast member (bool, bool, regbits, regbits, word_width, regbits) STORECON
+/* ****************************************************************** */
+union clause ast = STORECON : (bool, bool, regbits, regbits, word_width, regbits)
 
-function clause decode (0b00011 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) =
-  Some(STORECON(aq, rl, rs2, rs1, WORD, rd))
-function clause decode (0b00011 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) =
-  Some(STORECON(aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode 0b00011 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(STORECON(aq, rl, rs2, rs1, WORD, rd))
+function clause decode 0b00011 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(STORECON(aq, rl, rs2, rs1, DOUBLE, rd))
 
 function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
-  (*(bit)*) status = if speculate_conditional_success() then 0 else 1;
-  wGPR(rd) = (bits(64)) (EXTZ([status]));
-
-  if status == 1 then () else {
-    (bits(64)) addr = rGPR(rs1);
-    switch width {
-      case WORD   -> mem_write_ea(addr, 4, aq, rl, true)
-      case DOUBLE -> mem_write_ea(addr, 8, aq, rl, true)
+  status : bits(1) = if speculate_conditional_success() then 0b0 else 0b1;
+  wGPR(rd) = EXTZ(status);
+
+  if status == 0b1 then () else {
+    addr : bits(64) = rGPR(rs1);
+    match width {
+      WORD   => mem_write_ea(addr, 4, aq, rl, true),
+      DOUBLE => mem_write_ea(addr, 8, aq, rl, true)
     };
     rs2_val = rGPR(rs2);
-    switch width {
-      case WORD   -> mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true)
-      case DOUBLE -> mem_write_value(addr, 8, rs2_val,        aq, rl, true)
+    match width {
+      WORD   => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true),
+      DOUBLE => mem_write_value(addr, 8, rs2_val,        aq, rl, true)
     };
   };
 }
 
-(********************************************************************)
-union ast member (amoop, bool, bool, regbits, regbits, word_width, regbits) AMO
-
-function clause decode (0b00001 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) =
-  Some(AMO(AMOSWAP, aq, rl, rs2, rs1, WORD,   rd))
-function clause decode (0b00001 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) =
-  Some(AMO(AMOSWAP, aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode (0b00000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) =
-  Some(AMO(AMOADD , aq, rl, rs2, rs1, WORD,   rd))
-function clause decode (0b00000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) =
-  Some(AMO(AMOADD , aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode (0b00100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) =
-  Some(AMO(AMOXOR , aq, rl, rs2, rs1, WORD,   rd))
-function clause decode (0b00100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) =
-  Some(AMO(AMOXOR , aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode (0b01100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) =
-  Some(AMO(AMOAND , aq, rl, rs2, rs1, WORD,   rd))
-function clause decode (0b01100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) =
-  Some(AMO(AMOAND , aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode (0b01000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) =
-  Some(AMO(AMOOR  , aq, rl, rs2, rs1, WORD,   rd))
-function clause decode (0b01000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) =
-  Some(AMO(AMOOR  , aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode (0b10000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) =
-  Some(AMO(AMOMIN , aq, rl, rs2, rs1, WORD,   rd))
-function clause decode (0b10000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) =
-  Some(AMO(AMOMIN , aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode (0b10100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) =
-  Some(AMO(AMOMAX , aq, rl, rs2, rs1, WORD,   rd))
-function clause decode (0b10100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) =
-  Some(AMO(AMOMAX , aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode (0b11000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) =
-  Some(AMO(AMOMINU, aq, rl, rs2, rs1, WORD,   rd))
-function clause decode (0b11000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) =
-  Some(AMO(AMOMINU, aq, rl, rs2, rs1, DOUBLE, rd))
-function clause decode (0b11100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) =
-  Some(AMO(AMOMAXU, aq, rl, rs2, rs1, WORD,   rd))
-function clause decode (0b11100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) =
-  Some(AMO(AMOMAXU, aq, rl, rs2, rs1, DOUBLE, rd))
+/* ****************************************************************** */
+union clause ast = AMO : (amoop, bool, bool, regbits, regbits, word_width, regbits)
+
+function clause decode 0b00001 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOSWAP, aq, rl, rs2, rs1, WORD,   rd))
+function clause decode 0b00001 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOSWAP, aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode 0b00000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOADD , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode 0b00000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOADD , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode 0b00100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOXOR , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode 0b00100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOXOR , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode 0b01100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOAND , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode 0b01100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOAND , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode 0b01000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOOR  , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode 0b01000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOOR  , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode 0b10000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMIN , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode 0b10000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMIN , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode 0b10100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMAX , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode 0b10100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMAX , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode 0b11000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMINU, aq, rl, rs2, rs1, WORD,   rd))
+function clause decode 0b11000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMINU, aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode 0b11100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMAXU, aq, rl, rs2, rs1, WORD,   rd))
+function clause decode 0b11100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMAXU, aq, rl, rs2, rs1, DOUBLE, rd))
 
 function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
-  (bits(64)) addr = rGPR(rs1);
+  addr : bits(64) = rGPR(rs1);
 
-  switch (width) {
-    case WORD   -> mem_write_ea(addr, 4, aq & rl, rl, true)
-    case DOUBLE -> mem_write_ea(addr, 8, aq & rl, rl, true)
+  match width {
+    WORD   => mem_write_ea(addr, 4, aq & rl, rl, true),
+    DOUBLE => mem_write_ea(addr, 8, aq & rl, rl, true)
   };
 
-  (bits(64)) loaded =
-    switch (width) {
-      case WORD   -> EXTS(mem_read(addr, 4, aq, aq & rl, true))
-      case DOUBLE -> mem_read(addr, 8, aq, aq & rl, true)
+  loaded : bits(64) =
+    match width {
+      WORD   => EXTS(mem_read(addr, 4, aq, aq & rl, true)),
+      DOUBLE => mem_read(addr, 8, aq, aq & rl, true)
     };
-  wGPR(rd, loaded);
-
-  (bits(64)) rs2_val = rGPR(rs2);
-  (bits(64)) result =
-    switch(op) {
-      case AMOSWAP -> rs2_val
-      case AMOADD  -> rs2_val + loaded
-      case AMOXOR  -> rs2_val ^ loaded
-      case AMOAND  -> rs2_val & loaded
-      case AMOOR   -> rs2_val | loaded
-
-      case AMOMIN  -> (bits(64)) (min(signed(rs2_val),   signed(loaded)))
-      case AMOMAX  -> (bits(64)) (max(signed(rs2_val),   signed(loaded)))
-      case AMOMINU -> (bits(64)) (min(unsigned(rs2_val), unsigned(loaded)))
-      case AMOMAXU -> (bits(64)) (max(unsigned(rs2_val), unsigned(loaded)))
+  wGPR(rd) = loaded;
+
+  rs2_val : bits(64) = rGPR(rs2);
+  result : bits(64) =
+    match op {
+      AMOSWAP => rs2_val,
+      AMOADD  => rs2_val + loaded,
+      AMOXOR  => rs2_val ^ loaded,
+      AMOAND  => rs2_val & loaded,
+      AMOOR   => rs2_val | loaded,
+
+      /* Have to convert number to vector here. Check this */
+      AMOMIN  => vector64(min(signed(rs2_val),   signed(loaded))),
+      AMOMAX  => vector64(max(signed(rs2_val),   signed(loaded))),
+      AMOMINU => vector64(min(unsigned(rs2_val), unsigned(loaded))),
+      AMOMAXU => vector64(max(unsigned(rs2_val), unsigned(loaded)))
     };
 
-  switch (width) {
-    case WORD   -> mem_write_value(addr, 4, result[31..0], aq & rl, rl, true)
-    case DOUBLE -> mem_write_value(addr, 8, result,        aq & rl, rl, true)
+  match width {
+    WORD   => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true),
+    DOUBLE => mem_write_value(addr, 8, result,        aq & rl, rl, true)
   };
 }
 
-(********************************************************************)
+/* ****************************************************************** */
 
 function clause decode _ = None
-*/
+
 end ast
 end decode
 end execute
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index a593792d..b1b070bb 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -6,8 +6,9 @@ type regval = bits(64)
 
 type regno ('n : Int), 0 <= 'n < 32 = atom('n)
 type regbits = bits(5)
-val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. atom('n)}
-function regbits_to_regno n = unsigned(n)
+
+val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)}
+function regbits_to_regno n = let 'N = unsigned(n) in N
 
 /* register x0 : regval is hard-wired zero */
 register x1 : regval
@@ -166,13 +167,10 @@ enum word_width = {BYTE, HALF, WORD, DOUBLE}
 
 /* Ideally these would be sail builtin */
 
-/*
-function (bit[64]) shift_right_arith64 ((bit[64]) v, (bit[6]) shift) =
-    let (bit[128]) v128 = EXTS(v) in
+function shift_right_arith64 (v : bits(64), shift : bits(6)) -> bits(64) =
+    let v128 : bits(128) = EXTS(v) in
     (v128 >> shift)[63..0]
 
-function (bit[32]) shift_right_arith32 ((bit[32]) v, (bit[5]) shift) =
-    let (bit[64]) v64 = EXTS(v) in
-    (v64 >> shift)[31..0]
-
-*/
+function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) =
+    let v64 : bits(64) = EXTS(v) in
+    (v64 >> shift)[31..0]
\ No newline at end of file
diff --git a/src/type_check.ml b/src/type_check.ml
index 04c16ad5..27f6d8a2 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -504,6 +504,7 @@ end = struct
     else typ_error (id_loc id) ("Could not prove " ^ string_of_list ", " string_of_n_constraint ncs ^ " for type constructor " ^ string_of_id id)
 
   let rec expand_synonyms env (Typ_aux (typ, l) as t) =
+    typ_debug ("Expanding synonyms for " ^ string_of_typ t);
     match typ with
     | Typ_tup typs -> Typ_aux (Typ_tup (List.map (expand_synonyms env) typs), l)
     | Typ_fn (typ1, typ2, effs) -> Typ_aux (Typ_fn (expand_synonyms env typ1, expand_synonyms env typ2, effs), l)
@@ -523,7 +524,31 @@ end = struct
          with
          | Not_found -> Typ_aux (Typ_id id, l)
        end
-    | typ -> Typ_aux (typ, l)
+    | Typ_exist (kids, nc, typ) ->
+       (* When expanding an existential synonym we need to take care
+          to add the type variables and constraints to the
+          environment, so we can check constraints attached to type
+          synonyms within the existential. Furthermore, we must take
+          care to avoid clobbering any existing type variables in
+          scope while doing this. *)
+       let rebindings = ref [] in
+
+       let rename_kid kid = if KBindings.mem kid env.typ_vars then prepend_kid "syn#" kid else kid in
+       let add_typ_var env kid =
+         if KBindings.mem kid env.typ_vars then
+           (rebindings := kid :: !rebindings; { env with typ_vars = KBindings.add (prepend_kid "syn#" kid) BK_nat env.typ_vars })
+         else
+           { env with typ_vars = KBindings.add kid BK_nat env.typ_vars }
+       in
+
+       let env = List.fold_left add_typ_var env kids in
+       let kids = List.map rename_kid kids in
+       let nc = List.fold_left (fun nc kid -> nc_subst_nexp kid (Nexp_var (prepend_kid "syn#" kid)) nc) nc !rebindings in
+       let typ = List.fold_left (fun typ kid -> typ_subst_nexp kid (Nexp_var (prepend_kid "syn#" kid)) typ) typ !rebindings in
+       typ_print ("Synonym existential: {" ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ ^ "}");
+       let env = { env with constraints = nc :: env.constraints } in
+       Typ_aux (Typ_exist (kids, nc, expand_synonyms env typ), l)
+    | Typ_var v -> Typ_aux (Typ_var v, l)
   and expand_synonyms_arg env (Typ_arg_aux (typ_arg, l)) =
     match typ_arg with
     | Typ_arg_typ typ -> Typ_arg_aux (Typ_arg_typ (expand_synonyms env typ), l)
@@ -551,7 +576,8 @@ end = struct
     | Typ_app (id, _) -> typ_error l ("Undefined type " ^ string_of_id id)
     | Typ_exist ([], _, _) -> typ_error l ("Existential must have some type variables")
     | Typ_exist (kids, nc, typ) when KidSet.is_empty exs ->
-       wf_constraint ~exs:(KidSet.of_list kids) env nc; wf_typ ~exs:(KidSet.of_list kids) env typ
+       wf_constraint ~exs:(KidSet.of_list kids) env nc;
+       wf_typ ~exs:(KidSet.of_list kids) { env with constraints = nc :: env.constraints } typ
     | Typ_exist (_, _, _) -> typ_error l ("Nested existentials are not allowed")
   and wf_typ_arg ?exs:(exs=KidSet.empty) env (Typ_arg_aux (typ_arg_aux, _)) =
     match typ_arg_aux with
@@ -625,10 +651,11 @@ end = struct
     with
     | Not_found -> typ_error (id_loc id) ("No val spec found for " ^ string_of_id id)
 
-  let update_val_spec id bind env =
+  let update_val_spec id (typq, typ) env =
     begin
-      typ_print ("Adding val spec binding " ^ string_of_id id ^ " :: " ^ string_of_bind bind);
-      { env with top_val_specs = Bindings.add id bind env.top_val_specs }
+      let typ = expand_synonyms env typ in
+      typ_print ("Adding val spec binding " ^ string_of_id id ^ " :: " ^ string_of_bind (typq, typ));
+      { env with top_val_specs = Bindings.add id (typq, typ) env.top_val_specs }
     end
 
   let add_val_spec id bind env =
@@ -1430,11 +1457,9 @@ let merge_unifiers l kid uvar1 uvar2 =
   | None, None -> None
 
 let rec unify l env typ1 typ2 =
-  let typ1 = Env.expand_synonyms env typ1 in
-  let typ2 = Env.expand_synonyms env typ2 in
-
   typ_print ("Unify " ^ string_of_typ typ1 ^ " with " ^ string_of_typ typ2);
   let goals = KidSet.inter (KidSet.diff (typ_frees typ1) (typ_frees typ2)) (typ_frees typ1) in
+
   let rec unify_typ l (Typ_aux (typ1_aux, _) as typ1) (Typ_aux (typ2_aux, _) as typ2) =
     typ_debug ("UNIFYING TYPES " ^ string_of_typ typ1 ^ " AND " ^ string_of_typ typ2);
     match typ1_aux, typ2_aux with
@@ -1499,6 +1524,7 @@ let rec unify l env typ1 typ2 =
     | Typ_arg_order ord1, Typ_arg_order ord2 -> unify_order l ord1 ord2
     | _, _ -> unify_error l (string_of_typ_arg typ_arg1 ^ " cannot be unified with type argument " ^ string_of_typ_arg typ_arg2)
   in
+
   match destruct_exist env typ2 with
   | Some (kids, nc, typ2) ->
      let typ1, typ2 = Env.expand_synonyms env typ1, Env.expand_synonyms env typ2 in
@@ -1643,11 +1669,14 @@ let rec subtyp l env typ1 typ2 =
      let env = Env.add_constraint nc env in
      subtyp l env typ1 typ2
   | _, Some (kids, nc, typ2) ->
+     typ_debug "XXXXXXX";
      let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids in
+     typ_debug "YYYYYYY";
      let unifiers, existential_kids, existential_nc =
        try unify l env typ2 typ1 with
        | Unification_error (_, m) -> typ_error l m
      in
+     typ_debug "ZZZZZZZ";
      let nc = List.fold_left (fun nc (kid, uvar) -> nc_subst_uvar kid uvar nc) nc (KBindings.bindings unifiers) in
      let env = match existential_kids, existential_nc with
        | [], None -> env