source: extracted/structuredTraces.ml @ 2827

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

Everything extracted again.

File size: 72.2 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 **)
[2827]221let rec abstract_status_rect_Type4 h_mk_abstract_status x_16544 =
[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 =
[2827]224    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16544
[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 **)
[2827]234let rec abstract_status_rect_Type5 h_mk_abstract_status x_16546 =
[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 =
[2827]237    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16546
[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 **)
[2827]247let rec abstract_status_rect_Type3 h_mk_abstract_status x_16548 =
[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 =
[2827]250    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16548
[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 **)
[2827]260let rec abstract_status_rect_Type2 h_mk_abstract_status x_16550 =
[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 =
[2827]263    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16550
[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 **)
[2827]273let rec abstract_status_rect_Type1 h_mk_abstract_status x_16552 =
[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 =
[2827]276    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16552
[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 **)
[2827]286let rec abstract_status_rect_Type0 h_mk_abstract_status x_16554 =
[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 =
[2827]289    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16554
[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 **)
[2827]823let rec trace_any_call_rect_Type4 s h_tac_base h_tac_step_call h_tac_step_default x_16632 x_16631 = 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,
[2827]827     status_start_fun_call, x_16637, x_16635) ->
[2601]828  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
[2827]829    status_start_fun_call __ __ __ x_16637 __ x_16635
[2601]830    (trace_any_call_rect_Type4 s h_tac_base h_tac_step_call
[2827]831      h_tac_step_default status_after_fun_call status_final x_16635)
832| Tac_step_default (status_pre, status_end, status_init, x_16642) ->
833  h_tac_step_default status_pre status_end status_init __ x_16642 __ __
[2601]834    (trace_any_call_rect_Type4 s h_tac_base h_tac_step_call
[2827]835      h_tac_step_default status_init status_end x_16642)
[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 **)
[2827]842let rec trace_any_call_rect_Type3 s h_tac_base h_tac_step_call h_tac_step_default x_16664 x_16663 = 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,
[2827]846     status_start_fun_call, x_16669, x_16667) ->
[2601]847  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
[2827]848    status_start_fun_call __ __ __ x_16669 __ x_16667
[2601]849    (trace_any_call_rect_Type3 s h_tac_base h_tac_step_call
[2827]850      h_tac_step_default status_after_fun_call status_final x_16667)
851| Tac_step_default (status_pre, status_end, status_init, x_16674) ->
852  h_tac_step_default status_pre status_end status_init __ x_16674 __ __
[2601]853    (trace_any_call_rect_Type3 s h_tac_base h_tac_step_call
[2827]854      h_tac_step_default status_init status_end x_16674)
[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 **)
[2827]861let rec trace_any_call_rect_Type2 s h_tac_base h_tac_step_call h_tac_step_default x_16680 x_16679 = 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,
[2827]865     status_start_fun_call, x_16685, x_16683) ->
[2601]866  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
[2827]867    status_start_fun_call __ __ __ x_16685 __ x_16683
[2601]868    (trace_any_call_rect_Type2 s h_tac_base h_tac_step_call
[2827]869      h_tac_step_default status_after_fun_call status_final x_16683)
870| Tac_step_default (status_pre, status_end, status_init, x_16690) ->
871  h_tac_step_default status_pre status_end status_init __ x_16690 __ __
[2601]872    (trace_any_call_rect_Type2 s h_tac_base h_tac_step_call
[2827]873      h_tac_step_default status_init status_end x_16690)
[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 **)
[2827]880let rec trace_any_call_rect_Type1 s h_tac_base h_tac_step_call h_tac_step_default x_16696 x_16695 = 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,
[2827]884     status_start_fun_call, x_16701, x_16699) ->
[2601]885  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
[2827]886    status_start_fun_call __ __ __ x_16701 __ x_16699
[2601]887    (trace_any_call_rect_Type1 s h_tac_base h_tac_step_call
[2827]888      h_tac_step_default status_after_fun_call status_final x_16699)
889| Tac_step_default (status_pre, status_end, status_init, x_16706) ->
890  h_tac_step_default status_pre status_end status_init __ x_16706 __ __
[2601]891    (trace_any_call_rect_Type1 s h_tac_base h_tac_step_call
[2827]892      h_tac_step_default status_init status_end x_16706)
[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 **)
[2827]899let rec trace_any_call_rect_Type0 s h_tac_base h_tac_step_call h_tac_step_default x_16712 x_16711 = 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,
[2827]903     status_start_fun_call, x_16717, x_16715) ->
[2601]904  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
[2827]905    status_start_fun_call __ __ __ x_16717 __ x_16715
[2601]906    (trace_any_call_rect_Type0 s h_tac_base h_tac_step_call
[2827]907      h_tac_step_default status_after_fun_call status_final x_16715)
908| Tac_step_default (status_pre, status_end, status_init, x_16722) ->
909  h_tac_step_default status_pre status_end status_init __ x_16722 __ __
[2601]910    (trace_any_call_rect_Type0 s h_tac_base h_tac_step_call
[2827]911      h_tac_step_default status_init status_end x_16722)
[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 **)
[2827]980let rec trace_label_call_rect_Type4 s h_tlc_base x_16830 x_16829 = function
981| Tlc_base (start_status, end_status, x_16833) ->
982  h_tlc_base start_status end_status x_16833 __
[2601]983
984(** val trace_label_call_rect_Type5 :
985    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
986    -> trace_label_call -> 'a1 **)
[2827]987let rec trace_label_call_rect_Type5 s h_tlc_base x_16836 x_16835 = function
988| Tlc_base (start_status, end_status, x_16839) ->
989  h_tlc_base start_status end_status x_16839 __
[2601]990
991(** val trace_label_call_rect_Type3 :
992    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
993    -> trace_label_call -> 'a1 **)
[2827]994let rec trace_label_call_rect_Type3 s h_tlc_base x_16842 x_16841 = function
995| Tlc_base (start_status, end_status, x_16845) ->
996  h_tlc_base start_status end_status x_16845 __
[2601]997
998(** val trace_label_call_rect_Type2 :
999    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
1000    -> trace_label_call -> 'a1 **)
[2827]1001let rec trace_label_call_rect_Type2 s h_tlc_base x_16848 x_16847 = function
1002| Tlc_base (start_status, end_status, x_16851) ->
1003  h_tlc_base start_status end_status x_16851 __
[2601]1004
1005(** val trace_label_call_rect_Type1 :
1006    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
1007    -> trace_label_call -> 'a1 **)
[2827]1008let rec trace_label_call_rect_Type1 s h_tlc_base x_16854 x_16853 = function
1009| Tlc_base (start_status, end_status, x_16857) ->
1010  h_tlc_base start_status end_status x_16857 __
[2601]1011
1012(** val trace_label_call_rect_Type0 :
1013    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
1014    -> trace_label_call -> 'a1 **)
[2827]1015let rec trace_label_call_rect_Type0 s h_tlc_base x_16860 x_16859 = function
1016| Tlc_base (start_status, end_status, x_16863) ->
1017  h_tlc_base start_status end_status x_16863 __
[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 **)
[2827]1172let rec trace_whole_program_rect_Type4 s h_twp_terminating h_twp_diverges x_16912 = function
[2743]1173| Twp_terminating
[2827]1174    (status_initial, status_start_fun, status_final, x_16915) ->
[2743]1175  h_twp_terminating status_initial status_start_fun status_final __ __
[2827]1176    x_16915 __
1177| Twp_diverges (status_initial, status_start_fun, x_16918) ->
1178  h_twp_diverges status_initial status_start_fun __ __ x_16918
[2601]1179
1180(** val trace_whole_program_rect_Type5 :
1181    abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1182    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1183    -> trace_whole_program -> 'a1 **)
[2827]1184let rec trace_whole_program_rect_Type5 s h_twp_terminating h_twp_diverges x_16923 = function
[2743]1185| Twp_terminating
[2827]1186    (status_initial, status_start_fun, status_final, x_16926) ->
[2743]1187  h_twp_terminating status_initial status_start_fun status_final __ __
[2827]1188    x_16926 __
1189| Twp_diverges (status_initial, status_start_fun, x_16929) ->
1190  h_twp_diverges status_initial status_start_fun __ __ x_16929
[2601]1191
1192(** val trace_whole_program_rect_Type3 :
1193    abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1194    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1195    -> trace_whole_program -> 'a1 **)
[2827]1196let rec trace_whole_program_rect_Type3 s h_twp_terminating h_twp_diverges x_16934 = function
[2743]1197| Twp_terminating
[2827]1198    (status_initial, status_start_fun, status_final, x_16937) ->
[2743]1199  h_twp_terminating status_initial status_start_fun status_final __ __
[2827]1200    x_16937 __
1201| Twp_diverges (status_initial, status_start_fun, x_16940) ->
1202  h_twp_diverges status_initial status_start_fun __ __ x_16940
[2601]1203
1204(** val trace_whole_program_rect_Type2 :
1205    abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1206    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1207    -> trace_whole_program -> 'a1 **)
[2827]1208let rec trace_whole_program_rect_Type2 s h_twp_terminating h_twp_diverges x_16945 = function
[2743]1209| Twp_terminating
[2827]1210    (status_initial, status_start_fun, status_final, x_16948) ->
[2743]1211  h_twp_terminating status_initial status_start_fun status_final __ __
[2827]1212    x_16948 __
1213| Twp_diverges (status_initial, status_start_fun, x_16951) ->
1214  h_twp_diverges status_initial status_start_fun __ __ x_16951
[2601]1215
1216(** val trace_whole_program_rect_Type1 :
1217    abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1218    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1219    -> trace_whole_program -> 'a1 **)
[2827]1220let rec trace_whole_program_rect_Type1 s h_twp_terminating h_twp_diverges x_16956 = function
[2743]1221| Twp_terminating
[2827]1222    (status_initial, status_start_fun, status_final, x_16959) ->
[2743]1223  h_twp_terminating status_initial status_start_fun status_final __ __
[2827]1224    x_16959 __
1225| Twp_diverges (status_initial, status_start_fun, x_16962) ->
1226  h_twp_diverges status_initial status_start_fun __ __ x_16962
[2601]1227
1228(** val trace_whole_program_rect_Type0 :
1229    abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1230    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1231    -> trace_whole_program -> 'a1 **)
[2827]1232let rec trace_whole_program_rect_Type0 s h_twp_terminating h_twp_diverges x_16967 = function
[2743]1233| Twp_terminating
[2827]1234    (status_initial, status_start_fun, status_final, x_16970) ->
[2743]1235  h_twp_terminating status_initial status_start_fun status_final __ __
[2827]1236    x_16970 __
1237| Twp_diverges (status_initial, status_start_fun, x_16973) ->
1238  h_twp_diverges status_initial status_start_fun __ __ x_16973
[2601]1239
1240(** val trace_whole_program_inv_rect_Type4 :
1241    abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ ->
1242    __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1243    __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **)
1244let trace_whole_program_inv_rect_Type4 x1 x2 hterm h1 h2 =
1245  let hcut = trace_whole_program_rect_Type4 x1 h1 h2 x2 hterm in hcut __ __
1246
1247(** val trace_whole_program_inv_rect_Type3 :
1248    abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ ->
1249    __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1250    __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **)
1251let trace_whole_program_inv_rect_Type3 x1 x2 hterm h1 h2 =
1252  let hcut = trace_whole_program_rect_Type3 x1 h1 h2 x2 hterm in hcut __ __
1253
1254(** val trace_whole_program_inv_rect_Type2 :
1255    abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ ->
1256    __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1257    __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **)
1258let trace_whole_program_inv_rect_Type2 x1 x2 hterm h1 h2 =
1259  let hcut = trace_whole_program_rect_Type2 x1 h1 h2 x2 hterm in hcut __ __
1260
1261(** val trace_whole_program_inv_rect_Type1 :
1262    abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ ->
1263    __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1264    __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **)
1265let trace_whole_program_inv_rect_Type1 x1 x2 hterm h1 h2 =
1266  let hcut = trace_whole_program_rect_Type1 x1 h1 h2 x2 hterm in hcut __ __
1267
1268(** val trace_whole_program_inv_rect_Type0 :
1269    abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ ->
1270    __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1271    __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **)
1272let trace_whole_program_inv_rect_Type0 x1 x2 hterm h1 h2 =
1273  let hcut = trace_whole_program_rect_Type0 x1 h1 h2 x2 hterm in hcut __ __
1274
1275(** val trace_whole_program_jmdiscr :
1276    abstract_status -> __ -> trace_whole_program -> trace_whole_program -> __ **)
1277let trace_whole_program_jmdiscr a1 a2 x y =
1278  Logic.eq_rect_Type2 x
1279    (match x with
1280     | Twp_terminating (a0, a10, a20, a5) ->
1281       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)
1282     | Twp_diverges (a0, a10, a4) ->
1283       Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
1284
1285(** val tal_tl_label :
1286    abstract_status -> __ -> __ -> trace_any_label -> CostLabel.costlabel **)
1287let tal_tl_label s st1 st2 tr =
[2773]1288  Types.pi1 (as_label_safe s st2)
[2601]1289
1290(** val tll_tl_label :
1291    abstract_status -> __ -> __ -> trace_label_label -> CostLabel.costlabel **)
1292let tll_tl_label s st1 st2 tr =
[2773]1293  Types.pi1 (as_label_safe s st2)
[2601]1294
1295type trace_any_any =
1296| Taa_base of __
1297| Taa_step of __ * __ * __ * trace_any_any
1298
1299(** val trace_any_any_rect_Type4 :
1300    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1301    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
[2827]1302let rec trace_any_any_rect_Type4 s h_taa_base h_taa_step x_17197 x_17196 = function
[2601]1303| Taa_base st -> h_taa_base st
[2827]1304| Taa_step (st1, st2, st3, x_17199) ->
1305  h_taa_step st1 st2 st3 __ __ __ x_17199
1306    (trace_any_any_rect_Type4 s h_taa_base h_taa_step st2 st3 x_17199)
[2601]1307
1308(** val trace_any_any_rect_Type3 :
1309    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1310    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
[2827]1311let rec trace_any_any_rect_Type3 s h_taa_base h_taa_step x_17215 x_17214 = function
[2601]1312| Taa_base st -> h_taa_base st
[2827]1313| Taa_step (st1, st2, st3, x_17217) ->
1314  h_taa_step st1 st2 st3 __ __ __ x_17217
1315    (trace_any_any_rect_Type3 s h_taa_base h_taa_step st2 st3 x_17217)
[2601]1316
1317(** val trace_any_any_rect_Type2 :
1318    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1319    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
[2827]1320let rec trace_any_any_rect_Type2 s h_taa_base h_taa_step x_17224 x_17223 = function
[2601]1321| Taa_base st -> h_taa_base st
[2827]1322| Taa_step (st1, st2, st3, x_17226) ->
1323  h_taa_step st1 st2 st3 __ __ __ x_17226
1324    (trace_any_any_rect_Type2 s h_taa_base h_taa_step st2 st3 x_17226)
[2601]1325
1326(** val trace_any_any_rect_Type1 :
1327    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1328    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
[2827]1329let rec trace_any_any_rect_Type1 s h_taa_base h_taa_step x_17233 x_17232 = function
[2601]1330| Taa_base st -> h_taa_base st
[2827]1331| Taa_step (st1, st2, st3, x_17235) ->
1332  h_taa_step st1 st2 st3 __ __ __ x_17235
1333    (trace_any_any_rect_Type1 s h_taa_base h_taa_step st2 st3 x_17235)
[2601]1334
1335(** val trace_any_any_rect_Type0 :
1336    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1337    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
[2827]1338let rec trace_any_any_rect_Type0 s h_taa_base h_taa_step x_17242 x_17241 = function
[2601]1339| Taa_base st -> h_taa_base st
[2827]1340| Taa_step (st1, st2, st3, x_17244) ->
1341  h_taa_step st1 st2 st3 __ __ __ x_17244
1342    (trace_any_any_rect_Type0 s h_taa_base h_taa_step st2 st3 x_17244)
[2601]1343
1344(** val trace_any_any_inv_rect_Type4 :
1345    abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
1346    'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __
1347    -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1348let trace_any_any_inv_rect_Type4 x1 x2 x3 hterm h1 h2 =
1349  let hcut = trace_any_any_rect_Type4 x1 h1 h2 x2 x3 hterm in hcut __ __ __
1350
1351(** val trace_any_any_inv_rect_Type3 :
1352    abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
1353    'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __
1354    -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1355let trace_any_any_inv_rect_Type3 x1 x2 x3 hterm h1 h2 =
1356  let hcut = trace_any_any_rect_Type3 x1 h1 h2 x2 x3 hterm in hcut __ __ __
1357
1358(** val trace_any_any_inv_rect_Type2 :
1359    abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
1360    'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __
1361    -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1362let trace_any_any_inv_rect_Type2 x1 x2 x3 hterm h1 h2 =
1363  let hcut = trace_any_any_rect_Type2 x1 h1 h2 x2 x3 hterm in hcut __ __ __
1364
1365(** val trace_any_any_inv_rect_Type1 :
1366    abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
1367    'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __
1368    -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1369let trace_any_any_inv_rect_Type1 x1 x2 x3 hterm h1 h2 =
1370  let hcut = trace_any_any_rect_Type1 x1 h1 h2 x2 x3 hterm in hcut __ __ __
1371
1372(** val trace_any_any_inv_rect_Type0 :
1373    abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
1374    'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __
1375    -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1376let trace_any_any_inv_rect_Type0 x1 x2 x3 hterm h1 h2 =
1377  let hcut = trace_any_any_rect_Type0 x1 h1 h2 x2 x3 hterm in hcut __ __ __
1378
1379(** val trace_any_any_jmdiscr :
1380    abstract_status -> __ -> __ -> trace_any_any -> trace_any_any -> __ **)
1381let trace_any_any_jmdiscr a1 a2 a3 x y =
1382  Logic.eq_rect_Type2 x
1383    (match x with
1384     | Taa_base a0 -> Obj.magic (fun _ dH -> dH __)
1385     | Taa_step (a0, a10, a20, a6) ->
1386       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
1387
1388(** val taa_non_empty :
1389    abstract_status -> __ -> __ -> trace_any_any -> Bool.bool **)
1390let taa_non_empty s st1 st2 = function
1391| Taa_base x -> Bool.False
1392| Taa_step (x, x0, x1, x5) -> Bool.True
1393
[2743]1394(** val dpi1__o__taa_to_bool__o__inject :
1395    abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair ->
1396    Bool.bool Types.sig0 **)
1397let dpi1__o__taa_to_bool__o__inject x1 x2 x3 x5 =
1398  taa_non_empty x1 x2 x3 x5.Types.dpi1
1399
1400(** val dpi1__o__taa_to_bool__o__bool_to_Prop__o__inject :
1401    abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair -> __
1402    Types.sig0 **)
1403let dpi1__o__taa_to_bool__o__bool_to_Prop__o__inject x1 x2 x3 x5 =
1404  Util.bool_to_Prop__o__inject (taa_non_empty x1 x2 x3 x5.Types.dpi1)
1405
1406(** val eject__o__taa_to_bool__o__inject :
1407    abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> Bool.bool
1408    Types.sig0 **)
1409let eject__o__taa_to_bool__o__inject x1 x2 x3 x5 =
1410  taa_non_empty x1 x2 x3 (Types.pi1 x5)
1411
1412(** val eject__o__taa_to_bool__o__bool_to_Prop__o__inject :
1413    abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> __ Types.sig0 **)
1414let eject__o__taa_to_bool__o__bool_to_Prop__o__inject x1 x2 x3 x5 =
1415  Util.bool_to_Prop__o__inject (taa_non_empty x1 x2 x3 (Types.pi1 x5))
1416
1417(** val taa_to_bool__o__bool_to_Prop__o__inject :
1418    abstract_status -> __ -> __ -> trace_any_any -> __ Types.sig0 **)
1419let taa_to_bool__o__bool_to_Prop__o__inject x1 x2 x3 x4 =
1420  Util.bool_to_Prop__o__inject (taa_non_empty x1 x2 x3 x4)
1421
1422(** val taa_to_bool__o__inject :
1423    abstract_status -> __ -> __ -> trace_any_any -> Bool.bool Types.sig0 **)
1424let taa_to_bool__o__inject x1 x2 x3 x4 =
1425  taa_non_empty x1 x2 x3 x4
1426
1427(** val dpi1__o__taa_to_bool :
1428    abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair ->
1429    Bool.bool **)
1430let dpi1__o__taa_to_bool x0 x1 x2 x4 =
1431  taa_non_empty x0 x1 x2 x4.Types.dpi1
1432
1433(** val eject__o__taa_to_bool :
1434    abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> Bool.bool **)
1435let eject__o__taa_to_bool x0 x1 x2 x4 =
1436  taa_non_empty x0 x1 x2 (Types.pi1 x4)
1437
[2601]1438(** val taa_append_tal :
1439    abstract_status -> __ -> trace_ends_with_ret -> __ -> __ -> trace_any_any
1440    -> trace_any_label -> trace_any_label **)
1441let rec taa_append_tal s st1 fl st2 st3 taa =
1442  (match taa with
1443   | Taa_base st1' -> (fun fl0 st30 tal2 -> tal2)
1444   | Taa_step (st1', st2', st3', tl) ->
1445     (fun fl0 st30 tal2 -> Tal_step_default (fl0, st1', st2', st30,
1446       (taa_append_tal s st2' fl0 st3' st30 tl tal2)))) fl st3
1447
[2773]1448type intensional_event =
1449| IEVcost of CostLabel.costlabel
1450| IEVcall of AST.ident
1451| IEVtailcall of AST.ident * AST.ident
1452| IEVret of AST.ident
[2601]1453
[2773]1454(** val intensional_event_rect_Type4 :
1455    (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1456    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1457let rec intensional_event_rect_Type4 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
[2827]1458| IEVcost x_17315 -> h_IEVcost x_17315
1459| IEVcall x_17316 -> h_IEVcall x_17316
1460| IEVtailcall (x_17318, x_17317) -> h_IEVtailcall x_17318 x_17317
1461| IEVret x_17319 -> h_IEVret x_17319
[2601]1462
[2773]1463(** val intensional_event_rect_Type5 :
1464    (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1465    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1466let rec intensional_event_rect_Type5 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
[2827]1467| IEVcost x_17325 -> h_IEVcost x_17325
1468| IEVcall x_17326 -> h_IEVcall x_17326
1469| IEVtailcall (x_17328, x_17327) -> h_IEVtailcall x_17328 x_17327
1470| IEVret x_17329 -> h_IEVret x_17329
[2601]1471
[2773]1472(** val intensional_event_rect_Type3 :
1473    (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1474    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1475let rec intensional_event_rect_Type3 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
[2827]1476| IEVcost x_17335 -> h_IEVcost x_17335
1477| IEVcall x_17336 -> h_IEVcall x_17336
1478| IEVtailcall (x_17338, x_17337) -> h_IEVtailcall x_17338 x_17337
1479| IEVret x_17339 -> h_IEVret x_17339
[2601]1480
[2773]1481(** val intensional_event_rect_Type2 :
1482    (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1483    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1484let rec intensional_event_rect_Type2 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
[2827]1485| IEVcost x_17345 -> h_IEVcost x_17345
1486| IEVcall x_17346 -> h_IEVcall x_17346
1487| IEVtailcall (x_17348, x_17347) -> h_IEVtailcall x_17348 x_17347
1488| IEVret x_17349 -> h_IEVret x_17349
[2773]1489
1490(** val intensional_event_rect_Type1 :
1491    (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1492    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1493let rec intensional_event_rect_Type1 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
[2827]1494| IEVcost x_17355 -> h_IEVcost x_17355
1495| IEVcall x_17356 -> h_IEVcall x_17356
1496| IEVtailcall (x_17358, x_17357) -> h_IEVtailcall x_17358 x_17357
1497| IEVret x_17359 -> h_IEVret x_17359
[2773]1498
1499(** val intensional_event_rect_Type0 :
1500    (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1501    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1502let rec intensional_event_rect_Type0 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
[2827]1503| IEVcost x_17365 -> h_IEVcost x_17365
1504| IEVcall x_17366 -> h_IEVcall x_17366
1505| IEVtailcall (x_17368, x_17367) -> h_IEVtailcall x_17368 x_17367
1506| IEVret x_17369 -> h_IEVret x_17369
[2773]1507
1508(** val intensional_event_inv_rect_Type4 :
1509    intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident ->
1510    __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __
1511    -> 'a1) -> 'a1 **)
1512let intensional_event_inv_rect_Type4 hterm h1 h2 h3 h4 =
1513  let hcut = intensional_event_rect_Type4 h1 h2 h3 h4 hterm in hcut __
1514
1515(** val intensional_event_inv_rect_Type3 :
1516    intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident ->
1517    __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __
1518    -> 'a1) -> 'a1 **)
1519let intensional_event_inv_rect_Type3 hterm h1 h2 h3 h4 =
1520  let hcut = intensional_event_rect_Type3 h1 h2 h3 h4 hterm in hcut __
1521
1522(** val intensional_event_inv_rect_Type2 :
1523    intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident ->
1524    __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __
1525    -> 'a1) -> 'a1 **)
1526let intensional_event_inv_rect_Type2 hterm h1 h2 h3 h4 =
1527  let hcut = intensional_event_rect_Type2 h1 h2 h3 h4 hterm in hcut __
1528
1529(** val intensional_event_inv_rect_Type1 :
1530    intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident ->
1531    __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __
1532    -> 'a1) -> 'a1 **)
1533let intensional_event_inv_rect_Type1 hterm h1 h2 h3 h4 =
1534  let hcut = intensional_event_rect_Type1 h1 h2 h3 h4 hterm in hcut __
1535
1536(** val intensional_event_inv_rect_Type0 :
1537    intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident ->
1538    __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __
1539    -> 'a1) -> 'a1 **)
1540let intensional_event_inv_rect_Type0 hterm h1 h2 h3 h4 =
1541  let hcut = intensional_event_rect_Type0 h1 h2 h3 h4 hterm in hcut __
1542
1543(** val intensional_event_discr :
1544    intensional_event -> intensional_event -> __ **)
1545let intensional_event_discr x y =
1546  Logic.eq_rect_Type2 x
1547    (match x with
1548     | IEVcost a0 -> Obj.magic (fun _ dH -> dH __)
1549     | IEVcall a0 -> Obj.magic (fun _ dH -> dH __)
1550     | IEVtailcall (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1551     | IEVret a0 -> Obj.magic (fun _ dH -> dH __)) y
1552
1553(** val intensional_event_jmdiscr :
1554    intensional_event -> intensional_event -> __ **)
1555let intensional_event_jmdiscr x y =
1556  Logic.eq_rect_Type2 x
1557    (match x with
1558     | IEVcost a0 -> Obj.magic (fun _ dH -> dH __)
1559     | IEVcall a0 -> Obj.magic (fun _ dH -> dH __)
1560     | IEVtailcall (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1561     | IEVret a0 -> Obj.magic (fun _ dH -> dH __)) y
1562
1563type as_trace = intensional_event List.list Types.sig0
1564
1565(** val cons_safe :
1566    'a1 Types.sig0 -> 'a1 List.list Types.sig0 -> 'a1 List.list Types.sig0 **)
1567let cons_safe x l =
1568  List.Cons ((Types.pi1 x), (Types.pi1 l))
1569
1570(** val append_safe :
1571    'a1 List.list Types.sig0 -> 'a1 List.list Types.sig0 -> 'a1 List.list
1572    Types.sig0 **)
1573let append_safe l1 l2 =
1574  List.append (Types.pi1 l1) (Types.pi1 l2)
1575
1576(** val nil_safe : 'a1 List.list Types.sig0 **)
1577let nil_safe =
1578  List.Nil
1579
1580(** val emittable_cost :
1581    abstract_status -> as_cost_label -> intensional_event Types.sig0 **)
1582let emittable_cost s l =
1583  IEVcost (Types.pi1 l)
1584
1585(** val observables_trace_label_label :
1586    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
1587    -> AST.ident -> as_trace **)
1588let rec observables_trace_label_label s trace_ends_flag start_status final_status the_trace curr =
1589  let Tll_base (ends_flag, initial, final, given_trace) = the_trace in
1590  let label = as_label_safe s initial in
1591  cons_safe (emittable_cost s label)
1592    (observables_trace_any_label s ends_flag initial final given_trace curr)
1593(** val observables_trace_any_label :
1594    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
1595    AST.ident -> as_trace **)
1596and observables_trace_any_label s trace_ends_flag start_status final_status the_trace curr =
1597  match the_trace with
1598  | Tal_base_not_return (the_status, x) -> nil_safe
1599  | Tal_base_return (the_status, x) -> cons_safe (IEVret curr) nil_safe
1600  | Tal_base_call (pre_fun_call, start_fun_call, final, call_trace) ->
1601    let id = s.as_call_ident pre_fun_call in
1602    cons_safe (IEVcall id)
1603      (observables_trace_label_return s start_fun_call final call_trace id)
1604  | Tal_base_tailcall (pre_fun_call, start_fun_call, final, call_trace) ->
1605    let id = s.as_tailcall_ident pre_fun_call in
1606    cons_safe (IEVtailcall (curr, id))
1607      (observables_trace_label_return s start_fun_call final call_trace id)
1608  | Tal_step_call
1609      (end_flag, pre_fun_call, start_fun_call, after_fun_call, final,
1610       call_trace, final_trace) ->
1611    let id = s.as_call_ident pre_fun_call in
1612    let call_cost_trace =
1613      observables_trace_label_return s start_fun_call after_fun_call
1614        call_trace id
1615    in
1616    let final_cost_trace =
1617      observables_trace_any_label s end_flag after_fun_call final final_trace
1618        curr
1619    in
1620    append_safe (cons_safe (IEVcall id) call_cost_trace) final_cost_trace
1621  | Tal_step_default
1622      (end_flag, status_pre, status_init, status_end, tail_trace) ->
1623    observables_trace_any_label s end_flag status_init status_end tail_trace
1624      curr
1625(** val observables_trace_label_return :
1626    abstract_status -> __ -> __ -> trace_label_return -> AST.ident ->
1627    as_trace **)
1628and observables_trace_label_return s start_status final_status the_trace curr =
1629  match the_trace with
1630  | Tlr_base (before, after, trace_to_lift) ->
1631    observables_trace_label_label s Ends_with_ret before after trace_to_lift
1632      curr
1633  | Tlr_step (initial, labelled, final, labelled_trace, ret_trace) ->
1634    let labelled_cost =
1635      observables_trace_label_label s Doesnt_end_with_ret initial labelled
1636        labelled_trace curr
1637    in
1638    let return_cost =
1639      observables_trace_label_return s labelled final ret_trace curr
1640    in
1641    append_safe labelled_cost return_cost
1642
1643(** val filter_map :
1644    ('a1 -> 'a2 Types.option) -> 'a1 List.list -> 'a2 List.list **)
1645let rec filter_map f = function
1646| List.Nil -> List.Nil
1647| List.Cons (hd, tl) ->
1648  List.append
1649    (match f hd with
1650     | Types.None -> List.Nil
1651     | Types.Some y -> List.Cons (y, List.Nil)) (filter_map f tl)
1652
1653(** val list_distribute_sig_aux :
1654    'a1 List.list -> 'a1 Types.sig0 List.list **)
1655let rec list_distribute_sig_aux l =
1656  (match l with
1657   | List.Nil -> (fun _ -> List.Nil)
1658   | List.Cons (hd, tl) ->
1659     (fun _ -> List.Cons (hd, (list_distribute_sig_aux tl)))) __
1660
1661(** val list_distribute_sig :
1662    'a1 List.list Types.sig0 -> 'a1 Types.sig0 List.list **)
1663let list_distribute_sig l =
1664  list_distribute_sig_aux (Types.pi1 l)
1665
1666(** val list_factor_sig :
1667    'a1 Types.sig0 List.list -> 'a1 List.list Types.sig0 **)
1668let rec list_factor_sig = function
1669| List.Nil -> nil_safe
1670| List.Cons (hd, tl) -> cons_safe hd (list_factor_sig tl)
1671
1672(** val costlabels_of_observables :
1673    abstract_status -> as_trace -> as_cost_label List.list **)
1674let costlabels_of_observables s l =
1675  filter_map (fun ev ->
1676    (match Types.pi1 ev with
1677     | IEVcost c -> (fun _ -> Types.Some c)
1678     | IEVcall x -> (fun _ -> Types.None)
1679     | IEVtailcall (x, x0) -> (fun _ -> Types.None)
1680     | IEVret x -> (fun _ -> Types.None)) __) (list_distribute_sig l)
1681
1682(** val flatten_trace_label_return :
1683    abstract_status -> __ -> __ -> trace_label_return -> as_cost_label
1684    List.list **)
1685let flatten_trace_label_return s st1 st2 tlr =
1686  let dummy = Positive.One in
1687  costlabels_of_observables s
1688    (observables_trace_label_return s st1 st2 tlr dummy)
1689
[2601]1690(** val flatten_trace_label_label :
1691    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
1692    -> as_cost_label List.list **)
[2773]1693let flatten_trace_label_label s flag st1 st2 tll =
1694  let dummy = Positive.One in
1695  costlabels_of_observables s
1696    (observables_trace_label_label s flag st1 st2 tll dummy)
1697
[2601]1698(** val flatten_trace_any_label :
1699    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
1700    as_cost_label List.list **)
[2773]1701let flatten_trace_any_label s flag st1 st2 tll =
1702  let dummy = Positive.One in
1703  costlabels_of_observables s
1704    (observables_trace_any_label s flag st1 st2 tll dummy)
[2601]1705
Note: See TracBrowser for help on using the repository browser.