diff options
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 507 |
1 files changed, 306 insertions, 201 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index e117f1dc..1f17d844 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Changed by (and thus parts copyright ©) by Lionel Elie Mamane <lionel@mamane.lu> @@ -13,9 +15,9 @@ open Pp open CErrors open Util +open CAst open Names open Nameops -open Term open Termops open Declarations open Environ @@ -27,19 +29,23 @@ open Recordops open Misctypes open Printer open Printmod +open Context.Rel.Declaration + +(* module RelDecl = Context.Rel.Declaration *) +module NamedDecl = Context.Named.Declaration type object_pr = { - print_inductive : mutual_inductive -> std_ppcmds; - print_constant_with_infos : constant -> std_ppcmds; - print_section_variable : variable -> std_ppcmds; - print_syntactic_def : kernel_name -> std_ppcmds; - print_module : bool -> Names.module_path -> std_ppcmds; - print_modtype : module_path -> std_ppcmds; - print_named_decl : Context.Named.Declaration.t -> std_ppcmds; - print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; - print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; - print_typed_value_in_env : Environ.env -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds; - print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds; + 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; + print_modtype : ModPath.t -> Pp.t; + print_named_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Pp.t; + print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; + print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; + print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; + print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } let gallina_print_module = print_module @@ -65,28 +71,42 @@ 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 typ = Global.type_of_global_unsafe ref in +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 let typ = if reduce then let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ - in it_mkProd_or_LetIn ccl ctx + in EConstr.it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in + let variance = match ref with + | VarRef _ | ConstRef _ -> None + | IndRef (ind,_) | ConstructRef ((ind,_),_) -> + let mind = Environ.lookup_mind ind (Global.env ()) in + begin match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> None + | Declarations.Cumulative_ind cumi -> Some (Univ.ACumulativityInfo.variance cumi) + end + in + 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 sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) 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 (UState.of_binders bl) in let inst = if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs else mt () in - hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype_env env sigma typ ++ - Printer.pr_universe_ctx sigma univs) + hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ + Printer.pr_universe_ctx sigma ?variance univs) (********************************) (** Printing implicit arguments *) -let pr_impl_name imp = pr_id (name_of_implicit imp) +let pr_impl_name imp = Id.print (name_of_implicit imp) let print_impargs_by_name max = function | [] -> [] @@ -127,12 +147,11 @@ let print_impargs_list prefix l = let print_renames_list prefix l = if List.is_empty l then [] else [add_colon prefix ++ str "Arguments are renamed to " ++ - hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map pr_name l))] + hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map Name.print l))] let need_expansion impl ref = - let typ = Global.type_of_global_unsafe ref in - let ctx = prod_assum typ in - let open Context.Rel.Declaration in + let typ, _ = Global.type_of_global_in_context (Global.env ()) ref 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 @@ -144,7 +163,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"])) @@ -170,9 +189,8 @@ type opacity = | TransparentMaybeOpacified of Conv_oracle.level let opacity env = - let open Context.Named.Declaration in function - | VarRef v when is_local_def (Environ.lookup_named v env) -> + | VarRef v when NamedDecl.is_local_def (Environ.lookup_named v env) -> Some(TransparentMaybeOpacified (Conv_oracle.get_strategy (Environ.oracle env) (VarKey v))) | ConstRef cst -> @@ -202,6 +220,11 @@ let print_opacity ref = str "transparent (with minimal expansion weight)"] (*******************) + +let print_if_is_coercion ref = + if Classops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else [] + +(*******************) (* *) let print_polymorphism ref = @@ -224,10 +247,10 @@ let print_type_in_type ref = let print_primitive_record recflag mipv = function | Some (Some (_, ps,_)) -> let eta = match recflag with - | Decl_kinds.CoFinite | Decl_kinds.Finite -> str" without eta conversion" - | Decl_kinds.BiFinite -> str " with eta conversion" + | CoFinite | Finite -> str" without eta conversion" + | BiFinite -> str " with eta conversion" in - [pr_id mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."] + [Id.print mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."] | _ -> [] let print_primitive ref = @@ -246,7 +269,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 @ @@ -255,11 +278,12 @@ let print_name_infos ref = type_info_for_implicit @ print_renames_list (mt()) renames @ print_impargs_list (mt()) impls @ - print_argument_scopes (mt()) scopes + print_argument_scopes (mt()) scopes @ + print_if_is_coercion ref let print_id_args_data test pr id l = if List.exists test l then - pr (str "For " ++ pr_id id) l + pr (str "For " ++ Id.print id) l else [] @@ -292,16 +316,35 @@ let print_inductive_argument_scopes = (*********************) (* "Locate" commands *) +type 'a locatable_info = { + locate : qualid -> 'a option; + locate_all : qualid -> 'a list; + shortest_qualid : 'a -> qualid; + name : 'a -> Pp.t; + print : 'a -> Pp.t; + about : 'a -> Pp.t; +} + +type locatable = Locatable : 'a locatable_info -> locatable + type logical_name = | Term of global_reference | Dir of global_dir_reference - | Syntactic of kernel_name - | ModuleType of module_path - | Tactic of Nametab.ltac_constant + | Syntactic of KerName.t + | ModuleType of ModPath.t + | Other : 'a * 'a locatable_info -> logical_name | Undefined of qualid +(** Generic table for objects that are accessible through a name. *) +let locatable_map : locatable String.Map.t ref = ref String.Map.empty + +let register_locatable name f = + locatable_map := String.Map.add name (Locatable f) !locatable_map + +exception ObjFound of logical_name + let locate_any_name ref = - let (loc,qid) = qualid_of_reference ref in + let {v=qid} = qualid_of_reference ref in try Term (Nametab.locate qid) with Not_found -> try Syntactic (Nametab.locate_syndef qid) @@ -309,7 +352,13 @@ let locate_any_name ref = try Dir (Nametab.locate_dir qid) with Not_found -> try ModuleType (Nametab.locate_modtype qid) - with Not_found -> Undefined qid + with Not_found -> + let iter _ (Locatable info) = match info.locate qid with + | None -> () + | Some ans -> raise (ObjFound (Other (ans, info))) + in + try String.Map.iter iter !locatable_map; Undefined qid + with ObjFound obj -> obj let pr_located_qualid = function | Term ref -> @@ -323,17 +372,16 @@ 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) - | Tactic kn -> - str "Ltac" ++ spc () ++ pr_path (Nametab.path_of_tactic kn) + | Other (obj, info) -> info.name obj | Undefined qid -> pr_qualid qid ++ spc () ++ str "not a defined object." @@ -371,14 +419,10 @@ let locate_term qid = in List.map expand (Nametab.locate_extended_all qid) -let locate_tactic qid = - let all = Nametab.locate_extended_all_tactic qid in - List.map (fun kn -> (Tactic kn, Nametab.shortest_qualid_of_tactic kn)) all - 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 @@ -396,18 +440,35 @@ let locate_modtype qid = in modtypes @ List.map_filter map all +let locate_other s qid = + let Locatable info = String.Map.find s !locatable_map in + let ans = info.locate_all qid in + let map obj = (Other (obj, info), info.shortest_qualid obj) in + List.map map ans + +type locatable_kind = +| LocTerm +| LocModule +| LocOther of string +| LocAny + let print_located_qualid name flags ref = - let (loc,qid) = qualid_of_reference ref in - let located = [] in - let located = if List.mem `LTAC flags then locate_tactic qid @ located else located in - let located = if List.mem `MODTYPE flags then locate_modtype qid @ located else located in - let located = if List.mem `MODULE flags then locate_module qid @ located else located in - let located = if List.mem `TERM flags then locate_term qid @ located else located in + let {v=qid} = qualid_of_reference ref in + let located = match flags with + | LocTerm -> locate_term qid + | LocModule -> locate_modtype qid @ locate_module qid + | LocOther s -> locate_other s qid + | LocAny -> + locate_term qid @ + locate_modtype qid @ + locate_module qid @ + String.Map.fold (fun s _ accu -> locate_other s qid @ accu) !locatable_map [] + in match located with | [] -> let (dir,id) = repr_qualid qid in if DirPath.is_empty dir then - str "No " ++ str name ++ str " of basename" ++ spc () ++ pr_id id + str "No " ++ str name ++ str " of basename" ++ spc () ++ Id.print id else str "No " ++ str name ++ str " of suffix" ++ spc () ++ pr_qualid qid | l -> @@ -420,43 +481,43 @@ let print_located_qualid name flags ref = else mt ()) ++ display_alias o)) l -let print_located_term ref = print_located_qualid "term" [`TERM] ref -let print_located_tactic ref = print_located_qualid "tactic" [`LTAC] ref -let print_located_module ref = print_located_qualid "module" [`MODULE; `MODTYPE] ref -let print_located_qualid ref = print_located_qualid "object" [`TERM; `LTAC; `MODULE; `MODTYPE] ref +let print_located_term ref = print_located_qualid "term" LocTerm ref +let print_located_other s ref = print_located_qualid s (LocOther s) ref +let print_located_module ref = print_located_qualid "module" LocModule ref +let print_located_qualid ref = print_located_qualid "object" LocAny ref (******************************************) (**** Printing declarations and judgments *) (**** Gallina layer *****) let gallina_print_typed_value_in_env env sigma (trm,typ) = - (pr_lconstr_env env sigma trm ++ fnl () ++ - str " : " ++ pr_ltype_env env sigma typ) + (pr_leconstr_env env sigma trm ++ fnl () ++ + str " : " ++ pr_letype_env env sigma typ) (* To be improved; the type should be used to provide the types in the abstractions. This should be done recursively inside pr_lconstr, so that the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u) synthesizes the type nat of the abstraction on u *) -let print_named_def name body typ = - let pbody = pr_lconstr body in - let ptyp = pr_ltype typ in - let pbody = if isCast body then surround pbody else pbody in +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 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) ++ str "]") -let print_named_assum name typ = - str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]" +let print_named_assum env sigma name typ = + str "*** [" ++ str name ++ str " : " ++ pr_ltype_env env sigma typ ++ str "]" -let gallina_print_named_decl = +let gallina_print_named_decl env sigma = let open Context.Named.Declaration in function | LocalAssum (id, typ) -> - print_named_assum (Id.to_string id) typ + print_named_assum env sigma (Id.to_string id) typ | LocalDef (id, body, typ) -> - print_named_def (Id.to_string id) body typ + print_named_def env sigma (Id.to_string id) body typ let assumptions_for_print lna = List.fold_right (fun na env -> add_name na env) lna empty_names_context @@ -464,22 +525,22 @@ 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 @ print_inductive_implicit_args sp mipv @ print_inductive_argument_scopes sp mipv) -let print_named_decl id = - gallina_print_named_decl (Global.lookup_named id) ++ fnl () +let print_named_decl env sigma id = + gallina_print_named_decl env sigma (Global.lookup_named id) ++ fnl () -let gallina_print_section_variable id = - print_named_decl id ++ +let gallina_print_section_variable env sigma id = + print_named_decl env sigma id ++ with_line_skip (print_name_infos (VarRef id)) let print_body env evd = function @@ -489,102 +550,128 @@ let print_body env evd = function let print_typed_body env evd (val_0,typ) = (print_body env evd val_0 ++ fnl () ++ str " : " ++ pr_ltype_env env evd typ) -let ungeneralized_type_of_constant_type t = - Typeops.type_of_constant_type (Global.env ()) t - let print_instance sigma cb = - if cb.const_polymorphic then - pr_universe_instance sigma cb.const_universes + if Declareops.constant_is_polymorphic cb then + let univs = Declareops.constant_polymorphic_context cb in + let inst = Univ.AUContext.instance univs in + let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in + 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 = Declareops.type_of_constant cb in - let typ = ungeneralized_type_of_constant_type typ in - let univs = Univ.instantiate_univ_context - (Global.universes_of_constant_body cb) + let typ = + match cb.const_universes with + | Monomorphic_const _ -> cb.const_type + | Polymorphic_const univs -> + let inst = Univ.AUContext.instance univs in + Vars.subst_instance_constr inst cb.const_type + in + 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 -> Monomorphic_const_entry ctx, [] + | Polymorphic_const 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 -> + Monomorphic_const_entry (ContextSet.union body_uctxs ctx), [] + | Polymorphic_const 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)) + UState.of_binders + (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 - hov 0 (pr_polymorphic cb.const_polymorphic ++ + hov 0 (pr_polymorphic (Declareops.constant_is_polymorphic cb) ++ match val_0 with | None -> 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 (val_0,typ) else pr_ltype typ)++ - Printer.pr_universe_ctx sigma univs) + (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ + 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 kn = +let gallina_print_syntactic_def env kn = let qid = Nametab.shortest_qualid_of_syndef Id.Set.empty kn and (vars,a) = Syntax_def.search_syntactic_definition kn in - let c = Notation_ops.glob_constr_of_notation_constr Loc.ghost a in + let c = Notation_ops.glob_constr_of_notation_constr a in hov 2 (hov 4 (str "Notation " ++ pr_qualid qid ++ - prlist (fun id -> spc () ++ pr_id id) (List.map fst vars) ++ + prlist (fun id -> spc () ++ Id.print id) (List.map fst vars) ++ spc () ++ str ":=") ++ spc () ++ Constrextern.without_specific_symbols - [Notation.SynDefRule kn] pr_glob_constr c) + [Notation.SynDefRule kn] (pr_glob_constr_env env) c) -let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) = +let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) = let sep = if with_values then " = " else " : " and tag = object_tag lobj in match (oname,tag) with | (_,"VARIABLE") -> (* Outside sections, VARIABLES still exist but only with universes constraints *) - (try Some(print_named_decl (basename sp)) with Not_found -> None) + (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None) | (_,"CONSTANT") -> - Some (print_constant with_values sep (constant_of_kn kn)) + Some (print_constant with_values sep (Constant.make1 kn) None) | (_,"INDUCTIVE") -> - Some (gallina_print_inductive (mind_of_kn kn)) + Some (gallina_print_inductive (MutInd.make1 kn) None) | (_,"MODULE") -> - let (mp,_,l) = repr_kn kn in + let (mp,_,l) = KerName.repr kn in Some (print_module with_values (MPdot (mp,l))) | (_,"MODULE TYPE") -> - let (mp,_,l) = repr_kn kn in + let (mp,_,l) = KerName.repr kn in Some (print_modtype (MPdot (mp,l))) | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"| "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None (* To deal with forgotten cases... *) | (_,s) -> None -let gallina_print_library_entry with_values ent = - let pr_name (sp,_) = pr_id (basename sp) in +let gallina_print_library_entry env sigma with_values ent = + let pr_name (sp,_) = Id.print (basename sp) in match ent with | (oname,Lib.Leaf lobj) -> - gallina_print_leaf_entry with_values (oname,lobj) + gallina_print_leaf_entry env sigma with_values (oname,lobj) | (oname,Lib.OpenedSection (dir,_)) -> 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 _) -> Some (str " >>>>>>> Closed Module " ++ pr_name oname) - | (_,Lib.FrozenState _) -> - None -let gallina_print_context with_values = +let gallina_print_context env sigma with_values = let rec prec n = function | h::rest when Option.is_empty n || Option.get n > 0 -> - (match gallina_print_library_entry with_values h with + (match gallina_print_library_entry env sigma with_values h with | None -> prec n rest | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) | _ -> mt () @@ -639,49 +726,51 @@ let print_judgment env sigma {uj_val=trm;uj_type=typ} = let print_safe_judgment env sigma j = let trm = Safe_typing.j_val j in let typ = Safe_typing.j_type j in + let trm = EConstr.of_constr trm in + let typ = EConstr.of_constr typ in print_typed_value_in_env env sigma (trm, typ) (*********************) (* *) -let print_full_context () = print_context true None (Lib.contents ()) -let print_full_context_typ () = print_context false None (Lib.contents ()) +let print_full_context env sigma = print_context env sigma true None (Lib.contents ()) +let print_full_context_typ env sigma = print_context env sigma false None (Lib.contents ()) -let print_full_pure_context () = +let print_full_pure_context env sigma = let rec prec = function | ((_,kn),Lib.Leaf lobj)::rest -> let pp = match object_tag lobj with | "CONSTANT" -> let con = Global.constant_of_delta_kn kn in let cb = Global.lookup_constant con in - let typ = ungeneralized_type_of_constant_type cb.const_type in + let typ = cb.const_type in hov 0 ( match cb.const_body with | Undef _ -> str "Parameter " ++ - print_basename con ++ str " : " ++ cut () ++ pr_ltype typ + print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ | OpaqueDef lc -> str "Theorem " ++ print_basename con ++ cut () ++ - str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++ - str "Proof " ++ pr_lconstr (Opaqueproof.force_proof (Global.opaque_tables ()) lc) + str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++ + str "Proof " ++ pr_lconstr_env env sigma (Opaqueproof.force_proof (Global.opaque_tables ()) lc) | Def c -> str "Definition " ++ print_basename con ++ cut () ++ - str " : " ++ pr_ltype typ ++ cut () ++ str " := " ++ - pr_lconstr (Mod_subst.force_constr c)) + str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++ + pr_lconstr_env env sigma (Mod_subst.force_constr c)) ++ str "." ++ fnl () ++ fnl () | "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 *) - let (mp,_,l) = repr_kn kn in + let (mp,_,l) = KerName.repr kn in print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | "MODULE TYPE" -> (* TODO: make it reparsable *) (* TODO: make it reparsable *) - let (mp,_,l) = repr_kn kn in + let (mp,_,l) = KerName.repr kn in print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | _ -> mt () in prec rest ++ pp @@ -696,16 +785,16 @@ let print_full_pure_context () = (* This is designed to print the contents of an opened section *) let read_sec_context r = - let loc,qid = qualid_of_reference r in + let qid = qualid_of_reference r in let dir = - try Nametab.locate_section qid + try Nametab.locate_section qid.v with Not_found -> - user_err_loc (loc,"read_sec_context", str "Unknown section.") in + user_err ?loc:qid.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 -> - error "Cannot print the contents of a closed section." + user_err Pp.(str "Cannot print the contents of a closed section.") (* LEM: Actually, we could if we wanted to. *) | [] -> [] | hd::rest -> get_cxt (hd::in_cxt) rest @@ -713,90 +802,106 @@ let read_sec_context r = let cxt = Lib.contents () in List.rev (get_cxt [] cxt) -let print_sec_context sec = - print_context true None (read_sec_context sec) - -let print_sec_context_typ sec = - print_context false None (read_sec_context sec) - -let print_any_name = function - | Term (ConstRef sp) -> print_constant_with_infos sp - | Term (IndRef (sp,_)) -> print_inductive sp - | Term (ConstructRef ((sp,_),_)) -> print_inductive sp - | Term (VarRef sp) -> print_section_variable sp - | Syntactic kn -> print_syntactic_def kn - | Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp +let print_sec_context env sigma sec = + print_context env sigma true None (read_sec_context sec) + +let print_sec_context_typ env sigma sec = + print_context env sigma false None (read_sec_context sec) + +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 { obj_dir; obj_mp; _ } ) -> print_module (printable_body obj_dir) obj_mp | Dir _ -> mt () | ModuleType mp -> print_modtype mp - | Tactic kn -> mt () (** TODO *) + | Other (obj, info) -> info.print obj | Undefined qid -> try (* Var locale de but, pas var de section... donc pas d'implicits *) let dir,str = repr_qualid qid in if not (DirPath.is_empty dir) then raise Not_found; - let open Context.Named.Declaration in - str |> Global.lookup_named |> set_id str |> print_named_decl - with Not_found -> - errorlabstrm - "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") + str |> Global.lookup_named |> print_named_decl env sigma -let print_name = function - | ByNotation (loc,ntn,sc) -> - print_any_name - (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true) + with Not_found -> + user_err + ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") + +let print_name env sigma na udecl = + match na with + | {loc; v=ByNotation (ntn,sc)} -> + print_any_name env sigma + (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) - | AN ref -> - print_any_name (locate_any_name ref) + udecl + | {loc; v=AN ref} -> + print_any_name env sigma (locate_any_name ref) udecl -let print_opaque_name qid = - let env = Global.env () in +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 - error "Not a defined constant." + user_err Pp.(str "Not a defined constant.") | IndRef (sp,_) -> - print_inductive sp + print_inductive sp None | ConstructRef cstr as gr -> - let ty = Universes.unsafe_type_of_global gr in + let ty, ctx = Global.type_of_global_in_context env gr in + let inst = Univ.AUContext.instance ctx in + let ty = Vars.subst_instance_constr inst ty in + let ty = EConstr.of_constr ty in + let open EConstr in print_typed_value (mkConstruct cstr, ty) | VarRef id -> - let open Context.Named.Declaration in - lookup_named id env |> set_id id |> print_named_decl + env |> lookup_named id |> print_named_decl env sigma -let print_about_any loc 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; + 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 @ [hov 0 (str "Expands to: " ++ pr_located_qualid k)]) | Syntactic kn -> let () = match Syntax_def.search_syntactic_definition kn with - | [],Notation_term.NRef ref -> Dumpglob.add_glob loc ref + | [],Notation_term.NRef ref -> Dumpglob.add_glob ?loc ref | _ -> () in v 0 ( - print_syntactic_def kn ++ fnl () ++ + print_syntactic_def env kn ++ fnl () ++ hov 0 (str "Expands to: " ++ pr_located_qualid k)) - | Dir _ | ModuleType _ | Tactic _ | Undefined _ -> + | Dir _ | ModuleType _ | Undefined _ -> hov 0 (pr_located_qualid k) + | Other (obj, info) -> hov 0 (info.about obj) -let print_about = function - | ByNotation (loc,ntn,sc) -> - print_about_any loc - (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true) - ntn sc)) - | AN ref -> - print_about_any (loc_of_reference ref) (locate_any_name ref) +let print_about env sigma na udecl = + match na with + | {loc;v=ByNotation (ntn,sc)} -> + print_about_any ?loc env sigma + (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) + ntn sc)) udecl + | {loc;v=AN ref} -> + print_about_any ?loc env sigma (locate_any_name ref) udecl (* for debug *) -let inspect depth = - print_context false (Some depth) (Lib.contents ()) +let inspect env sigma depth = + print_context env sigma false (Some depth) (Lib.contents ()) (*************************************************************************) @@ -804,54 +909,54 @@ let inspect depth = open Classops -let print_coercion_value v = pr_lconstr (get_coercion_value v) +let print_coercion_value env sigma v = pr_lconstr_env env sigma (get_coercion_value v) let print_class i = let cl,_ = class_info_from_index i in pr_class cl -let print_path ((i,j),p) = +let print_path env sigma ((i,j),p) = hov 2 ( - str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++ + str"[" ++ hov 0 (prlist_with_sep pr_semicolon (print_coercion_value env sigma) p) ++ str"] : ") ++ print_class i ++ str" >-> " ++ print_class j let _ = Classops.install_path_printer print_path -let print_graph () = - prlist_with_sep fnl print_path (inheritance_graph()) +let print_graph env sigma = + prlist_with_sep fnl (print_path env sigma) (inheritance_graph()) let print_classes () = pr_sequence pr_class (classes()) -let print_coercions () = - pr_sequence print_coercion_value (coercions()) +let print_coercions env sigma = + pr_sequence (print_coercion_value env sigma) (coercions()) let index_of_class cl = try fst (class_info cl) with Not_found -> - errorlabstrm "index_of_class" + user_err ~hdr:"index_of_class" (pr_class cl ++ spc() ++ str "not a defined class.") -let print_path_between cls clt = +let print_path_between env sigma cls clt = let i = index_of_class cls in let j = index_of_class clt in let p = try lookup_path_between_class (i,j) with Not_found -> - errorlabstrm "index_cl_of_id" + user_err ~hdr:"index_cl_of_id" (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt ++ str ".") in - print_path ((i,j),p) + print_path env sigma ((i,j),p) -let print_canonical_projections () = +let print_canonical_projections env sigma = prlist_with_sep fnl (fun ((r1,r2),o) -> pr_cs_pattern r2 ++ str " <- " ++ - pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )") + pr_global r1 ++ str " ( " ++ pr_lconstr_env env sigma o.o_DEF ++ str " )") (canonical_projections ()) (*************************************************************************) @@ -862,7 +967,7 @@ let print_canonical_projections () = 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 @@ -871,7 +976,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 |