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
|
(************************************************************************)
(* 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 *)
(************************************************************************)
(* The proofview datastructure is a pure datastructure underlying the notion
of proof (namely, a proof is a proofview which can evolve and has safety
mechanisms attached).
The general idea of the structure is that it is composed of a chemical
solution: an unstructured bag of stuff which has some relations with
one another, which represents the various subnodes of the proof, together
with a comb: a datastructure that gives order to some of these nodes,
namely the open goals.
The natural candidate for the solution is an {!Evd.evar_map}, that is
a calculus of evars. The comb is then a list of goals (evars wrapped
with some extra information, like possible name anotations).
There is also need of a list of the evars which initialised the proofview
to be able to return information about the proofview. *)
open Term
type proofview
(* Initialises a proofview, the argument is a list of environement,
conclusion types, creating that many initial goals. *)
val init : (Environ.env * Term.types) list -> proofview
(* Returns whether this proofview is finished or not.That is,
if it has empty subgoals in the comb. There could still be unsolved
subgoaled, but they would then be out of the view, focused out. *)
val finished : proofview -> bool
(* Returns the current value of the proofview partial proofs. *)
val return : proofview -> (constr*types) list
(*** Focusing operations ***)
(* [IndexOutOfRange] occurs in case of malformed indices
with respect to list lengths. *)
exception IndexOutOfRange
(* Type of the object which allow to unfocus a view.*)
type focus_context
(* [focus i j] focuses a proofview on the goals from index [i] to index [j]
(inclusive). (i.e. goals number [i] to [j] become the only goals of the
returned proofview).
It returns the focus proof, and a context for the focus trace. *)
val focus : int -> int -> proofview -> proofview * focus_context
(* Unfocuses a proofview with respect to a context. *)
val unfocus : focus_context -> proofview -> proofview
(* The tactic monad:
- Tactics are objects which apply a transformation to all
the subgoals of the current view at the same time. By opposed
to the old vision of applying it to a single goal. It mostly
allows to consider tactic like [reorder] to reorder the goals
in the current view (which might be useful for the tactic designer)
(* spiwack: the ordering of goals, though, is actually rather
brittle. It would be much more interesting to find a more
robust way to adress goals, I have no idea at this time
though*)
or global automation tactic for dependent subgoals (instantiating
an evar has influences on the other goals of the proof in progress,
not being able to take that into account causes the current eauto
tactic to fail on some instances where it could succeed).
- Tactics are a monad ['a tactic], in a sense a tactic can be
seens as a function (without argument) which returns a value
of type 'a and modifies the environement (in our case: the view).
Tactics of course have arguments, but these are given at the
meta-level as OCaml functions.
Most tactics in the sense we are used to return [ () ], that is
no really interesting values. But some might, to pass information
around; for instance [Proofview.freeze] allows to store a certain
goal sensitive value "at the present time" (which means, considering the
structure of the dynamics of proofs, [Proofview.freeze s] will have,
for every current goal [gl], and for any of its descendent [g'] in
the future the same value in [g'] that in [gl]).
(* spiwack: I don't know how much all this relates to F. Kirchner and
C. Muñoz. I wasn't able to understand how they used the monad
structure in there developpement.
*)
The tactics seen in Coq's Ltac are (for now at least) only
[unit tactic], the return values are kept for the OCaml toolkit.
The operation or the monad are [Proofview.tclIDTAC] (which is the
"return" of the tactic monad) [Proofview.tclBIND] (which is
the "bind") and [Proofview.tclTHEN] (which is a specialized
bind on unit-returning tactics).
*)
type +'a tactic
(* Applies a tactic to the current proofview. *)
val apply : Environ.env -> 'a tactic -> proofview -> proofview
(*** tacticals ***)
(* Unit of the tactic monad *)
val tclUNIT : 'a -> 'a tactic
(* Bind operation of the tactic monad *)
val tclBIND : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
(* Interprets the ";" (semicolon) of Ltac.
As a monadic operation, it's a specialized "bind"
on unit-returning tactic (meaning "there is no value to bind") *)
val tclTHEN : unit tactic -> 'a tactic -> 'a tactic
(* [tclIGNORE t] has the same operational content as [t],
but drops the value at the end. *)
val tclIGNORE : 'a tactic -> unit tactic
(* [tclOR t1 t2 = t1] if t1 succeeds and [tclOR t1 t2 = t2] if t2 fails.
No interleaving at this point. *)
val tclOR : 'a tactic -> 'a tactic -> 'a tactic
(* [tclZERO] always fails *)
val tclZERO : exn -> 'a tactic
(* Focuses a tactic at a range of subgoals, found by their indices. *)
val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
(* Dispatch tacticals are used to apply a different tactic to each goal under
consideration. They come in two flavours:
[tclDISPATCH] takes a list of [unit tactic]-s and build a [unit tactic].
[tclDISPATCHS] takes a list of ['a sensitive tactic] and returns and returns
and ['a sensitive tactic] where the ['a sensitive] interpreted in a goal [g]
corresponds to that of the tactic which created [g].
It is to be noted that the return value of [tclDISPATCHS ts] makes only
sense in the goals immediatly built by it, and would cause an anomaly
is used otherwise. *)
val tclDISPATCH : unit tactic list -> unit tactic
val tclDISPATCHS : 'a Goal.sensitive tactic list -> 'a Goal.sensitive tactic
(* [tclEXTEND b r e] is a variant to [tclDISPATCH], where the [r] tactic
is "repeated" enough time such that every goal has a tactic assigned to it
([b] is the list of tactics applied to the first goals, [e] to the last goals, and [r]
is applied to every goal in between. *)
val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tactic
(* A sort of bind which takes a [Goal.sensitive] as a first argument,
the tactic then acts on each goal separately.
Allows backtracking between goals. *)
val tclGOALBIND : 'a Goal.sensitive -> ('a -> 'b Goal.sensitive tactic) -> 'b Goal.sensitive tactic
val tclGOALBINDU : 'a Goal.sensitive -> ('a -> unit tactic) -> unit tactic
(* [tclSENSITIVE] views goal-type tactics as a special kind of tactics.*)
val tclSENSITIVE : Goal.subgoals Goal.sensitive -> unit tactic
(*** Commands ***)
val in_proofview : proofview -> (Evd.evar_map -> 'a) -> 'a
(* Notations for building tactics. *)
module Notations : sig
(* Goal.bind *)
val (>-) : 'a Goal.sensitive -> ('a -> 'b Goal.sensitive) -> 'b Goal.sensitive
(* tclGOALBINDU *)
val (>>-) : 'a Goal.sensitive -> ('a -> unit tactic) -> unit tactic
(* tclGOALBIND *)
val (>>--) : 'a Goal.sensitive -> ('a -> 'b Goal.sensitive tactic) -> 'b Goal.sensitive tactic
(* tclBIND *)
val (>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
(* [(>>=)] (and its goal sensitive variant [(>>==)]) "binds" in one step the
tactic monad and the goal-sensitive monad.
It is strongly advised to use it everytieme an ['a Goal.sensitive tactic]
needs a bind, since it usually avoids to delay the interpretation of the
goal sensitive value to a location where it does not make sense anymore. *)
val (>>=) : 'a Goal.sensitive tactic -> ('a -> unit tactic) -> unit tactic
val (>>==) : 'a Goal.sensitive tactic -> ('a -> 'b Goal.sensitive tactic) -> 'b Goal.sensitive tactic
(* tclTHEN *)
val (<*>) : unit tactic -> 'a tactic -> 'a tactic
(* tclOR *)
val (<+>) : 'a tactic -> 'a tactic -> 'a tactic
end
(*** Compatibility layer with <= 8.2 tactics ***)
module V82 : sig
type tac = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
val tactic : tac -> unit tactic
val has_unresolved_evar : proofview -> bool
(* Main function in the implementation of Grab Existential Variables.
Resets the proofview's goals so that it contains all unresolved evars
(in chronological order of insertion). *)
val grab : proofview -> proofview
(* Returns the open goals of the proofview together with the evar_map to
interprete them. *)
val goals : proofview -> Goal.goal list Evd.sigma
val top_goals : proofview -> Goal.goal list Evd.sigma
(* returns the existential variable used to start the proof *)
val top_evars : proofview -> Evd.evar list
(* Implements the Existential command *)
val instantiate_evar : int -> Topconstr.constr_expr -> proofview -> proofview
(* spiwack: [purify] might be useful while writing tactics manipulating exception
explicitely or from the [V82] submodule (neither being advised, though *)
val purify : 'a tactic -> 'a tactic
end
|
