extracted/iOMonad.mli

   1 open Preamble
   2
   3 open Div_and_mod
   4
   5 open Jmeq
   6
   7 open Russell
   8
   9 open Util
  10
  11 open Bool
  12
  13 open Relations
  14
  15 open Nat
  16
  17 open List
  18
  19 open Hints_declaration
  20
  21 open Core_notation
  22
  23 open Pts
  24
  25 open Logic
  26
  27 open Types
  28
  29 open Extralib
  30
  31 open ErrorMessages
  32
  33 open Option
  34
  35 open Setoids
  36
  37 open Monad
  38
  39 open Positive
  40
  41 open PreIdentifiers
  42
  43 open Errors
  44
  45 type ('output, 'input, 't) iO =
  46 | Interact of 'output * ('input -> ('output, 'input, 't) iO)
  47 | Value of 't
  48 | Wrong of Errors.errmsg
  49
  50 val iO_rect_Type4 :
  51   ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
  52   -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4
  53
  54 val iO_rect_Type3 :
  55   ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
  56   -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4
  57
  58 val iO_rect_Type2 :
  59   ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
  60   -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4
  61
  62 val iO_rect_Type1 :
  63   ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
  64   -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4
  65
  66 val iO_rect_Type0 :
  67   ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
  68   -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4
  69
  70 val iO_inv_rect_Type4 :
  71   ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
  72   'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
  73   'a4
  74
  75 val iO_inv_rect_Type3 :
  76   ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
  77   'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
  78   'a4
  79
  80 val iO_inv_rect_Type2 :
  81   ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
  82   'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
  83   'a4
  84
  85 val iO_inv_rect_Type1 :
  86   ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
  87   'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
  88   'a4
  89
  90 val iO_inv_rect_Type0 :
  91   ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
  92   'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
  93   'a4
  94
  95 val iO_discr : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3) iO -> __
  96
  97 val iO_jmdiscr : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3) iO -> __
  98
  99 open Proper
 100
 101 val bindIO :
 102   ('a1, 'a2, 'a3) iO -> ('a3 -> ('a1, 'a2, 'a4) iO) -> ('a1, 'a2, 'a4) iO
 103
 104 val iOMonad : Monad.monadProps
 105
 106 val bindIO2 : __ -> ('a3 -> 'a4 -> __) -> __
 107
 108 val iORel : Monad.monadRel
 109
 110 val pred_io_inject : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO
 111
 112 val iOPred : Monad.injMonadPred
 113
 114 val err_to_io : 'a3 Errors.res -> ('a1, 'a2, 'a3) iO
 115
 116 val dpi1__o__err_to_io__o__inject :
 117   ('a2 Errors.res, 'a3) Types.dPair -> ('a1, 'a4, 'a2) iO Types.sig0
 118
 119 val eject__o__err_to_io__o__inject :
 120   'a2 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0
 121
 122 val err_to_io__o__inject : 'a2 Errors.res -> ('a1, 'a3, 'a2) iO Types.sig0
 123
 124 val dpi1__o__err_to_io :
 125   ('a2 Errors.res, 'a3) Types.dPair -> ('a1, 'a4, 'a2) iO
 126
 127 val eject__o__err_to_io : 'a2 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO
 128
 129 val err_to_io_sig :
 130   'a3 Types.sig0 Errors.res -> ('a1, 'a2, 'a3 Types.sig0) iO
 131
 132 val io_inject_0 : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO
 133
 134 val io_inject :
 135   ('a1, 'a2, 'a3) iO Types.option -> ('a1, 'a2, 'a3 Types.sig0) iO
 136
 137 val io_eject : ('a1, 'a2, 'a3 Types.sig0) iO -> ('a1, 'a2, 'a3) iO
 138
 139 val dpi1__o__io_inject__o__inject :
 140   (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2
 141   Types.sig0) iO Types.sig0
 142
 143 val eject__o__io_inject__o__inject :
 144   ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2 Types.sig0) iO
 145   Types.sig0
 146
 147 val io_inject__o__inject :
 148   ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2 Types.sig0) iO Types.sig0
 149
 150 val dpi1__o__io_inject :
 151   (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2
 152   Types.sig0) iO
 153
 154 val eject__o__io_inject :
 155   ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2 Types.sig0) iO
 156
 157 val io_inject__o__io_eject__o__inject :
 158   ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2) iO Types.sig0
 159
 160 val dpi1__o__err_to_io__o__io_eject__o__inject :
 161   ('a2 Types.sig0 Errors.res, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
 162   Types.sig0
 163
 164 val dpi1__o__io_inject__o__io_eject__o__inject :
 165   (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
 166   Types.sig0
 167
 168 val eject__o__err_to_io__o__io_eject__o__inject :
 169   'a2 Types.sig0 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0
 170
 171 val eject__o__io_inject__o__io_eject__o__inject :
 172   ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0
 173
 174 val err_to_io__o__io_eject__o__inject :
 175   'a2 Types.sig0 Errors.res -> ('a1, 'a3, 'a2) iO Types.sig0
 176
 177 val dpi1__o__io_eject__o__inject :
 178   (('a1, 'a3, 'a2 Types.sig0) iO, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
 179   Types.sig0
 180
 181 val eject__o__io_eject__o__inject :
 182   ('a1, 'a3, 'a2 Types.sig0) iO Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0
 183
 184 val io_eject__o__inject :
 185   ('a1, 'a3, 'a2 Types.sig0) iO -> ('a1, 'a3, 'a2) iO Types.sig0
 186
 187 val io_inject__o__io_eject :
 188   ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2) iO
 189
 190 val dpi1__o__err_to_io__o__io_eject :
 191   ('a2 Types.sig0 Errors.res, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
 192
 193 val dpi1__o__io_inject__o__io_eject :
 194   (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
 195
 196 val eject__o__err_to_io__o__io_eject :
 197   'a2 Types.sig0 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO
 198
 199 val eject__o__io_inject__o__io_eject :
 200   ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2) iO
 201
 202 val err_to_io__o__io_eject : 'a2 Types.sig0 Errors.res -> ('a1, 'a3, 'a2) iO
 203
 204 val dpi1__o__io_eject :
 205   (('a1, 'a3, 'a2 Types.sig0) iO, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
 206
 207 val eject__o__io_eject :
 208   ('a1, 'a3, 'a2 Types.sig0) iO Types.sig0 -> ('a1, 'a3, 'a2) iO
 209
 210 val opt_to_io : Errors.errmsg -> 'a3 Types.option -> ('a1, 'a2, 'a3) iO
 211
 212 val bind_res_value :
 213   'a3 Errors.res -> ('a3 -> 'a4 Errors.res) -> 'a4 -> ('a3 -> __ -> __ ->
 214   'a5) -> 'a5
 215
 216 val bindIO_value :
 217   ('a1, 'a2, 'a3) iO -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a4 -> ('a3 -> __ ->
 218   __ -> 'a5) -> 'a5
 219
 220 val bindIO_res_interact :
 221   'a3 Errors.res -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1 -> ('a2 -> ('a1, 'a2,
 222   'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5
 223
 224 val bindIO_opt_interact :
 225   Errors.errmsg -> 'a3 Types.option -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1 ->
 226   ('a2 -> ('a1, 'a2, 'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5
 227
 228 val eq_to_rel_io__o__io_eq_from_res__o__inject :
 229   'a2 Errors.res -> 'a2 -> __ Types.sig0
 230
 231 val eq_to_rel_io__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
 232   Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0
 233
 234 val jmeq_to_eq__o__io_eq_from_res__o__inject :
 235   'a2 Errors.res -> 'a2 -> __ Types.sig0
 236
 237 val jmeq_to_eq__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
 238   Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0
 239
 240 val dpi1__o__io_eq_from_res__o__inject :
 241   'a2 Errors.res -> 'a2 -> (__, 'a4) Types.dPair -> __ Types.sig0
 242
 243 val dpi1__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
 244   Errors.errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a4) Types.dPair -> __
 245   Types.sig0
 246
 247 val eject__o__io_eq_from_res__o__inject :
 248   'a2 Errors.res -> 'a2 -> __ Types.sig0 -> __ Types.sig0
 249
 250 val eject__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
 251   Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __ Types.sig0
 252
 253 val io_eq_from_res__o__opt_eq_from_res__o__inject :
 254   Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0
 255
 256 val io_eq_from_res__o__inject : 'a2 Errors.res -> 'a2 -> __ Types.sig0
 257
 258 val jmeq_to_eq__o__io_monad_eq_from_res__o__inject :
 259   'a2 Errors.res -> 'a2 -> __ Types.sig0
 260
 261 val jmeq_to_eq__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
 262   Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0
 263
 264 val dpi1__o__io_monad_eq_from_res__o__inject :
 265   'a2 Errors.res -> 'a2 -> (__, 'a4) Types.dPair -> __ Types.sig0
 266
 267 val dpi1__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
 268   Errors.errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a4) Types.dPair -> __
 269   Types.sig0
 270
 271 val eject__o__io_monad_eq_from_res__o__inject :
 272   'a2 Errors.res -> 'a2 -> __ Types.sig0 -> __ Types.sig0
 273
 274 val eject__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
 275   Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __ Types.sig0
 276
 277 val io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
 278   Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0
 279
 280 val io_monad_eq_from_res__o__inject : 'a2 Errors.res -> 'a2 -> __ Types.sig0
 281
 282 val eq_to_rel_io__o__io_eq_from_opt__o__inject :
 283   Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0
 284
 285 val jmeq_to_eq__o__io_eq_from_opt__o__inject :
 286   Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0
 287
 288 val dpi1__o__io_eq_from_opt__o__inject :
 289   Errors.errmsg -> 'a2 Types.option -> 'a2 -> (__, 'a4) Types.dPair -> __
 290   Types.sig0
 291
 292 val eject__o__io_eq_from_opt__o__inject :
 293   Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 -> __ Types.sig0
 294
 295 val io_eq_from_opt__o__inject :
 296   Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0
 297
 298 val jmeq_to_eq__o__io_monad_eq_from_opt__o__inject :
 299   Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0
 300
 301 val dpi1__o__io_monad_eq_from_opt__o__inject :
 302   Errors.errmsg -> 'a2 Types.option -> 'a2 -> (__, 'a4) Types.dPair -> __
 303   Types.sig0
 304
 305 val eject__o__io_monad_eq_from_opt__o__inject :
 306   Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 -> __ Types.sig0
 307
 308 val io_monad_eq_from_opt__o__inject :
 309   Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0
 310