extracted/errors.ml

   1 open Preamble
   2
   3 open Hints_declaration
   4
   5 open Core_notation
   6
   7 open Pts
   8
   9 open Logic
  10
  11 open Types
  12
  13 open Bool
  14
  15 open Relations
  16
  17 open Nat
  18
  19 open List
  20
  21 open Positive
  22
  23 open PreIdentifiers
  24
  25 open Jmeq
  26
  27 open Russell
  28
  29 open Setoids
  30
  31 open Monad
  32
  33 open Option
  34
  35 open ErrorMessages
  36
  37 type errcode =
  38 | MSG of ErrorMessages.errorMessage
  39 | CTX of PreIdentifiers.identifierTag * PreIdentifiers.identifier
  40
  41 (** val errcode_rect_Type4 :
  42     (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
  43     PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
  44 let rec errcode_rect_Type4 h_MSG h_CTX = function
  45 | MSG x_3113 -> h_MSG x_3113
  46 | CTX (tag, x_3114) -> h_CTX tag x_3114
  47
  48 (** val errcode_rect_Type5 :
  49     (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
  50     PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
  51 let rec errcode_rect_Type5 h_MSG h_CTX = function
  52 | MSG x_3118 -> h_MSG x_3118
  53 | CTX (tag, x_3119) -> h_CTX tag x_3119
  54
  55 (** val errcode_rect_Type3 :
  56     (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
  57     PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
  58 let rec errcode_rect_Type3 h_MSG h_CTX = function
  59 | MSG x_3123 -> h_MSG x_3123
  60 | CTX (tag, x_3124) -> h_CTX tag x_3124
  61
  62 (** val errcode_rect_Type2 :
  63     (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
  64     PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
  65 let rec errcode_rect_Type2 h_MSG h_CTX = function
  66 | MSG x_3128 -> h_MSG x_3128
  67 | CTX (tag, x_3129) -> h_CTX tag x_3129
  68
  69 (** val errcode_rect_Type1 :
  70     (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
  71     PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
  72 let rec errcode_rect_Type1 h_MSG h_CTX = function
  73 | MSG x_3133 -> h_MSG x_3133
  74 | CTX (tag, x_3134) -> h_CTX tag x_3134
  75
  76 (** val errcode_rect_Type0 :
  77     (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
  78     PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
  79 let rec errcode_rect_Type0 h_MSG h_CTX = function
  80 | MSG x_3138 -> h_MSG x_3138
  81 | CTX (tag, x_3139) -> h_CTX tag x_3139
  82
  83 (** val errcode_inv_rect_Type4 :
  84     errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
  85     (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
  86     -> 'a1 **)
  87 let errcode_inv_rect_Type4 hterm h1 h2 =
  88   let hcut = errcode_rect_Type4 h1 h2 hterm in hcut __
  89
  90 (** val errcode_inv_rect_Type3 :
  91     errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
  92     (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
  93     -> 'a1 **)
  94 let errcode_inv_rect_Type3 hterm h1 h2 =
  95   let hcut = errcode_rect_Type3 h1 h2 hterm in hcut __
  96
  97 (** val errcode_inv_rect_Type2 :
  98     errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
  99     (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
 100     -> 'a1 **)
 101 let errcode_inv_rect_Type2 hterm h1 h2 =
 102   let hcut = errcode_rect_Type2 h1 h2 hterm in hcut __
 103
 104 (** val errcode_inv_rect_Type1 :
 105     errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
 106     (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
 107     -> 'a1 **)
 108 let errcode_inv_rect_Type1 hterm h1 h2 =
 109   let hcut = errcode_rect_Type1 h1 h2 hterm in hcut __
 110
 111 (** val errcode_inv_rect_Type0 :
 112     errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
 113     (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
 114     -> 'a1 **)
 115 let errcode_inv_rect_Type0 hterm h1 h2 =
 116   let hcut = errcode_rect_Type0 h1 h2 hterm in hcut __
 117
 118 (** val errcode_discr : errcode -> errcode -> __ **)
 119 let errcode_discr x y =
 120   Logic.eq_rect_Type2 x
 121     (match x with
 122      | MSG a0 -> Obj.magic (fun _ dH -> dH __)
 123      | CTX (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
 124
 125 (** val errcode_jmdiscr : errcode -> errcode -> __ **)
 126 let errcode_jmdiscr x y =
 127   Logic.eq_rect_Type2 x
 128     (match x with
 129      | MSG a0 -> Obj.magic (fun _ dH -> dH __)
 130      | CTX (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
 131
 132 type errmsg = errcode List.list
 133
 134 (** val msg : ErrorMessages.errorMessage -> errmsg **)
 135 let msg s =
 136   List.Cons ((MSG s), List.Nil)
 137
 138 type 'a res =
 139 | OK of 'a
 140 | Error of errmsg
 141
 142 (** val res_rect_Type4 :
 143     ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
 144 let rec res_rect_Type4 h_OK h_Error = function
 145 | OK x_3178 -> h_OK x_3178
 146 | Error x_3179 -> h_Error x_3179
 147
 148 (** val res_rect_Type5 :
 149     ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
 150 let rec res_rect_Type5 h_OK h_Error = function
 151 | OK x_3183 -> h_OK x_3183
 152 | Error x_3184 -> h_Error x_3184
 153
 154 (** val res_rect_Type3 :
 155     ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
 156 let rec res_rect_Type3 h_OK h_Error = function
 157 | OK x_3188 -> h_OK x_3188
 158 | Error x_3189 -> h_Error x_3189
 159
 160 (** val res_rect_Type2 :
 161     ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
 162 let rec res_rect_Type2 h_OK h_Error = function
 163 | OK x_3193 -> h_OK x_3193
 164 | Error x_3194 -> h_Error x_3194
 165
 166 (** val res_rect_Type1 :
 167     ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
 168 let rec res_rect_Type1 h_OK h_Error = function
 169 | OK x_3198 -> h_OK x_3198
 170 | Error x_3199 -> h_Error x_3199
 171
 172 (** val res_rect_Type0 :
 173     ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
 174 let rec res_rect_Type0 h_OK h_Error = function
 175 | OK x_3203 -> h_OK x_3203
 176 | Error x_3204 -> h_Error x_3204
 177
 178 (** val res_inv_rect_Type4 :
 179     'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
 180 let res_inv_rect_Type4 hterm h1 h2 =
 181   let hcut = res_rect_Type4 h1 h2 hterm in hcut __
 182
 183 (** val res_inv_rect_Type3 :
 184     'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
 185 let res_inv_rect_Type3 hterm h1 h2 =
 186   let hcut = res_rect_Type3 h1 h2 hterm in hcut __
 187
 188 (** val res_inv_rect_Type2 :
 189     'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
 190 let res_inv_rect_Type2 hterm h1 h2 =
 191   let hcut = res_rect_Type2 h1 h2 hterm in hcut __
 192
 193 (** val res_inv_rect_Type1 :
 194     'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
 195 let res_inv_rect_Type1 hterm h1 h2 =
 196   let hcut = res_rect_Type1 h1 h2 hterm in hcut __
 197
 198 (** val res_inv_rect_Type0 :
 199     'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
 200 let res_inv_rect_Type0 hterm h1 h2 =
 201   let hcut = res_rect_Type0 h1 h2 hterm in hcut __
 202
 203 (** val res_discr : 'a1 res -> 'a1 res -> __ **)
 204 let res_discr x y =
 205   Logic.eq_rect_Type2 x
 206     (match x with
 207      | OK a0 -> Obj.magic (fun _ dH -> dH __)
 208      | Error a0 -> Obj.magic (fun _ dH -> dH __)) y
 209
 210 (** val res_jmdiscr : 'a1 res -> 'a1 res -> __ **)
 211 let res_jmdiscr x y =
 212   Logic.eq_rect_Type2 x
 213     (match x with
 214      | OK a0 -> Obj.magic (fun _ dH -> dH __)
 215      | Error a0 -> Obj.magic (fun _ dH -> dH __)) y
 216
 217 (** val res0 : Monad.monadProps **)
 218 let res0 =
 219   Monad.makeMonadProps (fun _ x -> OK x) (fun _ _ m f ->
 220     match m with
 221     | OK x -> f x
 222     | Error msg0 -> Error msg0)
 223
 224 (** val mfold_left_i_aux :
 225     (Nat.nat -> 'a1 -> 'a2 -> 'a1 res) -> 'a1 res -> Nat.nat -> 'a2 List.list
 226     -> __ **)
 227 let rec mfold_left_i_aux f x i = function
 228 | List.Nil -> Obj.magic x
 229 | List.Cons (hd, tl) ->
 230   Monad.m_bind0 (Monad.max_def res0) (Obj.magic x) (fun x0 ->
 231     mfold_left_i_aux f (f i x0 hd) (Nat.S i) tl)
 232
 233 (** val mfold_left_i :
 234     (Nat.nat -> 'a1 -> 'a2 -> 'a1 res) -> 'a1 res -> 'a2 List.list -> __ **)
 235 let mfold_left_i f x =
 236   mfold_left_i_aux f x Nat.O
 237
 238 (** val mfold_left2 :
 239     ('a1 -> 'a2 -> 'a3 -> 'a1 res) -> 'a1 res -> 'a2 List.list -> 'a3
 240     List.list -> 'a1 res **)
 241 let rec mfold_left2 f accu left right =
 242   match left with
 243   | List.Nil ->
 244     (match right with
 245      | List.Nil -> accu
 246      | List.Cons (hd, tl) -> Error (msg ErrorMessages.WrongLength))
 247   | List.Cons (hd, tl) ->
 248     (match right with
 249      | List.Nil -> Error (msg ErrorMessages.WrongLength)
 250      | List.Cons (hd', tl') ->
 251        Obj.magic
 252          (Monad.m_bind0 (Monad.max_def res0) (Obj.magic accu) (fun accu0 ->
 253            Obj.magic (mfold_left2 f (f accu0 hd hd') tl tl'))))
 254
 255 (** val opt_to_res : errmsg -> 'a1 Types.option -> 'a1 res **)
 256 let opt_to_res msg0 = function
 257 | Types.None -> Error msg0
 258 | Types.Some v0 -> OK v0
 259
 260 (** val jmeq_to_eq__o__opt_eq_from_res__o__inject :
 261     errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
 262 let jmeq_to_eq__o__opt_eq_from_res__o__inject x1 x2 x3 =
 263   __
 264
 265 (** val dpi1__o__opt_eq_from_res__o__inject :
 266     errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a2) Types.dPair -> __
 267     Types.sig0 **)
 268 let dpi1__o__opt_eq_from_res__o__inject x1 x2 x3 x6 =
 269   __
 270
 271 (** val eject__o__opt_eq_from_res__o__inject :
 272     errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __ Types.sig0 **)
 273 let eject__o__opt_eq_from_res__o__inject x1 x2 x3 x6 =
 274   __
 275
 276 (** val opt_eq_from_res__o__inject :
 277     errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
 278 let opt_eq_from_res__o__inject x1 x2 x3 =
 279   __
 280
 281 (** val bind_eq : 'a1 res -> ('a1 -> __ -> 'a2 res) -> 'a2 res **)
 282 let bind_eq f g =
 283   (match f with
 284    | OK x -> g x
 285    | Error msg0 -> (fun _ -> Error msg0)) __
 286
 287 (** val bind2_eq :
 288     ('a1, 'a2) Types.prod res -> ('a1 -> 'a2 -> __ -> 'a3 res) -> 'a3 res **)
 289 let bind2_eq f g =
 290   (match f with
 291    | OK x -> let { Types.fst = a; Types.snd = b } = x in g a b
 292    | Error msg0 -> (fun _ -> Error msg0)) __
 293
 294 (** val res_to_opt : 'a1 res -> 'a1 Types.option **)
 295 let res_to_opt = function
 296 | OK v0 -> Types.Some v0
 297 | Error x -> Types.None
 298
 299 (** val bind : __ -> ('a1 -> __) -> __ **)
 300 let bind x_768 x_769 =
 301   Monad.m_bind0 (Monad.max_def res0) x_768 x_769
 302
 303 (** val bind2 : __ -> ('a1 -> 'a2 -> __) -> __ **)
 304 let bind2 m f =
 305   Monad.m_bind2 (Monad.max_def res0) m f
 306
 307 (** val bind3 : __ -> ('a1 -> 'a2 -> 'a3 -> __) -> __ **)
 308 let bind3 x x0 =
 309   Monad.m_bind3 (Monad.max_def res0) x x0
 310
 311 (** val mmap : ('a1 -> __) -> 'a1 List.list -> __ **)
 312 let mmap x x0 =
 313   Monad.m_list_map (Monad.max_def res0) x x0
 314
 315 (** val mmap_sigma : ('a1 -> __) -> 'a1 List.list -> __ **)
 316 let mmap_sigma x x0 =
 317   Monad.m_list_map_sigma (Monad.max_def res0) x x0
 318