blob: b5003425bd2300a0552f0eb3ce51aa31a02e9e39 (
plain)
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id$ i*)
(*i*)
open Util
open Pp
open Names
open Term
open Sign
open Environ
open Decl_kinds
open Tacmach
open Tacexpr
(*i*)
(*s Several proofs can be opened simultaneously but at most one is
focused at some time. The following functions work by side-effect
on current set of open proofs. In this module, ``proofs'' means an
open proof (something started by vernacular command [Goal], [Lemma]
or [Theorem]), and ``goal'' means a subgoal of the current focused
proof *)
(*s [refining ()] tells if there is some proof in progress, even if a not
focused one *)
val refining : unit -> bool
(* [check_no_pending_proofs ()] fails if there is still some proof in
progress *)
val check_no_pending_proofs : unit -> unit
(*s [delete_proof name] deletes proof of name [name] or fails if no proof
has this name *)
val delete_proof : identifier located -> unit
(* [delete_current_proof ()] deletes current focused proof or fails if
no proof is focused *)
val delete_current_proof : unit -> unit
(* [delete_all_proofs ()] deletes all open proofs if any *)
val delete_all_proofs : unit -> unit
(*s [undo n] undoes the effect of the last [n] tactics applied to the
current proof; it fails if no proof is focused or if the ``undo''
stack is exhausted *)
val undo : int -> unit
(* Same as undo, but undoes the current proof stack to reach depth
[n]. This is used in [vernac_backtrack]. *)
val undo_todepth : int -> unit
(* Returns the depth of the current focused proof stack, this is used
to put informations in coq prompt (in emacs mode). *)
val current_proof_depth: unit -> int
(* [set_undo (Some n)] sets the size of the ``undo'' stack; [set_undo None]
sets the size to the default value (12) *)
val set_undo : int option -> unit
val get_undo : unit -> int option
(*s [start_proof s str env t hook tac] starts a proof of name [s] and
conclusion [t]; [hook] is optionally a function to be applied at
proof end (e.g. to declare the built constructions as a coercion
or a setoid morphism); init_tac is possibly a tactic to
systematically apply at initialization time (e.g. to start the
proof of mutually dependent theorems) *)
type lemma_possible_guards = int list list
val start_proof :
identifier -> goal_kind -> named_context_val -> constr ->
?init_tac:tactic -> ?compute_guard:lemma_possible_guards ->
declaration_hook -> unit
(* [restart_proof ()] restarts the current focused proof from the beginning
or fails if no proof is focused *)
val restart_proof : unit -> unit
(*s [resume_last_proof ()] focus on the last unfocused proof or fails
if there is no suspended proofs *)
val resume_last_proof : unit -> unit
(* [resume_proof name] focuses on the proof of name [name] or
raises [UserError] if no proof has name [name] *)
val resume_proof : identifier located -> unit
(* [suspend_proof ()] unfocuses the current focused proof or
failed with [UserError] if no proof is currently focused *)
val suspend_proof : unit -> unit
(*s [cook_proof opacity] turns the current proof (assumed completed) into
a constant with its name, kind and possible hook (see [start_proof]);
it fails if there is no current proof of if it is not completed;
it also tells if the guardness condition has to be inferred. *)
val cook_proof : (Refiner.pftreestate -> unit) ->
identifier *
(Entries.definition_entry * lemma_possible_guards * goal_kind *
declaration_hook)
(* To export completed proofs to xml *)
val set_xml_cook_proof : (goal_kind * pftreestate -> unit) -> unit
(*s [get_pftreestate ()] returns the current focused pending proof or
raises [UserError "no focused proof"] *)
val get_pftreestate : unit -> pftreestate
(* [get_end_tac ()] returns the current tactic to apply to all new subgoal *)
val get_end_tac : unit -> tactic option
(* [get_goal_context n] returns the context of the [n]th subgoal of
the current focused proof or raises a [UserError] if there is no
focused proof or if there is no more subgoals *)
val get_goal_context : int -> Evd.evar_map * env
(* [get_current_goal_context ()] works as [get_goal_context 1] *)
val get_current_goal_context : unit -> Evd.evar_map * env
(* [current_proof_statement] *)
val current_proof_statement :
unit -> identifier * goal_kind * types * declaration_hook
(*s [get_current_proof_name ()] return the name of the current focused
proof or failed if no proof is focused *)
val get_current_proof_name : unit -> identifier
(* [get_all_proof_names ()] returns the list of all pending proof names *)
val get_all_proof_names : unit -> identifier list
(*s [set_end_tac tac] applies tactic [tac] to all subgoal generate
by [solve_nth] *)
val set_end_tac : tactic -> unit
(*s [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the
current focused proof or raises a UserError if no proof is focused or
if there is no [n]th subgoal *)
val solve_nth : int -> tactic -> unit
(* [by tac] applies tactic [tac] to the 1st subgoal of the current
focused proof or raises a UserError if there is no focused proof or
if there is no more subgoals *)
val by : tactic -> unit
(* [instantiate_nth_evar_com n c] instantiate the [n]th undefined
existential variable of the current focused proof by [c] or raises a
UserError if no proof is focused or if there is no such [n]th
existential variable *)
val instantiate_nth_evar_com : int -> Topconstr.constr_expr -> unit
(*s To deal with subgoal focus *)
val make_focus : int -> unit
val focus : unit -> int
val focused_goal : unit -> int
val subtree_solved : unit -> bool
val tree_solved : unit -> bool
val top_tree_solved : unit -> bool
val reset_top_of_tree : unit -> unit
val reset_top_of_script : unit -> unit
val traverse : int -> unit
val traverse_nth_goal : int -> unit
val traverse_next_unproven : unit -> unit
val traverse_prev_unproven : unit -> unit
(* These two functions make it possible to implement more elaborate
proof and goal management, as it is done, for instance in pcoq *)
val traverse_to : int list -> unit
val mutate : (pftreestate -> pftreestate) -> unit
(* [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *)
val build_constant_by_tactic : named_context_val -> types -> tactic ->
Entries.definition_entry
val build_by_tactic : types -> tactic -> constr
|
