open Preamble

open Types

open Hints_declaration

open Core_notation

open Pts

open Logic

open Jmeq

open Russell

open BitVectorTrie

open String

open Exp

open Arithmetic

open Vector

open FoldStuff

open BitVector

open Extranat

open Integers

open AST

open LabelledObjects

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Setoids

open Monad

open Option

open Div_and_mod

open Util

open List

open Lists

open Bool

open Relations

open Nat

open Positive

open Identifiers

open CostLabel

open ASM

type time = Nat.nat

type serialBufferType =
| Eight of BitVector.byte
| Nine of BitVector.bit * BitVector.byte

val serialBufferType_rect_Type4 :
  (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
  serialBufferType -> 'a1

val serialBufferType_rect_Type5 :
  (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
  serialBufferType -> 'a1

val serialBufferType_rect_Type3 :
  (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
  serialBufferType -> 'a1

val serialBufferType_rect_Type2 :
  (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
  serialBufferType -> 'a1

val serialBufferType_rect_Type1 :
  (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
  serialBufferType -> 'a1

val serialBufferType_rect_Type0 :
  (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
  serialBufferType -> 'a1

val serialBufferType_inv_rect_Type4 :
  serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
  BitVector.byte -> __ -> 'a1) -> 'a1

val serialBufferType_inv_rect_Type3 :
  serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
  BitVector.byte -> __ -> 'a1) -> 'a1

val serialBufferType_inv_rect_Type2 :
  serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
  BitVector.byte -> __ -> 'a1) -> 'a1

val serialBufferType_inv_rect_Type1 :
  serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
  BitVector.byte -> __ -> 'a1) -> 'a1

val serialBufferType_inv_rect_Type0 :
  serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
  BitVector.byte -> __ -> 'a1) -> 'a1

val serialBufferType_discr : serialBufferType -> serialBufferType -> __

val serialBufferType_jmdiscr : serialBufferType -> serialBufferType -> __

type lineType =
| P1 of BitVector.byte
| P3 of BitVector.byte
| SerialBuffer of serialBufferType

val lineType_rect_Type4 :
  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
  'a1) -> lineType -> 'a1

val lineType_rect_Type5 :
  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
  'a1) -> lineType -> 'a1

val lineType_rect_Type3 :
  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
  'a1) -> lineType -> 'a1

val lineType_rect_Type2 :
  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
  'a1) -> lineType -> 'a1

val lineType_rect_Type1 :
  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
  'a1) -> lineType -> 'a1

val lineType_rect_Type0 :
  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
  'a1) -> lineType -> 'a1

val lineType_inv_rect_Type4 :
  lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1)
  -> (serialBufferType -> __ -> 'a1) -> 'a1

val lineType_inv_rect_Type3 :
  lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1)
  -> (serialBufferType -> __ -> 'a1) -> 'a1

val lineType_inv_rect_Type2 :
  lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1)
  -> (serialBufferType -> __ -> 'a1) -> 'a1

val lineType_inv_rect_Type1 :
  lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1)
  -> (serialBufferType -> __ -> 'a1) -> 'a1

val lineType_inv_rect_Type0 :
  lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1)
  -> (serialBufferType -> __ -> 'a1) -> 'a1

val lineType_discr : lineType -> lineType -> __

val lineType_jmdiscr : lineType -> lineType -> __

type sFR8051 =
| SFR_SP
| SFR_DPL
| SFR_DPH
| SFR_PCON
| SFR_TCON
| SFR_TMOD
| SFR_TL0
| SFR_TL1
| SFR_TH0
| SFR_TH1
| SFR_P1
| SFR_SCON
| SFR_SBUF
| SFR_IE
| SFR_P3
| SFR_IP
| SFR_PSW
| SFR_ACC_A
| SFR_ACC_B

val sFR8051_rect_Type4 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1

val sFR8051_rect_Type5 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1

val sFR8051_rect_Type3 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1

val sFR8051_rect_Type2 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1

val sFR8051_rect_Type1 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1

val sFR8051_rect_Type0 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1

val sFR8051_inv_rect_Type4 :
  sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val sFR8051_inv_rect_Type3 :
  sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val sFR8051_inv_rect_Type2 :
  sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val sFR8051_inv_rect_Type1 :
  sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val sFR8051_inv_rect_Type0 :
  sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val sFR8051_discr : sFR8051 -> sFR8051 -> __

val sFR8051_jmdiscr : sFR8051 -> sFR8051 -> __

val sfr_8051_index : sFR8051 -> Nat.nat

type sFR8052 =
| SFR_T2CON
| SFR_RCAP2L
| SFR_RCAP2H
| SFR_TL2
| SFR_TH2

val sFR8052_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1

val sFR8052_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1

val sFR8052_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1

val sFR8052_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1

val sFR8052_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1

val sFR8052_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1

val sFR8052_inv_rect_Type4 :
  sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> 'a1

val sFR8052_inv_rect_Type3 :
  sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> 'a1

val sFR8052_inv_rect_Type2 :
  sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> 'a1

val sFR8052_inv_rect_Type1 :
  sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> 'a1

val sFR8052_inv_rect_Type0 :
  sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
  -> 'a1) -> 'a1

val sFR8052_discr : sFR8052 -> sFR8052 -> __

val sFR8052_jmdiscr : sFR8052 -> sFR8052 -> __

val sfr_8052_index : sFR8052 -> Nat.nat

type 'm preStatus = { low_internal_ram : BitVector.byte
                                         BitVectorTrie.bitVectorTrie;
                      high_internal_ram : BitVector.byte
                                          BitVectorTrie.bitVectorTrie;
                      external_ram : BitVector.byte
                                     BitVectorTrie.bitVectorTrie;
                      program_counter : BitVector.word;
                      special_function_registers_8051 : BitVector.byte
                                                        Vector.vector;
                      special_function_registers_8052 : BitVector.byte
                                                        Vector.vector;
                      p1_latch : BitVector.byte; p3_latch : BitVector.byte;
                      clock : time }

val preStatus_rect_Type4 :
  'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
  BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
  -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
  Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
  preStatus -> 'a2

val preStatus_rect_Type5 :
  'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
  BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
  -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
  Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
  preStatus -> 'a2

val preStatus_rect_Type3 :
  'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
  BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
  -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
  Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
  preStatus -> 'a2

val preStatus_rect_Type2 :
  'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
  BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
  -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
  Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
  preStatus -> 'a2

val preStatus_rect_Type1 :
  'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
  BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
  -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
  Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
  preStatus -> 'a2

val preStatus_rect_Type0 :
  'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
  BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
  -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
  Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
  preStatus -> 'a2

val low_internal_ram :
  'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie

val high_internal_ram :
  'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie

val external_ram :
  'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie

val program_counter : 'a1 -> 'a1 preStatus -> BitVector.word

val special_function_registers_8051 :
  'a1 -> 'a1 preStatus -> BitVector.byte Vector.vector

val special_function_registers_8052 :
  'a1 -> 'a1 preStatus -> BitVector.byte Vector.vector

val p1_latch : 'a1 -> 'a1 preStatus -> BitVector.byte

val p3_latch : 'a1 -> 'a1 preStatus -> BitVector.byte

val clock : 'a1 -> 'a1 preStatus -> time

val preStatus_inv_rect_Type4 :
  'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
  BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
  Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
  BitVector.byte -> time -> __ -> 'a2) -> 'a2

val preStatus_inv_rect_Type3 :
  'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
  BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
  Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
  BitVector.byte -> time -> __ -> 'a2) -> 'a2

val preStatus_inv_rect_Type2 :
  'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
  BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
  Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
  BitVector.byte -> time -> __ -> 'a2) -> 'a2

val preStatus_inv_rect_Type1 :
  'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
  BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
  Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
  BitVector.byte -> time -> __ -> 'a2) -> 'a2

val preStatus_inv_rect_Type0 :
  'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
  BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
  Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
  BitVector.byte -> time -> __ -> 'a2) -> 'a2

val preStatus_jmdiscr : 'a1 -> 'a1 preStatus -> 'a1 preStatus -> __

type status = BitVector.byte BitVectorTrie.bitVectorTrie preStatus

type pseudoStatus = ASM.pseudo_assembly_program preStatus

val set_clock : 'a1 -> 'a1 preStatus -> time -> 'a1 preStatus

val set_p1_latch : 'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus

val set_p3_latch : 'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus

val get_8051_sfr : 'a1 -> 'a1 preStatus -> sFR8051 -> BitVector.byte

val get_8052_sfr : 'a1 -> 'a1 preStatus -> sFR8052 -> BitVector.byte

val set_8051_sfr :
  'a1 -> 'a1 preStatus -> sFR8051 -> BitVector.byte -> 'a1 preStatus

val set_8052_sfr :
  'a1 -> 'a1 preStatus -> sFR8052 -> BitVector.byte -> 'a1 preStatus

val set_program_counter :
  'a1 -> 'a1 preStatus -> BitVector.word -> 'a1 preStatus

val set_code_memory : 'a1 -> 'a1 preStatus -> 'a2 -> 'a2 preStatus

val set_low_internal_ram :
  'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
  preStatus

val update_low_internal_ram :
  'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
  preStatus

val set_high_internal_ram :
  'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
  preStatus

val update_high_internal_ram :
  'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
  preStatus

val set_external_ram :
  'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
  preStatus

val update_external_ram :
  'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
  preStatus

val get_psw_flags : 'a1 -> 'a1 preStatus -> Nat.nat -> Bool.bool

val get_cy_flag : 'a1 -> 'a1 preStatus -> Bool.bool

val get_ac_flag : 'a1 -> 'a1 preStatus -> Bool.bool

val get_fo_flag : 'a1 -> 'a1 preStatus -> Bool.bool

val get_rs1_flag : 'a1 -> 'a1 preStatus -> Bool.bool

val get_rs0_flag : 'a1 -> 'a1 preStatus -> Bool.bool

val get_ov_flag : 'a1 -> 'a1 preStatus -> Bool.bool

val get_ud_flag : 'a1 -> 'a1 preStatus -> Bool.bool

val get_p_flag : 'a1 -> 'a1 preStatus -> Bool.bool

val set_flags :
  'a1 -> 'a1 preStatus -> BitVector.bit -> BitVector.bit Types.option ->
  BitVector.bit -> 'a1 preStatus

val initialise_status : 'a1 -> 'a1 preStatus

val sfr_of_Byte : BitVector.byte -> (sFR8051, sFR8052) Types.sum Types.option

val get_bit_addressable_sfr :
  'a1 -> 'a1 preStatus -> BitVector.byte -> Bool.bool -> BitVector.byte

val set_bit_addressable_sfr :
  'a1 -> 'a1 preStatus -> BitVector.byte -> BitVector.byte -> 'a1 preStatus

val bit_address_of_register :
  'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.bitVector

val get_register :
  'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte

val set_register :
  'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
  preStatus

val read_from_external_ram :
  'a1 -> 'a1 preStatus -> BitVector.word -> BitVector.byte

val read_from_internal_ram :
  'a1 -> 'a1 preStatus -> BitVector.byte -> BitVector.byte

val read_at_stack_pointer : 'a1 -> 'a1 preStatus -> BitVector.byte

val write_at_stack_pointer :
  'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus

val set_arg_16' :
  'a1 -> 'a1 preStatus -> BitVector.word -> ASM.subaddressing_mode -> 'a1
  preStatus Types.sig0

val set_arg_16 :
  'a1 -> 'a1 preStatus -> BitVector.word -> ASM.subaddressing_mode -> 'a1
  preStatus

val get_arg_16 :
  'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> BitVector.word

val get_arg_8 :
  'a1 -> 'a1 preStatus -> Bool.bool -> ASM.subaddressing_mode ->
  BitVector.byte

val set_arg_8 :
  'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> BitVector.byte -> 'a1
  preStatus

val get_arg_1 :
  'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> Bool.bool -> Bool.bool

val set_arg_1 :
  'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> BitVector.bit -> 'a1
  preStatus

val construct_datalabels :
  (ASM.identifier, BitVector.word) Types.prod List.list -> BitVector.word
  Identifiers.identifier_map