further changes to support rmem

19 files changed, 1365 insertions, 0 deletions

diff --git a/gen/ast.hgen b/gen/ast.hgen
new file mode 100644
index 0000000..4bad813
--- /dev/null
+++ b/gen/ast.hgen
@@ -0,0 +1,21 @@
+| `RISCVStopFetching (* this is a special instruction used by rmem to
+                        indicate the end of a litmus thread *)
+| `RISCVThreadStart  (* this instruction indicates a thread creation in ELF files *)
+
+| `RISCVUTYPE of bit20 * reg * riscvUop
+| `RISCVJAL   of bit20 * reg
+| `RISCVJALR  of bit12 * reg * reg
+| `RISCVBType of bit12 * reg * reg * riscvBop
+| `RISCVIType of bit12 * reg * reg * riscvIop
+| `RISCVShiftIop of bit6 * reg * reg * riscvSop
+| `RISCVRType of reg * reg * reg * riscvRop
+| `RISCVLoad of bit12 * reg * reg * bool * wordWidth * bool * bool
+| `RISCVStore of bit12 * reg * reg * wordWidth * bool * bool
+| `RISCVADDIW of bit12 * reg * reg
+| `RISCVSHIFTW of bit5 * reg * reg * riscvSop
+| `RISCVRTYPEW of reg * reg * reg * riscvRopw
+| `RISCVFENCE of riscv_fence_mode * bit4 * bit4
+| `RISCVFENCEI
+| `RISCVLoadRes of bool * bool * reg * wordWidth * reg
+| `RISCVStoreCon of bool * bool * reg * reg * wordWidth * reg
+| `RISCVAMO of riscvAmoop * bool * bool * reg * reg * wordWidth * reg
diff --git a/gen/fold.hgen b/gen/fold.hgen
new file mode 100644
index 0000000..a47aa24
--- /dev/null
+++ b/gen/fold.hgen
@@ -0,0 +1,20 @@
+| `RISCVThreadStart                      -> (y_reg, y_sreg)
+| `RISCVStopFetching                     -> (y_reg, y_sreg)
+
+| `RISCVUTYPE (_, r0, _)                 -> fold_reg r0 (y_reg, y_sreg)
+| `RISCVJAL (_, r0)                      -> fold_reg r0 (y_reg, y_sreg)
+| `RISCVJALR (_, r0, r1)                 -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVBType (_, r0, r1, _)             -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVIType (_, r0, r1, _)             -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVShiftIop (_, r0, r1, _)          -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVRType (r0, r1, r2, _)            -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg)))
+| `RISCVLoad (_, r0, r1, _, _, _, _)     -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVStore (_, r0, r1, _, _, _)       -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVADDIW (_, r0, r1)                -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVSHIFTW (_, r0, r1, _)            -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVRTYPEW (r0, r1, r2, _)           -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg)))
+| `RISCVFENCE (_, _, _)                  -> (y_reg, y_sreg)
+| `RISCVFENCEI                           -> (y_reg, y_sreg)
+| `RISCVLoadRes (_, _, rs1, _, rd)       -> fold_reg rs1 (fold_reg rd (y_reg, y_sreg))
+| `RISCVStoreCon (_, _, rs2, rs1, _, rd) -> fold_reg rs2 (fold_reg rs1 (fold_reg rd (y_reg, y_sreg)))
+| `RISCVAMO (_, _, _, rs2, rs1, _, rd)   -> fold_reg rs2 (fold_reg rs1 (fold_reg rd (y_reg, y_sreg)))
diff --git a/gen/herdtools_ast_to_shallow_ast.hgen b/gen/herdtools_ast_to_shallow_ast.hgen
new file mode 100644
index 0000000..f36949f
--- /dev/null
+++ b/gen/herdtools_ast_to_shallow_ast.hgen
@@ -0,0 +1,88 @@
+| `RISCVThreadStart  -> THREAD_START()
+| `RISCVStopFetching -> STOP_FETCHING()
+
+| `RISCVUTYPE(imm, rd, op) -> UTYPE(
+      translate_imm20 "imm" imm,
+      translate_reg "rd" rd,
+      translate_uop op)
+| `RISCVJAL(imm, rd) -> RISCV_JAL(
+      translate_imm21 "imm" imm,
+      translate_reg "rd" rd)
+| `RISCVJALR(imm, rs, rd) -> RISCV_JALR(
+      translate_imm12 "imm" imm,
+      translate_reg "rs" rd,
+      translate_reg "rd" rd)
+| `RISCVBType(imm, rs2, rs1, op) -> BTYPE(
+      translate_imm13 "imm" imm,
+      translate_reg "rs2" rs2,
+      translate_reg "rs1" rs1,
+      translate_bop op)
+| `RISCVIType(imm, rs1, rd, op) -> ITYPE(
+      translate_imm12 "imm" imm,
+      translate_reg "rs1" rs1,
+      translate_reg "rd" rd,
+      translate_iop op)
+| `RISCVShiftIop(imm, rs, rd, op) -> SHIFTIOP(
+      translate_imm6 "imm" imm,
+      translate_reg "rs" rs,
+      translate_reg "rd" rd,
+      translate_sop op)
+| `RISCVRType (rs2, rs1, rd, op) -> RTYPE (
+      translate_reg "rs2" rs2,
+      translate_reg "rs1" rs1,
+      translate_reg "rd" rd,
+      translate_rop op)
+| `RISCVLoad(imm, rs, rd, unsigned, width, aq, rl) -> LOAD(
+      translate_imm12 "imm" imm,
+      translate_reg "rs" rs,
+      translate_reg "rd" rd,
+      translate_bool "unsigned" unsigned,
+      translate_wordWidth width,
+      translate_bool "aq" aq,
+      translate_bool "rl" rl)
+| `RISCVStore(imm, rs, rd, width, aq, rl) -> STORE (
+      translate_imm12 "imm" imm,
+      translate_reg "rs" rs,
+      translate_reg "rd" rd,
+      translate_wordWidth width,
+      translate_bool "aq" aq,
+      translate_bool "rl" rl)
+| `RISCVADDIW(imm, rs, rd) -> ADDIW(
+      translate_imm12 "imm" imm,
+      translate_reg "rs" rs,
+      translate_reg "rd" rd)
+| `RISCVSHIFTW(imm, rs, rd, op) -> SHIFTW(
+      translate_imm5 "imm" imm,
+      translate_reg "rs" rs,
+      translate_reg "rd" rd,
+      translate_sop op)
+| `RISCVRTYPEW(rs2, rs1, rd, op) -> RTYPEW(
+      translate_reg "rs2" rs2,
+      translate_reg "rs1" rs1,
+      translate_reg "rd" rd,
+      translate_ropw op)
+| `RISCVFENCE(mode, pred, succ) -> FENCE(
+      translate_imm4 "pred" pred,
+      translate_imm4 "succ" succ)
+| `RISCVFENCEI -> FENCEI ()
+| `RISCVLoadRes(aq, rl, rs1, width, rd) -> LOADRES(
+      translate_bool "aq" aq,
+      translate_bool "rl" rl,
+      translate_reg "rs1" rs1,
+      translate_wordWidth width,
+      translate_reg "rd" rd)
+| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) -> STORECON(
+      translate_bool "aq" aq,
+      translate_bool "rl" rl,
+      translate_reg "rs2" rs2,
+      translate_reg "rs1" rs1,
+      translate_wordWidth width,
+      translate_reg "rd" rd)
+| `RISCVAMO (op, aq, rl, rs2, rs1, width, rd) -> AMO(
+      translate_amoop op,
+      translate_bool "aq" aq,
+      translate_bool "rl" rl,
+      translate_reg "rs2" rs2,
+      translate_reg "rs1" rs1,
+      translate_wordWidth width,
+      translate_reg "rd" rd)
diff --git a/gen/herdtools_types_to_shallow_types.hgen b/gen/herdtools_types_to_shallow_types.hgen
new file mode 100644
index 0000000..8bd311b
--- /dev/null
+++ b/gen/herdtools_types_to_shallow_types.hgen
@@ -0,0 +1,90 @@
+let is_inc = false
+
+let translate_reg name value =
+    Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty5_dict (Nat_big_num.of_int (reg_to_int value))
+
+let translate_uop op = match op with
+  | RISCVLUI   -> RISCV_LUI
+  | RISCVAUIPC -> RISCV_AUIPC
+
+let translate_bop op = match op with
+  | 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  -> 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 -> RISCV_SLLI
+  | RISCVSRLI -> RISCV_SRLI
+  | RISCVSRAI -> RISCV_SRAI
+
+let translate_rop op = match op with
+  | 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 -> RISCV_ADDW
+  | RISCVSUBW -> RISCV_SUBW
+  | RISCVSLLW -> RISCV_SLLW
+  | RISCVSRLW -> RISCV_SRLW
+  | RISCVSRAW -> RISCV_SRAW
+
+let translate_amoop op = match op with
+  | RISCVAMOSWAP -> AMOSWAP
+  | RISCVAMOADD  -> AMOADD
+  | RISCVAMOXOR  -> AMOXOR
+  | RISCVAMOAND  -> AMOAND
+  | RISCVAMOOR   -> AMOOR
+  | RISCVAMOMIN  -> AMOMIN
+  | RISCVAMOMAX  -> AMOMAX
+  | RISCVAMOMINU -> AMOMINU
+  | RISCVAMOMAXU -> AMOMAXU
+
+let translate_wordWidth op = match op with
+  | RISCVBYTE   -> BYTE  
+  | RISCVHALF   -> HALF  
+  | RISCVWORD   -> WORD  
+  | RISCVDOUBLE -> DOUBLE
+
+let translate_bool name b = b (* function
+   * | true -> trueSail2_values.B10
+   * | false -> false Sail2_values.B00 *)
+
+let translate_imm21 name value =
+  Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty21_dict (Nat_big_num.of_int value)
+  
+let translate_imm20 name value = 
+  Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty20_dict (Nat_big_num.of_int value)
+  
+let translate_imm13 name value =
+  Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty13_dict (Nat_big_num.of_int value)
+  
+let translate_imm12 name value =
+  Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty12_dict (Nat_big_num.of_int value)
+  
+let translate_imm6 name value =
+  Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty6_dict (Nat_big_num.of_int value)
+  
+let translate_imm5 name value =
+  Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty5_dict (Nat_big_num.of_int value)
+  
+let translate_imm4 name value =
+  Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty4_dict (Nat_big_num.of_int value)
diff --git a/gen/lexer.hgen b/gen/lexer.hgen
new file mode 100644
index 0000000..9009f33
--- /dev/null
+++ b/gen/lexer.hgen
@@ -0,0 +1,63 @@
+(** RV32I (and RV64I) ***********************************************)
+"lui"   , UTYPE { op=RISCVLUI   };
+"auipc" , UTYPE { op=RISCVAUIPC };
+
+"jal",  JAL ();
+"jalr", JALR ();
+
+"beq",  BTYPE {op=RISCVBEQ};
+"bne",  BTYPE {op=RISCVBNE};
+"blt",  BTYPE {op=RISCVBLT};
+"bge",  BTYPE {op=RISCVBGE};
+"bltu", BTYPE {op=RISCVBLTU};
+"bgeu", BTYPE {op=RISCVBGEU};
+
+"addi",  ITYPE {op=RISCVADDI};
+"stli",  ITYPE {op=RISCVSLTI};
+"sltiu", ITYPE {op=RISCVSLTIU};
+"xori",  ITYPE {op=RISCVXORI};
+"ori",   ITYPE {op=RISCVORI};
+"andi",  ITYPE {op=RISCVANDI};
+
+"add",  RTYPE {op=RISCVADD};
+"sub",  RTYPE {op=RISCVSUB};
+"sll",  RTYPE {op=RISCVSLL};
+"slt",  RTYPE {op=RISCVSLT};
+"sltu", RTYPE {op=RISCVSLT};
+"xor",  RTYPE {op=RISCVXOR};
+"srl",  RTYPE {op=RISCVSRL};
+"sra",  RTYPE {op=RISCVSRA};
+"or",   RTYPE {op=RISCVOR};
+"and",  RTYPE {op=RISCVAND};
+
+"fence",     FENCE ();
+"fence.tso", FENCETSO ();
+"fence.i",   FENCEI ();
+
+(** RV64I (in addition to RV32I) ************************************)
+
+"addiw", ADDIW ();
+
+"addw", RTYPEW {op=RISCVADDW};
+"subw", RTYPEW {op=RISCVSUBW};
+"sllw", RTYPEW {op=RISCVSLLW};
+"srlw", RTYPEW {op=RISCVSRLW};
+"sraw", RTYPEW {op=RISCVSRAW};
+
+"slli", SHIFTIOP {op=RISCVSLLI};
+"srli", SHIFTIOP {op=RISCVSRLI};
+"srai", SHIFTIOP {op=RISCVSRAI};
+
+"slliw", SHIFTW {op=RISCVSLLI};
+"srliw", SHIFTW {op=RISCVSRLI};
+"sraiw", SHIFTW {op=RISCVSRAI};
+
+(** RV32A (and RV64A) ***********************************************)
+
+"r",  FENCEOPTION Fence_R;
+"w",  FENCEOPTION Fence_W;
+"rw", FENCEOPTION Fence_RW;
+
+(** pseudo instructions *********************************************)
+
+"li", LI ()
diff --git a/gen/lexer_regexps.hgen b/gen/lexer_regexps.hgen
new file mode 100644
index 0000000..b8f3ca6
--- /dev/null
+++ b/gen/lexer_regexps.hgen
@@ -0,0 +1,131 @@
+(** RV32I (and RV64I) ***********************************************)
+
+| 'l' (('b'|'h') as width) ("u"? as u) (".aq"? as aq) (".rl"? as rl) as load
+    { if (rl = ".rl") && not (aq = ".aq") then failwith ("'" ^ load ^ "' is not a valid instruction") else
+      LOAD  { width    = (match width with 'b' -> RISCVBYTE | 'h' -> RISCVHALF | _ -> failwith "bad width");
+              unsigned = (u = "u");
+              aq       = (aq = ".aq");
+              rl       = (rl = ".rl");
+            }
+    }
+
+| "lw" (".aq"? as aq) (".rl"? as rl) as load
+    { if (rl = ".rl") && not (aq = ".aq") then failwith ("'" ^ load ^ "' is not a valid instruction") else
+      LOAD  { width    = RISCVWORD;
+              unsigned = false;
+              aq       = (aq = ".aq");
+              rl       = (rl = ".rl");
+            }
+    }
+
+| 's' (('b'|'h'|'w') as width) (".aq"? as aq) (".rl"? as rl) as store
+    { if (aq = ".aq") && not (rl = ".rl") then failwith ("'" ^ store ^ "' is not a valid instruction") else
+      STORE { width    = (match width with 'b' -> RISCVBYTE | 'h' -> RISCVHALF | 'w' -> RISCVWORD | _ -> failwith "bad width");
+              aq       = (aq = ".aq");
+              rl       = (rl = ".rl");
+            }
+    }
+
+(** RV64I (in addition to RV32I) ************************************)
+
+| "lwu" (".aq"? as aq) (".rl"? as rl) as load
+    { if (rl = ".rl") && not (aq = ".aq") then failwith ("'" ^ load ^ "' is not a valid instruction") else
+      LOAD  { width    = RISCVWORD;
+              unsigned = true;
+              aq       = (aq = ".aq");
+              rl       = (rl = ".rl");
+            }
+    }
+
+| "ld" (".aq"? as aq) (".rl"? as rl) as load
+    { if (rl = ".rl") && not (aq = ".aq") then failwith ("'" ^ load ^ "' is not a valid instruction") else
+      LOAD  { width    = RISCVDOUBLE;
+              unsigned = false;
+              aq       = (aq = ".aq");
+              rl       = (rl = ".rl");
+            }
+    }
+
+| "sd" (".aq"? as aq) (".rl"? as rl) as store
+    { if (aq = ".aq") && not (rl = ".rl") then failwith ("'" ^ store ^ "' is not a valid instruction") else
+      STORE { width    = RISCVDOUBLE;
+              aq       = (aq = ".aq");
+              rl       = (rl = ".rl");
+            }
+    }
+
+(** RV32A (and RV64A) ***********************************************)
+
+| "lr.w" (".aq"? as aq) (".rl"? as rl) as lr
+    { if (rl = ".rl") && not (aq = ".aq") then failwith ("'" ^ lr ^ "' is not a valid instruction") else
+      LOADRES { width = RISCVWORD;
+                aq    = (aq = ".aq");
+                rl    = (rl = ".rl");
+              }
+    }
+
+| "sc.w" (".aq"? as aq) (".rl"? as rl) as sc
+    { if (aq = ".aq") && not (rl = ".rl") then failwith ("'" ^ sc ^ "' is not a valid instruction") else
+      STORECON  { width = RISCVWORD;
+                  aq    = (aq = ".aq");
+                  rl    = (rl = ".rl");
+                }
+    }
+
+| "amo" (("swap"|"add"|"and"|"or"|"xor"|"max"|"min"|"maxu"|"minu") as op) ".w" (".aq"? as aq) (".rl"? as rl)
+    { AMO { op    =
+              begin match op with
+              | "swap" -> RISCVAMOSWAP;
+              | "add"  -> RISCVAMOADD;
+              | "and"  -> RISCVAMOAND;
+              | "or"   -> RISCVAMOOR;
+              | "xor"  -> RISCVAMOXOR;
+              | "max"  -> RISCVAMOMAX;
+              | "min"  -> RISCVAMOMIN;
+              | "maxu" -> RISCVAMOMAXU;
+              | "minu" -> RISCVAMOMINU;
+              | _ -> failwith "bad amo"
+              end;
+            width = RISCVWORD;
+            aq    = (aq = ".aq");
+            rl    = (rl = ".rl");
+          }
+    }
+
+(** RV64A (in addition to RV32A) ************************************)
+
+| "lr.d" (".aq"? as aq) (".rl"? as rl) as lr
+    { if (rl = ".rl") && not (aq = ".aq") then failwith ("'" ^ lr ^ "' is not a valid instruction") else
+      LOADRES { width = RISCVDOUBLE;
+                aq    = (aq = ".aq");
+                rl    = (rl = ".rl");
+              }
+    }
+
+| "sc.d" (".aq"? as aq) (".rl"? as rl) as sc
+    { if (aq = ".aq") && not (rl = ".rl") then failwith ("'" ^ sc ^ "' is not a valid instruction") else
+      STORECON  { width = RISCVDOUBLE;
+                  aq    = (aq = ".aq");
+                  rl    = (rl = ".rl");
+                }
+    }
+
+| "amo" (("swap"|"add"|"and"|"or"|"xor"|"max"|"min"|"maxu"|"minu") as op) ".d" (".aq"? as aq) (".rl"? as rl)
+    { AMO { op    =
+              begin match op with
+              | "swap" -> RISCVAMOSWAP;
+              | "add"  -> RISCVAMOADD;
+              | "and"  -> RISCVAMOAND;
+              | "or"   -> RISCVAMOOR;
+              | "xor"  -> RISCVAMOXOR;
+              | "max"  -> RISCVAMOMAX;
+              | "min"  -> RISCVAMOMIN;
+              | "maxu" -> RISCVAMOMAXU;
+              | "minu" -> RISCVAMOMINU;
+              | _ -> failwith "bad amo"
+              end;
+            width = RISCVDOUBLE;
+            aq    = (aq = ".aq");
+            rl    = (rl = ".rl");
+          }
+    }
diff --git a/gen/map.hgen b/gen/map.hgen
new file mode 100644
index 0000000..28e36e0
--- /dev/null
+++ b/gen/map.hgen
@@ -0,0 +1,20 @@
+| `RISCVThreadStart                        -> `RISCVThreadStart
+| `RISCVStopFetching                       -> `RISCVStopFetching
+
+| `RISCVUTYPE (x, r0, y)                   -> `RISCVUTYPE (x, map_reg r0, y)
+| `RISCVJAL (x, r0)                        -> `RISCVJAL (x, map_reg r0)
+| `RISCVJALR (x, r0, r1)                   -> `RISCVJALR (x, map_reg r0, map_reg r1)
+| `RISCVBType (x, r0, r1, y)               -> `RISCVBType (x, map_reg r0, map_reg r1, y)
+| `RISCVIType (x, r0, r1, y)               -> `RISCVIType (x, map_reg r0, map_reg r1, y)
+| `RISCVShiftIop (x, r0, r1, y)            -> `RISCVShiftIop (x, map_reg r0, map_reg r1, y)
+| `RISCVRType (r0, r1, r2, y)              -> `RISCVRType (r0, map_reg r1, map_reg r2, y)
+| `RISCVLoad (x, r0, r1, y, z, a, b)       -> `RISCVLoad (x, map_reg r0, map_reg r1, y, z, a, b)
+| `RISCVStore (x, r0, r1, y, z, a)         -> `RISCVStore (x, map_reg r0, map_reg r1, y, z, a)
+| `RISCVADDIW (x, r0, r1)                  -> `RISCVADDIW (x, map_reg r0, map_reg r1)
+| `RISCVSHIFTW (x, r0, r1, y)              -> `RISCVSHIFTW (x, map_reg r0, map_reg r1, y)
+| `RISCVRTYPEW (r0, r1, r2, x)             -> `RISCVRTYPEW (r0, map_reg r1, map_reg r2, x)
+| `RISCVFENCE (m, p, s)                    -> `RISCVFENCE (m, p, s)
+| `RISCVFENCEI                             -> `RISCVFENCEI
+| `RISCVLoadRes (aq, rl, rs1, w, rd)       -> `RISCVLoadRes (aq, rl, map_reg rs1, w, map_reg rd)
+| `RISCVStoreCon (aq, rl, rs2, rs1, w, rd) -> `RISCVStoreCon (aq, rl, map_reg rs2, map_reg rs1, w, map_reg rd)
+| `RISCVAMO (op, aq, rl, rs2, rs1, w, rd)  -> `RISCVAMO (op, aq, rl, map_reg rs2, map_reg rs1, w, map_reg rd)
diff --git a/gen/parser.hgen b/gen/parser.hgen
new file mode 100644
index 0000000..b0ed4b3
--- /dev/null
+++ b/gen/parser.hgen
@@ -0,0 +1,76 @@
+| UTYPE reg COMMA NUM
+  { (* it's not clear if NUM here should be before or after filling the
+      lowest 12 bits with zeros, or if it should be signed or unsigned;
+      currently assuming: NUM does not include the 12 zeros, and is unsigned *)
+    if not (iskbituimm 20 $4) then failwith "immediate is not 20bit"
+    else `RISCVUTYPE ($4, $2, $1.op) }
+| JAL reg COMMA NUM
+  { if not ($4 mod 2 = 0) then failwith "odd offset"
+    else if not (iskbitsimm 21 $4) then failwith "offset is not 21bit"
+    else `RISCVJAL ($4, $2) }
+| JALR reg COMMA reg COMMA NUM
+  { if not (iskbitsimm 12 $6) then failwith "offset is not 12bit"
+    else `RISCVJALR ($6, $4, $2) }
+| BTYPE reg COMMA reg COMMA NUM
+  { if not ($6 mod 2 = 0) then failwith "odd offset"
+    else if not (iskbitsimm 13 $6) then failwith "offset is not 13bit"
+    else `RISCVBType ($6, $4, $2, $1.op) }
+| ITYPE reg COMMA reg COMMA NUM
+  { if $1.op <> RISCVSLTIU && not (iskbitsimm 12 $6) then failwith "immediate is not 12bit"
+    else if $1.op = RISCVSLTIU && not (iskbituimm 12 $6) then failwith "unsigned immediate is not 12bit"
+    else `RISCVIType ($6, $4, $2, $1.op) }
+| ADDIW reg COMMA reg COMMA NUM
+  { if not (iskbitsimm 12 $6) then failwith "immediate is not 12bit"
+    else `RISCVADDIW ($6, $4, $2) }
+| SHIFTIOP reg COMMA reg COMMA NUM
+  { if not (iskbituimm 6 $6) then failwith "unsigned immediate is not 6bit"
+    else `RISCVShiftIop ($6, $4, $2, $1.op) }
+| SHIFTW reg COMMA reg COMMA NUM
+  { if not (iskbituimm 5 $6) then failwith "unsigned immediate is not 5bit"
+    else `RISCVSHIFTW ($6, $4, $2, $1.op) }
+| RTYPE reg COMMA reg COMMA reg
+  { `RISCVRType ($6, $4, $2, $1.op) }
+| LOAD reg COMMA NUM LPAR reg RPAR
+  { if not (iskbitsimm 12 $4) then failwith "offset is not 12bit"
+    else `RISCVLoad ($4, $6, $2, $1.unsigned, $1.width, $1.aq, $1.rl) }
+| STORE reg COMMA NUM LPAR reg RPAR
+  { if not (iskbitsimm 12 $4) then failwith "offset is not 12bit"
+    else `RISCVStore ($4, $2, $6, $1.width, $1.aq, $1.rl) }
+| RTYPEW reg COMMA reg COMMA reg
+  { `RISCVRTYPEW ($6, $4, $2, $1.op) }
+| FENCE FENCEOPTION COMMA FENCEOPTION
+  { match ($2, $4) with
+    | (Fence_RW, Fence_RW) -> `RISCVFENCE (RISCV_FM_NORMAL, 0b0011, 0b0011)
+    | (Fence_R,  Fence_RW) -> `RISCVFENCE (RISCV_FM_NORMAL, 0b0010, 0b0011)
+    | (Fence_W,  Fence_RW) -> `RISCVFENCE (RISCV_FM_NORMAL, 0b0001, 0b0011)
+    | (Fence_RW, Fence_R)  -> `RISCVFENCE (RISCV_FM_NORMAL, 0b0011, 0b0010)
+    | (Fence_R,  Fence_R)  -> `RISCVFENCE (RISCV_FM_NORMAL, 0b0010, 0b0010)
+    | (Fence_W,  Fence_R)  -> `RISCVFENCE (RISCV_FM_NORMAL, 0b0001, 0b0010)
+    | (Fence_RW, Fence_W)  -> `RISCVFENCE (RISCV_FM_NORMAL, 0b0011, 0b0001)
+    | (Fence_R,  Fence_W)  -> `RISCVFENCE (RISCV_FM_NORMAL, 0b0010, 0b0001)
+    | (Fence_W,  Fence_W)  -> `RISCVFENCE (RISCV_FM_NORMAL, 0b0001, 0b0001)
+  }
+| FENCETSO
+  { `RISCVFENCE (RISCV_FM_TSO, 0b0011, 0b0011) }
+| FENCEI
+  { `RISCVFENCEI }
+| LOADRES reg COMMA LPAR reg RPAR
+  { `RISCVLoadRes ($1.aq, $1.rl, $5, $1.width, $2) }
+| LOADRES reg COMMA NUM LPAR reg RPAR
+  { if $4 <> 0 then failwith "'lr' offset must be 0" else
+    `RISCVLoadRes ($1.aq, $1.rl, $6, $1.width, $2) }
+| STORECON reg COMMA reg COMMA LPAR reg RPAR
+  { `RISCVStoreCon ($1.aq, $1.rl, $4, $7, $1.width, $2) }
+| STORECON reg COMMA reg COMMA NUM LPAR reg RPAR
+  { if $6 <> 0 then failwith "'sc' offset must be 0" else
+    `RISCVStoreCon ($1.aq, $1.rl, $4, $8, $1.width, $2) }
+| AMO reg COMMA reg COMMA LPAR reg RPAR
+  { `RISCVAMO ($1.op, $1.aq, $1.rl, $4, $7, $1.width, $2) }
+| AMO reg COMMA reg COMMA NUM LPAR reg RPAR
+  { if $6 <> 0 then failwith "'amo<op>' offset must be 0" else
+    `RISCVAMO ($1.op, $1.aq, $1.rl, $4, $8, $1.width, $2) }
+
+/* pseudo-ops */
+| LI reg COMMA NUM
+  { if not (iskbitsimm 12 $4) then failwith "immediate is not 12bit (li is currently implemented only with small immediate)"
+    else `RISCVIType ($4, IReg R0, $2, RISCVORI) }
diff --git a/gen/pretty.hgen b/gen/pretty.hgen
new file mode 100644
index 0000000..a283b7e
--- /dev/null
+++ b/gen/pretty.hgen
@@ -0,0 +1,38 @@
+| `RISCVThreadStart               -> "start"
+| `RISCVStopFetching              -> "stop"
+
+| `RISCVUTYPE(imm, rd, op)        -> sprintf "%s %s, %d" (pp_riscv_uop op) (pp_reg rd) imm
+| `RISCVJAL(imm, rd)              -> sprintf "jal  %s, %d" (pp_reg rd) imm
+| `RISCVJALR(imm, rs, rd)         -> sprintf "jalr %s, %s, %d" (pp_reg rd) (pp_reg rs) imm
+| `RISCVBType(imm, rs2, rs1, op)  -> sprintf "%s %s, %s, %d" (pp_riscv_bop op) (pp_reg rs1) (pp_reg rs2) imm
+| `RISCVIType(imm, rs2, rs1, op)  -> sprintf "%s %s, %s, %d" (pp_riscv_iop op) (pp_reg rs1) (pp_reg rs2) imm
+| `RISCVShiftIop(imm, rs, rd, op) -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm
+| `RISCVRType (rs2, rs1, rd, op)  -> sprintf "%s %s, %s, %s" (pp_riscv_rop op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2)
+
+| `RISCVLoad(imm, rs, rd, unsigned, width, aq, rl) ->
+    sprintf "%s %s, %d(%s)" (pp_riscv_load_op (unsigned, width, aq, rl)) (pp_reg rd) imm (pp_reg rs)
+
+| `RISCVStore(imm, rs2, rs1, width, aq, rl) ->
+    sprintf "%s %s, %d(%s)" (pp_riscv_store_op (width, aq, rl)) (pp_reg rs2) imm (pp_reg rs1)
+
+| `RISCVADDIW(imm, rs, rd)        -> sprintf "addiw %s, %s, %d" (pp_reg rd) (pp_reg rs) imm
+| `RISCVSHIFTW(imm, rs, rd, op)   -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm
+| `RISCVRTYPEW(rs2, rs1, rd, op)  -> sprintf "%s %s, %s, %s" (pp_riscv_ropw op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2)
+
+| `RISCVFENCE(RISCV_FM_NORMAL, pred, succ)
+                                  -> sprintf "fence %s,%s" (pp_riscv_fence_option pred) (pp_riscv_fence_option succ)
+
+| `RISCVFENCE(RISCV_FM_TSO, 0b0011, 0b0011)
+                                  -> sprintf "fence.tso"
+| `RISCVFENCE(RISCV_FM_TSO, _, _) -> failwith "bad fence.tso"
+
+| `RISCVFENCEI                    -> sprintf "fence.i"
+
+| `RISCVLoadRes(aq, rl, rs1, width, rd) ->
+    sprintf "%s %s, (%s)" (pp_riscv_load_reserved_op (aq, rl, width)) (pp_reg rd) (pp_reg rs1)
+
+| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) ->
+    sprintf "%s %s, %s, (%s)" (pp_riscv_store_conditional_op (aq, rl, width)) (pp_reg rd) (pp_reg rs2) (pp_reg rs1)
+
+| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) ->
+    sprintf "%s %s, %s, (%s)" (pp_riscv_amo_op (op, aq, rl, width)) (pp_reg rd) (pp_reg rs2) (pp_reg rs1)
diff --git a/gen/pretty_xml.hgen b/gen/pretty_xml.hgen
new file mode 100644
index 0000000..c2c350a
--- /dev/null
+++ b/gen/pretty_xml.hgen
@@ -0,0 +1,138 @@
+| `RISCVThreadStart -> ("op_thread_start", [])
+
+| `RISCVStopFetching -> ("op_stop_fetching", [])
+
+| `RISCVUTYPE(imm, rd, op) ->
+    ("op_U_type",
+      [ ("op",   pp_riscv_uop op);
+        ("uimm", sprintf "%d" imm);
+        ("dest", pp_reg rd);
+      ])
+
+| `RISCVJAL(imm, rd) ->
+    ("op_jal",
+      [ ("offset", sprintf "%d" imm);
+        ("dest",   pp_reg rd);
+      ])
+
+| `RISCVJALR(imm, rs1, rd) ->
+    ("op_jalr",
+      [ ("offset", sprintf "%d" imm);
+        ("base",   pp_reg rs1);
+        ("dest",   pp_reg rd);
+      ])
+
+| `RISCVBType(imm, rs2, rs1, op) ->
+    ("op_branch",
+      [ ("op",     pp_riscv_bop op);
+        ("offset", sprintf "%d" imm);
+        ("src2",   pp_reg rs2);
+        ("src1",   pp_reg rs1);
+      ])
+
+| `RISCVIType(imm, rs1, rd, op) ->
+    ("op_I_type",
+      [ ("op",   pp_riscv_iop op);
+        ("iimm", sprintf "%d" imm);
+        ("src",  pp_reg rs1);
+        ("dest", pp_reg rd);
+      ])
+
+| `RISCVShiftIop(imm, rs1, rd, op) ->
+    ("op_IS_type",
+      [ ("op",     pp_riscv_sop op);
+        ("shamt",  sprintf "%d" imm);
+        ("src",    pp_reg rs1);
+        ("dest",   pp_reg rd);
+      ])
+
+| `RISCVSHIFTW(imm, rs1, rd, op) ->
+    ("op_ISW_type",
+      [ ("op",    pp_riscv_sop op);
+        ("shamt", sprintf "%d" imm);
+        ("src",   pp_reg rs1);
+        ("dest",  pp_reg rd);
+      ])
+
+| `RISCVRType (rs2, rs1, rd, op) ->
+    ("op_R_type",
+      [ ("op",   pp_riscv_rop op);
+        ("src2", pp_reg rs2);
+        ("src1", pp_reg rs1);
+        ("dest", pp_reg rd);
+      ])
+
+| `RISCVLoad(imm, rs1, rd, unsigned, width, aq, rl) ->
+    ("op_load",
+      [ ("aq",       if aq then "true" else "false");
+        ("rl",       if rl then "true" else "false");
+        ("width",    pp_word_width width);
+        ("unsigned", if unsigned then "true" else "false");
+        ("base",     pp_reg rs1);
+        ("offset",   sprintf "%d" imm);
+        ("dest",     pp_reg rd);
+      ])
+
+| `RISCVStore(imm, rs2, rs1, width, aq, rl) ->
+    ("op_store",
+      [ ("aq",       if aq then "true" else "false");
+        ("rl",       if rl then "true" else "false");
+        ("width",    pp_word_width width);
+        ("src",      pp_reg rs2);
+        ("base",     pp_reg rs1);
+        ("offset",   sprintf "%d" imm);
+      ])
+
+| `RISCVADDIW(imm, rs1, rd) ->
+    ("op_addiw",
+      [ ("iimm",  sprintf "%d" imm);
+        ("src",   pp_reg rs1);
+        ("dest",  pp_reg rd);
+      ])
+
+| `RISCVRTYPEW(rs2, rs1, rd, op) ->
+    ("op_RW_type",
+      [ ("op",   pp_riscv_ropw op);
+        ("src2", pp_reg rs2);
+        ("src1", pp_reg rs1);
+        ("dest", pp_reg rd);
+      ])
+
+| `RISCVFENCE(mode, pred, succ) ->
+    ("op_fence",
+      [ ("mode", match mode with RISCV_FM_NORMAL -> "normal" | RISCV_FM_TSO -> "tso");
+        ("pred", pp_riscv_fence_option pred);
+        ("succ", pp_riscv_fence_option succ);
+      ])
+
+| `RISCVFENCEI -> ("op_fence_i", [])
+
+| `RISCVLoadRes(aq, rl, rs1, width, rd) ->
+    ("op_lr",
+      [ ("aq",    if aq then "true" else "false");
+        ("rl",    if rl then "true" else "false");
+        ("width", pp_word_width width);
+        ("addr",  pp_reg rs1);
+        ("dest",  pp_reg rd);
+      ])
+
+| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) ->
+    ("op_sc",
+      [ ("aq",    if aq then "true" else "false");
+        ("rl",    if rl then "true" else "false");
+        ("width", pp_word_width width);
+        ("addr",  pp_reg rs1);
+        ("src",   pp_reg rs2);
+        ("dest",  pp_reg rd);
+      ])
+
+| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) ->
+    ("op_amo",
+      [ ("op",    pp_riscv_amo_op_part op);
+        ("aq",    if aq then "true" else "false");
+        ("rl",    if rl then "true" else "false");
+        ("width", pp_word_width width);
+        ("src",   pp_reg rs2);
+        ("addr",  pp_reg rs1);
+        ("dest",  pp_reg rd);
+      ])
diff --git a/gen/sail_trans_out.hgen b/gen/sail_trans_out.hgen
new file mode 100644
index 0000000..3c25250
--- /dev/null
+++ b/gen/sail_trans_out.hgen
@@ -0,0 +1,25 @@
+| ("StopFetching", [])            -> `RISCVStopFetching
+| ("ThreadStart", [])             -> `RISCVThreadStart
+
+| ("UTYPE", [imm; rd; op])        -> `RISCVUTYPE(translate_out_simm20 imm, translate_out_ireg rd, translate_out_uop op)
+| ("JAL", [imm; rd])              -> `RISCVJAL(translate_out_simm21 imm, translate_out_ireg  rd)
+| ("JALR", [imm; rs; rd])         -> `RISCVJALR(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
+| ("BTYPE", [imm; rs2; rs1; op])  -> `RISCVBType(translate_out_simm13 imm, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_bop op)
+| ("ITYPE", [imm; rs1; rd; op])   -> `RISCVIType(translate_out_simm12 imm, translate_out_ireg rs1, translate_out_ireg rd, translate_out_iop op)
+| ("SHIFTIOP", [imm; rs; rd; op]) -> `RISCVShiftIop(translate_out_imm6 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
+| ("RTYPE", [rs2; rs1; rd; op])   -> `RISCVRType (translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_rop op)
+| ("LOAD", [imm; rs; rd; unsigned; width; aq; rl])
+                                  -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl)
+| ("STORE", [imm; rs; rd; width; aq; rl])
+                                  -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl)
+| ("ADDIW", [imm; rs; rd])        -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
+| ("SHIFTW", [imm; rs; rd; op])   -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
+| ("RTYPEW", [rs2; rs1; rd; op])  -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op)
+| ("FENCE", [mode; pred; succ])   -> `RISCVFENCE(translate_out_fm_mode mode, translate_out_imm4 pred, translate_out_imm4 succ)
+| ("FENCEI", [])                  -> `RISCVFENCEI
+| ("LOADRES", [aq; rl; rs1; width; rd])
+                                  -> `RISCVLoadRes(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
+| ("STORECON", [aq; rl; rs2; rs1; width; rd])
+                                  -> `RISCVStoreCon(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
+| ("AMO", [op; aq; rl; rs2; rs1; width; rd])
+                                  -> `RISCVAMO(translate_out_amoop op, translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
diff --git a/gen/shallow_ast_to_herdtools_ast.hgen b/gen/shallow_ast_to_herdtools_ast.hgen
new file mode 100644
index 0000000..e612f8c
--- /dev/null
+++ b/gen/shallow_ast_to_herdtools_ast.hgen
@@ -0,0 +1,25 @@
+| STOP_FETCHING ()                -> `RISCVStopFetching
+| THREAD_START ()                 -> `RISCVThreadStart
+
+| UTYPE( imm, rd, op)         -> `RISCVUTYPE(translate_out_simm20 imm, translate_out_ireg rd, translate_out_uop op)
+| RISCV_JAL( imm, rd)         -> `RISCVJAL(translate_out_simm21 imm, translate_out_ireg  rd)
+| RISCV_JALR( imm, rs, rd)    -> `RISCVJALR(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
+| BTYPE( imm, rs2, rs1, op)   -> `RISCVBType(translate_out_simm13 imm, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_bop op)
+| ITYPE( imm, rs1, rd, op)    -> `RISCVIType(translate_out_simm12 imm, translate_out_ireg rs1, translate_out_ireg rd, translate_out_iop op)
+| SHIFTIOP( imm, rs, rd, op)  -> `RISCVShiftIop(translate_out_imm6 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
+| RTYPE( rs2, rs1, rd, op)    -> `RISCVRType (translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_rop op)
+| LOAD( imm, rs, rd, unsigned, width, aq, rl)
+                              -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl)
+| STORE( imm, rs, rd, width, aq, rl)
+                              -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl)
+| ADDIW( imm, rs, rd)         -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
+| SHIFTW( imm, rs, rd, op)    -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
+| RTYPEW( rs2, rs1, rd, op)   -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op)
+| FENCE( pred, succ)    -> `RISCVFENCE(RISCV_FM_NORMAL, translate_out_imm4 pred, translate_out_imm4 succ)
+| FENCEI ()                      -> `RISCVFENCEI
+| LOADRES( aq, rl, rs1, width, rd)
+                              -> `RISCVLoadRes(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
+| STORECON( aq, rl, rs2, rs1, width, rd)
+                              -> `RISCVStoreCon(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
+| AMO( op, aq, rl, rs2, rs1, width, rd)
+                              -> `RISCVAMO(translate_out_amoop op, translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
diff --git a/gen/shallow_types_to_herdtools_types.hgen b/gen/shallow_types_to_herdtools_types.hgen
new file mode 100644
index 0000000..5a659cd
--- /dev/null
+++ b/gen/shallow_types_to_herdtools_types.hgen
@@ -0,0 +1,91 @@
+(* let translate_out_big_bit = Sail_values.unsigned
+ * 
+ * let translate_out_int inst = (Nat_big_num.to_int (translate_out_big_bit inst))
+ * let translate_out_signed_int inst bits = 
+ *     let i = (Nat_big_num.to_int (translate_out_big_bit inst)) in
+ *     if (i >= (1 lsl (bits - 1))) then
+ *     (i - (1 lsl bits)) else
+ *       i *)
+
+let translate_out_int i = Nat_big_num.to_int (Lem.naturalFromWord i)
+let translate_out_signed_int i = Nat_big_num.to_int (Lem.signedIntegerFromWord i)
+
+let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg))
+
+let translate_out_uop op = match op with
+  | RISCV_LUI   -> RISCVLUI
+  | RISCV_AUIPC -> RISCVAUIPC
+
+let translate_out_bop op = match op with
+  | 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
+  | 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
+  | RISCV_SLLI -> RISCVSLLI
+  | RISCV_SRLI -> RISCVSRLI
+  | RISCV_SRAI -> RISCVSRAI
+
+let translate_out_rop op = match op with
+  | 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
+  | 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
+  | AMOADD  -> RISCVAMOADD
+  | AMOXOR  -> RISCVAMOXOR
+  | AMOAND  -> RISCVAMOAND
+  | AMOOR   -> RISCVAMOOR
+  | AMOMIN  -> RISCVAMOMIN
+  | AMOMAX  -> RISCVAMOMAX
+  | AMOMINU -> RISCVAMOMINU
+  | AMOMAXU -> RISCVAMOMAXU
+
+let translate_out_wordWidth op = match op with
+  | BYTE   -> RISCVBYTE  
+  | HALF   -> RISCVHALF  
+  | WORD   -> RISCVWORD  
+  | DOUBLE -> RISCVDOUBLE
+
+(* let translate_out_fm_mode = function
+ *   | FM_NORMAL -> RISCV_FM_NORMAL
+ *   | FM_TSO    -> RISCV_FM_TSO *)
+
+let translate_out_bool b = b (* function
+   * | Sail_values.B1  -> true
+   * | Sail_values.B0 -> false
+   * | _ -> failwith "translate_out_bool Undef" *)
+
+let translate_out_simm21 imm = translate_out_signed_int imm (* 21 *)
+let translate_out_simm20 imm = translate_out_signed_int imm (* 20 *)
+let translate_out_simm13 imm = translate_out_signed_int imm (* 13 *)
+let translate_out_simm12 imm = translate_out_signed_int imm (* 12 *)
+let translate_out_imm6 imm = translate_out_int imm
+let translate_out_imm5 imm = translate_out_int imm
+let translate_out_imm4 imm = translate_out_int imm
diff --git a/gen/token_types.hgen b/gen/token_types.hgen
new file mode 100644
index 0000000..1a2895a
--- /dev/null
+++ b/gen/token_types.hgen
@@ -0,0 +1,24 @@
+type token_UTYPE    = {op : riscvUop }
+type token_JAL      = unit
+type token_JALR     = unit
+type token_BType    = {op : riscvBop }
+type token_IType    = {op : riscvIop }
+type token_ShiftIop = {op : riscvSop }
+type token_RTYPE    = {op : riscvRop }
+type token_Load     = {unsigned: bool; width : wordWidth; aq: bool; rl: bool }
+type token_Store    = {width : wordWidth; aq: bool; rl: bool }
+type token_ADDIW    = unit
+type token_SHIFTW   = {op : riscvSop }
+type token_RTYPEW   = {op : riscvRopw }
+type token_FENCE    = unit
+type token_FENCETSO = unit
+type token_FENCEI   = unit
+type token_LoadRes  = {width : wordWidth; aq: bool; rl: bool }
+type token_StoreCon = {width : wordWidth; aq: bool; rl: bool }
+type token_AMO      = {width : wordWidth; aq: bool; rl: bool; op: riscvAmoop }
+
+type token_FENCEOPTION = Fence_R | Fence_W | Fence_RW
+
+(* pseudo-ops *)
+
+type token_LI = unit
diff --git a/gen/tokens.hgen b/gen/tokens.hgen
new file mode 100644
index 0000000..37c76a2
--- /dev/null
+++ b/gen/tokens.hgen
@@ -0,0 +1,20 @@
+%token <RISCVHGenBase.token_UTYPE>    UTYPE   
+%token <RISCVHGenBase.token_JAL>      JAL     
+%token <RISCVHGenBase.token_JALR>     JALR    
+%token <RISCVHGenBase.token_BType>    BTYPE   
+%token <RISCVHGenBase.token_IType>    ITYPE   
+%token <RISCVHGenBase.token_ShiftIop> SHIFTIOP
+%token <RISCVHGenBase.token_RTYPE>    RTYPE   
+%token <RISCVHGenBase.token_Load>     LOAD    
+%token <RISCVHGenBase.token_Store>    STORE   
+%token <RISCVHGenBase.token_ADDIW>    ADDIW   
+%token <RISCVHGenBase.token_SHIFTW>   SHIFTW  
+%token <RISCVHGenBase.token_RTYPEW>   RTYPEW  
+%token <RISCVHGenBase.token_FENCE>    FENCE
+%token <RISCVHGenBase.token_FENCEOPTION> FENCEOPTION
+%token <RISCVHGenBase.token_FENCETSO> FENCETSO
+%token <RISCVHGenBase.token_FENCEI>   FENCEI
+%token <RISCVHGenBase.token_LoadRes>  LOADRES
+%token <RISCVHGenBase.token_StoreCon> STORECON
+%token <RISCVHGenBase.token_AMO>      AMO
+%token <RISCVHGenBase.token_LI>       LI
diff --git a/gen/trans_sail.hgen b/gen/trans_sail.hgen
new file mode 100644
index 0000000..bff31ce
--- /dev/null
+++ b/gen/trans_sail.hgen
@@ -0,0 +1,156 @@
+| `RISCVStopFetching -> ("StopFetching", [], [])
+| `RISCVThreadStart  -> ("ThreadStart", [], [])
+
+| `RISCVUTYPE(imm, rd, op) -> 
+    ("UTYPE",
+      [
+      translate_imm20 "imm" imm;
+      translate_reg "rd" rd;
+      translate_uop "op" op;
+       ],
+      [])
+| `RISCVJAL(imm, rd) -> 
+   ("JAL",
+    [
+      translate_imm21 "imm" imm;
+      translate_reg "rd" rd;
+    ],
+    [])
+| `RISCVJALR(imm, rs, rd) -> 
+   ("JALR",
+    [
+      translate_imm12 "imm" imm;
+      translate_reg "rs" rd;
+      translate_reg "rd" rd;
+    ],
+    [])
+| `RISCVBType(imm, rs2, rs1, op)  -> 
+   ("BTYPE",
+    [
+      translate_imm13 "imm" imm;
+      translate_reg "rs2" rs2;
+      translate_reg "rs1" rs1;
+      translate_bop "op" op;
+    ],
+    [])
+| `RISCVIType(imm, rs1, rd, op)  -> 
+   ("ITYPE",
+    [
+      translate_imm12 "imm" imm;
+      translate_reg "rs1" rs1;
+      translate_reg "rd" rd;
+      translate_iop "op" op;
+    ],
+    [])
+| `RISCVShiftIop(imm, rs, rd, op) -> 
+   ("SHIFTIOP",
+    [
+      translate_imm6 "imm" imm;
+      translate_reg "rs" rs;
+      translate_reg "rd" rd;
+      translate_sop "op" op;
+    ],
+    [])
+| `RISCVRType (rs2, rs1, rd, op)  -> 
+   ("RTYPE",
+    [
+      translate_reg "rs2" rs2;
+      translate_reg "rs1" rs1;
+      translate_reg "rd" rd;
+      translate_rop "op" op;
+    ],
+    [])
+| `RISCVLoad(imm, rs, rd, unsigned, width, aq, rl) ->
+   ("LOAD",
+    [
+      translate_imm12 "imm" imm;
+      translate_reg "rs" rs;
+      translate_reg "rd" rd;
+      translate_bool "unsigned" unsigned;
+      translate_width "width" width;
+      translate_bool "aq" aq;
+      translate_bool "rl" rl;
+    ],
+    [])
+| `RISCVStore(imm, rs2, rs1, width, aq, rl) ->
+   ("STORE",
+    [
+      translate_imm12 "imm" imm;
+      translate_reg "rs2" rs2;
+      translate_reg "rs1" rs1;
+      translate_width "width" width;
+      translate_bool "aq" aq;
+      translate_bool "rl" rl;
+    ],
+    [])
+| `RISCVADDIW(imm, rs, rd)        -> 
+   ("ADDIW",
+    [
+      translate_imm12 "imm" imm;
+      translate_reg "rs" rs;
+      translate_reg "rd" rd;
+    ],
+    [])
+| `RISCVSHIFTW(imm, rs, rd, op)   -> 
+   ("SHIFTW",
+    [
+      translate_imm5 "imm" imm;
+      translate_reg "rs" rs;
+      translate_reg "rd" rd;
+      translate_sop "op" op;
+    ],
+    [])
+| `RISCVRTYPEW(rs2, rs1, rd, op)  -> 
+   ("RTYPEW",
+    [
+      translate_reg "rs2" rs2;
+      translate_reg "rs1" rs1;
+      translate_reg "rd" rd;
+      translate_ropw "op" op;
+    ],
+    [])
+| `RISCVFENCE(mode, pred, succ) ->
+  ("FENCE", 
+  [
+     translate_fm_mode "mode" mode;
+     translate_imm4 "pred" pred;
+     translate_imm4 "succ" succ;
+  ], 
+  [])
+| `RISCVFENCEI ->
+  ("FENCEI",
+  [],
+  [])
+| `RISCVLoadRes(aq, rl, rs1, width, rd) ->
+   ("LOADRES",
+    [
+      translate_bool "aq" aq;
+      translate_bool "rl" rl;
+      translate_reg "rs1" rs1;
+      translate_width "width" width;
+      translate_reg "rd" rd;
+    ],
+    [])
+| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) ->
+   ("STORECON",
+    [
+      translate_bool "aq" aq;
+      translate_bool "rl" rl;
+      translate_reg "rs2" rs2;
+      translate_reg "rs1" rs1;
+      translate_width "width" width;
+      translate_reg "rd" rd;
+    ],
+    [])
+| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) ->
+   ("AMO",
+    [
+      translate_amoop "op" op;
+      translate_bool "aq" aq;
+      translate_bool "rl" rl;
+      translate_reg "rs2" rs2;
+      translate_reg "rs1" rs1;
+      translate_width "width" width;
+      translate_reg "rd" rd;
+    ],
+    [])
diff --git a/gen/types.hgen b/gen/types.hgen
new file mode 100644
index 0000000..5ad0b73
--- /dev/null
+++ b/gen/types.hgen
@@ -0,0 +1,177 @@
+type bit20 = int
+type bit12 = int
+type bit6  = int
+type bit5  = int
+type bit4  = int
+
+type riscvUop =  (* upper immediate ops *)
+| RISCVLUI
+| RISCVAUIPC
+
+let pp_riscv_uop = function
+| RISCVLUI   -> "lui"
+| RISCVAUIPC -> "auipc"
+
+
+type riscvBop =  (* branch ops *)
+| RISCVBEQ 
+| RISCVBNE
+| RISCVBLT
+| RISCVBGE
+| RISCVBLTU
+| RISCVBGEU
+
+let pp_riscv_bop = function
+| RISCVBEQ  -> "beq"
+| RISCVBNE  -> "bne"
+| RISCVBLT  -> "blt"
+| RISCVBGE  -> "bge"
+| RISCVBLTU -> "bltu"
+| RISCVBGEU -> "bgeu"
+
+type riscvIop = (* immediate ops *)
+| RISCVADDI
+| RISCVSLTI
+| RISCVSLTIU
+| RISCVXORI
+| RISCVORI
+| RISCVANDI
+
+let pp_riscv_iop = function
+| RISCVADDI  -> "addi"
+| RISCVSLTI  -> "slti"
+| RISCVSLTIU -> "sltiu"
+| RISCVXORI  -> "xori"
+| RISCVORI   -> "ori"
+| RISCVANDI  -> "andi"
+
+type riscvSop = (* shift ops *)
+| RISCVSLLI
+| RISCVSRLI
+| RISCVSRAI
+
+let pp_riscv_sop = function
+| RISCVSLLI -> "slli"
+| RISCVSRLI -> "srli"
+| RISCVSRAI -> "srai"
+
+type riscvRop = (* reg-reg ops *)
+| RISCVADD
+| RISCVSUB
+| RISCVSLL
+| RISCVSLT 
+| RISCVSLTU
+| RISCVXOR
+| RISCVSRL
+| RISCVSRA
+| RISCVOR
+| RISCVAND
+
+let pp_riscv_rop = function
+| RISCVADD  -> "add"
+| RISCVSUB  -> "sub"
+| RISCVSLL  -> "sll"
+| RISCVSLT  -> "slt"
+| RISCVSLTU -> "sltu"
+| RISCVXOR  -> "xor"
+| RISCVSRL  -> "srl"
+| RISCVSRA  -> "sra"
+| RISCVOR   -> "or"
+| RISCVAND  -> "and"
+
+type riscvRopw = (* reg-reg 32-bit ops *)
+| RISCVADDW
+| RISCVSUBW
+| RISCVSLLW
+| RISCVSRLW
+| RISCVSRAW
+
+let pp_riscv_ropw = function
+| RISCVADDW -> "addw"
+| RISCVSUBW -> "subw"
+| RISCVSLLW -> "sllw"
+| RISCVSRLW -> "srlw"
+| RISCVSRAW -> "sraw"
+
+type wordWidth = 
+  | RISCVBYTE
+  | RISCVHALF
+  | RISCVWORD
+  | RISCVDOUBLE
+
+let pp_word_width width : string =
+  begin match width with
+  | RISCVBYTE   -> "b"
+  | RISCVHALF   -> "h"
+  | RISCVWORD   -> "w"
+  | RISCVDOUBLE -> "d"
+  end
+
+let pp_riscv_load_op (unsigned, width, aq, rl) =
+  "l" ^
+  (pp_word_width width) ^
+  (if unsigned then "u" else "") ^
+  (if aq then ".aq" else "") ^
+  (if rl then ".rl" else "")
+
+let pp_riscv_store_op (width, aq, rl) =
+  "s" ^
+  (pp_word_width width) ^
+  (if aq then ".aq" else "") ^
+  (if rl then ".rl" else "")
+
+let pp_riscv_load_reserved_op (aq, rl, width) =
+  "lr." ^
+  (pp_word_width width) ^
+  (if aq then ".aq" else "") ^
+  (if rl then ".rl" else "")
+
+let pp_riscv_store_conditional_op (aq, rl, width) =
+  "sc." ^
+  (pp_word_width width) ^
+  (if aq then ".aq" else "") ^
+  (if rl then ".rl" else "")
+
+type riscvAmoop =
+  | RISCVAMOSWAP
+  | RISCVAMOADD
+  | RISCVAMOXOR
+  | RISCVAMOAND
+  | RISCVAMOOR
+  | RISCVAMOMIN
+  | RISCVAMOMAX
+  | RISCVAMOMINU
+  | RISCVAMOMAXU
+
+let pp_riscv_amo_op_part = function
+  | RISCVAMOSWAP -> "swap"
+  | RISCVAMOADD  -> "add"
+  | RISCVAMOXOR  -> "xor"
+  | RISCVAMOAND  -> "and"
+  | RISCVAMOOR   -> "or"
+  | RISCVAMOMIN  -> "min"
+  | RISCVAMOMAX  -> "max"
+  | RISCVAMOMINU -> "minu"
+  | RISCVAMOMAXU -> "maxu"
+
+let pp_riscv_amo_op (op, aq, rl, width) =
+  "amo" ^
+  pp_riscv_amo_op_part op ^
+  begin match width with
+  | RISCVWORD   -> ".w"
+  | RISCVDOUBLE -> ".d"
+  | _ -> assert false
+  end ^
+  (if aq then ".aq" else "") ^
+  (if rl then ".rl" else "")
+
+let pp_riscv_fence_option = function
+  | 0b0011 -> "rw"
+  | 0b0010 -> "r"
+  | 0b0001 -> "w"
+  | _ -> failwith "unexpected fence option"
+
+type riscv_fence_mode =
+  | RISCV_FM_NORMAL
+  | RISCV_FM_TSO
+
diff --git a/gen/types_sail_trans_out.hgen b/gen/types_sail_trans_out.hgen
new file mode 100644
index 0000000..66e8eec
--- /dev/null
+++ b/gen/types_sail_trans_out.hgen
@@ -0,0 +1,103 @@
+let translate_out_big_bit = function
+  | (name, Bvector _, bits) -> IInt.integer_of_bit_list bits
+  | _ -> assert false
+
+let translate_out_int inst = (Nat_big_num.to_int (translate_out_big_bit inst))
+let translate_out_signed_int inst bits = 
+    let i = (Nat_big_num.to_int (translate_out_big_bit inst)) in
+    if (i >= (1 lsl (bits - 1))) then
+    (i - (1 lsl bits)) else
+    i
+
+let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg))
+
+let translate_out_simm21 imm = translate_out_signed_int imm 21
+let translate_out_simm20 imm = translate_out_signed_int imm 20
+let translate_out_simm13 imm = translate_out_signed_int imm 13
+let translate_out_simm12 imm = translate_out_signed_int imm 12
+let translate_out_imm6 imm = translate_out_int imm
+let translate_out_imm5 imm = translate_out_int imm
+let translate_out_imm4 imm = translate_out_int imm
+
+let translate_out_bool = function
+  | (name, Bit, [Bitc_one])  -> true
+  | (name, Bit, [Bitc_zero]) -> false
+  | _ -> assert false
+
+let translate_out_enum (name,_,bits) =
+    Nat_big_num.to_int (IInt.integer_of_bit_list bits)
+
+let translate_out_wordWidth w = 
+    match translate_out_enum w with
+    | 0 -> RISCVBYTE
+    | 1 -> RISCVHALF
+    | 2 -> RISCVWORD
+    | 3 -> RISCVDOUBLE
+    | _ -> failwith "Unknown wordWidth in sail translate out"
+
+let translate_out_uop op = match translate_out_enum op with
+    | 0 -> RISCVLUI
+    | 1 -> RISCVAUIPC
+    | _ -> failwith "Unknown uop in sail translate out"
+
+let translate_out_bop op = match translate_out_enum op with
+| 0 -> RISCVBEQ 
+| 1 -> RISCVBNE 
+| 2 -> RISCVBLT 
+| 3 -> RISCVBGE 
+| 4 -> RISCVBLTU
+| 5 -> RISCVBGEU
+| _ -> failwith "Unknown bop in sail translate out"
+
+let translate_out_iop op = match translate_out_enum op with
+| 0 -> RISCVADDI 
+| 1 -> RISCVSLTI 
+| 2 -> RISCVSLTIU
+| 3 -> RISCVXORI 
+| 4 -> RISCVORI  
+| 5 -> RISCVANDI 
+| _ -> failwith "Unknown iop in sail translate out"
+
+let translate_out_sop op = match translate_out_enum op with 
+| 0 -> RISCVSLLI
+| 1 -> RISCVSRLI
+| 2 -> RISCVSRAI
+| _ -> failwith "Unknown sop in sail translate out"
+
+let translate_out_rop op = match translate_out_enum op with
+| 0 -> RISCVADD 
+| 1 -> RISCVSUB 
+| 2 -> RISCVSLL 
+| 3 -> RISCVSLT 
+| 4 -> RISCVSLTU
+| 5 -> RISCVXOR 
+| 6 -> RISCVSRL 
+| 7 -> RISCVSRA 
+| 8 -> RISCVOR  
+| 9 -> RISCVAND 
+| _ -> failwith "Unknown rop in sail translate out"
+
+let translate_out_ropw op = match translate_out_enum op with
+| 0 -> RISCVADDW
+| 1 -> RISCVSUBW
+| 2 -> RISCVSLLW
+| 3 -> RISCVSRLW
+| 4 -> RISCVSRAW
+| _ -> failwith "Unknown ropw in sail translate out"
+
+let translate_out_amoop op = match translate_out_enum op with
+| 0 -> RISCVAMOSWAP
+| 1 -> RISCVAMOADD
+| 2 -> RISCVAMOXOR
+| 3 -> RISCVAMOAND
+| 4 -> RISCVAMOOR
+| 5 -> RISCVAMOMIN
+| 6 -> RISCVAMOMAX
+| 7 -> RISCVAMOMINU
+| 8 -> RISCVAMOMAXU
+| _ -> failwith "Unknown amoop in sail translate out"
+
+let translate_out_fm_mode mode = match translate_out_enum mode with
+| 0 -> RISCV_FM_NORMAL
+| 1    -> RISCV_FM_TSO
+| _ -> failwith "Unknown fm_mode in sail translate out"
diff --git a/gen/types_trans_sail.hgen b/gen/types_trans_sail.hgen
new file mode 100644
index 0000000..eb6aa45
--- /dev/null
+++ b/gen/types_trans_sail.hgen
@@ -0,0 +1,59 @@
+let translate_enum enum_values name value =
+  let rec bit_count n =
+    if n = 0 then 0
+    else 1 + (bit_count (n lsr 1)) in
+  let rec find_index element = function
+    | h::tail -> if h = element then 0 else 1 + (find_index element tail)
+    | _ -> failwith "translate_enum could not find value"
+    in
+  let size = bit_count (List.length enum_values) in
+  let index = find_index value enum_values in
+  (name, Range0 (Some size),  IInt.bit_list_of_integer size (Nat_big_num.of_int index))
+
+let translate_uop = translate_enum [RISCVLUI; RISCVAUIPC]
+
+let translate_bop = translate_enum [RISCVBEQ; RISCVBNE; RISCVBLT; RISCVBGE; RISCVBLTU; RISCVBGEU] (* branch ops *)
+
+let translate_iop = translate_enum [RISCVADDI; RISCVSLTI; RISCVSLTIU; RISCVXORI; RISCVORI; RISCVANDI] (* immediate ops *)
+
+let translate_sop = translate_enum [RISCVSLLI; RISCVSRLI; RISCVSRAI] (* shift ops *)
+
+let translate_rop = translate_enum [RISCVADD; RISCVSUB; RISCVSLL; RISCVSLT; RISCVSLTU; RISCVXOR; RISCVSRL; RISCVSRA; RISCVOR; RISCVAND] (* reg-reg ops *)
+
+let translate_ropw = translate_enum [RISCVADDW; RISCVSUBW; RISCVSLLW; RISCVSRLW; RISCVSRAW] (* reg-reg 32-bit ops *)
+
+let translate_amoop = translate_enum [RISCVAMOSWAP; RISCVAMOADD; RISCVAMOXOR; RISCVAMOAND; RISCVAMOOR; RISCVAMOMIN; RISCVAMOMAX; RISCVAMOMINU; RISCVAMOMAXU]
+
+let translate_width = translate_enum [RISCVBYTE; RISCVHALF; RISCVWORD; RISCVDOUBLE] 
+
+let translate_fm_mode = translate_enum [RISCV_FM_NORMAL; RISCV_FM_TSO]
+
+let translate_reg name value = 
+    (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int (reg_to_int value)))
+
+let translate_imm21 name value = 
+    (name, Bvector (Some 21), bit_list_of_integer 21 (Nat_big_num.of_int value))
+
+let translate_imm20 name value = 
+    (name, Bvector (Some 20), bit_list_of_integer 20 (Nat_big_num.of_int value))
+
+let translate_imm16 name value = 
+    (name, Bvector (Some 16), bit_list_of_integer 16 (Nat_big_num.of_int value))
+
+let translate_imm13 name value = 
+    (name, Bvector (Some 13), bit_list_of_integer 13 (Nat_big_num.of_int value))
+
+let translate_imm12 name value = 
+    (name, Bvector (Some 12), bit_list_of_integer 12 (Nat_big_num.of_int value))
+
+let translate_imm6 name value = 
+    (name, Bvector (Some 6), bit_list_of_integer 6 (Nat_big_num.of_int value))
+
+let translate_imm5 name value = 
+    (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int value))
+
+let translate_imm4 name value = 
+    (name, Bvector (Some 4), bit_list_of_integer 4 (Nat_big_num.of_int value))
+
+let translate_bool name value =
+  (name, Bit, [if value then Bitc_one else Bitc_zero])