open Preamble open Deqsets_extra open CostSpec open Sets open Listb open StructuredTraces open BitVectorTrie open Graphs open Order open Registers open FrontEndOps open RTLabs_syntax open SmallstepExec open CostLabel open Events open IOMonad open IO open Extra_bool open Coqlib open Values open FrontEndVal open Hide open ByteValues open Division open Z open BitVectorZ open Pointers open GenMem open FrontEndMem open Proper open PositiveMap open Deqsets open Extralib open Lists open Identifiers open Exp open Arithmetic open Vector open Div_and_mod open Util open FoldStuff open BitVector open Extranat open Integers open AST open Globalenvs open ErrorMessages open Option open Setoids open Monad open Jmeq open Russell open Positive open PreIdentifiers open Errors open Bool open Relations open Nat open Hints_declaration open Core_notation open Pts open Logic open Types open List open RTLabs_semantics open RTLabs_abstract open CostMisc open Executions open Listb_extra type ('o, 'i) flat_trace = ('o, 'i) __flat_trace Lazy.t and ('o, 'i) __flat_trace = | Ft_stop of RTLabs_semantics.state | Ft_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state * ('o, 'i) flat_trace (** val flat_trace_inv_rect_Type4 : RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace -> (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **) let flat_trace_inv_rect_Type4 x3 x4 hterm h1 h2 = let hcut = match Lazy.force hterm with | Ft_stop x -> h1 x __ | Ft_step (x, x0, x1, x2) -> h2 x x0 x1 __ x2 in hcut __ __ (** val flat_trace_inv_rect_Type3 : RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace -> (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **) let flat_trace_inv_rect_Type3 x3 x4 hterm h1 h2 = let hcut = match Lazy.force hterm with | Ft_stop x -> h1 x __ | Ft_step (x, x0, x1, x2) -> h2 x x0 x1 __ x2 in hcut __ __ (** val flat_trace_inv_rect_Type2 : RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace -> (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **) let flat_trace_inv_rect_Type2 x3 x4 hterm h1 h2 = let hcut = match Lazy.force hterm with | Ft_stop x -> h1 x __ | Ft_step (x, x0, x1, x2) -> h2 x x0 x1 __ x2 in hcut __ __ (** val flat_trace_inv_rect_Type1 : RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace -> (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **) let flat_trace_inv_rect_Type1 x3 x4 hterm h1 h2 = let hcut = match Lazy.force hterm with | Ft_stop x -> h1 x __ | Ft_step (x, x0, x1, x2) -> h2 x x0 x1 __ x2 in hcut __ __ (** val flat_trace_inv_rect_Type0 : RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace -> (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **) let flat_trace_inv_rect_Type0 x3 x4 hterm h1 h2 = let hcut = match Lazy.force hterm with | Ft_stop x -> h1 x __ | Ft_step (x, x0, x1, x2) -> h2 x x0 x1 __ x2 in hcut __ __ (** val flat_trace_discr : RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace -> ('a1, 'a2) flat_trace -> __ **) let flat_trace_discr a3 a4 x y = Logic.eq_rect_Type2 x (match Lazy.force x with | Ft_stop a0 -> Obj.magic (fun _ dH -> dH __ __) | Ft_step (a0, a10, a20, a40) -> Obj.magic (fun _ dH -> dH __ __ __ __ __)) y (** val flat_trace_jmdiscr : RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace -> ('a1, 'a2) flat_trace -> __ **) let flat_trace_jmdiscr a3 a4 x y = Logic.eq_rect_Type2 x (match Lazy.force x with | Ft_stop a0 -> Obj.magic (fun _ dH -> dH __ __) | Ft_step (a0, a10, a20, a40) -> Obj.magic (fun _ dH -> dH __ __ __ __ __)) y (** val make_flat_trace : __ -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace **) let rec make_flat_trace ge s = let e = SmallstepExec.exec_inf_aux RTLabs_semantics.rTLabs_fullexec.SmallstepExec.es1 ge (Obj.magic (RTLabs_semantics.eval_statement (Obj.magic ge) s)) in (match Lazy.force e with | SmallstepExec.E_stop (tr, i, s') -> (fun _ -> lazy (Ft_step (s, tr, (Obj.magic s'), (lazy (Ft_stop (Obj.magic s')))))) | SmallstepExec.E_step (tr, s', e') -> (fun _ -> lazy (Ft_step (s, tr, (Obj.magic s'), (make_flat_trace ge (Obj.magic s'))))) | SmallstepExec.E_wrong m -> (fun _ -> assert false (* absurd case *)) | SmallstepExec.E_interact (o, f) -> (fun _ -> assert false (* absurd case *))) __ (** val make_whole_flat_trace : __ -> __ -> (IO.io_out, IO.io_in) flat_trace **) let make_whole_flat_trace p s = let ge = RTLabs_semantics.rTLabs_fullexec.SmallstepExec.make_global p in let e = SmallstepExec.exec_inf_aux RTLabs_semantics.rTLabs_fullexec.SmallstepExec.es1 ge (IOMonad.Value { Types.fst = Events.e0; Types.snd = s }) in (match Lazy.force e with | SmallstepExec.E_stop (tr, i, s') -> (fun _ -> lazy (Ft_stop (Obj.magic s))) | SmallstepExec.E_step (x, x0, e') -> (fun _ -> make_flat_trace ge (Obj.magic s)) | SmallstepExec.E_wrong m -> (fun _ -> assert false (* absurd case *)) | SmallstepExec.E_interact (o, f) -> (fun _ -> assert false (* absurd case *))) __ type will_return = | Wr_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return | Wr_call of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return | Wr_ret of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return | Wr_base of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state * (IO.io_out, IO.io_in) flat_trace (** val will_return_rect_Type4 : RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> 'a1 **) let rec will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1409 s x_1408 = function | Wr_step (s0, tr, s', depth, trace, x_1411) -> h_wr_step s0 tr s' depth __ trace __ x_1411 (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth s' trace x_1411) | Wr_call (s0, tr, s', depth, trace, x_1413) -> h_wr_call s0 tr s' depth __ trace __ x_1413 (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S depth) s' trace x_1413) | Wr_ret (s0, tr, s', depth, trace, x_1415) -> h_wr_ret s0 tr s' depth __ trace __ x_1415 (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth s' trace x_1415) | Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __ (** val will_return_rect_Type3 : RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> 'a1 **) let rec will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1437 s x_1436 = function | Wr_step (s0, tr, s', depth, trace, x_1439) -> h_wr_step s0 tr s' depth __ trace __ x_1439 (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth s' trace x_1439) | Wr_call (s0, tr, s', depth, trace, x_1441) -> h_wr_call s0 tr s' depth __ trace __ x_1441 (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S depth) s' trace x_1441) | Wr_ret (s0, tr, s', depth, trace, x_1443) -> h_wr_ret s0 tr s' depth __ trace __ x_1443 (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth s' trace x_1443) | Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __ (** val will_return_rect_Type2 : RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> 'a1 **) let rec will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1451 s x_1450 = function | Wr_step (s0, tr, s', depth, trace, x_1453) -> h_wr_step s0 tr s' depth __ trace __ x_1453 (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth s' trace x_1453) | Wr_call (s0, tr, s', depth, trace, x_1455) -> h_wr_call s0 tr s' depth __ trace __ x_1455 (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S depth) s' trace x_1455) | Wr_ret (s0, tr, s', depth, trace, x_1457) -> h_wr_ret s0 tr s' depth __ trace __ x_1457 (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth s' trace x_1457) | Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __ (** val will_return_rect_Type1 : RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> 'a1 **) let rec will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1465 s x_1464 = function | Wr_step (s0, tr, s', depth, trace, x_1467) -> h_wr_step s0 tr s' depth __ trace __ x_1467 (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth s' trace x_1467) | Wr_call (s0, tr, s', depth, trace, x_1469) -> h_wr_call s0 tr s' depth __ trace __ x_1469 (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S depth) s' trace x_1469) | Wr_ret (s0, tr, s', depth, trace, x_1471) -> h_wr_ret s0 tr s' depth __ trace __ x_1471 (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth s' trace x_1471) | Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __ (** val will_return_rect_Type0 : RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> 'a1 **) let rec will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1479 s x_1478 = function | Wr_step (s0, tr, s', depth, trace, x_1481) -> h_wr_step s0 tr s' depth __ trace __ x_1481 (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth s' trace x_1481) | Wr_call (s0, tr, s', depth, trace, x_1483) -> h_wr_call s0 tr s' depth __ trace __ x_1483 (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S depth) s' trace x_1483) | Wr_ret (s0, tr, s', depth, trace, x_1485) -> h_wr_ret s0 tr s' depth __ trace __ x_1485 (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth s' trace x_1485) | Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __ (** val will_return_inv_rect_Type4 : RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let will_return_inv_rect_Type4 x1 x2 x3 x4 hterm h1 h2 h3 h4 = let hcut = will_return_rect_Type4 x1 h1 h2 h3 h4 x2 x3 x4 hterm in hcut __ __ __ __ (** val will_return_inv_rect_Type3 : RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let will_return_inv_rect_Type3 x1 x2 x3 x4 hterm h1 h2 h3 h4 = let hcut = will_return_rect_Type3 x1 h1 h2 h3 h4 x2 x3 x4 hterm in hcut __ __ __ __ (** val will_return_inv_rect_Type2 : RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let will_return_inv_rect_Type2 x1 x2 x3 x4 hterm h1 h2 h3 h4 = let hcut = will_return_rect_Type2 x1 h1 h2 h3 h4 x2 x3 x4 hterm in hcut __ __ __ __ (** val will_return_inv_rect_Type1 : RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let will_return_inv_rect_Type1 x1 x2 x3 x4 hterm h1 h2 h3 h4 = let hcut = will_return_rect_Type1 x1 h1 h2 h3 h4 x2 x3 x4 hterm in hcut __ __ __ __ (** val will_return_inv_rect_Type0 : RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let will_return_inv_rect_Type0 x1 x2 x3 x4 hterm h1 h2 h3 h4 = let hcut = will_return_rect_Type0 x1 h1 h2 h3 h4 x2 x3 x4 hterm in hcut __ __ __ __ (** val will_return_jmdiscr : RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> will_return -> __ **) let will_return_jmdiscr a1 a2 a3 a4 x y = Logic.eq_rect_Type2 x (match x with | Wr_step (a0, a10, a20, a30, a5, a7) -> Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __) | Wr_call (a0, a10, a20, a30, a5, a7) -> Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __) | Wr_ret (a0, a10, a20, a30, a5, a7) -> Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __) | Wr_base (a0, a10, a20, a40) -> Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y (** val will_return_length : RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat **) let rec will_return_length ge d s tr = function | Wr_step (x, x0, x1, x2, x4, t') -> Nat.S (will_return_length ge x2 x1 x4 t') | Wr_call (x, x0, x1, x2, x4, t') -> Nat.S (will_return_length ge (Nat.S x2) x1 x4 t') | Wr_ret (x, x0, x1, x2, x4, t') -> Nat.S (will_return_length ge x2 x1 x4 t') | Wr_base (x, x0, x1, x3) -> Nat.S Nat.O (** val will_return_end : RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state, (IO.io_out, IO.io_in) flat_trace) Types.dPair **) let rec will_return_end ge d s tr = function | Wr_step (x, x0, x1, x2, x4, t') -> will_return_end ge x2 x1 x4 t' | Wr_call (x, x0, x1, x2, x4, t') -> will_return_end ge (Nat.S x2) x1 x4 t' | Wr_ret (x, x0, x1, x2, x4, t') -> will_return_end ge x2 x1 x4 t' | Wr_base (x, x0, x1, tr') -> { Types.dpi1 = x1; Types.dpi2 = tr' } (** val will_return_call : RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> will_return Types.sig0 **) let will_return_call ge d s tr s' trace tERM = will_return_inv_rect_Type0 ge d s (lazy (Ft_step (s, tr, s', trace))) tERM (fun h19 h20 h21 h22 _ h24 _ h26 h27 _ _ _ _ -> assert false (* absurd case *)) (fun h33 h34 h35 h36 _ h38 _ h40 h41 _ _ _ _ -> Logic.eq_rect_Type0_r h36 (fun tERM0 h410 _ -> Logic.eq_rect_Type0_r h33 (fun _ _ _ tERM1 h411 _ -> Obj.magic flat_trace_jmdiscr ge h33 (lazy (Ft_step (h33, tr, s', trace))) (lazy (Ft_step (h33, h34, h35, h38))) __ (fun _ -> Logic.streicherK h33 (fun _ -> Logic.eq_rect_Type0_r h34 (fun _ _ tERM2 h412 _ _ -> Logic.eq_rect_Type0_r h35 (fun trace0 _ _ tERM3 h413 _ _ -> Logic.eq_rect_Type0_r __ (fun _ tERM4 h414 _ _ -> Logic.eq_rect_Type0_r h38 (fun _ tERM5 h415 _ -> Logic.streicherK (lazy (Ft_step (h33, h34, h35, h38))) (Logic.eq_rect_Type0_r (Wr_call (h33, h34, h35, h36, h38, h40)) (fun h416 -> h40) tERM5 h415)) trace0 __ tERM4 h414 __) __ __ tERM3 h413 __) s' trace __ __ tERM2 h412 __) tr __ __ tERM1 h411 __))) s __ __ __ tERM0 h410 __) d tERM h41 __) (fun h47 h48 h49 h50 _ h52 _ h54 h55 _ _ _ _ -> assert false (* absurd case *)) (fun h61 h62 h63 _ h65 _ _ _ _ _ -> assert false (* absurd case *)) (** val will_return_return : RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> __ **) let will_return_return ge d s tr s' trace tERM = will_return_inv_rect_Type0 ge d s (lazy (Ft_step (s, tr, s', trace))) tERM (fun h19 h20 h21 h22 _ h24 _ h26 h27 _ _ _ _ -> assert false (* absurd case *)) (fun h33 h34 h35 h36 _ h38 _ h40 h41 _ _ _ _ -> assert false (* absurd case *)) (fun h47 h48 h49 h50 _ h52 _ h54 h55 _ _ _ _ -> Logic.eq_rect_Type0_r (Nat.S h50) (fun tERM0 h550 _ -> Logic.eq_rect_Type0_r h47 (fun _ _ _ tERM1 h551 _ -> Obj.magic flat_trace_jmdiscr ge h47 (lazy (Ft_step (h47, tr, s', trace))) (lazy (Ft_step (h47, h48, h49, h52))) __ (fun _ -> Logic.streicherK h47 (fun _ -> Logic.eq_rect_Type0_r h48 (fun _ _ tERM2 h552 _ _ -> Logic.eq_rect_Type0_r h49 (fun trace0 _ _ tERM3 h553 _ _ -> Logic.eq_rect_Type0_r __ (fun _ tERM4 h554 _ _ -> Logic.eq_rect_Type0_r h52 (fun _ tERM5 h555 _ -> Logic.streicherK (lazy (Ft_step (h47, h48, h49, h52))) (Logic.eq_rect_Type0_r (Wr_ret (h47, h48, h49, h50, h52, h54)) (fun h556 -> h54) tERM5 h555)) trace0 __ tERM4 h554 __) __ __ tERM3 h553 __) s' trace __ __ tERM2 h552 __) tr __ __ tERM1 h551 __))) s __ __ __ tERM0 h550 __) d tERM h55 __) (Obj.magic __) (** val will_return_notfn : RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> (__, __) Types.sum -> will_return -> will_return Types.sig0 **) let will_return_notfn ge d s tr s' trace = function | Types.Inl _ -> (fun tERM -> will_return_inv_rect_Type0 ge d s (lazy (Ft_step (s, tr, s', trace))) tERM (fun h290 h291 h292 h293 _ h295 _ h297 h298 _ _ _ _ -> Logic.eq_rect_Type0_r h293 (fun tERM0 h2980 _ -> Logic.eq_rect_Type0_r h290 (fun _ _ _ tERM1 h2981 _ -> Obj.magic flat_trace_jmdiscr ge h290 (lazy (Ft_step (h290, tr, s', trace))) (lazy (Ft_step (h290, h291, h292, h295))) __ (fun _ -> Logic.streicherK h290 (fun _ -> Logic.eq_rect_Type0_r h291 (fun _ _ tERM2 h2982 _ _ -> Logic.eq_rect_Type0_r h292 (fun trace0 _ _ tERM3 h2983 _ _ -> Logic.eq_rect_Type0_r __ (fun _ tERM4 h2984 _ _ -> Logic.eq_rect_Type0_r h295 (fun _ tERM5 h2985 _ -> Logic.streicherK (lazy (Ft_step (h290, h291, h292, h295))) (Logic.eq_rect_Type0_r (Wr_step (h290, h291, h292, h293, h295, h297)) (fun h2986 -> h297) tERM5 h2985)) trace0 __ tERM4 h2984 __) __ __ tERM3 h2983 __) s' trace __ __ tERM2 h2982 __) tr __ __ tERM1 h2981 __))) s __ __ __ tERM0 h2980 __) d tERM h298 __) (fun h304 h305 h306 h307 _ h309 _ h311 h312 _ _ _ _ -> assert false (* absurd case *)) (fun h318 h319 h320 h321 _ h323 _ h325 h326 _ _ _ _ -> assert false (* absurd case *)) (fun h332 h333 h334 _ h336 _ _ _ _ _ -> assert false (* absurd case *))) | Types.Inr _ -> (fun tERM -> will_return_inv_rect_Type0 ge d s (lazy (Ft_step (s, tr, s', trace))) tERM (fun h343 h344 h345 h346 _ h348 _ h350 h351 _ _ _ _ -> Logic.eq_rect_Type0_r h346 (fun tERM0 h3510 _ -> Logic.eq_rect_Type0_r h343 (fun _ _ _ tERM1 h3511 _ -> Obj.magic flat_trace_jmdiscr ge h343 (lazy (Ft_step (h343, tr, s', trace))) (lazy (Ft_step (h343, h344, h345, h348))) __ (fun _ -> Logic.streicherK h343 (fun _ -> Logic.eq_rect_Type0_r h344 (fun _ _ tERM2 h3512 _ _ -> Logic.eq_rect_Type0_r h345 (fun trace0 _ _ tERM3 h3513 _ _ -> Logic.eq_rect_Type0_r __ (fun _ tERM4 h3514 _ _ -> Logic.eq_rect_Type0_r h348 (fun _ tERM5 h3515 _ -> Logic.streicherK (lazy (Ft_step (h343, h344, h345, h348))) (Logic.eq_rect_Type0_r (Wr_step (h343, h344, h345, h346, h348, h350)) (fun h3516 -> h350) tERM5 h3515)) trace0 __ tERM4 h3514 __) __ __ tERM3 h3513 __) s' trace __ __ tERM2 h3512 __) tr __ __ tERM1 h3511 __))) s __ __ __ tERM0 h3510 __) d tERM h351 __) (fun h357 h358 h359 h360 _ h362 _ h364 h365 _ _ _ _ -> assert false (* absurd case *)) (fun h371 h372 h373 h374 _ h376 _ h378 h379 _ _ _ _ -> assert false (* absurd case *)) (fun h385 h386 h387 _ h389 _ _ _ _ _ -> assert false (* absurd case *))) (** val will_return_prepend : RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> will_return **) let will_return_prepend ge d1 s1 tr1 t1 d2 s2 t2 x = will_return_rect_Type0 ge (fun s tr s' depth _ t _ t0 iH d3 s3 t3 t4 _ -> Wr_step (s, tr, s', (Nat.plus depth (Nat.S d3)), t, (iH d3 s3 t3 t4 __))) (fun s tr s' depth _ t _ t0 iH d3 s3 t3 t4 _ -> Wr_call (s, tr, s', (Nat.plus depth (Nat.S d3)), t, (iH d3 s3 t3 t4 __))) (fun s tr s' depth _ t _ t0 iH s3 s20 t3 t4 _ -> Wr_ret (s, tr, s', (Nat.plus depth (Nat.S s3)), t, (iH s3 s20 t3 t4 __))) (fun s tr s' _ t _ d3 s3 t3 t4 _ -> Obj.magic Types.dPair_discr { Types.dpi1 = s'; Types.dpi2 = t } { Types.dpi1 = s3; Types.dpi2 = t3 } __ (fun _ -> Logic.eq_rect_Type0_r s3 (fun _ t0 _ _ -> Logic.eq_rect_Type0_r t3 (fun _ -> Logic.streicherK { Types.dpi1 = s3; Types.dpi2 = t3 } (Wr_ret (s, tr, s3, d3, t3, t4))) t0 __) s' __ t __)) d1 s1 tr1 t1 d2 s2 t2 x __ (** val nat_jmdiscr : Nat.nat -> Nat.nat -> __ **) let nat_jmdiscr x y = Logic.eq_rect_Type2 x (match x with | Nat.O -> Obj.magic (fun _ dH -> dH) | Nat.S a0 -> Obj.magic (fun _ dH -> dH __)) y (** val will_return_remove_call : RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> will_return -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return **) let will_return_remove_call ge d1x s1x t1x t1 d2 x s2 t2 = will_return_rect_Type0 ge (fun s tr s' d1 _ t _ t0 iH d3 t3 s3 t4 _ -> iH d3 (will_return_inv_rect_Type0 ge (Nat.plus d1 (Nat.S d3)) s (lazy (Ft_step (s, tr, s', t))) t3 (fun h1 h2 h3 h4 _ h6 _ h8 h9 _ _ _ _ -> Logic.eq_rect_Type0 (Nat.plus d1 (Nat.S d3)) (fun h80 h90 _ -> Logic.eq_rect_Type0_r h1 (fun _ _ t20 _ _ h91 _ -> Obj.magic flat_trace_jmdiscr ge h1 (lazy (Ft_step (h1, tr, s', t))) (lazy (Ft_step (h1, h2, h3, h6))) __ (fun _ -> Logic.streicherK h1 (fun _ -> Logic.eq_rect_Type0_r h2 (fun _ t21 _ _ h92 _ _ -> Logic.eq_rect_Type0_r h3 (fun t5 t6 iH0 _ t22 _ _ h93 _ _ -> Logic.eq_rect_Type0_r __ (fun t23 _ _ h94 _ _ -> Logic.eq_rect_Type0_r h6 (fun t7 iH1 t24 _ _ h95 _ -> Logic.streicherK (lazy (Ft_step (h1, h2, h3, h6))) (Logic.eq_rect_Type0_r (Wr_step (h1, h2, h3, (Nat.plus d1 (Nat.S d3)), h6, h80)) (fun h96 -> h80) t24 h95)) t5 t6 iH0 t23 __ __ h94 __) __ t22 __ __ h93 __) s' t t0 iH __ t21 __ __ h92 __) tr __ t20 __ __ h91 __))) s __ __ t3 __ __ h90 __) h4 h8 h9 __) (fun h15 h16 h17 h18 _ h20 _ h22 h23 _ _ _ _ -> assert false (* absurd case *)) (fun h29 h30 h31 h32 _ h34 _ h36 h37 _ _ _ _ -> assert false (* absurd case *)) (fun h43 h44 h45 _ h47 _ _ _ _ _ -> assert false (* absurd case *))) s3 t4 __) (fun s tr s' d1 _ t _ t0 iH d3 t3 s3 t4 _ -> iH d3 (will_return_inv_rect_Type0 ge (Nat.plus d1 (Nat.S d3)) s (lazy (Ft_step (s, tr, s', t))) t3 (fun h1 h2 h3 h4 _ h6 _ h8 h9 _ _ _ _ -> assert false (* absurd case *)) (fun h15 h16 h17 h18 _ h20 _ h22 h23 _ _ _ _ -> Logic.eq_rect_Type0 (Nat.plus d1 (Nat.S d3)) (fun h220 h230 _ -> Logic.eq_rect_Type0_r h15 (fun _ _ t20 _ _ h231 _ -> Obj.magic flat_trace_jmdiscr ge h15 (lazy (Ft_step (h15, tr, s', t))) (lazy (Ft_step (h15, h16, h17, h20))) __ (fun _ -> Logic.streicherK h15 (fun _ -> Logic.eq_rect_Type0_r h16 (fun _ t21 _ _ h232 _ _ -> Logic.eq_rect_Type0_r h17 (fun t5 t6 iH0 _ t22 _ _ h233 _ _ -> Logic.eq_rect_Type0_r __ (fun t23 _ _ h234 _ _ -> Logic.eq_rect_Type0_r h20 (fun t7 iH1 t24 _ _ h235 _ -> Logic.streicherK (lazy (Ft_step (h15, h16, h17, h20))) (Logic.eq_rect_Type0_r (Wr_call (h15, h16, h17, (Nat.plus d1 (Nat.S d3)), h20, h220)) (fun h236 -> h220) t24 h235)) t5 t6 iH0 t23 __ __ h234 __) __ t22 __ __ h233 __) s' t t0 iH __ t21 __ __ h232 __) tr __ t20 __ __ h231 __))) s __ __ t3 __ __ h230 __) h18 h22 h23 __) (fun h29 h30 h31 h32 _ h34 _ h36 h37 _ _ _ _ -> assert false (* absurd case *)) (fun h43 h44 h45 _ h47 _ _ _ _ _ -> assert false (* absurd case *))) s3 t4 __) (fun s tr s' d1 _ t _ t0 iH d3 t3 s3 t4 _ -> iH d3 (will_return_inv_rect_Type0 ge (Nat.plus (Nat.S d1) (Nat.S d3)) s (lazy (Ft_step (s, tr, s', t))) t3 (fun h1 h2 h3 h4 _ h6 _ h8 h9 _ _ _ _ -> assert false (* absurd case *)) (fun h15 h16 h17 h18 _ h20 _ h22 h23 _ _ _ _ -> assert false (* absurd case *)) (fun h29 h30 h31 h32 _ h34 _ h36 h37 _ _ _ _ -> Obj.magic nat_jmdiscr (Nat.S (Nat.plus d1 (Nat.S d3))) (Nat.S h32) __ (Logic.eq_rect_Type0_r h29 (fun _ _ t20 _ h370 _ _ -> Obj.magic flat_trace_jmdiscr ge h29 (lazy (Ft_step (h29, tr, s', t))) (lazy (Ft_step (h29, h30, h31, h34))) __ (fun _ -> Logic.streicherK h29 (fun _ -> Logic.eq_rect_Type0_r h30 (fun _ t21 _ h371 _ _ _ -> Logic.eq_rect_Type0_r h31 (fun t5 t6 iH0 _ t22 _ h372 _ _ _ -> Logic.eq_rect_Type0_r __ (fun t23 _ h373 _ _ _ -> Logic.eq_rect_Type0_r h34 (fun t7 iH1 t24 _ h374 _ _ -> Logic.streicherK (lazy (Ft_step (h29, h30, h31, h34))) (fun _ -> Logic.eq_rect_Type0 (Nat.plus d1 (Nat.S d3)) (fun h360 _ h375 _ -> Logic.streicherK (Nat.S (Nat.plus d1 (Nat.S d3))) (Logic.eq_rect_Type0_r (Wr_ret (h29, h30, h31, (Nat.plus d1 (Nat.S d3)), h34, h360)) (fun h376 -> h360) t24 h375)) h32 h36 __ h374 __)) t5 t6 iH0 t23 __ h373 __ __) __ t22 __ h372 __ __) s' t t0 iH __ t21 __ h371 __ __) tr __ t20 __ h370 __ __))) s __ __ t3 __ h37 __ __)) (fun h43 h44 h45 _ h47 _ _ _ _ _ -> assert false (* absurd case *))) s3 t4 __) (fun s tr s' _ t _ d3 t3 s3 t4 _ -> Obj.magic Types.dPair_discr { Types.dpi1 = s'; Types.dpi2 = t } { Types.dpi1 = s3; Types.dpi2 = t4 } __ (fun _ -> Logic.eq_rect_Type0_r s3 (fun _ t0 t20 _ _ -> Logic.eq_rect_Type0_r t4 (fun t21 _ -> Logic.streicherK { Types.dpi1 = s3; Types.dpi2 = t4 } (will_return_inv_rect_Type0 ge (Nat.plus Nat.O (Nat.S d3)) s (lazy (Ft_step (s, tr, s3, t4))) t21 (fun h1 h2 h3 h4 _ h6 _ h8 h9 _ _ _ _ -> assert false (* absurd case *)) (fun h15 h16 h17 h18 _ h20 _ h22 h23 _ _ _ _ -> assert false (* absurd case *)) (fun h29 h30 h31 h32 _ h34 _ h36 h37 _ _ _ _ -> Obj.magic nat_jmdiscr (Nat.S d3) (Nat.S h32) __ (Logic.eq_rect_Type0_r h29 (fun _ _ t22 h370 _ _ -> Obj.magic flat_trace_jmdiscr ge h29 (lazy (Ft_step (h29, tr, s3, t4))) (lazy (Ft_step (h29, h30, h31, h34))) __ (fun _ -> Logic.streicherK h29 (fun _ -> Logic.eq_rect_Type0_r h30 (fun _ t23 h371 _ _ _ -> Logic.eq_rect_Type0_r h31 (fun t24 _ t25 h372 _ _ _ -> Logic.eq_rect_Type0_r __ (fun t26 h373 _ _ _ -> Logic.eq_rect_Type0_r h34 (fun t27 h374 _ _ -> Logic.streicherK (lazy (Ft_step (h29, h30, h31, h34))) (fun _ -> Logic.eq_rect_Type0_r h32 (fun _ t28 h375 _ -> Logic.streicherK (Nat.S h32) (Logic.eq_rect_Type0_r (Wr_ret (h29, h30, h31, h32, h34, h36)) (fun h376 -> h36) t28 h375)) d3 __ t27 h374 __)) t24 t26 h373 __ __) __ t25 h372 __ __) s3 t4 __ t23 h371 __ __) tr __ t22 h370 __ __))) s __ __ t21 h37 __ __)) (fun h43 h44 h45 _ h47 _ _ _ _ _ -> assert false (* absurd case *)))) t0 t20 __) s' __ t t3 __)) d1x s1x t1x t1 d2 x s2 t2 __ (** val will_return_lower : RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> will_return **) let will_return_lower ge d0 s0 t0 tM d' = will_return_rect_Type0 ge (fun s tr s' d _ tr0 _ tM1 iH d'0 _ -> Wr_step (s, tr, s', d'0, tr0, (iH d'0 __))) (fun s tr s' d _ tr0 _ tM1 iH d'0 _ -> Wr_call (s, tr, s', d'0, tr0, (iH (Nat.S d'0) __))) (fun s tr s' d _ tr0 _ tM1 iH clearme -> match clearme with | Nat.O -> (fun _ -> Wr_base (s, tr, s', tr0)) | Nat.S d'0 -> (fun _ -> Wr_ret (s, tr, s', d'0, tr0, (iH d'0 __)))) (fun s tr s' _ tr0 _ clearme -> match clearme with | Nat.O -> (fun _ -> Wr_base (s, tr, s', tr0)) | Nat.S d'0 -> (fun _ -> assert false (* absurd case *))) d0 s0 t0 tM d' __ (** val list_jmdiscr : 'a1 List.list -> 'a1 List.list -> __ **) let list_jmdiscr x y = Logic.eq_rect_Type2 x (match x with | List.Nil -> Obj.magic (fun _ dH -> dH) | List.Cons (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y type 't trace_result = { new_state : RTLabs_abstract.rTLabs_ext_state; remainder : (IO.io_out, IO.io_in) flat_trace; new_trace : 't; terminates : __ } (** val trace_result_rect_Type4 : RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result -> 'a2 **) let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_2020 = let { new_state = new_state0; remainder = remainder0; new_trace = new_trace0; terminates = terminates0 } = x_2020 in h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0 (** val trace_result_rect_Type5 : RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result -> 'a2 **) let rec trace_result_rect_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_2022 = let { new_state = new_state0; remainder = remainder0; new_trace = new_trace0; terminates = terminates0 } = x_2022 in h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0 (** val trace_result_rect_Type3 : RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result -> 'a2 **) let rec trace_result_rect_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_2024 = let { new_state = new_state0; remainder = remainder0; new_trace = new_trace0; terminates = terminates0 } = x_2024 in h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0 (** val trace_result_rect_Type2 : RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result -> 'a2 **) let rec trace_result_rect_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_2026 = let { new_state = new_state0; remainder = remainder0; new_trace = new_trace0; terminates = terminates0 } = x_2026 in h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0 (** val trace_result_rect_Type1 : RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result -> 'a2 **) let rec trace_result_rect_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_2028 = let { new_state = new_state0; remainder = remainder0; new_trace = new_trace0; terminates = terminates0 } = x_2028 in h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0 (** val trace_result_rect_Type0 : RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result -> 'a2 **) let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_2030 = let { new_state = new_state0; remainder = remainder0; new_trace = new_trace0; terminates = terminates0 } = x_2030 in h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0 (** val new_state : RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1 trace_result -> RTLabs_abstract.rTLabs_ext_state **) let rec new_state ge depth ends start full original_terminates limit xxx = xxx.new_state (** val remainder : RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1 trace_result -> (IO.io_out, IO.io_in) flat_trace **) let rec remainder ge depth ends start full original_terminates limit xxx = xxx.remainder (** val new_trace : RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1 trace_result -> 'a1 **) let rec new_trace ge depth ends start full original_terminates limit xxx = xxx.new_trace (** val terminates : RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1 trace_result -> __ **) let rec terminates ge depth ends start full original_terminates limit xxx = xxx.terminates (** val trace_result_inv_rect_Type4 : RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1 trace_result -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2 **) let trace_result_inv_rect_Type4 x1 x2 x3 x4 x5 x6 x8 hterm h1 = let hcut = trace_result_rect_Type4 x1 x2 x3 x4 x5 x6 x8 h1 hterm in hcut __ (** val trace_result_inv_rect_Type3 : RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1 trace_result -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2 **) let trace_result_inv_rect_Type3 x1 x2 x3 x4 x5 x6 x8 hterm h1 = let hcut = trace_result_rect_Type3 x1 x2 x3 x4 x5 x6 x8 h1 hterm in hcut __ (** val trace_result_inv_rect_Type2 : RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1 trace_result -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2 **) let trace_result_inv_rect_Type2 x1 x2 x3 x4 x5 x6 x8 hterm h1 = let hcut = trace_result_rect_Type2 x1 x2 x3 x4 x5 x6 x8 h1 hterm in hcut __ (** val trace_result_inv_rect_Type1 : RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1 trace_result -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2 **) let trace_result_inv_rect_Type1 x1 x2 x3 x4 x5 x6 x8 hterm h1 = let hcut = trace_result_rect_Type1 x1 x2 x3 x4 x5 x6 x8 h1 hterm in hcut __ (** val trace_result_inv_rect_Type0 : RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1 trace_result -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2 **) let trace_result_inv_rect_Type0 x1 x2 x3 x4 x5 x6 x8 hterm h1 = let hcut = trace_result_rect_Type0 x1 x2 x3 x4 x5 x6 x8 h1 hterm in hcut __ (** val trace_result_jmdiscr : RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1 trace_result -> 'a1 trace_result -> __ **) let trace_result_jmdiscr a1 a2 a3 a4 a5 a6 a8 x y = Logic.eq_rect_Type2 x (let { new_state = a0; remainder = a10; new_trace = a30; terminates = a50 } = x in Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y type 't sub_trace_result = { ends : StructuredTraces.trace_ends_with_ret; trace_res : 't trace_result } (** val sub_trace_result_rect_Type4 : RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1 sub_trace_result -> 'a2 **) let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_2048 = let { ends = ends0; trace_res = trace_res0 } = x_2048 in h_mk_sub_trace_result ends0 trace_res0 (** val sub_trace_result_rect_Type5 : RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1 sub_trace_result -> 'a2 **) let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_2050 = let { ends = ends0; trace_res = trace_res0 } = x_2050 in h_mk_sub_trace_result ends0 trace_res0 (** val sub_trace_result_rect_Type3 : RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1 sub_trace_result -> 'a2 **) let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_2052 = let { ends = ends0; trace_res = trace_res0 } = x_2052 in h_mk_sub_trace_result ends0 trace_res0 (** val sub_trace_result_rect_Type2 : RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1 sub_trace_result -> 'a2 **) let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_2054 = let { ends = ends0; trace_res = trace_res0 } = x_2054 in h_mk_sub_trace_result ends0 trace_res0 (** val sub_trace_result_rect_Type1 : RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1 sub_trace_result -> 'a2 **) let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_2056 = let { ends = ends0; trace_res = trace_res0 } = x_2056 in h_mk_sub_trace_result ends0 trace_res0 (** val sub_trace_result_rect_Type0 : RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1 sub_trace_result -> 'a2 **) let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_2058 = let { ends = ends0; trace_res = trace_res0 } = x_2058 in h_mk_sub_trace_result ends0 trace_res0 (** val ends : RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1 sub_trace_result -> StructuredTraces.trace_ends_with_ret **) let rec ends ge depth start full original_terminates limit xxx = xxx.ends (** val trace_res : RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1 sub_trace_result -> 'a1 trace_result **) let rec trace_res ge depth start full original_terminates limit xxx = xxx.trace_res (** val sub_trace_result_inv_rect_Type4 : RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1 sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> __ -> 'a2) -> 'a2 **) let sub_trace_result_inv_rect_Type4 x1 x2 x3 x4 x5 x7 hterm h1 = let hcut = sub_trace_result_rect_Type4 x1 x2 x3 x4 x5 x7 h1 hterm in hcut __ (** val sub_trace_result_inv_rect_Type3 : RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1 sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> __ -> 'a2) -> 'a2 **) let sub_trace_result_inv_rect_Type3 x1 x2 x3 x4 x5 x7 hterm h1 = let hcut = sub_trace_result_rect_Type3 x1 x2 x3 x4 x5 x7 h1 hterm in hcut __ (** val sub_trace_result_inv_rect_Type2 : RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1 sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> __ -> 'a2) -> 'a2 **) let sub_trace_result_inv_rect_Type2 x1 x2 x3 x4 x5 x7 hterm h1 = let hcut = sub_trace_result_rect_Type2 x1 x2 x3 x4 x5 x7 h1 hterm in hcut __ (** val sub_trace_result_inv_rect_Type1 : RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1 sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> __ -> 'a2) -> 'a2 **) let sub_trace_result_inv_rect_Type1 x1 x2 x3 x4 x5 x7 hterm h1 = let hcut = sub_trace_result_rect_Type1 x1 x2 x3 x4 x5 x7 h1 hterm in hcut __ (** val sub_trace_result_inv_rect_Type0 : RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1 sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> __ -> 'a2) -> 'a2 **) let sub_trace_result_inv_rect_Type0 x1 x2 x3 x4 x5 x7 hterm h1 = let hcut = sub_trace_result_rect_Type0 x1 x2 x3 x4 x5 x7 h1 hterm in hcut __ (** val sub_trace_result_discr : RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1 sub_trace_result -> 'a1 sub_trace_result -> __ **) let sub_trace_result_discr a1 a2 a3 a4 a5 a7 x y = Logic.eq_rect_Type2 x (let { ends = a0; trace_res = a10 } = x in Obj.magic (fun _ dH -> dH __ __)) y (** val sub_trace_result_jmdiscr : RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1 sub_trace_result -> 'a1 sub_trace_result -> __ **) let sub_trace_result_jmdiscr a1 a2 a3 a4 a5 a7 x y = Logic.eq_rect_Type2 x (let { ends = a0; trace_res = a10 } = x in Obj.magic (fun _ dH -> dH __ __)) y (** val replace_trace : RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret -> RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> (IO.io_out, IO.io_in) flat_trace -> will_return -> will_return -> Nat.nat -> Nat.nat -> 'a1 trace_result -> 'a2 -> 'a2 trace_result **) let replace_trace ge d e s1 s2 t1 t2 tM1 tM2 l1 l2 r trace = { new_state = r.new_state; remainder = r.remainder; new_trace = trace; terminates = ((match e with | StructuredTraces.Ends_with_ret -> Logic.eq_rect_Type0 (will_return_end ge d s1.RTLabs_abstract.ras_state t1 tM1) (fun clearme -> let { new_state = x; remainder = x0; new_trace = x1; terminates = x2 } = clearme in (match d with | Nat.O -> Obj.magic __ | Nat.S d' -> (fun tM10 tM20 ns rem _ t1NS _ clearme0 -> let tMa = Obj.magic clearme0 in Obj.magic tMa)) tM1 tM2 x x0 __ x1 __ x2) (will_return_end ge d s2.RTLabs_abstract.ras_state t2 tM2) | StructuredTraces.Doesnt_end_with_ret -> Logic.eq_rect_Type0 (will_return_end ge d s1.RTLabs_abstract.ras_state t1 tM1) (fun clearme -> let { new_state = ns; remainder = rem; new_trace = t1NS; terminates = clearme0 } = clearme in let tMa = Obj.magic clearme0 in Obj.magic tMa) (will_return_end ge d s2.RTLabs_abstract.ras_state t2 tM2)) r) } (** val replace_sub_trace : RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> (IO.io_out, IO.io_in) flat_trace -> will_return -> will_return -> Nat.nat -> Nat.nat -> 'a1 sub_trace_result -> 'a2 -> 'a2 sub_trace_result **) let replace_sub_trace ge d s1 s2 t1 t2 tM1 tM2 l1 l2 r trace = { ends = r.ends; trace_res = (replace_trace ge d r.ends s1 s2 t1 t2 tM1 tM2 l1 l2 r.trace_res trace) } (** val make_label_return : RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> StructuredTraces.trace_label_return trace_result **) let rec make_label_return ge depth s trace tERMINATES tIME = (match tIME with | Nat.O -> (fun _ -> assert false (* absurd case *)) | Nat.S tIME0 -> (fun _ -> let r = make_label_label ge depth s trace tERMINATES tIME0 in (match r.ends with | StructuredTraces.Ends_with_ret -> (fun r0 -> replace_trace ge depth StructuredTraces.Ends_with_ret s s trace trace tERMINATES tERMINATES (will_return_length ge depth s.RTLabs_abstract.ras_state trace tERMINATES) (will_return_length ge depth s.RTLabs_abstract.ras_state trace tERMINATES) r0 (StructuredTraces.Tlr_base ((Obj.magic s), (Obj.magic r0.new_state), r0.new_trace))) | StructuredTraces.Doesnt_end_with_ret -> (fun r0 -> let r' = make_label_return ge depth r0.new_state r0.remainder (Types.pi1 (Obj.magic r0.terminates)) tIME0 in replace_trace ge depth StructuredTraces.Ends_with_ret r0.new_state s r0.remainder trace (Types.pi1 (Obj.magic r0.terminates)) tERMINATES (will_return_length ge depth r0.new_state.RTLabs_abstract.ras_state r0.remainder (Types.pi1 (Obj.magic r0.terminates))) (will_return_length ge depth s.RTLabs_abstract.ras_state trace tERMINATES) r' (StructuredTraces.Tlr_step ((Obj.magic s), (Obj.magic r0.new_state), (Obj.magic r'.new_state), r0.new_trace, r'.new_trace)))) r.trace_res)) __ (** val make_label_label : RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> StructuredTraces.trace_label_label sub_trace_result **) and make_label_label ge depth s trace tERMINATES tIME = (match tIME with | Nat.O -> (fun _ -> assert false (* absurd case *)) | Nat.S tIME0 -> (fun _ -> let r = make_any_label ge depth s trace tERMINATES tIME0 in replace_sub_trace ge depth s s trace trace tERMINATES tERMINATES (will_return_length ge depth s.RTLabs_abstract.ras_state trace tERMINATES) (will_return_length ge depth s.RTLabs_abstract.ras_state trace tERMINATES) r (StructuredTraces.Tll_base (r.ends, (Obj.magic s), (Obj.magic r.trace_res.new_state), r.trace_res.new_trace)))) __ (** val make_any_label : RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> StructuredTraces.trace_any_label sub_trace_result **) and make_any_label ge depth s0 trace tERMINATES tIME = (match tIME with | Nat.O -> (fun _ -> assert false (* absurd case *)) | Nat.S tIME0 -> (fun _ -> (let { RTLabs_abstract.ras_state = s; RTLabs_abstract.ras_fn_stack = stk } = s0 in (fun trace0 _ tM _ -> (match Lazy.force trace0 with | Ft_stop st -> (fun _ _ tERMINATES0 _ -> assert false (* absurd case *)) | Ft_step (start, tr, next, trace') -> (fun _ _ tERMINATES0 _ -> let start' = { RTLabs_abstract.ras_state = start; RTLabs_abstract.ras_fn_stack = stk } in let next' = RTLabs_abstract.next_state ge start' next tr in (match RTLabs_abstract.rTLabs_classify start with | StructuredTraces.Cl_return -> (fun _ -> { ends = StructuredTraces.Ends_with_ret; trace_res = { new_state = next'; remainder = trace'; new_trace = (StructuredTraces.Tal_base_return ((Obj.magic start'), (Obj.magic next'))); terminates = (will_return_return ge depth start tr next trace' tERMINATES0) } }) | StructuredTraces.Cl_jump -> (fun _ -> { ends = StructuredTraces.Doesnt_end_with_ret; trace_res = { new_state = next'; remainder = trace'; new_trace = (StructuredTraces.Tal_base_not_return ((Obj.magic start'), (Obj.magic next'))); terminates = (Obj.magic (will_return_notfn ge depth start tr next trace' (Types.Inr __) tERMINATES0)) } }) | StructuredTraces.Cl_call -> (fun _ -> let r = make_label_return ge (Nat.S depth) next' trace' (Types.pi1 (will_return_call ge depth start tr next trace' tERMINATES0)) tIME0 in (match RTLabs_abstract.rTLabs_cost r.new_state.RTLabs_abstract.ras_state with | Bool.True -> (fun _ -> { ends = StructuredTraces.Doesnt_end_with_ret; trace_res = { new_state = r.new_state; remainder = r.remainder; new_trace = (StructuredTraces.Tal_base_call ((Obj.magic start'), (Obj.magic next'), (Obj.magic r.new_state), r.new_trace)); terminates = (let tMr = Obj.magic r.terminates in Obj.magic tMr) } }) | Bool.False -> (fun _ -> let r' = make_any_label ge depth r.new_state r.remainder (Types.pi1 (Obj.magic r.terminates)) tIME0 in replace_sub_trace ge depth r.new_state start' r.remainder (lazy (Ft_step (start, tr, next, trace'))) (Types.pi1 (Obj.magic r.terminates)) tERMINATES0 (will_return_length ge depth r.new_state.RTLabs_abstract.ras_state r.remainder (Types.pi1 (Obj.magic r.terminates))) (will_return_length ge depth start (lazy (Ft_step (start, tr, next, trace'))) tERMINATES0) r' (StructuredTraces.Tal_step_call (r'.ends, (Obj.magic start'), (Obj.magic next'), (Obj.magic r.new_state), (Obj.magic r'.trace_res.new_state), r.new_trace, r'.trace_res.new_trace)))) __) | StructuredTraces.Cl_tailcall -> (fun _ -> assert false (* absurd case *)) | StructuredTraces.Cl_other -> (fun _ -> (match RTLabs_abstract.rTLabs_cost next with | Bool.True -> (fun _ -> { ends = StructuredTraces.Doesnt_end_with_ret; trace_res = { new_state = next'; remainder = trace'; new_trace = (StructuredTraces.Tal_base_not_return ((Obj.magic start'), (Obj.magic next'))); terminates = (Obj.magic (will_return_notfn ge depth start tr next trace' (Types.Inl __) tERMINATES0)) } }) | Bool.False -> (fun _ -> let r = make_any_label ge depth next' trace' (Types.pi1 (will_return_notfn ge depth start tr next trace' (Types.Inl __) tERMINATES0)) tIME0 in replace_sub_trace ge depth next' start' trace' (lazy (Ft_step (start, tr, next, trace'))) (Types.pi1 (will_return_notfn ge depth start tr next trace' (Types.Inl __) tERMINATES0)) tERMINATES0 (will_return_length ge depth next'.RTLabs_abstract.ras_state trace' (Types.pi1 (will_return_notfn ge depth start tr next trace' (Types.Inl __) tERMINATES0))) (will_return_length ge depth start (lazy (Ft_step (start, tr, next, trace'))) tERMINATES0) r (StructuredTraces.Tal_step_default (r.ends, (Obj.magic start'), (Obj.magic next'), (Obj.magic r.trace_res.new_state), r.trace_res.new_trace)))) __)) __)) __ __ tM __)) trace __ tERMINATES __)) __ (** val make_label_return' : RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> will_return -> StructuredTraces.trace_label_return trace_result **) let rec make_label_return' ge depth s trace tERMINATES = make_label_return ge depth s trace tERMINATES (Nat.plus (Nat.S (Nat.S Nat.O)) (Nat.times (Nat.S (Nat.S (Nat.S Nat.O))) (will_return_length ge depth s.RTLabs_abstract.ras_state trace tERMINATES))) (** val actual_successor : RTLabs_semantics.state -> Graphs.label Types.option **) let actual_successor = function | RTLabs_semantics.State (f, fs, m) -> Types.Some f.RTLabs_semantics.next | RTLabs_semantics.Callstate (x, x0, x1, x2, fs, x3) -> (match fs with | List.Nil -> Types.None | List.Cons (f, x4) -> Types.Some f.RTLabs_semantics.next) | RTLabs_semantics.Returnstate (x, x0, x1, x2) -> Types.None | RTLabs_semantics.Finalstate x -> Types.None (** val steps_for_statement : RTLabs_syntax.statement -> Nat.nat **) let steps_for_statement s = Nat.S (match s with | RTLabs_syntax.St_skip x -> Nat.O | RTLabs_syntax.St_cost (x, x0) -> Nat.O | RTLabs_syntax.St_const (x, x0, x1, x2) -> Nat.O | RTLabs_syntax.St_op1 (x, x0, x1, x2, x3, x4) -> Nat.O | RTLabs_syntax.St_op2 (x, x0, x1, x2, x3, x4, x5, x6) -> Nat.O | RTLabs_syntax.St_load (x, x0, x1, x2) -> Nat.O | RTLabs_syntax.St_store (x, x0, x1, x2) -> Nat.O | RTLabs_syntax.St_call_id (x, x0, x1, x2) -> Nat.S Nat.O | RTLabs_syntax.St_call_ptr (x, x0, x1, x2) -> Nat.S Nat.O | RTLabs_syntax.St_cond (x, x0, x1) -> Nat.O | RTLabs_syntax.St_return -> Nat.S Nat.O) type remainder_ok = | Mk_remainder_ok (** val remainder_ok_rect_Type4 : RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok -> 'a1 **) let rec remainder_ok_rect_Type4 ge s t h_mk_remainder_ok = function | Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __ (** val remainder_ok_rect_Type5 : RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok -> 'a1 **) let rec remainder_ok_rect_Type5 ge s t h_mk_remainder_ok = function | Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __ (** val remainder_ok_rect_Type3 : RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok -> 'a1 **) let rec remainder_ok_rect_Type3 ge s t h_mk_remainder_ok = function | Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __ (** val remainder_ok_rect_Type2 : RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok -> 'a1 **) let rec remainder_ok_rect_Type2 ge s t h_mk_remainder_ok = function | Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __ (** val remainder_ok_rect_Type1 : RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok -> 'a1 **) let rec remainder_ok_rect_Type1 ge s t h_mk_remainder_ok = function | Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __ (** val remainder_ok_rect_Type0 : RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok -> 'a1 **) let rec remainder_ok_rect_Type0 ge s t h_mk_remainder_ok = function | Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __ (** val remainder_ok_inv_rect_Type4 : RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let remainder_ok_inv_rect_Type4 x1 x2 x3 hterm h1 = let hcut = remainder_ok_rect_Type4 x1 x2 x3 h1 hterm in hcut __ (** val remainder_ok_inv_rect_Type3 : RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let remainder_ok_inv_rect_Type3 x1 x2 x3 hterm h1 = let hcut = remainder_ok_rect_Type3 x1 x2 x3 h1 hterm in hcut __ (** val remainder_ok_inv_rect_Type2 : RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let remainder_ok_inv_rect_Type2 x1 x2 x3 hterm h1 = let hcut = remainder_ok_rect_Type2 x1 x2 x3 h1 hterm in hcut __ (** val remainder_ok_inv_rect_Type1 : RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let remainder_ok_inv_rect_Type1 x1 x2 x3 hterm h1 = let hcut = remainder_ok_rect_Type1 x1 x2 x3 h1 hterm in hcut __ (** val remainder_ok_inv_rect_Type0 : RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let remainder_ok_inv_rect_Type0 x1 x2 x3 hterm h1 = let hcut = remainder_ok_rect_Type0 x1 x2 x3 h1 hterm in hcut __ (** val remainder_ok_discr : RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> remainder_ok -> remainder_ok -> __ **) let remainder_ok_discr a1 a2 a3 x y = Logic.eq_rect_Type2 x (let Mk_remainder_ok = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y (** val remainder_ok_jmdiscr : RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> remainder_ok -> remainder_ok -> __ **) let remainder_ok_jmdiscr a1 a2 a3 x y = Logic.eq_rect_Type2 x (let Mk_remainder_ok = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y (** val init_state_is : RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state -> (Pointers.block, __) Types.dPair **) let init_state_is p s = RTLabs_semantics.bind_ok (Globalenvs.init_mem (fun x -> x) p) (fun x -> let main = p.AST.prog_main in Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, main)), List.Nil)))) (Globalenvs.find_symbol (RTLabs_semantics.make_global p) main))) (fun b -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, main)), List.Nil)))) (Globalenvs.find_funct_ptr (RTLabs_semantics.make_global p) b))) (fun f -> Obj.magic (Errors.OK (RTLabs_semantics.Callstate (main, f, List.Nil, Types.None, List.Nil, x))))))) s (fun m _ _ -> RTLabs_semantics.bind_ok (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, p.AST.prog_main)), List.Nil)))) (Globalenvs.find_symbol (RTLabs_semantics.make_global p) p.AST.prog_main)) (fun x -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, p.AST.prog_main)), List.Nil)))) (Globalenvs.find_funct_ptr (RTLabs_semantics.make_global p) x))) (fun f -> Obj.magic (Errors.OK (RTLabs_semantics.Callstate (p.AST.prog_main, f, List.Nil, Types.None, List.Nil, m)))))) s (fun b _ _ -> RTLabs_semantics.bind_ok (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, p.AST.prog_main)), List.Nil)))) (Globalenvs.find_funct_ptr (RTLabs_semantics.make_global p) b)) (fun x -> Errors.OK (RTLabs_semantics.Callstate (p.AST.prog_main, x, List.Nil, Types.None, List.Nil, m))) s (fun f _ _ -> Obj.magic Errors.res_discr (Errors.OK (RTLabs_semantics.Callstate (p.AST.prog_main, f, List.Nil, Types.None, List.Nil, m))) (Errors.OK s) __ (fun _ -> Logic.eq_rect_Type0 (RTLabs_semantics.Callstate (p.AST.prog_main, f, List.Nil, Types.None, List.Nil, m)) (fun _ -> Logic.streicherK (Errors.OK (RTLabs_semantics.Callstate (p.AST.prog_main, f, List.Nil, Types.None, List.Nil, m))) { Types.dpi1 = b; Types.dpi2 = __ }) s __)))) (** val ras_state_initial : RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state -> RTLabs_abstract.rTLabs_ext_state **) let ras_state_initial p s = { RTLabs_abstract.ras_state = s; RTLabs_abstract.ras_fn_stack = (List.Cons ((init_state_is p s).Types.dpi1, List.Nil)) } (** val deprop_execute : RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state -> Events.trace Types.sig0 **) let rec deprop_execute ge s s' = (match RTLabs_semantics.eval_statement ge s with | IOMonad.Interact (x, x0) -> (fun _ -> assert false (* absurd case *)) | IOMonad.Value ts -> (fun _ -> ts.Types.fst) | IOMonad.Wrong x -> (fun _ -> assert false (* absurd case *))) __ (** val deprop_as_execute : RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state -> Events.trace Types.sig0 **) let rec deprop_as_execute ge s s' = deprop_execute ge s.RTLabs_abstract.ras_state s'.RTLabs_abstract.ras_state type ('o, 'i) partial_flat_trace = | Pft_base of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state | Pft_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state * RTLabs_semantics.state * ('o, 'i) partial_flat_trace (** val partial_flat_trace_rect_Type4 : RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state -> RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **) let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_2393 x_2392 = function | Pft_base (s, tr, s') -> h_pft_base s tr s' __ | Pft_step (s, tr, s', s'', x_2396) -> h_pft_step s tr s' s'' __ x_2396 (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_2396) (** val partial_flat_trace_rect_Type3 : RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state -> RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **) let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_2409 x_2408 = function | Pft_base (s, tr, s') -> h_pft_base s tr s' __ | Pft_step (s, tr, s', s'', x_2412) -> h_pft_step s tr s' s'' __ x_2412 (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_2412) (** val partial_flat_trace_rect_Type2 : RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state -> RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **) let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_2417 x_2416 = function | Pft_base (s, tr, s') -> h_pft_base s tr s' __ | Pft_step (s, tr, s', s'', x_2420) -> h_pft_step s tr s' s'' __ x_2420 (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_2420) (** val partial_flat_trace_rect_Type1 : RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state -> RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **) let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_2425 x_2424 = function | Pft_base (s, tr, s') -> h_pft_base s tr s' __ | Pft_step (s, tr, s', s'', x_2428) -> h_pft_step s tr s' s'' __ x_2428 (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_2428) (** val partial_flat_trace_rect_Type0 : RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state -> RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **) let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_2433 x_2432 = function | Pft_base (s, tr, s') -> h_pft_base s tr s' __ | Pft_step (s, tr, s', s'', x_2436) -> h_pft_step s tr s' s'' __ x_2436 (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_2436) (** val partial_flat_trace_inv_rect_Type4 : RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **) let partial_flat_trace_inv_rect_Type4 x3 x4 x5 hterm h1 h2 = let hcut = partial_flat_trace_rect_Type4 x3 h1 h2 x4 x5 hterm in hcut __ __ __ (** val partial_flat_trace_inv_rect_Type3 : RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **) let partial_flat_trace_inv_rect_Type3 x3 x4 x5 hterm h1 h2 = let hcut = partial_flat_trace_rect_Type3 x3 h1 h2 x4 x5 hterm in hcut __ __ __ (** val partial_flat_trace_inv_rect_Type2 : RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **) let partial_flat_trace_inv_rect_Type2 x3 x4 x5 hterm h1 h2 = let hcut = partial_flat_trace_rect_Type2 x3 h1 h2 x4 x5 hterm in hcut __ __ __ (** val partial_flat_trace_inv_rect_Type1 : RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **) let partial_flat_trace_inv_rect_Type1 x3 x4 x5 hterm h1 h2 = let hcut = partial_flat_trace_rect_Type1 x3 h1 h2 x4 x5 hterm in hcut __ __ __ (** val partial_flat_trace_inv_rect_Type0 : RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) -> (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **) let partial_flat_trace_inv_rect_Type0 x3 x4 x5 hterm h1 h2 = let hcut = partial_flat_trace_rect_Type0 x3 h1 h2 x4 x5 hterm in hcut __ __ __ (** val partial_flat_trace_jmdiscr : RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2) partial_flat_trace -> __ **) let partial_flat_trace_jmdiscr a3 a4 a5 x y = Logic.eq_rect_Type2 x (match x with | Pft_base (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __ __) | Pft_step (a0, a10, a20, a30, a50) -> Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y (** val append_partial_flat_trace : RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state -> RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2) partial_flat_trace **) let rec append_partial_flat_trace ge s1 s2 s3 = function | Pft_base (s, tr, s') -> (fun x -> Pft_step (s, tr, s', s3, x)) | Pft_step (s, tr, s', s'', tr') -> (fun tr2 -> Pft_step (s, tr, s', s3, (append_partial_flat_trace ge s' s'' s3 tr' tr2))) (** val partial_to_flat_trace : RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2) flat_trace -> ('a1, 'a2) flat_trace **) let rec partial_to_flat_trace ge s1 s2 = function | Pft_base (s, tr0, s') -> (fun x -> lazy (Ft_step (s, tr0, s', x))) | Pft_step (s, tr0, s', s'', tr') -> (fun tr'' -> lazy (Ft_step (s, tr0, s', (partial_to_flat_trace ge s' s'' tr' tr'')))) (** val flat_trace_of_label_return : RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state -> StructuredTraces.trace_label_return -> (IO.io_out, IO.io_in) partial_flat_trace **) let rec flat_trace_of_label_return ge s s' = function | StructuredTraces.Tlr_base (s1, s2, tll) -> flat_trace_of_label_label ge StructuredTraces.Ends_with_ret (Obj.magic s1) (Obj.magic s2) tll | StructuredTraces.Tlr_step (s1, s2, s3, tll, tlr) -> append_partial_flat_trace ge (Obj.magic s1).RTLabs_abstract.ras_state (Obj.magic s2).RTLabs_abstract.ras_state (Obj.magic s3).RTLabs_abstract.ras_state (flat_trace_of_label_label ge StructuredTraces.Doesnt_end_with_ret (Obj.magic s1) (Obj.magic s2) tll) (flat_trace_of_label_return ge (Obj.magic s2) (Obj.magic s3) tlr) (** val flat_trace_of_label_label : RTLabs_semantics.genv -> StructuredTraces.trace_ends_with_ret -> RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state -> StructuredTraces.trace_label_label -> (IO.io_out, IO.io_in) partial_flat_trace **) and flat_trace_of_label_label ge ends0 s s' = function | StructuredTraces.Tll_base (e, s1, s2, tal) -> flat_trace_of_any_label ge e (Obj.magic s1) (Obj.magic s2) tal (** val flat_trace_of_any_label : RTLabs_semantics.genv -> StructuredTraces.trace_ends_with_ret -> RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state -> StructuredTraces.trace_any_label -> (IO.io_out, IO.io_in) partial_flat_trace **) and flat_trace_of_any_label ge ends0 s s' = function | StructuredTraces.Tal_base_not_return (s1, s2) -> let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in Pft_base ((Obj.magic s1).RTLabs_abstract.ras_state, tr0, (Obj.magic s2).RTLabs_abstract.ras_state) | StructuredTraces.Tal_base_return (s1, s2) -> let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in Pft_base ((Obj.magic s1).RTLabs_abstract.ras_state, tr0, (Obj.magic s2).RTLabs_abstract.ras_state) | StructuredTraces.Tal_base_call (s1, s2, s3, tlr) -> let suffix' = flat_trace_of_label_return ge (Obj.magic s2) (Obj.magic s3) tlr in let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0, (Obj.magic s2).RTLabs_abstract.ras_state, (Obj.magic s3).RTLabs_abstract.ras_state, suffix') | StructuredTraces.Tal_base_tailcall (s1, s2, s3, tlr) -> assert false (* absurd case *) | StructuredTraces.Tal_step_call (ends1, s1, s2, s3, s4, tlr, tal) -> let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0, (Obj.magic s2).RTLabs_abstract.ras_state, (Obj.magic s4).RTLabs_abstract.ras_state, (append_partial_flat_trace ge (Obj.magic s2).RTLabs_abstract.ras_state (Obj.magic s3).RTLabs_abstract.ras_state (Obj.magic s4).RTLabs_abstract.ras_state (flat_trace_of_label_return ge (Obj.magic s2) (Obj.magic s3) tlr) (flat_trace_of_any_label ge ends1 (Obj.magic s3) (Obj.magic s4) tal))) | StructuredTraces.Tal_step_default (ends1, s1, s2, s3, tal) -> let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0, (Obj.magic s2).RTLabs_abstract.ras_state, (Obj.magic s3).RTLabs_abstract.ras_state, (flat_trace_of_any_label ge ends1 (Obj.magic s2) (Obj.magic s3) tal)) (** val flat_trace_of_any_call : RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state -> Events.trace -> StructuredTraces.trace_any_call -> (IO.io_out, IO.io_in) partial_flat_trace **) let rec flat_trace_of_any_call ge s s' s'' et tr = (match tr with | StructuredTraces.Tac_base s1 -> (fun _ -> Pft_base ((Obj.magic s1).RTLabs_abstract.ras_state, et, s''.RTLabs_abstract.ras_state)) | StructuredTraces.Tac_step_call (s1, s2, s3, s4, tlr, tac) -> (fun _ -> let et0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s4) in Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, et0, (Obj.magic s4).RTLabs_abstract.ras_state, s''.RTLabs_abstract.ras_state, (append_partial_flat_trace ge (Obj.magic s4).RTLabs_abstract.ras_state (Obj.magic s2).RTLabs_abstract.ras_state s''.RTLabs_abstract.ras_state (flat_trace_of_label_return ge (Obj.magic s4) (Obj.magic s2) tlr) (flat_trace_of_any_call ge (Obj.magic s2) (Obj.magic s3) s'' et tac)))) | StructuredTraces.Tac_step_default (s1, s2, s3, tal) -> (fun _ -> let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s3) in Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0, (Obj.magic s3).RTLabs_abstract.ras_state, s''.RTLabs_abstract.ras_state, (flat_trace_of_any_call ge (Obj.magic s3) (Obj.magic s2) s'' et tal)))) __ (** val flat_trace_of_label_call : RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state -> Events.trace -> StructuredTraces.trace_label_call -> (IO.io_out, IO.io_in) partial_flat_trace **) let rec flat_trace_of_label_call ge s s' s'' et tr = (let StructuredTraces.Tlc_base (s1, s2, tac) = tr in (fun _ -> flat_trace_of_any_call ge (Obj.magic s1) (Obj.magic s2) s'' et tac)) __ (** val flat_trace_of_label_diverges : RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> StructuredTraces.trace_label_diverges -> (IO.io_out, IO.io_in) flat_trace **) let rec flat_trace_of_label_diverges ge s tr = match Lazy.force tr with | StructuredTraces.Tld_step (sx, sy, tll, tld) -> (let { RTLabs_abstract.ras_state = sy'; RTLabs_abstract.ras_fn_stack = stk } = Obj.magic sy in (fun tll0 -> (match flat_trace_of_label_label ge StructuredTraces.Doesnt_end_with_ret (Obj.magic sx) { RTLabs_abstract.ras_state = sy'; RTLabs_abstract.ras_fn_stack = stk } tll0 with | Pft_base (s1, tr0, s2) -> (fun _ tld0 -> lazy (Ft_step (s1, tr0, s2, (flat_trace_of_label_diverges ge { RTLabs_abstract.ras_state = s2; RTLabs_abstract.ras_fn_stack = stk } tld0)))) | Pft_step (s1, et, s2, s3, tr') -> (fun _ tld0 -> lazy (Ft_step (s1, et, s2, (add_partial_flat_trace ge s2 { RTLabs_abstract.ras_state = s3; RTLabs_abstract.ras_fn_stack = stk } tr' tld0))))) __)) tll tld | StructuredTraces.Tld_base (s1, s2, s3, tlc, tld) -> (let { RTLabs_abstract.ras_state = s3'; RTLabs_abstract.ras_fn_stack = stk } = Obj.magic s3 in (fun _ -> let tr0 = deprop_as_execute ge (Obj.magic s2) { RTLabs_abstract.ras_state = s3'; RTLabs_abstract.ras_fn_stack = stk } in (match flat_trace_of_label_call ge (Obj.magic s1) (Obj.magic s2) { RTLabs_abstract.ras_state = s3'; RTLabs_abstract.ras_fn_stack = stk } tr0 tlc with | Pft_base (s10, tr1, s20) -> (fun _ tld0 -> lazy (Ft_step (s10, tr1, s20, (flat_trace_of_label_diverges ge { RTLabs_abstract.ras_state = s20; RTLabs_abstract.ras_fn_stack = stk } tld0)))) | Pft_step (s10, et, s20, s30, tr') -> (fun _ tld0 -> lazy (Ft_step (s10, et, s20, (add_partial_flat_trace ge s20 { RTLabs_abstract.ras_state = s30; RTLabs_abstract.ras_fn_stack = stk } tr' tld0))))) __)) __ tld (** val add_partial_flat_trace : RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) partial_flat_trace -> StructuredTraces.trace_label_diverges -> (IO.io_out, IO.io_in) flat_trace **) and add_partial_flat_trace ge s s' = let { RTLabs_abstract.ras_state = sx; RTLabs_abstract.ras_fn_stack = stk } = s' in (fun ptr -> (match ptr with | Pft_base (s0, tr, s'0) -> (fun _ tr0 -> lazy (Ft_step (s0, tr, s'0, (flat_trace_of_label_diverges ge { RTLabs_abstract.ras_state = s'0; RTLabs_abstract.ras_fn_stack = stk } tr0)))) | Pft_step (s1, et, s2, s3, tr') -> (fun _ tr -> lazy (Ft_step (s1, et, s2, (add_partial_flat_trace ge s2 { RTLabs_abstract.ras_state = s3; RTLabs_abstract.ras_fn_stack = stk } tr' tr))))) __) (** val flat_trace_of_whole_program : RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> StructuredTraces.trace_whole_program -> (IO.io_out, IO.io_in) flat_trace **) let rec flat_trace_of_whole_program ge s = function | StructuredTraces.Twp_terminating (s1, s2, sf, tlr) -> let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in lazy (Ft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0, (Obj.magic s2).RTLabs_abstract.ras_state, (partial_to_flat_trace ge (Obj.magic s2).RTLabs_abstract.ras_state (Obj.magic sf).RTLabs_abstract.ras_state (flat_trace_of_label_return ge (Obj.magic s2) (Obj.magic sf) tlr) (lazy (Ft_stop (Obj.magic sf).RTLabs_abstract.ras_state))))) | StructuredTraces.Twp_diverges (s1, s2, tld) -> let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in lazy (Ft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0, (Obj.magic s2).RTLabs_abstract.ras_state, (flat_trace_of_label_diverges ge (Obj.magic s2) tld))) (** val state_fn : RTLabs_semantics.genv -> __ -> Pointers.block Types.option **) let state_fn ge s = match (Obj.magic s).RTLabs_abstract.ras_fn_stack with | List.Nil -> Types.None | List.Cons (h, t) -> (match (Obj.magic s).RTLabs_abstract.ras_state with | RTLabs_semantics.State (x, x0, x1) -> Types.Some h | RTLabs_semantics.Callstate (x, x0, x1, x2, x3, x4) -> (match t with | List.Nil -> Types.None | List.Cons (h', x5) -> Types.Some h') | RTLabs_semantics.Returnstate (x, x0, x1, x2) -> Types.Some h | RTLabs_semantics.Finalstate x -> Types.Some h) (** val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __ **) let option_jmdiscr x y = Logic.eq_rect_Type2 x (match x with | Types.None -> Obj.magic (fun _ dH -> dH) | Types.Some a0 -> Obj.magic (fun _ dH -> dH __)) y