63 open Hints_declaration
75 type property_lattice = { l_bottom : __; l_equal : (__ -> __ -> Bool.bool);
76 l_included : (__ -> __ -> Bool.bool);
77 l_is_maximal : (__ -> Bool.bool) }
79 (** val property_lattice_rect_Type4 :
80 (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
81 Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
82 let 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
86 h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
88 (** val property_lattice_rect_Type5 :
89 (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
90 Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
91 let 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
95 h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
97 (** val property_lattice_rect_Type3 :
98 (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
99 Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
100 let 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
104 h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
106 (** val property_lattice_rect_Type2 :
107 (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
108 Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
109 let 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
113 h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
115 (** val property_lattice_rect_Type1 :
116 (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
117 Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
118 let 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
122 h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
124 (** val property_lattice_rect_Type0 :
125 (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
126 Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
127 let 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
131 h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
135 (** val l_bottom : property_lattice -> __ **)
136 let rec l_bottom xxx =
139 (** val l_equal : property_lattice -> __ -> __ -> Bool.bool **)
140 let rec l_equal xxx =
143 (** val l_included : property_lattice -> __ -> __ -> Bool.bool **)
144 let rec l_included xxx =
147 (** val l_is_maximal : property_lattice -> __ -> Bool.bool **)
148 let rec l_is_maximal xxx =
151 (** val property_lattice_inv_rect_Type4 :
152 property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
153 Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1 **)
154 let property_lattice_inv_rect_Type4 hterm h1 =
155 let hcut = property_lattice_rect_Type4 h1 hterm in hcut __
157 (** val property_lattice_inv_rect_Type3 :
158 property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
159 Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1 **)
160 let property_lattice_inv_rect_Type3 hterm h1 =
161 let hcut = property_lattice_rect_Type3 h1 hterm in hcut __
163 (** val property_lattice_inv_rect_Type2 :
164 property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
165 Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1 **)
166 let property_lattice_inv_rect_Type2 hterm h1 =
167 let hcut = property_lattice_rect_Type2 h1 hterm in hcut __
169 (** val property_lattice_inv_rect_Type1 :
170 property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
171 Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1 **)
172 let property_lattice_inv_rect_Type1 hterm h1 =
173 let hcut = property_lattice_rect_Type1 h1 hterm in hcut __
175 (** val property_lattice_inv_rect_Type0 :
176 property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
177 Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1 **)
178 let property_lattice_inv_rect_Type0 hterm h1 =
179 let hcut = property_lattice_rect_Type0 h1 hterm in hcut __
181 (** val property_lattice_jmdiscr :
182 property_lattice -> property_lattice -> __ **)
183 let 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 =
188 Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
190 type valuation = Graphs.label -> __
192 type rhs = valuation -> __
194 type equations = Graphs.label -> rhs
198 (* singleton inductive, whose constructor was mk_fixpoint *)
200 (** val fixpoint_rect_Type4 :
201 property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
203 let rec fixpoint_rect_Type4 latt eqs h_mk_fixpoint x_18916 =
204 let fix_lfp = x_18916 in h_mk_fixpoint fix_lfp __
206 (** val fixpoint_rect_Type5 :
207 property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
209 let rec fixpoint_rect_Type5 latt eqs h_mk_fixpoint x_18918 =
210 let fix_lfp = x_18918 in h_mk_fixpoint fix_lfp __
212 (** val fixpoint_rect_Type3 :
213 property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
215 let rec fixpoint_rect_Type3 latt eqs h_mk_fixpoint x_18920 =
216 let fix_lfp = x_18920 in h_mk_fixpoint fix_lfp __
218 (** val fixpoint_rect_Type2 :
219 property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
221 let rec fixpoint_rect_Type2 latt eqs h_mk_fixpoint x_18922 =
222 let fix_lfp = x_18922 in h_mk_fixpoint fix_lfp __
224 (** val fixpoint_rect_Type1 :
225 property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
227 let rec fixpoint_rect_Type1 latt eqs h_mk_fixpoint x_18924 =
228 let fix_lfp = x_18924 in h_mk_fixpoint fix_lfp __
230 (** val fixpoint_rect_Type0 :
231 property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
233 let rec fixpoint_rect_Type0 latt eqs h_mk_fixpoint x_18926 =
234 let fix_lfp = x_18926 in h_mk_fixpoint fix_lfp __
236 (** val fix_lfp : property_lattice -> equations -> fixpoint -> valuation **)
237 let rec fix_lfp latt eqs xxx =
240 (** val fixpoint_inv_rect_Type4 :
241 property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ ->
243 let fixpoint_inv_rect_Type4 x1 x2 hterm h1 =
244 let hcut = fixpoint_rect_Type4 x1 x2 h1 hterm in hcut __
246 (** val fixpoint_inv_rect_Type3 :
247 property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ ->
249 let fixpoint_inv_rect_Type3 x1 x2 hterm h1 =
250 let hcut = fixpoint_rect_Type3 x1 x2 h1 hterm in hcut __
252 (** val fixpoint_inv_rect_Type2 :
253 property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ ->
255 let fixpoint_inv_rect_Type2 x1 x2 hterm h1 =
256 let hcut = fixpoint_rect_Type2 x1 x2 h1 hterm in hcut __
258 (** val fixpoint_inv_rect_Type1 :
259 property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ ->
261 let fixpoint_inv_rect_Type1 x1 x2 hterm h1 =
262 let hcut = fixpoint_rect_Type1 x1 x2 h1 hterm in hcut __
264 (** val fixpoint_inv_rect_Type0 :
265 property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ ->
267 let fixpoint_inv_rect_Type0 x1 x2 hterm h1 =
268 let hcut = fixpoint_rect_Type0 x1 x2 h1 hterm in hcut __
270 (** val fixpoint_discr :
271 property_lattice -> equations -> fixpoint -> fixpoint -> __ **)
272 let fixpoint_discr a1 a2 x y =
273 Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
275 (** val fixpoint_jmdiscr :
276 property_lattice -> equations -> fixpoint -> fixpoint -> __ **)
277 let fixpoint_jmdiscr a1 a2 x y =
278 Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
280 (** val dpi1__o__fix_lfp__o__inject :
281 property_lattice -> equations -> (fixpoint, 'a1) Types.dPair -> valuation
283 let dpi1__o__fix_lfp__o__inject x0 x2 x4 =
284 fix_lfp x0 x2 x4.Types.dpi1
286 (** val eject__o__fix_lfp__o__inject :
287 property_lattice -> equations -> fixpoint Types.sig0 -> valuation
289 let eject__o__fix_lfp__o__inject x0 x2 x4 =
290 fix_lfp x0 x2 (Types.pi1 x4)
292 (** val fix_lfp__o__inject :
293 property_lattice -> equations -> fixpoint -> valuation Types.sig0 **)
294 let fix_lfp__o__inject x0 x2 x3 =
297 (** val dpi1__o__fix_lfp :
298 property_lattice -> equations -> (fixpoint, 'a1) Types.dPair -> valuation **)
299 let dpi1__o__fix_lfp x0 x1 x3 =
300 fix_lfp x0 x1 x3.Types.dpi1
302 (** val eject__o__fix_lfp :
303 property_lattice -> equations -> fixpoint Types.sig0 -> valuation **)
304 let eject__o__fix_lfp x0 x1 x3 =
305 fix_lfp x0 x1 (Types.pi1 x3)
307 type fixpoint_computer = property_lattice -> equations -> fixpoint
309 (** val dpi1__o__apply_fixpoint :
310 property_lattice -> equations -> (fixpoint, 'a1) Types.dPair ->
311 Graphs.label -> __ **)
312 let dpi1__o__apply_fixpoint x0 x1 x3 =
314 let eqs = x1 in let f = x3.Types.dpi1 in (fun l -> fix_lfp latt eqs f l)
316 (** val eject__o__apply_fixpoint :
317 property_lattice -> equations -> fixpoint Types.sig0 -> Graphs.label ->
319 let eject__o__apply_fixpoint x0 x1 x3 =
321 let eqs = x1 in let f = Types.pi1 x3 in (fun l -> fix_lfp latt eqs f l)