diff options
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 209 |
1 files changed, 209 insertions, 0 deletions
diff --git a/printing/printer.mli b/printing/printer.mli new file mode 100644 index 0000000000..9a06d555e4 --- /dev/null +++ b/printing/printer.mli @@ -0,0 +1,209 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open Constr +open Environ +open Pattern +open Evd +open Glob_term +open Ltac_pretype + +(** 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 + +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 + +(** 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 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 + +val pr_open_constr_env : env -> evar_map -> open_constr -> Pp.t + +val pr_open_lconstr_env : 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 + +val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t + +val pr_lglob_constr_env : env -> 'a glob_constr_g -> Pp.t + +val pr_glob_constr_env : env -> 'a glob_constr_g -> Pp.t + +val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t + +val pr_constr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t + +val pr_cases_pattern : cases_pattern -> Pp.t + +val pr_sort : evar_map -> Sorts.t -> Pp.t + +(** Universe constraints *) + +val pr_universe_instance : evar_map -> Univ.Instance.t -> Pp.t +val pr_universe_instance_constraints : evar_map -> Univ.Instance.t -> Univ.Constraint.t -> Pp.t +val pr_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> + Univ.UContext.t -> Pp.t +val pr_abstract_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> + Univ.AUContext.t -> priv:Univ.ContextSet.t option -> Pp.t +val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t +val pr_constant_universes : evar_map -> priv:Univ.ContextSet.t option -> Declarations.constant_universes -> Pp.t +val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t +val pr_abstract_cumulativity_info : evar_map -> Univ.ACumulativityInfo.t -> Pp.t + +(** Printing global references using names as short as possible *) + +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 +val pr_existential : env -> evar_map -> existential -> Pp.t +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 -> evar_map -> pconstant -> Pp.t +val pr_pinductive : env -> evar_map -> pinductive -> Pp.t +val pr_pconstructor : env -> evar_map -> pconstructor -> Pp.t + + +(** Contexts *) + +(** Display compact contexts of goals (simple hyps on the same line) *) +val set_compact_context : bool -> unit +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 -> 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 -> Constr.named_context -> Pp.t +val pr_named_context_of : env -> evar_map -> 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 + +(** Predicates *) + +val pr_predicate : ('a -> Pp.t) -> (bool * 'a list) -> Pp.t +val pr_cpred : Cpred.t -> Pp.t +val pr_idpred : Id.Pred.t -> Pp.t +val pr_transparent_state : TransparentState.t -> Pp.t + +(** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *) + +(** [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.goal sigma) -> Goal.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 * Goal.goal Evar.Map.t) -> Pp.t option -> evar_map + -> seeds:Goal.goal list -> shelf:Goal.goal list -> stack:int list + -> unfocused:Goal.goal list -> goals:Goal.goal list -> Pp.t + +val pr_subgoal : int -> evar_map -> Goal.goal list -> 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.goal sigma) -> evar_map -> Goal.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 +val pr_evars_int : evar_map -> shelf:Goal.goal list -> given_up:Goal.goal list -> int -> evar_info Evar.Map.t -> Pp.t +val pr_evars : evar_map -> evar_info Evar.Map.t -> Pp.t +val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map -> + Evar.Set.t -> Pp.t + +val print_and_diff : Proof.t option -> Proof.t option -> unit + +(** Declarations for the "Print Assumption" command *) +type axiom = + | Constant of Constant.t (* An axiom or a constant. *) + | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) + | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *) + +type context_object = + | Variable of Id.t (* A section variable or a Let definition *) + | Axiom of axiom * (Label.t * Constr.rel_context * types) list + | Opaque of Constant.t (* An opaque constant. *) + | Transparent of Constant.t + +module ContextObjectSet : Set.S with type elt = context_object +module ContextObjectMap : CMap.ExtS + with type key = context_object and module Set := ContextObjectSet + +val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t + +val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t + |