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

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/identifiers.ml

    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
    5351(** val universe_rect_Type4 :
    54     String.string -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    55 let rec universe_rect_Type4 tag h_mk_universe x_2108 =
    56   let next_identifier = x_2108 in h_mk_universe next_identifier
     52    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
     53let rec universe_rect_Type4 tag h_mk_universe x_1095 =
     54  let next_identifier = x_1095 in h_mk_universe next_identifier
    5755
    5856(** val universe_rect_Type5 :
    59     String.string -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    60 let rec universe_rect_Type5 tag h_mk_universe x_2110 =
    61   let next_identifier = x_2110 in h_mk_universe next_identifier
     57    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
     58let rec universe_rect_Type5 tag h_mk_universe x_1097 =
     59  let next_identifier = x_1097 in h_mk_universe next_identifier
    6260
    6361(** val universe_rect_Type3 :
    64     String.string -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    65 let rec universe_rect_Type3 tag h_mk_universe x_2112 =
    66   let next_identifier = x_2112 in h_mk_universe next_identifier
     62    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
     63let rec universe_rect_Type3 tag h_mk_universe x_1099 =
     64  let next_identifier = x_1099 in h_mk_universe next_identifier
    6765
    6866(** val universe_rect_Type2 :
    69     String.string -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    70 let rec universe_rect_Type2 tag h_mk_universe x_2114 =
    71   let next_identifier = x_2114 in h_mk_universe next_identifier
     67    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
     68let rec universe_rect_Type2 tag h_mk_universe x_1101 =
     69  let next_identifier = x_1101 in h_mk_universe next_identifier
    7270
    7371(** val universe_rect_Type1 :
    74     String.string -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    75 let rec universe_rect_Type1 tag h_mk_universe x_2116 =
    76   let next_identifier = x_2116 in h_mk_universe next_identifier
     72    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
     73let rec universe_rect_Type1 tag h_mk_universe x_1103 =
     74  let next_identifier = x_1103 in h_mk_universe next_identifier
    7775
    7876(** val universe_rect_Type0 :
    79     String.string -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    80 let rec universe_rect_Type0 tag h_mk_universe x_2118 =
    81   let next_identifier = x_2118 in h_mk_universe next_identifier
    82 
    83 (** val next_identifier : String.string -> universe -> Positive.pos **)
     77    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
     78let rec universe_rect_Type0 tag h_mk_universe x_1105 =
     79  let next_identifier = x_1105 in h_mk_universe next_identifier
     80
     81(** val next_identifier :
     82    PreIdentifiers.identifierTag -> universe -> Positive.pos **)
    8483let rec next_identifier tag xxx =
    8584  let yyy = xxx in yyy
    8685
    8786(** val universe_inv_rect_Type4 :
    88     String.string -> universe -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
     87    PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1)
     88    -> 'a1 **)
    8989let universe_inv_rect_Type4 x1 hterm h1 =
    9090  let hcut = universe_rect_Type4 x1 h1 hterm in hcut __
    9191
    9292(** val universe_inv_rect_Type3 :
    93     String.string -> universe -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
     93    PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1)
     94    -> 'a1 **)
    9495let universe_inv_rect_Type3 x1 hterm h1 =
    9596  let hcut = universe_rect_Type3 x1 h1 hterm in hcut __
    9697
    9798(** val universe_inv_rect_Type2 :
    98     String.string -> universe -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
     99    PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1)
     100    -> 'a1 **)
    99101let universe_inv_rect_Type2 x1 hterm h1 =
    100102  let hcut = universe_rect_Type2 x1 h1 hterm in hcut __
    101103
    102104(** val universe_inv_rect_Type1 :
    103     String.string -> universe -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
     105    PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1)
     106    -> 'a1 **)
    104107let universe_inv_rect_Type1 x1 hterm h1 =
    105108  let hcut = universe_rect_Type1 x1 h1 hterm in hcut __
    106109
    107110(** val universe_inv_rect_Type0 :
    108     String.string -> universe -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
     111    PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1)
     112    -> 'a1 **)
    109113let universe_inv_rect_Type0 x1 hterm h1 =
    110114  let hcut = universe_rect_Type0 x1 h1 hterm in hcut __
    111115
    112 (** val universe_discr : String.string -> universe -> universe -> __ **)
     116(** val universe_discr :
     117    PreIdentifiers.identifierTag -> universe -> universe -> __ **)
    113118let universe_discr a1 x y =
    114119  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
    115120
    116 (** val universe_jmdiscr : String.string -> universe -> universe -> __ **)
     121(** val universe_jmdiscr :
     122    PreIdentifiers.identifierTag -> universe -> universe -> __ **)
    117123let universe_jmdiscr a1 x y =
    118124  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
    119125
    120 (** val new_universe : String.string -> universe **)
     126(** val new_universe : PreIdentifiers.identifierTag -> universe **)
    121127let new_universe tag =
    122128  Positive.One
    123129
    124130(** val fresh :
    125     String.string -> universe -> (PreIdentifiers.identifier, universe)
    126     Types.prod **)
     131    PreIdentifiers.identifierTag -> universe -> (PreIdentifiers.identifier,
     132    universe) Types.prod **)
    127133let rec fresh tag u =
    128134  let id = next_identifier tag u in
     
    134140
    135141(** val eq_identifier :
    136     String.string -> PreIdentifiers.identifier -> PreIdentifiers.identifier
    137     -> Bool.bool **)
     142    PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
     143    PreIdentifiers.identifier -> Bool.bool **)
    138144let eq_identifier t l r =
    139145  let l' = l in let r' = r in Positive.eqb0 l' r'
    140146
    141147(** val eq_identifier_elim :
    142     String.string -> PreIdentifiers.identifier -> PreIdentifiers.identifier
    143     -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     148    PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
     149    PreIdentifiers.identifier -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
    144150let eq_identifier_elim t clearme =
    145151  let x = clearme in
     
    150156open Deqsets
    151157
    152 (** val deq_identifier : String.string -> Deqsets.deqSet **)
     158(** val deq_identifier : PreIdentifiers.identifierTag -> Deqsets.deqSet **)
    153159let deq_identifier tag =
    154160  Obj.magic (eq_identifier tag)
    155161
    156162(** val word_of_identifier :
    157     String.string -> PreIdentifiers.identifier -> Positive.pos **)
     163    PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> Positive.pos **)
    158164let word_of_identifier t l =
    159165  let l' = l in l'
    160166
    161167(** val identifier_eq :
    162     String.string -> PreIdentifiers.identifier -> PreIdentifiers.identifier
    163     -> (__, __) Types.sum **)
     168    PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
     169    PreIdentifiers.identifier -> (__, __) Types.sum **)
    164170let identifier_eq tag clearme =
    165171  let x = clearme in
     
    171177
    172178(** val identifier_of_nat :
    173     String.string -> Nat.nat -> PreIdentifiers.identifier **)
     179    PreIdentifiers.identifierTag -> Nat.nat -> PreIdentifiers.identifier **)
    174180let identifier_of_nat tag n =
    175181  Positive.succ_pos_of_nat n
     
    177183type distinct_env = __
    178184
    179 (** val duplicateVariable : String.string **)
    180 let duplicateVariable = "duplicate variable"
    181   (*failwith "AXIOM TO BE REALIZED"*)
    182 
    183185(** val check_member_env :
    184     String.string -> PreIdentifiers.identifier -> (PreIdentifiers.identifier,
    185     'a1) Types.prod List.list -> __ Errors.res **)
     186    PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
     187    (PreIdentifiers.identifier, 'a1) Types.prod List.list -> __ Errors.res **)
    186188let rec check_member_env tag id = function
    187189| List.Nil -> Errors.OK __
     
    189191  (match identifier_eq tag id hd0.Types.fst with
    190192   | Types.Inl _ ->
    191      Errors.Error (List.Cons ((Errors.MSG duplicateVariable), (List.Cons
    192        ((Errors.CTX (tag, id)), List.Nil))))
     193     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.DuplicateVariable),
     194       (List.Cons ((Errors.CTX (tag, id)), List.Nil))))
    193195   | Types.Inr _ ->
    194196     Obj.magic
     
    198200
    199201(** val check_distinct_env :
    200     String.string -> (PreIdentifiers.identifier, 'a1) Types.prod List.list ->
    201     __ Errors.res **)
     202    PreIdentifiers.identifierTag -> (PreIdentifiers.identifier, 'a1)
     203    Types.prod List.list -> __ Errors.res **)
    202204let rec check_distinct_env tag = function
    203205| List.Nil -> Errors.OK __
     
    217219
    218220(** val identifier_map_rect_Type4 :
    219     String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
    220     identifier_map -> 'a2 **)
    221 let rec identifier_map_rect_Type4 tag h_an_id_map x_2280 =
    222   let x_2281 = x_2280 in h_an_id_map x_2281
     221    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
     222    'a1 identifier_map -> 'a2 **)
     223let rec identifier_map_rect_Type4 tag h_an_id_map x_1122 =
     224  let x_1123 = x_1122 in h_an_id_map x_1123
    223225
    224226(** val identifier_map_rect_Type5 :
    225     String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
    226     identifier_map -> 'a2 **)
    227 let rec identifier_map_rect_Type5 tag h_an_id_map x_2283 =
    228   let x_2284 = x_2283 in h_an_id_map x_2284
     227    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
     228    'a1 identifier_map -> 'a2 **)
     229let rec identifier_map_rect_Type5 tag h_an_id_map x_1125 =
     230  let x_1126 = x_1125 in h_an_id_map x_1126
    229231
    230232(** val identifier_map_rect_Type3 :
    231     String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
    232     identifier_map -> 'a2 **)
    233 let rec identifier_map_rect_Type3 tag h_an_id_map x_2286 =
    234   let x_2287 = x_2286 in h_an_id_map x_2287
     233    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
     234    'a1 identifier_map -> 'a2 **)
     235let rec identifier_map_rect_Type3 tag h_an_id_map x_1128 =
     236  let x_1129 = x_1128 in h_an_id_map x_1129
    235237
    236238(** val identifier_map_rect_Type2 :
    237     String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
    238     identifier_map -> 'a2 **)
    239 let rec identifier_map_rect_Type2 tag h_an_id_map x_2289 =
    240   let x_2290 = x_2289 in h_an_id_map x_2290
     239    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
     240    'a1 identifier_map -> 'a2 **)
     241let rec identifier_map_rect_Type2 tag h_an_id_map x_1131 =
     242  let x_1132 = x_1131 in h_an_id_map x_1132
    241243
    242244(** val identifier_map_rect_Type1 :
    243     String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
    244     identifier_map -> 'a2 **)
    245 let rec identifier_map_rect_Type1 tag h_an_id_map x_2292 =
    246   let x_2293 = x_2292 in h_an_id_map x_2293
     245    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
     246    'a1 identifier_map -> 'a2 **)
     247let rec identifier_map_rect_Type1 tag h_an_id_map x_1134 =
     248  let x_1135 = x_1134 in h_an_id_map x_1135
    247249
    248250(** val identifier_map_rect_Type0 :
    249     String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
    250     identifier_map -> 'a2 **)
    251 let rec identifier_map_rect_Type0 tag h_an_id_map x_2295 =
    252   let x_2296 = x_2295 in h_an_id_map x_2296
     251    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
     252    'a1 identifier_map -> 'a2 **)
     253let rec identifier_map_rect_Type0 tag h_an_id_map x_1137 =
     254  let x_1138 = x_1137 in h_an_id_map x_1138
    253255
    254256(** val identifier_map_inv_rect_Type4 :
    255     String.string -> 'a1 identifier_map -> ('a1 PositiveMap.positive_map ->
    256     __ -> 'a2) -> 'a2 **)
     257    PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
     258    PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
    257259let identifier_map_inv_rect_Type4 x1 hterm h1 =
    258260  let hcut = identifier_map_rect_Type4 x1 h1 hterm in hcut __
    259261
    260262(** val identifier_map_inv_rect_Type3 :
    261     String.string -> 'a1 identifier_map -> ('a1 PositiveMap.positive_map ->
    262     __ -> 'a2) -> 'a2 **)
     263    PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
     264    PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
    263265let identifier_map_inv_rect_Type3 x1 hterm h1 =
    264266  let hcut = identifier_map_rect_Type3 x1 h1 hterm in hcut __
    265267
    266268(** val identifier_map_inv_rect_Type2 :
    267     String.string -> 'a1 identifier_map -> ('a1 PositiveMap.positive_map ->
    268     __ -> 'a2) -> 'a2 **)
     269    PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
     270    PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
    269271let identifier_map_inv_rect_Type2 x1 hterm h1 =
    270272  let hcut = identifier_map_rect_Type2 x1 h1 hterm in hcut __
    271273
    272274(** val identifier_map_inv_rect_Type1 :
    273     String.string -> 'a1 identifier_map -> ('a1 PositiveMap.positive_map ->
    274     __ -> 'a2) -> 'a2 **)
     275    PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
     276    PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
    275277let identifier_map_inv_rect_Type1 x1 hterm h1 =
    276278  let hcut = identifier_map_rect_Type1 x1 h1 hterm in hcut __
    277279
    278280(** val identifier_map_inv_rect_Type0 :
    279     String.string -> 'a1 identifier_map -> ('a1 PositiveMap.positive_map ->
    280     __ -> 'a2) -> 'a2 **)
     281    PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
     282    PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
    281283let identifier_map_inv_rect_Type0 x1 hterm h1 =
    282284  let hcut = identifier_map_rect_Type0 x1 h1 hterm in hcut __
    283285
    284286(** val identifier_map_discr :
    285     String.string -> 'a1 identifier_map -> 'a1 identifier_map -> __ **)
     287    PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map
     288    -> __ **)
    286289let identifier_map_discr a1 x y =
    287290  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
    288291
    289292(** val identifier_map_jmdiscr :
    290     String.string -> 'a1 identifier_map -> 'a1 identifier_map -> __ **)
     293    PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map
     294    -> __ **)
    291295let identifier_map_jmdiscr a1 x y =
    292296  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
    293297
    294 (** val empty_map : String.string -> 'a1 identifier_map **)
     298(** val empty_map : PreIdentifiers.identifierTag -> 'a1 identifier_map **)
    295299let empty_map tag =
    296300  PositiveMap.Pm_leaf
    297301
    298302(** val lookup0 :
    299     String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1
    300     Types.option **)
     303    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     304    PreIdentifiers.identifier -> 'a1 Types.option **)
    301305let rec lookup0 tag m l =
    302306  PositiveMap.lookup_opt (let l' = l in l') (let m' = m in m')
    303307
    304308(** val lookup_def :
    305     String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1
    306     -> 'a1 **)
     309    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     310    PreIdentifiers.identifier -> 'a1 -> 'a1 **)
    307311let lookup_def tag m l d =
    308312  match lookup0 tag m l with
     
    311315
    312316(** val member0 :
    313     String.string -> 'a1 identifier_map -> PreIdentifiers.identifier ->
    314     Bool.bool **)
     317    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     318    PreIdentifiers.identifier -> Bool.bool **)
    315319let member0 tag m l =
    316320  match lookup0 tag m l with
     
    319323
    320324(** val lookup_safe :
    321     String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1 **)
     325    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     326    PreIdentifiers.identifier -> 'a1 **)
    322327let lookup_safe tag m i =
    323328  (match lookup0 tag m i with
     
    326331
    327332(** val add :
    328     String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1
    329     -> 'a1 identifier_map **)
     333    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     334    PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map **)
    330335let rec add tag m l a =
    331336  PositiveMap.insert (let l' = l in l') a (let m' = m in m')
    332337
    333338(** val elements :
    334     String.string -> 'a1 identifier_map -> (PreIdentifiers.identifier, 'a1)
    335     Types.prod List.list **)
     339    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     340    (PreIdentifiers.identifier, 'a1) Types.prod List.list **)
    336341let elements tag m =
    337342  PositiveMap.fold0 (fun l a el -> List.Cons ({ Types.fst = l; Types.snd =
     
    339344
    340345(** val idmap_all :
    341     String.string -> 'a1 identifier_map -> (PreIdentifiers.identifier -> 'a1
    342     -> __ -> Bool.bool) -> Bool.bool **)
     346    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     347    (PreIdentifiers.identifier -> 'a1 -> __ -> Bool.bool) -> Bool.bool **)
    343348let idmap_all tag m f =
    344349  PositiveMap.pm_all (let m' = m in m') (fun p a _ -> f p a __)
    345350
    346 (** val missingId : String.string **)
    347 let missingId = "missing id"
    348   (*failwith "AXIOM TO BE REALIZED"*)
    349 
    350351(** val update0 :
    351     String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1
    352     -> 'a1 identifier_map Errors.res **)
     352    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     353    PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map Errors.res **)
    353354let update0 tag m l a =
    354355  match PositiveMap.update (let l' = l in l') a (let m' = m in m') with
    355356  | Types.None ->
    356     Errors.Error (List.Cons ((Errors.MSG missingId), (List.Cons ((Errors.CTX
    357       (tag, l)), List.Nil))))
     357    Errors.Error (List.Cons ((Errors.MSG ErrorMessages.MissingId), (List.Cons
     358      ((Errors.CTX (tag, l)), List.Nil))))
    358359  | Types.Some m' -> Errors.OK m'
    359360
    360361(** val remove :
    361     String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1
    362     identifier_map **)
     362    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     363    PreIdentifiers.identifier -> 'a1 identifier_map **)
    363364let remove tag m id =
    364365  PositiveMap.pm_set (let p = id in p) Types.None (let m0 = m in m0)
    365366
    366367(** val foldi0 :
    367     String.string -> (PreIdentifiers.identifier -> 'a1 -> 'a2 -> 'a2) -> 'a1
    368     identifier_map -> 'a2 -> 'a2 **)
     368    PreIdentifiers.identifierTag -> (PreIdentifiers.identifier -> 'a1 -> 'a2
     369    -> 'a2) -> 'a1 identifier_map -> 'a2 -> 'a2 **)
    369370let foldi0 tag f m b =
    370371  let m' = m in PositiveMap.fold0 (fun bv -> f bv) m' b
    371372
    372373(** val fold_inf :
    373     String.string -> 'a1 identifier_map -> (PreIdentifiers.identifier -> 'a1
    374     -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a2 **)
     374    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     375    (PreIdentifiers.identifier -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a2 **)
    375376let fold_inf tag m =
    376377  let m' = m in
     
    378379
    379380(** val find0 :
    380     String.string -> 'a1 identifier_map -> (PreIdentifiers.identifier -> 'a1
    381     -> Bool.bool) -> (PreIdentifiers.identifier, 'a1) Types.prod Types.option **)
     381    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     382    (PreIdentifiers.identifier -> 'a1 -> Bool.bool) ->
     383    (PreIdentifiers.identifier, 'a1) Types.prod Types.option **)
    382384let find0 tag m p =
    383385  let m' = m in
     
    386388
    387389(** val lookup_present :
    388     String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1 **)
     390    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     391    PreIdentifiers.identifier -> 'a1 **)
    389392let lookup_present tag m id =
    390393  (match lookup0 tag m id with
     
    393396
    394397(** val update_present :
    395     String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1
    396     -> 'a1 identifier_map **)
     398    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     399    PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map **)
    397400let update_present tag m l a =
    398401  let l' = let l' = l in l' in
     
    407410type identifier_set = Types.unit0 identifier_map
    408411
    409 (** val empty_set : String.string -> identifier_set **)
     412(** val empty_set : PreIdentifiers.identifierTag -> identifier_set **)
    410413let empty_set tag =
    411414  empty_map tag
    412415
    413416(** val add_set :
    414     String.string -> identifier_set -> PreIdentifiers.identifier ->
    415     identifier_set **)
     417    PreIdentifiers.identifierTag -> identifier_set ->
     418    PreIdentifiers.identifier -> identifier_set **)
    416419let add_set tag s i =
    417420  add tag s i Types.It
    418421
    419422(** val singleton_set :
    420     String.string -> PreIdentifiers.identifier -> identifier_set **)
     423    PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
     424    identifier_set **)
    421425let singleton_set tag i =
    422426  add_set tag (empty_set tag) i
    423427
    424428(** val union_set :
    425     String.string -> 'a1 identifier_map -> 'a2 identifier_map ->
    426     identifier_set **)
     429    PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map
     430    -> identifier_set **)
    427431let rec union_set tag s s' =
    428432  PositiveMap.merge (fun o o' ->
     
    436440
    437441(** val minus_set :
    438     String.string -> 'a1 identifier_map -> 'a2 identifier_map -> 'a1
    439     identifier_map **)
     442    PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map
     443    -> 'a1 identifier_map **)
    440444let rec minus_set tag s s' =
    441445  PositiveMap.merge (fun o o' ->
     
    444448    | Types.Some x -> Types.None) (let s0 = s in s0) (let s1 = s' in s1)
    445449
    446 (** val identifierSet : String.string -> Setoids.setoid **)
     450(** val identifierSet : PreIdentifiers.identifierTag -> Setoids.setoid **)
    447451let identifierSet tag =
    448452  Setoids.Mk_Setoid
    449453
    450 (** val id_map_size : String.string -> 'a1 identifier_map -> Nat.nat **)
     454(** val id_map_size :
     455    PreIdentifiers.identifierTag -> 'a1 identifier_map -> Nat.nat **)
    451456let id_map_size tag s =
    452457  let p = s in PositiveMap.domain_size p
     
    455460
    456461(** val set_from_list :
    457     String.string -> PreIdentifiers.identifier List.list -> Types.unit0
    458     identifier_map **)
     462    PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
     463    Types.unit0 identifier_map **)
    459464let set_from_list tag =
    460465  Util.foldl (add_set tag) (empty_set tag)
    461466
    462467(** val choose :
    463     String.string -> 'a1 identifier_map -> ((PreIdentifiers.identifier, 'a1)
    464     Types.prod, 'a1 identifier_map) Types.prod Types.option **)
     468    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     469    ((PreIdentifiers.identifier, 'a1) Types.prod, 'a1 identifier_map)
     470    Types.prod Types.option **)
    465471let choose tag m =
    466472  match PositiveMap.pm_choose (let m' = m in m') with
     
    471477
    472478(** val try_remove :
    473     String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> ('a1,
    474     'a1 identifier_map) Types.prod Types.option **)
     479    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
     480    PreIdentifiers.identifier -> ('a1, 'a1 identifier_map) Types.prod
     481    Types.option **)
    475482let try_remove tag m id =
    476483  match PositiveMap.pm_try_remove (let id' = id in id') (let m' = m in m') with
     
    480487
    481488(** val id_set_of_map :
    482     String.string -> 'a1 identifier_map -> identifier_set **)
     489    PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set **)
    483490let id_set_of_map tag m =
    484491  PositiveMap.map0 (fun x -> Types.It) (let m' = m in m')
    485492
    486493(** val set_of_list :
    487     String.string -> PreIdentifiers.identifier List.list -> identifier_set **)
     494    PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
     495    identifier_set **)
    488496let set_of_list tag l =
    489497  Util.foldl (fun s id -> add_set tag s id) (empty_set tag) l
    490498
    491499(** val domain_of_map :
    492     String.string -> 'a1 identifier_map -> identifier_set **)
     500    PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set **)
    493501let domain_of_map tag m =
    494502  PositiveMap.domain_of_pm (let m0 = m in m0)
Note: See TracChangeset for help on using the changeset viewer.