diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 83 | ||||
| -rw-r--r-- | printing/prettyp.ml | 126 | ||||
| -rw-r--r-- | printing/prettyp.mli | 10 | ||||
| -rw-r--r-- | printing/printer.ml | 16 | ||||
| -rw-r--r-- | printing/printer.mli | 16 | ||||
| -rw-r--r-- | printing/printmod.ml | 30 | ||||
| -rw-r--r-- | printing/printmod.mli | 4 |
7 files changed, 161 insertions, 124 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 143f9ddcc5..46ef2ac031 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 ()) @@ -319,23 +324,18 @@ open Decl_kinds | SortClass -> keyword "Sortclass" | RefClass qid -> pr_smart_global qid - let pr_assumption_token many (l,a) = - let l = match l with Some x -> x | None -> Decl_kinds.Global in - match l, a with - | (Discharge,Logical) -> - keyword (if many then "Hypotheses" else "Hypothesis") - | (Discharge,Definitional) -> - keyword (if many then "Variables" else "Variable") - | (Global,Logical) -> + let pr_assumption_token many discharge kind = + match discharge, kind with + | (NoDischarge,Logical) -> keyword (if many then "Axioms" else "Axiom") - | (Global,Definitional) -> + | (NoDischarge,Definitional) -> keyword (if many then "Parameters" else "Parameter") - | (Local, Logical) -> - keyword (if many then "Local Axioms" else "Local Axiom") - | (Local,Definitional) -> - keyword (if many then "Local Parameters" else "Local Parameter") - | (Global,Conjectural) -> str"Conjecture" - | ((Discharge | Local),Conjectural) -> + | (NoDischarge,Conjectural) -> str"Conjecture" + | (DoDischarge,Logical) -> + keyword (if many then "Hypotheses" else "Hypothesis") + | (DoDischarge,Definitional) -> + keyword (if many then "Variables" else "Variable") + | (DoDischarge,Conjectural) -> anomaly (Pp.str "Don't know how to beautify a local conjecture.") let pr_params pr_c (xl,(c,t)) = @@ -447,7 +447,7 @@ open Decl_kinds | PrintGrammar ent -> keyword "Print Grammar" ++ spc() ++ str ent | PrintLoadPath dir -> - keyword "Print LoadPath" ++ pr_opt pr_dirpath dir + keyword "Print LoadPath" ++ pr_opt DirPath.print dir | PrintModules -> keyword "Print Modules" | PrintMLLoadPath -> @@ -488,8 +488,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 +502,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 @@ -518,7 +518,7 @@ open Decl_kinds in keyword cmd ++ spc() ++ pr_smart_global qid | PrintNamespace dp -> - keyword "Print Namespace" ++ pr_dirpath dp + keyword "Print Namespace" ++ DirPath.print dp | PrintStrategy None -> keyword "Print Strategies" | PrintStrategy (Some qid) -> @@ -626,7 +626,7 @@ open Decl_kinds return (keyword "Fail" ++ spc() ++ pr_vernac_body v) (* Syntax *) - | VernacOpenCloseScope (_,(opening,sc)) -> + | VernacOpenCloseScope (opening,sc) -> return ( keyword (if opening then "Open " else "Close ") ++ keyword "Scope" ++ spc() ++ str sc @@ -655,7 +655,7 @@ open Decl_kinds ++ spc() ++ pr_smart_global q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" ) - | VernacInfix (_,((_,s),mv),q,sn) -> (* A Verifier *) + | VernacInfix (((_,s),mv),q,sn) -> (* A Verifier *) return ( hov 0 (hov 0 (keyword "Infix " ++ qs s ++ str " :=" ++ pr_constrarg q) ++ @@ -664,7 +664,7 @@ open Decl_kinds | None -> mt() | Some sc -> spc() ++ str":" ++ spc() ++ str sc)) ) - | VernacNotation (_,c,((_,s),l),opt) -> + | VernacNotation (c,((_,s),l),opt) -> return ( hov 2 (keyword "Notation" ++ spc() ++ qs s ++ str " :=" ++ Flags.without_option Flags.beautify pr_constrarg c ++ pr_syntax_modifiers l ++ @@ -672,7 +672,7 @@ open Decl_kinds | None -> mt() | Some sc -> str" :" ++ spc() ++ str sc)) ) - | VernacSyntaxExtension (_, _,(s,l)) -> + | VernacSyntaxExtension (_, (s, l)) -> return ( keyword "Reserved Notation" ++ spc() ++ pr_located qs s ++ pr_syntax_modifiers l @@ -683,10 +683,9 @@ open Decl_kinds ) (* Gallina *) - | VernacDefinition (d,id,b) -> (* A verifier... *) - let pr_def_token (l,dk) = - let l = match l with Some x -> x | None -> Decl_kinds.Global in - keyword (Kindops.string_of_definition_kind (l,false,dk)) + | VernacDefinition ((discharge,kind),id,b) -> (* A verifier... *) + let pr_def_token dk = + keyword (Kindops.string_of_definition_object_kind dk) in let pr_reduce = function | None -> mt() @@ -707,7 +706,7 @@ open Decl_kinds let (binds,typ,c) = pr_def_body b in return ( hov 2 ( - pr_def_token d ++ spc() + pr_def_token kind ++ spc() ++ pr_ident_decl id ++ binds ++ typ ++ (match c with | None -> mt() @@ -732,13 +731,13 @@ open Decl_kinds ) | VernacExactProof c -> return (hov 2 (keyword "Proof" ++ pr_lconstrarg c)) - | VernacAssumption (stre,t,l) -> + | VernacAssumption ((discharge,kind),t,l) -> let n = List.length (List.flatten (List.map fst (List.map snd l))) in let pr_params (c, (xl, t)) = hov 2 (prlist_with_sep sep pr_ident_decl xl ++ spc() ++ (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr t)) in let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in - return (hov 2 (pr_assumption_token (n > 1) stre ++ + return (hov 2 (pr_assumption_token (n > 1) discharge kind ++ pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions)) | VernacInductive (cum, p,f,l) -> let pr_constructor (coe,(id,c)) = @@ -788,9 +787,8 @@ open Decl_kinds | VernacFixpoint (local, recs) -> let local = match local with - | Some Discharge -> "Let " - | Some Local -> "Local " - | None | Some Global -> "" + | DoDischarge -> "Let " + | NoDischarge -> "" in return ( hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++ @@ -800,9 +798,8 @@ open Decl_kinds | VernacCoFixpoint (local, corecs) -> let local = match local with - | Some Discharge -> keyword "Let" ++ spc () - | Some Local -> keyword "Local" ++ spc () - | None | Some Global -> str "" + | DoDischarge -> keyword "Let" ++ spc () + | NoDischarge -> str "" in let pr_onecorec ((iddecl,bl,c,def),ntn) = pr_ident_decl iddecl ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++ @@ -863,14 +860,14 @@ open Decl_kinds return ( keyword "Canonical Structure" ++ spc() ++ pr_smart_global q ) - | VernacCoercion (_,id,c1,c2) -> + | VernacCoercion (id,c1,c2) -> return ( hov 1 ( keyword "Coercion" ++ spc() ++ pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2) ) - | VernacIdentityCoercion (_,id,c1,c2) -> + | VernacIdentityCoercion (id,c1,c2) -> return ( hov 1 ( keyword "Identity Coercion" ++ spc() ++ pr_lident id ++ @@ -964,7 +961,7 @@ open Decl_kinds keyword "LoadPath" ++ spc() ++ qs s ++ (match d with | None -> mt() - | Some dir -> spc() ++ keyword "as" ++ spc() ++ pr_dirpath dir)) + | Some dir -> spc() ++ keyword "as" ++ spc() ++ DirPath.print dir)) ) | VernacRemoveLoadPath s -> return (keyword "Remove LoadPath" ++ qs s) @@ -994,9 +991,9 @@ open Decl_kinds prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++ pr_opt_hintbases dbnames) ) - | VernacHints (_, dbnames,h) -> + | VernacHints (dbnames,h) -> return (pr_hints dbnames h pr_constr pr_constr_pattern_expr) - | VernacSyntacticDefinition (id,(ids,c),_,compat) -> + | VernacSyntacticDefinition (id,(ids,c),compat) -> return ( hov 2 (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++ diff --git a/printing/prettyp.ml b/printing/prettyp.ml index e2d23ce7b0..1eb2c31c88 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -15,7 +15,6 @@ open CErrors open Util open Names open Nameops -open Term open Termops open Declarations open Environ @@ -33,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; @@ -69,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 @@ -82,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 @@ -139,7 +139,7 @@ let print_renames_list prefix l = let need_expansion impl ref = let typ, _ = Global.type_of_global_in_context (Global.env ()) ref in - let ctx = prod_assum typ in + let ctx = Term.prod_assum typ in let nprods = List.count is_local_assum ctx in not (List.is_empty impl) && List.length impl >= nprods && let _,lastimpl = List.chop nprods impl in @@ -151,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"])) @@ -257,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 @ @@ -360,13 +360,13 @@ let pr_located_qualid = function str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn) | Dir dir -> let s,dir = match dir with - | DirOpenModule (dir,_) -> "Open Module", dir - | DirOpenModtype (dir,_) -> "Open Module Type", dir - | DirOpenSection (dir,_) -> "Open Section", dir - | DirModule (dir,_) -> "Module", dir + | DirOpenModule { obj_dir ; _ } -> "Open Module", obj_dir + | DirOpenModtype { obj_dir ; _ } -> "Open Module Type", obj_dir + | DirOpenSection { obj_dir ; _ } -> "Open Section", obj_dir + | DirModule { obj_dir ; _ } -> "Module", obj_dir | DirClosedSection dir -> "Closed Section", dir in - str s ++ spc () ++ pr_dirpath dir + str s ++ spc () ++ DirPath.print dir | ModuleType mp -> str "Module Type" ++ spc () ++ pr_path (Nametab.path_of_modtype mp) | Other (obj, info) -> info.name obj @@ -410,7 +410,7 @@ let locate_term qid = let locate_module qid = let all = Nametab.locate_extended_all_dir qid in let map dir = match dir with - | DirModule (_, (mp, _)) -> Some (Dir dir, Nametab.shortest_qualid_of_module mp) + | DirModule { obj_mp ; _ } -> Some (Dir dir, Nametab.shortest_qualid_of_module obj_mp) | DirOpenModule _ -> Some (Dir dir, qid) | _ -> None in @@ -490,7 +490,7 @@ let gallina_print_typed_value_in_env env sigma (trm,typ) = let print_named_def env sigma name body typ = let pbody = pr_lconstr_env env sigma body in let ptyp = pr_ltype_env env sigma typ in - let pbody = if isCast body then surround pbody else pbody in + let pbody = if Constr.isCast body then surround pbody else pbody in (str "*** [" ++ str name ++ str " " ++ hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++ str ":" ++ brk (1,2) ++ ptyp) ++ @@ -513,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 @ @@ -546,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 = @@ -556,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 @@ -590,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 = @@ -623,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))) @@ -646,8 +649,8 @@ let gallina_print_library_entry env sigma with_values ent = Some (str " >>>>>>> Section " ++ pr_name oname) | (oname,Lib.ClosedSection _) -> Some (str " >>>>>>> Closed Section " ++ pr_name oname) - | (_,Lib.CompilingLibrary (dir,_)) -> - Some (str " >>>>>>> Library " ++ pr_dirpath dir) + | (_,Lib.CompilingLibrary { obj_dir; _ }) -> + Some (str " >>>>>>> Library " ++ DirPath.print obj_dir) | (oname,Lib.OpenedModule _) -> Some (str " >>>>>>> Module " ++ pr_name oname) | (oname,Lib.ClosedModule _) -> @@ -746,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 *) @@ -776,8 +779,8 @@ let read_sec_context r = with Not_found -> user_err ?loc ~hdr:"read_sec_context" (str "Unknown section.") in let rec get_cxt in_cxt = function - | (_,Lib.OpenedSection ((dir',_),_) as hd)::rest -> - if DirPath.equal dir dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest + | (_,Lib.OpenedSection ({obj_dir;_},_) as hd)::rest -> + if DirPath.equal dir obj_dir then (hd::in_cxt) else get_cxt (hd::in_cxt) rest | (_,Lib.ClosedSection _)::rest -> user_err Pp.(str "Cannot print the contents of a closed section.") (* LEM: Actually, we could if we wanted to. *) @@ -793,13 +796,22 @@ 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 + | Dir (DirModule { obj_dir; obj_mp; _ } ) -> print_module (printable_body obj_dir) obj_mp | Dir _ -> mt () | ModuleType mp -> print_modtype mp | Other (obj, info) -> info.print obj @@ -813,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 @@ -841,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 @ @@ -863,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 = @@ -941,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 @@ -950,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 89099a043f..8f3a6ddc47 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 377a6b4e12..6a0597860c 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -10,7 +10,6 @@ open Pp open CErrors open Util open Names -open Term open Constr open Environ open Globnames @@ -257,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 @@ -264,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 @@ -584,7 +594,7 @@ let default_pr_subgoal n sigma = in prrec n -let pr_internal_existential_key ev = str (string_of_existential ev) +let pr_internal_existential_key ev = Evar.print ev let print_evar_constraints gl sigma = let pr_env = @@ -763,7 +773,7 @@ let default_pr_subgoals ?(pr_first=true) type printer_pr = { - pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t; + pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t; pr_subgoal : int -> evar_map -> goal list -> Pp.t; pr_goal : goal sigma -> Pp.t; } diff --git a/printing/printer.mli b/printing/printer.mli index e014baa2cd..36ca1bdcca 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 *) @@ -129,7 +131,7 @@ val pr_global_env : Id.Set.t -> global_reference -> Pp.t val pr_global : global_reference -> Pp.t val pr_constant : env -> Constant.t -> Pp.t -val pr_existential_key : evar_map -> existential_key -> Pp.t +val pr_existential_key : evar_map -> Evar.t -> Pp.t val pr_existential : env -> evar_map -> existential -> Pp.t val pr_constructor : env -> constructor -> Pp.t val pr_inductive : env -> inductive -> Pp.t @@ -178,15 +180,15 @@ val pr_goal : goal sigma -> Pp.t focused goals unless the conrresponding option [enable_unfocused_goal_printing] is set. [seeds] is for printing dependent evars (mainly for emacs proof tree mode). *) -val pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list +val pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t val pr_subgoal : int -> evar_map -> goal list -> Pp.t val pr_concl : int -> evar_map -> goal -> Pp.t -val pr_open_subgoals : proof:Proof.proof -> Pp.t -val pr_nth_open_subgoal : proof:Proof.proof -> int -> Pp.t -val pr_evar : evar_map -> (evar * evar_info) -> Pp.t +val pr_open_subgoals : proof:Proof.t -> Pp.t +val pr_nth_open_subgoal : proof:Proof.t -> int -> Pp.t +val pr_evar : evar_map -> (Evar.t * evar_info) -> Pp.t val pr_evars_int : evar_map -> int -> evar_info Evar.Map.t -> Pp.t val pr_evars : evar_map -> evar_info Evar.Map.t -> Pp.t val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map -> @@ -218,10 +220,10 @@ module ContextObjectMap : CMap.ExtS val pr_assumptionset : env -> types ContextObjectMap.t -> Pp.t -val pr_goal_by_id : proof:Proof.proof -> Id.t -> Pp.t +val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t type printer_pr = { - pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t; + pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t; pr_subgoal : int -> evar_map -> goal list -> Pp.t; pr_goal : goal sigma -> Pp.t; } diff --git a/printing/printmod.ml b/printing/printmod.ml index 13a03e9b48..05292b06ba 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 *) @@ -237,10 +245,10 @@ let print_kn locals kn = with Not_found -> print_modpath locals kn -let nametab_register_dir mp = +let nametab_register_dir obj_mp = let id = mk_fake_top () in - let dir = DirPath.make [id] in - Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,DirPath.empty))) + let obj_dir = DirPath.make [id] in + Nametab.push_dir (Nametab.Until 1) obj_dir (DirModule { obj_dir; obj_mp; obj_sec = DirPath.empty }) (** Nota: the [global_reference] we register in the nametab below might differ from internal ones, since we cannot recreate here @@ -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 b0bbb21e05..97ed063fe3 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 |