source: extracted/structuredTraces.ml @ 3043

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

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 80.2 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Relations
12
13open Bool
14
15open Jmeq
16
17open Proper
18
19open PositiveMap
20
21open Deqsets
22
23open ErrorMessages
24
25open PreIdentifiers
26
27open Errors
28
29open Extralib
30
31open Setoids
32
33open Monad
34
35open Option
36
37open Div_and_mod
38
39open Russell
40
41open Util
42
43open List
44
45open Lists
46
47open Nat
48
49open Positive
50
51open Types
52
53open Identifiers
54
55open CostLabel
56
57open Sets
58
59open Listb
60
61open Integers
62
63open AST
64
65open Division
66
67open Exp
68
69open Arithmetic
70
71open Extranat
72
73open Vector
74
75open FoldStuff
76
77open BitVector
78
79open Z
80
81open BitVectorZ
82
83open Pointers
84
85open Coqlib
86
87open Values
88
89open Events
90
91open IOMonad
92
93open IO
94
95open Hide
96
97type status_class =
98| Cl_return
99| Cl_jump
100| Cl_call
101| Cl_tailcall
102| Cl_other
103
104(** val status_class_rect_Type4 :
105    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
106let rec status_class_rect_Type4 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
107| Cl_return -> h_cl_return
108| Cl_jump -> h_cl_jump
109| Cl_call -> h_cl_call
110| Cl_tailcall -> h_cl_tailcall
111| Cl_other -> h_cl_other
112
113(** val status_class_rect_Type5 :
114    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
115let rec status_class_rect_Type5 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
116| Cl_return -> h_cl_return
117| Cl_jump -> h_cl_jump
118| Cl_call -> h_cl_call
119| Cl_tailcall -> h_cl_tailcall
120| Cl_other -> h_cl_other
121
122(** val status_class_rect_Type3 :
123    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
124let rec status_class_rect_Type3 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
125| Cl_return -> h_cl_return
126| Cl_jump -> h_cl_jump
127| Cl_call -> h_cl_call
128| Cl_tailcall -> h_cl_tailcall
129| Cl_other -> h_cl_other
130
131(** val status_class_rect_Type2 :
132    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
133let rec status_class_rect_Type2 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
134| Cl_return -> h_cl_return
135| Cl_jump -> h_cl_jump
136| Cl_call -> h_cl_call
137| Cl_tailcall -> h_cl_tailcall
138| Cl_other -> h_cl_other
139
140(** val status_class_rect_Type1 :
141    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
142let rec status_class_rect_Type1 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
143| Cl_return -> h_cl_return
144| Cl_jump -> h_cl_jump
145| Cl_call -> h_cl_call
146| Cl_tailcall -> h_cl_tailcall
147| Cl_other -> h_cl_other
148
149(** val status_class_rect_Type0 :
150    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
151let rec status_class_rect_Type0 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
152| Cl_return -> h_cl_return
153| Cl_jump -> h_cl_jump
154| Cl_call -> h_cl_call
155| Cl_tailcall -> h_cl_tailcall
156| Cl_other -> h_cl_other
157
158(** val status_class_inv_rect_Type4 :
159    status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
160    -> (__ -> 'a1) -> 'a1 **)
161let status_class_inv_rect_Type4 hterm h1 h2 h3 h4 h5 =
162  let hcut = status_class_rect_Type4 h1 h2 h3 h4 h5 hterm in hcut __
163
164(** val status_class_inv_rect_Type3 :
165    status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
166    -> (__ -> 'a1) -> 'a1 **)
167let status_class_inv_rect_Type3 hterm h1 h2 h3 h4 h5 =
168  let hcut = status_class_rect_Type3 h1 h2 h3 h4 h5 hterm in hcut __
169
170(** val status_class_inv_rect_Type2 :
171    status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
172    -> (__ -> 'a1) -> 'a1 **)
173let status_class_inv_rect_Type2 hterm h1 h2 h3 h4 h5 =
174  let hcut = status_class_rect_Type2 h1 h2 h3 h4 h5 hterm in hcut __
175
176(** val status_class_inv_rect_Type1 :
177    status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
178    -> (__ -> 'a1) -> 'a1 **)
179let status_class_inv_rect_Type1 hterm h1 h2 h3 h4 h5 =
180  let hcut = status_class_rect_Type1 h1 h2 h3 h4 h5 hterm in hcut __
181
182(** val status_class_inv_rect_Type0 :
183    status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
184    -> (__ -> 'a1) -> 'a1 **)
185let status_class_inv_rect_Type0 hterm h1 h2 h3 h4 h5 =
186  let hcut = status_class_rect_Type0 h1 h2 h3 h4 h5 hterm in hcut __
187
188(** val status_class_discr : status_class -> status_class -> __ **)
189let status_class_discr x y =
190  Logic.eq_rect_Type2 x
191    (match x with
192     | Cl_return -> Obj.magic (fun _ dH -> dH)
193     | Cl_jump -> Obj.magic (fun _ dH -> dH)
194     | Cl_call -> Obj.magic (fun _ dH -> dH)
195     | Cl_tailcall -> Obj.magic (fun _ dH -> dH)
196     | Cl_other -> Obj.magic (fun _ dH -> dH)) y
197
198(** val status_class_jmdiscr : status_class -> status_class -> __ **)
199let status_class_jmdiscr x y =
200  Logic.eq_rect_Type2 x
201    (match x with
202     | Cl_return -> Obj.magic (fun _ dH -> dH)
203     | Cl_jump -> Obj.magic (fun _ dH -> dH)
204     | Cl_call -> Obj.magic (fun _ dH -> dH)
205     | Cl_tailcall -> Obj.magic (fun _ dH -> dH)
206     | Cl_other -> Obj.magic (fun _ dH -> dH)) y
207
208type abstract_status = { as_pc : Deqsets.deqSet; as_pc_of : (__ -> __);
209                         as_classify : (__ -> status_class);
210                         as_label_of_pc : (__ -> CostLabel.costlabel
211                                          Types.option);
212                         as_result : (__ -> Integers.int Types.option);
213                         as_call_ident : (__ Types.sig0 -> AST.ident);
214                         as_tailcall_ident : (__ Types.sig0 -> AST.ident) }
215
216(** val abstract_status_rect_Type4 :
217    (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
218    -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
219    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
220    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
221let rec abstract_status_rect_Type4 h_mk_abstract_status x_81 =
222  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
223    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
224    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_81
225  in
226  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
227    as_result0 as_call_ident0 as_tailcall_ident0
228
229(** val abstract_status_rect_Type5 :
230    (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
231    -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
232    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
233    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
234let rec abstract_status_rect_Type5 h_mk_abstract_status x_83 =
235  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
236    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
237    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_83
238  in
239  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
240    as_result0 as_call_ident0 as_tailcall_ident0
241
242(** val abstract_status_rect_Type3 :
243    (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
244    -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
245    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
246    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
247let rec abstract_status_rect_Type3 h_mk_abstract_status x_85 =
248  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
249    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
250    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_85
251  in
252  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
253    as_result0 as_call_ident0 as_tailcall_ident0
254
255(** val abstract_status_rect_Type2 :
256    (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
257    -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
258    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
259    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
260let rec abstract_status_rect_Type2 h_mk_abstract_status x_87 =
261  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
262    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
263    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_87
264  in
265  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
266    as_result0 as_call_ident0 as_tailcall_ident0
267
268(** val abstract_status_rect_Type1 :
269    (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
270    -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
271    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
272    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
273let rec abstract_status_rect_Type1 h_mk_abstract_status x_89 =
274  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
275    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
276    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_89
277  in
278  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
279    as_result0 as_call_ident0 as_tailcall_ident0
280
281(** val abstract_status_rect_Type0 :
282    (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
283    -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
284    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
285    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
286let rec abstract_status_rect_Type0 h_mk_abstract_status x_91 =
287  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
288    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
289    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_91
290  in
291  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
292    as_result0 as_call_ident0 as_tailcall_ident0
293
294type as_status = __
295
296(** val as_pc : abstract_status -> Deqsets.deqSet **)
297let rec as_pc xxx =
298  xxx.as_pc
299
300(** val as_pc_of : abstract_status -> __ -> __ **)
301let rec as_pc_of xxx =
302  xxx.as_pc_of
303
304(** val as_classify : abstract_status -> __ -> status_class **)
305let rec as_classify xxx =
306  xxx.as_classify
307
308(** val as_label_of_pc :
309    abstract_status -> __ -> CostLabel.costlabel Types.option **)
310let rec as_label_of_pc xxx =
311  xxx.as_label_of_pc
312
313(** val as_result : abstract_status -> __ -> Integers.int Types.option **)
314let rec as_result xxx =
315  xxx.as_result
316
317(** val as_call_ident : abstract_status -> __ Types.sig0 -> AST.ident **)
318let rec as_call_ident xxx =
319  xxx.as_call_ident
320
321(** val as_tailcall_ident : abstract_status -> __ Types.sig0 -> AST.ident **)
322let rec as_tailcall_ident xxx =
323  xxx.as_tailcall_ident
324
325(** val abstract_status_inv_rect_Type4 :
326    abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
327    status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
328    Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
329    Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
330let abstract_status_inv_rect_Type4 hterm h1 =
331  let hcut = abstract_status_rect_Type4 h1 hterm in hcut __
332
333(** val abstract_status_inv_rect_Type3 :
334    abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
335    status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
336    Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
337    Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
338let abstract_status_inv_rect_Type3 hterm h1 =
339  let hcut = abstract_status_rect_Type3 h1 hterm in hcut __
340
341(** val abstract_status_inv_rect_Type2 :
342    abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
343    status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
344    Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
345    Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
346let abstract_status_inv_rect_Type2 hterm h1 =
347  let hcut = abstract_status_rect_Type2 h1 hterm in hcut __
348
349(** val abstract_status_inv_rect_Type1 :
350    abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
351    status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
352    Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
353    Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
354let abstract_status_inv_rect_Type1 hterm h1 =
355  let hcut = abstract_status_rect_Type1 h1 hterm in hcut __
356
357(** val abstract_status_inv_rect_Type0 :
358    abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
359    status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
360    Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
361    Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
362let abstract_status_inv_rect_Type0 hterm h1 =
363  let hcut = abstract_status_rect_Type0 h1 hterm in hcut __
364
365(** val abstract_status_jmdiscr :
366    abstract_status -> abstract_status -> __ **)
367let abstract_status_jmdiscr x y =
368  Logic.eq_rect_Type2 x
369    (let { as_pc = a2; as_pc_of = a3; as_classify = a4; as_label_of_pc = a5;
370       as_result = a7; as_call_ident = a8; as_tailcall_ident = a9 } = x
371     in
372    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)) y
373
374(** val as_label :
375    abstract_status -> __ -> CostLabel.costlabel Types.option **)
376let as_label s s0 =
377  s.as_label_of_pc (s.as_pc_of s0)
378
379(** val as_costed_exc : abstract_status -> __ -> (__, __) Types.sum **)
380let as_costed_exc s s0 =
381  match as_label s s0 with
382  | Types.None -> Types.Inr __
383  | Types.Some c -> Types.Inl __
384
385type as_cost_label = CostLabel.costlabel Types.sig0
386
387type as_cost_labels = as_cost_label List.list
388
389(** val as_cost_get_label :
390    abstract_status -> as_cost_label -> CostLabel.costlabel **)
391let as_cost_get_label s l_sig =
392  Types.pi1 l_sig
393
394type as_cost_map = as_cost_label -> Nat.nat
395
396(** val as_label_safe : abstract_status -> __ Types.sig0 -> as_cost_label **)
397let as_label_safe a_s st_sig =
398  Option.opt_safe (as_label a_s (Types.pi1 st_sig))
399
400(** val lift_sigma_map_id :
401    'a2 -> ('a1 -> (__, __) Types.sum) -> ('a1 Types.sig0 -> 'a2) -> 'a1
402    Types.sig0 -> 'a2 **)
403let lift_sigma_map_id dflt dec m a_sig =
404  match dec (Types.pi1 a_sig) with
405  | Types.Inl _ -> m (Types.pi1 a_sig)
406  | Types.Inr _ -> dflt
407
408(** val lift_cost_map_id :
409    abstract_status -> abstract_status -> (CostLabel.costlabel -> (__, __)
410    Types.sum) -> as_cost_map -> as_cost_map **)
411let lift_cost_map_id s_in s_out =
412  lift_sigma_map_id Nat.O
413
414type trace_ends_with_ret =
415| Ends_with_ret
416| Doesnt_end_with_ret
417
418(** val trace_ends_with_ret_rect_Type4 :
419    'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
420let rec trace_ends_with_ret_rect_Type4 h_ends_with_ret h_doesnt_end_with_ret = function
421| Ends_with_ret -> h_ends_with_ret
422| Doesnt_end_with_ret -> h_doesnt_end_with_ret
423
424(** val trace_ends_with_ret_rect_Type5 :
425    'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
426let rec trace_ends_with_ret_rect_Type5 h_ends_with_ret h_doesnt_end_with_ret = function
427| Ends_with_ret -> h_ends_with_ret
428| Doesnt_end_with_ret -> h_doesnt_end_with_ret
429
430(** val trace_ends_with_ret_rect_Type3 :
431    'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
432let rec trace_ends_with_ret_rect_Type3 h_ends_with_ret h_doesnt_end_with_ret = function
433| Ends_with_ret -> h_ends_with_ret
434| Doesnt_end_with_ret -> h_doesnt_end_with_ret
435
436(** val trace_ends_with_ret_rect_Type2 :
437    'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
438let rec trace_ends_with_ret_rect_Type2 h_ends_with_ret h_doesnt_end_with_ret = function
439| Ends_with_ret -> h_ends_with_ret
440| Doesnt_end_with_ret -> h_doesnt_end_with_ret
441
442(** val trace_ends_with_ret_rect_Type1 :
443    'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
444let rec trace_ends_with_ret_rect_Type1 h_ends_with_ret h_doesnt_end_with_ret = function
445| Ends_with_ret -> h_ends_with_ret
446| Doesnt_end_with_ret -> h_doesnt_end_with_ret
447
448(** val trace_ends_with_ret_rect_Type0 :
449    'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
450let rec trace_ends_with_ret_rect_Type0 h_ends_with_ret h_doesnt_end_with_ret = function
451| Ends_with_ret -> h_ends_with_ret
452| Doesnt_end_with_ret -> h_doesnt_end_with_ret
453
454(** val trace_ends_with_ret_inv_rect_Type4 :
455    trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
456let trace_ends_with_ret_inv_rect_Type4 hterm h1 h2 =
457  let hcut = trace_ends_with_ret_rect_Type4 h1 h2 hterm in hcut __
458
459(** val trace_ends_with_ret_inv_rect_Type3 :
460    trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
461let trace_ends_with_ret_inv_rect_Type3 hterm h1 h2 =
462  let hcut = trace_ends_with_ret_rect_Type3 h1 h2 hterm in hcut __
463
464(** val trace_ends_with_ret_inv_rect_Type2 :
465    trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
466let trace_ends_with_ret_inv_rect_Type2 hterm h1 h2 =
467  let hcut = trace_ends_with_ret_rect_Type2 h1 h2 hterm in hcut __
468
469(** val trace_ends_with_ret_inv_rect_Type1 :
470    trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
471let trace_ends_with_ret_inv_rect_Type1 hterm h1 h2 =
472  let hcut = trace_ends_with_ret_rect_Type1 h1 h2 hterm in hcut __
473
474(** val trace_ends_with_ret_inv_rect_Type0 :
475    trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
476let trace_ends_with_ret_inv_rect_Type0 hterm h1 h2 =
477  let hcut = trace_ends_with_ret_rect_Type0 h1 h2 hterm in hcut __
478
479(** val trace_ends_with_ret_discr :
480    trace_ends_with_ret -> trace_ends_with_ret -> __ **)
481let trace_ends_with_ret_discr 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
487(** val trace_ends_with_ret_jmdiscr :
488    trace_ends_with_ret -> trace_ends_with_ret -> __ **)
489let trace_ends_with_ret_jmdiscr x y =
490  Logic.eq_rect_Type2 x
491    (match x with
492     | Ends_with_ret -> Obj.magic (fun _ dH -> dH)
493     | Doesnt_end_with_ret -> Obj.magic (fun _ dH -> dH)) y
494
495type trace_label_return =
496| Tlr_base of __ * __ * trace_label_label
497| Tlr_step of __ * __ * __ * trace_label_label * trace_label_return
498and trace_label_label =
499| Tll_base of trace_ends_with_ret * __ * __ * trace_any_label
500and trace_any_label =
501| Tal_base_not_return of __ * __
502| Tal_base_return of __ * __
503| Tal_base_call of __ * __ * __ * trace_label_return
504| Tal_base_tailcall of __ * __ * __ * trace_label_return
505| Tal_step_call of trace_ends_with_ret * __ * __ * __ * __
506   * trace_label_return * trace_any_label
507| Tal_step_default of trace_ends_with_ret * __ * __ * __ * trace_any_label
508
509(** val trace_label_return_inv_rect_Type4 :
510    abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
511    trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
512    trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
513let trace_label_return_inv_rect_Type4 x1 x2 x3 hterm h1 h2 =
514  let hcut =
515    match hterm with
516    | Tlr_base (x, x0, x4) -> h1 x x0 x4
517    | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
518  in
519  hcut __ __ __
520
521(** val trace_label_return_inv_rect_Type3 :
522    abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
523    trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
524    trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
525let trace_label_return_inv_rect_Type3 x1 x2 x3 hterm h1 h2 =
526  let hcut =
527    match hterm with
528    | Tlr_base (x, x0, x4) -> h1 x x0 x4
529    | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
530  in
531  hcut __ __ __
532
533(** val trace_label_return_inv_rect_Type2 :
534    abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
535    trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
536    trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
537let trace_label_return_inv_rect_Type2 x1 x2 x3 hterm h1 h2 =
538  let hcut =
539    match hterm with
540    | Tlr_base (x, x0, x4) -> h1 x x0 x4
541    | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
542  in
543  hcut __ __ __
544
545(** val trace_label_return_inv_rect_Type1 :
546    abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
547    trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
548    trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
549let trace_label_return_inv_rect_Type1 x1 x2 x3 hterm h1 h2 =
550  let hcut =
551    match hterm with
552    | Tlr_base (x, x0, x4) -> h1 x x0 x4
553    | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
554  in
555  hcut __ __ __
556
557(** val trace_label_return_inv_rect_Type0 :
558    abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
559    trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
560    trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
561let trace_label_return_inv_rect_Type0 x1 x2 x3 hterm h1 h2 =
562  let hcut =
563    match hterm with
564    | Tlr_base (x, x0, x4) -> h1 x x0 x4
565    | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
566  in
567  hcut __ __ __
568
569(** val trace_label_label_inv_rect_Type4 :
570    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
571    -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
572    -> __ -> __ -> 'a1) -> 'a1 **)
573let trace_label_label_inv_rect_Type4 x1 x2 x3 x4 hterm h1 =
574  let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
575  hcut __ __ __ __
576
577(** val trace_label_label_inv_rect_Type3 :
578    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
579    -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
580    -> __ -> __ -> 'a1) -> 'a1 **)
581let trace_label_label_inv_rect_Type3 x1 x2 x3 x4 hterm h1 =
582  let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
583  hcut __ __ __ __
584
585(** val trace_label_label_inv_rect_Type2 :
586    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
587    -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
588    -> __ -> __ -> 'a1) -> 'a1 **)
589let trace_label_label_inv_rect_Type2 x1 x2 x3 x4 hterm h1 =
590  let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
591  hcut __ __ __ __
592
593(** val trace_label_label_inv_rect_Type1 :
594    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
595    -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
596    -> __ -> __ -> 'a1) -> 'a1 **)
597let trace_label_label_inv_rect_Type1 x1 x2 x3 x4 hterm h1 =
598  let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
599  hcut __ __ __ __
600
601(** val trace_label_label_inv_rect_Type0 :
602    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
603    -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
604    -> __ -> __ -> 'a1) -> 'a1 **)
605let trace_label_label_inv_rect_Type0 x1 x2 x3 x4 hterm h1 =
606  let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
607  hcut __ __ __ __
608
609(** val trace_any_label_inv_rect_Type4 :
610    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
611    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
612    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
613    __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
614    (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
615    -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
616    -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
617    'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
618    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
619let trace_any_label_inv_rect_Type4 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
620  let hcut =
621    match hterm with
622    | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
623    | Tal_base_return (x, x0) -> h2 x x0 __ __
624    | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
625    | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
626    | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
627      h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
628    | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
629  in
630  hcut __ __ __ __
631
632(** val trace_any_label_inv_rect_Type3 :
633    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
634    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
635    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
636    __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
637    (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
638    -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
639    -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
640    'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
641    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
642let trace_any_label_inv_rect_Type3 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
643  let hcut =
644    match hterm with
645    | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
646    | Tal_base_return (x, x0) -> h2 x x0 __ __
647    | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
648    | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
649    | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
650      h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
651    | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
652  in
653  hcut __ __ __ __
654
655(** val trace_any_label_inv_rect_Type2 :
656    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
657    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
658    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
659    __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
660    (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
661    -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
662    -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
663    'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
664    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
665let trace_any_label_inv_rect_Type2 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
666  let hcut =
667    match hterm with
668    | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
669    | Tal_base_return (x, x0) -> h2 x x0 __ __
670    | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
671    | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
672    | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
673      h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
674    | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
675  in
676  hcut __ __ __ __
677
678(** val trace_any_label_inv_rect_Type1 :
679    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
680    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
681    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
682    __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
683    (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
684    -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
685    -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
686    'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
687    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
688let trace_any_label_inv_rect_Type1 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
689  let hcut =
690    match hterm with
691    | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
692    | Tal_base_return (x, x0) -> h2 x x0 __ __
693    | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
694    | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
695    | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
696      h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
697    | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
698  in
699  hcut __ __ __ __
700
701(** val trace_any_label_inv_rect_Type0 :
702    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
703    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
704    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
705    __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
706    (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
707    -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
708    -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
709    'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
710    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
711let trace_any_label_inv_rect_Type0 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
712  let hcut =
713    match hterm with
714    | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
715    | Tal_base_return (x, x0) -> h2 x x0 __ __
716    | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
717    | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
718    | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
719      h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
720    | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
721  in
722  hcut __ __ __ __
723
724(** val trace_label_return_discr :
725    abstract_status -> __ -> __ -> trace_label_return -> trace_label_return
726    -> __ **)
727let trace_label_return_discr a1 a2 a3 x y =
728  Logic.eq_rect_Type2 x
729    (match x with
730     | Tlr_base (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
731     | Tlr_step (a0, a10, a20, a30, a4) ->
732       Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
733
734(** val trace_label_label_discr :
735    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
736    -> trace_label_label -> __ **)
737let trace_label_label_discr a1 a2 a3 a4 x y =
738  Logic.eq_rect_Type2 x
739    (let Tll_base (a0, a10, a20, a30) = x in
740    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
741
742(** val trace_label_return_jmdiscr :
743    abstract_status -> __ -> __ -> trace_label_return -> trace_label_return
744    -> __ **)
745let trace_label_return_jmdiscr a1 a2 a3 x y =
746  Logic.eq_rect_Type2 x
747    (match x with
748     | Tlr_base (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
749     | Tlr_step (a0, a10, a20, a30, a4) ->
750       Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
751
752(** val trace_label_label_jmdiscr :
753    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
754    -> trace_label_label -> __ **)
755let trace_label_label_jmdiscr a1 a2 a3 a4 x y =
756  Logic.eq_rect_Type2 x
757    (let Tll_base (a0, a10, a20, a30) = x in
758    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
759
760(** val trace_any_label_jmdiscr :
761    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
762    trace_any_label -> __ **)
763let trace_any_label_jmdiscr a1 a2 a3 a4 x y =
764  Logic.eq_rect_Type2 x
765    (match x with
766     | Tal_base_not_return (a0, a10) ->
767       Obj.magic (fun _ dH -> dH __ __ __ __ __)
768     | Tal_base_return (a0, a10) -> Obj.magic (fun _ dH -> dH __ __ __ __)
769     | Tal_base_call (a0, a10, a20, a6) ->
770       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)
771     | Tal_base_tailcall (a0, a10, a20, a5) ->
772       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
773     | Tal_step_call (a0, a10, a20, a30, a40, a8, a100) ->
774       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)
775     | Tal_step_default (a0, a10, a20, a30, a5) ->
776       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)) y
777
778(** val tal_pc_list :
779    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
780    __ List.list **)
781let rec tal_pc_list s fl st1 st2 = function
782| Tal_base_not_return (pre, x) -> List.Cons ((s.as_pc_of pre), List.Nil)
783| Tal_base_return (pre, x) -> List.Cons ((s.as_pc_of pre), List.Nil)
784| Tal_base_call (pre, x, x0, x4) -> List.Cons ((s.as_pc_of pre), List.Nil)
785| Tal_base_tailcall (pre, x, x0, x3) ->
786  List.Cons ((s.as_pc_of pre), List.Nil)
787| Tal_step_call (fl', pre, x, st1', st2', x3, tl) ->
788  List.Cons ((s.as_pc_of pre), (tal_pc_list s fl' st1' st2' tl))
789| Tal_step_default (fl', pre, st1', st2', tl) ->
790  List.Cons ((s.as_pc_of pre), (tal_pc_list s fl' st1' st2' tl))
791
792(** val as_trace_any_label_length' :
793    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
794    Nat.nat **)
795let as_trace_any_label_length' s trace_ends_flag start_status final_status the_trace =
796  List.length
797    (tal_pc_list s trace_ends_flag start_status final_status the_trace)
798
799(** val tll_hd_label :
800    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
801    -> CostLabel.costlabel **)
802let tll_hd_label s fl st1 st2 tr =
803  (let Tll_base (x, st1', x0, x1) = tr in
804  (fun _ _ _ _ -> Types.pi1 (as_label_safe s st1'))) __ __ __ __
805
806(** val tlr_hd_label :
807    abstract_status -> __ -> __ -> trace_label_return -> CostLabel.costlabel **)
808let tlr_hd_label s st1 st2 = function
809| Tlr_base (st1', st2', tll) -> tll_hd_label s Ends_with_ret st1' st2' tll
810| Tlr_step (st1', st2', x, tll, x0) ->
811  tll_hd_label s Doesnt_end_with_ret st1' st2' tll
812
813type trace_any_call =
814| Tac_base of __
815| Tac_step_call of __ * __ * __ * __ * trace_label_return * trace_any_call
816| Tac_step_default of __ * __ * __ * trace_any_call
817
818(** val trace_any_call_rect_Type4 :
819    abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
820    -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
821    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
822    __ -> trace_any_call -> 'a1 **)
823let rec trace_any_call_rect_Type4 s h_tac_base h_tac_step_call h_tac_step_default x_169 x_168 = function
824| Tac_base status -> h_tac_base status __
825| Tac_step_call
826    (status_pre_fun_call, status_after_fun_call, status_final,
827     status_start_fun_call, x_174, x_172) ->
828  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
829    status_start_fun_call __ __ __ x_174 __ x_172
830    (trace_any_call_rect_Type4 s h_tac_base h_tac_step_call
831      h_tac_step_default status_after_fun_call status_final x_172)
832| Tac_step_default (status_pre, status_end, status_init, x_179) ->
833  h_tac_step_default status_pre status_end status_init __ x_179 __ __
834    (trace_any_call_rect_Type4 s h_tac_base h_tac_step_call
835      h_tac_step_default status_init status_end x_179)
836
837(** val trace_any_call_rect_Type3 :
838    abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
839    -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
840    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
841    __ -> trace_any_call -> 'a1 **)
842let rec trace_any_call_rect_Type3 s h_tac_base h_tac_step_call h_tac_step_default x_201 x_200 = function
843| Tac_base status -> h_tac_base status __
844| Tac_step_call
845    (status_pre_fun_call, status_after_fun_call, status_final,
846     status_start_fun_call, x_206, x_204) ->
847  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
848    status_start_fun_call __ __ __ x_206 __ x_204
849    (trace_any_call_rect_Type3 s h_tac_base h_tac_step_call
850      h_tac_step_default status_after_fun_call status_final x_204)
851| Tac_step_default (status_pre, status_end, status_init, x_211) ->
852  h_tac_step_default status_pre status_end status_init __ x_211 __ __
853    (trace_any_call_rect_Type3 s h_tac_base h_tac_step_call
854      h_tac_step_default status_init status_end x_211)
855
856(** val trace_any_call_rect_Type2 :
857    abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
858    -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
859    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
860    __ -> trace_any_call -> 'a1 **)
861let rec trace_any_call_rect_Type2 s h_tac_base h_tac_step_call h_tac_step_default x_217 x_216 = function
862| Tac_base status -> h_tac_base status __
863| Tac_step_call
864    (status_pre_fun_call, status_after_fun_call, status_final,
865     status_start_fun_call, x_222, x_220) ->
866  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
867    status_start_fun_call __ __ __ x_222 __ x_220
868    (trace_any_call_rect_Type2 s h_tac_base h_tac_step_call
869      h_tac_step_default status_after_fun_call status_final x_220)
870| Tac_step_default (status_pre, status_end, status_init, x_227) ->
871  h_tac_step_default status_pre status_end status_init __ x_227 __ __
872    (trace_any_call_rect_Type2 s h_tac_base h_tac_step_call
873      h_tac_step_default status_init status_end x_227)
874
875(** val trace_any_call_rect_Type1 :
876    abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
877    -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
878    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
879    __ -> trace_any_call -> 'a1 **)
880let rec trace_any_call_rect_Type1 s h_tac_base h_tac_step_call h_tac_step_default x_233 x_232 = function
881| Tac_base status -> h_tac_base status __
882| Tac_step_call
883    (status_pre_fun_call, status_after_fun_call, status_final,
884     status_start_fun_call, x_238, x_236) ->
885  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
886    status_start_fun_call __ __ __ x_238 __ x_236
887    (trace_any_call_rect_Type1 s h_tac_base h_tac_step_call
888      h_tac_step_default status_after_fun_call status_final x_236)
889| Tac_step_default (status_pre, status_end, status_init, x_243) ->
890  h_tac_step_default status_pre status_end status_init __ x_243 __ __
891    (trace_any_call_rect_Type1 s h_tac_base h_tac_step_call
892      h_tac_step_default status_init status_end x_243)
893
894(** val trace_any_call_rect_Type0 :
895    abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
896    -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
897    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
898    __ -> trace_any_call -> 'a1 **)
899let rec trace_any_call_rect_Type0 s h_tac_base h_tac_step_call h_tac_step_default x_249 x_248 = function
900| Tac_base status -> h_tac_base status __
901| Tac_step_call
902    (status_pre_fun_call, status_after_fun_call, status_final,
903     status_start_fun_call, x_254, x_252) ->
904  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
905    status_start_fun_call __ __ __ x_254 __ x_252
906    (trace_any_call_rect_Type0 s h_tac_base h_tac_step_call
907      h_tac_step_default status_after_fun_call status_final x_252)
908| Tac_step_default (status_pre, status_end, status_init, x_259) ->
909  h_tac_step_default status_pre status_end status_init __ x_259 __ __
910    (trace_any_call_rect_Type0 s h_tac_base h_tac_step_call
911      h_tac_step_default status_init status_end x_259)
912
913(** val trace_any_call_inv_rect_Type4 :
914    abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
915    __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
916    trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
917    __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
918    -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
919let trace_any_call_inv_rect_Type4 x1 x2 x3 hterm h1 h2 h3 =
920  let hcut = trace_any_call_rect_Type4 x1 h1 h2 h3 x2 x3 hterm in
921  hcut __ __ __
922
923(** val trace_any_call_inv_rect_Type3 :
924    abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
925    __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
926    trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
927    __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
928    -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
929let trace_any_call_inv_rect_Type3 x1 x2 x3 hterm h1 h2 h3 =
930  let hcut = trace_any_call_rect_Type3 x1 h1 h2 h3 x2 x3 hterm in
931  hcut __ __ __
932
933(** val trace_any_call_inv_rect_Type2 :
934    abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
935    __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
936    trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
937    __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
938    -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
939let trace_any_call_inv_rect_Type2 x1 x2 x3 hterm h1 h2 h3 =
940  let hcut = trace_any_call_rect_Type2 x1 h1 h2 h3 x2 x3 hterm in
941  hcut __ __ __
942
943(** val trace_any_call_inv_rect_Type1 :
944    abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
945    __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
946    trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
947    __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
948    -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
949let trace_any_call_inv_rect_Type1 x1 x2 x3 hterm h1 h2 h3 =
950  let hcut = trace_any_call_rect_Type1 x1 h1 h2 h3 x2 x3 hterm in
951  hcut __ __ __
952
953(** val trace_any_call_inv_rect_Type0 :
954    abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
955    __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
956    trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
957    __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
958    -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
959let trace_any_call_inv_rect_Type0 x1 x2 x3 hterm h1 h2 h3 =
960  let hcut = trace_any_call_rect_Type0 x1 h1 h2 h3 x2 x3 hterm in
961  hcut __ __ __
962
963(** val trace_any_call_jmdiscr :
964    abstract_status -> __ -> __ -> trace_any_call -> trace_any_call -> __ **)
965let trace_any_call_jmdiscr a1 a2 a3 x y =
966  Logic.eq_rect_Type2 x
967    (match x with
968     | Tac_base a0 -> Obj.magic (fun _ dH -> dH __ __)
969     | Tac_step_call (a0, a10, a20, a30, a7, a9) ->
970       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)
971     | Tac_step_default (a0, a10, a20, a4) ->
972       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
973
974type trace_label_call =
975| Tlc_base of __ * __ * trace_any_call
976
977(** val trace_label_call_rect_Type4 :
978    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
979    -> trace_label_call -> 'a1 **)
980let rec trace_label_call_rect_Type4 s h_tlc_base x_367 x_366 = function
981| Tlc_base (start_status, end_status, x_370) ->
982  h_tlc_base start_status end_status x_370 __
983
984(** val trace_label_call_rect_Type5 :
985    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
986    -> trace_label_call -> 'a1 **)
987let rec trace_label_call_rect_Type5 s h_tlc_base x_373 x_372 = function
988| Tlc_base (start_status, end_status, x_376) ->
989  h_tlc_base start_status end_status x_376 __
990
991(** val trace_label_call_rect_Type3 :
992    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
993    -> trace_label_call -> 'a1 **)
994let rec trace_label_call_rect_Type3 s h_tlc_base x_379 x_378 = function
995| Tlc_base (start_status, end_status, x_382) ->
996  h_tlc_base start_status end_status x_382 __
997
998(** val trace_label_call_rect_Type2 :
999    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
1000    -> trace_label_call -> 'a1 **)
1001let rec trace_label_call_rect_Type2 s h_tlc_base x_385 x_384 = function
1002| Tlc_base (start_status, end_status, x_388) ->
1003  h_tlc_base start_status end_status x_388 __
1004
1005(** val trace_label_call_rect_Type1 :
1006    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
1007    -> trace_label_call -> 'a1 **)
1008let rec trace_label_call_rect_Type1 s h_tlc_base x_391 x_390 = function
1009| Tlc_base (start_status, end_status, x_394) ->
1010  h_tlc_base start_status end_status x_394 __
1011
1012(** val trace_label_call_rect_Type0 :
1013    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
1014    -> trace_label_call -> 'a1 **)
1015let rec trace_label_call_rect_Type0 s h_tlc_base x_397 x_396 = function
1016| Tlc_base (start_status, end_status, x_400) ->
1017  h_tlc_base start_status end_status x_400 __
1018
1019(** val trace_label_call_inv_rect_Type4 :
1020    abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1021    trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1022let trace_label_call_inv_rect_Type4 x1 x2 x3 hterm h1 =
1023  let hcut = trace_label_call_rect_Type4 x1 h1 x2 x3 hterm in hcut __ __ __
1024
1025(** val trace_label_call_inv_rect_Type3 :
1026    abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1027    trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1028let trace_label_call_inv_rect_Type3 x1 x2 x3 hterm h1 =
1029  let hcut = trace_label_call_rect_Type3 x1 h1 x2 x3 hterm in hcut __ __ __
1030
1031(** val trace_label_call_inv_rect_Type2 :
1032    abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1033    trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1034let trace_label_call_inv_rect_Type2 x1 x2 x3 hterm h1 =
1035  let hcut = trace_label_call_rect_Type2 x1 h1 x2 x3 hterm in hcut __ __ __
1036
1037(** val trace_label_call_inv_rect_Type1 :
1038    abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1039    trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1040let trace_label_call_inv_rect_Type1 x1 x2 x3 hterm h1 =
1041  let hcut = trace_label_call_rect_Type1 x1 h1 x2 x3 hterm in hcut __ __ __
1042
1043(** val trace_label_call_inv_rect_Type0 :
1044    abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1045    trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1046let trace_label_call_inv_rect_Type0 x1 x2 x3 hterm h1 =
1047  let hcut = trace_label_call_rect_Type0 x1 h1 x2 x3 hterm in hcut __ __ __
1048
1049(** val trace_label_call_discr :
1050    abstract_status -> __ -> __ -> trace_label_call -> trace_label_call -> __ **)
1051let trace_label_call_discr a1 a2 a3 x y =
1052  Logic.eq_rect_Type2 x
1053    (let Tlc_base (a0, a10, a20) = x in
1054    Obj.magic (fun _ dH -> dH __ __ __ __)) y
1055
1056(** val trace_label_call_jmdiscr :
1057    abstract_status -> __ -> __ -> trace_label_call -> trace_label_call -> __ **)
1058let trace_label_call_jmdiscr a1 a2 a3 x y =
1059  Logic.eq_rect_Type2 x
1060    (let Tlc_base (a0, a10, a20) = x in
1061    Obj.magic (fun _ dH -> dH __ __ __ __)) y
1062
1063(** val tlc_hd_label :
1064    abstract_status -> __ -> __ -> trace_label_call -> CostLabel.costlabel **)
1065let tlc_hd_label s st1 st2 tr =
1066  (let Tlc_base (st1', x, x0) = tr in
1067  (fun _ _ _ -> Types.pi1 (as_label_safe s st1'))) __ __ __
1068
1069type trace_label_diverges = __trace_label_diverges Lazy.t
1070and __trace_label_diverges =
1071| Tld_step of __ * __ * trace_label_label * trace_label_diverges
1072| Tld_base of __ * __ * __ * trace_label_call * trace_label_diverges
1073
1074(** val trace_label_diverges_inv_rect_Type4 :
1075    abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1076    trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1077    __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1078    __ -> 'a1) -> 'a1 **)
1079let trace_label_diverges_inv_rect_Type4 x1 x2 hterm h1 h2 =
1080  let hcut =
1081    match Lazy.force
1082    hterm with
1083    | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1084    | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1085  in
1086  hcut __ __
1087
1088(** val trace_label_diverges_inv_rect_Type3 :
1089    abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1090    trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1091    __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1092    __ -> 'a1) -> 'a1 **)
1093let trace_label_diverges_inv_rect_Type3 x1 x2 hterm h1 h2 =
1094  let hcut =
1095    match Lazy.force
1096    hterm with
1097    | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1098    | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1099  in
1100  hcut __ __
1101
1102(** val trace_label_diverges_inv_rect_Type2 :
1103    abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1104    trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1105    __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1106    __ -> 'a1) -> 'a1 **)
1107let trace_label_diverges_inv_rect_Type2 x1 x2 hterm h1 h2 =
1108  let hcut =
1109    match Lazy.force
1110    hterm with
1111    | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1112    | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1113  in
1114  hcut __ __
1115
1116(** val trace_label_diverges_inv_rect_Type1 :
1117    abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1118    trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1119    __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1120    __ -> 'a1) -> 'a1 **)
1121let trace_label_diverges_inv_rect_Type1 x1 x2 hterm h1 h2 =
1122  let hcut =
1123    match Lazy.force
1124    hterm with
1125    | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1126    | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1127  in
1128  hcut __ __
1129
1130(** val trace_label_diverges_inv_rect_Type0 :
1131    abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1132    trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1133    __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1134    __ -> 'a1) -> 'a1 **)
1135let trace_label_diverges_inv_rect_Type0 x1 x2 hterm h1 h2 =
1136  let hcut =
1137    match Lazy.force
1138    hterm with
1139    | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1140    | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1141  in
1142  hcut __ __
1143
1144(** val trace_label_diverges_jmdiscr :
1145    abstract_status -> __ -> trace_label_diverges -> trace_label_diverges ->
1146    __ **)
1147let trace_label_diverges_jmdiscr a1 a2 x y =
1148  Logic.eq_rect_Type2 x
1149    (match Lazy.force
1150     x with
1151     | Tld_step (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1152     | Tld_base (a0, a10, a20, a3, a6) ->
1153       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
1154
1155(** val tld_hd_label :
1156    abstract_status -> __ -> trace_label_diverges -> CostLabel.costlabel **)
1157let tld_hd_label s st tr =
1158  match Lazy.force
1159  tr with
1160  | Tld_step (st', st'', tll, x) ->
1161    tll_hd_label s Doesnt_end_with_ret st' st'' tll
1162  | Tld_base (st', st'', x, tlc, x2) -> tlc_hd_label s st' st'' tlc
1163
1164type trace_whole_program =
1165| Twp_terminating of __ * __ * __ * trace_label_return
1166| Twp_diverges of __ * __ * trace_label_diverges
1167
1168(** val trace_whole_program_rect_Type4 :
1169    abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1170    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1171    -> trace_whole_program -> 'a1 **)
1172let rec trace_whole_program_rect_Type4 s h_twp_terminating h_twp_diverges x_449 = function
1173| Twp_terminating (status_initial, status_start_fun, status_final, x_452) ->
1174  h_twp_terminating status_initial status_start_fun status_final __ __ x_452
1175    __
1176| Twp_diverges (status_initial, status_start_fun, x_455) ->
1177  h_twp_diverges status_initial status_start_fun __ __ x_455
1178
1179(** val trace_whole_program_rect_Type5 :
1180    abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1181    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1182    -> trace_whole_program -> 'a1 **)
1183let rec trace_whole_program_rect_Type5 s h_twp_terminating h_twp_diverges x_460 = function
1184| Twp_terminating (status_initial, status_start_fun, status_final, x_463) ->
1185  h_twp_terminating status_initial status_start_fun status_final __ __ x_463
1186    __
1187| Twp_diverges (status_initial, status_start_fun, x_466) ->
1188  h_twp_diverges status_initial status_start_fun __ __ x_466
1189
1190(** val trace_whole_program_rect_Type3 :
1191    abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1192    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1193    -> trace_whole_program -> 'a1 **)
1194let rec trace_whole_program_rect_Type3 s h_twp_terminating h_twp_diverges x_471 = function
1195| Twp_terminating (status_initial, status_start_fun, status_final, x_474) ->
1196  h_twp_terminating status_initial status_start_fun status_final __ __ x_474
1197    __
1198| Twp_diverges (status_initial, status_start_fun, x_477) ->
1199  h_twp_diverges status_initial status_start_fun __ __ x_477
1200
1201(** val trace_whole_program_rect_Type2 :
1202    abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1203    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1204    -> trace_whole_program -> 'a1 **)
1205let rec trace_whole_program_rect_Type2 s h_twp_terminating h_twp_diverges x_482 = function
1206| Twp_terminating (status_initial, status_start_fun, status_final, x_485) ->
1207  h_twp_terminating status_initial status_start_fun status_final __ __ x_485
1208    __
1209| Twp_diverges (status_initial, status_start_fun, x_488) ->
1210  h_twp_diverges status_initial status_start_fun __ __ x_488
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_493 = function
1217| Twp_terminating (status_initial, status_start_fun, status_final, x_496) ->
1218  h_twp_terminating status_initial status_start_fun status_final __ __ x_496
1219    __
1220| Twp_diverges (status_initial, status_start_fun, x_499) ->
1221  h_twp_diverges status_initial status_start_fun __ __ x_499
1222
1223(** val trace_whole_program_rect_Type0 :
1224    abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1225    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1226    -> trace_whole_program -> 'a1 **)
1227let rec trace_whole_program_rect_Type0 s h_twp_terminating h_twp_diverges x_504 = function
1228| Twp_terminating (status_initial, status_start_fun, status_final, x_507) ->
1229  h_twp_terminating status_initial status_start_fun status_final __ __ x_507
1230    __
1231| Twp_diverges (status_initial, status_start_fun, x_510) ->
1232  h_twp_diverges status_initial status_start_fun __ __ x_510
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  Types.pi1 (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  Types.pi1 (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_734 x_733 = function
1297| Taa_base st -> h_taa_base st
1298| Taa_step (st1, st2, st3, x_736) ->
1299  h_taa_step st1 st2 st3 __ __ __ x_736
1300    (trace_any_any_rect_Type4 s h_taa_base h_taa_step st2 st3 x_736)
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_752 x_751 = function
1306| Taa_base st -> h_taa_base st
1307| Taa_step (st1, st2, st3, x_754) ->
1308  h_taa_step st1 st2 st3 __ __ __ x_754
1309    (trace_any_any_rect_Type3 s h_taa_base h_taa_step st2 st3 x_754)
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_761 x_760 = function
1315| Taa_base st -> h_taa_base st
1316| Taa_step (st1, st2, st3, x_763) ->
1317  h_taa_step st1 st2 st3 __ __ __ x_763
1318    (trace_any_any_rect_Type2 s h_taa_base h_taa_step st2 st3 x_763)
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_770 x_769 = function
1324| Taa_base st -> h_taa_base st
1325| Taa_step (st1, st2, st3, x_772) ->
1326  h_taa_step st1 st2 st3 __ __ __ x_772
1327    (trace_any_any_rect_Type1 s h_taa_base h_taa_step st2 st3 x_772)
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_779 x_778 = function
1333| Taa_base st -> h_taa_base st
1334| Taa_step (st1, st2, st3, x_781) ->
1335  h_taa_step st1 st2 st3 __ __ __ x_781
1336    (trace_any_any_rect_Type0 s h_taa_base h_taa_step st2 st3 x_781)
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 intensional_event =
1443| IEVcost of CostLabel.costlabel
1444| IEVcall of AST.ident
1445| IEVtailcall of AST.ident * AST.ident
1446| IEVret of AST.ident
1447
1448(** val intensional_event_rect_Type4 :
1449    (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1450    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1451let rec intensional_event_rect_Type4 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
1452| IEVcost x_852 -> h_IEVcost x_852
1453| IEVcall x_853 -> h_IEVcall x_853
1454| IEVtailcall (x_855, x_854) -> h_IEVtailcall x_855 x_854
1455| IEVret x_856 -> h_IEVret x_856
1456
1457(** val intensional_event_rect_Type5 :
1458    (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1459    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1460let rec intensional_event_rect_Type5 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
1461| IEVcost x_862 -> h_IEVcost x_862
1462| IEVcall x_863 -> h_IEVcall x_863
1463| IEVtailcall (x_865, x_864) -> h_IEVtailcall x_865 x_864
1464| IEVret x_866 -> h_IEVret x_866
1465
1466(** val intensional_event_rect_Type3 :
1467    (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1468    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1469let rec intensional_event_rect_Type3 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
1470| IEVcost x_872 -> h_IEVcost x_872
1471| IEVcall x_873 -> h_IEVcall x_873
1472| IEVtailcall (x_875, x_874) -> h_IEVtailcall x_875 x_874
1473| IEVret x_876 -> h_IEVret x_876
1474
1475(** val intensional_event_rect_Type2 :
1476    (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1477    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1478let rec intensional_event_rect_Type2 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
1479| IEVcost x_882 -> h_IEVcost x_882
1480| IEVcall x_883 -> h_IEVcall x_883
1481| IEVtailcall (x_885, x_884) -> h_IEVtailcall x_885 x_884
1482| IEVret x_886 -> h_IEVret x_886
1483
1484(** val intensional_event_rect_Type1 :
1485    (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1486    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1487let rec intensional_event_rect_Type1 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
1488| IEVcost x_892 -> h_IEVcost x_892
1489| IEVcall x_893 -> h_IEVcall x_893
1490| IEVtailcall (x_895, x_894) -> h_IEVtailcall x_895 x_894
1491| IEVret x_896 -> h_IEVret x_896
1492
1493(** val intensional_event_rect_Type0 :
1494    (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1495    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1496let rec intensional_event_rect_Type0 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
1497| IEVcost x_902 -> h_IEVcost x_902
1498| IEVcall x_903 -> h_IEVcall x_903
1499| IEVtailcall (x_905, x_904) -> h_IEVtailcall x_905 x_904
1500| IEVret x_906 -> h_IEVret x_906
1501
1502(** val intensional_event_inv_rect_Type4 :
1503    intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident ->
1504    __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __
1505    -> 'a1) -> 'a1 **)
1506let intensional_event_inv_rect_Type4 hterm h1 h2 h3 h4 =
1507  let hcut = intensional_event_rect_Type4 h1 h2 h3 h4 hterm in hcut __
1508
1509(** val intensional_event_inv_rect_Type3 :
1510    intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident ->
1511    __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __
1512    -> 'a1) -> 'a1 **)
1513let intensional_event_inv_rect_Type3 hterm h1 h2 h3 h4 =
1514  let hcut = intensional_event_rect_Type3 h1 h2 h3 h4 hterm in hcut __
1515
1516(** val intensional_event_inv_rect_Type2 :
1517    intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident ->
1518    __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __
1519    -> 'a1) -> 'a1 **)
1520let intensional_event_inv_rect_Type2 hterm h1 h2 h3 h4 =
1521  let hcut = intensional_event_rect_Type2 h1 h2 h3 h4 hterm in hcut __
1522
1523(** val intensional_event_inv_rect_Type1 :
1524    intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident ->
1525    __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __
1526    -> 'a1) -> 'a1 **)
1527let intensional_event_inv_rect_Type1 hterm h1 h2 h3 h4 =
1528  let hcut = intensional_event_rect_Type1 h1 h2 h3 h4 hterm in hcut __
1529
1530(** val intensional_event_inv_rect_Type0 :
1531    intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident ->
1532    __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __
1533    -> 'a1) -> 'a1 **)
1534let intensional_event_inv_rect_Type0 hterm h1 h2 h3 h4 =
1535  let hcut = intensional_event_rect_Type0 h1 h2 h3 h4 hterm in hcut __
1536
1537(** val intensional_event_discr :
1538    intensional_event -> intensional_event -> __ **)
1539let intensional_event_discr x y =
1540  Logic.eq_rect_Type2 x
1541    (match x with
1542     | IEVcost a0 -> Obj.magic (fun _ dH -> dH __)
1543     | IEVcall a0 -> Obj.magic (fun _ dH -> dH __)
1544     | IEVtailcall (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1545     | IEVret a0 -> Obj.magic (fun _ dH -> dH __)) y
1546
1547(** val intensional_event_jmdiscr :
1548    intensional_event -> intensional_event -> __ **)
1549let intensional_event_jmdiscr x y =
1550  Logic.eq_rect_Type2 x
1551    (match x with
1552     | IEVcost a0 -> Obj.magic (fun _ dH -> dH __)
1553     | IEVcall a0 -> Obj.magic (fun _ dH -> dH __)
1554     | IEVtailcall (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1555     | IEVret a0 -> Obj.magic (fun _ dH -> dH __)) y
1556
1557type as_trace = intensional_event List.list Types.sig0
1558
1559(** val cons_safe :
1560    'a1 Types.sig0 -> 'a1 List.list Types.sig0 -> 'a1 List.list Types.sig0 **)
1561let cons_safe x l =
1562  List.Cons ((Types.pi1 x), (Types.pi1 l))
1563
1564(** val append_safe :
1565    'a1 List.list Types.sig0 -> 'a1 List.list Types.sig0 -> 'a1 List.list
1566    Types.sig0 **)
1567let append_safe l1 l2 =
1568  List.append (Types.pi1 l1) (Types.pi1 l2)
1569
1570(** val nil_safe : 'a1 List.list Types.sig0 **)
1571let nil_safe =
1572  List.Nil
1573
1574(** val emittable_cost :
1575    abstract_status -> as_cost_label -> intensional_event Types.sig0 **)
1576let emittable_cost s l =
1577  IEVcost (Types.pi1 l)
1578
1579(** val observables_trace_label_label :
1580    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
1581    -> AST.ident -> as_trace **)
1582let rec observables_trace_label_label s trace_ends_flag start_status final_status the_trace curr =
1583  let Tll_base (ends_flag, initial, final, given_trace) = the_trace in
1584  let label = as_label_safe s initial in
1585  cons_safe (emittable_cost s label)
1586    (observables_trace_any_label s ends_flag initial final given_trace curr)
1587(** val observables_trace_any_label :
1588    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
1589    AST.ident -> as_trace **)
1590and observables_trace_any_label s trace_ends_flag start_status final_status the_trace curr =
1591  match the_trace with
1592  | Tal_base_not_return (the_status, x) -> nil_safe
1593  | Tal_base_return (the_status, x) -> cons_safe (IEVret curr) nil_safe
1594  | Tal_base_call (pre_fun_call, start_fun_call, final, call_trace) ->
1595    let id = s.as_call_ident pre_fun_call in
1596    cons_safe (IEVcall id)
1597      (observables_trace_label_return s start_fun_call final call_trace id)
1598  | Tal_base_tailcall (pre_fun_call, start_fun_call, final, call_trace) ->
1599    let id = s.as_tailcall_ident pre_fun_call in
1600    cons_safe (IEVtailcall (curr, id))
1601      (observables_trace_label_return s start_fun_call final call_trace id)
1602  | Tal_step_call
1603      (end_flag, pre_fun_call, start_fun_call, after_fun_call, final,
1604       call_trace, final_trace) ->
1605    let id = s.as_call_ident pre_fun_call in
1606    let call_cost_trace =
1607      observables_trace_label_return s start_fun_call after_fun_call
1608        call_trace id
1609    in
1610    let final_cost_trace =
1611      observables_trace_any_label s end_flag after_fun_call final final_trace
1612        curr
1613    in
1614    append_safe (cons_safe (IEVcall id) call_cost_trace) final_cost_trace
1615  | Tal_step_default
1616      (end_flag, status_pre, status_init, status_end, tail_trace) ->
1617    observables_trace_any_label s end_flag status_init status_end tail_trace
1618      curr
1619(** val observables_trace_label_return :
1620    abstract_status -> __ -> __ -> trace_label_return -> AST.ident ->
1621    as_trace **)
1622and observables_trace_label_return s start_status final_status the_trace curr =
1623  match the_trace with
1624  | Tlr_base (before, after, trace_to_lift) ->
1625    observables_trace_label_label s Ends_with_ret before after trace_to_lift
1626      curr
1627  | Tlr_step (initial, labelled, final, labelled_trace, ret_trace) ->
1628    let labelled_cost =
1629      observables_trace_label_label s Doesnt_end_with_ret initial labelled
1630        labelled_trace curr
1631    in
1632    let return_cost =
1633      observables_trace_label_return s labelled final ret_trace curr
1634    in
1635    append_safe labelled_cost return_cost
1636
1637(** val filter_map :
1638    ('a1 -> 'a2 Types.option) -> 'a1 List.list -> 'a2 List.list **)
1639let rec filter_map f = function
1640| List.Nil -> List.Nil
1641| List.Cons (hd, tl) ->
1642  List.append
1643    (match f hd with
1644     | Types.None -> List.Nil
1645     | Types.Some y -> List.Cons (y, List.Nil)) (filter_map f tl)
1646
1647(** val list_distribute_sig_aux :
1648    'a1 List.list -> 'a1 Types.sig0 List.list **)
1649let rec list_distribute_sig_aux l =
1650  (match l with
1651   | List.Nil -> (fun _ -> List.Nil)
1652   | List.Cons (hd, tl) ->
1653     (fun _ -> List.Cons (hd, (list_distribute_sig_aux tl)))) __
1654
1655(** val list_distribute_sig :
1656    'a1 List.list Types.sig0 -> 'a1 Types.sig0 List.list **)
1657let list_distribute_sig l =
1658  list_distribute_sig_aux (Types.pi1 l)
1659
1660(** val list_factor_sig :
1661    'a1 Types.sig0 List.list -> 'a1 List.list Types.sig0 **)
1662let rec list_factor_sig = function
1663| List.Nil -> nil_safe
1664| List.Cons (hd, tl) -> cons_safe hd (list_factor_sig tl)
1665
1666(** val costlabels_of_observables :
1667    abstract_status -> as_trace -> as_cost_label List.list **)
1668let costlabels_of_observables s l =
1669  filter_map (fun ev ->
1670    (match Types.pi1 ev with
1671     | IEVcost c -> (fun _ -> Types.Some c)
1672     | IEVcall x -> (fun _ -> Types.None)
1673     | IEVtailcall (x, x0) -> (fun _ -> Types.None)
1674     | IEVret x -> (fun _ -> Types.None)) __) (list_distribute_sig l)
1675
1676(** val flatten_trace_label_return :
1677    abstract_status -> __ -> __ -> trace_label_return -> as_cost_label
1678    List.list **)
1679let flatten_trace_label_return s st1 st2 tlr =
1680  let dummy = Positive.One in
1681  costlabels_of_observables s
1682    (observables_trace_label_return s st1 st2 tlr dummy)
1683
1684(** val flatten_trace_label_label :
1685    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
1686    -> as_cost_label List.list **)
1687let flatten_trace_label_label s flag st1 st2 tll =
1688  let dummy = Positive.One in
1689  costlabels_of_observables s
1690    (observables_trace_label_label s flag st1 st2 tll dummy)
1691
1692(** val flatten_trace_any_label :
1693    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
1694    as_cost_label List.list **)
1695let flatten_trace_any_label s flag st1 st2 tll =
1696  let dummy = Positive.One in
1697  costlabels_of_observables s
1698    (observables_trace_any_label s flag st1 st2 tll dummy)
1699
1700type trace_any_any_free =
1701| Taaf_base of __
1702| Taaf_step of __ * __ * __ * trace_any_any
1703| Taaf_step_jump of __ * __ * __ * trace_any_any
1704
1705(** val trace_any_any_free_rect_Type4 :
1706    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1707    -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1708    'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1709let rec trace_any_any_free_rect_Type4 s h_taaf_base h_taaf_step h_taaf_step_jump x_985 x_984 = function
1710| Taaf_base s0 -> h_taaf_base s0
1711| Taaf_step (s1, s2, s3, x_989) -> h_taaf_step s1 s2 s3 x_989 __ __
1712| Taaf_step_jump (s1, s2, s3, x_993) ->
1713  h_taaf_step_jump s1 s2 s3 x_993 __ __ __
1714
1715(** val trace_any_any_free_rect_Type5 :
1716    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1717    -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1718    'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1719let rec trace_any_any_free_rect_Type5 s h_taaf_base h_taaf_step h_taaf_step_jump x_998 x_997 = function
1720| Taaf_base s0 -> h_taaf_base s0
1721| Taaf_step (s1, s2, s3, x_1002) -> h_taaf_step s1 s2 s3 x_1002 __ __
1722| Taaf_step_jump (s1, s2, s3, x_1006) ->
1723  h_taaf_step_jump s1 s2 s3 x_1006 __ __ __
1724
1725(** val trace_any_any_free_rect_Type3 :
1726    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1727    -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1728    'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1729let rec trace_any_any_free_rect_Type3 s h_taaf_base h_taaf_step h_taaf_step_jump x_1011 x_1010 = function
1730| Taaf_base s0 -> h_taaf_base s0
1731| Taaf_step (s1, s2, s3, x_1015) -> h_taaf_step s1 s2 s3 x_1015 __ __
1732| Taaf_step_jump (s1, s2, s3, x_1019) ->
1733  h_taaf_step_jump s1 s2 s3 x_1019 __ __ __
1734
1735(** val trace_any_any_free_rect_Type2 :
1736    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1737    -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1738    'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1739let rec trace_any_any_free_rect_Type2 s h_taaf_base h_taaf_step h_taaf_step_jump x_1024 x_1023 = function
1740| Taaf_base s0 -> h_taaf_base s0
1741| Taaf_step (s1, s2, s3, x_1028) -> h_taaf_step s1 s2 s3 x_1028 __ __
1742| Taaf_step_jump (s1, s2, s3, x_1032) ->
1743  h_taaf_step_jump s1 s2 s3 x_1032 __ __ __
1744
1745(** val trace_any_any_free_rect_Type1 :
1746    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1747    -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1748    'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1749let rec trace_any_any_free_rect_Type1 s h_taaf_base h_taaf_step h_taaf_step_jump x_1037 x_1036 = function
1750| Taaf_base s0 -> h_taaf_base s0
1751| Taaf_step (s1, s2, s3, x_1041) -> h_taaf_step s1 s2 s3 x_1041 __ __
1752| Taaf_step_jump (s1, s2, s3, x_1045) ->
1753  h_taaf_step_jump s1 s2 s3 x_1045 __ __ __
1754
1755(** val trace_any_any_free_rect_Type0 :
1756    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1757    -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1758    'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1759let rec trace_any_any_free_rect_Type0 s h_taaf_base h_taaf_step h_taaf_step_jump x_1050 x_1049 = function
1760| Taaf_base s0 -> h_taaf_base s0
1761| Taaf_step (s1, s2, s3, x_1054) -> h_taaf_step s1 s2 s3 x_1054 __ __
1762| Taaf_step_jump (s1, s2, s3, x_1058) ->
1763  h_taaf_step_jump s1 s2 s3 x_1058 __ __ __
1764
1765(** val trace_any_any_free_inv_rect_Type4 :
1766    abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
1767    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1768    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1769    __ -> __ -> 'a1) -> 'a1 **)
1770let trace_any_any_free_inv_rect_Type4 x1 x2 x3 hterm h1 h2 h3 =
1771  let hcut = trace_any_any_free_rect_Type4 x1 h1 h2 h3 x2 x3 hterm in
1772  hcut __ __ __
1773
1774(** val trace_any_any_free_inv_rect_Type3 :
1775    abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
1776    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1777    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1778    __ -> __ -> 'a1) -> 'a1 **)
1779let trace_any_any_free_inv_rect_Type3 x1 x2 x3 hterm h1 h2 h3 =
1780  let hcut = trace_any_any_free_rect_Type3 x1 h1 h2 h3 x2 x3 hterm in
1781  hcut __ __ __
1782
1783(** val trace_any_any_free_inv_rect_Type2 :
1784    abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
1785    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1786    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1787    __ -> __ -> 'a1) -> 'a1 **)
1788let trace_any_any_free_inv_rect_Type2 x1 x2 x3 hterm h1 h2 h3 =
1789  let hcut = trace_any_any_free_rect_Type2 x1 h1 h2 h3 x2 x3 hterm in
1790  hcut __ __ __
1791
1792(** val trace_any_any_free_inv_rect_Type1 :
1793    abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
1794    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1795    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1796    __ -> __ -> 'a1) -> 'a1 **)
1797let trace_any_any_free_inv_rect_Type1 x1 x2 x3 hterm h1 h2 h3 =
1798  let hcut = trace_any_any_free_rect_Type1 x1 h1 h2 h3 x2 x3 hterm in
1799  hcut __ __ __
1800
1801(** val trace_any_any_free_inv_rect_Type0 :
1802    abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
1803    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1804    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1805    __ -> __ -> 'a1) -> 'a1 **)
1806let trace_any_any_free_inv_rect_Type0 x1 x2 x3 hterm h1 h2 h3 =
1807  let hcut = trace_any_any_free_rect_Type0 x1 h1 h2 h3 x2 x3 hterm in
1808  hcut __ __ __
1809
1810(** val trace_any_any_free_jmdiscr :
1811    abstract_status -> __ -> __ -> trace_any_any_free -> trace_any_any_free
1812    -> __ **)
1813let trace_any_any_free_jmdiscr a1 a2 a3 x y =
1814  Logic.eq_rect_Type2 x
1815    (match x with
1816     | Taaf_base a0 -> Obj.magic (fun _ dH -> dH __)
1817     | Taaf_step (a0, a10, a20, a30) ->
1818       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
1819     | Taaf_step_jump (a0, a10, a20, a30) ->
1820       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
1821
1822(** val taaf_non_empty :
1823    abstract_status -> __ -> __ -> trace_any_any_free -> Bool.bool **)
1824let taaf_non_empty s s1 s2 = function
1825| Taaf_base x -> Bool.False
1826| Taaf_step (x, x0, x1, x2) -> Bool.True
1827| Taaf_step_jump (x, x0, x1, x2) -> Bool.True
1828
1829(** val taa_append_taa :
1830    abstract_status -> __ -> __ -> __ -> trace_any_any -> trace_any_any ->
1831    trace_any_any **)
1832let rec taa_append_taa s st1 st2 st3 taa =
1833  (match taa with
1834   | Taa_base st1' -> (fun st30 taa2 -> taa2)
1835   | Taa_step (st1', st2', st3', tl) ->
1836     (fun st30 taa2 -> Taa_step (st1', st2', st30,
1837       (taa_append_taa s st2' st3' st30 tl taa2)))) st3
1838
1839(** val taaf_to_taa :
1840    abstract_status -> __ -> __ -> trace_any_any_free -> trace_any_any **)
1841let taaf_to_taa s s1 s2 taaf =
1842  (match taaf with
1843   | Taaf_base s0 -> (fun _ -> Taa_base s0)
1844   | Taaf_step (s10, s20, s3, taa) ->
1845     (fun _ ->
1846       taa_append_taa s s10 s20 s3 taa (Taa_step (s20, s3, s3, (Taa_base
1847         s3))))
1848   | Taaf_step_jump (s10, s20, s3, taa) ->
1849     (fun _ -> assert false (* absurd case *))) __
1850
1851(** val taaf_append_tal :
1852    abstract_status -> __ -> trace_ends_with_ret -> __ -> __ ->
1853    trace_any_any_free -> trace_any_label -> trace_any_label **)
1854let taaf_append_tal s st1 fl st2 st3 taaf =
1855  taa_append_tal s st1 fl st2 st3 (taaf_to_taa s st1 st2 taaf)
1856
1857(** val taaf_append_taa :
1858    abstract_status -> __ -> __ -> __ -> trace_any_any_free -> trace_any_any
1859    -> trace_any_any **)
1860let taaf_append_taa s st1 st2 st3 taaf =
1861  taa_append_taa s st1 st2 st3 (taaf_to_taa s st1 st2 taaf)
1862
1863(** val taaf_cons :
1864    abstract_status -> __ -> __ -> __ -> trace_any_any_free ->
1865    trace_any_any_free **)
1866let taaf_cons s s1 s2 s3 tl =
1867  (match tl with
1868   | Taaf_base s20 -> (fun _ _ -> Taaf_step (s1, s1, s20, (Taa_base s1)))
1869   | Taaf_step (s20, s30, s4, taa) ->
1870     (fun _ _ -> Taaf_step (s1, s30, s4, (Taa_step (s1, s20, s30, taa))))
1871   | Taaf_step_jump (s20, s30, s4, taa) ->
1872     (fun _ _ -> Taaf_step_jump (s1, s30, s4, (Taa_step (s1, s20, s30,
1873       taa))))) __ __
1874
1875(** val taaf_append_taaf :
1876    abstract_status -> __ -> __ -> __ -> trace_any_any_free ->
1877    trace_any_any_free -> trace_any_any_free **)
1878let taaf_append_taaf s st1 st2 st3 taaf1 taaf2 =
1879  (match taaf2 with
1880   | Taaf_base s1 -> (fun taaf10 _ -> taaf10)
1881   | Taaf_step (s1, s2, s3, taa) ->
1882     (fun taaf10 _ -> Taaf_step (st1, s2, s3,
1883       (taaf_append_taa s st1 s1 s2 taaf10 taa)))
1884   | Taaf_step_jump (s2, s3, s4, taa) ->
1885     (fun taaf10 _ -> Taaf_step_jump (st1, s3, s4,
1886       (taaf_append_taa s st1 s2 s3 taaf10 taa)))) taaf1 __
1887
Note: See TracBrowser for help on using the repository browser.