source: extracted/rTLabs_traces.ml @ 2743

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 91.3 KB
Line 
1open Preamble
2
3open Deqsets_extra
4
5open CostSpec
6
7open Sets
8
9open Listb
10
11open StructuredTraces
12
13open Graphs
14
15open Order
16
17open Registers
18
19open FrontEndOps
20
21open RTLabs_syntax
22
23open SmallstepExec
24
25open BitVectorTrie
26
27open CostLabel
28
29open Events
30
31open IOMonad
32
33open IO
34
35open Extra_bool
36
37open Coqlib
38
39open Values
40
41open FrontEndVal
42
43open Hide
44
45open ByteValues
46
47open Division
48
49open Z
50
51open BitVectorZ
52
53open Pointers
54
55open GenMem
56
57open FrontEndMem
58
59open Proper
60
61open PositiveMap
62
63open Deqsets
64
65open Extralib
66
67open Lists
68
69open Identifiers
70
71open Exp
72
73open Arithmetic
74
75open Vector
76
77open Div_and_mod
78
79open Util
80
81open FoldStuff
82
83open BitVector
84
85open Extranat
86
87open Integers
88
89open AST
90
91open Globalenvs
92
93open ErrorMessages
94
95open Option
96
97open Setoids
98
99open Monad
100
101open Jmeq
102
103open Russell
104
105open Positive
106
107open PreIdentifiers
108
109open Errors
110
111open Bool
112
113open Relations
114
115open Nat
116
117open Hints_declaration
118
119open Core_notation
120
121open Pts
122
123open Logic
124
125open Types
126
127open List
128
129open RTLabs_semantics
130
131open RTLabs_abstract
132
133open CostMisc
134
135open Executions
136
137open Listb_extra
138
139type ('o, 'i) flat_trace = ('o, 'i) __flat_trace Lazy.t
140and ('o, 'i) __flat_trace =
141| Ft_stop of RTLabs_semantics.state0
142| Ft_step of RTLabs_semantics.state0 * Events.trace * RTLabs_semantics.state0
143   * ('o, 'i) flat_trace
144
145(** val flat_trace_inv_rect_Type4 :
146    RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
147    -> (RTLabs_semantics.state0 -> __ -> __ -> __ -> 'a3) ->
148    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
149    -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **)
150let flat_trace_inv_rect_Type4 x3 x4 hterm h1 h2 =
151  let hcut =
152    match Lazy.force
153    hterm with
154    | Ft_stop x -> h1 x __
155    | Ft_step (x, x0, x1, x2) -> h2 x x0 x1 __ x2
156  in
157  hcut __ __
158
159(** val flat_trace_inv_rect_Type3 :
160    RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
161    -> (RTLabs_semantics.state0 -> __ -> __ -> __ -> 'a3) ->
162    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
163    -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **)
164let flat_trace_inv_rect_Type3 x3 x4 hterm h1 h2 =
165  let hcut =
166    match Lazy.force
167    hterm with
168    | Ft_stop x -> h1 x __
169    | Ft_step (x, x0, x1, x2) -> h2 x x0 x1 __ x2
170  in
171  hcut __ __
172
173(** val flat_trace_inv_rect_Type2 :
174    RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
175    -> (RTLabs_semantics.state0 -> __ -> __ -> __ -> 'a3) ->
176    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
177    -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **)
178let flat_trace_inv_rect_Type2 x3 x4 hterm h1 h2 =
179  let hcut =
180    match Lazy.force
181    hterm with
182    | Ft_stop x -> h1 x __
183    | Ft_step (x, x0, x1, x2) -> h2 x x0 x1 __ x2
184  in
185  hcut __ __
186
187(** val flat_trace_inv_rect_Type1 :
188    RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
189    -> (RTLabs_semantics.state0 -> __ -> __ -> __ -> 'a3) ->
190    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
191    -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **)
192let flat_trace_inv_rect_Type1 x3 x4 hterm h1 h2 =
193  let hcut =
194    match Lazy.force
195    hterm with
196    | Ft_stop x -> h1 x __
197    | Ft_step (x, x0, x1, x2) -> h2 x x0 x1 __ x2
198  in
199  hcut __ __
200
201(** val flat_trace_inv_rect_Type0 :
202    RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
203    -> (RTLabs_semantics.state0 -> __ -> __ -> __ -> 'a3) ->
204    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
205    -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **)
206let flat_trace_inv_rect_Type0 x3 x4 hterm h1 h2 =
207  let hcut =
208    match Lazy.force
209    hterm with
210    | Ft_stop x -> h1 x __
211    | Ft_step (x, x0, x1, x2) -> h2 x x0 x1 __ x2
212  in
213  hcut __ __
214
215(** val flat_trace_discr :
216    RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
217    -> ('a1, 'a2) flat_trace -> __ **)
218let flat_trace_discr a3 a4 x y =
219  Logic.eq_rect_Type2 x
220    (match Lazy.force
221     x with
222     | Ft_stop a0 -> Obj.magic (fun _ dH -> dH __ __)
223     | Ft_step (a0, a10, a20, a40) ->
224       Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
225
226(** val flat_trace_jmdiscr :
227    RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
228    -> ('a1, 'a2) flat_trace -> __ **)
229let flat_trace_jmdiscr a3 a4 x y =
230  Logic.eq_rect_Type2 x
231    (match Lazy.force
232     x with
233     | Ft_stop a0 -> Obj.magic (fun _ dH -> dH __ __)
234     | Ft_step (a0, a10, a20, a40) ->
235       Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
236
237(** val make_flat_trace :
238    __ -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace **)
239let rec make_flat_trace ge s =
240  let e1 =
241    SmallstepExec.exec_inf_aux
242      RTLabs_semantics.rTLabs_fullexec.SmallstepExec.es1 ge
243      (Obj.magic (RTLabs_semantics.eval_statement (Obj.magic ge) s))
244  in
245  (match Lazy.force
246   e1 with
247   | SmallstepExec.E_stop (tr, i, s') ->
248     (fun _ -> lazy (Ft_step (s, tr, (Obj.magic s'), (lazy (Ft_stop
249       (Obj.magic s'))))))
250   | SmallstepExec.E_step (tr, s', e') ->
251     (fun _ -> lazy (Ft_step (s, tr, (Obj.magic s'),
252       (make_flat_trace ge (Obj.magic s')))))
253   | SmallstepExec.E_wrong m -> (fun _ -> assert false (* absurd case *))
254   | SmallstepExec.E_interact (o, f) ->
255     (fun _ -> assert false (* absurd case *))) __
256
257(** val make_whole_flat_trace :
258    __ -> __ -> (IO.io_out, IO.io_in) flat_trace **)
259let make_whole_flat_trace p s =
260  let ge = RTLabs_semantics.rTLabs_fullexec.SmallstepExec.make_global p in
261  let e1 =
262    SmallstepExec.exec_inf_aux
263      RTLabs_semantics.rTLabs_fullexec.SmallstepExec.es1 ge (IOMonad.Value
264      { Types.fst = Events.e0; Types.snd = s })
265  in
266  (match Lazy.force
267   e1 with
268   | SmallstepExec.E_stop (tr, i, s') ->
269     (fun _ -> lazy (Ft_stop (Obj.magic s)))
270   | SmallstepExec.E_step (x, x0, e') ->
271     (fun _ -> make_flat_trace ge (Obj.magic s))
272   | SmallstepExec.E_wrong m -> (fun _ -> assert false (* absurd case *))
273   | SmallstepExec.E_interact (o, f) ->
274     (fun _ -> assert false (* absurd case *))) __
275
276type will_return =
277| Wr_step of RTLabs_semantics.state0 * Events.trace * RTLabs_semantics.state0
278   * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
279| Wr_call of RTLabs_semantics.state0 * Events.trace * RTLabs_semantics.state0
280   * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
281| Wr_ret of RTLabs_semantics.state0 * Events.trace * RTLabs_semantics.state0
282   * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
283| Wr_base of RTLabs_semantics.state0 * Events.trace * RTLabs_semantics.state0
284   * (IO.io_out, IO.io_in) flat_trace
285
286(** val will_return_rect_Type4 :
287    RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
288    RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
289    flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
290    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
291    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
292    'a1 -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
293    RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
294    flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
295    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
296    -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1) -> Nat.nat ->
297    RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace ->
298    will_return -> 'a1 **)
299let rec will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17438 s x_17437 = function
300| Wr_step (s0, tr, s', depth, trace0, x_17440) ->
301  h_wr_step s0 tr s' depth __ trace0 __ x_17440
302    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
303      s' trace0 x_17440)
304| Wr_call (s0, tr, s', depth, trace0, x_17442) ->
305  h_wr_call s0 tr s' depth __ trace0 __ x_17442
306    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
307      depth) s' trace0 x_17442)
308| Wr_ret (s0, tr, s', depth, trace0, x_17444) ->
309  h_wr_ret s0 tr s' depth __ trace0 __ x_17444
310    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
311      s' trace0 x_17444)
312| Wr_base (s0, tr, s', trace0) -> h_wr_base s0 tr s' __ trace0 __
313
314(** val will_return_rect_Type3 :
315    RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
316    RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
317    flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
318    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
319    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
320    'a1 -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
321    RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
322    flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
323    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
324    -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1) -> Nat.nat ->
325    RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace ->
326    will_return -> 'a1 **)
327let rec will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17466 s x_17465 = function
328| Wr_step (s0, tr, s', depth, trace0, x_17468) ->
329  h_wr_step s0 tr s' depth __ trace0 __ x_17468
330    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
331      s' trace0 x_17468)
332| Wr_call (s0, tr, s', depth, trace0, x_17470) ->
333  h_wr_call s0 tr s' depth __ trace0 __ x_17470
334    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
335      depth) s' trace0 x_17470)
336| Wr_ret (s0, tr, s', depth, trace0, x_17472) ->
337  h_wr_ret s0 tr s' depth __ trace0 __ x_17472
338    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
339      s' trace0 x_17472)
340| Wr_base (s0, tr, s', trace0) -> h_wr_base s0 tr s' __ trace0 __
341
342(** val will_return_rect_Type2 :
343    RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
344    RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
345    flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
346    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
347    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
348    'a1 -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
349    RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
350    flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
351    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
352    -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1) -> Nat.nat ->
353    RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace ->
354    will_return -> 'a1 **)
355let rec will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17480 s x_17479 = function
356| Wr_step (s0, tr, s', depth, trace0, x_17482) ->
357  h_wr_step s0 tr s' depth __ trace0 __ x_17482
358    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
359      s' trace0 x_17482)
360| Wr_call (s0, tr, s', depth, trace0, x_17484) ->
361  h_wr_call s0 tr s' depth __ trace0 __ x_17484
362    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
363      depth) s' trace0 x_17484)
364| Wr_ret (s0, tr, s', depth, trace0, x_17486) ->
365  h_wr_ret s0 tr s' depth __ trace0 __ x_17486
366    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
367      s' trace0 x_17486)
368| Wr_base (s0, tr, s', trace0) -> h_wr_base s0 tr s' __ trace0 __
369
370(** val will_return_rect_Type1 :
371    RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
372    RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
373    flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
374    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
375    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
376    'a1 -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
377    RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
378    flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
379    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
380    -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1) -> Nat.nat ->
381    RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace ->
382    will_return -> 'a1 **)
383let rec will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17494 s x_17493 = function
384| Wr_step (s0, tr, s', depth, trace0, x_17496) ->
385  h_wr_step s0 tr s' depth __ trace0 __ x_17496
386    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
387      s' trace0 x_17496)
388| Wr_call (s0, tr, s', depth, trace0, x_17498) ->
389  h_wr_call s0 tr s' depth __ trace0 __ x_17498
390    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
391      depth) s' trace0 x_17498)
392| Wr_ret (s0, tr, s', depth, trace0, x_17500) ->
393  h_wr_ret s0 tr s' depth __ trace0 __ x_17500
394    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
395      s' trace0 x_17500)
396| Wr_base (s0, tr, s', trace0) -> h_wr_base s0 tr s' __ trace0 __
397
398(** val will_return_rect_Type0 :
399    RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
400    RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
401    flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
402    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
403    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
404    'a1 -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
405    RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
406    flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
407    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
408    -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1) -> Nat.nat ->
409    RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace ->
410    will_return -> 'a1 **)
411let rec will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17508 s x_17507 = function
412| Wr_step (s0, tr, s', depth, trace0, x_17510) ->
413  h_wr_step s0 tr s' depth __ trace0 __ x_17510
414    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
415      s' trace0 x_17510)
416| Wr_call (s0, tr, s', depth, trace0, x_17512) ->
417  h_wr_call s0 tr s' depth __ trace0 __ x_17512
418    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
419      depth) s' trace0 x_17512)
420| Wr_ret (s0, tr, s', depth, trace0, x_17514) ->
421  h_wr_ret s0 tr s' depth __ trace0 __ x_17514
422    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
423      s' trace0 x_17514)
424| Wr_base (s0, tr, s', trace0) -> h_wr_base s0 tr s' __ trace0 __
425
426(** val will_return_inv_rect_Type4 :
427    RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
428    (IO.io_out, IO.io_in) flat_trace -> will_return ->
429    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
430    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
431    (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
432    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
433    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
434    (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
435    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
436    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
437    (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
438    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
439    -> (IO.io_out, IO.io_in) flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1)
440    -> 'a1 **)
441let will_return_inv_rect_Type4 x1 x2 x3 x4 hterm h1 h2 h3 h4 =
442  let hcut = will_return_rect_Type4 x1 h1 h2 h3 h4 x2 x3 x4 hterm in
443  hcut __ __ __ __
444
445(** val will_return_inv_rect_Type3 :
446    RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
447    (IO.io_out, IO.io_in) flat_trace -> will_return ->
448    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
449    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
450    (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
451    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
452    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
453    (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
454    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
455    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
456    (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
457    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
458    -> (IO.io_out, IO.io_in) flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1)
459    -> 'a1 **)
460let will_return_inv_rect_Type3 x1 x2 x3 x4 hterm h1 h2 h3 h4 =
461  let hcut = will_return_rect_Type3 x1 h1 h2 h3 h4 x2 x3 x4 hterm in
462  hcut __ __ __ __
463
464(** val will_return_inv_rect_Type2 :
465    RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
466    (IO.io_out, IO.io_in) flat_trace -> will_return ->
467    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
468    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
469    (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
470    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
471    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
472    (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
473    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
474    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
475    (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
476    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
477    -> (IO.io_out, IO.io_in) flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1)
478    -> 'a1 **)
479let will_return_inv_rect_Type2 x1 x2 x3 x4 hterm h1 h2 h3 h4 =
480  let hcut = will_return_rect_Type2 x1 h1 h2 h3 h4 x2 x3 x4 hterm in
481  hcut __ __ __ __
482
483(** val will_return_inv_rect_Type1 :
484    RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
485    (IO.io_out, IO.io_in) flat_trace -> will_return ->
486    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
487    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
488    (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
489    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
490    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
491    (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
492    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
493    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
494    (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
495    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
496    -> (IO.io_out, IO.io_in) flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1)
497    -> 'a1 **)
498let will_return_inv_rect_Type1 x1 x2 x3 x4 hterm h1 h2 h3 h4 =
499  let hcut = will_return_rect_Type1 x1 h1 h2 h3 h4 x2 x3 x4 hterm in
500  hcut __ __ __ __
501
502(** val will_return_inv_rect_Type0 :
503    RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
504    (IO.io_out, IO.io_in) flat_trace -> will_return ->
505    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
506    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
507    (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
508    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
509    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
510    (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
511    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
512    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
513    (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
514    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
515    -> (IO.io_out, IO.io_in) flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1)
516    -> 'a1 **)
517let will_return_inv_rect_Type0 x1 x2 x3 x4 hterm h1 h2 h3 h4 =
518  let hcut = will_return_rect_Type0 x1 h1 h2 h3 h4 x2 x3 x4 hterm in
519  hcut __ __ __ __
520
521(** val will_return_jmdiscr :
522    RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
523    (IO.io_out, IO.io_in) flat_trace -> will_return -> will_return -> __ **)
524let will_return_jmdiscr a1 a2 a3 a4 x y =
525  Logic.eq_rect_Type2 x
526    (match x with
527     | Wr_step (a0, a10, a20, a30, a5, a7) ->
528       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)
529     | Wr_call (a0, a10, a20, a30, a5, a7) ->
530       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)
531     | Wr_ret (a0, a10, a20, a30, a5, a7) ->
532       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)
533     | Wr_base (a0, a10, a20, a40) ->
534       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
535
536(** val will_return_length :
537    RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
538    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat **)
539let rec will_return_length ge d s tr = function
540| Wr_step (x, x0, x1, x2, x4, t') ->
541  Nat.S (will_return_length ge x2 x1 x4 t')
542| Wr_call (x, x0, x1, x2, x4, t') ->
543  Nat.S (will_return_length ge (Nat.S x2) x1 x4 t')
544| Wr_ret (x, x0, x1, x2, x4, t') -> Nat.S (will_return_length ge x2 x1 x4 t')
545| Wr_base (x, x0, x1, x3) -> Nat.S Nat.O
546
547(** val will_return_end :
548    RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
549    (IO.io_out, IO.io_in) flat_trace -> will_return ->
550    (RTLabs_semantics.state0, (IO.io_out, IO.io_in) flat_trace) Types.dPair **)
551let rec will_return_end ge d s tr = function
552| Wr_step (x, x0, x1, x2, x4, t') -> will_return_end ge x2 x1 x4 t'
553| Wr_call (x, x0, x1, x2, x4, t') -> will_return_end ge (Nat.S x2) x1 x4 t'
554| Wr_ret (x, x0, x1, x2, x4, t') -> will_return_end ge x2 x1 x4 t'
555| Wr_base (x, x0, x1, tr') -> { Types.dpi1 = x1; Types.dpi2 = tr' }
556
557(** val will_return_call :
558    RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
559    Events.trace -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in)
560    flat_trace -> will_return -> will_return Types.sig0 **)
561let will_return_call ge d s tr s' trace0 tERM =
562  will_return_inv_rect_Type0 ge d s (lazy (Ft_step (s, tr, s', trace0))) tERM
563    (fun h19 h20 h21 h22 _ h24 _ h26 h27 _ _ _ _ -> assert false
564    (* absurd case *)) (fun h33 h34 h35 h36 _ h38 _ h40 h41 _ _ _ _ ->
565    Logic.eq_rect_Type0_r h36 (fun tERM0 h410 _ ->
566      Logic.eq_rect_Type0_r h33 (fun _ _ _ tERM1 h411 _ ->
567        Obj.magic flat_trace_jmdiscr ge h33 (lazy (Ft_step (h33, tr, s',
568          trace0))) (lazy (Ft_step (h33, h34, h35, h38))) __ (fun _ ->
569          Logic.streicherK h33 (fun _ ->
570            Logic.eq_rect_Type0_r h34 (fun _ _ tERM2 h412 _ _ ->
571              Logic.eq_rect_Type0_r h35 (fun trace1 _ _ tERM3 h413 _ _ ->
572                Logic.eq_rect_Type0_r __ (fun _ tERM4 h414 _ _ ->
573                  Logic.eq_rect_Type0_r h38 (fun _ tERM5 h415 _ ->
574                    Logic.streicherK (lazy (Ft_step (h33, h34, h35, h38)))
575                      (Logic.eq_rect_Type0_r (Wr_call (h33, h34, h35, h36,
576                        h38, h40)) (fun h416 -> h40) tERM5 h415)) trace1 __
577                    tERM4 h414 __) __ __ tERM3 h413 __) s' trace0 __ __ tERM2
578                h412 __) tr __ __ tERM1 h411 __))) s __ __ __ tERM0 h410 __)
579      d tERM h41 __) (fun h47 h48 h49 h50 _ h52 _ h54 h55 _ _ _ _ ->
580    assert false (* absurd case *)) (fun h61 h62 h63 _ h65 _ _ _ _ _ ->
581    assert false (* absurd case *))
582
583(** val will_return_return :
584    RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
585    Events.trace -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in)
586    flat_trace -> will_return -> __ **)
587let will_return_return ge d s tr s' trace0 tERM =
588  will_return_inv_rect_Type0 ge d s (lazy (Ft_step (s, tr, s', trace0))) tERM
589    (fun h19 h20 h21 h22 _ h24 _ h26 h27 _ _ _ _ -> assert false
590    (* absurd case *)) (fun h33 h34 h35 h36 _ h38 _ h40 h41 _ _ _ _ ->
591    assert false (* absurd case *))
592    (fun h47 h48 h49 h50 _ h52 _ h54 h55 _ _ _ _ ->
593    Logic.eq_rect_Type0_r (Nat.S h50) (fun tERM0 h550 _ ->
594      Logic.eq_rect_Type0_r h47 (fun _ _ _ tERM1 h551 _ ->
595        Obj.magic flat_trace_jmdiscr ge h47 (lazy (Ft_step (h47, tr, s',
596          trace0))) (lazy (Ft_step (h47, h48, h49, h52))) __ (fun _ ->
597          Logic.streicherK h47 (fun _ ->
598            Logic.eq_rect_Type0_r h48 (fun _ _ tERM2 h552 _ _ ->
599              Logic.eq_rect_Type0_r h49 (fun trace1 _ _ tERM3 h553 _ _ ->
600                Logic.eq_rect_Type0_r __ (fun _ tERM4 h554 _ _ ->
601                  Logic.eq_rect_Type0_r h52 (fun _ tERM5 h555 _ ->
602                    Logic.streicherK (lazy (Ft_step (h47, h48, h49, h52)))
603                      (Logic.eq_rect_Type0_r (Wr_ret (h47, h48, h49, h50,
604                        h52, h54)) (fun h556 -> h54) tERM5 h555)) trace1 __
605                    tERM4 h554 __) __ __ tERM3 h553 __) s' trace0 __ __ tERM2
606                h552 __) tr __ __ tERM1 h551 __))) s __ __ __ tERM0 h550 __)
607      d tERM h55 __) (Obj.magic __)
608
609(** val will_return_notfn :
610    RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
611    Events.trace -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in)
612    flat_trace -> (__, __) Types.sum -> will_return -> will_return Types.sig0 **)
613let will_return_notfn ge d s tr s' trace0 = function
614| Types.Inl _ ->
615  (fun tERM ->
616    will_return_inv_rect_Type0 ge d s (lazy (Ft_step (s, tr, s', trace0)))
617      tERM (fun h290 h291 h292 h293 _ h295 _ h297 h298 _ _ _ _ ->
618      Logic.eq_rect_Type0_r h293 (fun tERM0 h2980 _ ->
619        Logic.eq_rect_Type0_r h290 (fun _ _ _ tERM1 h2981 _ ->
620          Obj.magic flat_trace_jmdiscr ge h290 (lazy (Ft_step (h290, tr, s',
621            trace0))) (lazy (Ft_step (h290, h291, h292, h295))) __ (fun _ ->
622            Logic.streicherK h290 (fun _ ->
623              Logic.eq_rect_Type0_r h291 (fun _ _ tERM2 h2982 _ _ ->
624                Logic.eq_rect_Type0_r h292 (fun trace1 _ _ tERM3 h2983 _ _ ->
625                  Logic.eq_rect_Type0_r __ (fun _ tERM4 h2984 _ _ ->
626                    Logic.eq_rect_Type0_r h295 (fun _ tERM5 h2985 _ ->
627                      Logic.streicherK (lazy (Ft_step (h290, h291, h292,
628                        h295)))
629                        (Logic.eq_rect_Type0_r (Wr_step (h290, h291, h292,
630                          h293, h295, h297)) (fun h2986 -> h297) tERM5 h2985))
631                      trace1 __ tERM4 h2984 __) __ __ tERM3 h2983 __) s'
632                  trace0 __ __ tERM2 h2982 __) tr __ __ tERM1 h2981 __))) s
633          __ __ __ tERM0 h2980 __) d tERM h298 __)
634      (fun h304 h305 h306 h307 _ h309 _ h311 h312 _ _ _ _ -> assert false
635      (* absurd case *))
636      (fun h318 h319 h320 h321 _ h323 _ h325 h326 _ _ _ _ -> assert false
637      (* absurd case *)) (fun h332 h333 h334 _ h336 _ _ _ _ _ -> assert false
638      (* absurd case *)))
639| Types.Inr _ ->
640  (fun tERM ->
641    will_return_inv_rect_Type0 ge d s (lazy (Ft_step (s, tr, s', trace0)))
642      tERM (fun h343 h344 h345 h346 _ h348 _ h350 h351 _ _ _ _ ->
643      Logic.eq_rect_Type0_r h346 (fun tERM0 h3510 _ ->
644        Logic.eq_rect_Type0_r h343 (fun _ _ _ tERM1 h3511 _ ->
645          Obj.magic flat_trace_jmdiscr ge h343 (lazy (Ft_step (h343, tr, s',
646            trace0))) (lazy (Ft_step (h343, h344, h345, h348))) __ (fun _ ->
647            Logic.streicherK h343 (fun _ ->
648              Logic.eq_rect_Type0_r h344 (fun _ _ tERM2 h3512 _ _ ->
649                Logic.eq_rect_Type0_r h345 (fun trace1 _ _ tERM3 h3513 _ _ ->
650                  Logic.eq_rect_Type0_r __ (fun _ tERM4 h3514 _ _ ->
651                    Logic.eq_rect_Type0_r h348 (fun _ tERM5 h3515 _ ->
652                      Logic.streicherK (lazy (Ft_step (h343, h344, h345,
653                        h348)))
654                        (Logic.eq_rect_Type0_r (Wr_step (h343, h344, h345,
655                          h346, h348, h350)) (fun h3516 -> h350) tERM5 h3515))
656                      trace1 __ tERM4 h3514 __) __ __ tERM3 h3513 __) s'
657                  trace0 __ __ tERM2 h3512 __) tr __ __ tERM1 h3511 __))) s
658          __ __ __ tERM0 h3510 __) d tERM h351 __)
659      (fun h357 h358 h359 h360 _ h362 _ h364 h365 _ _ _ _ -> assert false
660      (* absurd case *))
661      (fun h371 h372 h373 h374 _ h376 _ h378 h379 _ _ _ _ -> assert false
662      (* absurd case *)) (fun h385 h386 h387 _ h389 _ _ _ _ _ -> assert false
663      (* absurd case *)))
664
665(** val will_return_prepend :
666    RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
667    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
668    RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace ->
669    will_return -> will_return **)
670let will_return_prepend ge d1 s1 tr1 t1 d2 s2 t2 x =
671  will_return_rect_Type0 ge (fun s tr s' depth _ t _ t0 iH d3 s3 t3 t4 _ ->
672    Wr_step (s, tr, s', (Nat.plus depth (Nat.S d3)), t, (iH d3 s3 t3 t4 __)))
673    (fun s tr s' depth _ t _ t0 iH d3 s3 t3 t4 _ -> Wr_call (s, tr, s',
674    (Nat.plus depth (Nat.S d3)), t, (iH d3 s3 t3 t4 __)))
675    (fun s tr s' depth _ t _ t0 iH s3 s20 t3 t4 _ -> Wr_ret (s, tr, s',
676    (Nat.plus depth (Nat.S s3)), t, (iH s3 s20 t3 t4 __)))
677    (fun s tr s' _ t _ d3 s3 t3 t4 _ ->
678    Obj.magic Types.dPair_discr { Types.dpi1 = s'; Types.dpi2 = t }
679      { Types.dpi1 = s3; Types.dpi2 = t3 } __ (fun _ ->
680      Logic.eq_rect_Type0_r s3 (fun _ t0 _ _ ->
681        Logic.eq_rect_Type0_r t3 (fun _ ->
682          Logic.streicherK { Types.dpi1 = s3; Types.dpi2 = t3 } (Wr_ret (s,
683            tr, s3, d3, t3, t4))) t0 __) s' __ t __)) d1 s1 tr1 t1 d2 s2 t2 x
684    __
685
686(** val nat_jmdiscr : Nat.nat -> Nat.nat -> __ **)
687let nat_jmdiscr x y =
688  Logic.eq_rect_Type2 x
689    (match x with
690     | Nat.O -> Obj.magic (fun _ dH -> dH)
691     | Nat.S a0 -> Obj.magic (fun _ dH -> dH __)) y
692
693(** val will_return_remove_call :
694    RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
695    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> will_return
696    -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace ->
697    will_return **)
698let will_return_remove_call ge d1x s1x t1x t1 d2 x s2 t2 =
699  will_return_rect_Type0 ge (fun s tr s' d1 _ t _ t0 iH d3 t3 s3 t4 _ ->
700    iH d3
701      (will_return_inv_rect_Type0 ge (Nat.plus d1 (Nat.S d3)) s
702        (lazy (Ft_step (s, tr, s', t))) t3
703        (fun h1 h2 h3 h4 _ h6 _ h8 h9 _ _ _ _ ->
704        Logic.eq_rect_Type0 (Nat.plus d1 (Nat.S d3)) (fun h80 h90 _ ->
705          Logic.eq_rect_Type0_r h1 (fun _ _ t20 _ _ h91 _ ->
706            Obj.magic flat_trace_jmdiscr ge h1 (lazy (Ft_step (h1, tr, s',
707              t))) (lazy (Ft_step (h1, h2, h3, h6))) __ (fun _ ->
708              Logic.streicherK h1 (fun _ ->
709                Logic.eq_rect_Type0_r h2 (fun _ t21 _ _ h92 _ _ ->
710                  Logic.eq_rect_Type0_r h3
711                    (fun t5 t6 iH0 _ t22 _ _ h93 _ _ ->
712                    Logic.eq_rect_Type0_r __ (fun t23 _ _ h94 _ _ ->
713                      Logic.eq_rect_Type0_r h6 (fun t7 iH1 t24 _ _ h95 _ ->
714                        Logic.streicherK (lazy (Ft_step (h1, h2, h3, h6)))
715                          (Logic.eq_rect_Type0_r (Wr_step (h1, h2, h3,
716                            (Nat.plus d1 (Nat.S d3)), h6, h80)) (fun h96 ->
717                            h80) t24 h95)) t5 t6 iH0 t23 __ __ h94 __) __ t22
718                      __ __ h93 __) s' t t0 iH __ t21 __ __ h92 __) tr __ t20
719                  __ __ h91 __))) s __ __ t3 __ __ h90 __) h4 h8 h9 __)
720        (fun h15 h16 h17 h18 _ h20 _ h22 h23 _ _ _ _ -> assert false
721        (* absurd case *)) (fun h29 h30 h31 h32 _ h34 _ h36 h37 _ _ _ _ ->
722        assert false (* absurd case *)) (fun h43 h44 h45 _ h47 _ _ _ _ _ ->
723        assert false (* absurd case *))) s3 t4 __)
724    (fun s tr s' d1 _ t _ t0 iH d3 t3 s3 t4 _ ->
725    iH d3
726      (will_return_inv_rect_Type0 ge (Nat.plus d1 (Nat.S d3)) s
727        (lazy (Ft_step (s, tr, s', t))) t3
728        (fun h1 h2 h3 h4 _ h6 _ h8 h9 _ _ _ _ -> assert false
729        (* absurd case *)) (fun h15 h16 h17 h18 _ h20 _ h22 h23 _ _ _ _ ->
730        Logic.eq_rect_Type0 (Nat.plus d1 (Nat.S d3)) (fun h220 h230 _ ->
731          Logic.eq_rect_Type0_r h15 (fun _ _ t20 _ _ h231 _ ->
732            Obj.magic flat_trace_jmdiscr ge h15 (lazy (Ft_step (h15, tr, s',
733              t))) (lazy (Ft_step (h15, h16, h17, h20))) __ (fun _ ->
734              Logic.streicherK h15 (fun _ ->
735                Logic.eq_rect_Type0_r h16 (fun _ t21 _ _ h232 _ _ ->
736                  Logic.eq_rect_Type0_r h17
737                    (fun t5 t6 iH0 _ t22 _ _ h233 _ _ ->
738                    Logic.eq_rect_Type0_r __ (fun t23 _ _ h234 _ _ ->
739                      Logic.eq_rect_Type0_r h20 (fun t7 iH1 t24 _ _ h235 _ ->
740                        Logic.streicherK (lazy (Ft_step (h15, h16, h17,
741                          h20)))
742                          (Logic.eq_rect_Type0_r (Wr_call (h15, h16, h17,
743                            (Nat.plus d1 (Nat.S d3)), h20, h220))
744                            (fun h236 -> h220) t24 h235)) t5 t6 iH0 t23 __ __
745                        h234 __) __ t22 __ __ h233 __) s' t t0 iH __ t21 __
746                    __ h232 __) tr __ t20 __ __ h231 __))) s __ __ t3 __ __
747            h230 __) h18 h22 h23 __)
748        (fun h29 h30 h31 h32 _ h34 _ h36 h37 _ _ _ _ -> assert false
749        (* absurd case *)) (fun h43 h44 h45 _ h47 _ _ _ _ _ -> assert false
750        (* absurd case *))) s3 t4 __)
751    (fun s tr s' d1 _ t _ t0 iH d3 t3 s3 t4 _ ->
752    iH d3
753      (will_return_inv_rect_Type0 ge (Nat.plus (Nat.S d1) (Nat.S d3)) s
754        (lazy (Ft_step (s, tr, s', t))) t3
755        (fun h1 h2 h3 h4 _ h6 _ h8 h9 _ _ _ _ -> assert false
756        (* absurd case *)) (fun h15 h16 h17 h18 _ h20 _ h22 h23 _ _ _ _ ->
757        assert false (* absurd case *))
758        (fun h29 h30 h31 h32 _ h34 _ h36 h37 _ _ _ _ ->
759        Obj.magic nat_jmdiscr (Nat.S (Nat.plus d1 (Nat.S d3))) (Nat.S h32) __
760          (Logic.eq_rect_Type0_r h29 (fun _ _ t20 _ h370 _ _ ->
761            Obj.magic flat_trace_jmdiscr ge h29 (lazy (Ft_step (h29, tr, s',
762              t))) (lazy (Ft_step (h29, h30, h31, h34))) __ (fun _ ->
763              Logic.streicherK h29 (fun _ ->
764                Logic.eq_rect_Type0_r h30 (fun _ t21 _ h371 _ _ _ ->
765                  Logic.eq_rect_Type0_r h31
766                    (fun t5 t6 iH0 _ t22 _ h372 _ _ _ ->
767                    Logic.eq_rect_Type0_r __ (fun t23 _ h373 _ _ _ ->
768                      Logic.eq_rect_Type0_r h34 (fun t7 iH1 t24 _ h374 _ _ ->
769                        Logic.streicherK (lazy (Ft_step (h29, h30, h31,
770                          h34))) (fun _ ->
771                          Logic.eq_rect_Type0 (Nat.plus d1 (Nat.S d3))
772                            (fun h360 _ h375 _ ->
773                            Logic.streicherK (Nat.S (Nat.plus d1 (Nat.S d3)))
774                              (Logic.eq_rect_Type0_r (Wr_ret (h29, h30, h31,
775                                (Nat.plus d1 (Nat.S d3)), h34, h360))
776                                (fun h376 -> h360) t24 h375)) h32 h36 __ h374
777                            __)) t5 t6 iH0 t23 __ h373 __ __) __ t22 __ h372
778                      __ __) s' t t0 iH __ t21 __ h371 __ __) tr __ t20 __
779                  h370 __ __))) s __ __ t3 __ h37 __ __))
780        (fun h43 h44 h45 _ h47 _ _ _ _ _ -> assert false (* absurd case *)))
781      s3 t4 __) (fun s tr s' _ t _ d3 t3 s3 t4 _ ->
782    Obj.magic Types.dPair_discr { Types.dpi1 = s'; Types.dpi2 = t }
783      { Types.dpi1 = s3; Types.dpi2 = t4 } __ (fun _ ->
784      Logic.eq_rect_Type0_r s3 (fun _ t0 t20 _ _ ->
785        Logic.eq_rect_Type0_r t4 (fun t21 _ ->
786          Logic.streicherK { Types.dpi1 = s3; Types.dpi2 = t4 }
787            (will_return_inv_rect_Type0 ge (Nat.plus Nat.O (Nat.S d3)) s
788              (lazy (Ft_step (s, tr, s3, t4))) t21
789              (fun h1 h2 h3 h4 _ h6 _ h8 h9 _ _ _ _ -> assert false
790              (* absurd case *))
791              (fun h15 h16 h17 h18 _ h20 _ h22 h23 _ _ _ _ -> assert false
792              (* absurd case *))
793              (fun h29 h30 h31 h32 _ h34 _ h36 h37 _ _ _ _ ->
794              Obj.magic nat_jmdiscr (Nat.S d3) (Nat.S h32) __
795                (Logic.eq_rect_Type0_r h29 (fun _ _ t22 h370 _ _ ->
796                  Obj.magic flat_trace_jmdiscr ge h29 (lazy (Ft_step (h29,
797                    tr, s3, t4))) (lazy (Ft_step (h29, h30, h31, h34))) __
798                    (fun _ ->
799                    Logic.streicherK h29 (fun _ ->
800                      Logic.eq_rect_Type0_r h30 (fun _ t23 h371 _ _ _ ->
801                        Logic.eq_rect_Type0_r h31
802                          (fun t24 _ t25 h372 _ _ _ ->
803                          Logic.eq_rect_Type0_r __ (fun t26 h373 _ _ _ ->
804                            Logic.eq_rect_Type0_r h34 (fun t27 h374 _ _ ->
805                              Logic.streicherK (lazy (Ft_step (h29, h30, h31,
806                                h34))) (fun _ ->
807                                Logic.eq_rect_Type0_r h32
808                                  (fun _ t28 h375 _ ->
809                                  Logic.streicherK (Nat.S h32)
810                                    (Logic.eq_rect_Type0_r (Wr_ret (h29, h30,
811                                      h31, h32, h34, h36)) (fun h376 -> h36)
812                                      t28 h375)) d3 __ t27 h374 __)) t24 t26
813                              h373 __ __) __ t25 h372 __ __) s3 t4 __ t23
814                          h371 __ __) tr __ t22 h370 __ __))) s __ __ t21 h37
815                  __ __)) (fun h43 h44 h45 _ h47 _ _ _ _ _ -> assert false
816              (* absurd case *)))) t0 t20 __) s' __ t t3 __)) d1x s1x t1x t1
817    d2 x s2 t2 __
818
819(** val will_return_lower :
820    RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
821    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> will_return **)
822let will_return_lower ge d0 s0 t0 tM d' =
823  will_return_rect_Type0 ge (fun s tr s' d _ tr0 _ tM1 iH d'0 _ -> Wr_step
824    (s, tr, s', d'0, tr0, (iH d'0 __)))
825    (fun s tr s' d _ tr0 _ tM1 iH d'0 _ -> Wr_call (s, tr, s', d'0, tr0,
826    (iH (Nat.S d'0) __))) (fun s tr s' d _ tr0 _ tM1 iH clearme ->
827    match clearme with
828    | Nat.O -> (fun _ -> Wr_base (s, tr, s', tr0))
829    | Nat.S d'0 -> (fun _ -> Wr_ret (s, tr, s', d'0, tr0, (iH d'0 __))))
830    (fun s tr s' _ tr0 _ clearme ->
831    match clearme with
832    | Nat.O -> (fun _ -> Wr_base (s, tr, s', tr0))
833    | Nat.S d'0 -> (fun _ -> assert false (* absurd case *))) d0 s0 t0 tM d'
834    __
835
836(** val list_jmdiscr : 'a1 List.list -> 'a1 List.list -> __ **)
837let list_jmdiscr x y =
838  Logic.eq_rect_Type2 x
839    (match x with
840     | List.Nil -> Obj.magic (fun _ dH -> dH)
841     | List.Cons (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
842
843type 't trace_result = { new_state : RTLabs_abstract.rTLabs_ext_state;
844                         remainder : (IO.io_out, IO.io_in) flat_trace;
845                         new_trace : 't; terminates : __ }
846
847(** val trace_result_rect_Type4 :
848    RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
849    -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
850    -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state ->
851    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
852    trace_result -> 'a2 **)
853let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_18049 =
854  let { new_state = new_state0; remainder = remainder0; new_trace =
855    new_trace0; terminates = terminates0 } = x_18049
856  in
857  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
858
859(** val trace_result_rect_Type5 :
860    RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
861    -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
862    -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state ->
863    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
864    trace_result -> 'a2 **)
865let rec trace_result_rect_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_18051 =
866  let { new_state = new_state0; remainder = remainder0; new_trace =
867    new_trace0; terminates = terminates0 } = x_18051
868  in
869  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
870
871(** val trace_result_rect_Type3 :
872    RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
873    -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
874    -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state ->
875    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
876    trace_result -> 'a2 **)
877let rec trace_result_rect_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_18053 =
878  let { new_state = new_state0; remainder = remainder0; new_trace =
879    new_trace0; terminates = terminates0 } = x_18053
880  in
881  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
882
883(** val trace_result_rect_Type2 :
884    RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
885    -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
886    -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state ->
887    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
888    trace_result -> 'a2 **)
889let rec trace_result_rect_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_18055 =
890  let { new_state = new_state0; remainder = remainder0; new_trace =
891    new_trace0; terminates = terminates0 } = x_18055
892  in
893  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
894
895(** val trace_result_rect_Type1 :
896    RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
897    -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
898    -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state ->
899    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
900    trace_result -> 'a2 **)
901let rec trace_result_rect_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_18057 =
902  let { new_state = new_state0; remainder = remainder0; new_trace =
903    new_trace0; terminates = terminates0 } = x_18057
904  in
905  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
906
907(** val trace_result_rect_Type0 :
908    RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
909    -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
910    -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state ->
911    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
912    trace_result -> 'a2 **)
913let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_18059 =
914  let { new_state = new_state0; remainder = remainder0; new_trace =
915    new_trace0; terminates = terminates0 } = x_18059
916  in
917  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
918
919(** val new_state :
920    RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
921    -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
922    -> will_return -> Nat.nat -> 'a1 trace_result ->
923    RTLabs_abstract.rTLabs_ext_state **)
924let rec new_state ge depth ends start full original_terminates limit xxx =
925  xxx.new_state
926
927(** val remainder :
928    RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
929    -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
930    -> will_return -> Nat.nat -> 'a1 trace_result -> (IO.io_out, IO.io_in)
931    flat_trace **)
932let rec remainder ge depth ends start full original_terminates limit xxx =
933  xxx.remainder
934
935(** val new_trace :
936    RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
937    -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
938    -> will_return -> Nat.nat -> 'a1 trace_result -> 'a1 **)
939let rec new_trace ge depth ends start full original_terminates limit xxx =
940  xxx.new_trace
941
942(** val terminates :
943    RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
944    -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
945    -> will_return -> Nat.nat -> 'a1 trace_result -> __ **)
946let rec terminates ge depth ends start full original_terminates limit xxx =
947  xxx.terminates
948
949(** val trace_result_inv_rect_Type4 :
950    RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
951    -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
952    -> will_return -> Nat.nat -> 'a1 trace_result ->
953    (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
954    __ -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2 **)
955let trace_result_inv_rect_Type4 x1 x2 x3 x4 x5 x6 x8 hterm h1 =
956  let hcut = trace_result_rect_Type4 x1 x2 x3 x4 x5 x6 x8 h1 hterm in hcut __
957
958(** val trace_result_inv_rect_Type3 :
959    RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
960    -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
961    -> will_return -> Nat.nat -> 'a1 trace_result ->
962    (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
963    __ -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2 **)
964let trace_result_inv_rect_Type3 x1 x2 x3 x4 x5 x6 x8 hterm h1 =
965  let hcut = trace_result_rect_Type3 x1 x2 x3 x4 x5 x6 x8 h1 hterm in hcut __
966
967(** val trace_result_inv_rect_Type2 :
968    RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
969    -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
970    -> will_return -> Nat.nat -> 'a1 trace_result ->
971    (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
972    __ -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2 **)
973let trace_result_inv_rect_Type2 x1 x2 x3 x4 x5 x6 x8 hterm h1 =
974  let hcut = trace_result_rect_Type2 x1 x2 x3 x4 x5 x6 x8 h1 hterm in hcut __
975
976(** val trace_result_inv_rect_Type1 :
977    RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
978    -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
979    -> will_return -> Nat.nat -> 'a1 trace_result ->
980    (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
981    __ -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2 **)
982let trace_result_inv_rect_Type1 x1 x2 x3 x4 x5 x6 x8 hterm h1 =
983  let hcut = trace_result_rect_Type1 x1 x2 x3 x4 x5 x6 x8 h1 hterm in hcut __
984
985(** val trace_result_inv_rect_Type0 :
986    RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
987    -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
988    -> will_return -> Nat.nat -> 'a1 trace_result ->
989    (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
990    __ -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2 **)
991let trace_result_inv_rect_Type0 x1 x2 x3 x4 x5 x6 x8 hterm h1 =
992  let hcut = trace_result_rect_Type0 x1 x2 x3 x4 x5 x6 x8 h1 hterm in hcut __
993
994(** val trace_result_jmdiscr :
995    RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
996    -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
997    -> will_return -> Nat.nat -> 'a1 trace_result -> 'a1 trace_result -> __ **)
998let trace_result_jmdiscr a1 a2 a3 a4 a5 a6 a8 x y =
999  Logic.eq_rect_Type2 x
1000    (let { new_state = a0; remainder = a10; new_trace = a30; terminates =
1001       a50 } = x
1002     in
1003    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1004
1005type 't sub_trace_result = { ends : StructuredTraces.trace_ends_with_ret;
1006                             trace_res : 't trace_result }
1007
1008(** val sub_trace_result_rect_Type4 :
1009    RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1010    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1011    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
1012    sub_trace_result -> 'a2 **)
1013let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_18077 =
1014  let { ends = ends0; trace_res = trace_res0 } = x_18077 in
1015  h_mk_sub_trace_result ends0 trace_res0
1016
1017(** val sub_trace_result_rect_Type5 :
1018    RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1019    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1020    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
1021    sub_trace_result -> 'a2 **)
1022let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_18079 =
1023  let { ends = ends0; trace_res = trace_res0 } = x_18079 in
1024  h_mk_sub_trace_result ends0 trace_res0
1025
1026(** val sub_trace_result_rect_Type3 :
1027    RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1028    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1029    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
1030    sub_trace_result -> 'a2 **)
1031let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_18081 =
1032  let { ends = ends0; trace_res = trace_res0 } = x_18081 in
1033  h_mk_sub_trace_result ends0 trace_res0
1034
1035(** val sub_trace_result_rect_Type2 :
1036    RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1037    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1038    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
1039    sub_trace_result -> 'a2 **)
1040let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_18083 =
1041  let { ends = ends0; trace_res = trace_res0 } = x_18083 in
1042  h_mk_sub_trace_result ends0 trace_res0
1043
1044(** val sub_trace_result_rect_Type1 :
1045    RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1046    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1047    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
1048    sub_trace_result -> 'a2 **)
1049let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_18085 =
1050  let { ends = ends0; trace_res = trace_res0 } = x_18085 in
1051  h_mk_sub_trace_result ends0 trace_res0
1052
1053(** val sub_trace_result_rect_Type0 :
1054    RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1055    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1056    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
1057    sub_trace_result -> 'a2 **)
1058let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_18087 =
1059  let { ends = ends0; trace_res = trace_res0 } = x_18087 in
1060  h_mk_sub_trace_result ends0 trace_res0
1061
1062(** val ends :
1063    RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1064    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1065    sub_trace_result -> StructuredTraces.trace_ends_with_ret **)
1066let rec ends ge depth start full original_terminates limit xxx =
1067  xxx.ends
1068
1069(** val trace_res :
1070    RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1071    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1072    sub_trace_result -> 'a1 trace_result **)
1073let rec trace_res ge depth start full original_terminates limit xxx =
1074  xxx.trace_res
1075
1076(** val sub_trace_result_inv_rect_Type4 :
1077    RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1078    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1079    sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
1080    trace_result -> __ -> 'a2) -> 'a2 **)
1081let sub_trace_result_inv_rect_Type4 x1 x2 x3 x4 x5 x7 hterm h1 =
1082  let hcut = sub_trace_result_rect_Type4 x1 x2 x3 x4 x5 x7 h1 hterm in
1083  hcut __
1084
1085(** val sub_trace_result_inv_rect_Type3 :
1086    RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1087    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1088    sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
1089    trace_result -> __ -> 'a2) -> 'a2 **)
1090let sub_trace_result_inv_rect_Type3 x1 x2 x3 x4 x5 x7 hterm h1 =
1091  let hcut = sub_trace_result_rect_Type3 x1 x2 x3 x4 x5 x7 h1 hterm in
1092  hcut __
1093
1094(** val sub_trace_result_inv_rect_Type2 :
1095    RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1096    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1097    sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
1098    trace_result -> __ -> 'a2) -> 'a2 **)
1099let sub_trace_result_inv_rect_Type2 x1 x2 x3 x4 x5 x7 hterm h1 =
1100  let hcut = sub_trace_result_rect_Type2 x1 x2 x3 x4 x5 x7 h1 hterm in
1101  hcut __
1102
1103(** val sub_trace_result_inv_rect_Type1 :
1104    RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1105    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1106    sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
1107    trace_result -> __ -> 'a2) -> 'a2 **)
1108let sub_trace_result_inv_rect_Type1 x1 x2 x3 x4 x5 x7 hterm h1 =
1109  let hcut = sub_trace_result_rect_Type1 x1 x2 x3 x4 x5 x7 h1 hterm in
1110  hcut __
1111
1112(** val sub_trace_result_inv_rect_Type0 :
1113    RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1114    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1115    sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
1116    trace_result -> __ -> 'a2) -> 'a2 **)
1117let sub_trace_result_inv_rect_Type0 x1 x2 x3 x4 x5 x7 hterm h1 =
1118  let hcut = sub_trace_result_rect_Type0 x1 x2 x3 x4 x5 x7 h1 hterm in
1119  hcut __
1120
1121(** val sub_trace_result_discr :
1122    RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1123    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1124    sub_trace_result -> 'a1 sub_trace_result -> __ **)
1125let sub_trace_result_discr a1 a2 a3 a4 a5 a7 x y =
1126  Logic.eq_rect_Type2 x
1127    (let { ends = a0; trace_res = a10 } = x in
1128    Obj.magic (fun _ dH -> dH __ __)) y
1129
1130(** val sub_trace_result_jmdiscr :
1131    RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1132    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1133    sub_trace_result -> 'a1 sub_trace_result -> __ **)
1134let sub_trace_result_jmdiscr a1 a2 a3 a4 a5 a7 x y =
1135  Logic.eq_rect_Type2 x
1136    (let { ends = a0; trace_res = a10 } = x in
1137    Obj.magic (fun _ dH -> dH __ __)) y
1138
1139(** val replace_trace :
1140    RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
1141    -> RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state
1142    -> (IO.io_out, IO.io_in) flat_trace -> (IO.io_out, IO.io_in) flat_trace
1143    -> will_return -> will_return -> Nat.nat -> Nat.nat -> 'a1 trace_result
1144    -> 'a2 -> 'a2 trace_result **)
1145let replace_trace ge d e1 s1 s2 t1 t2 tM1 tM2 l1 l2 r trace0 =
1146  { new_state = r.new_state; remainder = r.remainder; new_trace = trace0;
1147    terminates =
1148    ((match e1 with
1149      | StructuredTraces.Ends_with_ret ->
1150        Logic.eq_rect_Type0
1151          (will_return_end ge d s1.RTLabs_abstract.ras_state t1 tM1)
1152          (fun clearme ->
1153          let { new_state = x; remainder = x0; new_trace = x1; terminates =
1154            x2 } = clearme
1155          in
1156          (match d with
1157           | Nat.O -> Obj.magic __
1158           | Nat.S d' ->
1159             (fun tM10 tM20 ns rem _ t1NS _ clearme0 ->
1160               let tMa = Obj.magic clearme0 in Obj.magic tMa)) tM1 tM2 x x0
1161            __ x1 __ x2)
1162          (will_return_end ge d s2.RTLabs_abstract.ras_state t2 tM2)
1163      | StructuredTraces.Doesnt_end_with_ret ->
1164        Logic.eq_rect_Type0
1165          (will_return_end ge d s1.RTLabs_abstract.ras_state t1 tM1)
1166          (fun clearme ->
1167          let { new_state = ns; remainder = rem; new_trace = t1NS;
1168            terminates = clearme0 } = clearme
1169          in
1170          let tMa = Obj.magic clearme0 in Obj.magic tMa)
1171          (will_return_end ge d s2.RTLabs_abstract.ras_state t2 tM2)) r) }
1172
1173(** val replace_sub_trace :
1174    RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1175    RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
1176    (IO.io_out, IO.io_in) flat_trace -> will_return -> will_return -> Nat.nat
1177    -> Nat.nat -> 'a1 sub_trace_result -> 'a2 -> 'a2 sub_trace_result **)
1178let replace_sub_trace ge d s1 s2 t1 t2 tM1 tM2 l1 l2 r trace0 =
1179  { ends = r.ends; trace_res =
1180    (replace_trace ge d r.ends s1 s2 t1 t2 tM1 tM2 l1 l2 r.trace_res trace0) }
1181
1182(** val make_label_return :
1183    RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1184    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1185    StructuredTraces.trace_label_return trace_result **)
1186let rec make_label_return ge depth s trace0 tERMINATES tIME =
1187  (match tIME with
1188   | Nat.O -> (fun _ -> assert false (* absurd case *))
1189   | Nat.S tIME0 ->
1190     (fun _ ->
1191       let r = make_label_label ge depth s trace0 tERMINATES tIME0 in
1192       (match r.ends with
1193        | StructuredTraces.Ends_with_ret ->
1194          (fun r5 ->
1195            replace_trace ge depth StructuredTraces.Ends_with_ret s s trace0
1196              trace0 tERMINATES tERMINATES
1197              (will_return_length ge depth s.RTLabs_abstract.ras_state trace0
1198                tERMINATES)
1199              (will_return_length ge depth s.RTLabs_abstract.ras_state trace0
1200                tERMINATES) r5 (StructuredTraces.Tlr_base ((Obj.magic s),
1201              (Obj.magic r5.new_state), r5.new_trace)))
1202        | StructuredTraces.Doesnt_end_with_ret ->
1203          (fun r5 ->
1204            let r' =
1205              make_label_return ge depth r5.new_state r5.remainder
1206                (Types.pi1 (Obj.magic r5.terminates)) tIME0
1207            in
1208            replace_trace ge depth StructuredTraces.Ends_with_ret
1209              r5.new_state s r5.remainder trace0
1210              (Types.pi1 (Obj.magic r5.terminates)) tERMINATES
1211              (will_return_length ge depth
1212                r5.new_state.RTLabs_abstract.ras_state r5.remainder
1213                (Types.pi1 (Obj.magic r5.terminates)))
1214              (will_return_length ge depth s.RTLabs_abstract.ras_state trace0
1215                tERMINATES) r' (StructuredTraces.Tlr_step ((Obj.magic s),
1216              (Obj.magic r5.new_state), (Obj.magic r'.new_state),
1217              r5.new_trace, r'.new_trace)))) r.trace_res)) __
1218(** val make_label_label :
1219    RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1220    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1221    StructuredTraces.trace_label_label sub_trace_result **)
1222and make_label_label ge depth s trace0 tERMINATES tIME =
1223  (match tIME with
1224   | Nat.O -> (fun _ -> assert false (* absurd case *))
1225   | Nat.S tIME0 ->
1226     (fun _ ->
1227       let r = make_any_label ge depth s trace0 tERMINATES tIME0 in
1228       replace_sub_trace ge depth s s trace0 trace0 tERMINATES tERMINATES
1229         (will_return_length ge depth s.RTLabs_abstract.ras_state trace0
1230           tERMINATES)
1231         (will_return_length ge depth s.RTLabs_abstract.ras_state trace0
1232           tERMINATES) r (StructuredTraces.Tll_base (r.ends, (Obj.magic s),
1233         (Obj.magic r.trace_res.new_state), r.trace_res.new_trace)))) __
1234(** val make_any_label :
1235    RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1236    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1237    StructuredTraces.trace_any_label sub_trace_result **)
1238and make_any_label ge depth s0 trace0 tERMINATES tIME =
1239  (match tIME with
1240   | Nat.O -> (fun _ -> assert false (* absurd case *))
1241   | Nat.S tIME0 ->
1242     (fun _ ->
1243       (let { RTLabs_abstract.ras_state = s; RTLabs_abstract.ras_fn_stack =
1244          stk } = s0
1245        in
1246       (fun trace1 _ tM _ ->
1247       (match Lazy.force
1248        trace1 with
1249        | Ft_stop st ->
1250          (fun _ _ tERMINATES0 _ -> assert false (* absurd case *))
1251        | Ft_step (start, tr, next0, trace') ->
1252          (fun _ _ tERMINATES0 _ ->
1253            let start' = { RTLabs_abstract.ras_state = start;
1254              RTLabs_abstract.ras_fn_stack = stk }
1255            in
1256            let next' = RTLabs_abstract.next_state ge start' next0 tr in
1257            (match RTLabs_abstract.rTLabs_classify start with
1258             | StructuredTraces.Cl_return ->
1259               (fun _ -> { ends = StructuredTraces.Ends_with_ret; trace_res =
1260                 { new_state = next'; remainder = trace'; new_trace =
1261                 (StructuredTraces.Tal_base_return ((Obj.magic start'),
1262                 (Obj.magic next'))); terminates =
1263                 (will_return_return ge depth start tr next0 trace'
1264                   tERMINATES0) } })
1265             | StructuredTraces.Cl_jump ->
1266               (fun _ -> { ends = StructuredTraces.Doesnt_end_with_ret;
1267                 trace_res = { new_state = next'; remainder = trace';
1268                 new_trace = (StructuredTraces.Tal_base_not_return
1269                 ((Obj.magic start'), (Obj.magic next'))); terminates =
1270                 (Obj.magic
1271                   (will_return_notfn ge depth start tr next0 trace'
1272                     (Types.Inr __) tERMINATES0)) } })
1273             | StructuredTraces.Cl_call ->
1274               (fun _ ->
1275                 let r =
1276                   make_label_return ge (Nat.S depth) next' trace'
1277                     (Types.pi1
1278                       (will_return_call ge depth start tr next0 trace'
1279                         tERMINATES0)) tIME0
1280                 in
1281                 (match RTLabs_abstract.rTLabs_cost
1282                          r.new_state.RTLabs_abstract.ras_state with
1283                  | Bool.True ->
1284                    (fun _ -> { ends = StructuredTraces.Doesnt_end_with_ret;
1285                      trace_res = { new_state = r.new_state; remainder =
1286                      r.remainder; new_trace =
1287                      (StructuredTraces.Tal_base_call ((Obj.magic start'),
1288                      (Obj.magic next'), (Obj.magic r.new_state),
1289                      r.new_trace)); terminates =
1290                      (let tMr = Obj.magic r.terminates in Obj.magic tMr) } })
1291                  | Bool.False ->
1292                    (fun _ ->
1293                      let r' =
1294                        make_any_label ge depth r.new_state r.remainder
1295                          (Types.pi1 (Obj.magic r.terminates)) tIME0
1296                      in
1297                      replace_sub_trace ge depth r.new_state start'
1298                        r.remainder (lazy (Ft_step (start, tr, next0,
1299                        trace'))) (Types.pi1 (Obj.magic r.terminates))
1300                        tERMINATES0
1301                        (will_return_length ge depth
1302                          r.new_state.RTLabs_abstract.ras_state r.remainder
1303                          (Types.pi1 (Obj.magic r.terminates)))
1304                        (will_return_length ge depth start (lazy (Ft_step
1305                          (start, tr, next0, trace'))) tERMINATES0) r'
1306                        (StructuredTraces.Tal_step_call (r'.ends,
1307                        (Obj.magic start'), (Obj.magic next'),
1308                        (Obj.magic r.new_state),
1309                        (Obj.magic r'.trace_res.new_state), r.new_trace,
1310                        r'.trace_res.new_trace)))) __)
1311             | StructuredTraces.Cl_tailcall ->
1312               (fun _ -> assert false (* absurd case *))
1313             | StructuredTraces.Cl_other ->
1314               (fun _ ->
1315                 (match RTLabs_abstract.rTLabs_cost next0 with
1316                  | Bool.True ->
1317                    (fun _ -> { ends = StructuredTraces.Doesnt_end_with_ret;
1318                      trace_res = { new_state = next'; remainder = trace';
1319                      new_trace = (StructuredTraces.Tal_base_not_return
1320                      ((Obj.magic start'), (Obj.magic next'))); terminates =
1321                      (Obj.magic
1322                        (will_return_notfn ge depth start tr next0 trace'
1323                          (Types.Inl __) tERMINATES0)) } })
1324                  | Bool.False ->
1325                    (fun _ ->
1326                      let r =
1327                        make_any_label ge depth next' trace'
1328                          (Types.pi1
1329                            (will_return_notfn ge depth start tr next0 trace'
1330                              (Types.Inl __) tERMINATES0)) tIME0
1331                      in
1332                      replace_sub_trace ge depth next' start' trace'
1333                        (lazy (Ft_step (start, tr, next0, trace')))
1334                        (Types.pi1
1335                          (will_return_notfn ge depth start tr next0 trace'
1336                            (Types.Inl __) tERMINATES0)) tERMINATES0
1337                        (will_return_length ge depth
1338                          next'.RTLabs_abstract.ras_state trace'
1339                          (Types.pi1
1340                            (will_return_notfn ge depth start tr next0 trace'
1341                              (Types.Inl __) tERMINATES0)))
1342                        (will_return_length ge depth start (lazy (Ft_step
1343                          (start, tr, next0, trace'))) tERMINATES0) r
1344                        (StructuredTraces.Tal_step_default (r.ends,
1345                        (Obj.magic start'), (Obj.magic next'),
1346                        (Obj.magic r.trace_res.new_state),
1347                        r.trace_res.new_trace)))) __)) __)) __ __ tM __))
1348         trace0 __ tERMINATES __)) __
1349
1350(** val make_label_return' :
1351    RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1352    (IO.io_out, IO.io_in) flat_trace -> will_return ->
1353    StructuredTraces.trace_label_return trace_result **)
1354let rec make_label_return' ge depth s trace0 tERMINATES =
1355  make_label_return ge depth s trace0 tERMINATES
1356    (Nat.plus (Nat.S (Nat.S Nat.O))
1357      (Nat.times (Nat.S (Nat.S (Nat.S Nat.O)))
1358        (will_return_length ge depth s.RTLabs_abstract.ras_state trace0
1359          tERMINATES)))
1360
1361(** val actual_successor :
1362    RTLabs_semantics.state0 -> Graphs.label Types.option **)
1363let actual_successor = function
1364| RTLabs_semantics.State (f, fs, m) -> Types.Some f.RTLabs_semantics.next
1365| RTLabs_semantics.Callstate (x, x0, x1, x2, fs, x3) ->
1366  (match fs with
1367   | List.Nil -> Types.None
1368   | List.Cons (f, x4) -> Types.Some f.RTLabs_semantics.next)
1369| RTLabs_semantics.Returnstate (x, x0, x1, x2) -> Types.None
1370| RTLabs_semantics.Finalstate x -> Types.None
1371
1372(** val steps_for_statement : RTLabs_syntax.statement -> Nat.nat **)
1373let steps_for_statement s =
1374  Nat.S
1375    (match s with
1376     | RTLabs_syntax.St_skip x -> Nat.O
1377     | RTLabs_syntax.St_cost (x, x0) -> Nat.O
1378     | RTLabs_syntax.St_const (x, x0, x1, x2) -> Nat.O
1379     | RTLabs_syntax.St_op1 (x, x0, x1, x2, x3, x4) -> Nat.O
1380     | RTLabs_syntax.St_op2 (x, x0, x1, x2, x3, x4, x5, x6) -> Nat.O
1381     | RTLabs_syntax.St_load (x, x0, x1, x2) -> Nat.O
1382     | RTLabs_syntax.St_store (x, x0, x1, x2) -> Nat.O
1383     | RTLabs_syntax.St_call_id (x, x0, x1, x2) -> Nat.S Nat.O
1384     | RTLabs_syntax.St_call_ptr (x, x0, x1, x2) -> Nat.S Nat.O
1385     | RTLabs_syntax.St_cond (x, x0, x1) -> Nat.O
1386     | RTLabs_syntax.St_return -> Nat.S Nat.O)
1387
1388type remainder_ok =
1389| Mk_remainder_ok
1390
1391(** val remainder_ok_rect_Type4 :
1392    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1393    IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
1394    'a1 **)
1395let rec remainder_ok_rect_Type4 ge s t h_mk_remainder_ok = function
1396| Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __
1397
1398(** val remainder_ok_rect_Type5 :
1399    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1400    IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
1401    'a1 **)
1402let rec remainder_ok_rect_Type5 ge s t h_mk_remainder_ok = function
1403| Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __
1404
1405(** val remainder_ok_rect_Type3 :
1406    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1407    IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
1408    'a1 **)
1409let rec remainder_ok_rect_Type3 ge s t h_mk_remainder_ok = function
1410| Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __
1411
1412(** val remainder_ok_rect_Type2 :
1413    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1414    IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
1415    'a1 **)
1416let rec remainder_ok_rect_Type2 ge s t h_mk_remainder_ok = function
1417| Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __
1418
1419(** val remainder_ok_rect_Type1 :
1420    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1421    IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
1422    'a1 **)
1423let rec remainder_ok_rect_Type1 ge s t h_mk_remainder_ok = function
1424| Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __
1425
1426(** val remainder_ok_rect_Type0 :
1427    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1428    IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
1429    'a1 **)
1430let rec remainder_ok_rect_Type0 ge s t h_mk_remainder_ok = function
1431| Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __
1432
1433(** val remainder_ok_inv_rect_Type4 :
1434    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1435    IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ ->
1436    'a1) -> 'a1 **)
1437let remainder_ok_inv_rect_Type4 x1 x2 x3 hterm h1 =
1438  let hcut = remainder_ok_rect_Type4 x1 x2 x3 h1 hterm in hcut __
1439
1440(** val remainder_ok_inv_rect_Type3 :
1441    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1442    IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ ->
1443    'a1) -> 'a1 **)
1444let remainder_ok_inv_rect_Type3 x1 x2 x3 hterm h1 =
1445  let hcut = remainder_ok_rect_Type3 x1 x2 x3 h1 hterm in hcut __
1446
1447(** val remainder_ok_inv_rect_Type2 :
1448    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1449    IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ ->
1450    'a1) -> 'a1 **)
1451let remainder_ok_inv_rect_Type2 x1 x2 x3 hterm h1 =
1452  let hcut = remainder_ok_rect_Type2 x1 x2 x3 h1 hterm in hcut __
1453
1454(** val remainder_ok_inv_rect_Type1 :
1455    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1456    IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ ->
1457    'a1) -> 'a1 **)
1458let remainder_ok_inv_rect_Type1 x1 x2 x3 hterm h1 =
1459  let hcut = remainder_ok_rect_Type1 x1 x2 x3 h1 hterm in hcut __
1460
1461(** val remainder_ok_inv_rect_Type0 :
1462    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1463    IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ ->
1464    'a1) -> 'a1 **)
1465let remainder_ok_inv_rect_Type0 x1 x2 x3 hterm h1 =
1466  let hcut = remainder_ok_rect_Type0 x1 x2 x3 h1 hterm in hcut __
1467
1468(** val remainder_ok_discr :
1469    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1470    IO.io_in) flat_trace -> remainder_ok -> remainder_ok -> __ **)
1471let remainder_ok_discr a1 a2 a3 x y =
1472  Logic.eq_rect_Type2 x
1473    (let Mk_remainder_ok = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
1474
1475(** val remainder_ok_jmdiscr :
1476    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1477    IO.io_in) flat_trace -> remainder_ok -> remainder_ok -> __ **)
1478let remainder_ok_jmdiscr a1 a2 a3 x y =
1479  Logic.eq_rect_Type2 x
1480    (let Mk_remainder_ok = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
1481
1482(** val init_state_is :
1483    RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state0 ->
1484    (Pointers.block, __) Types.dPair **)
1485let init_state_is p s =
1486  RTLabs_semantics.bind_ok
1487    (Globalenvs.init_mem (fun x -> List.Cons ((AST.Init_space x), List.Nil))
1488      p) (fun x ->
1489    let main = p.AST.prog_main in
1490    Obj.magic
1491      (Monad.m_bind0 (Monad.max_def Errors.res0)
1492        (Obj.magic
1493          (Errors.opt_to_res (List.Cons ((Errors.MSG
1494            ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX
1495            (PreIdentifiers.SymbolTag, main)), List.Nil))))
1496            (Globalenvs.find_symbol (RTLabs_semantics.make_global0 p) main)))
1497        (fun b ->
1498        Monad.m_bind0 (Monad.max_def Errors.res0)
1499          (Obj.magic
1500            (Errors.opt_to_res (List.Cons ((Errors.MSG
1501              ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
1502              (PreIdentifiers.SymbolTag, main)), List.Nil))))
1503              (Globalenvs.find_funct_ptr (RTLabs_semantics.make_global0 p) b)))
1504          (fun f ->
1505          Obj.magic (Errors.OK (RTLabs_semantics.Callstate (main, f,
1506            List.Nil, Types.None, List.Nil, x))))))) s (fun m _ _ ->
1507    RTLabs_semantics.bind_ok
1508      (Errors.opt_to_res (List.Cons ((Errors.MSG
1509        ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX
1510        (PreIdentifiers.SymbolTag, p.AST.prog_main)), List.Nil))))
1511        (Globalenvs.find_symbol (RTLabs_semantics.make_global0 p)
1512          p.AST.prog_main)) (fun x ->
1513      Obj.magic
1514        (Monad.m_bind0 (Monad.max_def Errors.res0)
1515          (Obj.magic
1516            (Errors.opt_to_res (List.Cons ((Errors.MSG
1517              ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
1518              (PreIdentifiers.SymbolTag, p.AST.prog_main)), List.Nil))))
1519              (Globalenvs.find_funct_ptr (RTLabs_semantics.make_global0 p) x)))
1520          (fun f ->
1521          Obj.magic (Errors.OK (RTLabs_semantics.Callstate (p.AST.prog_main,
1522            f, List.Nil, Types.None, List.Nil, m)))))) s (fun b _ _ ->
1523      RTLabs_semantics.bind_ok
1524        (Errors.opt_to_res (List.Cons ((Errors.MSG
1525          ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
1526          (PreIdentifiers.SymbolTag, p.AST.prog_main)), List.Nil))))
1527          (Globalenvs.find_funct_ptr (RTLabs_semantics.make_global0 p) b))
1528        (fun x -> Errors.OK (RTLabs_semantics.Callstate (p.AST.prog_main, x,
1529        List.Nil, Types.None, List.Nil, m))) s (fun f _ _ ->
1530        Obj.magic Errors.res_discr (Errors.OK (RTLabs_semantics.Callstate
1531          (p.AST.prog_main, f, List.Nil, Types.None, List.Nil, m)))
1532          (Errors.OK s) __ (fun _ ->
1533          Logic.eq_rect_Type0 (RTLabs_semantics.Callstate (p.AST.prog_main,
1534            f, List.Nil, Types.None, List.Nil, m)) (fun _ ->
1535            Logic.streicherK (Errors.OK (RTLabs_semantics.Callstate
1536              (p.AST.prog_main, f, List.Nil, Types.None, List.Nil, m)))
1537              { Types.dpi1 = b; Types.dpi2 = __ }) s __))))
1538
1539(** val ras_state_initial :
1540    RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state0 ->
1541    RTLabs_abstract.rTLabs_ext_state **)
1542let ras_state_initial p s =
1543  { RTLabs_abstract.ras_state = s; RTLabs_abstract.ras_fn_stack = (List.Cons
1544    ((init_state_is p s).Types.dpi1, List.Nil)) }
1545
1546(** val deprop_execute :
1547    RTLabs_semantics.genv -> RTLabs_semantics.state0 ->
1548    RTLabs_semantics.state0 -> Events.trace Types.sig0 **)
1549let rec deprop_execute ge s s' =
1550  (match RTLabs_semantics.eval_statement ge s with
1551   | IOMonad.Interact (x, x0) -> (fun _ -> assert false (* absurd case *))
1552   | IOMonad.Value ts -> (fun _ -> ts.Types.fst)
1553   | IOMonad.Wrong x -> (fun _ -> assert false (* absurd case *))) __
1554
1555(** val deprop_as_execute :
1556    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1557    RTLabs_abstract.rTLabs_ext_state -> Events.trace Types.sig0 **)
1558let rec deprop_as_execute ge s s' =
1559  deprop_execute ge s.RTLabs_abstract.ras_state s'.RTLabs_abstract.ras_state
1560
1561type ('o, 'i) partial_flat_trace =
1562| Pft_base of RTLabs_semantics.state0 * Events.trace
1563   * RTLabs_semantics.state0
1564| Pft_step of RTLabs_semantics.state0 * Events.trace
1565   * RTLabs_semantics.state0 * RTLabs_semantics.state0
1566   * ('o, 'i) partial_flat_trace
1567
1568(** val partial_flat_trace_rect_Type4 :
1569    RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
1570    RTLabs_semantics.state0 -> __ -> 'a3) -> (RTLabs_semantics.state0 ->
1571    Events.trace -> RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __
1572    -> ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) ->
1573    RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> ('a1, 'a2)
1574    partial_flat_trace -> 'a3 **)
1575let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_18422 x_18421 = function
1576| Pft_base (s, tr, s') -> h_pft_base s tr s' __
1577| Pft_step (s, tr, s', s'', x_18425) ->
1578  h_pft_step s tr s' s'' __ x_18425
1579    (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_18425)
1580
1581(** val partial_flat_trace_rect_Type3 :
1582    RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
1583    RTLabs_semantics.state0 -> __ -> 'a3) -> (RTLabs_semantics.state0 ->
1584    Events.trace -> RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __
1585    -> ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) ->
1586    RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> ('a1, 'a2)
1587    partial_flat_trace -> 'a3 **)
1588let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_18438 x_18437 = function
1589| Pft_base (s, tr, s') -> h_pft_base s tr s' __
1590| Pft_step (s, tr, s', s'', x_18441) ->
1591  h_pft_step s tr s' s'' __ x_18441
1592    (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_18441)
1593
1594(** val partial_flat_trace_rect_Type2 :
1595    RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
1596    RTLabs_semantics.state0 -> __ -> 'a3) -> (RTLabs_semantics.state0 ->
1597    Events.trace -> RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __
1598    -> ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) ->
1599    RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> ('a1, 'a2)
1600    partial_flat_trace -> 'a3 **)
1601let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_18446 x_18445 = function
1602| Pft_base (s, tr, s') -> h_pft_base s tr s' __
1603| Pft_step (s, tr, s', s'', x_18449) ->
1604  h_pft_step s tr s' s'' __ x_18449
1605    (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_18449)
1606
1607(** val partial_flat_trace_rect_Type1 :
1608    RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
1609    RTLabs_semantics.state0 -> __ -> 'a3) -> (RTLabs_semantics.state0 ->
1610    Events.trace -> RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __
1611    -> ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) ->
1612    RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> ('a1, 'a2)
1613    partial_flat_trace -> 'a3 **)
1614let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_18454 x_18453 = function
1615| Pft_base (s, tr, s') -> h_pft_base s tr s' __
1616| Pft_step (s, tr, s', s'', x_18457) ->
1617  h_pft_step s tr s' s'' __ x_18457
1618    (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_18457)
1619
1620(** val partial_flat_trace_rect_Type0 :
1621    RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
1622    RTLabs_semantics.state0 -> __ -> 'a3) -> (RTLabs_semantics.state0 ->
1623    Events.trace -> RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __
1624    -> ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) ->
1625    RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> ('a1, 'a2)
1626    partial_flat_trace -> 'a3 **)
1627let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_18462 x_18461 = function
1628| Pft_base (s, tr, s') -> h_pft_base s tr s' __
1629| Pft_step (s, tr, s', s'', x_18465) ->
1630  h_pft_step s tr s' s'' __ x_18465
1631    (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_18465)
1632
1633(** val partial_flat_trace_inv_rect_Type4 :
1634    RTLabs_semantics.genv -> RTLabs_semantics.state0 ->
1635    RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace ->
1636    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
1637    -> __ -> __ -> __ -> 'a3) -> (RTLabs_semantics.state0 -> Events.trace ->
1638    RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __ -> ('a1, 'a2)
1639    partial_flat_trace -> (__ -> __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3)
1640    -> 'a3 **)
1641let partial_flat_trace_inv_rect_Type4 x3 x4 x5 hterm h1 h2 =
1642  let hcut = partial_flat_trace_rect_Type4 x3 h1 h2 x4 x5 hterm in
1643  hcut __ __ __
1644
1645(** val partial_flat_trace_inv_rect_Type3 :
1646    RTLabs_semantics.genv -> RTLabs_semantics.state0 ->
1647    RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace ->
1648    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
1649    -> __ -> __ -> __ -> 'a3) -> (RTLabs_semantics.state0 -> Events.trace ->
1650    RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __ -> ('a1, 'a2)
1651    partial_flat_trace -> (__ -> __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3)
1652    -> 'a3 **)
1653let partial_flat_trace_inv_rect_Type3 x3 x4 x5 hterm h1 h2 =
1654  let hcut = partial_flat_trace_rect_Type3 x3 h1 h2 x4 x5 hterm in
1655  hcut __ __ __
1656
1657(** val partial_flat_trace_inv_rect_Type2 :
1658    RTLabs_semantics.genv -> RTLabs_semantics.state0 ->
1659    RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace ->
1660    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
1661    -> __ -> __ -> __ -> 'a3) -> (RTLabs_semantics.state0 -> Events.trace ->
1662    RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __ -> ('a1, 'a2)
1663    partial_flat_trace -> (__ -> __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3)
1664    -> 'a3 **)
1665let partial_flat_trace_inv_rect_Type2 x3 x4 x5 hterm h1 h2 =
1666  let hcut = partial_flat_trace_rect_Type2 x3 h1 h2 x4 x5 hterm in
1667  hcut __ __ __
1668
1669(** val partial_flat_trace_inv_rect_Type1 :
1670    RTLabs_semantics.genv -> RTLabs_semantics.state0 ->
1671    RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace ->
1672    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
1673    -> __ -> __ -> __ -> 'a3) -> (RTLabs_semantics.state0 -> Events.trace ->
1674    RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __ -> ('a1, 'a2)
1675    partial_flat_trace -> (__ -> __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3)
1676    -> 'a3 **)
1677let partial_flat_trace_inv_rect_Type1 x3 x4 x5 hterm h1 h2 =
1678  let hcut = partial_flat_trace_rect_Type1 x3 h1 h2 x4 x5 hterm in
1679  hcut __ __ __
1680
1681(** val partial_flat_trace_inv_rect_Type0 :
1682    RTLabs_semantics.genv -> RTLabs_semantics.state0 ->
1683    RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace ->
1684    (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
1685    -> __ -> __ -> __ -> 'a3) -> (RTLabs_semantics.state0 -> Events.trace ->
1686    RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __ -> ('a1, 'a2)
1687    partial_flat_trace -> (__ -> __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3)
1688    -> 'a3 **)
1689let partial_flat_trace_inv_rect_Type0 x3 x4 x5 hterm h1 h2 =
1690  let hcut = partial_flat_trace_rect_Type0 x3 h1 h2 x4 x5 hterm in
1691  hcut __ __ __
1692
1693(** val partial_flat_trace_jmdiscr :
1694    RTLabs_semantics.genv -> RTLabs_semantics.state0 ->
1695    RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2)
1696    partial_flat_trace -> __ **)
1697let partial_flat_trace_jmdiscr a3 a4 a5 x y =
1698  Logic.eq_rect_Type2 x
1699    (match x with
1700     | Pft_base (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1701     | Pft_step (a0, a10, a20, a30, a50) ->
1702       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1703
1704(** val append_partial_flat_trace :
1705    RTLabs_semantics.genv -> RTLabs_semantics.state0 ->
1706    RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> ('a1, 'a2)
1707    partial_flat_trace -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2)
1708    partial_flat_trace **)
1709let rec append_partial_flat_trace ge s1 s2 s3 = function
1710| Pft_base (s, tr, s') -> (fun x -> Pft_step (s, tr, s', s3, x))
1711| Pft_step (s, tr, s', s'', tr') ->
1712  (fun tr2 -> Pft_step (s, tr, s', s3,
1713    (append_partial_flat_trace ge s' s'' s3 tr' tr2)))
1714
1715(** val partial_to_flat_trace :
1716    RTLabs_semantics.genv -> RTLabs_semantics.state0 ->
1717    RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2)
1718    flat_trace -> ('a1, 'a2) flat_trace **)
1719let rec partial_to_flat_trace ge s1 s2 = function
1720| Pft_base (s, tr0, s') -> (fun x -> lazy (Ft_step (s, tr0, s', x)))
1721| Pft_step (s, tr0, s', s'', tr') ->
1722  (fun tr'' -> lazy (Ft_step (s, tr0, s',
1723    (partial_to_flat_trace ge s' s'' tr' tr''))))
1724
1725(** val flat_trace_of_label_return :
1726    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1727    RTLabs_abstract.rTLabs_ext_state -> StructuredTraces.trace_label_return
1728    -> (IO.io_out, IO.io_in) partial_flat_trace **)
1729let rec flat_trace_of_label_return ge s s' = function
1730| StructuredTraces.Tlr_base (s1, s2, tll) ->
1731  flat_trace_of_label_label ge StructuredTraces.Ends_with_ret (Obj.magic s1)
1732    (Obj.magic s2) tll
1733| StructuredTraces.Tlr_step (s1, s2, s3, tll, tlr) ->
1734  append_partial_flat_trace ge (Obj.magic s1).RTLabs_abstract.ras_state
1735    (Obj.magic s2).RTLabs_abstract.ras_state
1736    (Obj.magic s3).RTLabs_abstract.ras_state
1737    (flat_trace_of_label_label ge StructuredTraces.Doesnt_end_with_ret
1738      (Obj.magic s1) (Obj.magic s2) tll)
1739    (flat_trace_of_label_return ge (Obj.magic s2) (Obj.magic s3) tlr)
1740(** val flat_trace_of_label_label :
1741    RTLabs_semantics.genv -> StructuredTraces.trace_ends_with_ret ->
1742    RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
1743    StructuredTraces.trace_label_label -> (IO.io_out, IO.io_in)
1744    partial_flat_trace **)
1745and flat_trace_of_label_label ge ends0 s s' = function
1746| StructuredTraces.Tll_base (e1, s1, s2, tal) ->
1747  flat_trace_of_any_label ge e1 (Obj.magic s1) (Obj.magic s2) tal
1748(** val flat_trace_of_any_label :
1749    RTLabs_semantics.genv -> StructuredTraces.trace_ends_with_ret ->
1750    RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
1751    StructuredTraces.trace_any_label -> (IO.io_out, IO.io_in)
1752    partial_flat_trace **)
1753and flat_trace_of_any_label ge ends0 s s' = function
1754| StructuredTraces.Tal_base_not_return (s1, s2) ->
1755  let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1756  Pft_base ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1757  (Obj.magic s2).RTLabs_abstract.ras_state)
1758| StructuredTraces.Tal_base_return (s1, s2) ->
1759  let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1760  Pft_base ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1761  (Obj.magic s2).RTLabs_abstract.ras_state)
1762| StructuredTraces.Tal_base_call (s1, s2, s3, tlr) ->
1763  let suffix' =
1764    flat_trace_of_label_return ge (Obj.magic s2) (Obj.magic s3) tlr
1765  in
1766  let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1767  Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1768  (Obj.magic s2).RTLabs_abstract.ras_state,
1769  (Obj.magic s3).RTLabs_abstract.ras_state, suffix')
1770| StructuredTraces.Tal_base_tailcall (s1, s2, s3, tlr) ->
1771  assert false (* absurd case *)
1772| StructuredTraces.Tal_step_call (ends1, s1, s2, s3, s4, tlr, tal) ->
1773  let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1774  Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1775  (Obj.magic s2).RTLabs_abstract.ras_state,
1776  (Obj.magic s4).RTLabs_abstract.ras_state,
1777  (append_partial_flat_trace ge (Obj.magic s2).RTLabs_abstract.ras_state
1778    (Obj.magic s3).RTLabs_abstract.ras_state
1779    (Obj.magic s4).RTLabs_abstract.ras_state
1780    (flat_trace_of_label_return ge (Obj.magic s2) (Obj.magic s3) tlr)
1781    (flat_trace_of_any_label ge ends1 (Obj.magic s3) (Obj.magic s4) tal)))
1782| StructuredTraces.Tal_step_default (ends1, s1, s2, s3, tal) ->
1783  let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1784  Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1785  (Obj.magic s2).RTLabs_abstract.ras_state,
1786  (Obj.magic s3).RTLabs_abstract.ras_state,
1787  (flat_trace_of_any_label ge ends1 (Obj.magic s2) (Obj.magic s3) tal))
1788
1789(** val flat_trace_of_any_call :
1790    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1791    RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
1792    Events.trace -> StructuredTraces.trace_any_call -> (IO.io_out, IO.io_in)
1793    partial_flat_trace **)
1794let rec flat_trace_of_any_call ge s s' s'' et tr =
1795  (match tr with
1796   | StructuredTraces.Tac_base s1 ->
1797     (fun _ -> Pft_base ((Obj.magic s1).RTLabs_abstract.ras_state, et,
1798       s''.RTLabs_abstract.ras_state))
1799   | StructuredTraces.Tac_step_call (s1, s2, s3, s4, tlr, tac) ->
1800     (fun _ ->
1801       let et0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s4) in
1802       Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, et0,
1803       (Obj.magic s4).RTLabs_abstract.ras_state,
1804       s''.RTLabs_abstract.ras_state,
1805       (append_partial_flat_trace ge (Obj.magic s4).RTLabs_abstract.ras_state
1806         (Obj.magic s2).RTLabs_abstract.ras_state
1807         s''.RTLabs_abstract.ras_state
1808         (flat_trace_of_label_return ge (Obj.magic s4) (Obj.magic s2) tlr)
1809         (flat_trace_of_any_call ge (Obj.magic s2) (Obj.magic s3) s'' et tac))))
1810   | StructuredTraces.Tac_step_default (s1, s2, s3, tal) ->
1811     (fun _ ->
1812       let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s3) in
1813       Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1814       (Obj.magic s3).RTLabs_abstract.ras_state,
1815       s''.RTLabs_abstract.ras_state,
1816       (flat_trace_of_any_call ge (Obj.magic s3) (Obj.magic s2) s'' et tal))))
1817    __
1818
1819(** val flat_trace_of_label_call :
1820    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1821    RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
1822    Events.trace -> StructuredTraces.trace_label_call -> (IO.io_out,
1823    IO.io_in) partial_flat_trace **)
1824let rec flat_trace_of_label_call ge s s' s'' et tr =
1825  (let StructuredTraces.Tlc_base (s1, s2, tac) = tr in
1826  (fun _ ->
1827  flat_trace_of_any_call ge (Obj.magic s1) (Obj.magic s2) s'' et tac)) __
1828
1829(** val flat_trace_of_label_diverges :
1830    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1831    StructuredTraces.trace_label_diverges -> (IO.io_out, IO.io_in) flat_trace **)
1832let rec flat_trace_of_label_diverges ge s tr =
1833  match Lazy.force
1834  tr with
1835  | StructuredTraces.Tld_step (sx, sy, tll, tld) ->
1836    (let { RTLabs_abstract.ras_state = sy'; RTLabs_abstract.ras_fn_stack =
1837       stk } = Obj.magic sy
1838     in
1839    (fun tll0 ->
1840    (match flat_trace_of_label_label ge StructuredTraces.Doesnt_end_with_ret
1841             (Obj.magic sx) { RTLabs_abstract.ras_state = sy';
1842             RTLabs_abstract.ras_fn_stack = stk } tll0 with
1843     | Pft_base (s1, tr0, s2) ->
1844       (fun _ tld0 -> lazy (Ft_step (s1, tr0, s2,
1845         (flat_trace_of_label_diverges ge { RTLabs_abstract.ras_state = s2;
1846           RTLabs_abstract.ras_fn_stack = stk } tld0))))
1847     | Pft_step (s1, et, s2, s3, tr') ->
1848       (fun _ tld0 -> lazy (Ft_step (s1, et, s2,
1849         (add_partial_flat_trace ge s2 { RTLabs_abstract.ras_state = s3;
1850           RTLabs_abstract.ras_fn_stack = stk } tr' tld0))))) __)) tll tld
1851  | StructuredTraces.Tld_base (s1, s2, s3, tlc, tld) ->
1852    (let { RTLabs_abstract.ras_state = s3'; RTLabs_abstract.ras_fn_stack =
1853       stk } = Obj.magic s3
1854     in
1855    (fun _ ->
1856    let tr0 =
1857      deprop_as_execute ge (Obj.magic s2) { RTLabs_abstract.ras_state = s3';
1858        RTLabs_abstract.ras_fn_stack = stk }
1859    in
1860    (match flat_trace_of_label_call ge (Obj.magic s1) (Obj.magic s2)
1861             { RTLabs_abstract.ras_state = s3';
1862             RTLabs_abstract.ras_fn_stack = stk } tr0 tlc with
1863     | Pft_base (s10, tr1, s20) ->
1864       (fun _ tld0 -> lazy (Ft_step (s10, tr1, s20,
1865         (flat_trace_of_label_diverges ge { RTLabs_abstract.ras_state = s20;
1866           RTLabs_abstract.ras_fn_stack = stk } tld0))))
1867     | Pft_step (s10, et, s20, s30, tr') ->
1868       (fun _ tld0 -> lazy (Ft_step (s10, et, s20,
1869         (add_partial_flat_trace ge s20 { RTLabs_abstract.ras_state = s30;
1870           RTLabs_abstract.ras_fn_stack = stk } tr' tld0))))) __)) __ tld
1871(** val add_partial_flat_trace :
1872    RTLabs_semantics.genv -> RTLabs_semantics.state0 ->
1873    RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in)
1874    partial_flat_trace -> StructuredTraces.trace_label_diverges ->
1875    (IO.io_out, IO.io_in) flat_trace **)
1876and add_partial_flat_trace ge s s' =
1877  let { RTLabs_abstract.ras_state = sx; RTLabs_abstract.ras_fn_stack =
1878    stk } = s'
1879  in
1880  (fun ptr ->
1881  (match ptr with
1882   | Pft_base (s0, tr, s'0) ->
1883     (fun _ tr0 -> lazy (Ft_step (s0, tr, s'0,
1884       (flat_trace_of_label_diverges ge { RTLabs_abstract.ras_state = s'0;
1885         RTLabs_abstract.ras_fn_stack = stk } tr0))))
1886   | Pft_step (s1, et, s2, s3, tr') ->
1887     (fun _ tr -> lazy (Ft_step (s1, et, s2,
1888       (add_partial_flat_trace ge s2 { RTLabs_abstract.ras_state = s3;
1889         RTLabs_abstract.ras_fn_stack = stk } tr' tr))))) __)
1890
1891(** val flat_trace_of_whole_program :
1892    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1893    StructuredTraces.trace_whole_program -> (IO.io_out, IO.io_in) flat_trace **)
1894let rec flat_trace_of_whole_program ge s = function
1895| StructuredTraces.Twp_terminating (s1, s2, sf, tlr) ->
1896  let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1897  lazy (Ft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1898  (Obj.magic s2).RTLabs_abstract.ras_state,
1899  (partial_to_flat_trace ge (Obj.magic s2).RTLabs_abstract.ras_state
1900    (Obj.magic sf).RTLabs_abstract.ras_state
1901    (flat_trace_of_label_return ge (Obj.magic s2) (Obj.magic sf) tlr)
1902    (lazy (Ft_stop (Obj.magic sf).RTLabs_abstract.ras_state)))))
1903| StructuredTraces.Twp_diverges (s1, s2, tld) ->
1904  let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1905  lazy (Ft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1906  (Obj.magic s2).RTLabs_abstract.ras_state,
1907  (flat_trace_of_label_diverges ge (Obj.magic s2) tld)))
1908
1909(** val state_fn :
1910    RTLabs_semantics.genv -> __ -> Pointers.block Types.option **)
1911let state_fn ge s =
1912  match (Obj.magic s).RTLabs_abstract.ras_fn_stack with
1913  | List.Nil -> Types.None
1914  | List.Cons (h, t) ->
1915    (match (Obj.magic s).RTLabs_abstract.ras_state with
1916     | RTLabs_semantics.State (x, x0, x1) -> Types.Some h
1917     | RTLabs_semantics.Callstate (x, x0, x1, x2, x3, x4) ->
1918       (match t with
1919        | List.Nil -> Types.None
1920        | List.Cons (h', x5) -> Types.Some h')
1921     | RTLabs_semantics.Returnstate (x, x0, x1, x2) -> Types.Some h
1922     | RTLabs_semantics.Finalstate x -> Types.Some h)
1923
1924(** val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __ **)
1925let option_jmdiscr x y =
1926  Logic.eq_rect_Type2 x
1927    (match x with
1928     | Types.None -> Obj.magic (fun _ dH -> dH)
1929     | Types.Some a0 -> Obj.magic (fun _ dH -> dH __)) y
1930
Note: See TracBrowser for help on using the repository browser.