source: driver/extracted/joint_LTL_LIN.ml @ 3106

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

New extraction

File size: 12.8 KB
Line 
1open Preamble
2
3open Extra_bool
4
5open Coqlib
6
7open Values
8
9open FrontEndVal
10
11open GenMem
12
13open FrontEndMem
14
15open Globalenvs
16
17open String
18
19open Sets
20
21open Listb
22
23open LabelledObjects
24
25open BitVectorTrie
26
27open Graphs
28
29open I8051
30
31open Order
32
33open Registers
34
35open CostLabel
36
37open Hide
38
39open Proper
40
41open PositiveMap
42
43open Deqsets
44
45open ErrorMessages
46
47open PreIdentifiers
48
49open Errors
50
51open Extralib
52
53open Lists
54
55open Identifiers
56
57open Integers
58
59open AST
60
61open Division
62
63open Exp
64
65open Arithmetic
66
67open Setoids
68
69open Monad
70
71open Option
72
73open Extranat
74
75open Vector
76
77open Div_and_mod
78
79open Jmeq
80
81open Russell
82
83open List
84
85open Util
86
87open FoldStuff
88
89open BitVector
90
91open Types
92
93open Bool
94
95open Relations
96
97open Nat
98
99open Hints_declaration
100
101open Core_notation
102
103open Pts
104
105open Logic
106
107open Positive
108
109open Z
110
111open BitVectorZ
112
113open Pointers
114
115open ByteValues
116
117open BackEndOps
118
119open Joint
120
121type registers_move =
122| From_acc of I8051.register * Types.unit0
123| To_acc of Types.unit0 * I8051.register
124| Int_to_reg of I8051.register * BitVector.byte
125| Int_to_acc of Types.unit0 * BitVector.byte
126
127(** val registers_move_rect_Type4 :
128    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
129    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
130    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
131let rec registers_move_rect_Type4 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
132| From_acc (x_18638, x_18637) -> h_from_acc x_18638 x_18637
133| To_acc (x_18640, x_18639) -> h_to_acc x_18640 x_18639
134| Int_to_reg (x_18642, x_18641) -> h_int_to_reg x_18642 x_18641
135| Int_to_acc (x_18644, x_18643) -> h_int_to_acc x_18644 x_18643
136
137(** val registers_move_rect_Type5 :
138    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
139    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
140    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
141let rec registers_move_rect_Type5 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
142| From_acc (x_18651, x_18650) -> h_from_acc x_18651 x_18650
143| To_acc (x_18653, x_18652) -> h_to_acc x_18653 x_18652
144| Int_to_reg (x_18655, x_18654) -> h_int_to_reg x_18655 x_18654
145| Int_to_acc (x_18657, x_18656) -> h_int_to_acc x_18657 x_18656
146
147(** val registers_move_rect_Type3 :
148    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
149    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
150    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
151let rec registers_move_rect_Type3 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
152| From_acc (x_18664, x_18663) -> h_from_acc x_18664 x_18663
153| To_acc (x_18666, x_18665) -> h_to_acc x_18666 x_18665
154| Int_to_reg (x_18668, x_18667) -> h_int_to_reg x_18668 x_18667
155| Int_to_acc (x_18670, x_18669) -> h_int_to_acc x_18670 x_18669
156
157(** val registers_move_rect_Type2 :
158    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
159    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
160    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
161let rec registers_move_rect_Type2 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
162| From_acc (x_18677, x_18676) -> h_from_acc x_18677 x_18676
163| To_acc (x_18679, x_18678) -> h_to_acc x_18679 x_18678
164| Int_to_reg (x_18681, x_18680) -> h_int_to_reg x_18681 x_18680
165| Int_to_acc (x_18683, x_18682) -> h_int_to_acc x_18683 x_18682
166
167(** val registers_move_rect_Type1 :
168    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
169    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
170    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
171let rec registers_move_rect_Type1 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
172| From_acc (x_18690, x_18689) -> h_from_acc x_18690 x_18689
173| To_acc (x_18692, x_18691) -> h_to_acc x_18692 x_18691
174| Int_to_reg (x_18694, x_18693) -> h_int_to_reg x_18694 x_18693
175| Int_to_acc (x_18696, x_18695) -> h_int_to_acc x_18696 x_18695
176
177(** val registers_move_rect_Type0 :
178    (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register
179    -> 'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
180    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
181let rec registers_move_rect_Type0 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
182| From_acc (x_18703, x_18702) -> h_from_acc x_18703 x_18702
183| To_acc (x_18705, x_18704) -> h_to_acc x_18705 x_18704
184| Int_to_reg (x_18707, x_18706) -> h_int_to_reg x_18707 x_18706
185| Int_to_acc (x_18709, x_18708) -> h_int_to_acc x_18709 x_18708
186
187(** val registers_move_inv_rect_Type4 :
188    registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
189    (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
190    BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
191    'a1) -> 'a1 **)
192let registers_move_inv_rect_Type4 hterm h1 h2 h3 h4 =
193  let hcut = registers_move_rect_Type4 h1 h2 h3 h4 hterm in hcut __
194
195(** val registers_move_inv_rect_Type3 :
196    registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
197    (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
198    BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
199    'a1) -> 'a1 **)
200let registers_move_inv_rect_Type3 hterm h1 h2 h3 h4 =
201  let hcut = registers_move_rect_Type3 h1 h2 h3 h4 hterm in hcut __
202
203(** val registers_move_inv_rect_Type2 :
204    registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
205    (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
206    BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
207    'a1) -> 'a1 **)
208let registers_move_inv_rect_Type2 hterm h1 h2 h3 h4 =
209  let hcut = registers_move_rect_Type2 h1 h2 h3 h4 hterm in hcut __
210
211(** val registers_move_inv_rect_Type1 :
212    registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
213    (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
214    BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
215    'a1) -> 'a1 **)
216let registers_move_inv_rect_Type1 hterm h1 h2 h3 h4 =
217  let hcut = registers_move_rect_Type1 h1 h2 h3 h4 hterm in hcut __
218
219(** val registers_move_inv_rect_Type0 :
220    registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
221    (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
222    BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
223    'a1) -> 'a1 **)
224let registers_move_inv_rect_Type0 hterm h1 h2 h3 h4 =
225  let hcut = registers_move_rect_Type0 h1 h2 h3 h4 hterm in hcut __
226
227(** val registers_move_discr : registers_move -> registers_move -> __ **)
228let registers_move_discr x y =
229  Logic.eq_rect_Type2 x
230    (match x with
231     | From_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
232     | To_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
233     | Int_to_reg (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
234     | Int_to_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
235
236(** val registers_move_jmdiscr : registers_move -> registers_move -> __ **)
237let registers_move_jmdiscr x y =
238  Logic.eq_rect_Type2 x
239    (match x with
240     | From_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
241     | To_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
242     | Int_to_reg (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
243     | Int_to_acc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
244
245type ltl_lin_seq =
246| SAVE_CARRY
247| RESTORE_CARRY
248| LOW_ADDRESS of Graphs.label
249| HIGH_ADDRESS of Graphs.label
250
251(** val ltl_lin_seq_rect_Type4 :
252    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
253    ltl_lin_seq -> 'a1 **)
254let rec ltl_lin_seq_rect_Type4 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
255| SAVE_CARRY -> h_SAVE_CARRY
256| RESTORE_CARRY -> h_RESTORE_CARRY
257| LOW_ADDRESS x_18800 -> h_LOW_ADDRESS x_18800
258| HIGH_ADDRESS x_18801 -> h_HIGH_ADDRESS x_18801
259
260(** val ltl_lin_seq_rect_Type5 :
261    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
262    ltl_lin_seq -> 'a1 **)
263let rec ltl_lin_seq_rect_Type5 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
264| SAVE_CARRY -> h_SAVE_CARRY
265| RESTORE_CARRY -> h_RESTORE_CARRY
266| LOW_ADDRESS x_18807 -> h_LOW_ADDRESS x_18807
267| HIGH_ADDRESS x_18808 -> h_HIGH_ADDRESS x_18808
268
269(** val ltl_lin_seq_rect_Type3 :
270    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
271    ltl_lin_seq -> 'a1 **)
272let rec ltl_lin_seq_rect_Type3 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
273| SAVE_CARRY -> h_SAVE_CARRY
274| RESTORE_CARRY -> h_RESTORE_CARRY
275| LOW_ADDRESS x_18814 -> h_LOW_ADDRESS x_18814
276| HIGH_ADDRESS x_18815 -> h_HIGH_ADDRESS x_18815
277
278(** val ltl_lin_seq_rect_Type2 :
279    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
280    ltl_lin_seq -> 'a1 **)
281let rec ltl_lin_seq_rect_Type2 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
282| SAVE_CARRY -> h_SAVE_CARRY
283| RESTORE_CARRY -> h_RESTORE_CARRY
284| LOW_ADDRESS x_18821 -> h_LOW_ADDRESS x_18821
285| HIGH_ADDRESS x_18822 -> h_HIGH_ADDRESS x_18822
286
287(** val ltl_lin_seq_rect_Type1 :
288    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
289    ltl_lin_seq -> 'a1 **)
290let rec ltl_lin_seq_rect_Type1 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
291| SAVE_CARRY -> h_SAVE_CARRY
292| RESTORE_CARRY -> h_RESTORE_CARRY
293| LOW_ADDRESS x_18828 -> h_LOW_ADDRESS x_18828
294| HIGH_ADDRESS x_18829 -> h_HIGH_ADDRESS x_18829
295
296(** val ltl_lin_seq_rect_Type0 :
297    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
298    ltl_lin_seq -> 'a1 **)
299let rec ltl_lin_seq_rect_Type0 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
300| SAVE_CARRY -> h_SAVE_CARRY
301| RESTORE_CARRY -> h_RESTORE_CARRY
302| LOW_ADDRESS x_18835 -> h_LOW_ADDRESS x_18835
303| HIGH_ADDRESS x_18836 -> h_HIGH_ADDRESS x_18836
304
305(** val ltl_lin_seq_inv_rect_Type4 :
306    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
307    -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
308let ltl_lin_seq_inv_rect_Type4 hterm h1 h2 h3 h4 =
309  let hcut = ltl_lin_seq_rect_Type4 h1 h2 h3 h4 hterm in hcut __
310
311(** val ltl_lin_seq_inv_rect_Type3 :
312    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
313    -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
314let ltl_lin_seq_inv_rect_Type3 hterm h1 h2 h3 h4 =
315  let hcut = ltl_lin_seq_rect_Type3 h1 h2 h3 h4 hterm in hcut __
316
317(** val ltl_lin_seq_inv_rect_Type2 :
318    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
319    -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
320let ltl_lin_seq_inv_rect_Type2 hterm h1 h2 h3 h4 =
321  let hcut = ltl_lin_seq_rect_Type2 h1 h2 h3 h4 hterm in hcut __
322
323(** val ltl_lin_seq_inv_rect_Type1 :
324    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
325    -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
326let ltl_lin_seq_inv_rect_Type1 hterm h1 h2 h3 h4 =
327  let hcut = ltl_lin_seq_rect_Type1 h1 h2 h3 h4 hterm in hcut __
328
329(** val ltl_lin_seq_inv_rect_Type0 :
330    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
331    -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
332let ltl_lin_seq_inv_rect_Type0 hterm h1 h2 h3 h4 =
333  let hcut = ltl_lin_seq_rect_Type0 h1 h2 h3 h4 hterm in hcut __
334
335(** val ltl_lin_seq_discr : ltl_lin_seq -> ltl_lin_seq -> __ **)
336let ltl_lin_seq_discr 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 -> Obj.magic (fun _ dH -> dH __)
342     | HIGH_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)) y
343
344(** val ltl_lin_seq_jmdiscr : ltl_lin_seq -> ltl_lin_seq -> __ **)
345let ltl_lin_seq_jmdiscr x y =
346  Logic.eq_rect_Type2 x
347    (match x with
348     | SAVE_CARRY -> Obj.magic (fun _ dH -> dH)
349     | RESTORE_CARRY -> Obj.magic (fun _ dH -> dH)
350     | LOW_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)
351     | HIGH_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)) y
352
353(** val ltl_lin_seq_labels : ltl_lin_seq -> Graphs.label List.list **)
354let ltl_lin_seq_labels = function
355| SAVE_CARRY -> List.Nil
356| RESTORE_CARRY -> List.Nil
357| LOW_ADDRESS lbl -> List.Cons (lbl, List.Nil)
358| HIGH_ADDRESS lbl -> List.Cons (lbl, List.Nil)
359
360(** val lTL_LIN_uns : Joint.unserialized_params **)
361let lTL_LIN_uns =
362  { Joint.ext_seq_labels = (Obj.magic ltl_lin_seq_labels);
363    Joint.has_tailcalls = Bool.False }
364
365(** val lTL_LIN_functs : Joint.get_pseudo_reg_functs **)
366let lTL_LIN_functs =
367  { Joint.acc_a_regs = (fun x -> List.Nil); Joint.acc_b_regs = (fun x ->
368    List.Nil); Joint.acc_a_args = (fun x -> List.Nil); Joint.acc_b_args =
369    (fun x -> List.Nil); Joint.dpl_regs = (fun x -> List.Nil);
370    Joint.dph_regs = (fun x -> List.Nil); Joint.dpl_args = (fun x ->
371    List.Nil); Joint.dph_args = (fun x -> List.Nil); Joint.snd_args =
372    (fun x -> List.Nil); Joint.pair_move_regs = (fun x -> List.Nil);
373    Joint.f_call_args = (fun x -> List.Nil); Joint.f_call_dest = (fun x ->
374    List.Nil); Joint.ext_seq_regs = (fun x -> List.Nil); Joint.params_regs =
375    (fun x -> List.Nil) }
376
377(** val lTL_LIN : Joint.uns_params **)
378let lTL_LIN =
379  { Joint.u_pars = lTL_LIN_uns; Joint.functs = lTL_LIN_functs }
380
Note: See TracBrowser for help on using the repository browser.