extracted/i8051.ml

   1 open Preamble
   2
   3 open Bool
   4
   5 open Hints_declaration
   6
   7 open Core_notation
   8
   9 open Pts
  10
  11 open Logic
  12
  13 open Relations
  14
  15 open Nat
  16
  17 open Jmeq
  18
  19 open Exp
  20
  21 open Setoids
  22
  23 open Monad
  24
  25 open Option
  26
  27 open Extranat
  28
  29 open Vector
  30
  31 open Div_and_mod
  32
  33 open Russell
  34
  35 open Types
  36
  37 open List
  38
  39 open Util
  40
  41 open FoldStuff
  42
  43 open BitVector
  44
  45 open Arithmetic
  46
  47 (** val int_size : BitVector.bitVector **)
  48 let int_size =
  49   Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
  50     (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O)
  51
  52 (** val ptr_size : BitVector.bitVector **)
  53 let ptr_size =
  54   Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
  55     (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S Nat.O))
  56
  57 (** val alignment : 'a1 Types.option **)
  58 let alignment =
  59   Types.None
  60
  61 type register =
  62 | Register00
  63 | Register01
  64 | Register02
  65 | Register03
  66 | Register04
  67 | Register05
  68 | Register06
  69 | Register07
  70 | Register10
  71 | Register11
  72 | Register12
  73 | Register13
  74 | Register14
  75 | Register15
  76 | Register16
  77 | Register17
  78 | Register20
  79 | Register21
  80 | Register22
  81 | Register23
  82 | Register24
  83 | Register25
  84 | Register26
  85 | Register27
  86 | Register30
  87 | Register31
  88 | Register32
  89 | Register33
  90 | Register34
  91 | Register35
  92 | Register36
  93 | Register37
  94 | RegisterA
  95 | RegisterB
  96 | RegisterDPL
  97 | RegisterDPH
  98 | RegisterCarry
  99
 100 (** val register_rect_Type4 :
 101     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 102     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
 103     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 104     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1 **)
 105 let rec register_rect_Type4 h_Register00 h_Register01 h_Register02 h_Register03 h_Register04 h_Register05 h_Register06 h_Register07 h_Register10 h_Register11 h_Register12 h_Register13 h_Register14 h_Register15 h_Register16 h_Register17 h_Register20 h_Register21 h_Register22 h_Register23 h_Register24 h_Register25 h_Register26 h_Register27 h_Register30 h_Register31 h_Register32 h_Register33 h_Register34 h_Register35 h_Register36 h_Register37 h_RegisterA h_RegisterB h_RegisterDPL h_RegisterDPH h_RegisterCarry = function
 106 | Register00 -> h_Register00
 107 | Register01 -> h_Register01
 108 | Register02 -> h_Register02
 109 | Register03 -> h_Register03
 110 | Register04 -> h_Register04
 111 | Register05 -> h_Register05
 112 | Register06 -> h_Register06
 113 | Register07 -> h_Register07
 114 | Register10 -> h_Register10
 115 | Register11 -> h_Register11
 116 | Register12 -> h_Register12
 117 | Register13 -> h_Register13
 118 | Register14 -> h_Register14
 119 | Register15 -> h_Register15
 120 | Register16 -> h_Register16
 121 | Register17 -> h_Register17
 122 | Register20 -> h_Register20
 123 | Register21 -> h_Register21
 124 | Register22 -> h_Register22
 125 | Register23 -> h_Register23
 126 | Register24 -> h_Register24
 127 | Register25 -> h_Register25
 128 | Register26 -> h_Register26
 129 | Register27 -> h_Register27
 130 | Register30 -> h_Register30
 131 | Register31 -> h_Register31
 132 | Register32 -> h_Register32
 133 | Register33 -> h_Register33
 134 | Register34 -> h_Register34
 135 | Register35 -> h_Register35
 136 | Register36 -> h_Register36
 137 | Register37 -> h_Register37
 138 | RegisterA -> h_RegisterA
 139 | RegisterB -> h_RegisterB
 140 | RegisterDPL -> h_RegisterDPL
 141 | RegisterDPH -> h_RegisterDPH
 142 | RegisterCarry -> h_RegisterCarry
 143
 144 (** val register_rect_Type5 :
 145     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 146     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
 147     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 148     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1 **)
 149 let rec register_rect_Type5 h_Register00 h_Register01 h_Register02 h_Register03 h_Register04 h_Register05 h_Register06 h_Register07 h_Register10 h_Register11 h_Register12 h_Register13 h_Register14 h_Register15 h_Register16 h_Register17 h_Register20 h_Register21 h_Register22 h_Register23 h_Register24 h_Register25 h_Register26 h_Register27 h_Register30 h_Register31 h_Register32 h_Register33 h_Register34 h_Register35 h_Register36 h_Register37 h_RegisterA h_RegisterB h_RegisterDPL h_RegisterDPH h_RegisterCarry = function
 150 | Register00 -> h_Register00
 151 | Register01 -> h_Register01
 152 | Register02 -> h_Register02
 153 | Register03 -> h_Register03
 154 | Register04 -> h_Register04
 155 | Register05 -> h_Register05
 156 | Register06 -> h_Register06
 157 | Register07 -> h_Register07
 158 | Register10 -> h_Register10
 159 | Register11 -> h_Register11
 160 | Register12 -> h_Register12
 161 | Register13 -> h_Register13
 162 | Register14 -> h_Register14
 163 | Register15 -> h_Register15
 164 | Register16 -> h_Register16
 165 | Register17 -> h_Register17
 166 | Register20 -> h_Register20
 167 | Register21 -> h_Register21
 168 | Register22 -> h_Register22
 169 | Register23 -> h_Register23
 170 | Register24 -> h_Register24
 171 | Register25 -> h_Register25
 172 | Register26 -> h_Register26
 173 | Register27 -> h_Register27
 174 | Register30 -> h_Register30
 175 | Register31 -> h_Register31
 176 | Register32 -> h_Register32
 177 | Register33 -> h_Register33
 178 | Register34 -> h_Register34
 179 | Register35 -> h_Register35
 180 | Register36 -> h_Register36
 181 | Register37 -> h_Register37
 182 | RegisterA -> h_RegisterA
 183 | RegisterB -> h_RegisterB
 184 | RegisterDPL -> h_RegisterDPL
 185 | RegisterDPH -> h_RegisterDPH
 186 | RegisterCarry -> h_RegisterCarry
 187
 188 (** val register_rect_Type3 :
 189     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 190     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
 191     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 192     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1 **)
 193 let rec register_rect_Type3 h_Register00 h_Register01 h_Register02 h_Register03 h_Register04 h_Register05 h_Register06 h_Register07 h_Register10 h_Register11 h_Register12 h_Register13 h_Register14 h_Register15 h_Register16 h_Register17 h_Register20 h_Register21 h_Register22 h_Register23 h_Register24 h_Register25 h_Register26 h_Register27 h_Register30 h_Register31 h_Register32 h_Register33 h_Register34 h_Register35 h_Register36 h_Register37 h_RegisterA h_RegisterB h_RegisterDPL h_RegisterDPH h_RegisterCarry = function
 194 | Register00 -> h_Register00
 195 | Register01 -> h_Register01
 196 | Register02 -> h_Register02
 197 | Register03 -> h_Register03
 198 | Register04 -> h_Register04
 199 | Register05 -> h_Register05
 200 | Register06 -> h_Register06
 201 | Register07 -> h_Register07
 202 | Register10 -> h_Register10
 203 | Register11 -> h_Register11
 204 | Register12 -> h_Register12
 205 | Register13 -> h_Register13
 206 | Register14 -> h_Register14
 207 | Register15 -> h_Register15
 208 | Register16 -> h_Register16
 209 | Register17 -> h_Register17
 210 | Register20 -> h_Register20
 211 | Register21 -> h_Register21
 212 | Register22 -> h_Register22
 213 | Register23 -> h_Register23
 214 | Register24 -> h_Register24
 215 | Register25 -> h_Register25
 216 | Register26 -> h_Register26
 217 | Register27 -> h_Register27
 218 | Register30 -> h_Register30
 219 | Register31 -> h_Register31
 220 | Register32 -> h_Register32
 221 | Register33 -> h_Register33
 222 | Register34 -> h_Register34
 223 | Register35 -> h_Register35
 224 | Register36 -> h_Register36
 225 | Register37 -> h_Register37
 226 | RegisterA -> h_RegisterA
 227 | RegisterB -> h_RegisterB
 228 | RegisterDPL -> h_RegisterDPL
 229 | RegisterDPH -> h_RegisterDPH
 230 | RegisterCarry -> h_RegisterCarry
 231
 232 (** val register_rect_Type2 :
 233     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 234     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
 235     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 236     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1 **)
 237 let rec register_rect_Type2 h_Register00 h_Register01 h_Register02 h_Register03 h_Register04 h_Register05 h_Register06 h_Register07 h_Register10 h_Register11 h_Register12 h_Register13 h_Register14 h_Register15 h_Register16 h_Register17 h_Register20 h_Register21 h_Register22 h_Register23 h_Register24 h_Register25 h_Register26 h_Register27 h_Register30 h_Register31 h_Register32 h_Register33 h_Register34 h_Register35 h_Register36 h_Register37 h_RegisterA h_RegisterB h_RegisterDPL h_RegisterDPH h_RegisterCarry = function
 238 | Register00 -> h_Register00
 239 | Register01 -> h_Register01
 240 | Register02 -> h_Register02
 241 | Register03 -> h_Register03
 242 | Register04 -> h_Register04
 243 | Register05 -> h_Register05
 244 | Register06 -> h_Register06
 245 | Register07 -> h_Register07
 246 | Register10 -> h_Register10
 247 | Register11 -> h_Register11
 248 | Register12 -> h_Register12
 249 | Register13 -> h_Register13
 250 | Register14 -> h_Register14
 251 | Register15 -> h_Register15
 252 | Register16 -> h_Register16
 253 | Register17 -> h_Register17
 254 | Register20 -> h_Register20
 255 | Register21 -> h_Register21
 256 | Register22 -> h_Register22
 257 | Register23 -> h_Register23
 258 | Register24 -> h_Register24
 259 | Register25 -> h_Register25
 260 | Register26 -> h_Register26
 261 | Register27 -> h_Register27
 262 | Register30 -> h_Register30
 263 | Register31 -> h_Register31
 264 | Register32 -> h_Register32
 265 | Register33 -> h_Register33
 266 | Register34 -> h_Register34
 267 | Register35 -> h_Register35
 268 | Register36 -> h_Register36
 269 | Register37 -> h_Register37
 270 | RegisterA -> h_RegisterA
 271 | RegisterB -> h_RegisterB
 272 | RegisterDPL -> h_RegisterDPL
 273 | RegisterDPH -> h_RegisterDPH
 274 | RegisterCarry -> h_RegisterCarry
 275
 276 (** val register_rect_Type1 :
 277     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 278     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
 279     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 280     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1 **)
 281 let rec register_rect_Type1 h_Register00 h_Register01 h_Register02 h_Register03 h_Register04 h_Register05 h_Register06 h_Register07 h_Register10 h_Register11 h_Register12 h_Register13 h_Register14 h_Register15 h_Register16 h_Register17 h_Register20 h_Register21 h_Register22 h_Register23 h_Register24 h_Register25 h_Register26 h_Register27 h_Register30 h_Register31 h_Register32 h_Register33 h_Register34 h_Register35 h_Register36 h_Register37 h_RegisterA h_RegisterB h_RegisterDPL h_RegisterDPH h_RegisterCarry = function
 282 | Register00 -> h_Register00
 283 | Register01 -> h_Register01
 284 | Register02 -> h_Register02
 285 | Register03 -> h_Register03
 286 | Register04 -> h_Register04
 287 | Register05 -> h_Register05
 288 | Register06 -> h_Register06
 289 | Register07 -> h_Register07
 290 | Register10 -> h_Register10
 291 | Register11 -> h_Register11
 292 | Register12 -> h_Register12
 293 | Register13 -> h_Register13
 294 | Register14 -> h_Register14
 295 | Register15 -> h_Register15
 296 | Register16 -> h_Register16
 297 | Register17 -> h_Register17
 298 | Register20 -> h_Register20
 299 | Register21 -> h_Register21
 300 | Register22 -> h_Register22
 301 | Register23 -> h_Register23
 302 | Register24 -> h_Register24
 303 | Register25 -> h_Register25
 304 | Register26 -> h_Register26
 305 | Register27 -> h_Register27
 306 | Register30 -> h_Register30
 307 | Register31 -> h_Register31
 308 | Register32 -> h_Register32
 309 | Register33 -> h_Register33
 310 | Register34 -> h_Register34
 311 | Register35 -> h_Register35
 312 | Register36 -> h_Register36
 313 | Register37 -> h_Register37
 314 | RegisterA -> h_RegisterA
 315 | RegisterB -> h_RegisterB
 316 | RegisterDPL -> h_RegisterDPL
 317 | RegisterDPH -> h_RegisterDPH
 318 | RegisterCarry -> h_RegisterCarry
 319
 320 (** val register_rect_Type0 :
 321     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 322     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
 323     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 324     -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1 **)
 325 let rec register_rect_Type0 h_Register00 h_Register01 h_Register02 h_Register03 h_Register04 h_Register05 h_Register06 h_Register07 h_Register10 h_Register11 h_Register12 h_Register13 h_Register14 h_Register15 h_Register16 h_Register17 h_Register20 h_Register21 h_Register22 h_Register23 h_Register24 h_Register25 h_Register26 h_Register27 h_Register30 h_Register31 h_Register32 h_Register33 h_Register34 h_Register35 h_Register36 h_Register37 h_RegisterA h_RegisterB h_RegisterDPL h_RegisterDPH h_RegisterCarry = function
 326 | Register00 -> h_Register00
 327 | Register01 -> h_Register01
 328 | Register02 -> h_Register02
 329 | Register03 -> h_Register03
 330 | Register04 -> h_Register04
 331 | Register05 -> h_Register05
 332 | Register06 -> h_Register06
 333 | Register07 -> h_Register07
 334 | Register10 -> h_Register10
 335 | Register11 -> h_Register11
 336 | Register12 -> h_Register12
 337 | Register13 -> h_Register13
 338 | Register14 -> h_Register14
 339 | Register15 -> h_Register15
 340 | Register16 -> h_Register16
 341 | Register17 -> h_Register17
 342 | Register20 -> h_Register20
 343 | Register21 -> h_Register21
 344 | Register22 -> h_Register22
 345 | Register23 -> h_Register23
 346 | Register24 -> h_Register24
 347 | Register25 -> h_Register25
 348 | Register26 -> h_Register26
 349 | Register27 -> h_Register27
 350 | Register30 -> h_Register30
 351 | Register31 -> h_Register31
 352 | Register32 -> h_Register32
 353 | Register33 -> h_Register33
 354 | Register34 -> h_Register34
 355 | Register35 -> h_Register35
 356 | Register36 -> h_Register36
 357 | Register37 -> h_Register37
 358 | RegisterA -> h_RegisterA
 359 | RegisterB -> h_RegisterB
 360 | RegisterDPL -> h_RegisterDPL
 361 | RegisterDPH -> h_RegisterDPH
 362 | RegisterCarry -> h_RegisterCarry
 363
 364 (** val register_inv_rect_Type4 :
 365     register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 366     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 367     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 368     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 369     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 370     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 371     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 372     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 373 let register_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 =
 374   let hcut =
 375     register_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15
 376       h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33
 377       h34 h35 h36 h37 hterm
 378   in
 379   hcut __
 380
 381 (** val register_inv_rect_Type3 :
 382     register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 383     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 384     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 385     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 386     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 387     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 388     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 389     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 390 let register_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 =
 391   let hcut =
 392     register_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15
 393       h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33
 394       h34 h35 h36 h37 hterm
 395   in
 396   hcut __
 397
 398 (** val register_inv_rect_Type2 :
 399     register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 400     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 401     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 402     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 403     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 404     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 405     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 406     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 407 let register_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 =
 408   let hcut =
 409     register_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15
 410       h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33
 411       h34 h35 h36 h37 hterm
 412   in
 413   hcut __
 414
 415 (** val register_inv_rect_Type1 :
 416     register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 417     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 418     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 419     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 420     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 421     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 422     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 423     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 424 let register_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 =
 425   let hcut =
 426     register_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15
 427       h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33
 428       h34 h35 h36 h37 hterm
 429   in
 430   hcut __
 431
 432 (** val register_inv_rect_Type0 :
 433     register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 434     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 435     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 436     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 437     -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 438     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 439     -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 440     'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 441 let register_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 =
 442   let hcut =
 443     register_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15
 444       h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33
 445       h34 h35 h36 h37 hterm
 446   in
 447   hcut __
 448
 449 (** val register_discr : register -> register -> __ **)
 450 let register_discr x y =
 451   Logic.eq_rect_Type2 x
 452     (match x with
 453      | Register00 -> Obj.magic (fun _ dH -> dH)
 454      | Register01 -> Obj.magic (fun _ dH -> dH)
 455      | Register02 -> Obj.magic (fun _ dH -> dH)
 456      | Register03 -> Obj.magic (fun _ dH -> dH)
 457      | Register04 -> Obj.magic (fun _ dH -> dH)
 458      | Register05 -> Obj.magic (fun _ dH -> dH)
 459      | Register06 -> Obj.magic (fun _ dH -> dH)
 460      | Register07 -> Obj.magic (fun _ dH -> dH)
 461      | Register10 -> Obj.magic (fun _ dH -> dH)
 462      | Register11 -> Obj.magic (fun _ dH -> dH)
 463      | Register12 -> Obj.magic (fun _ dH -> dH)
 464      | Register13 -> Obj.magic (fun _ dH -> dH)
 465      | Register14 -> Obj.magic (fun _ dH -> dH)
 466      | Register15 -> Obj.magic (fun _ dH -> dH)
 467      | Register16 -> Obj.magic (fun _ dH -> dH)
 468      | Register17 -> Obj.magic (fun _ dH -> dH)
 469      | Register20 -> Obj.magic (fun _ dH -> dH)
 470      | Register21 -> Obj.magic (fun _ dH -> dH)
 471      | Register22 -> Obj.magic (fun _ dH -> dH)
 472      | Register23 -> Obj.magic (fun _ dH -> dH)
 473      | Register24 -> Obj.magic (fun _ dH -> dH)
 474      | Register25 -> Obj.magic (fun _ dH -> dH)
 475      | Register26 -> Obj.magic (fun _ dH -> dH)
 476      | Register27 -> Obj.magic (fun _ dH -> dH)
 477      | Register30 -> Obj.magic (fun _ dH -> dH)
 478      | Register31 -> Obj.magic (fun _ dH -> dH)
 479      | Register32 -> Obj.magic (fun _ dH -> dH)
 480      | Register33 -> Obj.magic (fun _ dH -> dH)
 481      | Register34 -> Obj.magic (fun _ dH -> dH)
 482      | Register35 -> Obj.magic (fun _ dH -> dH)
 483      | Register36 -> Obj.magic (fun _ dH -> dH)
 484      | Register37 -> Obj.magic (fun _ dH -> dH)
 485      | RegisterA -> Obj.magic (fun _ dH -> dH)
 486      | RegisterB -> Obj.magic (fun _ dH -> dH)
 487      | RegisterDPL -> Obj.magic (fun _ dH -> dH)
 488      | RegisterDPH -> Obj.magic (fun _ dH -> dH)
 489      | RegisterCarry -> Obj.magic (fun _ dH -> dH)) y
 490
 491 (** val register_jmdiscr : register -> register -> __ **)
 492 let register_jmdiscr x y =
 493   Logic.eq_rect_Type2 x
 494     (match x with
 495      | Register00 -> Obj.magic (fun _ dH -> dH)
 496      | Register01 -> Obj.magic (fun _ dH -> dH)
 497      | Register02 -> Obj.magic (fun _ dH -> dH)
 498      | Register03 -> Obj.magic (fun _ dH -> dH)
 499      | Register04 -> Obj.magic (fun _ dH -> dH)
 500      | Register05 -> Obj.magic (fun _ dH -> dH)
 501      | Register06 -> Obj.magic (fun _ dH -> dH)
 502      | Register07 -> Obj.magic (fun _ dH -> dH)
 503      | Register10 -> Obj.magic (fun _ dH -> dH)
 504      | Register11 -> Obj.magic (fun _ dH -> dH)
 505      | Register12 -> Obj.magic (fun _ dH -> dH)
 506      | Register13 -> Obj.magic (fun _ dH -> dH)
 507      | Register14 -> Obj.magic (fun _ dH -> dH)
 508      | Register15 -> Obj.magic (fun _ dH -> dH)
 509      | Register16 -> Obj.magic (fun _ dH -> dH)
 510      | Register17 -> Obj.magic (fun _ dH -> dH)
 511      | Register20 -> Obj.magic (fun _ dH -> dH)
 512      | Register21 -> Obj.magic (fun _ dH -> dH)
 513      | Register22 -> Obj.magic (fun _ dH -> dH)
 514      | Register23 -> Obj.magic (fun _ dH -> dH)
 515      | Register24 -> Obj.magic (fun _ dH -> dH)
 516      | Register25 -> Obj.magic (fun _ dH -> dH)
 517      | Register26 -> Obj.magic (fun _ dH -> dH)
 518      | Register27 -> Obj.magic (fun _ dH -> dH)
 519      | Register30 -> Obj.magic (fun _ dH -> dH)
 520      | Register31 -> Obj.magic (fun _ dH -> dH)
 521      | Register32 -> Obj.magic (fun _ dH -> dH)
 522      | Register33 -> Obj.magic (fun _ dH -> dH)
 523      | Register34 -> Obj.magic (fun _ dH -> dH)
 524      | Register35 -> Obj.magic (fun _ dH -> dH)
 525      | Register36 -> Obj.magic (fun _ dH -> dH)
 526      | Register37 -> Obj.magic (fun _ dH -> dH)
 527      | RegisterA -> Obj.magic (fun _ dH -> dH)
 528      | RegisterB -> Obj.magic (fun _ dH -> dH)
 529      | RegisterDPL -> Obj.magic (fun _ dH -> dH)
 530      | RegisterDPH -> Obj.magic (fun _ dH -> dH)
 531      | RegisterCarry -> Obj.magic (fun _ dH -> dH)) y
 532
 533 (** val nat_of_register : register -> Nat.nat **)
 534 let nat_of_register = function
 535 | Register00 -> Nat.O
 536 | Register01 -> Nat.S Nat.O
 537 | Register02 -> Nat.S (Nat.S Nat.O)
 538 | Register03 -> Nat.S (Nat.S (Nat.S Nat.O))
 539 | Register04 -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
 540 | Register05 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
 541 | Register06 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
 542 | Register07 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
 543 | Register10 ->
 544   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))
 545 | Register11 ->
 546   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
 547 | Register12 ->
 548   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 549     Nat.O)))))))))
 550 | Register13 ->
 551   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 552     Nat.O))))))))))
 553 | Register14 ->
 554   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 555     (Nat.S Nat.O)))))))))))
 556 | Register15 ->
 557   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 558     (Nat.S (Nat.S Nat.O))))))))))))
 559 | Register16 ->
 560   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 561     (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))
 562 | Register17 ->
 563   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 564     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))
 565 | Register20 ->
 566   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 567     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))
 568 | Register21 ->
 569   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 570     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))
 571 | Register22 ->
 572   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 573     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))
 574 | Register23 ->
 575   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 576     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 577     Nat.O))))))))))))))))))
 578 | Register24 ->
 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.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 581     Nat.O)))))))))))))))))))
 582 | Register25 ->
 583   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 584     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 585     Nat.O))))))))))))))))))))
 586 | Register26 ->
 587   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 588     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 589     (Nat.S Nat.O)))))))))))))))))))))
 590 | Register27 ->
 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.S (Nat.S (Nat.S
 593     (Nat.S (Nat.S Nat.O))))))))))))))))))))))
 594 | Register30 ->
 595   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 596     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 597     (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))))))
 598 | Register31 ->
 599   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 600     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 601     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))
 602 | Register32 ->
 603   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 604     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 605     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))))))))
 606 | Register33 ->
 607   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 608     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 609     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))))
 610 | Register34 ->
 611   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 612     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 613     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 614     Nat.O)))))))))))))))))))))))))))
 615 | Register35 ->
 616   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 617     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 618     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 619     Nat.O))))))))))))))))))))))))))))
 620 | Register36 ->
 621   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 622     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 623     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 624     Nat.O)))))))))))))))))))))))))))))
 625 | Register37 ->
 626   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 627     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 628     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 629     Nat.O))))))))))))))))))))))))))))))
 630 | RegisterA ->
 631   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 632     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 633     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 634     (Nat.S Nat.O)))))))))))))))))))))))))))))))
 635 | RegisterB ->
 636   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 637     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 638     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 639     (Nat.S (Nat.S Nat.O))))))))))))))))))))))))))))))))
 640 | RegisterDPL ->
 641   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 642     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 643     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 644     (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))))))))))))))))
 645 | RegisterDPH ->
 646   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 647     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 648     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 649     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))))))))))))
 650 | RegisterCarry ->
 651   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 652     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 653     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 654     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 655     Nat.O)))))))))))))))))))))))))))))))))))
 656
 657 (** val physical_register_count : Nat.nat **)
 658 let physical_register_count =
 659   Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 660     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 661     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 662     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 663     Nat.O)))))))))))))))))))))))))))))))))))
 664
 665 (** val bitvector_of_register : register -> BitVector.bitVector **)
 666 let bitvector_of_register register0 =
 667   Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 668     Nat.O)))))) (nat_of_register register0)
 669
 670 (** val eq_Register : register -> register -> Bool.bool **)
 671 let eq_Register r s =
 672   let r_as_nat = nat_of_register r in
 673   let s_as_nat = nat_of_register s in Nat.eqb r_as_nat s_as_nat
 674
 675 (** val registerSST : register **)
 676 let registerSST =
 677   Register10
 678
 679 (** val registerST0 : register **)
 680 let registerST0 =
 681   Register02
 682
 683 (** val registerST1 : register **)
 684 let registerST1 =
 685   Register03
 686
 687 (** val registerST2 : register **)
 688 let registerST2 =
 689   Register04
 690
 691 (** val registerST3 : register **)
 692 let registerST3 =
 693   Register05
 694
 695 (** val registerSTS : register List.list **)
 696 let registerSTS =
 697   List.Cons (registerST0, (List.Cons (registerST1, (List.Cons (registerST2,
 698     (List.Cons (registerST3, List.Nil)))))))
 699
 700 (** val registerSPL : register **)
 701 let registerSPL =
 702   Register06
 703
 704 (** val registerSPH : register **)
 705 let registerSPH =
 706   Register07
 707
 708 (** val registerParams : register List.list **)
 709 let registerParams =
 710   List.Cons (Register30, (List.Cons (Register31, (List.Cons (Register32,
 711     (List.Cons (Register33, (List.Cons (Register34, (List.Cons (Register35,
 712     (List.Cons (Register36, (List.Cons (Register37, List.Nil)))))))))))))))
 713
 714 (** val registers : register List.list **)
 715 let registers =
 716   List.Cons (Register00, (List.Cons (Register01, (List.Cons (Register02,
 717     (List.Cons (Register03, (List.Cons (Register04, (List.Cons (Register05,
 718     (List.Cons (Register06, (List.Cons (Register07, (List.Cons (Register10,
 719     (List.Cons (Register11, (List.Cons (Register12, (List.Cons (Register13,
 720     (List.Cons (Register14, (List.Cons (Register15, (List.Cons (Register16,
 721     (List.Cons (Register17, (List.Cons (Register20, (List.Cons (Register21,
 722     (List.Cons (Register22, (List.Cons (Register23, (List.Cons (Register24,
 723     (List.Cons (Register25, (List.Cons (Register26, (List.Cons (Register27,
 724     (List.Cons (Register30, (List.Cons (Register31, (List.Cons (Register32,
 725     (List.Cons (Register33, (List.Cons (Register34, (List.Cons (Register35,
 726     (List.Cons (Register36, (List.Cons (Register37, (List.Cons (RegisterA,
 727     (List.Cons (RegisterB, (List.Cons (RegisterDPL, (List.Cons (RegisterDPH,
 728     (List.Cons (registerSPL, (List.Cons (registerSPH, (List.Cons
 729     (registerST0, (List.Cons (registerST1, (List.Cons (registerSST,
 730     List.Nil)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 731
 732 (** val registerRets : register List.list **)
 733 let registerRets =
 734   List.Cons (RegisterDPL, (List.Cons (RegisterDPH, (List.Cons (Register00,
 735     (List.Cons (Register01, List.Nil)))))))
 736
 737 (** val registerCallerSaved : register List.list **)
 738 let registerCallerSaved =
 739   List.Cons (Register00, (List.Cons (Register01, (List.Cons (Register02,
 740     (List.Cons (Register03, (List.Cons (Register04, (List.Cons (Register05,
 741     (List.Cons (Register06, (List.Cons (Register07, (List.Cons (Register10,
 742     (List.Cons (Register11, (List.Cons (Register12, (List.Cons (Register13,
 743     (List.Cons (Register14, (List.Cons (Register15, (List.Cons (Register16,
 744     (List.Cons (Register17, (List.Cons (Register30, (List.Cons (Register31,
 745     (List.Cons (Register32, (List.Cons (Register33, (List.Cons (Register34,
 746     (List.Cons (Register35, (List.Cons (Register36, (List.Cons (Register37,
 747     List.Nil)))))))))))))))))))))))))))))))))))))))))))))))
 748
 749 (** val registerCalleeSaved : register List.list **)
 750 let registerCalleeSaved =
 751   List.Cons (Register20, (List.Cons (Register21, (List.Cons (Register22,
 752     (List.Cons (Register23, (List.Cons (Register24, (List.Cons (Register25,
 753     (List.Cons (Register26, (List.Cons (Register27, List.Nil)))))))))))))))
 754
 755 (** val registersForbidden : register List.list **)
 756 let registersForbidden =
 757   List.Cons (RegisterA, (List.Cons (RegisterB, (List.Cons (RegisterDPL,
 758     (List.Cons (RegisterDPH, (List.Cons (registerSPL, (List.Cons
 759     (registerSPH, (List.Cons (registerST0, (List.Cons (registerST1,
 760     (List.Cons (registerST2, (List.Cons (registerST3, (List.Cons
 761     (registerSST, List.Nil)))))))))))))))))))))
 762
 763 (** val registersAllocatable : register List.list **)
 764 let registersAllocatable =
 765   List.Cons (Register00, (List.Cons (Register01, (List.Cons (Register02,
 766     (List.Cons (Register03, (List.Cons (Register04, (List.Cons (Register05,
 767     (List.Cons (Register06, (List.Cons (Register07, (List.Cons (Register10,
 768     (List.Cons (Register11, (List.Cons (Register12, (List.Cons (Register13,
 769     (List.Cons (Register14, (List.Cons (Register15, (List.Cons (Register16,
 770     (List.Cons (Register17, (List.Cons (Register20, (List.Cons (Register21,
 771     (List.Cons (Register22, (List.Cons (Register23, (List.Cons (Register24,
 772     (List.Cons (Register25, (List.Cons (Register26, (List.Cons (Register27,
 773     (List.Cons (Register30, (List.Cons (Register31, (List.Cons (Register32,
 774     (List.Cons (Register33, (List.Cons (Register34, (List.Cons (Register35,
 775     (List.Cons (Register36, (List.Cons (Register37,
 776     List.Nil)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 777