extracted/errors.mli

   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
  45 val errcode_rect_Type5 :
  46   (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
  47   PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1
  48
  49 val errcode_rect_Type3 :
  50   (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
  51   PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1
  52
  53 val errcode_rect_Type2 :
  54   (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
  55   PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1
  56
  57 val errcode_rect_Type1 :
  58   (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
  59   PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1
  60
  61 val errcode_rect_Type0 :
  62   (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
  63   PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1
  64
  65 val errcode_inv_rect_Type4 :
  66   errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
  67   (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1) ->
  68   'a1
  69
  70 val errcode_inv_rect_Type3 :
  71   errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
  72   (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1) ->
  73   'a1
  74
  75 val errcode_inv_rect_Type2 :
  76   errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
  77   (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1) ->
  78   'a1
  79
  80 val errcode_inv_rect_Type1 :
  81   errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
  82   (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1) ->
  83   'a1
  84
  85 val errcode_inv_rect_Type0 :
  86   errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
  87   (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1) ->
  88   'a1
  89
  90 val errcode_discr : errcode -> errcode -> __
  91
  92 val errcode_jmdiscr : errcode -> errcode -> __
  93
  94 type errmsg = errcode List.list
  95
  96 val msg : ErrorMessages.errorMessage -> errmsg
  97
  98 type 'a res =
  99 | OK of 'a
 100 | Error of errmsg
 101
 102 val res_rect_Type4 : ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2
 103
 104 val res_rect_Type5 : ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2
 105
 106 val res_rect_Type3 : ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2
 107
 108 val res_rect_Type2 : ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2
 109
 110 val res_rect_Type1 : ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2
 111
 112 val res_rect_Type0 : ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2
 113
 114 val res_inv_rect_Type4 :
 115   'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2
 116
 117 val res_inv_rect_Type3 :
 118   'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2
 119
 120 val res_inv_rect_Type2 :
 121   'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2
 122
 123 val res_inv_rect_Type1 :
 124   'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2
 125
 126 val res_inv_rect_Type0 :
 127   'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2
 128
 129 val res_discr : 'a1 res -> 'a1 res -> __
 130
 131 val res_jmdiscr : 'a1 res -> 'a1 res -> __
 132
 133 val res0 : Monad.monadProps
 134
 135 val mfold_left_i_aux :
 136   (Nat.nat -> 'a1 -> 'a2 -> 'a1 res) -> 'a1 res -> Nat.nat -> 'a2 List.list
 137   -> __
 138
 139 val mfold_left_i :
 140   (Nat.nat -> 'a1 -> 'a2 -> 'a1 res) -> 'a1 res -> 'a2 List.list -> __
 141
 142 val mfold_left2 :
 143   ('a1 -> 'a2 -> 'a3 -> 'a1 res) -> 'a1 res -> 'a2 List.list -> 'a3 List.list
 144   -> 'a1 res
 145
 146 val opt_to_res : errmsg -> 'a1 Types.option -> 'a1 res
 147
 148 val jmeq_to_eq__o__opt_eq_from_res__o__inject :
 149   errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0
 150
 151 val dpi1__o__opt_eq_from_res__o__inject :
 152   errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a2) Types.dPair -> __ Types.sig0
 153
 154 val eject__o__opt_eq_from_res__o__inject :
 155   errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __ Types.sig0
 156
 157 val opt_eq_from_res__o__inject :
 158   errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0
 159
 160 val bind_eq : 'a1 res -> ('a1 -> __ -> 'a2 res) -> 'a2 res
 161
 162 val bind2_eq :
 163   ('a1, 'a2) Types.prod res -> ('a1 -> 'a2 -> __ -> 'a3 res) -> 'a3 res
 164
 165 val res_to_opt : 'a1 res -> 'a1 Types.option
 166
 167 val bind : __ -> ('a1 -> __) -> __
 168
 169 val bind2 : __ -> ('a1 -> 'a2 -> __) -> __
 170
 171 val bind3 : __ -> ('a1 -> 'a2 -> 'a3 -> __) -> __
 172
 173 val mmap : ('a1 -> __) -> 'a1 List.list -> __
 174
 175 val mmap_sigma : ('a1 -> __) -> 'a1 List.list -> __
 176