Merge PR #1033: Universe binder improvements

7 files changed, 105 insertions, 58 deletions

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index e897b1938..1a74538aa 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -41,6 +41,11 @@ open Decl_kinds
     pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
       pr_glob_level r
 
+  let pr_univ_name_list = function
+    | None -> mt ()
+    | Some l ->
+      str "@{" ++ prlist_with_sep spc pr_lname l ++ str"}"
+
   let pr_univdecl_instance l extensible =
     prlist_with_sep spc pr_lident l ++
     (if extensible then str"+" else mt ())
@@ -488,8 +493,8 @@ open Decl_kinds
         else "Print Universes"
       in
       keyword cmd ++ pr_opt str fopt
-    | PrintName qid ->
-      keyword "Print" ++ spc()  ++ pr_smart_global qid
+    | PrintName (qid,udecl) ->
+      keyword "Print" ++ spc()  ++ pr_smart_global qid ++ pr_univ_name_list udecl
     | PrintModuleType qid ->
       keyword "Print Module Type" ++ spc() ++ pr_reference qid
     | PrintModule qid ->
@@ -502,9 +507,9 @@ open Decl_kinds
       keyword "Print Scope" ++ spc() ++ str s
     | PrintVisibility s ->
       keyword "Print Visibility" ++ pr_opt str s
-    | PrintAbout (qid,gopt) ->
+    | PrintAbout (qid,l,gopt) ->
        pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt
-       ++ keyword "About" ++ spc()  ++ pr_smart_global qid
+       ++ keyword "About" ++ spc()  ++ pr_smart_global qid ++ pr_univ_name_list l
     | PrintImplicit qid ->
       keyword "Print Implicit" ++ spc()  ++ pr_smart_global qid
     (* spiwack: command printing all the axioms and section variables used in a
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 8fc00ed96..602b7a496 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -32,8 +32,8 @@ open Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
 type object_pr = {
-  print_inductive           : MutInd.t -> Pp.t;
-  print_constant_with_infos : Constant.t -> Pp.t;
+  print_inductive           : MutInd.t -> Universes.univ_name_list option -> Pp.t;
+  print_constant_with_infos : Constant.t -> Universes.univ_name_list option -> Pp.t;
   print_section_variable    : env -> Evd.evar_map -> variable -> Pp.t;
   print_syntactic_def       : env -> KerName.t -> Pp.t;
   print_module              : bool -> ModPath.t -> Pp.t;
@@ -68,7 +68,7 @@ let int_or_no n = if Int.equal n 0 then str "no" else int n
 
 let print_basename sp = pr_global (ConstRef sp)
 
-let print_ref reduce ref =
+let print_ref reduce ref udecl =
   let typ, ctx = Global.type_of_global_in_context (Global.env ()) ref in
   let typ = Vars.subst_instance_constr (Univ.AUContext.instance ctx) typ in
   let typ = EConstr.of_constr typ in
@@ -81,7 +81,8 @@ let print_ref reduce ref =
   let inst = Univ.AUContext.instance univs in
   let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
   let env = Global.env () in
-  let bl = Universes.universe_binders_of_global ref in
+  let bl = Universes.universe_binders_with_opt_names ref
+      (Array.to_list (Univ.Instance.to_array inst)) udecl in
   let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
   let inst =
     if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs
@@ -150,7 +151,7 @@ let print_impargs ref =
   let has_impl = not (List.is_empty impl) in
   (* Need to reduce since implicits are computed with products flattened *)
   pr_infos_list
-    ([ print_ref (need_expansion (select_impargs_size 0 impl) ref) ref;
+    ([ print_ref (need_expansion (select_impargs_size 0 impl) ref) ref None;
        blankline ] @
     (if has_impl then print_impargs_list (mt()) impl
      else [str "No implicit arguments"]))
@@ -256,7 +257,7 @@ let print_name_infos ref =
     if need_expansion (select_impargs_size 0 impls) ref then
       (* Need to reduce since implicits are computed with products flattened *)
       [str "Expanded type for implicit arguments";
-       print_ref true ref; blankline]
+       print_ref true ref None; blankline]
     else
       [] in
   print_polymorphism ref @
@@ -512,11 +513,11 @@ let assumptions_for_print lna =
 (*********************)
 (* *)
 
-let gallina_print_inductive sp =
+let gallina_print_inductive sp udecl =
   let env = Global.env() in
   let mib = Environ.lookup_mind sp env in
   let mipv = mib.mind_packets in
-  pr_mutual_inductive_body env sp mib ++
+  pr_mutual_inductive_body env sp mib udecl ++
   with_line_skip
     (print_primitive_record mib.mind_finite mipv mib.mind_record @
      print_inductive_renames sp mipv @
@@ -545,7 +546,7 @@ let print_instance sigma cb =
     pr_universe_instance sigma univs
   else mt()
 				
-let print_constant with_values sep sp =
+let print_constant with_values sep sp udecl =
   let cb = Global.lookup_constant sp in
   let val_0 = Global.body_of_constant_body cb in
   let typ =
@@ -555,31 +556,34 @@ let print_constant with_values sep sp =
       let inst = Univ.AUContext.instance univs in
       Vars.subst_instance_constr inst cb.const_type
   in
-  let univs =
+  let univs, ulist =
+    let open Entries in
+    let open Univ in
     let otab = Global.opaque_tables () in
     match cb.const_body with
     | Undef _ | Def _ ->
       begin
         match cb.const_universes with
-        | Monomorphic_const ctx -> ctx
+        | Monomorphic_const ctx -> Monomorphic_const_entry ctx, []
         | Polymorphic_const ctx ->
-          let inst = Univ.AUContext.instance ctx in
-          Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx)
+          let inst = AUContext.instance ctx in
+          Polymorphic_const_entry (UContext.make (inst, AUContext.instantiate inst ctx)),
+          Array.to_list (Instance.to_array inst)
       end
     | OpaqueDef o ->
       let body_uctxs = Opaqueproof.force_constraints otab o in
       match cb.const_universes with
       | Monomorphic_const ctx ->
-        let uctxs = Univ.ContextSet.of_context ctx in
-        Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs)
+        Monomorphic_const_entry (ContextSet.union body_uctxs ctx), []
       | Polymorphic_const ctx ->
-        assert(Univ.ContextSet.is_empty body_uctxs);
-        let inst = Univ.AUContext.instance ctx in
-        Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx)
+        assert(ContextSet.is_empty body_uctxs);
+        let inst = AUContext.instance ctx in
+        Polymorphic_const_entry (UContext.make (inst, AUContext.instantiate inst ctx)),
+        Array.to_list (Instance.to_array inst)
   in
   let ctx =
     Evd.evar_universe_context_of_binders
-      (Universes.universe_binders_of_global (ConstRef sp))
+      (Universes.universe_binders_with_opt_names (ConstRef sp) ulist udecl)
   in
   let env = Global.env () and sigma = Evd.from_ctx ctx in
   let pr_ltype = pr_ltype_env env sigma in
@@ -589,15 +593,15 @@ let print_constant with_values sep sp =
 	str"*** [ " ++
 	print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++
 	str" ]" ++
-	Printer.pr_universe_ctx sigma univs
+        Printer.pr_constant_universes sigma univs
     | Some (c, ctx) ->
         let c = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in
 	print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
 	(if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++
-        Printer.pr_universe_ctx sigma univs)
+        Printer.pr_constant_universes sigma univs)
 
-let gallina_print_constant_with_infos sp =
-  print_constant true " = " sp ++
+let gallina_print_constant_with_infos sp udecl =
+  print_constant true " = " sp udecl ++
   with_line_skip (print_name_infos (ConstRef sp))
 
 let gallina_print_syntactic_def env kn =
@@ -622,9 +626,9 @@ let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) =
              constraints *)
           (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None)
       | (_,"CONSTANT") ->
-	  Some (print_constant with_values sep (Constant.make1 kn))
+          Some (print_constant with_values sep (Constant.make1 kn) None)
       | (_,"INDUCTIVE") ->
-	  Some (gallina_print_inductive (MutInd.make1 kn))
+          Some (gallina_print_inductive (MutInd.make1 kn) None)
       | (_,"MODULE") ->
 	  let (mp,_,l) = KerName.repr kn in
 	    Some (print_module with_values (MPdot (mp,l)))
@@ -745,7 +749,7 @@ let print_full_pure_context env sigma =
       | "INDUCTIVE" ->
 	  let mind = Global.mind_of_delta_kn kn in
 	  let mib = Global.lookup_mind mind in
-	  pr_mutual_inductive_body (Global.env()) mind mib ++
+          pr_mutual_inductive_body (Global.env()) mind mib None ++
 	    str "." ++ fnl () ++ fnl ()
       | "MODULE" ->
 	  (* TODO: make it reparsable *)
@@ -792,10 +796,19 @@ let print_sec_context env sigma sec =
 let print_sec_context_typ env sigma sec =
   print_context env sigma false None (read_sec_context sec)
 
-let print_any_name env sigma = function
-  | Term (ConstRef sp) -> print_constant_with_infos sp
-  | Term (IndRef (sp,_)) -> print_inductive sp
-  | Term (ConstructRef ((sp,_),_)) -> print_inductive sp
+let maybe_error_reject_univ_decl na udecl =
+  match na, udecl with
+  | _, None | Term (ConstRef _ | IndRef _ | ConstructRef _), Some _ -> ()
+  | (Term (VarRef _) | Syntactic _ | Dir _ | ModuleType _ | Other _ | Undefined _), Some udecl ->
+    (* TODO Print na somehow *)
+    user_err ~hdr:"reject_univ_decl" (str "This object does not support universe names.")
+
+let print_any_name env sigma na udecl =
+  maybe_error_reject_univ_decl na udecl;
+  match na with
+  | Term (ConstRef sp) -> print_constant_with_infos sp udecl
+  | Term (IndRef (sp,_)) -> print_inductive sp udecl
+  | Term (ConstructRef ((sp,_),_)) -> print_inductive sp udecl
   | Term (VarRef sp) -> print_section_variable env sigma sp
   | Syntactic kn -> print_syntactic_def env kn
   | Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp
@@ -812,24 +825,26 @@ let print_any_name env sigma = function
     user_err
       ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
 
-let print_name env sigma = function
+let print_name env sigma na udecl =
+  match na with
   | ByNotation (loc,(ntn,sc)) ->
       print_any_name env sigma
         (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
                ntn sc))
+        udecl
   | AN ref ->
-      print_any_name env sigma (locate_any_name ref)
+      print_any_name env sigma (locate_any_name ref) udecl
 
 let print_opaque_name env sigma qid =
   match Nametab.global qid with
     | ConstRef cst ->
 	let cb = Global.lookup_constant cst in
         if Declareops.constant_has_body cb then
-	  print_constant_with_infos cst
+          print_constant_with_infos cst None
         else
 	  user_err Pp.(str "Not a defined constant.")
     | IndRef (sp,_) ->
-        print_inductive sp
+        print_inductive sp None
     | ConstructRef cstr as gr ->
 	let ty, ctx = Global.type_of_global_in_context env gr in
 	let inst = Univ.AUContext.instance ctx in
@@ -840,13 +855,14 @@ let print_opaque_name env sigma qid =
     | VarRef id ->
         env |> lookup_named id |> print_named_decl env sigma
 
-let print_about_any ?loc env sigma k =
+let print_about_any ?loc env sigma k udecl =
+  maybe_error_reject_univ_decl k udecl;
   match k with
   | Term ref ->
     let rb = Reductionops.ReductionBehaviour.print ref in
     Dumpglob.add_glob ?loc ref;
       pr_infos_list
-       (print_ref false ref :: blankline ::
+       (print_ref false ref udecl :: blankline ::
 	print_name_infos ref @
 	(if Pp.ismt rb then [] else [rb]) @
 	print_opacity ref @
@@ -862,13 +878,14 @@ let print_about_any ?loc env sigma k =
       hov 0 (pr_located_qualid k)
   | Other (obj, info) -> hov 0 (info.about obj)
 
-let print_about env sigma = function
+let print_about env sigma na udecl =
+  match na with
   | ByNotation (loc,(ntn,sc)) ->
       print_about_any ?loc env sigma
         (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
-               ntn sc))
+               ntn sc)) udecl
   | AN ref ->
-      print_about_any ?loc:(loc_of_reference ref) env sigma (locate_any_name ref)
+      print_about_any ?loc:(loc_of_reference ref) env sigma (locate_any_name ref) udecl
 
 (* for debug *)
 let inspect env sigma depth =
@@ -940,7 +957,7 @@ let print_canonical_projections env sigma =
 open Typeclasses
 
 let pr_typeclass env t =
-  print_ref false t.cl_impl
+  print_ref false t.cl_impl None
 
 let print_typeclasses () =
   let env = Global.env () in
@@ -949,7 +966,7 @@ let print_typeclasses () =
 let pr_instance env i =
   (*   gallina_print_constant_with_infos i.is_impl *)
   (* lighter *)
-  print_ref false (instance_impl i) ++
+  print_ref false (instance_impl i) None ++
   begin match hint_priority i with
   | None -> mt ()
   | Some i -> spc () ++ str "|" ++ spc () ++ int i
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 89099a043..8f3a6ddc4 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -31,9 +31,11 @@ val print_eval :
   reduction_function -> env -> Evd.evar_map ->
     Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
 
-val print_name : env -> Evd.evar_map -> reference or_by_notation -> Pp.t
+val print_name : env -> Evd.evar_map -> reference or_by_notation ->
+  Vernacexpr.univ_name_list option -> Pp.t
 val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t
-val print_about : env -> Evd.evar_map -> reference or_by_notation -> Pp.t
+val print_about : env -> Evd.evar_map -> reference or_by_notation ->
+  Vernacexpr.univ_name_list option -> Pp.t
 val print_impargs : reference or_by_notation -> Pp.t
 
 (** Pretty-printing functions for classes and coercions *)
@@ -80,8 +82,8 @@ val print_located_module : reference -> Pp.t
 val print_located_other : string -> reference -> Pp.t
 
 type object_pr = {
-  print_inductive           : MutInd.t -> Pp.t;
-  print_constant_with_infos : Constant.t -> Pp.t;
+  print_inductive           : MutInd.t -> Universes.univ_name_list option -> Pp.t;
+  print_constant_with_infos : Constant.t -> Universes.univ_name_list option -> Pp.t;
   print_section_variable    : env -> Evd.evar_map -> variable -> Pp.t;
   print_syntactic_def       : env -> KerName.t -> Pp.t;
   print_module              : bool -> ModPath.t -> Pp.t;
diff --git a/printing/printer.ml b/printing/printer.ml
index 3d40c104e..6a0597860 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -256,6 +256,13 @@ let safe_pr_constr t =
   let (sigma, env) = Pfedit.get_current_context () in
   safe_pr_constr_env env sigma t
 
+let pr_universe_ctx_set sigma c =
+  if !Detyping.print_universes && not (Univ.ContextSet.is_empty c) then
+    fnl()++pr_in_comment (fun c -> v 0
+      (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c)) c
+  else
+    mt()
+
 let pr_universe_ctx sigma c =
   if !Detyping.print_universes && not (Univ.UContext.is_empty c) then
     fnl()++pr_in_comment (fun c -> v 0 
@@ -263,6 +270,10 @@ let pr_universe_ctx sigma c =
   else
     mt()
 
+let pr_constant_universes sigma = function
+  | Entries.Monomorphic_const_entry ctx -> pr_universe_ctx_set sigma ctx
+  | Entries.Polymorphic_const_entry ctx -> pr_universe_ctx sigma ctx
+
 let pr_cumulativity_info sigma cumi =
   if !Detyping.print_universes 
   && not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then
diff --git a/printing/printer.mli b/printing/printer.mli
index 5adc0e858..9e8622c6e 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -121,6 +121,8 @@ val pr_polymorphic         : bool -> Pp.t
 val pr_cumulative          : bool -> bool -> Pp.t
 val pr_universe_instance   : evar_map -> Univ.UContext.t -> Pp.t
 val pr_universe_ctx        : evar_map -> Univ.UContext.t -> Pp.t
+val pr_universe_ctx_set    : evar_map -> Univ.ContextSet.t -> Pp.t
+val pr_constant_universes  : evar_map -> Entries.constant_universes_entry -> Pp.t
 val pr_cumulativity_info   : evar_map -> Univ.CumulativityInfo.t -> Pp.t
 
 (** Printing global references using names as short as possible *)
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 13a03e9b4..c34543bbd 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -121,7 +121,7 @@ let instantiate_cumulativity_info cumi =
   in
   CumulativityInfo.make (expose univs, expose subtyp)
 
-let print_mutual_inductive env mind mib =
+let print_mutual_inductive env mind mib udecl =
   let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
   in
   let keyword =
@@ -131,7 +131,14 @@ let print_mutual_inductive env mind mib =
     | BiFinite -> "Variant"
     | CoFinite -> "CoInductive"
   in
-  let bl = Universes.universe_binders_of_global (IndRef (mind, 0)) in
+  let univs =
+    let open Univ in
+    if Declareops.inductive_is_polymorphic mib then
+      Array.to_list (Instance.to_array
+                       (AUContext.instance (Declareops.inductive_polymorphic_context mib)))
+    else []
+  in
+  let bl = Universes.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in
   let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
   hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
          Printer.pr_cumulative
@@ -159,7 +166,7 @@ let get_fields =
   in
   prodec_rec [] []
 
-let print_record env mind mib =
+let print_record env mind mib udecl =
   let u = 
     if Declareops.inductive_is_polymorphic mib then 
       Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib)
@@ -173,7 +180,8 @@ let print_record env mind mib =
   let cstrtype = hnf_prod_applist env cstrtypes.(0) args in
   let fields = get_fields cstrtype in
   let envpar = push_rel_context params env in
-  let bl = Universes.universe_binders_of_global (IndRef (mind,0)) in
+  let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0))
+      (Array.to_list (Univ.Instance.to_array u)) udecl in
   let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
   let keyword =
     let open Decl_kinds in
@@ -205,11 +213,11 @@ let print_record env mind mib =
         sigma (instantiate_cumulativity_info cumi)
   )
 
-let pr_mutual_inductive_body env mind mib =
+let pr_mutual_inductive_body env mind mib udecl =
   if mib.mind_record <> None && not !Flags.raw_print then
-    print_record env mind mib
+    print_record env mind mib udecl
   else
-    print_mutual_inductive env mind mib
+    print_mutual_inductive env mind mib udecl
 
 (** Modpaths *)
 
@@ -335,7 +343,7 @@ let print_body is_impl env mp (l,body) =
     | SFBmind mib ->
       try
 	let env = Option.get env in
-	pr_mutual_inductive_body env (MutInd.make2 mp l) mib
+        pr_mutual_inductive_body env (MutInd.make2 mp l) mib None
       with e when CErrors.noncritical e ->
         let keyword =
           let open Decl_kinds in
diff --git a/printing/printmod.mli b/printing/printmod.mli
index b0bbb21e0..97ed063fe 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -11,6 +11,8 @@ open Names
 (** false iff the module is an element of an open module type *)
 val printable_body : DirPath.t -> bool
 
-val pr_mutual_inductive_body : Environ.env -> MutInd.t -> Declarations.mutual_inductive_body -> Pp.t
+val pr_mutual_inductive_body : Environ.env ->
+  MutInd.t -> Declarations.mutual_inductive_body ->
+  Vernacexpr.univ_name_list option -> Pp.t
 val print_module : bool -> ModPath.t -> Pp.t
 val print_modtype : ModPath.t -> Pp.t