1(* mips - generated by L3 - Mon Sep 18 10:36:50 2017 *) 2 3signature mips = 4sig 5 6structure Map : Map 7 8(* ------------------------------------------------------------------------- 9 Types 10 ------------------------------------------------------------------------- *) 11 12type Index = { Index: BitsN.nbit, P: bool, index'rst: BitsN.nbit } 13 14type Random = { Random: BitsN.nbit, random'rst: BitsN.nbit } 15 16type Wired = { Wired: BitsN.nbit, wired'rst: BitsN.nbit } 17 18type EntryLo = 19 { C: BitsN.nbit, D: bool, G: bool, PFN: BitsN.nbit, V: bool, 20 entrylo'rst: BitsN.nbit } 21 22type PageMask = { Mask: BitsN.nbit, pagemask'rst: BitsN.nbit } 23 24type EntryHi = 25 { ASID: BitsN.nbit, R: BitsN.nbit, VPN2: BitsN.nbit, 26 entryhi'rst: BitsN.nbit } 27 28type StatusRegister = 29 { BEV: bool, CU0: bool, CU1: bool, ERL: bool, EXL: bool, FR: bool, 30 IE: bool, IM: BitsN.nbit, KSU: BitsN.nbit, KX: bool, RE: bool, 31 SX: bool, UX: bool, statusregister'rst: BitsN.nbit } 32 33type ConfigRegister = 34 { AR: BitsN.nbit, AT: BitsN.nbit, BE: bool, K0: BitsN.nbit, M: bool, 35 MT: BitsN.nbit, configregister'rst: BitsN.nbit } 36 37type ConfigRegister1 = 38 { C2: bool, CA: bool, DA: BitsN.nbit, DL: BitsN.nbit, DS: BitsN.nbit, 39 EP: bool, FP: bool, IA: BitsN.nbit, IL: BitsN.nbit, IS: BitsN.nbit, 40 M: bool, MD: bool, MMUSize: BitsN.nbit, PC: bool, WR: bool } 41 42type ConfigRegister2 = 43 { M: bool, SA: BitsN.nbit, SL: BitsN.nbit, SS: BitsN.nbit, 44 SU: BitsN.nbit, TA: BitsN.nbit, TL: BitsN.nbit, TS: BitsN.nbit, 45 TU: BitsN.nbit } 46 47type ConfigRegister3 = 48 { DSPP: bool, LPA: bool, M: bool, MT: bool, SM: bool, SP: bool, 49 TL: bool, ULRI: bool, VEIC: bool, VInt: bool, 50 configregister3'rst: BitsN.nbit } 51 52type ConfigRegister6 = 53 { LTLB: bool, TLBSize: BitsN.nbit, configregister6'rst: BitsN.nbit } 54 55type CauseRegister = 56 { BD: bool, CE: BitsN.nbit, ExcCode: BitsN.nbit, IP: BitsN.nbit, 57 TI: bool, causeregister'rst: BitsN.nbit } 58 59type Context = 60 { BadVPN2: BitsN.nbit, PTEBase: BitsN.nbit, context'rst: BitsN.nbit } 61 62type XContext = 63 { BadVPN2: BitsN.nbit, PTEBase: BitsN.nbit, R: BitsN.nbit, 64 xcontext'rst: BitsN.nbit } 65 66type HWREna = 67 { CC: bool, CCRes: bool, CPUNum: bool, UL: bool, hwrena'rst: BitsN.nbit 68 } 69 70type CP0 = 71 { BadVAddr: BitsN.nbit, Cause: CauseRegister, Compare: BitsN.nbit, 72 Config: ConfigRegister, Config1: ConfigRegister1, 73 Config2: ConfigRegister2, Config3: ConfigRegister3, 74 Config6: ConfigRegister6, Context: Context, Count: BitsN.nbit, 75 Debug: BitsN.nbit, EPC: BitsN.nbit, EntryHi: EntryHi, 76 EntryLo0: EntryLo, EntryLo1: EntryLo, ErrCtl: BitsN.nbit, 77 ErrorEPC: BitsN.nbit, HWREna: HWREna, Index: Index, 78 LLAddr: BitsN.nbit, PRId: BitsN.nbit, PageMask: PageMask, 79 Random: Random, Status: StatusRegister, UsrLocal: BitsN.nbit, 80 Wired: Wired, XContext: XContext } 81 82datatype ExceptionType 83 = Int | Mod | TLBL | TLBS | AdEL | AdES | Sys | Bp | ResI | CpU | Ov 84 | Tr | XTLBRefillL | XTLBRefillS 85 86datatype LorS = LOAD | STORE 87 88type FCSR = 89 { ABS2008: bool, CauseE: bool, CauseI: bool, CauseO: bool, CauseU: bool, 90 CauseV: bool, CauseZ: bool, EnableI: bool, EnableO: bool, 91 EnableU: bool, EnableV: bool, EnableZ: bool, FCC: BitsN.nbit, 92 FS: bool, FlagI: bool, FlagO: bool, FlagU: bool, FlagV: bool, 93 FlagZ: bool, NAN2008: bool, RM: BitsN.nbit, fcsr'rst: BitsN.nbit } 94 95type FIR = 96 { ASE: bool, D: bool, F64: bool, L: bool, PS: bool, PrID: BitsN.nbit, 97 Rev: BitsN.nbit, S: bool, W: bool, fir'rst: BitsN.nbit } 98 99datatype Branch 100 = BEQ of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 101 | BEQL of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 102 | BGEZ of BitsN.nbit * BitsN.nbit 103 | BGEZAL of BitsN.nbit * BitsN.nbit 104 | BGEZALL of BitsN.nbit * BitsN.nbit 105 | BGEZL of BitsN.nbit * BitsN.nbit 106 | BGTZ of BitsN.nbit * BitsN.nbit 107 | BGTZL of BitsN.nbit * BitsN.nbit 108 | BLEZ of BitsN.nbit * BitsN.nbit 109 | BLEZL of BitsN.nbit * BitsN.nbit 110 | BLTZ of BitsN.nbit * BitsN.nbit 111 | BLTZAL of BitsN.nbit * BitsN.nbit 112 | BLTZALL of BitsN.nbit * BitsN.nbit 113 | BLTZL of BitsN.nbit * BitsN.nbit 114 | BNE of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 115 | BNEL of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 116 | J of BitsN.nbit 117 | JAL of BitsN.nbit 118 | JALR of BitsN.nbit * BitsN.nbit 119 | JR of BitsN.nbit 120 121datatype CP 122 = DMFC0 of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 123 | DMTC0 of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 124 | MFC0 of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 125 | MTC0 of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 126 127datatype Store 128 = SB of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 129 | SC of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 130 | SCD of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 131 | SD of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 132 | SDL of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 133 | SDR of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 134 | SH of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 135 | SW of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 136 | SWL of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 137 | SWR of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 138 139datatype Load 140 = LB of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 141 | LBU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 142 | LD of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 143 | LDL of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 144 | LDR of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 145 | LH of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 146 | LHU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 147 | LL of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 148 | LLD of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 149 | LW of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 150 | LWL of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 151 | LWR of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 152 | LWU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 153 154datatype Trap 155 = TEQ of BitsN.nbit * BitsN.nbit 156 | TEQI of BitsN.nbit * BitsN.nbit 157 | TGE of BitsN.nbit * BitsN.nbit 158 | TGEI of BitsN.nbit * BitsN.nbit 159 | TGEIU of BitsN.nbit * BitsN.nbit 160 | TGEU of BitsN.nbit * BitsN.nbit 161 | TLT of BitsN.nbit * BitsN.nbit 162 | TLTI of BitsN.nbit * BitsN.nbit 163 | TLTIU of BitsN.nbit * BitsN.nbit 164 | TLTU of BitsN.nbit * BitsN.nbit 165 | TNE of BitsN.nbit * BitsN.nbit 166 | TNEI of BitsN.nbit * BitsN.nbit 167 168datatype Shift 169 = DSLL of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 170 | DSLL32 of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 171 | DSLLV of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 172 | DSRA of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 173 | DSRA32 of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 174 | DSRAV of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 175 | DSRL of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 176 | DSRL32 of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 177 | DSRLV of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 178 | SLL of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 179 | SLLV of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 180 | SRA of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 181 | SRAV of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 182 | SRL of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 183 | SRLV of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 184 185datatype MultDiv 186 = DDIV of BitsN.nbit * BitsN.nbit 187 | DDIVU of BitsN.nbit * BitsN.nbit 188 | DIV of BitsN.nbit * BitsN.nbit 189 | DIVU of BitsN.nbit * BitsN.nbit 190 | DMULT of BitsN.nbit * BitsN.nbit 191 | DMULTU of BitsN.nbit * BitsN.nbit 192 | MADD of BitsN.nbit * BitsN.nbit 193 | MADDU of BitsN.nbit * BitsN.nbit 194 | MFHI of BitsN.nbit 195 | MFLO of BitsN.nbit 196 | MSUB of BitsN.nbit * BitsN.nbit 197 | MSUBU of BitsN.nbit * BitsN.nbit 198 | MTHI of BitsN.nbit 199 | MTLO of BitsN.nbit 200 | MUL of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 201 | MULT of BitsN.nbit * BitsN.nbit 202 | MULTU of BitsN.nbit * BitsN.nbit 203 204datatype ArithR 205 = ADD of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 206 | ADDU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 207 | AND of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 208 | DADD of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 209 | DADDU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 210 | DSUB of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 211 | DSUBU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 212 | MOVN of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 213 | MOVZ of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 214 | NOR of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 215 | OR of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 216 | SLT of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 217 | SLTU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 218 | SUB of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 219 | SUBU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 220 | XOR of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 221 222datatype ArithI 223 = ADDI of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 224 | ADDIU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 225 | ANDI of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 226 | DADDI of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 227 | DADDIU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 228 | LUI of BitsN.nbit * BitsN.nbit 229 | ORI of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 230 | SLTI of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 231 | SLTIU of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 232 | XORI of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 233 234datatype COP1 235 = ABS_D of BitsN.nbit * BitsN.nbit 236 | ABS_S of BitsN.nbit * BitsN.nbit 237 | ADD_D of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 238 | ADD_S of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 239 | BC1F of BitsN.nbit * BitsN.nbit 240 | BC1FL of BitsN.nbit * BitsN.nbit 241 | BC1T of BitsN.nbit * BitsN.nbit 242 | BC1TL of BitsN.nbit * BitsN.nbit 243 | CEIL_L_D of BitsN.nbit * BitsN.nbit 244 | CEIL_L_S of BitsN.nbit * BitsN.nbit 245 | CEIL_W_D of BitsN.nbit * BitsN.nbit 246 | CEIL_W_S of BitsN.nbit * BitsN.nbit 247 | CFC1 of BitsN.nbit * BitsN.nbit 248 | CTC1 of BitsN.nbit * BitsN.nbit 249 | CVT_D_L of BitsN.nbit * BitsN.nbit 250 | CVT_D_S of BitsN.nbit * BitsN.nbit 251 | CVT_D_W of BitsN.nbit * BitsN.nbit 252 | CVT_L_D of BitsN.nbit * BitsN.nbit 253 | CVT_L_S of BitsN.nbit * BitsN.nbit 254 | CVT_S_D of BitsN.nbit * BitsN.nbit 255 | CVT_S_L of BitsN.nbit * BitsN.nbit 256 | CVT_S_W of BitsN.nbit * BitsN.nbit 257 | CVT_W_D of BitsN.nbit * BitsN.nbit 258 | CVT_W_S of BitsN.nbit * BitsN.nbit 259 | C_cond_D of BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) 260 | C_cond_S of BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) 261 | DIV_D of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 262 | DIV_S of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 263 | DMFC1 of BitsN.nbit * BitsN.nbit 264 | DMTC1 of BitsN.nbit * BitsN.nbit 265 | FLOOR_L_D of BitsN.nbit * BitsN.nbit 266 | FLOOR_L_S of BitsN.nbit * BitsN.nbit 267 | FLOOR_W_D of BitsN.nbit * BitsN.nbit 268 | FLOOR_W_S of BitsN.nbit * BitsN.nbit 269 | LDC1 of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 270 | LDXC1 of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 271 | LWC1 of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 272 | LWXC1 of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 273 | MADD_D of BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) 274 | MADD_S of BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) 275 | MFC1 of BitsN.nbit * BitsN.nbit 276 | MOVF of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 277 | MOVF_D of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 278 | MOVF_S of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 279 | MOVN_D of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 280 | MOVN_S of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 281 | MOVT of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 282 | MOVT_D of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 283 | MOVT_S of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 284 | MOVZ_D of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 285 | MOVZ_S of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 286 | MOV_D of BitsN.nbit * BitsN.nbit 287 | MOV_S of BitsN.nbit * BitsN.nbit 288 | MSUB_D of BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) 289 | MSUB_S of BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) 290 | MTC1 of BitsN.nbit * BitsN.nbit 291 | MUL_D of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 292 | MUL_S of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 293 | NEG_D of BitsN.nbit * BitsN.nbit 294 | NEG_S of BitsN.nbit * BitsN.nbit 295 | ROUND_L_D of BitsN.nbit * BitsN.nbit 296 | ROUND_L_S of BitsN.nbit * BitsN.nbit 297 | ROUND_W_D of BitsN.nbit * BitsN.nbit 298 | ROUND_W_S of BitsN.nbit * BitsN.nbit 299 | SDC1 of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 300 | SDXC1 of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 301 | SQRT_D of BitsN.nbit * BitsN.nbit 302 | SQRT_S of BitsN.nbit * BitsN.nbit 303 | SUB_D of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 304 | SUB_S of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 305 | SWC1 of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 306 | SWXC1 of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 307 | TRUNC_L_D of BitsN.nbit * BitsN.nbit 308 | TRUNC_L_S of BitsN.nbit * BitsN.nbit 309 | TRUNC_W_D of BitsN.nbit * BitsN.nbit 310 | TRUNC_W_S of BitsN.nbit * BitsN.nbit 311 | UnknownFPInstruction 312 313datatype instruction 314 = ArithI of ArithI 315 | ArithR of ArithR 316 | BREAK 317 | Branch of Branch 318 | CACHE of BitsN.nbit * (BitsN.nbit * BitsN.nbit) 319 | COP1 of COP1 320 | CP of CP 321 | ERET 322 | Load of Load 323 | MultDiv of MultDiv 324 | RDHWR of BitsN.nbit * BitsN.nbit 325 | ReservedInstruction 326 | SYNC of BitsN.nbit 327 | SYSCALL 328 | Shift of Shift 329 | Store of Store 330 | TLBP 331 | TLBR 332 | TLBWI 333 | TLBWR 334 | Trap of Trap 335 | Unpredictable 336 | WAIT 337 338datatype maybe_instruction 339 = FAIL of string | OK of instruction | WORD32 of BitsN.nbit 340 341(* ------------------------------------------------------------------------- 342 Exceptions 343 ------------------------------------------------------------------------- *) 344 345exception UNPREDICTABLE of string 346 347(* ------------------------------------------------------------------------- 348 Functions 349 ------------------------------------------------------------------------- *) 350 351structure Cast: 352sig 353 354val natToExceptionType: Nat.nat -> ExceptionType 355val ExceptionTypeToNat: ExceptionType -> Nat.nat 356val stringToExceptionType: string -> ExceptionType 357val ExceptionTypeToString: ExceptionType -> string 358val natToLorS: Nat.nat -> LorS 359val LorSToNat: LorS -> Nat.nat 360val stringToLorS: string -> LorS 361val LorSToString: LorS -> string 362 363end 364 365val BranchDelay: ((BitsN.nbit option) option) ref 366val BranchTo: ((bool * BitsN.nbit) option) ref 367val CP0: CP0 ref 368val FGR: (BitsN.nbit Map.map) ref 369val LLbit: (bool option) ref 370val MEM: (BitsN.nbit Map.map) ref 371val PC: BitsN.nbit ref 372val exceptionSignalled: bool ref 373val fcsr: FCSR ref 374val fir: FIR ref 375val gpr: (BitsN.nbit Map.map) ref 376val hi: (BitsN.nbit option) ref 377val lo: (BitsN.nbit option) ref 378val Index_Index_rupd: Index * BitsN.nbit -> Index 379val Index_P_rupd: Index * bool -> Index 380val Index_index'rst_rupd: Index * BitsN.nbit -> Index 381val Random_Random_rupd: Random * BitsN.nbit -> Random 382val Random_random'rst_rupd: Random * BitsN.nbit -> Random 383val Wired_Wired_rupd: Wired * BitsN.nbit -> Wired 384val Wired_wired'rst_rupd: Wired * BitsN.nbit -> Wired 385val EntryLo_C_rupd: EntryLo * BitsN.nbit -> EntryLo 386val EntryLo_D_rupd: EntryLo * bool -> EntryLo 387val EntryLo_G_rupd: EntryLo * bool -> EntryLo 388val EntryLo_PFN_rupd: EntryLo * BitsN.nbit -> EntryLo 389val EntryLo_V_rupd: EntryLo * bool -> EntryLo 390val EntryLo_entrylo'rst_rupd: EntryLo * BitsN.nbit -> EntryLo 391val PageMask_Mask_rupd: PageMask * BitsN.nbit -> PageMask 392val PageMask_pagemask'rst_rupd: PageMask * BitsN.nbit -> PageMask 393val EntryHi_ASID_rupd: EntryHi * BitsN.nbit -> EntryHi 394val EntryHi_R_rupd: EntryHi * BitsN.nbit -> EntryHi 395val EntryHi_VPN2_rupd: EntryHi * BitsN.nbit -> EntryHi 396val EntryHi_entryhi'rst_rupd: EntryHi * BitsN.nbit -> EntryHi 397val StatusRegister_BEV_rupd: StatusRegister * bool -> StatusRegister 398val StatusRegister_CU0_rupd: StatusRegister * bool -> StatusRegister 399val StatusRegister_CU1_rupd: StatusRegister * bool -> StatusRegister 400val StatusRegister_ERL_rupd: StatusRegister * bool -> StatusRegister 401val StatusRegister_EXL_rupd: StatusRegister * bool -> StatusRegister 402val StatusRegister_FR_rupd: StatusRegister * bool -> StatusRegister 403val StatusRegister_IE_rupd: StatusRegister * bool -> StatusRegister 404val StatusRegister_IM_rupd: StatusRegister * BitsN.nbit -> StatusRegister 405val StatusRegister_KSU_rupd: StatusRegister * BitsN.nbit -> StatusRegister 406val StatusRegister_KX_rupd: StatusRegister * bool -> StatusRegister 407val StatusRegister_RE_rupd: StatusRegister * bool -> StatusRegister 408val StatusRegister_SX_rupd: StatusRegister * bool -> StatusRegister 409val StatusRegister_UX_rupd: StatusRegister * bool -> StatusRegister 410val StatusRegister_statusregister'rst_rupd: 411 StatusRegister * BitsN.nbit -> StatusRegister 412val ConfigRegister_AR_rupd: ConfigRegister * BitsN.nbit -> ConfigRegister 413val ConfigRegister_AT_rupd: ConfigRegister * BitsN.nbit -> ConfigRegister 414val ConfigRegister_BE_rupd: ConfigRegister * bool -> ConfigRegister 415val ConfigRegister_K0_rupd: ConfigRegister * BitsN.nbit -> ConfigRegister 416val ConfigRegister_M_rupd: ConfigRegister * bool -> ConfigRegister 417val ConfigRegister_MT_rupd: ConfigRegister * BitsN.nbit -> ConfigRegister 418val ConfigRegister_configregister'rst_rupd: 419 ConfigRegister * BitsN.nbit -> ConfigRegister 420val ConfigRegister1_C2_rupd: ConfigRegister1 * bool -> ConfigRegister1 421val ConfigRegister1_CA_rupd: ConfigRegister1 * bool -> ConfigRegister1 422val ConfigRegister1_DA_rupd: 423 ConfigRegister1 * BitsN.nbit -> ConfigRegister1 424val ConfigRegister1_DL_rupd: 425 ConfigRegister1 * BitsN.nbit -> ConfigRegister1 426val ConfigRegister1_DS_rupd: 427 ConfigRegister1 * BitsN.nbit -> ConfigRegister1 428val ConfigRegister1_EP_rupd: ConfigRegister1 * bool -> ConfigRegister1 429val ConfigRegister1_FP_rupd: ConfigRegister1 * bool -> ConfigRegister1 430val ConfigRegister1_IA_rupd: 431 ConfigRegister1 * BitsN.nbit -> ConfigRegister1 432val ConfigRegister1_IL_rupd: 433 ConfigRegister1 * BitsN.nbit -> ConfigRegister1 434val ConfigRegister1_IS_rupd: 435 ConfigRegister1 * BitsN.nbit -> ConfigRegister1 436val ConfigRegister1_M_rupd: ConfigRegister1 * bool -> ConfigRegister1 437val ConfigRegister1_MD_rupd: ConfigRegister1 * bool -> ConfigRegister1 438val ConfigRegister1_MMUSize_rupd: 439 ConfigRegister1 * BitsN.nbit -> ConfigRegister1 440val ConfigRegister1_PC_rupd: ConfigRegister1 * bool -> ConfigRegister1 441val ConfigRegister1_WR_rupd: ConfigRegister1 * bool -> ConfigRegister1 442val ConfigRegister2_M_rupd: ConfigRegister2 * bool -> ConfigRegister2 443val ConfigRegister2_SA_rupd: 444 ConfigRegister2 * BitsN.nbit -> ConfigRegister2 445val ConfigRegister2_SL_rupd: 446 ConfigRegister2 * BitsN.nbit -> ConfigRegister2 447val ConfigRegister2_SS_rupd: 448 ConfigRegister2 * BitsN.nbit -> ConfigRegister2 449val ConfigRegister2_SU_rupd: 450 ConfigRegister2 * BitsN.nbit -> ConfigRegister2 451val ConfigRegister2_TA_rupd: 452 ConfigRegister2 * BitsN.nbit -> ConfigRegister2 453val ConfigRegister2_TL_rupd: 454 ConfigRegister2 * BitsN.nbit -> ConfigRegister2 455val ConfigRegister2_TS_rupd: 456 ConfigRegister2 * BitsN.nbit -> ConfigRegister2 457val ConfigRegister2_TU_rupd: 458 ConfigRegister2 * BitsN.nbit -> ConfigRegister2 459val ConfigRegister3_DSPP_rupd: ConfigRegister3 * bool -> ConfigRegister3 460val ConfigRegister3_LPA_rupd: ConfigRegister3 * bool -> ConfigRegister3 461val ConfigRegister3_M_rupd: ConfigRegister3 * bool -> ConfigRegister3 462val ConfigRegister3_MT_rupd: ConfigRegister3 * bool -> ConfigRegister3 463val ConfigRegister3_SM_rupd: ConfigRegister3 * bool -> ConfigRegister3 464val ConfigRegister3_SP_rupd: ConfigRegister3 * bool -> ConfigRegister3 465val ConfigRegister3_TL_rupd: ConfigRegister3 * bool -> ConfigRegister3 466val ConfigRegister3_ULRI_rupd: ConfigRegister3 * bool -> ConfigRegister3 467val ConfigRegister3_VEIC_rupd: ConfigRegister3 * bool -> ConfigRegister3 468val ConfigRegister3_VInt_rupd: ConfigRegister3 * bool -> ConfigRegister3 469val ConfigRegister3_configregister3'rst_rupd: 470 ConfigRegister3 * BitsN.nbit -> ConfigRegister3 471val ConfigRegister6_LTLB_rupd: ConfigRegister6 * bool -> ConfigRegister6 472val ConfigRegister6_TLBSize_rupd: 473 ConfigRegister6 * BitsN.nbit -> ConfigRegister6 474val ConfigRegister6_configregister6'rst_rupd: 475 ConfigRegister6 * BitsN.nbit -> ConfigRegister6 476val CauseRegister_BD_rupd: CauseRegister * bool -> CauseRegister 477val CauseRegister_CE_rupd: CauseRegister * BitsN.nbit -> CauseRegister 478val CauseRegister_ExcCode_rupd: 479 CauseRegister * BitsN.nbit -> CauseRegister 480val CauseRegister_IP_rupd: CauseRegister * BitsN.nbit -> CauseRegister 481val CauseRegister_TI_rupd: CauseRegister * bool -> CauseRegister 482val CauseRegister_causeregister'rst_rupd: 483 CauseRegister * BitsN.nbit -> CauseRegister 484val Context_BadVPN2_rupd: Context * BitsN.nbit -> Context 485val Context_PTEBase_rupd: Context * BitsN.nbit -> Context 486val Context_context'rst_rupd: Context * BitsN.nbit -> Context 487val XContext_BadVPN2_rupd: XContext * BitsN.nbit -> XContext 488val XContext_PTEBase_rupd: XContext * BitsN.nbit -> XContext 489val XContext_R_rupd: XContext * BitsN.nbit -> XContext 490val XContext_xcontext'rst_rupd: XContext * BitsN.nbit -> XContext 491val HWREna_CC_rupd: HWREna * bool -> HWREna 492val HWREna_CCRes_rupd: HWREna * bool -> HWREna 493val HWREna_CPUNum_rupd: HWREna * bool -> HWREna 494val HWREna_UL_rupd: HWREna * bool -> HWREna 495val HWREna_hwrena'rst_rupd: HWREna * BitsN.nbit -> HWREna 496val CP0_BadVAddr_rupd: CP0 * BitsN.nbit -> CP0 497val CP0_Cause_rupd: CP0 * CauseRegister -> CP0 498val CP0_Compare_rupd: CP0 * BitsN.nbit -> CP0 499val CP0_Config_rupd: CP0 * ConfigRegister -> CP0 500val CP0_Config1_rupd: CP0 * ConfigRegister1 -> CP0 501val CP0_Config2_rupd: CP0 * ConfigRegister2 -> CP0 502val CP0_Config3_rupd: CP0 * ConfigRegister3 -> CP0 503val CP0_Config6_rupd: CP0 * ConfigRegister6 -> CP0 504val CP0_Context_rupd: CP0 * Context -> CP0 505val CP0_Count_rupd: CP0 * BitsN.nbit -> CP0 506val CP0_Debug_rupd: CP0 * BitsN.nbit -> CP0 507val CP0_EPC_rupd: CP0 * BitsN.nbit -> CP0 508val CP0_EntryHi_rupd: CP0 * EntryHi -> CP0 509val CP0_EntryLo0_rupd: CP0 * EntryLo -> CP0 510val CP0_EntryLo1_rupd: CP0 * EntryLo -> CP0 511val CP0_ErrCtl_rupd: CP0 * BitsN.nbit -> CP0 512val CP0_ErrorEPC_rupd: CP0 * BitsN.nbit -> CP0 513val CP0_HWREna_rupd: CP0 * HWREna -> CP0 514val CP0_Index_rupd: CP0 * Index -> CP0 515val CP0_LLAddr_rupd: CP0 * BitsN.nbit -> CP0 516val CP0_PRId_rupd: CP0 * BitsN.nbit -> CP0 517val CP0_PageMask_rupd: CP0 * PageMask -> CP0 518val CP0_Random_rupd: CP0 * Random -> CP0 519val CP0_Status_rupd: CP0 * StatusRegister -> CP0 520val CP0_UsrLocal_rupd: CP0 * BitsN.nbit -> CP0 521val CP0_Wired_rupd: CP0 * Wired -> CP0 522val CP0_XContext_rupd: CP0 * XContext -> CP0 523val FCSR_ABS2008_rupd: FCSR * bool -> FCSR 524val FCSR_CauseE_rupd: FCSR * bool -> FCSR 525val FCSR_CauseI_rupd: FCSR * bool -> FCSR 526val FCSR_CauseO_rupd: FCSR * bool -> FCSR 527val FCSR_CauseU_rupd: FCSR * bool -> FCSR 528val FCSR_CauseV_rupd: FCSR * bool -> FCSR 529val FCSR_CauseZ_rupd: FCSR * bool -> FCSR 530val FCSR_EnableI_rupd: FCSR * bool -> FCSR 531val FCSR_EnableO_rupd: FCSR * bool -> FCSR 532val FCSR_EnableU_rupd: FCSR * bool -> FCSR 533val FCSR_EnableV_rupd: FCSR * bool -> FCSR 534val FCSR_EnableZ_rupd: FCSR * bool -> FCSR 535val FCSR_FCC_rupd: FCSR * BitsN.nbit -> FCSR 536val FCSR_FS_rupd: FCSR * bool -> FCSR 537val FCSR_FlagI_rupd: FCSR * bool -> FCSR 538val FCSR_FlagO_rupd: FCSR * bool -> FCSR 539val FCSR_FlagU_rupd: FCSR * bool -> FCSR 540val FCSR_FlagV_rupd: FCSR * bool -> FCSR 541val FCSR_FlagZ_rupd: FCSR * bool -> FCSR 542val FCSR_NAN2008_rupd: FCSR * bool -> FCSR 543val FCSR_RM_rupd: FCSR * BitsN.nbit -> FCSR 544val FCSR_fcsr'rst_rupd: FCSR * BitsN.nbit -> FCSR 545val FIR_ASE_rupd: FIR * bool -> FIR 546val FIR_D_rupd: FIR * bool -> FIR 547val FIR_F64_rupd: FIR * bool -> FIR 548val FIR_L_rupd: FIR * bool -> FIR 549val FIR_PS_rupd: FIR * bool -> FIR 550val FIR_PrID_rupd: FIR * BitsN.nbit -> FIR 551val FIR_Rev_rupd: FIR * BitsN.nbit -> FIR 552val FIR_S_rupd: FIR * bool -> FIR 553val FIR_W_rupd: FIR * bool -> FIR 554val FIR_fir'rst_rupd: FIR * BitsN.nbit -> FIR 555val boolify'32: 556 BitsN.nbit -> 557 bool * 558 (bool * 559 (bool * 560 (bool * 561 (bool * 562 (bool * 563 (bool * 564 (bool * 565 (bool * 566 (bool * 567 (bool * 568 (bool * 569 (bool * 570 (bool * 571 (bool * 572 (bool * 573 (bool * 574 (bool * 575 (bool * 576 (bool * 577 (bool * 578 (bool * 579 (bool * 580 (bool * 581 (bool * 582 (bool * 583 (bool * 584 (bool * (bool * (bool * (bool * bool)))))))))))))))))))))))))))))) 585val boolify'5: BitsN.nbit -> bool * (bool * (bool * (bool * bool))) 586val boolify'26: 587 BitsN.nbit -> 588 bool * 589 (bool * 590 (bool * 591 (bool * 592 (bool * 593 (bool * 594 (bool * 595 (bool * 596 (bool * 597 (bool * 598 (bool * 599 (bool * 600 (bool * 601 (bool * 602 (bool * 603 (bool * 604 (bool * 605 (bool * 606 (bool * 607 (bool * 608 (bool * (bool * (bool * (bool * (bool * bool)))))))))))))))))))))))) 609val rec'Index: BitsN.nbit -> Index 610val reg'Index: Index -> BitsN.nbit 611val write'rec'Index: (BitsN.nbit * Index) -> BitsN.nbit 612val write'reg'Index: (Index * BitsN.nbit) -> Index 613val rec'Random: BitsN.nbit -> Random 614val reg'Random: Random -> BitsN.nbit 615val write'rec'Random: (BitsN.nbit * Random) -> BitsN.nbit 616val write'reg'Random: (Random * BitsN.nbit) -> Random 617val rec'Wired: BitsN.nbit -> Wired 618val reg'Wired: Wired -> BitsN.nbit 619val write'rec'Wired: (BitsN.nbit * Wired) -> BitsN.nbit 620val write'reg'Wired: (Wired * BitsN.nbit) -> Wired 621val rec'EntryLo: BitsN.nbit -> EntryLo 622val reg'EntryLo: EntryLo -> BitsN.nbit 623val write'rec'EntryLo: (BitsN.nbit * EntryLo) -> BitsN.nbit 624val write'reg'EntryLo: (EntryLo * BitsN.nbit) -> EntryLo 625val rec'PageMask: BitsN.nbit -> PageMask 626val reg'PageMask: PageMask -> BitsN.nbit 627val write'rec'PageMask: (BitsN.nbit * PageMask) -> BitsN.nbit 628val write'reg'PageMask: (PageMask * BitsN.nbit) -> PageMask 629val rec'EntryHi: BitsN.nbit -> EntryHi 630val reg'EntryHi: EntryHi -> BitsN.nbit 631val write'rec'EntryHi: (BitsN.nbit * EntryHi) -> BitsN.nbit 632val write'reg'EntryHi: (EntryHi * BitsN.nbit) -> EntryHi 633val rec'StatusRegister: BitsN.nbit -> StatusRegister 634val reg'StatusRegister: StatusRegister -> BitsN.nbit 635val write'rec'StatusRegister: (BitsN.nbit * StatusRegister) -> BitsN.nbit 636val write'reg'StatusRegister: 637 (StatusRegister * BitsN.nbit) -> StatusRegister 638val rec'ConfigRegister: BitsN.nbit -> ConfigRegister 639val reg'ConfigRegister: ConfigRegister -> BitsN.nbit 640val write'rec'ConfigRegister: (BitsN.nbit * ConfigRegister) -> BitsN.nbit 641val write'reg'ConfigRegister: 642 (ConfigRegister * BitsN.nbit) -> ConfigRegister 643val rec'ConfigRegister1: BitsN.nbit -> ConfigRegister1 644val reg'ConfigRegister1: ConfigRegister1 -> BitsN.nbit 645val write'rec'ConfigRegister1: 646 (BitsN.nbit * ConfigRegister1) -> BitsN.nbit 647val write'reg'ConfigRegister1: 648 (ConfigRegister1 * BitsN.nbit) -> ConfigRegister1 649val rec'ConfigRegister2: BitsN.nbit -> ConfigRegister2 650val reg'ConfigRegister2: ConfigRegister2 -> BitsN.nbit 651val write'rec'ConfigRegister2: 652 (BitsN.nbit * ConfigRegister2) -> BitsN.nbit 653val write'reg'ConfigRegister2: 654 (ConfigRegister2 * BitsN.nbit) -> ConfigRegister2 655val rec'ConfigRegister3: BitsN.nbit -> ConfigRegister3 656val reg'ConfigRegister3: ConfigRegister3 -> BitsN.nbit 657val write'rec'ConfigRegister3: 658 (BitsN.nbit * ConfigRegister3) -> BitsN.nbit 659val write'reg'ConfigRegister3: 660 (ConfigRegister3 * BitsN.nbit) -> ConfigRegister3 661val rec'ConfigRegister6: BitsN.nbit -> ConfigRegister6 662val reg'ConfigRegister6: ConfigRegister6 -> BitsN.nbit 663val write'rec'ConfigRegister6: 664 (BitsN.nbit * ConfigRegister6) -> BitsN.nbit 665val write'reg'ConfigRegister6: 666 (ConfigRegister6 * BitsN.nbit) -> ConfigRegister6 667val rec'CauseRegister: BitsN.nbit -> CauseRegister 668val reg'CauseRegister: CauseRegister -> BitsN.nbit 669val write'rec'CauseRegister: (BitsN.nbit * CauseRegister) -> BitsN.nbit 670val write'reg'CauseRegister: (CauseRegister * BitsN.nbit) -> CauseRegister 671val rec'Context: BitsN.nbit -> Context 672val reg'Context: Context -> BitsN.nbit 673val write'rec'Context: (BitsN.nbit * Context) -> BitsN.nbit 674val write'reg'Context: (Context * BitsN.nbit) -> Context 675val rec'XContext: BitsN.nbit -> XContext 676val reg'XContext: XContext -> BitsN.nbit 677val write'rec'XContext: (BitsN.nbit * XContext) -> BitsN.nbit 678val write'reg'XContext: (XContext * BitsN.nbit) -> XContext 679val rec'HWREna: BitsN.nbit -> HWREna 680val reg'HWREna: HWREna -> BitsN.nbit 681val write'rec'HWREna: (BitsN.nbit * HWREna) -> BitsN.nbit 682val write'reg'HWREna: (HWREna * BitsN.nbit) -> HWREna 683val ConditionalBranch: (bool * BitsN.nbit) -> unit 684val ConditionalBranchLikely: (bool * BitsN.nbit) -> unit 685val NotWordValue: BitsN.nbit -> bool 686val ExceptionCode: ExceptionType -> unit 687val SignalException: ExceptionType -> unit 688val SignalCP1UnusableException: unit -> unit 689val UserMode: unit -> bool 690val SupervisorMode: unit -> bool 691val KernelMode: unit -> bool 692val GPR: BitsN.nbit -> BitsN.nbit 693val write'GPR: (BitsN.nbit * BitsN.nbit) -> unit 694val HI: unit -> BitsN.nbit 695val write'HI: BitsN.nbit -> unit 696val LO: unit -> BitsN.nbit 697val write'LO: BitsN.nbit -> unit 698val CPR: (Nat.nat * (BitsN.nbit * BitsN.nbit)) -> BitsN.nbit 699val write'CPR: 700 (BitsN.nbit * (Nat.nat * (BitsN.nbit * BitsN.nbit))) -> unit 701val BYTE: BitsN.nbit 702val HALFWORD: BitsN.nbit 703val WORD: BitsN.nbit 704val DOUBLEWORD: BitsN.nbit 705val BigEndianMem: unit -> bool 706val ReverseEndian: unit -> BitsN.nbit 707val BigEndianCPU: unit -> BitsN.nbit 708val AddressTranslation: (BitsN.nbit * LorS) -> (BitsN.nbit * BitsN.nbit) 709val Aligned: (BitsN.nbit * BitsN.nbit) -> bool 710val AdjustEndian: (BitsN.nbit * BitsN.nbit) -> BitsN.nbit 711val ReadData: BitsN.nbit -> BitsN.nbit 712val LoadMemory: 713 (BitsN.nbit * (BitsN.nbit * (bool * (BitsN.nbit * (bool option))))) -> 714 BitsN.nbit 715val loadByte: (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * bool))) -> unit 716val loadHalf: (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * bool))) -> unit 717val loadWord: 718 (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * bool)))) -> unit 719val loadDoubleword: 720 (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit 721val Fetch: unit -> (BitsN.nbit option) 722val WriteData: (BitsN.nbit * (BitsN.nbit * (Nat.nat * Nat.nat))) -> unit 723val StoreMemory: 724 (BitsN.nbit * (BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * bool))))) -> 725 bool 726val storeWord: (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * bool))) -> bool 727val storeDoubleword: 728 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * bool))) -> bool 729val rec'FCSR: BitsN.nbit -> FCSR 730val reg'FCSR: FCSR -> BitsN.nbit 731val write'rec'FCSR: (BitsN.nbit * FCSR) -> BitsN.nbit 732val write'reg'FCSR: (FCSR * BitsN.nbit) -> FCSR 733val rec'FIR: BitsN.nbit -> FIR 734val reg'FIR: FIR -> BitsN.nbit 735val write'rec'FIR: (BitsN.nbit * FIR) -> BitsN.nbit 736val write'reg'FIR: (FIR * BitsN.nbit) -> FIR 737val IntToWordMIPS: IntInf.int -> BitsN.nbit 738val IntToDWordMIPS: IntInf.int -> BitsN.nbit 739val PostOpF32: BitsN.nbit -> BitsN.nbit 740val PostOpF64: BitsN.nbit -> BitsN.nbit 741val FP32_Abs1985: BitsN.nbit -> BitsN.nbit 742val FP32_Neg1985: BitsN.nbit -> BitsN.nbit 743val FP64_Abs1985: BitsN.nbit -> BitsN.nbit 744val FP64_Neg1985: BitsN.nbit -> BitsN.nbit 745val FP64_Unordered: (BitsN.nbit * BitsN.nbit) -> bool 746val FP32_Unordered: (BitsN.nbit * BitsN.nbit) -> bool 747val Rounding_Mode: unit -> IEEEReal.rounding_mode 748val dfn'ABS_D: (BitsN.nbit * BitsN.nbit) -> unit 749val dfn'ABS_S: (BitsN.nbit * BitsN.nbit) -> unit 750val dfn'ADD_D: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 751val dfn'ADD_S: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 752val dfn'BC1F: (BitsN.nbit * BitsN.nbit) -> unit 753val dfn'BC1FL: (BitsN.nbit * BitsN.nbit) -> unit 754val dfn'BC1T: (BitsN.nbit * BitsN.nbit) -> unit 755val dfn'BC1TL: (BitsN.nbit * BitsN.nbit) -> unit 756val dfn'C_cond_D: 757 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit 758val dfn'C_cond_S: 759 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit 760val dfn'CEIL_L_D: (BitsN.nbit * BitsN.nbit) -> unit 761val dfn'CEIL_L_S: (BitsN.nbit * BitsN.nbit) -> unit 762val dfn'CEIL_W_D: (BitsN.nbit * BitsN.nbit) -> unit 763val dfn'CEIL_W_S: (BitsN.nbit * BitsN.nbit) -> unit 764val dfn'CVT_D_L: (BitsN.nbit * BitsN.nbit) -> unit 765val dfn'CVT_D_S: (BitsN.nbit * BitsN.nbit) -> unit 766val dfn'CVT_D_W: (BitsN.nbit * BitsN.nbit) -> unit 767val dfn'CVT_L_D: (BitsN.nbit * BitsN.nbit) -> unit 768val dfn'CVT_L_S: (BitsN.nbit * BitsN.nbit) -> unit 769val dfn'CVT_S_D: (BitsN.nbit * BitsN.nbit) -> unit 770val dfn'CVT_S_L: (BitsN.nbit * BitsN.nbit) -> unit 771val dfn'CVT_S_W: (BitsN.nbit * BitsN.nbit) -> unit 772val dfn'CVT_W_D: (BitsN.nbit * BitsN.nbit) -> unit 773val dfn'CVT_W_S: (BitsN.nbit * BitsN.nbit) -> unit 774val dfn'DIV_D: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 775val dfn'DIV_S: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 776val dfn'FLOOR_L_D: (BitsN.nbit * BitsN.nbit) -> unit 777val dfn'FLOOR_L_S: (BitsN.nbit * BitsN.nbit) -> unit 778val dfn'FLOOR_W_D: (BitsN.nbit * BitsN.nbit) -> unit 779val dfn'FLOOR_W_S: (BitsN.nbit * BitsN.nbit) -> unit 780val dfn'LDC1: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 781val dfn'LDXC1: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 782val dfn'LWC1: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 783val dfn'LWXC1: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 784val dfn'MADD_D: 785 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit 786val dfn'MADD_S: 787 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit 788val dfn'MOV_D: (BitsN.nbit * BitsN.nbit) -> unit 789val dfn'MOV_S: (BitsN.nbit * BitsN.nbit) -> unit 790val dfn'MOVF: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 791val dfn'MOVF_D: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 792val dfn'MOVF_S: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 793val dfn'MOVN_D: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 794val dfn'MOVN_S: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 795val dfn'MOVT: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 796val dfn'MOVT_D: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 797val dfn'MOVT_S: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 798val dfn'MOVZ_D: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 799val dfn'MOVZ_S: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 800val dfn'MSUB_D: 801 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit 802val dfn'MSUB_S: 803 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit 804val dfn'MUL_D: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 805val dfn'MUL_S: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 806val dfn'NEG_D: (BitsN.nbit * BitsN.nbit) -> unit 807val dfn'NEG_S: (BitsN.nbit * BitsN.nbit) -> unit 808val dfn'ROUND_L_D: (BitsN.nbit * BitsN.nbit) -> unit 809val dfn'ROUND_L_S: (BitsN.nbit * BitsN.nbit) -> unit 810val dfn'ROUND_W_D: (BitsN.nbit * BitsN.nbit) -> unit 811val dfn'ROUND_W_S: (BitsN.nbit * BitsN.nbit) -> unit 812val dfn'SDC1: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 813val dfn'SDXC1: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 814val dfn'SQRT_D: (BitsN.nbit * BitsN.nbit) -> unit 815val dfn'SQRT_S: (BitsN.nbit * BitsN.nbit) -> unit 816val dfn'SUB_D: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 817val dfn'SUB_S: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 818val dfn'SWC1: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 819val dfn'SWXC1: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 820val dfn'TRUNC_L_D: (BitsN.nbit * BitsN.nbit) -> unit 821val dfn'TRUNC_L_S: (BitsN.nbit * BitsN.nbit) -> unit 822val dfn'TRUNC_W_D: (BitsN.nbit * BitsN.nbit) -> unit 823val dfn'TRUNC_W_S: (BitsN.nbit * BitsN.nbit) -> unit 824val dfn'DMFC1: (BitsN.nbit * BitsN.nbit) -> unit 825val dfn'DMTC1: (BitsN.nbit * BitsN.nbit) -> unit 826val dfn'MFC1: (BitsN.nbit * BitsN.nbit) -> unit 827val dfn'MTC1: (BitsN.nbit * BitsN.nbit) -> unit 828val dfn'CFC1: (BitsN.nbit * BitsN.nbit) -> unit 829val dfn'CTC1: (BitsN.nbit * BitsN.nbit) -> unit 830val dfn'UnknownFPInstruction: unit -> unit 831val dfn'ADDI: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 832val dfn'ADDIU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 833val dfn'DADDI: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 834val dfn'DADDIU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 835val dfn'SLTI: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 836val dfn'SLTIU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 837val dfn'ANDI: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 838val dfn'ORI: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 839val dfn'XORI: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 840val dfn'LUI: (BitsN.nbit * BitsN.nbit) -> unit 841val dfn'ADD: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 842val dfn'ADDU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 843val dfn'SUB: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 844val dfn'SUBU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 845val dfn'DADD: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 846val dfn'DADDU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 847val dfn'DSUB: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 848val dfn'DSUBU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 849val dfn'SLT: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 850val dfn'SLTU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 851val dfn'AND: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 852val dfn'OR: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 853val dfn'XOR: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 854val dfn'NOR: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 855val dfn'MOVN: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 856val dfn'MOVZ: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 857val dfn'MADD: (BitsN.nbit * BitsN.nbit) -> unit 858val dfn'MADDU: (BitsN.nbit * BitsN.nbit) -> unit 859val dfn'MSUB: (BitsN.nbit * BitsN.nbit) -> unit 860val dfn'MSUBU: (BitsN.nbit * BitsN.nbit) -> unit 861val dfn'MUL: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 862val dfn'MULT: (BitsN.nbit * BitsN.nbit) -> unit 863val dfn'MULTU: (BitsN.nbit * BitsN.nbit) -> unit 864val dfn'DMULT: (BitsN.nbit * BitsN.nbit) -> unit 865val dfn'DMULTU: (BitsN.nbit * BitsN.nbit) -> unit 866val dfn'DIV: (BitsN.nbit * BitsN.nbit) -> unit 867val dfn'DIVU: (BitsN.nbit * BitsN.nbit) -> unit 868val dfn'DDIV: (BitsN.nbit * BitsN.nbit) -> unit 869val dfn'DDIVU: (BitsN.nbit * BitsN.nbit) -> unit 870val dfn'MFHI: BitsN.nbit -> unit 871val dfn'MFLO: BitsN.nbit -> unit 872val dfn'MTHI: BitsN.nbit -> unit 873val dfn'MTLO: BitsN.nbit -> unit 874val dfn'SLL: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 875val dfn'SRL: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 876val dfn'SRA: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 877val dfn'SLLV: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 878val dfn'SRLV: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 879val dfn'SRAV: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 880val dfn'DSLL: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 881val dfn'DSRL: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 882val dfn'DSRA: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 883val dfn'DSLLV: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 884val dfn'DSRLV: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 885val dfn'DSRAV: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 886val dfn'DSLL32: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 887val dfn'DSRL32: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 888val dfn'DSRA32: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 889val dfn'TGE: (BitsN.nbit * BitsN.nbit) -> unit 890val dfn'TGEU: (BitsN.nbit * BitsN.nbit) -> unit 891val dfn'TLT: (BitsN.nbit * BitsN.nbit) -> unit 892val dfn'TLTU: (BitsN.nbit * BitsN.nbit) -> unit 893val dfn'TEQ: (BitsN.nbit * BitsN.nbit) -> unit 894val dfn'TNE: (BitsN.nbit * BitsN.nbit) -> unit 895val dfn'TGEI: (BitsN.nbit * BitsN.nbit) -> unit 896val dfn'TGEIU: (BitsN.nbit * BitsN.nbit) -> unit 897val dfn'TLTI: (BitsN.nbit * BitsN.nbit) -> unit 898val dfn'TLTIU: (BitsN.nbit * BitsN.nbit) -> unit 899val dfn'TEQI: (BitsN.nbit * BitsN.nbit) -> unit 900val dfn'TNEI: (BitsN.nbit * BitsN.nbit) -> unit 901val dfn'LB: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 902val dfn'LBU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 903val dfn'LH: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 904val dfn'LHU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 905val dfn'LW: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 906val dfn'LWU: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 907val dfn'LL: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 908val dfn'LD: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 909val dfn'LLD: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 910val dfn'LWL: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 911val dfn'LWR: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 912val dfn'LDL: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 913val dfn'LDR: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 914val dfn'SB: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 915val dfn'SH: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 916val dfn'SW: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 917val dfn'SD: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 918val dfn'SC: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 919val dfn'SCD: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 920val dfn'SWL: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 921val dfn'SWR: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 922val dfn'SDL: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 923val dfn'SDR: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 924val dfn'SYNC: BitsN.nbit -> unit 925val dfn'BREAK: unit -> unit 926val dfn'SYSCALL: unit -> unit 927val dfn'ERET: unit -> unit 928val dfn'MTC0: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 929val dfn'DMTC0: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 930val dfn'MFC0: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 931val dfn'DMFC0: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 932val dfn'J: BitsN.nbit -> unit 933val dfn'JAL: BitsN.nbit -> unit 934val dfn'JR: BitsN.nbit -> unit 935val dfn'JALR: (BitsN.nbit * BitsN.nbit) -> unit 936val dfn'BEQ: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 937val dfn'BNE: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 938val dfn'BLEZ: (BitsN.nbit * BitsN.nbit) -> unit 939val dfn'BGTZ: (BitsN.nbit * BitsN.nbit) -> unit 940val dfn'BLTZ: (BitsN.nbit * BitsN.nbit) -> unit 941val dfn'BGEZ: (BitsN.nbit * BitsN.nbit) -> unit 942val dfn'BLTZAL: (BitsN.nbit * BitsN.nbit) -> unit 943val dfn'BGEZAL: (BitsN.nbit * BitsN.nbit) -> unit 944val dfn'BEQL: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 945val dfn'BNEL: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 946val dfn'BLEZL: (BitsN.nbit * BitsN.nbit) -> unit 947val dfn'BGTZL: (BitsN.nbit * BitsN.nbit) -> unit 948val dfn'BLTZL: (BitsN.nbit * BitsN.nbit) -> unit 949val dfn'BGEZL: (BitsN.nbit * BitsN.nbit) -> unit 950val dfn'BLTZALL: (BitsN.nbit * BitsN.nbit) -> unit 951val dfn'BGEZALL: (BitsN.nbit * BitsN.nbit) -> unit 952val dfn'WAIT: unit 953val dfn'TLBP: unit -> unit 954val dfn'TLBR: unit -> unit 955val dfn'TLBWI: unit -> unit 956val dfn'TLBWR: unit -> unit 957val dfn'CACHE: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit 958val dfn'RDHWR: (BitsN.nbit * BitsN.nbit) -> unit 959val dfn'ReservedInstruction: unit -> unit 960val dfn'Unpredictable: unit -> unit 961val Run: instruction -> unit 962val COP1Decode: BitsN.nbit -> instruction 963val LDC1Decode: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> instruction 964val LWC1Decode: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> instruction 965val SDC1Decode: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> instruction 966val SWC1Decode: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> instruction 967val MOVCIDecode: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> instruction 968val COP3Decode: BitsN.nbit -> instruction 969val Decode: BitsN.nbit -> instruction 970val Next: unit -> unit 971val cpr: BitsN.nbit -> string 972val reg_name: BitsN.nbit -> string 973val op1i: Nat.nat -> (string * BitsN.nbit) -> string 974val op1ai: Nat.nat -> (string * BitsN.nbit) -> string 975val op1lai: Nat.nat -> (string * BitsN.nbit) -> string 976val op1r: (string * BitsN.nbit) -> string 977val op1ri: Nat.nat -> (string * (BitsN.nbit * BitsN.nbit)) -> string 978val op1rai: Nat.nat -> (string * (BitsN.nbit * BitsN.nbit)) -> string 979val op1rlai: Nat.nat -> (string * (BitsN.nbit * BitsN.nbit)) -> string 980val op2r: (string * (BitsN.nbit * BitsN.nbit)) -> string 981val op2ri: Nat.nat -> 982 (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string 983val op2rai: Nat.nat -> 984 (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string 985val op2rlai: Nat.nat -> 986 (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string 987val op3r: (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string 988val op2roi: Nat.nat -> 989 (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string 990val opmem: Nat.nat -> 991 (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string 992val op1fpr: (string * BitsN.nbit) -> string 993val op1fpri: Nat.nat -> (string * (BitsN.nbit * BitsN.nbit)) -> string 994val op2fpr: (string * (BitsN.nbit * BitsN.nbit)) -> string 995val op2rfpr: (string * (BitsN.nbit * BitsN.nbit)) -> string 996val op2rcfpr: (string * (BitsN.nbit * BitsN.nbit)) -> string 997val op2ccfpr: 998 (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string 999val op3fpr: (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string 1000val op4fpr: 1001 (string * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 1002 string 1003val opfpmem: Nat.nat -> 1004 (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string 1005val opfpmem2: 1006 (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string 1007val COP1Encode: COP1 -> BitsN.nbit 1008val form1: 1009 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 1010 BitsN.nbit 1011val form2: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> BitsN.nbit 1012val form3: 1013 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> BitsN.nbit 1014val form4: 1015 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> BitsN.nbit 1016val form5: 1017 (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> BitsN.nbit 1018val form6: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> BitsN.nbit 1019val Encode: instruction -> BitsN.nbit 1020val COP1InstructionToString: COP1 -> string 1021val instructionToString: instruction -> string 1022val skipSpaces: string -> string 1023val stripSpaces: string -> string 1024val p_number: string -> (Nat.nat option) 1025val p_tokens: string -> (string list) 1026val p_fp_cc: string -> (BitsN.nbit option) 1027val p_fp_reg: string -> (BitsN.nbit option) 1028val p_cfp_reg: string -> (BitsN.nbit option) 1029val p_reg: string -> (BitsN.nbit option) 1030val p_reg2: (string list) -> ((BitsN.nbit * BitsN.nbit) option) 1031val p_address: string -> ((BitsN.nbit * BitsN.nbit) option) 1032val p_index_address: string -> ((BitsN.nbit * BitsN.nbit) option) 1033val p_arg0: string -> maybe_instruction 1034val p_r1: (string * (string * BitsN.nbit)) -> maybe_instruction 1035val p_r2: 1036 (string * (string * (BitsN.nbit * BitsN.nbit))) -> maybe_instruction 1037val p_rcfpr: 1038 (string * (string * (BitsN.nbit * BitsN.nbit))) -> maybe_instruction 1039val p_rfpr2: 1040 (string * (string * (BitsN.nbit * BitsN.nbit))) -> maybe_instruction 1041val p_fpr2: 1042 (string * (string * (BitsN.nbit * BitsN.nbit))) -> maybe_instruction 1043val p_ccfpr2: 1044 (string * (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 1045 maybe_instruction 1046val p_r2cc: 1047 (string * (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 1048 maybe_instruction 1049val p_fpr2r: 1050 (string * (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 1051 maybe_instruction 1052val p_fpr2cc: 1053 (string * (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 1054 maybe_instruction 1055val p_r3: 1056 (string * (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 1057 maybe_instruction 1058val p_fpr3: 1059 (string * (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 1060 maybe_instruction 1061val p_fpr4: 1062 (string * 1063 (string * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) -> 1064 maybe_instruction 1065val imm_ok: Nat.nat -> 1066 ((bool option) * (Nat.nat * string)) -> (BitsN.nbit * string) 1067val p_1i: (string * (string * Nat.nat)) -> maybe_instruction 1068val p_cc1i: 1069 (string * (string * (BitsN.nbit * Nat.nat))) -> maybe_instruction 1070val p_r1i: 1071 (string * (string * (BitsN.nbit * Nat.nat))) -> maybe_instruction 1072val p_r2i: 1073 (string * (string * (BitsN.nbit * (BitsN.nbit * Nat.nat)))) -> 1074 maybe_instruction 1075val p_opmem: 1076 (string * (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 1077 maybe_instruction 1078val p_opfpmem: 1079 (string * (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 1080 maybe_instruction 1081val p_opfpmem2: 1082 (string * (string * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> 1083 maybe_instruction 1084val instructionFromString: string -> maybe_instruction 1085val encodeInstruction: string -> string 1086 1087end