71 open Hints_declaration
90 (** val transrel_rect_Type4 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
91 let rec transrel_rect_Type4 h_mk_transrel = function
92 | Mk_transrel -> h_mk_transrel __ __ __
94 (** val transrel_rect_Type5 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
95 let rec transrel_rect_Type5 h_mk_transrel = function
96 | Mk_transrel -> h_mk_transrel __ __ __
98 (** val transrel_rect_Type3 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
99 let rec transrel_rect_Type3 h_mk_transrel = function
100 | Mk_transrel -> h_mk_transrel __ __ __
102 (** val transrel_rect_Type2 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
103 let rec transrel_rect_Type2 h_mk_transrel = function
104 | Mk_transrel -> h_mk_transrel __ __ __
106 (** val transrel_rect_Type1 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
107 let rec transrel_rect_Type1 h_mk_transrel = function
108 | Mk_transrel -> h_mk_transrel __ __ __
110 (** val transrel_rect_Type0 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
111 let rec transrel_rect_Type0 h_mk_transrel = function
112 | Mk_transrel -> h_mk_transrel __ __ __
118 (** val transrel_inv_rect_Type4 :
119 transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
120 let transrel_inv_rect_Type4 hterm h1 =
121 let hcut = transrel_rect_Type4 h1 hterm in hcut __
123 (** val transrel_inv_rect_Type3 :
124 transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
125 let transrel_inv_rect_Type3 hterm h1 =
126 let hcut = transrel_rect_Type3 h1 hterm in hcut __
128 (** val transrel_inv_rect_Type2 :
129 transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
130 let transrel_inv_rect_Type2 hterm h1 =
131 let hcut = transrel_rect_Type2 h1 hterm in hcut __
133 (** val transrel_inv_rect_Type1 :
134 transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
135 let transrel_inv_rect_Type1 hterm h1 =
136 let hcut = transrel_rect_Type1 h1 hterm in hcut __
138 (** val transrel_inv_rect_Type0 :
139 transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
140 let transrel_inv_rect_Type0 hterm h1 =
141 let hcut = transrel_rect_Type0 h1 hterm in hcut __
143 (** val transrel_jmdiscr : transrel -> transrel -> __ **)
144 let transrel_jmdiscr x y =
145 Logic.eq_rect_Type2 x
146 (let Mk_transrel = x in Obj.magic (fun _ dH -> dH __ __ __)) y
148 type program_behavior =
149 | Terminates of Events.trace * Integers.int
150 | Diverges of Events.trace
151 | Reacts of Events.traceinf
152 | Goes_wrong of Events.trace
154 (** val program_behavior_rect_Type4 :
155 (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
156 (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
158 let rec program_behavior_rect_Type4 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
159 | Terminates (x_6965, x_6964) -> h_Terminates x_6965 x_6964
160 | Diverges x_6966 -> h_Diverges x_6966
161 | Reacts x_6967 -> h_Reacts x_6967
162 | Goes_wrong x_6968 -> h_Goes_wrong x_6968
164 (** val program_behavior_rect_Type5 :
165 (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
166 (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
168 let rec program_behavior_rect_Type5 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
169 | Terminates (x_6975, x_6974) -> h_Terminates x_6975 x_6974
170 | Diverges x_6976 -> h_Diverges x_6976
171 | Reacts x_6977 -> h_Reacts x_6977
172 | Goes_wrong x_6978 -> h_Goes_wrong x_6978
174 (** val program_behavior_rect_Type3 :
175 (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
176 (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
178 let rec program_behavior_rect_Type3 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
179 | Terminates (x_6985, x_6984) -> h_Terminates x_6985 x_6984
180 | Diverges x_6986 -> h_Diverges x_6986
181 | Reacts x_6987 -> h_Reacts x_6987
182 | Goes_wrong x_6988 -> h_Goes_wrong x_6988
184 (** val program_behavior_rect_Type2 :
185 (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
186 (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
188 let rec program_behavior_rect_Type2 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
189 | Terminates (x_6995, x_6994) -> h_Terminates x_6995 x_6994
190 | Diverges x_6996 -> h_Diverges x_6996
191 | Reacts x_6997 -> h_Reacts x_6997
192 | Goes_wrong x_6998 -> h_Goes_wrong x_6998
194 (** val program_behavior_rect_Type1 :
195 (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
196 (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
198 let rec program_behavior_rect_Type1 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
199 | Terminates (x_7005, x_7004) -> h_Terminates x_7005 x_7004
200 | Diverges x_7006 -> h_Diverges x_7006
201 | Reacts x_7007 -> h_Reacts x_7007
202 | Goes_wrong x_7008 -> h_Goes_wrong x_7008
204 (** val program_behavior_rect_Type0 :
205 (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
206 (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
208 let rec program_behavior_rect_Type0 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
209 | Terminates (x_7015, x_7014) -> h_Terminates x_7015 x_7014
210 | Diverges x_7016 -> h_Diverges x_7016
211 | Reacts x_7017 -> h_Reacts x_7017
212 | Goes_wrong x_7018 -> h_Goes_wrong x_7018
214 (** val program_behavior_inv_rect_Type4 :
215 program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
216 (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
217 (Events.trace -> __ -> 'a1) -> 'a1 **)
218 let program_behavior_inv_rect_Type4 hterm h1 h2 h3 h4 =
219 let hcut = program_behavior_rect_Type4 h1 h2 h3 h4 hterm in hcut __
221 (** val program_behavior_inv_rect_Type3 :
222 program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
223 (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
224 (Events.trace -> __ -> 'a1) -> 'a1 **)
225 let program_behavior_inv_rect_Type3 hterm h1 h2 h3 h4 =
226 let hcut = program_behavior_rect_Type3 h1 h2 h3 h4 hterm in hcut __
228 (** val program_behavior_inv_rect_Type2 :
229 program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
230 (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
231 (Events.trace -> __ -> 'a1) -> 'a1 **)
232 let program_behavior_inv_rect_Type2 hterm h1 h2 h3 h4 =
233 let hcut = program_behavior_rect_Type2 h1 h2 h3 h4 hterm in hcut __
235 (** val program_behavior_inv_rect_Type1 :
236 program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
237 (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
238 (Events.trace -> __ -> 'a1) -> 'a1 **)
239 let program_behavior_inv_rect_Type1 hterm h1 h2 h3 h4 =
240 let hcut = program_behavior_rect_Type1 h1 h2 h3 h4 hterm in hcut __
242 (** val program_behavior_inv_rect_Type0 :
243 program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
244 (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
245 (Events.trace -> __ -> 'a1) -> 'a1 **)
246 let program_behavior_inv_rect_Type0 hterm h1 h2 h3 h4 =
247 let hcut = program_behavior_rect_Type0 h1 h2 h3 h4 hterm in hcut __
249 (** val program_behavior_discr :
250 program_behavior -> program_behavior -> __ **)
251 let program_behavior_discr x y =
252 Logic.eq_rect_Type2 x
254 | Terminates (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
255 | Diverges a0 -> Obj.magic (fun _ dH -> dH __)
256 | Reacts a0 -> Obj.magic (fun _ dH -> dH __)
257 | Goes_wrong a0 -> Obj.magic (fun _ dH -> dH __)) y
259 (** val program_behavior_jmdiscr :
260 program_behavior -> program_behavior -> __ **)
261 let program_behavior_jmdiscr x y =
262 Logic.eq_rect_Type2 x
264 | Terminates (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
265 | Diverges a0 -> Obj.magic (fun _ dH -> dH __)
266 | Reacts a0 -> Obj.magic (fun _ dH -> dH __)
267 | Goes_wrong a0 -> Obj.magic (fun _ dH -> dH __)) y
269 type semantics = { trans : transrel; ge : __ }
271 (** val semantics_rect_Type4 :
272 (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
273 let rec semantics_rect_Type4 h_mk_semantics x_7345 =
274 let { trans = trans0; ge = ge0 } = x_7345 in
275 h_mk_semantics trans0 __ __ ge0
277 (** val semantics_rect_Type5 :
278 (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
279 let rec semantics_rect_Type5 h_mk_semantics x_7347 =
280 let { trans = trans0; ge = ge0 } = x_7347 in
281 h_mk_semantics trans0 __ __ ge0
283 (** val semantics_rect_Type3 :
284 (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
285 let rec semantics_rect_Type3 h_mk_semantics x_7349 =
286 let { trans = trans0; ge = ge0 } = x_7349 in
287 h_mk_semantics trans0 __ __ ge0
289 (** val semantics_rect_Type2 :
290 (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
291 let rec semantics_rect_Type2 h_mk_semantics x_7351 =
292 let { trans = trans0; ge = ge0 } = x_7351 in
293 h_mk_semantics trans0 __ __ ge0
295 (** val semantics_rect_Type1 :
296 (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
297 let rec semantics_rect_Type1 h_mk_semantics x_7353 =
298 let { trans = trans0; ge = ge0 } = x_7353 in
299 h_mk_semantics trans0 __ __ ge0
301 (** val semantics_rect_Type0 :
302 (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
303 let rec semantics_rect_Type0 h_mk_semantics x_7355 =
304 let { trans = trans0; ge = ge0 } = x_7355 in
305 h_mk_semantics trans0 __ __ ge0
307 (** val trans : semantics -> transrel **)
311 (** val ge : semantics -> __ **)
315 (** val semantics_inv_rect_Type4 :
316 semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
317 let semantics_inv_rect_Type4 hterm h1 =
318 let hcut = semantics_rect_Type4 h1 hterm in hcut __
320 (** val semantics_inv_rect_Type3 :
321 semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
322 let semantics_inv_rect_Type3 hterm h1 =
323 let hcut = semantics_rect_Type3 h1 hterm in hcut __
325 (** val semantics_inv_rect_Type2 :
326 semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
327 let semantics_inv_rect_Type2 hterm h1 =
328 let hcut = semantics_rect_Type2 h1 hterm in hcut __
330 (** val semantics_inv_rect_Type1 :
331 semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
332 let semantics_inv_rect_Type1 hterm h1 =
333 let hcut = semantics_rect_Type1 h1 hterm in hcut __
335 (** val semantics_inv_rect_Type0 :
336 semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
337 let semantics_inv_rect_Type0 hterm h1 =
338 let hcut = semantics_rect_Type0 h1 hterm in hcut __
340 (** val semantics_jmdiscr : semantics -> semantics -> __ **)
341 let semantics_jmdiscr x y =
342 Logic.eq_rect_Type2 x
343 (let { trans = a0; ge = a3 } = x in
344 Obj.magic (fun _ dH -> dH __ __ __ __)) y
346 type related_semantics = { sem1 : semantics; sem2 : semantics }
348 (** val related_semantics_rect_Type4 :
349 (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
351 let rec related_semantics_rect_Type4 h_mk_related_semantics x_7374 =
352 let { sem1 = sem3; sem2 = sem4 } = x_7374 in
353 h_mk_related_semantics sem3 sem4 __ __ __
355 (** val related_semantics_rect_Type5 :
356 (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
358 let rec related_semantics_rect_Type5 h_mk_related_semantics x_7376 =
359 let { sem1 = sem3; sem2 = sem4 } = x_7376 in
360 h_mk_related_semantics sem3 sem4 __ __ __
362 (** val related_semantics_rect_Type3 :
363 (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
365 let rec related_semantics_rect_Type3 h_mk_related_semantics x_7378 =
366 let { sem1 = sem3; sem2 = sem4 } = x_7378 in
367 h_mk_related_semantics sem3 sem4 __ __ __
369 (** val related_semantics_rect_Type2 :
370 (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
372 let rec related_semantics_rect_Type2 h_mk_related_semantics x_7380 =
373 let { sem1 = sem3; sem2 = sem4 } = x_7380 in
374 h_mk_related_semantics sem3 sem4 __ __ __
376 (** val related_semantics_rect_Type1 :
377 (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
379 let rec related_semantics_rect_Type1 h_mk_related_semantics x_7382 =
380 let { sem1 = sem3; sem2 = sem4 } = x_7382 in
381 h_mk_related_semantics sem3 sem4 __ __ __
383 (** val related_semantics_rect_Type0 :
384 (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
386 let rec related_semantics_rect_Type0 h_mk_related_semantics x_7384 =
387 let { sem1 = sem3; sem2 = sem4 } = x_7384 in
388 h_mk_related_semantics sem3 sem4 __ __ __
390 (** val sem1 : related_semantics -> semantics **)
394 (** val sem2 : related_semantics -> semantics **)
398 (** val related_semantics_inv_rect_Type4 :
399 related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
401 let related_semantics_inv_rect_Type4 hterm h1 =
402 let hcut = related_semantics_rect_Type4 h1 hterm in hcut __
404 (** val related_semantics_inv_rect_Type3 :
405 related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
407 let related_semantics_inv_rect_Type3 hterm h1 =
408 let hcut = related_semantics_rect_Type3 h1 hterm in hcut __
410 (** val related_semantics_inv_rect_Type2 :
411 related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
413 let related_semantics_inv_rect_Type2 hterm h1 =
414 let hcut = related_semantics_rect_Type2 h1 hterm in hcut __
416 (** val related_semantics_inv_rect_Type1 :
417 related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
419 let related_semantics_inv_rect_Type1 hterm h1 =
420 let hcut = related_semantics_rect_Type1 h1 hterm in hcut __
422 (** val related_semantics_inv_rect_Type0 :
423 related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
425 let related_semantics_inv_rect_Type0 hterm h1 =
426 let hcut = related_semantics_rect_Type0 h1 hterm in hcut __
428 (** val related_semantics_jmdiscr :
429 related_semantics -> related_semantics -> __ **)
430 let related_semantics_jmdiscr x y =
431 Logic.eq_rect_Type2 x
432 (let { sem1 = a0; sem2 = a1 } = x in
433 Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
437 (* singleton inductive, whose constructor was mk_order_sim *)
439 (** val order_sim_rect_Type4 :
440 (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
441 let rec order_sim_rect_Type4 h_mk_order_sim x_7405 =
442 let sem = x_7405 in h_mk_order_sim sem __ __
444 (** val order_sim_rect_Type5 :
445 (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
446 let rec order_sim_rect_Type5 h_mk_order_sim x_7407 =
447 let sem = x_7407 in h_mk_order_sim sem __ __
449 (** val order_sim_rect_Type3 :
450 (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
451 let rec order_sim_rect_Type3 h_mk_order_sim x_7409 =
452 let sem = x_7409 in h_mk_order_sim sem __ __
454 (** val order_sim_rect_Type2 :
455 (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
456 let rec order_sim_rect_Type2 h_mk_order_sim x_7411 =
457 let sem = x_7411 in h_mk_order_sim sem __ __
459 (** val order_sim_rect_Type1 :
460 (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
461 let rec order_sim_rect_Type1 h_mk_order_sim x_7413 =
462 let sem = x_7413 in h_mk_order_sim sem __ __
464 (** val order_sim_rect_Type0 :
465 (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
466 let rec order_sim_rect_Type0 h_mk_order_sim x_7415 =
467 let sem = x_7415 in h_mk_order_sim sem __ __
469 (** val sem : order_sim -> related_semantics **)
473 (** val order_sim_inv_rect_Type4 :
474 order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
475 let order_sim_inv_rect_Type4 hterm h1 =
476 let hcut = order_sim_rect_Type4 h1 hterm in hcut __
478 (** val order_sim_inv_rect_Type3 :
479 order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
480 let order_sim_inv_rect_Type3 hterm h1 =
481 let hcut = order_sim_rect_Type3 h1 hterm in hcut __
483 (** val order_sim_inv_rect_Type2 :
484 order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
485 let order_sim_inv_rect_Type2 hterm h1 =
486 let hcut = order_sim_rect_Type2 h1 hterm in hcut __
488 (** val order_sim_inv_rect_Type1 :
489 order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
490 let order_sim_inv_rect_Type1 hterm h1 =
491 let hcut = order_sim_rect_Type1 h1 hterm in hcut __
493 (** val order_sim_inv_rect_Type0 :
494 order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
495 let order_sim_inv_rect_Type0 hterm h1 =
496 let hcut = order_sim_rect_Type0 h1 hterm in hcut __
498 (** val order_sim_jmdiscr : order_sim -> order_sim -> __ **)
499 let order_sim_jmdiscr x y =
500 Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __ __)) y