source: driver/extracted/fixpoints.ml @ 3106

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

New extraction

File size: 10.1 KB
Line 
1open Preamble
2
3open Exp
4
5open Arithmetic
6
7open Integers
8
9open AST
10
11open Proper
12
13open PositiveMap
14
15open ErrorMessages
16
17open PreIdentifiers
18
19open Errors
20
21open Extralib
22
23open Lists
24
25open Positive
26
27open Identifiers
28
29open Deqsets
30
31open Setoids
32
33open Monad
34
35open Option
36
37open Extranat
38
39open Vector
40
41open Div_and_mod
42
43open Jmeq
44
45open Russell
46
47open List
48
49open Util
50
51open FoldStuff
52
53open Bool
54
55open Relations
56
57open Nat
58
59open BitVector
60
61open BitVectorTrie
62
63open Hints_declaration
64
65open Core_notation
66
67open Pts
68
69open Logic
70
71open Types
72
73open Graphs
74
75type property_lattice = { l_bottom : __; l_equal : (__ -> __ -> Bool.bool);
76                          l_included : (__ -> __ -> Bool.bool);
77                          l_is_maximal : (__ -> Bool.bool) }
78
79(** val property_lattice_rect_Type4 :
80    (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
81    Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
82let rec property_lattice_rect_Type4 h_mk_property_lattice x_18885 =
83  let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
84    l_is_maximal = l_is_maximal0 } = x_18885
85  in
86  h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
87
88(** val property_lattice_rect_Type5 :
89    (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
90    Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
91let rec property_lattice_rect_Type5 h_mk_property_lattice x_18887 =
92  let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
93    l_is_maximal = l_is_maximal0 } = x_18887
94  in
95  h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
96
97(** val property_lattice_rect_Type3 :
98    (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
99    Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
100let rec property_lattice_rect_Type3 h_mk_property_lattice x_18889 =
101  let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
102    l_is_maximal = l_is_maximal0 } = x_18889
103  in
104  h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
105
106(** val property_lattice_rect_Type2 :
107    (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
108    Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
109let rec property_lattice_rect_Type2 h_mk_property_lattice x_18891 =
110  let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
111    l_is_maximal = l_is_maximal0 } = x_18891
112  in
113  h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
114
115(** val property_lattice_rect_Type1 :
116    (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
117    Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
118let rec property_lattice_rect_Type1 h_mk_property_lattice x_18893 =
119  let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
120    l_is_maximal = l_is_maximal0 } = x_18893
121  in
122  h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
123
124(** val property_lattice_rect_Type0 :
125    (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
126    Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
127let rec property_lattice_rect_Type0 h_mk_property_lattice x_18895 =
128  let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
129    l_is_maximal = l_is_maximal0 } = x_18895
130  in
131  h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
132
133type l_property = __
134
135(** val l_bottom : property_lattice -> __ **)
136let rec l_bottom xxx =
137  xxx.l_bottom
138
139(** val l_equal : property_lattice -> __ -> __ -> Bool.bool **)
140let rec l_equal xxx =
141  xxx.l_equal
142
143(** val l_included : property_lattice -> __ -> __ -> Bool.bool **)
144let rec l_included xxx =
145  xxx.l_included
146
147(** val l_is_maximal : property_lattice -> __ -> Bool.bool **)
148let rec l_is_maximal xxx =
149  xxx.l_is_maximal
150
151(** val property_lattice_inv_rect_Type4 :
152    property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
153    Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1 **)
154let property_lattice_inv_rect_Type4 hterm h1 =
155  let hcut = property_lattice_rect_Type4 h1 hterm in hcut __
156
157(** val property_lattice_inv_rect_Type3 :
158    property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
159    Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1 **)
160let property_lattice_inv_rect_Type3 hterm h1 =
161  let hcut = property_lattice_rect_Type3 h1 hterm in hcut __
162
163(** val property_lattice_inv_rect_Type2 :
164    property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
165    Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1 **)
166let property_lattice_inv_rect_Type2 hterm h1 =
167  let hcut = property_lattice_rect_Type2 h1 hterm in hcut __
168
169(** val property_lattice_inv_rect_Type1 :
170    property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
171    Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1 **)
172let property_lattice_inv_rect_Type1 hterm h1 =
173  let hcut = property_lattice_rect_Type1 h1 hterm in hcut __
174
175(** val property_lattice_inv_rect_Type0 :
176    property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
177    Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1 **)
178let property_lattice_inv_rect_Type0 hterm h1 =
179  let hcut = property_lattice_rect_Type0 h1 hterm in hcut __
180
181(** val property_lattice_jmdiscr :
182    property_lattice -> property_lattice -> __ **)
183let property_lattice_jmdiscr x y =
184  Logic.eq_rect_Type2 x
185    (let { l_bottom = a1; l_equal = a2; l_included = a3; l_is_maximal =
186       a4 } = x
187     in
188    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
189
190type valuation = Graphs.label -> __
191
192type rhs = valuation -> __
193
194type equations = Graphs.label -> rhs
195
196type fixpoint =
197  valuation
198  (* singleton inductive, whose constructor was mk_fixpoint *)
199
200(** val fixpoint_rect_Type4 :
201    property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
202    'a1 **)
203let rec fixpoint_rect_Type4 latt eqs h_mk_fixpoint x_18916 =
204  let fix_lfp = x_18916 in h_mk_fixpoint fix_lfp __
205
206(** val fixpoint_rect_Type5 :
207    property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
208    'a1 **)
209let rec fixpoint_rect_Type5 latt eqs h_mk_fixpoint x_18918 =
210  let fix_lfp = x_18918 in h_mk_fixpoint fix_lfp __
211
212(** val fixpoint_rect_Type3 :
213    property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
214    'a1 **)
215let rec fixpoint_rect_Type3 latt eqs h_mk_fixpoint x_18920 =
216  let fix_lfp = x_18920 in h_mk_fixpoint fix_lfp __
217
218(** val fixpoint_rect_Type2 :
219    property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
220    'a1 **)
221let rec fixpoint_rect_Type2 latt eqs h_mk_fixpoint x_18922 =
222  let fix_lfp = x_18922 in h_mk_fixpoint fix_lfp __
223
224(** val fixpoint_rect_Type1 :
225    property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
226    'a1 **)
227let rec fixpoint_rect_Type1 latt eqs h_mk_fixpoint x_18924 =
228  let fix_lfp = x_18924 in h_mk_fixpoint fix_lfp __
229
230(** val fixpoint_rect_Type0 :
231    property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
232    'a1 **)
233let rec fixpoint_rect_Type0 latt eqs h_mk_fixpoint x_18926 =
234  let fix_lfp = x_18926 in h_mk_fixpoint fix_lfp __
235
236(** val fix_lfp : property_lattice -> equations -> fixpoint -> valuation **)
237let rec fix_lfp latt eqs xxx =
238  let yyy = xxx in yyy
239
240(** val fixpoint_inv_rect_Type4 :
241    property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ ->
242    'a1) -> 'a1 **)
243let fixpoint_inv_rect_Type4 x1 x2 hterm h1 =
244  let hcut = fixpoint_rect_Type4 x1 x2 h1 hterm in hcut __
245
246(** val fixpoint_inv_rect_Type3 :
247    property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ ->
248    'a1) -> 'a1 **)
249let fixpoint_inv_rect_Type3 x1 x2 hterm h1 =
250  let hcut = fixpoint_rect_Type3 x1 x2 h1 hterm in hcut __
251
252(** val fixpoint_inv_rect_Type2 :
253    property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ ->
254    'a1) -> 'a1 **)
255let fixpoint_inv_rect_Type2 x1 x2 hterm h1 =
256  let hcut = fixpoint_rect_Type2 x1 x2 h1 hterm in hcut __
257
258(** val fixpoint_inv_rect_Type1 :
259    property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ ->
260    'a1) -> 'a1 **)
261let fixpoint_inv_rect_Type1 x1 x2 hterm h1 =
262  let hcut = fixpoint_rect_Type1 x1 x2 h1 hterm in hcut __
263
264(** val fixpoint_inv_rect_Type0 :
265    property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ ->
266    'a1) -> 'a1 **)
267let fixpoint_inv_rect_Type0 x1 x2 hterm h1 =
268  let hcut = fixpoint_rect_Type0 x1 x2 h1 hterm in hcut __
269
270(** val fixpoint_discr :
271    property_lattice -> equations -> fixpoint -> fixpoint -> __ **)
272let fixpoint_discr a1 a2 x y =
273  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
274
275(** val fixpoint_jmdiscr :
276    property_lattice -> equations -> fixpoint -> fixpoint -> __ **)
277let fixpoint_jmdiscr a1 a2 x y =
278  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
279
280(** val dpi1__o__fix_lfp__o__inject :
281    property_lattice -> equations -> (fixpoint, 'a1) Types.dPair -> valuation
282    Types.sig0 **)
283let dpi1__o__fix_lfp__o__inject x0 x2 x4 =
284  fix_lfp x0 x2 x4.Types.dpi1
285
286(** val eject__o__fix_lfp__o__inject :
287    property_lattice -> equations -> fixpoint Types.sig0 -> valuation
288    Types.sig0 **)
289let eject__o__fix_lfp__o__inject x0 x2 x4 =
290  fix_lfp x0 x2 (Types.pi1 x4)
291
292(** val fix_lfp__o__inject :
293    property_lattice -> equations -> fixpoint -> valuation Types.sig0 **)
294let fix_lfp__o__inject x0 x2 x3 =
295  fix_lfp x0 x2 x3
296
297(** val dpi1__o__fix_lfp :
298    property_lattice -> equations -> (fixpoint, 'a1) Types.dPair -> valuation **)
299let dpi1__o__fix_lfp x0 x1 x3 =
300  fix_lfp x0 x1 x3.Types.dpi1
301
302(** val eject__o__fix_lfp :
303    property_lattice -> equations -> fixpoint Types.sig0 -> valuation **)
304let eject__o__fix_lfp x0 x1 x3 =
305  fix_lfp x0 x1 (Types.pi1 x3)
306
307type fixpoint_computer = property_lattice -> equations -> fixpoint
308
309(** val dpi1__o__apply_fixpoint :
310    property_lattice -> equations -> (fixpoint, 'a1) Types.dPair ->
311    Graphs.label -> __ **)
312let dpi1__o__apply_fixpoint x0 x1 x3 =
313  let latt = x0 in
314  let eqs = x1 in let f = x3.Types.dpi1 in (fun l -> fix_lfp latt eqs f l)
315
316(** val eject__o__apply_fixpoint :
317    property_lattice -> equations -> fixpoint Types.sig0 -> Graphs.label ->
318    __ **)
319let eject__o__apply_fixpoint x0 x1 x3 =
320  let latt = x0 in
321  let eqs = x1 in let f = Types.pi1 x3 in (fun l -> fix_lfp latt eqs f l)
322
Note: See TracBrowser for help on using the repository browser.