source: extracted/structuredTraces.ml @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

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