source: extracted/joint_LTL_LIN.ml @ 2873

Last change on this file since 2873 was 2873, checked in by sacerdot, 8 years ago

Extracted again.

File size: 13.4 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_21672, x_21671) -> h_from_acc x_21672 x_21671
119| To_acc (x_21674, x_21673) -> h_to_acc x_21674 x_21673
120| Int_to_reg (x_21676, x_21675) -> h_int_to_reg x_21676 x_21675
121| Int_to_acc (x_21678, x_21677) -> h_int_to_acc x_21678 x_21677
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_21685, x_21684) -> h_from_acc x_21685 x_21684
129| To_acc (x_21687, x_21686) -> h_to_acc x_21687 x_21686
130| Int_to_reg (x_21689, x_21688) -> h_int_to_reg x_21689 x_21688
131| Int_to_acc (x_21691, x_21690) -> h_int_to_acc x_21691 x_21690
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_21698, x_21697) -> h_from_acc x_21698 x_21697
139| To_acc (x_21700, x_21699) -> h_to_acc x_21700 x_21699
140| Int_to_reg (x_21702, x_21701) -> h_int_to_reg x_21702 x_21701
141| Int_to_acc (x_21704, x_21703) -> h_int_to_acc x_21704 x_21703
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_21711, x_21710) -> h_from_acc x_21711 x_21710
149| To_acc (x_21713, x_21712) -> h_to_acc x_21713 x_21712
150| Int_to_reg (x_21715, x_21714) -> h_int_to_reg x_21715 x_21714
151| Int_to_acc (x_21717, x_21716) -> h_int_to_acc x_21717 x_21716
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_21724, x_21723) -> h_from_acc x_21724 x_21723
159| To_acc (x_21726, x_21725) -> h_to_acc x_21726 x_21725
160| Int_to_reg (x_21728, x_21727) -> h_int_to_reg x_21728 x_21727
161| Int_to_acc (x_21730, x_21729) -> h_int_to_acc x_21730 x_21729
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_21737, x_21736) -> h_from_acc x_21737 x_21736
169| To_acc (x_21739, x_21738) -> h_to_acc x_21739 x_21738
170| Int_to_reg (x_21741, x_21740) -> h_int_to_reg x_21741 x_21740
171| Int_to_acc (x_21743, x_21742) -> h_int_to_acc x_21743 x_21742
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_21837, x_21836) -> h_LOW_ADDRESS x_21837 x_21836
244| HIGH_ADDRESS (x_21839, x_21838) -> h_HIGH_ADDRESS x_21839 x_21838
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_21846, x_21845) -> h_LOW_ADDRESS x_21846 x_21845
253| HIGH_ADDRESS (x_21848, x_21847) -> h_HIGH_ADDRESS x_21848 x_21847
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_21855, x_21854) -> h_LOW_ADDRESS x_21855 x_21854
262| HIGH_ADDRESS (x_21857, x_21856) -> h_HIGH_ADDRESS x_21857 x_21856
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_21864, x_21863) -> h_LOW_ADDRESS x_21864 x_21863
271| HIGH_ADDRESS (x_21866, x_21865) -> h_HIGH_ADDRESS x_21866 x_21865
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_21873, x_21872) -> h_LOW_ADDRESS x_21873 x_21872
280| HIGH_ADDRESS (x_21875, x_21874) -> h_HIGH_ADDRESS x_21875 x_21874
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_21882, x_21881) -> h_LOW_ADDRESS x_21882 x_21881
289| HIGH_ADDRESS (x_21884, x_21883) -> h_HIGH_ADDRESS x_21884 x_21883
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.