Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/rTLabs_traces.ml

    r2743 r2773  
    1111open StructuredTraces
    1212
     13open BitVectorTrie
     14
    1315open Graphs
    1416
     
    2224
    2325open SmallstepExec
    24 
    25 open BitVectorTrie
    2626
    2727open CostLabel
     
    139139type ('o, 'i) flat_trace = ('o, 'i) __flat_trace Lazy.t
    140140and ('o, 'i) __flat_trace =
    141 | Ft_stop of RTLabs_semantics.state0
    142 | Ft_step of RTLabs_semantics.state0 * Events.trace * RTLabs_semantics.state0
     141| Ft_stop of RTLabs_semantics.state
     142| Ft_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
    143143   * ('o, 'i) flat_trace
    144144
    145145(** val flat_trace_inv_rect_Type4 :
    146     RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
    147     -> (RTLabs_semantics.state0 -> __ -> __ -> __ -> 'a3) ->
    148     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
     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 -> __
    149149    -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **)
    150150let flat_trace_inv_rect_Type4 x3 x4 hterm h1 h2 =
     
    158158
    159159(** val flat_trace_inv_rect_Type3 :
    160     RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
    161     -> (RTLabs_semantics.state0 -> __ -> __ -> __ -> 'a3) ->
    162     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
     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 -> __
    163163    -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **)
    164164let flat_trace_inv_rect_Type3 x3 x4 hterm h1 h2 =
     
    172172
    173173(** val flat_trace_inv_rect_Type2 :
    174     RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
    175     -> (RTLabs_semantics.state0 -> __ -> __ -> __ -> 'a3) ->
    176     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
     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 -> __
    177177    -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **)
    178178let flat_trace_inv_rect_Type2 x3 x4 hterm h1 h2 =
     
    186186
    187187(** val flat_trace_inv_rect_Type1 :
    188     RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
    189     -> (RTLabs_semantics.state0 -> __ -> __ -> __ -> 'a3) ->
    190     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
     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 -> __
    191191    -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **)
    192192let flat_trace_inv_rect_Type1 x3 x4 hterm h1 h2 =
     
    200200
    201201(** val flat_trace_inv_rect_Type0 :
    202     RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
    203     -> (RTLabs_semantics.state0 -> __ -> __ -> __ -> 'a3) ->
    204     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
     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 -> __
    205205    -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **)
    206206let flat_trace_inv_rect_Type0 x3 x4 hterm h1 h2 =
     
    214214
    215215(** val flat_trace_discr :
    216     RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
     216    RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace
    217217    -> ('a1, 'a2) flat_trace -> __ **)
    218218let flat_trace_discr a3 a4 x y =
     
    225225
    226226(** val flat_trace_jmdiscr :
    227     RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
     227    RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace
    228228    -> ('a1, 'a2) flat_trace -> __ **)
    229229let flat_trace_jmdiscr a3 a4 x y =
     
    236236
    237237(** val make_flat_trace :
    238     __ -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace **)
     238    __ -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace **)
    239239let rec make_flat_trace ge s =
    240   let e1 =
     240  let e =
    241241    SmallstepExec.exec_inf_aux
    242242      RTLabs_semantics.rTLabs_fullexec.SmallstepExec.es1 ge
     
    244244  in
    245245  (match Lazy.force
    246    e1 with
     246   e with
    247247   | SmallstepExec.E_stop (tr, i, s') ->
    248248     (fun _ -> lazy (Ft_step (s, tr, (Obj.magic s'), (lazy (Ft_stop
     
    259259let make_whole_flat_trace p s =
    260260  let ge = RTLabs_semantics.rTLabs_fullexec.SmallstepExec.make_global p in
    261   let e1 =
     261  let e =
    262262    SmallstepExec.exec_inf_aux
    263263      RTLabs_semantics.rTLabs_fullexec.SmallstepExec.es1 ge (IOMonad.Value
     
    265265  in
    266266  (match Lazy.force
    267    e1 with
     267   e with
    268268   | SmallstepExec.E_stop (tr, i, s') ->
    269269     (fun _ -> lazy (Ft_stop (Obj.magic s)))
     
    275275
    276276type will_return =
    277 | Wr_step of RTLabs_semantics.state0 * Events.trace * RTLabs_semantics.state0
     277| Wr_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
    278278   * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
    279 | Wr_call of RTLabs_semantics.state0 * Events.trace * RTLabs_semantics.state0
     279| Wr_call of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
    280280   * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
    281 | Wr_ret of RTLabs_semantics.state0 * Events.trace * RTLabs_semantics.state0
     281| Wr_ret of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
    282282   * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
    283 | Wr_base of RTLabs_semantics.state0 * Events.trace * RTLabs_semantics.state0
     283| Wr_base of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
    284284   * (IO.io_out, IO.io_in) flat_trace
    285285
    286286(** val will_return_rect_Type4 :
    287     RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
    288     RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    289     flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
    290     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
     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 ->
    291293    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    292     'a1 -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
    293     RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    294     flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
    295     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
    296     -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1) -> Nat.nat ->
    297     RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace ->
    298     will_return -> 'a1 **)
    299 let rec will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17438 s x_17437 = function
    300 | Wr_step (s0, tr, s', depth, trace0, x_17440) ->
    301   h_wr_step s0 tr s' depth __ trace0 __ x_17440
     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_12748 s x_12747 = function
     299| Wr_step (s0, tr, s', depth, trace, x_12750) ->
     300  h_wr_step s0 tr s' depth __ trace __ x_12750
    302301    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    303       s' trace0 x_17440)
    304 | Wr_call (s0, tr, s', depth, trace0, x_17442) ->
    305   h_wr_call s0 tr s' depth __ trace0 __ x_17442
     302      s' trace x_12750)
     303| Wr_call (s0, tr, s', depth, trace, x_12752) ->
     304  h_wr_call s0 tr s' depth __ trace __ x_12752
    306305    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    307       depth) s' trace0 x_17442)
    308 | Wr_ret (s0, tr, s', depth, trace0, x_17444) ->
    309   h_wr_ret s0 tr s' depth __ trace0 __ x_17444
     306      depth) s' trace x_12752)
     307| Wr_ret (s0, tr, s', depth, trace, x_12754) ->
     308  h_wr_ret s0 tr s' depth __ trace __ x_12754
    310309    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    311       s' trace0 x_17444)
    312 | Wr_base (s0, tr, s', trace0) -> h_wr_base s0 tr s' __ trace0 __
     310      s' trace x_12754)
     311| Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
    313312
    314313(** val will_return_rect_Type3 :
    315     RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
    316     RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    317     flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
    318     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
     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 ->
    319320    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    320     'a1 -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
    321     RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    322     flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
    323     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
    324     -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1) -> Nat.nat ->
    325     RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace ->
    326     will_return -> 'a1 **)
    327 let rec will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17466 s x_17465 = function
    328 | Wr_step (s0, tr, s', depth, trace0, x_17468) ->
    329   h_wr_step s0 tr s' depth __ trace0 __ x_17468
     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_12776 s x_12775 = function
     326| Wr_step (s0, tr, s', depth, trace, x_12778) ->
     327  h_wr_step s0 tr s' depth __ trace __ x_12778
    330328    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    331       s' trace0 x_17468)
    332 | Wr_call (s0, tr, s', depth, trace0, x_17470) ->
    333   h_wr_call s0 tr s' depth __ trace0 __ x_17470
     329      s' trace x_12778)
     330| Wr_call (s0, tr, s', depth, trace, x_12780) ->
     331  h_wr_call s0 tr s' depth __ trace __ x_12780
    334332    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    335       depth) s' trace0 x_17470)
    336 | Wr_ret (s0, tr, s', depth, trace0, x_17472) ->
    337   h_wr_ret s0 tr s' depth __ trace0 __ x_17472
     333      depth) s' trace x_12780)
     334| Wr_ret (s0, tr, s', depth, trace, x_12782) ->
     335  h_wr_ret s0 tr s' depth __ trace __ x_12782
    338336    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    339       s' trace0 x_17472)
    340 | Wr_base (s0, tr, s', trace0) -> h_wr_base s0 tr s' __ trace0 __
     337      s' trace x_12782)
     338| Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
    341339
    342340(** val will_return_rect_Type2 :
    343     RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
    344     RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    345     flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
    346     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
     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 ->
    347347    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    348     'a1 -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
    349     RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    350     flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
    351     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
    352     -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1) -> Nat.nat ->
    353     RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace ->
    354     will_return -> 'a1 **)
    355 let rec will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17480 s x_17479 = function
    356 | Wr_step (s0, tr, s', depth, trace0, x_17482) ->
    357   h_wr_step s0 tr s' depth __ trace0 __ x_17482
     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_12790 s x_12789 = function
     353| Wr_step (s0, tr, s', depth, trace, x_12792) ->
     354  h_wr_step s0 tr s' depth __ trace __ x_12792
    358355    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    359       s' trace0 x_17482)
    360 | Wr_call (s0, tr, s', depth, trace0, x_17484) ->
    361   h_wr_call s0 tr s' depth __ trace0 __ x_17484
     356      s' trace x_12792)
     357| Wr_call (s0, tr, s', depth, trace, x_12794) ->
     358  h_wr_call s0 tr s' depth __ trace __ x_12794
    362359    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    363       depth) s' trace0 x_17484)
    364 | Wr_ret (s0, tr, s', depth, trace0, x_17486) ->
    365   h_wr_ret s0 tr s' depth __ trace0 __ x_17486
     360      depth) s' trace x_12794)
     361| Wr_ret (s0, tr, s', depth, trace, x_12796) ->
     362  h_wr_ret s0 tr s' depth __ trace __ x_12796
    366363    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    367       s' trace0 x_17486)
    368 | Wr_base (s0, tr, s', trace0) -> h_wr_base s0 tr s' __ trace0 __
     364      s' trace x_12796)
     365| Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
    369366
    370367(** val will_return_rect_Type1 :
    371     RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
    372     RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    373     flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
    374     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
     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 ->
    375374    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    376     'a1 -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
    377     RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    378     flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
    379     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
    380     -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1) -> Nat.nat ->
    381     RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace ->
    382     will_return -> 'a1 **)
    383 let rec will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17494 s x_17493 = function
    384 | Wr_step (s0, tr, s', depth, trace0, x_17496) ->
    385   h_wr_step s0 tr s' depth __ trace0 __ x_17496
     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_12804 s x_12803 = function
     380| Wr_step (s0, tr, s', depth, trace, x_12806) ->
     381  h_wr_step s0 tr s' depth __ trace __ x_12806
    386382    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    387       s' trace0 x_17496)
    388 | Wr_call (s0, tr, s', depth, trace0, x_17498) ->
    389   h_wr_call s0 tr s' depth __ trace0 __ x_17498
     383      s' trace x_12806)
     384| Wr_call (s0, tr, s', depth, trace, x_12808) ->
     385  h_wr_call s0 tr s' depth __ trace __ x_12808
    390386    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    391       depth) s' trace0 x_17498)
    392 | Wr_ret (s0, tr, s', depth, trace0, x_17500) ->
    393   h_wr_ret s0 tr s' depth __ trace0 __ x_17500
     387      depth) s' trace x_12808)
     388| Wr_ret (s0, tr, s', depth, trace, x_12810) ->
     389  h_wr_ret s0 tr s' depth __ trace __ x_12810
    394390    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    395       s' trace0 x_17500)
    396 | Wr_base (s0, tr, s', trace0) -> h_wr_base s0 tr s' __ trace0 __
     391      s' trace x_12810)
     392| Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
    397393
    398394(** val will_return_rect_Type0 :
    399     RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
    400     RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    401     flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
    402     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
     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 ->
    403401    Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    404     'a1 -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
    405     RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    406     flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
    407     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
    408     -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1) -> Nat.nat ->
    409     RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace ->
    410     will_return -> 'a1 **)
    411 let rec will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17508 s x_17507 = function
    412 | Wr_step (s0, tr, s', depth, trace0, x_17510) ->
    413   h_wr_step s0 tr s' depth __ trace0 __ x_17510
     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_12818 s x_12817 = function
     407| Wr_step (s0, tr, s', depth, trace, x_12820) ->
     408  h_wr_step s0 tr s' depth __ trace __ x_12820
    414409    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    415       s' trace0 x_17510)
    416 | Wr_call (s0, tr, s', depth, trace0, x_17512) ->
    417   h_wr_call s0 tr s' depth __ trace0 __ x_17512
     410      s' trace x_12820)
     411| Wr_call (s0, tr, s', depth, trace, x_12822) ->
     412  h_wr_call s0 tr s' depth __ trace __ x_12822
    418413    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    419       depth) s' trace0 x_17512)
    420 | Wr_ret (s0, tr, s', depth, trace0, x_17514) ->
    421   h_wr_ret s0 tr s' depth __ trace0 __ x_17514
     414      depth) s' trace x_12822)
     415| Wr_ret (s0, tr, s', depth, trace, x_12824) ->
     416  h_wr_ret s0 tr s' depth __ trace __ x_12824
    422417    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    423       s' trace0 x_17514)
    424 | Wr_base (s0, tr, s', trace0) -> h_wr_base s0 tr s' __ trace0 __
     418      s' trace x_12824)
     419| Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
    425420
    426421(** val will_return_inv_rect_Type4 :
    427     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
    428     (IO.io_out, IO.io_in) flat_trace -> will_return ->
    429     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
    430     Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    431     (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
    432     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
    433     Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    434     (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
    435     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
    436     Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    437     (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
    438     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
    439     -> (IO.io_out, IO.io_in) flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1)
    440     -> 'a1 **)
     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 **)
    441435let will_return_inv_rect_Type4 x1 x2 x3 x4 hterm h1 h2 h3 h4 =
    442436  let hcut = will_return_rect_Type4 x1 h1 h2 h3 h4 x2 x3 x4 hterm in
     
    444438
    445439(** val will_return_inv_rect_Type3 :
    446     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
    447     (IO.io_out, IO.io_in) flat_trace -> will_return ->
    448     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
    449     Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    450     (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
    451     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
    452     Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    453     (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
    454     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
    455     Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    456     (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
    457     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
    458     -> (IO.io_out, IO.io_in) flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1)
    459     -> 'a1 **)
     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 **)
    460453let will_return_inv_rect_Type3 x1 x2 x3 x4 hterm h1 h2 h3 h4 =
    461454  let hcut = will_return_rect_Type3 x1 h1 h2 h3 h4 x2 x3 x4 hterm in
     
    463456
    464457(** val will_return_inv_rect_Type2 :
    465     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
    466     (IO.io_out, IO.io_in) flat_trace -> will_return ->
    467     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
    468     Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    469     (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
    470     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
    471     Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    472     (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
    473     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
    474     Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    475     (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
    476     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
    477     -> (IO.io_out, IO.io_in) flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1)
    478     -> 'a1 **)
     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 **)
    479471let will_return_inv_rect_Type2 x1 x2 x3 x4 hterm h1 h2 h3 h4 =
    480472  let hcut = will_return_rect_Type2 x1 h1 h2 h3 h4 x2 x3 x4 hterm in
     
    482474
    483475(** val will_return_inv_rect_Type1 :
    484     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
    485     (IO.io_out, IO.io_in) flat_trace -> will_return ->
    486     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
    487     Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    488     (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
    489     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
    490     Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    491     (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
    492     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
    493     Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    494     (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
    495     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
    496     -> (IO.io_out, IO.io_in) flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1)
    497     -> 'a1 **)
     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 **)
    498489let will_return_inv_rect_Type1 x1 x2 x3 x4 hterm h1 h2 h3 h4 =
    499490  let hcut = will_return_rect_Type1 x1 h1 h2 h3 h4 x2 x3 x4 hterm in
     
    501492
    502493(** val will_return_inv_rect_Type0 :
    503     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
    504     (IO.io_out, IO.io_in) flat_trace -> will_return ->
    505     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
    506     Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    507     (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
    508     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
    509     Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    510     (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
    511     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
    512     Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    513     (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) ->
    514     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
    515     -> (IO.io_out, IO.io_in) flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1)
    516     -> 'a1 **)
     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 **)
    517507let will_return_inv_rect_Type0 x1 x2 x3 x4 hterm h1 h2 h3 h4 =
    518508  let hcut = will_return_rect_Type0 x1 h1 h2 h3 h4 x2 x3 x4 hterm in
     
    520510
    521511(** val will_return_jmdiscr :
    522     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
    523     (IO.io_out, IO.io_in) flat_trace -> will_return -> will_return -> __ **)
     512    RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
     513    IO.io_in) flat_trace -> will_return -> will_return -> __ **)
    524514let will_return_jmdiscr a1 a2 a3 a4 x y =
    525515  Logic.eq_rect_Type2 x
     
    535525
    536526(** val will_return_length :
    537     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
    538     (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat **)
     527    RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
     528    IO.io_in) flat_trace -> will_return -> Nat.nat **)
    539529let rec will_return_length ge d s tr = function
    540530| Wr_step (x, x0, x1, x2, x4, t') ->
     
    546536
    547537(** val will_return_end :
    548     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
    549     (IO.io_out, IO.io_in) flat_trace -> will_return ->
    550     (RTLabs_semantics.state0, (IO.io_out, IO.io_in) flat_trace) Types.dPair **)
     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 **)
    551541let rec will_return_end ge d s tr = function
    552542| Wr_step (x, x0, x1, x2, x4, t') -> will_return_end ge x2 x1 x4 t'
     
    556546
    557547(** val will_return_call :
    558     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
    559     Events.trace -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in)
     548    RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state ->
     549    Events.trace -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    560550    flat_trace -> will_return -> will_return Types.sig0 **)
    561 let will_return_call ge d s tr s' trace0 tERM =
    562   will_return_inv_rect_Type0 ge d s (lazy (Ft_step (s, tr, s', trace0))) tERM
     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
    563553    (fun h19 h20 h21 h22 _ h24 _ h26 h27 _ _ _ _ -> assert false
    564554    (* absurd case *)) (fun h33 h34 h35 h36 _ h38 _ h40 h41 _ _ _ _ ->
     
    566556      Logic.eq_rect_Type0_r h33 (fun _ _ _ tERM1 h411 _ ->
    567557        Obj.magic flat_trace_jmdiscr ge h33 (lazy (Ft_step (h33, tr, s',
    568           trace0))) (lazy (Ft_step (h33, h34, h35, h38))) __ (fun _ ->
     558          trace))) (lazy (Ft_step (h33, h34, h35, h38))) __ (fun _ ->
    569559          Logic.streicherK h33 (fun _ ->
    570560            Logic.eq_rect_Type0_r h34 (fun _ _ tERM2 h412 _ _ ->
    571               Logic.eq_rect_Type0_r h35 (fun trace1 _ _ tERM3 h413 _ _ ->
     561              Logic.eq_rect_Type0_r h35 (fun trace0 _ _ tERM3 h413 _ _ ->
    572562                Logic.eq_rect_Type0_r __ (fun _ tERM4 h414 _ _ ->
    573563                  Logic.eq_rect_Type0_r h38 (fun _ tERM5 h415 _ ->
    574564                    Logic.streicherK (lazy (Ft_step (h33, h34, h35, h38)))
    575565                      (Logic.eq_rect_Type0_r (Wr_call (h33, h34, h35, h36,
    576                         h38, h40)) (fun h416 -> h40) tERM5 h415)) trace1 __
    577                     tERM4 h414 __) __ __ tERM3 h413 __) s' trace0 __ __ tERM2
     566                        h38, h40)) (fun h416 -> h40) tERM5 h415)) trace0 __
     567                    tERM4 h414 __) __ __ tERM3 h413 __) s' trace __ __ tERM2
    578568                h412 __) tr __ __ tERM1 h411 __))) s __ __ __ tERM0 h410 __)
    579569      d tERM h41 __) (fun h47 h48 h49 h50 _ h52 _ h54 h55 _ _ _ _ ->
     
    582572
    583573(** val will_return_return :
    584     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
    585     Events.trace -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in)
     574    RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state ->
     575    Events.trace -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    586576    flat_trace -> will_return -> __ **)
    587 let will_return_return ge d s tr s' trace0 tERM =
    588   will_return_inv_rect_Type0 ge d s (lazy (Ft_step (s, tr, s', trace0))) tERM
     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
    589579    (fun h19 h20 h21 h22 _ h24 _ h26 h27 _ _ _ _ -> assert false
    590580    (* absurd case *)) (fun h33 h34 h35 h36 _ h38 _ h40 h41 _ _ _ _ ->
     
    594584      Logic.eq_rect_Type0_r h47 (fun _ _ _ tERM1 h551 _ ->
    595585        Obj.magic flat_trace_jmdiscr ge h47 (lazy (Ft_step (h47, tr, s',
    596           trace0))) (lazy (Ft_step (h47, h48, h49, h52))) __ (fun _ ->
     586          trace))) (lazy (Ft_step (h47, h48, h49, h52))) __ (fun _ ->
    597587          Logic.streicherK h47 (fun _ ->
    598588            Logic.eq_rect_Type0_r h48 (fun _ _ tERM2 h552 _ _ ->
    599               Logic.eq_rect_Type0_r h49 (fun trace1 _ _ tERM3 h553 _ _ ->
     589              Logic.eq_rect_Type0_r h49 (fun trace0 _ _ tERM3 h553 _ _ ->
    600590                Logic.eq_rect_Type0_r __ (fun _ tERM4 h554 _ _ ->
    601591                  Logic.eq_rect_Type0_r h52 (fun _ tERM5 h555 _ ->
    602592                    Logic.streicherK (lazy (Ft_step (h47, h48, h49, h52)))
    603593                      (Logic.eq_rect_Type0_r (Wr_ret (h47, h48, h49, h50,
    604                         h52, h54)) (fun h556 -> h54) tERM5 h555)) trace1 __
    605                     tERM4 h554 __) __ __ tERM3 h553 __) s' trace0 __ __ tERM2
     594                        h52, h54)) (fun h556 -> h54) tERM5 h555)) trace0 __
     595                    tERM4 h554 __) __ __ tERM3 h553 __) s' trace __ __ tERM2
    606596                h552 __) tr __ __ tERM1 h551 __))) s __ __ __ tERM0 h550 __)
    607597      d tERM h55 __) (Obj.magic __)
    608598
    609599(** val will_return_notfn :
    610     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
    611     Events.trace -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in)
     600    RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state ->
     601    Events.trace -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    612602    flat_trace -> (__, __) Types.sum -> will_return -> will_return Types.sig0 **)
    613 let will_return_notfn ge d s tr s' trace0 = function
     603let will_return_notfn ge d s tr s' trace = function
    614604| Types.Inl _ ->
    615605  (fun tERM ->
    616     will_return_inv_rect_Type0 ge d s (lazy (Ft_step (s, tr, s', trace0)))
     606    will_return_inv_rect_Type0 ge d s (lazy (Ft_step (s, tr, s', trace)))
    617607      tERM (fun h290 h291 h292 h293 _ h295 _ h297 h298 _ _ _ _ ->
    618608      Logic.eq_rect_Type0_r h293 (fun tERM0 h2980 _ ->
    619609        Logic.eq_rect_Type0_r h290 (fun _ _ _ tERM1 h2981 _ ->
    620610          Obj.magic flat_trace_jmdiscr ge h290 (lazy (Ft_step (h290, tr, s',
    621             trace0))) (lazy (Ft_step (h290, h291, h292, h295))) __ (fun _ ->
     611            trace))) (lazy (Ft_step (h290, h291, h292, h295))) __ (fun _ ->
    622612            Logic.streicherK h290 (fun _ ->
    623613              Logic.eq_rect_Type0_r h291 (fun _ _ tERM2 h2982 _ _ ->
    624                 Logic.eq_rect_Type0_r h292 (fun trace1 _ _ tERM3 h2983 _ _ ->
     614                Logic.eq_rect_Type0_r h292 (fun trace0 _ _ tERM3 h2983 _ _ ->
    625615                  Logic.eq_rect_Type0_r __ (fun _ tERM4 h2984 _ _ ->
    626616                    Logic.eq_rect_Type0_r h295 (fun _ tERM5 h2985 _ ->
     
    629619                        (Logic.eq_rect_Type0_r (Wr_step (h290, h291, h292,
    630620                          h293, h295, h297)) (fun h2986 -> h297) tERM5 h2985))
    631                       trace1 __ tERM4 h2984 __) __ __ tERM3 h2983 __) s'
    632                   trace0 __ __ tERM2 h2982 __) tr __ __ tERM1 h2981 __))) s
    633           __ __ __ tERM0 h2980 __) d tERM h298 __)
     621                      trace0 __ tERM4 h2984 __) __ __ tERM3 h2983 __) s'
     622                  trace __ __ tERM2 h2982 __) tr __ __ tERM1 h2981 __))) s __
     623          __ __ tERM0 h2980 __) d tERM h298 __)
    634624      (fun h304 h305 h306 h307 _ h309 _ h311 h312 _ _ _ _ -> assert false
    635625      (* absurd case *))
     
    639629| Types.Inr _ ->
    640630  (fun tERM ->
    641     will_return_inv_rect_Type0 ge d s (lazy (Ft_step (s, tr, s', trace0)))
     631    will_return_inv_rect_Type0 ge d s (lazy (Ft_step (s, tr, s', trace)))
    642632      tERM (fun h343 h344 h345 h346 _ h348 _ h350 h351 _ _ _ _ ->
    643633      Logic.eq_rect_Type0_r h346 (fun tERM0 h3510 _ ->
    644634        Logic.eq_rect_Type0_r h343 (fun _ _ _ tERM1 h3511 _ ->
    645635          Obj.magic flat_trace_jmdiscr ge h343 (lazy (Ft_step (h343, tr, s',
    646             trace0))) (lazy (Ft_step (h343, h344, h345, h348))) __ (fun _ ->
     636            trace))) (lazy (Ft_step (h343, h344, h345, h348))) __ (fun _ ->
    647637            Logic.streicherK h343 (fun _ ->
    648638              Logic.eq_rect_Type0_r h344 (fun _ _ tERM2 h3512 _ _ ->
    649                 Logic.eq_rect_Type0_r h345 (fun trace1 _ _ tERM3 h3513 _ _ ->
     639                Logic.eq_rect_Type0_r h345 (fun trace0 _ _ tERM3 h3513 _ _ ->
    650640                  Logic.eq_rect_Type0_r __ (fun _ tERM4 h3514 _ _ ->
    651641                    Logic.eq_rect_Type0_r h348 (fun _ tERM5 h3515 _ ->
     
    654644                        (Logic.eq_rect_Type0_r (Wr_step (h343, h344, h345,
    655645                          h346, h348, h350)) (fun h3516 -> h350) tERM5 h3515))
    656                       trace1 __ tERM4 h3514 __) __ __ tERM3 h3513 __) s'
    657                   trace0 __ __ tERM2 h3512 __) tr __ __ tERM1 h3511 __))) s
    658           __ __ __ tERM0 h3510 __) d tERM h351 __)
     646                      trace0 __ tERM4 h3514 __) __ __ tERM3 h3513 __) s'
     647                  trace __ __ tERM2 h3512 __) tr __ __ tERM1 h3511 __))) s __
     648          __ __ tERM0 h3510 __) d tERM h351 __)
    659649      (fun h357 h358 h359 h360 _ h362 _ h364 h365 _ _ _ _ -> assert false
    660650      (* absurd case *))
     
    664654
    665655(** val will_return_prepend :
    666     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
    667     (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
    668     RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace ->
    669     will_return -> will_return **)
     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 **)
    670659let will_return_prepend ge d1 s1 tr1 t1 d2 s2 t2 x =
    671660  will_return_rect_Type0 ge (fun s tr s' depth _ t _ t0 iH d3 s3 t3 t4 _ ->
     
    692681
    693682(** val will_return_remove_call :
    694     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
    695     (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> will_return
    696     -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace ->
    697     will_return **)
     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 **)
    698686let will_return_remove_call ge d1x s1x t1x t1 d2 x s2 t2 =
    699687  will_return_rect_Type0 ge (fun s tr s' d1 _ t _ t0 iH d3 t3 s3 t4 _ ->
     
    818806
    819807(** val will_return_lower :
    820     RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 ->
    821     (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> will_return **)
     808    RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
     809    IO.io_in) flat_trace -> will_return -> Nat.nat -> will_return **)
    822810let will_return_lower ge d0 s0 t0 tM d' =
    823811  will_return_rect_Type0 ge (fun s tr s' d _ tr0 _ tM1 iH d'0 _ -> Wr_step
     
    851839    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    852840    trace_result -> 'a2 **)
    853 let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_18049 =
     841let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_13359 =
    854842  let { new_state = new_state0; remainder = remainder0; new_trace =
    855     new_trace0; terminates = terminates0 } = x_18049
     843    new_trace0; terminates = terminates0 } = x_13359
    856844  in
    857845  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    863851    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    864852    trace_result -> 'a2 **)
    865 let rec trace_result_rect_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_18051 =
     853let rec trace_result_rect_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_13361 =
    866854  let { new_state = new_state0; remainder = remainder0; new_trace =
    867     new_trace0; terminates = terminates0 } = x_18051
     855    new_trace0; terminates = terminates0 } = x_13361
    868856  in
    869857  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    875863    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    876864    trace_result -> 'a2 **)
    877 let rec trace_result_rect_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_18053 =
     865let rec trace_result_rect_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_13363 =
    878866  let { new_state = new_state0; remainder = remainder0; new_trace =
    879     new_trace0; terminates = terminates0 } = x_18053
     867    new_trace0; terminates = terminates0 } = x_13363
    880868  in
    881869  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    887875    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    888876    trace_result -> 'a2 **)
    889 let rec trace_result_rect_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_18055 =
     877let rec trace_result_rect_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_13365 =
    890878  let { new_state = new_state0; remainder = remainder0; new_trace =
    891     new_trace0; terminates = terminates0 } = x_18055
     879    new_trace0; terminates = terminates0 } = x_13365
    892880  in
    893881  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    899887    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    900888    trace_result -> 'a2 **)
    901 let rec trace_result_rect_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_18057 =
     889let rec trace_result_rect_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_13367 =
    902890  let { new_state = new_state0; remainder = remainder0; new_trace =
    903     new_trace0; terminates = terminates0 } = x_18057
     891    new_trace0; terminates = terminates0 } = x_13367
    904892  in
    905893  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    911899    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    912900    trace_result -> 'a2 **)
    913 let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_18059 =
     901let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_13369 =
    914902  let { new_state = new_state0; remainder = remainder0; new_trace =
    915     new_trace0; terminates = terminates0 } = x_18059
     903    new_trace0; terminates = terminates0 } = x_13369
    916904  in
    917905  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    1011999    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10121000    sub_trace_result -> 'a2 **)
    1013 let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_18077 =
    1014   let { ends = ends0; trace_res = trace_res0 } = x_18077 in
     1001let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_13387 =
     1002  let { ends = ends0; trace_res = trace_res0 } = x_13387 in
    10151003  h_mk_sub_trace_result ends0 trace_res0
    10161004
     
    10201008    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10211009    sub_trace_result -> 'a2 **)
    1022 let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_18079 =
    1023   let { ends = ends0; trace_res = trace_res0 } = x_18079 in
     1010let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_13389 =
     1011  let { ends = ends0; trace_res = trace_res0 } = x_13389 in
    10241012  h_mk_sub_trace_result ends0 trace_res0
    10251013
     
    10291017    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10301018    sub_trace_result -> 'a2 **)
    1031 let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_18081 =
    1032   let { ends = ends0; trace_res = trace_res0 } = x_18081 in
     1019let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_13391 =
     1020  let { ends = ends0; trace_res = trace_res0 } = x_13391 in
    10331021  h_mk_sub_trace_result ends0 trace_res0
    10341022
     
    10381026    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10391027    sub_trace_result -> 'a2 **)
    1040 let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_18083 =
    1041   let { ends = ends0; trace_res = trace_res0 } = x_18083 in
     1028let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_13393 =
     1029  let { ends = ends0; trace_res = trace_res0 } = x_13393 in
    10421030  h_mk_sub_trace_result ends0 trace_res0
    10431031
     
    10471035    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10481036    sub_trace_result -> 'a2 **)
    1049 let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_18085 =
    1050   let { ends = ends0; trace_res = trace_res0 } = x_18085 in
     1037let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_13395 =
     1038  let { ends = ends0; trace_res = trace_res0 } = x_13395 in
    10511039  h_mk_sub_trace_result ends0 trace_res0
    10521040
     
    10561044    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10571045    sub_trace_result -> 'a2 **)
    1058 let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_18087 =
    1059   let { ends = ends0; trace_res = trace_res0 } = x_18087 in
     1046let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_13397 =
     1047  let { ends = ends0; trace_res = trace_res0 } = x_13397 in
    10601048  h_mk_sub_trace_result ends0 trace_res0
    10611049
     
    11431131    -> will_return -> will_return -> Nat.nat -> Nat.nat -> 'a1 trace_result
    11441132    -> 'a2 -> 'a2 trace_result **)
    1145 let replace_trace ge d e1 s1 s2 t1 t2 tM1 tM2 l1 l2 r trace0 =
    1146   { new_state = r.new_state; remainder = r.remainder; new_trace = trace0;
     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;
    11471135    terminates =
    1148     ((match e1 with
     1136    ((match e with
    11491137      | StructuredTraces.Ends_with_ret ->
    11501138        Logic.eq_rect_Type0
     
    11761164    (IO.io_out, IO.io_in) flat_trace -> will_return -> will_return -> Nat.nat
    11771165    -> Nat.nat -> 'a1 sub_trace_result -> 'a2 -> 'a2 sub_trace_result **)
    1178 let replace_sub_trace ge d s1 s2 t1 t2 tM1 tM2 l1 l2 r trace0 =
     1166let replace_sub_trace ge d s1 s2 t1 t2 tM1 tM2 l1 l2 r trace =
    11791167  { ends = r.ends; trace_res =
    1180     (replace_trace ge d r.ends s1 s2 t1 t2 tM1 tM2 l1 l2 r.trace_res trace0) }
     1168    (replace_trace ge d r.ends s1 s2 t1 t2 tM1 tM2 l1 l2 r.trace_res trace) }
    11811169
    11821170(** val make_label_return :
     
    11841172    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
    11851173    StructuredTraces.trace_label_return trace_result **)
    1186 let rec make_label_return ge depth s trace0 tERMINATES tIME =
     1174let rec make_label_return ge depth s trace tERMINATES tIME =
    11871175  (match tIME with
    11881176   | Nat.O -> (fun _ -> assert false (* absurd case *))
    11891177   | Nat.S tIME0 ->
    11901178     (fun _ ->
    1191        let r = make_label_label ge depth s trace0 tERMINATES tIME0 in
     1179       let r = make_label_label ge depth s trace tERMINATES tIME0 in
    11921180       (match r.ends with
    11931181        | StructuredTraces.Ends_with_ret ->
    1194           (fun r5 ->
    1195             replace_trace ge depth StructuredTraces.Ends_with_ret s s trace0
    1196               trace0 tERMINATES tERMINATES
    1197               (will_return_length ge depth s.RTLabs_abstract.ras_state trace0
     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
    11981186                tERMINATES)
    1199               (will_return_length ge depth s.RTLabs_abstract.ras_state trace0
    1200                 tERMINATES) r5 (StructuredTraces.Tlr_base ((Obj.magic s),
    1201               (Obj.magic r5.new_state), r5.new_trace)))
     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)))
    12021190        | StructuredTraces.Doesnt_end_with_ret ->
    1203           (fun r5 ->
     1191          (fun r0 ->
    12041192            let r' =
    1205               make_label_return ge depth r5.new_state r5.remainder
    1206                 (Types.pi1 (Obj.magic r5.terminates)) tIME0
     1193              make_label_return ge depth r0.new_state r0.remainder
     1194                (Types.pi1 (Obj.magic r0.terminates)) tIME0
    12071195            in
    12081196            replace_trace ge depth StructuredTraces.Ends_with_ret
    1209               r5.new_state s r5.remainder trace0
    1210               (Types.pi1 (Obj.magic r5.terminates)) tERMINATES
     1197              r0.new_state s r0.remainder trace
     1198              (Types.pi1 (Obj.magic r0.terminates)) tERMINATES
    12111199              (will_return_length ge depth
    1212                 r5.new_state.RTLabs_abstract.ras_state r5.remainder
    1213                 (Types.pi1 (Obj.magic r5.terminates)))
    1214               (will_return_length ge depth s.RTLabs_abstract.ras_state trace0
     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
    12151203                tERMINATES) r' (StructuredTraces.Tlr_step ((Obj.magic s),
    1216               (Obj.magic r5.new_state), (Obj.magic r'.new_state),
    1217               r5.new_trace, r'.new_trace)))) r.trace_res)) __
     1204              (Obj.magic r0.new_state), (Obj.magic r'.new_state),
     1205              r0.new_trace, r'.new_trace)))) r.trace_res)) __
    12181206(** val make_label_label :
    12191207    RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
    12201208    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
    12211209    StructuredTraces.trace_label_label sub_trace_result **)
    1222 and make_label_label ge depth s trace0 tERMINATES tIME =
     1210and make_label_label ge depth s trace tERMINATES tIME =
    12231211  (match tIME with
    12241212   | Nat.O -> (fun _ -> assert false (* absurd case *))
    12251213   | Nat.S tIME0 ->
    12261214     (fun _ ->
    1227        let r = make_any_label ge depth s trace0 tERMINATES tIME0 in
    1228        replace_sub_trace ge depth s s trace0 trace0 tERMINATES tERMINATES
    1229          (will_return_length ge depth s.RTLabs_abstract.ras_state trace0
     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
    12301218           tERMINATES)
    1231          (will_return_length ge depth s.RTLabs_abstract.ras_state trace0
     1219         (will_return_length ge depth s.RTLabs_abstract.ras_state trace
    12321220           tERMINATES) r (StructuredTraces.Tll_base (r.ends, (Obj.magic s),
    12331221         (Obj.magic r.trace_res.new_state), r.trace_res.new_trace)))) __
     
    12361224    (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
    12371225    StructuredTraces.trace_any_label sub_trace_result **)
    1238 and make_any_label ge depth s0 trace0 tERMINATES tIME =
     1226and make_any_label ge depth s0 trace tERMINATES tIME =
    12391227  (match tIME with
    12401228   | Nat.O -> (fun _ -> assert false (* absurd case *))
     
    12441232          stk } = s0
    12451233        in
    1246        (fun trace1 _ tM _ ->
     1234       (fun trace0 _ tM _ ->
    12471235       (match Lazy.force
    1248         trace1 with
     1236        trace0 with
    12491237        | Ft_stop st ->
    12501238          (fun _ _ tERMINATES0 _ -> assert false (* absurd case *))
    1251         | Ft_step (start, tr, next0, trace') ->
     1239        | Ft_step (start, tr, next, trace') ->
    12521240          (fun _ _ tERMINATES0 _ ->
    12531241            let start' = { RTLabs_abstract.ras_state = start;
    12541242              RTLabs_abstract.ras_fn_stack = stk }
    12551243            in
    1256             let next' = RTLabs_abstract.next_state ge start' next0 tr in
     1244            let next' = RTLabs_abstract.next_state ge start' next tr in
    12571245            (match RTLabs_abstract.rTLabs_classify start with
    12581246             | StructuredTraces.Cl_return ->
     
    12611249                 (StructuredTraces.Tal_base_return ((Obj.magic start'),
    12621250                 (Obj.magic next'))); terminates =
    1263                  (will_return_return ge depth start tr next0 trace'
     1251                 (will_return_return ge depth start tr next trace'
    12641252                   tERMINATES0) } })
    12651253             | StructuredTraces.Cl_jump ->
     
    12691257                 ((Obj.magic start'), (Obj.magic next'))); terminates =
    12701258                 (Obj.magic
    1271                    (will_return_notfn ge depth start tr next0 trace'
     1259                   (will_return_notfn ge depth start tr next trace'
    12721260                     (Types.Inr __) tERMINATES0)) } })
    12731261             | StructuredTraces.Cl_call ->
     
    12761264                   make_label_return ge (Nat.S depth) next' trace'
    12771265                     (Types.pi1
    1278                        (will_return_call ge depth start tr next0 trace'
     1266                       (will_return_call ge depth start tr next trace'
    12791267                         tERMINATES0)) tIME0
    12801268                 in
     
    12961284                      in
    12971285                      replace_sub_trace ge depth r.new_state start'
    1298                         r.remainder (lazy (Ft_step (start, tr, next0,
     1286                        r.remainder (lazy (Ft_step (start, tr, next,
    12991287                        trace'))) (Types.pi1 (Obj.magic r.terminates))
    13001288                        tERMINATES0
     
    13031291                          (Types.pi1 (Obj.magic r.terminates)))
    13041292                        (will_return_length ge depth start (lazy (Ft_step
    1305                           (start, tr, next0, trace'))) tERMINATES0) r'
     1293                          (start, tr, next, trace'))) tERMINATES0) r'
    13061294                        (StructuredTraces.Tal_step_call (r'.ends,
    13071295                        (Obj.magic start'), (Obj.magic next'),
     
    13131301             | StructuredTraces.Cl_other ->
    13141302               (fun _ ->
    1315                  (match RTLabs_abstract.rTLabs_cost next0 with
     1303                 (match RTLabs_abstract.rTLabs_cost next with
    13161304                  | Bool.True ->
    13171305                    (fun _ -> { ends = StructuredTraces.Doesnt_end_with_ret;
     
    13201308                      ((Obj.magic start'), (Obj.magic next'))); terminates =
    13211309                      (Obj.magic
    1322                         (will_return_notfn ge depth start tr next0 trace'
     1310                        (will_return_notfn ge depth start tr next trace'
    13231311                          (Types.Inl __) tERMINATES0)) } })
    13241312                  | Bool.False ->
     
    13271315                        make_any_label ge depth next' trace'
    13281316                          (Types.pi1
    1329                             (will_return_notfn ge depth start tr next0 trace'
     1317                            (will_return_notfn ge depth start tr next trace'
    13301318                              (Types.Inl __) tERMINATES0)) tIME0
    13311319                      in
    13321320                      replace_sub_trace ge depth next' start' trace'
    1333                         (lazy (Ft_step (start, tr, next0, trace')))
     1321                        (lazy (Ft_step (start, tr, next, trace')))
    13341322                        (Types.pi1
    1335                           (will_return_notfn ge depth start tr next0 trace'
     1323                          (will_return_notfn ge depth start tr next trace'
    13361324                            (Types.Inl __) tERMINATES0)) tERMINATES0
    13371325                        (will_return_length ge depth
    13381326                          next'.RTLabs_abstract.ras_state trace'
    13391327                          (Types.pi1
    1340                             (will_return_notfn ge depth start tr next0 trace'
     1328                            (will_return_notfn ge depth start tr next trace'
    13411329                              (Types.Inl __) tERMINATES0)))
    13421330                        (will_return_length ge depth start (lazy (Ft_step
    1343                           (start, tr, next0, trace'))) tERMINATES0) r
     1331                          (start, tr, next, trace'))) tERMINATES0) r
    13441332                        (StructuredTraces.Tal_step_default (r.ends,
    13451333                        (Obj.magic start'), (Obj.magic next'),
    13461334                        (Obj.magic r.trace_res.new_state),
    13471335                        r.trace_res.new_trace)))) __)) __)) __ __ tM __))
    1348          trace0 __ tERMINATES __)) __
     1336         trace __ tERMINATES __)) __
    13491337
    13501338(** val make_label_return' :
     
    13521340    (IO.io_out, IO.io_in) flat_trace -> will_return ->
    13531341    StructuredTraces.trace_label_return trace_result **)
    1354 let rec make_label_return' ge depth s trace0 tERMINATES =
    1355   make_label_return ge depth s trace0 tERMINATES
     1342let rec make_label_return' ge depth s trace tERMINATES =
     1343  make_label_return ge depth s trace tERMINATES
    13561344    (Nat.plus (Nat.S (Nat.S Nat.O))
    13571345      (Nat.times (Nat.S (Nat.S (Nat.S Nat.O)))
    1358         (will_return_length ge depth s.RTLabs_abstract.ras_state trace0
     1346        (will_return_length ge depth s.RTLabs_abstract.ras_state trace
    13591347          tERMINATES)))
    13601348
    13611349(** val actual_successor :
    1362     RTLabs_semantics.state0 -> Graphs.label Types.option **)
     1350    RTLabs_semantics.state -> Graphs.label Types.option **)
    13631351let actual_successor = function
    13641352| RTLabs_semantics.State (f, fs, m) -> Types.Some f.RTLabs_semantics.next
     
    14811469
    14821470(** val init_state_is :
    1483     RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state0 ->
     1471    RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state ->
    14841472    (Pointers.block, __) Types.dPair **)
    14851473let init_state_is p s =
     
    14941482            ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX
    14951483            (PreIdentifiers.SymbolTag, main)), List.Nil))))
    1496             (Globalenvs.find_symbol (RTLabs_semantics.make_global0 p) main)))
     1484            (Globalenvs.find_symbol (RTLabs_semantics.make_global p) main)))
    14971485        (fun b ->
    14981486        Monad.m_bind0 (Monad.max_def Errors.res0)
     
    15011489              ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
    15021490              (PreIdentifiers.SymbolTag, main)), List.Nil))))
    1503               (Globalenvs.find_funct_ptr (RTLabs_semantics.make_global0 p) b)))
     1491              (Globalenvs.find_funct_ptr (RTLabs_semantics.make_global p) b)))
    15041492          (fun f ->
    15051493          Obj.magic (Errors.OK (RTLabs_semantics.Callstate (main, f,
     
    15091497        ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX
    15101498        (PreIdentifiers.SymbolTag, p.AST.prog_main)), List.Nil))))
    1511         (Globalenvs.find_symbol (RTLabs_semantics.make_global0 p)
     1499        (Globalenvs.find_symbol (RTLabs_semantics.make_global p)
    15121500          p.AST.prog_main)) (fun x ->
    15131501      Obj.magic
     
    15171505              ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
    15181506              (PreIdentifiers.SymbolTag, p.AST.prog_main)), List.Nil))))
    1519               (Globalenvs.find_funct_ptr (RTLabs_semantics.make_global0 p) x)))
     1507              (Globalenvs.find_funct_ptr (RTLabs_semantics.make_global p) x)))
    15201508          (fun f ->
    15211509          Obj.magic (Errors.OK (RTLabs_semantics.Callstate (p.AST.prog_main,
     
    15251513          ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
    15261514          (PreIdentifiers.SymbolTag, p.AST.prog_main)), List.Nil))))
    1527           (Globalenvs.find_funct_ptr (RTLabs_semantics.make_global0 p) b))
     1515          (Globalenvs.find_funct_ptr (RTLabs_semantics.make_global p) b))
    15281516        (fun x -> Errors.OK (RTLabs_semantics.Callstate (p.AST.prog_main, x,
    15291517        List.Nil, Types.None, List.Nil, m))) s (fun f _ _ ->
     
    15381526
    15391527(** val ras_state_initial :
    1540     RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state0 ->
     1528    RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state ->
    15411529    RTLabs_abstract.rTLabs_ext_state **)
    15421530let ras_state_initial p s =
     
    15451533
    15461534(** val deprop_execute :
    1547     RTLabs_semantics.genv -> RTLabs_semantics.state0 ->
    1548     RTLabs_semantics.state0 -> Events.trace Types.sig0 **)
     1535    RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
     1536    -> Events.trace Types.sig0 **)
    15491537let rec deprop_execute ge s s' =
    15501538  (match RTLabs_semantics.eval_statement ge s with
     
    15601548
    15611549type ('o, 'i) partial_flat_trace =
    1562 | Pft_base of RTLabs_semantics.state0 * Events.trace
    1563    * RTLabs_semantics.state0
    1564 | Pft_step of RTLabs_semantics.state0 * Events.trace
    1565    * RTLabs_semantics.state0 * RTLabs_semantics.state0
    1566    * ('o, 'i) partial_flat_trace
     1550| Pft_base of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
     1551| Pft_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
     1552   * RTLabs_semantics.state * ('o, 'i) partial_flat_trace
    15671553
    15681554(** val partial_flat_trace_rect_Type4 :
    1569     RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
    1570     RTLabs_semantics.state0 -> __ -> 'a3) -> (RTLabs_semantics.state0 ->
    1571     Events.trace -> RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __
    1572     -> ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) ->
    1573     RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> ('a1, 'a2)
    1574     partial_flat_trace -> 'a3 **)
    1575 let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_18422 x_18421 = function
     1555    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
     1556    RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
     1557    Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
     1558    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
     1559    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
     1560let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_13732 x_13731 = function
    15761561| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1577 | Pft_step (s, tr, s', s'', x_18425) ->
    1578   h_pft_step s tr s' s'' __ x_18425
    1579     (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_18425)
     1562| Pft_step (s, tr, s', s'', x_13735) ->
     1563  h_pft_step s tr s' s'' __ x_13735
     1564    (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_13735)
    15801565
    15811566(** val partial_flat_trace_rect_Type3 :
    1582     RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
    1583     RTLabs_semantics.state0 -> __ -> 'a3) -> (RTLabs_semantics.state0 ->
    1584     Events.trace -> RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __
    1585     -> ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) ->
    1586     RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> ('a1, 'a2)
    1587     partial_flat_trace -> 'a3 **)
    1588 let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_18438 x_18437 = function
     1567    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
     1568    RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
     1569    Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
     1570    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
     1571    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
     1572let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_13748 x_13747 = function
    15891573| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1590 | Pft_step (s, tr, s', s'', x_18441) ->
    1591   h_pft_step s tr s' s'' __ x_18441
    1592     (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_18441)
     1574| Pft_step (s, tr, s', s'', x_13751) ->
     1575  h_pft_step s tr s' s'' __ x_13751
     1576    (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_13751)
    15931577
    15941578(** val partial_flat_trace_rect_Type2 :
    1595     RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
    1596     RTLabs_semantics.state0 -> __ -> 'a3) -> (RTLabs_semantics.state0 ->
    1597     Events.trace -> RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __
    1598     -> ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) ->
    1599     RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> ('a1, 'a2)
    1600     partial_flat_trace -> 'a3 **)
    1601 let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_18446 x_18445 = function
     1579    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
     1580    RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
     1581    Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
     1582    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
     1583    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
     1584let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_13756 x_13755 = function
    16021585| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1603 | Pft_step (s, tr, s', s'', x_18449) ->
    1604   h_pft_step s tr s' s'' __ x_18449
    1605     (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_18449)
     1586| Pft_step (s, tr, s', s'', x_13759) ->
     1587  h_pft_step s tr s' s'' __ x_13759
     1588    (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_13759)
    16061589
    16071590(** val partial_flat_trace_rect_Type1 :
    1608     RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
    1609     RTLabs_semantics.state0 -> __ -> 'a3) -> (RTLabs_semantics.state0 ->
    1610     Events.trace -> RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __
    1611     -> ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) ->
    1612     RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> ('a1, 'a2)
    1613     partial_flat_trace -> 'a3 **)
    1614 let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_18454 x_18453 = function
     1591    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
     1592    RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
     1593    Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
     1594    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
     1595    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
     1596let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_13764 x_13763 = function
    16151597| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1616 | Pft_step (s, tr, s', s'', x_18457) ->
    1617   h_pft_step s tr s' s'' __ x_18457
    1618     (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_18457)
     1598| Pft_step (s, tr, s', s'', x_13767) ->
     1599  h_pft_step s tr s' s'' __ x_13767
     1600    (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_13767)
    16191601
    16201602(** val partial_flat_trace_rect_Type0 :
    1621     RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
    1622     RTLabs_semantics.state0 -> __ -> 'a3) -> (RTLabs_semantics.state0 ->
    1623     Events.trace -> RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __
    1624     -> ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) ->
    1625     RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> ('a1, 'a2)
    1626     partial_flat_trace -> 'a3 **)
    1627 let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_18462 x_18461 = function
     1603    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
     1604    RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
     1605    Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
     1606    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
     1607    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
     1608let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_13772 x_13771 = function
    16281609| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1629 | Pft_step (s, tr, s', s'', x_18465) ->
    1630   h_pft_step s tr s' s'' __ x_18465
    1631     (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_18465)
     1610| Pft_step (s, tr, s', s'', x_13775) ->
     1611  h_pft_step s tr s' s'' __ x_13775
     1612    (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_13775)
    16321613
    16331614(** val partial_flat_trace_inv_rect_Type4 :
    1634     RTLabs_semantics.genv -> RTLabs_semantics.state0 ->
    1635     RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace ->
    1636     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
    1637     -> __ -> __ -> __ -> 'a3) -> (RTLabs_semantics.state0 -> Events.trace ->
    1638     RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __ -> ('a1, 'a2)
    1639     partial_flat_trace -> (__ -> __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3)
    1640     -> 'a3 **)
     1615    RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
     1616    -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state ->
     1617    Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
     1618    (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
     1619    RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ ->
     1620    __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **)
    16411621let partial_flat_trace_inv_rect_Type4 x3 x4 x5 hterm h1 h2 =
    16421622  let hcut = partial_flat_trace_rect_Type4 x3 h1 h2 x4 x5 hterm in
     
    16441624
    16451625(** val partial_flat_trace_inv_rect_Type3 :
    1646     RTLabs_semantics.genv -> RTLabs_semantics.state0 ->
    1647     RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace ->
    1648     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
    1649     -> __ -> __ -> __ -> 'a3) -> (RTLabs_semantics.state0 -> Events.trace ->
    1650     RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __ -> ('a1, 'a2)
    1651     partial_flat_trace -> (__ -> __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3)
    1652     -> 'a3 **)
     1626    RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
     1627    -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state ->
     1628    Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
     1629    (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
     1630    RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ ->
     1631    __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **)
    16531632let partial_flat_trace_inv_rect_Type3 x3 x4 x5 hterm h1 h2 =
    16541633  let hcut = partial_flat_trace_rect_Type3 x3 h1 h2 x4 x5 hterm in
     
    16561635
    16571636(** val partial_flat_trace_inv_rect_Type2 :
    1658     RTLabs_semantics.genv -> RTLabs_semantics.state0 ->
    1659     RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace ->
    1660     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
    1661     -> __ -> __ -> __ -> 'a3) -> (RTLabs_semantics.state0 -> Events.trace ->
    1662     RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __ -> ('a1, 'a2)
    1663     partial_flat_trace -> (__ -> __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3)
    1664     -> 'a3 **)
     1637    RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
     1638    -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state ->
     1639    Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
     1640    (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
     1641    RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ ->
     1642    __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **)
    16651643let partial_flat_trace_inv_rect_Type2 x3 x4 x5 hterm h1 h2 =
    16661644  let hcut = partial_flat_trace_rect_Type2 x3 h1 h2 x4 x5 hterm in
     
    16681646
    16691647(** val partial_flat_trace_inv_rect_Type1 :
    1670     RTLabs_semantics.genv -> RTLabs_semantics.state0 ->
    1671     RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace ->
    1672     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
    1673     -> __ -> __ -> __ -> 'a3) -> (RTLabs_semantics.state0 -> Events.trace ->
    1674     RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __ -> ('a1, 'a2)
    1675     partial_flat_trace -> (__ -> __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3)
    1676     -> 'a3 **)
     1648    RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
     1649    -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state ->
     1650    Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
     1651    (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
     1652    RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ ->
     1653    __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **)
    16771654let partial_flat_trace_inv_rect_Type1 x3 x4 x5 hterm h1 h2 =
    16781655  let hcut = partial_flat_trace_rect_Type1 x3 h1 h2 x4 x5 hterm in
     
    16801657
    16811658(** val partial_flat_trace_inv_rect_Type0 :
    1682     RTLabs_semantics.genv -> RTLabs_semantics.state0 ->
    1683     RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace ->
    1684     (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
    1685     -> __ -> __ -> __ -> 'a3) -> (RTLabs_semantics.state0 -> Events.trace ->
    1686     RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __ -> ('a1, 'a2)
    1687     partial_flat_trace -> (__ -> __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3)
    1688     -> 'a3 **)
     1659    RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
     1660    -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state ->
     1661    Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
     1662    (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
     1663    RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ ->
     1664    __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **)
    16891665let partial_flat_trace_inv_rect_Type0 x3 x4 x5 hterm h1 h2 =
    16901666  let hcut = partial_flat_trace_rect_Type0 x3 h1 h2 x4 x5 hterm in
     
    16921668
    16931669(** val partial_flat_trace_jmdiscr :
    1694     RTLabs_semantics.genv -> RTLabs_semantics.state0 ->
    1695     RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2)
    1696     partial_flat_trace -> __ **)
     1670    RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
     1671    -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2) partial_flat_trace -> __ **)
    16971672let partial_flat_trace_jmdiscr a3 a4 a5 x y =
    16981673  Logic.eq_rect_Type2 x
     
    17031678
    17041679(** val append_partial_flat_trace :
    1705     RTLabs_semantics.genv -> RTLabs_semantics.state0 ->
    1706     RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> ('a1, 'a2)
    1707     partial_flat_trace -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2)
    1708     partial_flat_trace **)
     1680    RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
     1681    -> RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2)
     1682    partial_flat_trace -> ('a1, 'a2) partial_flat_trace **)
    17091683let rec append_partial_flat_trace ge s1 s2 s3 = function
    17101684| Pft_base (s, tr, s') -> (fun x -> Pft_step (s, tr, s', s3, x))
     
    17141688
    17151689(** val partial_to_flat_trace :
    1716     RTLabs_semantics.genv -> RTLabs_semantics.state0 ->
    1717     RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2)
    1718     flat_trace -> ('a1, 'a2) flat_trace **)
     1690    RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
     1691    -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2) flat_trace -> ('a1, 'a2)
     1692    flat_trace **)
    17191693let rec partial_to_flat_trace ge s1 s2 = function
    17201694| Pft_base (s, tr0, s') -> (fun x -> lazy (Ft_step (s, tr0, s', x)))
     
    17441718    partial_flat_trace **)
    17451719and flat_trace_of_label_label ge ends0 s s' = function
    1746 | StructuredTraces.Tll_base (e1, s1, s2, tal) ->
    1747   flat_trace_of_any_label ge e1 (Obj.magic s1) (Obj.magic s2) tal
     1720| StructuredTraces.Tll_base (e, s1, s2, tal) ->
     1721  flat_trace_of_any_label ge e (Obj.magic s1) (Obj.magic s2) tal
    17481722(** val flat_trace_of_any_label :
    17491723    RTLabs_semantics.genv -> StructuredTraces.trace_ends_with_ret ->
     
    18701844           RTLabs_abstract.ras_fn_stack = stk } tr' tld0))))) __)) __ tld
    18711845(** val add_partial_flat_trace :
    1872     RTLabs_semantics.genv -> RTLabs_semantics.state0 ->
     1846    RTLabs_semantics.genv -> RTLabs_semantics.state ->
    18731847    RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in)
    18741848    partial_flat_trace -> StructuredTraces.trace_label_diverges ->
Note: See TracChangeset for help on using the changeset viewer.