source: extracted/structuredTraces.ml @ 2730

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

Exported again.

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