diff options
Diffstat (limited to 'engine/universes.ml')
| -rw-r--r-- | engine/universes.ml | 72 |
1 files changed, 52 insertions, 20 deletions
diff --git a/engine/universes.ml b/engine/universes.ml index 5ac1bc685..30490ec56 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -14,10 +14,37 @@ open Constr open Environ open Univ open Globnames - -let pr_with_global_universes l = - try Id.print (LMap.find l (snd (Global.global_universe_names ()))) - with Not_found -> Level.pr l +open Nametab + +let reference_of_level l = + match Level.name l with + | Some (d, n as na) -> + let qid = + try Nametab.shortest_qualid_of_universe na + with Not_found -> + let name = Id.of_string_soft (string_of_int n) in + Libnames.make_qualid d name + in Libnames.Qualid (Loc.tag @@ qid) + | None -> Libnames.Ident (Loc.tag @@ Id.of_string_soft (Level.to_string l)) + +let pr_with_global_universes l = Libnames.pr_reference (reference_of_level l) + +(** Global universe information outside the kernel, to handle + polymorphic universe names in sections that have to be discharged. *) + +let universe_map = (Summary.ref UnivIdMap.empty ~name:"global universe info" : bool Nametab.UnivIdMap.t ref) + +let add_global_universe u p = + match Level.name u with + | Some n -> universe_map := Nametab.UnivIdMap.add n p !universe_map + | None -> () + +let is_polymorphic l = + match Level.name l with + | Some n -> + (try Nametab.UnivIdMap.find n !universe_map + with Not_found -> false) + | None -> false (** Local universe names of polymorphic references *) @@ -53,12 +80,14 @@ let ubinder_obj : Globnames.global_reference * universe_binders -> Libobject.obj rebuild_function = (fun x -> x); } let register_universe_binders ref ubinders = - (* Add the polymorphic (section) universes *) let open Names in - let ubinders = Id.Map.fold (fun id (poly,lvl) ubinders -> - if poly then Id.Map.add id lvl ubinders - else ubinders) - (fst (Global.global_universe_names ())) ubinders + (* Add the polymorphic (section) universes *) + let ubinders = UnivIdMap.fold (fun lvl poly ubinders -> + let qid = Nametab.shortest_qualid_of_universe lvl in + let level = Level.make (fst lvl) (snd lvl) in + if poly then Id.Map.add (snd (Libnames.repr_qualid qid)) level ubinders + else ubinders) + !universe_map ubinders in if not (Id.Map.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders)) @@ -236,14 +265,17 @@ let eq_constr_universes_proj env m n = res, !cstrs (* Generator of levels *) -let new_univ_level, set_remote_new_univ_level = +type universe_id = DirPath.t * int + +let new_univ_id, set_remote_new_univ_id = RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1) - ~build:(fun n -> Univ.Level.make (Global.current_dirpath ()) n) + ~build:(fun n -> Global.current_dirpath (), n) -let new_univ_level _ = new_univ_level () - (* Univ.Level.make db (new_univ_level ()) *) +let new_univ_level () = + let dp, id = new_univ_id () in + Univ.Level.make dp id -let fresh_level () = new_univ_level (Global.current_dirpath ()) +let fresh_level () = new_univ_level () (* TODO: remove *) let new_univ dp = Univ.Universe.make (new_univ_level dp) @@ -251,7 +283,7 @@ let new_Type dp = mkType (new_univ dp) let new_Type_sort dp = Type (new_univ dp) let fresh_universe_instance ctx = - let init _ = new_univ_level (Global.current_dirpath ()) in + let init _ = new_univ_level () in Instance.of_array (Array.init (AUContext.size ctx) init) let fresh_instance_from_context ctx = @@ -262,7 +294,7 @@ let fresh_instance_from_context ctx = let fresh_instance ctx = let ctx' = ref LSet.empty in let init _ = - let u = new_univ_level (Global.current_dirpath ()) in + let u = new_univ_level () in ctx' := LSet.add u !ctx'; u in let inst = Instance.of_array (Array.init (AUContext.size ctx) init) @@ -459,7 +491,7 @@ module LevelUnionFind = Unionfind.Make (Univ.LSet) (Univ.LMap) let add_list_map u t map = try let l = LMap.find u map in - LMap.update u (t :: l) map + LMap.set u (t :: l) map with Not_found -> LMap.add u [t] map @@ -552,7 +584,7 @@ let normalize_univ_variable_subst subst = let find l = Univ.LMap.find l !subst in let update l b = assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); - try subst := Univ.LMap.update l b !subst; b with Not_found -> assert false in + try subst := Univ.LMap.set l b !subst; b with Not_found -> assert false in normalize_univ_variable ~find ~update let normalize_universe_opt_subst subst = @@ -914,8 +946,8 @@ let normalize_context_set ctx us algs = let us = normalize_opt_subst us in (us, algs), (ctx', Constraint.union noneqs eqs) -(* let normalize_conkey = Profile.declare_profile "normalize_context_set" *) -(* let normalize_context_set a b c = Profile.profile3 normalize_conkey normalize_context_set a b c *) +(* let normalize_conkey = CProfile.declare_profile "normalize_context_set" *) +(* let normalize_context_set a b c = CProfile.profile3 normalize_conkey normalize_context_set a b c *) let is_trivial_leq (l,d,r) = Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r)) |