-
Notifications
You must be signed in to change notification settings - Fork 632
/
printer.mli
269 lines (201 loc) · 13.2 KB
/
printer.mli
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \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
open Notation_term
(** These are the entry points for printing terms, context, tac, ... *)
val print_goal_tag_opt_name : string list
(** Terms *)
(** 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].
[~impargs:some_list_of_binding_kind] indicates the implicit arguments
of the external quatification. Only used for printing types (not
terms), and at toplevel (only "l" versions). It defaults to [None].
[~lax:true] is for debugging purpose. It defaults to [~lax:false]. *)
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 -> Constrexpr.entry_relative_level -> 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_constr_env : env -> evar_map -> constr -> Pp.t
val safe_pr_lconstr_env : env -> evar_map -> constr -> 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_econstr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> EConstr.t -> 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 -> ?impargs:Glob_term.binding_kind list -> EConstr.types -> 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
(** 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 -> ?impargs:Glob_term.binding_kind list -> 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 -> Constrexpr.entry_relative_level -> 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
val pr_lglob_constr_env : env -> evar_map -> 'a glob_constr_g -> Pp.t
val pr_glob_constr_env : env -> evar_map -> '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.Constraints.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.AbstractContext.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
(** [universe_binders_with_opt_names ref l]
If [l] is [Some univs] return the universe binders naming the
bound levels of [ref] by [univs] (generating names for Anonymous).
May error if the lengths mismatch.
Otherwise return the bound universe names registered for [ref].
Inefficient on large contexts due to name generation. *)
val universe_binders_with_opt_names : Univ.AbstractContext.t ->
UnivNames.univ_name_list option -> UnivNames.universe_binders
(** 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 : Tacred.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
val print_dependent_evars : Evar.t option -> evar_map -> Evar.t list -> Pp.t
(** 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 GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
| TypeInType of GlobRef.t (* a constant which relies on type in type *)
| UIP of MutInd.t (* An inductive using the special reduction rule. *)
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
val pr_goal_emacs : proof:Proof.t option -> int -> int -> Pp.t
val pr_typing_flags : Declarations.typing_flags -> Pp.t
(** Tells if flag "Printing Goal Names" is activated *)
val print_goal_names : unit -> bool