From 20c98eab851210702b39e1c66e005acfc351d8dd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 1 Dec 2017 10:11:41 +0100
Subject: Proper nametab handling of global universe names

They are now bound at the library + module level and can be qualified
and shadowed according to the usual rules of qualified names.
Parsing and printing of universes "u+n" done as well.
In sections, global universes are discharged as well, checking that
they can be defined globally when they are introduced
---
 engine/termops.ml    |  1 +
 engine/termops.mli   |  2 ++
 engine/uState.ml     | 12 ++++++----
 engine/uState.mli    |  1 +
 engine/universes.ml  | 64 +++++++++++++++++++++++++++++++++++++++-------------
 engine/universes.mli | 20 ++++++++++++----
 6 files changed, 74 insertions(+), 26 deletions(-)

(limited to 'engine')

diff --git a/engine/termops.ml b/engine/termops.ml
index 07fe902220..a71bdff31e 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -288,6 +288,7 @@ let has_no_evar sigma =
   with Exit -> false
 
 let pr_evd_level evd = UState.pr_uctx_level (Evd.evar_universe_context evd)
+let reference_of_level evd l = UState.reference_of_level (Evd.evar_universe_context evd) l
 
 let pr_evar_universe_context ctx =
   let open UState in
diff --git a/engine/termops.mli b/engine/termops.mli
index c9a530076c..c1600abe80 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -271,6 +271,8 @@ val is_Prop : Evd.evar_map -> constr -> bool
 val is_Set : Evd.evar_map -> constr -> bool
 val is_Type : Evd.evar_map -> constr -> bool
 
+val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.reference
+
 (** Combinators on judgments *)
 
 val on_judgment       : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment
diff --git a/engine/uState.ml b/engine/uState.ml
index 4e30640e46..511d553284 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -263,13 +263,15 @@ let constrain_variables diff ctx =
   in
   { ctx with uctx_local = (univs, local); uctx_univ_variables = vars }
   
-
-let pr_uctx_level uctx = 
+let reference_of_level uctx =
   let map, map_rev = uctx.uctx_names in 
     fun l ->
-      try Id.print (Option.get (Univ.LMap.find l map_rev).uname)
+      try Libnames.Ident (Loc.tag @@ Option.get (Univ.LMap.find l map_rev).uname)
       with Not_found | Option.IsNone ->
-        Universes.pr_with_global_universes l
+        Universes.reference_of_level l
+
+let pr_uctx_level uctx l =
+  Libnames.pr_reference (reference_of_level uctx l)
 
 type universe_decl =
   (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
@@ -430,7 +432,7 @@ let emit_side_effects eff u =
 
 let new_univ_variable ?loc rigid name
   ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
-  let u = Universes.new_univ_level (Global.current_dirpath ()) in
+  let u = Universes.new_univ_level () in
   let ctx' = Univ.ContextSet.add_universe u ctx in
   let uctx', pred =
     match rigid with
diff --git a/engine/uState.mli b/engine/uState.mli
index 16fba41e06..2c39e85f77 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -154,3 +154,4 @@ val update_sigma_env : t -> Environ.env -> t
 (** {5 Pretty-printing} *)
 
 val pr_uctx_level : t -> Univ.Level.t -> Pp.t
+val reference_of_level : t -> Univ.Level.t -> Libnames.reference
diff --git a/engine/universes.ml b/engine/universes.ml
index 5ac1bc6857..93696b4ca8 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)
diff --git a/engine/universes.mli b/engine/universes.mli
index 1401c4ee8d..fc9278eb56 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -18,6 +18,13 @@ val is_set_minimization : unit -> bool
 (** Universes *)
 
 val pr_with_global_universes : Level.t -> Pp.t
+val reference_of_level : Level.t -> Libnames.reference
+
+(** Global universe information outside the kernel, to handle
+    polymorphic universes in sections that have to be discharged. *)
+val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
+
+val is_polymorphic : Level.t -> bool
 
 (** Local universe name <-> level mapping *)
 
@@ -40,14 +47,17 @@ val universe_binders_with_opt_names : Globnames.global_reference ->
   Univ.Level.t list -> univ_name_list option -> universe_binders
 
 (** The global universe counter *)
-val set_remote_new_univ_level : Level.t RemoteCounter.installer
+type universe_id = DirPath.t * int
+
+val set_remote_new_univ_id : universe_id RemoteCounter.installer
 
 (** Side-effecting functions creating new universe levels. *)
 
-val new_univ_level : DirPath.t -> Level.t
-val new_univ : DirPath.t -> Universe.t
-val new_Type : DirPath.t -> types
-val new_Type_sort : DirPath.t -> Sorts.t
+val new_univ_id : unit -> universe_id
+val new_univ_level : unit -> Level.t
+val new_univ : unit -> Universe.t
+val new_Type : unit -> types
+val new_Type_sort : unit -> Sorts.t
 
 val new_global_univ : unit -> Universe.t in_universe_context_set
 val new_sort_in_family : Sorts.family -> Sorts.t
-- 
cgit v1.2.3


From 4fcf1fa32ff395d6bd5f6ce4803eee18173c4d36 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 22 Nov 2017 18:39:34 +0100
Subject: Cleanup API for registering universe binders.

- Regularly declared for for polymorphic constants
- Declared globally for monomorphic constants.

  E.g mono@{i} := Type@{i} is printed as
  mono@{mono.i} := Type@{mono.i}.

  There can be a name clash if there's a module and a constant of the
  same name. It is detected and is an error if the constant is first
  but is not detected and the name for the constant not
  registered (??) if the constant comes second.

Accept VarRef when registering universe binders

Fix two problems found by Gaëtan where binders were not registered properly

Simplify API substantially by not passing around a substructure of an
already carrier-around structure in interpretation/declaration code of
constants and proofs

Fix an issue of the stronger restrict universe context + no evd leak

This is uncovered by not having an evd leak in interp_definition, and
the stronger restrict_universe_context. This patch could be backported
to 8.7, it could also be triggered by the previous restrict_context I
think.
---
 engine/eConstr.ml  | 18 ++++++++++++++++++
 engine/eConstr.mli |  4 ++++
 2 files changed, 22 insertions(+)

(limited to 'engine')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index afdceae061..ea098902a2 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -645,6 +645,24 @@ let eq_constr_universes_proj env sigma m n =
     let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in
     if res then Some !cstrs else None
 
+let universes_of_constr sigma c =
+  let open Univ in
+  let rec aux s c =
+    match kind sigma c with
+    | Const (_, u) | Ind (_, u) | Construct (_, u) ->
+      LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
+    | Sort u ->
+       let sort = ESorts.kind sigma u in
+       if Sorts.is_small sort then s
+       else
+         let u = Sorts.univ_of_sort sort in
+         LSet.fold LSet.add (Universe.levels u) s
+    | Evar (k, args) ->
+       let concl = Evd.evar_concl (Evd.find sigma k) in
+       fold sigma aux (aux s (of_constr concl)) c
+    | _ -> fold sigma aux s c
+  in aux LSet.empty c
+
 open Context
 open Environ
 
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index e9ef302cf6..3e6a13f709 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -201,6 +201,10 @@ val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a ->
 val iter_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
 val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
 
+(** Gather the universes transitively used in the term, including in the
+   type of evars appearing in it. *)
+val universes_of_constr : Evd.evar_map -> t -> Univ.LSet.t
+
 (** {6 Substitutions} *)
 
 module Vars :
-- 
cgit v1.2.3