source: extracted/structuredTraces.ml @ 2649

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

...

File size: 61.3 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Relations
14
15open Bool
16
17open Jmeq
18
19open Proper
20
21open PositiveMap
22
23open Deqsets
24
25open ErrorMessages
26
27open PreIdentifiers
28
29open Errors
30
31open Extralib
32
33open Setoids
34
35open Monad
36
37open Option
38
39open Lists
40
41open Positive
42
43open Identifiers
44
45open Arithmetic
46
47open Vector
48
49open Div_and_mod
50
51open Russell
52
53open List
54
55open Util
56
57open FoldStuff
58
59open BitVector
60
61open Extranat
62
63open Nat
64
65open Integers
66
67open AST
68
69open CostLabel
70
71open Sets
72
73open Listb
74
75type status_class =
76| Cl_return
77| Cl_jump
78| Cl_call
79| Cl_tailcall
80| Cl_other
81
82(** val status_class_rect_Type4 :
83    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
84let rec status_class_rect_Type4 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
85| Cl_return -> h_cl_return
86| Cl_jump -> h_cl_jump
87| Cl_call -> h_cl_call
88| Cl_tailcall -> h_cl_tailcall
89| Cl_other -> h_cl_other
90
91(** val status_class_rect_Type5 :
92    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
93let rec status_class_rect_Type5 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
94| Cl_return -> h_cl_return
95| Cl_jump -> h_cl_jump
96| Cl_call -> h_cl_call
97| Cl_tailcall -> h_cl_tailcall
98| Cl_other -> h_cl_other
99
100(** val status_class_rect_Type3 :
101    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
102let rec status_class_rect_Type3 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
103| Cl_return -> h_cl_return
104| Cl_jump -> h_cl_jump
105| Cl_call -> h_cl_call
106| Cl_tailcall -> h_cl_tailcall
107| Cl_other -> h_cl_other
108
109(** val status_class_rect_Type2 :
110    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
111let rec status_class_rect_Type2 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
112| Cl_return -> h_cl_return
113| Cl_jump -> h_cl_jump
114| Cl_call -> h_cl_call
115| Cl_tailcall -> h_cl_tailcall
116| Cl_other -> h_cl_other
117
118(** val status_class_rect_Type1 :
119    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
120let rec status_class_rect_Type1 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
121| Cl_return -> h_cl_return
122| Cl_jump -> h_cl_jump
123| Cl_call -> h_cl_call
124| Cl_tailcall -> h_cl_tailcall
125| Cl_other -> h_cl_other
126
127(** val status_class_rect_Type0 :
128    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
129let rec status_class_rect_Type0 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
130| Cl_return -> h_cl_return
131| Cl_jump -> h_cl_jump
132| Cl_call -> h_cl_call
133| Cl_tailcall -> h_cl_tailcall
134| Cl_other -> h_cl_other
135
136(** val status_class_inv_rect_Type4 :
137    status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
138    -> (__ -> 'a1) -> 'a1 **)
139let status_class_inv_rect_Type4 hterm h1 h2 h3 h4 h5 =
140  let hcut = status_class_rect_Type4 h1 h2 h3 h4 h5 hterm in hcut __
141
142(** val status_class_inv_rect_Type3 :
143    status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
144    -> (__ -> 'a1) -> 'a1 **)
145let status_class_inv_rect_Type3 hterm h1 h2 h3 h4 h5 =
146  let hcut = status_class_rect_Type3 h1 h2 h3 h4 h5 hterm in hcut __
147
148(** val status_class_inv_rect_Type2 :
149    status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
150    -> (__ -> 'a1) -> 'a1 **)
151let status_class_inv_rect_Type2 hterm h1 h2 h3 h4 h5 =
152  let hcut = status_class_rect_Type2 h1 h2 h3 h4 h5 hterm in hcut __
153
154(** val status_class_inv_rect_Type1 :
155    status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
156    -> (__ -> 'a1) -> 'a1 **)
157let status_class_inv_rect_Type1 hterm h1 h2 h3 h4 h5 =
158  let hcut = status_class_rect_Type1 h1 h2 h3 h4 h5 hterm in hcut __
159
160(** val status_class_inv_rect_Type0 :
161    status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
162    -> (__ -> 'a1) -> 'a1 **)
163let status_class_inv_rect_Type0 hterm h1 h2 h3 h4 h5 =
164  let hcut = status_class_rect_Type0 h1 h2 h3 h4 h5 hterm in hcut __
165
166(** val status_class_discr : status_class -> status_class -> __ **)
167let status_class_discr x y =
168  Logic.eq_rect_Type2 x
169    (match x with
170     | Cl_return -> Obj.magic (fun _ dH -> dH)
171     | Cl_jump -> Obj.magic (fun _ dH -> dH)
172     | Cl_call -> Obj.magic (fun _ dH -> dH)
173     | Cl_tailcall -> Obj.magic (fun _ dH -> dH)
174     | Cl_other -> Obj.magic (fun _ dH -> dH)) y
175
176(** val status_class_jmdiscr : status_class -> status_class -> __ **)
177let status_class_jmdiscr x y =
178  Logic.eq_rect_Type2 x
179    (match x with
180     | Cl_return -> Obj.magic (fun _ dH -> dH)
181     | Cl_jump -> Obj.magic (fun _ dH -> dH)
182     | Cl_call -> Obj.magic (fun _ dH -> dH)
183     | Cl_tailcall -> Obj.magic (fun _ dH -> dH)
184     | Cl_other -> Obj.magic (fun _ dH -> dH)) y
185
186type abstract_status = { as_pc : Deqsets.deqSet; as_pc_of : (__ -> __);
187                         as_classify : (__ -> status_class Types.option);
188                         as_label_of_pc : (__ -> CostLabel.costlabel
189                                          Types.option);
190                         as_call_ident : (__ Types.sig0 -> AST.ident);
191                         as_tailcall_ident : (__ Types.sig0 -> AST.ident) }
192
193(** val abstract_status_rect_Type4 :
194    (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class
195    Types.option) -> (__ -> CostLabel.costlabel Types.option) -> __ -> __ ->
196    (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
197    abstract_status -> 'a1 **)
198let rec abstract_status_rect_Type4 h_mk_abstract_status x_2837 =
199  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
200    as_label_of_pc = as_label_of_pc0; as_call_ident = as_call_ident0;
201    as_tailcall_ident = as_tailcall_ident0 } = x_2837
202  in
203  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
204    __ as_call_ident0 as_tailcall_ident0
205
206(** val abstract_status_rect_Type5 :
207    (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class
208    Types.option) -> (__ -> CostLabel.costlabel Types.option) -> __ -> __ ->
209    (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
210    abstract_status -> 'a1 **)
211let rec abstract_status_rect_Type5 h_mk_abstract_status x_2839 =
212  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
213    as_label_of_pc = as_label_of_pc0; as_call_ident = as_call_ident0;
214    as_tailcall_ident = as_tailcall_ident0 } = x_2839
215  in
216  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
217    __ as_call_ident0 as_tailcall_ident0
218
219(** val abstract_status_rect_Type3 :
220    (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class
221    Types.option) -> (__ -> CostLabel.costlabel Types.option) -> __ -> __ ->
222    (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
223    abstract_status -> 'a1 **)
224let rec abstract_status_rect_Type3 h_mk_abstract_status x_2841 =
225  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
226    as_label_of_pc = as_label_of_pc0; as_call_ident = as_call_ident0;
227    as_tailcall_ident = as_tailcall_ident0 } = x_2841
228  in
229  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
230    __ as_call_ident0 as_tailcall_ident0
231
232(** val abstract_status_rect_Type2 :
233    (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class
234    Types.option) -> (__ -> CostLabel.costlabel Types.option) -> __ -> __ ->
235    (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
236    abstract_status -> 'a1 **)
237let rec abstract_status_rect_Type2 h_mk_abstract_status x_2843 =
238  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
239    as_label_of_pc = as_label_of_pc0; as_call_ident = as_call_ident0;
240    as_tailcall_ident = as_tailcall_ident0 } = x_2843
241  in
242  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
243    __ as_call_ident0 as_tailcall_ident0
244
245(** val abstract_status_rect_Type1 :
246    (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class
247    Types.option) -> (__ -> CostLabel.costlabel Types.option) -> __ -> __ ->
248    (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
249    abstract_status -> 'a1 **)
250let rec abstract_status_rect_Type1 h_mk_abstract_status x_2845 =
251  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
252    as_label_of_pc = as_label_of_pc0; as_call_ident = as_call_ident0;
253    as_tailcall_ident = as_tailcall_ident0 } = x_2845
254  in
255  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
256    __ as_call_ident0 as_tailcall_ident0
257
258(** val abstract_status_rect_Type0 :
259    (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class
260    Types.option) -> (__ -> CostLabel.costlabel Types.option) -> __ -> __ ->
261    (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
262    abstract_status -> 'a1 **)
263let rec abstract_status_rect_Type0 h_mk_abstract_status x_2847 =
264  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
265    as_label_of_pc = as_label_of_pc0; as_call_ident = as_call_ident0;
266    as_tailcall_ident = as_tailcall_ident0 } = x_2847
267  in
268  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
269    __ as_call_ident0 as_tailcall_ident0
270
271type as_status = __
272
273type as_execute = __
274
275(** val as_pc : abstract_status -> Deqsets.deqSet **)
276let rec as_pc xxx =
277  xxx.as_pc
278
279(** val as_pc_of : abstract_status -> __ -> __ **)
280let rec as_pc_of xxx =
281  xxx.as_pc_of
282
283(** val as_classify : abstract_status -> __ -> status_class Types.option **)
284let rec as_classify xxx =
285  xxx.as_classify
286
287(** val as_label_of_pc :
288    abstract_status -> __ -> CostLabel.costlabel Types.option **)
289let rec as_label_of_pc xxx =
290  xxx.as_label_of_pc
291
292type as_after_return = __
293
294type as_final = __
295
296(** val as_call_ident : abstract_status -> __ Types.sig0 -> AST.ident **)
297let rec as_call_ident xxx =
298  xxx.as_call_ident
299
300(** val as_tailcall_ident : abstract_status -> __ Types.sig0 -> AST.ident **)
301let rec as_tailcall_ident xxx =
302  xxx.as_tailcall_ident
303
304(** val abstract_status_inv_rect_Type4 :
305    abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
306    status_class Types.option) -> (__ -> CostLabel.costlabel Types.option) ->
307    __ -> __ -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident)
308    -> __ -> 'a1) -> 'a1 **)
309let abstract_status_inv_rect_Type4 hterm h1 =
310  let hcut = abstract_status_rect_Type4 h1 hterm in hcut __
311
312(** val abstract_status_inv_rect_Type3 :
313    abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
314    status_class Types.option) -> (__ -> CostLabel.costlabel Types.option) ->
315    __ -> __ -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident)
316    -> __ -> 'a1) -> 'a1 **)
317let abstract_status_inv_rect_Type3 hterm h1 =
318  let hcut = abstract_status_rect_Type3 h1 hterm in hcut __
319
320(** val abstract_status_inv_rect_Type2 :
321    abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
322    status_class Types.option) -> (__ -> CostLabel.costlabel Types.option) ->
323    __ -> __ -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident)
324    -> __ -> 'a1) -> 'a1 **)
325let abstract_status_inv_rect_Type2 hterm h1 =
326  let hcut = abstract_status_rect_Type2 h1 hterm in hcut __
327
328(** val abstract_status_inv_rect_Type1 :
329    abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
330    status_class Types.option) -> (__ -> CostLabel.costlabel Types.option) ->
331    __ -> __ -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident)
332    -> __ -> 'a1) -> 'a1 **)
333let abstract_status_inv_rect_Type1 hterm h1 =
334  let hcut = abstract_status_rect_Type1 h1 hterm in hcut __
335
336(** val abstract_status_inv_rect_Type0 :
337    abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
338    status_class Types.option) -> (__ -> CostLabel.costlabel Types.option) ->
339    __ -> __ -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident)
340    -> __ -> 'a1) -> 'a1 **)
341let abstract_status_inv_rect_Type0 hterm h1 =
342  let hcut = abstract_status_rect_Type0 h1 hterm in hcut __
343
344(** val abstract_status_jmdiscr :
345    abstract_status -> abstract_status -> __ **)
346let abstract_status_jmdiscr x y =
347  Logic.eq_rect_Type2 x
348    (let { as_pc = a2; as_pc_of = a3; as_classify = a4; as_label_of_pc = a5;
349       as_call_ident = a8; as_tailcall_ident = a9 } = x
350     in
351    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)) y
352
353(** val as_label :
354    abstract_status -> __ -> CostLabel.costlabel Types.option **)
355let as_label s s0 =
356  s.as_label_of_pc (s.as_pc_of s0)
357
358(** val as_label_safe :
359    abstract_status -> __ Types.sig0 -> CostLabel.costlabel **)
360let as_label_safe a_s st_sig =
361  Option.opt_safe (as_label a_s (Types.pi1 st_sig))
362
363(** val as_costed_exc : abstract_status -> __ -> (__, __) Types.sum **)
364let as_costed_exc s s0 =
365  match as_label s s0 with
366  | Types.None -> Types.Inr __
367  | Types.Some c -> Types.Inl __
368
369type as_cost_label = CostLabel.costlabel Types.sig0
370
371type as_cost_labels = as_cost_label List.list
372
373(** val as_cost_get_label :
374    abstract_status -> as_cost_label -> CostLabel.costlabel **)
375let as_cost_get_label s l_sig =
376  Types.pi1 l_sig
377
378(** val as_cost_get_labels :
379    abstract_status -> as_cost_label PositiveMap.positive_map ->
380    CostLabel.costlabel PositiveMap.positive_map **)
381let as_cost_get_labels s =
382  PositiveMap.map0 (as_cost_get_label s)
383
384type as_cost_map = as_cost_label -> Nat.nat
385
386(** val lift_sigma_map_id :
387    'a2 -> ('a1 -> (__, __) Types.sum) -> ('a1 Types.sig0 -> 'a2) -> 'a1
388    Types.sig0 -> 'a2 **)
389let lift_sigma_map_id dflt dec m a_sig =
390  match dec (Types.pi1 a_sig) with
391  | Types.Inl _ -> m (Types.pi1 a_sig)
392  | Types.Inr _ -> dflt
393
394(** val lift_cost_map_id :
395    abstract_status -> abstract_status -> (CostLabel.costlabel -> (__, __)
396    Types.sum) -> as_cost_map -> as_cost_map **)
397let lift_cost_map_id s_in s_out =
398  lift_sigma_map_id Nat.O
399
400type trace_ends_with_ret =
401| Ends_with_ret
402| Doesnt_end_with_ret
403
404(** val trace_ends_with_ret_rect_Type4 :
405    'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
406let rec trace_ends_with_ret_rect_Type4 h_ends_with_ret h_doesnt_end_with_ret = function
407| Ends_with_ret -> h_ends_with_ret
408| Doesnt_end_with_ret -> h_doesnt_end_with_ret
409
410(** val trace_ends_with_ret_rect_Type5 :
411    'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
412let rec trace_ends_with_ret_rect_Type5 h_ends_with_ret h_doesnt_end_with_ret = function
413| Ends_with_ret -> h_ends_with_ret
414| Doesnt_end_with_ret -> h_doesnt_end_with_ret
415
416(** val trace_ends_with_ret_rect_Type3 :
417    'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
418let rec trace_ends_with_ret_rect_Type3 h_ends_with_ret h_doesnt_end_with_ret = function
419| Ends_with_ret -> h_ends_with_ret
420| Doesnt_end_with_ret -> h_doesnt_end_with_ret
421
422(** val trace_ends_with_ret_rect_Type2 :
423    'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
424let rec trace_ends_with_ret_rect_Type2 h_ends_with_ret h_doesnt_end_with_ret = function
425| Ends_with_ret -> h_ends_with_ret
426| Doesnt_end_with_ret -> h_doesnt_end_with_ret
427
428(** val trace_ends_with_ret_rect_Type1 :
429    'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
430let rec trace_ends_with_ret_rect_Type1 h_ends_with_ret h_doesnt_end_with_ret = function
431| Ends_with_ret -> h_ends_with_ret
432| Doesnt_end_with_ret -> h_doesnt_end_with_ret
433
434(** val trace_ends_with_ret_rect_Type0 :
435    'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
436let rec trace_ends_with_ret_rect_Type0 h_ends_with_ret h_doesnt_end_with_ret = function
437| Ends_with_ret -> h_ends_with_ret
438| Doesnt_end_with_ret -> h_doesnt_end_with_ret
439
440(** val trace_ends_with_ret_inv_rect_Type4 :
441    trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
442let trace_ends_with_ret_inv_rect_Type4 hterm h1 h2 =
443  let hcut = trace_ends_with_ret_rect_Type4 h1 h2 hterm in hcut __
444
445(** val trace_ends_with_ret_inv_rect_Type3 :
446    trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
447let trace_ends_with_ret_inv_rect_Type3 hterm h1 h2 =
448  let hcut = trace_ends_with_ret_rect_Type3 h1 h2 hterm in hcut __
449
450(** val trace_ends_with_ret_inv_rect_Type2 :
451    trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
452let trace_ends_with_ret_inv_rect_Type2 hterm h1 h2 =
453  let hcut = trace_ends_with_ret_rect_Type2 h1 h2 hterm in hcut __
454
455(** val trace_ends_with_ret_inv_rect_Type1 :
456    trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
457let trace_ends_with_ret_inv_rect_Type1 hterm h1 h2 =
458  let hcut = trace_ends_with_ret_rect_Type1 h1 h2 hterm in hcut __
459
460(** val trace_ends_with_ret_inv_rect_Type0 :
461    trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
462let trace_ends_with_ret_inv_rect_Type0 hterm h1 h2 =
463  let hcut = trace_ends_with_ret_rect_Type0 h1 h2 hterm in hcut __
464
465(** val trace_ends_with_ret_discr :
466    trace_ends_with_ret -> trace_ends_with_ret -> __ **)
467let trace_ends_with_ret_discr x y =
468  Logic.eq_rect_Type2 x
469    (match x with
470     | Ends_with_ret -> Obj.magic (fun _ dH -> dH)
471     | Doesnt_end_with_ret -> Obj.magic (fun _ dH -> dH)) y
472
473(** val trace_ends_with_ret_jmdiscr :
474    trace_ends_with_ret -> trace_ends_with_ret -> __ **)
475let trace_ends_with_ret_jmdiscr x y =
476  Logic.eq_rect_Type2 x
477    (match x with
478     | Ends_with_ret -> Obj.magic (fun _ dH -> dH)
479     | Doesnt_end_with_ret -> Obj.magic (fun _ dH -> dH)) y
480
481type trace_label_return =
482| Tlr_base of __ * __ * trace_label_label
483| Tlr_step of __ * __ * __ * trace_label_label * trace_label_return
484and trace_label_label =
485| Tll_base of trace_ends_with_ret * __ * __ * trace_any_label
486and trace_any_label =
487| Tal_base_not_return of __ * __
488| Tal_base_return of __ * __
489| Tal_base_call of __ * __ * __ * trace_label_return
490| Tal_base_tailcall of __ * __ * __ * trace_label_return
491| Tal_step_call of trace_ends_with_ret * __ * __ * __ * __
492   * trace_label_return * trace_any_label
493| Tal_step_default of trace_ends_with_ret * __ * __ * __ * trace_any_label
494
495(** val trace_label_return_inv_rect_Type4 :
496    abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
497    trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
498    trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
499let trace_label_return_inv_rect_Type4 x1 x2 x3 hterm h1 h2 =
500  let hcut =
501    match hterm with
502    | Tlr_base (x, x0, x4) -> h1 x x0 x4
503    | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
504  in
505  hcut __ __ __
506
507(** val trace_label_return_inv_rect_Type3 :
508    abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
509    trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
510    trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
511let trace_label_return_inv_rect_Type3 x1 x2 x3 hterm h1 h2 =
512  let hcut =
513    match hterm with
514    | Tlr_base (x, x0, x4) -> h1 x x0 x4
515    | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
516  in
517  hcut __ __ __
518
519(** val trace_label_return_inv_rect_Type2 :
520    abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
521    trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
522    trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
523let trace_label_return_inv_rect_Type2 x1 x2 x3 hterm h1 h2 =
524  let hcut =
525    match hterm with
526    | Tlr_base (x, x0, x4) -> h1 x x0 x4
527    | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
528  in
529  hcut __ __ __
530
531(** val trace_label_return_inv_rect_Type1 :
532    abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
533    trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
534    trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
535let trace_label_return_inv_rect_Type1 x1 x2 x3 hterm h1 h2 =
536  let hcut =
537    match hterm with
538    | Tlr_base (x, x0, x4) -> h1 x x0 x4
539    | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
540  in
541  hcut __ __ __
542
543(** val trace_label_return_inv_rect_Type0 :
544    abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
545    trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
546    trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
547let trace_label_return_inv_rect_Type0 x1 x2 x3 hterm h1 h2 =
548  let hcut =
549    match hterm with
550    | Tlr_base (x, x0, x4) -> h1 x x0 x4
551    | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
552  in
553  hcut __ __ __
554
555(** val trace_label_label_inv_rect_Type4 :
556    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
557    -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
558    -> __ -> __ -> 'a1) -> 'a1 **)
559let trace_label_label_inv_rect_Type4 x1 x2 x3 x4 hterm h1 =
560  let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
561  hcut __ __ __ __
562
563(** val trace_label_label_inv_rect_Type3 :
564    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
565    -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
566    -> __ -> __ -> 'a1) -> 'a1 **)
567let trace_label_label_inv_rect_Type3 x1 x2 x3 x4 hterm h1 =
568  let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
569  hcut __ __ __ __
570
571(** val trace_label_label_inv_rect_Type2 :
572    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
573    -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
574    -> __ -> __ -> 'a1) -> 'a1 **)
575let trace_label_label_inv_rect_Type2 x1 x2 x3 x4 hterm h1 =
576  let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
577  hcut __ __ __ __
578
579(** val trace_label_label_inv_rect_Type1 :
580    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
581    -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
582    -> __ -> __ -> 'a1) -> 'a1 **)
583let trace_label_label_inv_rect_Type1 x1 x2 x3 x4 hterm h1 =
584  let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
585  hcut __ __ __ __
586
587(** val trace_label_label_inv_rect_Type0 :
588    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
589    -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
590    -> __ -> __ -> 'a1) -> 'a1 **)
591let trace_label_label_inv_rect_Type0 x1 x2 x3 x4 hterm h1 =
592  let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
593  hcut __ __ __ __
594
595(** val trace_any_label_inv_rect_Type4 :
596    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
597    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
598    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
599    __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
600    (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
601    -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
602    -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
603    'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
604    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
605let trace_any_label_inv_rect_Type4 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
606  let hcut =
607    match hterm with
608    | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
609    | Tal_base_return (x, x0) -> h2 x x0 __ __
610    | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
611    | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
612    | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
613      h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
614    | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
615  in
616  hcut __ __ __ __
617
618(** val trace_any_label_inv_rect_Type3 :
619    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
620    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
621    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
622    __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
623    (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
624    -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
625    -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
626    'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
627    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
628let trace_any_label_inv_rect_Type3 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
629  let hcut =
630    match hterm with
631    | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
632    | Tal_base_return (x, x0) -> h2 x x0 __ __
633    | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
634    | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
635    | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
636      h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
637    | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
638  in
639  hcut __ __ __ __
640
641(** val trace_any_label_inv_rect_Type2 :
642    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
643    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
644    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
645    __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
646    (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
647    -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
648    -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
649    'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
650    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
651let trace_any_label_inv_rect_Type2 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
652  let hcut =
653    match hterm with
654    | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
655    | Tal_base_return (x, x0) -> h2 x x0 __ __
656    | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
657    | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
658    | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
659      h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
660    | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
661  in
662  hcut __ __ __ __
663
664(** val trace_any_label_inv_rect_Type1 :
665    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
666    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
667    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
668    __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
669    (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
670    -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
671    -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
672    'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
673    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
674let trace_any_label_inv_rect_Type1 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
675  let hcut =
676    match hterm with
677    | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
678    | Tal_base_return (x, x0) -> h2 x x0 __ __
679    | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
680    | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
681    | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
682      h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
683    | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
684  in
685  hcut __ __ __ __
686
687(** val trace_any_label_inv_rect_Type0 :
688    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
689    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
690    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
691    __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
692    (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
693    -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
694    -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
695    'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
696    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
697let trace_any_label_inv_rect_Type0 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
698  let hcut =
699    match hterm with
700    | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
701    | Tal_base_return (x, x0) -> h2 x x0 __ __
702    | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
703    | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
704    | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
705      h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
706    | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
707  in
708  hcut __ __ __ __
709
710(** val trace_label_return_discr :
711    abstract_status -> __ -> __ -> trace_label_return -> trace_label_return
712    -> __ **)
713let trace_label_return_discr a1 a2 a3 x y =
714  Logic.eq_rect_Type2 x
715    (match x with
716     | Tlr_base (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
717     | Tlr_step (a0, a10, a20, a30, a4) ->
718       Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
719
720(** val trace_label_label_discr :
721    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
722    -> trace_label_label -> __ **)
723let trace_label_label_discr a1 a2 a3 a4 x y =
724  Logic.eq_rect_Type2 x
725    (let Tll_base (a0, a10, a20, a30) = x in
726    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
727
728(** val trace_label_return_jmdiscr :
729    abstract_status -> __ -> __ -> trace_label_return -> trace_label_return
730    -> __ **)
731let trace_label_return_jmdiscr a1 a2 a3 x y =
732  Logic.eq_rect_Type2 x
733    (match x with
734     | Tlr_base (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
735     | Tlr_step (a0, a10, a20, a30, a4) ->
736       Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
737
738(** val trace_label_label_jmdiscr :
739    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
740    -> trace_label_label -> __ **)
741let trace_label_label_jmdiscr a1 a2 a3 a4 x y =
742  Logic.eq_rect_Type2 x
743    (let Tll_base (a0, a10, a20, a30) = x in
744    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
745
746(** val trace_any_label_jmdiscr :
747    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
748    trace_any_label -> __ **)
749let trace_any_label_jmdiscr a1 a2 a3 a4 x y =
750  Logic.eq_rect_Type2 x
751    (match x with
752     | Tal_base_not_return (a0, a10) ->
753       Obj.magic (fun _ dH -> dH __ __ __ __ __)
754     | Tal_base_return (a0, a10) -> Obj.magic (fun _ dH -> dH __ __ __ __)
755     | Tal_base_call (a0, a10, a20, a6) ->
756       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)
757     | Tal_base_tailcall (a0, a10, a20, a5) ->
758       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
759     | Tal_step_call (a0, a10, a20, a30, a40, a8, a100) ->
760       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)
761     | Tal_step_default (a0, a10, a20, a30, a5) ->
762       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)) y
763
764(** val tal_pc_list :
765    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
766    __ List.list **)
767let rec tal_pc_list s fl st1 st2 = function
768| Tal_base_not_return (pre, x) -> List.Cons ((s.as_pc_of pre), List.Nil)
769| Tal_base_return (pre, x) -> List.Cons ((s.as_pc_of pre), List.Nil)
770| Tal_base_call (pre, x, x0, x4) -> List.Cons ((s.as_pc_of pre), List.Nil)
771| Tal_base_tailcall (pre, x, x0, x3) ->
772  List.Cons ((s.as_pc_of pre), List.Nil)
773| Tal_step_call (fl', pre, x, st1', st2', x3, tl) ->
774  List.Cons ((s.as_pc_of pre), (tal_pc_list s fl' st1' st2' tl))
775| Tal_step_default (fl', pre, st1', st2', tl) ->
776  List.Cons ((s.as_pc_of pre), (tal_pc_list s fl' st1' st2' tl))
777
778(** val as_trace_any_label_length' :
779    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
780    Nat.nat **)
781let as_trace_any_label_length' s trace_ends_flag start_status final_status the_trace =
782  List.length
783    (tal_pc_list s trace_ends_flag start_status final_status the_trace)
784
785type tal_unrepeating = __
786
787type tll_unrepeating = __
788
789type tlr_unrepeating = __
790
791(** val tll_hd_label :
792    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
793    -> CostLabel.costlabel **)
794let tll_hd_label s fl st1 st2 = function
795| Tll_base (x, st1', x0, x1) -> as_label_safe s st1'
796
797(** val tlr_hd_label :
798    abstract_status -> __ -> __ -> trace_label_return -> CostLabel.costlabel **)
799let tlr_hd_label s st1 st2 = function
800| Tlr_base (st1', st2', tll) -> tll_hd_label s Ends_with_ret st1' st2' tll
801| Tlr_step (st1', st2', x, tll, x0) ->
802  tll_hd_label s Doesnt_end_with_ret st1' st2' tll
803
804type trace_any_call =
805| Tac_base of __
806| Tac_step_call of __ * __ * __ * __ * trace_label_return * trace_any_call
807| Tac_step_default of __ * __ * __ * trace_any_call
808
809(** val trace_any_call_rect_Type4 :
810    abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
811    -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
812    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
813    __ -> trace_any_call -> 'a1 **)
814let rec trace_any_call_rect_Type4 s h_tac_base h_tac_step_call h_tac_step_default x_2927 x_2926 = function
815| Tac_base status -> h_tac_base status __
816| Tac_step_call
817    (status_pre_fun_call, status_after_fun_call, status_final,
818     status_start_fun_call, x_2932, x_2930) ->
819  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
820    status_start_fun_call __ __ __ x_2932 __ x_2930
821    (trace_any_call_rect_Type4 s h_tac_base h_tac_step_call
822      h_tac_step_default status_after_fun_call status_final x_2930)
823| Tac_step_default (status_pre, status_end, status_init, x_2937) ->
824  h_tac_step_default status_pre status_end status_init __ x_2937 __ __
825    (trace_any_call_rect_Type4 s h_tac_base h_tac_step_call
826      h_tac_step_default status_init status_end x_2937)
827
828(** val trace_any_call_rect_Type3 :
829    abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
830    -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
831    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
832    __ -> trace_any_call -> 'a1 **)
833let rec trace_any_call_rect_Type3 s h_tac_base h_tac_step_call h_tac_step_default x_2959 x_2958 = function
834| Tac_base status -> h_tac_base status __
835| Tac_step_call
836    (status_pre_fun_call, status_after_fun_call, status_final,
837     status_start_fun_call, x_2964, x_2962) ->
838  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
839    status_start_fun_call __ __ __ x_2964 __ x_2962
840    (trace_any_call_rect_Type3 s h_tac_base h_tac_step_call
841      h_tac_step_default status_after_fun_call status_final x_2962)
842| Tac_step_default (status_pre, status_end, status_init, x_2969) ->
843  h_tac_step_default status_pre status_end status_init __ x_2969 __ __
844    (trace_any_call_rect_Type3 s h_tac_base h_tac_step_call
845      h_tac_step_default status_init status_end x_2969)
846
847(** val trace_any_call_rect_Type2 :
848    abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
849    -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
850    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
851    __ -> trace_any_call -> 'a1 **)
852let rec trace_any_call_rect_Type2 s h_tac_base h_tac_step_call h_tac_step_default x_2975 x_2974 = function
853| Tac_base status -> h_tac_base status __
854| Tac_step_call
855    (status_pre_fun_call, status_after_fun_call, status_final,
856     status_start_fun_call, x_2980, x_2978) ->
857  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
858    status_start_fun_call __ __ __ x_2980 __ x_2978
859    (trace_any_call_rect_Type2 s h_tac_base h_tac_step_call
860      h_tac_step_default status_after_fun_call status_final x_2978)
861| Tac_step_default (status_pre, status_end, status_init, x_2985) ->
862  h_tac_step_default status_pre status_end status_init __ x_2985 __ __
863    (trace_any_call_rect_Type2 s h_tac_base h_tac_step_call
864      h_tac_step_default status_init status_end x_2985)
865
866(** val trace_any_call_rect_Type1 :
867    abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
868    -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
869    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
870    __ -> trace_any_call -> 'a1 **)
871let rec trace_any_call_rect_Type1 s h_tac_base h_tac_step_call h_tac_step_default x_2991 x_2990 = function
872| Tac_base status -> h_tac_base status __
873| Tac_step_call
874    (status_pre_fun_call, status_after_fun_call, status_final,
875     status_start_fun_call, x_2996, x_2994) ->
876  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
877    status_start_fun_call __ __ __ x_2996 __ x_2994
878    (trace_any_call_rect_Type1 s h_tac_base h_tac_step_call
879      h_tac_step_default status_after_fun_call status_final x_2994)
880| Tac_step_default (status_pre, status_end, status_init, x_3001) ->
881  h_tac_step_default status_pre status_end status_init __ x_3001 __ __
882    (trace_any_call_rect_Type1 s h_tac_base h_tac_step_call
883      h_tac_step_default status_init status_end x_3001)
884
885(** val trace_any_call_rect_Type0 :
886    abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
887    -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
888    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
889    __ -> trace_any_call -> 'a1 **)
890let rec trace_any_call_rect_Type0 s h_tac_base h_tac_step_call h_tac_step_default x_3007 x_3006 = function
891| Tac_base status -> h_tac_base status __
892| Tac_step_call
893    (status_pre_fun_call, status_after_fun_call, status_final,
894     status_start_fun_call, x_3012, x_3010) ->
895  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
896    status_start_fun_call __ __ __ x_3012 __ x_3010
897    (trace_any_call_rect_Type0 s h_tac_base h_tac_step_call
898      h_tac_step_default status_after_fun_call status_final x_3010)
899| Tac_step_default (status_pre, status_end, status_init, x_3017) ->
900  h_tac_step_default status_pre status_end status_init __ x_3017 __ __
901    (trace_any_call_rect_Type0 s h_tac_base h_tac_step_call
902      h_tac_step_default status_init status_end x_3017)
903
904(** val trace_any_call_inv_rect_Type4 :
905    abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
906    __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
907    trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
908    __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
909    -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
910let trace_any_call_inv_rect_Type4 x1 x2 x3 hterm h1 h2 h3 =
911  let hcut = trace_any_call_rect_Type4 x1 h1 h2 h3 x2 x3 hterm in
912  hcut __ __ __
913
914(** val trace_any_call_inv_rect_Type3 :
915    abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
916    __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
917    trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
918    __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
919    -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
920let trace_any_call_inv_rect_Type3 x1 x2 x3 hterm h1 h2 h3 =
921  let hcut = trace_any_call_rect_Type3 x1 h1 h2 h3 x2 x3 hterm in
922  hcut __ __ __
923
924(** val trace_any_call_inv_rect_Type2 :
925    abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
926    __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
927    trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
928    __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
929    -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
930let trace_any_call_inv_rect_Type2 x1 x2 x3 hterm h1 h2 h3 =
931  let hcut = trace_any_call_rect_Type2 x1 h1 h2 h3 x2 x3 hterm in
932  hcut __ __ __
933
934(** val trace_any_call_inv_rect_Type1 :
935    abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
936    __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
937    trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
938    __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
939    -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
940let trace_any_call_inv_rect_Type1 x1 x2 x3 hterm h1 h2 h3 =
941  let hcut = trace_any_call_rect_Type1 x1 h1 h2 h3 x2 x3 hterm in
942  hcut __ __ __
943
944(** val trace_any_call_inv_rect_Type0 :
945    abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
946    __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
947    trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
948    __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
949    -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
950let trace_any_call_inv_rect_Type0 x1 x2 x3 hterm h1 h2 h3 =
951  let hcut = trace_any_call_rect_Type0 x1 h1 h2 h3 x2 x3 hterm in
952  hcut __ __ __
953
954(** val trace_any_call_jmdiscr :
955    abstract_status -> __ -> __ -> trace_any_call -> trace_any_call -> __ **)
956let trace_any_call_jmdiscr a1 a2 a3 x y =
957  Logic.eq_rect_Type2 x
958    (match x with
959     | Tac_base a0 -> Obj.magic (fun _ dH -> dH __ __)
960     | Tac_step_call (a0, a10, a20, a30, a7, a9) ->
961       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)
962     | Tac_step_default (a0, a10, a20, a4) ->
963       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
964
965type trace_label_call =
966| Tlc_base of __ * __ * trace_any_call
967
968(** val trace_label_call_rect_Type4 :
969    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
970    -> trace_label_call -> 'a1 **)
971let rec trace_label_call_rect_Type4 s h_tlc_base x_3125 x_3124 = function
972| Tlc_base (start_status, end_status, x_3128) ->
973  h_tlc_base start_status end_status x_3128 __
974
975(** val trace_label_call_rect_Type5 :
976    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
977    -> trace_label_call -> 'a1 **)
978let rec trace_label_call_rect_Type5 s h_tlc_base x_3131 x_3130 = function
979| Tlc_base (start_status, end_status, x_3134) ->
980  h_tlc_base start_status end_status x_3134 __
981
982(** val trace_label_call_rect_Type3 :
983    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
984    -> trace_label_call -> 'a1 **)
985let rec trace_label_call_rect_Type3 s h_tlc_base x_3137 x_3136 = function
986| Tlc_base (start_status, end_status, x_3140) ->
987  h_tlc_base start_status end_status x_3140 __
988
989(** val trace_label_call_rect_Type2 :
990    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
991    -> trace_label_call -> 'a1 **)
992let rec trace_label_call_rect_Type2 s h_tlc_base x_3143 x_3142 = function
993| Tlc_base (start_status, end_status, x_3146) ->
994  h_tlc_base start_status end_status x_3146 __
995
996(** val trace_label_call_rect_Type1 :
997    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
998    -> trace_label_call -> 'a1 **)
999let rec trace_label_call_rect_Type1 s h_tlc_base x_3149 x_3148 = function
1000| Tlc_base (start_status, end_status, x_3152) ->
1001  h_tlc_base start_status end_status x_3152 __
1002
1003(** val trace_label_call_rect_Type0 :
1004    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
1005    -> trace_label_call -> 'a1 **)
1006let rec trace_label_call_rect_Type0 s h_tlc_base x_3155 x_3154 = function
1007| Tlc_base (start_status, end_status, x_3158) ->
1008  h_tlc_base start_status end_status x_3158 __
1009
1010(** val trace_label_call_inv_rect_Type4 :
1011    abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1012    trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1013let trace_label_call_inv_rect_Type4 x1 x2 x3 hterm h1 =
1014  let hcut = trace_label_call_rect_Type4 x1 h1 x2 x3 hterm in hcut __ __ __
1015
1016(** val trace_label_call_inv_rect_Type3 :
1017    abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1018    trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1019let trace_label_call_inv_rect_Type3 x1 x2 x3 hterm h1 =
1020  let hcut = trace_label_call_rect_Type3 x1 h1 x2 x3 hterm in hcut __ __ __
1021
1022(** val trace_label_call_inv_rect_Type2 :
1023    abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1024    trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1025let trace_label_call_inv_rect_Type2 x1 x2 x3 hterm h1 =
1026  let hcut = trace_label_call_rect_Type2 x1 h1 x2 x3 hterm in hcut __ __ __
1027
1028(** val trace_label_call_inv_rect_Type1 :
1029    abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1030    trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1031let trace_label_call_inv_rect_Type1 x1 x2 x3 hterm h1 =
1032  let hcut = trace_label_call_rect_Type1 x1 h1 x2 x3 hterm in hcut __ __ __
1033
1034(** val trace_label_call_inv_rect_Type0 :
1035    abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1036    trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1037let trace_label_call_inv_rect_Type0 x1 x2 x3 hterm h1 =
1038  let hcut = trace_label_call_rect_Type0 x1 h1 x2 x3 hterm in hcut __ __ __
1039
1040(** val trace_label_call_discr :
1041    abstract_status -> __ -> __ -> trace_label_call -> trace_label_call -> __ **)
1042let trace_label_call_discr a1 a2 a3 x y =
1043  Logic.eq_rect_Type2 x
1044    (let Tlc_base (a0, a10, a20) = x in
1045    Obj.magic (fun _ dH -> dH __ __ __ __)) y
1046
1047(** val trace_label_call_jmdiscr :
1048    abstract_status -> __ -> __ -> trace_label_call -> trace_label_call -> __ **)
1049let trace_label_call_jmdiscr a1 a2 a3 x y =
1050  Logic.eq_rect_Type2 x
1051    (let Tlc_base (a0, a10, a20) = x in
1052    Obj.magic (fun _ dH -> dH __ __ __ __)) y
1053
1054(** val tlc_hd_label :
1055    abstract_status -> __ -> __ -> trace_label_call -> CostLabel.costlabel **)
1056let tlc_hd_label s st1 st2 = function
1057| Tlc_base (st1', x, x0) -> as_label_safe s st1'
1058
1059type trace_label_diverges = __trace_label_diverges Lazy.t
1060and __trace_label_diverges =
1061| Tld_step of __ * __ * trace_label_label * trace_label_diverges
1062| Tld_base of __ * __ * __ * trace_label_call * trace_label_diverges
1063
1064(** val trace_label_diverges_inv_rect_Type4 :
1065    abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1066    trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1067    __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1068    __ -> 'a1) -> 'a1 **)
1069let trace_label_diverges_inv_rect_Type4 x1 x2 hterm h1 h2 =
1070  let hcut =
1071    match Lazy.force
1072    hterm with
1073    | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1074    | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1075  in
1076  hcut __ __
1077
1078(** val trace_label_diverges_inv_rect_Type3 :
1079    abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1080    trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1081    __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1082    __ -> 'a1) -> 'a1 **)
1083let trace_label_diverges_inv_rect_Type3 x1 x2 hterm h1 h2 =
1084  let hcut =
1085    match Lazy.force
1086    hterm with
1087    | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1088    | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1089  in
1090  hcut __ __
1091
1092(** val trace_label_diverges_inv_rect_Type2 :
1093    abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1094    trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1095    __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1096    __ -> 'a1) -> 'a1 **)
1097let trace_label_diverges_inv_rect_Type2 x1 x2 hterm h1 h2 =
1098  let hcut =
1099    match Lazy.force
1100    hterm with
1101    | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1102    | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1103  in
1104  hcut __ __
1105
1106(** val trace_label_diverges_inv_rect_Type1 :
1107    abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1108    trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1109    __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1110    __ -> 'a1) -> 'a1 **)
1111let trace_label_diverges_inv_rect_Type1 x1 x2 hterm h1 h2 =
1112  let hcut =
1113    match Lazy.force
1114    hterm with
1115    | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1116    | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1117  in
1118  hcut __ __
1119
1120(** val trace_label_diverges_inv_rect_Type0 :
1121    abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1122    trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1123    __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1124    __ -> 'a1) -> 'a1 **)
1125let trace_label_diverges_inv_rect_Type0 x1 x2 hterm h1 h2 =
1126  let hcut =
1127    match Lazy.force
1128    hterm with
1129    | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1130    | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1131  in
1132  hcut __ __
1133
1134(** val trace_label_diverges_jmdiscr :
1135    abstract_status -> __ -> trace_label_diverges -> trace_label_diverges ->
1136    __ **)
1137let trace_label_diverges_jmdiscr a1 a2 x y =
1138  Logic.eq_rect_Type2 x
1139    (match Lazy.force
1140     x with
1141     | Tld_step (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1142     | Tld_base (a0, a10, a20, a3, a6) ->
1143       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
1144
1145(** val tld_hd_label :
1146    abstract_status -> __ -> trace_label_diverges -> CostLabel.costlabel **)
1147let tld_hd_label s st tr =
1148  match Lazy.force
1149  tr with
1150  | Tld_step (st', st'', tll, x) ->
1151    tll_hd_label s Doesnt_end_with_ret st' st'' tll
1152  | Tld_base (st', st'', x, tlc, x2) -> tlc_hd_label s st' st'' tlc
1153
1154type trace_whole_program =
1155| Twp_terminating of __ * __ * __ * trace_label_return
1156| Twp_diverges of __ * __ * trace_label_diverges
1157
1158(** val trace_whole_program_rect_Type4 :
1159    abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1160    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1161    -> trace_whole_program -> 'a1 **)
1162let rec trace_whole_program_rect_Type4 s h_twp_terminating h_twp_diverges x_3207 = function
1163| Twp_terminating (status_initial, status_start_fun, status_final, x_3210) ->
1164  h_twp_terminating status_initial status_start_fun status_final __ __ x_3210
1165    __
1166| Twp_diverges (status_initial, status_start_fun, x_3213) ->
1167  h_twp_diverges status_initial status_start_fun __ __ x_3213
1168
1169(** val trace_whole_program_rect_Type5 :
1170    abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1171    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1172    -> trace_whole_program -> 'a1 **)
1173let rec trace_whole_program_rect_Type5 s h_twp_terminating h_twp_diverges x_3218 = function
1174| Twp_terminating (status_initial, status_start_fun, status_final, x_3221) ->
1175  h_twp_terminating status_initial status_start_fun status_final __ __ x_3221
1176    __
1177| Twp_diverges (status_initial, status_start_fun, x_3224) ->
1178  h_twp_diverges status_initial status_start_fun __ __ x_3224
1179
1180(** val trace_whole_program_rect_Type3 :
1181    abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1182    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1183    -> trace_whole_program -> 'a1 **)
1184let rec trace_whole_program_rect_Type3 s h_twp_terminating h_twp_diverges x_3229 = function
1185| Twp_terminating (status_initial, status_start_fun, status_final, x_3232) ->
1186  h_twp_terminating status_initial status_start_fun status_final __ __ x_3232
1187    __
1188| Twp_diverges (status_initial, status_start_fun, x_3235) ->
1189  h_twp_diverges status_initial status_start_fun __ __ x_3235
1190
1191(** val trace_whole_program_rect_Type2 :
1192    abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1193    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1194    -> trace_whole_program -> 'a1 **)
1195let rec trace_whole_program_rect_Type2 s h_twp_terminating h_twp_diverges x_3240 = function
1196| Twp_terminating (status_initial, status_start_fun, status_final, x_3243) ->
1197  h_twp_terminating status_initial status_start_fun status_final __ __ x_3243
1198    __
1199| Twp_diverges (status_initial, status_start_fun, x_3246) ->
1200  h_twp_diverges status_initial status_start_fun __ __ x_3246
1201
1202(** val trace_whole_program_rect_Type1 :
1203    abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1204    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1205    -> trace_whole_program -> 'a1 **)
1206let rec trace_whole_program_rect_Type1 s h_twp_terminating h_twp_diverges x_3251 = function
1207| Twp_terminating (status_initial, status_start_fun, status_final, x_3254) ->
1208  h_twp_terminating status_initial status_start_fun status_final __ __ x_3254
1209    __
1210| Twp_diverges (status_initial, status_start_fun, x_3257) ->
1211  h_twp_diverges status_initial status_start_fun __ __ x_3257
1212
1213(** val trace_whole_program_rect_Type0 :
1214    abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1215    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1216    -> trace_whole_program -> 'a1 **)
1217let rec trace_whole_program_rect_Type0 s h_twp_terminating h_twp_diverges x_3262 = function
1218| Twp_terminating (status_initial, status_start_fun, status_final, x_3265) ->
1219  h_twp_terminating status_initial status_start_fun status_final __ __ x_3265
1220    __
1221| Twp_diverges (status_initial, status_start_fun, x_3268) ->
1222  h_twp_diverges status_initial status_start_fun __ __ x_3268
1223
1224(** val trace_whole_program_inv_rect_Type4 :
1225    abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ ->
1226    __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1227    __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **)
1228let trace_whole_program_inv_rect_Type4 x1 x2 hterm h1 h2 =
1229  let hcut = trace_whole_program_rect_Type4 x1 h1 h2 x2 hterm in hcut __ __
1230
1231(** val trace_whole_program_inv_rect_Type3 :
1232    abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ ->
1233    __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1234    __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **)
1235let trace_whole_program_inv_rect_Type3 x1 x2 hterm h1 h2 =
1236  let hcut = trace_whole_program_rect_Type3 x1 h1 h2 x2 hterm in hcut __ __
1237
1238(** val trace_whole_program_inv_rect_Type2 :
1239    abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ ->
1240    __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1241    __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **)
1242let trace_whole_program_inv_rect_Type2 x1 x2 hterm h1 h2 =
1243  let hcut = trace_whole_program_rect_Type2 x1 h1 h2 x2 hterm in hcut __ __
1244
1245(** val trace_whole_program_inv_rect_Type1 :
1246    abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ ->
1247    __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1248    __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **)
1249let trace_whole_program_inv_rect_Type1 x1 x2 hterm h1 h2 =
1250  let hcut = trace_whole_program_rect_Type1 x1 h1 h2 x2 hterm in hcut __ __
1251
1252(** val trace_whole_program_inv_rect_Type0 :
1253    abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ ->
1254    __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1255    __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **)
1256let trace_whole_program_inv_rect_Type0 x1 x2 hterm h1 h2 =
1257  let hcut = trace_whole_program_rect_Type0 x1 h1 h2 x2 hterm in hcut __ __
1258
1259(** val trace_whole_program_jmdiscr :
1260    abstract_status -> __ -> trace_whole_program -> trace_whole_program -> __ **)
1261let trace_whole_program_jmdiscr a1 a2 x y =
1262  Logic.eq_rect_Type2 x
1263    (match x with
1264     | Twp_terminating (a0, a10, a20, a5) ->
1265       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)
1266     | Twp_diverges (a0, a10, a4) ->
1267       Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
1268
1269(** val tal_tl_label :
1270    abstract_status -> __ -> __ -> trace_any_label -> CostLabel.costlabel **)
1271let tal_tl_label s st1 st2 tr =
1272  as_label_safe s st2
1273
1274(** val tll_tl_label :
1275    abstract_status -> __ -> __ -> trace_label_label -> CostLabel.costlabel **)
1276let tll_tl_label s st1 st2 tr =
1277  as_label_safe s st2
1278
1279type trace_any_any =
1280| Taa_base of __
1281| Taa_step of __ * __ * __ * trace_any_any
1282
1283(** val trace_any_any_rect_Type4 :
1284    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1285    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
1286let rec trace_any_any_rect_Type4 s h_taa_base h_taa_step x_3492 x_3491 = function
1287| Taa_base st -> h_taa_base st
1288| Taa_step (st1, st2, st3, x_3494) ->
1289  h_taa_step st1 st2 st3 __ __ __ x_3494
1290    (trace_any_any_rect_Type4 s h_taa_base h_taa_step st2 st3 x_3494)
1291
1292(** val trace_any_any_rect_Type3 :
1293    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1294    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
1295let rec trace_any_any_rect_Type3 s h_taa_base h_taa_step x_3510 x_3509 = function
1296| Taa_base st -> h_taa_base st
1297| Taa_step (st1, st2, st3, x_3512) ->
1298  h_taa_step st1 st2 st3 __ __ __ x_3512
1299    (trace_any_any_rect_Type3 s h_taa_base h_taa_step st2 st3 x_3512)
1300
1301(** val trace_any_any_rect_Type2 :
1302    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1303    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
1304let rec trace_any_any_rect_Type2 s h_taa_base h_taa_step x_3519 x_3518 = function
1305| Taa_base st -> h_taa_base st
1306| Taa_step (st1, st2, st3, x_3521) ->
1307  h_taa_step st1 st2 st3 __ __ __ x_3521
1308    (trace_any_any_rect_Type2 s h_taa_base h_taa_step st2 st3 x_3521)
1309
1310(** val trace_any_any_rect_Type1 :
1311    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1312    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
1313let rec trace_any_any_rect_Type1 s h_taa_base h_taa_step x_3528 x_3527 = function
1314| Taa_base st -> h_taa_base st
1315| Taa_step (st1, st2, st3, x_3530) ->
1316  h_taa_step st1 st2 st3 __ __ __ x_3530
1317    (trace_any_any_rect_Type1 s h_taa_base h_taa_step st2 st3 x_3530)
1318
1319(** val trace_any_any_rect_Type0 :
1320    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1321    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
1322let rec trace_any_any_rect_Type0 s h_taa_base h_taa_step x_3537 x_3536 = function
1323| Taa_base st -> h_taa_base st
1324| Taa_step (st1, st2, st3, x_3539) ->
1325  h_taa_step st1 st2 st3 __ __ __ x_3539
1326    (trace_any_any_rect_Type0 s h_taa_base h_taa_step st2 st3 x_3539)
1327
1328(** val trace_any_any_inv_rect_Type4 :
1329    abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
1330    'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __
1331    -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1332let trace_any_any_inv_rect_Type4 x1 x2 x3 hterm h1 h2 =
1333  let hcut = trace_any_any_rect_Type4 x1 h1 h2 x2 x3 hterm in hcut __ __ __
1334
1335(** val trace_any_any_inv_rect_Type3 :
1336    abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
1337    'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __
1338    -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1339let trace_any_any_inv_rect_Type3 x1 x2 x3 hterm h1 h2 =
1340  let hcut = trace_any_any_rect_Type3 x1 h1 h2 x2 x3 hterm in hcut __ __ __
1341
1342(** val trace_any_any_inv_rect_Type2 :
1343    abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
1344    'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __
1345    -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1346let trace_any_any_inv_rect_Type2 x1 x2 x3 hterm h1 h2 =
1347  let hcut = trace_any_any_rect_Type2 x1 h1 h2 x2 x3 hterm in hcut __ __ __
1348
1349(** val trace_any_any_inv_rect_Type1 :
1350    abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
1351    'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __
1352    -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1353let trace_any_any_inv_rect_Type1 x1 x2 x3 hterm h1 h2 =
1354  let hcut = trace_any_any_rect_Type1 x1 h1 h2 x2 x3 hterm in hcut __ __ __
1355
1356(** val trace_any_any_inv_rect_Type0 :
1357    abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
1358    'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __
1359    -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1360let trace_any_any_inv_rect_Type0 x1 x2 x3 hterm h1 h2 =
1361  let hcut = trace_any_any_rect_Type0 x1 h1 h2 x2 x3 hterm in hcut __ __ __
1362
1363(** val trace_any_any_jmdiscr :
1364    abstract_status -> __ -> __ -> trace_any_any -> trace_any_any -> __ **)
1365let trace_any_any_jmdiscr a1 a2 a3 x y =
1366  Logic.eq_rect_Type2 x
1367    (match x with
1368     | Taa_base a0 -> Obj.magic (fun _ dH -> dH __)
1369     | Taa_step (a0, a10, a20, a6) ->
1370       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
1371
1372(** val taa_non_empty :
1373    abstract_status -> __ -> __ -> trace_any_any -> Bool.bool **)
1374let taa_non_empty s st1 st2 = function
1375| Taa_base x -> Bool.False
1376| Taa_step (x, x0, x1, x5) -> Bool.True
1377
1378(** val taa_append_tal :
1379    abstract_status -> __ -> trace_ends_with_ret -> __ -> __ -> trace_any_any
1380    -> trace_any_label -> trace_any_label **)
1381let rec taa_append_tal s st1 fl st2 st3 taa =
1382  (match taa with
1383   | Taa_base st1' -> (fun fl0 st30 tal2 -> tal2)
1384   | Taa_step (st1', st2', st3', tl) ->
1385     (fun fl0 st30 tal2 -> Tal_step_default (fl0, st1', st2', st30,
1386       (taa_append_tal s st2' fl0 st3' st30 tl tal2)))) fl st3
1387
1388type tal_collapsable = __
1389
1390type tal_rel = __
1391
1392type tll_rel = __
1393
1394type tlr_rel = __
1395
1396(** val flatten_trace_label_label :
1397    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
1398    -> as_cost_label List.list **)
1399let rec flatten_trace_label_label s trace_ends_flag start_status final_status = function
1400| Tll_base (ends_flag, initial, final, given_trace) ->
1401  let label =
1402    (match as_label s initial with
1403     | Types.None -> (fun _ -> assert false (* absurd case *))
1404     | Types.Some l -> (fun _ -> l)) __
1405  in
1406  List.Cons (label,
1407  (flatten_trace_any_label s ends_flag initial final given_trace))
1408(** val flatten_trace_any_label :
1409    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
1410    as_cost_label List.list **)
1411and flatten_trace_any_label s trace_ends_flag start_status final_status = function
1412| Tal_base_not_return (the_status, x) -> List.Nil
1413| Tal_base_return (the_status, x) -> List.Nil
1414| Tal_base_call (pre_fun_call, start_fun_call, final, call_trace) ->
1415  flatten_trace_label_return s start_fun_call final call_trace
1416| Tal_base_tailcall (pre_fun_call, start_fun_call, final, call_trace) ->
1417  flatten_trace_label_return s start_fun_call final call_trace
1418| Tal_step_call
1419    (end_flag, pre_fun_call, start_fun_call, after_fun_call, final,
1420     call_trace, final_trace) ->
1421  let call_cost_trace =
1422    flatten_trace_label_return s start_fun_call after_fun_call call_trace
1423  in
1424  let final_cost_trace =
1425    flatten_trace_any_label s end_flag after_fun_call final final_trace
1426  in
1427  List.append call_cost_trace final_cost_trace
1428| Tal_step_default
1429    (end_flag, status_pre, status_init, status_end, tail_trace) ->
1430  flatten_trace_any_label s end_flag status_init status_end tail_trace
1431(** val flatten_trace_label_return :
1432    abstract_status -> __ -> __ -> trace_label_return -> as_cost_label
1433    List.list **)
1434and flatten_trace_label_return s start_status final_status = function
1435| Tlr_base (before, after, trace_to_lift) ->
1436  flatten_trace_label_label s Ends_with_ret before after trace_to_lift
1437| Tlr_step (initial, labelled, final, labelled_trace, ret_trace) ->
1438  let labelled_cost =
1439    flatten_trace_label_label s Doesnt_end_with_ret initial labelled
1440      labelled_trace
1441  in
1442  let return_cost = flatten_trace_label_return s labelled final ret_trace in
1443  List.append labelled_cost return_cost
1444
Note: See TracBrowser for help on using the repository browser.