source: driver/extracted/rTLabs_traces.ml @ 3106

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File size: 90.7 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_1409 s x_1408 = function
299| Wr_step (s0, tr, s', depth, trace, x_1411) ->
300  h_wr_step s0 tr s' depth __ trace __ x_1411
301    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
302      s' trace x_1411)
303| Wr_call (s0, tr, s', depth, trace, x_1413) ->
304  h_wr_call s0 tr s' depth __ trace __ x_1413
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_1413)
307| Wr_ret (s0, tr, s', depth, trace, x_1415) ->
308  h_wr_ret s0 tr s' depth __ trace __ x_1415
309    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
310      s' trace x_1415)
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_1437 s x_1436 = function
326| Wr_step (s0, tr, s', depth, trace, x_1439) ->
327  h_wr_step s0 tr s' depth __ trace __ x_1439
328    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
329      s' trace x_1439)
330| Wr_call (s0, tr, s', depth, trace, x_1441) ->
331  h_wr_call s0 tr s' depth __ trace __ x_1441
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_1441)
334| Wr_ret (s0, tr, s', depth, trace, x_1443) ->
335  h_wr_ret s0 tr s' depth __ trace __ x_1443
336    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
337      s' trace x_1443)
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_1451 s x_1450 = function
353| Wr_step (s0, tr, s', depth, trace, x_1453) ->
354  h_wr_step s0 tr s' depth __ trace __ x_1453
355    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
356      s' trace x_1453)
357| Wr_call (s0, tr, s', depth, trace, x_1455) ->
358  h_wr_call s0 tr s' depth __ trace __ x_1455
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_1455)
361| Wr_ret (s0, tr, s', depth, trace, x_1457) ->
362  h_wr_ret s0 tr s' depth __ trace __ x_1457
363    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
364      s' trace x_1457)
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_1465 s x_1464 = function
380| Wr_step (s0, tr, s', depth, trace, x_1467) ->
381  h_wr_step s0 tr s' depth __ trace __ x_1467
382    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
383      s' trace x_1467)
384| Wr_call (s0, tr, s', depth, trace, x_1469) ->
385  h_wr_call s0 tr s' depth __ trace __ x_1469
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_1469)
388| Wr_ret (s0, tr, s', depth, trace, x_1471) ->
389  h_wr_ret s0 tr s' depth __ trace __ x_1471
390    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
391      s' trace x_1471)
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_1479 s x_1478 = function
407| Wr_step (s0, tr, s', depth, trace, x_1481) ->
408  h_wr_step s0 tr s' depth __ trace __ x_1481
409    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
410      s' trace x_1481)
411| Wr_call (s0, tr, s', depth, trace, x_1483) ->
412  h_wr_call s0 tr s' depth __ trace __ x_1483
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_1483)
415| Wr_ret (s0, tr, s', depth, trace, x_1485) ->
416  h_wr_ret s0 tr s' depth __ trace __ x_1485
417    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
418      s' trace x_1485)
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_2020 =
842  let { new_state = new_state0; remainder = remainder0; new_trace =
843    new_trace0; terminates = terminates0 } = x_2020
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_2022 =
854  let { new_state = new_state0; remainder = remainder0; new_trace =
855    new_trace0; terminates = terminates0 } = x_2022
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_2024 =
866  let { new_state = new_state0; remainder = remainder0; new_trace =
867    new_trace0; terminates = terminates0 } = x_2024
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_2026 =
878  let { new_state = new_state0; remainder = remainder0; new_trace =
879    new_trace0; terminates = terminates0 } = x_2026
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_2028 =
890  let { new_state = new_state0; remainder = remainder0; new_trace =
891    new_trace0; terminates = terminates0 } = x_2028
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_2030 =
902  let { new_state = new_state0; remainder = remainder0; new_trace =
903    new_trace0; terminates = terminates0 } = x_2030
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_2048 =
1002  let { ends = ends0; trace_res = trace_res0 } = x_2048 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_2050 =
1011  let { ends = ends0; trace_res = trace_res0 } = x_2050 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_2052 =
1020  let { ends = ends0; trace_res = trace_res0 } = x_2052 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_2054 =
1029  let { ends = ends0; trace_res = trace_res0 } = x_2054 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_2056 =
1038  let { ends = ends0; trace_res = trace_res0 } = x_2056 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_2058 =
1047  let { ends = ends0; trace_res = trace_res0 } = x_2058 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 (Globalenvs.init_mem (fun x -> x) p) (fun x ->
1475    let main = p.AST.prog_main in
1476    Obj.magic
1477      (Monad.m_bind0 (Monad.max_def Errors.res0)
1478        (Obj.magic
1479          (Errors.opt_to_res (List.Cons ((Errors.MSG
1480            ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX
1481            (PreIdentifiers.SymbolTag, main)), List.Nil))))
1482            (Globalenvs.find_symbol (RTLabs_semantics.make_global p) main)))
1483        (fun b ->
1484        Monad.m_bind0 (Monad.max_def Errors.res0)
1485          (Obj.magic
1486            (Errors.opt_to_res (List.Cons ((Errors.MSG
1487              ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
1488              (PreIdentifiers.SymbolTag, main)), List.Nil))))
1489              (Globalenvs.find_funct_ptr (RTLabs_semantics.make_global p) b)))
1490          (fun f ->
1491          Obj.magic (Errors.OK (RTLabs_semantics.Callstate (main, f,
1492            List.Nil, Types.None, List.Nil, x))))))) s (fun m _ _ ->
1493    RTLabs_semantics.bind_ok
1494      (Errors.opt_to_res (List.Cons ((Errors.MSG
1495        ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX
1496        (PreIdentifiers.SymbolTag, p.AST.prog_main)), List.Nil))))
1497        (Globalenvs.find_symbol (RTLabs_semantics.make_global p)
1498          p.AST.prog_main)) (fun x ->
1499      Obj.magic
1500        (Monad.m_bind0 (Monad.max_def Errors.res0)
1501          (Obj.magic
1502            (Errors.opt_to_res (List.Cons ((Errors.MSG
1503              ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
1504              (PreIdentifiers.SymbolTag, p.AST.prog_main)), List.Nil))))
1505              (Globalenvs.find_funct_ptr (RTLabs_semantics.make_global p) x)))
1506          (fun f ->
1507          Obj.magic (Errors.OK (RTLabs_semantics.Callstate (p.AST.prog_main,
1508            f, List.Nil, Types.None, List.Nil, m)))))) s (fun b _ _ ->
1509      RTLabs_semantics.bind_ok
1510        (Errors.opt_to_res (List.Cons ((Errors.MSG
1511          ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
1512          (PreIdentifiers.SymbolTag, p.AST.prog_main)), List.Nil))))
1513          (Globalenvs.find_funct_ptr (RTLabs_semantics.make_global p) b))
1514        (fun x -> Errors.OK (RTLabs_semantics.Callstate (p.AST.prog_main, x,
1515        List.Nil, Types.None, List.Nil, m))) s (fun f _ _ ->
1516        Obj.magic Errors.res_discr (Errors.OK (RTLabs_semantics.Callstate
1517          (p.AST.prog_main, f, List.Nil, Types.None, List.Nil, m)))
1518          (Errors.OK s) __ (fun _ ->
1519          Logic.eq_rect_Type0 (RTLabs_semantics.Callstate (p.AST.prog_main,
1520            f, List.Nil, Types.None, List.Nil, m)) (fun _ ->
1521            Logic.streicherK (Errors.OK (RTLabs_semantics.Callstate
1522              (p.AST.prog_main, f, List.Nil, Types.None, List.Nil, m)))
1523              { Types.dpi1 = b; Types.dpi2 = __ }) s __))))
1524
1525(** val ras_state_initial :
1526    RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state ->
1527    RTLabs_abstract.rTLabs_ext_state **)
1528let ras_state_initial p s =
1529  { RTLabs_abstract.ras_state = s; RTLabs_abstract.ras_fn_stack = (List.Cons
1530    ((init_state_is p s).Types.dpi1, List.Nil)) }
1531
1532(** val deprop_execute :
1533    RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1534    -> Events.trace Types.sig0 **)
1535let rec deprop_execute ge s s' =
1536  (match RTLabs_semantics.eval_statement ge s with
1537   | IOMonad.Interact (x, x0) -> (fun _ -> assert false (* absurd case *))
1538   | IOMonad.Value ts -> (fun _ -> ts.Types.fst)
1539   | IOMonad.Wrong x -> (fun _ -> assert false (* absurd case *))) __
1540
1541(** val deprop_as_execute :
1542    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1543    RTLabs_abstract.rTLabs_ext_state -> Events.trace Types.sig0 **)
1544let rec deprop_as_execute ge s s' =
1545  deprop_execute ge s.RTLabs_abstract.ras_state s'.RTLabs_abstract.ras_state
1546
1547type ('o, 'i) partial_flat_trace =
1548| Pft_base of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
1549| Pft_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
1550   * RTLabs_semantics.state * ('o, 'i) partial_flat_trace
1551
1552(** val partial_flat_trace_rect_Type4 :
1553    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
1554    RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
1555    Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
1556    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
1557    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
1558let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_2393 x_2392 = function
1559| Pft_base (s, tr, s') -> h_pft_base s tr s' __
1560| Pft_step (s, tr, s', s'', x_2396) ->
1561  h_pft_step s tr s' s'' __ x_2396
1562    (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_2396)
1563
1564(** val partial_flat_trace_rect_Type3 :
1565    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
1566    RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
1567    Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
1568    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
1569    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
1570let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_2409 x_2408 = function
1571| Pft_base (s, tr, s') -> h_pft_base s tr s' __
1572| Pft_step (s, tr, s', s'', x_2412) ->
1573  h_pft_step s tr s' s'' __ x_2412
1574    (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_2412)
1575
1576(** val partial_flat_trace_rect_Type2 :
1577    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
1578    RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
1579    Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
1580    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
1581    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
1582let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_2417 x_2416 = function
1583| Pft_base (s, tr, s') -> h_pft_base s tr s' __
1584| Pft_step (s, tr, s', s'', x_2420) ->
1585  h_pft_step s tr s' s'' __ x_2420
1586    (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_2420)
1587
1588(** val partial_flat_trace_rect_Type1 :
1589    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
1590    RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
1591    Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
1592    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
1593    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
1594let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_2425 x_2424 = function
1595| Pft_base (s, tr, s') -> h_pft_base s tr s' __
1596| Pft_step (s, tr, s', s'', x_2428) ->
1597  h_pft_step s tr s' s'' __ x_2428
1598    (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_2428)
1599
1600(** val partial_flat_trace_rect_Type0 :
1601    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
1602    RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
1603    Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
1604    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
1605    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
1606let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_2433 x_2432 = function
1607| Pft_base (s, tr, s') -> h_pft_base s tr s' __
1608| Pft_step (s, tr, s', s'', x_2436) ->
1609  h_pft_step s tr s' s'' __ x_2436
1610    (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_2436)
1611
1612(** val partial_flat_trace_inv_rect_Type4 :
1613    RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1614    -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state ->
1615    Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
1616    (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
1617    RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ ->
1618    __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **)
1619let partial_flat_trace_inv_rect_Type4 x3 x4 x5 hterm h1 h2 =
1620  let hcut = partial_flat_trace_rect_Type4 x3 h1 h2 x4 x5 hterm in
1621  hcut __ __ __
1622
1623(** val partial_flat_trace_inv_rect_Type3 :
1624    RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1625    -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state ->
1626    Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
1627    (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
1628    RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ ->
1629    __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **)
1630let partial_flat_trace_inv_rect_Type3 x3 x4 x5 hterm h1 h2 =
1631  let hcut = partial_flat_trace_rect_Type3 x3 h1 h2 x4 x5 hterm in
1632  hcut __ __ __
1633
1634(** val partial_flat_trace_inv_rect_Type2 :
1635    RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1636    -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state ->
1637    Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
1638    (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
1639    RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ ->
1640    __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **)
1641let partial_flat_trace_inv_rect_Type2 x3 x4 x5 hterm h1 h2 =
1642  let hcut = partial_flat_trace_rect_Type2 x3 h1 h2 x4 x5 hterm in
1643  hcut __ __ __
1644
1645(** val partial_flat_trace_inv_rect_Type1 :
1646    RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1647    -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state ->
1648    Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
1649    (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
1650    RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ ->
1651    __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **)
1652let partial_flat_trace_inv_rect_Type1 x3 x4 x5 hterm h1 h2 =
1653  let hcut = partial_flat_trace_rect_Type1 x3 h1 h2 x4 x5 hterm in
1654  hcut __ __ __
1655
1656(** val partial_flat_trace_inv_rect_Type0 :
1657    RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1658    -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state ->
1659    Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
1660    (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
1661    RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ ->
1662    __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **)
1663let partial_flat_trace_inv_rect_Type0 x3 x4 x5 hterm h1 h2 =
1664  let hcut = partial_flat_trace_rect_Type0 x3 h1 h2 x4 x5 hterm in
1665  hcut __ __ __
1666
1667(** val partial_flat_trace_jmdiscr :
1668    RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1669    -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2) partial_flat_trace -> __ **)
1670let partial_flat_trace_jmdiscr a3 a4 a5 x y =
1671  Logic.eq_rect_Type2 x
1672    (match x with
1673     | Pft_base (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1674     | Pft_step (a0, a10, a20, a30, a50) ->
1675       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1676
1677(** val append_partial_flat_trace :
1678    RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1679    -> RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2)
1680    partial_flat_trace -> ('a1, 'a2) partial_flat_trace **)
1681let rec append_partial_flat_trace ge s1 s2 s3 = function
1682| Pft_base (s, tr, s') -> (fun x -> Pft_step (s, tr, s', s3, x))
1683| Pft_step (s, tr, s', s'', tr') ->
1684  (fun tr2 -> Pft_step (s, tr, s', s3,
1685    (append_partial_flat_trace ge s' s'' s3 tr' tr2)))
1686
1687(** val partial_to_flat_trace :
1688    RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1689    -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2) flat_trace -> ('a1, 'a2)
1690    flat_trace **)
1691let rec partial_to_flat_trace ge s1 s2 = function
1692| Pft_base (s, tr0, s') -> (fun x -> lazy (Ft_step (s, tr0, s', x)))
1693| Pft_step (s, tr0, s', s'', tr') ->
1694  (fun tr'' -> lazy (Ft_step (s, tr0, s',
1695    (partial_to_flat_trace ge s' s'' tr' tr''))))
1696
1697(** val flat_trace_of_label_return :
1698    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1699    RTLabs_abstract.rTLabs_ext_state -> StructuredTraces.trace_label_return
1700    -> (IO.io_out, IO.io_in) partial_flat_trace **)
1701let rec flat_trace_of_label_return ge s s' = function
1702| StructuredTraces.Tlr_base (s1, s2, tll) ->
1703  flat_trace_of_label_label ge StructuredTraces.Ends_with_ret (Obj.magic s1)
1704    (Obj.magic s2) tll
1705| StructuredTraces.Tlr_step (s1, s2, s3, tll, tlr) ->
1706  append_partial_flat_trace ge (Obj.magic s1).RTLabs_abstract.ras_state
1707    (Obj.magic s2).RTLabs_abstract.ras_state
1708    (Obj.magic s3).RTLabs_abstract.ras_state
1709    (flat_trace_of_label_label ge StructuredTraces.Doesnt_end_with_ret
1710      (Obj.magic s1) (Obj.magic s2) tll)
1711    (flat_trace_of_label_return ge (Obj.magic s2) (Obj.magic s3) tlr)
1712(** val flat_trace_of_label_label :
1713    RTLabs_semantics.genv -> StructuredTraces.trace_ends_with_ret ->
1714    RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
1715    StructuredTraces.trace_label_label -> (IO.io_out, IO.io_in)
1716    partial_flat_trace **)
1717and flat_trace_of_label_label ge ends0 s s' = function
1718| StructuredTraces.Tll_base (e, s1, s2, tal) ->
1719  flat_trace_of_any_label ge e (Obj.magic s1) (Obj.magic s2) tal
1720(** val flat_trace_of_any_label :
1721    RTLabs_semantics.genv -> StructuredTraces.trace_ends_with_ret ->
1722    RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
1723    StructuredTraces.trace_any_label -> (IO.io_out, IO.io_in)
1724    partial_flat_trace **)
1725and flat_trace_of_any_label ge ends0 s s' = function
1726| StructuredTraces.Tal_base_not_return (s1, s2) ->
1727  let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1728  Pft_base ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1729  (Obj.magic s2).RTLabs_abstract.ras_state)
1730| StructuredTraces.Tal_base_return (s1, s2) ->
1731  let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1732  Pft_base ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1733  (Obj.magic s2).RTLabs_abstract.ras_state)
1734| StructuredTraces.Tal_base_call (s1, s2, s3, tlr) ->
1735  let suffix' =
1736    flat_trace_of_label_return ge (Obj.magic s2) (Obj.magic s3) tlr
1737  in
1738  let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1739  Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1740  (Obj.magic s2).RTLabs_abstract.ras_state,
1741  (Obj.magic s3).RTLabs_abstract.ras_state, suffix')
1742| StructuredTraces.Tal_base_tailcall (s1, s2, s3, tlr) ->
1743  assert false (* absurd case *)
1744| StructuredTraces.Tal_step_call (ends1, s1, s2, s3, s4, tlr, tal) ->
1745  let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1746  Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1747  (Obj.magic s2).RTLabs_abstract.ras_state,
1748  (Obj.magic s4).RTLabs_abstract.ras_state,
1749  (append_partial_flat_trace ge (Obj.magic s2).RTLabs_abstract.ras_state
1750    (Obj.magic s3).RTLabs_abstract.ras_state
1751    (Obj.magic s4).RTLabs_abstract.ras_state
1752    (flat_trace_of_label_return ge (Obj.magic s2) (Obj.magic s3) tlr)
1753    (flat_trace_of_any_label ge ends1 (Obj.magic s3) (Obj.magic s4) tal)))
1754| StructuredTraces.Tal_step_default (ends1, s1, s2, s3, tal) ->
1755  let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1756  Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1757  (Obj.magic s2).RTLabs_abstract.ras_state,
1758  (Obj.magic s3).RTLabs_abstract.ras_state,
1759  (flat_trace_of_any_label ge ends1 (Obj.magic s2) (Obj.magic s3) tal))
1760
1761(** val flat_trace_of_any_call :
1762    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1763    RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
1764    Events.trace -> StructuredTraces.trace_any_call -> (IO.io_out, IO.io_in)
1765    partial_flat_trace **)
1766let rec flat_trace_of_any_call ge s s' s'' et tr =
1767  (match tr with
1768   | StructuredTraces.Tac_base s1 ->
1769     (fun _ -> Pft_base ((Obj.magic s1).RTLabs_abstract.ras_state, et,
1770       s''.RTLabs_abstract.ras_state))
1771   | StructuredTraces.Tac_step_call (s1, s2, s3, s4, tlr, tac) ->
1772     (fun _ ->
1773       let et0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s4) in
1774       Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, et0,
1775       (Obj.magic s4).RTLabs_abstract.ras_state,
1776       s''.RTLabs_abstract.ras_state,
1777       (append_partial_flat_trace ge (Obj.magic s4).RTLabs_abstract.ras_state
1778         (Obj.magic s2).RTLabs_abstract.ras_state
1779         s''.RTLabs_abstract.ras_state
1780         (flat_trace_of_label_return ge (Obj.magic s4) (Obj.magic s2) tlr)
1781         (flat_trace_of_any_call ge (Obj.magic s2) (Obj.magic s3) s'' et tac))))
1782   | StructuredTraces.Tac_step_default (s1, s2, s3, tal) ->
1783     (fun _ ->
1784       let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s3) in
1785       Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1786       (Obj.magic s3).RTLabs_abstract.ras_state,
1787       s''.RTLabs_abstract.ras_state,
1788       (flat_trace_of_any_call ge (Obj.magic s3) (Obj.magic s2) s'' et tal))))
1789    __
1790
1791(** val flat_trace_of_label_call :
1792    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1793    RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
1794    Events.trace -> StructuredTraces.trace_label_call -> (IO.io_out,
1795    IO.io_in) partial_flat_trace **)
1796let rec flat_trace_of_label_call ge s s' s'' et tr =
1797  (let StructuredTraces.Tlc_base (s1, s2, tac) = tr in
1798  (fun _ ->
1799  flat_trace_of_any_call ge (Obj.magic s1) (Obj.magic s2) s'' et tac)) __
1800
1801(** val flat_trace_of_label_diverges :
1802    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1803    StructuredTraces.trace_label_diverges -> (IO.io_out, IO.io_in) flat_trace **)
1804let rec flat_trace_of_label_diverges ge s tr =
1805  match Lazy.force
1806  tr with
1807  | StructuredTraces.Tld_step (sx, sy, tll, tld) ->
1808    (let { RTLabs_abstract.ras_state = sy'; RTLabs_abstract.ras_fn_stack =
1809       stk } = Obj.magic sy
1810     in
1811    (fun tll0 ->
1812    (match flat_trace_of_label_label ge StructuredTraces.Doesnt_end_with_ret
1813             (Obj.magic sx) { RTLabs_abstract.ras_state = sy';
1814             RTLabs_abstract.ras_fn_stack = stk } tll0 with
1815     | Pft_base (s1, tr0, s2) ->
1816       (fun _ tld0 -> lazy (Ft_step (s1, tr0, s2,
1817         (flat_trace_of_label_diverges ge { RTLabs_abstract.ras_state = s2;
1818           RTLabs_abstract.ras_fn_stack = stk } tld0))))
1819     | Pft_step (s1, et, s2, s3, tr') ->
1820       (fun _ tld0 -> lazy (Ft_step (s1, et, s2,
1821         (add_partial_flat_trace ge s2 { RTLabs_abstract.ras_state = s3;
1822           RTLabs_abstract.ras_fn_stack = stk } tr' tld0))))) __)) tll tld
1823  | StructuredTraces.Tld_base (s1, s2, s3, tlc, tld) ->
1824    (let { RTLabs_abstract.ras_state = s3'; RTLabs_abstract.ras_fn_stack =
1825       stk } = Obj.magic s3
1826     in
1827    (fun _ ->
1828    let tr0 =
1829      deprop_as_execute ge (Obj.magic s2) { RTLabs_abstract.ras_state = s3';
1830        RTLabs_abstract.ras_fn_stack = stk }
1831    in
1832    (match flat_trace_of_label_call ge (Obj.magic s1) (Obj.magic s2)
1833             { RTLabs_abstract.ras_state = s3';
1834             RTLabs_abstract.ras_fn_stack = stk } tr0 tlc with
1835     | Pft_base (s10, tr1, s20) ->
1836       (fun _ tld0 -> lazy (Ft_step (s10, tr1, s20,
1837         (flat_trace_of_label_diverges ge { RTLabs_abstract.ras_state = s20;
1838           RTLabs_abstract.ras_fn_stack = stk } tld0))))
1839     | Pft_step (s10, et, s20, s30, tr') ->
1840       (fun _ tld0 -> lazy (Ft_step (s10, et, s20,
1841         (add_partial_flat_trace ge s20 { RTLabs_abstract.ras_state = s30;
1842           RTLabs_abstract.ras_fn_stack = stk } tr' tld0))))) __)) __ tld
1843(** val add_partial_flat_trace :
1844    RTLabs_semantics.genv -> RTLabs_semantics.state ->
1845    RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in)
1846    partial_flat_trace -> StructuredTraces.trace_label_diverges ->
1847    (IO.io_out, IO.io_in) flat_trace **)
1848and add_partial_flat_trace ge s s' =
1849  let { RTLabs_abstract.ras_state = sx; RTLabs_abstract.ras_fn_stack =
1850    stk } = s'
1851  in
1852  (fun ptr ->
1853  (match ptr with
1854   | Pft_base (s0, tr, s'0) ->
1855     (fun _ tr0 -> lazy (Ft_step (s0, tr, s'0,
1856       (flat_trace_of_label_diverges ge { RTLabs_abstract.ras_state = s'0;
1857         RTLabs_abstract.ras_fn_stack = stk } tr0))))
1858   | Pft_step (s1, et, s2, s3, tr') ->
1859     (fun _ tr -> lazy (Ft_step (s1, et, s2,
1860       (add_partial_flat_trace ge s2 { RTLabs_abstract.ras_state = s3;
1861         RTLabs_abstract.ras_fn_stack = stk } tr' tr))))) __)
1862
1863(** val flat_trace_of_whole_program :
1864    RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1865    StructuredTraces.trace_whole_program -> (IO.io_out, IO.io_in) flat_trace **)
1866let rec flat_trace_of_whole_program ge s = function
1867| StructuredTraces.Twp_terminating (s1, s2, sf, tlr) ->
1868  let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1869  lazy (Ft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1870  (Obj.magic s2).RTLabs_abstract.ras_state,
1871  (partial_to_flat_trace ge (Obj.magic s2).RTLabs_abstract.ras_state
1872    (Obj.magic sf).RTLabs_abstract.ras_state
1873    (flat_trace_of_label_return ge (Obj.magic s2) (Obj.magic sf) tlr)
1874    (lazy (Ft_stop (Obj.magic sf).RTLabs_abstract.ras_state)))))
1875| StructuredTraces.Twp_diverges (s1, s2, tld) ->
1876  let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1877  lazy (Ft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1878  (Obj.magic s2).RTLabs_abstract.ras_state,
1879  (flat_trace_of_label_diverges ge (Obj.magic s2) tld)))
1880
1881(** val state_fn :
1882    RTLabs_semantics.genv -> __ -> Pointers.block Types.option **)
1883let state_fn ge s =
1884  match (Obj.magic s).RTLabs_abstract.ras_fn_stack with
1885  | List.Nil -> Types.None
1886  | List.Cons (h, t) ->
1887    (match (Obj.magic s).RTLabs_abstract.ras_state with
1888     | RTLabs_semantics.State (x, x0, x1) -> Types.Some h
1889     | RTLabs_semantics.Callstate (x, x0, x1, x2, x3, x4) ->
1890       (match t with
1891        | List.Nil -> Types.None
1892        | List.Cons (h', x5) -> Types.Some h')
1893     | RTLabs_semantics.Returnstate (x, x0, x1, x2) -> Types.Some h
1894     | RTLabs_semantics.Finalstate x -> Types.Some h)
1895
1896(** val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __ **)
1897let option_jmdiscr x y =
1898  Logic.eq_rect_Type2 x
1899    (match x with
1900     | Types.None -> Obj.magic (fun _ dH -> dH)
1901     | Types.Some a0 -> Obj.magic (fun _ dH -> dH __)) y
1902
Note: See TracBrowser for help on using the repository browser.