extracted/identifiers.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 Positive
  20
  21 open Setoids
  22
  23 open Monad
  24
  25 open Option
  26
  27 open Div_and_mod
  28
  29 open Jmeq
  30
  31 open Russell
  32
  33 open Util
  34
  35 open List
  36
  37 open Lists
  38
  39 open Extralib
  40
  41 open ErrorMessages
  42
  43 open PreIdentifiers
  44
  45 open Errors
  46
  47 type universe =
  48   Positive.pos
  49   (* singleton inductive, whose constructor was mk_universe *)
  50
  51 val universe_rect_Type4 :
  52   PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
  53
  54 val universe_rect_Type5 :
  55   PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
  56
  57 val universe_rect_Type3 :
  58   PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
  59
  60 val universe_rect_Type2 :
  61   PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
  62
  63 val universe_rect_Type1 :
  64   PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
  65
  66 val universe_rect_Type0 :
  67   PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
  68
  69 val next_identifier :
  70   PreIdentifiers.identifierTag -> universe -> Positive.pos
  71
  72 val universe_inv_rect_Type4 :
  73   PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
  74   'a1
  75
  76 val universe_inv_rect_Type3 :
  77   PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
  78   'a1
  79
  80 val universe_inv_rect_Type2 :
  81   PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
  82   'a1
  83
  84 val universe_inv_rect_Type1 :
  85   PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
  86   'a1
  87
  88 val universe_inv_rect_Type0 :
  89   PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
  90   'a1
  91
  92 val universe_discr :
  93   PreIdentifiers.identifierTag -> universe -> universe -> __
  94
  95 val universe_jmdiscr :
  96   PreIdentifiers.identifierTag -> universe -> universe -> __
  97
  98 val new_universe : PreIdentifiers.identifierTag -> universe
  99
 100 val fresh :
 101   PreIdentifiers.identifierTag -> universe -> (PreIdentifiers.identifier,
 102   universe) Types.prod
 103
 104 val eq_identifier :
 105   PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
 106   PreIdentifiers.identifier -> Bool.bool
 107
 108 val eq_identifier_elim :
 109   PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
 110   PreIdentifiers.identifier -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 111
 112 open Deqsets
 113
 114 val deq_identifier : PreIdentifiers.identifierTag -> Deqsets.deqSet
 115
 116 val word_of_identifier :
 117   PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> Positive.pos
 118
 119 val identifier_eq :
 120   PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
 121   PreIdentifiers.identifier -> (__, __) Types.sum
 122
 123 val identifier_of_nat :
 124   PreIdentifiers.identifierTag -> Nat.nat -> PreIdentifiers.identifier
 125
 126 val check_member_env :
 127   PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
 128   (PreIdentifiers.identifier, 'a1) Types.prod List.list -> __ Errors.res
 129
 130 val check_distinct_env :
 131   PreIdentifiers.identifierTag -> (PreIdentifiers.identifier, 'a1) Types.prod
 132   List.list -> __ Errors.res
 133
 134 open PositiveMap
 135
 136 type 'a identifier_map =
 137   'a PositiveMap.positive_map
 138   (* singleton inductive, whose constructor was an_id_map *)
 139
 140 val identifier_map_rect_Type4 :
 141   PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
 142   'a1 identifier_map -> 'a2
 143
 144 val identifier_map_rect_Type5 :
 145   PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
 146   'a1 identifier_map -> 'a2
 147
 148 val identifier_map_rect_Type3 :
 149   PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
 150   'a1 identifier_map -> 'a2
 151
 152 val identifier_map_rect_Type2 :
 153   PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
 154   'a1 identifier_map -> 'a2
 155
 156 val identifier_map_rect_Type1 :
 157   PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
 158   'a1 identifier_map -> 'a2
 159
 160 val identifier_map_rect_Type0 :
 161   PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
 162   'a1 identifier_map -> 'a2
 163
 164 val identifier_map_inv_rect_Type4 :
 165   PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
 166   PositiveMap.positive_map -> __ -> 'a2) -> 'a2
 167
 168 val identifier_map_inv_rect_Type3 :
 169   PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
 170   PositiveMap.positive_map -> __ -> 'a2) -> 'a2
 171
 172 val identifier_map_inv_rect_Type2 :
 173   PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
 174   PositiveMap.positive_map -> __ -> 'a2) -> 'a2
 175
 176 val identifier_map_inv_rect_Type1 :
 177   PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
 178   PositiveMap.positive_map -> __ -> 'a2) -> 'a2
 179
 180 val identifier_map_inv_rect_Type0 :
 181   PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
 182   PositiveMap.positive_map -> __ -> 'a2) -> 'a2
 183
 184 val identifier_map_discr :
 185   PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map ->
 186   __
 187
 188 val identifier_map_jmdiscr :
 189   PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map ->
 190   __
 191
 192 val empty_map : PreIdentifiers.identifierTag -> 'a1 identifier_map
 193
 194 val lookup :
 195   PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 196   PreIdentifiers.identifier -> 'a1 Types.option
 197
 198 val lookup_def :
 199   PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 200   PreIdentifiers.identifier -> 'a1 -> 'a1
 201
 202 val member :
 203   PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 204   PreIdentifiers.identifier -> Bool.bool
 205
 206 val lookup_safe :
 207   PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 208   PreIdentifiers.identifier -> 'a1
 209
 210 val add :
 211   PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 212   PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map
 213
 214 val elements :
 215   PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 216   (PreIdentifiers.identifier, 'a1) Types.prod List.list
 217
 218 val idmap_all :
 219   PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 220   (PreIdentifiers.identifier -> 'a1 -> __ -> Bool.bool) -> Bool.bool
 221
 222 val update :
 223   PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 224   PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map Errors.res
 225
 226 val remove :
 227   PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 228   PreIdentifiers.identifier -> 'a1 identifier_map
 229
 230 val foldi :
 231   PreIdentifiers.identifierTag -> (PreIdentifiers.identifier -> 'a1 -> 'a2 ->
 232   'a2) -> 'a1 identifier_map -> 'a2 -> 'a2
 233
 234 val fold_inf :
 235   PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 236   (PreIdentifiers.identifier -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a2
 237
 238 val find :
 239   PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 240   (PreIdentifiers.identifier -> 'a1 -> Bool.bool) ->
 241   (PreIdentifiers.identifier, 'a1) Types.prod Types.option
 242
 243 val lookup_present :
 244   PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 245   PreIdentifiers.identifier -> 'a1
 246
 247 val update_present :
 248   PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 249   PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map
 250
 251 type identifier_set = Types.unit0 identifier_map
 252
 253 val empty_set : PreIdentifiers.identifierTag -> identifier_set
 254
 255 val add_set :
 256   PreIdentifiers.identifierTag -> identifier_set -> PreIdentifiers.identifier
 257   -> identifier_set
 258
 259 val singleton_set :
 260   PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier_set
 261
 262 val union_set :
 263   PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map ->
 264   identifier_set
 265
 266 val minus_set :
 267   PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map ->
 268   'a1 identifier_map
 269
 270 val identifierSet : PreIdentifiers.identifierTag -> Setoids.setoid
 271
 272 val id_map_size :
 273   PreIdentifiers.identifierTag -> 'a1 identifier_map -> Nat.nat
 274
 275 open Proper
 276
 277 val set_from_list :
 278   PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
 279   Types.unit0 identifier_map
 280
 281 val dpi1__o__id_set_from_list__o__inject :
 282   PreIdentifiers.identifierTag -> (PreIdentifiers.identifier List.list, 'a1)
 283   Types.dPair -> Types.unit0 identifier_map Types.sig0
 284
 285 val eject__o__id_set_from_list__o__inject :
 286   PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list
 287   Types.sig0 -> Types.unit0 identifier_map Types.sig0
 288
 289 val id_set_from_list__o__inject :
 290   PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
 291   Types.unit0 identifier_map Types.sig0
 292
 293 val dpi1__o__id_set_from_list :
 294   PreIdentifiers.identifierTag -> (PreIdentifiers.identifier List.list, 'a1)
 295   Types.dPair -> Types.unit0 identifier_map
 296
 297 val eject__o__id_set_from_list :
 298   PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list
 299   Types.sig0 -> Types.unit0 identifier_map
 300
 301 val choose :
 302   PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 303   ((PreIdentifiers.identifier, 'a1) Types.prod, 'a1 identifier_map)
 304   Types.prod Types.option
 305
 306 val try_remove :
 307   PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 308   PreIdentifiers.identifier -> ('a1, 'a1 identifier_map) Types.prod
 309   Types.option
 310
 311 val id_set_of_map :
 312   PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set
 313
 314 val set_of_list :
 315   PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
 316   identifier_set
 317
 318 val domain_of_map :
 319   PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set
 320