source: driver/extracted/structuredTraces.ml @ 3106

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

New extraction
File size: 80.7 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Relations
12
13open Bool
14
15open Jmeq
16
17open Proper
18
19open PositiveMap
20
21open Deqsets
22
23open ErrorMessages
24
25open PreIdentifiers
26
27open Errors
28
29open Extralib
30
31open Setoids
32
33open Monad
34
35open Option
36
37open Div_and_mod
38
39open Russell
40
41open Util
42
43open List
44
45open Lists
46
47open Nat
48
49open Positive
50
51open Types
52
53open Identifiers
54
55open CostLabel
56
57open Sets
58
59open Listb
60
61open Integers
62
63open AST
64
65open Division
66
67open Exp
68
69open Arithmetic
70
71open Extranat
72
73open Vector
74
75open FoldStuff
76
77open BitVector
78
79open Z
80
81open BitVectorZ
82
83open Pointers
84
85open Coqlib
86
87open Values
88
89open Events
90
91open IOMonad
92
93open IO
94
95open Hide
96
97type status_class =
98| Cl_return
99| Cl_jump
100| Cl_call
101| Cl_tailcall
102| Cl_other
103
104(** val status_class_rect_Type4 :
105    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
106let rec status_class_rect_Type4 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
107| Cl_return -> h_cl_return
108| Cl_jump -> h_cl_jump
109| Cl_call -> h_cl_call
110| Cl_tailcall -> h_cl_tailcall
111| Cl_other -> h_cl_other
112
113(** val status_class_rect_Type5 :
114    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
115let rec status_class_rect_Type5 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
116| Cl_return -> h_cl_return
117| Cl_jump -> h_cl_jump
118| Cl_call -> h_cl_call
119| Cl_tailcall -> h_cl_tailcall
120| Cl_other -> h_cl_other
121
122(** val status_class_rect_Type3 :
123    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
124let rec status_class_rect_Type3 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
125| Cl_return -> h_cl_return
126| Cl_jump -> h_cl_jump
127| Cl_call -> h_cl_call
128| Cl_tailcall -> h_cl_tailcall
129| Cl_other -> h_cl_other
130
131(** val status_class_rect_Type2 :
132    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
133let rec status_class_rect_Type2 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
134| Cl_return -> h_cl_return
135| Cl_jump -> h_cl_jump
136| Cl_call -> h_cl_call
137| Cl_tailcall -> h_cl_tailcall
138| Cl_other -> h_cl_other
139
140(** val status_class_rect_Type1 :
141    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
142let rec status_class_rect_Type1 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
143| Cl_return -> h_cl_return
144| Cl_jump -> h_cl_jump
145| Cl_call -> h_cl_call
146| Cl_tailcall -> h_cl_tailcall
147| Cl_other -> h_cl_other
148
149(** val status_class_rect_Type0 :
150    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
151let rec status_class_rect_Type0 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
152| Cl_return -> h_cl_return
153| Cl_jump -> h_cl_jump
154| Cl_call -> h_cl_call
155| Cl_tailcall -> h_cl_tailcall
156| Cl_other -> h_cl_other
157
158(** val status_class_inv_rect_Type4 :
159    status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
160    -> (__ -> 'a1) -> 'a1 **)
161let status_class_inv_rect_Type4 hterm h1 h2 h3 h4 h5 =
162  let hcut = status_class_rect_Type4 h1 h2 h3 h4 h5 hterm in hcut __
163
164(** val status_class_inv_rect_Type3 :
165    status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
166    -> (__ -> 'a1) -> 'a1 **)
167let status_class_inv_rect_Type3 hterm h1 h2 h3 h4 h5 =
168  let hcut = status_class_rect_Type3 h1 h2 h3 h4 h5 hterm in hcut __
169
170(** val status_class_inv_rect_Type2 :
171    status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
172    -> (__ -> 'a1) -> 'a1 **)
173let status_class_inv_rect_Type2 hterm h1 h2 h3 h4 h5 =
174  let hcut = status_class_rect_Type2 h1 h2 h3 h4 h5 hterm in hcut __
175
176(** val status_class_inv_rect_Type1 :
177    status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
178    -> (__ -> 'a1) -> 'a1 **)
179let status_class_inv_rect_Type1 hterm h1 h2 h3 h4 h5 =
180  let hcut = status_class_rect_Type1 h1 h2 h3 h4 h5 hterm in hcut __
181
182(** val status_class_inv_rect_Type0 :
183    status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
184    -> (__ -> 'a1) -> 'a1 **)
185let status_class_inv_rect_Type0 hterm h1 h2 h3 h4 h5 =
186  let hcut = status_class_rect_Type0 h1 h2 h3 h4 h5 hterm in hcut __
187
188(** val status_class_discr : status_class -> status_class -> __ **)
189let status_class_discr x y =
190  Logic.eq_rect_Type2 x
191    (match x with
192     | Cl_return -> Obj.magic (fun _ dH -> dH)
193     | Cl_jump -> Obj.magic (fun _ dH -> dH)
194     | Cl_call -> Obj.magic (fun _ dH -> dH)
195     | Cl_tailcall -> Obj.magic (fun _ dH -> dH)
196     | Cl_other -> Obj.magic (fun _ dH -> dH)) y
197
198(** val status_class_jmdiscr : status_class -> status_class -> __ **)
199let status_class_jmdiscr x y =
200  Logic.eq_rect_Type2 x
201    (match x with
202     | Cl_return -> Obj.magic (fun _ dH -> dH)
203     | Cl_jump -> Obj.magic (fun _ dH -> dH)
204     | Cl_call -> Obj.magic (fun _ dH -> dH)
205     | Cl_tailcall -> Obj.magic (fun _ dH -> dH)
206     | Cl_other -> Obj.magic (fun _ dH -> dH)) y
207
208type abstract_status = { as_pc : Deqsets.deqSet; as_pc_of : (__ -> __);
209                         as_classify : (__ -> status_class);
210                         as_label_of_pc : (__ -> CostLabel.costlabel
211                                          Types.option);
212                         as_result : (__ -> Integers.int Types.option);
213                         as_call_ident : (__ Types.sig0 -> AST.ident);
214                         as_tailcall_ident : (__ Types.sig0 -> AST.ident) }
215
216(** val abstract_status_rect_Type4 :
217    (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
218    -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
219    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
220    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
221let rec abstract_status_rect_Type4 h_mk_abstract_status x_22380 =
222  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
223    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
224    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22380
225  in
226  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
227    as_result0 as_call_ident0 as_tailcall_ident0
228
229(** val abstract_status_rect_Type5 :
230    (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
231    -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
232    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
233    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
234let rec abstract_status_rect_Type5 h_mk_abstract_status x_22382 =
235  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
236    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
237    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22382
238  in
239  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
240    as_result0 as_call_ident0 as_tailcall_ident0
241
242(** val abstract_status_rect_Type3 :
243    (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
244    -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
245    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
246    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
247let rec abstract_status_rect_Type3 h_mk_abstract_status x_22384 =
248  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
249    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
250    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22384
251  in
252  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
253    as_result0 as_call_ident0 as_tailcall_ident0
254
255(** val abstract_status_rect_Type2 :
256    (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
257    -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
258    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
259    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
260let rec abstract_status_rect_Type2 h_mk_abstract_status x_22386 =
261  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
262    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
263    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22386
264  in
265  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
266    as_result0 as_call_ident0 as_tailcall_ident0
267
268(** val abstract_status_rect_Type1 :
269    (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
270    -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
271    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
272    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
273let rec abstract_status_rect_Type1 h_mk_abstract_status x_22388 =
274  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
275    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
276    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22388
277  in
278  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
279    as_result0 as_call_ident0 as_tailcall_ident0
280
281(** val abstract_status_rect_Type0 :
282    (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
283    -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
284    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
285    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
286let rec abstract_status_rect_Type0 h_mk_abstract_status x_22390 =
287  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
288    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
289    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22390
290  in
291  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
292    as_result0 as_call_ident0 as_tailcall_ident0
293
294type as_status = __
295
296(** val as_pc : abstract_status -> Deqsets.deqSet **)
297let rec as_pc xxx =
298  xxx.as_pc
299
300(** val as_pc_of : abstract_status -> __ -> __ **)
301let rec as_pc_of xxx =
302  xxx.as_pc_of
303
304(** val as_classify : abstract_status -> __ -> status_class **)
305let rec as_classify xxx =
306  xxx.as_classify
307
308(** val as_label_of_pc :
309    abstract_status -> __ -> CostLabel.costlabel Types.option **)
310let rec as_label_of_pc xxx =
311  xxx.as_label_of_pc
312
313(** val as_result : abstract_status -> __ -> Integers.int Types.option **)
314let rec as_result xxx =
315  xxx.as_result
316
317(** val as_call_ident : abstract_status -> __ Types.sig0 -> AST.ident **)
318let rec as_call_ident xxx =
319  xxx.as_call_ident
320
321(** val as_tailcall_ident : abstract_status -> __ Types.sig0 -> AST.ident **)
322let rec as_tailcall_ident xxx =
323  xxx.as_tailcall_ident
324
325(** val abstract_status_inv_rect_Type4 :
326    abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
327    status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
328    Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
329    Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
330let abstract_status_inv_rect_Type4 hterm h1 =
331  let hcut = abstract_status_rect_Type4 h1 hterm in hcut __
332
333(** val abstract_status_inv_rect_Type3 :
334    abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
335    status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
336    Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
337    Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
338let abstract_status_inv_rect_Type3 hterm h1 =
339  let hcut = abstract_status_rect_Type3 h1 hterm in hcut __
340
341(** val abstract_status_inv_rect_Type2 :
342    abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
343    status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
344    Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
345    Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
346let abstract_status_inv_rect_Type2 hterm h1 =
347  let hcut = abstract_status_rect_Type2 h1 hterm in hcut __
348
349(** val abstract_status_inv_rect_Type1 :
350    abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
351    status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
352    Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
353    Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
354let abstract_status_inv_rect_Type1 hterm h1 =
355  let hcut = abstract_status_rect_Type1 h1 hterm in hcut __
356
357(** val abstract_status_inv_rect_Type0 :
358    abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
359    status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
360    Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
361    Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
362let abstract_status_inv_rect_Type0 hterm h1 =
363  let hcut = abstract_status_rect_Type0 h1 hterm in hcut __
364
365(** val abstract_status_jmdiscr :
366    abstract_status -> abstract_status -> __ **)
367let abstract_status_jmdiscr x y =
368  Logic.eq_rect_Type2 x
369    (let { as_pc = a2; as_pc_of = a3; as_classify = a4; as_label_of_pc = a5;
370       as_result = a7; as_call_ident = a8; as_tailcall_ident = a9 } = x
371     in
372    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)) y
373
374(** val as_label :
375    abstract_status -> __ -> CostLabel.costlabel Types.option **)
376let as_label s s0 =
377  s.as_label_of_pc (s.as_pc_of s0)
378
379(** val as_costed_exc : abstract_status -> __ -> (__, __) Types.sum **)
380let as_costed_exc s s0 =
381  match as_label s s0 with
382  | Types.None -> Types.Inr __
383  | Types.Some c -> Types.Inl __
384
385type as_cost_label = CostLabel.costlabel Types.sig0
386
387type as_cost_labels = as_cost_label List.list
388
389(** val as_cost_get_label :
390    abstract_status -> as_cost_label -> CostLabel.costlabel **)
391let as_cost_get_label s l_sig =
392  Types.pi1 l_sig
393
394type as_cost_map = as_cost_label -> Nat.nat
395
396(** val as_label_safe : abstract_status -> __ Types.sig0 -> as_cost_label **)
397let as_label_safe a_s st_sig =
398  Option.opt_safe (as_label a_s (Types.pi1 st_sig))
399
400(** val lift_sigma_map_id :
401    'a2 -> ('a1 -> (__, __) Types.sum) -> ('a1 Types.sig0 -> 'a2) -> 'a1
402    Types.sig0 -> 'a2 **)
403let lift_sigma_map_id dflt dec m a_sig =
404  match dec (Types.pi1 a_sig) with
405  | Types.Inl _ -> m (Types.pi1 a_sig)
406  | Types.Inr _ -> dflt
407
408(** val lift_cost_map_id :
409    abstract_status -> abstract_status -> (CostLabel.costlabel -> (__, __)
410    Types.sum) -> as_cost_map -> as_cost_map **)
411let lift_cost_map_id s_in s_out =
412  lift_sigma_map_id Nat.O
413
414type trace_ends_with_ret =
415| Ends_with_ret
416| Doesnt_end_with_ret
417
418(** val trace_ends_with_ret_rect_Type4 :
419    'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
420let rec trace_ends_with_ret_rect_Type4 h_ends_with_ret h_doesnt_end_with_ret = function
421| Ends_with_ret -> h_ends_with_ret
422| Doesnt_end_with_ret -> h_doesnt_end_with_ret
423
424(** val trace_ends_with_ret_rect_Type5 :
425    'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
426let rec trace_ends_with_ret_rect_Type5 h_ends_with_ret h_doesnt_end_with_ret = function
427| Ends_with_ret -> h_ends_with_ret
428| Doesnt_end_with_ret -> h_doesnt_end_with_ret
429
430(** val trace_ends_with_ret_rect_Type3 :
431    'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
432let rec trace_ends_with_ret_rect_Type3 h_ends_with_ret h_doesnt_end_with_ret = function
433| Ends_with_ret -> h_ends_with_ret
434| Doesnt_end_with_ret -> h_doesnt_end_with_ret
435
436(** val trace_ends_with_ret_rect_Type2 :
437    'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
438let rec trace_ends_with_ret_rect_Type2 h_ends_with_ret h_doesnt_end_with_ret = function
439| Ends_with_ret -> h_ends_with_ret
440| Doesnt_end_with_ret -> h_doesnt_end_with_ret
441
442(** val trace_ends_with_ret_rect_Type1 :
443    'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
444let rec trace_ends_with_ret_rect_Type1 h_ends_with_ret h_doesnt_end_with_ret = function
445| Ends_with_ret -> h_ends_with_ret
446| Doesnt_end_with_ret -> h_doesnt_end_with_ret
447
448(** val trace_ends_with_ret_rect_Type0 :
449    'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
450let rec trace_ends_with_ret_rect_Type0 h_ends_with_ret h_doesnt_end_with_ret = function
451| Ends_with_ret -> h_ends_with_ret
452| Doesnt_end_with_ret -> h_doesnt_end_with_ret
453
454(** val trace_ends_with_ret_inv_rect_Type4 :
455    trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
456let trace_ends_with_ret_inv_rect_Type4 hterm h1 h2 =
457  let hcut = trace_ends_with_ret_rect_Type4 h1 h2 hterm in hcut __
458
459(** val trace_ends_with_ret_inv_rect_Type3 :
460    trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
461let trace_ends_with_ret_inv_rect_Type3 hterm h1 h2 =
462  let hcut = trace_ends_with_ret_rect_Type3 h1 h2 hterm in hcut __
463
464(** val trace_ends_with_ret_inv_rect_Type2 :
465    trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
466let trace_ends_with_ret_inv_rect_Type2 hterm h1 h2 =
467  let hcut = trace_ends_with_ret_rect_Type2 h1 h2 hterm in hcut __
468
469(** val trace_ends_with_ret_inv_rect_Type1 :
470    trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
471let trace_ends_with_ret_inv_rect_Type1 hterm h1 h2 =
472  let hcut = trace_ends_with_ret_rect_Type1 h1 h2 hterm in hcut __
473
474(** val trace_ends_with_ret_inv_rect_Type0 :
475    trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
476let trace_ends_with_ret_inv_rect_Type0 hterm h1 h2 =
477  let hcut = trace_ends_with_ret_rect_Type0 h1 h2 hterm in hcut __
478
479(** val trace_ends_with_ret_discr :
480    trace_ends_with_ret -> trace_ends_with_ret -> __ **)
481let trace_ends_with_ret_discr x y =
482  Logic.eq_rect_Type2 x
483    (match x with
484     | Ends_with_ret -> Obj.magic (fun _ dH -> dH)
485     | Doesnt_end_with_ret -> Obj.magic (fun _ dH -> dH)) y
486
487(** val trace_ends_with_ret_jmdiscr :
488    trace_ends_with_ret -> trace_ends_with_ret -> __ **)
489let trace_ends_with_ret_jmdiscr x y =
490  Logic.eq_rect_Type2 x
491    (match x with
492     | Ends_with_ret -> Obj.magic (fun _ dH -> dH)
493     | Doesnt_end_with_ret -> Obj.magic (fun _ dH -> dH)) y
494
495type trace_label_return =
496| Tlr_base of __ * __ * trace_label_label
497| Tlr_step of __ * __ * __ * trace_label_label * trace_label_return
498and trace_label_label =
499| Tll_base of trace_ends_with_ret * __ * __ * trace_any_label
500and trace_any_label =
501| Tal_base_not_return of __ * __
502| Tal_base_return of __ * __
503| Tal_base_call of __ * __ * __ * trace_label_return
504| Tal_base_tailcall of __ * __ * __ * trace_label_return
505| Tal_step_call of trace_ends_with_ret * __ * __ * __ * __
506   * trace_label_return * trace_any_label
507| Tal_step_default of trace_ends_with_ret * __ * __ * __ * trace_any_label
508
509(** val trace_label_return_inv_rect_Type4 :
510    abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
511    trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
512    trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
513let trace_label_return_inv_rect_Type4 x1 x2 x3 hterm h1 h2 =
514  let hcut =
515    match hterm with
516    | Tlr_base (x, x0, x4) -> h1 x x0 x4
517    | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
518  in
519  hcut __ __ __
520
521(** val trace_label_return_inv_rect_Type3 :
522    abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
523    trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
524    trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
525let trace_label_return_inv_rect_Type3 x1 x2 x3 hterm h1 h2 =
526  let hcut =
527    match hterm with
528    | Tlr_base (x, x0, x4) -> h1 x x0 x4
529    | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
530  in
531  hcut __ __ __
532
533(** val trace_label_return_inv_rect_Type2 :
534    abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
535    trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
536    trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
537let trace_label_return_inv_rect_Type2 x1 x2 x3 hterm h1 h2 =
538  let hcut =
539    match hterm with
540    | Tlr_base (x, x0, x4) -> h1 x x0 x4
541    | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
542  in
543  hcut __ __ __
544
545(** val trace_label_return_inv_rect_Type1 :
546    abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
547    trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
548    trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
549let trace_label_return_inv_rect_Type1 x1 x2 x3 hterm h1 h2 =
550  let hcut =
551    match hterm with
552    | Tlr_base (x, x0, x4) -> h1 x x0 x4
553    | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
554  in
555  hcut __ __ __
556
557(** val trace_label_return_inv_rect_Type0 :
558    abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
559    trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
560    trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
561let trace_label_return_inv_rect_Type0 x1 x2 x3 hterm h1 h2 =
562  let hcut =
563    match hterm with
564    | Tlr_base (x, x0, x4) -> h1 x x0 x4
565    | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
566  in
567  hcut __ __ __
568
569(** val trace_label_label_inv_rect_Type4 :
570    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
571    -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
572    -> __ -> __ -> 'a1) -> 'a1 **)
573let trace_label_label_inv_rect_Type4 x1 x2 x3 x4 hterm h1 =
574  let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
575  hcut __ __ __ __
576
577(** val trace_label_label_inv_rect_Type3 :
578    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
579    -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
580    -> __ -> __ -> 'a1) -> 'a1 **)
581let trace_label_label_inv_rect_Type3 x1 x2 x3 x4 hterm h1 =
582  let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
583  hcut __ __ __ __
584
585(** val trace_label_label_inv_rect_Type2 :
586    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
587    -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
588    -> __ -> __ -> 'a1) -> 'a1 **)
589let trace_label_label_inv_rect_Type2 x1 x2 x3 x4 hterm h1 =
590  let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
591  hcut __ __ __ __
592
593(** val trace_label_label_inv_rect_Type1 :
594    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
595    -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
596    -> __ -> __ -> 'a1) -> 'a1 **)
597let trace_label_label_inv_rect_Type1 x1 x2 x3 x4 hterm h1 =
598  let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
599  hcut __ __ __ __
600
601(** val trace_label_label_inv_rect_Type0 :
602    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
603    -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
604    -> __ -> __ -> 'a1) -> 'a1 **)
605let trace_label_label_inv_rect_Type0 x1 x2 x3 x4 hterm h1 =
606  let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
607  hcut __ __ __ __
608
609(** val trace_any_label_inv_rect_Type4 :
610    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
611    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
612    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
613    __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
614    (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
615    -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
616    -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
617    'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
618    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
619let trace_any_label_inv_rect_Type4 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
620  let hcut =
621    match hterm with
622    | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
623    | Tal_base_return (x, x0) -> h2 x x0 __ __
624    | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
625    | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
626    | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
627      h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
628    | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
629  in
630  hcut __ __ __ __
631
632(** val trace_any_label_inv_rect_Type3 :
633    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
634    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
635    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
636    __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
637    (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
638    -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
639    -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
640    'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
641    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
642let trace_any_label_inv_rect_Type3 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
643  let hcut =
644    match hterm with
645    | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
646    | Tal_base_return (x, x0) -> h2 x x0 __ __
647    | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
648    | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
649    | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
650      h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
651    | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
652  in
653  hcut __ __ __ __
654
655(** val trace_any_label_inv_rect_Type2 :
656    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
657    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
658    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
659    __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
660    (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
661    -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
662    -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
663    'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
664    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
665let trace_any_label_inv_rect_Type2 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
666  let hcut =
667    match hterm with
668    | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
669    | Tal_base_return (x, x0) -> h2 x x0 __ __
670    | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
671    | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
672    | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
673      h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
674    | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
675  in
676  hcut __ __ __ __
677
678(** val trace_any_label_inv_rect_Type1 :
679    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
680    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
681    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
682    __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
683    (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
684    -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
685    -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
686    'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
687    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
688let trace_any_label_inv_rect_Type1 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
689  let hcut =
690    match hterm with
691    | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
692    | Tal_base_return (x, x0) -> h2 x x0 __ __
693    | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
694    | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
695    | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
696      h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
697    | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
698  in
699  hcut __ __ __ __
700
701(** val trace_any_label_inv_rect_Type0 :
702    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
703    (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
704    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
705    __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
706    (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
707    -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
708    -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
709    'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
710    -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
711let trace_any_label_inv_rect_Type0 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
712  let hcut =
713    match hterm with
714    | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
715    | Tal_base_return (x, x0) -> h2 x x0 __ __
716    | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
717    | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
718    | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
719      h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
720    | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
721  in
722  hcut __ __ __ __
723
724(** val trace_label_return_discr :
725    abstract_status -> __ -> __ -> trace_label_return -> trace_label_return
726    -> __ **)
727let trace_label_return_discr a1 a2 a3 x y =
728  Logic.eq_rect_Type2 x
729    (match x with
730     | Tlr_base (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
731     | Tlr_step (a0, a10, a20, a30, a4) ->
732       Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
733
734(** val trace_label_label_discr :
735    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
736    -> trace_label_label -> __ **)
737let trace_label_label_discr a1 a2 a3 a4 x y =
738  Logic.eq_rect_Type2 x
739    (let Tll_base (a0, a10, a20, a30) = x in
740    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
741
742(** val trace_label_return_jmdiscr :
743    abstract_status -> __ -> __ -> trace_label_return -> trace_label_return
744    -> __ **)
745let trace_label_return_jmdiscr a1 a2 a3 x y =
746  Logic.eq_rect_Type2 x
747    (match x with
748     | Tlr_base (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
749     | Tlr_step (a0, a10, a20, a30, a4) ->
750       Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
751
752(** val trace_label_label_jmdiscr :
753    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
754    -> trace_label_label -> __ **)
755let trace_label_label_jmdiscr a1 a2 a3 a4 x y =
756  Logic.eq_rect_Type2 x
757    (let Tll_base (a0, a10, a20, a30) = x in
758    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
759
760(** val trace_any_label_jmdiscr :
761    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
762    trace_any_label -> __ **)
763let trace_any_label_jmdiscr a1 a2 a3 a4 x y =
764  Logic.eq_rect_Type2 x
765    (match x with
766     | Tal_base_not_return (a0, a10) ->
767       Obj.magic (fun _ dH -> dH __ __ __ __ __)
768     | Tal_base_return (a0, a10) -> Obj.magic (fun _ dH -> dH __ __ __ __)
769     | Tal_base_call (a0, a10, a20, a6) ->
770       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)
771     | Tal_base_tailcall (a0, a10, a20, a5) ->
772       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
773     | Tal_step_call (a0, a10, a20, a30, a40, a8, a100) ->
774       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)
775     | Tal_step_default (a0, a10, a20, a30, a5) ->
776       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)) y
777
778(** val tal_pc_list :
779    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
780    __ List.list **)
781let rec tal_pc_list s fl st1 st2 = function
782| Tal_base_not_return (pre, x) -> List.Cons ((s.as_pc_of pre), List.Nil)
783| Tal_base_return (pre, x) -> List.Cons ((s.as_pc_of pre), List.Nil)
784| Tal_base_call (pre, x, x0, x4) -> List.Cons ((s.as_pc_of pre), List.Nil)
785| Tal_base_tailcall (pre, x, x0, x3) ->
786  List.Cons ((s.as_pc_of pre), List.Nil)
787| Tal_step_call (fl', pre, x, st1', st2', x3, tl) ->
788  List.Cons ((s.as_pc_of pre), (tal_pc_list s fl' st1' st2' tl))
789| Tal_step_default (fl', pre, st1', st2', tl) ->
790  List.Cons ((s.as_pc_of pre), (tal_pc_list s fl' st1' st2' tl))
791
792(** val as_trace_any_label_length' :
793    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
794    Nat.nat **)
795let as_trace_any_label_length' s trace_ends_flag start_status final_status the_trace =
796  List.length
797    (tal_pc_list s trace_ends_flag start_status final_status the_trace)
798
799(** val tll_hd_label :
800    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
801    -> CostLabel.costlabel **)
802let tll_hd_label s fl st1 st2 tr =
803  (let Tll_base (x, st1', x0, x1) = tr in
804  (fun _ _ _ _ -> Types.pi1 (as_label_safe s st1'))) __ __ __ __
805
806(** val tlr_hd_label :
807    abstract_status -> __ -> __ -> trace_label_return -> CostLabel.costlabel **)
808let tlr_hd_label s st1 st2 = function
809| Tlr_base (st1', st2', tll) -> tll_hd_label s Ends_with_ret st1' st2' tll
810| Tlr_step (st1', st2', x, tll, x0) ->
811  tll_hd_label s Doesnt_end_with_ret st1' st2' tll
812
813type trace_any_call =
814| Tac_base of __
815| Tac_step_call of __ * __ * __ * __ * trace_label_return * trace_any_call
816| Tac_step_default of __ * __ * __ * trace_any_call
817
818(** val trace_any_call_rect_Type4 :
819    abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
820    -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
821    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
822    __ -> trace_any_call -> 'a1 **)
823let rec trace_any_call_rect_Type4 s h_tac_base h_tac_step_call h_tac_step_default x_22468 x_22467 = function
824| Tac_base status -> h_tac_base status __
825| Tac_step_call
826    (status_pre_fun_call, status_after_fun_call, status_final,
827     status_start_fun_call, x_22473, x_22471) ->
828  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
829    status_start_fun_call __ __ __ x_22473 __ x_22471
830    (trace_any_call_rect_Type4 s h_tac_base h_tac_step_call
831      h_tac_step_default status_after_fun_call status_final x_22471)
832| Tac_step_default (status_pre, status_end, status_init, x_22478) ->
833  h_tac_step_default status_pre status_end status_init __ x_22478 __ __
834    (trace_any_call_rect_Type4 s h_tac_base h_tac_step_call
835      h_tac_step_default status_init status_end x_22478)
836
837(** val trace_any_call_rect_Type3 :
838    abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
839    -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
840    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
841    __ -> trace_any_call -> 'a1 **)
842let rec trace_any_call_rect_Type3 s h_tac_base h_tac_step_call h_tac_step_default x_22500 x_22499 = function
843| Tac_base status -> h_tac_base status __
844| Tac_step_call
845    (status_pre_fun_call, status_after_fun_call, status_final,
846     status_start_fun_call, x_22505, x_22503) ->
847  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
848    status_start_fun_call __ __ __ x_22505 __ x_22503
849    (trace_any_call_rect_Type3 s h_tac_base h_tac_step_call
850      h_tac_step_default status_after_fun_call status_final x_22503)
851| Tac_step_default (status_pre, status_end, status_init, x_22510) ->
852  h_tac_step_default status_pre status_end status_init __ x_22510 __ __
853    (trace_any_call_rect_Type3 s h_tac_base h_tac_step_call
854      h_tac_step_default status_init status_end x_22510)
855
856(** val trace_any_call_rect_Type2 :
857    abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
858    -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
859    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
860    __ -> trace_any_call -> 'a1 **)
861let rec trace_any_call_rect_Type2 s h_tac_base h_tac_step_call h_tac_step_default x_22516 x_22515 = function
862| Tac_base status -> h_tac_base status __
863| Tac_step_call
864    (status_pre_fun_call, status_after_fun_call, status_final,
865     status_start_fun_call, x_22521, x_22519) ->
866  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
867    status_start_fun_call __ __ __ x_22521 __ x_22519
868    (trace_any_call_rect_Type2 s h_tac_base h_tac_step_call
869      h_tac_step_default status_after_fun_call status_final x_22519)
870| Tac_step_default (status_pre, status_end, status_init, x_22526) ->
871  h_tac_step_default status_pre status_end status_init __ x_22526 __ __
872    (trace_any_call_rect_Type2 s h_tac_base h_tac_step_call
873      h_tac_step_default status_init status_end x_22526)
874
875(** val trace_any_call_rect_Type1 :
876    abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
877    -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
878    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
879    __ -> trace_any_call -> 'a1 **)
880let rec trace_any_call_rect_Type1 s h_tac_base h_tac_step_call h_tac_step_default x_22532 x_22531 = function
881| Tac_base status -> h_tac_base status __
882| Tac_step_call
883    (status_pre_fun_call, status_after_fun_call, status_final,
884     status_start_fun_call, x_22537, x_22535) ->
885  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
886    status_start_fun_call __ __ __ x_22537 __ x_22535
887    (trace_any_call_rect_Type1 s h_tac_base h_tac_step_call
888      h_tac_step_default status_after_fun_call status_final x_22535)
889| Tac_step_default (status_pre, status_end, status_init, x_22542) ->
890  h_tac_step_default status_pre status_end status_init __ x_22542 __ __
891    (trace_any_call_rect_Type1 s h_tac_base h_tac_step_call
892      h_tac_step_default status_init status_end x_22542)
893
894(** val trace_any_call_rect_Type0 :
895    abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
896    -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
897    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
898    __ -> trace_any_call -> 'a1 **)
899let rec trace_any_call_rect_Type0 s h_tac_base h_tac_step_call h_tac_step_default x_22548 x_22547 = function
900| Tac_base status -> h_tac_base status __
901| Tac_step_call
902    (status_pre_fun_call, status_after_fun_call, status_final,
903     status_start_fun_call, x_22553, x_22551) ->
904  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
905    status_start_fun_call __ __ __ x_22553 __ x_22551
906    (trace_any_call_rect_Type0 s h_tac_base h_tac_step_call
907      h_tac_step_default status_after_fun_call status_final x_22551)
908| Tac_step_default (status_pre, status_end, status_init, x_22558) ->
909  h_tac_step_default status_pre status_end status_init __ x_22558 __ __
910    (trace_any_call_rect_Type0 s h_tac_base h_tac_step_call
911      h_tac_step_default status_init status_end x_22558)
912
913(** val trace_any_call_inv_rect_Type4 :
914    abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
915    __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
916    trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
917    __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
918    -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
919let trace_any_call_inv_rect_Type4 x1 x2 x3 hterm h1 h2 h3 =
920  let hcut = trace_any_call_rect_Type4 x1 h1 h2 h3 x2 x3 hterm in
921  hcut __ __ __
922
923(** val trace_any_call_inv_rect_Type3 :
924    abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
925    __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
926    trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
927    __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
928    -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
929let trace_any_call_inv_rect_Type3 x1 x2 x3 hterm h1 h2 h3 =
930  let hcut = trace_any_call_rect_Type3 x1 h1 h2 h3 x2 x3 hterm in
931  hcut __ __ __
932
933(** val trace_any_call_inv_rect_Type2 :
934    abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
935    __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
936    trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
937    __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
938    -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
939let trace_any_call_inv_rect_Type2 x1 x2 x3 hterm h1 h2 h3 =
940  let hcut = trace_any_call_rect_Type2 x1 h1 h2 h3 x2 x3 hterm in
941  hcut __ __ __
942
943(** val trace_any_call_inv_rect_Type1 :
944    abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
945    __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
946    trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
947    __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
948    -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
949let trace_any_call_inv_rect_Type1 x1 x2 x3 hterm h1 h2 h3 =
950  let hcut = trace_any_call_rect_Type1 x1 h1 h2 h3 x2 x3 hterm in
951  hcut __ __ __
952
953(** val trace_any_call_inv_rect_Type0 :
954    abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
955    __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
956    trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
957    __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
958    -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
959let trace_any_call_inv_rect_Type0 x1 x2 x3 hterm h1 h2 h3 =
960  let hcut = trace_any_call_rect_Type0 x1 h1 h2 h3 x2 x3 hterm in
961  hcut __ __ __
962
963(** val trace_any_call_jmdiscr :
964    abstract_status -> __ -> __ -> trace_any_call -> trace_any_call -> __ **)
965let trace_any_call_jmdiscr a1 a2 a3 x y =
966  Logic.eq_rect_Type2 x
967    (match x with
968     | Tac_base a0 -> Obj.magic (fun _ dH -> dH __ __)
969     | Tac_step_call (a0, a10, a20, a30, a7, a9) ->
970       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)
971     | Tac_step_default (a0, a10, a20, a4) ->
972       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
973
974type trace_label_call =
975| Tlc_base of __ * __ * trace_any_call
976
977(** val trace_label_call_rect_Type4 :
978    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
979    -> trace_label_call -> 'a1 **)
980let rec trace_label_call_rect_Type4 s h_tlc_base x_22666 x_22665 = function
981| Tlc_base (start_status, end_status, x_22669) ->
982  h_tlc_base start_status end_status x_22669 __
983
984(** val trace_label_call_rect_Type5 :
985    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
986    -> trace_label_call -> 'a1 **)
987let rec trace_label_call_rect_Type5 s h_tlc_base x_22672 x_22671 = function
988| Tlc_base (start_status, end_status, x_22675) ->
989  h_tlc_base start_status end_status x_22675 __
990
991(** val trace_label_call_rect_Type3 :
992    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
993    -> trace_label_call -> 'a1 **)
994let rec trace_label_call_rect_Type3 s h_tlc_base x_22678 x_22677 = function
995| Tlc_base (start_status, end_status, x_22681) ->
996  h_tlc_base start_status end_status x_22681 __
997
998(** val trace_label_call_rect_Type2 :
999    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
1000    -> trace_label_call -> 'a1 **)
1001let rec trace_label_call_rect_Type2 s h_tlc_base x_22684 x_22683 = function
1002| Tlc_base (start_status, end_status, x_22687) ->
1003  h_tlc_base start_status end_status x_22687 __
1004
1005(** val trace_label_call_rect_Type1 :
1006    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
1007    -> trace_label_call -> 'a1 **)
1008let rec trace_label_call_rect_Type1 s h_tlc_base x_22690 x_22689 = function
1009| Tlc_base (start_status, end_status, x_22693) ->
1010  h_tlc_base start_status end_status x_22693 __
1011
1012(** val trace_label_call_rect_Type0 :
1013    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
1014    -> trace_label_call -> 'a1 **)
1015let rec trace_label_call_rect_Type0 s h_tlc_base x_22696 x_22695 = function
1016| Tlc_base (start_status, end_status, x_22699) ->
1017  h_tlc_base start_status end_status x_22699 __
1018
1019(** val trace_label_call_inv_rect_Type4 :
1020    abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1021    trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1022let trace_label_call_inv_rect_Type4 x1 x2 x3 hterm h1 =
1023  let hcut = trace_label_call_rect_Type4 x1 h1 x2 x3 hterm in hcut __ __ __
1024
1025(** val trace_label_call_inv_rect_Type3 :
1026    abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1027    trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1028let trace_label_call_inv_rect_Type3 x1 x2 x3 hterm h1 =
1029  let hcut = trace_label_call_rect_Type3 x1 h1 x2 x3 hterm in hcut __ __ __
1030
1031(** val trace_label_call_inv_rect_Type2 :
1032    abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1033    trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1034let trace_label_call_inv_rect_Type2 x1 x2 x3 hterm h1 =
1035  let hcut = trace_label_call_rect_Type2 x1 h1 x2 x3 hterm in hcut __ __ __
1036
1037(** val trace_label_call_inv_rect_Type1 :
1038    abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1039    trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1040let trace_label_call_inv_rect_Type1 x1 x2 x3 hterm h1 =
1041  let hcut = trace_label_call_rect_Type1 x1 h1 x2 x3 hterm in hcut __ __ __
1042
1043(** val trace_label_call_inv_rect_Type0 :
1044    abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1045    trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1046let trace_label_call_inv_rect_Type0 x1 x2 x3 hterm h1 =
1047  let hcut = trace_label_call_rect_Type0 x1 h1 x2 x3 hterm in hcut __ __ __
1048
1049(** val trace_label_call_discr :
1050    abstract_status -> __ -> __ -> trace_label_call -> trace_label_call -> __ **)
1051let trace_label_call_discr a1 a2 a3 x y =
1052  Logic.eq_rect_Type2 x
1053    (let Tlc_base (a0, a10, a20) = x in
1054    Obj.magic (fun _ dH -> dH __ __ __ __)) y
1055
1056(** val trace_label_call_jmdiscr :
1057    abstract_status -> __ -> __ -> trace_label_call -> trace_label_call -> __ **)
1058let trace_label_call_jmdiscr a1 a2 a3 x y =
1059  Logic.eq_rect_Type2 x
1060    (let Tlc_base (a0, a10, a20) = x in
1061    Obj.magic (fun _ dH -> dH __ __ __ __)) y
1062
1063(** val tlc_hd_label :
1064    abstract_status -> __ -> __ -> trace_label_call -> CostLabel.costlabel **)
1065let tlc_hd_label s st1 st2 tr =
1066  (let Tlc_base (st1', x, x0) = tr in
1067  (fun _ _ _ -> Types.pi1 (as_label_safe s st1'))) __ __ __
1068
1069type trace_label_diverges = __trace_label_diverges Lazy.t
1070and __trace_label_diverges =
1071| Tld_step of __ * __ * trace_label_label * trace_label_diverges
1072| Tld_base of __ * __ * __ * trace_label_call * trace_label_diverges
1073
1074(** val trace_label_diverges_inv_rect_Type4 :
1075    abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1076    trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1077    __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1078    __ -> 'a1) -> 'a1 **)
1079let trace_label_diverges_inv_rect_Type4 x1 x2 hterm h1 h2 =
1080  let hcut =
1081    match Lazy.force
1082    hterm with
1083    | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1084    | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1085  in
1086  hcut __ __
1087
1088(** val trace_label_diverges_inv_rect_Type3 :
1089    abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1090    trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1091    __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1092    __ -> 'a1) -> 'a1 **)
1093let trace_label_diverges_inv_rect_Type3 x1 x2 hterm h1 h2 =
1094  let hcut =
1095    match Lazy.force
1096    hterm with
1097    | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1098    | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1099  in
1100  hcut __ __
1101
1102(** val trace_label_diverges_inv_rect_Type2 :
1103    abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1104    trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1105    __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1106    __ -> 'a1) -> 'a1 **)
1107let trace_label_diverges_inv_rect_Type2 x1 x2 hterm h1 h2 =
1108  let hcut =
1109    match Lazy.force
1110    hterm with
1111    | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1112    | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1113  in
1114  hcut __ __
1115
1116(** val trace_label_diverges_inv_rect_Type1 :
1117    abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1118    trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1119    __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1120    __ -> 'a1) -> 'a1 **)
1121let trace_label_diverges_inv_rect_Type1 x1 x2 hterm h1 h2 =
1122  let hcut =
1123    match Lazy.force
1124    hterm with
1125    | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1126    | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1127  in
1128  hcut __ __
1129
1130(** val trace_label_diverges_inv_rect_Type0 :
1131    abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1132    trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1133    __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1134    __ -> 'a1) -> 'a1 **)
1135let trace_label_diverges_inv_rect_Type0 x1 x2 hterm h1 h2 =
1136  let hcut =
1137    match Lazy.force
1138    hterm with
1139    | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1140    | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1141  in
1142  hcut __ __
1143
1144(** val trace_label_diverges_jmdiscr :
1145    abstract_status -> __ -> trace_label_diverges -> trace_label_diverges ->
1146    __ **)
1147let trace_label_diverges_jmdiscr a1 a2 x y =
1148  Logic.eq_rect_Type2 x
1149    (match Lazy.force
1150     x with
1151     | Tld_step (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1152     | Tld_base (a0, a10, a20, a3, a6) ->
1153       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
1154
1155(** val tld_hd_label :
1156    abstract_status -> __ -> trace_label_diverges -> CostLabel.costlabel **)
1157let tld_hd_label s st tr =
1158  match Lazy.force
1159  tr with
1160  | Tld_step (st', st'', tll, x) ->
1161    tll_hd_label s Doesnt_end_with_ret st' st'' tll
1162  | Tld_base (st', st'', x, tlc, x2) -> tlc_hd_label s st' st'' tlc
1163
1164type trace_whole_program =
1165| Twp_terminating of __ * __ * __ * trace_label_return
1166| Twp_diverges of __ * __ * trace_label_diverges
1167
1168(** val trace_whole_program_rect_Type4 :
1169    abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1170    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1171    -> trace_whole_program -> 'a1 **)
1172let rec trace_whole_program_rect_Type4 s h_twp_terminating h_twp_diverges x_22748 = function
1173| Twp_terminating
1174    (status_initial, status_start_fun, status_final, x_22751) ->
1175  h_twp_terminating status_initial status_start_fun status_final __ __
1176    x_22751 __
1177| Twp_diverges (status_initial, status_start_fun, x_22754) ->
1178  h_twp_diverges status_initial status_start_fun __ __ x_22754
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 **)
1184let rec trace_whole_program_rect_Type5 s h_twp_terminating h_twp_diverges x_22759 = function
1185| Twp_terminating
1186    (status_initial, status_start_fun, status_final, x_22762) ->
1187  h_twp_terminating status_initial status_start_fun status_final __ __
1188    x_22762 __
1189| Twp_diverges (status_initial, status_start_fun, x_22765) ->
1190  h_twp_diverges status_initial status_start_fun __ __ x_22765
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 **)
1196let rec trace_whole_program_rect_Type3 s h_twp_terminating h_twp_diverges x_22770 = function
1197| Twp_terminating
1198    (status_initial, status_start_fun, status_final, x_22773) ->
1199  h_twp_terminating status_initial status_start_fun status_final __ __
1200    x_22773 __
1201| Twp_diverges (status_initial, status_start_fun, x_22776) ->
1202  h_twp_diverges status_initial status_start_fun __ __ x_22776
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 **)
1208let rec trace_whole_program_rect_Type2 s h_twp_terminating h_twp_diverges x_22781 = function
1209| Twp_terminating
1210    (status_initial, status_start_fun, status_final, x_22784) ->
1211  h_twp_terminating status_initial status_start_fun status_final __ __
1212    x_22784 __
1213| Twp_diverges (status_initial, status_start_fun, x_22787) ->
1214  h_twp_diverges status_initial status_start_fun __ __ x_22787
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 **)
1220let rec trace_whole_program_rect_Type1 s h_twp_terminating h_twp_diverges x_22792 = function
1221| Twp_terminating
1222    (status_initial, status_start_fun, status_final, x_22795) ->
1223  h_twp_terminating status_initial status_start_fun status_final __ __
1224    x_22795 __
1225| Twp_diverges (status_initial, status_start_fun, x_22798) ->
1226  h_twp_diverges status_initial status_start_fun __ __ x_22798
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 **)
1232let rec trace_whole_program_rect_Type0 s h_twp_terminating h_twp_diverges x_22803 = function
1233| Twp_terminating
1234    (status_initial, status_start_fun, status_final, x_22806) ->
1235  h_twp_terminating status_initial status_start_fun status_final __ __
1236    x_22806 __
1237| Twp_diverges (status_initial, status_start_fun, x_22809) ->
1238  h_twp_diverges status_initial status_start_fun __ __ x_22809
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 =
1288  Types.pi1 (as_label_safe s st2)
1289
1290(** val tll_tl_label :
1291    abstract_status -> __ -> __ -> trace_label_label -> CostLabel.costlabel **)
1292let tll_tl_label s st1 st2 tr =
1293  Types.pi1 (as_label_safe s st2)
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 **)
1302let rec trace_any_any_rect_Type4 s h_taa_base h_taa_step x_23033 x_23032 = function
1303| Taa_base st -> h_taa_base st
1304| Taa_step (st1, st2, st3, x_23035) ->
1305  h_taa_step st1 st2 st3 __ __ __ x_23035
1306    (trace_any_any_rect_Type4 s h_taa_base h_taa_step st2 st3 x_23035)
1307
1308(** val trace_any_any_rect_Type3 :
1309    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1310    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
1311let rec trace_any_any_rect_Type3 s h_taa_base h_taa_step x_23051 x_23050 = function
1312| Taa_base st -> h_taa_base st
1313| Taa_step (st1, st2, st3, x_23053) ->
1314  h_taa_step st1 st2 st3 __ __ __ x_23053
1315    (trace_any_any_rect_Type3 s h_taa_base h_taa_step st2 st3 x_23053)
1316
1317(** val trace_any_any_rect_Type2 :
1318    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1319    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
1320let rec trace_any_any_rect_Type2 s h_taa_base h_taa_step x_23060 x_23059 = function
1321| Taa_base st -> h_taa_base st
1322| Taa_step (st1, st2, st3, x_23062) ->
1323  h_taa_step st1 st2 st3 __ __ __ x_23062
1324    (trace_any_any_rect_Type2 s h_taa_base h_taa_step st2 st3 x_23062)
1325
1326(** val trace_any_any_rect_Type1 :
1327    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1328    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
1329let rec trace_any_any_rect_Type1 s h_taa_base h_taa_step x_23069 x_23068 = function
1330| Taa_base st -> h_taa_base st
1331| Taa_step (st1, st2, st3, x_23071) ->
1332  h_taa_step st1 st2 st3 __ __ __ x_23071
1333    (trace_any_any_rect_Type1 s h_taa_base h_taa_step st2 st3 x_23071)
1334
1335(** val trace_any_any_rect_Type0 :
1336    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1337    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
1338let rec trace_any_any_rect_Type0 s h_taa_base h_taa_step x_23078 x_23077 = function
1339| Taa_base st -> h_taa_base st
1340| Taa_step (st1, st2, st3, x_23080) ->
1341  h_taa_step st1 st2 st3 __ __ __ x_23080
1342    (trace_any_any_rect_Type0 s h_taa_base h_taa_step st2 st3 x_23080)
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
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
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
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
1453
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
1458| IEVcost x_23151 -> h_IEVcost x_23151
1459| IEVcall x_23152 -> h_IEVcall x_23152
1460| IEVtailcall (x_23154, x_23153) -> h_IEVtailcall x_23154 x_23153
1461| IEVret x_23155 -> h_IEVret x_23155
1462
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
1467| IEVcost x_23161 -> h_IEVcost x_23161
1468| IEVcall x_23162 -> h_IEVcall x_23162
1469| IEVtailcall (x_23164, x_23163) -> h_IEVtailcall x_23164 x_23163
1470| IEVret x_23165 -> h_IEVret x_23165
1471
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
1476| IEVcost x_23171 -> h_IEVcost x_23171
1477| IEVcall x_23172 -> h_IEVcall x_23172
1478| IEVtailcall (x_23174, x_23173) -> h_IEVtailcall x_23174 x_23173
1479| IEVret x_23175 -> h_IEVret x_23175
1480
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
1485| IEVcost x_23181 -> h_IEVcost x_23181
1486| IEVcall x_23182 -> h_IEVcall x_23182
1487| IEVtailcall (x_23184, x_23183) -> h_IEVtailcall x_23184 x_23183
1488| IEVret x_23185 -> h_IEVret x_23185
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
1494| IEVcost x_23191 -> h_IEVcost x_23191
1495| IEVcall x_23192 -> h_IEVcall x_23192
1496| IEVtailcall (x_23194, x_23193) -> h_IEVtailcall x_23194 x_23193
1497| IEVret x_23195 -> h_IEVret x_23195
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
1503| IEVcost x_23201 -> h_IEVcost x_23201
1504| IEVcall x_23202 -> h_IEVcall x_23202
1505| IEVtailcall (x_23204, x_23203) -> h_IEVtailcall x_23204 x_23203
1506| IEVret x_23205 -> h_IEVret x_23205
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
1690(** val flatten_trace_label_label :
1691    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
1692    -> as_cost_label List.list **)
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
1698(** val flatten_trace_any_label :
1699    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
1700    as_cost_label List.list **)
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)
1705
1706type trace_any_any_free =
1707| Taaf_base of __
1708| Taaf_step of __ * __ * __ * trace_any_any
1709| Taaf_step_jump of __ * __ * __ * trace_any_any
1710
1711(** val trace_any_any_free_rect_Type4 :
1712    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1713    -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1714    'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1715let rec trace_any_any_free_rect_Type4 s h_taaf_base h_taaf_step h_taaf_step_jump x_23284 x_23283 = function
1716| Taaf_base s0 -> h_taaf_base s0
1717| Taaf_step (s1, s2, s3, x_23288) -> h_taaf_step s1 s2 s3 x_23288 __ __
1718| Taaf_step_jump (s1, s2, s3, x_23292) ->
1719  h_taaf_step_jump s1 s2 s3 x_23292 __ __ __
1720
1721(** val trace_any_any_free_rect_Type5 :
1722    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1723    -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1724    'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1725let rec trace_any_any_free_rect_Type5 s h_taaf_base h_taaf_step h_taaf_step_jump x_23297 x_23296 = function
1726| Taaf_base s0 -> h_taaf_base s0
1727| Taaf_step (s1, s2, s3, x_23301) -> h_taaf_step s1 s2 s3 x_23301 __ __
1728| Taaf_step_jump (s1, s2, s3, x_23305) ->
1729  h_taaf_step_jump s1 s2 s3 x_23305 __ __ __
1730
1731(** val trace_any_any_free_rect_Type3 :
1732    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1733    -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1734    'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1735let rec trace_any_any_free_rect_Type3 s h_taaf_base h_taaf_step h_taaf_step_jump x_23310 x_23309 = function
1736| Taaf_base s0 -> h_taaf_base s0
1737| Taaf_step (s1, s2, s3, x_23314) -> h_taaf_step s1 s2 s3 x_23314 __ __
1738| Taaf_step_jump (s1, s2, s3, x_23318) ->
1739  h_taaf_step_jump s1 s2 s3 x_23318 __ __ __
1740
1741(** val trace_any_any_free_rect_Type2 :
1742    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1743    -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1744    'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1745let rec trace_any_any_free_rect_Type2 s h_taaf_base h_taaf_step h_taaf_step_jump x_23323 x_23322 = function
1746| Taaf_base s0 -> h_taaf_base s0
1747| Taaf_step (s1, s2, s3, x_23327) -> h_taaf_step s1 s2 s3 x_23327 __ __
1748| Taaf_step_jump (s1, s2, s3, x_23331) ->
1749  h_taaf_step_jump s1 s2 s3 x_23331 __ __ __
1750
1751(** val trace_any_any_free_rect_Type1 :
1752    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1753    -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1754    'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1755let rec trace_any_any_free_rect_Type1 s h_taaf_base h_taaf_step h_taaf_step_jump x_23336 x_23335 = function
1756| Taaf_base s0 -> h_taaf_base s0
1757| Taaf_step (s1, s2, s3, x_23340) -> h_taaf_step s1 s2 s3 x_23340 __ __
1758| Taaf_step_jump (s1, s2, s3, x_23344) ->
1759  h_taaf_step_jump s1 s2 s3 x_23344 __ __ __
1760
1761(** val trace_any_any_free_rect_Type0 :
1762    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1763    -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1764    'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1765let rec trace_any_any_free_rect_Type0 s h_taaf_base h_taaf_step h_taaf_step_jump x_23349 x_23348 = function
1766| Taaf_base s0 -> h_taaf_base s0
1767| Taaf_step (s1, s2, s3, x_23353) -> h_taaf_step s1 s2 s3 x_23353 __ __
1768| Taaf_step_jump (s1, s2, s3, x_23357) ->
1769  h_taaf_step_jump s1 s2 s3 x_23357 __ __ __
1770
1771(** val trace_any_any_free_inv_rect_Type4 :
1772    abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
1773    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1774    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1775    __ -> __ -> 'a1) -> 'a1 **)
1776let trace_any_any_free_inv_rect_Type4 x1 x2 x3 hterm h1 h2 h3 =
1777  let hcut = trace_any_any_free_rect_Type4 x1 h1 h2 h3 x2 x3 hterm in
1778  hcut __ __ __
1779
1780(** val trace_any_any_free_inv_rect_Type3 :
1781    abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
1782    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1783    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1784    __ -> __ -> 'a1) -> 'a1 **)
1785let trace_any_any_free_inv_rect_Type3 x1 x2 x3 hterm h1 h2 h3 =
1786  let hcut = trace_any_any_free_rect_Type3 x1 h1 h2 h3 x2 x3 hterm in
1787  hcut __ __ __
1788
1789(** val trace_any_any_free_inv_rect_Type2 :
1790    abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
1791    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1792    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1793    __ -> __ -> 'a1) -> 'a1 **)
1794let trace_any_any_free_inv_rect_Type2 x1 x2 x3 hterm h1 h2 h3 =
1795  let hcut = trace_any_any_free_rect_Type2 x1 h1 h2 h3 x2 x3 hterm in
1796  hcut __ __ __
1797
1798(** val trace_any_any_free_inv_rect_Type1 :
1799    abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
1800    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1801    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1802    __ -> __ -> 'a1) -> 'a1 **)
1803let trace_any_any_free_inv_rect_Type1 x1 x2 x3 hterm h1 h2 h3 =
1804  let hcut = trace_any_any_free_rect_Type1 x1 h1 h2 h3 x2 x3 hterm in
1805  hcut __ __ __
1806
1807(** val trace_any_any_free_inv_rect_Type0 :
1808    abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
1809    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1810    __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1811    __ -> __ -> 'a1) -> 'a1 **)
1812let trace_any_any_free_inv_rect_Type0 x1 x2 x3 hterm h1 h2 h3 =
1813  let hcut = trace_any_any_free_rect_Type0 x1 h1 h2 h3 x2 x3 hterm in
1814  hcut __ __ __
1815
1816(** val trace_any_any_free_jmdiscr :
1817    abstract_status -> __ -> __ -> trace_any_any_free -> trace_any_any_free
1818    -> __ **)
1819let trace_any_any_free_jmdiscr a1 a2 a3 x y =
1820  Logic.eq_rect_Type2 x
1821    (match x with
1822     | Taaf_base a0 -> Obj.magic (fun _ dH -> dH __)
1823     | Taaf_step (a0, a10, a20, a30) ->
1824       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
1825     | Taaf_step_jump (a0, a10, a20, a30) ->
1826       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
1827
1828(** val taaf_non_empty :
1829    abstract_status -> __ -> __ -> trace_any_any_free -> Bool.bool **)
1830let taaf_non_empty s s1 s2 = function
1831| Taaf_base x -> Bool.False
1832| Taaf_step (x, x0, x1, x2) -> Bool.True
1833| Taaf_step_jump (x, x0, x1, x2) -> Bool.True
1834
1835(** val taa_append_taa :
1836    abstract_status -> __ -> __ -> __ -> trace_any_any -> trace_any_any ->
1837    trace_any_any **)
1838let rec taa_append_taa s st1 st2 st3 taa =
1839  (match taa with
1840   | Taa_base st1' -> (fun st30 taa2 -> taa2)
1841   | Taa_step (st1', st2', st3', tl) ->
1842     (fun st30 taa2 -> Taa_step (st1', st2', st30,
1843       (taa_append_taa s st2' st3' st30 tl taa2)))) st3
1844
1845(** val taaf_to_taa :
1846    abstract_status -> __ -> __ -> trace_any_any_free -> trace_any_any **)
1847let taaf_to_taa s s1 s2 taaf =
1848  (match taaf with
1849   | Taaf_base s0 -> (fun _ -> Taa_base s0)
1850   | Taaf_step (s10, s20, s3, taa) ->
1851     (fun _ ->
1852       taa_append_taa s s10 s20 s3 taa (Taa_step (s20, s3, s3, (Taa_base
1853         s3))))
1854   | Taaf_step_jump (s10, s20, s3, taa) ->
1855     (fun _ -> assert false (* absurd case *))) __
1856
1857(** val taaf_append_tal :
1858    abstract_status -> __ -> trace_ends_with_ret -> __ -> __ ->
1859    trace_any_any_free -> trace_any_label -> trace_any_label **)
1860let taaf_append_tal s st1 fl st2 st3 taaf =
1861  taa_append_tal s st1 fl st2 st3 (taaf_to_taa s st1 st2 taaf)
1862
1863(** val taaf_append_taa :
1864    abstract_status -> __ -> __ -> __ -> trace_any_any_free -> trace_any_any
1865    -> trace_any_any **)
1866let taaf_append_taa s st1 st2 st3 taaf =
1867  taa_append_taa s st1 st2 st3 (taaf_to_taa s st1 st2 taaf)
1868
1869(** val taaf_cons :
1870    abstract_status -> __ -> __ -> __ -> trace_any_any_free ->
1871    trace_any_any_free **)
1872let taaf_cons s s1 s2 s3 tl =
1873  (match tl with
1874   | Taaf_base s20 -> (fun _ _ -> Taaf_step (s1, s1, s20, (Taa_base s1)))
1875   | Taaf_step (s20, s30, s4, taa) ->
1876     (fun _ _ -> Taaf_step (s1, s30, s4, (Taa_step (s1, s20, s30, taa))))
1877   | Taaf_step_jump (s20, s30, s4, taa) ->
1878     (fun _ _ -> Taaf_step_jump (s1, s30, s4, (Taa_step (s1, s20, s30,
1879       taa))))) __ __
1880
1881(** val taaf_append_taaf :
1882    abstract_status -> __ -> __ -> __ -> trace_any_any_free ->
1883    trace_any_any_free -> trace_any_any_free **)
1884let taaf_append_taaf s st1 st2 st3 taaf1 taaf2 =
1885  (match taaf2 with
1886   | Taaf_base s1 -> (fun taaf10 _ -> taaf10)
1887   | Taaf_step (s1, s2, s3, taa) ->
1888     (fun taaf10 _ -> Taaf_step (st1, s2, s3,
1889       (taaf_append_taa s st1 s1 s2 taaf10 taa)))
1890   | Taaf_step_jump (s2, s3, s4, taa) ->
1891     (fun taaf10 _ -> Taaf_step_jump (st1, s3, s4,
1892       (taaf_append_taa s st1 s2 s3 taaf10 taa)))) taaf1 __
1893
Note: See TracBrowser for help on using the repository browser.