renamed hgen to gen

17 files changed, 1196 insertions, 0 deletions

diff --git a/mips/gen/ast.hgen b/mips/gen/ast.hgen
new file mode 100644
index 00000000..a251adff
--- /dev/null
+++ b/mips/gen/ast.hgen
@@ -0,0 +1,18 @@
+| `MIPSThreadStart
+| `MIPSRType of mipsRTypeOp * reg * reg * reg
+| `MIPSIType of mipsITypeOp * reg * reg * bit16
+| `MIPSShiftI of mipsShiftIOp * reg * reg * bit5
+| `MIPSShiftV of mipsShiftVOp * reg * reg * reg
+| `MIPSMulDiv of mipsMulDivOp * reg * reg
+| `MIPSMFHiLo of mipsMFHiLoOp * reg
+| `MIPSLUI of reg * bit16
+| `MIPSLoad of mipsWordWidth * bool * bool * reg * reg * bit16 (* width, signed, linked, base, rt, offset *)
+| `MIPSStore of mipsWordWidth * bool * reg * reg * bit16       (* width, conditional, base, rt, offset *)
+| `MIPSLSLR of bool * bool * bool  * reg * reg * bit16         (* store, double, left, base, rt, offset *)
+| `MIPSSYNC
+| `MIPSBEQ of reg * reg * bit16 * bool * bool                  (* rs, rt, offset, not equal, likely *)
+| `MIPSBCMPZ of reg * bit16 * mipsCmp * bool * bool            (* rs, offset, cmp, link, likely *)
+| `MIPSJ of bit26
+| `MIPSJAL of bit26
+| `MIPSJR of reg
+| `MIPSJALR of reg * reg                                       (* rs, rd *)
diff --git a/mips/gen/fold.hgen b/mips/gen/fold.hgen
new file mode 100644
index 00000000..05b9c808
--- /dev/null
+++ b/mips/gen/fold.hgen
@@ -0,0 +1,19 @@
+| `MIPSThreadStart -> (y_reg, y_sreg)
+| `MIPSRType  (op, rd, rs, rt)  -> fold_reg rt (fold_reg rs (fold_reg rd (y_reg, y_sreg)))
+| `MIPSIType  (op, rs, rt, imm) -> fold_reg rs (fold_reg rt (y_reg, y_sreg))
+| `MIPSShiftI (op, rd, rt, imm) -> fold_reg rt (fold_reg rd (y_reg, y_sreg))
+| `MIPSShiftV (op, rd, rt, rs)  -> fold_reg rs (fold_reg rt (fold_reg rd (y_reg, y_sreg)))
+| `MIPSMulDiv (op, rs, rt)      -> fold_reg rs (fold_reg rt  (y_reg, y_sreg))
+| `MIPSMFHiLo (op, rs)          -> fold_reg rs (y_reg, y_sreg)
+| `MIPSLUI (rt, imm)            -> fold_reg rt (y_reg, y_sreg)
+| `MIPSLoad (width, signed, linked, base, rt, offset) -> fold_reg rt (fold_reg base (y_reg, y_sreg))
+| `MIPSStore (width, conditional, base, rt, offset) -> fold_reg rt (fold_reg base (y_reg, y_sreg))
+| `MIPSLSLR (store, double, left, base, rt, offset) -> fold_reg rt (fold_reg base (y_reg, y_sreg))
+| `MIPSSYNC -> (y_reg, y_sreg)
+| `MIPSBEQ (rs, rt, offset, ne, likely) -> fold_reg rs (fold_reg rt (y_reg, y_sreg))
+| `MIPSBCMPZ (rs, offset, cmp, link, likely) -> fold_reg rs (y_reg, y_sreg)
+| `MIPSJ (offset) -> (y_reg, y_sreg)
+| `MIPSJAL (offset) -> fold_reg (IReg(R31)) (y_reg, y_sreg)
+| `MIPSJR (rd) -> fold_reg rd (y_reg, y_sreg)
+| `MIPSJALR (rd, rs) -> fold_reg rd (fold_reg rs (y_reg, y_sreg))
+
diff --git a/mips/gen/herdtools_ast_to_shallow_ast.hgen b/mips/gen/herdtools_ast_to_shallow_ast.hgen
new file mode 100644
index 00000000..7b1a58d9
--- /dev/null
+++ b/mips/gen/herdtools_ast_to_shallow_ast.hgen
@@ -0,0 +1,121 @@
+| `MIPSThreadStart ->
+    SYSCALL_THREAD_START
+
+| `MIPSStopFetching ->
+    ImplementationDefinedStopFetching0
+
+(* Note different argument order, which reflects difference
+   between instruction encoding and asm format  *)
+| `MIPSRType (op, rd, rs, rt) ->
+    (translate_rtype_op op)
+      (
+      translate_reg "rs" rs,
+      translate_reg "rt" rt,
+      translate_reg "rd" rd
+       )
+      
+
+(* Note different argument order similar to above *)
+| `MIPSIType (op, rt, rs, imm) ->
+    (translate_itype_op op)
+      (
+      translate_reg "rs" rs,
+      translate_reg "rt" rt,
+      translate_imm16 "imm" imm
+       )
+      
+
+| `MIPSShiftI (op, rd, rt, sa) ->
+    (translate_shifti_op op)
+      (
+      translate_reg "rt" rt,
+      translate_reg "rd" rd,
+      translate_imm5 "sa" sa
+       )
+      
+
+| `MIPSShiftV (op, rd, rt, rs) ->
+    (translate_shiftv_op op)
+      (
+      translate_reg "rs" rs,
+      translate_reg "rt" rt,
+      translate_reg "rd" rd
+      )
+      
+
+| `MIPSMulDiv (op, rs, rt) ->
+    (translate_muldiv_op op)
+      (
+      translate_reg "rs" rs,
+      translate_reg "rt" rt
+      )
+      
+
+| `MIPSMFHiLo (op, rs) ->
+    (translate_mfhilo_op op)
+      (
+      translate_reg "rs" rs
+      )
+      
+| `MIPSLUI (rt, imm) ->
+  LUI
+      (
+      translate_reg "rt" rt,
+      translate_imm16 "imm" imm
+      )
+      
+| `MIPSLoad (width, signed, linked, base, rt, offset) ->
+  Load
+      (
+      translate_wordsize "width" width,
+      translate_bool "signed" signed,
+      translate_bool "linked" linked,
+      translate_reg "base" base,
+      translate_reg "rt" rt,
+      translate_imm16 "offset" offset
+      )
+      
+| `MIPSStore (width, conditional, base, rt, offset) ->
+  Store
+      (
+      translate_wordsize "width" width,
+      translate_bool "conditional" conditional,
+      translate_reg "base" base,
+      translate_reg "rt" rt,
+      translate_imm16 "offset" offset
+      )
+      
+| `MIPSLSLR (store, double, left, base, rt, offset) ->
+  (translate_lslr_op store double left)
+      (
+      translate_reg "base" base,
+      translate_reg "rt" rt,
+      translate_imm16 "offset" offset
+      )
+      
+| `MIPSSYNC -> SYNC
+| `MIPSBEQ (rs, rt, offset, ne, likely) ->
+  BEQ
+  (translate_reg "rs" rs,
+   translate_reg "rt" rt,
+   translate_imm16 "offset" offset,
+   translate_bool "ne" ne,
+   translate_bool "likely" likely
+   ) 
+
+| `MIPSBCMPZ (rs, offset, cmp, link, likely) ->
+  BCMPZ
+  (translate_reg "rs" rs,
+   translate_imm16 "offset" offset,
+   translate_cmp "cmp" cmp,
+   translate_bool "link" link,
+   translate_bool "likely" likely
+   ) 
+| `MIPSJ (offset) ->
+  J (translate_imm26 "offset" offset) 
+| `MIPSJAL (offset) ->
+  JAL (translate_imm26 "offset" offset) 
+| `MIPSJR(rd) ->
+  JR (translate_reg "rd" rd) 
+| `MIPSJALR(rd, rs) ->
+  JALR (translate_reg "rd" rd, translate_reg "rs" rs) 
diff --git a/mips/gen/herdtools_types_to_shallow_types.hgen b/mips/gen/herdtools_types_to_shallow_types.hgen
new file mode 100644
index 00000000..5a0e3bfc
--- /dev/null
+++ b/mips/gen/herdtools_types_to_shallow_types.hgen
@@ -0,0 +1,120 @@
+let is_inc = false
+
+let translate_rtype_op op  = uppercase (pp_rtype_op op)
+
+let translate_rtype_op op x = match op with
+  | MIPSROpADD    -> ADD x
+  | MIPSROpADDU   -> ADDU x
+  | MIPSROpAND    -> AND x
+  | MIPSROpDADD   -> DADD x
+  | MIPSROpDADDU  -> DADDU x
+  | MIPSROpDSUB   -> DSUB x
+  | MIPSROpDSUBU  -> DSUBU x
+  | MIPSROpMOVN   -> MOVN x
+  | MIPSROpMOVZ   -> MOVZ x
+  | MIPSROpMUL    -> MUL x
+  | MIPSROpNOR    -> NOR x
+  | MIPSROpOR     -> OR x
+  | MIPSROpSLT    -> SLT x 
+  | MIPSROpSLTU   -> SLTU x
+  | MIPSROpSUB    -> SUB x
+  | MIPSROpSUBU   -> SUBU x
+  | MIPSROpXOR    -> XOR x
+
+let translate_itype_op op x = match op with
+  | MIPSIOpADDI   -> ADDI x
+  | MIPSIOpADDIU  -> ADDIU x
+  | MIPSIOpANDI   -> ANDI x
+  | MIPSIOpDADDI  -> DADDI x
+  | MIPSIOpDADDIU -> DADDIU x
+  | MIPSIOpORI    -> ORI x
+  | MIPSIOpSLTI   -> SLTI x
+  | MIPSIOpSLTIU  -> SLTIU x
+  | MIPSIOpXORI   -> XORI x
+
+let translate_shifti_op op x = match op with
+  | MIPSDSLL   -> DSLL x 
+  | MIPSDSLL32 -> DSLL32 x
+  | MIPSDSRA   -> DSRA x
+  | MIPSDSRA32 -> DSRA32 x
+  | MIPSDSRL   -> DSRL x
+  | MIPSDSRL32 -> DSRL32 x
+  | MIPSSLL    -> SLL x
+  | MIPSSRA    -> SRA x 
+  | MIPSSRL    -> SRL x 
+
+let translate_shiftv_op op x = match op with
+  | MIPSDSLLV -> DSLLV x
+  | MIPSDSRAV -> DSRAV x
+  | MIPSDSRLV -> DSRLV x
+  | MIPSSLLV  -> SLLV x 
+  | MIPSSRAV  -> SRAV x 
+  | MIPSSRLV  -> SRLV x 
+
+let translate_muldiv_op op x = match op with
+  | MIPSDDIV   -> DDIV x  
+  | MIPSDDIVU  -> DDIVU x 
+  | MIPSDIV    -> DIV x   
+  | MIPSDIVU   -> DIVU x  
+  | MIPSDMULT  -> DMULT x 
+  | MIPSDMULTU -> DMULTU x
+  | MIPSMADD   -> MADD x  
+  | MIPSMADDU  -> MADDU x 
+  | MIPSMSUB   -> MSUB x  
+  | MIPSMSUBU  -> MSUBU x 
+  | MIPSMULT   -> MULT x  
+  | MIPSMULTU  -> MULTU x 
+
+let translate_mfhilo_op op x = match op with
+  | MIPSMFHI -> MFHI x
+  | MIPSMFLO -> MFLO x
+  | MIPSMTHI -> MTHI x
+  | MIPSMTLO -> MTLO x
+
+let translate_load_op width signed linked = uppercase (pp_load_op width signed linked)
+
+let translate_store_op width conditional  = uppercase (pp_store_op width conditional)
+
+let translate_lslr_op store double left x = match (store,double,left) with
+  | (false, false, true ) -> LWL x
+  | (false, false, false) -> LWR x
+  | (false, true , true ) -> LDL x
+  | (false, true , false) -> LDR x
+  | (true , false, true ) -> SWL x
+  | (true , false, false) -> SWR x
+  | (true , true , true ) -> SDL x
+  | (true , true , false) -> SDR x
+
+let translate_beq_op ne likely            = uppercase (pp_beq_op ne likely)
+
+let translate_bcmpz_op cmp link likely    = uppercase (pp_bcmpz_op cmp link likely)
+
+
+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_imm26 name value = 
+    Sail_values.to_vec0 is_inc (Nat_big_num.of_int 26,Nat_big_num.of_int value)
+let translate_imm16 name value = 
+    Sail_values.to_vec0 is_inc (Nat_big_num.of_int 16,Nat_big_num.of_int value)
+let translate_imm5 name value = 
+    Sail_values.to_vec0 is_inc (Nat_big_num.of_int 5,Nat_big_num.of_int value)
+let translate_bool name = function
+  | true -> Sail_values.B1
+  | false -> Sail_values.B0
+
+let translate_wordsize _ = function
+ | MIPSByte -> Mips_embed_types.B2
+ | MIPSHalf -> Mips_embed_types.H
+ | MIPSWord -> Mips_embed_types.W
+ | MIPSDouble -> Mips_embed_types.D
+
+let translate_cmp _ = function
+  | MIPS_EQ  -> EQ'
+  | MIPS_NE  -> NE
+  | MIPS_GE  -> GE
+  | MIPS_GEU -> GEU
+  | MIPS_GT  -> GT'
+  | MIPS_LE  -> LE
+  | MIPS_LT  -> LT'
+  | MIPS_LTU -> LTU
diff --git a/mips/gen/lexer.hgen b/mips/gen/lexer.hgen
new file mode 100644
index 00000000..c01b14cc
--- /dev/null
+++ b/mips/gen/lexer.hgen
@@ -0,0 +1,116 @@
+"add"   , RTYPE {txt="ADD"   ; op=MIPSROpADD    };
+"addu"  , RTYPE {txt="ADDU"  ; op=MIPSROpADDU   };
+"and"   , RTYPE {txt="AND"   ; op=MIPSROpAND    };
+"dadd"  , RTYPE {txt="DADD"  ; op=MIPSROpDADD   };
+"daddu" , RTYPE {txt="DADDU" ; op=MIPSROpDADDU  };
+"dsub"  , RTYPE {txt="DSUB"  ; op=MIPSROpDSUB   };
+"dsubu" , RTYPE {txt="DSUBU" ; op=MIPSROpDSUBU  };
+"movn"  , RTYPE {txt="MOVN"  ; op=MIPSROpMOVN   };
+"movz"  , RTYPE {txt="MOVZ"  ; op=MIPSROpMOVZ   };
+"mul"   , RTYPE {txt="MUL"   ; op=MIPSROpMUL    };
+"nor"   , RTYPE {txt="NOR"   ; op=MIPSROpNOR    };
+"or"    , RTYPE {txt="OR"    ; op=MIPSROpOR     };
+"slt"   , RTYPE {txt="SLT"   ; op=MIPSROpSLT    };
+"sltu"  , RTYPE {txt="SLTU"  ; op=MIPSROpSLTU   };
+"sub"   , RTYPE {txt="SUB"   ; op=MIPSROpSUB    };
+"subu"  , RTYPE {txt="SUBU"  ; op=MIPSROpSUBU   };
+"xor"   , RTYPE {txt="XOR"   ; op=MIPSROpXOR    };
+
+"addi"  , ITYPE {txt="ADDI"  ; op=MIPSIOpADDI   };
+"addiu" , ITYPE {txt="ADDIU" ; op=MIPSIOpADDIU  };
+"andi"  , ITYPE {txt="ANDI"  ; op=MIPSIOpANDI   };
+"daddi" , ITYPE {txt="DADDI" ; op=MIPSIOpDADDI  };
+"daddiu", ITYPE {txt="DADDIU"; op=MIPSIOpDADDIU };
+"ori"   , ITYPE {txt="ORI"   ; op=MIPSIOpORI    };
+"slti"  , ITYPE {txt="SLTI"  ; op=MIPSIOpSLTI   };
+"sltiu" , ITYPE {txt="SLTIU" ; op=MIPSIOpSLTIU  };
+"xori"  , ITYPE {txt="XORI"  ; op=MIPSIOpXORI   };
+
+"dsll"   , SHIFTI {txt="DSLL"   ; op=MIPSDSLL   };
+"dsll32" , SHIFTI {txt="DSLL32" ; op=MIPSDSLL32 };
+"dsra"   , SHIFTI {txt="DSRA"   ; op=MIPSDSRA   };
+"dsra32" , SHIFTI {txt="DSRA32" ; op=MIPSDSRA32 };
+"dsrl"   , SHIFTI {txt="DSRL"   ; op=MIPSDSRL   };
+"dsrl32" , SHIFTI {txt="DSRL32" ; op=MIPSDSRL32 };
+"sll"    , SHIFTI {txt="SLL"    ; op=MIPSSLL    };
+"sra"    , SHIFTI {txt="SRA"    ; op=MIPSSRA    };
+"srl"    , SHIFTI {txt="SRL"    ; op=MIPSSRL    };
+
+"dsllv", SHIFTV {txt="DSLLV" ; op=MIPSDSLLV };
+"dsrav", SHIFTV {txt="DSRAV" ; op=MIPSDSRAV };
+"dsrlv", SHIFTV {txt="DSRLV" ; op=MIPSDSRLV };
+"sllv" , SHIFTV {txt="SLLV"  ; op=MIPSSLLV  };
+"srav" , SHIFTV {txt="SRAV"  ; op=MIPSSRAV  };
+"srlv" , SHIFTV {txt="SRLV"  ; op=MIPSSRLV  };
+
+"ddiv"  , MULDIV {txt="DDIV"  ; op=MIPSDDIV   };
+"ddivu" , MULDIV {txt="DDIVU" ; op=MIPSDDIVU  };
+"div"   , MULDIV {txt="DIV"   ; op=MIPSDIV    };
+"divu"  , MULDIV {txt="DIVU"  ; op=MIPSDIVU   };
+"dmult" , MULDIV {txt="DMULT" ; op=MIPSDMULT  };
+"dmultu", MULDIV {txt="DMULTU"; op=MIPSDMULTU };
+"madd"  , MULDIV {txt="MADD"  ; op=MIPSMADD   };
+"maddu" , MULDIV {txt="MADDU" ; op=MIPSMADDU  };
+"msub"  , MULDIV {txt="MSUB"  ; op=MIPSMSUB   };
+"msubu" , MULDIV {txt="MSUBU" ; op=MIPSMSUBU  };
+"mult"  , MULDIV {txt="MULT"  ; op=MIPSMULT   };
+"multu" , MULDIV {txt="MULTU" ; op=MIPSMULTU  };
+
+"mfhi" , MFHILO {txt="MFHI" ; op=MIPSMFHI };
+"mflo" , MFHILO {txt="MFLO" ; op=MIPSMFLO };
+"mthi" , MFHILO {txt="MTHI" ; op=MIPSMTHI };
+"mtlo" , MFHILO {txt="MTLO" ; op=MIPSMTLO };
+
+"lui" , LUI {txt="LUI" };
+
+"lb"  , LOAD {txt="LB"  ; width=MIPSByte   ; signed=true;  linked=false };
+"lbu" , LOAD {txt="LBU" ; width=MIPSByte   ; signed=false; linked=false };
+"lh"  , LOAD {txt="LH"  ; width=MIPSHalf   ; signed=true;  linked=false };
+"lhu" , LOAD {txt="LHU" ; width=MIPSHalf   ; signed=false; linked=false };
+"lw"  , LOAD {txt="LW"  ; width=MIPSWord   ; signed=true;  linked=false };
+"lwu" , LOAD {txt="LWU" ; width=MIPSWord   ; signed=false; linked=false };
+"ld"  , LOAD {txt="LD"  ; width=MIPSDouble ; signed=false; linked=false };
+"ll"  , LOAD {txt="LL"  ; width=MIPSWord   ; signed=true;  linked=true  };
+"lld" , LOAD {txt="LLD" ; width=MIPSDouble ; signed=false; linked=true  };
+
+"sb"  , STORE {txt="SB"  ; width=MIPSByte   ; conditional=false };
+"sh"  , STORE {txt="SH"  ; width=MIPSHalf   ; conditional=false };
+"sw"  , STORE {txt="SW"  ; width=MIPSWord   ; conditional=false };
+"sd"  , STORE {txt="SD"  ; width=MIPSDouble ; conditional=false };
+"sc"  , STORE {txt="SC"  ; width=MIPSWord   ; conditional=true  };
+"scd" , STORE {txt="SCD" ; width=MIPSDouble ; conditional=true  };
+
+"lwl" , LSLR {txt="LWL" ; store=false; double=false; left=true };
+"lwr" , LSLR {txt="LWR" ; store=false; double=false; left=false};
+"ldl" , LSLR {txt="LDL" ; store=false; double=true ; left=true };
+"ldr" , LSLR {txt="LDR" ; store=false; double=true ; left=false};
+"swl" , LSLR {txt="SWL" ; store=true ; double=false; left=true };
+"swr" , LSLR {txt="SWR" ; store=true ; double=false; left=false};
+"sdl" , LSLR {txt="SDL" ; store=true ; double=true ; left=true };
+"sdr" , LSLR {txt="SDR" ; store=true ; double=true ; left=false};
+"sync", SYNC {txt="SYNC"};
+
+"beq",  BEQ {txt="BEQ"; ne=false; likely=false };
+"beql", BEQ {txt="BEQ"; ne=false; likely=true  };
+"bne",  BEQ {txt="BEQ"; ne=true ; likely=false };
+"bnel", BEQ {txt="BEQ"; ne=true ; likely=true  };
+
+"bltz",   BCMPZ {txt="BCMPZ"; cmp=MIPS_LT; likely=false; link=false };
+"bltzal", BCMPZ {txt="BCMPZ"; cmp=MIPS_LT; likely=false; link=true  };
+"bltzl",  BCMPZ {txt="BCMPZ"; cmp=MIPS_LT; likely=true;  link=false };
+"bltzall",BCMPZ {txt="BCMPZ"; cmp=MIPS_LT; likely=true;  link=true  };
+
+"bgez",   BCMPZ {txt="BCMPZ"; cmp=MIPS_GE; likely=false; link=false };
+"bgezal", BCMPZ {txt="BCMPZ"; cmp=MIPS_GE; likely=false; link=true  };
+"bgezl",  BCMPZ {txt="BCMPZ"; cmp=MIPS_GE; likely=true;  link=false };
+"bgezall",BCMPZ {txt="BCMPZ"; cmp=MIPS_GE; likely=true;  link=true  };
+
+"bgtz",   BCMPZ {txt="BCMPZ"; cmp=MIPS_GT; likely=false; link=false };
+"bgtzl",  BCMPZ {txt="BCMPZ"; cmp=MIPS_GT; likely=true;  link=false };
+
+"blez",   BCMPZ {txt="BCMPZ"; cmp=MIPS_LE; likely=false; link=false };
+"blezl",  BCMPZ {txt="BCMPZ"; cmp=MIPS_LE; likely=true;  link=false };
+"j",      J     {txt="J"};
+"jal",    JAL   {txt="JAL"};
+"jr",     JR    {txt="JR"};
+"jalr",   JALR  {txt="JALR"};
diff --git a/mips/gen/map.hgen b/mips/gen/map.hgen
new file mode 100644
index 00000000..f5116bae
--- /dev/null
+++ b/mips/gen/map.hgen
@@ -0,0 +1,19 @@
+| `MIPSThreadStart -> `MIPSThreadStart
+| `MIPSRType  (op, rd, rs, rt)  -> `MIPSRType (op, map_reg rd, map_reg rs, map_reg rt)
+| `MIPSIType  (op, rs, rt, imm) -> `MIPSIType  (op, map_reg rs, map_reg rt, imm)
+| `MIPSShiftI (op, rd, rt, imm) -> `MIPSShiftI (op, map_reg rd, map_reg rt, imm)
+| `MIPSShiftV (op, rd, rt, rs)  -> `MIPSShiftV (op, map_reg rd, map_reg rt, map_reg rs)
+| `MIPSMulDiv (op, rs, rt)      -> `MIPSMulDiv (op, map_reg rs, map_reg rt)
+| `MIPSMFHiLo (op, rs)          -> `MIPSMFHiLo (op, map_reg rs)
+| `MIPSLUI (rt, imm)            -> `MIPSLUI (map_reg rt, imm)
+| `MIPSLoad (width, signed, linked, base, rt, offset) -> `MIPSLoad (width, signed, linked, map_reg base, map_reg rt, offset)
+| `MIPSStore (width, conditional, base, rt, offset) -> `MIPSStore (width, conditional, map_reg base, map_reg rt, offset)
+| `MIPSLSLR (store, double, left, base, rt, offset) -> `MIPSLSLR (store, double, left, map_reg base, map_reg rt, offset)
+| `MIPSSYNC -> `MIPSSYNC
+| `MIPSBEQ (rs, rt, offset, ne, likely) -> `MIPSBEQ (map_reg rs, map_reg rt, offset, ne, likely)
+| `MIPSBCMPZ (rs, offset, cmp, link, likely) -> `MIPSBCMPZ (map_reg rs, offset, cmp, link, likely)
+| `MIPSJ (offset) -> `MIPSJ (offset)
+| `MIPSJAL (offset) -> `MIPSJAL (offset) (* implicit R31? *)
+| `MIPSJR (rd) -> `MIPSJR (map_reg rd)
+| `MIPSJALR (rd, rs) -> `MIPSJALR(map_reg rd, map_reg rs)
+
diff --git a/mips/gen/parser.hgen b/mips/gen/parser.hgen
new file mode 100644
index 00000000..8f573aa5
--- /dev/null
+++ b/mips/gen/parser.hgen
@@ -0,0 +1,34 @@
+| RTYPE reg COMMA reg COMMA reg
+    { `MIPSRType ($1.op, $2, $4, $6) }
+| ITYPE reg COMMA reg COMMA NUM
+    { `MIPSIType ($1.op, $2, $4, $6) }
+| SHIFTI reg COMMA reg COMMA NUM
+    { `MIPSShiftI ($1.op, $2, $4, $6) }
+| SHIFTV reg COMMA reg COMMA reg
+    { `MIPSShiftV ($1.op, $2, $4, $6) }
+| MULDIV reg COMMA reg
+    { `MIPSMulDiv ($1.op, $2, $4) }
+| MFHILO reg
+    { `MIPSMFHiLo ($1.op, $2) }
+| LUI reg COMMA NUM
+    { `MIPSLUI ($2, $4) }
+| LOAD reg COMMA NUM LPAR reg RPAR
+    { `MIPSLoad ($1.width, $1.signed, $1.linked, $6, $2, $4) }
+| STORE reg COMMA NUM LPAR reg RPAR
+    { `MIPSStore ($1.width, $1.conditional, $6, $2, $4) }
+| LSLR  reg COMMA NUM LPAR reg RPAR
+    { `MIPSLSLR ($1.store, $1.double, $1.left, $6, $2, $4) }
+| SYNC
+    { `MIPSSYNC }
+| BEQ reg COMMA reg COMMA NUM
+    { `MIPSBEQ ( $2, $4, $6, $1.ne, $1.likely) }
+| BCMPZ reg COMMA NUM
+    { `MIPSBCMPZ ( $2, $4, $1.cmp, $1.link, $1.likely) }
+| J NUM
+    { `MIPSJ ($2) }
+| JAL NUM
+    { `MIPSJAL ($2) }
+| JR reg
+    { `MIPSJR ($2) }
+| JALR reg COMMA reg
+    { `MIPSJALR ($2, $4) }
diff --git a/mips/gen/pretty.hgen b/mips/gen/pretty.hgen
new file mode 100644
index 00000000..98f56f2e
--- /dev/null
+++ b/mips/gen/pretty.hgen
@@ -0,0 +1,36 @@
+| `MIPSThreadStart -> "syscall 0xfffff" (*  thread start *)
+| `MIPSStopFetching -> "STOP" (* TODO *)
+| `MIPSRType (op, rd,rs,rt) ->
+      sprintf "%s %s,%s,%s" (pp_rtype_op op) (pp_reg rd) (pp_reg rs) (pp_reg rt)
+| `MIPSIType (op,rd,rs,imm) ->
+      sprintf "%s %s,%s,%d" (pp_itype_op op) (pp_reg rd) (pp_reg rs) imm
+| `MIPSShiftI (op, rs, rt, imm) ->
+      sprintf "%s %s,%s,%d" (pp_shifti_op op) (pp_reg rs) (pp_reg rt) imm
+| `MIPSShiftV (op, rd,rs,rt) ->
+      sprintf "%s %s,%s,%s" (pp_shiftv_op op) (pp_reg rd) (pp_reg rs) (pp_reg rt)
+| `MIPSMulDiv (op, rs, rt) ->
+      sprintf "%s %s,%s" (pp_muldiv_op op) (pp_reg rs) (pp_reg rt)
+| `MIPSMFHiLo (op, rs) ->
+      sprintf "%s %s" (pp_mfhilo_op op) (pp_reg rs)
+| `MIPSLUI (rt, imm) ->
+      sprintf "lui %s,%d" (pp_reg rt) imm
+| `MIPSLoad (width, signed, linked, base, rt, offset) ->
+      sprintf "%s %s,%d(%s)" (pp_load_op width signed linked) (pp_reg rt) offset (pp_reg base)
+| `MIPSStore (width, conditional, base, rt, offset) ->
+      sprintf "%s %s,%d(%s)" (pp_store_op width conditional) (pp_reg rt) offset (pp_reg base)
+| `MIPSLSLR (store, double, left, base, rt, offset) ->
+      sprintf "%s %s,%d(%s)" (pp_lslr_op store double left) (pp_reg rt) offset (pp_reg base)
+| `MIPSSYNC -> "sync"
+| `MIPSBEQ (rs, rt, offset, ne, likely) ->
+      sprintf "%s %s,%s,.%+d" (pp_beq_op ne likely) (pp_reg rs) (pp_reg rt) offset
+| `MIPSBCMPZ (rs, offset, cmp, link, likely) ->
+      sprintf "%s,%s,.%+d" (pp_bcmpz_op cmp link likely) (pp_reg rs) offset
+| `MIPSJ (offset) ->
+  sprintf "j %d" offset
+| `MIPSJAL (offset) ->
+  sprintf "jal %d" offset
+| `MIPSJR(rd) ->
+  sprintf "jr %s" (pp_reg rd)
+| `MIPSJALR(rd, rs) ->
+  sprintf "jalr %s,%s" (pp_reg rd) (pp_reg rs)
+
diff --git a/mips/gen/sail_trans_out.hgen b/mips/gen/sail_trans_out.hgen
new file mode 100644
index 00000000..f2d006e8
--- /dev/null
+++ b/mips/gen/sail_trans_out.hgen
@@ -0,0 +1,98 @@
+| ("SYSCALL_THREAD_START", []) -> `MIPSThreadStart
+| ("ADD"   , [rs; rt; rd]) -> `MIPSRType (MIPSROpADD   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| ("ADDU"  , [rs; rt; rd]) -> `MIPSRType (MIPSROpADDU  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| ("AND"   , [rs; rt; rd]) -> `MIPSRType (MIPSROpAND   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| ("DADD"  , [rs; rt; rd]) -> `MIPSRType (MIPSROpDADD  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| ("DADDU" , [rs; rt; rd]) -> `MIPSRType (MIPSROpDADDU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| ("DSUB"  , [rs; rt; rd]) -> `MIPSRType (MIPSROpDSUB  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| ("DSUBU" , [rs; rt; rd]) -> `MIPSRType (MIPSROpDSUBU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| ("MOVN"  , [rs; rt; rd]) -> `MIPSRType (MIPSROpMOVN  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| ("MOVZ"  , [rs; rt; rd]) -> `MIPSRType (MIPSROpMOVZ  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| ("MUL"   , [rs; rt; rd]) -> `MIPSRType (MIPSROpMUL   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| ("NOR"   , [rs; rt; rd]) -> `MIPSRType (MIPSROpNOR   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| ("OR"    , [rs; rt; rd]) -> `MIPSRType (MIPSROpOR    , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| ("SLT"   , [rs; rt; rd]) -> `MIPSRType (MIPSROpSLT   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| ("SLTU"  , [rs; rt; rd]) -> `MIPSRType (MIPSROpSLTU  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| ("SUB"   , [rs; rt; rd]) -> `MIPSRType (MIPSROpSUB   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| ("SUBU"  , [rs; rt; rd]) -> `MIPSRType (MIPSROpSUBU  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| ("XOR"   , [rs; rt; rd]) -> `MIPSRType (MIPSROpXOR   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+
+| ("ADDI"  , [rs; rt; imm]) -> `MIPSIType (MIPSIOpADDI  ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| ("ADDIU" , [rs; rt; imm]) -> `MIPSIType (MIPSIOpADDIU ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| ("ANDI"  , [rs; rt; imm]) -> `MIPSIType (MIPSIOpANDI  ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm))
+| ("DADDI" , [rs; rt; imm]) -> `MIPSIType (MIPSIOpDADDI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| ("DADDIU", [rs; rt; imm]) -> `MIPSIType (MIPSIOpDADDIU,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| ("ORI"   , [rs; rt; imm]) -> `MIPSIType (MIPSIOpORI   ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm))
+| ("SLTI"  , [rs; rt; imm]) -> `MIPSIType (MIPSIOpSLTI  ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| ("SLTIU" , [rs; rt; imm]) -> `MIPSIType (MIPSIOpSLTIU ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| ("XORI"  , [rs; rt; imm]) -> `MIPSIType (MIPSIOpXORI  ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm))
+
+| ("DSLL"   , [rt; rd; sa]) -> `MIPSShiftI (MIPSDSLL   , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| ("DSLL32" , [rt; rd; sa]) -> `MIPSShiftI (MIPSDSLL32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| ("DSRA"   , [rt; rd; sa]) -> `MIPSShiftI (MIPSDSRA   , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| ("DSRA32" , [rt; rd; sa]) -> `MIPSShiftI (MIPSDSRA32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| ("DSRL"   , [rt; rd; sa]) -> `MIPSShiftI (MIPSDSRL   , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| ("DSRL32" , [rt; rd; sa]) -> `MIPSShiftI (MIPSDSRL32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| ("SLL"    , [rt; rd; sa]) -> `MIPSShiftI (MIPSSLL    , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| ("SRA"    , [rt; rd; sa]) -> `MIPSShiftI (MIPSSRA    , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| ("SRL"    , [rt; rd; sa]) -> `MIPSShiftI (MIPSSRL    , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+
+| "DSLLV" , [rs; rt; rd] -> `MIPSShiftV (MIPSDSLLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+| "DSRAV" , [rs; rt; rd] -> `MIPSShiftV (MIPSDSRAV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+| "DSRLV" , [rs; rt; rd] -> `MIPSShiftV (MIPSDSRLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+| "SLLV"  , [rs; rt; rd] -> `MIPSShiftV (MIPSSLLV  , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+| "SRAV"  , [rs; rt; rd] -> `MIPSShiftV (MIPSSRAV  , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+| "SRLV"  , [rs; rt; rd] -> `MIPSShiftV (MIPSSRLV  , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+
+| "DDIV"  , [rs; rt] -> `MIPSMulDiv (MIPSDDIV   , (translate_out_ireg rs), (translate_out_ireg rt))
+| "DDIVU" , [rs; rt] -> `MIPSMulDiv (MIPSDDIVU  , (translate_out_ireg rs), (translate_out_ireg rt))
+| "DIV"   , [rs; rt] -> `MIPSMulDiv (MIPSDIV    , (translate_out_ireg rs), (translate_out_ireg rt))
+| "DIVU"  , [rs; rt] -> `MIPSMulDiv (MIPSDIVU   , (translate_out_ireg rs), (translate_out_ireg rt))
+| "DMULT" , [rs; rt] -> `MIPSMulDiv (MIPSDMULT  , (translate_out_ireg rs), (translate_out_ireg rt))
+| "DMULTU", [rs; rt] -> `MIPSMulDiv (MIPSDMULTU , (translate_out_ireg rs), (translate_out_ireg rt))
+| "MADD"  , [rs; rt] -> `MIPSMulDiv (MIPSMADD   , (translate_out_ireg rs), (translate_out_ireg rt))
+| "MADDU" , [rs; rt] -> `MIPSMulDiv (MIPSMADDU  , (translate_out_ireg rs), (translate_out_ireg rt))
+| "MSUB"  , [rs; rt] -> `MIPSMulDiv (MIPSMSUB   , (translate_out_ireg rs), (translate_out_ireg rt))
+| "MSUBU" , [rs; rt] -> `MIPSMulDiv (MIPSMSUBU  , (translate_out_ireg rs), (translate_out_ireg rt))
+| "MULT"  , [rs; rt] -> `MIPSMulDiv (MIPSMULT   , (translate_out_ireg rs), (translate_out_ireg rt))
+| "MULTU" , [rs; rt] -> `MIPSMulDiv (MIPSMULTU  , (translate_out_ireg rs), (translate_out_ireg rt))
+
+| "MFHI" , [rs]  -> `MIPSMFHiLo (MIPSMFHI, (translate_out_ireg rs))
+| "MFLO" , [rs]  -> `MIPSMFHiLo (MIPSMFLO, (translate_out_ireg rs))
+| "MTHI" , [rs]  -> `MIPSMFHiLo (MIPSMTHI, (translate_out_ireg rs))
+| "MTLO" , [rs]  -> `MIPSMFHiLo (MIPSMTLO, (translate_out_ireg rs))
+
+| "LUI" , [rt; imm] -> `MIPSLUI ((translate_out_ireg rt), (translate_out_imm16 imm))
+| "Load", [width; signed; linked; base; rt; offset] ->
+  `MIPSLoad (
+     (translate_out_wordWidth width), 
+     (translate_out_bool signed),
+     (translate_out_bool linked),
+     (translate_out_ireg  base),
+     (translate_out_ireg  rt),
+     (translate_out_simm16 offset)
+   )
+| "Store", [width; conditional; base; rt; offset] ->
+  `MIPSStore (
+     (translate_out_wordWidth width), 
+     (translate_out_bool conditional),
+     (translate_out_ireg  base),
+     (translate_out_ireg  rt),
+     (translate_out_simm16  offset)
+   )
+| "LWL", [base; rt; offset] -> `MIPSLSLR (false, false, true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| "LWR", [base; rt; offset] -> `MIPSLSLR (false, false, false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| "LDL", [base; rt; offset] -> `MIPSLSLR (false, true , true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| "LDR", [base; rt; offset] -> `MIPSLSLR (false, true , false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| "SWL", [base; rt; offset] -> `MIPSLSLR (true , false, true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| "SWR", [base; rt; offset] -> `MIPSLSLR (true , false, false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| "SDL", [base; rt; offset] -> `MIPSLSLR (true , true , true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| "SDR", [base; rt; offset] -> `MIPSLSLR (true , true , false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| "SYNC", [] -> `MIPSSYNC
+| "BEQ", [rs; rt; offset; ne; likely] -> `MIPSBEQ ((translate_out_ireg rs), (translate_out_ireg rt), (translate_out_simm16 offset), (translate_out_bool ne), (translate_out_bool likely))
+| "BCMPZ", [rs; offset; cmp; link; likely] -> `MIPSBCMPZ ((translate_out_ireg rs), (translate_out_simm16 offset), (translate_out_cmp cmp), (translate_out_bool link), (translate_out_bool likely))
+| "J", [offset] -> `MIPSJ (translate_out_imm26 offset)
+| "JAL", [offset] -> `MIPSJAL (translate_out_imm26 offset)
+| "JR", [rd] -> `MIPSJR (translate_out_ireg rd)
+| "JALR", [rd; rs] -> `MIPSJALR (translate_out_ireg rd, translate_out_ireg rs)
+
diff --git a/mips/gen/shallow_ast_to_herdtools_ast.hgen b/mips/gen/shallow_ast_to_herdtools_ast.hgen
new file mode 100644
index 00000000..efe2c77e
--- /dev/null
+++ b/mips/gen/shallow_ast_to_herdtools_ast.hgen
@@ -0,0 +1,98 @@
+| SYSCALL_THREAD_START -> `MIPSThreadStart
+| (ADD    (rs, rt, rd)) -> `MIPSRType (MIPSROpADD   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (ADDU   (rs, rt, rd)) -> `MIPSRType (MIPSROpADDU  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (AND    (rs, rt, rd)) -> `MIPSRType (MIPSROpAND   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (DADD   (rs, rt, rd)) -> `MIPSRType (MIPSROpDADD  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (DADDU  (rs, rt, rd)) -> `MIPSRType (MIPSROpDADDU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (DSUB   (rs, rt, rd)) -> `MIPSRType (MIPSROpDSUB  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (DSUBU  (rs, rt, rd)) -> `MIPSRType (MIPSROpDSUBU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (MOVN   (rs, rt, rd)) -> `MIPSRType (MIPSROpMOVN  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (MOVZ   (rs, rt, rd)) -> `MIPSRType (MIPSROpMOVZ  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (MUL    (rs, rt, rd)) -> `MIPSRType (MIPSROpMUL   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (NOR    (rs, rt, rd)) -> `MIPSRType (MIPSROpNOR   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (OR     (rs, rt, rd)) -> `MIPSRType (MIPSROpOR    , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (SLT    (rs, rt, rd)) -> `MIPSRType (MIPSROpSLT   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (SLTU   (rs, rt, rd)) -> `MIPSRType (MIPSROpSLTU  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (SUB    (rs, rt, rd)) -> `MIPSRType (MIPSROpSUB   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (SUBU   (rs, rt, rd)) -> `MIPSRType (MIPSROpSUBU  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+| (XOR    (rs, rt, rd)) -> `MIPSRType (MIPSROpXOR   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
+
+| (ADDI   (rs, rt, imm)) -> `MIPSIType (MIPSIOpADDI  ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| (ADDIU  (rs, rt, imm)) -> `MIPSIType (MIPSIOpADDIU ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| (ANDI   (rs, rt, imm)) -> `MIPSIType (MIPSIOpANDI  ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm))
+| (DADDI  (rs, rt, imm)) -> `MIPSIType (MIPSIOpDADDI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| (DADDIU (rs, rt, imm)) -> `MIPSIType (MIPSIOpDADDIU,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| (ORI    (rs, rt, imm)) -> `MIPSIType (MIPSIOpORI   ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm))
+| (SLTI   (rs, rt, imm)) -> `MIPSIType (MIPSIOpSLTI  ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| (SLTIU  (rs, rt, imm)) -> `MIPSIType (MIPSIOpSLTIU ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
+| (XORI   (rs, rt, imm)) -> `MIPSIType (MIPSIOpXORI  ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm))
+
+| (DSLL    (rt, rd, sa)) -> `MIPSShiftI (MIPSDSLL   , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (DSLL32  (rt, rd, sa)) -> `MIPSShiftI (MIPSDSLL32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (DSRA    (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRA   , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (DSRA32  (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRA32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (DSRL    (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRL   , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (DSRL32  (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRL32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (SLL     (rt, rd, sa)) -> `MIPSShiftI (MIPSSLL    , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (SRA     (rt, rd, sa)) -> `MIPSShiftI (MIPSSRA    , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+| (SRL     (rt, rd, sa)) -> `MIPSShiftI (MIPSSRL    , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
+
+| DSLLV  (rs, rt, rd) -> `MIPSShiftV (MIPSDSLLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+| DSRAV  (rs, rt, rd) -> `MIPSShiftV (MIPSDSRAV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+| DSRLV  (rs, rt, rd) -> `MIPSShiftV (MIPSDSRLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+| SLLV   (rs, rt, rd) -> `MIPSShiftV (MIPSSLLV  , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+| SRAV   (rs, rt, rd) -> `MIPSShiftV (MIPSSRAV  , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+| SRLV   (rs, rt, rd) -> `MIPSShiftV (MIPSSRLV  , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
+
+| DDIV   (rs, rt) -> `MIPSMulDiv (MIPSDDIV   , (translate_out_ireg rs), (translate_out_ireg rt))
+| DDIVU  (rs, rt) -> `MIPSMulDiv (MIPSDDIVU  , (translate_out_ireg rs), (translate_out_ireg rt))
+| DIV    (rs, rt) -> `MIPSMulDiv (MIPSDIV    , (translate_out_ireg rs), (translate_out_ireg rt))
+| DIVU   (rs, rt) -> `MIPSMulDiv (MIPSDIVU   , (translate_out_ireg rs), (translate_out_ireg rt))
+| DMULT  (rs, rt) -> `MIPSMulDiv (MIPSDMULT  , (translate_out_ireg rs), (translate_out_ireg rt))
+| DMULTU (rs, rt) -> `MIPSMulDiv (MIPSDMULTU , (translate_out_ireg rs), (translate_out_ireg rt))
+| MADD   (rs, rt) -> `MIPSMulDiv (MIPSMADD   , (translate_out_ireg rs), (translate_out_ireg rt))
+| MADDU  (rs, rt) -> `MIPSMulDiv (MIPSMADDU  , (translate_out_ireg rs), (translate_out_ireg rt))
+| MSUB   (rs, rt) -> `MIPSMulDiv (MIPSMSUB   , (translate_out_ireg rs), (translate_out_ireg rt))
+| MSUBU  (rs, rt) -> `MIPSMulDiv (MIPSMSUBU  , (translate_out_ireg rs), (translate_out_ireg rt))
+| MULT   (rs, rt) -> `MIPSMulDiv (MIPSMULT   , (translate_out_ireg rs), (translate_out_ireg rt))
+| MULTU  (rs, rt) -> `MIPSMulDiv (MIPSMULTU  , (translate_out_ireg rs), (translate_out_ireg rt))
+
+| MFHI  (rs)  -> `MIPSMFHiLo (MIPSMFHI, (translate_out_ireg rs))
+| MFLO  (rs)  -> `MIPSMFHiLo (MIPSMFLO, (translate_out_ireg rs))
+| MTHI  (rs)  -> `MIPSMFHiLo (MIPSMTHI, (translate_out_ireg rs))
+| MTLO  (rs)  -> `MIPSMFHiLo (MIPSMTLO, (translate_out_ireg rs))
+
+| LUI  (rt, imm) -> `MIPSLUI ((translate_out_ireg rt), (translate_out_imm16 imm))
+| Load (width, signed, linked, base, rt, offset) ->
+  `MIPSLoad (
+     (translate_out_wordWidth width), 
+     (translate_out_bool signed),
+     (translate_out_bool linked),
+     (translate_out_ireg  base),
+     (translate_out_ireg  rt),
+     (translate_out_simm16 offset)
+   )
+| Store (width, conditional, base, rt, offset) ->
+  `MIPSStore (
+     (translate_out_wordWidth width), 
+     (translate_out_bool conditional),
+     (translate_out_ireg  base),
+     (translate_out_ireg  rt),
+     (translate_out_simm16  offset)
+   )
+| LWL (base, rt, offset) -> `MIPSLSLR (false, false, true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| LWR (base, rt, offset) -> `MIPSLSLR (false, false, false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| LDL (base, rt, offset) -> `MIPSLSLR (false, true , true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| LDR (base, rt, offset) -> `MIPSLSLR (false, true , false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| SWL (base, rt, offset) -> `MIPSLSLR (true , false, true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| SWR (base, rt, offset) -> `MIPSLSLR (true , false, false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| SDL (base, rt, offset) -> `MIPSLSLR (true , true , true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| SDR (base, rt, offset) -> `MIPSLSLR (true , true , false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
+| SYNC -> `MIPSSYNC
+| BEQ (rs, rt, offset, ne, likely) -> `MIPSBEQ ((translate_out_ireg rs), (translate_out_ireg rt), (translate_out_simm16 offset), (translate_out_bool ne), (translate_out_bool likely))
+| BCMPZ (rs, offset, cmp, link, likely) -> `MIPSBCMPZ ((translate_out_ireg rs), (translate_out_simm16 offset), (translate_out_cmp cmp), (translate_out_bool link), (translate_out_bool likely))
+| J (offset) -> `MIPSJ (translate_out_imm26 offset)
+| JAL (offset) -> `MIPSJAL (translate_out_imm26 offset)
+| JR (rd) -> `MIPSJR (translate_out_ireg rd)
+| JALR (rd, rs) -> `MIPSJALR (translate_out_ireg rd, translate_out_ireg rs)
+
diff --git a/mips/gen/shallow_types_to_herdtools_types.hgen b/mips/gen/shallow_types_to_herdtools_types.hgen
new file mode 100644
index 00000000..a02d83b7
--- /dev/null
+++ b/mips/gen/shallow_types_to_herdtools_types.hgen
@@ -0,0 +1,39 @@
+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_ireg ireg = IReg (int_to_ireg (translate_out_int ireg))
+
+let translate_out_imm26 imm = translate_out_int imm
+
+let translate_out_imm16 imm = translate_out_int imm
+let translate_out_simm16 imm = translate_out_signed_int imm 16
+
+let translate_out_imm5 imm = translate_out_int imm
+
+let translate_out_bool = function
+  | Sail_values.B1  -> true
+  | Sail_values.B0 -> false
+  | _ -> failwith "translate_out_bool Undef"
+
+
+let translate_out_wordWidth = function
+    | Mips_embed_types.B2 -> MIPSByte
+    | Mips_embed_types.H -> MIPSHalf
+    | Mips_embed_types.W -> MIPSWord
+    | Mips_embed_types.D -> MIPSDouble
+
+let translate_out_cmp = function
+    | Mips_embed_types.EQ' -> MIPS_EQ  (* equal *)
+    | Mips_embed_types.NE -> MIPS_NE  (* not equal *)
+    | Mips_embed_types.GE -> MIPS_GE  (* signed greater than or equal *)
+    | Mips_embed_types.GEU -> MIPS_GEU (* unsigned greater than or equal *) 
+    | Mips_embed_types.GT' -> MIPS_GT  (* signed strictly greater than *) 
+    | Mips_embed_types.LE -> MIPS_LE  (* signed less than or equal *) 
+    | Mips_embed_types.LT' -> MIPS_LT  (* signed strictly less than *) 
+    | Mips_embed_types.LTU -> MIPS_LTU (* unsigned less than or qual *) 
diff --git a/mips/gen/token_types.hgen b/mips/gen/token_types.hgen
new file mode 100644
index 00000000..170b42d3
--- /dev/null
+++ b/mips/gen/token_types.hgen
@@ -0,0 +1,39 @@
+type token_RTYPE = {txt : string; op : mipsRTypeOp }
+type token_ITYPE = {txt : string; op : mipsITypeOp }
+type token_ShiftI = {txt : string; op : mipsShiftIOp }
+type token_ShiftV = {txt : string; op : mipsShiftVOp }
+type token_MulDiv = {txt : string; op : mipsMulDivOp }
+type token_MFHiLo = {txt : string; op : mipsMFHiLoOp }
+type token_LUI    = {txt : string }
+type token_Load   = {txt : string; width: mipsWordWidth; signed : bool; linked : bool}
+type token_Store  = {txt : string; width: mipsWordWidth; conditional : bool}
+type token_LSLR   = {txt : string; store : bool; double : bool; left: bool } (* Load/Store Left/Right *)
+type token_SYNC   = {txt : string}
+type token_BEQ    = {txt : string; ne : bool; likely : bool }
+type token_BCMPZ  = {txt : string; cmp : mipsCmp; likely : bool; link : bool }
+type token_J      = {txt : string}
+type token_JAL    = {txt : string}
+type token_JR     = {txt : string}
+type token_JALR   = {txt : string}
+(*
+(regno, imm16, Comparison) TRAPIMM
+
+(regno, regno) RDHWR
+(regno, regno, Comparison) TRAPREG
+(regno, regno, bit[3], bool) MFC0
+(regno, regno, bit[3], bool) MTC0
+(regno, regno, imm16, bool, bool) BEQ
+TLBP
+TLBR
+TLBWI
+TLBWR
+
+regregimm16 CACHE
+regregimm16 PREF
+
+unit BREAK
+unit ERET
+unit HCF
+unit SYSCALL
+unit WAIT
+*)
\ No newline at end of file
diff --git a/mips/gen/tokens.hgen b/mips/gen/tokens.hgen
new file mode 100644
index 00000000..937c6354
--- /dev/null
+++ b/mips/gen/tokens.hgen
@@ -0,0 +1,17 @@
+%token <MIPSHGenBase.token_RTYPE> RTYPE
+%token <MIPSHGenBase.token_ITYPE> ITYPE
+%token <MIPSHGenBase.token_ShiftI> SHIFTI
+%token <MIPSHGenBase.token_ShiftV> SHIFTV
+%token <MIPSHGenBase.token_MulDiv> MULDIV
+%token <MIPSHGenBase.token_MFHiLo> MFHILO
+%token <MIPSHGenBase.token_LUI> LUI
+%token <MIPSHGenBase.token_Load> LOAD
+%token <MIPSHGenBase.token_Store> STORE
+%token <MIPSHGenBase.token_LSLR> LSLR
+%token <MIPSHGenBase.token_SYNC> SYNC
+%token <MIPSHGenBase.token_BEQ> BEQ
+%token <MIPSHGenBase.token_BCMPZ> BCMPZ
+%token <MIPSHGenBase.token_J> J
+%token <MIPSHGenBase.token_JAL> JAL
+%token <MIPSHGenBase.token_JR> JR
+%token <MIPSHGenBase.token_JALR> JALR
diff --git a/mips/gen/trans_sail.hgen b/mips/gen/trans_sail.hgen
new file mode 100644
index 00000000..e42d1b19
--- /dev/null
+++ b/mips/gen/trans_sail.hgen
@@ -0,0 +1,122 @@
+| `MIPSThreadStart ->
+  ("SYSCALL_THREAD_START", [], [])
+| `MIPSStopFetching ->
+    ("ImplementationDefinedStopFetching",
+      [],
+      [])
+
+(* Note different argument order, which reflects difference
+   between instruction encoding and asm format  *)
+| `MIPSRType (op, rd, rs, rt) ->
+    (translate_rtype_op op,
+      [
+      translate_reg "rs" rs;
+      translate_reg "rt" rt;
+      translate_reg "rd" rd;
+       ],
+      [])
+
+(* Note different argument order similar to above *)
+| `MIPSIType (op, rt, rs, imm) ->
+    (translate_itype_op op,
+      [
+      translate_reg "rs" rs;
+      translate_reg "rt" rt;
+      translate_imm16 "imm" imm;
+       ],
+      [])
+
+| `MIPSShiftI (op, rd, rt, sa) ->
+    (translate_shifti_op op,
+      [
+      translate_reg "rt" rt;
+      translate_reg "rd" rd;
+      translate_imm5 "sa" sa;
+       ],
+      [])
+
+| `MIPSShiftV (op, rd, rt, rs) ->
+    (translate_shiftv_op op,
+      [
+      translate_reg "rs" rs;
+      translate_reg "rt" rt;
+      translate_reg "rd" rd;
+      ],
+      [])
+
+| `MIPSMulDiv (op, rs, rt) ->
+    (translate_muldiv_op op,
+      [
+      translate_reg "rs" rs;
+      translate_reg "rt" rt;
+      ],
+      [])
+
+| `MIPSMFHiLo (op, rs) ->
+    (translate_mfhilo_op op,
+      [
+      translate_reg "rs" rs;
+      ],
+      [])
+| `MIPSLUI (rt, imm) ->
+  ("LUI",
+      [
+      translate_reg "rt" rt;
+      translate_imm16 "imm" imm;
+      ],
+      [])
+| `MIPSLoad (width, signed, linked, base, rt, offset) ->
+  ("Load",
+      [
+      translate_wordsize "width" width;
+      translate_bool "signed" signed;
+      translate_bool "linked" linked;
+      translate_reg "base" base;
+      translate_reg "rt" rt;
+      translate_imm16 "offset" offset;
+      ],
+      [])
+| `MIPSStore (width, conditional, base, rt, offset) ->
+  ("Store",
+      [
+      translate_wordsize "width" width;
+      translate_bool "conditional" conditional;
+      translate_reg "base" base;
+      translate_reg "rt" rt;
+      translate_imm16 "offset" offset;
+      ],
+      [])
+| `MIPSLSLR (store, double, left, base, rt, offset) ->
+  (translate_lslr_op store double left,
+      [
+      translate_reg "base" base;
+      translate_reg "rt" rt;
+      translate_imm16 "offset" offset;
+      ],
+      [])
+| `MIPSSYNC -> ("SYNC", [], [])
+| `MIPSBEQ (rs, rt, offset, ne, likely) ->
+  ("BEQ",
+  [translate_reg "rs" rs;
+   translate_reg "rt" rt;
+   translate_imm16 "offset" offset;
+   translate_bool "ne" ne;
+   translate_bool "likely" likely;
+   ], [])
+
+| `MIPSBCMPZ (rs, offset, cmp, link, likely) ->
+  ("BCMPZ",
+  [translate_reg "rs" rs;
+   translate_imm16 "offset" offset;
+   translate_cmp "cmp" cmp;
+   translate_bool "link" link;
+   translate_bool "likely" likely;
+   ], [])
+| `MIPSJ (offset) ->
+  ("J", [translate_imm26 "offset" offset;], [])
+| `MIPSJAL (offset) ->
+  ("JAL", [translate_imm26 "offset" offset;], [])
+| `MIPSJR(rd) ->
+  ("JR", [translate_reg "rd" rd;], [])
+| `MIPSJALR(rd, rs) ->
+  ("JALR", [translate_reg "rd" rd; translate_reg "rs" rs;], [])
diff --git a/mips/gen/types.hgen b/mips/gen/types.hgen
new file mode 100644
index 00000000..a1c61f4b
--- /dev/null
+++ b/mips/gen/types.hgen
@@ -0,0 +1,209 @@
+type mipsRTypeOp = 
+| MIPSROpADD
+| MIPSROpADDU
+| MIPSROpAND
+| MIPSROpDADD
+| MIPSROpDADDU
+| MIPSROpDSUB
+| MIPSROpDSUBU
+| MIPSROpMOVN
+| MIPSROpMOVZ
+| MIPSROpMUL
+| MIPSROpNOR
+| MIPSROpOR
+| MIPSROpSLT
+| MIPSROpSLTU
+| MIPSROpSUB
+| MIPSROpSUBU
+| MIPSROpXOR
+
+let pp_rtype_op = function
+| MIPSROpADD    -> "add"  
+| MIPSROpADDU   -> "addu"
+| MIPSROpAND    -> "and"  
+| MIPSROpDADD   -> "dadd"
+| MIPSROpDADDU  -> "daddu"
+| MIPSROpDSUB   -> "dsub"
+| MIPSROpDSUBU  -> "dsubu"
+| MIPSROpMOVN   -> "movn"
+| MIPSROpMOVZ   -> "movz"
+| MIPSROpMUL    -> "mul"  
+| MIPSROpNOR    -> "nor"  
+| MIPSROpOR     -> "or"   
+| MIPSROpSLT    -> "slt"  
+| MIPSROpSLTU   -> "sltu"
+| MIPSROpSUB    -> "sub"  
+| MIPSROpSUBU   -> "subu"
+| MIPSROpXOR    -> "xor"  
+
+type bit26 = int
+type bit16 = int
+type bit5  = int
+
+type mipsITypeOp = 
+| MIPSIOpADDI
+| MIPSIOpADDIU
+| MIPSIOpANDI
+| MIPSIOpDADDI
+| MIPSIOpDADDIU
+| MIPSIOpORI
+| MIPSIOpSLTI
+| MIPSIOpSLTIU
+| MIPSIOpXORI
+
+let pp_itype_op = function
+| MIPSIOpADDI   -> "addi"
+| MIPSIOpADDIU  -> "addiu"
+| MIPSIOpANDI   -> "andi"
+| MIPSIOpDADDI  -> "daddi"
+| MIPSIOpDADDIU -> "daddiu"
+| MIPSIOpORI    -> "ori"
+| MIPSIOpSLTI   -> "slti"
+| MIPSIOpSLTIU  -> "sltiu"
+| MIPSIOpXORI   -> "xori"
+
+type mipsShiftIOp = 
+| MIPSDSLL
+| MIPSDSLL32
+| MIPSDSRA
+| MIPSDSRA32
+| MIPSDSRL
+| MIPSDSRL32
+| MIPSSLL
+| MIPSSRA
+| MIPSSRL
+
+let pp_shifti_op = function
+| MIPSDSLL   -> "dsll" 
+| MIPSDSLL32 -> "dsll32"
+| MIPSDSRA   -> "dsra"  
+| MIPSDSRA32 -> "dsra32"
+| MIPSDSRL   -> "dsrl"  
+| MIPSDSRL32 -> "dsrl32"
+| MIPSSLL    -> "sll"   
+| MIPSSRA    -> "sra"   
+| MIPSSRL    -> "srl"   
+
+type mipsShiftVOp = 
+| MIPSDSLLV
+| MIPSDSRAV
+| MIPSDSRLV
+| MIPSSLLV
+| MIPSSRAV
+| MIPSSRLV
+
+let pp_shiftv_op = function
+| MIPSDSLLV -> "dsllv"
+| MIPSDSRAV -> "dsrav"
+| MIPSDSRLV -> "dsrlv"
+| MIPSSLLV  -> "sllv" 
+| MIPSSRAV  -> "srav" 
+| MIPSSRLV  -> "srlv" 
+
+type mipsMulDivOp =
+| MIPSDDIV
+| MIPSDDIVU
+| MIPSDIV
+| MIPSDIVU
+| MIPSDMULT
+| MIPSDMULTU
+| MIPSMADD
+| MIPSMADDU
+| MIPSMSUB
+| MIPSMSUBU
+| MIPSMULT
+| MIPSMULTU
+
+let pp_muldiv_op = function
+| MIPSDDIV   -> "ddiv"  
+| MIPSDDIVU  -> "ddivu" 
+| MIPSDIV    -> "div"   
+| MIPSDIVU   -> "divu"  
+| MIPSDMULT  -> "dmult" 
+| MIPSDMULTU -> "dmultu"
+| MIPSMADD   -> "madd"  
+| MIPSMADDU  -> "maddu" 
+| MIPSMSUB   -> "msub"  
+| MIPSMSUBU  -> "msubu" 
+| MIPSMULT   -> "mult"  
+| MIPSMULTU  -> "multu" 
+
+type mipsMFHiLoOp =
+| MIPSMFHI
+| MIPSMFLO
+| MIPSMTHI
+| MIPSMTLO
+
+let pp_mfhilo_op = function
+| MIPSMFHI -> "mfhi"
+| MIPSMFLO -> "mflo"
+| MIPSMTHI -> "mthi"
+| MIPSMTLO -> "mtlo"
+
+type mipsWordWidth = 
+| MIPSByte
+| MIPSHalf
+| MIPSWord
+| MIPSDouble
+
+type mipsCmp =
+| MIPS_EQ  (* equal *)
+| MIPS_NE  (* not equal *)
+| MIPS_GE  (* signed greater than or equal *)
+| MIPS_GEU (* unsigned greater than or equal *) 
+| MIPS_GT  (* signed strictly greater than *) 
+| MIPS_LE  (* signed less than or equal *) 
+| MIPS_LT  (* signed strictly less than *) 
+| MIPS_LTU (* unsigned less than or qual *) 
+
+let pp_load_op width signed linked = match (width, signed, linked) with
+  | (MIPSByte, true, false)    -> "lb"
+  | (MIPSByte, false, false)   -> "lbu"
+  | (MIPSHalf, true, false)    -> "lh"
+  | (MIPSHalf, false, false)   -> "lhu"
+  | (MIPSWord, true, false)    -> "lw"
+  | (MIPSWord, false, false)   -> "lwu"
+  | (MIPSDouble, false, false) -> "ld"
+  | (MIPSWord, true, true)     -> "ll"
+  | (MIPSDouble, false, true)  -> "lld"
+  | _                          -> failwith "unexpected load op"
+
+let pp_store_op width conditional = match (width, conditional) with
+  | (MIPSByte,   false) -> "sb"
+  | (MIPSHalf,   false) -> "sh"
+  | (MIPSWord,   false) -> "sw"
+  | (MIPSDouble, false) -> "sd"
+  | (MIPSWord,   true)  -> "sc"
+  | (MIPSDouble, true)  -> "scd"
+  | _                   -> failwith "unexpected store op"
+
+let pp_lslr_op store double left = match (store, double, left) with
+  | (false, false, true ) -> "lwl"
+  | (false, false, false) -> "lwr"
+  | (false, true , true ) -> "ldl"
+  | (false, true , false) -> "ldr"
+  | (true , false, true ) -> "swl"
+  | (true , false, false) -> "swr"
+  | (true , true , true ) -> "sdl"
+  | (true , true , false) -> "sdr"
+
+let pp_beq_op ne likely = match (ne, likely) with
+  | (false, false) -> "beq"
+  | (false, true)  -> "beql"
+  | (true , false) -> "bne"
+  | (true , true)  -> "bnel"
+
+let pp_bcmpz_op cmp link likely = match (cmp, likely, link) with
+| (MIPS_LT, false , false ) -> "bltz"
+| (MIPS_LT, false , true  ) -> "bltzal"
+| (MIPS_LT, true  , false ) -> "bltzl"
+| (MIPS_LT, true  , true  ) -> "bltzall"
+| (MIPS_GE, false , false ) -> "bgez"
+| (MIPS_GE, false , true  ) -> "bgezal"
+| (MIPS_GE, true  , false ) -> "bgezl"
+| (MIPS_GE, true  , true  ) -> "bgezall"
+| (MIPS_GT, false , false ) -> "bgtz"
+| (MIPS_GT, true  , false ) -> "bgtzl"
+| (MIPS_LE, false , false ) -> "blez"
+| (MIPS_LE, true  , false ) -> "blezl"
+| _ -> failwith "unknown bcmpz instruction"
diff --git a/mips/gen/types_sail_trans_out.hgen b/mips/gen/types_sail_trans_out.hgen
new file mode 100644
index 00000000..ebd31fcb
--- /dev/null
+++ b/mips/gen/types_sail_trans_out.hgen
@@ -0,0 +1,47 @@
+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_imm26 imm = translate_out_int imm
+
+let translate_out_imm16 imm = translate_out_int imm
+let translate_out_simm16 imm = translate_out_signed_int imm 16
+
+let translate_out_imm5 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 inst = 
+    match translate_out_enum inst with
+    | 0 -> MIPSByte
+    | 1 -> MIPSHalf
+    | 2 -> MIPSWord
+    | 3 -> MIPSDouble
+    | _ -> failwith "Unknown wordWidth in sail translate out"
+
+let translate_out_cmp inst = 
+    match translate_out_enum inst with
+    | 0 -> MIPS_EQ  (* equal *)
+    | 1 -> MIPS_NE  (* not equal *)
+    | 2 -> MIPS_GE  (* signed greater than or equal *)
+    | 3 -> MIPS_GEU (* unsigned greater than or equal *) 
+    | 4 -> MIPS_GT  (* signed strictly greater than *) 
+    | 5 -> MIPS_LE  (* signed less than or equal *) 
+    | 6 -> MIPS_LT  (* signed strictly less than *) 
+    | 7 -> MIPS_LTU (* unsigned less than or qual *) 
+    | _ -> failwith "Unknown mipsCmp in sail translate out"
diff --git a/mips/gen/types_trans_sail.hgen b/mips/gen/types_trans_sail.hgen
new file mode 100644
index 00000000..63880ae9
--- /dev/null
+++ b/mips/gen/types_trans_sail.hgen
@@ -0,0 +1,44 @@
+let translate_rtype_op op  = uppercase (pp_rtype_op op)
+let translate_itype_op op  = uppercase (pp_itype_op op)
+let translate_shifti_op op = uppercase (pp_shifti_op op)
+let translate_shiftv_op op = uppercase (pp_shiftv_op op)
+let translate_muldiv_op op = uppercase (pp_muldiv_op op)
+let translate_mfhilo_op op = uppercase (pp_mfhilo_op op)
+let translate_load_op width signed linked = uppercase (pp_load_op width signed linked)
+let translate_store_op width conditional  = uppercase (pp_store_op width conditional)
+let translate_lslr_op store double left   = uppercase (pp_lslr_op store double left)
+let translate_beq_op ne likely            = uppercase (pp_beq_op ne likely)
+let translate_bcmpz_op cmp link likely    = uppercase (pp_bcmpz_op cmp link likely)
+
+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_imm26 name value = 
+    (name, Bvector (Some 26), bit_list_of_integer 26 (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_imm5 name value = 
+    (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int value))
+let translate_bool name value =
+  (name, Bit, [if value then Bitc_one else Bitc_zero])
+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_wordsize = translate_enum [MIPSByte; MIPSHalf; MIPSWord; MIPSDouble]
+let translate_cmp = translate_enum [
+MIPS_EQ  ;(* equal *)
+MIPS_NE  ;(* not equal *)
+MIPS_GE  ;(* signed greater than or equal *)
+MIPS_GEU ;(* unsigned greater than or equal *) 
+MIPS_GT  ;(* signed strictly greater than *) 
+MIPS_LE  ;(* signed less than or equal *) 
+MIPS_LT  ;(* signed strictly less than *) 
+MIPS_LTU ;(* unsigned less than or qual *) 
+]
\ No newline at end of file