extracted/iO.mli

   1 open Preamble
   2
   3 open Proper
   4
   5 open ErrorMessages
   6
   7 open Option
   8
   9 open Setoids
  10
  11 open Monad
  12
  13 open Positive
  14
  15 open PreIdentifiers
  16
  17 open Errors
  18
  19 open Div_and_mod
  20
  21 open Jmeq
  22
  23 open Russell
  24
  25 open Util
  26
  27 open Bool
  28
  29 open Relations
  30
  31 open Nat
  32
  33 open List
  34
  35 open Hints_declaration
  36
  37 open Core_notation
  38
  39 open Pts
  40
  41 open Logic
  42
  43 open Types
  44
  45 open Extralib
  46
  47 open IOMonad
  48
  49 open CostLabel
  50
  51 open PositiveMap
  52
  53 open Deqsets
  54
  55 open Lists
  56
  57 open Identifiers
  58
  59 open Integers
  60
  61 open AST
  62
  63 open Division
  64
  65 open Exp
  66
  67 open Arithmetic
  68
  69 open Extranat
  70
  71 open Vector
  72
  73 open FoldStuff
  74
  75 open BitVector
  76
  77 open Z
  78
  79 open BitVectorZ
  80
  81 open Pointers
  82
  83 open Coqlib
  84
  85 open Values
  86
  87 open Events
  88
  89 type eventval_type = __
  90
  91 val mk_eventval : AST.typ -> eventval_type -> Events.eventval
  92
  93 val mk_val : AST.typ -> eventval_type -> Values.val0
  94
  95 val convert_eventval : Events.eventval -> AST.typ -> Values.val0 Errors.res
  96
  97 val check_eventval' : Values.val0 -> AST.typ -> Events.eventval Errors.res
  98
  99 val check_eventval_list :
 100   Values.val0 List.list -> AST.typ List.list -> Events.eventval List.list
 101   Errors.res
 102
 103 type io_out = { io_function : AST.ident; io_args : Events.eventval List.list;
 104                 io_in_typ : AST.typ }
 105
 106 val io_out_rect_Type4 :
 107   (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
 108
 109 val io_out_rect_Type5 :
 110   (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
 111
 112 val io_out_rect_Type3 :
 113   (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
 114
 115 val io_out_rect_Type2 :
 116   (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
 117
 118 val io_out_rect_Type1 :
 119   (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
 120
 121 val io_out_rect_Type0 :
 122   (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
 123
 124 val io_function : io_out -> AST.ident
 125
 126 val io_args : io_out -> Events.eventval List.list
 127
 128 val io_in_typ : io_out -> AST.typ
 129
 130 val io_out_inv_rect_Type4 :
 131   io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
 132   -> 'a1
 133
 134 val io_out_inv_rect_Type3 :
 135   io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
 136   -> 'a1
 137
 138 val io_out_inv_rect_Type2 :
 139   io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
 140   -> 'a1
 141
 142 val io_out_inv_rect_Type1 :
 143   io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
 144   -> 'a1
 145
 146 val io_out_inv_rect_Type0 :
 147   io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
 148   -> 'a1
 149
 150 val io_out_discr : io_out -> io_out -> __
 151
 152 val io_out_jmdiscr : io_out -> io_out -> __
 153
 154 type io_in = eventval_type
 155
 156 val do_io :
 157   AST.ident -> Events.eventval List.list -> AST.typ -> (io_out, io_in,
 158   eventval_type) IOMonad.iO
 159
 160 val ret : 'a1 -> (io_out, io_in, 'a1) IOMonad.iO
 161