diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 3 | ||||
| -rw-r--r-- | printing/prettyp.ml | 984 | ||||
| -rw-r--r-- | printing/prettyp.mli | 129 | ||||
| -rw-r--r-- | printing/printer.ml | 101 | ||||
| -rw-r--r-- | printing/printer.mli | 86 | ||||
| -rw-r--r-- | printing/printing.mllib | 1 | ||||
| -rw-r--r-- | printing/printmod.ml | 52 | ||||
| -rw-r--r-- | printing/proof_diffs.ml | 20 | ||||
| -rw-r--r-- | printing/proof_diffs.mli | 9 |
9 files changed, 154 insertions, 1231 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 5ed96dd5e3..2da163b8ee 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -249,7 +249,8 @@ let tag_var = tag Tag.variable let pp (c, p) = pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc (lpatrec, Any) p in - str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}", lpatrec + (if l = [] then str "{| |}" + else str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}"), lpatrec | CPatAlias (p, na) -> pr_patt mt (las,E) p ++ str " as " ++ pr_lname na, las 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 *) -(* <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 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(* Changed by (and thus parts copyright ©) by Lionel Elie Mamane <lionel@mamane.lu> - * 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"<no body>") - -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 *) -(* <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 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names -open Environ -open Reductionops -open Libnames - -(** A Pretty-Printer for the Calculus of Inductive Constructions. *) - -val assumptions_for_print : Name.t list -> 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/printer.ml b/printing/printer.ml index 10a31ac256..bb54f587fd 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -76,25 +76,22 @@ let () = and only names of goal/section variables and rel names that do _not_ occur in the scope of the binder to be printed are avoided. *) -let pr_econstr_n_core goal_concl_style env sigma n t = - pr_constr_expr_n env sigma n (extern_constr goal_concl_style env sigma t) -let pr_econstr_core goal_concl_style env sigma t = - pr_constr_expr env sigma (extern_constr goal_concl_style env sigma t) -let pr_leconstr_core = Proof_diffs.pr_leconstr_core - -let pr_constr_n_env env sigma n c = pr_econstr_n_core false env sigma n (EConstr.of_constr c) +let pr_econstr_n_env ?lax ?inctx ?scope env sigma n t = + pr_constr_expr_n env sigma n (extern_constr ?lax ?inctx ?scope env sigma t) +let pr_econstr_env ?lax ?inctx ?scope env sigma t = + pr_constr_expr env sigma (extern_constr ?lax ?inctx ?scope env sigma t) +let pr_leconstr_env = Proof_diffs.pr_leconstr_env + +let pr_constr_n_env ?lax ?inctx ?scope env sigma n c = + pr_econstr_n_env ?lax ?inctx ?scope env sigma n (EConstr.of_constr c) +let pr_constr_env ?lax ?inctx ?scope env sigma c = + pr_econstr_env ?lax ?inctx ?scope env sigma (EConstr.of_constr c) let pr_lconstr_env = Proof_diffs.pr_lconstr_env -let pr_constr_env env sigma c = pr_econstr_core false env sigma (EConstr.of_constr c) - -let pr_lconstr_goal_style_env env sigma c = pr_leconstr_core true env sigma (EConstr.of_constr c) -let pr_constr_goal_style_env env sigma c = pr_econstr_core true env sigma (EConstr.of_constr c) - -let pr_econstr_n_env env sigma c = pr_econstr_n_core false env sigma c -let pr_leconstr_env env sigma c = pr_leconstr_core false env sigma c -let pr_econstr_env env sigma c = pr_econstr_core false env sigma c -let pr_open_lconstr_env env sigma (_,c) = pr_leconstr_env env sigma c -let pr_open_constr_env env sigma (_,c) = pr_econstr_env env sigma c +let pr_open_lconstr_env ?lax ?inctx ?scope env sigma (_,c) = + pr_leconstr_env ?lax ?inctx ?scope env sigma c +let pr_open_constr_env ?lax ?inctx ?scope env sigma (_,c) = + pr_econstr_env ?lax ?inctx ?scope env sigma c let pr_constr_under_binders_env_gen pr env sigma (ids,c) = (* Warning: clashes can occur with variables of same name in env but *) @@ -106,16 +103,14 @@ let pr_constr_under_binders_env_gen pr env sigma (ids,c) = let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_econstr_env let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_leconstr_env -let pr_etype_core goal_concl_style env sigma t = - pr_constr_expr env sigma (extern_type goal_concl_style env sigma t) -let pr_letype_core = Proof_diffs.pr_letype_core +let pr_etype_env ?lax ?goal_concl_style env sigma t = + pr_constr_expr env sigma (extern_type ?lax ?goal_concl_style env sigma t) +let pr_letype_env = Proof_diffs.pr_letype_env -let pr_ltype_env env sigma c = pr_letype_core false env sigma (EConstr.of_constr c) -let pr_type_env env sigma c = pr_etype_core false env sigma (EConstr.of_constr c) - -let pr_etype_env env sigma c = pr_etype_core false env sigma c -let pr_letype_env env sigma c = pr_letype_core false env sigma c -let pr_goal_concl_style_env env sigma c = pr_letype_core true env sigma c +let pr_type_env ?lax ?goal_concl_style env sigma c = + pr_etype_env ?lax ?goal_concl_style env sigma (EConstr.of_constr c) +let pr_ltype_env ?lax ?goal_concl_style env sigma c = + pr_letype_env ?lax ?goal_concl_style env sigma (EConstr.of_constr c) let pr_ljudge_env env sigma j = (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type) @@ -125,10 +120,10 @@ let pr_lglob_constr_env env c = let pr_glob_constr_env env c = pr_constr_expr env (Evd.from_env env) (extern_glob_constr (Termops.vars_of_env env) c) -let pr_closed_glob_n_env env sigma n c = - pr_constr_expr_n env sigma n (extern_closed_glob false env sigma c) -let pr_closed_glob_env env sigma c = - pr_constr_expr env sigma (extern_closed_glob false env sigma c) +let pr_closed_glob_n_env ?lax ?goal_concl_style ?inctx ?scope env sigma n c = + pr_constr_expr_n env sigma n (extern_closed_glob ?lax ?goal_concl_style ?inctx ?scope env sigma c) +let pr_closed_glob_env ?lax ?goal_concl_style ?inctx ?scope env sigma c = + pr_constr_expr env sigma (extern_closed_glob ?lax ?goal_concl_style ?inctx ?scope env sigma c) let pr_lconstr_pattern_env env sigma c = pr_lconstr_pattern_expr env sigma (extern_constr_pattern (Termops.names_of_rel_context env) sigma c) @@ -141,7 +136,7 @@ let pr_cases_pattern t = let pr_sort sigma s = pr_glob_sort (extern_sort sigma s) let () = Termops.Internal.set_print_constr - (fun env sigma t -> pr_lconstr_expr env sigma (extern_constr ~lax:true false env sigma t)) + (fun env sigma t -> pr_lconstr_expr env sigma (extern_constr ~lax:true env sigma t)) let pr_in_comment x = str "(* " ++ x ++ str " *)" @@ -304,10 +299,10 @@ let pr_rel_decl env sigma decl = let pbody = match decl with | RelDecl.LocalAssum _ -> mt () | RelDecl.LocalDef (_,c,_) -> - (* Force evaluation *) - let pb = pr_lconstr_env env sigma c in - let pb = if isCast c then surround pb else pb in - (str":=" ++ spc () ++ pb ++ spc ()) in + (* Force evaluation *) + let pb = pr_lconstr_env env sigma c in + let pb = if isCast c then surround pb else pb in + (str":=" ++ spc () ++ pb ++ spc ()) in let ptyp = pr_ltype_env env sigma typ in match na with | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) @@ -329,7 +324,7 @@ let pr_var_list_decl env sigma decl = let pr_named_context env sigma ne_context = hv 0 (Context.Named.fold_outside - (fun d pps -> pps ++ ws 2 ++ pr_named_decl env sigma d) + (fun d pps -> pps ++ ws 2 ++ pr_named_decl env sigma d) ne_context ~init:(mt ())) let pr_rel_context env sigma rel_context = @@ -436,7 +431,7 @@ let pr_predicate pr_elt (b, elts) = let pr_elts = prlist_with_sep spc pr_elt elts in if b then str"all" ++ - (if List.is_empty elts then mt () else str" except: " ++ pr_elts) + (if List.is_empty elts then mt () else str" except: " ++ pr_elts) else if List.is_empty elts then str"none" else pr_elts @@ -462,7 +457,7 @@ let pr_goal ?(diffs=false) ?og_s g_s = else pr_context_of env sigma ++ cut () ++ str "============================" ++ cut () ++ - pr_goal_concl_style_env env sigma concl + pr_letype_env ~goal_concl_style:true env sigma concl in str " " ++ v 0 goal @@ -489,7 +484,7 @@ let pr_concl n ?(diffs=false) ?og_s sigma g = if diffs then Proof_diffs.diff_concl ?og_s sigma g else - pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) + pr_letype_env ~goal_concl_style:true env sigma (Goal.V82.concl sigma g) in let header = pr_goal_header (int n) sigma g in header ++ str " is:" ++ cut () ++ str" " ++ pc @@ -565,10 +560,10 @@ let pr_subgoal n sigma = let rec prrec p = function | [] -> user_err Pp.(str "No such goal.") | g::rest -> - if Int.equal p 1 then + if Int.equal p 1 then pr_selected_subgoal (int n) sigma g - else - prrec (p-1) rest + else + prrec (p-1) rest in prrec n @@ -736,7 +731,7 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map pr_goal ~diffs ?og_s { it = g ; sigma = sigma } ++ (if l=[] then mt () else cut ()) ++ pr_rec 2 l - else + else pr_rec 1 (g::l) in let pr_evar_info gl sigma seeds = @@ -792,15 +787,15 @@ let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof = begin match bgoals,shelf,given_up with | [] , [] , [] -> pr_subgoals None sigma ~seeds ~shelf ~stack ~unfocused:[] ~goals | [] , [] , _ -> - Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:"); - fnl () + Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:"); + fnl () ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:given_up ++ fnl () ++ str "You need to go back and solve them." | [] , _ , _ -> - Feedback.msg_info (str "All the remaining goals are on the shelf."); - fnl () + Feedback.msg_info (str "All the remaining goals are on the shelf."); + fnl () ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:shelf - | _ , _, _ -> + | _ , _, _ -> let cmd = if quiet then None else Some (str "This subproof is complete, but there are some unfocused goals." ++ @@ -809,8 +804,8 @@ let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof = fnl ()) in pr_subgoals ~pr_first:false cmd bsigma ~seeds ~shelf ~stack:[] ~unfocused:[] ~goals:bgoals - end - | _ -> + end + | _ -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in let bgoals_focused, bgoals_unfocused = List.partition (fun x -> List.mem x goals) bgoals in let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in @@ -981,17 +976,17 @@ let pr_assumptionset env sigma s = let tran = safe_pr_constant env kn ++ safe_pr_ltype env sigma typ in (v, a, o, tran :: tr) in - let (vars, axioms, opaque, trans) = + let (vars, axioms, opaque, trans) = ContextObjectMap.fold fold s ([], [], [], []) in let theory = if is_impredicative_set env then - [str "Set is impredicative"] + [str "Set is impredicative"] else [] in let theory = if type_in_type env then - str "Type hierarchy is collapsed (logic is inconsistent)" :: theory + str "Type hierarchy is collapsed (logic is inconsistent)" :: theory else theory in let opt_list title = function diff --git a/printing/printer.mli b/printing/printer.mli index 87b09ff755..1d7a25cbb6 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -15,55 +15,93 @@ open Pattern open Evd open Glob_term open Ltac_pretype +open Notation_term (** These are the entry points for printing terms, context, tac, ... *) - val enable_unfocused_goal_printing: bool ref val enable_goal_tags_printing : bool ref val enable_goal_names_printing : bool ref (** Terms *) -val pr_lconstr_env : env -> evar_map -> constr -> Pp.t -val pr_lconstr_goal_style_env : env -> evar_map -> constr -> Pp.t +(** Printers for terms. + + The "lconstr" variant does not require parentheses to isolate the + expression from the surrounding context (for instance [3 + 4] + will be written [3 + 4]). The "constr" variant (w/o "l") + enforces parentheses whenever the term is not an atom (for + instance, [3] will be written [3] but [3 + 4] will be + written [(3 + 4)]. + + [~inctx:true] indicates that the term is intended to be printed in + a context where its type is known so that a head coercion would be + skipped, or implicit arguments inferable from the context will not + be made explicit. For instance, if [foo] is declared as a + coercion, [foo bar] will be printed as [bar] if [inctx] is [true] + and as [foo bar] otherwise. + + [~scope:some_scope_name] indicates that the head of the term is + intended to be printed in scope [some_scope_name]. It defaults to + [None]. + + [~lax:true] is for debugging purpose. It defaults to [~lax:false]. *) -val pr_constr_env : env -> evar_map -> constr -> Pp.t -val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t -val pr_constr_n_env : env -> evar_map -> Notation_gram.tolerability -> constr -> Pp.t +val pr_constr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> constr -> Pp.t +val pr_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> constr -> Pp.t + +val pr_constr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> constr -> Pp.t (** Same, but resilient to [Nametab] errors. Prints fully-qualified names when [shortest_qualid_of_global] has failed. Prints "??" in case of remaining issues (such as reference not in env). *) -val safe_pr_lconstr_env : env -> evar_map -> constr -> Pp.t - -val safe_pr_constr_env : env -> evar_map -> constr -> Pp.t - -val pr_econstr_env : env -> evar_map -> EConstr.t -> Pp.t -val pr_leconstr_env : env -> evar_map -> EConstr.t -> Pp.t +val safe_pr_constr_env : env -> evar_map -> constr -> Pp.t +val safe_pr_lconstr_env : env -> evar_map -> constr -> Pp.t -val pr_econstr_n_env : env -> evar_map -> Notation_gram.tolerability -> EConstr.t -> Pp.t +val pr_econstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> EConstr.t -> Pp.t +val pr_leconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> EConstr.t -> Pp.t -val pr_etype_env : env -> evar_map -> EConstr.types -> Pp.t -val pr_letype_env : env -> evar_map -> EConstr.types -> Pp.t +val pr_econstr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> EConstr.t -> Pp.t -val pr_open_constr_env : env -> evar_map -> open_constr -> Pp.t +val pr_etype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t +val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t -val pr_open_lconstr_env : env -> evar_map -> open_constr -> Pp.t +val pr_open_constr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> open_constr -> Pp.t +val pr_open_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> open_constr -> Pp.t val pr_constr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t -val pr_goal_concl_style_env : env -> evar_map -> EConstr.types -> Pp.t -val pr_ltype_env : env -> evar_map -> types -> Pp.t - -val pr_type_env : env -> evar_map -> types -> Pp.t - -val pr_closed_glob_n_env : env -> evar_map -> Notation_gram.tolerability -> closed_glob_constr -> Pp.t -val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> Pp.t +(** Printers for types. Types are printed in scope "type_scope" and + under the constraint of being of type a sort. + + The "ltype" variant does not require parentheses to isolate the + expression from the surrounding context (for instance [nat * bool] + will be written [nat * bool]). The "type" variant (w/o "l") + enforces parentheses whenever the term is not an atom (for + instance, [nat] will be written [nat] but [nat * bool] will be + written [(nat * bool)]. + + [~goal_concl_style:true] tells to print the type the same way as + command [Show] would print a goal. Concretely, it means that all + names of goal/section variables and all names of variables + referred by de Bruijn indices (if any) in the given environment + and all short names of global definitions of the current module + must be avoided while printing bound variables. Otherwise, short + names of global definitions are printed qualified and only names + of goal/section variables and rel names that do _not_ occur in the + scope of the binder to be printed are avoided. + + [~lax:true] is for debugging purpose. *) + +val pr_ltype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t +val pr_type_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t + +val pr_closed_glob_n_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> closed_glob_constr -> Pp.t +val pr_closed_glob_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> closed_glob_constr -> Pp.t val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t 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/printing/printmod.ml b/printing/printmod.ml index 4cc6bc2052..85bb287c22 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -63,9 +63,9 @@ let get_new_id locals id = let rec get_id l id = let dir = DirPath.make [id] in if not (Nametab.exists_dir dir) then - id + id else - get_id (Id.Set.add id l) (Namegen.next_ident_away id l) + get_id (Id.Set.add id l) (Namegen.next_ident_away id l) in let avoid = List.fold_left (fun accu (_, id) -> Id.Set.add id accu) Id.Set.empty locals in get_id avoid id @@ -205,10 +205,10 @@ let print_kn locals kn = pr_qualid qid with Not_found -> - try - print_local_modpath locals kn - with - Not_found -> print_modpath locals kn + try + print_local_modpath locals kn + with + Not_found -> print_modpath locals kn let nametab_register_dir obj_mp = let id = mk_fake_top () in @@ -234,11 +234,11 @@ let nametab_register_body mp dir (l,body) = | SFBmind mib -> let mind = MutInd.make2 mp l in Array.iteri - (fun i mip -> + (fun i mip -> push mip.mind_typename (GlobRef.IndRef (mind,i)); Array.iteri (fun j id -> push id (GlobRef.ConstructRef ((mind,i),j+1))) - mip.mind_consnames) - mib.mind_packets + mip.mind_consnames) + mib.mind_packets type mod_ops = { import_module : export:bool -> ModPath.t -> unit @@ -285,22 +285,22 @@ let print_body is_impl extent env mp (l,body) = | SFBconst cb -> let ctx = Declareops.constant_polymorphic_context cb in (match cb.const_body with - | Def _ -> def "Definition" ++ spc () - | OpaqueDef _ when is_impl -> def "Theorem" ++ spc () - | _ -> def "Parameter" ++ spc ()) ++ name ++ + | Def _ -> def "Definition" ++ spc () + | OpaqueDef _ when is_impl -> def "Theorem" ++ spc () + | _ -> def "Parameter" ++ spc ()) ++ name ++ (match extent with | OnlyNames -> mt () | WithContents -> let bl = UnivNames.universe_binders_with_opt_names ctx None in let sigma = Evd.from_ctx (UState.of_binders bl) in - str " :" ++ spc () ++ + str " :" ++ spc () ++ hov 0 (Printer.pr_ltype_env env sigma cb.const_type) ++ - (match cb.const_body with - | Def l when is_impl -> - spc () ++ - hov 2 (str ":= " ++ + (match cb.const_body with + | Def l when is_impl -> + spc () ++ + hov 2 (str ":= " ++ Printer.pr_lconstr_env env sigma (Mod_subst.force_constr l)) - | _ -> mt ()) ++ str "." ++ + | _ -> mt ()) ++ str "." ++ Printer.pr_abstract_universe_ctx sigma ctx) | SFBmind mib -> match extent with @@ -314,7 +314,7 @@ let print_body is_impl extent env mp (l,body) = | BiFinite -> def "Variant" | CoFinite -> def "CoInductive" in - keyword ++ spc () ++ name) + keyword ++ spc () ++ name) let print_struct is_impl extent env mp struc = prlist_with_sep spc (print_body is_impl extent env mp) struc @@ -324,7 +324,7 @@ let print_structure ~mod_ops is_type extent env mp locals struc = nametab_register_module_body ~mod_ops mp struc; let kwd = if is_type then "Sig" else "Struct" in hv 2 (keyword kwd ++ spc () ++ print_struct false extent env' mp struc ++ - brk (1,-2) ++ keyword "End") + brk (1,-2) ++ keyword "End") let rec flatten_app mexpr l = match mexpr with | MEapply (mexpr, arg) -> flatten_app mexpr (arg::l) @@ -339,7 +339,7 @@ let rec print_typ_expr extent env mp locals mty = let fapp = List.hd lapp in let mapp = List.tl lapp in hov 3 (str"(" ++ (print_kn locals fapp) ++ spc () ++ - prlist_with_sep spc (print_modpath locals) mapp ++ str")") + prlist_with_sep spc (print_modpath locals) mapp ++ str")") | MEwith(me,WithDef(idl,(c, _)))-> let s = String.concat "." (List.map Id.to_string idl) in let body = match extent with @@ -378,7 +378,7 @@ let rec print_functor ~mod_ops fty fatom is_type extent env mp locals = function let kwd = if is_type then "Funsig" else "Functor" in hov 2 (keyword kwd ++ spc () ++ - str "(" ++ Id.print id ++ str ":" ++ pr_mtb1 ++ str ")" ++ + str "(" ++ Id.print id ++ str ":" ++ pr_mtb1 ++ str ")" ++ spc() ++ print_functor ~mod_ops fty fatom is_type extent env' mp locals' me2) let rec print_expression ~mod_ops x = @@ -399,11 +399,11 @@ let rec printable_body dir = try let open Nametab.GlobDirRef in match Nametab.locate_dir (qualid_of_dirpath dir) with - DirOpenModtype _ -> false - | DirModule _ | DirOpenModule _ -> printable_body dir - | _ -> true + DirOpenModtype _ -> false + | DirModule _ | DirOpenModule _ -> printable_body dir + | _ -> true with - Not_found -> true + Not_found -> true (** Since we might play with nametab above, we should reset to prior state after the printing *) diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 233163d097..dec87f8071 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -245,18 +245,18 @@ let process_goal sigma g : EConstr.t reified_goal = let hyps = List.map to_tuple hyps in { name; ty; hyps; env; sigma };; -let pr_letype_core goal_concl_style env sigma t = - Ppconstr.pr_lconstr_expr env sigma (Constrextern.extern_type goal_concl_style env sigma t) +let pr_letype_env ?lax ?goal_concl_style env sigma t = + Ppconstr.pr_lconstr_expr env sigma + (Constrextern.extern_type ?lax ?goal_concl_style env sigma t) let pp_of_type env sigma ty = - pr_letype_core true env sigma ty + pr_letype_env ~goal_concl_style:true env sigma ty -let pr_leconstr_core goal_concl_style env sigma t = - Ppconstr.pr_lconstr_expr env sigma (Constrextern.extern_constr goal_concl_style env sigma t) +let pr_leconstr_env ?lax ?inctx ?scope env sigma t = + Ppconstr.pr_lconstr_expr env sigma (Constrextern.extern_constr ?lax ?inctx ?scope env sigma t) -let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c) - -let pr_lconstr_env_econstr env sigma c = pr_leconstr_core false env sigma c +let pr_lconstr_env ?lax ?inctx ?scope env sigma c = + pr_leconstr_env ?lax ?inctx ?scope env sigma (EConstr.of_constr c) let diff_concl ?og_s nsigma ng = let open Evd in @@ -301,7 +301,7 @@ let goal_info goal sigma = line_idents := idents :: !line_idents; let mid = match body with | Some c -> - let pb = pr_lconstr_env_econstr env sigma c in + let pb = pr_leconstr_env env sigma c in let pb = if EConstr.isCast sigma c then surround pb else pb in str " := " ++ pb | None -> mt() in @@ -556,7 +556,7 @@ let to_constr pf = (* pprf generally has only one element, but it may have more in the derive plugin *) let t = List.hd pprf in let sigma, env = get_proof_context pf in - let x = Constrextern.extern_constr false env sigma t in (* todo: right options?? *) + let x = Constrextern.extern_constr env sigma t in (* todo: right options?? *) x.v diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index f6fca91eea..eebdaccd32 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -16,6 +16,9 @@ val write_diffs_option : string -> unit (** Returns true if the diffs option is "on" or "removed" *) val show_diffs : unit -> bool +(** Returns true if the diffs option is "removed" *) +val show_removed : unit -> bool + (** controls whether color output is enabled *) val write_color_enabled : bool -> unit @@ -54,9 +57,9 @@ val diff_goal : ?og_s:(Goal.goal sigma) -> Goal.goal -> Evd.evar_map -> Pp.t (** Convert a string to a list of token strings using the lexer *) val tokenize_string : string -> string list -val pr_letype_core : bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t -val pr_leconstr_core : bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t -val pr_lconstr_env : env -> evar_map -> constr -> Pp.t +val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t +val pr_leconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t +val pr_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> env -> evar_map -> constr -> Pp.t (** Computes diffs for a single conclusion *) val diff_concl : ?og_s:Goal.goal sigma -> Evd.evar_map -> Goal.goal -> Pp.t |