summaryrefslogtreecommitdiff
path: root/printing/printer.mli
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:23 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:23 -0500
commit9ebf44d84754adc5b64fcf612c6816c02c80462d (patch)
treebf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /printing/printer.mli
parent9043add656177eeac1491a73d2f3ab92bec0013c (diff)
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'printing/printer.mli')
-rw-r--r--printing/printer.mli97
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
-