Remove cheri and mips specs -- they now have their own repository.

17 files changed, 0 insertions, 1196 deletions

diff --git a/mips/gen/ast.hgen b/mips/gen/ast.hgen
deleted file mode 100644
index a251adff..00000000
--- a/mips/gen/ast.hgen
+++ /dev/null
@@ -1,18 +0,0 @@
-| `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
deleted file mode 100644
index 05b9c808..00000000
--- a/mips/gen/fold.hgen
+++ /dev/null
@@ -1,19 +0,0 @@
-| `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
deleted file mode 100644
index 7b1a58d9..00000000
--- a/mips/gen/herdtools_ast_to_shallow_ast.hgen
+++ /dev/null
@@ -1,121 +0,0 @@
-| `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
deleted file mode 100644
index 5a0e3bfc..00000000
--- a/mips/gen/herdtools_types_to_shallow_types.hgen
+++ /dev/null
@@ -1,120 +0,0 @@
-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
deleted file mode 100644
index c01b14cc..00000000
--- a/mips/gen/lexer.hgen
+++ /dev/null
@@ -1,116 +0,0 @@
-"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
deleted file mode 100644
index f5116bae..00000000
--- a/mips/gen/map.hgen
+++ /dev/null
@@ -1,19 +0,0 @@
-| `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
deleted file mode 100644
index 8f573aa5..00000000
--- a/mips/gen/parser.hgen
+++ /dev/null
@@ -1,34 +0,0 @@
-| 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
deleted file mode 100644
index 98f56f2e..00000000
--- a/mips/gen/pretty.hgen
+++ /dev/null
@@ -1,36 +0,0 @@
-| `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
deleted file mode 100644
index f2d006e8..00000000
--- a/mips/gen/sail_trans_out.hgen
+++ /dev/null
@@ -1,98 +0,0 @@
-| ("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
deleted file mode 100644
index efe2c77e..00000000
--- a/mips/gen/shallow_ast_to_herdtools_ast.hgen
+++ /dev/null
@@ -1,98 +0,0 @@
-| 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
deleted file mode 100644
index a02d83b7..00000000
--- a/mips/gen/shallow_types_to_herdtools_types.hgen
+++ /dev/null
@@ -1,39 +0,0 @@
-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
deleted file mode 100644
index 170b42d3..00000000
--- a/mips/gen/token_types.hgen
+++ /dev/null
@@ -1,39 +0,0 @@
-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
deleted file mode 100644
index 937c6354..00000000
--- a/mips/gen/tokens.hgen
+++ /dev/null
@@ -1,17 +0,0 @@
-%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
deleted file mode 100644
index e42d1b19..00000000
--- a/mips/gen/trans_sail.hgen
+++ /dev/null
@@ -1,122 +0,0 @@
-| `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
deleted file mode 100644
index a1c61f4b..00000000
--- a/mips/gen/types.hgen
+++ /dev/null
@@ -1,209 +0,0 @@
-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
deleted file mode 100644
index ebd31fcb..00000000
--- a/mips/gen/types_sail_trans_out.hgen
+++ /dev/null
@@ -1,47 +0,0 @@
-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
deleted file mode 100644
index 63880ae9..00000000
--- a/mips/gen/types_trans_sail.hgen
+++ /dev/null
@@ -1,44 +0,0 @@
-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