Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: printer.mli Sprache: SML

Original von: Coq^©

(************************************************************************)
(*         *   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 ->
  ?priv:Univ.ContextSet.t -> Univ.AUContext.t -> Pp.t
val pr_universe_ctx_set    : evar_map -> Univ.ContextSet.t -> Pp.t
val pr_universes  : evar_map ->
  ?variance:Univ.Variance.t array -> ?priv:Univ.ContextSet.t ->
  Declarations.universes -> 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 *)
  | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism
                                       on parameter universes has not been checked. *)

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

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.