104 (** val status_class_rect_Type4 :
105 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
106 let rec status_class_rect_Type4 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
107 | Cl_return -> h_cl_return
108 | Cl_jump -> h_cl_jump
109 | Cl_call -> h_cl_call
110 | Cl_tailcall -> h_cl_tailcall
111 | Cl_other -> h_cl_other
113 (** val status_class_rect_Type5 :
114 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
115 let rec status_class_rect_Type5 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
116 | Cl_return -> h_cl_return
117 | Cl_jump -> h_cl_jump
118 | Cl_call -> h_cl_call
119 | Cl_tailcall -> h_cl_tailcall
120 | Cl_other -> h_cl_other
122 (** val status_class_rect_Type3 :
123 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
124 let rec status_class_rect_Type3 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
125 | Cl_return -> h_cl_return
126 | Cl_jump -> h_cl_jump
127 | Cl_call -> h_cl_call
128 | Cl_tailcall -> h_cl_tailcall
129 | Cl_other -> h_cl_other
131 (** val status_class_rect_Type2 :
132 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
133 let rec status_class_rect_Type2 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
134 | Cl_return -> h_cl_return
135 | Cl_jump -> h_cl_jump
136 | Cl_call -> h_cl_call
137 | Cl_tailcall -> h_cl_tailcall
138 | Cl_other -> h_cl_other
140 (** val status_class_rect_Type1 :
141 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
142 let rec status_class_rect_Type1 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
143 | Cl_return -> h_cl_return
144 | Cl_jump -> h_cl_jump
145 | Cl_call -> h_cl_call
146 | Cl_tailcall -> h_cl_tailcall
147 | Cl_other -> h_cl_other
149 (** val status_class_rect_Type0 :
150 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
151 let rec status_class_rect_Type0 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
152 | Cl_return -> h_cl_return
153 | Cl_jump -> h_cl_jump
154 | Cl_call -> h_cl_call
155 | Cl_tailcall -> h_cl_tailcall
156 | Cl_other -> h_cl_other
158 (** val status_class_inv_rect_Type4 :
159 status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
160 -> (__ -> 'a1) -> 'a1 **)
161 let status_class_inv_rect_Type4 hterm h1 h2 h3 h4 h5 =
162 let hcut = status_class_rect_Type4 h1 h2 h3 h4 h5 hterm in hcut __
164 (** val status_class_inv_rect_Type3 :
165 status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
166 -> (__ -> 'a1) -> 'a1 **)
167 let status_class_inv_rect_Type3 hterm h1 h2 h3 h4 h5 =
168 let hcut = status_class_rect_Type3 h1 h2 h3 h4 h5 hterm in hcut __
170 (** val status_class_inv_rect_Type2 :
171 status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
172 -> (__ -> 'a1) -> 'a1 **)
173 let status_class_inv_rect_Type2 hterm h1 h2 h3 h4 h5 =
174 let hcut = status_class_rect_Type2 h1 h2 h3 h4 h5 hterm in hcut __
176 (** val status_class_inv_rect_Type1 :
177 status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
178 -> (__ -> 'a1) -> 'a1 **)
179 let status_class_inv_rect_Type1 hterm h1 h2 h3 h4 h5 =
180 let hcut = status_class_rect_Type1 h1 h2 h3 h4 h5 hterm in hcut __
182 (** val status_class_inv_rect_Type0 :
183 status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
184 -> (__ -> 'a1) -> 'a1 **)
185 let status_class_inv_rect_Type0 hterm h1 h2 h3 h4 h5 =
186 let hcut = status_class_rect_Type0 h1 h2 h3 h4 h5 hterm in hcut __
188 (** val status_class_discr : status_class -> status_class -> __ **)
189 let status_class_discr x y =
190 Logic.eq_rect_Type2 x
192 | Cl_return -> Obj.magic (fun _ dH -> dH)
193 | Cl_jump -> Obj.magic (fun _ dH -> dH)
194 | Cl_call -> Obj.magic (fun _ dH -> dH)
195 | Cl_tailcall -> Obj.magic (fun _ dH -> dH)
196 | Cl_other -> Obj.magic (fun _ dH -> dH)) y
198 (** val status_class_jmdiscr : status_class -> status_class -> __ **)
199 let status_class_jmdiscr x y =
200 Logic.eq_rect_Type2 x
202 | Cl_return -> Obj.magic (fun _ dH -> dH)
203 | Cl_jump -> Obj.magic (fun _ dH -> dH)
204 | Cl_call -> Obj.magic (fun _ dH -> dH)
205 | Cl_tailcall -> Obj.magic (fun _ dH -> dH)
206 | Cl_other -> Obj.magic (fun _ dH -> dH)) y
208 type abstract_status = { as_pc : Deqsets.deqSet; as_pc_of : (__ -> __);
209 as_classify : (__ -> status_class);
210 as_label_of_pc : (__ -> CostLabel.costlabel
212 as_result : (__ -> Integers.int Types.option);
213 as_call_ident : (__ Types.sig0 -> AST.ident);
214 as_tailcall_ident : (__ Types.sig0 -> AST.ident) }
216 (** val abstract_status_rect_Type4 :
217 (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
218 -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
219 Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
220 AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
221 let rec abstract_status_rect_Type4 h_mk_abstract_status x_22380 =
222 let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
223 as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
224 as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22380
226 h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
227 as_result0 as_call_ident0 as_tailcall_ident0
229 (** val abstract_status_rect_Type5 :
230 (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
231 -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
232 Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
233 AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
234 let rec abstract_status_rect_Type5 h_mk_abstract_status x_22382 =
235 let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
236 as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
237 as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22382
239 h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
240 as_result0 as_call_ident0 as_tailcall_ident0
242 (** val abstract_status_rect_Type3 :
243 (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
244 -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
245 Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
246 AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
247 let rec abstract_status_rect_Type3 h_mk_abstract_status x_22384 =
248 let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
249 as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
250 as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22384
252 h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
253 as_result0 as_call_ident0 as_tailcall_ident0
255 (** val abstract_status_rect_Type2 :
256 (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
257 -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
258 Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
259 AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
260 let rec abstract_status_rect_Type2 h_mk_abstract_status x_22386 =
261 let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
262 as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
263 as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22386
265 h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
266 as_result0 as_call_ident0 as_tailcall_ident0
268 (** val abstract_status_rect_Type1 :
269 (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
270 -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
271 Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
272 AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
273 let rec abstract_status_rect_Type1 h_mk_abstract_status x_22388 =
274 let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
275 as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
276 as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22388
278 h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
279 as_result0 as_call_ident0 as_tailcall_ident0
281 (** val abstract_status_rect_Type0 :
282 (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
283 -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
284 Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
285 AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
286 let rec abstract_status_rect_Type0 h_mk_abstract_status x_22390 =
287 let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
288 as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
289 as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22390
291 h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
292 as_result0 as_call_ident0 as_tailcall_ident0
296 (** val as_pc : abstract_status -> Deqsets.deqSet **)
300 (** val as_pc_of : abstract_status -> __ -> __ **)
301 let rec as_pc_of xxx =
304 (** val as_classify : abstract_status -> __ -> status_class **)
305 let rec as_classify xxx =
308 (** val as_label_of_pc :
309 abstract_status -> __ -> CostLabel.costlabel Types.option **)
310 let rec as_label_of_pc xxx =
313 (** val as_result : abstract_status -> __ -> Integers.int Types.option **)
314 let rec as_result xxx =
317 (** val as_call_ident : abstract_status -> __ Types.sig0 -> AST.ident **)
318 let rec as_call_ident xxx =
321 (** val as_tailcall_ident : abstract_status -> __ Types.sig0 -> AST.ident **)
322 let rec as_tailcall_ident xxx =
323 xxx.as_tailcall_ident
325 (** val abstract_status_inv_rect_Type4 :
326 abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
327 status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
328 Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
329 Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
330 let abstract_status_inv_rect_Type4 hterm h1 =
331 let hcut = abstract_status_rect_Type4 h1 hterm in hcut __
333 (** val abstract_status_inv_rect_Type3 :
334 abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
335 status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
336 Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
337 Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
338 let abstract_status_inv_rect_Type3 hterm h1 =
339 let hcut = abstract_status_rect_Type3 h1 hterm in hcut __
341 (** val abstract_status_inv_rect_Type2 :
342 abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
343 status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
344 Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
345 Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
346 let abstract_status_inv_rect_Type2 hterm h1 =
347 let hcut = abstract_status_rect_Type2 h1 hterm in hcut __
349 (** val abstract_status_inv_rect_Type1 :
350 abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
351 status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
352 Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
353 Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
354 let abstract_status_inv_rect_Type1 hterm h1 =
355 let hcut = abstract_status_rect_Type1 h1 hterm in hcut __
357 (** val abstract_status_inv_rect_Type0 :
358 abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
359 status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
360 Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
361 Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
362 let abstract_status_inv_rect_Type0 hterm h1 =
363 let hcut = abstract_status_rect_Type0 h1 hterm in hcut __
365 (** val abstract_status_jmdiscr :
366 abstract_status -> abstract_status -> __ **)
367 let abstract_status_jmdiscr x y =
368 Logic.eq_rect_Type2 x
369 (let { as_pc = a2; as_pc_of = a3; as_classify = a4; as_label_of_pc = a5;
370 as_result = a7; as_call_ident = a8; as_tailcall_ident = a9 } = x
372 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)) y
375 abstract_status -> __ -> CostLabel.costlabel Types.option **)
377 s.as_label_of_pc (s.as_pc_of s0)
379 (** val as_costed_exc : abstract_status -> __ -> (__, __) Types.sum **)
380 let as_costed_exc s s0 =
381 match as_label s s0 with
382 | Types.None -> Types.Inr __
383 | Types.Some c -> Types.Inl __
385 type as_cost_label = CostLabel.costlabel Types.sig0
387 type as_cost_labels = as_cost_label List.list
389 (** val as_cost_get_label :
390 abstract_status -> as_cost_label -> CostLabel.costlabel **)
391 let as_cost_get_label s l_sig =
394 type as_cost_map = as_cost_label -> Nat.nat
396 (** val as_label_safe : abstract_status -> __ Types.sig0 -> as_cost_label **)
397 let as_label_safe a_s st_sig =
398 Option.opt_safe (as_label a_s (Types.pi1 st_sig))
400 (** val lift_sigma_map_id :
401 'a2 -> ('a1 -> (__, __) Types.sum) -> ('a1 Types.sig0 -> 'a2) -> 'a1
402 Types.sig0 -> 'a2 **)
403 let lift_sigma_map_id dflt dec m a_sig =
404 match dec (Types.pi1 a_sig) with
405 | Types.Inl _ -> m (Types.pi1 a_sig)
406 | Types.Inr _ -> dflt
408 (** val lift_cost_map_id :
409 abstract_status -> abstract_status -> (CostLabel.costlabel -> (__, __)
410 Types.sum) -> as_cost_map -> as_cost_map **)
411 let lift_cost_map_id s_in s_out =
412 lift_sigma_map_id Nat.O
414 type trace_ends_with_ret =
416 | Doesnt_end_with_ret
418 (** val trace_ends_with_ret_rect_Type4 :
419 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
420 let rec trace_ends_with_ret_rect_Type4 h_ends_with_ret h_doesnt_end_with_ret = function
421 | Ends_with_ret -> h_ends_with_ret
422 | Doesnt_end_with_ret -> h_doesnt_end_with_ret
424 (** val trace_ends_with_ret_rect_Type5 :
425 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
426 let rec trace_ends_with_ret_rect_Type5 h_ends_with_ret h_doesnt_end_with_ret = function
427 | Ends_with_ret -> h_ends_with_ret
428 | Doesnt_end_with_ret -> h_doesnt_end_with_ret
430 (** val trace_ends_with_ret_rect_Type3 :
431 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
432 let rec trace_ends_with_ret_rect_Type3 h_ends_with_ret h_doesnt_end_with_ret = function
433 | Ends_with_ret -> h_ends_with_ret
434 | Doesnt_end_with_ret -> h_doesnt_end_with_ret
436 (** val trace_ends_with_ret_rect_Type2 :
437 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
438 let rec trace_ends_with_ret_rect_Type2 h_ends_with_ret h_doesnt_end_with_ret = function
439 | Ends_with_ret -> h_ends_with_ret
440 | Doesnt_end_with_ret -> h_doesnt_end_with_ret
442 (** val trace_ends_with_ret_rect_Type1 :
443 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
444 let rec trace_ends_with_ret_rect_Type1 h_ends_with_ret h_doesnt_end_with_ret = function
445 | Ends_with_ret -> h_ends_with_ret
446 | Doesnt_end_with_ret -> h_doesnt_end_with_ret
448 (** val trace_ends_with_ret_rect_Type0 :
449 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
450 let rec trace_ends_with_ret_rect_Type0 h_ends_with_ret h_doesnt_end_with_ret = function
451 | Ends_with_ret -> h_ends_with_ret
452 | Doesnt_end_with_ret -> h_doesnt_end_with_ret
454 (** val trace_ends_with_ret_inv_rect_Type4 :
455 trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
456 let trace_ends_with_ret_inv_rect_Type4 hterm h1 h2 =
457 let hcut = trace_ends_with_ret_rect_Type4 h1 h2 hterm in hcut __
459 (** val trace_ends_with_ret_inv_rect_Type3 :
460 trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
461 let trace_ends_with_ret_inv_rect_Type3 hterm h1 h2 =
462 let hcut = trace_ends_with_ret_rect_Type3 h1 h2 hterm in hcut __
464 (** val trace_ends_with_ret_inv_rect_Type2 :
465 trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
466 let trace_ends_with_ret_inv_rect_Type2 hterm h1 h2 =
467 let hcut = trace_ends_with_ret_rect_Type2 h1 h2 hterm in hcut __
469 (** val trace_ends_with_ret_inv_rect_Type1 :
470 trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
471 let trace_ends_with_ret_inv_rect_Type1 hterm h1 h2 =
472 let hcut = trace_ends_with_ret_rect_Type1 h1 h2 hterm in hcut __
474 (** val trace_ends_with_ret_inv_rect_Type0 :
475 trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
476 let trace_ends_with_ret_inv_rect_Type0 hterm h1 h2 =
477 let hcut = trace_ends_with_ret_rect_Type0 h1 h2 hterm in hcut __
479 (** val trace_ends_with_ret_discr :
480 trace_ends_with_ret -> trace_ends_with_ret -> __ **)
481 let trace_ends_with_ret_discr x y =
482 Logic.eq_rect_Type2 x
484 | Ends_with_ret -> Obj.magic (fun _ dH -> dH)
485 | Doesnt_end_with_ret -> Obj.magic (fun _ dH -> dH)) y
487 (** val trace_ends_with_ret_jmdiscr :
488 trace_ends_with_ret -> trace_ends_with_ret -> __ **)
489 let trace_ends_with_ret_jmdiscr x y =
490 Logic.eq_rect_Type2 x
492 | Ends_with_ret -> Obj.magic (fun _ dH -> dH)
493 | Doesnt_end_with_ret -> Obj.magic (fun _ dH -> dH)) y
495 type trace_label_return =
496 | Tlr_base of __ * __ * trace_label_label
497 | Tlr_step of __ * __ * __ * trace_label_label * trace_label_return
498 and trace_label_label =
499 | Tll_base of trace_ends_with_ret * __ * __ * trace_any_label
500 and trace_any_label =
501 | Tal_base_not_return of __ * __
502 | Tal_base_return of __ * __
503 | Tal_base_call of __ * __ * __ * trace_label_return
504 | Tal_base_tailcall of __ * __ * __ * trace_label_return
505 | Tal_step_call of trace_ends_with_ret * __ * __ * __ * __
506 * trace_label_return * trace_any_label
507 | Tal_step_default of trace_ends_with_ret * __ * __ * __ * trace_any_label
509 (** val trace_label_return_inv_rect_Type4 :
510 abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
511 trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
512 trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
513 let trace_label_return_inv_rect_Type4 x1 x2 x3 hterm h1 h2 =
516 | Tlr_base (x, x0, x4) -> h1 x x0 x4
517 | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
521 (** val trace_label_return_inv_rect_Type3 :
522 abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
523 trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
524 trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
525 let trace_label_return_inv_rect_Type3 x1 x2 x3 hterm h1 h2 =
528 | Tlr_base (x, x0, x4) -> h1 x x0 x4
529 | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
533 (** val trace_label_return_inv_rect_Type2 :
534 abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
535 trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
536 trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
537 let trace_label_return_inv_rect_Type2 x1 x2 x3 hterm h1 h2 =
540 | Tlr_base (x, x0, x4) -> h1 x x0 x4
541 | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
545 (** val trace_label_return_inv_rect_Type1 :
546 abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
547 trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
548 trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
549 let trace_label_return_inv_rect_Type1 x1 x2 x3 hterm h1 h2 =
552 | Tlr_base (x, x0, x4) -> h1 x x0 x4
553 | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
557 (** val trace_label_return_inv_rect_Type0 :
558 abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
559 trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
560 trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
561 let trace_label_return_inv_rect_Type0 x1 x2 x3 hterm h1 h2 =
564 | Tlr_base (x, x0, x4) -> h1 x x0 x4
565 | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
569 (** val trace_label_label_inv_rect_Type4 :
570 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
571 -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
572 -> __ -> __ -> 'a1) -> 'a1 **)
573 let trace_label_label_inv_rect_Type4 x1 x2 x3 x4 hterm h1 =
574 let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
577 (** val trace_label_label_inv_rect_Type3 :
578 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
579 -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
580 -> __ -> __ -> 'a1) -> 'a1 **)
581 let trace_label_label_inv_rect_Type3 x1 x2 x3 x4 hterm h1 =
582 let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
585 (** val trace_label_label_inv_rect_Type2 :
586 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
587 -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
588 -> __ -> __ -> 'a1) -> 'a1 **)
589 let trace_label_label_inv_rect_Type2 x1 x2 x3 x4 hterm h1 =
590 let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
593 (** val trace_label_label_inv_rect_Type1 :
594 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
595 -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
596 -> __ -> __ -> 'a1) -> 'a1 **)
597 let trace_label_label_inv_rect_Type1 x1 x2 x3 x4 hterm h1 =
598 let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
601 (** val trace_label_label_inv_rect_Type0 :
602 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
603 -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
604 -> __ -> __ -> 'a1) -> 'a1 **)
605 let trace_label_label_inv_rect_Type0 x1 x2 x3 x4 hterm h1 =
606 let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
609 (** val trace_any_label_inv_rect_Type4 :
610 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
611 (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
612 -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
613 __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
614 (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
615 -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
616 -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
617 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
618 -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
619 let trace_any_label_inv_rect_Type4 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
622 | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
623 | Tal_base_return (x, x0) -> h2 x x0 __ __
624 | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
625 | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
626 | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
627 h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
628 | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
632 (** val trace_any_label_inv_rect_Type3 :
633 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
634 (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
635 -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
636 __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
637 (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
638 -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
639 -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
640 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
641 -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
642 let trace_any_label_inv_rect_Type3 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
645 | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
646 | Tal_base_return (x, x0) -> h2 x x0 __ __
647 | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
648 | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
649 | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
650 h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
651 | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
655 (** val trace_any_label_inv_rect_Type2 :
656 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
657 (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
658 -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
659 __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
660 (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
661 -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
662 -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
663 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
664 -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
665 let trace_any_label_inv_rect_Type2 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
668 | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
669 | Tal_base_return (x, x0) -> h2 x x0 __ __
670 | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
671 | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
672 | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
673 h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
674 | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
678 (** val trace_any_label_inv_rect_Type1 :
679 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
680 (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
681 -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
682 __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
683 (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
684 -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
685 -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
686 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
687 -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
688 let trace_any_label_inv_rect_Type1 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
691 | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
692 | Tal_base_return (x, x0) -> h2 x x0 __ __
693 | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
694 | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
695 | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
696 h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
697 | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
701 (** val trace_any_label_inv_rect_Type0 :
702 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
703 (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
704 -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
705 __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
706 (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
707 -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
708 -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
709 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
710 -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
711 let trace_any_label_inv_rect_Type0 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
714 | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
715 | Tal_base_return (x, x0) -> h2 x x0 __ __
716 | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
717 | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
718 | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
719 h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
720 | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
724 (** val trace_label_return_discr :
725 abstract_status -> __ -> __ -> trace_label_return -> trace_label_return
727 let trace_label_return_discr a1 a2 a3 x y =
728 Logic.eq_rect_Type2 x
730 | Tlr_base (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
731 | Tlr_step (a0, a10, a20, a30, a4) ->
732 Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
734 (** val trace_label_label_discr :
735 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
736 -> trace_label_label -> __ **)
737 let trace_label_label_discr a1 a2 a3 a4 x y =
738 Logic.eq_rect_Type2 x
739 (let Tll_base (a0, a10, a20, a30) = x in
740 Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
742 (** val trace_label_return_jmdiscr :
743 abstract_status -> __ -> __ -> trace_label_return -> trace_label_return
745 let trace_label_return_jmdiscr a1 a2 a3 x y =
746 Logic.eq_rect_Type2 x
748 | Tlr_base (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
749 | Tlr_step (a0, a10, a20, a30, a4) ->
750 Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
752 (** val trace_label_label_jmdiscr :
753 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
754 -> trace_label_label -> __ **)
755 let trace_label_label_jmdiscr a1 a2 a3 a4 x y =
756 Logic.eq_rect_Type2 x
757 (let Tll_base (a0, a10, a20, a30) = x in
758 Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
760 (** val trace_any_label_jmdiscr :
761 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
762 trace_any_label -> __ **)
763 let trace_any_label_jmdiscr a1 a2 a3 a4 x y =
764 Logic.eq_rect_Type2 x
766 | Tal_base_not_return (a0, a10) ->
767 Obj.magic (fun _ dH -> dH __ __ __ __ __)
768 | Tal_base_return (a0, a10) -> Obj.magic (fun _ dH -> dH __ __ __ __)
769 | Tal_base_call (a0, a10, a20, a6) ->
770 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)
771 | Tal_base_tailcall (a0, a10, a20, a5) ->
772 Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
773 | Tal_step_call (a0, a10, a20, a30, a40, a8, a100) ->
774 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)
775 | Tal_step_default (a0, a10, a20, a30, a5) ->
776 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)) y
778 (** val tal_pc_list :
779 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
781 let rec tal_pc_list s fl st1 st2 = function
782 | Tal_base_not_return (pre, x) -> List.Cons ((s.as_pc_of pre), List.Nil)
783 | Tal_base_return (pre, x) -> List.Cons ((s.as_pc_of pre), List.Nil)
784 | Tal_base_call (pre, x, x0, x4) -> List.Cons ((s.as_pc_of pre), List.Nil)
785 | Tal_base_tailcall (pre, x, x0, x3) ->
786 List.Cons ((s.as_pc_of pre), List.Nil)
787 | Tal_step_call (fl', pre, x, st1', st2', x3, tl) ->
788 List.Cons ((s.as_pc_of pre), (tal_pc_list s fl' st1' st2' tl))
789 | Tal_step_default (fl', pre, st1', st2', tl) ->
790 List.Cons ((s.as_pc_of pre), (tal_pc_list s fl' st1' st2' tl))
792 (** val as_trace_any_label_length' :
793 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
795 let as_trace_any_label_length' s trace_ends_flag start_status final_status the_trace =
797 (tal_pc_list s trace_ends_flag start_status final_status the_trace)
799 (** val tll_hd_label :
800 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
801 -> CostLabel.costlabel **)
802 let tll_hd_label s fl st1 st2 tr =
803 (let Tll_base (x, st1', x0, x1) = tr in
804 (fun _ _ _ _ -> Types.pi1 (as_label_safe s st1'))) __ __ __ __
806 (** val tlr_hd_label :
807 abstract_status -> __ -> __ -> trace_label_return -> CostLabel.costlabel **)
808 let tlr_hd_label s st1 st2 = function
809 | Tlr_base (st1', st2', tll) -> tll_hd_label s Ends_with_ret st1' st2' tll
810 | Tlr_step (st1', st2', x, tll, x0) ->
811 tll_hd_label s Doesnt_end_with_ret st1' st2' tll
813 type trace_any_call =
815 | Tac_step_call of __ * __ * __ * __ * trace_label_return * trace_any_call
816 | Tac_step_default of __ * __ * __ * trace_any_call
818 (** val trace_any_call_rect_Type4 :
819 abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
820 -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
821 -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
822 __ -> trace_any_call -> 'a1 **)
823 let rec trace_any_call_rect_Type4 s h_tac_base h_tac_step_call h_tac_step_default x_22468 x_22467 = function
824 | Tac_base status -> h_tac_base status __
826 (status_pre_fun_call, status_after_fun_call, status_final,
827 status_start_fun_call, x_22473, x_22471) ->
828 h_tac_step_call status_pre_fun_call status_after_fun_call status_final
829 status_start_fun_call __ __ __ x_22473 __ x_22471
830 (trace_any_call_rect_Type4 s h_tac_base h_tac_step_call
831 h_tac_step_default status_after_fun_call status_final x_22471)
832 | Tac_step_default (status_pre, status_end, status_init, x_22478) ->
833 h_tac_step_default status_pre status_end status_init __ x_22478 __ __
834 (trace_any_call_rect_Type4 s h_tac_base h_tac_step_call
835 h_tac_step_default status_init status_end x_22478)
837 (** val trace_any_call_rect_Type3 :
838 abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
839 -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
840 -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
841 __ -> trace_any_call -> 'a1 **)
842 let rec trace_any_call_rect_Type3 s h_tac_base h_tac_step_call h_tac_step_default x_22500 x_22499 = function
843 | Tac_base status -> h_tac_base status __
845 (status_pre_fun_call, status_after_fun_call, status_final,
846 status_start_fun_call, x_22505, x_22503) ->
847 h_tac_step_call status_pre_fun_call status_after_fun_call status_final
848 status_start_fun_call __ __ __ x_22505 __ x_22503
849 (trace_any_call_rect_Type3 s h_tac_base h_tac_step_call
850 h_tac_step_default status_after_fun_call status_final x_22503)
851 | Tac_step_default (status_pre, status_end, status_init, x_22510) ->
852 h_tac_step_default status_pre status_end status_init __ x_22510 __ __
853 (trace_any_call_rect_Type3 s h_tac_base h_tac_step_call
854 h_tac_step_default status_init status_end x_22510)
856 (** val trace_any_call_rect_Type2 :
857 abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
858 -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
859 -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
860 __ -> trace_any_call -> 'a1 **)
861 let rec trace_any_call_rect_Type2 s h_tac_base h_tac_step_call h_tac_step_default x_22516 x_22515 = function
862 | Tac_base status -> h_tac_base status __
864 (status_pre_fun_call, status_after_fun_call, status_final,
865 status_start_fun_call, x_22521, x_22519) ->
866 h_tac_step_call status_pre_fun_call status_after_fun_call status_final
867 status_start_fun_call __ __ __ x_22521 __ x_22519
868 (trace_any_call_rect_Type2 s h_tac_base h_tac_step_call
869 h_tac_step_default status_after_fun_call status_final x_22519)
870 | Tac_step_default (status_pre, status_end, status_init, x_22526) ->
871 h_tac_step_default status_pre status_end status_init __ x_22526 __ __
872 (trace_any_call_rect_Type2 s h_tac_base h_tac_step_call
873 h_tac_step_default status_init status_end x_22526)
875 (** val trace_any_call_rect_Type1 :
876 abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
877 -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
878 -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
879 __ -> trace_any_call -> 'a1 **)
880 let rec trace_any_call_rect_Type1 s h_tac_base h_tac_step_call h_tac_step_default x_22532 x_22531 = function
881 | Tac_base status -> h_tac_base status __
883 (status_pre_fun_call, status_after_fun_call, status_final,
884 status_start_fun_call, x_22537, x_22535) ->
885 h_tac_step_call status_pre_fun_call status_after_fun_call status_final
886 status_start_fun_call __ __ __ x_22537 __ x_22535
887 (trace_any_call_rect_Type1 s h_tac_base h_tac_step_call
888 h_tac_step_default status_after_fun_call status_final x_22535)
889 | Tac_step_default (status_pre, status_end, status_init, x_22542) ->
890 h_tac_step_default status_pre status_end status_init __ x_22542 __ __
891 (trace_any_call_rect_Type1 s h_tac_base h_tac_step_call
892 h_tac_step_default status_init status_end x_22542)
894 (** val trace_any_call_rect_Type0 :
895 abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
896 -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
897 -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
898 __ -> trace_any_call -> 'a1 **)
899 let rec trace_any_call_rect_Type0 s h_tac_base h_tac_step_call h_tac_step_default x_22548 x_22547 = function
900 | Tac_base status -> h_tac_base status __
902 (status_pre_fun_call, status_after_fun_call, status_final,
903 status_start_fun_call, x_22553, x_22551) ->
904 h_tac_step_call status_pre_fun_call status_after_fun_call status_final
905 status_start_fun_call __ __ __ x_22553 __ x_22551
906 (trace_any_call_rect_Type0 s h_tac_base h_tac_step_call
907 h_tac_step_default status_after_fun_call status_final x_22551)
908 | Tac_step_default (status_pre, status_end, status_init, x_22558) ->
909 h_tac_step_default status_pre status_end status_init __ x_22558 __ __
910 (trace_any_call_rect_Type0 s h_tac_base h_tac_step_call
911 h_tac_step_default status_init status_end x_22558)
913 (** val trace_any_call_inv_rect_Type4 :
914 abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
915 __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
916 trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
917 __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
918 -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
919 let trace_any_call_inv_rect_Type4 x1 x2 x3 hterm h1 h2 h3 =
920 let hcut = trace_any_call_rect_Type4 x1 h1 h2 h3 x2 x3 hterm in
923 (** val trace_any_call_inv_rect_Type3 :
924 abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
925 __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
926 trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
927 __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
928 -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
929 let trace_any_call_inv_rect_Type3 x1 x2 x3 hterm h1 h2 h3 =
930 let hcut = trace_any_call_rect_Type3 x1 h1 h2 h3 x2 x3 hterm in
933 (** val trace_any_call_inv_rect_Type2 :
934 abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
935 __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
936 trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
937 __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
938 -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
939 let trace_any_call_inv_rect_Type2 x1 x2 x3 hterm h1 h2 h3 =
940 let hcut = trace_any_call_rect_Type2 x1 h1 h2 h3 x2 x3 hterm in
943 (** val trace_any_call_inv_rect_Type1 :
944 abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
945 __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
946 trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
947 __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
948 -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
949 let trace_any_call_inv_rect_Type1 x1 x2 x3 hterm h1 h2 h3 =
950 let hcut = trace_any_call_rect_Type1 x1 h1 h2 h3 x2 x3 hterm in
953 (** val trace_any_call_inv_rect_Type0 :
954 abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
955 __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
956 trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
957 __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
958 -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
959 let trace_any_call_inv_rect_Type0 x1 x2 x3 hterm h1 h2 h3 =
960 let hcut = trace_any_call_rect_Type0 x1 h1 h2 h3 x2 x3 hterm in
963 (** val trace_any_call_jmdiscr :
964 abstract_status -> __ -> __ -> trace_any_call -> trace_any_call -> __ **)
965 let trace_any_call_jmdiscr a1 a2 a3 x y =
966 Logic.eq_rect_Type2 x
968 | Tac_base a0 -> Obj.magic (fun _ dH -> dH __ __)
969 | Tac_step_call (a0, a10, a20, a30, a7, a9) ->
970 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)
971 | Tac_step_default (a0, a10, a20, a4) ->
972 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
974 type trace_label_call =
975 | Tlc_base of __ * __ * trace_any_call
977 (** val trace_label_call_rect_Type4 :
978 abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
979 -> trace_label_call -> 'a1 **)
980 let rec trace_label_call_rect_Type4 s h_tlc_base x_22666 x_22665 = function
981 | Tlc_base (start_status, end_status, x_22669) ->
982 h_tlc_base start_status end_status x_22669 __
984 (** val trace_label_call_rect_Type5 :
985 abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
986 -> trace_label_call -> 'a1 **)
987 let rec trace_label_call_rect_Type5 s h_tlc_base x_22672 x_22671 = function
988 | Tlc_base (start_status, end_status, x_22675) ->
989 h_tlc_base start_status end_status x_22675 __
991 (** val trace_label_call_rect_Type3 :
992 abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
993 -> trace_label_call -> 'a1 **)
994 let rec trace_label_call_rect_Type3 s h_tlc_base x_22678 x_22677 = function
995 | Tlc_base (start_status, end_status, x_22681) ->
996 h_tlc_base start_status end_status x_22681 __
998 (** val trace_label_call_rect_Type2 :
999 abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
1000 -> trace_label_call -> 'a1 **)
1001 let rec trace_label_call_rect_Type2 s h_tlc_base x_22684 x_22683 = function
1002 | Tlc_base (start_status, end_status, x_22687) ->
1003 h_tlc_base start_status end_status x_22687 __
1005 (** val trace_label_call_rect_Type1 :
1006 abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
1007 -> trace_label_call -> 'a1 **)
1008 let rec trace_label_call_rect_Type1 s h_tlc_base x_22690 x_22689 = function
1009 | Tlc_base (start_status, end_status, x_22693) ->
1010 h_tlc_base start_status end_status x_22693 __
1012 (** val trace_label_call_rect_Type0 :
1013 abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
1014 -> trace_label_call -> 'a1 **)
1015 let rec trace_label_call_rect_Type0 s h_tlc_base x_22696 x_22695 = function
1016 | Tlc_base (start_status, end_status, x_22699) ->
1017 h_tlc_base start_status end_status x_22699 __
1019 (** val trace_label_call_inv_rect_Type4 :
1020 abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1021 trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1022 let trace_label_call_inv_rect_Type4 x1 x2 x3 hterm h1 =
1023 let hcut = trace_label_call_rect_Type4 x1 h1 x2 x3 hterm in hcut __ __ __
1025 (** val trace_label_call_inv_rect_Type3 :
1026 abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1027 trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1028 let trace_label_call_inv_rect_Type3 x1 x2 x3 hterm h1 =
1029 let hcut = trace_label_call_rect_Type3 x1 h1 x2 x3 hterm in hcut __ __ __
1031 (** val trace_label_call_inv_rect_Type2 :
1032 abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1033 trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1034 let trace_label_call_inv_rect_Type2 x1 x2 x3 hterm h1 =
1035 let hcut = trace_label_call_rect_Type2 x1 h1 x2 x3 hterm in hcut __ __ __
1037 (** val trace_label_call_inv_rect_Type1 :
1038 abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1039 trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1040 let trace_label_call_inv_rect_Type1 x1 x2 x3 hterm h1 =
1041 let hcut = trace_label_call_rect_Type1 x1 h1 x2 x3 hterm in hcut __ __ __
1043 (** val trace_label_call_inv_rect_Type0 :
1044 abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1045 trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1046 let trace_label_call_inv_rect_Type0 x1 x2 x3 hterm h1 =
1047 let hcut = trace_label_call_rect_Type0 x1 h1 x2 x3 hterm in hcut __ __ __
1049 (** val trace_label_call_discr :
1050 abstract_status -> __ -> __ -> trace_label_call -> trace_label_call -> __ **)
1051 let trace_label_call_discr a1 a2 a3 x y =
1052 Logic.eq_rect_Type2 x
1053 (let Tlc_base (a0, a10, a20) = x in
1054 Obj.magic (fun _ dH -> dH __ __ __ __)) y
1056 (** val trace_label_call_jmdiscr :
1057 abstract_status -> __ -> __ -> trace_label_call -> trace_label_call -> __ **)
1058 let trace_label_call_jmdiscr a1 a2 a3 x y =
1059 Logic.eq_rect_Type2 x
1060 (let Tlc_base (a0, a10, a20) = x in
1061 Obj.magic (fun _ dH -> dH __ __ __ __)) y
1063 (** val tlc_hd_label :
1064 abstract_status -> __ -> __ -> trace_label_call -> CostLabel.costlabel **)
1065 let tlc_hd_label s st1 st2 tr =
1066 (let Tlc_base (st1', x, x0) = tr in
1067 (fun _ _ _ -> Types.pi1 (as_label_safe s st1'))) __ __ __
1069 type trace_label_diverges = __trace_label_diverges Lazy.t
1070 and __trace_label_diverges =
1071 | Tld_step of __ * __ * trace_label_label * trace_label_diverges
1072 | Tld_base of __ * __ * __ * trace_label_call * trace_label_diverges
1074 (** val trace_label_diverges_inv_rect_Type4 :
1075 abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1076 trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1077 __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1078 __ -> 'a1) -> 'a1 **)
1079 let trace_label_diverges_inv_rect_Type4 x1 x2 hterm h1 h2 =
1083 | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1084 | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1088 (** val trace_label_diverges_inv_rect_Type3 :
1089 abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1090 trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1091 __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1092 __ -> 'a1) -> 'a1 **)
1093 let trace_label_diverges_inv_rect_Type3 x1 x2 hterm h1 h2 =
1097 | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1098 | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1102 (** val trace_label_diverges_inv_rect_Type2 :
1103 abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1104 trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1105 __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1106 __ -> 'a1) -> 'a1 **)
1107 let trace_label_diverges_inv_rect_Type2 x1 x2 hterm h1 h2 =
1111 | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1112 | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1116 (** val trace_label_diverges_inv_rect_Type1 :
1117 abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1118 trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1119 __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1120 __ -> 'a1) -> 'a1 **)
1121 let trace_label_diverges_inv_rect_Type1 x1 x2 hterm h1 h2 =
1125 | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1126 | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1130 (** val trace_label_diverges_inv_rect_Type0 :
1131 abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1132 trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1133 __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1134 __ -> 'a1) -> 'a1 **)
1135 let trace_label_diverges_inv_rect_Type0 x1 x2 hterm h1 h2 =
1139 | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1140 | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1144 (** val trace_label_diverges_jmdiscr :
1145 abstract_status -> __ -> trace_label_diverges -> trace_label_diverges ->
1147 let trace_label_diverges_jmdiscr a1 a2 x y =
1148 Logic.eq_rect_Type2 x
1151 | Tld_step (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1152 | Tld_base (a0, a10, a20, a3, a6) ->
1153 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
1155 (** val tld_hd_label :
1156 abstract_status -> __ -> trace_label_diverges -> CostLabel.costlabel **)
1157 let tld_hd_label s st tr =
1160 | Tld_step (st', st'', tll, x) ->
1161 tll_hd_label s Doesnt_end_with_ret st' st'' tll
1162 | Tld_base (st', st'', x, tlc, x2) -> tlc_hd_label s st' st'' tlc
1164 type trace_whole_program =
1165 | Twp_terminating of __ * __ * __ * trace_label_return
1166 | Twp_diverges of __ * __ * trace_label_diverges
1168 (** val trace_whole_program_rect_Type4 :
1169 abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1170 __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1171 -> trace_whole_program -> 'a1 **)
1172 let rec trace_whole_program_rect_Type4 s h_twp_terminating h_twp_diverges x_22748 = function
1174 (status_initial, status_start_fun, status_final, x_22751) ->
1175 h_twp_terminating status_initial status_start_fun status_final __ __
1177 | Twp_diverges (status_initial, status_start_fun, x_22754) ->
1178 h_twp_diverges status_initial status_start_fun __ __ x_22754
1180 (** val trace_whole_program_rect_Type5 :
1181 abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1182 __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1183 -> trace_whole_program -> 'a1 **)
1184 let rec trace_whole_program_rect_Type5 s h_twp_terminating h_twp_diverges x_22759 = function
1186 (status_initial, status_start_fun, status_final, x_22762) ->
1187 h_twp_terminating status_initial status_start_fun status_final __ __
1189 | Twp_diverges (status_initial, status_start_fun, x_22765) ->
1190 h_twp_diverges status_initial status_start_fun __ __ x_22765
1192 (** val trace_whole_program_rect_Type3 :
1193 abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1194 __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1195 -> trace_whole_program -> 'a1 **)
1196 let rec trace_whole_program_rect_Type3 s h_twp_terminating h_twp_diverges x_22770 = function
1198 (status_initial, status_start_fun, status_final, x_22773) ->
1199 h_twp_terminating status_initial status_start_fun status_final __ __
1201 | Twp_diverges (status_initial, status_start_fun, x_22776) ->
1202 h_twp_diverges status_initial status_start_fun __ __ x_22776
1204 (** val trace_whole_program_rect_Type2 :
1205 abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1206 __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1207 -> trace_whole_program -> 'a1 **)
1208 let rec trace_whole_program_rect_Type2 s h_twp_terminating h_twp_diverges x_22781 = function
1210 (status_initial, status_start_fun, status_final, x_22784) ->
1211 h_twp_terminating status_initial status_start_fun status_final __ __
1213 | Twp_diverges (status_initial, status_start_fun, x_22787) ->
1214 h_twp_diverges status_initial status_start_fun __ __ x_22787
1216 (** val trace_whole_program_rect_Type1 :
1217 abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1218 __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1219 -> trace_whole_program -> 'a1 **)
1220 let rec trace_whole_program_rect_Type1 s h_twp_terminating h_twp_diverges x_22792 = function
1222 (status_initial, status_start_fun, status_final, x_22795) ->
1223 h_twp_terminating status_initial status_start_fun status_final __ __
1225 | Twp_diverges (status_initial, status_start_fun, x_22798) ->
1226 h_twp_diverges status_initial status_start_fun __ __ x_22798
1228 (** val trace_whole_program_rect_Type0 :
1229 abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1230 __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1231 -> trace_whole_program -> 'a1 **)
1232 let rec trace_whole_program_rect_Type0 s h_twp_terminating h_twp_diverges x_22803 = function
1234 (status_initial, status_start_fun, status_final, x_22806) ->
1235 h_twp_terminating status_initial status_start_fun status_final __ __
1237 | Twp_diverges (status_initial, status_start_fun, x_22809) ->
1238 h_twp_diverges status_initial status_start_fun __ __ x_22809
1240 (** val trace_whole_program_inv_rect_Type4 :
1241 abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ ->
1242 __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1243 __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **)
1244 let trace_whole_program_inv_rect_Type4 x1 x2 hterm h1 h2 =
1245 let hcut = trace_whole_program_rect_Type4 x1 h1 h2 x2 hterm in hcut __ __
1247 (** val trace_whole_program_inv_rect_Type3 :
1248 abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ ->
1249 __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1250 __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **)
1251 let trace_whole_program_inv_rect_Type3 x1 x2 hterm h1 h2 =
1252 let hcut = trace_whole_program_rect_Type3 x1 h1 h2 x2 hterm in hcut __ __
1254 (** val trace_whole_program_inv_rect_Type2 :
1255 abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ ->
1256 __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1257 __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **)
1258 let trace_whole_program_inv_rect_Type2 x1 x2 hterm h1 h2 =
1259 let hcut = trace_whole_program_rect_Type2 x1 h1 h2 x2 hterm in hcut __ __
1261 (** val trace_whole_program_inv_rect_Type1 :
1262 abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ ->
1263 __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1264 __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **)
1265 let trace_whole_program_inv_rect_Type1 x1 x2 hterm h1 h2 =
1266 let hcut = trace_whole_program_rect_Type1 x1 h1 h2 x2 hterm in hcut __ __
1268 (** val trace_whole_program_inv_rect_Type0 :
1269 abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ ->
1270 __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1271 __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **)
1272 let trace_whole_program_inv_rect_Type0 x1 x2 hterm h1 h2 =
1273 let hcut = trace_whole_program_rect_Type0 x1 h1 h2 x2 hterm in hcut __ __
1275 (** val trace_whole_program_jmdiscr :
1276 abstract_status -> __ -> trace_whole_program -> trace_whole_program -> __ **)
1277 let trace_whole_program_jmdiscr a1 a2 x y =
1278 Logic.eq_rect_Type2 x
1280 | Twp_terminating (a0, a10, a20, a5) ->
1281 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)
1282 | Twp_diverges (a0, a10, a4) ->
1283 Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
1285 (** val tal_tl_label :
1286 abstract_status -> __ -> __ -> trace_any_label -> CostLabel.costlabel **)
1287 let tal_tl_label s st1 st2 tr =
1288 Types.pi1 (as_label_safe s st2)
1290 (** val tll_tl_label :
1291 abstract_status -> __ -> __ -> trace_label_label -> CostLabel.costlabel **)
1292 let tll_tl_label s st1 st2 tr =
1293 Types.pi1 (as_label_safe s st2)
1295 type trace_any_any =
1297 | Taa_step of __ * __ * __ * trace_any_any
1299 (** val trace_any_any_rect_Type4 :
1300 abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1301 trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
1302 let rec trace_any_any_rect_Type4 s h_taa_base h_taa_step x_23033 x_23032 = function
1303 | Taa_base st -> h_taa_base st
1304 | Taa_step (st1, st2, st3, x_23035) ->
1305 h_taa_step st1 st2 st3 __ __ __ x_23035
1306 (trace_any_any_rect_Type4 s h_taa_base h_taa_step st2 st3 x_23035)
1308 (** val trace_any_any_rect_Type3 :
1309 abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1310 trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
1311 let rec trace_any_any_rect_Type3 s h_taa_base h_taa_step x_23051 x_23050 = function
1312 | Taa_base st -> h_taa_base st
1313 | Taa_step (st1, st2, st3, x_23053) ->
1314 h_taa_step st1 st2 st3 __ __ __ x_23053
1315 (trace_any_any_rect_Type3 s h_taa_base h_taa_step st2 st3 x_23053)
1317 (** val trace_any_any_rect_Type2 :
1318 abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1319 trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
1320 let rec trace_any_any_rect_Type2 s h_taa_base h_taa_step x_23060 x_23059 = function
1321 | Taa_base st -> h_taa_base st
1322 | Taa_step (st1, st2, st3, x_23062) ->
1323 h_taa_step st1 st2 st3 __ __ __ x_23062
1324 (trace_any_any_rect_Type2 s h_taa_base h_taa_step st2 st3 x_23062)
1326 (** val trace_any_any_rect_Type1 :
1327 abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1328 trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
1329 let rec trace_any_any_rect_Type1 s h_taa_base h_taa_step x_23069 x_23068 = function
1330 | Taa_base st -> h_taa_base st
1331 | Taa_step (st1, st2, st3, x_23071) ->
1332 h_taa_step st1 st2 st3 __ __ __ x_23071
1333 (trace_any_any_rect_Type1 s h_taa_base h_taa_step st2 st3 x_23071)
1335 (** val trace_any_any_rect_Type0 :
1336 abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1337 trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
1338 let rec trace_any_any_rect_Type0 s h_taa_base h_taa_step x_23078 x_23077 = function
1339 | Taa_base st -> h_taa_base st
1340 | Taa_step (st1, st2, st3, x_23080) ->
1341 h_taa_step st1 st2 st3 __ __ __ x_23080
1342 (trace_any_any_rect_Type0 s h_taa_base h_taa_step st2 st3 x_23080)
1344 (** val trace_any_any_inv_rect_Type4 :
1345 abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
1346 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __
1347 -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1348 let trace_any_any_inv_rect_Type4 x1 x2 x3 hterm h1 h2 =
1349 let hcut = trace_any_any_rect_Type4 x1 h1 h2 x2 x3 hterm in hcut __ __ __
1351 (** val trace_any_any_inv_rect_Type3 :
1352 abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
1353 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __
1354 -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1355 let trace_any_any_inv_rect_Type3 x1 x2 x3 hterm h1 h2 =
1356 let hcut = trace_any_any_rect_Type3 x1 h1 h2 x2 x3 hterm in hcut __ __ __
1358 (** val trace_any_any_inv_rect_Type2 :
1359 abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
1360 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __
1361 -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1362 let trace_any_any_inv_rect_Type2 x1 x2 x3 hterm h1 h2 =
1363 let hcut = trace_any_any_rect_Type2 x1 h1 h2 x2 x3 hterm in hcut __ __ __
1365 (** val trace_any_any_inv_rect_Type1 :
1366 abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
1367 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __
1368 -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1369 let trace_any_any_inv_rect_Type1 x1 x2 x3 hterm h1 h2 =
1370 let hcut = trace_any_any_rect_Type1 x1 h1 h2 x2 x3 hterm in hcut __ __ __
1372 (** val trace_any_any_inv_rect_Type0 :
1373 abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
1374 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __
1375 -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1376 let trace_any_any_inv_rect_Type0 x1 x2 x3 hterm h1 h2 =
1377 let hcut = trace_any_any_rect_Type0 x1 h1 h2 x2 x3 hterm in hcut __ __ __
1379 (** val trace_any_any_jmdiscr :
1380 abstract_status -> __ -> __ -> trace_any_any -> trace_any_any -> __ **)
1381 let trace_any_any_jmdiscr a1 a2 a3 x y =
1382 Logic.eq_rect_Type2 x
1384 | Taa_base a0 -> Obj.magic (fun _ dH -> dH __)
1385 | Taa_step (a0, a10, a20, a6) ->
1386 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
1388 (** val taa_non_empty :
1389 abstract_status -> __ -> __ -> trace_any_any -> Bool.bool **)
1390 let taa_non_empty s st1 st2 = function
1391 | Taa_base x -> Bool.False
1392 | Taa_step (x, x0, x1, x5) -> Bool.True
1394 (** val dpi1__o__taa_to_bool__o__inject :
1395 abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair ->
1396 Bool.bool Types.sig0 **)
1397 let dpi1__o__taa_to_bool__o__inject x1 x2 x3 x5 =
1398 taa_non_empty x1 x2 x3 x5.Types.dpi1
1400 (** val dpi1__o__taa_to_bool__o__bool_to_Prop__o__inject :
1401 abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair -> __
1403 let dpi1__o__taa_to_bool__o__bool_to_Prop__o__inject x1 x2 x3 x5 =
1404 Util.bool_to_Prop__o__inject (taa_non_empty x1 x2 x3 x5.Types.dpi1)
1406 (** val eject__o__taa_to_bool__o__inject :
1407 abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> Bool.bool
1409 let eject__o__taa_to_bool__o__inject x1 x2 x3 x5 =
1410 taa_non_empty x1 x2 x3 (Types.pi1 x5)
1412 (** val eject__o__taa_to_bool__o__bool_to_Prop__o__inject :
1413 abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> __ Types.sig0 **)
1414 let eject__o__taa_to_bool__o__bool_to_Prop__o__inject x1 x2 x3 x5 =
1415 Util.bool_to_Prop__o__inject (taa_non_empty x1 x2 x3 (Types.pi1 x5))
1417 (** val taa_to_bool__o__bool_to_Prop__o__inject :
1418 abstract_status -> __ -> __ -> trace_any_any -> __ Types.sig0 **)
1419 let taa_to_bool__o__bool_to_Prop__o__inject x1 x2 x3 x4 =
1420 Util.bool_to_Prop__o__inject (taa_non_empty x1 x2 x3 x4)
1422 (** val taa_to_bool__o__inject :
1423 abstract_status -> __ -> __ -> trace_any_any -> Bool.bool Types.sig0 **)
1424 let taa_to_bool__o__inject x1 x2 x3 x4 =
1425 taa_non_empty x1 x2 x3 x4
1427 (** val dpi1__o__taa_to_bool :
1428 abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair ->
1430 let dpi1__o__taa_to_bool x0 x1 x2 x4 =
1431 taa_non_empty x0 x1 x2 x4.Types.dpi1
1433 (** val eject__o__taa_to_bool :
1434 abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> Bool.bool **)
1435 let eject__o__taa_to_bool x0 x1 x2 x4 =
1436 taa_non_empty x0 x1 x2 (Types.pi1 x4)
1438 (** val taa_append_tal :
1439 abstract_status -> __ -> trace_ends_with_ret -> __ -> __ -> trace_any_any
1440 -> trace_any_label -> trace_any_label **)
1441 let rec taa_append_tal s st1 fl st2 st3 taa =
1443 | Taa_base st1' -> (fun fl0 st30 tal2 -> tal2)
1444 | Taa_step (st1', st2', st3', tl) ->
1445 (fun fl0 st30 tal2 -> Tal_step_default (fl0, st1', st2', st30,
1446 (taa_append_tal s st2' fl0 st3' st30 tl tal2)))) fl st3
1448 type intensional_event =
1449 | IEVcost of CostLabel.costlabel
1450 | IEVcall of AST.ident
1451 | IEVtailcall of AST.ident * AST.ident
1452 | IEVret of AST.ident
1454 (** val intensional_event_rect_Type4 :
1455 (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1456 AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1457 let rec intensional_event_rect_Type4 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
1458 | IEVcost x_23151 -> h_IEVcost x_23151
1459 | IEVcall x_23152 -> h_IEVcall x_23152
1460 | IEVtailcall (x_23154, x_23153) -> h_IEVtailcall x_23154 x_23153
1461 | IEVret x_23155 -> h_IEVret x_23155
1463 (** val intensional_event_rect_Type5 :
1464 (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1465 AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1466 let rec intensional_event_rect_Type5 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
1467 | IEVcost x_23161 -> h_IEVcost x_23161
1468 | IEVcall x_23162 -> h_IEVcall x_23162
1469 | IEVtailcall (x_23164, x_23163) -> h_IEVtailcall x_23164 x_23163
1470 | IEVret x_23165 -> h_IEVret x_23165
1472 (** val intensional_event_rect_Type3 :
1473 (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1474 AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1475 let rec intensional_event_rect_Type3 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
1476 | IEVcost x_23171 -> h_IEVcost x_23171
1477 | IEVcall x_23172 -> h_IEVcall x_23172
1478 | IEVtailcall (x_23174, x_23173) -> h_IEVtailcall x_23174 x_23173
1479 | IEVret x_23175 -> h_IEVret x_23175
1481 (** val intensional_event_rect_Type2 :
1482 (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1483 AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1484 let rec intensional_event_rect_Type2 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
1485 | IEVcost x_23181 -> h_IEVcost x_23181
1486 | IEVcall x_23182 -> h_IEVcall x_23182
1487 | IEVtailcall (x_23184, x_23183) -> h_IEVtailcall x_23184 x_23183
1488 | IEVret x_23185 -> h_IEVret x_23185
1490 (** val intensional_event_rect_Type1 :
1491 (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1492 AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1493 let rec intensional_event_rect_Type1 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
1494 | IEVcost x_23191 -> h_IEVcost x_23191
1495 | IEVcall x_23192 -> h_IEVcall x_23192
1496 | IEVtailcall (x_23194, x_23193) -> h_IEVtailcall x_23194 x_23193
1497 | IEVret x_23195 -> h_IEVret x_23195
1499 (** val intensional_event_rect_Type0 :
1500 (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1501 AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1502 let rec intensional_event_rect_Type0 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
1503 | IEVcost x_23201 -> h_IEVcost x_23201
1504 | IEVcall x_23202 -> h_IEVcall x_23202
1505 | IEVtailcall (x_23204, x_23203) -> h_IEVtailcall x_23204 x_23203
1506 | IEVret x_23205 -> h_IEVret x_23205
1508 (** val intensional_event_inv_rect_Type4 :
1509 intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident ->
1510 __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __
1512 let intensional_event_inv_rect_Type4 hterm h1 h2 h3 h4 =
1513 let hcut = intensional_event_rect_Type4 h1 h2 h3 h4 hterm in hcut __
1515 (** val intensional_event_inv_rect_Type3 :
1516 intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident ->
1517 __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __
1519 let intensional_event_inv_rect_Type3 hterm h1 h2 h3 h4 =
1520 let hcut = intensional_event_rect_Type3 h1 h2 h3 h4 hterm in hcut __
1522 (** val intensional_event_inv_rect_Type2 :
1523 intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident ->
1524 __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __
1526 let intensional_event_inv_rect_Type2 hterm h1 h2 h3 h4 =
1527 let hcut = intensional_event_rect_Type2 h1 h2 h3 h4 hterm in hcut __
1529 (** val intensional_event_inv_rect_Type1 :
1530 intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident ->
1531 __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __
1533 let intensional_event_inv_rect_Type1 hterm h1 h2 h3 h4 =
1534 let hcut = intensional_event_rect_Type1 h1 h2 h3 h4 hterm in hcut __
1536 (** val intensional_event_inv_rect_Type0 :
1537 intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident ->
1538 __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __
1540 let intensional_event_inv_rect_Type0 hterm h1 h2 h3 h4 =
1541 let hcut = intensional_event_rect_Type0 h1 h2 h3 h4 hterm in hcut __
1543 (** val intensional_event_discr :
1544 intensional_event -> intensional_event -> __ **)
1545 let intensional_event_discr x y =
1546 Logic.eq_rect_Type2 x
1548 | IEVcost a0 -> Obj.magic (fun _ dH -> dH __)
1549 | IEVcall a0 -> Obj.magic (fun _ dH -> dH __)
1550 | IEVtailcall (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1551 | IEVret a0 -> Obj.magic (fun _ dH -> dH __)) y
1553 (** val intensional_event_jmdiscr :
1554 intensional_event -> intensional_event -> __ **)
1555 let intensional_event_jmdiscr x y =
1556 Logic.eq_rect_Type2 x
1558 | IEVcost a0 -> Obj.magic (fun _ dH -> dH __)
1559 | IEVcall a0 -> Obj.magic (fun _ dH -> dH __)
1560 | IEVtailcall (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1561 | IEVret a0 -> Obj.magic (fun _ dH -> dH __)) y
1563 type as_trace = intensional_event List.list Types.sig0
1566 'a1 Types.sig0 -> 'a1 List.list Types.sig0 -> 'a1 List.list Types.sig0 **)
1568 List.Cons ((Types.pi1 x), (Types.pi1 l))
1570 (** val append_safe :
1571 'a1 List.list Types.sig0 -> 'a1 List.list Types.sig0 -> 'a1 List.list
1573 let append_safe l1 l2 =
1574 List.append (Types.pi1 l1) (Types.pi1 l2)
1576 (** val nil_safe : 'a1 List.list Types.sig0 **)
1580 (** val emittable_cost :
1581 abstract_status -> as_cost_label -> intensional_event Types.sig0 **)
1582 let emittable_cost s l =
1583 IEVcost (Types.pi1 l)
1585 (** val observables_trace_label_label :
1586 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
1587 -> AST.ident -> as_trace **)
1588 let rec observables_trace_label_label s trace_ends_flag start_status final_status the_trace curr =
1589 let Tll_base (ends_flag, initial, final, given_trace) = the_trace in
1590 let label = as_label_safe s initial in
1591 cons_safe (emittable_cost s label)
1592 (observables_trace_any_label s ends_flag initial final given_trace curr)
1593 (** val observables_trace_any_label :
1594 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
1595 AST.ident -> as_trace **)
1596 and observables_trace_any_label s trace_ends_flag start_status final_status the_trace curr =
1597 match the_trace with
1598 | Tal_base_not_return (the_status, x) -> nil_safe
1599 | Tal_base_return (the_status, x) -> cons_safe (IEVret curr) nil_safe
1600 | Tal_base_call (pre_fun_call, start_fun_call, final, call_trace) ->
1601 let id = s.as_call_ident pre_fun_call in
1602 cons_safe (IEVcall id)
1603 (observables_trace_label_return s start_fun_call final call_trace id)
1604 | Tal_base_tailcall (pre_fun_call, start_fun_call, final, call_trace) ->
1605 let id = s.as_tailcall_ident pre_fun_call in
1606 cons_safe (IEVtailcall (curr, id))
1607 (observables_trace_label_return s start_fun_call final call_trace id)
1609 (end_flag, pre_fun_call, start_fun_call, after_fun_call, final,
1610 call_trace, final_trace) ->
1611 let id = s.as_call_ident pre_fun_call in
1612 let call_cost_trace =
1613 observables_trace_label_return s start_fun_call after_fun_call
1616 let final_cost_trace =
1617 observables_trace_any_label s end_flag after_fun_call final final_trace
1620 append_safe (cons_safe (IEVcall id) call_cost_trace) final_cost_trace
1622 (end_flag, status_pre, status_init, status_end, tail_trace) ->
1623 observables_trace_any_label s end_flag status_init status_end tail_trace
1625 (** val observables_trace_label_return :
1626 abstract_status -> __ -> __ -> trace_label_return -> AST.ident ->
1628 and observables_trace_label_return s start_status final_status the_trace curr =
1629 match the_trace with
1630 | Tlr_base (before, after, trace_to_lift) ->
1631 observables_trace_label_label s Ends_with_ret before after trace_to_lift
1633 | Tlr_step (initial, labelled, final, labelled_trace, ret_trace) ->
1635 observables_trace_label_label s Doesnt_end_with_ret initial labelled
1639 observables_trace_label_return s labelled final ret_trace curr
1641 append_safe labelled_cost return_cost
1643 (** val filter_map :
1644 ('a1 -> 'a2 Types.option) -> 'a1 List.list -> 'a2 List.list **)
1645 let rec filter_map f = function
1646 | List.Nil -> List.Nil
1647 | List.Cons (hd, tl) ->
1650 | Types.None -> List.Nil
1651 | Types.Some y -> List.Cons (y, List.Nil)) (filter_map f tl)
1653 (** val list_distribute_sig_aux :
1654 'a1 List.list -> 'a1 Types.sig0 List.list **)
1655 let rec list_distribute_sig_aux l =
1657 | List.Nil -> (fun _ -> List.Nil)
1658 | List.Cons (hd, tl) ->
1659 (fun _ -> List.Cons (hd, (list_distribute_sig_aux tl)))) __
1661 (** val list_distribute_sig :
1662 'a1 List.list Types.sig0 -> 'a1 Types.sig0 List.list **)
1663 let list_distribute_sig l =
1664 list_distribute_sig_aux (Types.pi1 l)
1666 (** val list_factor_sig :
1667 'a1 Types.sig0 List.list -> 'a1 List.list Types.sig0 **)
1668 let rec list_factor_sig = function
1669 | List.Nil -> nil_safe
1670 | List.Cons (hd, tl) -> cons_safe hd (list_factor_sig tl)
1672 (** val costlabels_of_observables :
1673 abstract_status -> as_trace -> as_cost_label List.list **)
1674 let costlabels_of_observables s l =
1675 filter_map (fun ev ->
1676 (match Types.pi1 ev with
1677 | IEVcost c -> (fun _ -> Types.Some c)
1678 | IEVcall x -> (fun _ -> Types.None)
1679 | IEVtailcall (x, x0) -> (fun _ -> Types.None)
1680 | IEVret x -> (fun _ -> Types.None)) __) (list_distribute_sig l)
1682 (** val flatten_trace_label_return :
1683 abstract_status -> __ -> __ -> trace_label_return -> as_cost_label
1685 let flatten_trace_label_return s st1 st2 tlr =
1686 let dummy = Positive.One in
1687 costlabels_of_observables s
1688 (observables_trace_label_return s st1 st2 tlr dummy)
1690 (** val flatten_trace_label_label :
1691 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
1692 -> as_cost_label List.list **)
1693 let flatten_trace_label_label s flag st1 st2 tll =
1694 let dummy = Positive.One in
1695 costlabels_of_observables s
1696 (observables_trace_label_label s flag st1 st2 tll dummy)
1698 (** val flatten_trace_any_label :
1699 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
1700 as_cost_label List.list **)
1701 let flatten_trace_any_label s flag st1 st2 tll =
1702 let dummy = Positive.One in
1703 costlabels_of_observables s
1704 (observables_trace_any_label s flag st1 st2 tll dummy)
1706 type trace_any_any_free =
1708 | Taaf_step of __ * __ * __ * trace_any_any
1709 | Taaf_step_jump of __ * __ * __ * trace_any_any
1711 (** val trace_any_any_free_rect_Type4 :
1712 abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1713 -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1714 'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1715 let rec trace_any_any_free_rect_Type4 s h_taaf_base h_taaf_step h_taaf_step_jump x_23284 x_23283 = function
1716 | Taaf_base s0 -> h_taaf_base s0
1717 | Taaf_step (s1, s2, s3, x_23288) -> h_taaf_step s1 s2 s3 x_23288 __ __
1718 | Taaf_step_jump (s1, s2, s3, x_23292) ->
1719 h_taaf_step_jump s1 s2 s3 x_23292 __ __ __
1721 (** val trace_any_any_free_rect_Type5 :
1722 abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1723 -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1724 'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1725 let rec trace_any_any_free_rect_Type5 s h_taaf_base h_taaf_step h_taaf_step_jump x_23297 x_23296 = function
1726 | Taaf_base s0 -> h_taaf_base s0
1727 | Taaf_step (s1, s2, s3, x_23301) -> h_taaf_step s1 s2 s3 x_23301 __ __
1728 | Taaf_step_jump (s1, s2, s3, x_23305) ->
1729 h_taaf_step_jump s1 s2 s3 x_23305 __ __ __
1731 (** val trace_any_any_free_rect_Type3 :
1732 abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1733 -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1734 'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1735 let rec trace_any_any_free_rect_Type3 s h_taaf_base h_taaf_step h_taaf_step_jump x_23310 x_23309 = function
1736 | Taaf_base s0 -> h_taaf_base s0
1737 | Taaf_step (s1, s2, s3, x_23314) -> h_taaf_step s1 s2 s3 x_23314 __ __
1738 | Taaf_step_jump (s1, s2, s3, x_23318) ->
1739 h_taaf_step_jump s1 s2 s3 x_23318 __ __ __
1741 (** val trace_any_any_free_rect_Type2 :
1742 abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1743 -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1744 'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1745 let rec trace_any_any_free_rect_Type2 s h_taaf_base h_taaf_step h_taaf_step_jump x_23323 x_23322 = function
1746 | Taaf_base s0 -> h_taaf_base s0
1747 | Taaf_step (s1, s2, s3, x_23327) -> h_taaf_step s1 s2 s3 x_23327 __ __
1748 | Taaf_step_jump (s1, s2, s3, x_23331) ->
1749 h_taaf_step_jump s1 s2 s3 x_23331 __ __ __
1751 (** val trace_any_any_free_rect_Type1 :
1752 abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1753 -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1754 'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1755 let rec trace_any_any_free_rect_Type1 s h_taaf_base h_taaf_step h_taaf_step_jump x_23336 x_23335 = function
1756 | Taaf_base s0 -> h_taaf_base s0
1757 | Taaf_step (s1, s2, s3, x_23340) -> h_taaf_step s1 s2 s3 x_23340 __ __
1758 | Taaf_step_jump (s1, s2, s3, x_23344) ->
1759 h_taaf_step_jump s1 s2 s3 x_23344 __ __ __
1761 (** val trace_any_any_free_rect_Type0 :
1762 abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1763 -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1764 'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1765 let rec trace_any_any_free_rect_Type0 s h_taaf_base h_taaf_step h_taaf_step_jump x_23349 x_23348 = function
1766 | Taaf_base s0 -> h_taaf_base s0
1767 | Taaf_step (s1, s2, s3, x_23353) -> h_taaf_step s1 s2 s3 x_23353 __ __
1768 | Taaf_step_jump (s1, s2, s3, x_23357) ->
1769 h_taaf_step_jump s1 s2 s3 x_23357 __ __ __
1771 (** val trace_any_any_free_inv_rect_Type4 :
1772 abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
1773 __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1774 __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1775 __ -> __ -> 'a1) -> 'a1 **)
1776 let trace_any_any_free_inv_rect_Type4 x1 x2 x3 hterm h1 h2 h3 =
1777 let hcut = trace_any_any_free_rect_Type4 x1 h1 h2 h3 x2 x3 hterm in
1780 (** val trace_any_any_free_inv_rect_Type3 :
1781 abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
1782 __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1783 __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1784 __ -> __ -> 'a1) -> 'a1 **)
1785 let trace_any_any_free_inv_rect_Type3 x1 x2 x3 hterm h1 h2 h3 =
1786 let hcut = trace_any_any_free_rect_Type3 x1 h1 h2 h3 x2 x3 hterm in
1789 (** val trace_any_any_free_inv_rect_Type2 :
1790 abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
1791 __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1792 __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1793 __ -> __ -> 'a1) -> 'a1 **)
1794 let trace_any_any_free_inv_rect_Type2 x1 x2 x3 hterm h1 h2 h3 =
1795 let hcut = trace_any_any_free_rect_Type2 x1 h1 h2 h3 x2 x3 hterm in
1798 (** val trace_any_any_free_inv_rect_Type1 :
1799 abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
1800 __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1801 __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1802 __ -> __ -> 'a1) -> 'a1 **)
1803 let trace_any_any_free_inv_rect_Type1 x1 x2 x3 hterm h1 h2 h3 =
1804 let hcut = trace_any_any_free_rect_Type1 x1 h1 h2 h3 x2 x3 hterm in
1807 (** val trace_any_any_free_inv_rect_Type0 :
1808 abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
1809 __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1810 __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1811 __ -> __ -> 'a1) -> 'a1 **)
1812 let trace_any_any_free_inv_rect_Type0 x1 x2 x3 hterm h1 h2 h3 =
1813 let hcut = trace_any_any_free_rect_Type0 x1 h1 h2 h3 x2 x3 hterm in
1816 (** val trace_any_any_free_jmdiscr :
1817 abstract_status -> __ -> __ -> trace_any_any_free -> trace_any_any_free
1819 let trace_any_any_free_jmdiscr a1 a2 a3 x y =
1820 Logic.eq_rect_Type2 x
1822 | Taaf_base a0 -> Obj.magic (fun _ dH -> dH __)
1823 | Taaf_step (a0, a10, a20, a30) ->
1824 Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
1825 | Taaf_step_jump (a0, a10, a20, a30) ->
1826 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
1828 (** val taaf_non_empty :
1829 abstract_status -> __ -> __ -> trace_any_any_free -> Bool.bool **)
1830 let taaf_non_empty s s1 s2 = function
1831 | Taaf_base x -> Bool.False
1832 | Taaf_step (x, x0, x1, x2) -> Bool.True
1833 | Taaf_step_jump (x, x0, x1, x2) -> Bool.True
1835 (** val taa_append_taa :
1836 abstract_status -> __ -> __ -> __ -> trace_any_any -> trace_any_any ->
1838 let rec taa_append_taa s st1 st2 st3 taa =
1840 | Taa_base st1' -> (fun st30 taa2 -> taa2)
1841 | Taa_step (st1', st2', st3', tl) ->
1842 (fun st30 taa2 -> Taa_step (st1', st2', st30,
1843 (taa_append_taa s st2' st3' st30 tl taa2)))) st3
1845 (** val taaf_to_taa :
1846 abstract_status -> __ -> __ -> trace_any_any_free -> trace_any_any **)
1847 let taaf_to_taa s s1 s2 taaf =
1849 | Taaf_base s0 -> (fun _ -> Taa_base s0)
1850 | Taaf_step (s10, s20, s3, taa) ->
1852 taa_append_taa s s10 s20 s3 taa (Taa_step (s20, s3, s3, (Taa_base
1854 | Taaf_step_jump (s10, s20, s3, taa) ->
1855 (fun _ -> assert false (* absurd case *))) __
1857 (** val taaf_append_tal :
1858 abstract_status -> __ -> trace_ends_with_ret -> __ -> __ ->
1859 trace_any_any_free -> trace_any_label -> trace_any_label **)
1860 let taaf_append_tal s st1 fl st2 st3 taaf =
1861 taa_append_tal s st1 fl st2 st3 (taaf_to_taa s st1 st2 taaf)
1863 (** val taaf_append_taa :
1864 abstract_status -> __ -> __ -> __ -> trace_any_any_free -> trace_any_any
1865 -> trace_any_any **)
1866 let taaf_append_taa s st1 st2 st3 taaf =
1867 taa_append_taa s st1 st2 st3 (taaf_to_taa s st1 st2 taaf)
1870 abstract_status -> __ -> __ -> __ -> trace_any_any_free ->
1871 trace_any_any_free **)
1872 let taaf_cons s s1 s2 s3 tl =
1874 | Taaf_base s20 -> (fun _ _ -> Taaf_step (s1, s1, s20, (Taa_base s1)))
1875 | Taaf_step (s20, s30, s4, taa) ->
1876 (fun _ _ -> Taaf_step (s1, s30, s4, (Taa_step (s1, s20, s30, taa))))
1877 | Taaf_step_jump (s20, s30, s4, taa) ->
1878 (fun _ _ -> Taaf_step_jump (s1, s30, s4, (Taa_step (s1, s20, s30,
1881 (** val taaf_append_taaf :
1882 abstract_status -> __ -> __ -> __ -> trace_any_any_free ->
1883 trace_any_any_free -> trace_any_any_free **)
1884 let taaf_append_taaf s st1 st2 st3 taaf1 taaf2 =
1886 | Taaf_base s1 -> (fun taaf10 _ -> taaf10)
1887 | Taaf_step (s1, s2, s3, taa) ->
1888 (fun taaf10 _ -> Taaf_step (st1, s2, s3,
1889 (taaf_append_taa s st1 s1 s2 taaf10 taa)))
1890 | Taaf_step_jump (s2, s3, s4, taa) ->
1891 (fun taaf10 _ -> Taaf_step_jump (st1, s3, s4,
1892 (taaf_append_taa s st1 s2 s3 taaf10 taa)))) taaf1 __