summaryrefslogtreecommitdiff
path: root/mips/gen
diff options
context:
space:
mode:
Diffstat (limited to 'mips/gen')
-rw-r--r--mips/gen/ast.hgen18
-rw-r--r--mips/gen/fold.hgen19
-rw-r--r--mips/gen/herdtools_ast_to_shallow_ast.hgen121
-rw-r--r--mips/gen/herdtools_types_to_shallow_types.hgen120
-rw-r--r--mips/gen/lexer.hgen116
-rw-r--r--mips/gen/map.hgen19
-rw-r--r--mips/gen/parser.hgen34
-rw-r--r--mips/gen/pretty.hgen36
-rw-r--r--mips/gen/sail_trans_out.hgen98
-rw-r--r--mips/gen/shallow_ast_to_herdtools_ast.hgen98
-rw-r--r--mips/gen/shallow_types_to_herdtools_types.hgen39
-rw-r--r--mips/gen/token_types.hgen39
-rw-r--r--mips/gen/tokens.hgen17
-rw-r--r--mips/gen/trans_sail.hgen122
-rw-r--r--mips/gen/types.hgen209
-rw-r--r--mips/gen/types_sail_trans_out.hgen47
-rw-r--r--mips/gen/types_trans_sail.hgen44
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 11:28:59 +0000