source: extracted/structuredTraces.ml @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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