diff options
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 97 |
1 files changed, 56 insertions, 41 deletions
diff --git a/printing/printer.mli b/printing/printer.mli index 41843680..518c5b93 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Globnames open Constr open Environ open Pattern @@ -37,7 +36,7 @@ val pr_constr : constr -> Pp.t [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t -val pr_constr_n_env : env -> evar_map -> Notation_term.tolerability -> constr -> Pp.t +val pr_constr_n_env : 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 "??" @@ -58,7 +57,7 @@ val pr_leconstr_env : env -> evar_map -> EConstr.t -> Pp.t val pr_leconstr : EConstr.t -> Pp.t [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] -val pr_econstr_n_env : env -> evar_map -> Notation_term.tolerability -> EConstr.t -> Pp.t +val pr_econstr_n_env : env -> evar_map -> Notation_gram.tolerability -> 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 @@ -88,7 +87,7 @@ val pr_type_env : env -> evar_map -> types -> Pp.t val pr_type : types -> Pp.t [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] -val pr_closed_glob_n_env : env -> evar_map -> Notation_term.tolerability -> closed_glob_constr -> 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 val pr_closed_glob : closed_glob_constr -> Pp.t [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] @@ -121,7 +120,7 @@ val pr_sort : evar_map -> Sorts.t -> Pp.t val pr_polymorphic : bool -> Pp.t val pr_cumulative : bool -> bool -> Pp.t -val pr_universe_instance : evar_map -> Univ.UContext.t -> Pp.t +val pr_universe_instance : evar_map -> Univ.Instance.t -> Pp.t val pr_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> Univ.UContext.t -> Pp.t val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t @@ -130,8 +129,8 @@ val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t (** Printing global references using names as short as possible *) -val pr_global_env : Id.Set.t -> global_reference -> Pp.t -val pr_global : global_reference -> Pp.t +val pr_global_env : Id.Set.t -> GlobRef.t -> Pp.t +val pr_global : GlobRef.t -> Pp.t val pr_constant : env -> Constant.t -> Pp.t val pr_existential_key : evar_map -> Evar.t -> Pp.t @@ -140,9 +139,9 @@ val pr_constructor : env -> constructor -> Pp.t val pr_inductive : env -> inductive -> Pp.t val pr_evaluable_reference : evaluable_global_reference -> Pp.t -val pr_pconstant : env -> pconstant -> Pp.t -val pr_pinductive : env -> pinductive -> Pp.t -val pr_pconstructor : env -> pconstructor -> Pp.t +val pr_pconstant : env -> evar_map -> pconstant -> Pp.t +val pr_pinductive : env -> evar_map -> pinductive -> Pp.t +val pr_pconstructor : env -> evar_map -> pconstructor -> Pp.t (** Contexts *) @@ -153,13 +152,13 @@ val get_compact_context : unit -> bool val pr_context_unlimited : env -> evar_map -> Pp.t val pr_ne_context_of : Pp.t -> env -> evar_map -> Pp.t -val pr_named_decl : env -> evar_map -> Context.Named.Declaration.t -> Pp.t -val pr_compacted_decl : env -> evar_map -> Context.Compacted.Declaration.t -> Pp.t -val pr_rel_decl : env -> evar_map -> Context.Rel.Declaration.t -> Pp.t +val pr_named_decl : env -> evar_map -> Constr.named_declaration -> Pp.t +val pr_compacted_decl : env -> evar_map -> Constr.compacted_declaration -> Pp.t +val pr_rel_decl : env -> evar_map -> Constr.rel_declaration -> Pp.t -val pr_named_context : env -> evar_map -> Context.Named.t -> Pp.t +val pr_named_context : env -> evar_map -> Constr.named_context -> Pp.t val pr_named_context_of : env -> evar_map -> Pp.t -val pr_rel_context : env -> evar_map -> Context.Rel.t -> Pp.t +val pr_rel_context : env -> evar_map -> Constr.rel_context -> Pp.t val pr_rel_context_of : env -> evar_map -> Pp.t val pr_context_of : env -> evar_map -> Pp.t @@ -172,22 +171,46 @@ val pr_transparent_state : transparent_state -> Pp.t (** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *) -val pr_goal : goal sigma -> Pp.t - -(** [pr_subgoals ~pr_first pp sigma seeds shelf focus_stack unfocused goals] - prints the goals of the list [goals] followed by the goals in - [unfocused], in a short way (typically only the conclusion) except - for the first goal if [pr_first] is true. This function can be - replaced by another one by calling [set_printer_pr] (see below), - typically by plugin writers. The default printer prints only the - focused goals unless the conrresponding option - [enable_unfocused_goal_printing] is set. [seeds] is for printing - dependent evars (mainly for emacs proof tree mode). *) -val pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t +(** [pr_goal ~diffs ~og_s g_s] prints the goal specified by [g_s]. If [diffs] is true, + highlight the differences between the old goal, [og_s], and [g_s]. [g_s] and [og_s] are + records containing the goal and sigma for, respectively, the new and old proof steps, + e.g. [{ it = g ; sigma = sigma }]. +*) +val pr_goal : ?diffs:bool -> ?og_s:(goal sigma) -> goal sigma -> Pp.t + +(** [pr_subgoals ~pr_first ~diffs ~os_map close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals] + prints the goals in [goals] followed by the goals in [unfocused] in a compact form + (typically only the conclusion). If [pr_first] is true, print the first goal in full. + [close_cmd] is printed afterwards verbatim. + + If [diffs] is true, then highlight diffs relative to [os_map] in the output for first goal. + [os_map] contains sigma for the old proof step and the goal map created by + [Proof_diffs.make_goal_map]. + + This function prints only the focused goals unless the corresponding option [enable_unfocused_goal_printing] is set. + [seeds] is for printing dependent evars (mainly for emacs proof tree mode). [shelf] is from + Proof.proof and is used to identify shelved goals in a message if there are no more subgoals but + there are non-instantiated existential variables. [stack] is used to print summary info on unfocused + goals. +*) +val pr_subgoals : ?pr_first:bool -> ?diffs:bool -> ?os_map:(evar_map * Evar.t Evar.Map.t) -> Pp.t option -> evar_map + -> seeds:goal list -> shelf:goal list -> stack:int list + -> unfocused: goal list -> goals:goal list -> Pp.t val pr_subgoal : int -> evar_map -> goal list -> Pp.t -val pr_concl : int -> evar_map -> goal -> Pp.t +(** [pr_concl n ~diffs ~og_s sigma g] prints the conclusion of the goal [g] using [sigma]. The output + is labelled "subgoal [n]". If [diffs] is true, highlight the differences between the old conclusion, + [og_s], and [g]+[sigma]. [og_s] is a record containing the old goal and sigma, e.g. [{ it = g ; sigma = sigma }]. +*) +val pr_concl : int -> ?diffs:bool -> ?og_s:(goal sigma) -> evar_map -> goal -> Pp.t + +(** [pr_open_subgoals_diff ~quiet ~diffs ~oproof proof] shows the context for [proof] as used by, for example, coqtop. + The first active goal is printed with all its antecedents and the conclusion. The other active goals only show their + conclusions. If [diffs] is true, highlight the differences between the old proof, [oproof], and [proof]. [quiet] + disables printing messages as Feedback. +*) +val pr_open_subgoals_diff : ?quiet:bool -> ?diffs:bool -> ?oproof:Proof.t -> Proof.t -> Pp.t val pr_open_subgoals : proof:Proof.t -> Pp.t val pr_nth_open_subgoal : proof:Proof.t -> int -> Pp.t val pr_evar : evar_map -> (Evar.t * evar_info) -> Pp.t @@ -197,11 +220,14 @@ val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map -> Evar.Set.t -> Pp.t val pr_prim_rule : prim_rule -> Pp.t +[@@ocaml.deprecated "[pr_prim_rule] is scheduled to be removed along with the legacy proof engine"] + +val print_and_diff : Proof.t option -> Proof.t option -> unit (** Backwards compatibility *) val prterm : constr -> Pp.t (** = pr_lconstr *) - +[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] (** Declarations for the "Print Assumption" command *) type axiom = @@ -211,7 +237,7 @@ type axiom = type context_object = | Variable of Id.t (* A section variable or a Let definition *) - | Axiom of axiom * (Label.t * Context.Rel.t * types) list + | Axiom of axiom * (Label.t * Constr.rel_context * types) list | Opaque of Constant.t (* An opaque constant. *) | Transparent of Constant.t @@ -223,14 +249,3 @@ val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t -type printer_pr = { - pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t; - - pr_subgoal : int -> evar_map -> goal list -> Pp.t; - pr_goal : goal sigma -> Pp.t; -} - -val set_printer_pr : printer_pr -> unit - -val default_printer_pr : printer_pr - |