source: extracted/eRTLptr.ml @ 2773

Last change on this file since 2773 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 9.0 KB
RevLine 
[2717]1open Preamble
2
3open String
4
5open Sets
6
7open Listb
8
9open LabelledObjects
10
[2773]11open BitVectorTrie
12
[2717]13open Graphs
14
15open I8051
16
17open Order
18
19open Registers
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 Lists
40
41open Identifiers
42
43open Integers
44
45open AST
46
47open Division
48
49open Exp
50
51open Arithmetic
52
[2773]53open Setoids
54
55open Monad
56
57open Option
58
[2717]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
107open ERTL
108
109type ertlptr_seq =
110| Ertlptr_ertl of ERTL.ertl_seq
111| LOW_ADDRESS of Registers.register * Graphs.label
112| HIGH_ADDRESS of Registers.register * Graphs.label
113
114(** val ertlptr_seq_rect_Type4 :
115    (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
116    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
117let rec ertlptr_seq_rect_Type4 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
[2773]118| Ertlptr_ertl x_16345 -> h_ertlptr_ertl x_16345
119| LOW_ADDRESS (x_16347, x_16346) -> h_LOW_ADDRESS x_16347 x_16346
120| HIGH_ADDRESS (x_16349, x_16348) -> h_HIGH_ADDRESS x_16349 x_16348
[2717]121
122(** val ertlptr_seq_rect_Type5 :
123    (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
124    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
125let rec ertlptr_seq_rect_Type5 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
[2773]126| Ertlptr_ertl x_16354 -> h_ertlptr_ertl x_16354
127| LOW_ADDRESS (x_16356, x_16355) -> h_LOW_ADDRESS x_16356 x_16355
128| HIGH_ADDRESS (x_16358, x_16357) -> h_HIGH_ADDRESS x_16358 x_16357
[2717]129
130(** val ertlptr_seq_rect_Type3 :
131    (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
132    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
133let rec ertlptr_seq_rect_Type3 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
[2773]134| Ertlptr_ertl x_16363 -> h_ertlptr_ertl x_16363
135| LOW_ADDRESS (x_16365, x_16364) -> h_LOW_ADDRESS x_16365 x_16364
136| HIGH_ADDRESS (x_16367, x_16366) -> h_HIGH_ADDRESS x_16367 x_16366
[2717]137
138(** val ertlptr_seq_rect_Type2 :
139    (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
140    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
141let rec ertlptr_seq_rect_Type2 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
[2773]142| Ertlptr_ertl x_16372 -> h_ertlptr_ertl x_16372
143| LOW_ADDRESS (x_16374, x_16373) -> h_LOW_ADDRESS x_16374 x_16373
144| HIGH_ADDRESS (x_16376, x_16375) -> h_HIGH_ADDRESS x_16376 x_16375
[2717]145
146(** val ertlptr_seq_rect_Type1 :
147    (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
148    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
149let rec ertlptr_seq_rect_Type1 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
[2773]150| Ertlptr_ertl x_16381 -> h_ertlptr_ertl x_16381
151| LOW_ADDRESS (x_16383, x_16382) -> h_LOW_ADDRESS x_16383 x_16382
152| HIGH_ADDRESS (x_16385, x_16384) -> h_HIGH_ADDRESS x_16385 x_16384
[2717]153
154(** val ertlptr_seq_rect_Type0 :
155    (ERTL.ertl_seq -> 'a1) -> (Registers.register -> Graphs.label -> 'a1) ->
156    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
157let rec ertlptr_seq_rect_Type0 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
[2773]158| Ertlptr_ertl x_16390 -> h_ertlptr_ertl x_16390
159| LOW_ADDRESS (x_16392, x_16391) -> h_LOW_ADDRESS x_16392 x_16391
160| HIGH_ADDRESS (x_16394, x_16393) -> h_HIGH_ADDRESS x_16394 x_16393
[2717]161
162(** val ertlptr_seq_inv_rect_Type4 :
163    ertlptr_seq -> (ERTL.ertl_seq -> __ -> 'a1) -> (Registers.register ->
164    Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> __
165    -> 'a1) -> 'a1 **)
166let ertlptr_seq_inv_rect_Type4 hterm h1 h2 h3 =
167  let hcut = ertlptr_seq_rect_Type4 h1 h2 h3 hterm in hcut __
168
169(** val ertlptr_seq_inv_rect_Type3 :
170    ertlptr_seq -> (ERTL.ertl_seq -> __ -> 'a1) -> (Registers.register ->
171    Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> __
172    -> 'a1) -> 'a1 **)
173let ertlptr_seq_inv_rect_Type3 hterm h1 h2 h3 =
174  let hcut = ertlptr_seq_rect_Type3 h1 h2 h3 hterm in hcut __
175
176(** val ertlptr_seq_inv_rect_Type2 :
177    ertlptr_seq -> (ERTL.ertl_seq -> __ -> 'a1) -> (Registers.register ->
178    Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> __
179    -> 'a1) -> 'a1 **)
180let ertlptr_seq_inv_rect_Type2 hterm h1 h2 h3 =
181  let hcut = ertlptr_seq_rect_Type2 h1 h2 h3 hterm in hcut __
182
183(** val ertlptr_seq_inv_rect_Type1 :
184    ertlptr_seq -> (ERTL.ertl_seq -> __ -> 'a1) -> (Registers.register ->
185    Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> __
186    -> 'a1) -> 'a1 **)
187let ertlptr_seq_inv_rect_Type1 hterm h1 h2 h3 =
188  let hcut = ertlptr_seq_rect_Type1 h1 h2 h3 hterm in hcut __
189
190(** val ertlptr_seq_inv_rect_Type0 :
191    ertlptr_seq -> (ERTL.ertl_seq -> __ -> 'a1) -> (Registers.register ->
192    Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label -> __
193    -> 'a1) -> 'a1 **)
194let ertlptr_seq_inv_rect_Type0 hterm h1 h2 h3 =
195  let hcut = ertlptr_seq_rect_Type0 h1 h2 h3 hterm in hcut __
196
197(** val ertlptr_seq_discr : ertlptr_seq -> ertlptr_seq -> __ **)
198let ertlptr_seq_discr x y =
199  Logic.eq_rect_Type2 x
200    (match x with
201     | Ertlptr_ertl a0 -> Obj.magic (fun _ dH -> dH __)
202     | LOW_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
203     | HIGH_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
204
205(** val ertlptr_seq_jmdiscr : ertlptr_seq -> ertlptr_seq -> __ **)
206let ertlptr_seq_jmdiscr x y =
207  Logic.eq_rect_Type2 x
208    (match x with
209     | Ertlptr_ertl a0 -> Obj.magic (fun _ dH -> dH __)
210     | LOW_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
211     | HIGH_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
212
213(** val eRTLptr_uns : Joint.unserialized_params **)
214let eRTLptr_uns =
215  { Joint.ext_seq_labels = (fun s ->
216    match Obj.magic s with
217    | Ertlptr_ertl x -> List.Nil
218    | LOW_ADDRESS (x, l) -> List.Cons (l, List.Nil)
219    | HIGH_ADDRESS (x, l) -> List.Cons (l, List.Nil)); Joint.has_tailcalls =
220    Bool.False }
221
222(** val eRTLptr : Joint.graph_params **)
223let eRTLptr =
224  eRTLptr_uns
225
226type ertlptr_program = Joint.joint_program
227
228(** val ertlptr_seq_joint : AST.ident List.list -> __ -> Joint.joint_seq **)
229let ertlptr_seq_joint =
230  Obj.magic (fun _ x -> Joint.Extension_seq x)
231
[2743]232(** val dpi1__o__ertlptr_seq_to_joint_seq__o__inject :
233    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq
234    Types.sig0 **)
235let dpi1__o__ertlptr_seq_to_joint_seq__o__inject x1 x2 =
236  ertlptr_seq_joint x1 x2.Types.dpi1
237
238(** val dpi1__o__ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject :
239    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step
240    Types.sig0 **)
241let dpi1__o__ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
242  Joint.seq_to_step__o__inject
243    (Joint.gp_to_p__o__stmt_pars__o__uns_pars eRTLptr) x1
244    (ertlptr_seq_joint x1 x2.Types.dpi1)
245
246(** val dpi1__o__ertlptr_seq_to_joint_seq__o__seq_to_step :
247    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step **)
248let dpi1__o__ertlptr_seq_to_joint_seq__o__seq_to_step x1 x2 =
249  Joint.Step_seq (ertlptr_seq_joint x1 x2.Types.dpi1)
250
251(** val eject__o__ertlptr_seq_to_joint_seq__o__inject :
252    AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq Types.sig0 **)
253let eject__o__ertlptr_seq_to_joint_seq__o__inject x1 x2 =
254  ertlptr_seq_joint x1 (Types.pi1 x2)
255
256(** val eject__o__ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject :
257    AST.ident List.list -> __ Types.sig0 -> Joint.joint_step Types.sig0 **)
258let eject__o__ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
259  Joint.seq_to_step__o__inject
260    (Joint.gp_to_p__o__stmt_pars__o__uns_pars eRTLptr) x1
261    (ertlptr_seq_joint x1 (Types.pi1 x2))
262
263(** val eject__o__ertlptr_seq_to_joint_seq__o__seq_to_step :
264    AST.ident List.list -> __ Types.sig0 -> Joint.joint_step **)
265let eject__o__ertlptr_seq_to_joint_seq__o__seq_to_step x1 x2 =
266  Joint.Step_seq (ertlptr_seq_joint x1 (Types.pi1 x2))
267
268(** val ertlptr_seq_to_joint_seq__o__seq_to_step :
269    AST.ident List.list -> __ -> Joint.joint_step **)
270let ertlptr_seq_to_joint_seq__o__seq_to_step x0 x1 =
271  Joint.Step_seq (ertlptr_seq_joint x0 x1)
272
273(** val ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject :
274    AST.ident List.list -> __ -> Joint.joint_step Types.sig0 **)
275let ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject x0 x1 =
276  Joint.seq_to_step__o__inject
277    (Joint.gp_to_p__o__stmt_pars__o__uns_pars eRTLptr) x0
278    (ertlptr_seq_joint x0 x1)
279
280(** val ertlptr_seq_to_joint_seq__o__inject :
281    AST.ident List.list -> __ -> Joint.joint_seq Types.sig0 **)
282let ertlptr_seq_to_joint_seq__o__inject x0 x1 =
283  ertlptr_seq_joint x0 x1
284
285(** val dpi1__o__ertlptr_seq_to_joint_seq :
286    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq **)
287let dpi1__o__ertlptr_seq_to_joint_seq x1 x2 =
288  ertlptr_seq_joint x1 x2.Types.dpi1
289
290(** val eject__o__ertlptr_seq_to_joint_seq :
291    AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq **)
292let eject__o__ertlptr_seq_to_joint_seq x1 x2 =
293  ertlptr_seq_joint x1 (Types.pi1 x2)
294
Note: See TracBrowser for help on using the repository browser.