Univs: proper printing of global and local universe names (only

printing functions touched in the kernel).

Author: mattam82

dev/top_printers.ml

@@ -207,21 +207,22 @@ let ppuni u = pp(pr_uni u)
 let ppuni_level u = pp (Level.pr u)
 let ppuniverse u = pp (str"[" ++ Universe.pr u ++ str"]")
 
-let ppuniverse_set l = pp (LSet.pr l)
-let ppuniverse_instance l = pp (Instance.pr l)
-let ppuniverse_context l = pp (pr_universe_context l)
-let ppuniverse_context_set l = pp (pr_universe_context_set l)
+let prlev = Universes.pr_with_global_universes
+let ppuniverse_set l = pp (LSet.pr prlev l)
+let ppuniverse_instance l = pp (Instance.pr prlev l)
+let ppuniverse_context l = pp (pr_universe_context prlev l)
+let ppuniverse_context_set l = pp (pr_universe_context_set prlev l)
 let ppuniverse_subst l = pp (Univ.pr_universe_subst l)
 let ppuniverse_opt_subst l = pp (Universes.pr_universe_opt_subst l)
 let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst l)
 let ppevar_universe_context l = pp (Evd.pr_evar_universe_context l)
 let ppconstraints_map c = pp (Universes.pr_constraints_map c)
-let ppconstraints c = pp (pr_constraints c)
+let ppconstraints c = pp (pr_constraints Level.pr c)
 let ppuniverseconstraints c = pp (Universes.Constraints.pr c)
 let ppuniverse_context_future c = 
   let ctx = Future.force c in
     ppuniverse_context ctx
-let ppuniverses u = pp (Univ.pr_universes u)
+let ppuniverses u = pp (Univ.pr_universes Level.pr u)
 let ppnamedcontextval e =
   pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e))
 

interp/constrextern.ml

@@ -956,7 +956,7 @@ let extern_type goal_concl_style env sigma t =
   let r = Detyping.detype goal_concl_style avoid env sigma t in
   extern_glob_type (vars_of_env env) r
 
-let extern_sort s = extern_glob_sort (detype_sort s)
+let extern_sort sigma s = extern_glob_sort (detype_sort sigma s)
 
 let extern_closed_glob ?lax goal_concl_style env sigma t =
   let avoid = if goal_concl_style then ids_of_context env else [] in

interp/constrextern.mli

@@ -40,7 +40,7 @@ val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr
 val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr
 val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference
 val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
-val extern_sort : sorts -> glob_sort
+val extern_sort : Evd.evar_map -> sorts -> glob_sort
 val extern_rel_context : constr option -> env -> Evd.evar_map ->
   rel_context -> local_binder list
 

kernel/univ.ml

@@ -343,8 +343,8 @@ end
 module LSet = struct
   include LMap.Set
 
-  let pr s =
-    str"{" ++ prlist_with_sep spc Level.pr (elements s) ++ str"}"
+  let pr prl s =
+    str"{" ++ prlist_with_sep spc prl (elements s) ++ str"}"
 
   let of_array l =
     Array.fold_left (fun acc x -> add x acc) empty l
@@ -1265,10 +1265,10 @@ struct
   module S = Set.Make(UConstraintOrd)
   include S
 
-  let pr c =
+  let pr prl c =
     fold (fun (u1,op,u2) pp_std ->
-      pp_std ++  Level.pr u1 ++ pr_constraint_type op ++
-	Level.pr u2 ++ fnl () )  c (str "")
+      pp_std ++ prl u1 ++ pr_constraint_type op ++
+	prl u2 ++ fnl () )  c (str "")
 
 end
 
@@ -1641,7 +1641,7 @@ module Instance : sig
 
     val subst_fn : universe_level_subst_fn -> t -> t
 
-    val pr : t -> Pp.std_ppcmds
+    val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds
     val levels : t -> LSet.t
     val check_eq : t check_function 
 end = 
@@ -1718,7 +1718,7 @@ struct
   let levels x = LSet.of_array x
 
   let pr =
-    prvect_with_sep spc Level.pr
+    prvect_with_sep spc
 
   let equal t u = 
     t == u ||
@@ -1764,9 +1764,9 @@ struct
   let empty = (Instance.empty, Constraint.empty)
   let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst
 
-  let pr (univs, cst as ctx) =
+  let pr prl (univs, cst as ctx) =
     if is_empty ctx then mt() else
-      Instance.pr univs ++ str " |= " ++ v 0 (Constraint.pr cst)
+      Instance.pr prl univs ++ str " |= " ++ v 0 (Constraint.pr prl cst)
 
   let hcons (univs, cst) =
     (Instance.hcons univs, hcons_constraints cst)
@@ -1832,9 +1832,9 @@ struct
   let of_context (ctx, cst) =
     (Instance.levels ctx, cst)
 
-  let pr (univs, cst as ctx) =
+  let pr prl (univs, cst as ctx) =
     if is_empty ctx then mt() else
-      LSet.pr univs ++ str " |= " ++ v 0 (Constraint.pr cst)
+      LSet.pr prl univs ++ str " |= " ++ v 0 (Constraint.pr prl cst)
 
   let constraints (univs, cst) = cst
   let levels (univs, cst) = univs
@@ -1983,28 +1983,28 @@ let abstract_universes poly ctx =
 
 (** Pretty-printing *)
 
-let pr_arc = function
+let pr_arc prl = function
   | _, Canonical {univ=u; lt=[]; le=[]} ->
       mt ()
   | _, Canonical {univ=u; lt=lt; le=le} ->
       let opt_sep = match lt, le with
       | [], _ | _, [] -> mt ()
       | _ -> spc ()
       in
-      Level.pr u ++ str " " ++
+      prl u ++ str " " ++
       v 0
-        (pr_sequence (fun v -> str "< " ++ Level.pr v) lt ++
+        (pr_sequence (fun v -> str "< " ++ prl v) lt ++
 	 opt_sep ++
-         pr_sequence (fun v -> str "<= " ++ Level.pr v) le) ++
+         pr_sequence (fun v -> str "<= " ++ prl v) le) ++
       fnl ()
   | u, Equiv v ->
-      Level.pr u  ++ str " = " ++ Level.pr v ++ fnl ()
+      prl u  ++ str " = " ++ prl v ++ fnl ()
 
-let pr_universes g =
+let pr_universes prl g =
   let graph = UMap.fold (fun u a l -> (u,a)::l) g [] in
-  prlist pr_arc graph
+  prlist (pr_arc prl) graph
 
-let pr_constraints = Constraint.pr
+let pr_constraints prl = Constraint.pr prl
 
 let pr_universe_context = UContext.pr
 
@@ -2049,21 +2049,22 @@ let hcons_universe_context_set (v, c) =
 
 let hcons_univ x = Universe.hcons x
 
-let explain_universe_inconsistency (o,u,v,p) =
-    let pr_rel = function
-      | Eq -> str"=" | Lt -> str"<" | Le -> str"<=" 
-    in
-    let reason = match p with
-      | None | Some [] -> mt()
-      | Some p ->
-	str " because" ++ spc() ++ pr_uni v ++
-	  prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ pr_uni v)
-	  p ++
-	  (if Universe.equal (snd (List.last p)) u then mt() else
-	      (spc() ++ str "= " ++ pr_uni u)) 
-    in
-      str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++
-        pr_rel o ++ spc() ++ pr_uni v ++ reason ++ str")"
+let explain_universe_inconsistency prl (o,u,v,p) =
+  let pr_uni = Universe.pr_with prl in
+  let pr_rel = function
+    | Eq -> str"=" | Lt -> str"<" | Le -> str"<=" 
+  in
+  let reason = match p with
+    | None | Some [] -> mt()
+    | Some p ->
+      str " because" ++ spc() ++ pr_uni v ++
+	prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ pr_uni v)
+	p ++
+	(if Universe.equal (snd (List.last p)) u then mt() else
+	    (spc() ++ str "= " ++ pr_uni u)) 
+  in
+    str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++
+      pr_rel o ++ spc() ++ pr_uni v ++ reason ++ str")"
 
 let compare_levels = Level.compare
 let eq_levels = Level.equal

kernel/univ.mli

@@ -49,7 +49,7 @@ module LSet :
 sig 
   include CSig.SetS with type elt = universe_level
 
-  val pr : t -> Pp.std_ppcmds
+  val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds
   (** Pretty-printing *)
 end
 
@@ -292,7 +292,7 @@ sig
   val subst_fn : universe_level_subst_fn -> t -> t
   (** Substitution by a level-to-level function. *)
 
-  val pr : t -> Pp.std_ppcmds
+  val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds
   (** Pretty-printing, no comments *)
 
   val levels : t -> LSet.t
@@ -413,14 +413,16 @@ val instantiate_univ_constraints : universe_instance -> universe_context -> cons
 
 (** {6 Pretty-printing of universes. } *)
 
-val pr_universes : universes -> Pp.std_ppcmds
+val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds
 val pr_constraint_type : constraint_type -> Pp.std_ppcmds
-val pr_constraints : constraints -> Pp.std_ppcmds
-val pr_universe_context : universe_context -> Pp.std_ppcmds
-val pr_universe_context_set : universe_context_set -> Pp.std_ppcmds
+val pr_constraints : (Level.t -> Pp.std_ppcmds) -> constraints -> Pp.std_ppcmds
+val pr_universe_context : (Level.t -> Pp.std_ppcmds) -> universe_context -> Pp.std_ppcmds
+val pr_universe_context_set : (Level.t -> Pp.std_ppcmds) -> universe_context_set -> Pp.std_ppcmds
+val explain_universe_inconsistency : (Level.t -> Pp.std_ppcmds) -> 
+  univ_inconsistency -> Pp.std_ppcmds
+
 val pr_universe_level_subst : universe_level_subst -> Pp.std_ppcmds
 val pr_universe_subst : universe_subst -> Pp.std_ppcmds
-val explain_universe_inconsistency : univ_inconsistency -> Pp.std_ppcmds
 
 (** {6 Dumping to a file } *)
 

library/universes.ml

@@ -22,6 +22,9 @@ let global_universes = Summary.ref ~name:"Global universe names"
 let global_universe_names () = !global_universes
 let set_global_universe_names s = global_universes := s
 
+let pr_with_global_universes l = 
+  try Nameops.pr_id (LMap.find l (snd !global_universes))
+  with Not_found -> Level.pr l
 
 type universe_constraint_type = ULe | UEq | ULub
 

library/universes.mli

@@ -23,6 +23,8 @@ type universe_names =
 val global_universe_names : unit -> universe_names
 val set_global_universe_names : universe_names -> unit
 
+val pr_with_global_universes : Level.t -> Pp.std_ppcmds
+
 (** The global universe counter *)
 val set_remote_new_univ_level : universe_level RemoteCounter.installer
 

pretyping/detyping.ml

@@ -394,18 +394,13 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
       let eqnl = detype_eqns constructs constagsl bl in
       GCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
 
-let detype_sort = function
+let detype_sort sigma = function
   | Prop Null -> GProp
   | Prop Pos -> GSet
   | Type u ->
     GType
       (if !print_universes
-       then 
-	  let _, map = Universes.global_universe_names () in
-	  let pr_level u = 
-	    try Nameops.pr_id (Univ.LMap.find u map) with Not_found -> Univ.Level.pr u
-	  in 
-	    [Pp.string_of_ppcmds (Univ.Universe.pr_with pr_level u)]
+       then [Pp.string_of_ppcmds (Univ.Universe.pr_with (Evd.pr_evd_level sigma) u)]
        else [])
 
 type binder_kind = BProd | BLambda | BLetIn
@@ -416,12 +411,12 @@ type binder_kind = BProd | BLambda | BLetIn
 let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable"))
 let set_detype_anonymous f = detype_anonymous := f
 
-let detype_level l =
-  GType (Some (Pp.string_of_ppcmds (Univ.Level.pr l)))
+let detype_level sigma l =
+  GType (Some (Pp.string_of_ppcmds (Evd.pr_evd_level sigma l)))
 
-let detype_instance l = 
+let detype_instance sigma l = 
   if Univ.Instance.is_empty l then None
-  else Some (List.map detype_level (Array.to_list (Univ.Instance.to_array l)))
+  else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l)))
 
 let rec detype flags avoid env sigma t =
   match kind_of_term (collapse_appl t) with
@@ -439,7 +434,7 @@ let rec detype flags avoid env sigma t =
     | Var id ->
 	(try let _ = Global.lookup_named id in GRef (dl, VarRef id, None)
 	 with Not_found -> GVar (dl, id))
-    | Sort s -> GSort (dl,detype_sort s)
+    | Sort s -> GSort (dl,detype_sort sigma s)
     | Cast (c1,REVERTcast,c2) when not !Flags.raw_print ->
         detype flags avoid env sigma c1
     | Cast (c1,k,c2) ->
@@ -463,7 +458,7 @@ let rec detype flags avoid env sigma t =
       in
 	mkapp (detype flags avoid env sigma f)
 	  (Array.map_to_list (detype flags avoid env sigma) args)
-    | Const (sp,u) -> GRef (dl, ConstRef sp, detype_instance u)
+    | Const (sp,u) -> GRef (dl, ConstRef sp, detype_instance sigma u)
     | Proj (p,c) ->
       let noparams () = 
 	let pb = Environ.lookup_projection p (snd env) in
@@ -521,9 +516,9 @@ let rec detype flags avoid env sigma t =
         GEvar (dl,id,
                List.map (on_snd (detype flags avoid env sigma)) l)
     | Ind (ind_sp,u) ->
-	GRef (dl, IndRef ind_sp, detype_instance u)
+	GRef (dl, IndRef ind_sp, detype_instance sigma u)
     | Construct (cstr_sp,u) ->
-	GRef (dl, ConstructRef cstr_sp, detype_instance u)
+	GRef (dl, ConstructRef cstr_sp, detype_instance sigma u)
     | Case (ci,p,c,bl) ->
 	let comp = computable p (List.length (ci.ci_pp_info.ind_tags)) in
 	detype_case comp (detype flags avoid env sigma)

pretyping/detyping.mli

@@ -43,7 +43,7 @@ val detype_case :
   Id.t list -> inductive * case_style * bool list array * bool list ->
     constr option -> constr -> constr array -> glob_constr
 
-val detype_sort : sorts -> glob_sort
+val detype_sort : evar_map -> sorts -> glob_sort
 
 val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> 
   evar_map -> rel_context -> glob_decl list