extracted/identifiers.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 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 let rec universe_rect_Type4 tag h_mk_universe x_3239 =
  54   let next_identifier = x_3239 in h_mk_universe next_identifier
  55
  56 (** val universe_rect_Type5 :
  57     PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
  58 let rec universe_rect_Type5 tag h_mk_universe x_3241 =
  59   let next_identifier = x_3241 in h_mk_universe next_identifier
  60
  61 (** val universe_rect_Type3 :
  62     PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
  63 let rec universe_rect_Type3 tag h_mk_universe x_3243 =
  64   let next_identifier = x_3243 in h_mk_universe next_identifier
  65
  66 (** val universe_rect_Type2 :
  67     PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
  68 let rec universe_rect_Type2 tag h_mk_universe x_3245 =
  69   let next_identifier = x_3245 in h_mk_universe next_identifier
  70
  71 (** val universe_rect_Type1 :
  72     PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
  73 let rec universe_rect_Type1 tag h_mk_universe x_3247 =
  74   let next_identifier = x_3247 in h_mk_universe next_identifier
  75
  76 (** val universe_rect_Type0 :
  77     PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
  78 let rec universe_rect_Type0 tag h_mk_universe x_3249 =
  79   let next_identifier = x_3249 in h_mk_universe next_identifier
  80
  81 (** val next_identifier :
  82     PreIdentifiers.identifierTag -> universe -> Positive.pos **)
  83 let rec next_identifier tag xxx =
  84   let yyy = xxx in yyy
  85
  86 (** val universe_inv_rect_Type4 :
  87     PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1)
  88     -> 'a1 **)
  89 let universe_inv_rect_Type4 x1 hterm h1 =
  90   let hcut = universe_rect_Type4 x1 h1 hterm in hcut __
  91
  92 (** val universe_inv_rect_Type3 :
  93     PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1)
  94     -> 'a1 **)
  95 let universe_inv_rect_Type3 x1 hterm h1 =
  96   let hcut = universe_rect_Type3 x1 h1 hterm in hcut __
  97
  98 (** val universe_inv_rect_Type2 :
  99     PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1)
 100     -> 'a1 **)
 101 let universe_inv_rect_Type2 x1 hterm h1 =
 102   let hcut = universe_rect_Type2 x1 h1 hterm in hcut __
 103
 104 (** val universe_inv_rect_Type1 :
 105     PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1)
 106     -> 'a1 **)
 107 let universe_inv_rect_Type1 x1 hterm h1 =
 108   let hcut = universe_rect_Type1 x1 h1 hterm in hcut __
 109
 110 (** val universe_inv_rect_Type0 :
 111     PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1)
 112     -> 'a1 **)
 113 let universe_inv_rect_Type0 x1 hterm h1 =
 114   let hcut = universe_rect_Type0 x1 h1 hterm in hcut __
 115
 116 (** val universe_discr :
 117     PreIdentifiers.identifierTag -> universe -> universe -> __ **)
 118 let universe_discr a1 x y =
 119   Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
 120
 121 (** val universe_jmdiscr :
 122     PreIdentifiers.identifierTag -> universe -> universe -> __ **)
 123 let universe_jmdiscr a1 x y =
 124   Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
 125
 126 (** val new_universe : PreIdentifiers.identifierTag -> universe **)
 127 let new_universe tag =
 128   Positive.One
 129
 130 (** val fresh :
 131     PreIdentifiers.identifierTag -> universe -> (PreIdentifiers.identifier,
 132     universe) Types.prod **)
 133 let rec fresh tag u =
 134   let id = next_identifier tag u in
 135   { Types.fst = id; Types.snd = (Positive.succ id) }
 136
 137 (** val eq_identifier :
 138     PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
 139     PreIdentifiers.identifier -> Bool.bool **)
 140 let eq_identifier t l r =
 141   let l' = l in let r' = r in Positive.eqb l' r'
 142
 143 (** val eq_identifier_elim :
 144     PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
 145     PreIdentifiers.identifier -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 146 let eq_identifier_elim t clearme =
 147   let x = clearme in
 148   (fun clearme0 ->
 149   let y = clearme0 in
 150   (fun t0 f -> Positive.eqb_elim x y (fun _ -> t0 __) (fun _ -> f __)))
 151
 152 open Deqsets
 153
 154 (** val deq_identifier : PreIdentifiers.identifierTag -> Deqsets.deqSet **)
 155 let deq_identifier tag =
 156   Obj.magic (eq_identifier tag)
 157
 158 (** val word_of_identifier :
 159     PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> Positive.pos **)
 160 let word_of_identifier t l =
 161   let l' = l in l'
 162
 163 (** val identifier_eq :
 164     PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
 165     PreIdentifiers.identifier -> (__, __) Types.sum **)
 166 let identifier_eq tag clearme =
 167   let x = clearme in
 168   (fun clearme0 ->
 169   let y = clearme0 in
 170   (match Positive.eqb x y with
 171    | Bool.True -> (fun _ -> Types.Inl __)
 172    | Bool.False -> (fun _ -> Types.Inr __)) __)
 173
 174 (** val identifier_of_nat :
 175     PreIdentifiers.identifierTag -> Nat.nat -> PreIdentifiers.identifier **)
 176 let identifier_of_nat tag n =
 177   Positive.succ_pos_of_nat n
 178
 179 (** val check_member_env :
 180     PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
 181     (PreIdentifiers.identifier, 'a1) Types.prod List.list -> __ Errors.res **)
 182 let rec check_member_env tag id = function
 183 | List.Nil -> Errors.OK __
 184 | List.Cons (hd, tl) ->
 185   (match identifier_eq tag id hd.Types.fst with
 186    | Types.Inl _ ->
 187      Errors.Error (List.Cons ((Errors.MSG ErrorMessages.DuplicateVariable),
 188        (List.Cons ((Errors.CTX (tag, id)), List.Nil))))
 189    | Types.Inr _ ->
 190      Obj.magic
 191        (Monad.m_bind0 (Monad.max_def Errors.res0)
 192          (Obj.magic (check_member_env tag id tl)) (fun _ ->
 193          Obj.magic (Errors.OK __))))
 194
 195 (** val check_distinct_env :
 196     PreIdentifiers.identifierTag -> (PreIdentifiers.identifier, 'a1)
 197     Types.prod List.list -> __ Errors.res **)
 198 let rec check_distinct_env tag = function
 199 | List.Nil -> Errors.OK __
 200 | List.Cons (hd, tl) ->
 201   Obj.magic
 202     (Monad.m_bind0 (Monad.max_def Errors.res0)
 203       (Obj.magic (check_member_env tag hd.Types.fst tl)) (fun _ ->
 204       Monad.m_bind0 (Monad.max_def Errors.res0)
 205         (Obj.magic (check_distinct_env tag tl)) (fun _ ->
 206         Obj.magic (Errors.OK __))))
 207
 208 open PositiveMap
 209
 210 type 'a identifier_map =
 211   'a PositiveMap.positive_map
 212   (* singleton inductive, whose constructor was an_id_map *)
 213
 214 (** val identifier_map_rect_Type4 :
 215     PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
 216     'a1 identifier_map -> 'a2 **)
 217 let rec identifier_map_rect_Type4 tag h_an_id_map x_3411 =
 218   let x_3412 = x_3411 in h_an_id_map x_3412
 219
 220 (** val identifier_map_rect_Type5 :
 221     PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
 222     'a1 identifier_map -> 'a2 **)
 223 let rec identifier_map_rect_Type5 tag h_an_id_map x_3414 =
 224   let x_3415 = x_3414 in h_an_id_map x_3415
 225
 226 (** val identifier_map_rect_Type3 :
 227     PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
 228     'a1 identifier_map -> 'a2 **)
 229 let rec identifier_map_rect_Type3 tag h_an_id_map x_3417 =
 230   let x_3418 = x_3417 in h_an_id_map x_3418
 231
 232 (** val identifier_map_rect_Type2 :
 233     PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
 234     'a1 identifier_map -> 'a2 **)
 235 let rec identifier_map_rect_Type2 tag h_an_id_map x_3420 =
 236   let x_3421 = x_3420 in h_an_id_map x_3421
 237
 238 (** val identifier_map_rect_Type1 :
 239     PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
 240     'a1 identifier_map -> 'a2 **)
 241 let rec identifier_map_rect_Type1 tag h_an_id_map x_3423 =
 242   let x_3424 = x_3423 in h_an_id_map x_3424
 243
 244 (** val identifier_map_rect_Type0 :
 245     PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
 246     'a1 identifier_map -> 'a2 **)
 247 let rec identifier_map_rect_Type0 tag h_an_id_map x_3426 =
 248   let x_3427 = x_3426 in h_an_id_map x_3427
 249
 250 (** val identifier_map_inv_rect_Type4 :
 251     PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
 252     PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
 253 let identifier_map_inv_rect_Type4 x1 hterm h1 =
 254   let hcut = identifier_map_rect_Type4 x1 h1 hterm in hcut __
 255
 256 (** val identifier_map_inv_rect_Type3 :
 257     PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
 258     PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
 259 let identifier_map_inv_rect_Type3 x1 hterm h1 =
 260   let hcut = identifier_map_rect_Type3 x1 h1 hterm in hcut __
 261
 262 (** val identifier_map_inv_rect_Type2 :
 263     PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
 264     PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
 265 let identifier_map_inv_rect_Type2 x1 hterm h1 =
 266   let hcut = identifier_map_rect_Type2 x1 h1 hterm in hcut __
 267
 268 (** val identifier_map_inv_rect_Type1 :
 269     PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
 270     PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
 271 let identifier_map_inv_rect_Type1 x1 hterm h1 =
 272   let hcut = identifier_map_rect_Type1 x1 h1 hterm in hcut __
 273
 274 (** val identifier_map_inv_rect_Type0 :
 275     PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
 276     PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
 277 let identifier_map_inv_rect_Type0 x1 hterm h1 =
 278   let hcut = identifier_map_rect_Type0 x1 h1 hterm in hcut __
 279
 280 (** val identifier_map_discr :
 281     PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map
 282     -> __ **)
 283 let identifier_map_discr a1 x y =
 284   Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
 285
 286 (** val identifier_map_jmdiscr :
 287     PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map
 288     -> __ **)
 289 let identifier_map_jmdiscr a1 x y =
 290   Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
 291
 292 (** val empty_map : PreIdentifiers.identifierTag -> 'a1 identifier_map **)
 293 let empty_map tag =
 294   PositiveMap.Pm_leaf
 295
 296 (** val lookup :
 297     PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 298     PreIdentifiers.identifier -> 'a1 Types.option **)
 299 let rec lookup tag m l =
 300   PositiveMap.lookup_opt (let l' = l in l') (let m' = m in m')
 301
 302 (** val lookup_def :
 303     PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 304     PreIdentifiers.identifier -> 'a1 -> 'a1 **)
 305 let lookup_def tag m l d =
 306   match lookup tag m l with
 307   | Types.None -> d
 308   | Types.Some x -> x
 309
 310 (** val member :
 311     PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 312     PreIdentifiers.identifier -> Bool.bool **)
 313 let member tag m l =
 314   match lookup tag m l with
 315   | Types.None -> Bool.False
 316   | Types.Some x -> Bool.True
 317
 318 (** val lookup_safe :
 319     PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 320     PreIdentifiers.identifier -> 'a1 **)
 321 let lookup_safe tag m i =
 322   (match lookup tag m i with
 323    | Types.None -> (fun _ -> assert false (* absurd case *))
 324    | Types.Some x -> (fun _ -> x)) __
 325
 326 (** val add :
 327     PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 328     PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map **)
 329 let rec add tag m l a =
 330   PositiveMap.insert (let l' = l in l') a (let m' = m in m')
 331
 332 (** val elements :
 333     PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 334     (PreIdentifiers.identifier, 'a1) Types.prod List.list **)
 335 let elements tag m =
 336   PositiveMap.fold (fun l a el -> List.Cons ({ Types.fst = l; Types.snd =
 337     a }, el)) (let m' = m in m') List.Nil
 338
 339 (** val idmap_all :
 340     PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 341     (PreIdentifiers.identifier -> 'a1 -> __ -> Bool.bool) -> Bool.bool **)
 342 let idmap_all tag m f =
 343   PositiveMap.pm_all (let m' = m in m') (fun p a _ -> f p a __)
 344
 345 (** val update :
 346     PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 347     PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map Errors.res **)
 348 let update tag m l a =
 349   match PositiveMap.update (let l' = l in l') a (let m' = m in m') with
 350   | Types.None ->
 351     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.MissingId), (List.Cons
 352       ((Errors.CTX (tag, l)), List.Nil))))
 353   | Types.Some m' -> Errors.OK m'
 354
 355 (** val remove :
 356     PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 357     PreIdentifiers.identifier -> 'a1 identifier_map **)
 358 let remove tag m id =
 359   PositiveMap.pm_set (let p = id in p) Types.None (let m0 = m in m0)
 360
 361 (** val foldi :
 362     PreIdentifiers.identifierTag -> (PreIdentifiers.identifier -> 'a1 -> 'a2
 363     -> 'a2) -> 'a1 identifier_map -> 'a2 -> 'a2 **)
 364 let foldi tag f m b =
 365   let m' = m in PositiveMap.fold (fun bv -> f bv) m' b
 366
 367 (** val fold_inf :
 368     PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 369     (PreIdentifiers.identifier -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a2 **)
 370 let fold_inf tag m =
 371   let m' = m in
 372   (fun f b -> PositiveMap.pm_fold_inf m' (fun bv a _ -> f bv a __) b)
 373
 374 (** val find :
 375     PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 376     (PreIdentifiers.identifier -> 'a1 -> Bool.bool) ->
 377     (PreIdentifiers.identifier, 'a1) Types.prod Types.option **)
 378 let find tag m p =
 379   let m' = m in
 380   Types.option_map (fun x -> { Types.fst = x.Types.fst; Types.snd =
 381     x.Types.snd }) (PositiveMap.pm_find m' (fun id -> p id))
 382
 383 (** val lookup_present :
 384     PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 385     PreIdentifiers.identifier -> 'a1 **)
 386 let lookup_present tag m id =
 387   (match lookup tag m id with
 388    | Types.None -> (fun _ -> assert false (* absurd case *))
 389    | Types.Some a -> (fun _ -> a)) __
 390
 391 (** val update_present :
 392     PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 393     PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map **)
 394 let update_present tag m l a =
 395   let l' = let l' = l in l' in
 396   let m' = let m' = m in m' in
 397   let u' = PositiveMap.update l' a m' in
 398   (match u' with
 399    | Types.None -> (fun _ -> assert false (* absurd case *))
 400    | Types.Some m'0 -> (fun _ -> m'0)) __
 401
 402 type identifier_set = Types.unit0 identifier_map
 403
 404 (** val empty_set : PreIdentifiers.identifierTag -> identifier_set **)
 405 let empty_set tag =
 406   empty_map tag
 407
 408 (** val add_set :
 409     PreIdentifiers.identifierTag -> identifier_set ->
 410     PreIdentifiers.identifier -> identifier_set **)
 411 let add_set tag s i =
 412   add tag s i Types.It
 413
 414 (** val singleton_set :
 415     PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
 416     identifier_set **)
 417 let singleton_set tag i =
 418   add_set tag (empty_set tag) i
 419
 420 (** val union_set :
 421     PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map
 422     -> identifier_set **)
 423 let rec union_set tag s s' =
 424   PositiveMap.merge (fun o o' ->
 425     match o with
 426     | Types.None ->
 427       Obj.magic
 428         (Monad.m_bind0 (Monad.max_def Option.option) (Obj.magic o') (fun x ->
 429           Monad.m_return0 (Monad.max_def Option.option) Types.It))
 430     | Types.Some x -> Types.Some Types.It) (let s0 = s in s0)
 431     (let s1 = s' in s1)
 432
 433 (** val minus_set :
 434     PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map
 435     -> 'a1 identifier_map **)
 436 let rec minus_set tag s s' =
 437   PositiveMap.merge (fun o o' ->
 438     match o' with
 439     | Types.None -> o
 440     | Types.Some x -> Types.None) (let s0 = s in s0) (let s1 = s' in s1)
 441
 442 (** val identifierSet : PreIdentifiers.identifierTag -> Setoids.setoid **)
 443 let identifierSet tag =
 444   Setoids.Mk_Setoid
 445
 446 (** val id_map_size :
 447     PreIdentifiers.identifierTag -> 'a1 identifier_map -> Nat.nat **)
 448 let id_map_size tag s =
 449   let p = s in PositiveMap.domain_size p
 450
 451 open Proper
 452
 453 (** val set_from_list :
 454     PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
 455     Types.unit0 identifier_map **)
 456 let set_from_list tag =
 457   Util.foldl (add_set tag) (empty_set tag)
 458
 459 (** val dpi1__o__id_set_from_list__o__inject :
 460     PreIdentifiers.identifierTag -> (PreIdentifiers.identifier List.list,
 461     'a1) Types.dPair -> Types.unit0 identifier_map Types.sig0 **)
 462 let dpi1__o__id_set_from_list__o__inject x0 x3 =
 463   set_from_list x0 x3.Types.dpi1
 464
 465 (** val eject__o__id_set_from_list__o__inject :
 466     PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list
 467     Types.sig0 -> Types.unit0 identifier_map Types.sig0 **)
 468 let eject__o__id_set_from_list__o__inject x0 x3 =
 469   set_from_list x0 (Types.pi1 x3)
 470
 471 (** val id_set_from_list__o__inject :
 472     PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
 473     Types.unit0 identifier_map Types.sig0 **)
 474 let id_set_from_list__o__inject x0 x2 =
 475   set_from_list x0 x2
 476
 477 (** val dpi1__o__id_set_from_list :
 478     PreIdentifiers.identifierTag -> (PreIdentifiers.identifier List.list,
 479     'a1) Types.dPair -> Types.unit0 identifier_map **)
 480 let dpi1__o__id_set_from_list x0 x2 =
 481   set_from_list x0 x2.Types.dpi1
 482
 483 (** val eject__o__id_set_from_list :
 484     PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list
 485     Types.sig0 -> Types.unit0 identifier_map **)
 486 let eject__o__id_set_from_list x0 x2 =
 487   set_from_list x0 (Types.pi1 x2)
 488
 489 (** val choose :
 490     PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 491     ((PreIdentifiers.identifier, 'a1) Types.prod, 'a1 identifier_map)
 492     Types.prod Types.option **)
 493 let choose tag m =
 494   match PositiveMap.pm_choose (let m' = m in m') with
 495   | Types.None -> Types.None
 496   | Types.Some x ->
 497     Types.Some { Types.fst = { Types.fst = x.Types.fst.Types.fst; Types.snd =
 498       x.Types.fst.Types.snd }; Types.snd = x.Types.snd }
 499
 500 (** val try_remove :
 501     PreIdentifiers.identifierTag -> 'a1 identifier_map ->
 502     PreIdentifiers.identifier -> ('a1, 'a1 identifier_map) Types.prod
 503     Types.option **)
 504 let try_remove tag m id =
 505   match PositiveMap.pm_try_remove (let id' = id in id') (let m' = m in m') with
 506   | Types.None -> Types.None
 507   | Types.Some x ->
 508     Types.Some { Types.fst = x.Types.fst; Types.snd = x.Types.snd }
 509
 510 (** val id_set_of_map :
 511     PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set **)
 512 let id_set_of_map tag m =
 513   PositiveMap.map (fun x -> Types.It) (let m' = m in m')
 514
 515 (** val set_of_list :
 516     PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
 517     identifier_set **)
 518 let set_of_list tag l =
 519   Util.foldl (fun s id -> add_set tag s id) (empty_set tag) l
 520
 521 (** val domain_of_map :
 522     PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set **)
 523 let domain_of_map tag m =
 524   PositiveMap.domain_of_pm (let m0 = m in m0)
 525