open Preamble

open Proper

open ErrorMessages

open Option

open Setoids

open Monad

open Positive

open PreIdentifiers

open Errors

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 IOMonad

open CostLabel

open PositiveMap

open Deqsets

open Lists

open Identifiers

open Integers

open AST

open Division

open Exp

open Arithmetic

open Extranat

open Vector

open FoldStuff

open BitVector

open Z

open BitVectorZ

open Pointers

open Coqlib

open Values

open Events

type eventval_type = __

(** val mk_eventval : AST.typ -> eventval_type -> Events.eventval **)
let mk_eventval = function
| AST.ASTint (sz, sg) -> (fun v -> Events.EVint (sz, (Obj.magic v)))
| AST.ASTptr -> Obj.magic (fun _ -> assert false (* absurd case *))

(** val mk_val : AST.typ -> eventval_type -> Values.val0 **)
let mk_val = function
| AST.ASTint (sz, x) -> (fun v -> Values.Vint (sz, (Obj.magic v)))
| AST.ASTptr -> Obj.magic (fun _ -> assert false (* absurd case *))

(** val convert_eventval :
    Events.eventval -> AST.typ -> Values.val0 Errors.res **)
let convert_eventval ev = function
| AST.ASTint (sz, x) ->
  let Events.EVint (sz', i) = ev in
  (match AST.eq_intsize sz sz' with
   | Bool.True -> Errors.OK (Values.Vint (sz', i))
   | Bool.False -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent))
| AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)

(** val check_eventval' :
    Values.val0 -> AST.typ -> Events.eventval Errors.res **)
let check_eventval' v = function
| AST.ASTint (sz, x) ->
  (match v with
   | Values.Vundef -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
   | Values.Vint (sz', i) ->
     (match AST.eq_intsize sz sz' with
      | Bool.True -> Errors.OK (Events.EVint (sz', i))
      | Bool.False -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent))
   | Values.Vnull -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
   | Values.Vptr x0 -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent))
| AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)

(** val check_eventval_list :
    Values.val0 List.list -> AST.typ List.list -> Events.eventval List.list
    Errors.res **)
let rec check_eventval_list vs tys =
  match vs with
  | List.Nil ->
    (match tys with
     | List.Nil -> Errors.OK List.Nil
     | List.Cons (x, x0) ->
       Errors.Error (Errors.msg ErrorMessages.IllTypedEvent))
  | List.Cons (v, vt) ->
    (match tys with
     | List.Nil -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
     | List.Cons (ty, tyt) ->
       Obj.magic
         (Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic (check_eventval' v ty)) (fun ev ->
           Monad.m_bind0 (Monad.max_def Errors.res0)
             (Obj.magic (check_eventval_list vt tyt)) (fun evt ->
             Obj.magic (Errors.OK (List.Cons (ev, evt)))))))

type io_out = { io_function : AST.ident; io_args : Events.eventval List.list;
                io_in_typ : AST.typ }

(** val io_out_rect_Type4 :
    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
    'a1 **)
let rec io_out_rect_Type4 h_mk_io_out x_5899 =
  let { io_function = io_function0; io_args = io_args0; io_in_typ =
    io_in_typ0 } = x_5899
  in
  h_mk_io_out io_function0 io_args0 io_in_typ0

(** val io_out_rect_Type5 :
    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
    'a1 **)
let rec io_out_rect_Type5 h_mk_io_out x_5901 =
  let { io_function = io_function0; io_args = io_args0; io_in_typ =
    io_in_typ0 } = x_5901
  in
  h_mk_io_out io_function0 io_args0 io_in_typ0

(** val io_out_rect_Type3 :
    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
    'a1 **)
let rec io_out_rect_Type3 h_mk_io_out x_5903 =
  let { io_function = io_function0; io_args = io_args0; io_in_typ =
    io_in_typ0 } = x_5903
  in
  h_mk_io_out io_function0 io_args0 io_in_typ0

(** val io_out_rect_Type2 :
    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
    'a1 **)
let rec io_out_rect_Type2 h_mk_io_out x_5905 =
  let { io_function = io_function0; io_args = io_args0; io_in_typ =
    io_in_typ0 } = x_5905
  in
  h_mk_io_out io_function0 io_args0 io_in_typ0

(** val io_out_rect_Type1 :
    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
    'a1 **)
let rec io_out_rect_Type1 h_mk_io_out x_5907 =
  let { io_function = io_function0; io_args = io_args0; io_in_typ =
    io_in_typ0 } = x_5907
  in
  h_mk_io_out io_function0 io_args0 io_in_typ0

(** val io_out_rect_Type0 :
    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
    'a1 **)
let rec io_out_rect_Type0 h_mk_io_out x_5909 =
  let { io_function = io_function0; io_args = io_args0; io_in_typ =
    io_in_typ0 } = x_5909
  in
  h_mk_io_out io_function0 io_args0 io_in_typ0

(** val io_function : io_out -> AST.ident **)
let rec io_function xxx =
  xxx.io_function

(** val io_args : io_out -> Events.eventval List.list **)
let rec io_args xxx =
  xxx.io_args

(** val io_in_typ : io_out -> AST.typ **)
let rec io_in_typ xxx =
  xxx.io_in_typ

(** val io_out_inv_rect_Type4 :
    io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
    'a1) -> 'a1 **)
let io_out_inv_rect_Type4 hterm h1 =
  let hcut = io_out_rect_Type4 h1 hterm in hcut __

(** val io_out_inv_rect_Type3 :
    io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
    'a1) -> 'a1 **)
let io_out_inv_rect_Type3 hterm h1 =
  let hcut = io_out_rect_Type3 h1 hterm in hcut __

(** val io_out_inv_rect_Type2 :
    io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
    'a1) -> 'a1 **)
let io_out_inv_rect_Type2 hterm h1 =
  let hcut = io_out_rect_Type2 h1 hterm in hcut __

(** val io_out_inv_rect_Type1 :
    io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
    'a1) -> 'a1 **)
let io_out_inv_rect_Type1 hterm h1 =
  let hcut = io_out_rect_Type1 h1 hterm in hcut __

(** val io_out_inv_rect_Type0 :
    io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
    'a1) -> 'a1 **)
let io_out_inv_rect_Type0 hterm h1 =
  let hcut = io_out_rect_Type0 h1 hterm in hcut __

(** val io_out_discr : io_out -> io_out -> __ **)
let io_out_discr x y =
  Logic.eq_rect_Type2 x
    (let { io_function = a0; io_args = a1; io_in_typ = a2 } = x in
    Obj.magic (fun _ dH -> dH __ __ __)) y

(** val io_out_jmdiscr : io_out -> io_out -> __ **)
let io_out_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { io_function = a0; io_args = a1; io_in_typ = a2 } = x in
    Obj.magic (fun _ dH -> dH __ __ __)) y

type io_in = eventval_type

(** val do_io :
    AST.ident -> Events.eventval List.list -> AST.typ -> (io_out, io_in,
    eventval_type) IOMonad.iO **)
let do_io fn args t =
  IOMonad.Interact ({ io_function = fn; io_args = args; io_in_typ = t },
    (fun res -> IOMonad.Value res))

(** val ret : 'a1 -> (io_out, io_in, 'a1) IOMonad.iO **)
let ret x =
  IOMonad.Value x