From 215b7e43cba768bfc82914718b159a22797f9d2b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 28 Oct 2019 16:48:21 +0100 Subject: Move prettyp (Print implementation) to vernac/ --- printing/prettyp.ml | 984 ------------------------------------------------ printing/prettyp.mli | 129 ------- printing/printing.mllib | 1 - vernac/prettyp.ml | 984 ++++++++++++++++++++++++++++++++++++++++++++++++ vernac/prettyp.mli | 129 +++++++ vernac/vernac.mllib | 1 + 6 files changed, 1114 insertions(+), 1114 deletions(-) delete mode 100644 printing/prettyp.ml delete mode 100644 printing/prettyp.mli create mode 100644 vernac/prettyp.ml create mode 100644 vernac/prettyp.mli diff --git a/printing/prettyp.ml b/printing/prettyp.ml deleted file mode 100644 index c995887f31..0000000000 --- a/printing/prettyp.ml +++ /dev/null @@ -1,984 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* - * on May-June 2006 for implementation of abstraction of pretty-printing of objects. - *) - -open Pp -open CErrors -open Util -open CAst -open Names -open Nameops -open Termops -open Declarations -open Environ -open Impargs -open Libobject -open Libnames -open Globnames -open Recordops -open Printer -open Printmod -open Context.Rel.Declaration - -(* module RelDecl = Context.Rel.Declaration *) -module NamedDecl = Context.Named.Declaration - -type object_pr = { - print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; - print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.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 : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t; - print_modtype : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t; - print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; - print_context : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> 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 -let gallina_print_modtype = print_modtype - -(**************) -(** Utilities *) - -let print_closed_sections = ref false - -let pr_infos_list l = v 0 (prlist_with_sep cut (fun x -> x) l) - -let with_line_skip l = if List.is_empty l then mt() else fnl() ++ fnl () ++ pr_infos_list l - -let blankline = mt() (* add a blank sentence in the list of infos *) - -let add_colon prefix = if ismt prefix then mt () else prefix ++ str ": " - -let int_or_no n = if Int.equal n 0 then str "no" else int n - -(*******************) -(** Basic printing *) - -let print_basename sp = pr_global (GlobRef.ConstRef sp) - -let print_ref reduce ref udecl = - let env = Global.env () in - let typ, univs = Typeops.type_of_global_in_context env ref in - let inst = Univ.make_abstract_instance univs in - let bl = UnivNames.universe_binders_with_opt_names (Environ.universes_of_global env ref) udecl in - let sigma = Evd.from_ctx (UState.of_binders bl) in - let typ = EConstr.of_constr typ in - let typ = - if reduce then - let ctx,ccl = Reductionops.splay_prod_assum env sigma typ - in EConstr.it_mkProd_or_LetIn ccl ctx - else typ in - let variance = let open GlobRef in match ref with - | VarRef _ | ConstRef _ -> None - | IndRef (ind,_) | ConstructRef ((ind,_),_) -> - let mind = Environ.lookup_mind ind env in - mind.Declarations.mind_variance - in - let inst = - if Global.is_polymorphic ref - then Printer.pr_universe_instance sigma inst - else mt () - in - let priv = None in (* We deliberately don't print private univs in About. *) - hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ - Printer.pr_abstract_universe_ctx sigma ?variance univs ?priv) - -(********************************) -(** Printing implicit arguments *) - -let pr_impl_name imp = Id.print (name_of_implicit imp) - -let print_impargs_by_name max = function - | [] -> [] - | impls -> - let n = List.length impls in - [hov 0 (str (String.plural n "Argument") ++ spc() ++ - prlist_with_sep pr_comma pr_impl_name impls ++ spc() ++ - str (String.conjugate_verb_to_be n) ++ str" implicit" ++ - (if max then strbrk " and maximally inserted" else mt()))] - -let print_one_impargs_list l = - let imps = List.filter is_status_implicit l in - let maximps = List.filter Impargs.maximal_insertion_of imps in - let nonmaximps = List.subtract (=) imps maximps in (* FIXME *) - print_impargs_by_name false nonmaximps @ - print_impargs_by_name true maximps - -let print_impargs_list prefix l = - let l = extract_impargs_data l in - List.flatten (List.map (fun (cond,imps) -> - match cond with - | None -> - List.map (fun pp -> add_colon prefix ++ pp) - (print_one_impargs_list imps) - | Some (n1,n2) -> - [v 2 (prlist_with_sep cut (fun x -> x) - [(if ismt prefix then str "When" else prefix ++ str ", when") ++ - str " applied to " ++ - (if Int.equal n1 n2 then int_or_no n2 else - if Int.equal n1 0 then str "no more than " ++ int n2 - else int n1 ++ str " to " ++ int_or_no n2) ++ - str (String.plural n2 " argument") ++ str ":"; - v 0 (prlist_with_sep cut (fun x -> x) - (if List.exists is_status_implicit imps - then print_one_impargs_list imps - else [str "No implicit arguments"]))])]) 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 Name.print l))] - -let need_expansion impl ref = - let typ, _ = Typeops.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 - List.exists is_status_implicit lastimpl - -let print_impargs ref = - let ref = Smartlocate.smart_global ref in - let impl = implicits_of_global ref in - 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 None; - blankline ] @ - (if has_impl then print_impargs_list (mt()) impl - else [str "No implicit arguments"])) - -(*********************) -(** Printing Scopes *) - -let print_argument_scopes prefix = function - | [Some sc] -> - [add_colon prefix ++ str"Argument scope is [" ++ str sc ++ str"]"] - | l when not (List.for_all Option.is_empty l) -> - [add_colon prefix ++ hov 2 (str"Argument scopes are" ++ spc() ++ - str "[" ++ - pr_sequence (function Some sc -> str sc | None -> str "_") l ++ - str "]")] - | _ -> [] - -(*********************) -(** Printing Opacity *) - -type opacity = - | FullyOpaque - | TransparentMaybeOpacified of Conv_oracle.level - -let opacity env = - function - | GlobRef.VarRef v when NamedDecl.is_local_def (Environ.lookup_named v env) -> - Some(TransparentMaybeOpacified - (Conv_oracle.get_strategy (Environ.oracle env) (VarKey v))) - | GlobRef.ConstRef cst -> - let cb = Environ.lookup_constant cst env in - (match cb.const_body with - | Undef _ | Primitive _ -> None - | OpaqueDef _ -> Some FullyOpaque - | Def _ -> Some - (TransparentMaybeOpacified - (Conv_oracle.get_strategy (Environ.oracle env) (ConstKey cst)))) - | _ -> None - -let print_opacity ref = - match opacity (Global.env()) ref with - | None -> [] - | Some s -> - [pr_global ref ++ str " is " ++ - match s with - | FullyOpaque -> str "opaque" - | TransparentMaybeOpacified Conv_oracle.Opaque -> - str "basically transparent but considered opaque for reduction" - | TransparentMaybeOpacified lev when Conv_oracle.is_transparent lev -> - str "transparent" - | TransparentMaybeOpacified (Conv_oracle.Level n) -> - str "transparent (with expansion weight " ++ int n ++ str ")" - | TransparentMaybeOpacified Conv_oracle.Expand -> - 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 pr_template_variables = function - | [] -> mt () - | vars -> str "on " ++ prlist_with_sep spc UnivNames.pr_with_global_universes vars - -let print_polymorphism ref = - let poly = Global.is_polymorphic ref in - let template_poly = Global.is_template_polymorphic ref in - let template_checked = Global.is_template_checked ref in - let template_variables = Global.get_template_polymorphic_variables ref in - [ pr_global ref ++ str " is " ++ - (if poly then str "universe polymorphic" - else if template_poly then - (if not template_checked then str "assumed " else mt()) ++ - str "template universe polymorphic " - ++ h 0 (pr_template_variables template_variables) - else str "not universe polymorphic") ] - -let print_type_in_type ref = - let unsafe = Global.is_type_in_type ref in - if unsafe then - [ pr_global ref ++ str " relies on an unsafe universe hierarchy"] - else [] - -let print_primitive_record recflag mipv = function - | PrimRecord _ -> - let eta = match recflag with - | CoFinite | Finite -> str" without eta conversion" - | BiFinite -> str " with eta conversion" - in - [Id.print mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."] - | FakeRecord | NotRecord -> [] - -let print_primitive ref = - match ref with - | GlobRef.IndRef ind -> - let mib,_ = Global.lookup_inductive ind in - print_primitive_record mib.mind_finite mib.mind_packets mib.mind_record - | _ -> [] - -let print_name_infos ref = - let impls = implicits_of_global ref in - let scopes = Notation.find_arguments_scope ref in - let renames = - try Arguments_renaming.arguments_names ref with Not_found -> [] in - let type_info_for_implicit = - 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 None; blankline] - else - [] in - print_type_in_type ref @ - print_primitive ref @ - type_info_for_implicit @ - print_renames_list (mt()) renames @ - print_impargs_list (mt()) impls @ - 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 " ++ Id.print id) l - else - [] - -let print_args_data_of_inductive_ids get test pr sp mipv = - List.flatten (Array.to_list (Array.mapi - (fun i mip -> - print_id_args_data test pr mip.mind_typename (get (GlobRef.IndRef (sp,i))) @ - List.flatten (Array.to_list (Array.mapi - (fun j idc -> - print_id_args_data test pr idc (get (GlobRef.ConstructRef ((sp,i),j+1)))) - mip.mind_consnames))) - mipv)) - -let print_inductive_implicit_args = - print_args_data_of_inductive_ids - implicits_of_global (fun l -> not (List.is_empty (positions_of_implicits l))) - print_impargs_list - -let print_inductive_renames = - print_args_data_of_inductive_ids - (fun r -> - try Arguments_renaming.arguments_names r with Not_found -> []) - ((!=) Anonymous) - print_renames_list - -let print_inductive_argument_scopes = - print_args_data_of_inductive_ids - Notation.find_arguments_scope (Option.has_some) print_argument_scopes - -let print_bidi_hints gr = - match Pretyping.get_bidirectionality_hint gr with - | None -> [] - | Some nargs -> - [str "Using typing information from context after typing the " ++ int nargs ++ str " first arguments"] - -(*********************) -(* "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 GlobRef.t - | Dir of Nametab.GlobDirRef.t - | 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 qid = - try Term (Nametab.locate qid) - with Not_found -> - try Syntactic (Nametab.locate_syndef qid) - with Not_found -> - try Dir (Nametab.locate_dir qid) - with Not_found -> - try ModuleType (Nametab.locate_modtype 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 -> - let ref_str = let open GlobRef in match ref with - ConstRef _ -> "Constant" - | IndRef _ -> "Inductive" - | ConstructRef _ -> "Constructor" - | VarRef _ -> "Variable" in - str ref_str ++ spc () ++ pr_path (Nametab.path_of_global ref) - | Syntactic kn -> - str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn) - | Dir dir -> - let s,dir = - let open Nametab in - let open GlobDirRef in match dir with - | 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 - in - 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 - | Undefined qid -> - pr_qualid qid ++ spc () ++ str "not a defined object." - -let canonize_ref = let open GlobRef in function - | ConstRef c -> - let kn = Constant.canonical c in - if KerName.equal (Constant.user c) kn then None - else Some (ConstRef (Constant.make1 kn)) - | IndRef (ind,i) -> - let kn = MutInd.canonical ind in - if KerName.equal (MutInd.user ind) kn then None - else Some (IndRef (MutInd.make1 kn, i)) - | ConstructRef ((ind,i),j) -> - let kn = MutInd.canonical ind in - if KerName.equal (MutInd.user ind) kn then None - else Some (ConstructRef ((MutInd.make1 kn, i),j)) - | VarRef _ -> None - -let display_alias = function - | Term r -> - begin match canonize_ref r with - | None -> mt () - | Some r' -> - let q' = Nametab.shortest_qualid_of_global Id.Set.empty r' in - spc () ++ str "(alias of " ++ pr_qualid q' ++ str ")" - end - | _ -> mt () - -let locate_term qid = - let expand = function - | TrueGlobal ref -> - Term ref, Nametab.shortest_qualid_of_global Id.Set.empty ref - | SynDef kn -> - Syntactic kn, Nametab.shortest_qualid_of_syndef Id.Set.empty kn - in - List.map expand (Nametab.locate_extended_all qid) - -let locate_module qid = - let all = Nametab.locate_extended_all_dir qid in - let map dir = let open Nametab.GlobDirRef in match dir with - | DirModule { Nametab.obj_mp ; _ } -> Some (Dir dir, Nametab.shortest_qualid_of_module obj_mp) - | DirOpenModule _ -> Some (Dir dir, qid) - | _ -> None - in - List.map_filter map all - -let locate_modtype qid = - let all = Nametab.locate_extended_all_modtype qid in - let map mp = ModuleType mp, Nametab.shortest_qualid_of_modtype mp in - let modtypes = List.map map all in - (* Don't forget the opened module types: they are not part of the same name tab. *) - let all = Nametab.locate_extended_all_dir qid in - let map dir = let open Nametab.GlobDirRef in match dir with - | DirOpenModtype _ -> Some (Dir dir, qid) - | _ -> None - 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 qid = - 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 () ++ Id.print id - else - str "No " ++ str name ++ str " of suffix" ++ spc () ++ pr_qualid qid - | l -> - prlist_with_sep fnl - (fun (o,oqid) -> - hov 2 (pr_located_qualid o ++ - (if not (qualid_eq oqid qid) then - spc() ++ str "(shorter name to refer to it in current context is " - ++ pr_qualid oqid ++ str")" - else mt ()) ++ - display_alias o)) l - -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_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 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 env sigma name typ = - str "*** [" ++ str name ++ str " : " ++ pr_ltype_env env sigma typ ++ str "]" - -let gallina_print_named_decl env sigma = - let open Context.Named.Declaration in - function - | LocalAssum (id, typ) -> - print_named_assum env sigma (Id.to_string id.Context.binder_name) typ - | LocalDef (id, body, typ) -> - print_named_def env sigma (Id.to_string id.Context.binder_name) body typ - -let assumptions_for_print lna = - List.fold_right (fun na env -> add_name na env) lna empty_names_context - -(*********************) -(* *) - -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 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 env sigma id = - gallina_print_named_decl env sigma (Global.lookup_named id) ++ fnl () - -let gallina_print_section_variable env sigma id = - print_named_decl env sigma id ++ - with_line_skip (print_name_infos (GlobRef.VarRef id)) - -let print_body env evd = function - | Some c -> pr_lconstr_env env evd c - | None -> (str"") - -let print_typed_body env evd (val_0,typ) = - (print_body env evd val_0 ++ fnl () ++ str " : " ++ pr_ltype_env env evd typ) - -let print_instance sigma cb = - if Declareops.constant_is_polymorphic cb then - let univs = Declareops.constant_polymorphic_context cb in - let inst = Univ.make_abstract_instance univs in - pr_universe_instance sigma inst - else mt() - -let print_constant indirect_accessor with_values sep sp udecl = - let cb = Global.lookup_constant sp in - let val_0 = Global.body_of_constant_body indirect_accessor cb in - let typ = cb.const_type in - let univs = - let open Univ in - let otab = Global.opaque_tables () in - match cb.const_body with - | Undef _ | Def _ | Primitive _ -> cb.const_universes - | OpaqueDef o -> - let body_uctxs = Opaqueproof.force_constraints indirect_accessor otab o in - match cb.const_universes with - | Monomorphic ctx -> - Monomorphic (ContextSet.union body_uctxs ctx) - | Polymorphic ctx -> - assert(ContextSet.is_empty body_uctxs); - Polymorphic ctx - in - let ctx = - UState.of_binders - (UnivNames.universe_binders_with_opt_names (Declareops.constant_polymorphic_context cb) udecl) - in - let env = Global.env () and sigma = Evd.from_ctx ctx in - let pr_ltype = pr_ltype_env env sigma in - hov 0 ( - match val_0 with - | None -> - str"*** [ " ++ - print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ - str" ]" ++ - Printer.pr_universes sigma univs - | Some (c, priv, ctx) -> - let priv = match priv with - | Opaqueproof.PrivateMonomorphic () -> None - | Opaqueproof.PrivatePolymorphic (_, ctx) -> Some ctx - 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_universes sigma univs ?priv) - -let gallina_print_constant_with_infos indirect_accessor sp udecl = - print_constant indirect_accessor true " = " sp udecl ++ - with_line_skip (print_name_infos (GlobRef.ConstRef sp)) - -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 a in - hov 2 - (hov 4 - (str "Notation " ++ pr_qualid qid ++ - prlist (fun id -> spc () ++ Id.print id) (List.map fst vars) ++ - spc () ++ str ":=") ++ - spc () ++ - Constrextern.without_specific_symbols - [Notation.SynDefRule kn] (pr_glob_constr_env env) c) - -let gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values ((sp,kn as oname),lobj) = - let sep = if with_values then " = " else " : " in - match lobj with - | AtomicObject o -> - let tag = object_tag o in - begin match (oname,tag) with - | (_,"VARIABLE") -> - (* Outside sections, VARIABLES still exist but only with universes - constraints *) - (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None) - | (_,"CONSTANT") -> - Some (print_constant indirect_accessor with_values sep (Constant.make1 kn) None) - | (_,"INDUCTIVE") -> - Some (gallina_print_inductive (MutInd.make1 kn) None) - | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"| - "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None - (* To deal with forgotten cases... *) - | (_,s) -> None - end - | ModuleObject _ -> - let (mp,l) = KerName.repr kn in - Some (print_module ~mod_ops with_values (MPdot (mp,l))) - | ModuleTypeObject _ -> - let (mp,l) = KerName.repr kn in - Some (print_modtype ~mod_ops (MPdot (mp,l))) - | _ -> None - -let gallina_print_library_entry ~mod_ops indirect_accessor 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 ~mod_ops indirect_accessor env sigma with_values (oname,lobj) - | (oname,Lib.OpenedSection (dir,_)) -> - Some (str " >>>>>>> Section " ++ pr_name oname) - | (_,Lib.CompilingLibrary { Nametab.obj_dir; _ }) -> - Some (str " >>>>>>> Library " ++ DirPath.print obj_dir) - | (oname,Lib.OpenedModule _) -> - Some (str " >>>>>>> Module " ++ pr_name oname) - -let gallina_print_context ~mod_ops indirect_accessor 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 ~mod_ops indirect_accessor env sigma with_values h with - | None -> prec n rest - | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) - | _ -> mt () - in - prec - -let gallina_print_eval red_fun env sigma _ {uj_val=trm;uj_type=typ} = - let ntrm = red_fun env sigma trm in - (str " = " ++ gallina_print_typed_value_in_env env sigma (ntrm,typ)) - -(******************************************) -(**** Printing abstraction layer *) - -let default_object_pr = { - print_inductive = gallina_print_inductive; - print_constant_with_infos = gallina_print_constant_with_infos; - print_section_variable = gallina_print_section_variable; - print_syntactic_def = gallina_print_syntactic_def; - print_module = gallina_print_module; - print_modtype = gallina_print_modtype; - print_named_decl = gallina_print_named_decl; - print_library_entry = gallina_print_library_entry; - print_context = gallina_print_context; - print_typed_value_in_env = gallina_print_typed_value_in_env; - print_eval = gallina_print_eval; -} - -let object_pr = ref default_object_pr -let set_object_pr = (:=) object_pr - -let print_inductive x = !object_pr.print_inductive x -let print_constant_with_infos c = !object_pr.print_constant_with_infos c -let print_section_variable c = !object_pr.print_section_variable c -let print_syntactic_def x = !object_pr.print_syntactic_def x -let print_module x = !object_pr.print_module x -let print_modtype x = !object_pr.print_modtype x -let print_named_decl x = !object_pr.print_named_decl x -let print_library_entry ~mod_ops x = !object_pr.print_library_entry ~mod_ops x -let print_context ~mod_ops x = !object_pr.print_context ~mod_ops x -let print_typed_value_in_env x = !object_pr.print_typed_value_in_env x -let print_eval x = !object_pr.print_eval x - -(******************************************) -(**** Printing declarations and judgments *) -(**** Abstract layer *****) - -let print_judgment env sigma {uj_val=trm;uj_type=typ} = - print_typed_value_in_env env sigma (trm, 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 ~mod_ops indirect_accessor env sigma = - print_context ~mod_ops indirect_accessor env sigma true None (Lib.contents ()) -let print_full_context_typ ~mod_ops indirect_accessor env sigma = - print_context ~mod_ops indirect_accessor env sigma false None (Lib.contents ()) - -let print_full_pure_context ~mod_ops ~library_accessor env sigma = - let rec prec = function - | ((_,kn),Lib.Leaf AtomicObject 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 = cb.const_type in - hov 0 ( - match cb.const_body with - | Undef _ -> - str "Parameter " ++ - print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ - | OpaqueDef lc -> - str "Theorem " ++ print_basename con ++ cut () ++ - str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++ - str "Proof " ++ pr_lconstr_env env sigma (fst (Opaqueproof.force_proof library_accessor (Global.opaque_tables ()) lc)) - | Def c -> - str "Definition " ++ print_basename con ++ cut () ++ - str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++ - pr_lconstr_env env sigma (Mod_subst.force_constr c) - | Primitive _ -> - str "Primitive " ++ - print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ) - ++ 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 None ++ - str "." ++ fnl () ++ fnl () - | _ -> mt () in - prec rest ++ pp - | ((_,kn),Lib.Leaf ModuleObject _)::rest -> - (* TODO: make it reparsable *) - let (mp,l) = KerName.repr kn in - prec rest ++ print_module ~mod_ops true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () - | ((_,kn),Lib.Leaf ModuleTypeObject _)::rest -> - (* TODO: make it reparsable *) - let (mp,l) = KerName.repr kn in - prec rest ++ print_modtype ~mod_ops (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () - | _::rest -> prec rest - | _ -> mt () in - prec (Lib.contents ()) - -(* For printing an inductive definition with - its constructors and elimination, - assume that the declaration of constructors and eliminations - follows the definition of the inductive type *) - -(* This is designed to print the contents of an opened section *) -let read_sec_context qid = - let dir = - try Nametab.locate_section qid - with Not_found -> - user_err ?loc:qid.loc ~hdr:"read_sec_context" (str "Unknown section.") in - let rec get_cxt in_cxt = function - | (_,Lib.OpenedSection ({Nametab.obj_dir;_},_) as hd)::rest -> - if DirPath.equal dir obj_dir then (hd::in_cxt) else get_cxt (hd::in_cxt) rest - | [] -> [] - | hd::rest -> get_cxt (hd::in_cxt) rest - in - let cxt = Lib.contents () in - List.rev (get_cxt [] cxt) - -let print_sec_context ~mod_ops indirect_accessor env sigma sec = - print_context ~mod_ops indirect_accessor env sigma true None (read_sec_context sec) - -let print_sec_context_typ ~mod_ops indirect_accessor env sigma sec = - print_context ~mod_ops indirect_accessor env sigma false None (read_sec_context sec) - -let maybe_error_reject_univ_decl na udecl = - let open GlobRef in - 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 ~mod_ops indirect_accessor env sigma na udecl = - maybe_error_reject_univ_decl na udecl; - let open GlobRef in - match na with - | Term (ConstRef sp) -> print_constant_with_infos indirect_accessor 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 (Nametab.GlobDirRef.DirModule Nametab.{ obj_dir; obj_mp; _ } ) -> - print_module ~mod_ops (printable_body obj_dir) obj_mp - | Dir _ -> mt () - | ModuleType mp -> print_modtype ~mod_ops mp - | 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; - str |> Global.lookup_named |> print_named_decl env sigma - - with Not_found -> - user_err - ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") - -let print_name ~mod_ops indirect_accessor env sigma na udecl = - match na with - | {loc; v=Constrexpr.ByNotation (ntn,sc)} -> - print_any_name ~mod_ops indirect_accessor env sigma - (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) - ntn sc)) - udecl - | {loc; v=Constrexpr.AN ref} -> - print_any_name ~mod_ops indirect_accessor env sigma (locate_any_name ref) udecl - -let print_opaque_name indirect_accessor env sigma qid = - let open GlobRef in - 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 indirect_accessor cst None - else - user_err Pp.(str "Not a defined constant.") - | IndRef (sp,_) -> - print_inductive sp None - | ConstructRef cstr as gr -> - let ty, ctx = Typeops.type_of_global_in_context env gr in - let ty = EConstr.of_constr ty in - let open EConstr in - print_typed_value_in_env env sigma (mkConstruct cstr, ty) - | VarRef id -> - env |> lookup_named id |> print_named_decl env sigma - -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 udecl :: blankline :: - print_polymorphism ref @ - print_name_infos ref @ - (if Pp.ismt rb then [] else [rb]) @ - print_opacity ref @ - print_bidi_hints 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 - | _ -> () in - v 0 ( - print_syntactic_def env kn ++ fnl () ++ - hov 0 (str "Expands to: " ++ pr_located_qualid k)) - | Dir _ | ModuleType _ | Undefined _ -> - hov 0 (pr_located_qualid k) - | Other (obj, info) -> hov 0 (info.about obj) - -let print_about env sigma na udecl = - match na with - | {loc;v=Constrexpr.ByNotation (ntn,sc)} -> - print_about_any ?loc env sigma - (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) - ntn sc)) udecl - | {loc;v=Constrexpr.AN ref} -> - print_about_any ?loc env sigma (locate_any_name ref) udecl - -(* for debug *) -let inspect ~mod_ops indirect_accessor env sigma depth = - print_context ~mod_ops indirect_accessor env sigma false (Some depth) (Lib.contents ()) - -(*************************************************************************) -(* Pretty-printing functions coming from classops.ml *) - -open Classops - -let print_coercion_value v = Printer.pr_global v.coe_value - -let print_class i = - let cl,_ = class_info_from_index i in - pr_class cl - -let print_path ((i,j),p) = - hov 2 ( - str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value 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_classes () = - pr_sequence pr_class (classes()) - -let print_coercions () = - pr_sequence print_coercion_value (coercions()) - -let index_of_class cl = - try - fst (class_info cl) - with Not_found -> - user_err ~hdr:"index_of_class" - (pr_class cl ++ spc() ++ str "not a defined class.") - -let print_path_between 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 -> - 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) - -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_env env sigma o.o_DEF ++ str " )") - (canonical_projections ()) - -(*************************************************************************) - -(*************************************************************************) -(* Pretty-printing functions for type classes *) - -open Typeclasses - -let pr_typeclass env t = - print_ref false t.cl_impl None - -let print_typeclasses () = - let env = Global.env () in - prlist_with_sep fnl (pr_typeclass env) (typeclasses ()) - -let pr_instance env i = - (* gallina_print_constant_with_infos i.is_impl *) - (* lighter *) - print_ref false (instance_impl i) None ++ - begin match hint_priority i with - | None -> mt () - | Some i -> spc () ++ str "|" ++ spc () ++ int i - end - -let print_all_instances () = - let env = Global.env () in - let inst = all_instances () in - prlist_with_sep fnl (pr_instance env) inst - -let print_instances r = - let env = Global.env () in - let sigma = Evd.from_env env in - let inst = instances env sigma r in - prlist_with_sep fnl (pr_instance env) inst diff --git a/printing/prettyp.mli b/printing/prettyp.mli deleted file mode 100644 index c8b361d95b..0000000000 --- a/printing/prettyp.mli +++ /dev/null @@ -1,129 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* Termops.names_context - -val print_closed_sections : bool ref -val print_context - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map - -> bool -> int option -> Lib.library_segment -> Pp.t -val print_library_entry - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map - -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option -val print_full_context - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t -val print_full_context_typ - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t - -val print_full_pure_context - : mod_ops:Printmod.mod_ops - -> library_accessor:Opaqueproof.indirect_accessor - -> env - -> Evd.evar_map - -> Pp.t - -val print_sec_context - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t -val print_sec_context_typ - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t -val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t -val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t -val print_eval : - reduction_function -> env -> Evd.evar_map -> - Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t - -val print_name - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map -> qualid Constrexpr.or_by_notation - -> UnivNames.univ_name_list option -> Pp.t -val print_opaque_name - : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t -val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> - UnivNames.univ_name_list option -> Pp.t -val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t - -(** Pretty-printing functions for classes and coercions *) -val print_graph : unit -> Pp.t -val print_classes : unit -> Pp.t -val print_coercions : unit -> Pp.t -val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t -val print_canonical_projections : env -> Evd.evar_map -> Pp.t - -(** Pretty-printing functions for type classes and instances *) -val print_typeclasses : unit -> Pp.t -val print_instances : GlobRef.t -> Pp.t -val print_all_instances : unit -> Pp.t - -val inspect - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map -> int -> Pp.t - -(** {5 Locate} *) - -type 'a locatable_info = { - locate : qualid -> 'a option; - (** Locate the most precise object with the provided name if any. *) - locate_all : qualid -> 'a list; - (** Locate all objects whose name is a suffix of the provided name *) - shortest_qualid : 'a -> qualid; - (** Return the shortest name in the current context *) - name : 'a -> Pp.t; - (** Data as printed by the Locate command *) - print : 'a -> Pp.t; - (** Data as printed by the Print command *) - about : 'a -> Pp.t; - (** Data as printed by the About command *) -} -(** Generic data structure representing locatable objects. *) - -val register_locatable : string -> 'a locatable_info -> unit -(** Define a new type of locatable objects that can be reached via the - corresponding generic vernacular commands. The string should be a unique - name describing the kind of objects considered and that is added as a - grammar command prefix for vernacular commands Locate. *) - -val print_located_qualid : qualid -> Pp.t -val print_located_term : qualid -> Pp.t -val print_located_module : qualid -> Pp.t -val print_located_other : string -> qualid -> Pp.t - -type object_pr = { - print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; - print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.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 : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t; - print_modtype : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t; - print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; - print_context : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> 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; -} - -val set_object_pr : object_pr -> unit -val default_object_pr : object_pr diff --git a/printing/printing.mllib b/printing/printing.mllib index deb52ad270..5b5b6590a4 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -4,4 +4,3 @@ Ppconstr Proof_diffs Printer Printmod -Prettyp diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml new file mode 100644 index 0000000000..fa534a0936 --- /dev/null +++ b/vernac/prettyp.ml @@ -0,0 +1,984 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* + * on May-June 2006 for implementation of abstraction of pretty-printing of objects. + *) + +open Pp +open CErrors +open Util +open CAst +open Names +open Nameops +open Termops +open Declarations +open Environ +open Impargs +open Libobject +open Libnames +open Globnames +open Recordops +open Printer +open Printmod +open Context.Rel.Declaration + +(* module RelDecl = Context.Rel.Declaration *) +module NamedDecl = Context.Named.Declaration + +type object_pr = { + print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; + print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.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 : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t; + print_modtype : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t; + print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; + print_library_entry : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; + print_context : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> 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 +let gallina_print_modtype = print_modtype + +(**************) +(** Utilities *) + +let print_closed_sections = ref false + +let pr_infos_list l = v 0 (prlist_with_sep cut (fun x -> x) l) + +let with_line_skip l = if List.is_empty l then mt() else fnl() ++ fnl () ++ pr_infos_list l + +let blankline = mt() (* add a blank sentence in the list of infos *) + +let add_colon prefix = if ismt prefix then mt () else prefix ++ str ": " + +let int_or_no n = if Int.equal n 0 then str "no" else int n + +(*******************) +(** Basic printing *) + +let print_basename sp = pr_global (GlobRef.ConstRef sp) + +let print_ref reduce ref udecl = + let env = Global.env () in + let typ, univs = Typeops.type_of_global_in_context env ref in + let inst = Univ.make_abstract_instance univs in + let bl = UnivNames.universe_binders_with_opt_names (Environ.universes_of_global env ref) udecl in + let sigma = Evd.from_ctx (UState.of_binders bl) in + let typ = EConstr.of_constr typ in + let typ = + if reduce then + let ctx,ccl = Reductionops.splay_prod_assum env sigma typ + in EConstr.it_mkProd_or_LetIn ccl ctx + else typ in + let variance = let open GlobRef in match ref with + | VarRef _ | ConstRef _ -> None + | IndRef (ind,_) | ConstructRef ((ind,_),_) -> + let mind = Environ.lookup_mind ind env in + mind.Declarations.mind_variance + in + let inst = + if Global.is_polymorphic ref + then Printer.pr_universe_instance sigma inst + else mt () + in + let priv = None in (* We deliberately don't print private univs in About. *) + hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ + Printer.pr_abstract_universe_ctx sigma ?variance univs ?priv) + +(********************************) +(** Printing implicit arguments *) + +let pr_impl_name imp = Id.print (name_of_implicit imp) + +let print_impargs_by_name max = function + | [] -> [] + | impls -> + let n = List.length impls in + [hov 0 (str (String.plural n "Argument") ++ spc() ++ + prlist_with_sep pr_comma pr_impl_name impls ++ spc() ++ + str (String.conjugate_verb_to_be n) ++ str" implicit" ++ + (if max then strbrk " and maximally inserted" else mt()))] + +let print_one_impargs_list l = + let imps = List.filter is_status_implicit l in + let maximps = List.filter Impargs.maximal_insertion_of imps in + let nonmaximps = List.subtract (=) imps maximps in (* FIXME *) + print_impargs_by_name false nonmaximps @ + print_impargs_by_name true maximps + +let print_impargs_list prefix l = + let l = extract_impargs_data l in + List.flatten (List.map (fun (cond,imps) -> + match cond with + | None -> + List.map (fun pp -> add_colon prefix ++ pp) + (print_one_impargs_list imps) + | Some (n1,n2) -> + [v 2 (prlist_with_sep cut (fun x -> x) + [(if ismt prefix then str "When" else prefix ++ str ", when") ++ + str " applied to " ++ + (if Int.equal n1 n2 then int_or_no n2 else + if Int.equal n1 0 then str "no more than " ++ int n2 + else int n1 ++ str " to " ++ int_or_no n2) ++ + str (String.plural n2 " argument") ++ str ":"; + v 0 (prlist_with_sep cut (fun x -> x) + (if List.exists is_status_implicit imps + then print_one_impargs_list imps + else [str "No implicit arguments"]))])]) 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 Name.print l))] + +let need_expansion impl ref = + let typ, _ = Typeops.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 + List.exists is_status_implicit lastimpl + +let print_impargs ref = + let ref = Smartlocate.smart_global ref in + let impl = implicits_of_global ref in + 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 None; + blankline ] @ + (if has_impl then print_impargs_list (mt()) impl + else [str "No implicit arguments"])) + +(*********************) +(** Printing Scopes *) + +let print_argument_scopes prefix = function + | [Some sc] -> + [add_colon prefix ++ str"Argument scope is [" ++ str sc ++ str"]"] + | l when not (List.for_all Option.is_empty l) -> + [add_colon prefix ++ hov 2 (str"Argument scopes are" ++ spc() ++ + str "[" ++ + pr_sequence (function Some sc -> str sc | None -> str "_") l ++ + str "]")] + | _ -> [] + +(*********************) +(** Printing Opacity *) + +type opacity = + | FullyOpaque + | TransparentMaybeOpacified of Conv_oracle.level + +let opacity env = + function + | GlobRef.VarRef v when NamedDecl.is_local_def (Environ.lookup_named v env) -> + Some(TransparentMaybeOpacified + (Conv_oracle.get_strategy (Environ.oracle env) (VarKey v))) + | GlobRef.ConstRef cst -> + let cb = Environ.lookup_constant cst env in + (match cb.const_body with + | Undef _ | Primitive _ -> None + | OpaqueDef _ -> Some FullyOpaque + | Def _ -> Some + (TransparentMaybeOpacified + (Conv_oracle.get_strategy (Environ.oracle env) (ConstKey cst)))) + | _ -> None + +let print_opacity ref = + match opacity (Global.env()) ref with + | None -> [] + | Some s -> + [pr_global ref ++ str " is " ++ + match s with + | FullyOpaque -> str "opaque" + | TransparentMaybeOpacified Conv_oracle.Opaque -> + str "basically transparent but considered opaque for reduction" + | TransparentMaybeOpacified lev when Conv_oracle.is_transparent lev -> + str "transparent" + | TransparentMaybeOpacified (Conv_oracle.Level n) -> + str "transparent (with expansion weight " ++ int n ++ str ")" + | TransparentMaybeOpacified Conv_oracle.Expand -> + 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 pr_template_variables = function + | [] -> mt () + | vars -> str "on " ++ prlist_with_sep spc UnivNames.pr_with_global_universes vars + +let print_polymorphism ref = + let poly = Global.is_polymorphic ref in + let template_poly = Global.is_template_polymorphic ref in + let template_checked = Global.is_template_checked ref in + let template_variables = Global.get_template_polymorphic_variables ref in + [ pr_global ref ++ str " is " ++ + (if poly then str "universe polymorphic" + else if template_poly then + (if not template_checked then str "assumed " else mt()) ++ + str "template universe polymorphic " + ++ h 0 (pr_template_variables template_variables) + else str "not universe polymorphic") ] + +let print_type_in_type ref = + let unsafe = Global.is_type_in_type ref in + if unsafe then + [ pr_global ref ++ str " relies on an unsafe universe hierarchy"] + else [] + +let print_primitive_record recflag mipv = function + | PrimRecord _ -> + let eta = match recflag with + | CoFinite | Finite -> str" without eta conversion" + | BiFinite -> str " with eta conversion" + in + [Id.print mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."] + | FakeRecord | NotRecord -> [] + +let print_primitive ref = + match ref with + | GlobRef.IndRef ind -> + let mib,_ = Global.lookup_inductive ind in + print_primitive_record mib.mind_finite mib.mind_packets mib.mind_record + | _ -> [] + +let print_name_infos ref = + let impls = implicits_of_global ref in + let scopes = Notation.find_arguments_scope ref in + let renames = + try Arguments_renaming.arguments_names ref with Not_found -> [] in + let type_info_for_implicit = + 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 None; blankline] + else + [] in + print_type_in_type ref @ + print_primitive ref @ + type_info_for_implicit @ + print_renames_list (mt()) renames @ + print_impargs_list (mt()) impls @ + 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 " ++ Id.print id) l + else + [] + +let print_args_data_of_inductive_ids get test pr sp mipv = + List.flatten (Array.to_list (Array.mapi + (fun i mip -> + print_id_args_data test pr mip.mind_typename (get (GlobRef.IndRef (sp,i))) @ + List.flatten (Array.to_list (Array.mapi + (fun j idc -> + print_id_args_data test pr idc (get (GlobRef.ConstructRef ((sp,i),j+1)))) + mip.mind_consnames))) + mipv)) + +let print_inductive_implicit_args = + print_args_data_of_inductive_ids + implicits_of_global (fun l -> not (List.is_empty (positions_of_implicits l))) + print_impargs_list + +let print_inductive_renames = + print_args_data_of_inductive_ids + (fun r -> + try Arguments_renaming.arguments_names r with Not_found -> []) + ((!=) Anonymous) + print_renames_list + +let print_inductive_argument_scopes = + print_args_data_of_inductive_ids + Notation.find_arguments_scope (Option.has_some) print_argument_scopes + +let print_bidi_hints gr = + match Pretyping.get_bidirectionality_hint gr with + | None -> [] + | Some nargs -> + [str "Using typing information from context after typing the " ++ int nargs ++ str " first arguments"] + +(*********************) +(* "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 GlobRef.t + | Dir of Nametab.GlobDirRef.t + | 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 qid = + try Term (Nametab.locate qid) + with Not_found -> + try Syntactic (Nametab.locate_syndef qid) + with Not_found -> + try Dir (Nametab.locate_dir qid) + with Not_found -> + try ModuleType (Nametab.locate_modtype 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 -> + let ref_str = let open GlobRef in match ref with + ConstRef _ -> "Constant" + | IndRef _ -> "Inductive" + | ConstructRef _ -> "Constructor" + | VarRef _ -> "Variable" in + str ref_str ++ spc () ++ pr_path (Nametab.path_of_global ref) + | Syntactic kn -> + str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn) + | Dir dir -> + let s,dir = + let open Nametab in + let open GlobDirRef in match dir with + | 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 + in + 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 + | Undefined qid -> + pr_qualid qid ++ spc () ++ str "not a defined object." + +let canonize_ref = let open GlobRef in function + | ConstRef c -> + let kn = Constant.canonical c in + if KerName.equal (Constant.user c) kn then None + else Some (ConstRef (Constant.make1 kn)) + | IndRef (ind,i) -> + let kn = MutInd.canonical ind in + if KerName.equal (MutInd.user ind) kn then None + else Some (IndRef (MutInd.make1 kn, i)) + | ConstructRef ((ind,i),j) -> + let kn = MutInd.canonical ind in + if KerName.equal (MutInd.user ind) kn then None + else Some (ConstructRef ((MutInd.make1 kn, i),j)) + | VarRef _ -> None + +let display_alias = function + | Term r -> + begin match canonize_ref r with + | None -> mt () + | Some r' -> + let q' = Nametab.shortest_qualid_of_global Id.Set.empty r' in + spc () ++ str "(alias of " ++ pr_qualid q' ++ str ")" + end + | _ -> mt () + +let locate_term qid = + let expand = function + | TrueGlobal ref -> + Term ref, Nametab.shortest_qualid_of_global Id.Set.empty ref + | SynDef kn -> + Syntactic kn, Nametab.shortest_qualid_of_syndef Id.Set.empty kn + in + List.map expand (Nametab.locate_extended_all qid) + +let locate_module qid = + let all = Nametab.locate_extended_all_dir qid in + let map dir = let open Nametab.GlobDirRef in match dir with + | DirModule { Nametab.obj_mp ; _ } -> Some (Dir dir, Nametab.shortest_qualid_of_module obj_mp) + | DirOpenModule _ -> Some (Dir dir, qid) + | _ -> None + in + List.map_filter map all + +let locate_modtype qid = + let all = Nametab.locate_extended_all_modtype qid in + let map mp = ModuleType mp, Nametab.shortest_qualid_of_modtype mp in + let modtypes = List.map map all in + (* Don't forget the opened module types: they are not part of the same name tab. *) + let all = Nametab.locate_extended_all_dir qid in + let map dir = let open Nametab.GlobDirRef in match dir with + | DirOpenModtype _ -> Some (Dir dir, qid) + | _ -> None + 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 qid = + 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 () ++ Id.print id + else + str "No " ++ str name ++ str " of suffix" ++ spc () ++ pr_qualid qid + | l -> + prlist_with_sep fnl + (fun (o,oqid) -> + hov 2 (pr_located_qualid o ++ + (if not (qualid_eq oqid qid) then + spc() ++ str "(shorter name to refer to it in current context is " + ++ pr_qualid oqid ++ str")" + else mt ()) ++ + display_alias o)) l + +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_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 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 env sigma name typ = + str "*** [" ++ str name ++ str " : " ++ pr_ltype_env env sigma typ ++ str "]" + +let gallina_print_named_decl env sigma = + let open Context.Named.Declaration in + function + | LocalAssum (id, typ) -> + print_named_assum env sigma (Id.to_string id.Context.binder_name) typ + | LocalDef (id, body, typ) -> + print_named_def env sigma (Id.to_string id.Context.binder_name) body typ + +let assumptions_for_print lna = + List.fold_right (fun na env -> add_name na env) lna empty_names_context + +(*********************) +(* *) + +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 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 env sigma id = + gallina_print_named_decl env sigma (Global.lookup_named id) ++ fnl () + +let gallina_print_section_variable env sigma id = + print_named_decl env sigma id ++ + with_line_skip (print_name_infos (GlobRef.VarRef id)) + +let print_body env evd = function + | Some c -> pr_lconstr_env env evd c + | None -> (str"") + +let print_typed_body env evd (val_0,typ) = + (print_body env evd val_0 ++ fnl () ++ str " : " ++ pr_ltype_env env evd typ) + +let print_instance sigma cb = + if Declareops.constant_is_polymorphic cb then + let univs = Declareops.constant_polymorphic_context cb in + let inst = Univ.make_abstract_instance univs in + pr_universe_instance sigma inst + else mt() + +let print_constant indirect_accessor with_values sep sp udecl = + let cb = Global.lookup_constant sp in + let val_0 = Global.body_of_constant_body indirect_accessor cb in + let typ = cb.const_type in + let univs = + let open Univ in + let otab = Global.opaque_tables () in + match cb.const_body with + | Undef _ | Def _ | Primitive _ -> cb.const_universes + | OpaqueDef o -> + let body_uctxs = Opaqueproof.force_constraints indirect_accessor otab o in + match cb.const_universes with + | Monomorphic ctx -> + Monomorphic (ContextSet.union body_uctxs ctx) + | Polymorphic ctx -> + assert(ContextSet.is_empty body_uctxs); + Polymorphic ctx + in + let ctx = + UState.of_binders + (UnivNames.universe_binders_with_opt_names (Declareops.constant_polymorphic_context cb) udecl) + in + let env = Global.env () and sigma = Evd.from_ctx ctx in + let pr_ltype = pr_ltype_env env sigma in + hov 0 ( + match val_0 with + | None -> + str"*** [ " ++ + print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ + str" ]" ++ + Printer.pr_universes sigma univs + | Some (c, priv, ctx) -> + let priv = match priv with + | Opaqueproof.PrivateMonomorphic () -> None + | Opaqueproof.PrivatePolymorphic (_, ctx) -> Some ctx + 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_universes sigma univs ?priv) + +let gallina_print_constant_with_infos indirect_accessor sp udecl = + print_constant indirect_accessor true " = " sp udecl ++ + with_line_skip (print_name_infos (GlobRef.ConstRef sp)) + +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 a in + hov 2 + (hov 4 + (str "Notation " ++ pr_qualid qid ++ + prlist (fun id -> spc () ++ Id.print id) (List.map fst vars) ++ + spc () ++ str ":=") ++ + spc () ++ + Constrextern.without_specific_symbols + [Notation.SynDefRule kn] (pr_glob_constr_env env) c) + +let gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values ((sp,kn as oname),lobj) = + let sep = if with_values then " = " else " : " in + match lobj with + | AtomicObject o -> + let tag = object_tag o in + begin match (oname,tag) with + | (_,"VARIABLE") -> + (* Outside sections, VARIABLES still exist but only with universes + constraints *) + (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None) + | (_,"CONSTANT") -> + Some (print_constant indirect_accessor with_values sep (Constant.make1 kn) None) + | (_,"INDUCTIVE") -> + Some (gallina_print_inductive (MutInd.make1 kn) None) + | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"| + "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None + (* To deal with forgotten cases... *) + | (_,s) -> None + end + | ModuleObject _ -> + let (mp,l) = KerName.repr kn in + Some (print_module ~mod_ops with_values (MPdot (mp,l))) + | ModuleTypeObject _ -> + let (mp,l) = KerName.repr kn in + Some (print_modtype ~mod_ops (MPdot (mp,l))) + | _ -> None + +let gallina_print_library_entry ~mod_ops indirect_accessor 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 ~mod_ops indirect_accessor env sigma with_values (oname,lobj) + | (oname,Lib.OpenedSection (dir,_)) -> + Some (str " >>>>>>> Section " ++ pr_name oname) + | (_,Lib.CompilingLibrary { Nametab.obj_dir; _ }) -> + Some (str " >>>>>>> Library " ++ DirPath.print obj_dir) + | (oname,Lib.OpenedModule _) -> + Some (str " >>>>>>> Module " ++ pr_name oname) + +let gallina_print_context ~mod_ops indirect_accessor 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 ~mod_ops indirect_accessor env sigma with_values h with + | None -> prec n rest + | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) + | _ -> mt () + in + prec + +let gallina_print_eval red_fun env sigma _ {uj_val=trm;uj_type=typ} = + let ntrm = red_fun env sigma trm in + (str " = " ++ gallina_print_typed_value_in_env env sigma (ntrm,typ)) + +(******************************************) +(**** Printing abstraction layer *) + +let default_object_pr = { + print_inductive = gallina_print_inductive; + print_constant_with_infos = gallina_print_constant_with_infos; + print_section_variable = gallina_print_section_variable; + print_syntactic_def = gallina_print_syntactic_def; + print_module = gallina_print_module; + print_modtype = gallina_print_modtype; + print_named_decl = gallina_print_named_decl; + print_library_entry = gallina_print_library_entry; + print_context = gallina_print_context; + print_typed_value_in_env = gallina_print_typed_value_in_env; + print_eval = gallina_print_eval; +} + +let object_pr = ref default_object_pr +let set_object_pr = (:=) object_pr + +let print_inductive x = !object_pr.print_inductive x +let print_constant_with_infos c = !object_pr.print_constant_with_infos c +let print_section_variable c = !object_pr.print_section_variable c +let print_syntactic_def x = !object_pr.print_syntactic_def x +let print_module x = !object_pr.print_module x +let print_modtype x = !object_pr.print_modtype x +let print_named_decl x = !object_pr.print_named_decl x +let print_library_entry ~mod_ops x = !object_pr.print_library_entry ~mod_ops x +let print_context ~mod_ops x = !object_pr.print_context ~mod_ops x +let print_typed_value_in_env x = !object_pr.print_typed_value_in_env x +let print_eval x = !object_pr.print_eval x + +(******************************************) +(**** Printing declarations and judgments *) +(**** Abstract layer *****) + +let print_judgment env sigma {uj_val=trm;uj_type=typ} = + print_typed_value_in_env env sigma (trm, 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 ~mod_ops indirect_accessor env sigma = + print_context ~mod_ops indirect_accessor env sigma true None (Lib.contents ()) +let print_full_context_typ ~mod_ops indirect_accessor env sigma = + print_context ~mod_ops indirect_accessor env sigma false None (Lib.contents ()) + +let print_full_pure_context ~mod_ops ~library_accessor env sigma = + let rec prec = function + | ((_,kn),Lib.Leaf AtomicObject 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 = cb.const_type in + hov 0 ( + match cb.const_body with + | Undef _ -> + str "Parameter " ++ + print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ + | OpaqueDef lc -> + str "Theorem " ++ print_basename con ++ cut () ++ + str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++ + str "Proof " ++ pr_lconstr_env env sigma (fst (Opaqueproof.force_proof library_accessor (Global.opaque_tables ()) lc)) + | Def c -> + str "Definition " ++ print_basename con ++ cut () ++ + str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++ + pr_lconstr_env env sigma (Mod_subst.force_constr c) + | Primitive _ -> + str "Primitive " ++ + print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ) + ++ 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 None ++ + str "." ++ fnl () ++ fnl () + | _ -> mt () in + prec rest ++ pp + | ((_,kn),Lib.Leaf ModuleObject _)::rest -> + (* TODO: make it reparsable *) + let (mp,l) = KerName.repr kn in + prec rest ++ print_module ~mod_ops true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + | ((_,kn),Lib.Leaf ModuleTypeObject _)::rest -> + (* TODO: make it reparsable *) + let (mp,l) = KerName.repr kn in + prec rest ++ print_modtype ~mod_ops (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + | _::rest -> prec rest + | _ -> mt () in + prec (Lib.contents ()) + +(* For printing an inductive definition with + its constructors and elimination, + assume that the declaration of constructors and eliminations + follows the definition of the inductive type *) + +(* This is designed to print the contents of an opened section *) +let read_sec_context qid = + let dir = + try Nametab.locate_section qid + with Not_found -> + user_err ?loc:qid.loc ~hdr:"read_sec_context" (str "Unknown section.") in + let rec get_cxt in_cxt = function + | (_,Lib.OpenedSection ({Nametab.obj_dir;_},_) as hd)::rest -> + if DirPath.equal dir obj_dir then (hd::in_cxt) else get_cxt (hd::in_cxt) rest + | [] -> [] + | hd::rest -> get_cxt (hd::in_cxt) rest + in + let cxt = Lib.contents () in + List.rev (get_cxt [] cxt) + +let print_sec_context ~mod_ops indirect_accessor env sigma sec = + print_context ~mod_ops indirect_accessor env sigma true None (read_sec_context sec) + +let print_sec_context_typ ~mod_ops indirect_accessor env sigma sec = + print_context ~mod_ops indirect_accessor env sigma false None (read_sec_context sec) + +let maybe_error_reject_univ_decl na udecl = + let open GlobRef in + 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 ~mod_ops indirect_accessor env sigma na udecl = + maybe_error_reject_univ_decl na udecl; + let open GlobRef in + match na with + | Term (ConstRef sp) -> print_constant_with_infos indirect_accessor 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 (Nametab.GlobDirRef.DirModule Nametab.{ obj_dir; obj_mp; _ } ) -> + print_module ~mod_ops (printable_body obj_dir) obj_mp + | Dir _ -> mt () + | ModuleType mp -> print_modtype ~mod_ops mp + | 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; + str |> Global.lookup_named |> print_named_decl env sigma + + with Not_found -> + user_err + ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") + +let print_name ~mod_ops indirect_accessor env sigma na udecl = + match na with + | {loc; v=Constrexpr.ByNotation (ntn,sc)} -> + print_any_name ~mod_ops indirect_accessor env sigma + (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) + ntn sc)) + udecl + | {loc; v=Constrexpr.AN ref} -> + print_any_name ~mod_ops indirect_accessor env sigma (locate_any_name ref) udecl + +let print_opaque_name indirect_accessor env sigma qid = + let open GlobRef in + 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 indirect_accessor cst None + else + user_err Pp.(str "Not a defined constant.") + | IndRef (sp,_) -> + print_inductive sp None + | ConstructRef cstr as gr -> + let ty, ctx = Typeops.type_of_global_in_context env gr in + let ty = EConstr.of_constr ty in + let open EConstr in + print_typed_value_in_env env sigma (mkConstruct cstr, ty) + | VarRef id -> + env |> lookup_named id |> print_named_decl env sigma + +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 udecl :: blankline :: + print_polymorphism ref @ + print_name_infos ref @ + (if Pp.ismt rb then [] else [rb]) @ + print_opacity ref @ + print_bidi_hints 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 + | _ -> () in + v 0 ( + print_syntactic_def env kn ++ fnl () ++ + hov 0 (str "Expands to: " ++ pr_located_qualid k)) + | Dir _ | ModuleType _ | Undefined _ -> + hov 0 (pr_located_qualid k) + | Other (obj, info) -> hov 0 (info.about obj) + +let print_about env sigma na udecl = + match na with + | {loc;v=Constrexpr.ByNotation (ntn,sc)} -> + print_about_any ?loc env sigma + (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) + ntn sc)) udecl + | {loc;v=Constrexpr.AN ref} -> + print_about_any ?loc env sigma (locate_any_name ref) udecl + +(* for debug *) +let inspect ~mod_ops indirect_accessor env sigma depth = + print_context ~mod_ops indirect_accessor env sigma false (Some depth) (Lib.contents ()) + +(*************************************************************************) +(* Pretty-printing functions coming from classops.ml *) + +open Classops + +let print_coercion_value v = Printer.pr_global v.coe_value + +let print_class i = + let cl,_ = class_info_from_index i in + pr_class cl + +let print_path ((i,j),p) = + hov 2 ( + str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value 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_classes () = + pr_sequence pr_class (classes()) + +let print_coercions () = + pr_sequence print_coercion_value (coercions()) + +let index_of_class cl = + try + fst (class_info cl) + with Not_found -> + user_err ~hdr:"index_of_class" + (pr_class cl ++ spc() ++ str "not a defined class.") + +let print_path_between 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 -> + 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) + +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_env env sigma o.o_DEF ++ str " )") + (canonical_projections ()) + +(*************************************************************************) + +(*************************************************************************) +(* Pretty-printing functions for type classes *) + +open Typeclasses + +let pr_typeclass env t = + print_ref false t.cl_impl None + +let print_typeclasses () = + let env = Global.env () in + prlist_with_sep fnl (pr_typeclass env) (typeclasses ()) + +let pr_instance env i = + (* gallina_print_constant_with_infos i.is_impl *) + (* lighter *) + print_ref false (instance_impl i) None ++ + begin match hint_priority i with + | None -> mt () + | Some i -> spc () ++ str "|" ++ spc () ++ int i + end + +let print_all_instances () = + let env = Global.env () in + let inst = all_instances () in + prlist_with_sep fnl (pr_instance env) inst + +let print_instances r = + let env = Global.env () in + let sigma = Evd.from_env env in + let inst = instances env sigma r in + prlist_with_sep fnl (pr_instance env) inst diff --git a/vernac/prettyp.mli b/vernac/prettyp.mli new file mode 100644 index 0000000000..c8b361d95b --- /dev/null +++ b/vernac/prettyp.mli @@ -0,0 +1,129 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* Termops.names_context + +val print_closed_sections : bool ref +val print_context + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor + -> env -> Evd.evar_map + -> bool -> int option -> Lib.library_segment -> Pp.t +val print_library_entry + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor + -> env -> Evd.evar_map + -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option +val print_full_context + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t +val print_full_context_typ + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t + +val print_full_pure_context + : mod_ops:Printmod.mod_ops + -> library_accessor:Opaqueproof.indirect_accessor + -> env + -> Evd.evar_map + -> Pp.t + +val print_sec_context + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t +val print_sec_context_typ + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t +val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t +val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t +val print_eval : + reduction_function -> env -> Evd.evar_map -> + Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t + +val print_name + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor + -> env -> Evd.evar_map -> qualid Constrexpr.or_by_notation + -> UnivNames.univ_name_list option -> Pp.t +val print_opaque_name + : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t +val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> + UnivNames.univ_name_list option -> Pp.t +val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t + +(** Pretty-printing functions for classes and coercions *) +val print_graph : unit -> Pp.t +val print_classes : unit -> Pp.t +val print_coercions : unit -> Pp.t +val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t +val print_canonical_projections : env -> Evd.evar_map -> Pp.t + +(** Pretty-printing functions for type classes and instances *) +val print_typeclasses : unit -> Pp.t +val print_instances : GlobRef.t -> Pp.t +val print_all_instances : unit -> Pp.t + +val inspect + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor + -> env -> Evd.evar_map -> int -> Pp.t + +(** {5 Locate} *) + +type 'a locatable_info = { + locate : qualid -> 'a option; + (** Locate the most precise object with the provided name if any. *) + locate_all : qualid -> 'a list; + (** Locate all objects whose name is a suffix of the provided name *) + shortest_qualid : 'a -> qualid; + (** Return the shortest name in the current context *) + name : 'a -> Pp.t; + (** Data as printed by the Locate command *) + print : 'a -> Pp.t; + (** Data as printed by the Print command *) + about : 'a -> Pp.t; + (** Data as printed by the About command *) +} +(** Generic data structure representing locatable objects. *) + +val register_locatable : string -> 'a locatable_info -> unit +(** Define a new type of locatable objects that can be reached via the + corresponding generic vernacular commands. The string should be a unique + name describing the kind of objects considered and that is added as a + grammar command prefix for vernacular commands Locate. *) + +val print_located_qualid : qualid -> Pp.t +val print_located_term : qualid -> Pp.t +val print_located_module : qualid -> Pp.t +val print_located_other : string -> qualid -> Pp.t + +type object_pr = { + print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; + print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.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 : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t; + print_modtype : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t; + print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; + print_library_entry : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; + print_context : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> 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; +} + +val set_object_pr : object_pr -> unit +val default_object_pr : object_pr diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 102da20257..7563b4a5d5 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -10,6 +10,7 @@ Locality Egramml Vernacextend Ppvernac +Prettyp Proof_using Egramcoq Metasyntax -- cgit v1.2.3