source: extracted/joint_LTL_LIN.ml @ 3019

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

New extraction after ERTLptr abortion.

File size: 12.5 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_16, x_15) -> h_from_acc x_16 x_15
133| To_acc (x_18, x_17) -> h_to_acc x_18 x_17
134| Int_to_reg (x_20, x_19) -> h_int_to_reg x_20 x_19
135| Int_to_acc (x_22, x_21) -> h_int_to_acc x_22 x_21
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_29, x_28) -> h_from_acc x_29 x_28
143| To_acc (x_31, x_30) -> h_to_acc x_31 x_30
144| Int_to_reg (x_33, x_32) -> h_int_to_reg x_33 x_32
145| Int_to_acc (x_35, x_34) -> h_int_to_acc x_35 x_34
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_42, x_41) -> h_from_acc x_42 x_41
153| To_acc (x_44, x_43) -> h_to_acc x_44 x_43
154| Int_to_reg (x_46, x_45) -> h_int_to_reg x_46 x_45
155| Int_to_acc (x_48, x_47) -> h_int_to_acc x_48 x_47
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_55, x_54) -> h_from_acc x_55 x_54
163| To_acc (x_57, x_56) -> h_to_acc x_57 x_56
164| Int_to_reg (x_59, x_58) -> h_int_to_reg x_59 x_58
165| Int_to_acc (x_61, x_60) -> h_int_to_acc x_61 x_60
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_68, x_67) -> h_from_acc x_68 x_67
173| To_acc (x_70, x_69) -> h_to_acc x_70 x_69
174| Int_to_reg (x_72, x_71) -> h_int_to_reg x_72 x_71
175| Int_to_acc (x_74, x_73) -> h_int_to_acc x_74 x_73
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_81, x_80) -> h_from_acc x_81 x_80
183| To_acc (x_83, x_82) -> h_to_acc x_83 x_82
184| Int_to_reg (x_85, x_84) -> h_int_to_reg x_85 x_84
185| Int_to_acc (x_87, x_86) -> h_int_to_acc x_87 x_86
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_178 -> h_LOW_ADDRESS x_178
258| HIGH_ADDRESS x_179 -> h_HIGH_ADDRESS x_179
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_185 -> h_LOW_ADDRESS x_185
267| HIGH_ADDRESS x_186 -> h_HIGH_ADDRESS x_186
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_192 -> h_LOW_ADDRESS x_192
276| HIGH_ADDRESS x_193 -> h_HIGH_ADDRESS x_193
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_199 -> h_LOW_ADDRESS x_199
285| HIGH_ADDRESS x_200 -> h_HIGH_ADDRESS x_200
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_206 -> h_LOW_ADDRESS x_206
294| HIGH_ADDRESS x_207 -> h_HIGH_ADDRESS x_207
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_213 -> h_LOW_ADDRESS x_213
303| HIGH_ADDRESS x_214 -> h_HIGH_ADDRESS x_214
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.