Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/identifiers.mli

    r2601 r2649  
    1111open Types
    1212
    13 open Char
    14 
    1513open Bool
    1614
     
    1917open Nat
    2018
     19open Positive
     20
     21open Setoids
     22
     23open Monad
     24
     25open Option
     26
     27open Div_and_mod
     28
     29open Jmeq
     30
     31open Russell
     32
     33open Util
     34
    2135open List
    2236
    23 open String
    24 
    25 open Positive
    26 
    27 open Setoids
    28 
    29 open Monad
    30 
    31 open Option
    32 
    33 open Div_and_mod
    34 
    35 open Jmeq
    36 
    37 open Russell
    38 
    39 open Util
    40 
    4137open Lists
    4238
    4339open Extralib
     40
     41open ErrorMessages
    4442
    4543open PreIdentifiers
     
    5250
    5351val universe_rect_Type4 :
    54   String.string -> (Positive.pos -> 'a1) -> universe -> 'a1
     52  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
    5553
    5654val universe_rect_Type5 :
    57   String.string -> (Positive.pos -> 'a1) -> universe -> 'a1
     55  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
    5856
    5957val universe_rect_Type3 :
    60   String.string -> (Positive.pos -> 'a1) -> universe -> 'a1
     58  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
    6159
    6260val universe_rect_Type2 :
    63   String.string -> (Positive.pos -> 'a1) -> universe -> 'a1
     61  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
    6462
    6563val universe_rect_Type1 :
    66   String.string -> (Positive.pos -> 'a1) -> universe -> 'a1
     64  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
    6765
    6866val universe_rect_Type0 :
    69   String.string -> (Positive.pos -> 'a1) -> universe -> 'a1
    70 
    71 val next_identifier : String.string -> universe -> Positive.pos
     67  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
     68
     69val next_identifier :
     70  PreIdentifiers.identifierTag -> universe -> Positive.pos
    7271
    7372val universe_inv_rect_Type4 :
    74   String.string -> universe -> (Positive.pos -> __ -> 'a1) -> 'a1
     73  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
     74  'a1
    7575
    7676val universe_inv_rect_Type3 :
    77   String.string -> universe -> (Positive.pos -> __ -> 'a1) -> 'a1
     77  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
     78  'a1
    7879
    7980val universe_inv_rect_Type2 :
    80   String.string -> universe -> (Positive.pos -> __ -> 'a1) -> 'a1
     81  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
     82  'a1
    8183
    8284val universe_inv_rect_Type1 :
    83   String.string -> universe -> (Positive.pos -> __ -> 'a1) -> 'a1
     85  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
     86  'a1
    8487
    8588val universe_inv_rect_Type0 :
    86   String.string -> universe -> (Positive.pos -> __ -> 'a1) -> 'a1
    87 
    88 val universe_discr : String.string -> universe -> universe -> __
    89 
    90 val universe_jmdiscr : String.string -> universe -> universe -> __
    91 
    92 val new_universe : String.string -> universe
     89  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
     90  'a1
     91
     92val universe_discr :
     93  PreIdentifiers.identifierTag -> universe -> universe -> __
     94
     95val universe_jmdiscr :
     96  PreIdentifiers.identifierTag -> universe -> universe -> __
     97
     98val new_universe : PreIdentifiers.identifierTag -> universe
    9399
    94100val fresh :
    95   String.string -> universe -> (PreIdentifiers.identifier, universe)
    96   Types.prod
     101  PreIdentifiers.identifierTag -> universe -> (PreIdentifiers.identifier,
     102  universe) Types.prod
    97103
    98104type fresh_for_univ = __
     
    101107
    102108val eq_identifier :
    103   String.string -> PreIdentifiers.identifier -> PreIdentifiers.identifier ->
    104   Bool.bool
     109  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
     110  PreIdentifiers.identifier -> Bool.bool
    105111
    106112val eq_identifier_elim :
    107   String.string -> PreIdentifiers.identifier -> PreIdentifiers.identifier ->
    108   (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     113  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
     114  PreIdentifiers.identifier -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
    109115
    110116open Deqsets
    111117
    112 val deq_identifier : String.string -> Deqsets.deqSet
     118val deq_identifier : PreIdentifiers.identifierTag -> Deqsets.deqSet
    113119
    114120val word_of_identifier :
    115   String.string -> PreIdentifiers.identifier -> Positive.pos
     121  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> Positive.pos
    116122
    117123val identifier_eq :
    118   String.string -> PreIdentifiers.identifier -> PreIdentifiers.identifier ->
    119   (__, __) Types.sum
    120 
    121 val identifier_of_nat : String.string -> Nat.nat -> PreIdentifiers.identifier
     124  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
     125  PreIdentifiers.identifier -> (__, __) Types.sum
     126
     127val identifier_of_nat :
     128  PreIdentifiers.identifierTag -> Nat.nat -> PreIdentifiers.identifier
    122129
    123130type distinct_env = __
    124131
    125 val duplicateVariable : String.string
    126 
    127132val check_member_env :
    128   String.string -> PreIdentifiers.identifier -> (PreIdentifiers.identifier,
    129   'a1) Types.prod List.list -> __ Errors.res
     133  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
     134  (PreIdentifiers.identifier, 'a1) Types.prod List.list -> __ Errors.res
    130135
    131136val check_distinct_env :
    132   String.string -> (PreIdentifiers.identifier, 'a1) Types.prod List.list ->
    133   __ Errors.res
     137  PreIdentifiers.identifierTag -> (PreIdentifiers.identifier, 'a1) Types.prod
     138  List.list -> __ Errors.res
    134139
    135140open PositiveMap
     
    140145
    141146val identifier_map_rect_Type4 :
    142   String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
    143   identifier_map -> 'a2
     147  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
     148  'a1 identifier_map -> 'a2
    144149
    145150val identifier_map_rect_Type5 :
    146   String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
    147   identifier_map -> 'a2
     151  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
     152  'a1 identifier_map -> 'a2
    148153
    149154val identifier_map_rect_Type3 :
    150   String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
    151   identifier_map -> 'a2
     155  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
     156  'a1 identifier_map -> 'a2
    152157
    153158val identifier_map_rect_Type2 :
    154   String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
    155   identifier_map -> 'a2
     159  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
     160  'a1 identifier_map -> 'a2
    156161
    157162val identifier_map_rect_Type1 :
    158   String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
    159   identifier_map -> 'a2
     163  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
     164  'a1 identifier_map -> 'a2
    160165
    161166val identifier_map_rect_Type0 :
    162   String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
    163   identifier_map -> 'a2
     167  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
     168  'a1 identifier_map -> 'a2
    164169
    165170val identifier_map_inv_rect_Type4 :
    166   String.string -> 'a1 identifier_map -> ('a1 PositiveMap.positive_map -> __
    167   -> 'a2) -> 'a2
     171  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
     172  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
    168173
    169174val identifier_map_inv_rect_Type3 :
    170   String.string -> 'a1 identifier_map -> ('a1 PositiveMap.positive_map -> __
    171   -> 'a2) -> 'a2
     175  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
     176  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
    172177
    173178val identifier_map_inv_rect_Type2 :
    174   String.string -> 'a1 identifier_map -> ('a1 PositiveMap.positive_map -> __
    175   -> 'a2) -> 'a2
     179  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
     180  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
    176181
    177182val identifier_map_inv_rect_Type1 :
    178   String.string -> 'a1 identifier_map -> ('a1 PositiveMap.positive_map -> __
    179   -> 'a2) -> 'a2
     183  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
     184  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
    180185
    181186val identifier_map_inv_rect_Type0 :
    182   String.string -> 'a1 identifier_map -> ('a1 PositiveMap.positive_map -> __
    183   -> 'a2) -> 'a2
     187  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
     188  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
    184189
    185190val identifier_map_discr :
    186   String.string -> 'a1 identifier_map -> 'a1 identifier_map -> __
     191  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map ->
     192  __
    187193
    188194val identifier_map_jmdiscr :
    189   String.string -> 'a1 identifier_map -> 'a1 identifier_map -> __
    190 
    191 val empty_map : String.string -> 'a1 identifier_map
     195  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map ->
     196  __
     197
     198val empty_map : PreIdentifiers.identifierTag -> 'a1 identifier_map
    192199
    193200val lookup0 :
    194   String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1
     201  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     202  PreIdentifiers.identifier -> 'a1 Types.option
     203
     204val lookup_def :
     205  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     206  PreIdentifiers.identifier -> 'a1 -> 'a1
     207
     208val member0 :
     209  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     210  PreIdentifiers.identifier -> Bool.bool
     211
     212val lookup_safe :
     213  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     214  PreIdentifiers.identifier -> 'a1
     215
     216val add :
     217  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     218  PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map
     219
     220val elements :
     221  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     222  (PreIdentifiers.identifier, 'a1) Types.prod List.list
     223
     224val idmap_all :
     225  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     226  (PreIdentifiers.identifier -> 'a1 -> __ -> Bool.bool) -> Bool.bool
     227
     228val update0 :
     229  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     230  PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map Errors.res
     231
     232val remove :
     233  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     234  PreIdentifiers.identifier -> 'a1 identifier_map
     235
     236val foldi0 :
     237  PreIdentifiers.identifierTag -> (PreIdentifiers.identifier -> 'a1 -> 'a2 ->
     238  'a2) -> 'a1 identifier_map -> 'a2 -> 'a2
     239
     240val fold_inf :
     241  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     242  (PreIdentifiers.identifier -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a2
     243
     244val find0 :
     245  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     246  (PreIdentifiers.identifier -> 'a1 -> Bool.bool) ->
     247  (PreIdentifiers.identifier, 'a1) Types.prod Types.option
     248
     249val lookup_present :
     250  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     251  PreIdentifiers.identifier -> 'a1
     252
     253val update_present :
     254  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     255  PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map
     256
     257type fresh_for_map = __
     258
     259type identifier_set = Types.unit0 identifier_map
     260
     261val empty_set : PreIdentifiers.identifierTag -> identifier_set
     262
     263val add_set :
     264  PreIdentifiers.identifierTag -> identifier_set -> PreIdentifiers.identifier
     265  -> identifier_set
     266
     267val singleton_set :
     268  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier_set
     269
     270val union_set :
     271  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map ->
     272  identifier_set
     273
     274val minus_set :
     275  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map ->
     276  'a1 identifier_map
     277
     278val identifierSet : PreIdentifiers.identifierTag -> Setoids.setoid
     279
     280val id_map_size :
     281  PreIdentifiers.identifierTag -> 'a1 identifier_map -> Nat.nat
     282
     283open Proper
     284
     285val set_from_list :
     286  PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
     287  Types.unit0 identifier_map
     288
     289val choose :
     290  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     291  ((PreIdentifiers.identifier, 'a1) Types.prod, 'a1 identifier_map)
     292  Types.prod Types.option
     293
     294val try_remove :
     295  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     296  PreIdentifiers.identifier -> ('a1, 'a1 identifier_map) Types.prod
    195297  Types.option
    196298
    197 val lookup_def :
    198   String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1 ->
    199   'a1
    200 
    201 val member0 :
    202   String.string -> 'a1 identifier_map -> PreIdentifiers.identifier ->
    203   Bool.bool
    204 
    205 val lookup_safe :
    206   String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1
    207 
    208 val add :
    209   String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1 ->
    210   'a1 identifier_map
    211 
    212 val elements :
    213   String.string -> 'a1 identifier_map -> (PreIdentifiers.identifier, 'a1)
    214   Types.prod List.list
    215 
    216 val idmap_all :
    217   String.string -> 'a1 identifier_map -> (PreIdentifiers.identifier -> 'a1 ->
    218   __ -> Bool.bool) -> Bool.bool
    219 
    220 val missingId : String.string
    221 
    222 val update0 :
    223   String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1 ->
    224   'a1 identifier_map Errors.res
    225 
    226 val remove :
    227   String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1
    228   identifier_map
    229 
    230 val foldi0 :
    231   String.string -> (PreIdentifiers.identifier -> 'a1 -> 'a2 -> 'a2) -> 'a1
    232   identifier_map -> 'a2 -> 'a2
    233 
    234 val fold_inf :
    235   String.string -> 'a1 identifier_map -> (PreIdentifiers.identifier -> 'a1 ->
    236   __ -> 'a2 -> 'a2) -> 'a2 -> 'a2
    237 
    238 val find0 :
    239   String.string -> 'a1 identifier_map -> (PreIdentifiers.identifier -> 'a1 ->
    240   Bool.bool) -> (PreIdentifiers.identifier, 'a1) Types.prod Types.option
    241 
    242 val lookup_present :
    243   String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1
    244 
    245 val update_present :
    246   String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1 ->
    247   'a1 identifier_map
    248 
    249 type fresh_for_map = __
    250 
    251 type identifier_set = Types.unit0 identifier_map
    252 
    253 val empty_set : String.string -> identifier_set
    254 
    255 val add_set :
    256   String.string -> identifier_set -> PreIdentifiers.identifier ->
     299val id_set_of_map :
     300  PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set
     301
     302val set_of_list :
     303  PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
    257304  identifier_set
    258305
    259 val singleton_set :
    260   String.string -> PreIdentifiers.identifier -> identifier_set
    261 
    262 val union_set :
    263   String.string -> 'a1 identifier_map -> 'a2 identifier_map -> identifier_set
    264 
    265 val minus_set :
    266   String.string -> 'a1 identifier_map -> 'a2 identifier_map -> 'a1
    267   identifier_map
    268 
    269 val identifierSet : String.string -> Setoids.setoid
    270 
    271 val id_map_size : String.string -> 'a1 identifier_map -> Nat.nat
    272 
    273 open Proper
    274 
    275 val set_from_list :
    276   String.string -> PreIdentifiers.identifier List.list -> Types.unit0
    277   identifier_map
    278 
    279 val choose :
    280   String.string -> 'a1 identifier_map -> ((PreIdentifiers.identifier, 'a1)
    281   Types.prod, 'a1 identifier_map) Types.prod Types.option
    282 
    283 val try_remove :
    284   String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> ('a1,
    285   'a1 identifier_map) Types.prod Types.option
    286 
    287 val id_set_of_map : String.string -> 'a1 identifier_map -> identifier_set
    288 
    289 val set_of_list :
    290   String.string -> PreIdentifiers.identifier List.list -> identifier_set
    291 
    292 val domain_of_map : String.string -> 'a1 identifier_map -> identifier_set
    293 
     306val domain_of_map :
     307  PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set
     308
Note: See TracChangeset for help on using the changeset viewer.