source: extracted/joint_LTL_LIN.ml @ 2731

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

Exported again.

File size: 12.5 KB
RevLine 
[2717]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
[2730]118| From_acc (x_7486, x_7485) -> h_from_acc x_7486 x_7485
119| To_acc (x_7488, x_7487) -> h_to_acc x_7488 x_7487
120| Int_to_reg (x_7490, x_7489) -> h_int_to_reg x_7490 x_7489
121| Int_to_acc (x_7492, x_7491) -> h_int_to_acc x_7492 x_7491
[2717]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
[2730]128| From_acc (x_7499, x_7498) -> h_from_acc x_7499 x_7498
129| To_acc (x_7501, x_7500) -> h_to_acc x_7501 x_7500
130| Int_to_reg (x_7503, x_7502) -> h_int_to_reg x_7503 x_7502
131| Int_to_acc (x_7505, x_7504) -> h_int_to_acc x_7505 x_7504
[2717]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
[2730]138| From_acc (x_7512, x_7511) -> h_from_acc x_7512 x_7511
139| To_acc (x_7514, x_7513) -> h_to_acc x_7514 x_7513
140| Int_to_reg (x_7516, x_7515) -> h_int_to_reg x_7516 x_7515
141| Int_to_acc (x_7518, x_7517) -> h_int_to_acc x_7518 x_7517
[2717]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
[2730]148| From_acc (x_7525, x_7524) -> h_from_acc x_7525 x_7524
149| To_acc (x_7527, x_7526) -> h_to_acc x_7527 x_7526
150| Int_to_reg (x_7529, x_7528) -> h_int_to_reg x_7529 x_7528
151| Int_to_acc (x_7531, x_7530) -> h_int_to_acc x_7531 x_7530
[2717]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
[2730]158| From_acc (x_7538, x_7537) -> h_from_acc x_7538 x_7537
159| To_acc (x_7540, x_7539) -> h_to_acc x_7540 x_7539
160| Int_to_reg (x_7542, x_7541) -> h_int_to_reg x_7542 x_7541
161| Int_to_acc (x_7544, x_7543) -> h_int_to_acc x_7544 x_7543
[2717]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
[2730]168| From_acc (x_7551, x_7550) -> h_from_acc x_7551 x_7550
169| To_acc (x_7553, x_7552) -> h_to_acc x_7553 x_7552
170| Int_to_reg (x_7555, x_7554) -> h_int_to_reg x_7555 x_7554
171| Int_to_acc (x_7557, x_7556) -> h_int_to_acc x_7557 x_7556
[2717]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
[2730]243| LOW_ADDRESS (x_7651, x_7650) -> h_LOW_ADDRESS x_7651 x_7650
244| HIGH_ADDRESS (x_7653, x_7652) -> h_HIGH_ADDRESS x_7653 x_7652
[2717]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
[2730]252| LOW_ADDRESS (x_7660, x_7659) -> h_LOW_ADDRESS x_7660 x_7659
253| HIGH_ADDRESS (x_7662, x_7661) -> h_HIGH_ADDRESS x_7662 x_7661
[2717]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
[2730]261| LOW_ADDRESS (x_7669, x_7668) -> h_LOW_ADDRESS x_7669 x_7668
262| HIGH_ADDRESS (x_7671, x_7670) -> h_HIGH_ADDRESS x_7671 x_7670
[2717]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
[2730]270| LOW_ADDRESS (x_7678, x_7677) -> h_LOW_ADDRESS x_7678 x_7677
271| HIGH_ADDRESS (x_7680, x_7679) -> h_HIGH_ADDRESS x_7680 x_7679
[2717]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
[2730]279| LOW_ADDRESS (x_7687, x_7686) -> h_LOW_ADDRESS x_7687 x_7686
280| HIGH_ADDRESS (x_7689, x_7688) -> h_HIGH_ADDRESS x_7689 x_7688
[2717]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
[2730]288| LOW_ADDRESS (x_7696, x_7695) -> h_LOW_ADDRESS x_7696 x_7695
289| HIGH_ADDRESS (x_7698, x_7697) -> h_HIGH_ADDRESS x_7698 x_7697
[2717]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.