extracted/extraMonads.ml

   1 open Preamble
   2
   3 open ErrorMessages
   4
   5 open Option
   6
   7 open Setoids
   8
   9 open Monad
  10
  11 open Jmeq
  12
  13 open Russell
  14
  15 open Positive
  16
  17 open PreIdentifiers
  18
  19 open Bool
  20
  21 open Relations
  22
  23 open Nat
  24
  25 open List
  26
  27 open Hints_declaration
  28
  29 open Core_notation
  30
  31 open Pts
  32
  33 open Logic
  34
  35 open Types
  36
  37 open Errors
  38
  39 open Proper
  40
  41 open Div_and_mod
  42
  43 open Util
  44
  45 open Extralib
  46
  47 open IOMonad
  48
  49 type monadFunctRel =
  50 | Mk_MonadFunctRel
  51
  52 (** val monadFunctRel_rect_Type4 :
  53     Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
  54     monadFunctRel -> 'a1 **)
  55 let rec monadFunctRel_rect_Type4 m1 m2 h_mk_MonadFunctRel = function
  56 | Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
  57
  58 (** val monadFunctRel_rect_Type5 :
  59     Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
  60     monadFunctRel -> 'a1 **)
  61 let rec monadFunctRel_rect_Type5 m1 m2 h_mk_MonadFunctRel = function
  62 | Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
  63
  64 (** val monadFunctRel_rect_Type3 :
  65     Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
  66     monadFunctRel -> 'a1 **)
  67 let rec monadFunctRel_rect_Type3 m1 m2 h_mk_MonadFunctRel = function
  68 | Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
  69
  70 (** val monadFunctRel_rect_Type2 :
  71     Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
  72     monadFunctRel -> 'a1 **)
  73 let rec monadFunctRel_rect_Type2 m1 m2 h_mk_MonadFunctRel = function
  74 | Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
  75
  76 (** val monadFunctRel_rect_Type1 :
  77     Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
  78     monadFunctRel -> 'a1 **)
  79 let rec monadFunctRel_rect_Type1 m1 m2 h_mk_MonadFunctRel = function
  80 | Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
  81
  82 (** val monadFunctRel_rect_Type0 :
  83     Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> 'a1) ->
  84     monadFunctRel -> 'a1 **)
  85 let rec monadFunctRel_rect_Type0 m1 m2 h_mk_MonadFunctRel = function
  86 | Mk_MonadFunctRel -> h_mk_MonadFunctRel __ __ __ __
  87
  88 (** val monadFunctRel_inv_rect_Type4 :
  89     Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
  90     __ -> 'a1) -> 'a1 **)
  91 let monadFunctRel_inv_rect_Type4 x1 x2 hterm h1 =
  92   let hcut = monadFunctRel_rect_Type4 x1 x2 h1 hterm in hcut __
  93
  94 (** val monadFunctRel_inv_rect_Type3 :
  95     Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
  96     __ -> 'a1) -> 'a1 **)
  97 let monadFunctRel_inv_rect_Type3 x1 x2 hterm h1 =
  98   let hcut = monadFunctRel_rect_Type3 x1 x2 h1 hterm in hcut __
  99
 100 (** val monadFunctRel_inv_rect_Type2 :
 101     Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
 102     __ -> 'a1) -> 'a1 **)
 103 let monadFunctRel_inv_rect_Type2 x1 x2 hterm h1 =
 104   let hcut = monadFunctRel_rect_Type2 x1 x2 h1 hterm in hcut __
 105
 106 (** val monadFunctRel_inv_rect_Type1 :
 107     Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
 108     __ -> 'a1) -> 'a1 **)
 109 let monadFunctRel_inv_rect_Type1 x1 x2 hterm h1 =
 110   let hcut = monadFunctRel_rect_Type1 x1 x2 h1 hterm in hcut __
 111
 112 (** val monadFunctRel_inv_rect_Type0 :
 113     Monad.monad -> Monad.monad -> monadFunctRel -> (__ -> __ -> __ -> __ ->
 114     __ -> 'a1) -> 'a1 **)
 115 let monadFunctRel_inv_rect_Type0 x1 x2 hterm h1 =
 116   let hcut = monadFunctRel_rect_Type0 x1 x2 h1 hterm in hcut __
 117
 118 (** val monadFunctRel_jmdiscr :
 119     Monad.monad -> Monad.monad -> monadFunctRel -> monadFunctRel -> __ **)
 120 let monadFunctRel_jmdiscr a1 a2 x y =
 121   Logic.eq_rect_Type2 x
 122     (let Mk_MonadFunctRel = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
 123
 124 type monadFunctRel1 =
 125 | Mk_MonadFunctRel1
 126
 127 (** val monadFunctRel1_rect_Type4 :
 128     Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
 129     monadFunctRel1 -> 'a1 **)
 130 let rec monadFunctRel1_rect_Type4 m1 m2 h_mk_MonadFunctRel1 = function
 131 | Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
 132
 133 (** val monadFunctRel1_rect_Type5 :
 134     Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
 135     monadFunctRel1 -> 'a1 **)
 136 let rec monadFunctRel1_rect_Type5 m1 m2 h_mk_MonadFunctRel1 = function
 137 | Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
 138
 139 (** val monadFunctRel1_rect_Type3 :
 140     Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
 141     monadFunctRel1 -> 'a1 **)
 142 let rec monadFunctRel1_rect_Type3 m1 m2 h_mk_MonadFunctRel1 = function
 143 | Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
 144
 145 (** val monadFunctRel1_rect_Type2 :
 146     Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
 147     monadFunctRel1 -> 'a1 **)
 148 let rec monadFunctRel1_rect_Type2 m1 m2 h_mk_MonadFunctRel1 = function
 149 | Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
 150
 151 (** val monadFunctRel1_rect_Type1 :
 152     Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
 153     monadFunctRel1 -> 'a1 **)
 154 let rec monadFunctRel1_rect_Type1 m1 m2 h_mk_MonadFunctRel1 = function
 155 | Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
 156
 157 (** val monadFunctRel1_rect_Type0 :
 158     Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
 159     monadFunctRel1 -> 'a1 **)
 160 let rec monadFunctRel1_rect_Type0 m1 m2 h_mk_MonadFunctRel1 = function
 161 | Mk_MonadFunctRel1 -> h_mk_MonadFunctRel1 __ __ __ __ __
 162
 163 (** val monadFunctRel1_inv_rect_Type4 :
 164     Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
 165     __ -> __ -> 'a1) -> 'a1 **)
 166 let monadFunctRel1_inv_rect_Type4 x1 x2 hterm h1 =
 167   let hcut = monadFunctRel1_rect_Type4 x1 x2 h1 hterm in hcut __
 168
 169 (** val monadFunctRel1_inv_rect_Type3 :
 170     Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
 171     __ -> __ -> 'a1) -> 'a1 **)
 172 let monadFunctRel1_inv_rect_Type3 x1 x2 hterm h1 =
 173   let hcut = monadFunctRel1_rect_Type3 x1 x2 h1 hterm in hcut __
 174
 175 (** val monadFunctRel1_inv_rect_Type2 :
 176     Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
 177     __ -> __ -> 'a1) -> 'a1 **)
 178 let monadFunctRel1_inv_rect_Type2 x1 x2 hterm h1 =
 179   let hcut = monadFunctRel1_rect_Type2 x1 x2 h1 hterm in hcut __
 180
 181 (** val monadFunctRel1_inv_rect_Type1 :
 182     Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
 183     __ -> __ -> 'a1) -> 'a1 **)
 184 let monadFunctRel1_inv_rect_Type1 x1 x2 hterm h1 =
 185   let hcut = monadFunctRel1_rect_Type1 x1 x2 h1 hterm in hcut __
 186
 187 (** val monadFunctRel1_inv_rect_Type0 :
 188     Monad.monad -> Monad.monad -> monadFunctRel1 -> (__ -> __ -> __ -> __ ->
 189     __ -> __ -> 'a1) -> 'a1 **)
 190 let monadFunctRel1_inv_rect_Type0 x1 x2 hterm h1 =
 191   let hcut = monadFunctRel1_rect_Type0 x1 x2 h1 hterm in hcut __
 192
 193 (** val monadFunctRel1_jmdiscr :
 194     Monad.monad -> Monad.monad -> monadFunctRel1 -> monadFunctRel1 -> __ **)
 195 let monadFunctRel1_jmdiscr a1 a2 x y =
 196   Logic.eq_rect_Type2 x
 197     (let Mk_MonadFunctRel1 = x in Obj.magic (fun _ dH -> dH __ __ __ __ __))
 198     y
 199
 200 type monadGenRel =
 201 | Mk_MonadGenRel
 202
 203 (** val monadGenRel_rect_Type4 :
 204     Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
 205     monadGenRel -> 'a1 **)
 206 let rec monadGenRel_rect_Type4 m1 m2 h_mk_MonadGenRel = function
 207 | Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __
 208
 209 (** val monadGenRel_rect_Type5 :
 210     Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
 211     monadGenRel -> 'a1 **)
 212 let rec monadGenRel_rect_Type5 m1 m2 h_mk_MonadGenRel = function
 213 | Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __
 214
 215 (** val monadGenRel_rect_Type3 :
 216     Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
 217     monadGenRel -> 'a1 **)
 218 let rec monadGenRel_rect_Type3 m1 m2 h_mk_MonadGenRel = function
 219 | Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __
 220
 221 (** val monadGenRel_rect_Type2 :
 222     Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
 223     monadGenRel -> 'a1 **)
 224 let rec monadGenRel_rect_Type2 m1 m2 h_mk_MonadGenRel = function
 225 | Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __
 226
 227 (** val monadGenRel_rect_Type1 :
 228     Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
 229     monadGenRel -> 'a1 **)
 230 let rec monadGenRel_rect_Type1 m1 m2 h_mk_MonadGenRel = function
 231 | Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __
 232
 233 (** val monadGenRel_rect_Type0 :
 234     Monad.monad -> Monad.monad -> (__ -> __ -> __ -> __ -> __ -> 'a1) ->
 235     monadGenRel -> 'a1 **)
 236 let rec monadGenRel_rect_Type0 m1 m2 h_mk_MonadGenRel = function
 237 | Mk_MonadGenRel -> h_mk_MonadGenRel __ __ __ __ __
 238
 239 (** val monadGenRel_inv_rect_Type4 :
 240     Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __
 241     -> __ -> 'a1) -> 'a1 **)
 242 let monadGenRel_inv_rect_Type4 x1 x2 hterm h1 =
 243   let hcut = monadGenRel_rect_Type4 x1 x2 h1 hterm in hcut __
 244
 245 (** val monadGenRel_inv_rect_Type3 :
 246     Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __
 247     -> __ -> 'a1) -> 'a1 **)
 248 let monadGenRel_inv_rect_Type3 x1 x2 hterm h1 =
 249   let hcut = monadGenRel_rect_Type3 x1 x2 h1 hterm in hcut __
 250
 251 (** val monadGenRel_inv_rect_Type2 :
 252     Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __
 253     -> __ -> 'a1) -> 'a1 **)
 254 let monadGenRel_inv_rect_Type2 x1 x2 hterm h1 =
 255   let hcut = monadGenRel_rect_Type2 x1 x2 h1 hterm in hcut __
 256
 257 (** val monadGenRel_inv_rect_Type1 :
 258     Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __
 259     -> __ -> 'a1) -> 'a1 **)
 260 let monadGenRel_inv_rect_Type1 x1 x2 hterm h1 =
 261   let hcut = monadGenRel_rect_Type1 x1 x2 h1 hterm in hcut __
 262
 263 (** val monadGenRel_inv_rect_Type0 :
 264     Monad.monad -> Monad.monad -> monadGenRel -> (__ -> __ -> __ -> __ -> __
 265     -> __ -> 'a1) -> 'a1 **)
 266 let monadGenRel_inv_rect_Type0 x1 x2 hterm h1 =
 267   let hcut = monadGenRel_rect_Type0 x1 x2 h1 hterm in hcut __
 268
 269 (** val monadGenRel_jmdiscr :
 270     Monad.monad -> Monad.monad -> monadGenRel -> monadGenRel -> __ **)
 271 let monadGenRel_jmdiscr a1 a2 x y =
 272   Logic.eq_rect_Type2 x
 273     (let Mk_MonadGenRel = x in Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
 274
 275 (** val res_preserve : monadFunctRel **)
 276 let res_preserve =
 277   Mk_MonadFunctRel
 278
 279 (** val res_preserve1 : monadFunctRel1 **)
 280 let res_preserve1 =
 281   Mk_MonadFunctRel1
 282
 283 (** val gen_res_preserve : monadGenRel **)
 284 let gen_res_preserve =
 285   Mk_MonadGenRel
 286
 287 (** val opt_preserve : monadFunctRel **)
 288 let opt_preserve =
 289   Mk_MonadFunctRel
 290
 291 (** val opt_preserve1 : monadFunctRel1 **)
 292 let opt_preserve1 =
 293   Mk_MonadFunctRel1
 294
 295 (** val gen_opt_preserve : monadGenRel **)
 296 let gen_opt_preserve =
 297   Mk_MonadGenRel
 298
 299 (** val io_preserve : monadFunctRel **)
 300 let io_preserve =
 301   Mk_MonadFunctRel
 302
 303 (** val io_preserve1 : monadFunctRel1 **)
 304 let io_preserve1 =
 305   Mk_MonadFunctRel1
 306
 307 (** val gen_io_preserve : monadGenRel **)
 308 let gen_io_preserve =
 309   Mk_MonadGenRel
 310