source: extracted/joint_LTL_LIN.ml @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 12.6 KB
Line 
1open Preamble
2
3open String
4
5open Sets
6
7open Listb
8
9open LabelledObjects
10
11open Graphs
12
13open I8051
14
15open Order
16
17open Registers
18
19open BitVectorTrie
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 Setoids
40
41open Monad
42
43open Option
44
45open Lists
46
47open Identifiers
48
49open Integers
50
51open AST
52
53open Division
54
55open Exp
56
57open Arithmetic
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_21157, x_21156) -> h_from_acc x_21157 x_21156
119| To_acc (x_21159, x_21158) -> h_to_acc x_21159 x_21158
120| Int_to_reg (x_21161, x_21160) -> h_int_to_reg x_21161 x_21160
121| Int_to_acc (x_21163, x_21162) -> h_int_to_acc x_21163 x_21162
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_21170, x_21169) -> h_from_acc x_21170 x_21169
129| To_acc (x_21172, x_21171) -> h_to_acc x_21172 x_21171
130| Int_to_reg (x_21174, x_21173) -> h_int_to_reg x_21174 x_21173
131| Int_to_acc (x_21176, x_21175) -> h_int_to_acc x_21176 x_21175
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_21183, x_21182) -> h_from_acc x_21183 x_21182
139| To_acc (x_21185, x_21184) -> h_to_acc x_21185 x_21184
140| Int_to_reg (x_21187, x_21186) -> h_int_to_reg x_21187 x_21186
141| Int_to_acc (x_21189, x_21188) -> h_int_to_acc x_21189 x_21188
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_21196, x_21195) -> h_from_acc x_21196 x_21195
149| To_acc (x_21198, x_21197) -> h_to_acc x_21198 x_21197
150| Int_to_reg (x_21200, x_21199) -> h_int_to_reg x_21200 x_21199
151| Int_to_acc (x_21202, x_21201) -> h_int_to_acc x_21202 x_21201
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_21209, x_21208) -> h_from_acc x_21209 x_21208
159| To_acc (x_21211, x_21210) -> h_to_acc x_21211 x_21210
160| Int_to_reg (x_21213, x_21212) -> h_int_to_reg x_21213 x_21212
161| Int_to_acc (x_21215, x_21214) -> h_int_to_acc x_21215 x_21214
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_21222, x_21221) -> h_from_acc x_21222 x_21221
169| To_acc (x_21224, x_21223) -> h_to_acc x_21224 x_21223
170| Int_to_reg (x_21226, x_21225) -> h_int_to_reg x_21226 x_21225
171| Int_to_acc (x_21228, x_21227) -> h_int_to_acc x_21228 x_21227
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_21322, x_21321) -> h_LOW_ADDRESS x_21322 x_21321
244| HIGH_ADDRESS (x_21324, x_21323) -> h_HIGH_ADDRESS x_21324 x_21323
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_21331, x_21330) -> h_LOW_ADDRESS x_21331 x_21330
253| HIGH_ADDRESS (x_21333, x_21332) -> h_HIGH_ADDRESS x_21333 x_21332
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_21340, x_21339) -> h_LOW_ADDRESS x_21340 x_21339
262| HIGH_ADDRESS (x_21342, x_21341) -> h_HIGH_ADDRESS x_21342 x_21341
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_21349, x_21348) -> h_LOW_ADDRESS x_21349 x_21348
271| HIGH_ADDRESS (x_21351, x_21350) -> h_HIGH_ADDRESS x_21351 x_21350
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_21358, x_21357) -> h_LOW_ADDRESS x_21358 x_21357
280| HIGH_ADDRESS (x_21360, x_21359) -> h_HIGH_ADDRESS x_21360 x_21359
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_21367, x_21366) -> h_LOW_ADDRESS x_21367 x_21366
289| HIGH_ADDRESS (x_21369, x_21368) -> h_HIGH_ADDRESS x_21369 x_21368
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 : Joint.unserialized_params **)
352let lTL_LIN =
353  { Joint.ext_seq_labels = (Obj.magic ltl_lin_seq_labels);
354    Joint.has_tailcalls = Bool.False }
355
Note: See TracBrowser for help on using the repository browser.