source: extracted/structuredTraces.ml @ 2960

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File size: 80.4 KB
RevLine 
[2601]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
[2649]23open ErrorMessages
24
[2601]25open PreIdentifiers
26
27open Errors
28
29open Extralib
30
31open Setoids
32
33open Monad
34
35open Option
36
[2773]37open Div_and_mod
38
39open Russell
40
41open Util
42
43open List
44
[2601]45open Lists
46
[2773]47open Nat
48
[2601]49open Positive
50
[2773]51open Types
52
[2601]53open Identifiers
54
[2773]55open CostLabel
[2717]56
[2773]57open Sets
[2601]58
[2773]59open Listb
[2601]60
[2773]61open Integers
[2601]62
[2773]63open AST
[2601]64
[2773]65open Division
[2601]66
[2773]67open Exp
[2601]68
[2773]69open Arithmetic
70
71open Extranat
72
73open Vector
74
[2601]75open FoldStuff
76
77open BitVector
78
[2773]79open Z
[2601]80
[2773]81open BitVectorZ
[2601]82
[2773]83open Pointers
[2601]84
[2773]85open Coqlib
[2601]86
[2773]87open Values
[2601]88
[2773]89open Events
[2601]90
[2773]91open IOMonad
[2601]92
[2773]93open IO
94
95open Hide
96
[2601]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 : (__ -> __);
[2773]209                         as_classify : (__ -> status_class);
[2601]210                         as_label_of_pc : (__ -> CostLabel.costlabel
211                                          Types.option);
[2773]212                         as_result : (__ -> Integers.int Types.option);
[2601]213                         as_call_ident : (__ Types.sig0 -> AST.ident);
214                         as_tailcall_ident : (__ Types.sig0 -> AST.ident) }
215
216(** val abstract_status_rect_Type4 :
[2773]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 **)
[2951]221let rec abstract_status_rect_Type4 h_mk_abstract_status x_3280 =
[2601]222  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
[2773]223    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
[2951]224    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_3280
[2601]225  in
226  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
[2773]227    as_result0 as_call_ident0 as_tailcall_ident0
[2601]228
229(** val abstract_status_rect_Type5 :
[2773]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 **)
[2951]234let rec abstract_status_rect_Type5 h_mk_abstract_status x_3282 =
[2601]235  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
[2773]236    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
[2951]237    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_3282
[2601]238  in
239  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
[2773]240    as_result0 as_call_ident0 as_tailcall_ident0
[2601]241
242(** val abstract_status_rect_Type3 :
[2773]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 **)
[2951]247let rec abstract_status_rect_Type3 h_mk_abstract_status x_3284 =
[2601]248  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
[2773]249    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
[2951]250    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_3284
[2601]251  in
252  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
[2773]253    as_result0 as_call_ident0 as_tailcall_ident0
[2601]254
255(** val abstract_status_rect_Type2 :
[2773]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 **)
[2951]260let rec abstract_status_rect_Type2 h_mk_abstract_status x_3286 =
[2601]261  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
[2773]262    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
[2951]263    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_3286
[2601]264  in
265  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
[2773]266    as_result0 as_call_ident0 as_tailcall_ident0
[2601]267
268(** val abstract_status_rect_Type1 :
[2773]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 **)
[2951]273let rec abstract_status_rect_Type1 h_mk_abstract_status x_3288 =
[2601]274  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
[2773]275    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
[2951]276    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_3288
[2601]277  in
278  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
[2773]279    as_result0 as_call_ident0 as_tailcall_ident0
[2601]280
281(** val abstract_status_rect_Type0 :
[2773]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 **)
[2951]286let rec abstract_status_rect_Type0 h_mk_abstract_status x_3290 =
[2601]287  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
[2773]288    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
[2951]289    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_3290
[2601]290  in
291  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
[2773]292    as_result0 as_call_ident0 as_tailcall_ident0
[2601]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
[2773]304(** val as_classify : abstract_status -> __ -> status_class **)
[2601]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
[2773]313(** val as_result : abstract_status -> __ -> Integers.int Types.option **)
314let rec as_result xxx =
315  xxx.as_result
[2601]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 -> (__ -> __) -> (__ ->
[2773]327    status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
328    Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
329    Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
[2601]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 -> (__ -> __) -> (__ ->
[2773]335    status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
336    Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
337    Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
[2601]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 -> (__ -> __) -> (__ ->
[2773]343    status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
344    Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
345    Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
[2601]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 -> (__ -> __) -> (__ ->
[2773]351    status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
352    Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
353    Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
[2601]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 -> (__ -> __) -> (__ ->
[2773]359    status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
360    Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
361    Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
[2601]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;
[2773]370       as_result = a7; as_call_ident = a8; as_tailcall_ident = a9 } = x
[2601]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
[2773]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
[2601]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 **)
[2773]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'))) __ __ __ __
[2601]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 **)
[2951]823let rec trace_any_call_rect_Type4 s h_tac_base h_tac_step_call h_tac_step_default x_3368 x_3367 = function
[2601]824| Tac_base status -> h_tac_base status __
825| Tac_step_call
826    (status_pre_fun_call, status_after_fun_call, status_final,
[2951]827     status_start_fun_call, x_3373, x_3371) ->
[2601]828  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
[2951]829    status_start_fun_call __ __ __ x_3373 __ x_3371
[2601]830    (trace_any_call_rect_Type4 s h_tac_base h_tac_step_call
[2951]831      h_tac_step_default status_after_fun_call status_final x_3371)
832| Tac_step_default (status_pre, status_end, status_init, x_3378) ->
833  h_tac_step_default status_pre status_end status_init __ x_3378 __ __
[2601]834    (trace_any_call_rect_Type4 s h_tac_base h_tac_step_call
[2951]835      h_tac_step_default status_init status_end x_3378)
[2601]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 **)
[2951]842let rec trace_any_call_rect_Type3 s h_tac_base h_tac_step_call h_tac_step_default x_3400 x_3399 = function
[2601]843| Tac_base status -> h_tac_base status __
844| Tac_step_call
845    (status_pre_fun_call, status_after_fun_call, status_final,
[2951]846     status_start_fun_call, x_3405, x_3403) ->
[2601]847  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
[2951]848    status_start_fun_call __ __ __ x_3405 __ x_3403
[2601]849    (trace_any_call_rect_Type3 s h_tac_base h_tac_step_call
[2951]850      h_tac_step_default status_after_fun_call status_final x_3403)
851| Tac_step_default (status_pre, status_end, status_init, x_3410) ->
852  h_tac_step_default status_pre status_end status_init __ x_3410 __ __
[2601]853    (trace_any_call_rect_Type3 s h_tac_base h_tac_step_call
[2951]854      h_tac_step_default status_init status_end x_3410)
[2601]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 **)
[2951]861let rec trace_any_call_rect_Type2 s h_tac_base h_tac_step_call h_tac_step_default x_3416 x_3415 = function
[2601]862| Tac_base status -> h_tac_base status __
863| Tac_step_call
864    (status_pre_fun_call, status_after_fun_call, status_final,
[2951]865     status_start_fun_call, x_3421, x_3419) ->
[2601]866  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
[2951]867    status_start_fun_call __ __ __ x_3421 __ x_3419
[2601]868    (trace_any_call_rect_Type2 s h_tac_base h_tac_step_call
[2951]869      h_tac_step_default status_after_fun_call status_final x_3419)
870| Tac_step_default (status_pre, status_end, status_init, x_3426) ->
871  h_tac_step_default status_pre status_end status_init __ x_3426 __ __
[2601]872    (trace_any_call_rect_Type2 s h_tac_base h_tac_step_call
[2951]873      h_tac_step_default status_init status_end x_3426)
[2601]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 **)
[2951]880let rec trace_any_call_rect_Type1 s h_tac_base h_tac_step_call h_tac_step_default x_3432 x_3431 = function
[2601]881| Tac_base status -> h_tac_base status __
882| Tac_step_call
883    (status_pre_fun_call, status_after_fun_call, status_final,
[2951]884     status_start_fun_call, x_3437, x_3435) ->
[2601]885  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
[2951]886    status_start_fun_call __ __ __ x_3437 __ x_3435
[2601]887    (trace_any_call_rect_Type1 s h_tac_base h_tac_step_call
[2951]888      h_tac_step_default status_after_fun_call status_final x_3435)
889| Tac_step_default (status_pre, status_end, status_init, x_3442) ->
890  h_tac_step_default status_pre status_end status_init __ x_3442 __ __
[2601]891    (trace_any_call_rect_Type1 s h_tac_base h_tac_step_call
[2951]892      h_tac_step_default status_init status_end x_3442)
[2601]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 **)
[2951]899let rec trace_any_call_rect_Type0 s h_tac_base h_tac_step_call h_tac_step_default x_3448 x_3447 = function
[2601]900| Tac_base status -> h_tac_base status __
901| Tac_step_call
902    (status_pre_fun_call, status_after_fun_call, status_final,
[2951]903     status_start_fun_call, x_3453, x_3451) ->
[2601]904  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
[2951]905    status_start_fun_call __ __ __ x_3453 __ x_3451
[2601]906    (trace_any_call_rect_Type0 s h_tac_base h_tac_step_call
[2951]907      h_tac_step_default status_after_fun_call status_final x_3451)
908| Tac_step_default (status_pre, status_end, status_init, x_3458) ->
909  h_tac_step_default status_pre status_end status_init __ x_3458 __ __
[2601]910    (trace_any_call_rect_Type0 s h_tac_base h_tac_step_call
[2951]911      h_tac_step_default status_init status_end x_3458)
[2601]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 **)
[2951]980let rec trace_label_call_rect_Type4 s h_tlc_base x_3566 x_3565 = function
981| Tlc_base (start_status, end_status, x_3569) ->
982  h_tlc_base start_status end_status x_3569 __
[2601]983
984(** val trace_label_call_rect_Type5 :
985    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
986    -> trace_label_call -> 'a1 **)
[2951]987let rec trace_label_call_rect_Type5 s h_tlc_base x_3572 x_3571 = function
988| Tlc_base (start_status, end_status, x_3575) ->
989  h_tlc_base start_status end_status x_3575 __
[2601]990
991(** val trace_label_call_rect_Type3 :
992    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
993    -> trace_label_call -> 'a1 **)
[2951]994let rec trace_label_call_rect_Type3 s h_tlc_base x_3578 x_3577 = function
995| Tlc_base (start_status, end_status, x_3581) ->
996  h_tlc_base start_status end_status x_3581 __
[2601]997
998(** val trace_label_call_rect_Type2 :
999    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
1000    -> trace_label_call -> 'a1 **)
[2951]1001let rec trace_label_call_rect_Type2 s h_tlc_base x_3584 x_3583 = function
1002| Tlc_base (start_status, end_status, x_3587) ->
1003  h_tlc_base start_status end_status x_3587 __
[2601]1004
1005(** val trace_label_call_rect_Type1 :
1006    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
1007    -> trace_label_call -> 'a1 **)
[2951]1008let rec trace_label_call_rect_Type1 s h_tlc_base x_3590 x_3589 = function
1009| Tlc_base (start_status, end_status, x_3593) ->
1010  h_tlc_base start_status end_status x_3593 __
[2601]1011
1012(** val trace_label_call_rect_Type0 :
1013    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
1014    -> trace_label_call -> 'a1 **)
[2951]1015let rec trace_label_call_rect_Type0 s h_tlc_base x_3596 x_3595 = function
1016| Tlc_base (start_status, end_status, x_3599) ->
1017  h_tlc_base start_status end_status x_3599 __
[2601]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 **)
[2773]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'))) __ __ __
[2601]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 **)
[2951]1172let rec trace_whole_program_rect_Type4 s h_twp_terminating h_twp_diverges x_3648 = function
1173| Twp_terminating (status_initial, status_start_fun, status_final, x_3651) ->
1174  h_twp_terminating status_initial status_start_fun status_final __ __ x_3651
1175    __
1176| Twp_diverges (status_initial, status_start_fun, x_3654) ->
1177  h_twp_diverges status_initial status_start_fun __ __ x_3654
[2601]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 **)
[2951]1183let rec trace_whole_program_rect_Type5 s h_twp_terminating h_twp_diverges x_3659 = function
1184| Twp_terminating (status_initial, status_start_fun, status_final, x_3662) ->
1185  h_twp_terminating status_initial status_start_fun status_final __ __ x_3662
1186    __
1187| Twp_diverges (status_initial, status_start_fun, x_3665) ->
1188  h_twp_diverges status_initial status_start_fun __ __ x_3665
[2601]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 **)
[2951]1194let rec trace_whole_program_rect_Type3 s h_twp_terminating h_twp_diverges x_3670 = function
1195| Twp_terminating (status_initial, status_start_fun, status_final, x_3673) ->
1196  h_twp_terminating status_initial status_start_fun status_final __ __ x_3673
1197    __
1198| Twp_diverges (status_initial, status_start_fun, x_3676) ->
1199  h_twp_diverges status_initial status_start_fun __ __ x_3676
[2601]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 **)
[2951]1205let rec trace_whole_program_rect_Type2 s h_twp_terminating h_twp_diverges x_3681 = function
1206| Twp_terminating (status_initial, status_start_fun, status_final, x_3684) ->
1207  h_twp_terminating status_initial status_start_fun status_final __ __ x_3684
1208    __
1209| Twp_diverges (status_initial, status_start_fun, x_3687) ->
1210  h_twp_diverges status_initial status_start_fun __ __ x_3687
[2601]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 **)
[2951]1216let rec trace_whole_program_rect_Type1 s h_twp_terminating h_twp_diverges x_3692 = function
1217| Twp_terminating (status_initial, status_start_fun, status_final, x_3695) ->
1218  h_twp_terminating status_initial status_start_fun status_final __ __ x_3695
1219    __
1220| Twp_diverges (status_initial, status_start_fun, x_3698) ->
1221  h_twp_diverges status_initial status_start_fun __ __ x_3698
[2601]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 **)
[2951]1227let rec trace_whole_program_rect_Type0 s h_twp_terminating h_twp_diverges x_3703 = function
1228| Twp_terminating (status_initial, status_start_fun, status_final, x_3706) ->
1229  h_twp_terminating status_initial status_start_fun status_final __ __ x_3706
1230    __
1231| Twp_diverges (status_initial, status_start_fun, x_3709) ->
1232  h_twp_diverges status_initial status_start_fun __ __ x_3709
[2601]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 =
[2773]1282  Types.pi1 (as_label_safe s st2)
[2601]1283
1284(** val tll_tl_label :
1285    abstract_status -> __ -> __ -> trace_label_label -> CostLabel.costlabel **)
1286let tll_tl_label s st1 st2 tr =
[2773]1287  Types.pi1 (as_label_safe s st2)
[2601]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 **)
[2951]1296let rec trace_any_any_rect_Type4 s h_taa_base h_taa_step x_3933 x_3932 = function
[2601]1297| Taa_base st -> h_taa_base st
[2951]1298| Taa_step (st1, st2, st3, x_3935) ->
1299  h_taa_step st1 st2 st3 __ __ __ x_3935
1300    (trace_any_any_rect_Type4 s h_taa_base h_taa_step st2 st3 x_3935)
[2601]1301
1302(** val trace_any_any_rect_Type3 :
1303    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1304    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
[2951]1305let rec trace_any_any_rect_Type3 s h_taa_base h_taa_step x_3951 x_3950 = function
[2601]1306| Taa_base st -> h_taa_base st
[2951]1307| Taa_step (st1, st2, st3, x_3953) ->
1308  h_taa_step st1 st2 st3 __ __ __ x_3953
1309    (trace_any_any_rect_Type3 s h_taa_base h_taa_step st2 st3 x_3953)
[2601]1310
1311(** val trace_any_any_rect_Type2 :
1312    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1313    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
[2951]1314let rec trace_any_any_rect_Type2 s h_taa_base h_taa_step x_3960 x_3959 = function
[2601]1315| Taa_base st -> h_taa_base st
[2951]1316| Taa_step (st1, st2, st3, x_3962) ->
1317  h_taa_step st1 st2 st3 __ __ __ x_3962
1318    (trace_any_any_rect_Type2 s h_taa_base h_taa_step st2 st3 x_3962)
[2601]1319
1320(** val trace_any_any_rect_Type1 :
1321    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1322    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
[2951]1323let rec trace_any_any_rect_Type1 s h_taa_base h_taa_step x_3969 x_3968 = function
[2601]1324| Taa_base st -> h_taa_base st
[2951]1325| Taa_step (st1, st2, st3, x_3971) ->
1326  h_taa_step st1 st2 st3 __ __ __ x_3971
1327    (trace_any_any_rect_Type1 s h_taa_base h_taa_step st2 st3 x_3971)
[2601]1328
1329(** val trace_any_any_rect_Type0 :
1330    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1331    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
[2951]1332let rec trace_any_any_rect_Type0 s h_taa_base h_taa_step x_3978 x_3977 = function
[2601]1333| Taa_base st -> h_taa_base st
[2951]1334| Taa_step (st1, st2, st3, x_3980) ->
1335  h_taa_step st1 st2 st3 __ __ __ x_3980
1336    (trace_any_any_rect_Type0 s h_taa_base h_taa_step st2 st3 x_3980)
[2601]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
[2743]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
[2601]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
[2773]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
[2601]1447
[2773]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
[2951]1452| IEVcost x_4051 -> h_IEVcost x_4051
1453| IEVcall x_4052 -> h_IEVcall x_4052
1454| IEVtailcall (x_4054, x_4053) -> h_IEVtailcall x_4054 x_4053
1455| IEVret x_4055 -> h_IEVret x_4055
[2601]1456
[2773]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
[2951]1461| IEVcost x_4061 -> h_IEVcost x_4061
1462| IEVcall x_4062 -> h_IEVcall x_4062
1463| IEVtailcall (x_4064, x_4063) -> h_IEVtailcall x_4064 x_4063
1464| IEVret x_4065 -> h_IEVret x_4065
[2601]1465
[2773]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
[2951]1470| IEVcost x_4071 -> h_IEVcost x_4071
1471| IEVcall x_4072 -> h_IEVcall x_4072
1472| IEVtailcall (x_4074, x_4073) -> h_IEVtailcall x_4074 x_4073
1473| IEVret x_4075 -> h_IEVret x_4075
[2601]1474
[2773]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
[2951]1479| IEVcost x_4081 -> h_IEVcost x_4081
1480| IEVcall x_4082 -> h_IEVcall x_4082
1481| IEVtailcall (x_4084, x_4083) -> h_IEVtailcall x_4084 x_4083
1482| IEVret x_4085 -> h_IEVret x_4085
[2773]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
[2951]1488| IEVcost x_4091 -> h_IEVcost x_4091
1489| IEVcall x_4092 -> h_IEVcall x_4092
1490| IEVtailcall (x_4094, x_4093) -> h_IEVtailcall x_4094 x_4093
1491| IEVret x_4095 -> h_IEVret x_4095
[2773]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
[2951]1497| IEVcost x_4101 -> h_IEVcost x_4101
1498| IEVcall x_4102 -> h_IEVcall x_4102
1499| IEVtailcall (x_4104, x_4103) -> h_IEVtailcall x_4104 x_4103
1500| IEVret x_4105 -> h_IEVret x_4105
[2773]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
[2601]1684(** val flatten_trace_label_label :
1685    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
1686    -> as_cost_label List.list **)
[2773]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
[2601]1692(** val flatten_trace_any_label :
1693    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
1694    as_cost_label List.list **)
[2773]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)
[2601]1699
[2873]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 **)
[2951]1709let rec trace_any_any_free_rect_Type4 s h_taaf_base h_taaf_step h_taaf_step_jump x_4184 x_4183 = function
[2873]1710| Taaf_base s0 -> h_taaf_base s0
[2951]1711| Taaf_step (s1, s2, s3, x_4188) -> h_taaf_step s1 s2 s3 x_4188 __ __
1712| Taaf_step_jump (s1, s2, s3, x_4192) ->
1713  h_taaf_step_jump s1 s2 s3 x_4192 __ __ __
[2873]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 **)
[2951]1719let rec trace_any_any_free_rect_Type5 s h_taaf_base h_taaf_step h_taaf_step_jump x_4197 x_4196 = function
[2873]1720| Taaf_base s0 -> h_taaf_base s0
[2951]1721| Taaf_step (s1, s2, s3, x_4201) -> h_taaf_step s1 s2 s3 x_4201 __ __
1722| Taaf_step_jump (s1, s2, s3, x_4205) ->
1723  h_taaf_step_jump s1 s2 s3 x_4205 __ __ __
[2873]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 **)
[2951]1729let rec trace_any_any_free_rect_Type3 s h_taaf_base h_taaf_step h_taaf_step_jump x_4210 x_4209 = function
[2873]1730| Taaf_base s0 -> h_taaf_base s0
[2951]1731| Taaf_step (s1, s2, s3, x_4214) -> h_taaf_step s1 s2 s3 x_4214 __ __
1732| Taaf_step_jump (s1, s2, s3, x_4218) ->
1733  h_taaf_step_jump s1 s2 s3 x_4218 __ __ __
[2873]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 **)
[2951]1739let rec trace_any_any_free_rect_Type2 s h_taaf_base h_taaf_step h_taaf_step_jump x_4223 x_4222 = function
[2873]1740| Taaf_base s0 -> h_taaf_base s0
[2951]1741| Taaf_step (s1, s2, s3, x_4227) -> h_taaf_step s1 s2 s3 x_4227 __ __
1742| Taaf_step_jump (s1, s2, s3, x_4231) ->
1743  h_taaf_step_jump s1 s2 s3 x_4231 __ __ __
[2873]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 **)
[2951]1749let rec trace_any_any_free_rect_Type1 s h_taaf_base h_taaf_step h_taaf_step_jump x_4236 x_4235 = function
[2873]1750| Taaf_base s0 -> h_taaf_base s0
[2951]1751| Taaf_step (s1, s2, s3, x_4240) -> h_taaf_step s1 s2 s3 x_4240 __ __
1752| Taaf_step_jump (s1, s2, s3, x_4244) ->
1753  h_taaf_step_jump s1 s2 s3 x_4244 __ __ __
[2873]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 **)
[2951]1759let rec trace_any_any_free_rect_Type0 s h_taaf_base h_taaf_step h_taaf_step_jump x_4249 x_4248 = function
[2873]1760| Taaf_base s0 -> h_taaf_base s0
[2951]1761| Taaf_step (s1, s2, s3, x_4253) -> h_taaf_step s1 s2 s3 x_4253 __ __
1762| Taaf_step_jump (s1, s2, s3, x_4257) ->
1763  h_taaf_step_jump s1 s2 s3 x_4257 __ __ __
[2873]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.