source: extracted/rTLabs_traces.ml @ 2827

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

Everything extracted again.

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