open Preamble

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 Proper

open ErrorMessages

open Option

open Setoids

open Monad

open Positive

open PreIdentifiers

open Errors

open IOMonad

open Exp

open Arithmetic

open Vector

open FoldStuff

open BitVector

open Extranat

open Integers

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

type ('outty, 'inty) trans_system = { is_final : (__ -> __ -> Integers.int
                                                 Types.option);
                                      step : (__ -> __ -> ('outty, 'inty,
                                             (Events.trace, __) Types.prod)
                                             IOMonad.iO) }

(** val trans_system_rect_Type4 :
    (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
    'a2) trans_system -> 'a3 **)
let rec trans_system_rect_Type4 h_mk_trans_system x_5925 =
  let { is_final = is_final0; step = step0 } = x_5925 in
  h_mk_trans_system __ __ is_final0 step0

(** val trans_system_rect_Type5 :
    (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
    'a2) trans_system -> 'a3 **)
let rec trans_system_rect_Type5 h_mk_trans_system x_5927 =
  let { is_final = is_final0; step = step0 } = x_5927 in
  h_mk_trans_system __ __ is_final0 step0

(** val trans_system_rect_Type3 :
    (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
    'a2) trans_system -> 'a3 **)
let rec trans_system_rect_Type3 h_mk_trans_system x_5929 =
  let { is_final = is_final0; step = step0 } = x_5929 in
  h_mk_trans_system __ __ is_final0 step0

(** val trans_system_rect_Type2 :
    (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
    'a2) trans_system -> 'a3 **)
let rec trans_system_rect_Type2 h_mk_trans_system x_5931 =
  let { is_final = is_final0; step = step0 } = x_5931 in
  h_mk_trans_system __ __ is_final0 step0

(** val trans_system_rect_Type1 :
    (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
    'a2) trans_system -> 'a3 **)
let rec trans_system_rect_Type1 h_mk_trans_system x_5933 =
  let { is_final = is_final0; step = step0 } = x_5933 in
  h_mk_trans_system __ __ is_final0 step0

(** val trans_system_rect_Type0 :
    (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ ->
    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
    'a2) trans_system -> 'a3 **)
let rec trans_system_rect_Type0 h_mk_trans_system x_5935 =
  let { is_final = is_final0; step = step0 } = x_5935 in
  h_mk_trans_system __ __ is_final0 step0

type ('x, 'x0) global = __

type ('x, 'x0) state = __

(** val is_final :
    ('a1, 'a2) trans_system -> __ -> __ -> Integers.int Types.option **)
let rec is_final xxx =
  xxx.is_final

(** val step :
    ('a1, 'a2) trans_system -> __ -> __ -> ('a1, 'a2, (Events.trace, __)
    Types.prod) IOMonad.iO **)
let rec step xxx =
  xxx.step

(** val trans_system_inv_rect_Type4 :
    ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
    Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
    IOMonad.iO) -> __ -> 'a3) -> 'a3 **)
let trans_system_inv_rect_Type4 hterm h1 =
  let hcut = trans_system_rect_Type4 h1 hterm in hcut __

(** val trans_system_inv_rect_Type3 :
    ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
    Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
    IOMonad.iO) -> __ -> 'a3) -> 'a3 **)
let trans_system_inv_rect_Type3 hterm h1 =
  let hcut = trans_system_rect_Type3 h1 hterm in hcut __

(** val trans_system_inv_rect_Type2 :
    ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
    Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
    IOMonad.iO) -> __ -> 'a3) -> 'a3 **)
let trans_system_inv_rect_Type2 hterm h1 =
  let hcut = trans_system_rect_Type2 h1 hterm in hcut __

(** val trans_system_inv_rect_Type1 :
    ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
    Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
    IOMonad.iO) -> __ -> 'a3) -> 'a3 **)
let trans_system_inv_rect_Type1 hterm h1 =
  let hcut = trans_system_rect_Type1 h1 hterm in hcut __

(** val trans_system_inv_rect_Type0 :
    ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
    Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
    IOMonad.iO) -> __ -> 'a3) -> 'a3 **)
let trans_system_inv_rect_Type0 hterm h1 =
  let hcut = trans_system_rect_Type0 h1 hterm in hcut __

(** val repeat :
    Nat.nat -> ('a1, 'a2) trans_system -> __ -> __ -> ('a1, 'a2,
    (Events.trace, __) Types.prod) IOMonad.iO **)
let rec repeat n exec g s =
  match n with
  | Nat.O -> IOMonad.Value { Types.fst = Events.e0; Types.snd = s }
  | Nat.S n' ->
    Obj.magic
      (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
        (Obj.magic (exec.step g s)) (fun t1 s1 ->
        Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
          (Obj.magic (repeat n' exec g s1)) (fun tn sn ->
          Obj.magic (IOMonad.Value { Types.fst = (Events.eapp t1 tn);
            Types.snd = sn }))))

(** val trace_map :
    ('a1 -> (Events.trace, 'a2) Types.prod Errors.res) -> 'a1 List.list ->
    (Events.trace, 'a2 List.list) Types.prod Errors.res **)
let rec trace_map f = function
| List.Nil -> Errors.OK { Types.fst = Events.e0; Types.snd = List.Nil }
| List.Cons (h, t) ->
  Obj.magic
    (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic f h) (fun tr h' ->
      Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (trace_map f t))
        (fun tr' t' ->
        Obj.magic (Errors.OK { Types.fst = (Events.eapp tr tr'); Types.snd =
          (List.Cons (h', t')) }))))

type await_value_stuff = { avs_exec : (__, __) trans_system; avs_g : 
                           __; avs_inv : (__ -> Bool.bool) }

(** val await_value_stuff_rect_Type4 :
    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
    await_value_stuff -> 'a1 **)
let rec await_value_stuff_rect_Type4 h_mk_await_value_stuff x_6097 =
  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6097
  in
  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0

(** val await_value_stuff_rect_Type5 :
    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
    await_value_stuff -> 'a1 **)
let rec await_value_stuff_rect_Type5 h_mk_await_value_stuff x_6099 =
  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6099
  in
  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0

(** val await_value_stuff_rect_Type3 :
    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
    await_value_stuff -> 'a1 **)
let rec await_value_stuff_rect_Type3 h_mk_await_value_stuff x_6101 =
  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6101
  in
  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0

(** val await_value_stuff_rect_Type2 :
    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
    await_value_stuff -> 'a1 **)
let rec await_value_stuff_rect_Type2 h_mk_await_value_stuff x_6103 =
  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6103
  in
  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0

(** val await_value_stuff_rect_Type1 :
    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
    await_value_stuff -> 'a1 **)
let rec await_value_stuff_rect_Type1 h_mk_await_value_stuff x_6105 =
  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6105
  in
  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0

(** val await_value_stuff_rect_Type0 :
    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
    await_value_stuff -> 'a1 **)
let rec await_value_stuff_rect_Type0 h_mk_await_value_stuff x_6107 =
  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6107
  in
  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0

type avs_O = __

type avs_I = __

(** val avs_exec : await_value_stuff -> (__, __) trans_system **)
let rec avs_exec xxx =
  xxx.avs_exec

(** val avs_g : await_value_stuff -> __ **)
let rec avs_g xxx =
  xxx.avs_g

(** val avs_inv : await_value_stuff -> __ -> Bool.bool **)
let rec avs_inv xxx =
  xxx.avs_inv

(** val await_value_stuff_inv_rect_Type4 :
    await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
    Bool.bool) -> __ -> 'a1) -> 'a1 **)
let await_value_stuff_inv_rect_Type4 hterm h1 =
  let hcut = await_value_stuff_rect_Type4 h1 hterm in hcut __

(** val await_value_stuff_inv_rect_Type3 :
    await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
    Bool.bool) -> __ -> 'a1) -> 'a1 **)
let await_value_stuff_inv_rect_Type3 hterm h1 =
  let hcut = await_value_stuff_rect_Type3 h1 hterm in hcut __

(** val await_value_stuff_inv_rect_Type2 :
    await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
    Bool.bool) -> __ -> 'a1) -> 'a1 **)
let await_value_stuff_inv_rect_Type2 hterm h1 =
  let hcut = await_value_stuff_rect_Type2 h1 hterm in hcut __

(** val await_value_stuff_inv_rect_Type1 :
    await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
    Bool.bool) -> __ -> 'a1) -> 'a1 **)
let await_value_stuff_inv_rect_Type1 hterm h1 =
  let hcut = await_value_stuff_rect_Type1 h1 hterm in hcut __

(** val await_value_stuff_inv_rect_Type0 :
    await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
    Bool.bool) -> __ -> 'a1) -> 'a1 **)
let await_value_stuff_inv_rect_Type0 hterm h1 =
  let hcut = await_value_stuff_rect_Type0 h1 hterm in hcut __

type ('state, 'output, 'input) execution = ('state, 'output, 'input) __execution Lazy.t
and ('state, 'output, 'input) __execution =
| E_stop of Events.trace * Integers.int * 'state
| E_step of Events.trace * 'state * ('state, 'output, 'input) execution
| E_wrong of Errors.errmsg
| E_interact of 'output * ('input -> ('state, 'output, 'input) execution)

(** val execution_inv_rect_Type4 :
    ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __
    -> 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ ->
    'a4) -> (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3)
    execution) -> __ -> 'a4) -> 'a4 **)
let execution_inv_rect_Type4 hterm h1 h2 h3 h4 =
  let hcut =
    match Lazy.force
    hterm with
    | E_stop (x, x0, x1) -> h1 x x0 x1
    | E_step (x, x0, x1) -> h2 x x0 x1
    | E_wrong x -> h3 x
    | E_interact (x, x0) -> h4 x x0
  in
  hcut __

(** val execution_inv_rect_Type3 :
    ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __
    -> 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ ->
    'a4) -> (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3)
    execution) -> __ -> 'a4) -> 'a4 **)
let execution_inv_rect_Type3 hterm h1 h2 h3 h4 =
  let hcut =
    match Lazy.force
    hterm with
    | E_stop (x, x0, x1) -> h1 x x0 x1
    | E_step (x, x0, x1) -> h2 x x0 x1
    | E_wrong x -> h3 x
    | E_interact (x, x0) -> h4 x x0
  in
  hcut __

(** val execution_inv_rect_Type2 :
    ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __
    -> 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ ->
    'a4) -> (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3)
    execution) -> __ -> 'a4) -> 'a4 **)
let execution_inv_rect_Type2 hterm h1 h2 h3 h4 =
  let hcut =
    match Lazy.force
    hterm with
    | E_stop (x, x0, x1) -> h1 x x0 x1
    | E_step (x, x0, x1) -> h2 x x0 x1
    | E_wrong x -> h3 x
    | E_interact (x, x0) -> h4 x x0
  in
  hcut __

(** val execution_inv_rect_Type1 :
    ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __
    -> 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ ->
    'a4) -> (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3)
    execution) -> __ -> 'a4) -> 'a4 **)
let execution_inv_rect_Type1 hterm h1 h2 h3 h4 =
  let hcut =
    match Lazy.force
    hterm with
    | E_stop (x, x0, x1) -> h1 x x0 x1
    | E_step (x, x0, x1) -> h2 x x0 x1
    | E_wrong x -> h3 x
    | E_interact (x, x0) -> h4 x x0
  in
  hcut __

(** val execution_inv_rect_Type0 :
    ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __
    -> 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ ->
    'a4) -> (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3)
    execution) -> __ -> 'a4) -> 'a4 **)
let execution_inv_rect_Type0 hterm h1 h2 h3 h4 =
  let hcut =
    match Lazy.force
    hterm with
    | E_stop (x, x0, x1) -> h1 x x0 x1
    | E_step (x, x0, x1) -> h2 x x0 x1
    | E_wrong x -> h3 x
    | E_interact (x, x0) -> h4 x x0
  in
  hcut __

(** val execution_discr :
    ('a1, 'a2, 'a3) execution -> ('a1, 'a2, 'a3) execution -> __ **)
let execution_discr x y =
  Logic.eq_rect_Type2 x
    (match Lazy.force
     x with
     | E_stop (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
     | E_step (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
     | E_wrong a0 -> Obj.magic (fun _ dH -> dH __)
     | E_interact (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val execution_jmdiscr :
    ('a1, 'a2, 'a3) execution -> ('a1, 'a2, 'a3) execution -> __ **)
let execution_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match Lazy.force
     x with
     | E_stop (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
     | E_step (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
     | E_wrong a0 -> Obj.magic (fun _ dH -> dH __)
     | E_interact (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val exec_inf_aux :
    ('a1, 'a2) trans_system -> __ -> ('a1, 'a2, (Events.trace, __)
    Types.prod) IOMonad.iO -> (__, 'a1, 'a2) execution **)
let rec exec_inf_aux exec g = function
| IOMonad.Interact (out, k') ->
  lazy (E_interact (out, (fun v -> exec_inf_aux exec g (k' v))))
| IOMonad.Value v ->
  let { Types.fst = t; Types.snd = s' } = v in
  (match exec.is_final g s' with
   | Types.None ->
     lazy (E_step (t, s', (exec_inf_aux exec g (exec.step g s'))))
   | Types.Some r -> lazy (E_stop (t, r, s')))
| IOMonad.Wrong m -> lazy (E_wrong m)

type ('outty, 'inty) fullexec = { es1 : ('outty, 'inty) trans_system;
                                  make_global : (__ -> __);
                                  make_initial_state : (__ -> __ Errors.res) }

(** val fullexec_rect_Type4 :
    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
let rec fullexec_rect_Type4 h_mk_fullexec x_6125 =
  let { es1 = es2; make_global = make_global0; make_initial_state =
    make_initial_state0 } = x_6125
  in
  h_mk_fullexec __ es2 make_global0 make_initial_state0

(** val fullexec_rect_Type5 :
    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
let rec fullexec_rect_Type5 h_mk_fullexec x_6127 =
  let { es1 = es2; make_global = make_global0; make_initial_state =
    make_initial_state0 } = x_6127
  in
  h_mk_fullexec __ es2 make_global0 make_initial_state0

(** val fullexec_rect_Type3 :
    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
let rec fullexec_rect_Type3 h_mk_fullexec x_6129 =
  let { es1 = es2; make_global = make_global0; make_initial_state =
    make_initial_state0 } = x_6129
  in
  h_mk_fullexec __ es2 make_global0 make_initial_state0

(** val fullexec_rect_Type2 :
    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
let rec fullexec_rect_Type2 h_mk_fullexec x_6131 =
  let { es1 = es2; make_global = make_global0; make_initial_state =
    make_initial_state0 } = x_6131
  in
  h_mk_fullexec __ es2 make_global0 make_initial_state0

(** val fullexec_rect_Type1 :
    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
let rec fullexec_rect_Type1 h_mk_fullexec x_6133 =
  let { es1 = es2; make_global = make_global0; make_initial_state =
    make_initial_state0 } = x_6133
  in
  h_mk_fullexec __ es2 make_global0 make_initial_state0

(** val fullexec_rect_Type0 :
    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
let rec fullexec_rect_Type0 h_mk_fullexec x_6135 =
  let { es1 = es2; make_global = make_global0; make_initial_state =
    make_initial_state0 } = x_6135
  in
  h_mk_fullexec __ es2 make_global0 make_initial_state0

type ('x, 'x0) program = __

(** val es1 : ('a1, 'a2) fullexec -> ('a1, 'a2) trans_system **)
let rec es1 xxx =
  xxx.es1

(** val make_global : ('a1, 'a2) fullexec -> __ -> __ **)
let rec make_global xxx =
  xxx.make_global

(** val make_initial_state : ('a1, 'a2) fullexec -> __ -> __ Errors.res **)
let rec make_initial_state xxx =
  xxx.make_initial_state

(** val fullexec_inv_rect_Type4 :
    ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
    (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
let fullexec_inv_rect_Type4 hterm h1 =
  let hcut = fullexec_rect_Type4 h1 hterm in hcut __

(** val fullexec_inv_rect_Type3 :
    ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
    (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
let fullexec_inv_rect_Type3 hterm h1 =
  let hcut = fullexec_rect_Type3 h1 hterm in hcut __

(** val fullexec_inv_rect_Type2 :
    ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
    (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
let fullexec_inv_rect_Type2 hterm h1 =
  let hcut = fullexec_rect_Type2 h1 hterm in hcut __

(** val fullexec_inv_rect_Type1 :
    ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
    (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
let fullexec_inv_rect_Type1 hterm h1 =
  let hcut = fullexec_rect_Type1 h1 hterm in hcut __

(** val fullexec_inv_rect_Type0 :
    ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) ->
    (__ -> __ Errors.res) -> __ -> 'a3) -> 'a3 **)
let fullexec_inv_rect_Type0 hterm h1 =
  let hcut = fullexec_rect_Type0 h1 hterm in hcut __

(** val exec_inf : ('a1, 'a2) fullexec -> __ -> (__, 'a1, 'a2) execution **)
let exec_inf fx p =
  match fx.make_initial_state p with
  | Errors.OK s ->
    exec_inf_aux fx.es1 (fx.make_global p) (IOMonad.Value { Types.fst =
      Events.e0; Types.snd = s })
  | Errors.Error m -> lazy (E_wrong m)

type 'x execution_prefix = (Events.trace, 'x) Types.prod List.list

(** val split_trace :
    ('a3, 'a1, 'a2) execution -> Nat.nat -> ('a3 execution_prefix, ('a3, 'a1,
    'a2) execution) Types.prod Types.option **)
let rec split_trace x = function
| Nat.O -> Types.Some { Types.fst = List.Nil; Types.snd = x }
| Nat.S n' ->
  (match Lazy.force
   x with
   | E_stop (tr, r, s) ->
     (match n' with
      | Nat.O ->
        Types.Some { Types.fst = (List.Cons ({ Types.fst = tr; Types.snd =
          s }, List.Nil)); Types.snd = x }
      | Nat.S x0 -> Types.None)
   | E_step (tr, s, x') ->
     Obj.magic
       (Monad.m_bind2 (Monad.max_def Option.option)
         (Obj.magic (split_trace x' n')) (fun pre x'' ->
         Obj.magic (Types.Some { Types.fst = (List.Cons ({ Types.fst = tr;
           Types.snd = s }, pre)); Types.snd = x'' })))
   | E_wrong x0 -> Types.None
   | E_interact (x0, x1) -> Types.None)

(** val exec_steps :
    Nat.nat -> ('a1, 'a2) fullexec -> __ -> __ -> ((__, Events.trace)
    Types.prod List.list, __) Types.prod Errors.res **)
let rec exec_steps n fx g s =
  match n with
  | Nat.O ->
    Obj.magic
      (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = List.Nil;
        Types.snd = s })
  | Nat.S m ->
    (match fx.es1.is_final g s with
     | Types.None ->
       (match fx.es1.step g s with
        | IOMonad.Interact (x, x0) ->
          Errors.Error (Errors.msg ErrorMessages.UnexpectedIO)
        | IOMonad.Value trs ->
          Obj.magic
            (Monad.m_bind2 (Monad.max_def Errors.res0)
              (Obj.magic (exec_steps m fx g trs.Types.snd)) (fun tl s' ->
              Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
                (List.Cons ({ Types.fst = s; Types.snd = trs.Types.fst },
                tl)); Types.snd = s' }))
        | IOMonad.Wrong m0 -> Errors.Error m0)
     | Types.Some r ->
       Errors.Error (Errors.msg ErrorMessages.TerminatedEarly))

(** val gather_trace :
    ('a1, Events.trace) Types.prod List.list -> Events.trace **)
let rec gather_trace = function
| List.Nil -> Events.e0
| List.Cons (h, t) -> Events.eapp h.Types.snd (gather_trace t)

(** val switch_trace_aux :
    Events.trace -> ('a1, Events.trace) Types.prod List.list -> 'a1 ->
    (Events.trace, 'a1) Types.prod List.list **)
let rec switch_trace_aux tr l s' =
  match l with
  | List.Nil -> List.Cons ({ Types.fst = tr; Types.snd = s' }, List.Nil)
  | List.Cons (h, t) ->
    List.Cons ({ Types.fst = tr; Types.snd = h.Types.fst },
      (switch_trace_aux h.Types.snd t s'))

(** val switch_trace :
    ('a1, Events.trace) Types.prod List.list -> 'a1 -> (Events.trace, 'a1)
    Types.prod List.list **)
let switch_trace l s' =
  match l with
  | List.Nil -> List.Nil
  | List.Cons (h, t) -> switch_trace_aux h.Types.snd t s'