added RISCV_ prefix to some values to stop Lem from renaming them

4 files changed, 140 insertions, 140 deletions

diff --git a/risc-v/hgen/herdtools_types_to_shallow_types.hgen b/risc-v/hgen/herdtools_types_to_shallow_types.hgen
index a63f9aed..e6edd24d 100644
--- a/risc-v/hgen/herdtools_types_to_shallow_types.hgen
+++ b/risc-v/hgen/herdtools_types_to_shallow_types.hgen
@@ -4,48 +4,48 @@ let translate_reg name value =
     Sail_values.to_vec0 is_inc (Nat_big_num.of_int 5,Nat_big_num.of_int (reg_to_int value))
 
 let translate_uop op = match op with
-  | RISCVLUI   -> LUI0
-  | RISCVAUIPC -> AUIPC
+  | RISCVLUI   -> RISCV_LUI
+  | RISCVAUIPC -> RISCV_AUIPC
 
 let translate_bop op = match op with
-  | RISCVBEQ  -> BEQ0
-  | RISCVBNE  -> BNE
-  | RISCVBLT  -> BLT
-  | RISCVBGE  -> BGE
-  | RISCVBLTU -> BLTU
-  | RISCVBGEU -> BGEU
+  | RISCVBEQ  -> RISCV_BEQ
+  | RISCVBNE  -> RISCV_BNE
+  | RISCVBLT  -> RISCV_BLT
+  | RISCVBGE  -> RISCV_BGE
+  | RISCVBLTU -> RISCV_BLTU
+  | RISCVBGEU -> RISCV_BGEU
 
 let translate_iop op = match op with
-  | RISCVADDI  -> ADDI0 
-  | RISCVSLTI  -> SLTI0
-  | RISCVSLTIU -> SLTIU0
-  | RISCVXORI  -> XORI0
-  | RISCVORI   -> ORI0
-  | RISCVANDI  -> ANDI0
+  | RISCVADDI  -> RISCV_ADDI
+  | RISCVSLTI  -> RISCV_SLTI
+  | RISCVSLTIU -> RISCV_SLTIU
+  | RISCVXORI  -> RISCV_XORI
+  | RISCVORI   -> RISCV_ORI
+  | RISCVANDI  -> RISCV_ANDI
 
 let translate_sop op = match op with
-  | RISCVSLLI -> SLLI
-  | RISCVSRLI -> SRLI
-  | RISCVSRAI -> SRAI
+  | RISCVSLLI -> RISCV_SLLI
+  | RISCVSRLI -> RISCV_SRLI
+  | RISCVSRAI -> RISCV_SRAI
 
 let translate_rop op = match op with
-  | RISCVADD  -> ADD0 
-  | RISCVSUB  -> SUB0 
-  | RISCVSLL  -> SLL0 
-  | RISCVSLT  -> SLT0 
-  | RISCVSLTU -> SLTU0
-  | RISCVXOR  -> XOR0 
-  | RISCVSRL  -> SRL0 
-  | RISCVSRA  -> SRA0 
-  | RISCVOR   -> OR0  
-  | RISCVAND  -> AND0 
+  | RISCVADD  -> RISCV_ADD
+  | RISCVSUB  -> RISCV_SUB
+  | RISCVSLL  -> RISCV_SLL
+  | RISCVSLT  -> RISCV_SLT
+  | RISCVSLTU -> RISCV_SLTU
+  | RISCVXOR  -> RISCV_XOR
+  | RISCVSRL  -> RISCV_SRL
+  | RISCVSRA  -> RISCV_SRA
+  | RISCVOR   -> RISCV_OR
+  | RISCVAND  -> RISCV_AND
 
 let translate_ropw op = match op with
-  | RISCVADDW -> ADDW 
-  | RISCVSUBW -> SUBW 
-  | RISCVSLLW -> SLLW 
-  | RISCVSRLW -> SRLW 
-  | RISCVSRAW -> SRAW 
+  | RISCVADDW -> RISCV_ADDW
+  | RISCVSUBW -> RISCV_SUBW
+  | RISCVSLLW -> RISCV_SLLW
+  | RISCVSRLW -> RISCV_SRLW
+  | RISCVSRAW -> RISCV_SRAW
 
 let translate_amoop op = match op with
   | RISCVAMOSWAP -> AMOSWAP
diff --git a/risc-v/hgen/shallow_types_to_herdtools_types.hgen b/risc-v/hgen/shallow_types_to_herdtools_types.hgen
index 03b8820c..6b3b7f51 100644
--- a/risc-v/hgen/shallow_types_to_herdtools_types.hgen
+++ b/risc-v/hgen/shallow_types_to_herdtools_types.hgen
@@ -10,48 +10,48 @@ let translate_out_signed_int inst bits =
 let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg))
 
 let translate_out_uop op = match op with
-  | LUI0  -> RISCVLUI  
-  | AUIPC -> RISCVAUIPC
+  | RISCV_LUI   -> RISCVLUI
+  | RISCV_AUIPC -> RISCVAUIPC
 
 let translate_out_bop op = match op with
-  | BEQ0 -> RISCVBEQ 
-  | BNE  -> RISCVBNE 
-  | BLT  -> RISCVBLT 
-  | BGE  -> RISCVBGE 
-  | BLTU -> RISCVBLTU
-  | BGEU -> RISCVBGEU
+  | RISCV_BEQ  -> RISCVBEQ
+  | RISCV_BNE  -> RISCVBNE
+  | RISCV_BLT  -> RISCVBLT
+  | RISCV_BGE  -> RISCVBGE
+  | RISCV_BLTU -> RISCVBLTU
+  | RISCV_BGEU -> RISCVBGEU
 
 let translate_out_iop op = match op with
-  | ADDI0  -> RISCVADDI 
-  | SLTI0  -> RISCVSLTI 
-  | SLTIU0 -> RISCVSLTIU
-  | XORI0  -> RISCVXORI 
-  | ORI0   -> RISCVORI  
-  | ANDI0  -> RISCVANDI 
+  | RISCV_ADDI   -> RISCVADDI
+  | RISCV_SLTI   -> RISCVSLTI
+  | RISCV_SLTIU  -> RISCVSLTIU
+  | RISCV_XORI   -> RISCVXORI
+  | RISCV_ORI    -> RISCVORI
+  | RISCV_ANDI   -> RISCVANDI
 
 let translate_out_sop op = match op with
-  | SLLI -> RISCVSLLI
-  | SRLI -> RISCVSRLI
-  | SRAI -> RISCVSRAI
+  | RISCV_SLLI -> RISCVSLLI
+  | RISCV_SRLI -> RISCVSRLI
+  | RISCV_SRAI -> RISCVSRAI
 
 let translate_out_rop op = match op with
-  | ADD0  -> RISCVADD 
-  | SUB0  -> RISCVSUB 
-  | SLL0  -> RISCVSLL 
-  | SLT0  -> RISCVSLT 
-  | SLTU0 -> RISCVSLTU
-  | XOR0  -> RISCVXOR 
-  | SRL0  -> RISCVSRL 
-  | SRA0  -> RISCVSRA 
-  | OR0   -> RISCVOR  
-  | AND0  -> RISCVAND 
+  | RISCV_ADD   -> RISCVADD
+  | RISCV_SUB   -> RISCVSUB
+  | RISCV_SLL   -> RISCVSLL
+  | RISCV_SLT   -> RISCVSLT
+  | RISCV_SLTU  -> RISCVSLTU
+  | RISCV_XOR   -> RISCVXOR
+  | RISCV_SRL   -> RISCVSRL
+  | RISCV_SRA   -> RISCVSRA
+  | RISCV_OR    -> RISCVOR
+  | RISCV_AND   -> RISCVAND
 
 let translate_out_ropw op = match op with
-  | ADDW  -> RISCVADDW
-  | SUBW  -> RISCVSUBW
-  | SLLW  -> RISCVSLLW
-  | SRLW  -> RISCVSRLW
-  | SRAW  -> RISCVSRAW
+  | RISCV_ADDW  -> RISCVADDW
+  | RISCV_SUBW  -> RISCVSUBW
+  | RISCV_SLLW  -> RISCVSLLW
+  | RISCV_SRLW  -> RISCVSRLW
+  | RISCV_SRAW  -> RISCVSRAW
 
 let translate_out_amoop op = match op with
   | AMOSWAP -> RISCVAMOSWAP
diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail
index e0a6efba..3a54e0c8 100644
--- a/risc-v/riscv.sail
+++ b/risc-v/riscv.sail
@@ -8,14 +8,14 @@ scattered function unit execute
 (********************************************************************)
 union ast member ((bit[20]), regno, uop) UTYPE
 
-function clause decode ((bit[20]) imm : (regno) rd : 0b0110111) = Some(UTYPE(imm, rd, LUI))
-function clause decode ((bit[20]) imm : (regno) rd : 0b0010111) = Some(UTYPE(imm, rd, AUIPC))
+function clause decode ((bit[20]) imm : (regno) rd : 0b0110111) = Some(UTYPE(imm, rd, RISCV_LUI))
+function clause decode ((bit[20]) imm : (regno) rd : 0b0010111) = Some(UTYPE(imm, rd, RISCV_AUIPC))
 
 function clause execute (UTYPE(imm, rd, op)) =
     let (bit[64]) off = EXTS(imm : 0x000) in
     let ret = switch (op) {
-      case LUI   -> off
-      case AUIPC -> PC + off
+      case RISCV_LUI   -> off
+      case RISCV_AUIPC -> PC + off
     } in
     wGPR(rd, ret)
 
@@ -48,28 +48,28 @@ function clause execute (JALR(imm, rs1, rd)) = {
 union ast member ((bit[13]), regno, regno, bop) BTYPE
 
 function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b1100011) =
-  Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BEQ))
+  Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, RISCV_BEQ))
 function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b1100011) =
-  Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BNE))
+  Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, RISCV_BNE))
 function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b100 : (bit[5]) imm5 : 0b1100011) =
-  Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BLT))
+  Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, RISCV_BLT))
 function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b101 : (bit[5]) imm5 : 0b1100011) =
-  Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BGE))
+  Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, RISCV_BGE))
 function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b110 : (bit[5]) imm5 : 0b1100011) =
-  Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BLTU))
+  Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, RISCV_BLTU))
 function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b111 : (bit[5]) imm5 : 0b1100011) =
-  Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BGEU))
+  Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, RISCV_BGEU))
 
 function clause execute (BTYPE(imm, rs2, rs1, op)) =
   let rs1_val = rGPR(rs1) in
   let rs2_val = rGPR(rs2) in
   let taken   = switch(op) {
-    case BEQ  -> rs1_val == rs2_val
-    case BNE  -> rs1_val != rs2_val
-    case BLT  -> rs1_val <_s rs2_val
-    case BGE  -> rs1_val >=_s rs2_val
-    case BLTU -> rs1_val <_u rs2_val
-    case BGEU -> unsigned(rs1_val) >= unsigned(rs2_val) (* XXX sail missing >=_u *)
+    case RISCV_BEQ  -> rs1_val == rs2_val
+    case RISCV_BNE  -> rs1_val != rs2_val
+    case RISCV_BLT  -> rs1_val <_s rs2_val
+    case RISCV_BGE  -> rs1_val >=_s rs2_val
+    case RISCV_BLTU -> rs1_val <_u rs2_val
+    case RISCV_BGEU -> unsigned(rs1_val) >= unsigned(rs2_val) (* XXX sail missing >=_u *)
   } in
   if (taken) then
       nextPC := PC + EXTS(imm)
@@ -77,70 +77,70 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) =
 (********************************************************************)
 union ast member ((bit[12]), regno, regno, iop) ITYPE
 
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ADDI))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, SLTI))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, SLTIU))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, XORI))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ORI))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b111 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ANDI))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, RISCV_ADDI))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, RISCV_SLTI))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, RISCV_SLTIU))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, RISCV_XORI))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, RISCV_ORI))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b111 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, RISCV_ANDI))
 
 function clause execute (ITYPE (imm, rs1, rd, op)) =
   let rs1_val = rGPR(rs1) in
   let imm64 = (bit[64]) (EXTS(imm)) in
   let (bit[64]) result = switch(op) {
-    case ADDI  -> rs1_val + imm64
-    case SLTI  -> EXTZ(rs1_val <_s imm64)
-    case SLTIU -> EXTZ(rs1_val <_u imm64)
-    case XORI  -> rs1_val ^ imm64
-    case ORI   -> rs1_val | imm64
-    case ANDI  -> rs1_val & imm64
+    case RISCV_ADDI  -> rs1_val + imm64
+    case RISCV_SLTI  -> EXTZ(rs1_val <_s imm64)
+    case RISCV_SLTIU -> EXTZ(rs1_val <_u imm64)
+    case RISCV_XORI  -> rs1_val ^ imm64
+    case RISCV_ORI   -> rs1_val | imm64
+    case RISCV_ANDI  -> rs1_val & imm64
   } in
   wGPR(rd, result)
 
 (********************************************************************)
 union ast member ((bit[6]), regno, regno, sop) SHIFTIOP
 
-function clause decode (0b000000 : (bit[6]) shamt : (regno) rs1 : 0b001 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SLLI))
-function clause decode (0b000000 : (bit[6]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SRLI))
-function clause decode (0b010000 : (bit[6]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SRAI))
+function clause decode (0b000000 : (bit[6]) shamt : (regno) rs1 : 0b001 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SLLI))
+function clause decode (0b000000 : (bit[6]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SRLI))
+function clause decode (0b010000 : (bit[6]) shamt : (regno) rs1 : 0b101 : (regno) rd : 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 SLLI -> rs1_val >> shamt
-      case SRLI -> rs1_val << shamt
-      case SRAI -> shift_right_arith64(rs1_val, shamt)
+      case RISCV_SLLI -> rs1_val >> shamt
+      case RISCV_SRLI -> rs1_val << shamt
+      case RISCV_SRAI -> shift_right_arith64(rs1_val, shamt)
     } in
     wGPR(rd, result)
 
 (********************************************************************)
 union ast member (regno, regno, regno, rop) RTYPE
 
-function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, ADD))
-function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SUB))
-function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b001 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SLL))
-function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SLT))
-function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SLTU))
-function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b100 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, XOR))
-function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SRL))
-function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SRA))
-function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b110 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, OR))
-function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b111 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, AND))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_ADD))
+function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SUB))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b001 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SLL))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SLT))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SLTU))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b100 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_XOR))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SRL))
+function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SRA))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b110 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_OR))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b111 : (regno) rd : 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 (bit[64]) result = switch(op) {
-    case ADD  -> rs1_val + rs2_val
-    case SUB  -> rs1_val - rs2_val
-    case SLL  -> rs1_val << (rs2_val[5..0])
-    case SLT  -> EXTZ(rs1_val <_s rs2_val)
-    case SLTU -> EXTZ(rs1_val <_u rs2_val)
-    case XOR  -> rs1_val ^ rs2_val
-    case SRL  -> rs1_val >> (rs2_val[5..0])
-    case SRA  -> shift_right_arith64(rs1_val, rs2_val[5..0])
-    case OR   -> rs1_val | rs2_val
-    case AND  -> rs1_val & rs2_val
+    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
   } in
   wGPR(rd, result)
 
@@ -217,37 +217,37 @@ function clause execute (ADDIW(imm, rs1, rd)) =
 (********************************************************************)
 union ast member ((bit[5]), regno, regno, sop) SHIFTW
 
-function clause decode (0b0000000 : (bit[5]) shamt : (regno) rs1 : 0b001 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SLLI))
-function clause decode (0b0000000 : (bit[5]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SRLI))
-function clause decode (0b0100000 : (bit[5]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SRAI))
+function clause decode (0b0000000 : (bit[5]) shamt : (regno) rs1 : 0b001 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, RISCV_SLLI))
+function clause decode (0b0000000 : (bit[5]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, RISCV_SRLI))
+function clause decode (0b0100000 : (bit[5]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, RISCV_SRAI))
 
 function clause execute (SHIFTW(shamt, rs1, rd, op)) = 
     let rs1_val = (rGPR(rs1))[31..0] in
     let result = switch(op) {
-      case SLLI -> rs1_val >> shamt
-      case SRLI -> rs1_val << shamt
-      case SRAI -> shift_right_arith32(rs1_val, shamt)
+      case RISCV_SLLI -> rs1_val >> shamt
+      case RISCV_SRLI -> rs1_val << shamt
+      case RISCV_SRAI -> shift_right_arith32(rs1_val, shamt)
     } in
     wGPR(rd, EXTS(result))
 
 (********************************************************************)
 union ast member (regno, regno, regno, ropw) RTYPEW
 
-function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, ADDW))
-function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SUBW))
-function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b001 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SLLW))
-function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SRLW))
-function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SRAW))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_ADDW))
+function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_SUBW))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b001 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_SLLW))
+function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_SRLW))
+function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 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 (bit[32]) result = switch(op) {
-    case ADDW -> rs1_val + rs2_val
-    case SUBW -> rs1_val - rs2_val
-    case SLLW -> rs1_val << (rs2_val[4..0])
-    case SRLW -> rs1_val >> (rs2_val[4..0])
-    case SRAW -> shift_right_arith32(rs1_val, rs2_val[4..0])
+    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])
   } in
   wGPR(rd, EXTS(result))
 
diff --git a/risc-v/riscv_types.sail b/risc-v/riscv_types.sail
index a7cda963..b584ae9b 100644
--- a/risc-v/riscv_types.sail
+++ b/risc-v/riscv_types.sail
@@ -143,12 +143,12 @@ val extern unit -> unit effect { barr } MEM_fence_rw_w
 val extern unit -> unit effect { barr } MEM_fence_w_w
 val extern unit -> unit effect { barr } MEM_fence_i
 
-typedef uop = enumerate {LUI; AUIPC} (* upper immediate ops *)
-typedef bop = enumerate {BEQ; BNE; BLT; BGE; BLTU; BGEU} (* branch ops *)
-typedef iop = enumerate {ADDI; SLTI; SLTIU; XORI; ORI; ANDI} (* immediate ops *)
-typedef sop = enumerate {SLLI; SRLI; SRAI} (* shift ops *)
-typedef rop = enumerate {ADD; SUB; SLL; SLT; SLTU; XOR; SRL; SRA; OR; AND} (* reg-reg ops *)
-typedef ropw = enumerate {ADDW; SUBW; SLLW; SRLW; SRAW} (* reg-reg 32-bit ops *)
+typedef uop = enumerate {RISCV_LUI; RISCV_AUIPC} (* upper immediate ops *)
+typedef bop = enumerate {RISCV_BEQ; RISCV_BNE; RISCV_BLT; RISCV_BGE; RISCV_BLTU; RISCV_BGEU} (* branch ops *)
+typedef iop = enumerate {RISCV_ADDI; RISCV_SLTI; RISCV_SLTIU; RISCV_XORI; RISCV_ORI; RISCV_ANDI} (* immediate ops *)
+typedef sop = enumerate {RISCV_SLLI; RISCV_SRLI; RISCV_SRAI} (* shift ops *)
+typedef rop = enumerate {RISCV_ADD; RISCV_SUB; RISCV_SLL; RISCV_SLT; RISCV_SLTU; RISCV_XOR; RISCV_SRL; RISCV_SRA; RISCV_OR; RISCV_AND} (* reg-reg ops *)
+typedef ropw = enumerate {RISCV_ADDW; RISCV_SUBW; RISCV_SLLW; RISCV_SRLW; RISCV_SRAW} (* reg-reg 32-bit ops *)
 typedef amoop = enumerate {AMOSWAP; AMOADD; AMOXOR; AMOAND; AMOOR;
     AMOMIN; AMOMAX; AMOMINU; AMOMAXU} (* AMO ops *)