source: extracted/joint_LTL_LIN.ml @ 2854

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

Pretty printing of the LTL program.

File size: 13.3 KB
Line 
1open Preamble
2
3open String
4
5open Sets
6
7open Listb
8
9open LabelledObjects
10
11open BitVectorTrie
12
13open Graphs
14
15open I8051
16
17open Order
18
19open Registers
20
21open CostLabel
22
23open Hide
24
25open Proper
26
27open PositiveMap
28
29open Deqsets
30
31open ErrorMessages
32
33open PreIdentifiers
34
35open Errors
36
37open Extralib
38
39open Lists
40
41open Identifiers
42
43open Integers
44
45open AST
46
47open Division
48
49open Exp
50
51open Arithmetic
52
53open Setoids
54
55open Monad
56
57open Option
58
59open Extranat
60
61open Vector
62
63open Div_and_mod
64
65open Jmeq
66
67open Russell
68
69open List
70
71open Util
72
73open FoldStuff
74
75open BitVector
76
77open Types
78
79open Bool
80
81open Relations
82
83open Nat
84
85open Hints_declaration
86
87open Core_notation
88
89open Pts
90
91open Logic
92
93open Positive
94
95open Z
96
97open BitVectorZ
98
99open Pointers
100
101open ByteValues
102
103open BackEndOps
104
105open Joint
106
107type registers_move =
108| From_acc of I8051.register * Types.unit0
109| To_acc of Types.unit0 * I8051.register
110| Int_to_reg of I8051.register * BitVector.byte
111| Int_to_acc of Types.unit0 * BitVector.byte
112
113(** val registers_move_rect_Type4 :
114    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
115    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
116    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
117let rec registers_move_rect_Type4 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
118| From_acc (x_1508, x_1507) -> h_from_acc x_1508 x_1507
119| To_acc (x_1510, x_1509) -> h_to_acc x_1510 x_1509
120| Int_to_reg (x_1512, x_1511) -> h_int_to_reg x_1512 x_1511
121| Int_to_acc (x_1514, x_1513) -> h_int_to_acc x_1514 x_1513
122
123(** val registers_move_rect_Type5 :
124    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
125    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
126    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
127let rec registers_move_rect_Type5 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
128| From_acc (x_1521, x_1520) -> h_from_acc x_1521 x_1520
129| To_acc (x_1523, x_1522) -> h_to_acc x_1523 x_1522
130| Int_to_reg (x_1525, x_1524) -> h_int_to_reg x_1525 x_1524
131| Int_to_acc (x_1527, x_1526) -> h_int_to_acc x_1527 x_1526
132
133(** val registers_move_rect_Type3 :
134    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
135    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
136    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
137let rec registers_move_rect_Type3 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
138| From_acc (x_1534, x_1533) -> h_from_acc x_1534 x_1533
139| To_acc (x_1536, x_1535) -> h_to_acc x_1536 x_1535
140| Int_to_reg (x_1538, x_1537) -> h_int_to_reg x_1538 x_1537
141| Int_to_acc (x_1540, x_1539) -> h_int_to_acc x_1540 x_1539
142
143(** val registers_move_rect_Type2 :
144    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
145    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
146    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
147let rec registers_move_rect_Type2 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
148| From_acc (x_1547, x_1546) -> h_from_acc x_1547 x_1546
149| To_acc (x_1549, x_1548) -> h_to_acc x_1549 x_1548
150| Int_to_reg (x_1551, x_1550) -> h_int_to_reg x_1551 x_1550
151| Int_to_acc (x_1553, x_1552) -> h_int_to_acc x_1553 x_1552
152
153(** val registers_move_rect_Type1 :
154    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
155    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
156    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
157let rec registers_move_rect_Type1 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
158| From_acc (x_1560, x_1559) -> h_from_acc x_1560 x_1559
159| To_acc (x_1562, x_1561) -> h_to_acc x_1562 x_1561
160| Int_to_reg (x_1564, x_1563) -> h_int_to_reg x_1564 x_1563
161| Int_to_acc (x_1566, x_1565) -> h_int_to_acc x_1566 x_1565
162
163(** val registers_move_rect_Type0 :
164    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
165    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
166    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
167let rec registers_move_rect_Type0 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
168| From_acc (x_1573, x_1572) -> h_from_acc x_1573 x_1572
169| To_acc (x_1575, x_1574) -> h_to_acc x_1575 x_1574
170| Int_to_reg (x_1577, x_1576) -> h_int_to_reg x_1577 x_1576
171| Int_to_acc (x_1579, x_1578) -> h_int_to_acc x_1579 x_1578
172
173(** val registers_move_inv_rect_Type4 :
174    registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
175    (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
176    BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
177    'a1) -> 'a1 **)
178let registers_move_inv_rect_Type4 hterm h1 h2 h3 h4 =
179  let hcut = registers_move_rect_Type4 h1 h2 h3 h4 hterm in hcut __
180
181(** val registers_move_inv_rect_Type3 :
182    registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
183    (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
184    BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
185    'a1) -> 'a1 **)
186let registers_move_inv_rect_Type3 hterm h1 h2 h3 h4 =
187  let hcut = registers_move_rect_Type3 h1 h2 h3 h4 hterm in hcut __
188
189(** val registers_move_inv_rect_Type2 :
190    registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
191    (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
192    BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
193    'a1) -> 'a1 **)
194let registers_move_inv_rect_Type2 hterm h1 h2 h3 h4 =
195  let hcut = registers_move_rect_Type2 h1 h2 h3 h4 hterm in hcut __
196
197(** val registers_move_inv_rect_Type1 :
198    registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
199    (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
200    BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
201    'a1) -> 'a1 **)
202let registers_move_inv_rect_Type1 hterm h1 h2 h3 h4 =
203  let hcut = registers_move_rect_Type1 h1 h2 h3 h4 hterm in hcut __
204
205(** val registers_move_inv_rect_Type0 :
206    registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
207    (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
208    BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
209    'a1) -> 'a1 **)
210let registers_move_inv_rect_Type0 hterm h1 h2 h3 h4 =
211  let hcut = registers_move_rect_Type0 h1 h2 h3 h4 hterm in hcut __
212
213(** val registers_move_discr : registers_move -> registers_move -> __ **)
214let registers_move_discr x y =
215  Logic.eq_rect_Type2 x
216    (match x with
217     | From_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
218     | To_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
219     | Int_to_reg (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
220     | Int_to_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
221
222(** val registers_move_jmdiscr : registers_move -> registers_move -> __ **)
223let registers_move_jmdiscr x y =
224  Logic.eq_rect_Type2 x
225    (match x with
226     | From_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
227     | To_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
228     | Int_to_reg (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
229     | Int_to_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
230
231type ltl_lin_seq =
232| SAVE_CARRY
233| RESTORE_CARRY
234| LOW_ADDRESS of I8051.register * Graphs.label
235| HIGH_ADDRESS of I8051.register * Graphs.label
236
237(** val ltl_lin_seq_rect_Type4 :
238    'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
239    -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
240let rec ltl_lin_seq_rect_Type4 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
241| SAVE_CARRY -> h_SAVE_CARRY
242| RESTORE_CARRY -> h_RESTORE_CARRY
243| LOW_ADDRESS (x_1673, x_1672) -> h_LOW_ADDRESS x_1673 x_1672
244| HIGH_ADDRESS (x_1675, x_1674) -> h_HIGH_ADDRESS x_1675 x_1674
245
246(** val ltl_lin_seq_rect_Type5 :
247    'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
248    -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
249let rec ltl_lin_seq_rect_Type5 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
250| SAVE_CARRY -> h_SAVE_CARRY
251| RESTORE_CARRY -> h_RESTORE_CARRY
252| LOW_ADDRESS (x_1682, x_1681) -> h_LOW_ADDRESS x_1682 x_1681
253| HIGH_ADDRESS (x_1684, x_1683) -> h_HIGH_ADDRESS x_1684 x_1683
254
255(** val ltl_lin_seq_rect_Type3 :
256    'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
257    -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
258let rec ltl_lin_seq_rect_Type3 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
259| SAVE_CARRY -> h_SAVE_CARRY
260| RESTORE_CARRY -> h_RESTORE_CARRY
261| LOW_ADDRESS (x_1691, x_1690) -> h_LOW_ADDRESS x_1691 x_1690
262| HIGH_ADDRESS (x_1693, x_1692) -> h_HIGH_ADDRESS x_1693 x_1692
263
264(** val ltl_lin_seq_rect_Type2 :
265    'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
266    -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
267let rec ltl_lin_seq_rect_Type2 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
268| SAVE_CARRY -> h_SAVE_CARRY
269| RESTORE_CARRY -> h_RESTORE_CARRY
270| LOW_ADDRESS (x_1700, x_1699) -> h_LOW_ADDRESS x_1700 x_1699
271| HIGH_ADDRESS (x_1702, x_1701) -> h_HIGH_ADDRESS x_1702 x_1701
272
273(** val ltl_lin_seq_rect_Type1 :
274    'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
275    -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
276let rec ltl_lin_seq_rect_Type1 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
277| SAVE_CARRY -> h_SAVE_CARRY
278| RESTORE_CARRY -> h_RESTORE_CARRY
279| LOW_ADDRESS (x_1709, x_1708) -> h_LOW_ADDRESS x_1709 x_1708
280| HIGH_ADDRESS (x_1711, x_1710) -> h_HIGH_ADDRESS x_1711 x_1710
281
282(** val ltl_lin_seq_rect_Type0 :
283    'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
284    -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
285let rec ltl_lin_seq_rect_Type0 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
286| SAVE_CARRY -> h_SAVE_CARRY
287| RESTORE_CARRY -> h_RESTORE_CARRY
288| LOW_ADDRESS (x_1718, x_1717) -> h_LOW_ADDRESS x_1718 x_1717
289| HIGH_ADDRESS (x_1720, x_1719) -> h_HIGH_ADDRESS x_1720 x_1719
290
291(** val ltl_lin_seq_inv_rect_Type4 :
292    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
293    Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ ->
294    'a1) -> 'a1 **)
295let ltl_lin_seq_inv_rect_Type4 hterm h1 h2 h3 h4 =
296  let hcut = ltl_lin_seq_rect_Type4 h1 h2 h3 h4 hterm in hcut __
297
298(** val ltl_lin_seq_inv_rect_Type3 :
299    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
300    Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ ->
301    'a1) -> 'a1 **)
302let ltl_lin_seq_inv_rect_Type3 hterm h1 h2 h3 h4 =
303  let hcut = ltl_lin_seq_rect_Type3 h1 h2 h3 h4 hterm in hcut __
304
305(** val ltl_lin_seq_inv_rect_Type2 :
306    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
307    Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ ->
308    'a1) -> 'a1 **)
309let ltl_lin_seq_inv_rect_Type2 hterm h1 h2 h3 h4 =
310  let hcut = ltl_lin_seq_rect_Type2 h1 h2 h3 h4 hterm in hcut __
311
312(** val ltl_lin_seq_inv_rect_Type1 :
313    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
314    Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ ->
315    'a1) -> 'a1 **)
316let ltl_lin_seq_inv_rect_Type1 hterm h1 h2 h3 h4 =
317  let hcut = ltl_lin_seq_rect_Type1 h1 h2 h3 h4 hterm in hcut __
318
319(** val ltl_lin_seq_inv_rect_Type0 :
320    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
321    Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ ->
322    'a1) -> 'a1 **)
323let ltl_lin_seq_inv_rect_Type0 hterm h1 h2 h3 h4 =
324  let hcut = ltl_lin_seq_rect_Type0 h1 h2 h3 h4 hterm in hcut __
325
326(** val ltl_lin_seq_discr : ltl_lin_seq -> ltl_lin_seq -> __ **)
327let ltl_lin_seq_discr x y =
328  Logic.eq_rect_Type2 x
329    (match x with
330     | SAVE_CARRY -> Obj.magic (fun _ dH -> dH)
331     | RESTORE_CARRY -> Obj.magic (fun _ dH -> dH)
332     | LOW_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
333     | HIGH_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
334
335(** val ltl_lin_seq_jmdiscr : ltl_lin_seq -> ltl_lin_seq -> __ **)
336let ltl_lin_seq_jmdiscr x y =
337  Logic.eq_rect_Type2 x
338    (match x with
339     | SAVE_CARRY -> Obj.magic (fun _ dH -> dH)
340     | RESTORE_CARRY -> Obj.magic (fun _ dH -> dH)
341     | LOW_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
342     | HIGH_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
343
344(** val ltl_lin_seq_labels : ltl_lin_seq -> Graphs.label List.list **)
345let ltl_lin_seq_labels = function
346| SAVE_CARRY -> List.Nil
347| RESTORE_CARRY -> List.Nil
348| LOW_ADDRESS (x, lbl) -> List.Cons (lbl, List.Nil)
349| HIGH_ADDRESS (x, lbl) -> List.Cons (lbl, List.Nil)
350
351(** val lTL_LIN_uns : Joint.unserialized_params **)
352let lTL_LIN_uns =
353  { Joint.ext_seq_labels = (Obj.magic ltl_lin_seq_labels);
354    Joint.has_tailcalls = Bool.False }
355
356(** val lTL_LIN_functs : Joint.get_pseudo_reg_functs **)
357let lTL_LIN_functs =
358  { Joint.acc_a_regs = (fun x -> List.Nil); Joint.acc_b_regs = (fun x ->
359    List.Nil); Joint.acc_a_args = (fun x -> List.Nil); Joint.acc_b_args =
360    (fun x -> List.Nil); Joint.dpl_regs = (fun x -> List.Nil);
361    Joint.dph_regs = (fun x -> List.Nil); Joint.dpl_args = (fun x ->
362    List.Nil); Joint.dph_args = (fun x -> List.Nil); Joint.snd_args =
363    (fun x -> List.Nil); Joint.pair_move_regs = (fun x -> List.Nil);
364    Joint.f_call_args = (fun x -> List.Nil); Joint.f_call_dest = (fun x ->
365    List.Nil); Joint.ext_seq_regs = (fun x -> List.Nil); Joint.params_regs =
366    (fun x -> List.Nil) }
367
368(** val lTL_LIN : Joint.uns_params **)
369let lTL_LIN =
370  { Joint.u_pars = lTL_LIN_uns; Joint.functs = lTL_LIN_functs }
371
Note: See TracBrowser for help on using the repository browser.