Use Maps and ids for universe binders

Before sometimes there were lists and strings.

6 files changed, 36 insertions, 31 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 60bd6de2a..ca1196b94 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -802,7 +802,7 @@ let make_evar_universe_context e l =
   | Some us ->
       List.fold_left
         (fun uctx (loc,id) ->
-        fst (UState.new_univ_variable ?loc univ_rigid (Some (Id.to_string id)) uctx))
+        fst (UState.new_univ_variable ?loc univ_rigid (Some id) uctx))
         uctx us
 
 (****************************************)
diff --git a/engine/evd.mli b/engine/evd.mli
index 853a34bc4..36c399e98 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -502,12 +502,12 @@ val constrain_variables : Univ.LSet.t -> UState.t -> UState.t
 
 val evar_universe_context_of_binders :
   Universes.universe_binders -> UState.t
-							    
+
 val make_evar_universe_context : env -> (Id.t located) list option -> UState.t
-val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map							   
+val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
 (** Raises Not_found if not a name for a universe in this map. *)
-val universe_of_name : evar_map -> string -> Univ.Level.t
-val add_universe_name : evar_map -> string -> Univ.Level.t -> evar_map
+val universe_of_name : evar_map -> Id.t -> Univ.Level.t
+val add_universe_name : evar_map -> Id.t -> Univ.Level.t -> evar_map
 
 val add_constraints_context : UState.t -> 
   Univ.constraints -> UState.t
@@ -519,9 +519,9 @@ val normalize_evar_universe_context_variables : UState.t ->
 val normalize_evar_universe_context : UState.t -> 
   UState.t
 
-val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.Level.t
-val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.Universe.t
-val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Sorts.t
+val new_univ_level_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t
+val new_univ_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Universe.t
+val new_sort_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Sorts.t
 
 val add_global_univ : evar_map -> Univ.Level.t -> evar_map
 
diff --git a/engine/uState.ml b/engine/uState.ml
index 123b64314..498d73fd3 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -11,16 +11,16 @@ open CErrors
 open Util
 open Names
 
-module UNameMap = String.Map
+module UNameMap = Names.Id.Map
     
 type uinfo = {
-  uname : string option;
+  uname : Id.t option;
   uloc : Loc.t option;
 }
 
 (* 2nd part used to check consistency on the fly. *)
 type t =
- { uctx_names : Univ.Level.t UNameMap.t * uinfo Univ.LMap.t;
+ { uctx_names : Universes.universe_binders * uinfo Univ.LMap.t;
    uctx_local : Univ.ContextSet.t; (** The local context of variables *)
    uctx_univ_variables : Universes.universe_opt_subst;
    (** The local universes that are unification variables *)
@@ -107,10 +107,12 @@ let add_uctx_loc l loc (names, names_rev) =
 
 let of_binders b =
   let ctx = empty in
-  let names =
-    List.fold_left (fun acc (id, l) -> add_uctx_names (Id.to_string id) l acc)
-                   ctx.uctx_names b
-  in { ctx with uctx_names = names }
+  let rmap =
+    UNameMap.fold (fun id l rmap ->
+        Univ.LMap.add l { uname = Some id; uloc = None } rmap)
+      b Univ.LMap.empty
+  in
+  { ctx with uctx_names = b, rmap }
 
 let instantiate_variable l b v =
   try v := Univ.LMap.update l (Some b) !v
@@ -249,20 +251,20 @@ let constrain_variables diff ctx =
 let pr_uctx_level uctx = 
   let map, map_rev = uctx.uctx_names in 
     fun l ->
-      try str (Option.get (Univ.LMap.find l map_rev).uname)
+      try Id.print (Option.get (Univ.LMap.find l map_rev).uname)
       with Not_found | Option.IsNone ->
         Universes.pr_with_global_universes l
 
 type universe_decl =
   (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
 
-let universe_context ~names ~extensible ctx =
-  let levels = Univ.ContextSet.levels ctx.uctx_local in
+let universe_context ~names ~extensible uctx =
+  let levels = Univ.ContextSet.levels uctx.uctx_local in
   let newinst, left =
     List.fold_right
       (fun (loc,id) (newinst, acc) ->
          let l =
-           try UNameMap.find (Id.to_string id) (fst ctx.uctx_names)
+           try UNameMap.find id (fst uctx.uctx_names)
            with Not_found ->
              user_err ?loc ~hdr:"universe_context"
                (str"Universe " ++ Id.print id ++ str" is not bound anymore.")
@@ -274,23 +276,22 @@ let universe_context ~names ~extensible ctx =
     let loc =
       try
         let info =
-          Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in
+          Univ.LMap.find (Univ.LSet.choose left) (snd uctx.uctx_names) in
         info.uloc
       with Not_found -> None
     in
     user_err ?loc ~hdr:"universe_context"
       ((str(CString.plural n "Universe") ++ spc () ++
-	Univ.LSet.pr (pr_uctx_level ctx) left ++
+        Univ.LSet.pr (pr_uctx_level uctx) left ++
 	spc () ++ str (CString.conjugate_verb_to_be n) ++
         str" unbound."))
   else
     let left = Univ.ContextSet.sort_levels (Array.of_list (Univ.LSet.elements left)) in
     let inst = Array.append (Array.of_list newinst) left in
     let inst = Univ.Instance.of_array inst in
-    let map = List.map (fun (s,l) -> Id.of_string s, l) (UNameMap.bindings (fst ctx.uctx_names)) in
     let ctx = Univ.UContext.make (inst,
-                                  Univ.ContextSet.constraints ctx.uctx_local) in
-    map, ctx
+                                  Univ.ContextSet.constraints uctx.uctx_local) in
+    fst uctx.uctx_names, ctx
 
 let check_implication uctx cstrs ctx =
   let gr = initial_graph uctx in
diff --git a/engine/uState.mli b/engine/uState.mli
index f54bcc832..7f2357a68 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -71,10 +71,10 @@ val add_universe_constraints : t -> Universes.universe_constraints -> t
 
 (** {5 Names} *)
 
-val add_universe_name : t -> string -> Univ.Level.t -> t
+val add_universe_name : t -> Id.t -> Univ.Level.t -> t
 (** Associate a human-readable name to a local variable. *)
 
-val universe_of_name : t -> string -> Univ.Level.t
+val universe_of_name : t -> Id.t -> Univ.Level.t
 (** Retrieve the universe associated to the name. *)
 
 (** {5 Unification} *)
@@ -93,7 +93,7 @@ val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.ContextSet.t -> t
 val merge_subst : t -> Universes.universe_opt_subst -> t
 val emit_side_effects : Safe_typing.private_constants -> t -> t
 
-val new_univ_variable : ?loc:Loc.t -> rigid -> string option -> t -> t * Univ.Level.t
+val new_univ_variable : ?loc:Loc.t -> rigid -> Id.t option -> t -> t * Univ.Level.t
 val add_global_univ : t -> Univ.Level.t -> t
 
 (** [make_flexible_variable g algebraic l]
diff --git a/engine/universes.ml b/engine/universes.ml
index 6c1b64d74..459c53002 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -21,14 +21,16 @@ let pr_with_global_universes l =
 
 (** Local universe names of polymorphic references *)
 
-type universe_binders = (Id.t * Univ.Level.t) list
+type universe_binders = Univ.Level.t Names.Id.Map.t
+
+let empty_binders = Id.Map.empty
 
 let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders"
 
-let universe_binders_of_global ref =
+let universe_binders_of_global ref : universe_binders =
   try
     let l = Refmap.find ref !universe_binders_table in l
-  with Not_found -> []
+  with Not_found -> Names.Id.Map.empty
 
 let register_universe_binders ref l =
   universe_binders_table := Refmap.add ref l !universe_binders_table
diff --git a/engine/universes.mli b/engine/universes.mli
index a960099ed..621ca5e84 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -21,7 +21,9 @@ val pr_with_global_universes : Level.t -> Pp.t
 
 (** Local universe name <-> level mapping *)
 
-type universe_binders = (Id.t * Univ.Level.t) list
+type universe_binders = Univ.Level.t Names.Id.Map.t
+
+val empty_binders : universe_binders
 
 val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
 val universe_binders_of_global : Globnames.global_reference -> universe_binders