extracted/lINToASM.ml

   1 open Preamble
   2
   3 open Deqsets
   4
   5 open Setoids
   6
   7 open Monad
   8
   9 open Option
  10
  11 open Extranat
  12
  13 open Vector
  14
  15 open Div_and_mod
  16
  17 open Jmeq
  18
  19 open Russell
  20
  21 open List
  22
  23 open Util
  24
  25 open FoldStuff
  26
  27 open Bool
  28
  29 open Relations
  30
  31 open Nat
  32
  33 open BitVector
  34
  35 open Hints_declaration
  36
  37 open Core_notation
  38
  39 open Pts
  40
  41 open Logic
  42
  43 open Types
  44
  45 open BitVectorTrie
  46
  47 open BitVectorTrieSet
  48
  49 open State
  50
  51 open String
  52
  53 open Exp
  54
  55 open Arithmetic
  56
  57 open Integers
  58
  59 open AST
  60
  61 open LabelledObjects
  62
  63 open Proper
  64
  65 open PositiveMap
  66
  67 open ErrorMessages
  68
  69 open PreIdentifiers
  70
  71 open Errors
  72
  73 open Extralib
  74
  75 open Lists
  76
  77 open Positive
  78
  79 open Identifiers
  80
  81 open CostLabel
  82
  83 open ASM
  84
  85 open Extra_bool
  86
  87 open Coqlib
  88
  89 open Values
  90
  91 open FrontEndVal
  92
  93 open GenMem
  94
  95 open FrontEndMem
  96
  97 open Globalenvs
  98
  99 open Sets
 100
 101 open Listb
 102
 103 open Graphs
 104
 105 open I8051
 106
 107 open Order
 108
 109 open Registers
 110
 111 open Hide
 112
 113 open Division
 114
 115 open Z
 116
 117 open BitVectorZ
 118
 119 open Pointers
 120
 121 open ByteValues
 122
 123 open BackEndOps
 124
 125 open Joint
 126
 127 open Joint_LTL_LIN
 128
 129 open LIN
 130
 131 type aSM_universe = { id_univ : Identifiers.universe;
 132                       current_funct : AST.ident;
 133                       ident_map : ASM.identifier Identifiers.identifier_map;
 134                       label_map : ASM.identifier Identifiers.identifier_map
 135                                   Identifiers.identifier_map;
 136                       fresh_cost_label : Positive.pos }
 137
 138 (** val aSM_universe_rect_Type4 :
 139     (Identifiers.universe -> AST.ident -> ASM.identifier
 140     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
 141     Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
 142 let rec aSM_universe_rect_Type4 h_mk_ASM_universe x_588 =
 143   let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
 144     ident_map0; label_map = label_map0; fresh_cost_label =
 145     fresh_cost_label0 } = x_588
 146   in
 147   h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
 148     fresh_cost_label0
 149
 150 (** val aSM_universe_rect_Type5 :
 151     (Identifiers.universe -> AST.ident -> ASM.identifier
 152     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
 153     Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
 154 let rec aSM_universe_rect_Type5 h_mk_ASM_universe x_590 =
 155   let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
 156     ident_map0; label_map = label_map0; fresh_cost_label =
 157     fresh_cost_label0 } = x_590
 158   in
 159   h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
 160     fresh_cost_label0
 161
 162 (** val aSM_universe_rect_Type3 :
 163     (Identifiers.universe -> AST.ident -> ASM.identifier
 164     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
 165     Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
 166 let rec aSM_universe_rect_Type3 h_mk_ASM_universe x_592 =
 167   let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
 168     ident_map0; label_map = label_map0; fresh_cost_label =
 169     fresh_cost_label0 } = x_592
 170   in
 171   h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
 172     fresh_cost_label0
 173
 174 (** val aSM_universe_rect_Type2 :
 175     (Identifiers.universe -> AST.ident -> ASM.identifier
 176     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
 177     Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
 178 let rec aSM_universe_rect_Type2 h_mk_ASM_universe x_594 =
 179   let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
 180     ident_map0; label_map = label_map0; fresh_cost_label =
 181     fresh_cost_label0 } = x_594
 182   in
 183   h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
 184     fresh_cost_label0
 185
 186 (** val aSM_universe_rect_Type1 :
 187     (Identifiers.universe -> AST.ident -> ASM.identifier
 188     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
 189     Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
 190 let rec aSM_universe_rect_Type1 h_mk_ASM_universe x_596 =
 191   let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
 192     ident_map0; label_map = label_map0; fresh_cost_label =
 193     fresh_cost_label0 } = x_596
 194   in
 195   h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
 196     fresh_cost_label0
 197
 198 (** val aSM_universe_rect_Type0 :
 199     (Identifiers.universe -> AST.ident -> ASM.identifier
 200     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
 201     Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
 202 let rec aSM_universe_rect_Type0 h_mk_ASM_universe x_598 =
 203   let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
 204     ident_map0; label_map = label_map0; fresh_cost_label =
 205     fresh_cost_label0 } = x_598
 206   in
 207   h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
 208     fresh_cost_label0
 209
 210 (** val id_univ : aSM_universe -> Identifiers.universe **)
 211 let rec id_univ xxx =
 212   xxx.id_univ
 213
 214 (** val current_funct : aSM_universe -> AST.ident **)
 215 let rec current_funct xxx =
 216   xxx.current_funct
 217
 218 (** val ident_map :
 219     aSM_universe -> ASM.identifier Identifiers.identifier_map **)
 220 let rec ident_map xxx =
 221   xxx.ident_map
 222
 223 (** val label_map :
 224     aSM_universe -> ASM.identifier Identifiers.identifier_map
 225     Identifiers.identifier_map **)
 226 let rec label_map xxx =
 227   xxx.label_map
 228
 229 (** val fresh_cost_label : aSM_universe -> Positive.pos **)
 230 let rec fresh_cost_label xxx =
 231   xxx.fresh_cost_label
 232
 233 (** val aSM_universe_inv_rect_Type4 :
 234     aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
 235     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
 236     Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1 **)
 237 let aSM_universe_inv_rect_Type4 hterm h1 =
 238   let hcut = aSM_universe_rect_Type4 h1 hterm in hcut __
 239
 240 (** val aSM_universe_inv_rect_Type3 :
 241     aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
 242     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
 243     Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1 **)
 244 let aSM_universe_inv_rect_Type3 hterm h1 =
 245   let hcut = aSM_universe_rect_Type3 h1 hterm in hcut __
 246
 247 (** val aSM_universe_inv_rect_Type2 :
 248     aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
 249     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
 250     Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1 **)
 251 let aSM_universe_inv_rect_Type2 hterm h1 =
 252   let hcut = aSM_universe_rect_Type2 h1 hterm in hcut __
 253
 254 (** val aSM_universe_inv_rect_Type1 :
 255     aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
 256     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
 257     Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1 **)
 258 let aSM_universe_inv_rect_Type1 hterm h1 =
 259   let hcut = aSM_universe_rect_Type1 h1 hterm in hcut __
 260
 261 (** val aSM_universe_inv_rect_Type0 :
 262     aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
 263     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
 264     Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1 **)
 265 let aSM_universe_inv_rect_Type0 hterm h1 =
 266   let hcut = aSM_universe_rect_Type0 h1 hterm in hcut __
 267
 268 (** val aSM_universe_discr : aSM_universe -> aSM_universe -> __ **)
 269 let aSM_universe_discr x y =
 270   Logic.eq_rect_Type2 x
 271     (let { id_univ = a0; current_funct = a1; ident_map = a2; label_map = a3;
 272        fresh_cost_label = a4 } = x
 273      in
 274     Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
 275
 276 (** val aSM_universe_jmdiscr : aSM_universe -> aSM_universe -> __ **)
 277 let aSM_universe_jmdiscr x y =
 278   Logic.eq_rect_Type2 x
 279     (let { id_univ = a0; current_funct = a1; ident_map = a2; label_map = a3;
 280        fresh_cost_label = a4 } = x
 281      in
 282     Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
 283
 284 (** val report_cost :
 285     CostLabel.costlabel -> Types.unit0 Monad.smax_def__o__monad **)
 286 let report_cost cl =
 287   Obj.magic (fun u ->
 288     let clw = Identifiers.word_of_identifier PreIdentifiers.CostTag cl in
 289     (match Positive.leb u.fresh_cost_label clw with
 290      | Bool.True ->
 291        { Types.fst = { id_univ = u.id_univ; current_funct = u.current_funct;
 292          ident_map = u.ident_map; label_map = u.label_map; fresh_cost_label =
 293          (Positive.succ clw) }; Types.snd = Types.It }
 294      | Bool.False -> { Types.fst = u; Types.snd = Types.It }))
 295
 296 (** val identifier_of_label :
 297     Graphs.label -> ASM.identifier Monad.smax_def__o__monad **)
 298 let identifier_of_label l =
 299   Obj.magic (fun u ->
 300     let current = u.current_funct in
 301     let lmap =
 302       Identifiers.lookup_def PreIdentifiers.SymbolTag u.label_map current
 303         (Identifiers.empty_map PreIdentifiers.LabelTag)
 304     in
 305     let { Types.fst = eta2825; Types.snd = lmap0 } =
 306       match Identifiers.lookup PreIdentifiers.LabelTag lmap l with
 307       | Types.None ->
 308         let { Types.fst = id; Types.snd = univ } =
 309           Identifiers.fresh PreIdentifiers.ASMTag u.id_univ
 310         in
 311         { Types.fst = { Types.fst = id; Types.snd = univ }; Types.snd =
 312         (Identifiers.add PreIdentifiers.LabelTag lmap l id) }
 313       | Types.Some id ->
 314         { Types.fst = { Types.fst = id; Types.snd = u.id_univ }; Types.snd =
 315           lmap }
 316     in
 317     let { Types.fst = id; Types.snd = univ } = eta2825 in
 318     { Types.fst = { id_univ = univ; current_funct = current; ident_map =
 319     u.ident_map; label_map =
 320     (Identifiers.add PreIdentifiers.SymbolTag u.label_map current lmap0);
 321     fresh_cost_label = u.fresh_cost_label }; Types.snd = id })
 322
 323 (** val identifier_of_ident :
 324     AST.ident -> ASM.identifier Monad.smax_def__o__monad **)
 325 let identifier_of_ident i =
 326   Obj.magic (fun u ->
 327     let imap = u.ident_map in
 328     let res =
 329       match Identifiers.lookup PreIdentifiers.SymbolTag imap i with
 330       | Types.None ->
 331         let { Types.fst = id; Types.snd = univ } =
 332           Identifiers.fresh PreIdentifiers.ASMTag u.id_univ
 333         in
 334         { Types.fst = { Types.fst = id; Types.snd = univ }; Types.snd =
 335         (Identifiers.add PreIdentifiers.SymbolTag imap i id) }
 336       | Types.Some id ->
 337         { Types.fst = { Types.fst = id; Types.snd = u.id_univ }; Types.snd =
 338           imap }
 339     in
 340     let id = res.Types.fst.Types.fst in
 341     let univ = res.Types.fst.Types.snd in
 342     let imap0 = res.Types.snd in
 343     { Types.fst = { id_univ = univ; current_funct = u.current_funct;
 344     ident_map = imap0; label_map = u.label_map; fresh_cost_label =
 345     u.fresh_cost_label }; Types.snd = id })
 346
 347 (** val new_ASM_universe : Joint.joint_program -> aSM_universe **)
 348 let new_ASM_universe p =
 349   { id_univ = Positive.One; current_funct = Positive.One; ident_map =
 350     (Identifiers.empty_map PreIdentifiers.SymbolTag); label_map =
 351     (Identifiers.empty_map PreIdentifiers.SymbolTag); fresh_cost_label =
 352     Positive.One }
 353
 354 (** val start_funct_translation :
 355     AST.ident List.list -> AST.ident List.list -> (AST.ident,
 356     Joint.joint_function) Types.prod -> Types.unit0 Monad.smax_def__o__monad **)
 357 let start_funct_translation g functs id_f =
 358   Obj.magic (fun u -> { Types.fst = { id_univ = u.id_univ; current_funct =
 359     id_f.Types.fst; ident_map = u.ident_map; label_map = u.label_map;
 360     fresh_cost_label = u.fresh_cost_label }; Types.snd = Types.It })
 361
 362 (** val aSM_fresh : ASM.identifier Monad.smax_def__o__monad **)
 363 let aSM_fresh =
 364   Obj.magic (fun u ->
 365     let { Types.fst = id; Types.snd = univ } =
 366       Identifiers.fresh PreIdentifiers.ASMTag u.id_univ
 367     in
 368     { Types.fst = { id_univ = univ; current_funct = u.current_funct;
 369     ident_map = u.ident_map; label_map = u.label_map; fresh_cost_label =
 370     u.fresh_cost_label }; Types.snd = id })
 371
 372 (** val register_address : I8051.register -> ASM.subaddressing_mode **)
 373 let register_address r =
 374   (match r with
 375    | I8051.Register00 ->
 376      (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
 377        (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
 378        Bool.False, Vector.VEmpty)))))))
 379    | I8051.Register01 ->
 380      (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
 381        (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
 382        Bool.True, Vector.VEmpty)))))))
 383    | I8051.Register02 ->
 384      (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
 385        (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
 386        Bool.False, Vector.VEmpty)))))))
 387    | I8051.Register03 ->
 388      (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
 389        (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
 390        Bool.True, Vector.VEmpty)))))))
 391    | I8051.Register04 ->
 392      (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
 393        (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
 394        Bool.False, Vector.VEmpty)))))))
 395    | I8051.Register05 ->
 396      (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
 397        (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
 398        Bool.True, Vector.VEmpty)))))))
 399    | I8051.Register06 ->
 400      (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
 401        (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
 402        Bool.False, Vector.VEmpty)))))))
 403    | I8051.Register07 ->
 404      (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
 405        (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
 406        Bool.True, Vector.VEmpty)))))))
 407    | I8051.Register10 ->
 408      (fun _ -> ASM.DIRECT
 409        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 410          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 411    | I8051.Register11 ->
 412      (fun _ -> ASM.DIRECT
 413        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 414          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 415    | I8051.Register12 ->
 416      (fun _ -> ASM.DIRECT
 417        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 418          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 419    | I8051.Register13 ->
 420      (fun _ -> ASM.DIRECT
 421        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 422          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 423    | I8051.Register14 ->
 424      (fun _ -> ASM.DIRECT
 425        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 426          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 427    | I8051.Register15 ->
 428      (fun _ -> ASM.DIRECT
 429        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 430          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 431    | I8051.Register16 ->
 432      (fun _ -> ASM.DIRECT
 433        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 434          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 435    | I8051.Register17 ->
 436      (fun _ -> ASM.DIRECT
 437        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 438          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 439    | I8051.Register20 ->
 440      (fun _ -> ASM.DIRECT
 441        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 442          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 443    | I8051.Register21 ->
 444      (fun _ -> ASM.DIRECT
 445        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 446          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 447    | I8051.Register22 ->
 448      (fun _ -> ASM.DIRECT
 449        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 450          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 451    | I8051.Register23 ->
 452      (fun _ -> ASM.DIRECT
 453        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 454          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 455    | I8051.Register24 ->
 456      (fun _ -> ASM.DIRECT
 457        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 458          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 459    | I8051.Register25 ->
 460      (fun _ -> ASM.DIRECT
 461        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 462          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 463    | I8051.Register26 ->
 464      (fun _ -> ASM.DIRECT
 465        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 466          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 467    | I8051.Register27 ->
 468      (fun _ -> ASM.DIRECT
 469        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 470          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 471    | I8051.Register30 ->
 472      (fun _ -> ASM.DIRECT
 473        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 474          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 475    | I8051.Register31 ->
 476      (fun _ -> ASM.DIRECT
 477        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 478          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 479    | I8051.Register32 ->
 480      (fun _ -> ASM.DIRECT
 481        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 482          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 483    | I8051.Register33 ->
 484      (fun _ -> ASM.DIRECT
 485        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 486          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 487    | I8051.Register34 ->
 488      (fun _ -> ASM.DIRECT
 489        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 490          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 491    | I8051.Register35 ->
 492      (fun _ -> ASM.DIRECT
 493        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 494          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 495    | I8051.Register36 ->
 496      (fun _ -> ASM.DIRECT
 497        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 498          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 499    | I8051.Register37 ->
 500      (fun _ -> ASM.DIRECT
 501        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 502          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
 503    | I8051.RegisterA -> (fun _ -> ASM.ACC_A)
 504    | I8051.RegisterB ->
 505      (fun _ -> ASM.DIRECT
 506        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 507          (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 508          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 509          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 510          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 511          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 512          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 513          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 514          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 515          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 516          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 517          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 518          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 519          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 520          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 521          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 522          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 523          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 524          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 525          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 526          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 527          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 528          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 529          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 530          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 531          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 532          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 533          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 534          (Nat.S
 535          Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 536    | I8051.RegisterDPL ->
 537      (fun _ -> ASM.DIRECT
 538        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 539          (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 540          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 541          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 542          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 543          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 544          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 545          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 546          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 547          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 548          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 549          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 550          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 551          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 552          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 553          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 554          Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 555    | I8051.RegisterDPH ->
 556      (fun _ -> ASM.DIRECT
 557        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 558          (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 559          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 560          (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.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 562          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 563          (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.S (Nat.S (Nat.S (Nat.S (Nat.S
 565          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 566          (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.S (Nat.S (Nat.S (Nat.S
 568          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 569          (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.S (Nat.S (Nat.S
 571          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 572          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 573          Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 574    | I8051.RegisterCarry ->
 575      (fun _ -> ASM.DIRECT
 576        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 577          (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))) __
 578
 579 (** val vector_cast :
 580     Nat.nat -> Nat.nat -> 'a1 -> 'a1 Vector.vector -> 'a1 Vector.vector **)
 581 let vector_cast n m dflt v =
 582   Util.if_then_else_safe (Nat.leb n m) (fun _ ->
 583     Vector.append (Nat.minus m n) n (Vector.replicate (Nat.minus m n) dflt) v)
 584     (fun _ -> (Vector.vsplit (Nat.minus n m) m v).Types.snd)
 585
 586 (** val arg_address : Joint.hdw_argument -> ASM.subaddressing_mode **)
 587 let arg_address = function
 588 | Joint.Reg r ->
 589   let x =
 590     ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S Nat.O))
 591       (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
 592       ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons
 593       (Nat.O, ASM.Registr, Vector.VEmpty)))))) (Vector.VCons ((Nat.S (Nat.S
 594       (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
 595       ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons
 596       (Nat.O, ASM.Data, Vector.VEmpty)))))))) (register_address r)
 597   in
 598   x
 599 | Joint.Imm v -> let x = ASM.DATA v in x
 600
 601 type lin_statement = Joint.joint_statement LabelledObjects.labelled_obj
 602
 603 (** val data_of_int : BitVector.byte -> ASM.addressing_mode **)
 604 let data_of_int bv =
 605   ASM.DATA bv
 606
 607 (** val data16_of_int : Nat.nat -> ASM.addressing_mode **)
 608 let data16_of_int bv =
 609   ASM.DATA16
 610     (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 611       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 612       Nat.O)))))))))))))))) bv)
 613
 614 (** val accumulator_address : ASM.addressing_mode **)
 615 let accumulator_address =
 616   ASM.DIRECT
 617     (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 618       (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 619       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 620       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 621       (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 (Nat.S
 624       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 625       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 626       (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.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 630       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 631       (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.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 635       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 636       (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.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 640       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 641       Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 642
 643 (** val asm_other_bit : ASM.addressing_mode **)
 644 let asm_other_bit =
 645   ASM.BIT_ADDR Joint.zero_byte
 646
 647 (** val one_word : BitVector.word **)
 648 let one_word =
 649   Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 650     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))
 651     (Nat.S Nat.O)
 652     (BitVector.zero (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.O))))))))))))))))
 654     (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty))
 655
 656 (** val translate_statements :
 657     AST.ident List.list -> Joint.joint_statement -> ASM.pseudo_instruction
 658     Monad.smax_def__o__monad **)
 659 let translate_statements globals = function
 660 | Joint.Sequential (instr, x) ->
 661   (match instr with
 662    | Joint.COST_LABEL lbl ->
 663      Monad.m_bind0 (Monad.smax_def State.state_monad) (report_cost lbl)
 664        (fun x0 ->
 665        Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Cost lbl))
 666    | Joint.CALL (f, x0, x1) ->
 667      (match f with
 668       | Types.Inl id ->
 669         Monad.m_bind0 (Monad.smax_def State.state_monad)
 670           (identifier_of_ident id) (fun id' ->
 671           Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Call
 672             (ASM.toASM_ident PreIdentifiers.ASMTag id')))
 673       | Types.Inr x2 ->
 674         Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
 675           (ASM.JMP ASM.ACC_DPTR)))
 676    | Joint.COND (x0, lbl) ->
 677      Monad.m_bind0 (Monad.smax_def State.state_monad)
 678        (identifier_of_label lbl) (fun l ->
 679        Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
 680          (ASM.JNZ l)))
 681    | Joint.Step_seq instr' ->
 682      (match instr' with
 683       | Joint.COMMENT comment ->
 684         Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Comment
 685           comment)
 686       | Joint.MOVE regs ->
 687         Monad.m_return0 (Monad.smax_def State.state_monad)
 688           (match Obj.magic regs with
 689            | Joint_LTL_LIN.From_acc (reg, x0) ->
 690              (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O))
 691                       (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a,
 692                       (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons
 693                       (Nat.O, ASM.Registr, Vector.VEmpty))))))
 694                       (register_address reg) with
 695               | ASM.DIRECT d ->
 696                 (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl
 697                   (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT d);
 698                   Types.snd = ASM.ACC_A }))))))
 699               | ASM.INDIRECT x1 -> (fun _ -> assert false (* absurd case *))
 700               | ASM.EXT_INDIRECT x1 ->
 701                 (fun _ -> assert false (* absurd case *))
 702               | ASM.REGISTER r ->
 703                 (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl
 704                   (Types.Inl (Types.Inl (Types.Inr { Types.fst =
 705                   (ASM.REGISTER r); Types.snd = ASM.ACC_A })))))))
 706               | ASM.ACC_A -> (fun _ -> ASM.Instruction ASM.NOP)
 707               | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
 708               | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
 709               | ASM.DATA x1 -> (fun _ -> assert false (* absurd case *))
 710               | ASM.DATA16 x1 -> (fun _ -> assert false (* absurd case *))
 711               | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
 712               | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
 713               | ASM.EXT_INDIRECT_DPTR ->
 714                 (fun _ -> assert false (* absurd case *))
 715               | ASM.INDIRECT_DPTR ->
 716                 (fun _ -> assert false (* absurd case *))
 717               | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
 718               | ASM.BIT_ADDR x1 -> (fun _ -> assert false (* absurd case *))
 719               | ASM.N_BIT_ADDR x1 ->
 720                 (fun _ -> assert false (* absurd case *))
 721               | ASM.RELATIVE x1 -> (fun _ -> assert false (* absurd case *))
 722               | ASM.ADDR11 x1 -> (fun _ -> assert false (* absurd case *))
 723               | ASM.ADDR16 x1 -> (fun _ -> assert false (* absurd case *)))
 724                __
 725            | Joint_LTL_LIN.To_acc (x0, reg) ->
 726              (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O))
 727                       (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a,
 728                       (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons
 729                       (Nat.O, ASM.Registr, Vector.VEmpty))))))
 730                       (register_address reg) with
 731               | ASM.DIRECT d ->
 732                 (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl
 733                   (Types.Inl (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A;
 734                   Types.snd = (ASM.DIRECT d) })))))))
 735               | ASM.INDIRECT x1 -> (fun _ -> assert false (* absurd case *))
 736               | ASM.EXT_INDIRECT x1 ->
 737                 (fun _ -> assert false (* absurd case *))
 738               | ASM.REGISTER r ->
 739                 (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl
 740                   (Types.Inl (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A;
 741                   Types.snd = (ASM.REGISTER r) })))))))
 742               | ASM.ACC_A -> (fun _ -> ASM.Instruction ASM.NOP)
 743               | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
 744               | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
 745               | ASM.DATA x1 -> (fun _ -> assert false (* absurd case *))
 746               | ASM.DATA16 x1 -> (fun _ -> assert false (* absurd case *))
 747               | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
 748               | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
 749               | ASM.EXT_INDIRECT_DPTR ->
 750                 (fun _ -> assert false (* absurd case *))
 751               | ASM.INDIRECT_DPTR ->
 752                 (fun _ -> assert false (* absurd case *))
 753               | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
 754               | ASM.BIT_ADDR x1 -> (fun _ -> assert false (* absurd case *))
 755               | ASM.N_BIT_ADDR x1 ->
 756                 (fun _ -> assert false (* absurd case *))
 757               | ASM.RELATIVE x1 -> (fun _ -> assert false (* absurd case *))
 758               | ASM.ADDR11 x1 -> (fun _ -> assert false (* absurd case *))
 759               | ASM.ADDR16 x1 -> (fun _ -> assert false (* absurd case *)))
 760                __
 761            | Joint_LTL_LIN.Int_to_reg (reg, b) ->
 762              (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O))
 763                       (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a,
 764                       (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons
 765                       (Nat.O, ASM.Registr, Vector.VEmpty))))))
 766                       (register_address reg) with
 767               | ASM.DIRECT d ->
 768                 (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl
 769                   (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT d);
 770                   Types.snd = (ASM.DATA b) }))))))
 771               | ASM.INDIRECT x0 -> (fun _ -> assert false (* absurd case *))
 772               | ASM.EXT_INDIRECT x0 ->
 773                 (fun _ -> assert false (* absurd case *))
 774               | ASM.REGISTER r ->
 775                 (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl
 776                   (Types.Inl (Types.Inl (Types.Inr { Types.fst =
 777                   (ASM.REGISTER r); Types.snd = (ASM.DATA b) })))))))
 778               | ASM.ACC_A ->
 779                 (fun _ ->
 780                   match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 781                           (Nat.S (Nat.S (Nat.S Nat.O))))))))
 782                           (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 783                             (Nat.S (Nat.S (Nat.S Nat.O))))))))) b with
 784                   | Bool.True -> ASM.Instruction (ASM.CLR ASM.ACC_A)
 785                   | Bool.False ->
 786                     ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl
 787                       (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A;
 788                       Types.snd = (ASM.DATA b) })))))))
 789               | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
 790               | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
 791               | ASM.DATA x0 -> (fun _ -> assert false (* absurd case *))
 792               | ASM.DATA16 x0 -> (fun _ -> assert false (* absurd case *))
 793               | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
 794               | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
 795               | ASM.EXT_INDIRECT_DPTR ->
 796                 (fun _ -> assert false (* absurd case *))
 797               | ASM.INDIRECT_DPTR ->
 798                 (fun _ -> assert false (* absurd case *))
 799               | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
 800               | ASM.BIT_ADDR x0 -> (fun _ -> assert false (* absurd case *))
 801               | ASM.N_BIT_ADDR x0 ->
 802                 (fun _ -> assert false (* absurd case *))
 803               | ASM.RELATIVE x0 -> (fun _ -> assert false (* absurd case *))
 804               | ASM.ADDR11 x0 -> (fun _ -> assert false (* absurd case *))
 805               | ASM.ADDR16 x0 -> (fun _ -> assert false (* absurd case *)))
 806                __
 807            | Joint_LTL_LIN.Int_to_acc (x0, b) ->
 808              (match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 809                       (Nat.S (Nat.S Nat.O))))))))
 810                       (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 811                         (Nat.S (Nat.S (Nat.S Nat.O))))))))) b with
 812               | Bool.True -> ASM.Instruction (ASM.CLR ASM.ACC_A)
 813               | Bool.False ->
 814                 ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl
 815                   (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
 816                   (ASM.DATA b) }))))))))
 817       | Joint.POP x0 ->
 818         Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
 819           (ASM.POP accumulator_address))
 820       | Joint.PUSH x0 ->
 821         Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
 822           (ASM.PUSH accumulator_address))
 823       | Joint.ADDRESS (id, off, x0, x1) ->
 824         Monad.m_bind0 (Monad.smax_def State.state_monad)
 825           (identifier_of_ident id) (fun id0 ->
 826           Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Mov
 827             ((Types.Inl ASM.DPTR), id0, off)))
 828       | Joint.OPACCS (accs, x0, x1, x2, x3) ->
 829         Monad.m_return0 (Monad.smax_def State.state_monad)
 830           (match accs with
 831            | BackEndOps.Mul ->
 832              ASM.Instruction (ASM.MUL (ASM.ACC_A, ASM.ACC_B))
 833            | BackEndOps.DivuModu ->
 834              ASM.Instruction (ASM.DIV (ASM.ACC_A, ASM.ACC_B)))
 835       | Joint.OP1 (op1, x0, x1) ->
 836         Monad.m_return0 (Monad.smax_def State.state_monad)
 837           (match op1 with
 838            | BackEndOps.Cmpl -> ASM.Instruction (ASM.CPL ASM.ACC_A)
 839            | BackEndOps.Inc -> ASM.Instruction (ASM.INC ASM.ACC_A)
 840            | BackEndOps.Rl -> ASM.Instruction (ASM.RL ASM.ACC_A))
 841       | Joint.OP2 (op2, x0, x1, reg) ->
 842         Monad.m_return0 (Monad.smax_def State.state_monad)
 843           ((match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
 844                     (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
 845                     (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct,
 846                     (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons
 847                     (Nat.O, ASM.Data, Vector.VEmpty))))))))
 848                     (arg_address (Obj.magic reg)) with
 849             | ASM.DIRECT d ->
 850               (fun _ ->
 851                 match op2 with
 852                 | BackEndOps.Add ->
 853                   ASM.Instruction (ASM.ADD (ASM.ACC_A, (ASM.DIRECT d)))
 854                 | BackEndOps.Addc ->
 855                   ASM.Instruction (ASM.ADDC (ASM.ACC_A, (ASM.DIRECT d)))
 856                 | BackEndOps.Sub ->
 857                   ASM.Instruction (ASM.SUBB (ASM.ACC_A, (ASM.DIRECT d)))
 858                 | BackEndOps.And ->
 859                   ASM.Instruction (ASM.ANL (Types.Inl (Types.Inl
 860                     { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT d) })))
 861                 | BackEndOps.Or ->
 862                   ASM.Instruction (ASM.ORL (Types.Inl (Types.Inl
 863                     { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT d) })))
 864                 | BackEndOps.Xor ->
 865                   ASM.Instruction (ASM.XRL (Types.Inl { Types.fst =
 866                     ASM.ACC_A; Types.snd = (ASM.DIRECT d) })))
 867             | ASM.INDIRECT x2 -> (fun _ -> assert false (* absurd case *))
 868             | ASM.EXT_INDIRECT x2 ->
 869               (fun _ -> assert false (* absurd case *))
 870             | ASM.REGISTER r ->
 871               (fun _ ->
 872                 match op2 with
 873                 | BackEndOps.Add ->
 874                   ASM.Instruction (ASM.ADD (ASM.ACC_A, (ASM.REGISTER r)))
 875                 | BackEndOps.Addc ->
 876                   ASM.Instruction (ASM.ADDC (ASM.ACC_A, (ASM.REGISTER r)))
 877                 | BackEndOps.Sub ->
 878                   ASM.Instruction (ASM.SUBB (ASM.ACC_A, (ASM.REGISTER r)))
 879                 | BackEndOps.And ->
 880                   ASM.Instruction (ASM.ANL (Types.Inl (Types.Inl
 881                     { Types.fst = ASM.ACC_A; Types.snd = (ASM.REGISTER
 882                     r) })))
 883                 | BackEndOps.Or ->
 884                   ASM.Instruction (ASM.ORL (Types.Inl (Types.Inl
 885                     { Types.fst = ASM.ACC_A; Types.snd = (ASM.REGISTER
 886                     r) })))
 887                 | BackEndOps.Xor ->
 888                   ASM.Instruction (ASM.XRL (Types.Inl { Types.fst =
 889                     ASM.ACC_A; Types.snd = (ASM.REGISTER r) })))
 890             | ASM.ACC_A ->
 891               (fun _ ->
 892                 match op2 with
 893                 | BackEndOps.Add ->
 894                   ASM.Instruction (ASM.ADD (ASM.ACC_A, accumulator_address))
 895                 | BackEndOps.Addc ->
 896                   ASM.Instruction (ASM.ADDC (ASM.ACC_A, accumulator_address))
 897                 | BackEndOps.Sub ->
 898                   ASM.Instruction (ASM.SUBB (ASM.ACC_A, accumulator_address))
 899                 | BackEndOps.And -> ASM.Instruction ASM.NOP
 900                 | BackEndOps.Or -> ASM.Instruction ASM.NOP
 901                 | BackEndOps.Xor -> ASM.Instruction (ASM.CLR ASM.ACC_A))
 902             | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
 903             | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
 904             | ASM.DATA b ->
 905               (fun _ ->
 906                 match op2 with
 907                 | BackEndOps.Add ->
 908                   ASM.Instruction (ASM.ADD (ASM.ACC_A, (ASM.DATA b)))
 909                 | BackEndOps.Addc ->
 910                   ASM.Instruction (ASM.ADDC (ASM.ACC_A, (ASM.DATA b)))
 911                 | BackEndOps.Sub ->
 912                   ASM.Instruction (ASM.SUBB (ASM.ACC_A, (ASM.DATA b)))
 913                 | BackEndOps.And ->
 914                   ASM.Instruction (ASM.ANL (Types.Inl (Types.Inl
 915                     { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA b) })))
 916                 | BackEndOps.Or ->
 917                   ASM.Instruction (ASM.ORL (Types.Inl (Types.Inl
 918                     { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA b) })))
 919                 | BackEndOps.Xor ->
 920                   ASM.Instruction (ASM.XRL (Types.Inl { Types.fst =
 921                     ASM.ACC_A; Types.snd = (ASM.DATA b) })))
 922             | ASM.DATA16 x2 -> (fun _ -> assert false (* absurd case *))
 923             | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
 924             | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
 925             | ASM.EXT_INDIRECT_DPTR ->
 926               (fun _ -> assert false (* absurd case *))
 927             | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 928             | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
 929             | ASM.BIT_ADDR x2 -> (fun _ -> assert false (* absurd case *))
 930             | ASM.N_BIT_ADDR x2 -> (fun _ -> assert false (* absurd case *))
 931             | ASM.RELATIVE x2 -> (fun _ -> assert false (* absurd case *))
 932             | ASM.ADDR11 x2 -> (fun _ -> assert false (* absurd case *))
 933             | ASM.ADDR16 x2 -> (fun _ -> assert false (* absurd case *))) __)
 934       | Joint.CLEAR_CARRY ->
 935         Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
 936           (ASM.CLR ASM.CARRY))
 937       | Joint.SET_CARRY ->
 938         Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
 939           (ASM.SETB ASM.CARRY))
 940       | Joint.LOAD (x0, x1, x2) ->
 941         Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
 942           (ASM.MOVX (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
 943           ASM.EXT_INDIRECT_DPTR })))
 944       | Joint.STORE (x0, x1, x2) ->
 945         Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
 946           (ASM.MOVX (Types.Inr { Types.fst = ASM.EXT_INDIRECT_DPTR;
 947           Types.snd = ASM.ACC_A })))
 948       | Joint.Extension_seq ext ->
 949         (match Obj.magic ext with
 950          | Joint_LTL_LIN.SAVE_CARRY ->
 951            Monad.m_return0 (Monad.smax_def State.state_monad)
 952              (ASM.Instruction (ASM.MOV (Types.Inr { Types.fst =
 953              asm_other_bit; Types.snd = ASM.CARRY })))
 954          | Joint_LTL_LIN.RESTORE_CARRY ->
 955            Monad.m_return0 (Monad.smax_def State.state_monad)
 956              (ASM.Instruction (ASM.MOV (Types.Inl (Types.Inr { Types.fst =
 957              ASM.CARRY; Types.snd = asm_other_bit }))))
 958          | Joint_LTL_LIN.LOW_ADDRESS lbl ->
 959            Monad.m_bind0 (Monad.smax_def State.state_monad)
 960              (identifier_of_label lbl) (fun lbl' ->
 961              Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Mov
 962                ((Types.Inr { Types.fst = (register_address I8051.RegisterA);
 963                Types.snd = ASM.LOW }), lbl', one_word)))
 964          | Joint_LTL_LIN.HIGH_ADDRESS lbl ->
 965            Monad.m_bind0 (Monad.smax_def State.state_monad)
 966              (identifier_of_label lbl) (fun lbl' ->
 967              Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Mov
 968                ((Types.Inr { Types.fst = (register_address I8051.RegisterA);
 969                Types.snd = ASM.HIGH }), lbl', one_word))))))
 970 | Joint.Final instr ->
 971   (match instr with
 972    | Joint.GOTO lbl ->
 973      Monad.m_bind0 (Monad.smax_def State.state_monad)
 974        (identifier_of_label lbl) (fun lbl' ->
 975        Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Jmp
 976          (ASM.toASM_ident PreIdentifiers.ASMTag lbl')))
 977    | Joint.RETURN ->
 978      Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
 979        ASM.RET)
 980    | Joint.TAILCALL (x, x0) -> assert false (* absurd case *))
 981 | Joint.FCOND (x0, lbl_true, lbl_false) ->
 982   Monad.m_bind0 (Monad.smax_def State.state_monad)
 983     (identifier_of_label lbl_true) (fun l1 ->
 984     Monad.m_bind0 (Monad.smax_def State.state_monad)
 985       (identifier_of_label lbl_false) (fun l2 ->
 986       Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Jnz (ASM.ACC_A,
 987         l1, l2))))
 988
 989 (** val build_translated_statement :
 990     AST.ident List.list -> lin_statement -> __ **)
 991 let build_translated_statement globals statement =
 992   Monad.m_bind0 (Monad.smax_def State.state_monad)
 993     (translate_statements globals statement.Types.snd) (fun stmt ->
 994     match statement.Types.fst with
 995     | Types.None ->
 996       Monad.m_return0 (Monad.smax_def State.state_monad) { Types.fst =
 997         Types.None; Types.snd = stmt }
 998     | Types.Some lbl ->
 999       Monad.m_bind0 (Monad.smax_def State.state_monad)
1000         (identifier_of_label lbl) (fun lbl' ->
1001         Monad.m_return0 (Monad.smax_def State.state_monad) { Types.fst =
1002           (Types.Some lbl'); Types.snd = stmt }))
1003
1004 (** val translate_code :
1005     AST.ident List.list -> lin_statement List.list -> __ **)
1006 let translate_code globals code =
1007   Monad.m_list_map (Monad.smax_def State.state_monad)
1008     (build_translated_statement globals) code
1009
1010 (** val translate_fun_def :
1011     AST.ident List.list -> AST.ident List.list -> (AST.ident,
1012     Joint.joint_function) Types.prod -> __ **)
1013 let translate_fun_def globals functions id_def =
1014   Monad.m_bind0 (Monad.smax_def State.state_monad)
1015     (start_funct_translation globals functions id_def) (fun x ->
1016     match id_def.Types.snd with
1017     | AST.Internal int ->
1018       let code = (Types.pi1 int).Joint.joint_if_code in
1019       Monad.m_bind0 (Monad.smax_def State.state_monad)
1020         (identifier_of_ident id_def.Types.fst) (fun id ->
1021         Monad.m_bind0 (Monad.smax_def State.state_monad)
1022           (translate_code (List.append functions globals) (Obj.magic code))
1023           (fun code' ->
1024           match code' with
1025           | List.Nil ->
1026             Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons
1027               ({ Types.fst = (Types.Some id); Types.snd = (ASM.Instruction
1028               ASM.RET) }, List.Nil))
1029           | List.Cons (hd, tl) ->
1030             (match hd.Types.fst with
1031              | Types.None ->
1032                Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons
1033                  ({ Types.fst = (Types.Some id); Types.snd = hd.Types.snd },
1034                  tl))
1035              | Types.Some x0 ->
1036                Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons
1037                  ({ Types.fst = (Types.Some id); Types.snd = (ASM.Instruction
1038                  ASM.NOP) }, (List.Cons (hd, tl)))))))
1039     | AST.External x0 ->
1040       Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil)
1041
1042 type init_mutable = { virtual_dptr : (ASM.identifier, Z.z) Types.prod;
1043                       actual_dptr : (ASM.identifier, Z.z) Types.prod;
1044                       built_code : ASM.labelled_instruction List.list
1045                                    List.list;
1046                       built_preamble : (ASM.identifier, BitVector.word)
1047                                        Types.prod List.list }
1048
1049 (** val init_mutable_rect_Type4 :
1050     ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
1051     ASM.labelled_instruction List.list List.list -> (ASM.identifier,
1052     BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
1053 let rec init_mutable_rect_Type4 h_mk_init_mutable x_614 =
1054   let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
1055     built_code = built_code0; built_preamble = built_preamble0 } = x_614
1056   in
1057   h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
1058
1059 (** val init_mutable_rect_Type5 :
1060     ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
1061     ASM.labelled_instruction List.list List.list -> (ASM.identifier,
1062     BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
1063 let rec init_mutable_rect_Type5 h_mk_init_mutable x_616 =
1064   let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
1065     built_code = built_code0; built_preamble = built_preamble0 } = x_616
1066   in
1067   h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
1068
1069 (** val init_mutable_rect_Type3 :
1070     ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
1071     ASM.labelled_instruction List.list List.list -> (ASM.identifier,
1072     BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
1073 let rec init_mutable_rect_Type3 h_mk_init_mutable x_618 =
1074   let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
1075     built_code = built_code0; built_preamble = built_preamble0 } = x_618
1076   in
1077   h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
1078
1079 (** val init_mutable_rect_Type2 :
1080     ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
1081     ASM.labelled_instruction List.list List.list -> (ASM.identifier,
1082     BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
1083 let rec init_mutable_rect_Type2 h_mk_init_mutable x_620 =
1084   let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
1085     built_code = built_code0; built_preamble = built_preamble0 } = x_620
1086   in
1087   h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
1088
1089 (** val init_mutable_rect_Type1 :
1090     ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
1091     ASM.labelled_instruction List.list List.list -> (ASM.identifier,
1092     BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
1093 let rec init_mutable_rect_Type1 h_mk_init_mutable x_622 =
1094   let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
1095     built_code = built_code0; built_preamble = built_preamble0 } = x_622
1096   in
1097   h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
1098
1099 (** val init_mutable_rect_Type0 :
1100     ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
1101     ASM.labelled_instruction List.list List.list -> (ASM.identifier,
1102     BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
1103 let rec init_mutable_rect_Type0 h_mk_init_mutable x_624 =
1104   let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
1105     built_code = built_code0; built_preamble = built_preamble0 } = x_624
1106   in
1107   h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
1108
1109 (** val virtual_dptr : init_mutable -> (ASM.identifier, Z.z) Types.prod **)
1110 let rec virtual_dptr xxx =
1111   xxx.virtual_dptr
1112
1113 (** val actual_dptr : init_mutable -> (ASM.identifier, Z.z) Types.prod **)
1114 let rec actual_dptr xxx =
1115   xxx.actual_dptr
1116
1117 (** val built_code :
1118     init_mutable -> ASM.labelled_instruction List.list List.list **)
1119 let rec built_code xxx =
1120   xxx.built_code
1121
1122 (** val built_preamble :
1123     init_mutable -> (ASM.identifier, BitVector.word) Types.prod List.list **)
1124 let rec built_preamble xxx =
1125   xxx.built_preamble
1126
1127 (** val init_mutable_inv_rect_Type4 :
1128     init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier,
1129     Z.z) Types.prod -> ASM.labelled_instruction List.list List.list ->
1130     (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
1131     'a1 **)
1132 let init_mutable_inv_rect_Type4 hterm h1 =
1133   let hcut = init_mutable_rect_Type4 h1 hterm in hcut __
1134
1135 (** val init_mutable_inv_rect_Type3 :
1136     init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier,
1137     Z.z) Types.prod -> ASM.labelled_instruction List.list List.list ->
1138     (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
1139     'a1 **)
1140 let init_mutable_inv_rect_Type3 hterm h1 =
1141   let hcut = init_mutable_rect_Type3 h1 hterm in hcut __
1142
1143 (** val init_mutable_inv_rect_Type2 :
1144     init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier,
1145     Z.z) Types.prod -> ASM.labelled_instruction List.list List.list ->
1146     (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
1147     'a1 **)
1148 let init_mutable_inv_rect_Type2 hterm h1 =
1149   let hcut = init_mutable_rect_Type2 h1 hterm in hcut __
1150
1151 (** val init_mutable_inv_rect_Type1 :
1152     init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier,
1153     Z.z) Types.prod -> ASM.labelled_instruction List.list List.list ->
1154     (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
1155     'a1 **)
1156 let init_mutable_inv_rect_Type1 hterm h1 =
1157   let hcut = init_mutable_rect_Type1 h1 hterm in hcut __
1158
1159 (** val init_mutable_inv_rect_Type0 :
1160     init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier,
1161     Z.z) Types.prod -> ASM.labelled_instruction List.list List.list ->
1162     (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
1163     'a1 **)
1164 let init_mutable_inv_rect_Type0 hterm h1 =
1165   let hcut = init_mutable_rect_Type0 h1 hterm in hcut __
1166
1167 (** val init_mutable_discr : init_mutable -> init_mutable -> __ **)
1168 let init_mutable_discr x y =
1169   Logic.eq_rect_Type2 x
1170     (let { virtual_dptr = a0; actual_dptr = a1; built_code = a2;
1171        built_preamble = a3 } = x
1172      in
1173     Obj.magic (fun _ dH -> dH __ __ __ __)) y
1174
1175 (** val init_mutable_jmdiscr : init_mutable -> init_mutable -> __ **)
1176 let init_mutable_jmdiscr x y =
1177   Logic.eq_rect_Type2 x
1178     (let { virtual_dptr = a0; actual_dptr = a1; built_code = a2;
1179        built_preamble = a3 } = x
1180      in
1181     Obj.magic (fun _ dH -> dH __ __ __ __)) y
1182
1183 (** val store_byte_or_Identifier :
1184     (BitVector.byte, (ASM.word_side, ASM.identifier) Types.prod) Types.sum ->
1185     init_mutable -> init_mutable **)
1186 let store_byte_or_Identifier by mut =
1187   let { virtual_dptr = virt; actual_dptr = act; built_code = acc1;
1188     built_preamble = acc2 } = mut
1189   in
1190   let pre =
1191     match Identifiers.eq_identifier PreIdentifiers.ASMTag virt.Types.fst
1192             act.Types.fst with
1193     | Bool.True ->
1194       let off = Z.zminus virt.Types.snd act.Types.snd in
1195       (match Z.eqZb off Z.OZ with
1196        | Bool.True -> List.Nil
1197        | Bool.False ->
1198          (match Z.eqZb off (Z.z_of_nat (Nat.S Nat.O)) with
1199           | Bool.True ->
1200             List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction
1201               (ASM.INC ASM.DPTR)) }, List.Nil)
1202           | Bool.False ->
1203             List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Mov
1204               ((Types.Inl ASM.DPTR), virt.Types.fst,
1205               (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1206                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1207                 (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) virt.Types.snd))) },
1208               List.Nil)))
1209     | Bool.False ->
1210       List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Mov ((Types.Inl
1211         ASM.DPTR), virt.Types.fst,
1212         (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1213           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1214           (Nat.S Nat.O)))))))))))))))) virt.Types.snd))) }, List.Nil)
1215   in
1216   let post =
1217     match by with
1218     | Types.Inl by0 ->
1219       { Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.MOV
1220         (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inl { Types.fst =
1221         ASM.ACC_A; Types.snd = (ASM.DATA by0) }))))))) }
1222     | Types.Inr si_id ->
1223       { Types.fst = Types.None; Types.snd = (ASM.Mov ((Types.Inr
1224         { Types.fst = ASM.ACC_A; Types.snd = si_id.Types.fst }),
1225         si_id.Types.snd,
1226         (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1227           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1228           Nat.O))))))))))))))))))) }
1229   in
1230   { virtual_dptr = { Types.fst = virt.Types.fst; Types.snd =
1231   (Z.zsucc virt.Types.snd) }; actual_dptr = virt; built_code = (List.Cons
1232   ((List.append pre (List.Cons (post, (List.Cons ({ Types.fst = Types.None;
1233      Types.snd = (ASM.Instruction (ASM.MOVX (Types.Inr { Types.fst =
1234      ASM.EXT_INDIRECT_DPTR; Types.snd = ASM.ACC_A }))) }, List.Nil))))),
1235   acc1)); built_preamble = acc2 }
1236
1237 (** val do_store_init_data :
1238     init_mutable Monad.smax_def__o__monad -> AST.init_data -> init_mutable
1239     Monad.smax_def__o__monad **)
1240 let do_store_init_data m_mut data =
1241   Monad.m_bind0 (Monad.smax_def State.state_monad) m_mut (fun mut ->
1242     let store_byte = fun by -> store_byte_or_Identifier (Types.Inl by) in
1243     let store_Identifier = fun side id ->
1244       store_byte_or_Identifier (Types.Inr { Types.fst = side; Types.snd =
1245         id })
1246     in
1247     (match data with
1248      | AST.Init_int8 n ->
1249        Monad.m_return0 (Monad.smax_def State.state_monad) (store_byte n mut)
1250      | AST.Init_int16 n ->
1251        let { Types.fst = by0; Types.snd = by1 } =
1252          Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1253            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1254            (Nat.S (Nat.S Nat.O)))))))) n
1255        in
1256        Monad.m_return0 (Monad.smax_def State.state_monad)
1257          (store_byte by1 (store_byte by0 mut))
1258      | AST.Init_int32 n ->
1259        let { Types.fst = by0; Types.snd = n0 } =
1260          Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1261            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1262            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1263            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1264            Nat.O)))))))))))))))))))))))) n
1265        in
1266        let { Types.fst = by1; Types.snd = n1 } =
1267          Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1268            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (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
1270            (Nat.S Nat.O)))))))))))))))) n0
1271        in
1272        let { Types.fst = by2; Types.snd = by3 } =
1273          Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1274            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1275            (Nat.S (Nat.S Nat.O)))))))) n1
1276        in
1277        Monad.m_return0 (Monad.smax_def State.state_monad)
1278          (store_byte by3
1279            (store_byte by2 (store_byte by1 (store_byte by0 mut))))
1280      | AST.Init_space n ->
1281        let { Types.fst = virt_id; Types.snd = virt_off } = mut.virtual_dptr
1282        in
1283        Monad.m_return0 (Monad.smax_def State.state_monad) { virtual_dptr =
1284          { Types.fst = virt_id; Types.snd =
1285          (Z.zplus (Z.z_of_nat n) virt_off) }; actual_dptr = mut.actual_dptr;
1286          built_code = mut.built_code; built_preamble = mut.built_preamble }
1287      | AST.Init_null ->
1288        let z =
1289          BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1290            (Nat.S Nat.O))))))))
1291        in
1292        Monad.m_return0 (Monad.smax_def State.state_monad)
1293          (store_byte z (store_byte z mut))
1294      | AST.Init_addrof (symb, ofs) ->
1295        Monad.m_bind0 (Monad.smax_def State.state_monad)
1296          (identifier_of_ident symb) (fun id ->
1297          Monad.m_return0 (Monad.smax_def State.state_monad)
1298            (store_Identifier ASM.HIGH id (store_Identifier ASM.LOW id mut)))))
1299
1300 (** val do_store_global :
1301     init_mutable Monad.smax_def__o__monad -> ((AST.ident, AST.region)
1302     Types.prod, AST.init_data List.list) Types.prod -> init_mutable
1303     Monad.smax_def__o__monad **)
1304 let do_store_global m_mut id_reg_data =
1305   Monad.m_bind0 (Monad.smax_def State.state_monad) m_mut (fun mut ->
1306     let { Types.fst = eta2842; Types.snd = data } = id_reg_data in
1307     let { Types.fst = id; Types.snd = reg } = eta2842 in
1308     Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_ident id)
1309       (fun id0 ->
1310       let mut0 = { virtual_dptr = { Types.fst = id0; Types.snd = Z.OZ };
1311         actual_dptr = mut.actual_dptr; built_code = mut.built_code;
1312         built_preamble = (List.Cons ({ Types.fst = id0; Types.snd =
1313         (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1314           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1315           (Nat.S (Nat.S Nat.O))))))))))))))))
1316           (Globalenvs.size_init_data_list data)) }, mut.built_preamble)) }
1317       in
1318       Util.foldl do_store_init_data
1319         (Monad.m_return0 (Monad.smax_def State.state_monad) mut0) data))
1320
1321 (** val reversed_flatten_aux :
1322     'a1 List.list -> 'a1 List.list List.list -> 'a1 List.list **)
1323 let rec reversed_flatten_aux acc = function
1324 | List.Nil -> acc
1325 | List.Cons (hd, tl) -> reversed_flatten_aux (List.append hd acc) tl
1326
1327 (** val translate_premain :
1328     LIN.lin_program -> ASM.identifier -> (ASM.labelled_instruction List.list,
1329     (ASM.identifier, BitVector.word) Types.prod List.list) Types.prod
1330     Monad.smax_def__o__monad **)
1331 let translate_premain p exit_label =
1332   Monad.m_bind0 (Monad.smax_def State.state_monad)
1333     (identifier_of_ident p.Joint.joint_prog.AST.prog_main) (fun main ->
1334     Monad.m_bind0 (Monad.smax_def State.state_monad) State.state_get
1335       (fun u ->
1336       let dummy_dptr = { Types.fst = Positive.One; Types.snd =
1337         (Z.zopp (Z.z_of_nat (Nat.S Nat.O))) }
1338       in
1339       let mut = { virtual_dptr = dummy_dptr; actual_dptr = dummy_dptr;
1340         built_code = List.Nil; built_preamble = List.Nil }
1341       in
1342       Monad.m_bind0 (Monad.smax_def State.state_monad)
1343         (Util.foldl do_store_global
1344           (Monad.m_return0 (Monad.smax_def State.state_monad) mut)
1345           p.Joint.joint_prog.AST.prog_vars) (fun globals_init ->
1346         let { Types.fst = sph; Types.snd = spl } =
1347           Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1348             (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1349             (Nat.S (Nat.S Nat.O))))))))
1350             (BitVectorZ.bitvector_of_Z
1351               (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1352                 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1353                 (Nat.S (Nat.S (Nat.S Nat.O)))))))))
1354               (Z.zopp
1355                 (Z.z_of_nat (Nat.S
1356                   (Joint.globals_stacksize
1357                     (Joint.lin_params_to_params LIN.lIN) p)))))
1358         in
1359         let init_isp = ASM.DATA
1360           (Vector.append (Nat.S (Nat.S Nat.O))
1361             (Nat.plus (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S
1362               Nat.O))))) (BitVector.zero (Nat.S (Nat.S Nat.O)))
1363             (Vector.append (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S
1364               Nat.O)))) (Vector.VCons ((Nat.S Nat.O), Bool.True,
1365               (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty))))
1366               (BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))
1367         in
1368         let isp_direct = ASM.DIRECT
1369           (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1370             Nat.O))))))) (Nat.S Nat.O) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1371             (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1372             (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1373               Nat.O))))))))) (Vector.VCons (Nat.O, Bool.True,
1374             Vector.VEmpty)))
1375         in
1376         let reg_spl = ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1377           Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons
1378           (Nat.O, Bool.False, Vector.VEmpty))))))
1379         in
1380         let reg_sph = ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1381           Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons
1382           (Nat.O, Bool.True, Vector.VEmpty))))))
1383         in
1384         Monad.m_return0 (Monad.smax_def State.state_monad) { Types.fst =
1385           (List.append (List.Cons ({ Types.fst = Types.None; Types.snd =
1386             (ASM.Cost p.Joint.init_cost_label) }, (List.Cons ({ Types.fst =
1387             Types.None; Types.snd = (ASM.Instruction (ASM.MOV (Types.Inl
1388             (Types.Inl (Types.Inl (Types.Inr { Types.fst = isp_direct;
1389             Types.snd = init_isp })))))) }, (List.Cons ({ Types.fst =
1390             Types.None; Types.snd = (ASM.Instruction (ASM.MOV (Types.Inl
1391             (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst =
1392             reg_spl; Types.snd = (ASM.DATA spl) }))))))) }, (List.Cons
1393             ({ Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.MOV
1394             (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr
1395             { Types.fst = reg_sph; Types.snd = (ASM.DATA sph) }))))))) },
1396             List.Nil))))))))
1397             (List.append
1398               (reversed_flatten_aux List.Nil globals_init.built_code)
1399               (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Call
1400               main) }, (List.Cons ({ Types.fst = (Types.Some exit_label);
1401               Types.snd = (ASM.Cost u.fresh_cost_label) }, (List.Cons
1402               ({ Types.fst = Types.None; Types.snd = (ASM.Jmp exit_label) },
1403               List.Nil)))))))); Types.snd = globals_init.built_preamble })))
1404
1405 (** val get_symboltable :
1406     (ASM.identifier, AST.ident) Types.prod List.list Monad.smax_def__o__monad **)
1407 let get_symboltable =
1408   Obj.magic (fun u ->
1409     let imap = u.ident_map in
1410     let f = fun iold inew x -> List.Cons ({ Types.fst = inew; Types.snd =
1411       iold }, x)
1412     in
1413     { Types.fst = u; Types.snd =
1414     (Identifiers.foldi PreIdentifiers.SymbolTag f imap List.Nil) })
1415
1416 (** val lin_to_asm :
1417     LIN.lin_program -> ASM.pseudo_assembly_program Types.option **)
1418 let lin_to_asm p =
1419   State.state_run (new_ASM_universe p)
1420     (let add_translation = fun acc id_def ->
1421        Monad.m_bind0 (Monad.smax_def State.state_monad)
1422          (translate_fun_def p.Joint.jp_functions
1423            (List.map (fun x -> x.Types.fst.Types.fst)
1424              p.Joint.joint_prog.AST.prog_vars) id_def) (fun code ->
1425          Monad.m_bind0 (Monad.smax_def State.state_monad) acc (fun acc0 ->
1426            Monad.m_return0 (Monad.smax_def State.state_monad)
1427              (List.append code acc0)))
1428      in
1429     Monad.m_bind0 (Monad.smax_def State.state_monad) aSM_fresh
1430       (fun exit_label ->
1431       Monad.m_bind0 (Monad.smax_def State.state_monad)
1432         (Util.foldl add_translation
1433           (Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil)
1434           p.Joint.joint_prog.AST.prog_funct) (fun code ->
1435         Monad.m_bind0 (Monad.smax_def State.state_monad) get_symboltable
1436           (fun symboltable ->
1437           Monad.m_bind2 (Monad.smax_def State.state_monad)
1438             (translate_premain p exit_label) (fun init preamble ->
1439             Monad.m_return0 (Monad.smax_def State.state_monad)
1440               (let code0 = List.append init code in
1441               Monad.m_bind0 (Monad.max_def Option.option)
1442                 (Obj.magic (ASM.code_size_opt code0)) (fun _ ->
1443                 Monad.m_return0 (Monad.max_def Option.option)
1444                   { ASM.preamble = preamble; ASM.code = code0;
1445                   ASM.renamed_symbols = symboltable; ASM.final_label =
1446                   exit_label })))))))
1447