source: extracted/joint_LTL_LIN.ml @ 3001

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

New extraction.

File size: 13.4 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_5280, x_5279) -> h_from_acc x_5280 x_5279
133| To_acc (x_5282, x_5281) -> h_to_acc x_5282 x_5281
134| Int_to_reg (x_5284, x_5283) -> h_int_to_reg x_5284 x_5283
135| Int_to_acc (x_5286, x_5285) -> h_int_to_acc x_5286 x_5285
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_5293, x_5292) -> h_from_acc x_5293 x_5292
143| To_acc (x_5295, x_5294) -> h_to_acc x_5295 x_5294
144| Int_to_reg (x_5297, x_5296) -> h_int_to_reg x_5297 x_5296
145| Int_to_acc (x_5299, x_5298) -> h_int_to_acc x_5299 x_5298
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_5306, x_5305) -> h_from_acc x_5306 x_5305
153| To_acc (x_5308, x_5307) -> h_to_acc x_5308 x_5307
154| Int_to_reg (x_5310, x_5309) -> h_int_to_reg x_5310 x_5309
155| Int_to_acc (x_5312, x_5311) -> h_int_to_acc x_5312 x_5311
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_5319, x_5318) -> h_from_acc x_5319 x_5318
163| To_acc (x_5321, x_5320) -> h_to_acc x_5321 x_5320
164| Int_to_reg (x_5323, x_5322) -> h_int_to_reg x_5323 x_5322
165| Int_to_acc (x_5325, x_5324) -> h_int_to_acc x_5325 x_5324
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_5332, x_5331) -> h_from_acc x_5332 x_5331
173| To_acc (x_5334, x_5333) -> h_to_acc x_5334 x_5333
174| Int_to_reg (x_5336, x_5335) -> h_int_to_reg x_5336 x_5335
175| Int_to_acc (x_5338, x_5337) -> h_int_to_acc x_5338 x_5337
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_5345, x_5344) -> h_from_acc x_5345 x_5344
183| To_acc (x_5347, x_5346) -> h_to_acc x_5347 x_5346
184| Int_to_reg (x_5349, x_5348) -> h_int_to_reg x_5349 x_5348
185| Int_to_acc (x_5351, x_5350) -> h_int_to_acc x_5351 x_5350
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 I8051.register * Graphs.label
249| HIGH_ADDRESS of I8051.register * Graphs.label
250
251(** val ltl_lin_seq_rect_Type4 :
252    'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
253    -> Graphs.label -> 'a1) -> 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_5445, x_5444) -> h_LOW_ADDRESS x_5445 x_5444
258| HIGH_ADDRESS (x_5447, x_5446) -> h_HIGH_ADDRESS x_5447 x_5446
259
260(** val ltl_lin_seq_rect_Type5 :
261    'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
262    -> Graphs.label -> 'a1) -> 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_5454, x_5453) -> h_LOW_ADDRESS x_5454 x_5453
267| HIGH_ADDRESS (x_5456, x_5455) -> h_HIGH_ADDRESS x_5456 x_5455
268
269(** val ltl_lin_seq_rect_Type3 :
270    'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
271    -> Graphs.label -> 'a1) -> 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_5463, x_5462) -> h_LOW_ADDRESS x_5463 x_5462
276| HIGH_ADDRESS (x_5465, x_5464) -> h_HIGH_ADDRESS x_5465 x_5464
277
278(** val ltl_lin_seq_rect_Type2 :
279    'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
280    -> Graphs.label -> 'a1) -> 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_5472, x_5471) -> h_LOW_ADDRESS x_5472 x_5471
285| HIGH_ADDRESS (x_5474, x_5473) -> h_HIGH_ADDRESS x_5474 x_5473
286
287(** val ltl_lin_seq_rect_Type1 :
288    'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
289    -> Graphs.label -> 'a1) -> 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_5481, x_5480) -> h_LOW_ADDRESS x_5481 x_5480
294| HIGH_ADDRESS (x_5483, x_5482) -> h_HIGH_ADDRESS x_5483 x_5482
295
296(** val ltl_lin_seq_rect_Type0 :
297    'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
298    -> Graphs.label -> 'a1) -> 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_5490, x_5489) -> h_LOW_ADDRESS x_5490 x_5489
303| HIGH_ADDRESS (x_5492, x_5491) -> h_HIGH_ADDRESS x_5492 x_5491
304
305(** val ltl_lin_seq_inv_rect_Type4 :
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_Type4 hterm h1 h2 h3 h4 =
310  let hcut = ltl_lin_seq_rect_Type4 h1 h2 h3 h4 hterm in hcut __
311
312(** val ltl_lin_seq_inv_rect_Type3 :
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_Type3 hterm h1 h2 h3 h4 =
317  let hcut = ltl_lin_seq_rect_Type3 h1 h2 h3 h4 hterm in hcut __
318
319(** val ltl_lin_seq_inv_rect_Type2 :
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_Type2 hterm h1 h2 h3 h4 =
324  let hcut = ltl_lin_seq_rect_Type2 h1 h2 h3 h4 hterm in hcut __
325
326(** val ltl_lin_seq_inv_rect_Type1 :
327    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
328    Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ ->
329    'a1) -> 'a1 **)
330let ltl_lin_seq_inv_rect_Type1 hterm h1 h2 h3 h4 =
331  let hcut = ltl_lin_seq_rect_Type1 h1 h2 h3 h4 hterm in hcut __
332
333(** val ltl_lin_seq_inv_rect_Type0 :
334    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
335    Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ ->
336    'a1) -> 'a1 **)
337let ltl_lin_seq_inv_rect_Type0 hterm h1 h2 h3 h4 =
338  let hcut = ltl_lin_seq_rect_Type0 h1 h2 h3 h4 hterm in hcut __
339
340(** val ltl_lin_seq_discr : ltl_lin_seq -> ltl_lin_seq -> __ **)
341let ltl_lin_seq_discr x y =
342  Logic.eq_rect_Type2 x
343    (match x with
344     | SAVE_CARRY -> Obj.magic (fun _ dH -> dH)
345     | RESTORE_CARRY -> Obj.magic (fun _ dH -> dH)
346     | LOW_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
347     | HIGH_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
348
349(** val ltl_lin_seq_jmdiscr : ltl_lin_seq -> ltl_lin_seq -> __ **)
350let ltl_lin_seq_jmdiscr x y =
351  Logic.eq_rect_Type2 x
352    (match x with
353     | SAVE_CARRY -> Obj.magic (fun _ dH -> dH)
354     | RESTORE_CARRY -> Obj.magic (fun _ dH -> dH)
355     | LOW_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
356     | HIGH_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
357
358(** val ltl_lin_seq_labels : ltl_lin_seq -> Graphs.label List.list **)
359let ltl_lin_seq_labels = function
360| SAVE_CARRY -> List.Nil
361| RESTORE_CARRY -> List.Nil
362| LOW_ADDRESS (x, lbl) -> List.Cons (lbl, List.Nil)
363| HIGH_ADDRESS (x, lbl) -> List.Cons (lbl, List.Nil)
364
365(** val lTL_LIN_uns : Joint.unserialized_params **)
366let lTL_LIN_uns =
367  { Joint.ext_seq_labels = (Obj.magic ltl_lin_seq_labels);
368    Joint.has_tailcalls = Bool.False }
369
370(** val lTL_LIN_functs : Joint.get_pseudo_reg_functs **)
371let lTL_LIN_functs =
372  { Joint.acc_a_regs = (fun x -> List.Nil); Joint.acc_b_regs = (fun x ->
373    List.Nil); Joint.acc_a_args = (fun x -> List.Nil); Joint.acc_b_args =
374    (fun x -> List.Nil); Joint.dpl_regs = (fun x -> List.Nil);
375    Joint.dph_regs = (fun x -> List.Nil); Joint.dpl_args = (fun x ->
376    List.Nil); Joint.dph_args = (fun x -> List.Nil); Joint.snd_args =
377    (fun x -> List.Nil); Joint.pair_move_regs = (fun x -> List.Nil);
378    Joint.f_call_args = (fun x -> List.Nil); Joint.f_call_dest = (fun x ->
379    List.Nil); Joint.ext_seq_regs = (fun x -> List.Nil); Joint.params_regs =
380    (fun x -> List.Nil) }
381
382(** val lTL_LIN : Joint.uns_params **)
383let lTL_LIN =
384  { Joint.u_pars = lTL_LIN_uns; Joint.functs = lTL_LIN_functs }
385
Note: See TracBrowser for help on using the repository browser.