extracted/status.ml

   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 let rec serialBufferType_rect_Type4 h_Eight h_Nine = function
  91 | Eight x_21722 -> h_Eight x_21722
  92 | Nine (x_21724, x_21723) -> h_Nine x_21724 x_21723
  93
  94 (** val serialBufferType_rect_Type5 :
  95     (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
  96     serialBufferType -> 'a1 **)
  97 let rec serialBufferType_rect_Type5 h_Eight h_Nine = function
  98 | Eight x_21728 -> h_Eight x_21728
  99 | Nine (x_21730, x_21729) -> h_Nine x_21730 x_21729
 100
 101 (** val serialBufferType_rect_Type3 :
 102     (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
 103     serialBufferType -> 'a1 **)
 104 let rec serialBufferType_rect_Type3 h_Eight h_Nine = function
 105 | Eight x_21734 -> h_Eight x_21734
 106 | Nine (x_21736, x_21735) -> h_Nine x_21736 x_21735
 107
 108 (** val serialBufferType_rect_Type2 :
 109     (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
 110     serialBufferType -> 'a1 **)
 111 let rec serialBufferType_rect_Type2 h_Eight h_Nine = function
 112 | Eight x_21740 -> h_Eight x_21740
 113 | Nine (x_21742, x_21741) -> h_Nine x_21742 x_21741
 114
 115 (** val serialBufferType_rect_Type1 :
 116     (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
 117     serialBufferType -> 'a1 **)
 118 let rec serialBufferType_rect_Type1 h_Eight h_Nine = function
 119 | Eight x_21746 -> h_Eight x_21746
 120 | Nine (x_21748, x_21747) -> h_Nine x_21748 x_21747
 121
 122 (** val serialBufferType_rect_Type0 :
 123     (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
 124     serialBufferType -> 'a1 **)
 125 let rec serialBufferType_rect_Type0 h_Eight h_Nine = function
 126 | Eight x_21752 -> h_Eight x_21752
 127 | Nine (x_21754, x_21753) -> h_Nine x_21754 x_21753
 128
 129 (** val serialBufferType_inv_rect_Type4 :
 130     serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
 131     BitVector.byte -> __ -> 'a1) -> 'a1 **)
 132 let serialBufferType_inv_rect_Type4 hterm h1 h2 =
 133   let hcut = serialBufferType_rect_Type4 h1 h2 hterm in hcut __
 134
 135 (** val serialBufferType_inv_rect_Type3 :
 136     serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
 137     BitVector.byte -> __ -> 'a1) -> 'a1 **)
 138 let serialBufferType_inv_rect_Type3 hterm h1 h2 =
 139   let hcut = serialBufferType_rect_Type3 h1 h2 hterm in hcut __
 140
 141 (** val serialBufferType_inv_rect_Type2 :
 142     serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
 143     BitVector.byte -> __ -> 'a1) -> 'a1 **)
 144 let serialBufferType_inv_rect_Type2 hterm h1 h2 =
 145   let hcut = serialBufferType_rect_Type2 h1 h2 hterm in hcut __
 146
 147 (** val serialBufferType_inv_rect_Type1 :
 148     serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
 149     BitVector.byte -> __ -> 'a1) -> 'a1 **)
 150 let serialBufferType_inv_rect_Type1 hterm h1 h2 =
 151   let hcut = serialBufferType_rect_Type1 h1 h2 hterm in hcut __
 152
 153 (** val serialBufferType_inv_rect_Type0 :
 154     serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
 155     BitVector.byte -> __ -> 'a1) -> 'a1 **)
 156 let serialBufferType_inv_rect_Type0 hterm h1 h2 =
 157   let hcut = serialBufferType_rect_Type0 h1 h2 hterm in hcut __
 158
 159 (** val serialBufferType_discr :
 160     serialBufferType -> serialBufferType -> __ **)
 161 let serialBufferType_discr x y =
 162   Logic.eq_rect_Type2 x
 163     (match x with
 164      | Eight a0 -> Obj.magic (fun _ dH -> dH __)
 165      | Nine (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
 166
 167 (** val serialBufferType_jmdiscr :
 168     serialBufferType -> serialBufferType -> __ **)
 169 let serialBufferType_jmdiscr x y =
 170   Logic.eq_rect_Type2 x
 171     (match x with
 172      | Eight a0 -> Obj.magic (fun _ dH -> dH __)
 173      | Nine (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
 174
 175 type lineType =
 176 | P1 of BitVector.byte
 177 | P3 of BitVector.byte
 178 | SerialBuffer of serialBufferType
 179
 180 (** val lineType_rect_Type4 :
 181     (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
 182     -> 'a1) -> lineType -> 'a1 **)
 183 let rec lineType_rect_Type4 h_P1 h_P3 h_SerialBuffer = function
 184 | P1 x_21801 -> h_P1 x_21801
 185 | P3 x_21802 -> h_P3 x_21802
 186 | SerialBuffer x_21803 -> h_SerialBuffer x_21803
 187
 188 (** val lineType_rect_Type5 :
 189     (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
 190     -> 'a1) -> lineType -> 'a1 **)
 191 let rec lineType_rect_Type5 h_P1 h_P3 h_SerialBuffer = function
 192 | P1 x_21808 -> h_P1 x_21808
 193 | P3 x_21809 -> h_P3 x_21809
 194 | SerialBuffer x_21810 -> h_SerialBuffer x_21810
 195
 196 (** val lineType_rect_Type3 :
 197     (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
 198     -> 'a1) -> lineType -> 'a1 **)
 199 let rec lineType_rect_Type3 h_P1 h_P3 h_SerialBuffer = function
 200 | P1 x_21815 -> h_P1 x_21815
 201 | P3 x_21816 -> h_P3 x_21816
 202 | SerialBuffer x_21817 -> h_SerialBuffer x_21817
 203
 204 (** val lineType_rect_Type2 :
 205     (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
 206     -> 'a1) -> lineType -> 'a1 **)
 207 let rec lineType_rect_Type2 h_P1 h_P3 h_SerialBuffer = function
 208 | P1 x_21822 -> h_P1 x_21822
 209 | P3 x_21823 -> h_P3 x_21823
 210 | SerialBuffer x_21824 -> h_SerialBuffer x_21824
 211
 212 (** val lineType_rect_Type1 :
 213     (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
 214     -> 'a1) -> lineType -> 'a1 **)
 215 let rec lineType_rect_Type1 h_P1 h_P3 h_SerialBuffer = function
 216 | P1 x_21829 -> h_P1 x_21829
 217 | P3 x_21830 -> h_P3 x_21830
 218 | SerialBuffer x_21831 -> h_SerialBuffer x_21831
 219
 220 (** val lineType_rect_Type0 :
 221     (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
 222     -> 'a1) -> lineType -> 'a1 **)
 223 let rec lineType_rect_Type0 h_P1 h_P3 h_SerialBuffer = function
 224 | P1 x_21836 -> h_P1 x_21836
 225 | P3 x_21837 -> h_P3 x_21837
 226 | SerialBuffer x_21838 -> h_SerialBuffer x_21838
 227
 228 (** val lineType_inv_rect_Type4 :
 229     lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
 230     'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
 231 let lineType_inv_rect_Type4 hterm h1 h2 h3 =
 232   let hcut = lineType_rect_Type4 h1 h2 h3 hterm in hcut __
 233
 234 (** val lineType_inv_rect_Type3 :
 235     lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
 236     'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
 237 let lineType_inv_rect_Type3 hterm h1 h2 h3 =
 238   let hcut = lineType_rect_Type3 h1 h2 h3 hterm in hcut __
 239
 240 (** val lineType_inv_rect_Type2 :
 241     lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
 242     'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
 243 let lineType_inv_rect_Type2 hterm h1 h2 h3 =
 244   let hcut = lineType_rect_Type2 h1 h2 h3 hterm in hcut __
 245
 246 (** val lineType_inv_rect_Type1 :
 247     lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
 248     'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
 249 let lineType_inv_rect_Type1 hterm h1 h2 h3 =
 250   let hcut = lineType_rect_Type1 h1 h2 h3 hterm in hcut __
 251
 252 (** val lineType_inv_rect_Type0 :
 253     lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
 254     'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
 255 let lineType_inv_rect_Type0 hterm h1 h2 h3 =
 256   let hcut = lineType_rect_Type0 h1 h2 h3 hterm in hcut __
 257
 258 (** val lineType_discr : lineType -> lineType -> __ **)
 259 let lineType_discr x y =
 260   Logic.eq_rect_Type2 x
 261     (match x with
 262      | P1 a0 -> Obj.magic (fun _ dH -> dH __)
 263      | P3 a0 -> Obj.magic (fun _ dH -> dH __)
 264      | SerialBuffer a0 -> Obj.magic (fun _ dH -> dH __)) y
 265
 266 (** val lineType_jmdiscr : lineType -> lineType -> __ **)
 267 let lineType_jmdiscr x y =
 268   Logic.eq_rect_Type2 x
 269     (match x with
 270      | P1 a0 -> Obj.magic (fun _ dH -> dH __)
 271      | P3 a0 -> Obj.magic (fun _ dH -> dH __)
 272      | SerialBuffer a0 -> Obj.magic (fun _ dH -> dH __)) y
 273
 274 type sFR8051 =
 275 | SFR_SP
 276 | SFR_DPL
 277 | SFR_DPH
 278 | SFR_PCON
 279 | SFR_TCON
 280 | SFR_TMOD
 281 | SFR_TL0
 282 | SFR_TL1
 283 | SFR_TH0
 284 | SFR_TH1
 285 | SFR_P1
 286 | SFR_SCON
 287 | SFR_SBUF
 288 | SFR_IE
 289 | SFR_P3
 290 | SFR_IP
 291 | SFR_PSW
 292 | SFR_ACC_A
 293 | SFR_ACC_B
 294
 295 (** val sFR8051_rect_Type4 :
 296     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 297     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
 298 let rec sFR8051_rect_Type4 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
 299 | SFR_SP -> h_SFR_SP
 300 | SFR_DPL -> h_SFR_DPL
 301 | SFR_DPH -> h_SFR_DPH
 302 | SFR_PCON -> h_SFR_PCON
 303 | SFR_TCON -> h_SFR_TCON
 304 | SFR_TMOD -> h_SFR_TMOD
 305 | SFR_TL0 -> h_SFR_TL0
 306 | SFR_TL1 -> h_SFR_TL1
 307 | SFR_TH0 -> h_SFR_TH0
 308 | SFR_TH1 -> h_SFR_TH1
 309 | SFR_P1 -> h_SFR_P1
 310 | SFR_SCON -> h_SFR_SCON
 311 | SFR_SBUF -> h_SFR_SBUF
 312 | SFR_IE -> h_SFR_IE
 313 | SFR_P3 -> h_SFR_P3
 314 | SFR_IP -> h_SFR_IP
 315 | SFR_PSW -> h_SFR_PSW
 316 | SFR_ACC_A -> h_SFR_ACC_A
 317 | SFR_ACC_B -> h_SFR_ACC_B
 318
 319 (** val sFR8051_rect_Type5 :
 320     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 321     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
 322 let rec sFR8051_rect_Type5 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
 323 | SFR_SP -> h_SFR_SP
 324 | SFR_DPL -> h_SFR_DPL
 325 | SFR_DPH -> h_SFR_DPH
 326 | SFR_PCON -> h_SFR_PCON
 327 | SFR_TCON -> h_SFR_TCON
 328 | SFR_TMOD -> h_SFR_TMOD
 329 | SFR_TL0 -> h_SFR_TL0
 330 | SFR_TL1 -> h_SFR_TL1
 331 | SFR_TH0 -> h_SFR_TH0
 332 | SFR_TH1 -> h_SFR_TH1
 333 | SFR_P1 -> h_SFR_P1
 334 | SFR_SCON -> h_SFR_SCON
 335 | SFR_SBUF -> h_SFR_SBUF
 336 | SFR_IE -> h_SFR_IE
 337 | SFR_P3 -> h_SFR_P3
 338 | SFR_IP -> h_SFR_IP
 339 | SFR_PSW -> h_SFR_PSW
 340 | SFR_ACC_A -> h_SFR_ACC_A
 341 | SFR_ACC_B -> h_SFR_ACC_B
 342
 343 (** val sFR8051_rect_Type3 :
 344     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 345     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
 346 let rec sFR8051_rect_Type3 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
 347 | SFR_SP -> h_SFR_SP
 348 | SFR_DPL -> h_SFR_DPL
 349 | SFR_DPH -> h_SFR_DPH
 350 | SFR_PCON -> h_SFR_PCON
 351 | SFR_TCON -> h_SFR_TCON
 352 | SFR_TMOD -> h_SFR_TMOD
 353 | SFR_TL0 -> h_SFR_TL0
 354 | SFR_TL1 -> h_SFR_TL1
 355 | SFR_TH0 -> h_SFR_TH0
 356 | SFR_TH1 -> h_SFR_TH1
 357 | SFR_P1 -> h_SFR_P1
 358 | SFR_SCON -> h_SFR_SCON
 359 | SFR_SBUF -> h_SFR_SBUF
 360 | SFR_IE -> h_SFR_IE
 361 | SFR_P3 -> h_SFR_P3
 362 | SFR_IP -> h_SFR_IP
 363 | SFR_PSW -> h_SFR_PSW
 364 | SFR_ACC_A -> h_SFR_ACC_A
 365 | SFR_ACC_B -> h_SFR_ACC_B
 366
 367 (** val sFR8051_rect_Type2 :
 368     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 369     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
 370 let rec sFR8051_rect_Type2 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
 371 | SFR_SP -> h_SFR_SP
 372 | SFR_DPL -> h_SFR_DPL
 373 | SFR_DPH -> h_SFR_DPH
 374 | SFR_PCON -> h_SFR_PCON
 375 | SFR_TCON -> h_SFR_TCON
 376 | SFR_TMOD -> h_SFR_TMOD
 377 | SFR_TL0 -> h_SFR_TL0
 378 | SFR_TL1 -> h_SFR_TL1
 379 | SFR_TH0 -> h_SFR_TH0
 380 | SFR_TH1 -> h_SFR_TH1
 381 | SFR_P1 -> h_SFR_P1
 382 | SFR_SCON -> h_SFR_SCON
 383 | SFR_SBUF -> h_SFR_SBUF
 384 | SFR_IE -> h_SFR_IE
 385 | SFR_P3 -> h_SFR_P3
 386 | SFR_IP -> h_SFR_IP
 387 | SFR_PSW -> h_SFR_PSW
 388 | SFR_ACC_A -> h_SFR_ACC_A
 389 | SFR_ACC_B -> h_SFR_ACC_B
 390
 391 (** val sFR8051_rect_Type1 :
 392     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 393     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
 394 let rec sFR8051_rect_Type1 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
 395 | SFR_SP -> h_SFR_SP
 396 | SFR_DPL -> h_SFR_DPL
 397 | SFR_DPH -> h_SFR_DPH
 398 | SFR_PCON -> h_SFR_PCON
 399 | SFR_TCON -> h_SFR_TCON
 400 | SFR_TMOD -> h_SFR_TMOD
 401 | SFR_TL0 -> h_SFR_TL0
 402 | SFR_TL1 -> h_SFR_TL1
 403 | SFR_TH0 -> h_SFR_TH0
 404 | SFR_TH1 -> h_SFR_TH1
 405 | SFR_P1 -> h_SFR_P1
 406 | SFR_SCON -> h_SFR_SCON
 407 | SFR_SBUF -> h_SFR_SBUF
 408 | SFR_IE -> h_SFR_IE
 409 | SFR_P3 -> h_SFR_P3
 410 | SFR_IP -> h_SFR_IP
 411 | SFR_PSW -> h_SFR_PSW
 412 | SFR_ACC_A -> h_SFR_ACC_A
 413 | SFR_ACC_B -> h_SFR_ACC_B
 414
 415 (** val sFR8051_rect_Type0 :
 416     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 417     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
 418 let rec sFR8051_rect_Type0 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
 419 | SFR_SP -> h_SFR_SP
 420 | SFR_DPL -> h_SFR_DPL
 421 | SFR_DPH -> h_SFR_DPH
 422 | SFR_PCON -> h_SFR_PCON
 423 | SFR_TCON -> h_SFR_TCON
 424 | SFR_TMOD -> h_SFR_TMOD
 425 | SFR_TL0 -> h_SFR_TL0
 426 | SFR_TL1 -> h_SFR_TL1
 427 | SFR_TH0 -> h_SFR_TH0
 428 | SFR_TH1 -> h_SFR_TH1
 429 | SFR_P1 -> h_SFR_P1
 430 | SFR_SCON -> h_SFR_SCON
 431 | SFR_SBUF -> h_SFR_SBUF
 432 | SFR_IE -> h_SFR_IE
 433 | SFR_P3 -> h_SFR_P3
 434 | SFR_IP -> h_SFR_IP
 435 | SFR_PSW -> h_SFR_PSW
 436 | SFR_ACC_A -> h_SFR_ACC_A
 437 | SFR_ACC_B -> h_SFR_ACC_B
 438
 439 (** val sFR8051_inv_rect_Type4 :
 440     sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 441     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 442     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 443     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 444     -> 'a1) -> 'a1 **)
 445 let sFR8051_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
 446   let hcut =
 447     sFR8051_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
 448       h17 h18 h19 hterm
 449   in
 450   hcut __
 451
 452 (** val sFR8051_inv_rect_Type3 :
 453     sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 454     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 455     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 456     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 457     -> 'a1) -> 'a1 **)
 458 let sFR8051_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
 459   let hcut =
 460     sFR8051_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
 461       h17 h18 h19 hterm
 462   in
 463   hcut __
 464
 465 (** val sFR8051_inv_rect_Type2 :
 466     sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 467     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 468     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 469     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 470     -> 'a1) -> 'a1 **)
 471 let sFR8051_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
 472   let hcut =
 473     sFR8051_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
 474       h17 h18 h19 hterm
 475   in
 476   hcut __
 477
 478 (** val sFR8051_inv_rect_Type1 :
 479     sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 480     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 481     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 482     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 483     -> 'a1) -> 'a1 **)
 484 let sFR8051_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
 485   let hcut =
 486     sFR8051_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
 487       h17 h18 h19 hterm
 488   in
 489   hcut __
 490
 491 (** val sFR8051_inv_rect_Type0 :
 492     sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 493     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 494     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 495     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 496     -> 'a1) -> 'a1 **)
 497 let sFR8051_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
 498   let hcut =
 499     sFR8051_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
 500       h17 h18 h19 hterm
 501   in
 502   hcut __
 503
 504 (** val sFR8051_discr : sFR8051 -> sFR8051 -> __ **)
 505 let sFR8051_discr x y =
 506   Logic.eq_rect_Type2 x
 507     (match x with
 508      | SFR_SP -> Obj.magic (fun _ dH -> dH)
 509      | SFR_DPL -> Obj.magic (fun _ dH -> dH)
 510      | SFR_DPH -> Obj.magic (fun _ dH -> dH)
 511      | SFR_PCON -> Obj.magic (fun _ dH -> dH)
 512      | SFR_TCON -> Obj.magic (fun _ dH -> dH)
 513      | SFR_TMOD -> Obj.magic (fun _ dH -> dH)
 514      | SFR_TL0 -> Obj.magic (fun _ dH -> dH)
 515      | SFR_TL1 -> Obj.magic (fun _ dH -> dH)
 516      | SFR_TH0 -> Obj.magic (fun _ dH -> dH)
 517      | SFR_TH1 -> Obj.magic (fun _ dH -> dH)
 518      | SFR_P1 -> Obj.magic (fun _ dH -> dH)
 519      | SFR_SCON -> Obj.magic (fun _ dH -> dH)
 520      | SFR_SBUF -> Obj.magic (fun _ dH -> dH)
 521      | SFR_IE -> Obj.magic (fun _ dH -> dH)
 522      | SFR_P3 -> Obj.magic (fun _ dH -> dH)
 523      | SFR_IP -> Obj.magic (fun _ dH -> dH)
 524      | SFR_PSW -> Obj.magic (fun _ dH -> dH)
 525      | SFR_ACC_A -> Obj.magic (fun _ dH -> dH)
 526      | SFR_ACC_B -> Obj.magic (fun _ dH -> dH)) y
 527
 528 (** val sFR8051_jmdiscr : sFR8051 -> sFR8051 -> __ **)
 529 let sFR8051_jmdiscr x y =
 530   Logic.eq_rect_Type2 x
 531     (match x with
 532      | SFR_SP -> Obj.magic (fun _ dH -> dH)
 533      | SFR_DPL -> Obj.magic (fun _ dH -> dH)
 534      | SFR_DPH -> Obj.magic (fun _ dH -> dH)
 535      | SFR_PCON -> Obj.magic (fun _ dH -> dH)
 536      | SFR_TCON -> Obj.magic (fun _ dH -> dH)
 537      | SFR_TMOD -> Obj.magic (fun _ dH -> dH)
 538      | SFR_TL0 -> Obj.magic (fun _ dH -> dH)
 539      | SFR_TL1 -> Obj.magic (fun _ dH -> dH)
 540      | SFR_TH0 -> Obj.magic (fun _ dH -> dH)
 541      | SFR_TH1 -> Obj.magic (fun _ dH -> dH)
 542      | SFR_P1 -> Obj.magic (fun _ dH -> dH)
 543      | SFR_SCON -> Obj.magic (fun _ dH -> dH)
 544      | SFR_SBUF -> Obj.magic (fun _ dH -> dH)
 545      | SFR_IE -> Obj.magic (fun _ dH -> dH)
 546      | SFR_P3 -> Obj.magic (fun _ dH -> dH)
 547      | SFR_IP -> Obj.magic (fun _ dH -> dH)
 548      | SFR_PSW -> Obj.magic (fun _ dH -> dH)
 549      | SFR_ACC_A -> Obj.magic (fun _ dH -> dH)
 550      | SFR_ACC_B -> Obj.magic (fun _ dH -> dH)) y
 551
 552 (** val sfr_8051_index : sFR8051 -> Nat.nat **)
 553 let sfr_8051_index = function
 554 | SFR_SP -> Nat.O
 555 | SFR_DPL -> Nat.S Nat.O
 556 | SFR_DPH -> Nat.S (Nat.S Nat.O)
 557 | SFR_PCON -> Nat.S (Nat.S (Nat.S Nat.O))
 558 | SFR_TCON -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
 559 | SFR_TMOD -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
 560 | SFR_TL0 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
 561 | SFR_TL1 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
 562 | SFR_TH0 ->
 563   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))
 564 | SFR_TH1 ->
 565   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
 566 | SFR_P1 ->
 567   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 568     Nat.O)))))))))
 569 | SFR_SCON ->
 570   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 571     Nat.O))))))))))
 572 | SFR_SBUF ->
 573   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 574     (Nat.S Nat.O)))))))))))
 575 | SFR_IE ->
 576   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 577     (Nat.S (Nat.S Nat.O))))))))))))
 578 | SFR_P3 ->
 579   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 580     (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))
 581 | SFR_IP ->
 582   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 583     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))
 584 | SFR_PSW ->
 585   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 586     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))
 587 | SFR_ACC_A ->
 588   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 589     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))
 590 | SFR_ACC_B ->
 591   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 592     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))
 593
 594 type sFR8052 =
 595 | SFR_T2CON
 596 | SFR_RCAP2L
 597 | SFR_RCAP2H
 598 | SFR_TL2
 599 | SFR_TH2
 600
 601 (** val sFR8052_rect_Type4 :
 602     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
 603 let rec sFR8052_rect_Type4 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
 604 | SFR_T2CON -> h_SFR_T2CON
 605 | SFR_RCAP2L -> h_SFR_RCAP2L
 606 | SFR_RCAP2H -> h_SFR_RCAP2H
 607 | SFR_TL2 -> h_SFR_TL2
 608 | SFR_TH2 -> h_SFR_TH2
 609
 610 (** val sFR8052_rect_Type5 :
 611     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
 612 let rec sFR8052_rect_Type5 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
 613 | SFR_T2CON -> h_SFR_T2CON
 614 | SFR_RCAP2L -> h_SFR_RCAP2L
 615 | SFR_RCAP2H -> h_SFR_RCAP2H
 616 | SFR_TL2 -> h_SFR_TL2
 617 | SFR_TH2 -> h_SFR_TH2
 618
 619 (** val sFR8052_rect_Type3 :
 620     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
 621 let rec sFR8052_rect_Type3 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
 622 | SFR_T2CON -> h_SFR_T2CON
 623 | SFR_RCAP2L -> h_SFR_RCAP2L
 624 | SFR_RCAP2H -> h_SFR_RCAP2H
 625 | SFR_TL2 -> h_SFR_TL2
 626 | SFR_TH2 -> h_SFR_TH2
 627
 628 (** val sFR8052_rect_Type2 :
 629     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
 630 let rec sFR8052_rect_Type2 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
 631 | SFR_T2CON -> h_SFR_T2CON
 632 | SFR_RCAP2L -> h_SFR_RCAP2L
 633 | SFR_RCAP2H -> h_SFR_RCAP2H
 634 | SFR_TL2 -> h_SFR_TL2
 635 | SFR_TH2 -> h_SFR_TH2
 636
 637 (** val sFR8052_rect_Type1 :
 638     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
 639 let rec sFR8052_rect_Type1 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
 640 | SFR_T2CON -> h_SFR_T2CON
 641 | SFR_RCAP2L -> h_SFR_RCAP2L
 642 | SFR_RCAP2H -> h_SFR_RCAP2H
 643 | SFR_TL2 -> h_SFR_TL2
 644 | SFR_TH2 -> h_SFR_TH2
 645
 646 (** val sFR8052_rect_Type0 :
 647     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
 648 let rec sFR8052_rect_Type0 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
 649 | SFR_T2CON -> h_SFR_T2CON
 650 | SFR_RCAP2L -> h_SFR_RCAP2L
 651 | SFR_RCAP2H -> h_SFR_RCAP2H
 652 | SFR_TL2 -> h_SFR_TL2
 653 | SFR_TH2 -> h_SFR_TH2
 654
 655 (** val sFR8052_inv_rect_Type4 :
 656     sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 657     (__ -> 'a1) -> 'a1 **)
 658 let sFR8052_inv_rect_Type4 hterm h1 h2 h3 h4 h5 =
 659   let hcut = sFR8052_rect_Type4 h1 h2 h3 h4 h5 hterm in hcut __
 660
 661 (** val sFR8052_inv_rect_Type3 :
 662     sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 663     (__ -> 'a1) -> 'a1 **)
 664 let sFR8052_inv_rect_Type3 hterm h1 h2 h3 h4 h5 =
 665   let hcut = sFR8052_rect_Type3 h1 h2 h3 h4 h5 hterm in hcut __
 666
 667 (** val sFR8052_inv_rect_Type2 :
 668     sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 669     (__ -> 'a1) -> 'a1 **)
 670 let sFR8052_inv_rect_Type2 hterm h1 h2 h3 h4 h5 =
 671   let hcut = sFR8052_rect_Type2 h1 h2 h3 h4 h5 hterm in hcut __
 672
 673 (** val sFR8052_inv_rect_Type1 :
 674     sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 675     (__ -> 'a1) -> 'a1 **)
 676 let sFR8052_inv_rect_Type1 hterm h1 h2 h3 h4 h5 =
 677   let hcut = sFR8052_rect_Type1 h1 h2 h3 h4 h5 hterm in hcut __
 678
 679 (** val sFR8052_inv_rect_Type0 :
 680     sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 681     (__ -> 'a1) -> 'a1 **)
 682 let sFR8052_inv_rect_Type0 hterm h1 h2 h3 h4 h5 =
 683   let hcut = sFR8052_rect_Type0 h1 h2 h3 h4 h5 hterm in hcut __
 684
 685 (** val sFR8052_discr : sFR8052 -> sFR8052 -> __ **)
 686 let sFR8052_discr x y =
 687   Logic.eq_rect_Type2 x
 688     (match x with
 689      | SFR_T2CON -> Obj.magic (fun _ dH -> dH)
 690      | SFR_RCAP2L -> Obj.magic (fun _ dH -> dH)
 691      | SFR_RCAP2H -> Obj.magic (fun _ dH -> dH)
 692      | SFR_TL2 -> Obj.magic (fun _ dH -> dH)
 693      | SFR_TH2 -> Obj.magic (fun _ dH -> dH)) y
 694
 695 (** val sFR8052_jmdiscr : sFR8052 -> sFR8052 -> __ **)
 696 let sFR8052_jmdiscr x y =
 697   Logic.eq_rect_Type2 x
 698     (match x with
 699      | SFR_T2CON -> Obj.magic (fun _ dH -> dH)
 700      | SFR_RCAP2L -> Obj.magic (fun _ dH -> dH)
 701      | SFR_RCAP2H -> Obj.magic (fun _ dH -> dH)
 702      | SFR_TL2 -> Obj.magic (fun _ dH -> dH)
 703      | SFR_TH2 -> Obj.magic (fun _ dH -> dH)) y
 704
 705 (** val sfr_8052_index : sFR8052 -> Nat.nat **)
 706 let sfr_8052_index = function
 707 | SFR_T2CON -> Nat.O
 708 | SFR_RCAP2L -> Nat.S Nat.O
 709 | SFR_RCAP2H -> Nat.S (Nat.S Nat.O)
 710 | SFR_TL2 -> Nat.S (Nat.S (Nat.S Nat.O))
 711 | SFR_TH2 -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
 712
 713 type 'm preStatus = { low_internal_ram : BitVector.byte
 714                                          BitVectorTrie.bitVectorTrie;
 715                       high_internal_ram : BitVector.byte
 716                                           BitVectorTrie.bitVectorTrie;
 717                       external_ram : BitVector.byte
 718                                      BitVectorTrie.bitVectorTrie;
 719                       program_counter : BitVector.word;
 720                       special_function_registers_8051 : BitVector.byte
 721                                                         Vector.vector;
 722                       special_function_registers_8052 : BitVector.byte
 723                                                         Vector.vector;
 724                       p1_latch : BitVector.byte; p3_latch : BitVector.byte;
 725                       clock : time }
 726
 727 (** val preStatus_rect_Type4 :
 728     'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
 729     BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
 730     -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
 731     Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
 732     preStatus -> 'a2 **)
 733 let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_22224 =
 734   let { low_internal_ram = low_internal_ram0; high_internal_ram =
 735     high_internal_ram0; external_ram = external_ram0; program_counter =
 736     program_counter0; special_function_registers_8051 =
 737     special_function_registers_8053; special_function_registers_8052 =
 738     special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
 739     p3_latch0; clock = clock0 } = x_22224
 740   in
 741   h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
 742     program_counter0 special_function_registers_8053
 743     special_function_registers_8054 p1_latch0 p3_latch0 clock0
 744
 745 (** val preStatus_rect_Type5 :
 746     'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
 747     BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
 748     -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
 749     Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
 750     preStatus -> 'a2 **)
 751 let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_22226 =
 752   let { low_internal_ram = low_internal_ram0; high_internal_ram =
 753     high_internal_ram0; external_ram = external_ram0; program_counter =
 754     program_counter0; special_function_registers_8051 =
 755     special_function_registers_8053; special_function_registers_8052 =
 756     special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
 757     p3_latch0; clock = clock0 } = x_22226
 758   in
 759   h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
 760     program_counter0 special_function_registers_8053
 761     special_function_registers_8054 p1_latch0 p3_latch0 clock0
 762
 763 (** val preStatus_rect_Type3 :
 764     'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
 765     BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
 766     -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
 767     Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
 768     preStatus -> 'a2 **)
 769 let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_22228 =
 770   let { low_internal_ram = low_internal_ram0; high_internal_ram =
 771     high_internal_ram0; external_ram = external_ram0; program_counter =
 772     program_counter0; special_function_registers_8051 =
 773     special_function_registers_8053; special_function_registers_8052 =
 774     special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
 775     p3_latch0; clock = clock0 } = x_22228
 776   in
 777   h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
 778     program_counter0 special_function_registers_8053
 779     special_function_registers_8054 p1_latch0 p3_latch0 clock0
 780
 781 (** val preStatus_rect_Type2 :
 782     'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
 783     BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
 784     -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
 785     Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
 786     preStatus -> 'a2 **)
 787 let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_22230 =
 788   let { low_internal_ram = low_internal_ram0; high_internal_ram =
 789     high_internal_ram0; external_ram = external_ram0; program_counter =
 790     program_counter0; special_function_registers_8051 =
 791     special_function_registers_8053; special_function_registers_8052 =
 792     special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
 793     p3_latch0; clock = clock0 } = x_22230
 794   in
 795   h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
 796     program_counter0 special_function_registers_8053
 797     special_function_registers_8054 p1_latch0 p3_latch0 clock0
 798
 799 (** val preStatus_rect_Type1 :
 800     'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
 801     BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
 802     -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
 803     Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
 804     preStatus -> 'a2 **)
 805 let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_22232 =
 806   let { low_internal_ram = low_internal_ram0; high_internal_ram =
 807     high_internal_ram0; external_ram = external_ram0; program_counter =
 808     program_counter0; special_function_registers_8051 =
 809     special_function_registers_8053; special_function_registers_8052 =
 810     special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
 811     p3_latch0; clock = clock0 } = x_22232
 812   in
 813   h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
 814     program_counter0 special_function_registers_8053
 815     special_function_registers_8054 p1_latch0 p3_latch0 clock0
 816
 817 (** val preStatus_rect_Type0 :
 818     'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
 819     BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
 820     -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
 821     Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
 822     preStatus -> 'a2 **)
 823 let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_22234 =
 824   let { low_internal_ram = low_internal_ram0; high_internal_ram =
 825     high_internal_ram0; external_ram = external_ram0; program_counter =
 826     program_counter0; special_function_registers_8051 =
 827     special_function_registers_8053; special_function_registers_8052 =
 828     special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
 829     p3_latch0; clock = clock0 } = x_22234
 830   in
 831   h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
 832     program_counter0 special_function_registers_8053
 833     special_function_registers_8054 p1_latch0 p3_latch0 clock0
 834
 835 (** val low_internal_ram :
 836     'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie **)
 837 let rec low_internal_ram code_memory xxx =
 838   xxx.low_internal_ram
 839
 840 (** val high_internal_ram :
 841     'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie **)
 842 let rec high_internal_ram code_memory xxx =
 843   xxx.high_internal_ram
 844
 845 (** val external_ram :
 846     'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie **)
 847 let rec external_ram code_memory xxx =
 848   xxx.external_ram
 849
 850 (** val program_counter : 'a1 -> 'a1 preStatus -> BitVector.word **)
 851 let rec program_counter code_memory xxx =
 852   xxx.program_counter
 853
 854 (** val special_function_registers_8051 :
 855     'a1 -> 'a1 preStatus -> BitVector.byte Vector.vector **)
 856 let rec special_function_registers_8051 code_memory xxx =
 857   xxx.special_function_registers_8051
 858
 859 (** val special_function_registers_8052 :
 860     'a1 -> 'a1 preStatus -> BitVector.byte Vector.vector **)
 861 let rec special_function_registers_8052 code_memory xxx =
 862   xxx.special_function_registers_8052
 863
 864 (** val p1_latch : 'a1 -> 'a1 preStatus -> BitVector.byte **)
 865 let rec p1_latch code_memory xxx =
 866   xxx.p1_latch
 867
 868 (** val p3_latch : 'a1 -> 'a1 preStatus -> BitVector.byte **)
 869 let rec p3_latch code_memory xxx =
 870   xxx.p3_latch
 871
 872 (** val clock : 'a1 -> 'a1 preStatus -> time **)
 873 let rec clock code_memory xxx =
 874   xxx.clock
 875
 876 (** val preStatus_inv_rect_Type4 :
 877     'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
 878     BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
 879     BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
 880     Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
 881     BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
 882 let preStatus_inv_rect_Type4 x2 hterm h1 =
 883   let hcut = preStatus_rect_Type4 x2 h1 hterm in hcut __
 884
 885 (** val preStatus_inv_rect_Type3 :
 886     'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
 887     BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
 888     BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
 889     Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
 890     BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
 891 let preStatus_inv_rect_Type3 x2 hterm h1 =
 892   let hcut = preStatus_rect_Type3 x2 h1 hterm in hcut __
 893
 894 (** val preStatus_inv_rect_Type2 :
 895     'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
 896     BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
 897     BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
 898     Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
 899     BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
 900 let preStatus_inv_rect_Type2 x2 hterm h1 =
 901   let hcut = preStatus_rect_Type2 x2 h1 hterm in hcut __
 902
 903 (** val preStatus_inv_rect_Type1 :
 904     'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
 905     BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
 906     BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
 907     Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
 908     BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
 909 let preStatus_inv_rect_Type1 x2 hterm h1 =
 910   let hcut = preStatus_rect_Type1 x2 h1 hterm in hcut __
 911
 912 (** val preStatus_inv_rect_Type0 :
 913     'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
 914     BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
 915     BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
 916     Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
 917     BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
 918 let preStatus_inv_rect_Type0 x2 hterm h1 =
 919   let hcut = preStatus_rect_Type0 x2 h1 hterm in hcut __
 920
 921 (** val preStatus_jmdiscr : 'a1 -> 'a1 preStatus -> 'a1 preStatus -> __ **)
 922 let preStatus_jmdiscr a2 x y =
 923   Logic.eq_rect_Type2 x
 924     (let { low_internal_ram = a0; high_internal_ram = a10; external_ram =
 925        a20; program_counter = a3; special_function_registers_8051 = a4;
 926        special_function_registers_8052 = a5; p1_latch = a6; p3_latch = a7;
 927        clock = a8 } = x
 928      in
 929     Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __)) y
 930
 931 type status = BitVector.byte BitVectorTrie.bitVectorTrie preStatus
 932
 933 type pseudoStatus = ASM.pseudo_assembly_program preStatus
 934
 935 (** val set_clock : 'a1 -> 'a1 preStatus -> time -> 'a1 preStatus **)
 936 let set_clock code_memory s t =
 937   let old_low_internal_ram = s.low_internal_ram in
 938   let old_high_internal_ram = s.high_internal_ram in
 939   let old_external_ram = s.external_ram in
 940   let old_program_counter = s.program_counter in
 941   let old_special_function_registers_8051 = s.special_function_registers_8051
 942   in
 943   let old_special_function_registers_8052 = s.special_function_registers_8052
 944   in
 945   let old_p1_latch = s.p1_latch in
 946   let old_p3_latch = s.p3_latch in
 947   { low_internal_ram = old_low_internal_ram; high_internal_ram =
 948   old_high_internal_ram; external_ram = old_external_ram; program_counter =
 949   old_program_counter; special_function_registers_8051 =
 950   old_special_function_registers_8051; special_function_registers_8052 =
 951   old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
 952   old_p3_latch; clock = t }
 953
 954 (** val set_p1_latch :
 955     'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus **)
 956 let set_p1_latch code_memory s b =
 957   let old_low_internal_ram = s.low_internal_ram in
 958   let old_high_internal_ram = s.high_internal_ram in
 959   let old_external_ram = s.external_ram in
 960   let old_program_counter = s.program_counter in
 961   let old_special_function_registers_8051 = s.special_function_registers_8051
 962   in
 963   let old_special_function_registers_8052 = s.special_function_registers_8052
 964   in
 965   let old_p3_latch = s.p3_latch in
 966   let old_clock = s.clock in
 967   { low_internal_ram = old_low_internal_ram; high_internal_ram =
 968   old_high_internal_ram; external_ram = old_external_ram; program_counter =
 969   old_program_counter; special_function_registers_8051 =
 970   old_special_function_registers_8051; special_function_registers_8052 =
 971   old_special_function_registers_8052; p1_latch = b; p3_latch = old_p3_latch;
 972   clock = old_clock }
 973
 974 (** val set_p3_latch :
 975     'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus **)
 976 let set_p3_latch code_memory s b =
 977   let old_low_internal_ram = s.low_internal_ram in
 978   let old_high_internal_ram = s.high_internal_ram in
 979   let old_external_ram = s.external_ram in
 980   let old_program_counter = s.program_counter in
 981   let old_special_function_registers_8051 = s.special_function_registers_8051
 982   in
 983   let old_special_function_registers_8052 = s.special_function_registers_8052
 984   in
 985   let old_p1_latch = s.p1_latch in
 986   let old_clock = s.clock in
 987   { low_internal_ram = old_low_internal_ram; high_internal_ram =
 988   old_high_internal_ram; external_ram = old_external_ram; program_counter =
 989   old_program_counter; special_function_registers_8051 =
 990   old_special_function_registers_8051; special_function_registers_8052 =
 991   old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch = b;
 992   clock = old_clock }
 993
 994 (** val get_8051_sfr : 'a1 -> 'a1 preStatus -> sFR8051 -> BitVector.byte **)
 995 let get_8051_sfr code_memory s i =
 996   let sfr = s.special_function_registers_8051 in
 997   let index = sfr_8051_index i in
 998   Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 999     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1000     (Nat.S Nat.O))))))))))))))))))) sfr index
1001
1002 (** val get_8052_sfr : 'a1 -> 'a1 preStatus -> sFR8052 -> BitVector.byte **)
1003 let get_8052_sfr code_memory s i =
1004   let sfr = s.special_function_registers_8052 in
1005   let index = sfr_8052_index i in
1006   Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) sfr index
1007
1008 (** val set_8051_sfr :
1009     'a1 -> 'a1 preStatus -> sFR8051 -> BitVector.byte -> 'a1 preStatus **)
1010 let set_8051_sfr code_memory s i b =
1011   let index = sfr_8051_index i in
1012   let old_low_internal_ram = s.low_internal_ram in
1013   let old_high_internal_ram = s.high_internal_ram in
1014   let old_external_ram = s.external_ram in
1015   let old_program_counter = s.program_counter in
1016   let old_special_function_registers_8051 = s.special_function_registers_8051
1017   in
1018   let old_special_function_registers_8052 = s.special_function_registers_8052
1019   in
1020   let new_special_function_registers_8051 =
1021     Vector.set_index (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1022       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1023       (Nat.S Nat.O))))))))))))))))))) old_special_function_registers_8051
1024       index b
1025   in
1026   let old_p1_latch = s.p1_latch in
1027   let old_p3_latch = s.p3_latch in
1028   let old_clock = s.clock in
1029   { low_internal_ram = old_low_internal_ram; high_internal_ram =
1030   old_high_internal_ram; external_ram = old_external_ram; program_counter =
1031   old_program_counter; special_function_registers_8051 =
1032   new_special_function_registers_8051; special_function_registers_8052 =
1033   old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
1034   old_p3_latch; clock = old_clock }
1035
1036 (** val set_8052_sfr :
1037     'a1 -> 'a1 preStatus -> sFR8052 -> BitVector.byte -> 'a1 preStatus **)
1038 let set_8052_sfr code_memory s i b =
1039   let index = sfr_8052_index i in
1040   let old_low_internal_ram = s.low_internal_ram in
1041   let old_high_internal_ram = s.high_internal_ram in
1042   let old_external_ram = s.external_ram in
1043   let old_program_counter = s.program_counter in
1044   let old_special_function_registers_8051 = s.special_function_registers_8051
1045   in
1046   let old_special_function_registers_8052 = s.special_function_registers_8052
1047   in
1048   let new_special_function_registers_8052 =
1049     Vector.set_index (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
1050       old_special_function_registers_8052 index b
1051   in
1052   let old_p1_latch = s.p1_latch in
1053   let old_p3_latch = s.p3_latch in
1054   let old_clock = s.clock in
1055   { low_internal_ram = old_low_internal_ram; high_internal_ram =
1056   old_high_internal_ram; external_ram = old_external_ram; program_counter =
1057   old_program_counter; special_function_registers_8051 =
1058   old_special_function_registers_8051; special_function_registers_8052 =
1059   new_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
1060   old_p3_latch; clock = old_clock }
1061
1062 (** val set_program_counter :
1063     'a1 -> 'a1 preStatus -> BitVector.word -> 'a1 preStatus **)
1064 let set_program_counter code_memory s w =
1065   let old_low_internal_ram = s.low_internal_ram in
1066   let old_high_internal_ram = s.high_internal_ram in
1067   let old_external_ram = s.external_ram in
1068   let old_special_function_registers_8051 = s.special_function_registers_8051
1069   in
1070   let old_special_function_registers_8052 = s.special_function_registers_8052
1071   in
1072   let old_p1_latch = s.p1_latch in
1073   let old_p3_latch = s.p3_latch in
1074   let old_clock = s.clock in
1075   { low_internal_ram = old_low_internal_ram; high_internal_ram =
1076   old_high_internal_ram; external_ram = old_external_ram; program_counter =
1077   w; special_function_registers_8051 = old_special_function_registers_8051;
1078   special_function_registers_8052 = old_special_function_registers_8052;
1079   p1_latch = old_p1_latch; p3_latch = old_p3_latch; clock = old_clock }
1080
1081 (** val set_code_memory : 'a1 -> 'a1 preStatus -> 'a2 -> 'a2 preStatus **)
1082 let set_code_memory code_memory s r =
1083   let old_low_internal_ram = s.low_internal_ram in
1084   let old_high_internal_ram = s.high_internal_ram in
1085   let old_external_ram = s.external_ram in
1086   let old_program_counter = s.program_counter in
1087   let old_special_function_registers_8051 = s.special_function_registers_8051
1088   in
1089   let old_special_function_registers_8052 = s.special_function_registers_8052
1090   in
1091   let old_p1_latch = s.p1_latch in
1092   let old_p3_latch = s.p3_latch in
1093   let old_clock = s.clock in
1094   { low_internal_ram = old_low_internal_ram; high_internal_ram =
1095   old_high_internal_ram; external_ram = old_external_ram; program_counter =
1096   old_program_counter; special_function_registers_8051 =
1097   old_special_function_registers_8051; special_function_registers_8052 =
1098   old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
1099   old_p3_latch; clock = old_clock }
1100
1101 (** val set_low_internal_ram :
1102     'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
1103     preStatus **)
1104 let set_low_internal_ram code_memory s r =
1105   let old_high_internal_ram = s.high_internal_ram in
1106   let old_external_ram = s.external_ram in
1107   let old_program_counter = s.program_counter in
1108   let old_special_function_registers_8051 = s.special_function_registers_8051
1109   in
1110   let old_special_function_registers_8052 = s.special_function_registers_8052
1111   in
1112   let old_p1_latch = s.p1_latch in
1113   let old_p3_latch = s.p3_latch in
1114   let old_clock = s.clock in
1115   { low_internal_ram = r; high_internal_ram = old_high_internal_ram;
1116   external_ram = old_external_ram; program_counter = old_program_counter;
1117   special_function_registers_8051 = old_special_function_registers_8051;
1118   special_function_registers_8052 = old_special_function_registers_8052;
1119   p1_latch = old_p1_latch; p3_latch = old_p3_latch; clock = old_clock }
1120
1121 (** val update_low_internal_ram :
1122     'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
1123     preStatus **)
1124 let update_low_internal_ram code_memory s addr v =
1125   let old_low_internal_ram = s.low_internal_ram in
1126   let new_low_internal_ram =
1127     BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1128       Nat.O))))))) addr v old_low_internal_ram
1129   in
1130   set_low_internal_ram code_memory s new_low_internal_ram
1131
1132 (** val set_high_internal_ram :
1133     'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
1134     preStatus **)
1135 let set_high_internal_ram code_memory s r =
1136   let old_low_internal_ram = s.low_internal_ram in
1137   let old_high_internal_ram = s.high_internal_ram in
1138   let old_external_ram = s.external_ram in
1139   let old_program_counter = s.program_counter in
1140   let old_special_function_registers_8051 = s.special_function_registers_8051
1141   in
1142   let old_special_function_registers_8052 = s.special_function_registers_8052
1143   in
1144   let old_p1_latch = s.p1_latch in
1145   let old_p3_latch = s.p3_latch in
1146   let old_clock = s.clock in
1147   { low_internal_ram = old_low_internal_ram; high_internal_ram = r;
1148   external_ram = old_external_ram; program_counter = old_program_counter;
1149   special_function_registers_8051 = old_special_function_registers_8051;
1150   special_function_registers_8052 = old_special_function_registers_8052;
1151   p1_latch = old_p1_latch; p3_latch = old_p3_latch; clock = old_clock }
1152
1153 (** val update_high_internal_ram :
1154     'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
1155     preStatus **)
1156 let update_high_internal_ram code_memory s addr v =
1157   let old_high_internal_ram = s.high_internal_ram in
1158   let new_high_internal_ram =
1159     BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1160       Nat.O))))))) addr v old_high_internal_ram
1161   in
1162   set_high_internal_ram code_memory s new_high_internal_ram
1163
1164 (** val set_external_ram :
1165     'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
1166     preStatus **)
1167 let set_external_ram code_memory s r =
1168   let old_low_internal_ram = s.low_internal_ram in
1169   let old_high_internal_ram = s.high_internal_ram in
1170   let old_program_counter = s.program_counter in
1171   let old_special_function_registers_8051 = s.special_function_registers_8051
1172   in
1173   let old_special_function_registers_8052 = s.special_function_registers_8052
1174   in
1175   let old_p1_latch = s.p1_latch in
1176   let old_p3_latch = s.p3_latch in
1177   let old_clock = s.clock in
1178   { low_internal_ram = old_low_internal_ram; high_internal_ram =
1179   old_high_internal_ram; external_ram = r; program_counter =
1180   old_program_counter; special_function_registers_8051 =
1181   old_special_function_registers_8051; special_function_registers_8052 =
1182   old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
1183   old_p3_latch; clock = old_clock }
1184
1185 (** val update_external_ram :
1186     'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
1187     preStatus **)
1188 let update_external_ram code_memory s addr v =
1189   let old_external_ram = s.external_ram in
1190   let new_external_ram =
1191     BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1192       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1193       Nat.O)))))))))))))))) addr v old_external_ram
1194   in
1195   set_external_ram code_memory s new_external_ram
1196
1197 (** val get_psw_flags : 'a1 -> 'a1 preStatus -> Nat.nat -> Bool.bool **)
1198 let get_psw_flags code_memory s flag =
1199   let psw = get_8051_sfr code_memory s SFR_PSW in
1200   Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1201     Nat.O)))))))) psw flag
1202
1203 (** val get_cy_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1204 let get_cy_flag code_memory s =
1205   get_psw_flags code_memory s Nat.O
1206
1207 (** val get_ac_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1208 let get_ac_flag code_memory s =
1209   get_psw_flags code_memory s (Nat.S Nat.O)
1210
1211 (** val get_fo_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1212 let get_fo_flag code_memory s =
1213   get_psw_flags code_memory s (Nat.S (Nat.S Nat.O))
1214
1215 (** val get_rs1_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1216 let get_rs1_flag code_memory s =
1217   get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S Nat.O)))
1218
1219 (** val get_rs0_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1220 let get_rs0_flag code_memory s =
1221   get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
1222
1223 (** val get_ov_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1224 let get_ov_flag code_memory s =
1225   get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
1226
1227 (** val get_ud_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1228 let get_ud_flag code_memory s =
1229   get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1230     Nat.O))))))
1231
1232 (** val get_p_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1233 let get_p_flag code_memory s =
1234   get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1235     (Nat.S Nat.O)))))))
1236
1237 (** val set_flags :
1238     'a1 -> 'a1 preStatus -> BitVector.bit -> BitVector.bit Types.option ->
1239     BitVector.bit -> 'a1 preStatus **)
1240 let set_flags code_memory s cy ac ov =
1241   let old_cy = get_cy_flag code_memory s in
1242   let old_ac = get_ac_flag code_memory s in
1243   let old_fo = get_fo_flag code_memory s in
1244   let old_rs1 = get_rs1_flag code_memory s in
1245   let old_rs0 = get_rs0_flag code_memory s in
1246   let old_ov = get_ov_flag code_memory s in
1247   let old_ud = get_ud_flag code_memory s in
1248   let old_p = get_p_flag code_memory s in
1249   let new_ac =
1250     match ac with
1251     | Types.None -> old_ac
1252     | Types.Some j -> j
1253   in
1254   set_8051_sfr code_memory s SFR_PSW (Vector.VCons ((Nat.S (Nat.S (Nat.S
1255     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), cy, (Vector.VCons ((Nat.S
1256     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), new_ac, (Vector.VCons
1257     ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), old_fo, (Vector.VCons
1258     ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), old_rs1, (Vector.VCons ((Nat.S
1259     (Nat.S (Nat.S Nat.O))), old_rs0, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1260     ov, (Vector.VCons ((Nat.S Nat.O), old_ud, (Vector.VCons (Nat.O, old_p,
1261     Vector.VEmpty))))))))))))))))
1262
1263 (** val initialise_status : 'a1 -> 'a1 preStatus **)
1264 let initialise_status code_mem =
1265   let status0 = { low_internal_ram = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S
1266     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))); high_internal_ram =
1267     (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1268     Nat.O)))))))); external_ram = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S
1269     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1270     (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))); program_counter =
1271     (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1272       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1273       Nat.O))))))))))))))))); special_function_registers_8051 =
1274     (Vector.replicate (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1275       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1276       (Nat.S Nat.O)))))))))))))))))))
1277       (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1278         Nat.O)))))))))); special_function_registers_8052 =
1279     (Vector.replicate (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
1280       (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1281         Nat.O)))))))))); p1_latch =
1282     (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1283       Nat.O))))))))); p3_latch =
1284     (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1285       Nat.O))))))))); clock = Nat.O }
1286   in
1287   set_8051_sfr code_mem status0 SFR_SP
1288     (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1289       (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1290       (Nat.S Nat.O))))))))
1291
1292 (** val sfr_of_Byte :
1293     BitVector.byte -> (sFR8051, sFR8052) Types.sum Types.option **)
1294 let sfr_of_Byte b =
1295   let address =
1296     Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1297       (Nat.S (Nat.S Nat.O)))))))) b
1298   in
1299   (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1300            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1301            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1302            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1303            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1304            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1305            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1306            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1307            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1308            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1309            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1310            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1311            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1312            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1313            (Nat.S (Nat.S (Nat.S (Nat.S
1314            Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1315    | Bool.True -> Types.None
1316    | Bool.False ->
1317      (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1318               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1319               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1320               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1321               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1322               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1323               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1324               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1325               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1326               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1327               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1328               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1329               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1330               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1331               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1332               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1333               (Nat.S (Nat.S
1334               Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1335       | Bool.True -> Types.Some (Types.Inl SFR_P1)
1336       | Bool.False ->
1337         (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1338                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1339                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1340                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1341                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1342                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1343                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1344                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1345                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1346                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1347                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1348                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1349                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1350                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1351                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1352                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1353                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1354                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1355                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1356                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1357                  (Nat.S (Nat.S
1358                  Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1359          | Bool.True -> Types.None
1360          | Bool.False ->
1361            (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1362                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1363                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1364                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1365                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1366                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1367                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1368                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1369                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1370                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1371                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1372                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1373                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1374                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1375                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1376                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1377                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1378                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1379                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1380                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1381                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1382                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1383                     (Nat.S (Nat.S
1384                     Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1385             | Bool.True -> Types.Some (Types.Inl SFR_P3)
1386             | Bool.False ->
1387               (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1388                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1389                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1390                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1391                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1392                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1393                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1394                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1395                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1396                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1397                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1398                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1399                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1400                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1401                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1402                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1403                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1404                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1405                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1406                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1407                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1408                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1409                        (Nat.S
1410                        Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1411                | Bool.True -> Types.Some (Types.Inl SFR_SBUF)
1412                | Bool.False ->
1413                  (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1414                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1415                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1416                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1417                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1418                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1419                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1420                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1421                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1422                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1423                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1424                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1425                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1426                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1427                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1428                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1429                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1430                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1431                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1432                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1433                           Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1434                   | Bool.True -> Types.Some (Types.Inl SFR_TL0)
1435                   | Bool.False ->
1436                     (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1437                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1438                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1439                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1440                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1441                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1442                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1443                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1444                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1445                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1446                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1447                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1448                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1449                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1450                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1451                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1452                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1453                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1454                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1455                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1456                              (Nat.S
1457                              Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1458                      | Bool.True -> Types.Some (Types.Inl SFR_TL1)
1459                      | Bool.False ->
1460                        (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S
1461                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1462                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1463                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1464                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1465                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1466                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1467                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1468                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1469                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1470                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1471                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1472                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1473                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1474                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1475                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1476                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1477                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1478                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1479                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1480                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1481                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1482                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1483                                 (Nat.S (Nat.S (Nat.S (Nat.S
1484                                 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1485                         | Bool.True -> Types.Some (Types.Inl SFR_TH0)
1486                         | Bool.False ->
1487                           (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S
1488                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1489                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1490                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1491                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1492                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1493                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1494                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1495                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1496                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1497                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1498                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1499                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1500                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1501                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1502                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1503                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1504                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1505                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1506                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1507                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1508                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1509                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1510                                    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1511                                    Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1512                            | Bool.True -> Types.Some (Types.Inl SFR_TH1)
1513                            | Bool.False ->
1514                              (match Nat.eqb address (Nat.S (Nat.S (Nat.S
1515                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1516                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1517                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1518                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1519                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1520                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1521                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1522                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1523                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1524                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1525                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1526                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1527                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1528                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1529                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1530                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1531                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1532                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1533                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1534                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1535                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1536                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1537                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1538                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1539                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1540                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1541                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1542                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1543                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1544                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1545                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1546                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1547                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1548                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1549                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1550                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1551                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1552                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1553                                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1554                                       (Nat.S (Nat.S
1555                                       Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1556                               | Bool.True -> Types.Some (Types.Inr SFR_T2CON)
1557                               | Bool.False ->
1558                                 (match Nat.eqb address (Nat.S (Nat.S (Nat.S
1559                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1560                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1561                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1562                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1563                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1564                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1565                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1566                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1567                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1568                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1569                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1570                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1571                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1572                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1573                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1574                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1575                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1576                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1577                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1578                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1579                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1580                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1581                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1582                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1583                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1584                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1585                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1586                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1587                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1588                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1589                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1590                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1591                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1592                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1593                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1594                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1595                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1596                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1597                                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1598                                          (Nat.S (Nat.S (Nat.S (Nat.S
1599                                          Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1600                                  | Bool.True ->
1601                                    Types.Some (Types.Inr SFR_RCAP2L)
1602                                  | Bool.False ->
1603                                    (match Nat.eqb address (Nat.S (Nat.S
1604                                             (Nat.S (Nat.S (Nat.S (Nat.S
1605                                             (Nat.S (Nat.S (Nat.S (Nat.S
1606                                             (Nat.S (Nat.S (Nat.S (Nat.S
1607                                             (Nat.S (Nat.S (Nat.S (Nat.S
1608                                             (Nat.S (Nat.S (Nat.S (Nat.S
1609                                             (Nat.S (Nat.S (Nat.S (Nat.S
1610                                             (Nat.S (Nat.S (Nat.S (Nat.S
1611                                             (Nat.S (Nat.S (Nat.S (Nat.S
1612                                             (Nat.S (Nat.S (Nat.S (Nat.S
1613                                             (Nat.S (Nat.S (Nat.S (Nat.S
1614                                             (Nat.S (Nat.S (Nat.S (Nat.S
1615                                             (Nat.S (Nat.S (Nat.S (Nat.S
1616                                             (Nat.S (Nat.S (Nat.S (Nat.S
1617                                             (Nat.S (Nat.S (Nat.S (Nat.S
1618                                             (Nat.S (Nat.S (Nat.S (Nat.S
1619                                             (Nat.S (Nat.S (Nat.S (Nat.S
1620                                             (Nat.S (Nat.S (Nat.S (Nat.S
1621                                             (Nat.S (Nat.S (Nat.S (Nat.S
1622                                             (Nat.S (Nat.S (Nat.S (Nat.S
1623                                             (Nat.S (Nat.S (Nat.S (Nat.S
1624                                             (Nat.S (Nat.S (Nat.S (Nat.S
1625                                             (Nat.S (Nat.S (Nat.S (Nat.S
1626                                             (Nat.S (Nat.S (Nat.S (Nat.S
1627                                             (Nat.S (Nat.S (Nat.S (Nat.S
1628                                             (Nat.S (Nat.S (Nat.S (Nat.S
1629                                             (Nat.S (Nat.S (Nat.S (Nat.S
1630                                             (Nat.S (Nat.S (Nat.S (Nat.S
1631                                             (Nat.S (Nat.S (Nat.S (Nat.S
1632                                             (Nat.S (Nat.S (Nat.S (Nat.S
1633                                             (Nat.S (Nat.S (Nat.S (Nat.S
1634                                             (Nat.S (Nat.S (Nat.S (Nat.S
1635                                             (Nat.S (Nat.S (Nat.S (Nat.S
1636                                             (Nat.S (Nat.S (Nat.S (Nat.S
1637                                             (Nat.S (Nat.S (Nat.S (Nat.S
1638                                             (Nat.S (Nat.S (Nat.S (Nat.S
1639                                             (Nat.S (Nat.S (Nat.S (Nat.S
1640                                             (Nat.S (Nat.S (Nat.S (Nat.S
1641                                             (Nat.S (Nat.S (Nat.S (Nat.S
1642                                             (Nat.S (Nat.S (Nat.S (Nat.S
1643                                             (Nat.S (Nat.S (Nat.S (Nat.S
1644                                             (Nat.S (Nat.S (Nat.S (Nat.S
1645                                             (Nat.S (Nat.S (Nat.S (Nat.S
1646                                             (Nat.S (Nat.S (Nat.S (Nat.S
1647                                             (Nat.S (Nat.S (Nat.S (Nat.S
1648                                             (Nat.S (Nat.S (Nat.S (Nat.S
1649                                             (Nat.S (Nat.S (Nat.S (Nat.S
1650                                             (Nat.S (Nat.S (Nat.S (Nat.S
1651                                             (Nat.S (Nat.S (Nat.S (Nat.S
1652                                             (Nat.S (Nat.S (Nat.S (Nat.S
1653                                             (Nat.S (Nat.S (Nat.S (Nat.S
1654                                             (Nat.S
1655                                             Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1656                                     | Bool.True ->
1657                                       Types.Some (Types.Inr SFR_RCAP2H)
1658                                     | Bool.False ->
1659                                       (match Nat.eqb address (Nat.S (Nat.S
1660                                                (Nat.S (Nat.S (Nat.S (Nat.S
1661                                                (Nat.S (Nat.S (Nat.S (Nat.S
1662                                                (Nat.S (Nat.S (Nat.S (Nat.S
1663                                                (Nat.S (Nat.S (Nat.S (Nat.S
1664                                                (Nat.S (Nat.S (Nat.S (Nat.S
1665                                                (Nat.S (Nat.S (Nat.S (Nat.S
1666                                                (Nat.S (Nat.S (Nat.S (Nat.S
1667                                                (Nat.S (Nat.S (Nat.S (Nat.S
1668                                                (Nat.S (Nat.S (Nat.S (Nat.S
1669                                                (Nat.S (Nat.S (Nat.S (Nat.S
1670                                                (Nat.S (Nat.S (Nat.S (Nat.S
1671                                                (Nat.S (Nat.S (Nat.S (Nat.S
1672                                                (Nat.S (Nat.S (Nat.S (Nat.S
1673                                                (Nat.S (Nat.S (Nat.S (Nat.S
1674                                                (Nat.S (Nat.S (Nat.S (Nat.S
1675                                                (Nat.S (Nat.S (Nat.S (Nat.S
1676                                                (Nat.S (Nat.S (Nat.S (Nat.S
1677                                                (Nat.S (Nat.S (Nat.S (Nat.S
1678                                                (Nat.S (Nat.S (Nat.S (Nat.S
1679                                                (Nat.S (Nat.S (Nat.S (Nat.S
1680                                                (Nat.S (Nat.S (Nat.S (Nat.S
1681                                                (Nat.S (Nat.S (Nat.S (Nat.S
1682                                                (Nat.S (Nat.S (Nat.S (Nat.S
1683                                                (Nat.S (Nat.S (Nat.S (Nat.S
1684                                                (Nat.S (Nat.S (Nat.S (Nat.S
1685                                                (Nat.S (Nat.S (Nat.S (Nat.S
1686                                                (Nat.S (Nat.S (Nat.S (Nat.S
1687                                                (Nat.S (Nat.S (Nat.S (Nat.S
1688                                                (Nat.S (Nat.S (Nat.S (Nat.S
1689                                                (Nat.S (Nat.S (Nat.S (Nat.S
1690                                                (Nat.S (Nat.S (Nat.S (Nat.S
1691                                                (Nat.S (Nat.S (Nat.S (Nat.S
1692                                                (Nat.S (Nat.S (Nat.S (Nat.S
1693                                                (Nat.S (Nat.S (Nat.S (Nat.S
1694                                                (Nat.S (Nat.S (Nat.S (Nat.S
1695                                                (Nat.S (Nat.S (Nat.S (Nat.S
1696                                                (Nat.S (Nat.S (Nat.S (Nat.S
1697                                                (Nat.S (Nat.S (Nat.S (Nat.S
1698                                                (Nat.S (Nat.S (Nat.S (Nat.S
1699                                                (Nat.S (Nat.S (Nat.S (Nat.S
1700                                                (Nat.S (Nat.S (Nat.S (Nat.S
1701                                                (Nat.S (Nat.S (Nat.S (Nat.S
1702                                                (Nat.S (Nat.S (Nat.S (Nat.S
1703                                                (Nat.S (Nat.S (Nat.S (Nat.S
1704                                                (Nat.S (Nat.S (Nat.S (Nat.S
1705                                                (Nat.S (Nat.S (Nat.S (Nat.S
1706                                                (Nat.S (Nat.S (Nat.S (Nat.S
1707                                                (Nat.S (Nat.S (Nat.S (Nat.S
1708                                                (Nat.S (Nat.S (Nat.S (Nat.S
1709                                                (Nat.S (Nat.S (Nat.S (Nat.S
1710                                                (Nat.S (Nat.S
1711                                                Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1712                                        | Bool.True ->
1713                                          Types.Some (Types.Inr SFR_TL2)
1714                                        | Bool.False ->
1715                                          (match Nat.eqb address (Nat.S (Nat.S
1716                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1717                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1718                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1719                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1720                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1721                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1722                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1723                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1724                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1725                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1726                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1727                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1728                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1729                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1730                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1731                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1732                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1733                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1734                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1735                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1736                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1737                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1738                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1739                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1740                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1741                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1742                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1743                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1744                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1745                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1746                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1747                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1748                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1749                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1750                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1751                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1752                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1753                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1754                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1755                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1756                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1757                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1758                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1759                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1760                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1761                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1762                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1763                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1764                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1765                                                   (Nat.S (Nat.S (Nat.S (Nat.S
1766                                                   (Nat.S (Nat.S (Nat.S
1767                                                   Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1768                                           | Bool.True ->
1769                                             Types.Some (Types.Inr SFR_TH2)
1770                                           | Bool.False ->
1771                                             (match Nat.eqb address (Nat.S
1772                                                      (Nat.S (Nat.S (Nat.S
1773                                                      (Nat.S (Nat.S (Nat.S
1774                                                      (Nat.S (Nat.S (Nat.S
1775                                                      (Nat.S (Nat.S (Nat.S
1776                                                      (Nat.S (Nat.S (Nat.S
1777                                                      (Nat.S (Nat.S (Nat.S
1778                                                      (Nat.S (Nat.S (Nat.S
1779                                                      (Nat.S (Nat.S (Nat.S
1780                                                      (Nat.S (Nat.S (Nat.S
1781                                                      (Nat.S (Nat.S (Nat.S
1782                                                      (Nat.S (Nat.S (Nat.S
1783                                                      (Nat.S (Nat.S (Nat.S
1784                                                      (Nat.S (Nat.S (Nat.S
1785                                                      (Nat.S (Nat.S (Nat.S
1786                                                      (Nat.S (Nat.S (Nat.S
1787                                                      (Nat.S (Nat.S (Nat.S
1788                                                      (Nat.S (Nat.S (Nat.S
1789                                                      (Nat.S (Nat.S (Nat.S
1790                                                      (Nat.S (Nat.S (Nat.S
1791                                                      (Nat.S (Nat.S (Nat.S
1792                                                      (Nat.S (Nat.S (Nat.S
1793                                                      (Nat.S (Nat.S (Nat.S
1794                                                      (Nat.S (Nat.S (Nat.S
1795                                                      (Nat.S (Nat.S (Nat.S
1796                                                      (Nat.S (Nat.S (Nat.S
1797                                                      (Nat.S (Nat.S (Nat.S
1798                                                      (Nat.S (Nat.S (Nat.S
1799                                                      (Nat.S (Nat.S (Nat.S
1800                                                      (Nat.S (Nat.S (Nat.S
1801                                                      (Nat.S (Nat.S (Nat.S
1802                                                      (Nat.S (Nat.S (Nat.S
1803                                                      (Nat.S (Nat.S (Nat.S
1804                                                      (Nat.S (Nat.S (Nat.S
1805                                                      (Nat.S (Nat.S (Nat.S
1806                                                      (Nat.S (Nat.S (Nat.S
1807                                                      (Nat.S (Nat.S (Nat.S
1808                                                      (Nat.S (Nat.S (Nat.S
1809                                                      (Nat.S (Nat.S (Nat.S
1810                                                      (Nat.S (Nat.S (Nat.S
1811                                                      (Nat.S (Nat.S (Nat.S
1812                                                      (Nat.S (Nat.S (Nat.S
1813                                                      (Nat.S (Nat.S (Nat.S
1814                                                      (Nat.S (Nat.S (Nat.S
1815                                                      (Nat.S (Nat.S (Nat.S
1816                                                      (Nat.S (Nat.S
1817                                                      Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1818                                              | Bool.True ->
1819                                                Types.Some (Types.Inl
1820                                                  SFR_PCON)
1821                                              | Bool.False ->
1822                                                (match Nat.eqb address (Nat.S
1823                                                         (Nat.S (Nat.S (Nat.S
1824                                                         (Nat.S (Nat.S (Nat.S
1825                                                         (Nat.S (Nat.S (Nat.S
1826                                                         (Nat.S (Nat.S (Nat.S
1827                                                         (Nat.S (Nat.S (Nat.S
1828                                                         (Nat.S (Nat.S (Nat.S
1829                                                         (Nat.S (Nat.S (Nat.S
1830                                                         (Nat.S (Nat.S (Nat.S
1831                                                         (Nat.S (Nat.S (Nat.S
1832                                                         (Nat.S (Nat.S (Nat.S
1833                                                         (Nat.S (Nat.S (Nat.S
1834                                                         (Nat.S (Nat.S (Nat.S
1835                                                         (Nat.S (Nat.S (Nat.S
1836                                                         (Nat.S (Nat.S (Nat.S
1837                                                         (Nat.S (Nat.S (Nat.S
1838                                                         (Nat.S (Nat.S (Nat.S
1839                                                         (Nat.S (Nat.S (Nat.S
1840                                                         (Nat.S (Nat.S (Nat.S
1841                                                         (Nat.S (Nat.S (Nat.S
1842                                                         (Nat.S (Nat.S (Nat.S
1843                                                         (Nat.S (Nat.S (Nat.S
1844                                                         (Nat.S (Nat.S (Nat.S
1845                                                         (Nat.S (Nat.S (Nat.S
1846                                                         (Nat.S (Nat.S (Nat.S
1847                                                         (Nat.S (Nat.S (Nat.S
1848                                                         (Nat.S (Nat.S (Nat.S
1849                                                         (Nat.S (Nat.S (Nat.S
1850                                                         (Nat.S (Nat.S (Nat.S
1851                                                         (Nat.S (Nat.S (Nat.S
1852                                                         (Nat.S (Nat.S (Nat.S
1853                                                         (Nat.S (Nat.S (Nat.S
1854                                                         (Nat.S (Nat.S (Nat.S
1855                                                         (Nat.S (Nat.S (Nat.S
1856                                                         (Nat.S (Nat.S (Nat.S
1857                                                         (Nat.S (Nat.S (Nat.S
1858                                                         (Nat.S (Nat.S (Nat.S
1859                                                         (Nat.S (Nat.S (Nat.S
1860                                                         (Nat.S (Nat.S (Nat.S
1861                                                         (Nat.S (Nat.S (Nat.S
1862                                                         (Nat.S (Nat.S (Nat.S
1863                                                         (Nat.S (Nat.S (Nat.S
1864                                                         (Nat.S (Nat.S (Nat.S
1865                                                         (Nat.S (Nat.S (Nat.S
1866                                                         (Nat.S (Nat.S (Nat.S
1867                                                         (Nat.S (Nat.S (Nat.S
1868                                                         Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1869                                                 | Bool.True ->
1870                                                   Types.Some (Types.Inl
1871                                                     SFR_TCON)
1872                                                 | Bool.False ->
1873                                                   (match Nat.eqb address
1874                                                            (Nat.S (Nat.S
1875                                                            (Nat.S (Nat.S
1876                                                            (Nat.S (Nat.S
1877                                                            (Nat.S (Nat.S
1878                                                            (Nat.S (Nat.S
1879                                                            (Nat.S (Nat.S
1880                                                            (Nat.S (Nat.S
1881                                                            (Nat.S (Nat.S
1882                                                            (Nat.S (Nat.S
1883                                                            (Nat.S (Nat.S
1884                                                            (Nat.S (Nat.S
1885                                                            (Nat.S (Nat.S
1886                                                            (Nat.S (Nat.S
1887                                                            (Nat.S (Nat.S
1888                                                            (Nat.S (Nat.S
1889                                                            (Nat.S (Nat.S
1890                                                            (Nat.S (Nat.S
1891                                                            (Nat.S (Nat.S
1892                                                            (Nat.S (Nat.S
1893                                                            (Nat.S (Nat.S
1894                                                            (Nat.S (Nat.S
1895                                                            (Nat.S (Nat.S
1896                                                            (Nat.S (Nat.S
1897                                                            (Nat.S (Nat.S
1898                                                            (Nat.S (Nat.S
1899                                                            (Nat.S (Nat.S
1900                                                            (Nat.S (Nat.S
1901                                                            (Nat.S (Nat.S
1902                                                            (Nat.S (Nat.S
1903                                                            (Nat.S (Nat.S
1904                                                            (Nat.S (Nat.S
1905                                                            (Nat.S (Nat.S
1906                                                            (Nat.S (Nat.S
1907                                                            (Nat.S (Nat.S
1908                                                            (Nat.S (Nat.S
1909                                                            (Nat.S (Nat.S
1910                                                            (Nat.S (Nat.S
1911                                                            (Nat.S (Nat.S
1912                                                            (Nat.S (Nat.S
1913                                                            (Nat.S (Nat.S
1914                                                            (Nat.S (Nat.S
1915                                                            (Nat.S (Nat.S
1916                                                            (Nat.S (Nat.S
1917                                                            (Nat.S (Nat.S
1918                                                            (Nat.S (Nat.S
1919                                                            (Nat.S (Nat.S
1920                                                            (Nat.S (Nat.S
1921                                                            (Nat.S (Nat.S
1922                                                            (Nat.S (Nat.S
1923                                                            (Nat.S (Nat.S
1924                                                            (Nat.S (Nat.S
1925                                                            (Nat.S (Nat.S
1926                                                            (Nat.S (Nat.S
1927                                                            (Nat.S (Nat.S
1928                                                            (Nat.S (Nat.S
1929                                                            (Nat.S (Nat.S
1930                                                            (Nat.S (Nat.S
1931                                                            (Nat.S (Nat.S
1932                                                            (Nat.S (Nat.S
1933                                                            (Nat.S (Nat.S
1934                                                            (Nat.S (Nat.S
1935                                                            (Nat.S (Nat.S
1936                                                            (Nat.S (Nat.S
1937                                                            (Nat.S (Nat.S
1938                                                            (Nat.S (Nat.S
1939                                                            (Nat.S (Nat.S
1940                                                            (Nat.S (Nat.S
1941                                                            (Nat.S (Nat.S
1942                                                            (Nat.S
1943                                                            Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1944                                                    | Bool.True ->
1945                                                      Types.Some (Types.Inl
1946                                                        SFR_TMOD)
1947                                                    | Bool.False ->
1948                                                      (match Nat.eqb address
1949                                                               (Nat.S (Nat.S
1950                                                               (Nat.S (Nat.S
1951                                                               (Nat.S (Nat.S
1952                                                               (Nat.S (Nat.S
1953                                                               (Nat.S (Nat.S
1954                                                               (Nat.S (Nat.S
1955                                                               (Nat.S (Nat.S
1956                                                               (Nat.S (Nat.S
1957                                                               (Nat.S (Nat.S
1958                                                               (Nat.S (Nat.S
1959                                                               (Nat.S (Nat.S
1960                                                               (Nat.S (Nat.S
1961                                                               (Nat.S (Nat.S
1962                                                               (Nat.S (Nat.S
1963                                                               (Nat.S (Nat.S
1964                                                               (Nat.S (Nat.S
1965                                                               (Nat.S (Nat.S
1966                                                               (Nat.S (Nat.S
1967                                                               (Nat.S (Nat.S
1968                                                               (Nat.S (Nat.S
1969                                                               (Nat.S (Nat.S
1970                                                               (Nat.S (Nat.S
1971                                                               (Nat.S (Nat.S
1972                                                               (Nat.S (Nat.S
1973                                                               (Nat.S (Nat.S
1974                                                               (Nat.S (Nat.S
1975                                                               (Nat.S (Nat.S
1976                                                               (Nat.S (Nat.S
1977                                                               (Nat.S (Nat.S
1978                                                               (Nat.S (Nat.S
1979                                                               (Nat.S (Nat.S
1980                                                               (Nat.S (Nat.S
1981                                                               (Nat.S (Nat.S
1982                                                               (Nat.S (Nat.S
1983                                                               (Nat.S (Nat.S
1984                                                               (Nat.S (Nat.S
1985                                                               (Nat.S (Nat.S
1986                                                               (Nat.S (Nat.S
1987                                                               (Nat.S (Nat.S
1988                                                               (Nat.S (Nat.S
1989                                                               (Nat.S (Nat.S
1990                                                               (Nat.S (Nat.S
1991                                                               (Nat.S (Nat.S
1992                                                               (Nat.S (Nat.S
1993                                                               (Nat.S (Nat.S
1994                                                               (Nat.S (Nat.S
1995                                                               (Nat.S (Nat.S
1996                                                               (Nat.S (Nat.S
1997                                                               (Nat.S (Nat.S
1998                                                               (Nat.S (Nat.S
1999                                                               (Nat.S (Nat.S
2000                                                               (Nat.S (Nat.S
2001                                                               (Nat.S (Nat.S
2002                                                               (Nat.S (Nat.S
2003                                                               (Nat.S (Nat.S
2004                                                               (Nat.S (Nat.S
2005                                                               (Nat.S (Nat.S
2006                                                               (Nat.S (Nat.S
2007                                                               (Nat.S (Nat.S
2008                                                               (Nat.S (Nat.S
2009                                                               (Nat.S (Nat.S
2010                                                               (Nat.S (Nat.S
2011                                                               (Nat.S (Nat.S
2012                                                               (Nat.S (Nat.S
2013                                                               (Nat.S (Nat.S
2014                                                               (Nat.S (Nat.S
2015                                                               (Nat.S (Nat.S
2016                                                               (Nat.S (Nat.S
2017                                                               (Nat.S (Nat.S
2018                                                               (Nat.S (Nat.S
2019                                                               (Nat.S (Nat.S
2020                                                               (Nat.S (Nat.S
2021                                                               (Nat.S (Nat.S
2022                                                               (Nat.S (Nat.S
2023                                                               (Nat.S (Nat.S
2024                                                               (Nat.S (Nat.S
2025                                                               Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2026                                                       | Bool.True ->
2027                                                         Types.Some (Types.Inl
2028                                                           SFR_SCON)
2029                                                       | Bool.False ->
2030                                                         (match Nat.eqb
2031                                                                  address
2032                                                                  (Nat.S
2033                                                                  (Nat.S
2034                                                                  (Nat.S
2035                                                                  (Nat.S
2036                                                                  (Nat.S
2037                                                                  (Nat.S
2038                                                                  (Nat.S
2039                                                                  (Nat.S
2040                                                                  (Nat.S
2041                                                                  (Nat.S
2042                                                                  (Nat.S
2043                                                                  (Nat.S
2044                                                                  (Nat.S
2045                                                                  (Nat.S
2046                                                                  (Nat.S
2047                                                                  (Nat.S
2048                                                                  (Nat.S
2049                                                                  (Nat.S
2050                                                                  (Nat.S
2051                                                                  (Nat.S
2052                                                                  (Nat.S
2053                                                                  (Nat.S
2054                                                                  (Nat.S
2055                                                                  (Nat.S
2056                                                                  (Nat.S
2057                                                                  (Nat.S
2058                                                                  (Nat.S
2059                                                                  (Nat.S
2060                                                                  (Nat.S
2061                                                                  (Nat.S
2062                                                                  (Nat.S
2063                                                                  (Nat.S
2064                                                                  (Nat.S
2065                                                                  (Nat.S
2066                                                                  (Nat.S
2067                                                                  (Nat.S
2068                                                                  (Nat.S
2069                                                                  (Nat.S
2070                                                                  (Nat.S
2071                                                                  (Nat.S
2072                                                                  (Nat.S
2073                                                                  (Nat.S
2074                                                                  (Nat.S
2075                                                                  (Nat.S
2076                                                                  (Nat.S
2077                                                                  (Nat.S
2078                                                                  (Nat.S
2079                                                                  (Nat.S
2080                                                                  (Nat.S
2081                                                                  (Nat.S
2082                                                                  (Nat.S
2083                                                                  (Nat.S
2084                                                                  (Nat.S
2085                                                                  (Nat.S
2086                                                                  (Nat.S
2087                                                                  (Nat.S
2088                                                                  (Nat.S
2089                                                                  (Nat.S
2090                                                                  (Nat.S
2091                                                                  (Nat.S
2092                                                                  (Nat.S
2093                                                                  (Nat.S
2094                                                                  (Nat.S
2095                                                                  (Nat.S
2096                                                                  (Nat.S
2097                                                                  (Nat.S
2098                                                                  (Nat.S
2099                                                                  (Nat.S
2100                                                                  (Nat.S
2101                                                                  (Nat.S
2102                                                                  (Nat.S
2103                                                                  (Nat.S
2104                                                                  (Nat.S
2105                                                                  (Nat.S
2106                                                                  (Nat.S
2107                                                                  (Nat.S
2108                                                                  (Nat.S
2109                                                                  (Nat.S
2110                                                                  (Nat.S
2111                                                                  (Nat.S
2112                                                                  (Nat.S
2113                                                                  (Nat.S
2114                                                                  (Nat.S
2115                                                                  (Nat.S
2116                                                                  (Nat.S
2117                                                                  (Nat.S
2118                                                                  (Nat.S
2119                                                                  (Nat.S
2120                                                                  (Nat.S
2121                                                                  (Nat.S
2122                                                                  (Nat.S
2123                                                                  (Nat.S
2124                                                                  (Nat.S
2125                                                                  (Nat.S
2126                                                                  (Nat.S
2127                                                                  (Nat.S
2128                                                                  (Nat.S
2129                                                                  (Nat.S
2130                                                                  (Nat.S
2131                                                                  (Nat.S
2132                                                                  (Nat.S
2133                                                                  (Nat.S
2134                                                                  (Nat.S
2135                                                                  (Nat.S
2136                                                                  (Nat.S
2137                                                                  (Nat.S
2138                                                                  (Nat.S
2139                                                                  (Nat.S
2140                                                                  (Nat.S
2141                                                                  (Nat.S
2142                                                                  (Nat.S
2143                                                                  (Nat.S
2144                                                                  (Nat.S
2145                                                                  (Nat.S
2146                                                                  (Nat.S
2147                                                                  (Nat.S
2148                                                                  (Nat.S
2149                                                                  (Nat.S
2150                                                                  (Nat.S
2151                                                                  (Nat.S
2152                                                                  (Nat.S
2153                                                                  (Nat.S
2154                                                                  (Nat.S
2155                                                                  (Nat.S
2156                                                                  (Nat.S
2157                                                                  (Nat.S
2158                                                                  (Nat.S
2159                                                                  (Nat.S
2160                                                                  (Nat.S
2161                                                                  (Nat.S
2162                                                                  (Nat.S
2163                                                                  (Nat.S
2164                                                                  (Nat.S
2165                                                                  (Nat.S
2166                                                                  (Nat.S
2167                                                                  (Nat.S
2168                                                                  (Nat.S
2169                                                                  (Nat.S
2170                                                                  (Nat.S
2171                                                                  (Nat.S
2172                                                                  (Nat.S
2173                                                                  (Nat.S
2174                                                                  (Nat.S
2175                                                                  (Nat.S
2176                                                                  (Nat.S
2177                                                                  (Nat.S
2178                                                                  (Nat.S
2179                                                                  (Nat.S
2180                                                                  (Nat.S
2181                                                                  (Nat.S
2182                                                                  (Nat.S
2183                                                                  (Nat.S
2184                                                                  (Nat.S
2185                                                                  (Nat.S
2186                                                                  (Nat.S
2187                                                                  (Nat.S
2188                                                                  (Nat.S
2189                                                                  (Nat.S
2190                                                                  (Nat.S
2191                                                                  (Nat.S
2192                                                                  (Nat.S
2193                                                                  (Nat.S
2194                                                                  (Nat.S
2195                                                                  (Nat.S
2196                                                                  (Nat.S
2197                                                                  (Nat.S
2198                                                                  (Nat.S
2199                                                                  (Nat.S
2200                                                                  Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2201                                                          | Bool.True ->
2202                                                            Types.Some
2203                                                              (Types.Inl
2204                                                              SFR_IE)
2205                                                          | Bool.False ->
2206                                                            (match Nat.eqb
2207                                                                     address
2208                                                                     (Nat.S
2209                                                                     (Nat.S
2210                                                                     (Nat.S
2211                                                                     (Nat.S
2212                                                                     (Nat.S
2213                                                                     (Nat.S
2214                                                                     (Nat.S
2215                                                                     (Nat.S
2216                                                                     (Nat.S
2217                                                                     (Nat.S
2218                                                                     (Nat.S
2219                                                                     (Nat.S
2220                                                                     (Nat.S
2221                                                                     (Nat.S
2222                                                                     (Nat.S
2223                                                                     (Nat.S
2224                                                                     (Nat.S
2225                                                                     (Nat.S
2226                                                                     (Nat.S
2227                                                                     (Nat.S
2228                                                                     (Nat.S
2229                                                                     (Nat.S
2230                                                                     (Nat.S
2231                                                                     (Nat.S
2232                                                                     (Nat.S
2233                                                                     (Nat.S
2234                                                                     (Nat.S
2235                                                                     (Nat.S
2236                                                                     (Nat.S
2237                                                                     (Nat.S
2238                                                                     (Nat.S
2239                                                                     (Nat.S
2240                                                                     (Nat.S
2241                                                                     (Nat.S
2242                                                                     (Nat.S
2243                                                                     (Nat.S
2244                                                                     (Nat.S
2245                                                                     (Nat.S
2246                                                                     (Nat.S
2247                                                                     (Nat.S
2248                                                                     (Nat.S
2249                                                                     (Nat.S
2250                                                                     (Nat.S
2251                                                                     (Nat.S
2252                                                                     (Nat.S
2253                                                                     (Nat.S
2254                                                                     (Nat.S
2255                                                                     (Nat.S
2256                                                                     (Nat.S
2257                                                                     (Nat.S
2258                                                                     (Nat.S
2259                                                                     (Nat.S
2260                                                                     (Nat.S
2261                                                                     (Nat.S
2262                                                                     (Nat.S
2263                                                                     (Nat.S
2264                                                                     (Nat.S
2265                                                                     (Nat.S
2266                                                                     (Nat.S
2267                                                                     (Nat.S
2268                                                                     (Nat.S
2269                                                                     (Nat.S
2270                                                                     (Nat.S
2271                                                                     (Nat.S
2272                                                                     (Nat.S
2273                                                                     (Nat.S
2274                                                                     (Nat.S
2275                                                                     (Nat.S
2276                                                                     (Nat.S
2277                                                                     (Nat.S
2278                                                                     (Nat.S
2279                                                                     (Nat.S
2280                                                                     (Nat.S
2281                                                                     (Nat.S
2282                                                                     (Nat.S
2283                                                                     (Nat.S
2284                                                                     (Nat.S
2285                                                                     (Nat.S
2286                                                                     (Nat.S
2287                                                                     (Nat.S
2288                                                                     (Nat.S
2289                                                                     (Nat.S
2290                                                                     (Nat.S
2291                                                                     (Nat.S
2292                                                                     (Nat.S
2293                                                                     (Nat.S
2294                                                                     (Nat.S
2295                                                                     (Nat.S
2296                                                                     (Nat.S
2297                                                                     (Nat.S
2298                                                                     (Nat.S
2299                                                                     (Nat.S
2300                                                                     (Nat.S
2301                                                                     (Nat.S
2302                                                                     (Nat.S
2303                                                                     (Nat.S
2304                                                                     (Nat.S
2305                                                                     (Nat.S
2306                                                                     (Nat.S
2307                                                                     (Nat.S
2308                                                                     (Nat.S
2309                                                                     (Nat.S
2310                                                                     (Nat.S
2311                                                                     (Nat.S
2312                                                                     (Nat.S
2313                                                                     (Nat.S
2314                                                                     (Nat.S
2315                                                                     (Nat.S
2316                                                                     (Nat.S
2317                                                                     (Nat.S
2318                                                                     (Nat.S
2319                                                                     (Nat.S
2320                                                                     (Nat.S
2321                                                                     (Nat.S
2322                                                                     (Nat.S
2323                                                                     (Nat.S
2324                                                                     (Nat.S
2325                                                                     (Nat.S
2326                                                                     (Nat.S
2327                                                                     (Nat.S
2328                                                                     (Nat.S
2329                                                                     (Nat.S
2330                                                                     (Nat.S
2331                                                                     (Nat.S
2332                                                                     (Nat.S
2333                                                                     (Nat.S
2334                                                                     (Nat.S
2335                                                                     (Nat.S
2336                                                                     (Nat.S
2337                                                                     (Nat.S
2338                                                                     (Nat.S
2339                                                                     (Nat.S
2340                                                                     (Nat.S
2341                                                                     (Nat.S
2342                                                                     (Nat.S
2343                                                                     (Nat.S
2344                                                                     (Nat.S
2345                                                                     (Nat.S
2346                                                                     (Nat.S
2347                                                                     (Nat.S
2348                                                                     (Nat.S
2349                                                                     (Nat.S
2350                                                                     (Nat.S
2351                                                                     (Nat.S
2352                                                                     (Nat.S
2353                                                                     (Nat.S
2354                                                                     (Nat.S
2355                                                                     (Nat.S
2356                                                                     (Nat.S
2357                                                                     (Nat.S
2358                                                                     (Nat.S
2359                                                                     (Nat.S
2360                                                                     (Nat.S
2361                                                                     (Nat.S
2362                                                                     (Nat.S
2363                                                                     (Nat.S
2364                                                                     (Nat.S
2365                                                                     (Nat.S
2366                                                                     (Nat.S
2367                                                                     (Nat.S
2368                                                                     (Nat.S
2369                                                                     (Nat.S
2370                                                                     (Nat.S
2371                                                                     (Nat.S
2372                                                                     (Nat.S
2373                                                                     (Nat.S
2374                                                                     (Nat.S
2375                                                                     (Nat.S
2376                                                                     (Nat.S
2377                                                                     (Nat.S
2378                                                                     (Nat.S
2379                                                                     (Nat.S
2380                                                                     (Nat.S
2381                                                                     (Nat.S
2382                                                                     (Nat.S
2383                                                                     (Nat.S
2384                                                                     (Nat.S
2385                                                                     (Nat.S
2386                                                                     (Nat.S
2387                                                                     (Nat.S
2388                                                                     (Nat.S
2389                                                                     (Nat.S
2390                                                                     (Nat.S
2391                                                                     (Nat.S
2392                                                                     Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2393                                                             | Bool.True ->
2394                                                               Types.Some
2395                                                                 (Types.Inl
2396                                                                 SFR_IP)
2397                                                             | Bool.False ->
2398                                                               (match
2399                                                                Nat.eqb
2400                                                                  address
2401                                                                  (Nat.S
2402                                                                  (Nat.S
2403                                                                  (Nat.S
2404                                                                  (Nat.S
2405                                                                  (Nat.S
2406                                                                  (Nat.S
2407                                                                  (Nat.S
2408                                                                  (Nat.S
2409                                                                  (Nat.S
2410                                                                  (Nat.S
2411                                                                  (Nat.S
2412                                                                  (Nat.S
2413                                                                  (Nat.S
2414                                                                  (Nat.S
2415                                                                  (Nat.S
2416                                                                  (Nat.S
2417                                                                  (Nat.S
2418                                                                  (Nat.S
2419                                                                  (Nat.S
2420                                                                  (Nat.S
2421                                                                  (Nat.S
2422                                                                  (Nat.S
2423                                                                  (Nat.S
2424                                                                  (Nat.S
2425                                                                  (Nat.S
2426                                                                  (Nat.S
2427                                                                  (Nat.S
2428                                                                  (Nat.S
2429                                                                  (Nat.S
2430                                                                  (Nat.S
2431                                                                  (Nat.S
2432                                                                  (Nat.S
2433                                                                  (Nat.S
2434                                                                  (Nat.S
2435                                                                  (Nat.S
2436                                                                  (Nat.S
2437                                                                  (Nat.S
2438                                                                  (Nat.S
2439                                                                  (Nat.S
2440                                                                  (Nat.S
2441                                                                  (Nat.S
2442                                                                  (Nat.S
2443                                                                  (Nat.S
2444                                                                  (Nat.S
2445                                                                  (Nat.S
2446                                                                  (Nat.S
2447                                                                  (Nat.S
2448                                                                  (Nat.S
2449                                                                  (Nat.S
2450                                                                  (Nat.S
2451                                                                  (Nat.S
2452                                                                  (Nat.S
2453                                                                  (Nat.S
2454                                                                  (Nat.S
2455                                                                  (Nat.S
2456                                                                  (Nat.S
2457                                                                  (Nat.S
2458                                                                  (Nat.S
2459                                                                  (Nat.S
2460                                                                  (Nat.S
2461                                                                  (Nat.S
2462                                                                  (Nat.S
2463                                                                  (Nat.S
2464                                                                  (Nat.S
2465                                                                  (Nat.S
2466                                                                  (Nat.S
2467                                                                  (Nat.S
2468                                                                  (Nat.S
2469                                                                  (Nat.S
2470                                                                  (Nat.S
2471                                                                  (Nat.S
2472                                                                  (Nat.S
2473                                                                  (Nat.S
2474                                                                  (Nat.S
2475                                                                  (Nat.S
2476                                                                  (Nat.S
2477                                                                  (Nat.S
2478                                                                  (Nat.S
2479                                                                  (Nat.S
2480                                                                  (Nat.S
2481                                                                  (Nat.S
2482                                                                  (Nat.S
2483                                                                  (Nat.S
2484                                                                  (Nat.S
2485                                                                  (Nat.S
2486                                                                  (Nat.S
2487                                                                  (Nat.S
2488                                                                  (Nat.S
2489                                                                  (Nat.S
2490                                                                  (Nat.S
2491                                                                  (Nat.S
2492                                                                  (Nat.S
2493                                                                  (Nat.S
2494                                                                  (Nat.S
2495                                                                  (Nat.S
2496                                                                  (Nat.S
2497                                                                  (Nat.S
2498                                                                  (Nat.S
2499                                                                  (Nat.S
2500                                                                  (Nat.S
2501                                                                  (Nat.S
2502                                                                  (Nat.S
2503                                                                  (Nat.S
2504                                                                  (Nat.S
2505                                                                  (Nat.S
2506                                                                  (Nat.S
2507                                                                  (Nat.S
2508                                                                  (Nat.S
2509                                                                  (Nat.S
2510                                                                  (Nat.S
2511                                                                  (Nat.S
2512                                                                  (Nat.S
2513                                                                  (Nat.S
2514                                                                  (Nat.S
2515                                                                  (Nat.S
2516                                                                  (Nat.S
2517                                                                  (Nat.S
2518                                                                  (Nat.S
2519                                                                  (Nat.S
2520                                                                  (Nat.S
2521                                                                  (Nat.S
2522                                                                  (Nat.S
2523                                                                  (Nat.S
2524                                                                  (Nat.S
2525                                                                  (Nat.S
2526                                                                  (Nat.S
2527                                                                  (Nat.S
2528                                                                  (Nat.S
2529                                                                  (Nat.S
2530                                                                  Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2531                                                                | Bool.True ->
2532                                                                  Types.Some
2533                                                                    (Types.Inl
2534                                                                    SFR_SP)
2535                                                                | Bool.False ->
2536                                                                  (match
2537                                                                   Nat.eqb
2538                                                                     address
2539                                                                     (Nat.S
2540                                                                     (Nat.S
2541                                                                     (Nat.S
2542                                                                     (Nat.S
2543                                                                     (Nat.S
2544                                                                     (Nat.S
2545                                                                     (Nat.S
2546                                                                     (Nat.S
2547                                                                     (Nat.S
2548                                                                     (Nat.S
2549                                                                     (Nat.S
2550                                                                     (Nat.S
2551                                                                     (Nat.S
2552                                                                     (Nat.S
2553                                                                     (Nat.S
2554                                                                     (Nat.S
2555                                                                     (Nat.S
2556                                                                     (Nat.S
2557                                                                     (Nat.S
2558                                                                     (Nat.S
2559                                                                     (Nat.S
2560                                                                     (Nat.S
2561                                                                     (Nat.S
2562                                                                     (Nat.S
2563                                                                     (Nat.S
2564                                                                     (Nat.S
2565                                                                     (Nat.S
2566                                                                     (Nat.S
2567                                                                     (Nat.S
2568                                                                     (Nat.S
2569                                                                     (Nat.S
2570                                                                     (Nat.S
2571                                                                     (Nat.S
2572                                                                     (Nat.S
2573                                                                     (Nat.S
2574                                                                     (Nat.S
2575                                                                     (Nat.S
2576                                                                     (Nat.S
2577                                                                     (Nat.S
2578                                                                     (Nat.S
2579                                                                     (Nat.S
2580                                                                     (Nat.S
2581                                                                     (Nat.S
2582                                                                     (Nat.S
2583                                                                     (Nat.S
2584                                                                     (Nat.S
2585                                                                     (Nat.S
2586                                                                     (Nat.S
2587                                                                     (Nat.S
2588                                                                     (Nat.S
2589                                                                     (Nat.S
2590                                                                     (Nat.S
2591                                                                     (Nat.S
2592                                                                     (Nat.S
2593                                                                     (Nat.S
2594                                                                     (Nat.S
2595                                                                     (Nat.S
2596                                                                     (Nat.S
2597                                                                     (Nat.S
2598                                                                     (Nat.S
2599                                                                     (Nat.S
2600                                                                     (Nat.S
2601                                                                     (Nat.S
2602                                                                     (Nat.S
2603                                                                     (Nat.S
2604                                                                     (Nat.S
2605                                                                     (Nat.S
2606                                                                     (Nat.S
2607                                                                     (Nat.S
2608                                                                     (Nat.S
2609                                                                     (Nat.S
2610                                                                     (Nat.S
2611                                                                     (Nat.S
2612                                                                     (Nat.S
2613                                                                     (Nat.S
2614                                                                     (Nat.S
2615                                                                     (Nat.S
2616                                                                     (Nat.S
2617                                                                     (Nat.S
2618                                                                     (Nat.S
2619                                                                     (Nat.S
2620                                                                     (Nat.S
2621                                                                     (Nat.S
2622                                                                     (Nat.S
2623                                                                     (Nat.S
2624                                                                     (Nat.S
2625                                                                     (Nat.S
2626                                                                     (Nat.S
2627                                                                     (Nat.S
2628                                                                     (Nat.S
2629                                                                     (Nat.S
2630                                                                     (Nat.S
2631                                                                     (Nat.S
2632                                                                     (Nat.S
2633                                                                     (Nat.S
2634                                                                     (Nat.S
2635                                                                     (Nat.S
2636                                                                     (Nat.S
2637                                                                     (Nat.S
2638                                                                     (Nat.S
2639                                                                     (Nat.S
2640                                                                     (Nat.S
2641                                                                     (Nat.S
2642                                                                     (Nat.S
2643                                                                     (Nat.S
2644                                                                     (Nat.S
2645                                                                     (Nat.S
2646                                                                     (Nat.S
2647                                                                     (Nat.S
2648                                                                     (Nat.S
2649                                                                     (Nat.S
2650                                                                     (Nat.S
2651                                                                     (Nat.S
2652                                                                     (Nat.S
2653                                                                     (Nat.S
2654                                                                     (Nat.S
2655                                                                     (Nat.S
2656                                                                     (Nat.S
2657                                                                     (Nat.S
2658                                                                     (Nat.S
2659                                                                     (Nat.S
2660                                                                     (Nat.S
2661                                                                     (Nat.S
2662                                                                     (Nat.S
2663                                                                     (Nat.S
2664                                                                     (Nat.S
2665                                                                     (Nat.S
2666                                                                     (Nat.S
2667                                                                     (Nat.S
2668                                                                     (Nat.S
2669                                                                     Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2670                                                                   | Bool.True ->
2671                                                                     Types.Some
2672                                                                     (Types.Inl
2673                                                                     SFR_DPL)
2674                                                                   | Bool.False ->
2675                                                                     (match
2676                                                                     Nat.eqb
2677                                                                     address
2678                                                                     (Nat.S
2679                                                                     (Nat.S
2680                                                                     (Nat.S
2681                                                                     (Nat.S
2682                                                                     (Nat.S
2683                                                                     (Nat.S
2684                                                                     (Nat.S
2685                                                                     (Nat.S
2686                                                                     (Nat.S
2687                                                                     (Nat.S
2688                                                                     (Nat.S
2689                                                                     (Nat.S
2690                                                                     (Nat.S
2691                                                                     (Nat.S
2692                                                                     (Nat.S
2693                                                                     (Nat.S
2694                                                                     (Nat.S
2695                                                                     (Nat.S
2696                                                                     (Nat.S
2697                                                                     (Nat.S
2698                                                                     (Nat.S
2699                                                                     (Nat.S
2700                                                                     (Nat.S
2701                                                                     (Nat.S
2702                                                                     (Nat.S
2703                                                                     (Nat.S
2704                                                                     (Nat.S
2705                                                                     (Nat.S
2706                                                                     (Nat.S
2707                                                                     (Nat.S
2708                                                                     (Nat.S
2709                                                                     (Nat.S
2710                                                                     (Nat.S
2711                                                                     (Nat.S
2712                                                                     (Nat.S
2713                                                                     (Nat.S
2714                                                                     (Nat.S
2715                                                                     (Nat.S
2716                                                                     (Nat.S
2717                                                                     (Nat.S
2718                                                                     (Nat.S
2719                                                                     (Nat.S
2720                                                                     (Nat.S
2721                                                                     (Nat.S
2722                                                                     (Nat.S
2723                                                                     (Nat.S
2724                                                                     (Nat.S
2725                                                                     (Nat.S
2726                                                                     (Nat.S
2727                                                                     (Nat.S
2728                                                                     (Nat.S
2729                                                                     (Nat.S
2730                                                                     (Nat.S
2731                                                                     (Nat.S
2732                                                                     (Nat.S
2733                                                                     (Nat.S
2734                                                                     (Nat.S
2735                                                                     (Nat.S
2736                                                                     (Nat.S
2737                                                                     (Nat.S
2738                                                                     (Nat.S
2739                                                                     (Nat.S
2740                                                                     (Nat.S
2741                                                                     (Nat.S
2742                                                                     (Nat.S
2743                                                                     (Nat.S
2744                                                                     (Nat.S
2745                                                                     (Nat.S
2746                                                                     (Nat.S
2747                                                                     (Nat.S
2748                                                                     (Nat.S
2749                                                                     (Nat.S
2750                                                                     (Nat.S
2751                                                                     (Nat.S
2752                                                                     (Nat.S
2753                                                                     (Nat.S
2754                                                                     (Nat.S
2755                                                                     (Nat.S
2756                                                                     (Nat.S
2757                                                                     (Nat.S
2758                                                                     (Nat.S
2759                                                                     (Nat.S
2760                                                                     (Nat.S
2761                                                                     (Nat.S
2762                                                                     (Nat.S
2763                                                                     (Nat.S
2764                                                                     (Nat.S
2765                                                                     (Nat.S
2766                                                                     (Nat.S
2767                                                                     (Nat.S
2768                                                                     (Nat.S
2769                                                                     (Nat.S
2770                                                                     (Nat.S
2771                                                                     (Nat.S
2772                                                                     (Nat.S
2773                                                                     (Nat.S
2774                                                                     (Nat.S
2775                                                                     (Nat.S
2776                                                                     (Nat.S
2777                                                                     (Nat.S
2778                                                                     (Nat.S
2779                                                                     (Nat.S
2780                                                                     (Nat.S
2781                                                                     (Nat.S
2782                                                                     (Nat.S
2783                                                                     (Nat.S
2784                                                                     (Nat.S
2785                                                                     (Nat.S
2786                                                                     (Nat.S
2787                                                                     (Nat.S
2788                                                                     (Nat.S
2789                                                                     (Nat.S
2790                                                                     (Nat.S
2791                                                                     (Nat.S
2792                                                                     (Nat.S
2793                                                                     (Nat.S
2794                                                                     (Nat.S
2795                                                                     (Nat.S
2796                                                                     (Nat.S
2797                                                                     (Nat.S
2798                                                                     (Nat.S
2799                                                                     (Nat.S
2800                                                                     (Nat.S
2801                                                                     (Nat.S
2802                                                                     (Nat.S
2803                                                                     (Nat.S
2804                                                                     (Nat.S
2805                                                                     (Nat.S
2806                                                                     (Nat.S
2807                                                                     (Nat.S
2808                                                                     (Nat.S
2809                                                                     Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2810                                                                     | Bool.True ->
2811                                                                     Types.Some
2812                                                                     (Types.Inl
2813                                                                     SFR_DPH)
2814                                                                     | Bool.False ->
2815                                                                     (match
2816                                                                     Nat.eqb
2817                                                                     address
2818                                                                     (Nat.S
2819                                                                     (Nat.S
2820                                                                     (Nat.S
2821                                                                     (Nat.S
2822                                                                     (Nat.S
2823                                                                     (Nat.S
2824                                                                     (Nat.S
2825                                                                     (Nat.S
2826                                                                     (Nat.S
2827                                                                     (Nat.S
2828                                                                     (Nat.S
2829                                                                     (Nat.S
2830                                                                     (Nat.S
2831                                                                     (Nat.S
2832                                                                     (Nat.S
2833                                                                     (Nat.S
2834                                                                     (Nat.S
2835                                                                     (Nat.S
2836                                                                     (Nat.S
2837                                                                     (Nat.S
2838                                                                     (Nat.S
2839                                                                     (Nat.S
2840                                                                     (Nat.S
2841                                                                     (Nat.S
2842                                                                     (Nat.S
2843                                                                     (Nat.S
2844                                                                     (Nat.S
2845                                                                     (Nat.S
2846                                                                     (Nat.S
2847                                                                     (Nat.S
2848                                                                     (Nat.S
2849                                                                     (Nat.S
2850                                                                     (Nat.S
2851                                                                     (Nat.S
2852                                                                     (Nat.S
2853                                                                     (Nat.S
2854                                                                     (Nat.S
2855                                                                     (Nat.S
2856                                                                     (Nat.S
2857                                                                     (Nat.S
2858                                                                     (Nat.S
2859                                                                     (Nat.S
2860                                                                     (Nat.S
2861                                                                     (Nat.S
2862                                                                     (Nat.S
2863                                                                     (Nat.S
2864                                                                     (Nat.S
2865                                                                     (Nat.S
2866                                                                     (Nat.S
2867                                                                     (Nat.S
2868                                                                     (Nat.S
2869                                                                     (Nat.S
2870                                                                     (Nat.S
2871                                                                     (Nat.S
2872                                                                     (Nat.S
2873                                                                     (Nat.S
2874                                                                     (Nat.S
2875                                                                     (Nat.S
2876                                                                     (Nat.S
2877                                                                     (Nat.S
2878                                                                     (Nat.S
2879                                                                     (Nat.S
2880                                                                     (Nat.S
2881                                                                     (Nat.S
2882                                                                     (Nat.S
2883                                                                     (Nat.S
2884                                                                     (Nat.S
2885                                                                     (Nat.S
2886                                                                     (Nat.S
2887                                                                     (Nat.S
2888                                                                     (Nat.S
2889                                                                     (Nat.S
2890                                                                     (Nat.S
2891                                                                     (Nat.S
2892                                                                     (Nat.S
2893                                                                     (Nat.S
2894                                                                     (Nat.S
2895                                                                     (Nat.S
2896                                                                     (Nat.S
2897                                                                     (Nat.S
2898                                                                     (Nat.S
2899                                                                     (Nat.S
2900                                                                     (Nat.S
2901                                                                     (Nat.S
2902                                                                     (Nat.S
2903                                                                     (Nat.S
2904                                                                     (Nat.S
2905                                                                     (Nat.S
2906                                                                     (Nat.S
2907                                                                     (Nat.S
2908                                                                     (Nat.S
2909                                                                     (Nat.S
2910                                                                     (Nat.S
2911                                                                     (Nat.S
2912                                                                     (Nat.S
2913                                                                     (Nat.S
2914                                                                     (Nat.S
2915                                                                     (Nat.S
2916                                                                     (Nat.S
2917                                                                     (Nat.S
2918                                                                     (Nat.S
2919                                                                     (Nat.S
2920                                                                     (Nat.S
2921                                                                     (Nat.S
2922                                                                     (Nat.S
2923                                                                     (Nat.S
2924                                                                     (Nat.S
2925                                                                     (Nat.S
2926                                                                     (Nat.S
2927                                                                     (Nat.S
2928                                                                     (Nat.S
2929                                                                     (Nat.S
2930                                                                     (Nat.S
2931                                                                     (Nat.S
2932                                                                     (Nat.S
2933                                                                     (Nat.S
2934                                                                     (Nat.S
2935                                                                     (Nat.S
2936                                                                     (Nat.S
2937                                                                     (Nat.S
2938                                                                     (Nat.S
2939                                                                     (Nat.S
2940                                                                     (Nat.S
2941                                                                     (Nat.S
2942                                                                     (Nat.S
2943                                                                     (Nat.S
2944                                                                     (Nat.S
2945                                                                     (Nat.S
2946                                                                     (Nat.S
2947                                                                     (Nat.S
2948                                                                     (Nat.S
2949                                                                     (Nat.S
2950                                                                     (Nat.S
2951                                                                     (Nat.S
2952                                                                     (Nat.S
2953                                                                     (Nat.S
2954                                                                     (Nat.S
2955                                                                     (Nat.S
2956                                                                     (Nat.S
2957                                                                     (Nat.S
2958                                                                     (Nat.S
2959                                                                     (Nat.S
2960                                                                     (Nat.S
2961                                                                     (Nat.S
2962                                                                     (Nat.S
2963                                                                     (Nat.S
2964                                                                     (Nat.S
2965                                                                     (Nat.S
2966                                                                     (Nat.S
2967                                                                     (Nat.S
2968                                                                     (Nat.S
2969                                                                     (Nat.S
2970                                                                     (Nat.S
2971                                                                     (Nat.S
2972                                                                     (Nat.S
2973                                                                     (Nat.S
2974                                                                     (Nat.S
2975                                                                     (Nat.S
2976                                                                     (Nat.S
2977                                                                     (Nat.S
2978                                                                     (Nat.S
2979                                                                     (Nat.S
2980                                                                     (Nat.S
2981                                                                     (Nat.S
2982                                                                     (Nat.S
2983                                                                     (Nat.S
2984                                                                     (Nat.S
2985                                                                     (Nat.S
2986                                                                     (Nat.S
2987                                                                     (Nat.S
2988                                                                     (Nat.S
2989                                                                     (Nat.S
2990                                                                     (Nat.S
2991                                                                     (Nat.S
2992                                                                     (Nat.S
2993                                                                     (Nat.S
2994                                                                     (Nat.S
2995                                                                     (Nat.S
2996                                                                     (Nat.S
2997                                                                     (Nat.S
2998                                                                     (Nat.S
2999                                                                     (Nat.S
3000                                                                     (Nat.S
3001                                                                     (Nat.S
3002                                                                     (Nat.S
3003                                                                     (Nat.S
3004                                                                     (Nat.S
3005                                                                     (Nat.S
3006                                                                     (Nat.S
3007                                                                     (Nat.S
3008                                                                     (Nat.S
3009                                                                     (Nat.S
3010                                                                     (Nat.S
3011                                                                     (Nat.S
3012                                                                     (Nat.S
3013                                                                     (Nat.S
3014                                                                     (Nat.S
3015                                                                     (Nat.S
3016                                                                     (Nat.S
3017                                                                     (Nat.S
3018                                                                     (Nat.S
3019                                                                     (Nat.S
3020                                                                     (Nat.S
3021                                                                     (Nat.S
3022                                                                     (Nat.S
3023                                                                     (Nat.S
3024                                                                     (Nat.S
3025                                                                     (Nat.S
3026                                                                     Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
3027                                                                     | Bool.True ->
3028                                                                     Types.Some
3029                                                                     (Types.Inl
3030                                                                     SFR_PSW)
3031                                                                     | Bool.False ->
3032                                                                     (match
3033                                                                     Nat.eqb
3034                                                                     address
3035                                                                     (Nat.S
3036                                                                     (Nat.S
3037                                                                     (Nat.S
3038                                                                     (Nat.S
3039                                                                     (Nat.S
3040                                                                     (Nat.S
3041                                                                     (Nat.S
3042                                                                     (Nat.S
3043                                                                     (Nat.S
3044                                                                     (Nat.S
3045                                                                     (Nat.S
3046                                                                     (Nat.S
3047                                                                     (Nat.S
3048                                                                     (Nat.S
3049                                                                     (Nat.S
3050                                                                     (Nat.S
3051                                                                     (Nat.S
3052                                                                     (Nat.S
3053                                                                     (Nat.S
3054                                                                     (Nat.S
3055                                                                     (Nat.S
3056                                                                     (Nat.S
3057                                                                     (Nat.S
3058                                                                     (Nat.S
3059                                                                     (Nat.S
3060                                                                     (Nat.S
3061                                                                     (Nat.S
3062                                                                     (Nat.S
3063                                                                     (Nat.S
3064                                                                     (Nat.S
3065                                                                     (Nat.S
3066                                                                     (Nat.S
3067                                                                     (Nat.S
3068                                                                     (Nat.S
3069                                                                     (Nat.S
3070                                                                     (Nat.S
3071                                                                     (Nat.S
3072                                                                     (Nat.S
3073                                                                     (Nat.S
3074                                                                     (Nat.S
3075                                                                     (Nat.S
3076                                                                     (Nat.S
3077                                                                     (Nat.S
3078                                                                     (Nat.S
3079                                                                     (Nat.S
3080                                                                     (Nat.S
3081                                                                     (Nat.S
3082                                                                     (Nat.S
3083                                                                     (Nat.S
3084                                                                     (Nat.S
3085                                                                     (Nat.S
3086                                                                     (Nat.S
3087                                                                     (Nat.S
3088                                                                     (Nat.S
3089                                                                     (Nat.S
3090                                                                     (Nat.S
3091                                                                     (Nat.S
3092                                                                     (Nat.S
3093                                                                     (Nat.S
3094                                                                     (Nat.S
3095                                                                     (Nat.S
3096                                                                     (Nat.S
3097                                                                     (Nat.S
3098                                                                     (Nat.S
3099                                                                     (Nat.S
3100                                                                     (Nat.S
3101                                                                     (Nat.S
3102                                                                     (Nat.S
3103                                                                     (Nat.S
3104                                                                     (Nat.S
3105                                                                     (Nat.S
3106                                                                     (Nat.S
3107                                                                     (Nat.S
3108                                                                     (Nat.S
3109                                                                     (Nat.S
3110                                                                     (Nat.S
3111                                                                     (Nat.S
3112                                                                     (Nat.S
3113                                                                     (Nat.S
3114                                                                     (Nat.S
3115                                                                     (Nat.S
3116                                                                     (Nat.S
3117                                                                     (Nat.S
3118                                                                     (Nat.S
3119                                                                     (Nat.S
3120                                                                     (Nat.S
3121                                                                     (Nat.S
3122                                                                     (Nat.S
3123                                                                     (Nat.S
3124                                                                     (Nat.S
3125                                                                     (Nat.S
3126                                                                     (Nat.S
3127                                                                     (Nat.S
3128                                                                     (Nat.S
3129                                                                     (Nat.S
3130                                                                     (Nat.S
3131                                                                     (Nat.S
3132                                                                     (Nat.S
3133                                                                     (Nat.S
3134                                                                     (Nat.S
3135                                                                     (Nat.S
3136                                                                     (Nat.S
3137                                                                     (Nat.S
3138                                                                     (Nat.S
3139                                                                     (Nat.S
3140                                                                     (Nat.S
3141                                                                     (Nat.S
3142                                                                     (Nat.S
3143                                                                     (Nat.S
3144                                                                     (Nat.S
3145                                                                     (Nat.S
3146                                                                     (Nat.S
3147                                                                     (Nat.S
3148                                                                     (Nat.S
3149                                                                     (Nat.S
3150                                                                     (Nat.S
3151                                                                     (Nat.S
3152                                                                     (Nat.S
3153                                                                     (Nat.S
3154                                                                     (Nat.S
3155                                                                     (Nat.S
3156                                                                     (Nat.S
3157                                                                     (Nat.S
3158                                                                     (Nat.S
3159                                                                     (Nat.S
3160                                                                     (Nat.S
3161                                                                     (Nat.S
3162                                                                     (Nat.S
3163                                                                     (Nat.S
3164                                                                     (Nat.S
3165                                                                     (Nat.S
3166                                                                     (Nat.S
3167                                                                     (Nat.S
3168                                                                     (Nat.S
3169                                                                     (Nat.S
3170                                                                     (Nat.S
3171                                                                     (Nat.S
3172                                                                     (Nat.S
3173                                                                     (Nat.S
3174                                                                     (Nat.S
3175                                                                     (Nat.S
3176                                                                     (Nat.S
3177                                                                     (Nat.S
3178                                                                     (Nat.S
3179                                                                     (Nat.S
3180                                                                     (Nat.S
3181                                                                     (Nat.S
3182                                                                     (Nat.S
3183                                                                     (Nat.S
3184                                                                     (Nat.S
3185                                                                     (Nat.S
3186                                                                     (Nat.S
3187                                                                     (Nat.S
3188                                                                     (Nat.S
3189                                                                     (Nat.S
3190                                                                     (Nat.S
3191                                                                     (Nat.S
3192                                                                     (Nat.S
3193                                                                     (Nat.S
3194                                                                     (Nat.S
3195                                                                     (Nat.S
3196                                                                     (Nat.S
3197                                                                     (Nat.S
3198                                                                     (Nat.S
3199                                                                     (Nat.S
3200                                                                     (Nat.S
3201                                                                     (Nat.S
3202                                                                     (Nat.S
3203                                                                     (Nat.S
3204                                                                     (Nat.S
3205                                                                     (Nat.S
3206                                                                     (Nat.S
3207                                                                     (Nat.S
3208                                                                     (Nat.S
3209                                                                     (Nat.S
3210                                                                     (Nat.S
3211                                                                     (Nat.S
3212                                                                     (Nat.S
3213                                                                     (Nat.S
3214                                                                     (Nat.S
3215                                                                     (Nat.S
3216                                                                     (Nat.S
3217                                                                     (Nat.S
3218                                                                     (Nat.S
3219                                                                     (Nat.S
3220                                                                     (Nat.S
3221                                                                     (Nat.S
3222                                                                     (Nat.S
3223                                                                     (Nat.S
3224                                                                     (Nat.S
3225                                                                     (Nat.S
3226                                                                     (Nat.S
3227                                                                     (Nat.S
3228                                                                     (Nat.S
3229                                                                     (Nat.S
3230                                                                     (Nat.S
3231                                                                     (Nat.S
3232                                                                     (Nat.S
3233                                                                     (Nat.S
3234                                                                     (Nat.S
3235                                                                     (Nat.S
3236                                                                     (Nat.S
3237                                                                     (Nat.S
3238                                                                     (Nat.S
3239                                                                     (Nat.S
3240                                                                     (Nat.S
3241                                                                     (Nat.S
3242                                                                     (Nat.S
3243                                                                     (Nat.S
3244                                                                     (Nat.S
3245                                                                     (Nat.S
3246                                                                     (Nat.S
3247                                                                     (Nat.S
3248                                                                     (Nat.S
3249                                                                     (Nat.S
3250                                                                     (Nat.S
3251                                                                     (Nat.S
3252                                                                     (Nat.S
3253                                                                     (Nat.S
3254                                                                     (Nat.S
3255                                                                     (Nat.S
3256                                                                     (Nat.S
3257                                                                     (Nat.S
3258                                                                     (Nat.S
3259                                                                     Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
3260                                                                     | Bool.True ->
3261                                                                     Types.Some
3262                                                                     (Types.Inl
3263                                                                     SFR_ACC_A)
3264                                                                     | Bool.False ->
3265                                                                     (match
3266                                                                     Nat.eqb
3267                                                                     address
3268                                                                     (Nat.S
3269                                                                     (Nat.S
3270                                                                     (Nat.S
3271                                                                     (Nat.S
3272                                                                     (Nat.S
3273                                                                     (Nat.S
3274                                                                     (Nat.S
3275                                                                     (Nat.S
3276                                                                     (Nat.S
3277                                                                     (Nat.S
3278                                                                     (Nat.S
3279                                                                     (Nat.S
3280                                                                     (Nat.S
3281                                                                     (Nat.S
3282                                                                     (Nat.S
3283                                                                     (Nat.S
3284                                                                     (Nat.S
3285                                                                     (Nat.S
3286                                                                     (Nat.S
3287                                                                     (Nat.S
3288                                                                     (Nat.S
3289                                                                     (Nat.S
3290                                                                     (Nat.S
3291                                                                     (Nat.S
3292                                                                     (Nat.S
3293                                                                     (Nat.S
3294                                                                     (Nat.S
3295                                                                     (Nat.S
3296                                                                     (Nat.S
3297                                                                     (Nat.S
3298                                                                     (Nat.S
3299                                                                     (Nat.S
3300                                                                     (Nat.S
3301                                                                     (Nat.S
3302                                                                     (Nat.S
3303                                                                     (Nat.S
3304                                                                     (Nat.S
3305                                                                     (Nat.S
3306                                                                     (Nat.S
3307                                                                     (Nat.S
3308                                                                     (Nat.S
3309                                                                     (Nat.S
3310                                                                     (Nat.S
3311                                                                     (Nat.S
3312                                                                     (Nat.S
3313                                                                     (Nat.S
3314                                                                     (Nat.S
3315                                                                     (Nat.S
3316                                                                     (Nat.S
3317                                                                     (Nat.S
3318                                                                     (Nat.S
3319                                                                     (Nat.S
3320                                                                     (Nat.S
3321                                                                     (Nat.S
3322                                                                     (Nat.S
3323                                                                     (Nat.S
3324                                                                     (Nat.S
3325                                                                     (Nat.S
3326                                                                     (Nat.S
3327                                                                     (Nat.S
3328                                                                     (Nat.S
3329                                                                     (Nat.S
3330                                                                     (Nat.S
3331                                                                     (Nat.S
3332                                                                     (Nat.S
3333                                                                     (Nat.S
3334                                                                     (Nat.S
3335                                                                     (Nat.S
3336                                                                     (Nat.S
3337                                                                     (Nat.S
3338                                                                     (Nat.S
3339                                                                     (Nat.S
3340                                                                     (Nat.S
3341                                                                     (Nat.S
3342                                                                     (Nat.S
3343                                                                     (Nat.S
3344                                                                     (Nat.S
3345                                                                     (Nat.S
3346                                                                     (Nat.S
3347                                                                     (Nat.S
3348                                                                     (Nat.S
3349                                                                     (Nat.S
3350                                                                     (Nat.S
3351                                                                     (Nat.S
3352                                                                     (Nat.S
3353                                                                     (Nat.S
3354                                                                     (Nat.S
3355                                                                     (Nat.S
3356                                                                     (Nat.S
3357                                                                     (Nat.S
3358                                                                     (Nat.S
3359                                                                     (Nat.S
3360                                                                     (Nat.S
3361                                                                     (Nat.S
3362                                                                     (Nat.S
3363                                                                     (Nat.S
3364                                                                     (Nat.S
3365                                                                     (Nat.S
3366                                                                     (Nat.S
3367                                                                     (Nat.S
3368                                                                     (Nat.S
3369                                                                     (Nat.S
3370                                                                     (Nat.S
3371                                                                     (Nat.S
3372                                                                     (Nat.S
3373                                                                     (Nat.S
3374                                                                     (Nat.S
3375                                                                     (Nat.S
3376                                                                     (Nat.S
3377                                                                     (Nat.S
3378                                                                     (Nat.S
3379                                                                     (Nat.S
3380                                                                     (Nat.S
3381                                                                     (Nat.S
3382                                                                     (Nat.S
3383                                                                     (Nat.S
3384                                                                     (Nat.S
3385                                                                     (Nat.S
3386                                                                     (Nat.S
3387                                                                     (Nat.S
3388                                                                     (Nat.S
3389                                                                     (Nat.S
3390                                                                     (Nat.S
3391                                                                     (Nat.S
3392                                                                     (Nat.S
3393                                                                     (Nat.S
3394                                                                     (Nat.S
3395                                                                     (Nat.S
3396                                                                     (Nat.S
3397                                                                     (Nat.S
3398                                                                     (Nat.S
3399                                                                     (Nat.S
3400                                                                     (Nat.S
3401                                                                     (Nat.S
3402                                                                     (Nat.S
3403                                                                     (Nat.S
3404                                                                     (Nat.S
3405                                                                     (Nat.S
3406                                                                     (Nat.S
3407                                                                     (Nat.S
3408                                                                     (Nat.S
3409                                                                     (Nat.S
3410                                                                     (Nat.S
3411                                                                     (Nat.S
3412                                                                     (Nat.S
3413                                                                     (Nat.S
3414                                                                     (Nat.S
3415                                                                     (Nat.S
3416                                                                     (Nat.S
3417                                                                     (Nat.S
3418                                                                     (Nat.S
3419                                                                     (Nat.S
3420                                                                     (Nat.S
3421                                                                     (Nat.S
3422                                                                     (Nat.S
3423                                                                     (Nat.S
3424                                                                     (Nat.S
3425                                                                     (Nat.S
3426                                                                     (Nat.S
3427                                                                     (Nat.S
3428                                                                     (Nat.S
3429                                                                     (Nat.S
3430                                                                     (Nat.S
3431                                                                     (Nat.S
3432                                                                     (Nat.S
3433                                                                     (Nat.S
3434                                                                     (Nat.S
3435                                                                     (Nat.S
3436                                                                     (Nat.S
3437                                                                     (Nat.S
3438                                                                     (Nat.S
3439                                                                     (Nat.S
3440                                                                     (Nat.S
3441                                                                     (Nat.S
3442                                                                     (Nat.S
3443                                                                     (Nat.S
3444                                                                     (Nat.S
3445                                                                     (Nat.S
3446                                                                     (Nat.S
3447                                                                     (Nat.S
3448                                                                     (Nat.S
3449                                                                     (Nat.S
3450                                                                     (Nat.S
3451                                                                     (Nat.S
3452                                                                     (Nat.S
3453                                                                     (Nat.S
3454                                                                     (Nat.S
3455                                                                     (Nat.S
3456                                                                     (Nat.S
3457                                                                     (Nat.S
3458                                                                     (Nat.S
3459                                                                     (Nat.S
3460                                                                     (Nat.S
3461                                                                     (Nat.S
3462                                                                     (Nat.S
3463                                                                     (Nat.S
3464                                                                     (Nat.S
3465                                                                     (Nat.S
3466                                                                     (Nat.S
3467                                                                     (Nat.S
3468                                                                     (Nat.S
3469                                                                     (Nat.S
3470                                                                     (Nat.S
3471                                                                     (Nat.S
3472                                                                     (Nat.S
3473                                                                     (Nat.S
3474                                                                     (Nat.S
3475                                                                     (Nat.S
3476                                                                     (Nat.S
3477                                                                     (Nat.S
3478                                                                     (Nat.S
3479                                                                     (Nat.S
3480                                                                     (Nat.S
3481                                                                     (Nat.S
3482                                                                     (Nat.S
3483                                                                     (Nat.S
3484                                                                     (Nat.S
3485                                                                     (Nat.S
3486                                                                     (Nat.S
3487                                                                     (Nat.S
3488                                                                     (Nat.S
3489                                                                     (Nat.S
3490                                                                     (Nat.S
3491                                                                     (Nat.S
3492                                                                     (Nat.S
3493                                                                     (Nat.S
3494                                                                     (Nat.S
3495                                                                     (Nat.S
3496                                                                     (Nat.S
3497                                                                     (Nat.S
3498                                                                     (Nat.S
3499                                                                     (Nat.S
3500                                                                     (Nat.S
3501                                                                     (Nat.S
3502                                                                     (Nat.S
3503                                                                     (Nat.S
3504                                                                     (Nat.S
3505                                                                     (Nat.S
3506                                                                     (Nat.S
3507                                                                     (Nat.S
3508                                                                     Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
3509                                                                     | Bool.True ->
3510                                                                     Types.Some
3511                                                                     (Types.Inl
3512                                                                     SFR_ACC_B)
3513                                                                     | Bool.False ->
3514                                                                     Types.None))))))))))))))))))))))))))
3515
3516 (** val get_bit_addressable_sfr :
3517     'a1 -> 'a1 preStatus -> BitVector.byte -> Bool.bool -> BitVector.byte **)
3518 let get_bit_addressable_sfr code_memory s b l =
3519   match sfr_of_Byte b with
3520   | Types.None -> assert false (* absurd case *)
3521   | Types.Some sfr8051_8052 ->
3522     (match sfr8051_8052 with
3523      | Types.Inl sfr ->
3524        (match sfr with
3525         | SFR_SP -> get_8051_sfr code_memory s sfr
3526         | SFR_DPL -> get_8051_sfr code_memory s sfr
3527         | SFR_DPH -> get_8051_sfr code_memory s sfr
3528         | SFR_PCON -> get_8051_sfr code_memory s sfr
3529         | SFR_TCON -> get_8051_sfr code_memory s sfr
3530         | SFR_TMOD -> get_8051_sfr code_memory s sfr
3531         | SFR_TL0 -> get_8051_sfr code_memory s sfr
3532         | SFR_TL1 -> get_8051_sfr code_memory s sfr
3533         | SFR_TH0 -> get_8051_sfr code_memory s sfr
3534         | SFR_TH1 -> get_8051_sfr code_memory s sfr
3535         | SFR_P1 ->
3536           (match l with
3537            | Bool.True -> s.p1_latch
3538            | Bool.False -> get_8051_sfr code_memory s SFR_P1)
3539         | SFR_SCON -> get_8051_sfr code_memory s sfr
3540         | SFR_SBUF -> get_8051_sfr code_memory s sfr
3541         | SFR_IE -> get_8051_sfr code_memory s sfr
3542         | SFR_P3 ->
3543           (match l with
3544            | Bool.True -> s.p3_latch
3545            | Bool.False -> get_8051_sfr code_memory s SFR_P3)
3546         | SFR_IP -> get_8051_sfr code_memory s sfr
3547         | SFR_PSW -> get_8051_sfr code_memory s sfr
3548         | SFR_ACC_A -> get_8051_sfr code_memory s sfr
3549         | SFR_ACC_B -> get_8051_sfr code_memory s sfr)
3550      | Types.Inr sfr -> get_8052_sfr code_memory s sfr)
3551
3552 (** val set_bit_addressable_sfr :
3553     'a1 -> 'a1 preStatus -> BitVector.byte -> BitVector.byte -> 'a1 preStatus **)
3554 let set_bit_addressable_sfr code_memory s b v =
3555   match sfr_of_Byte b with
3556   | Types.None -> assert false (* absurd case *)
3557   | Types.Some sfr8051_8052 ->
3558     (match sfr8051_8052 with
3559      | Types.Inl sfr ->
3560        (match sfr with
3561         | SFR_SP -> set_8051_sfr code_memory s sfr v
3562         | SFR_DPL -> set_8051_sfr code_memory s sfr v
3563         | SFR_DPH -> set_8051_sfr code_memory s sfr v
3564         | SFR_PCON -> set_8051_sfr code_memory s sfr v
3565         | SFR_TCON -> set_8051_sfr code_memory s sfr v
3566         | SFR_TMOD -> set_8051_sfr code_memory s sfr v
3567         | SFR_TL0 -> set_8051_sfr code_memory s sfr v
3568         | SFR_TL1 -> set_8051_sfr code_memory s sfr v
3569         | SFR_TH0 -> set_8051_sfr code_memory s sfr v
3570         | SFR_TH1 -> set_8051_sfr code_memory s sfr v
3571         | SFR_P1 ->
3572           let status_1 = set_8051_sfr code_memory s SFR_P1 v in
3573           set_p1_latch code_memory s v
3574         | SFR_SCON -> set_8051_sfr code_memory s sfr v
3575         | SFR_SBUF -> set_8051_sfr code_memory s sfr v
3576         | SFR_IE -> set_8051_sfr code_memory s sfr v
3577         | SFR_P3 ->
3578           let status_1 = set_8051_sfr code_memory s SFR_P3 v in
3579           set_p3_latch code_memory s v
3580         | SFR_IP -> set_8051_sfr code_memory s sfr v
3581         | SFR_PSW -> set_8051_sfr code_memory s sfr v
3582         | SFR_ACC_A -> set_8051_sfr code_memory s sfr v
3583         | SFR_ACC_B -> set_8051_sfr code_memory s sfr v)
3584      | Types.Inr sfr -> set_8052_sfr code_memory s sfr v)
3585
3586 (** val bit_address_of_register :
3587     'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.bitVector **)
3588 let bit_address_of_register code_memory s r =
3589   let b = Vector.get_index_v (Nat.S (Nat.S (Nat.S Nat.O))) r Nat.O in
3590   let c = Vector.get_index_v (Nat.S (Nat.S (Nat.S Nat.O))) r (Nat.S Nat.O) in
3591   let d =
3592     Vector.get_index_v (Nat.S (Nat.S (Nat.S Nat.O))) r (Nat.S (Nat.S Nat.O))
3593   in
3594   let r1 = get_rs1_flag code_memory s in
3595   let r0 = get_rs0_flag code_memory s in
3596   let offset =
3597     match Bool.andb (Bool.notb r1) (Bool.notb r0) with
3598     | Bool.True -> Nat.O
3599     | Bool.False ->
3600       (match Bool.andb (Bool.notb r1) r0 with
3601        | Bool.True ->
3602          Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))
3603        | Bool.False ->
3604          (match Bool.andb r1 r0 with
3605           | Bool.True ->
3606             Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3607               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3608               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3609               Nat.O)))))))))))))))))))))))
3610           | Bool.False ->
3611             Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3612               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3613               Nat.O)))))))))))))))))
3614   in
3615   Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3616     (Nat.S Nat.O)))))))
3617     (Nat.plus offset
3618       (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
3619         (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
3620         (Vector.VCons ((Nat.S (Nat.S Nat.O)), b, (Vector.VCons ((Nat.S
3621         Nat.O), c, (Vector.VCons (Nat.O, d, Vector.VEmpty))))))))))
3622
3623 (** val get_register :
3624     'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte **)
3625 let get_register code_memory s r =
3626   let address = bit_address_of_register code_memory s r in
3627   BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3628     Nat.O))))))) address s.low_internal_ram
3629     (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3630       Nat.O)))))))))
3631
3632 (** val set_register :
3633     'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
3634     preStatus **)
3635 let set_register code_memory s r v =
3636   let address = bit_address_of_register code_memory s r in
3637   update_low_internal_ram code_memory s address v
3638
3639 (** val read_from_external_ram :
3640     'a1 -> 'a1 preStatus -> BitVector.word -> BitVector.byte **)
3641 let read_from_external_ram code_memory s addr =
3642   BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3643     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3644     Nat.O)))))))))))))))) addr s.external_ram
3645     (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3646       Nat.O)))))))))
3647
3648 (** val read_from_internal_ram :
3649     'a1 -> 'a1 preStatus -> BitVector.byte -> BitVector.byte **)
3650 let read_from_internal_ram code_memory s addr =
3651   let { Types.fst = bit_one; Types.snd = seven_bits } =
3652     Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3653       (Nat.S Nat.O))))))) addr
3654   in
3655   let memory =
3656     match Vector.head' Nat.O bit_one with
3657     | Bool.True -> s.high_internal_ram
3658     | Bool.False -> s.low_internal_ram
3659   in
3660   BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3661     Nat.O))))))) seven_bits memory
3662     (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3663       Nat.O)))))))))
3664
3665 (** val read_at_stack_pointer : 'a1 -> 'a1 preStatus -> BitVector.byte **)
3666 let read_at_stack_pointer code_memory s =
3667   read_from_internal_ram code_memory s (get_8051_sfr code_memory s SFR_SP)
3668
3669 (** val write_at_stack_pointer :
3670     'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus **)
3671 let write_at_stack_pointer code_memory s v =
3672   let { Types.fst = bit_one; Types.snd = seven_bits } =
3673     Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3674       (Nat.S Nat.O))))))) (get_8051_sfr code_memory s SFR_SP)
3675   in
3676   (match Vector.head' Nat.O bit_one with
3677    | Bool.True -> update_high_internal_ram code_memory s seven_bits v
3678    | Bool.False -> update_low_internal_ram code_memory s seven_bits v)
3679
3680 (** val set_arg_16' :
3681     'a1 -> 'a1 preStatus -> BitVector.word -> ASM.subaddressing_mode -> 'a1
3682     preStatus Types.sig0 **)
3683 let set_arg_16' code_memory s v a =
3684   (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Dptr,
3685            Vector.VEmpty)) a with
3686    | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
3687    | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
3688    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
3689    | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
3690    | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
3691    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
3692    | ASM.DPTR ->
3693      (fun _ ->
3694        (let { Types.fst = bu; Types.snd = bl } =
3695           Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3696             (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3697             (Nat.S (Nat.S Nat.O)))))))) v
3698         in
3699        (fun _ ->
3700        let status0 = set_8051_sfr code_memory s SFR_DPH bu in
3701        let status1 = set_8051_sfr code_memory status0 SFR_DPL bl in status1))
3702          __)
3703    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
3704    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
3705    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
3706    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
3707    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
3708    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
3709    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
3710    | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
3711    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
3712    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
3713    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
3714    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
3715
3716 (** val set_arg_16 :
3717     'a1 -> 'a1 preStatus -> BitVector.word -> ASM.subaddressing_mode -> 'a1
3718     preStatus **)
3719 let set_arg_16 code_memory s h h1 =
3720   Types.pi1 (set_arg_16' code_memory s h h1)
3721
3722 (** val get_arg_16 :
3723     'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> BitVector.word **)
3724 let get_arg_16 cm s a =
3725   (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
3726            ASM.Data16, (Vector.VCons (Nat.O, ASM.Acc_dptr, Vector.VEmpty))))
3727            a with
3728    | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
3729    | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
3730    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
3731    | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
3732    | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
3733    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
3734    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
3735    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
3736    | ASM.DATA16 d -> (fun _ -> d)
3737    | ASM.ACC_DPTR ->
3738      (fun _ ->
3739        let dptr =
3740          Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3741            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3742            (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_DPH)
3743            (get_8051_sfr cm s SFR_DPL)
3744        in
3745        let big_acc =
3746          Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3747            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3748            (Nat.S (Nat.S Nat.O))))))))
3749            (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3750              (Nat.S Nat.O))))))))) (get_8051_sfr cm s SFR_ACC_A)
3751        in
3752        Arithmetic.add
3753          (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3754            Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3755            (Nat.S Nat.O))))))))) big_acc dptr)
3756    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
3757    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
3758    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
3759    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
3760    | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
3761    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
3762    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
3763    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
3764    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
3765
3766 (** val get_arg_8 :
3767     'a1 -> 'a1 preStatus -> Bool.bool -> ASM.subaddressing_mode ->
3768     BitVector.byte **)
3769 let get_arg_8 cm s l a =
3770   (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3771            (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S
3772            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
3773            ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3774            (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons
3775            ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))),
3776            ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3777            (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S
3778            (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S
3779            (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
3780            (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S
3781            Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
3782            ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
3783            Vector.VEmpty)))))))))))))))))))) a with
3784    | ASM.DIRECT d ->
3785      (fun _ ->
3786        let { Types.fst = hd; Types.snd = seven_bits } =
3787          Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3788            (Nat.S (Nat.S Nat.O))))))) d
3789        in
3790        (match Vector.head' Nat.O hd with
3791         | Bool.True ->
3792           get_bit_addressable_sfr cm s (Vector.VCons ((Nat.S (Nat.S (Nat.S
3793             (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, seven_bits))
3794             l
3795         | Bool.False ->
3796           BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3797             (Nat.S Nat.O))))))) seven_bits s.low_internal_ram
3798             (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3799               (Nat.S Nat.O)))))))))))
3800    | ASM.INDIRECT i ->
3801      (fun _ ->
3802        let { Types.fst = hd; Types.snd = seven_bits } =
3803          Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3804            (Nat.S (Nat.S Nat.O)))))))
3805            (get_register cm s (Vector.VCons ((Nat.S (Nat.S Nat.O)),
3806              Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False,
3807              (Vector.VCons (Nat.O, i, Vector.VEmpty)))))))
3808        in
3809        (match Vector.head' Nat.O hd with
3810         | Bool.True ->
3811           BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3812             (Nat.S Nat.O))))))) seven_bits s.high_internal_ram
3813             (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3814               (Nat.S Nat.O)))))))))
3815         | Bool.False ->
3816           BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3817             (Nat.S Nat.O))))))) seven_bits s.low_internal_ram
3818             (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3819               (Nat.S Nat.O)))))))))))
3820    | ASM.EXT_INDIRECT e ->
3821      (fun _ ->
3822        let address =
3823          get_register cm s (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
3824            (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, e,
3825            Vector.VEmpty))))))
3826        in
3827        let padded_address =
3828          BitVector.pad (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3829            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3830            (Nat.S (Nat.S Nat.O)))))))) address
3831        in
3832        read_from_external_ram cm s padded_address)
3833    | ASM.REGISTER r -> (fun _ -> get_register cm s r)
3834    | ASM.ACC_A -> (fun _ -> get_8051_sfr cm s SFR_ACC_A)
3835    | ASM.ACC_B -> (fun _ -> get_8051_sfr cm s SFR_ACC_B)
3836    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
3837    | ASM.DATA d -> (fun _ -> d)
3838    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
3839    | ASM.ACC_DPTR ->
3840      (fun _ ->
3841        let dptr =
3842          Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3843            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3844            (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_DPH)
3845            (get_8051_sfr cm s SFR_DPL)
3846        in
3847        let padded_acc =
3848          BitVector.pad (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3849            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3850            (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_ACC_A)
3851        in
3852        let { Types.fst = carry; Types.snd = address } =
3853          Arithmetic.half_add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3854            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3855            Nat.O)))))))))))))))) dptr padded_acc
3856        in
3857        read_from_external_ram cm s address)
3858    | ASM.ACC_PC ->
3859      (fun _ ->
3860        let padded_acc =
3861          BitVector.pad (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3862            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3863            (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_ACC_A)
3864        in
3865        let { Types.fst = carry; Types.snd = address } =
3866          Arithmetic.half_add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3867            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3868            Nat.O)))))))))))))))) s.program_counter padded_acc
3869        in
3870        read_from_external_ram cm s address)
3871    | ASM.EXT_INDIRECT_DPTR ->
3872      (fun _ ->
3873        let address =
3874          Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3875            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3876            (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_DPH)
3877            (get_8051_sfr cm s SFR_DPL)
3878        in
3879        read_from_external_ram cm s address)
3880    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
3881    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
3882    | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
3883    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
3884    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
3885    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
3886    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
3887
3888 (** val set_arg_8 :
3889     'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> BitVector.byte -> 'a1
3890     preStatus **)
3891 let set_arg_8 cm s a v =
3892   (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3893            Nat.O)))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3894            (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S
3895            (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons
3896            ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons
3897            ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S
3898            (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O),
3899            ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
3900            Vector.VEmpty)))))))))))))) a with
3901    | ASM.DIRECT d ->
3902      (fun _ ->
3903        let { Types.fst = bit_one; Types.snd = seven_bits } =
3904          Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3905            (Nat.S (Nat.S Nat.O))))))) d
3906        in
3907        (match Vector.head' Nat.O bit_one with
3908         | Bool.True ->
3909           set_bit_addressable_sfr cm s (Vector.VCons ((Nat.S (Nat.S (Nat.S
3910             (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, seven_bits))
3911             v
3912         | Bool.False -> update_low_internal_ram cm s seven_bits v))
3913    | ASM.INDIRECT i ->
3914      (fun _ ->
3915        let register =
3916          get_register cm s (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
3917            (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, i,
3918            Vector.VEmpty))))))
3919        in
3920        let { Types.fst = bit_one; Types.snd = seven_bits } =
3921          Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3922            (Nat.S (Nat.S Nat.O))))))) register
3923        in
3924        (match Vector.head' Nat.O bit_one with
3925         | Bool.True -> update_high_internal_ram cm s seven_bits v
3926         | Bool.False -> update_low_internal_ram cm s seven_bits v))
3927    | ASM.EXT_INDIRECT e ->
3928      (fun _ ->
3929        let address =
3930          get_register cm s (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
3931            (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, e,
3932            Vector.VEmpty))))))
3933        in
3934        let padded_address =
3935          BitVector.pad (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3936            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3937            (Nat.S (Nat.S Nat.O)))))))) address
3938        in
3939        update_external_ram cm s padded_address v)
3940    | ASM.REGISTER r -> (fun _ -> set_register cm s r v)
3941    | ASM.ACC_A -> (fun _ -> set_8051_sfr cm s SFR_ACC_A v)
3942    | ASM.ACC_B -> (fun _ -> set_8051_sfr cm s SFR_ACC_B v)
3943    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
3944    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
3945    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
3946    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
3947    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
3948    | ASM.EXT_INDIRECT_DPTR ->
3949      (fun _ ->
3950        let address =
3951          Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3952            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3953            (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_DPH)
3954            (get_8051_sfr cm s SFR_DPL)
3955        in
3956        update_external_ram cm s address v)
3957    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
3958    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
3959    | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
3960    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
3961    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
3962    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
3963    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
3964
3965 (** val get_arg_1 :
3966     'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> Bool.bool -> Bool.bool **)
3967 let get_arg_1 cm s a l =
3968   (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
3969            (Nat.S Nat.O)), ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O),
3970            ASM.N_bit_addr, (Vector.VCons (Nat.O, ASM.Carry,
3971            Vector.VEmpty)))))) a with
3972    | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
3973    | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
3974    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
3975    | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
3976    | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
3977    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
3978    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
3979    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
3980    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
3981    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
3982    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
3983    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
3984    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
3985    | ASM.CARRY -> (fun _ -> get_cy_flag cm s)
3986    | ASM.BIT_ADDR b ->
3987      (fun _ ->
3988        let { Types.fst = bit_1; Types.snd = seven_bits } =
3989          Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3990            (Nat.S (Nat.S Nat.O))))))) b
3991        in
3992        let { Types.fst = four_bits; Types.snd = three_bits } =
3993          Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
3994            (Nat.S Nat.O))) seven_bits
3995        in
3996        (match Vector.head' Nat.O bit_1 with
3997         | Bool.True ->
3998           let trans =
3999             Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
4000               (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
4001               (Nat.S (Nat.S Nat.O)))), Bool.True, four_bits)) (Vector.VCons
4002               ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S
4003               Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
4004               Vector.VEmpty))))))
4005           in
4006           let sfr = get_bit_addressable_sfr cm s trans l in
4007           Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4008             (Nat.S Nat.O)))))))) sfr
4009             (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S Nat.O)))
4010               three_bits)
4011         | Bool.False ->
4012           let address' =
4013             Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
4014               (Nat.S Nat.O)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
4015               Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
4016               (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))) four_bits
4017           in
4018           let t =
4019             BitVectorTrie.lookup
4020               (Nat.plus (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
4021                 (Nat.S Nat.O))))) address' s.low_internal_ram
4022               (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4023                 (Nat.S (Nat.S Nat.O)))))))))
4024           in
4025           Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4026             (Nat.S Nat.O)))))))) t
4027             (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S Nat.O)))
4028               three_bits)))
4029    | ASM.N_BIT_ADDR n ->
4030      (fun _ ->
4031        let { Types.fst = bit_1; Types.snd = seven_bits } =
4032          Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4033            (Nat.S (Nat.S Nat.O))))))) n
4034        in
4035        let { Types.fst = four_bits; Types.snd = three_bits } =
4036          Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
4037            (Nat.S Nat.O))) seven_bits
4038        in
4039        (match Vector.head' Nat.O bit_1 with
4040         | Bool.True ->
4041           let trans =
4042             Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
4043               (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
4044               (Nat.S (Nat.S Nat.O)))), Bool.True, four_bits)) (Vector.VCons
4045               ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S
4046               Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
4047               Vector.VEmpty))))))
4048           in
4049           let sfr = get_bit_addressable_sfr cm s trans l in
4050           Bool.notb
4051             (Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4052               (Nat.S (Nat.S Nat.O)))))))) sfr
4053               (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S Nat.O)))
4054                 three_bits))
4055         | Bool.False ->
4056           let address' =
4057             Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
4058               (Nat.S Nat.O)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
4059               Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
4060               (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))) four_bits
4061           in
4062           let t =
4063             BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4064               (Nat.S Nat.O))))))) address' s.low_internal_ram
4065               (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4066                 (Nat.S (Nat.S Nat.O)))))))))
4067           in
4068           Bool.notb
4069             (Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4070               (Nat.S (Nat.S Nat.O)))))))) t
4071               (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S Nat.O)))
4072                 three_bits))))
4073    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
4074    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
4075    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
4076
4077 (** val set_arg_1 :
4078     'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> BitVector.bit -> 'a1
4079     preStatus **)
4080 let set_arg_1 cm s a v =
4081   (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
4082            ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))) a with
4083    | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
4084    | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
4085    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
4086    | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
4087    | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
4088    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
4089    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
4090    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
4091    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
4092    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
4093    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
4094    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
4095    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
4096    | ASM.CARRY ->
4097      (fun _ ->
4098        let { Types.fst = ignore; Types.snd = seven_bits } =
4099          Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4100            (Nat.S (Nat.S Nat.O))))))) (get_8051_sfr cm s SFR_PSW)
4101        in
4102        let new_psw = Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4103          (Nat.S Nat.O))))))), v, seven_bits)
4104        in
4105        set_8051_sfr cm s SFR_PSW new_psw)
4106    | ASM.BIT_ADDR b ->
4107      (fun _ ->
4108        let { Types.fst = bit_1; Types.snd = seven_bits } =
4109          Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4110            (Nat.S (Nat.S Nat.O))))))) b
4111        in
4112        let { Types.fst = four_bits; Types.snd = three_bits } =
4113          Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
4114            (Nat.S Nat.O))) seven_bits
4115        in
4116        (match Vector.head' Nat.O bit_1 with
4117         | Bool.True ->
4118           let trans =
4119             Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
4120               (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
4121               (Nat.S (Nat.S Nat.O)))), Bool.True, four_bits)) (Vector.VCons
4122               ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S
4123               Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
4124               Vector.VEmpty))))))
4125           in
4126           let sfr = get_bit_addressable_sfr cm s trans Bool.True in
4127           let new_sfr =
4128             Vector.set_index (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4129               (Nat.S Nat.O)))))))) sfr
4130               (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S Nat.O)))
4131                 three_bits) v
4132           in
4133           set_bit_addressable_sfr cm s new_sfr trans
4134         | Bool.False ->
4135           let address' =
4136             Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
4137               (Nat.S Nat.O)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
4138               Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
4139               (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))) four_bits
4140           in
4141           let t =
4142             BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4143               (Nat.S Nat.O))))))) address' s.low_internal_ram
4144               (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4145                 (Nat.S (Nat.S Nat.O)))))))))
4146           in
4147           let n_bit =
4148             Vector.set_index (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4149               (Nat.S Nat.O)))))))) t
4150               (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S Nat.O)))
4151                 three_bits) v
4152           in
4153           update_low_internal_ram cm s address' n_bit))
4154    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
4155    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
4156    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
4157    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
4158
4159 (** val construct_datalabels :
4160     (ASM.identifier, BitVector.word) Types.prod List.list -> BitVector.word
4161     Identifiers.identifier_map **)
4162 let construct_datalabels the_preamble =
4163   (Util.foldl (fun t preamble ->
4164     let { Types.fst = datalabels; Types.snd = addr } = t in
4165     let { Types.fst = name; Types.snd = size } = preamble in
4166     let { Types.fst = addr0; Types.snd = carry } =
4167       Arithmetic.sub_16_with_carry addr size Bool.False
4168     in
4169     { Types.fst =
4170     (Identifiers.add PreIdentifiers.ASMTag datalabels name addr0);
4171     Types.snd = addr0 }) { Types.fst =
4172     (Identifiers.empty_map PreIdentifiers.ASMTag); Types.snd =
4173     (BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4174       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4175       Nat.O))))))))))))))))) } the_preamble).Types.fst
4176