extracted/status.mli

   1 open Preamble
   2
   3 open Types
   4
   5 open Hints_declaration
   6
   7 open Core_notation
   8
   9 open Pts
  10
  11 open Logic
  12
  13 open Jmeq
  14
  15 open Russell
  16
  17 open BitVectorTrie
  18
  19 open String
  20
  21 open Exp
  22
  23 open Arithmetic
  24
  25 open Vector
  26
  27 open FoldStuff
  28
  29 open BitVector
  30
  31 open Extranat
  32
  33 open Integers
  34
  35 open AST
  36
  37 open LabelledObjects
  38
  39 open Proper
  40
  41 open PositiveMap
  42
  43 open Deqsets
  44
  45 open ErrorMessages
  46
  47 open PreIdentifiers
  48
  49 open Errors
  50
  51 open Extralib
  52
  53 open Setoids
  54
  55 open Monad
  56
  57 open Option
  58
  59 open Div_and_mod
  60
  61 open Util
  62
  63 open List
  64
  65 open Lists
  66
  67 open Bool
  68
  69 open Relations
  70
  71 open Nat
  72
  73 open Positive
  74
  75 open Identifiers
  76
  77 open CostLabel
  78
  79 open ASM
  80
  81 type time = Nat.nat
  82
  83 type serialBufferType =
  84 | Eight of BitVector.byte
  85 | Nine of BitVector.bit * BitVector.byte
  86
  87 val serialBufferType_rect_Type4 :
  88   (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
  89   serialBufferType -> 'a1
  90
  91 val serialBufferType_rect_Type5 :
  92   (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
  93   serialBufferType -> 'a1
  94
  95 val serialBufferType_rect_Type3 :
  96   (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
  97   serialBufferType -> 'a1
  98
  99 val serialBufferType_rect_Type2 :
 100   (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
 101   serialBufferType -> 'a1
 102
 103 val serialBufferType_rect_Type1 :
 104   (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
 105   serialBufferType -> 'a1
 106
 107 val serialBufferType_rect_Type0 :
 108   (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
 109   serialBufferType -> 'a1
 110
 111 val serialBufferType_inv_rect_Type4 :
 112   serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
 113   BitVector.byte -> __ -> 'a1) -> 'a1
 114
 115 val serialBufferType_inv_rect_Type3 :
 116   serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
 117   BitVector.byte -> __ -> 'a1) -> 'a1
 118
 119 val serialBufferType_inv_rect_Type2 :
 120   serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
 121   BitVector.byte -> __ -> 'a1) -> 'a1
 122
 123 val serialBufferType_inv_rect_Type1 :
 124   serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
 125   BitVector.byte -> __ -> 'a1) -> 'a1
 126
 127 val serialBufferType_inv_rect_Type0 :
 128   serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
 129   BitVector.byte -> __ -> 'a1) -> 'a1
 130
 131 val serialBufferType_discr : serialBufferType -> serialBufferType -> __
 132
 133 val serialBufferType_jmdiscr : serialBufferType -> serialBufferType -> __
 134
 135 type lineType =
 136 | P1 of BitVector.byte
 137 | P3 of BitVector.byte
 138 | SerialBuffer of serialBufferType
 139
 140 val lineType_rect_Type4 :
 141   (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
 142   'a1) -> lineType -> 'a1
 143
 144 val lineType_rect_Type5 :
 145   (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
 146   'a1) -> lineType -> 'a1
 147
 148 val lineType_rect_Type3 :
 149   (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
 150   'a1) -> lineType -> 'a1
 151
 152 val lineType_rect_Type2 :
 153   (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
 154   'a1) -> lineType -> 'a1
 155
 156 val lineType_rect_Type1 :
 157   (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
 158   'a1) -> lineType -> 'a1
 159
 160 val lineType_rect_Type0 :
 161   (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
 162   'a1) -> lineType -> 'a1
 163
 164 val lineType_inv_rect_Type4 :
 165   lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1)
 166   -> (serialBufferType -> __ -> 'a1) -> 'a1
 167
 168 val lineType_inv_rect_Type3 :
 169   lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1)
 170   -> (serialBufferType -> __ -> 'a1) -> 'a1
 171
 172 val lineType_inv_rect_Type2 :
 173   lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1)
 174   -> (serialBufferType -> __ -> 'a1) -> 'a1
 175
 176 val lineType_inv_rect_Type1 :
 177   lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1)
 178   -> (serialBufferType -> __ -> 'a1) -> 'a1
 179
 180 val lineType_inv_rect_Type0 :
 181   lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1)
 182   -> (serialBufferType -> __ -> 'a1) -> 'a1
 183
 184 val lineType_discr : lineType -> lineType -> __
 185
 186 val lineType_jmdiscr : lineType -> lineType -> __
 187
 188 type sFR8051 =
 189 | SFR_SP
 190 | SFR_DPL
 191 | SFR_DPH
 192 | SFR_PCON
 193 | SFR_TCON
 194 | SFR_TMOD
 195 | SFR_TL0
 196 | SFR_TL1
 197 | SFR_TH0
 198 | SFR_TH1
 199 | SFR_P1
 200 | SFR_SCON
 201 | SFR_SBUF
 202 | SFR_IE
 203 | SFR_P3
 204 | SFR_IP
 205 | SFR_PSW
 206 | SFR_ACC_A
 207 | SFR_ACC_B
 208
 209 val sFR8051_rect_Type4 :
 210   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 211   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1
 212
 213 val sFR8051_rect_Type5 :
 214   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 215   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1
 216
 217 val sFR8051_rect_Type3 :
 218   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 219   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1
 220
 221 val sFR8051_rect_Type2 :
 222   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 223   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1
 224
 225 val sFR8051_rect_Type1 :
 226   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 227   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1
 228
 229 val sFR8051_rect_Type0 :
 230   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 231   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1
 232
 233 val sFR8051_inv_rect_Type4 :
 234   sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 235   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 236   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 237   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 238
 239 val sFR8051_inv_rect_Type3 :
 240   sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 241   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 242   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 243   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 244
 245 val sFR8051_inv_rect_Type2 :
 246   sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 247   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 248   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 249   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 250
 251 val sFR8051_inv_rect_Type1 :
 252   sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 253   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 254   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 255   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 256
 257 val sFR8051_inv_rect_Type0 :
 258   sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 259   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 260   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 261   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 262
 263 val sFR8051_discr : sFR8051 -> sFR8051 -> __
 264
 265 val sFR8051_jmdiscr : sFR8051 -> sFR8051 -> __
 266
 267 val sfr_8051_index : sFR8051 -> Nat.nat
 268
 269 type sFR8052 =
 270 | SFR_T2CON
 271 | SFR_RCAP2L
 272 | SFR_RCAP2H
 273 | SFR_TL2
 274 | SFR_TH2
 275
 276 val sFR8052_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1
 277
 278 val sFR8052_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1
 279
 280 val sFR8052_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1
 281
 282 val sFR8052_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1
 283
 284 val sFR8052_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1
 285
 286 val sFR8052_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1
 287
 288 val sFR8052_inv_rect_Type4 :
 289   sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 290   -> 'a1) -> 'a1
 291
 292 val sFR8052_inv_rect_Type3 :
 293   sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 294   -> 'a1) -> 'a1
 295
 296 val sFR8052_inv_rect_Type2 :
 297   sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 298   -> 'a1) -> 'a1
 299
 300 val sFR8052_inv_rect_Type1 :
 301   sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 302   -> 'a1) -> 'a1
 303
 304 val sFR8052_inv_rect_Type0 :
 305   sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 306   -> 'a1) -> 'a1
 307
 308 val sFR8052_discr : sFR8052 -> sFR8052 -> __
 309
 310 val sFR8052_jmdiscr : sFR8052 -> sFR8052 -> __
 311
 312 val sfr_8052_index : sFR8052 -> Nat.nat
 313
 314 type 'm preStatus = { low_internal_ram : BitVector.byte
 315                                          BitVectorTrie.bitVectorTrie;
 316                       high_internal_ram : BitVector.byte
 317                                           BitVectorTrie.bitVectorTrie;
 318                       external_ram : BitVector.byte
 319                                      BitVectorTrie.bitVectorTrie;
 320                       program_counter : BitVector.word;
 321                       special_function_registers_8051 : BitVector.byte
 322                                                         Vector.vector;
 323                       special_function_registers_8052 : BitVector.byte
 324                                                         Vector.vector;
 325                       p1_latch : BitVector.byte; p3_latch : BitVector.byte;
 326                       clock : time }
 327
 328 val preStatus_rect_Type4 :
 329   'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
 330   BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
 331   -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
 332   Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
 333   preStatus -> 'a2
 334
 335 val preStatus_rect_Type5 :
 336   'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
 337   BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
 338   -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
 339   Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
 340   preStatus -> 'a2
 341
 342 val preStatus_rect_Type3 :
 343   'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
 344   BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
 345   -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
 346   Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
 347   preStatus -> 'a2
 348
 349 val preStatus_rect_Type2 :
 350   'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
 351   BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
 352   -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
 353   Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
 354   preStatus -> 'a2
 355
 356 val preStatus_rect_Type1 :
 357   'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
 358   BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
 359   -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
 360   Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
 361   preStatus -> 'a2
 362
 363 val preStatus_rect_Type0 :
 364   'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
 365   BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
 366   -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
 367   Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
 368   preStatus -> 'a2
 369
 370 val low_internal_ram :
 371   'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie
 372
 373 val high_internal_ram :
 374   'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie
 375
 376 val external_ram :
 377   'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie
 378
 379 val program_counter : 'a1 -> 'a1 preStatus -> BitVector.word
 380
 381 val special_function_registers_8051 :
 382   'a1 -> 'a1 preStatus -> BitVector.byte Vector.vector
 383
 384 val special_function_registers_8052 :
 385   'a1 -> 'a1 preStatus -> BitVector.byte Vector.vector
 386
 387 val p1_latch : 'a1 -> 'a1 preStatus -> BitVector.byte
 388
 389 val p3_latch : 'a1 -> 'a1 preStatus -> BitVector.byte
 390
 391 val clock : 'a1 -> 'a1 preStatus -> time
 392
 393 val preStatus_inv_rect_Type4 :
 394   'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
 395   BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
 396   BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
 397   Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
 398   BitVector.byte -> time -> __ -> 'a2) -> 'a2
 399
 400 val preStatus_inv_rect_Type3 :
 401   'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
 402   BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
 403   BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
 404   Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
 405   BitVector.byte -> time -> __ -> 'a2) -> 'a2
 406
 407 val preStatus_inv_rect_Type2 :
 408   'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
 409   BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
 410   BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
 411   Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
 412   BitVector.byte -> time -> __ -> 'a2) -> 'a2
 413
 414 val preStatus_inv_rect_Type1 :
 415   'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
 416   BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
 417   BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
 418   Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
 419   BitVector.byte -> time -> __ -> 'a2) -> 'a2
 420
 421 val preStatus_inv_rect_Type0 :
 422   'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
 423   BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
 424   BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
 425   Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
 426   BitVector.byte -> time -> __ -> 'a2) -> 'a2
 427
 428 val preStatus_jmdiscr : 'a1 -> 'a1 preStatus -> 'a1 preStatus -> __
 429
 430 type status = BitVector.byte BitVectorTrie.bitVectorTrie preStatus
 431
 432 type pseudoStatus = ASM.pseudo_assembly_program preStatus
 433
 434 val set_clock : 'a1 -> 'a1 preStatus -> time -> 'a1 preStatus
 435
 436 val set_p1_latch : 'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus
 437
 438 val set_p3_latch : 'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus
 439
 440 val get_8051_sfr : 'a1 -> 'a1 preStatus -> sFR8051 -> BitVector.byte
 441
 442 val get_8052_sfr : 'a1 -> 'a1 preStatus -> sFR8052 -> BitVector.byte
 443
 444 val set_8051_sfr :
 445   'a1 -> 'a1 preStatus -> sFR8051 -> BitVector.byte -> 'a1 preStatus
 446
 447 val set_8052_sfr :
 448   'a1 -> 'a1 preStatus -> sFR8052 -> BitVector.byte -> 'a1 preStatus
 449
 450 val set_program_counter :
 451   'a1 -> 'a1 preStatus -> BitVector.word -> 'a1 preStatus
 452
 453 val set_code_memory : 'a1 -> 'a1 preStatus -> 'a2 -> 'a2 preStatus
 454
 455 val set_low_internal_ram :
 456   'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
 457   preStatus
 458
 459 val update_low_internal_ram :
 460   'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
 461   preStatus
 462
 463 val set_high_internal_ram :
 464   'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
 465   preStatus
 466
 467 val update_high_internal_ram :
 468   'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
 469   preStatus
 470
 471 val set_external_ram :
 472   'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
 473   preStatus
 474
 475 val update_external_ram :
 476   'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
 477   preStatus
 478
 479 val get_psw_flags : 'a1 -> 'a1 preStatus -> Nat.nat -> Bool.bool
 480
 481 val get_cy_flag : 'a1 -> 'a1 preStatus -> Bool.bool
 482
 483 val get_ac_flag : 'a1 -> 'a1 preStatus -> Bool.bool
 484
 485 val get_fo_flag : 'a1 -> 'a1 preStatus -> Bool.bool
 486
 487 val get_rs1_flag : 'a1 -> 'a1 preStatus -> Bool.bool
 488
 489 val get_rs0_flag : 'a1 -> 'a1 preStatus -> Bool.bool
 490
 491 val get_ov_flag : 'a1 -> 'a1 preStatus -> Bool.bool
 492
 493 val get_ud_flag : 'a1 -> 'a1 preStatus -> Bool.bool
 494
 495 val get_p_flag : 'a1 -> 'a1 preStatus -> Bool.bool
 496
 497 val set_flags :
 498   'a1 -> 'a1 preStatus -> BitVector.bit -> BitVector.bit Types.option ->
 499   BitVector.bit -> 'a1 preStatus
 500
 501 val initialise_status : 'a1 -> 'a1 preStatus
 502
 503 val sfr_of_Byte : BitVector.byte -> (sFR8051, sFR8052) Types.sum Types.option
 504
 505 val get_bit_addressable_sfr :
 506   'a1 -> 'a1 preStatus -> BitVector.byte -> Bool.bool -> BitVector.byte
 507
 508 val set_bit_addressable_sfr :
 509   'a1 -> 'a1 preStatus -> BitVector.byte -> BitVector.byte -> 'a1 preStatus
 510
 511 val bit_address_of_register :
 512   'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.bitVector
 513
 514 val get_register :
 515   'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte
 516
 517 val set_register :
 518   'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
 519   preStatus
 520
 521 val read_from_external_ram :
 522   'a1 -> 'a1 preStatus -> BitVector.word -> BitVector.byte
 523
 524 val read_from_internal_ram :
 525   'a1 -> 'a1 preStatus -> BitVector.byte -> BitVector.byte
 526
 527 val read_at_stack_pointer : 'a1 -> 'a1 preStatus -> BitVector.byte
 528
 529 val write_at_stack_pointer :
 530   'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus
 531
 532 val set_arg_16' :
 533   'a1 -> 'a1 preStatus -> BitVector.word -> ASM.subaddressing_mode -> 'a1
 534   preStatus Types.sig0
 535
 536 val set_arg_16 :
 537   'a1 -> 'a1 preStatus -> BitVector.word -> ASM.subaddressing_mode -> 'a1
 538   preStatus
 539
 540 val get_arg_16 :
 541   'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> BitVector.word
 542
 543 val get_arg_8 :
 544   'a1 -> 'a1 preStatus -> Bool.bool -> ASM.subaddressing_mode ->
 545   BitVector.byte
 546
 547 val set_arg_8 :
 548   'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> BitVector.byte -> 'a1
 549   preStatus
 550
 551 val get_arg_1 :
 552   'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> Bool.bool -> Bool.bool
 553
 554 val set_arg_1 :
 555   'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> BitVector.bit -> 'a1
 556   preStatus
 557
 558 val construct_datalabels :
 559   (ASM.identifier, BitVector.word) Types.prod List.list -> BitVector.word
 560   Identifiers.identifier_map
 561