(* m0 - generated by L3 - Mon Sep 18 10:36:51 2017 *)

signature m0 =
sig

structure Map : Map

(* -------------------------------------------------------------------------
   Types
   ------------------------------------------------------------------------- *)

type PRIMASK = { PM: bool, primask'rst: BitsN.nbit }

type PSR =
  { C: bool, ExceptionNumber: BitsN.nbit, N: bool, T: bool, V: bool,
    Z: bool, psr'rst: BitsN.nbit }

type CONTROL = { SPSEL: bool, control'rst: bool, nPRIV: bool }

type AIRCR =
  { ENDIANNESS: bool, SYSRESETREQ: bool, VECTCLRACTIVE: bool,
    VECTKEY: BitsN.nbit, aircr'rst: BitsN.nbit }

type CCR = { STKALIGN: bool, UNALIGN_TRP: bool, ccr'rst: BitsN.nbit }

type SHPR2 = { PRI_11: BitsN.nbit, shpr2'rst: BitsN.nbit }

type SHPR3 =
  { PRI_14: BitsN.nbit, PRI_15: BitsN.nbit, shpr3'rst: BitsN.nbit }

type IPR =
  { PRI_N0: BitsN.nbit, PRI_N1: BitsN.nbit, PRI_N2: BitsN.nbit,
    PRI_N3: BitsN.nbit, ipr'rst: BitsN.nbit }

datatype Mode = Mode_Thread | Mode_Handler

datatype ARM_Exception
  = ExternalInterrupt of BitsN.nbit
  | HardFault
  | NMI
  | PendSV
  | Reset
  | SVCall
  | SysTick

datatype RName
  = RName_0 | RName_1 | RName_2 | RName_3 | RName_4 | RName_5 | RName_6
  | RName_7 | RName_8 | RName_9 | RName_10 | RName_11 | RName_12
  | RName_SP_main | RName_SP_process | RName_LR | RName_PC

datatype SRType
  = SRType_LSL | SRType_LSR | SRType_ASR | SRType_ROR | SRType_RRX

datatype offset
  = immediate_form of BitsN.nbit | register_form of BitsN.nbit

datatype Hint
  = Breakpoint of BitsN.nbit
  | DataMemoryBarrier of BitsN.nbit
  | DataSynchronizationBarrier of BitsN.nbit
  | InstructionSynchronizationBarrier of BitsN.nbit
  | SendEvent of unit
  | WaitForEvent of unit
  | WaitForInterrupt of unit
  | Yield of unit

datatype System
  = ChangeProcessorState of bool
  | MoveToRegisterFromSpecial of BitsN.nbit * BitsN.nbit
  | MoveToSpecialRegister of BitsN.nbit * BitsN.nbit
  | SupervisorCall of BitsN.nbit

datatype Store
  = Push of BitsN.nbit
  | StoreByte of BitsN.nbit * (BitsN.nbit * offset)
  | StoreHalf of BitsN.nbit * (BitsN.nbit * offset)
  | StoreMultiple of BitsN.nbit * BitsN.nbit
  | StoreWord of BitsN.nbit * (BitsN.nbit * offset)

datatype Load
  = LoadByte of bool * (BitsN.nbit * (BitsN.nbit * offset))
  | LoadHalf of bool * (BitsN.nbit * (BitsN.nbit * offset))
  | LoadLiteral of BitsN.nbit * BitsN.nbit
  | LoadMultiple of bool * (BitsN.nbit * BitsN.nbit)
  | LoadWord of BitsN.nbit * (BitsN.nbit * offset)

datatype Media
  = ByteReverse of BitsN.nbit * BitsN.nbit
  | ByteReversePackedHalfword of BitsN.nbit * BitsN.nbit
  | ByteReverseSignedHalfword of BitsN.nbit * BitsN.nbit
  | ExtendByte of bool * (BitsN.nbit * BitsN.nbit)
  | ExtendHalfword of bool * (BitsN.nbit * BitsN.nbit)

datatype Multiply = Multiply32 of BitsN.nbit * (BitsN.nbit * BitsN.nbit)

datatype Data
  = ArithLogicImmediate of
      BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
  | CompareImmediate of BitsN.nbit * BitsN.nbit
  | Move of BitsN.nbit * BitsN.nbit
  | Register of
      BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
  | ShiftImmediate of
      bool * (bool * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat))))
  | ShiftRegister of BitsN.nbit * (BitsN.nbit * (SRType * BitsN.nbit))
  | TestCompareRegister of BitsN.nbit * (BitsN.nbit * BitsN.nbit)

datatype Branch
  = BranchExchange of BitsN.nbit
  | BranchLinkExchangeRegister of BitsN.nbit
  | BranchLinkImmediate of BitsN.nbit
  | BranchTarget of BitsN.nbit

datatype instruction
  = Branch of Branch
  | Data of Data
  | Hint of Hint
  | Load of Load
  | Media of Media
  | Multiply of Multiply
  | NoOperation of unit
  | Store of Store
  | System of System
  | Undefined of BitsN.nbit

datatype MachineCode
  = Thumb of BitsN.nbit | Thumb2 of BitsN.nbit * BitsN.nbit

datatype enc = Enc_Thumb | Enc_Narrow | Enc_Wide

datatype maybeMachineCode
  = BadCode of string
  | Thumb16 of BitsN.nbit
  | Thumb32 of BitsN.nbit * BitsN.nbit

datatype maybe_instruction
  = FAIL of string
  | HALFWORD of BitsN.nbit
  | OK of (BitsN.nbit * string) * instruction
  | PENDING of string * ((BitsN.nbit * string) * instruction)

datatype nat_or_reg = NAT of Nat.nat | REGISTER of BitsN.nbit

(* -------------------------------------------------------------------------
   Exceptions
   ------------------------------------------------------------------------- *)

exception ASSERT of string

exception UNPREDICTABLE of string

(* -------------------------------------------------------------------------
   Functions
   ------------------------------------------------------------------------- *)

structure Cast:
sig

val natToMode: Nat.nat -> Mode
val ModeToNat: Mode -> Nat.nat
val stringToMode: string -> Mode
val ModeToString: Mode -> string
val natToRName: Nat.nat -> RName
val RNameToNat: RName -> Nat.nat
val stringToRName: string -> RName
val RNameToString: RName -> string
val natToSRType: Nat.nat -> SRType
val SRTypeToNat: SRType -> Nat.nat
val stringToSRType: string -> SRType
val SRTypeToString: SRType -> string
val natToenc: Nat.nat -> enc
val encToNat: enc -> Nat.nat
val stringToenc: string -> enc
val encToString: enc -> string

end

val AIRCR: AIRCR ref
val CCR: CCR ref
val CONTROL: CONTROL ref
val CurrentMode: Mode ref
val ExceptionActive: (bool Map.map) ref
val MEM: (BitsN.nbit Map.map) ref
val NVIC_IPR: (IPR Map.map) ref
val PRIMASK: PRIMASK ref
val PSR: PSR ref
val REG: (BitsN.nbit Map.map) ref
val SHPR2: SHPR2 ref
val SHPR3: SHPR3 ref
val VTOR: BitsN.nbit ref
val count: Nat.nat ref
val pcinc: BitsN.nbit ref
val pending: (ARM_Exception option) ref
val PRIMASK_PM_rupd: PRIMASK * bool -> PRIMASK
val PRIMASK_primask'rst_rupd: PRIMASK * BitsN.nbit -> PRIMASK
val PSR_C_rupd: PSR * bool -> PSR
val PSR_ExceptionNumber_rupd: PSR * BitsN.nbit -> PSR
val PSR_N_rupd: PSR * bool -> PSR
val PSR_T_rupd: PSR * bool -> PSR
val PSR_V_rupd: PSR * bool -> PSR
val PSR_Z_rupd: PSR * bool -> PSR
val PSR_psr'rst_rupd: PSR * BitsN.nbit -> PSR
val CONTROL_SPSEL_rupd: CONTROL * bool -> CONTROL
val CONTROL_control'rst_rupd: CONTROL * bool -> CONTROL
val CONTROL_nPRIV_rupd: CONTROL * bool -> CONTROL
val AIRCR_ENDIANNESS_rupd: AIRCR * bool -> AIRCR
val AIRCR_SYSRESETREQ_rupd: AIRCR * bool -> AIRCR
val AIRCR_VECTCLRACTIVE_rupd: AIRCR * bool -> AIRCR
val AIRCR_VECTKEY_rupd: AIRCR * BitsN.nbit -> AIRCR
val AIRCR_aircr'rst_rupd: AIRCR * BitsN.nbit -> AIRCR
val CCR_STKALIGN_rupd: CCR * bool -> CCR
val CCR_UNALIGN_TRP_rupd: CCR * bool -> CCR
val CCR_ccr'rst_rupd: CCR * BitsN.nbit -> CCR
val SHPR2_PRI_11_rupd: SHPR2 * BitsN.nbit -> SHPR2
val SHPR2_shpr2'rst_rupd: SHPR2 * BitsN.nbit -> SHPR2
val SHPR3_PRI_14_rupd: SHPR3 * BitsN.nbit -> SHPR3
val SHPR3_PRI_15_rupd: SHPR3 * BitsN.nbit -> SHPR3
val SHPR3_shpr3'rst_rupd: SHPR3 * BitsN.nbit -> SHPR3
val IPR_PRI_N0_rupd: IPR * BitsN.nbit -> IPR
val IPR_PRI_N1_rupd: IPR * BitsN.nbit -> IPR
val IPR_PRI_N2_rupd: IPR * BitsN.nbit -> IPR
val IPR_PRI_N3_rupd: IPR * BitsN.nbit -> IPR
val IPR_ipr'rst_rupd: IPR * BitsN.nbit -> IPR
val boolify'16:
  BitsN.nbit ->
  bool *
  (bool *
   (bool *
    (bool *
     (bool *
      (bool *
       (bool *
        (bool *
         (bool *
          (bool * (bool * (bool * (bool * (bool * (bool * bool))))))))))))))
val boolify'4: BitsN.nbit -> bool * (bool * (bool * bool))
val rec'PRIMASK: BitsN.nbit -> PRIMASK
val reg'PRIMASK: PRIMASK -> BitsN.nbit
val write'rec'PRIMASK: (BitsN.nbit * PRIMASK) -> BitsN.nbit
val write'reg'PRIMASK: (PRIMASK * BitsN.nbit) -> PRIMASK
val rec'PSR: BitsN.nbit -> PSR
val reg'PSR: PSR -> BitsN.nbit
val write'rec'PSR: (BitsN.nbit * PSR) -> BitsN.nbit
val write'reg'PSR: (PSR * BitsN.nbit) -> PSR
val rec'CONTROL: BitsN.nbit -> CONTROL
val reg'CONTROL: CONTROL -> BitsN.nbit
val write'rec'CONTROL: (BitsN.nbit * CONTROL) -> BitsN.nbit
val write'reg'CONTROL: (CONTROL * BitsN.nbit) -> CONTROL
val rec'AIRCR: BitsN.nbit -> AIRCR
val reg'AIRCR: AIRCR -> BitsN.nbit
val write'rec'AIRCR: (BitsN.nbit * AIRCR) -> BitsN.nbit
val write'reg'AIRCR: (AIRCR * BitsN.nbit) -> AIRCR
val rec'CCR: BitsN.nbit -> CCR
val reg'CCR: CCR -> BitsN.nbit
val write'rec'CCR: (BitsN.nbit * CCR) -> BitsN.nbit
val write'reg'CCR: (CCR * BitsN.nbit) -> CCR
val rec'SHPR2: BitsN.nbit -> SHPR2
val reg'SHPR2: SHPR2 -> BitsN.nbit
val write'rec'SHPR2: (BitsN.nbit * SHPR2) -> BitsN.nbit
val write'reg'SHPR2: (SHPR2 * BitsN.nbit) -> SHPR2
val rec'SHPR3: BitsN.nbit -> SHPR3
val reg'SHPR3: SHPR3 -> BitsN.nbit
val write'rec'SHPR3: (BitsN.nbit * SHPR3) -> BitsN.nbit
val write'reg'SHPR3: (SHPR3 * BitsN.nbit) -> SHPR3
val rec'IPR: BitsN.nbit -> IPR
val reg'IPR: IPR -> BitsN.nbit
val write'rec'IPR: (BitsN.nbit * IPR) -> BitsN.nbit
val write'reg'IPR: (IPR * BitsN.nbit) -> IPR
val ProcessorID: unit -> IntInf.int
val ConditionPassed: BitsN.nbit -> bool
val Raise: ARM_Exception -> unit
val CurrentModeIsPrivileged: unit -> bool
val LookUpSP: unit -> RName
val R: BitsN.nbit -> BitsN.nbit
val write'R: (BitsN.nbit * BitsN.nbit) -> unit
val SP_main: unit -> BitsN.nbit
val write'SP_main: BitsN.nbit -> unit
val SP_process: unit -> BitsN.nbit
val write'SP_process: BitsN.nbit -> unit
val SP: unit -> BitsN.nbit
val write'SP: BitsN.nbit -> unit
val LR: unit -> BitsN.nbit
val write'LR: BitsN.nbit -> unit
val PC: unit -> BitsN.nbit
val write'PC: BitsN.nbit -> unit
val mem1: BitsN.nbit -> (bool list)
val mem: (BitsN.nbit * Nat.nat) -> (bool list)
val write'mem: ((bool list) * (BitsN.nbit * Nat.nat)) -> unit
val BigEndianReverse: ((bool list) * Nat.nat) -> (bool list)
val Align: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
val Aligned: Nat.nat -> (BitsN.nbit * Nat.nat) -> bool
val MemA: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
val write'MemA: Nat.nat -> (BitsN.nbit * (BitsN.nbit * Nat.nat)) -> unit
val MemU: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
val write'MemU: Nat.nat -> (BitsN.nbit * (BitsN.nbit * Nat.nat)) -> unit
val ExcNumber: ARM_Exception -> BitsN.nbit
val TakeReset: unit -> unit
val ExceptionPriority: Nat.nat -> IntInf.int
val ExecutionPriority: unit -> IntInf.int
val ReturnAddress: unit -> BitsN.nbit
val PushStack: unit -> unit
val ExceptionTaken: BitsN.nbit -> unit
val ExceptionEntry: unit -> unit
val PopStack: (BitsN.nbit * BitsN.nbit) -> unit
val DeActivate: BitsN.nbit -> unit
val IsOnes: Nat.nat -> BitsN.nbit -> bool
val ExceptionActiveBitCount: unit -> Nat.nat
val ExceptionReturn: BitsN.nbit -> unit
val CallSupervisor: unit -> unit
val BranchTo: BitsN.nbit -> unit
val BranchWritePC: BitsN.nbit -> unit
val BXWritePC: BitsN.nbit -> unit
val BLXWritePC: BitsN.nbit -> unit
val LoadWritePC: BitsN.nbit -> unit
val ALUWritePC: BitsN.nbit -> unit
val IncPC: unit -> unit
val HighestSetBit: Nat.nat -> BitsN.nbit -> IntInf.int
val CountLeadingZeroBits: Nat.nat -> BitsN.nbit -> Nat.nat
val LowestSetBit: Nat.nat -> BitsN.nbit -> Nat.nat
val BitCount: Nat.nat -> BitsN.nbit -> Nat.nat
val SignExtendFrom: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
val Extend: Nat.nat * Nat.nat -> (bool * BitsN.nbit) -> BitsN.nbit
val UInt: Nat.nat -> BitsN.nbit -> IntInf.int
val LSL_C: Nat.nat -> (BitsN.nbit * Nat.nat) -> (BitsN.nbit * bool)
val LSL: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
val LSR_C: Nat.nat -> (BitsN.nbit * Nat.nat) -> (BitsN.nbit * bool)
val LSR: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
val ASR_C: Nat.nat -> (BitsN.nbit * Nat.nat) -> (BitsN.nbit * bool)
val ASR: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
val ROR_C: Nat.nat -> (BitsN.nbit * Nat.nat) -> (BitsN.nbit * bool)
val ROR: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
val RRX_C: Nat.nat -> (BitsN.nbit * bool) -> (BitsN.nbit * bool)
val RRX: Nat.nat -> (BitsN.nbit * bool) -> BitsN.nbit
val DecodeImmShift: (BitsN.nbit * BitsN.nbit) -> (SRType * Nat.nat)
val DecodeRegShift: BitsN.nbit -> SRType
val Shift_C: Nat.nat ->
  (BitsN.nbit * (SRType * (Nat.nat * bool))) -> (BitsN.nbit * bool)
val Shift: Nat.nat ->
  (BitsN.nbit * (SRType * (Nat.nat * bool))) -> BitsN.nbit
val AddWithCarry: Nat.nat ->
  (BitsN.nbit * (BitsN.nbit * bool)) -> (BitsN.nbit * (bool * bool))
val DataProcessingALU:
  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * bool))) ->
  (BitsN.nbit * (bool * bool))
val ArithmeticOpcode: BitsN.nbit -> bool
val dfn'BranchTarget: BitsN.nbit -> unit
val dfn'BranchExchange: BitsN.nbit -> unit
val dfn'BranchLinkImmediate: BitsN.nbit -> unit
val dfn'BranchLinkExchangeRegister: BitsN.nbit -> unit
val DataProcessing:
  (BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * bool))))) ->
  unit
val DataProcessingPC:
  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * bool))) -> unit
val dfn'Move: (BitsN.nbit * BitsN.nbit) -> unit
val dfn'CompareImmediate: (BitsN.nbit * BitsN.nbit) -> unit
val dfn'ArithLogicImmediate:
  (BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
val doRegister:
  (BitsN.nbit *
   (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat)))))) ->
  unit
val dfn'Register:
  (BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
val dfn'TestCompareRegister:
  (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'ShiftImmediate:
  (bool * (bool * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat))))) ->
  unit
val dfn'ShiftRegister:
  (BitsN.nbit * (BitsN.nbit * (SRType * BitsN.nbit))) -> unit
val dfn'Multiply32: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'ExtendByte: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'ExtendHalfword: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'ByteReverse: (BitsN.nbit * BitsN.nbit) -> unit
val dfn'ByteReversePackedHalfword: (BitsN.nbit * BitsN.nbit) -> unit
val dfn'ByteReverseSignedHalfword: (BitsN.nbit * BitsN.nbit) -> unit
val dfn'LoadWord: (BitsN.nbit * (BitsN.nbit * offset)) -> unit
val dfn'LoadLiteral: (BitsN.nbit * BitsN.nbit) -> unit
val dfn'LoadByte: (bool * (BitsN.nbit * (BitsN.nbit * offset))) -> unit
val dfn'LoadHalf: (bool * (BitsN.nbit * (BitsN.nbit * offset))) -> unit
val dfn'LoadMultiple: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'StoreWord: (BitsN.nbit * (BitsN.nbit * offset)) -> unit
val dfn'StoreByte: (BitsN.nbit * (BitsN.nbit * offset)) -> unit
val dfn'StoreHalf: (BitsN.nbit * (BitsN.nbit * offset)) -> unit
val dfn'StoreMultiple: (BitsN.nbit * BitsN.nbit) -> unit
val dfn'Push: BitsN.nbit -> unit
val dfn'SupervisorCall: BitsN.nbit -> unit
val dfn'ChangeProcessorState: bool -> unit
val dfn'MoveToRegisterFromSpecial: (BitsN.nbit * BitsN.nbit) -> unit
val dfn'MoveToSpecialRegister: (BitsN.nbit * BitsN.nbit) -> unit
val dfn'Undefined: BitsN.nbit -> unit
val dfn'NoOperation: unit -> unit
val dfn'Breakpoint: BitsN.nbit -> unit
val dfn'DataMemoryBarrier: BitsN.nbit -> unit
val dfn'DataSynchronizationBarrier: BitsN.nbit -> unit
val dfn'InstructionSynchronizationBarrier: BitsN.nbit -> unit
val dfn'SendEvent: unit -> unit
val dfn'WaitForEvent: unit -> unit
val dfn'WaitForInterrupt: unit -> unit
val dfn'Yield: unit -> unit
val Run: instruction -> unit
val Fetch: unit -> MachineCode
val DECODE_UNPREDICTABLE: (MachineCode * string) -> unit
val DecodeThumb: BitsN.nbit -> instruction
val DecodeThumb2: (BitsN.nbit * BitsN.nbit) -> instruction
val Decode: MachineCode -> instruction
val Next: unit -> unit
val EncodeImmShift: (SRType * Nat.nat) -> (BitsN.nbit * BitsN.nbit)
val e_branch: (BitsN.nbit * (Branch * enc)) -> maybeMachineCode
val e_data: Data -> maybeMachineCode
val e_media: Media -> maybeMachineCode
val e_hint: (Hint * enc) -> maybeMachineCode
val e_system: System -> maybeMachineCode
val e_multiply: Multiply -> maybeMachineCode
val e_load: Load -> maybeMachineCode
val e_store: Store -> maybeMachineCode
val instructionEncode:
  (BitsN.nbit * (instruction * enc)) -> maybeMachineCode
val SetPassCondition: BitsN.nbit -> unit
val Encode: (BitsN.nbit * (instruction * enc)) -> maybeMachineCode
val al: BitsN.nbit * string
val stripSpaces: string -> string
val p_number: string -> (Nat.nat option)
val p_signed_number: (bool * string) -> ((bool * Nat.nat) option)
val p_encode_immediate: Nat.nat -> string -> ((bool * BitsN.nbit) option)
val p_encode_signed_immediate: Nat.nat ->
  (bool * string) -> ((bool * (bool * BitsN.nbit)) option)
val p_encode_signed_offset: Nat.nat ->
  (bool * string) -> ((bool * BitsN.nbit) option)
val p_unbounded_immediate: string -> (Nat.nat option)
val p_immediate: Nat.nat -> string -> ((bool * BitsN.nbit) option)
val p_immediate_number: Nat.nat -> string -> ((bool * BitsN.nbit) option)
val p_signed_immediate: Nat.nat ->
  string -> ((bool * (bool * BitsN.nbit)) option)
val p_signed_offset: Nat.nat -> string -> ((bool * BitsN.nbit) option)
val p_offset: Nat.nat -> string -> ((bool * BitsN.nbit) option)
val p_label: string -> (string option)
val p_cond: string -> (BitsN.nbit option)
val p_suffix: string -> ((BitsN.nbit * string) option)
val p_al_suffix: string -> ((BitsN.nbit * string) option)
val p_special_register: string -> (BitsN.nbit option)
val p_register: string -> (BitsN.nbit option)
val p_register1: (string list) -> (BitsN.nbit option)
val p_register2: (string list) -> ((BitsN.nbit * BitsN.nbit) option)
val p_register3:
  (string list) -> ((BitsN.nbit * (BitsN.nbit * BitsN.nbit)) option)
val p_shift_amount:
  (SRType * (char * string)) -> (string * (SRType * nat_or_reg))
val p_shift_imm_or_reg: string -> (string * (SRType * nat_or_reg))
val p_arith_logic_full:
  (string * (BitsN.nbit * (bool * (string list)))) -> maybe_instruction
val p_arith_logic:
  (string * (BitsN.nbit * (bool * (string list)))) -> maybe_instruction
val p_test_compare:
  (string * (BitsN.nbit * (string list))) -> maybe_instruction
val p_mov_mvn:
  (string * (bool * (bool * (string list)))) -> maybe_instruction
val p_shift_full: (string * (SRType * (string list))) -> maybe_instruction
val p_shift: (string * (SRType * (string list))) -> maybe_instruction
val p_adr: (string * (string list)) -> maybe_instruction
val p_bx: (string * (string list)) -> maybe_instruction
val p_bl: (string * (string list)) -> maybe_instruction
val p_b: (string * (string list)) -> maybe_instruction
val p_blx: (string * (string list)) -> maybe_instruction
val p_mul: (string * (string list)) -> maybe_instruction
val p_sxtb_etc:
  (string * (bool * (bool * (string list)))) -> maybe_instruction
val p_rev: (string * (string list)) -> maybe_instruction
val p_rev16: (string * (string list)) -> maybe_instruction
val p_revsh: (string * (string list)) -> maybe_instruction
val closingRegList: string -> (string option)
val p_reg_list: (BitsN.nbit * string) -> (BitsN.nbit option)
val p_registers_loop: (BitsN.nbit * (string list)) -> (BitsN.nbit option)
val p_registers: (string list) -> (BitsN.nbit option)
val closingAddress: (string list) -> (string option)
val p_address_mode:
  (string list) -> (string * ((BitsN.nbit * offset) option))
val pick_ldr_str:
  (Nat.nat * (BitsN.nbit * (BitsN.nbit * offset))) -> instruction
val p_ldr_str: (string * (Nat.nat * (string list))) -> maybe_instruction
val p_ldrb_ldrh:
  (string * (bool * (bool * (string list)))) -> maybe_instruction
val p_pop_push: (string * (bool * (string list))) -> maybe_instruction
val p_ldm_stm: (string * (bool * (string list))) -> maybe_instruction
val p_cps: (bool * (string list)) -> maybe_instruction
val p_mrs: (string * (string list)) -> maybe_instruction
val p_msr: (string * (string list)) -> maybe_instruction
val p_barrier_option: (string list) -> (BitsN.nbit option)
val p_dmb_dsb: (string * (bool * (string list))) -> maybe_instruction
val p_isb: (string * (string list)) -> maybe_instruction
val p_call: (string * (Nat.nat * (string list))) -> maybe_instruction
val p_noarg: (string * instruction) -> maybe_instruction
val p_tokens: string -> (string list)
val instructionFromString: string -> maybe_instruction
val halfString: BitsN.nbit -> string
val EncodeThumb: string -> (string * (string option))
val s_cond: BitsN.nbit -> string
val s_reg: BitsN.nbit -> string
val s_reg2: (BitsN.nbit * BitsN.nbit) -> string
val s_reg3: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> string
val s_reg4:
  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string
val s_hex: Nat.nat -> BitsN.nbit -> string
val s_offset: BitsN.nbit -> string
val s_maybe_offset: BitsN.nbit -> string
val s_special_reg: BitsN.nbit -> string
val s_barrier_option: BitsN.nbit -> string
val s_imm_form: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> string
val s_reg_form: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> string
val contiguous:
  (((Nat.nat * Nat.nat) list) * (Nat.nat * (bool list))) ->
  ((Nat.nat * Nat.nat) list)
val s_registers_from_contiguous:
  (string * ((Nat.nat * Nat.nat) list)) -> string
val s_registers: Nat.nat -> BitsN.nbit -> string
val s_test_compare: BitsN.nbit -> string
val s_arith_logic: BitsN.nbit -> string
val s_shift: SRType -> string
val s_shift_n: (SRType * Nat.nat) -> string
val s_shift_r: (bool * (BitsN.nbit * (SRType * Nat.nat))) -> string
val s_branch: (BitsN.nbit * Branch) -> (string * string)
val s_data: Data -> (string * string)
val s_load: Load -> (string * string)
val s_store: Store -> (string * string)
val s_hint: Hint -> (string * string)
val s_media: Media -> (string * string)
val s_system: System -> (string * string)
val instructionToString: (BitsN.nbit * instruction) -> (string * string)

end