open Preamble

open IO

open CostLabel

open PositiveMap

open Deqsets

open Lists

open Identifiers

open AST

open Division

open Z

open BitVectorZ

open Pointers

open Coqlib

open Values

open Events

open Exp

open Arithmetic

open Vector

open FoldStuff

open BitVector

open Extranat

open Integers

open Proper

open ErrorMessages

open Option

open Setoids

open Monad

open Positive

open PreIdentifiers

open Errors

open IOMonad

open Div_and_mod

open Jmeq

open Russell

open Util

open Bool

open Relations

open Nat

open List

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Extralib

open SmallstepExec

open Executions

open Hide

open Sets

open Listb

open StructuredTraces

open Stacksize

type classified_system = { cs_exec : (IO.io_out, IO.io_in)
                                     SmallstepExec.fullexec; cs_global : 
                           __; cs_labelled : (__ -> Bool.bool);
                           cs_classify : (__ ->
                                         StructuredTraces.status_class);
                           cs_callee : (__ -> __ -> AST.ident) }

(** val classified_system_rect_Type4 :
    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool)
    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
    'a1) -> classified_system -> 'a1 **)
let rec classified_system_rect_Type4 h_mk_classified_system x_23662 =
  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
    x_23662
  in
  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
    cs_callee0

(** val classified_system_rect_Type5 :
    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool)
    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
    'a1) -> classified_system -> 'a1 **)
let rec classified_system_rect_Type5 h_mk_classified_system x_23664 =
  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
    x_23664
  in
  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
    cs_callee0

(** val classified_system_rect_Type3 :
    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool)
    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
    'a1) -> classified_system -> 'a1 **)
let rec classified_system_rect_Type3 h_mk_classified_system x_23666 =
  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
    x_23666
  in
  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
    cs_callee0

(** val classified_system_rect_Type2 :
    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool)
    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
    'a1) -> classified_system -> 'a1 **)
let rec classified_system_rect_Type2 h_mk_classified_system x_23668 =
  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
    x_23668
  in
  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
    cs_callee0

(** val classified_system_rect_Type1 :
    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool)
    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
    'a1) -> classified_system -> 'a1 **)
let rec classified_system_rect_Type1 h_mk_classified_system x_23670 =
  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
    x_23670
  in
  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
    cs_callee0

(** val classified_system_rect_Type0 :
    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool)
    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
    'a1) -> classified_system -> 'a1 **)
let rec classified_system_rect_Type0 h_mk_classified_system x_23672 =
  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
    x_23672
  in
  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
    cs_callee0

(** val cs_exec :
    classified_system -> (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
let rec cs_exec xxx =
  xxx.cs_exec

(** val cs_global : classified_system -> __ **)
let rec cs_global xxx =
  xxx.cs_global

(** val cs_labelled : classified_system -> __ -> Bool.bool **)
let rec cs_labelled xxx =
  xxx.cs_labelled

(** val cs_classify :
    classified_system -> __ -> StructuredTraces.status_class **)
let rec cs_classify xxx =
  xxx.cs_classify

(** val cs_callee0 : classified_system -> __ -> AST.ident **)
let rec cs_callee0 xxx s =
  (xxx.cs_callee) s __

(** val classified_system_inv_rect_Type4 :
    classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __
    -> (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ ->
    __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
let classified_system_inv_rect_Type4 hterm h1 =
  let hcut = classified_system_rect_Type4 h1 hterm in hcut __

(** val classified_system_inv_rect_Type3 :
    classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __
    -> (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ ->
    __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
let classified_system_inv_rect_Type3 hterm h1 =
  let hcut = classified_system_rect_Type3 h1 hterm in hcut __

(** val classified_system_inv_rect_Type2 :
    classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __
    -> (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ ->
    __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
let classified_system_inv_rect_Type2 hterm h1 =
  let hcut = classified_system_rect_Type2 h1 hterm in hcut __

(** val classified_system_inv_rect_Type1 :
    classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __
    -> (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ ->
    __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
let classified_system_inv_rect_Type1 hterm h1 =
  let hcut = classified_system_rect_Type1 h1 hterm in hcut __

(** val classified_system_inv_rect_Type0 :
    classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __
    -> (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ ->
    __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
let classified_system_inv_rect_Type0 hterm h1 =
  let hcut = classified_system_rect_Type0 h1 hterm in hcut __

(** val cs_exec__o__es1 :
    classified_system -> (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
let cs_exec__o__es1 x0 =
  x0.cs_exec.SmallstepExec.es1

type cs_state = __

(** val intensional_event_of_event :
    Events.event -> StructuredTraces.intensional_event List.list **)
let intensional_event_of_event = function
| Events.EVcost l -> List.Cons ((StructuredTraces.IEVcost l), List.Nil)
| Events.EVextcall (x, x0, x1) -> List.Nil

(** val intensional_events_of_events :
    Events.trace -> StructuredTraces.intensional_event List.list **)
let intensional_events_of_events tr =
  List.flatten (List.map intensional_event_of_event tr)

(** val intensional_state_change :
    classified_system -> AST.ident List.list -> __ -> (AST.ident List.list,
    StructuredTraces.intensional_event List.list) Types.prod **)
let intensional_state_change c callstack s =
  (match c.cs_classify s with
   | StructuredTraces.Cl_return ->
     (fun x ->
       match callstack with
       | List.Nil -> { Types.fst = List.Nil; Types.snd = List.Nil }
       | List.Cons (id, tl) ->
         { Types.fst = tl; Types.snd = (List.Cons ((StructuredTraces.IEVret
           id), List.Nil)) })
   | StructuredTraces.Cl_jump ->
     (fun x -> { Types.fst = callstack; Types.snd = List.Nil })
   | StructuredTraces.Cl_call ->
     (fun callee ->
       let id = callee __ in
       { Types.fst = (List.Cons (id, callstack)); Types.snd = (List.Cons
       ((StructuredTraces.IEVcall id), List.Nil)) })
   | StructuredTraces.Cl_tailcall ->
     (fun x -> { Types.fst = callstack; Types.snd = List.Nil })
   | StructuredTraces.Cl_other ->
     (fun x -> { Types.fst = callstack; Types.snd = List.Nil })) (fun _ ->
    cs_callee0 c s)

(** val intensional_trace_of_trace :
    classified_system -> AST.ident List.list -> (cs_state, Events.trace)
    Types.prod List.list -> (AST.ident List.list,
    StructuredTraces.intensional_event List.list) Types.prod **)
let rec intensional_trace_of_trace c callstack = function
| List.Nil -> { Types.fst = callstack; Types.snd = List.Nil }
| List.Cons (str, tl) ->
  let { Types.fst = s; Types.snd = tr } = str in
  let { Types.fst = callstack0; Types.snd = call_event } =
    intensional_state_change c callstack s
  in
  let other_events = intensional_events_of_events tr in
  let { Types.fst = callstack1; Types.snd = rem } =
    intensional_trace_of_trace c callstack0 tl
  in
  { Types.fst = callstack1; Types.snd =
  (List.append call_event (List.append other_events rem)) }

(** val normal_state : classified_system -> cs_state -> Bool.bool **)
let normal_state c s =
  match c.cs_classify s with
  | StructuredTraces.Cl_return -> Bool.False
  | StructuredTraces.Cl_jump -> Bool.True
  | StructuredTraces.Cl_call -> Bool.False
  | StructuredTraces.Cl_tailcall -> Bool.False
  | StructuredTraces.Cl_other -> Bool.True

(** val measure_stack :
    (AST.ident -> Nat.nat Types.option) -> Stacksize.stacksize_info ->
    StructuredTraces.intensional_event List.list -> Stacksize.stacksize_info **)
let measure_stack costs start ev =
  Stacksize.update_stacksize_info costs start
    (Stacksize.extract_call_ud_from_observables ev)

(** val will_return_aux :
    classified_system -> Nat.nat -> (cs_state, Events.trace) Types.prod
    List.list -> Bool.bool **)
let rec will_return_aux c depth = function
| List.Nil -> Bool.False
| List.Cons (h, tl) ->
  let { Types.fst = s; Types.snd = tr } = h in
  (match c.cs_classify s with
   | StructuredTraces.Cl_return ->
     (match depth with
      | Nat.O ->
        (match tl with
         | List.Nil -> Bool.True
         | List.Cons (x, x0) -> Bool.False)
      | Nat.S d -> will_return_aux c d tl)
   | StructuredTraces.Cl_jump -> will_return_aux c depth tl
   | StructuredTraces.Cl_call -> will_return_aux c (Nat.S depth) tl
   | StructuredTraces.Cl_tailcall -> will_return_aux c depth tl
   | StructuredTraces.Cl_other -> will_return_aux c depth tl)

(** val will_return' :
    classified_system -> (cs_state, Events.trace) Types.prod List.list ->
    Bool.bool **)
let will_return' c =
  will_return_aux c Nat.O

type preclassified_system = { pcs_exec : (IO.io_out, IO.io_in)
                                         SmallstepExec.fullexec;
                              pcs_labelled : (__ -> __ -> Bool.bool);
                              pcs_classify : (__ -> __ ->
                                             StructuredTraces.status_class);
                              pcs_callee : (__ -> __ -> __ -> AST.ident) }

(** val preclassified_system_rect_Type4 :
    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool)
    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
let rec preclassified_system_rect_Type4 h_mk_preclassified_system x_23692 =
  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
    pcs_classify0; pcs_callee = pcs_callee0 } = x_23692
  in
  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0

(** val preclassified_system_rect_Type5 :
    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool)
    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
let rec preclassified_system_rect_Type5 h_mk_preclassified_system x_23694 =
  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
    pcs_classify0; pcs_callee = pcs_callee0 } = x_23694
  in
  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0

(** val preclassified_system_rect_Type3 :
    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool)
    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
let rec preclassified_system_rect_Type3 h_mk_preclassified_system x_23696 =
  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
    pcs_classify0; pcs_callee = pcs_callee0 } = x_23696
  in
  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0

(** val preclassified_system_rect_Type2 :
    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool)
    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
let rec preclassified_system_rect_Type2 h_mk_preclassified_system x_23698 =
  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
    pcs_classify0; pcs_callee = pcs_callee0 } = x_23698
  in
  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0

(** val preclassified_system_rect_Type1 :
    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool)
    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
let rec preclassified_system_rect_Type1 h_mk_preclassified_system x_23700 =
  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
    pcs_classify0; pcs_callee = pcs_callee0 } = x_23700
  in
  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0

(** val preclassified_system_rect_Type0 :
    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool)
    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
let rec preclassified_system_rect_Type0 h_mk_preclassified_system x_23702 =
  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
    pcs_classify0; pcs_callee = pcs_callee0 } = x_23702
  in
  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0

(** val pcs_exec :
    preclassified_system -> (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
let rec pcs_exec xxx =
  xxx.pcs_exec

(** val pcs_labelled : preclassified_system -> __ -> __ -> Bool.bool **)
let rec pcs_labelled xxx =
  xxx.pcs_labelled

(** val pcs_classify :
    preclassified_system -> __ -> __ -> StructuredTraces.status_class **)
let rec pcs_classify xxx =
  xxx.pcs_classify

(** val pcs_callee0 : preclassified_system -> __ -> __ -> AST.ident **)
let rec pcs_callee0 xxx g s =
  (xxx.pcs_callee) g s __

(** val preclassified_system_inv_rect_Type4 :
    preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
    (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
    (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
let preclassified_system_inv_rect_Type4 hterm h1 =
  let hcut = preclassified_system_rect_Type4 h1 hterm in hcut __

(** val preclassified_system_inv_rect_Type3 :
    preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
    (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
    (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
let preclassified_system_inv_rect_Type3 hterm h1 =
  let hcut = preclassified_system_rect_Type3 h1 hterm in hcut __

(** val preclassified_system_inv_rect_Type2 :
    preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
    (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
    (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
let preclassified_system_inv_rect_Type2 hterm h1 =
  let hcut = preclassified_system_rect_Type2 h1 hterm in hcut __

(** val preclassified_system_inv_rect_Type1 :
    preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
    (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
    (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
let preclassified_system_inv_rect_Type1 hterm h1 =
  let hcut = preclassified_system_rect_Type1 h1 hterm in hcut __

(** val preclassified_system_inv_rect_Type0 :
    preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
    (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
    (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
let preclassified_system_inv_rect_Type0 hterm h1 =
  let hcut = preclassified_system_rect_Type0 h1 hterm in hcut __

(** val pcs_exec__o__es1 :
    preclassified_system -> (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
let pcs_exec__o__es1 x0 =
  x0.pcs_exec.SmallstepExec.es1

(** val pcs_to_cs : preclassified_system -> __ -> classified_system **)
let pcs_to_cs c g =
  { cs_exec = c.pcs_exec; cs_global = g; cs_labelled = (c.pcs_labelled g);
    cs_classify = (c.pcs_classify g); cs_callee = (fun x _ ->
    pcs_callee0 c g x) }

(** val observables :
    preclassified_system -> __ -> Nat.nat -> Nat.nat ->
    (StructuredTraces.intensional_event List.list,
    StructuredTraces.intensional_event List.list) Types.prod Errors.res **)
let observables c p m n =
  let g = c.pcs_exec.SmallstepExec.make_global p in
  let c' = pcs_to_cs c g in
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic (c.pcs_exec.SmallstepExec.make_initial_state p)) (fun s0 ->
      Monad.m_bind2 (Monad.max_def Errors.res0)
        (Obj.magic (SmallstepExec.exec_steps m c'.cs_exec g s0))
        (fun prefix s1 ->
        Monad.m_bind2 (Monad.max_def Errors.res0)
          (Obj.magic (SmallstepExec.exec_steps n c'.cs_exec g s1))
          (fun interesting s2 ->
          let { Types.fst = cs; Types.snd = prefix' } =
            intensional_trace_of_trace c' List.Nil prefix
          in
          Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = prefix';
            Types.snd =
            (intensional_trace_of_trace c' cs interesting).Types.snd }))))

(** val observe_all_in_measurable :
    Nat.nat -> classified_system -> (StructuredTraces.intensional_event ->
    Types.unit0) -> AST.ident List.list -> __ ->
    (StructuredTraces.intensional_event List.list, Integers.int Errors.res)
    Types.prod **)
let rec observe_all_in_measurable n fx observe callstack s =
  match n with
  | Nat.O ->
    let res =
      match (cs_exec__o__es1 fx).SmallstepExec.is_final fx.cs_global s with
      | Types.None -> Errors.Error (Errors.msg ErrorMessages.NotTerminated)
      | Types.Some r -> Errors.OK r
    in
    { Types.fst = List.Nil; Types.snd = res }
  | Nat.S m ->
    (match (cs_exec__o__es1 fx).SmallstepExec.is_final fx.cs_global s with
     | Types.None ->
       (match (cs_exec__o__es1 fx).SmallstepExec.step fx.cs_global s with
        | IOMonad.Interact (x, x0) ->
          { Types.fst = List.Nil; Types.snd = (Errors.Error
            (Errors.msg ErrorMessages.UnexpectedIO)) }
        | IOMonad.Value trs ->
          let costevents =
            List.flatten (List.map intensional_event_of_event trs.Types.fst)
          in
          let { Types.fst = callstack0; Types.snd = callevent } =
            (match fx.cs_classify s with
             | StructuredTraces.Cl_return ->
               (fun x ->
                 match callstack with
                 | List.Nil -> { Types.fst = List.Nil; Types.snd = List.Nil }
                 | List.Cons (id, tl) ->
                   { Types.fst = tl; Types.snd = (List.Cons
                     ((StructuredTraces.IEVret id), List.Nil)) })
             | StructuredTraces.Cl_jump ->
               (fun x -> { Types.fst = callstack; Types.snd = List.Nil })
             | StructuredTraces.Cl_call ->
               (fun callee ->
                 let id = callee __ in
                 { Types.fst = (List.Cons (id, callstack)); Types.snd =
                 (List.Cons ((StructuredTraces.IEVcall id), List.Nil)) })
             | StructuredTraces.Cl_tailcall ->
               (fun x -> { Types.fst = callstack; Types.snd = List.Nil })
             | StructuredTraces.Cl_other ->
               (fun x -> { Types.fst = callstack; Types.snd = List.Nil }))
              (fun _ -> cs_callee0 fx s)
          in
          let events = List.append costevents callevent in
          let dummy = List.map observe events in
          let { Types.fst = tl; Types.snd = res } =
            observe_all_in_measurable m fx observe callstack0 trs.Types.snd
          in
          { Types.fst = (List.append events tl); Types.snd = res }
        | IOMonad.Wrong m0 ->
          { Types.fst = List.Nil; Types.snd = (Errors.Error m0) })
     | Types.Some r -> { Types.fst = List.Nil; Types.snd = (Errors.OK r) })