source: extracted/lINToASM.ml @ 3080

Last change on this file since 3080 was 3080, checked in by sacerdot, 7 years ago

New extraction.

File size: 66.3 KB
RevLine 
[2717]1open Preamble
2
[2773]3open Deqsets
4
5open Setoids
6
7open Monad
8
9open Option
10
11open Extranat
12
13open Vector
14
[2717]15open Div_and_mod
16
17open Jmeq
18
19open Russell
20
[2773]21open List
22
23open Util
24
25open FoldStuff
26
[2717]27open Bool
28
29open Relations
30
31open Nat
32
[2773]33open BitVector
34
[2717]35open Hints_declaration
36
37open Core_notation
38
39open Pts
40
41open Logic
42
43open Types
44
45open BitVectorTrie
46
47open BitVectorTrieSet
48
[2773]49open State
50
[2717]51open String
52
[2773]53open Exp
[2717]54
[2773]55open Arithmetic
[2717]56
[2773]57open Integers
[2717]58
[2773]59open AST
[2717]60
[2773]61open LabelledObjects
[2717]62
63open Proper
64
65open PositiveMap
66
67open ErrorMessages
68
69open PreIdentifiers
70
71open Errors
72
73open Extralib
74
[2773]75open Lists
[2717]76
[2773]77open Positive
[2717]78
[2773]79open Identifiers
[2717]80
[2773]81open CostLabel
[2717]82
[2773]83open ASM
[2717]84
[2951]85open Extra_bool
86
87open Coqlib
88
89open Values
90
91open FrontEndVal
92
93open GenMem
94
95open FrontEndMem
96
97open Globalenvs
98
[2773]99open Sets
[2717]100
[2773]101open Listb
[2717]102
[2773]103open Graphs
[2717]104
[2773]105open I8051
[2717]106
[2773]107open Order
[2717]108
[2773]109open Registers
[2717]110
[2773]111open Hide
112
113open Division
114
[2717]115open Z
116
117open BitVectorZ
118
119open Pointers
120
121open ByteValues
122
123open BackEndOps
124
125open Joint
126
127open Joint_LTL_LIN
128
129open LIN
130
131type aSM_universe = { id_univ : Identifiers.universe;
132                      current_funct : AST.ident;
[2773]133                      ident_map : ASM.identifier Identifiers.identifier_map;
134                      label_map : ASM.identifier Identifiers.identifier_map
[2717]135                                  Identifiers.identifier_map;
[2979]136                      fresh_cost_label : Positive.pos }
[2717]137
138(** val aSM_universe_rect_Type4 :
[3043]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 **)
[3080]142let rec aSM_universe_rect_Type4 h_mk_ASM_universe x_21483 =
[2717]143  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
[3043]144    ident_map0; label_map = label_map0; fresh_cost_label =
[3080]145    fresh_cost_label0 } = x_21483
[2717]146  in
147  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
[3043]148    fresh_cost_label0
[2717]149
150(** val aSM_universe_rect_Type5 :
[3043]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 **)
[3080]154let rec aSM_universe_rect_Type5 h_mk_ASM_universe x_21485 =
[2717]155  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
[3043]156    ident_map0; label_map = label_map0; fresh_cost_label =
[3080]157    fresh_cost_label0 } = x_21485
[2717]158  in
159  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
[3043]160    fresh_cost_label0
[2717]161
162(** val aSM_universe_rect_Type3 :
[3043]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 **)
[3080]166let rec aSM_universe_rect_Type3 h_mk_ASM_universe x_21487 =
[2717]167  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
[3043]168    ident_map0; label_map = label_map0; fresh_cost_label =
[3080]169    fresh_cost_label0 } = x_21487
[2717]170  in
171  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
[3043]172    fresh_cost_label0
[2717]173
174(** val aSM_universe_rect_Type2 :
[3043]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 **)
[3080]178let rec aSM_universe_rect_Type2 h_mk_ASM_universe x_21489 =
[2717]179  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
[3043]180    ident_map0; label_map = label_map0; fresh_cost_label =
[3080]181    fresh_cost_label0 } = x_21489
[2717]182  in
183  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
[3043]184    fresh_cost_label0
[2717]185
186(** val aSM_universe_rect_Type1 :
[3043]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 **)
[3080]190let rec aSM_universe_rect_Type1 h_mk_ASM_universe x_21491 =
[2717]191  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
[3043]192    ident_map0; label_map = label_map0; fresh_cost_label =
[3080]193    fresh_cost_label0 } = x_21491
[2717]194  in
195  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
[3043]196    fresh_cost_label0
[2717]197
198(** val aSM_universe_rect_Type0 :
[3043]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 **)
[3080]202let rec aSM_universe_rect_Type0 h_mk_ASM_universe x_21493 =
[2717]203  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
[3043]204    ident_map0; label_map = label_map0; fresh_cost_label =
[3080]205    fresh_cost_label0 } = x_21493
[2717]206  in
207  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
[3043]208    fresh_cost_label0
[2717]209
[3043]210(** val id_univ : aSM_universe -> Identifiers.universe **)
211let rec id_univ xxx =
[2717]212  xxx.id_univ
213
[3043]214(** val current_funct : aSM_universe -> AST.ident **)
215let rec current_funct xxx =
[2717]216  xxx.current_funct
217
218(** val ident_map :
[3043]219    aSM_universe -> ASM.identifier Identifiers.identifier_map **)
220let rec ident_map xxx =
[2717]221  xxx.ident_map
222
223(** val label_map :
[3043]224    aSM_universe -> ASM.identifier Identifiers.identifier_map
225    Identifiers.identifier_map **)
226let rec label_map xxx =
[2717]227  xxx.label_map
228
[3043]229(** val fresh_cost_label : aSM_universe -> Positive.pos **)
230let rec fresh_cost_label xxx =
[2979]231  xxx.fresh_cost_label
232
[2717]233(** val aSM_universe_inv_rect_Type4 :
[3043]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 **)
237let aSM_universe_inv_rect_Type4 hterm h1 =
238  let hcut = aSM_universe_rect_Type4 h1 hterm in hcut __
[2717]239
240(** val aSM_universe_inv_rect_Type3 :
[3043]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 **)
244let aSM_universe_inv_rect_Type3 hterm h1 =
245  let hcut = aSM_universe_rect_Type3 h1 hterm in hcut __
[2717]246
247(** val aSM_universe_inv_rect_Type2 :
[3043]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 **)
251let aSM_universe_inv_rect_Type2 hterm h1 =
252  let hcut = aSM_universe_rect_Type2 h1 hterm in hcut __
[2717]253
254(** val aSM_universe_inv_rect_Type1 :
[3043]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 **)
258let aSM_universe_inv_rect_Type1 hterm h1 =
259  let hcut = aSM_universe_rect_Type1 h1 hterm in hcut __
[2717]260
261(** val aSM_universe_inv_rect_Type0 :
[3043]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 **)
265let aSM_universe_inv_rect_Type0 hterm h1 =
266  let hcut = aSM_universe_rect_Type0 h1 hterm in hcut __
[2717]267
[3043]268(** val aSM_universe_discr : aSM_universe -> aSM_universe -> __ **)
269let aSM_universe_discr x y =
[2717]270  Logic.eq_rect_Type2 x
[3043]271    (let { id_univ = a0; current_funct = a1; ident_map = a2; label_map = a3;
272       fresh_cost_label = a4 } = x
[2717]273     in
[3043]274    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
[2717]275
[3043]276(** val aSM_universe_jmdiscr : aSM_universe -> aSM_universe -> __ **)
277let 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
[2979]284(** val report_cost :
[3043]285    CostLabel.costlabel -> Types.unit0 Monad.smax_def__o__monad **)
286let report_cost cl =
[2979]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;
[3043]292         ident_map = u.ident_map; label_map = u.label_map; fresh_cost_label =
293         (Positive.succ clw) }; Types.snd = Types.It }
[2979]294     | Bool.False -> { Types.fst = u; Types.snd = Types.It }))
295
[2717]296(** val identifier_of_label :
[3043]297    Graphs.label -> ASM.identifier Monad.smax_def__o__monad **)
298let identifier_of_label l =
[2717]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
[3080]305    let { Types.fst = eta28616; Types.snd = lmap0 } =
[2773]306      match Identifiers.lookup PreIdentifiers.LabelTag lmap l with
[2717]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
[3080]317    let { Types.fst = id; Types.snd = univ } = eta28616 in
[2717]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);
[3043]321    fresh_cost_label = u.fresh_cost_label }; Types.snd = id })
[2717]322
323(** val identifier_of_ident :
[3043]324    AST.ident -> ASM.identifier Monad.smax_def__o__monad **)
325let identifier_of_ident i =
[2717]326  Obj.magic (fun u ->
327    let imap = u.ident_map in
[3043]328    let res =
[2773]329      match Identifiers.lookup PreIdentifiers.SymbolTag imap i with
[2717]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
[3043]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
[2717]343    { Types.fst = { id_univ = univ; current_funct = u.current_funct;
[3043]344    ident_map = imap0; label_map = u.label_map; fresh_cost_label =
345    u.fresh_cost_label }; Types.snd = id })
[2717]346
[3043]347(** val new_ASM_universe : Joint.joint_program -> aSM_universe **)
348let 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
[2717]354(** val start_funct_translation :
[3043]355    AST.ident List.list -> AST.ident List.list -> (AST.ident,
356    Joint.joint_function) Types.prod -> Types.unit0 Monad.smax_def__o__monad **)
357let start_funct_translation g functs id_f =
[2717]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;
[3043]360    fresh_cost_label = u.fresh_cost_label }; Types.snd = Types.It })
[2717]361
[3043]362(** val aSM_fresh : ASM.identifier Monad.smax_def__o__monad **)
363let aSM_fresh =
[2717]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;
[3043]369    ident_map = u.ident_map; label_map = u.label_map; fresh_cost_label =
370    u.fresh_cost_label }; Types.snd = id })
[2717]371
372(** val register_address : I8051.register -> ASM.subaddressing_mode **)
373let 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
[3029]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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
[2717]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
[3029]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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
[2717]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 **)
581let vector_cast n m dflt v =
582  Util.if_then_else_safe (Nat.leb n m) (fun _ ->
[2773]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)
[2717]585
586(** val arg_address : Joint.hdw_argument -> ASM.subaddressing_mode **)
587let 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
601type lin_statement = Joint.joint_statement LabelledObjects.labelled_obj
602
603(** val data_of_int : BitVector.byte -> ASM.addressing_mode **)
604let data_of_int bv =
605  ASM.DATA bv
606
607(** val data16_of_int : Nat.nat -> ASM.addressing_mode **)
608let 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 **)
615let 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 **)
644let asm_other_bit =
645  ASM.BIT_ADDR Joint.zero_byte
646
[3043]647(** val one_word : BitVector.word **)
648let 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
[2717]656(** val translate_statements :
657    AST.ident List.list -> Joint.joint_statement -> ASM.pseudo_instruction
658    Monad.smax_def__o__monad **)
659let translate_statements globals = function
660| Joint.Sequential (instr, x) ->
661  (match instr with
662   | Joint.COST_LABEL lbl ->
[3043]663     Monad.m_bind0 (Monad.smax_def State.state_monad) (report_cost lbl)
664       (fun x0 ->
[2979]665       Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Cost lbl))
[2717]666   | Joint.CALL (f, x0, x1) ->
667     (match f with
668      | Types.Inl id ->
669        Monad.m_bind0 (Monad.smax_def State.state_monad)
[3043]670          (identifier_of_ident id) (fun id' ->
[2717]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
[3043]675          (ASM.JMP ASM.ACC_DPTR)))
[2717]676   | Joint.COND (x0, lbl) ->
677     Monad.m_bind0 (Monad.smax_def State.state_monad)
[3043]678       (identifier_of_label lbl) (fun l ->
[2717]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))
[3043]823      | Joint.ADDRESS (id, off, x0, x1) ->
[2717]824        Monad.m_bind0 (Monad.smax_def State.state_monad)
[3043]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)))
[2717]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)))
[2773]835      | Joint.OP1 (op1, x0, x1) ->
[2717]836        Monad.m_return0 (Monad.smax_def State.state_monad)
[2773]837          (match op1 with
[2717]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))
[2773]841      | Joint.OP2 (op2, x0, x1, reg) ->
[2717]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 _ ->
[2773]851                match op2 with
[2717]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 _ ->
[2773]872                match op2 with
[2717]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 _ ->
[2773]892                match op2 with
[2717]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 _ ->
[2773]906                match op2 with
[2717]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 }))))
[3019]958         | Joint_LTL_LIN.LOW_ADDRESS lbl ->
[2717]959           Monad.m_bind0 (Monad.smax_def State.state_monad)
[3043]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)))
[3019]964         | Joint_LTL_LIN.HIGH_ADDRESS lbl ->
[2717]965           Monad.m_bind0 (Monad.smax_def State.state_monad)
[3043]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))))))
[2717]970| Joint.Final instr ->
971  (match instr with
972   | Joint.GOTO lbl ->
973     Monad.m_bind0 (Monad.smax_def State.state_monad)
[3043]974       (identifier_of_label lbl) (fun lbl' ->
[2717]975       Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Jmp
[3029]976         (ASM.toASM_ident PreIdentifiers.ASMTag lbl')))
[2717]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)
[3043]983    (identifier_of_label lbl_true) (fun l1 ->
[2717]984    Monad.m_bind0 (Monad.smax_def State.state_monad)
[3043]985      (identifier_of_label lbl_false) (fun l2 ->
[2717]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 -> __ **)
991let 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)
[3043]1000        (identifier_of_label lbl) (fun lbl' ->
[2717]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 -> __ **)
1006let 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 :
[3043]1011    AST.ident List.list -> AST.ident List.list -> (AST.ident,
1012    Joint.joint_function) Types.prod -> __ **)
1013let translate_fun_def globals functions id_def =
[2717]1014  Monad.m_bind0 (Monad.smax_def State.state_monad)
[3043]1015    (start_funct_translation globals functions id_def) (fun x ->
[2717]1016    match id_def.Types.snd with
[2773]1017    | AST.Internal int ->
1018      let code = (Types.pi1 int).Joint.joint_if_code in
[2717]1019      Monad.m_bind0 (Monad.smax_def State.state_monad)
[3043]1020        (identifier_of_ident id_def.Types.fst) (fun id ->
[2717]1021        Monad.m_bind0 (Monad.smax_def State.state_monad)
[3043]1022          (translate_code (List.append functions globals) (Obj.magic code))
1023          (fun code' ->
[2717]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))
[2773]1029          | List.Cons (hd, tl) ->
1030            (match hd.Types.fst with
[2717]1031             | Types.None ->
1032               Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons
[2773]1033                 ({ Types.fst = (Types.Some id); Types.snd = hd.Types.snd },
[2717]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
[2773]1038                 ASM.NOP) }, (List.Cons (hd, tl)))))))
[2717]1039    | AST.External x0 ->
1040      Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil)
1041
[3069]1042type init_mutable = { virtual_dptr : (ASM.identifier, Z.z) Types.prod;
1043                      actual_dptr : (ASM.identifier, Z.z) Types.prod;
[3043]1044                      built_code : ASM.labelled_instruction List.list
1045                                   List.list;
1046                      built_preamble : (ASM.identifier, BitVector.word)
1047                                       Types.prod List.list }
[2951]1048
[2986]1049(** val init_mutable_rect_Type4 :
[3069]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 **)
[3080]1053let rec init_mutable_rect_Type4 h_mk_init_mutable x_21509 =
[3043]1054  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
[3080]1055    built_code = built_code0; built_preamble = built_preamble0 } = x_21509
[2986]1056  in
[3043]1057  h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
[2986]1058
1059(** val init_mutable_rect_Type5 :
[3069]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 **)
[3080]1063let rec init_mutable_rect_Type5 h_mk_init_mutable x_21511 =
[3043]1064  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
[3080]1065    built_code = built_code0; built_preamble = built_preamble0 } = x_21511
[2986]1066  in
[3043]1067  h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
[2986]1068
1069(** val init_mutable_rect_Type3 :
[3069]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 **)
[3080]1073let rec init_mutable_rect_Type3 h_mk_init_mutable x_21513 =
[3043]1074  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
[3080]1075    built_code = built_code0; built_preamble = built_preamble0 } = x_21513
[2986]1076  in
[3043]1077  h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
[2986]1078
1079(** val init_mutable_rect_Type2 :
[3069]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 **)
[3080]1083let rec init_mutable_rect_Type2 h_mk_init_mutable x_21515 =
[3043]1084  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
[3080]1085    built_code = built_code0; built_preamble = built_preamble0 } = x_21515
[2986]1086  in
[3043]1087  h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
[2986]1088
1089(** val init_mutable_rect_Type1 :
[3069]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 **)
[3080]1093let rec init_mutable_rect_Type1 h_mk_init_mutable x_21517 =
[3043]1094  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
[3080]1095    built_code = built_code0; built_preamble = built_preamble0 } = x_21517
[2986]1096  in
[3043]1097  h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
[2986]1098
1099(** val init_mutable_rect_Type0 :
[3069]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 **)
[3080]1103let rec init_mutable_rect_Type0 h_mk_init_mutable x_21519 =
[3043]1104  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
[3080]1105    built_code = built_code0; built_preamble = built_preamble0 } = x_21519
[2986]1106  in
[3043]1107  h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
[2986]1108
[3069]1109(** val virtual_dptr : init_mutable -> (ASM.identifier, Z.z) Types.prod **)
[2986]1110let rec virtual_dptr xxx =
1111  xxx.virtual_dptr
1112
[3069]1113(** val actual_dptr : init_mutable -> (ASM.identifier, Z.z) Types.prod **)
[2986]1114let rec actual_dptr xxx =
1115  xxx.actual_dptr
1116
[3043]1117(** val built_code :
1118    init_mutable -> ASM.labelled_instruction List.list List.list **)
1119let rec built_code xxx =
1120  xxx.built_code
[2986]1121
[3043]1122(** val built_preamble :
1123    init_mutable -> (ASM.identifier, BitVector.word) Types.prod List.list **)
1124let rec built_preamble xxx =
1125  xxx.built_preamble
1126
[2986]1127(** val init_mutable_inv_rect_Type4 :
[3069]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 **)
[2986]1132let 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 :
[3069]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 **)
[2986]1140let 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 :
[3069]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 **)
[2986]1148let 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 :
[3069]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 **)
[2986]1156let 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 :
[3069]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 **)
[2986]1164let 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 -> __ **)
1168let init_mutable_discr x y =
1169  Logic.eq_rect_Type2 x
[3043]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
[2986]1174
1175(** val init_mutable_jmdiscr : init_mutable -> init_mutable -> __ **)
1176let init_mutable_jmdiscr x y =
1177  Logic.eq_rect_Type2 x
[3043]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
[2986]1182
[3043]1183(** val store_byte_or_Identifier :
1184    (BitVector.byte, (ASM.word_side, ASM.identifier) Types.prod) Types.sum ->
1185    init_mutable -> init_mutable **)
1186let store_byte_or_Identifier by mut =
1187  let { virtual_dptr = virt; actual_dptr = act; built_code = acc1;
1188    built_preamble = acc2 } = mut
1189  in
[2986]1190  let pre =
[3069]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)))
[2986]1209    | Bool.False ->
[3069]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)
[2986]1215  in
[3043]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
[3069]1230  { virtual_dptr = { Types.fst = virt.Types.fst; Types.snd =
1231  (Z.zsucc virt.Types.snd) }; actual_dptr = virt; built_code = (List.Cons
[3043]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 }
[2986]1236
[2951]1237(** val do_store_init_data :
[3059]1238    init_mutable Monad.smax_def__o__monad -> AST.init_data -> init_mutable
[3043]1239    Monad.smax_def__o__monad **)
[3059]1240let do_store_init_data m_mut data =
[3043]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 ->
[3069]1281       let { Types.fst = virt_id; Types.snd = virt_off } = mut.virtual_dptr
1282       in
[3043]1283       Monad.m_return0 (Monad.smax_def State.state_monad) { virtual_dptr =
[3069]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 }
[3043]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)))))
[2951]1299
[3043]1300(** val do_store_global :
[3059]1301    init_mutable Monad.smax_def__o__monad -> ((AST.ident, AST.region)
1302    Types.prod, AST.init_data List.list) Types.prod -> init_mutable
[3043]1303    Monad.smax_def__o__monad **)
[3059]1304let do_store_global m_mut id_reg_data =
[3043]1305  Monad.m_bind0 (Monad.smax_def State.state_monad) m_mut (fun mut ->
[3080]1306    let { Types.fst = eta28633; Types.snd = data } = id_reg_data in
1307    let { Types.fst = id; Types.snd = reg } = eta28633 in
[3043]1308    Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_ident id)
1309      (fun id0 ->
[3069]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
[3043]1314          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
[3069]1315          (Nat.S (Nat.S Nat.O))))))))))))))))
1316          (Globalenvs.size_init_data_list data)) }, mut.built_preamble)) }
[3043]1317      in
[3059]1318      Util.foldl do_store_init_data
[3043]1319        (Monad.m_return0 (Monad.smax_def State.state_monad) mut0) data))
[2951]1320
[3043]1321(** val reversed_flatten_aux :
1322    'a1 List.list -> 'a1 List.list List.list -> 'a1 List.list **)
1323let rec reversed_flatten_aux acc = function
1324| List.Nil -> acc
1325| List.Cons (hd, tl) -> reversed_flatten_aux (List.append hd acc) tl
1326
[2986]1327(** val translate_premain :
[3043]1328    LIN.lin_program -> ASM.identifier -> (ASM.labelled_instruction List.list,
1329    (ASM.identifier, BitVector.word) Types.prod List.list) Types.prod
[2951]1330    Monad.smax_def__o__monad **)
[2986]1331let translate_premain p exit_label =
1332  Monad.m_bind0 (Monad.smax_def State.state_monad)
[3043]1333    (identifier_of_ident p.Joint.joint_prog.AST.prog_main) (fun main ->
[2986]1334    Monad.m_bind0 (Monad.smax_def State.state_monad) State.state_get
1335      (fun u ->
[3069]1336      let dummy_dptr = { Types.fst = Positive.One; Types.snd =
1337        (Z.zopp (Z.z_of_nat (Nat.S Nat.O))) }
[2986]1338      in
[3069]1339      let mut = { virtual_dptr = dummy_dptr; actual_dptr = dummy_dptr;
1340        built_code = List.Nil; built_preamble = List.Nil }
[2986]1341      in
[3043]1342      Monad.m_bind0 (Monad.smax_def State.state_monad)
[3059]1343        (Util.foldl do_store_global
[3043]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
[3069]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)))))
[3043]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 })))
[2951]1404
[2773]1405(** val get_symboltable :
[3043]1406    (ASM.identifier, AST.ident) Types.prod List.list Monad.smax_def__o__monad **)
1407let get_symboltable =
[2773]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 **)
[2717]1418let 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)
[3043]1422         (translate_fun_def p.Joint.jp_functions
[2951]1423           (List.map (fun x -> x.Types.fst.Types.fst)
[3043]1424             p.Joint.joint_prog.AST.prog_vars) id_def) (fun code ->
[2717]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
[3043]1429    Monad.m_bind0 (Monad.smax_def State.state_monad) aSM_fresh
1430      (fun exit_label ->
[2717]1431      Monad.m_bind0 (Monad.smax_def State.state_monad)
[2986]1432        (Util.foldl add_translation
1433          (Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil)
[3043]1434          p.Joint.joint_prog.AST.prog_funct) (fun code ->
1435        Monad.m_bind0 (Monad.smax_def State.state_monad) get_symboltable
[2986]1436          (fun symboltable ->
[3043]1437          Monad.m_bind2 (Monad.smax_def State.state_monad)
1438            (translate_premain p exit_label) (fun init preamble ->
[2986]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)
[3043]1444                  { ASM.preamble = preamble; ASM.code = code0;
[2986]1445                  ASM.renamed_symbols = symboltable; ASM.final_label =
1446                  exit_label })))))))
[2717]1447
Note: See TracBrowser for help on using the repository browser.