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

val mk_val : AST.typ -> eventval_type -> Values.val0

val convert_eventval : Events.eventval -> AST.typ -> Values.val0 Errors.res

val check_eventval' : Values.val0 -> AST.typ -> Events.eventval Errors.res

val check_eventval_list :
  Values.val0 List.list -> AST.typ List.list -> Events.eventval List.list
  Errors.res

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

val io_out_rect_Type5 :
  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1

val io_out_rect_Type3 :
  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1

val io_out_rect_Type2 :
  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1

val io_out_rect_Type1 :
  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1

val io_out_rect_Type0 :
  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1

val io_function : io_out -> AST.ident

val io_args : io_out -> Events.eventval List.list

val io_in_typ : io_out -> AST.typ

val io_out_inv_rect_Type4 :
  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
  -> 'a1

val io_out_inv_rect_Type3 :
  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
  -> 'a1

val io_out_inv_rect_Type2 :
  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
  -> 'a1

val io_out_inv_rect_Type1 :
  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
  -> 'a1

val io_out_inv_rect_Type0 :
  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
  -> 'a1

val io_out_discr : io_out -> io_out -> __

val io_out_jmdiscr : io_out -> io_out -> __

type io_in = eventval_type

val do_io :
  AST.ident -> Events.eventval List.list -> AST.typ -> (io_out, io_in,
  eventval_type) IOMonad.iO

val ret : 'a1 -> (io_out, io_in, 'a1) IOMonad.iO