1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: refiner.mli 11735 2009-01-02 17:22:31Z herbelin $ i*)
20
(* The refiner (handles primitive rules and high-level tactics). *)
22
val sig_it : 'a sigma -> 'a
23
val project : 'a sigma -> evar_map
25
val pf_env : goal sigma -> Environ.env
26
val pf_hyps : goal sigma -> named_context
28
val unpackage : 'a sigma -> evar_map ref * 'a
29
val repackage : evar_map ref -> 'a -> 'a sigma
31
evar_map ref -> (goal sigma -> (goal list) sigma * validation) -> goal -> (goal list) * validation
33
type transformation_tactic = proof_tree -> (goal list * validation)
35
(*s Hiding the implementation of tactics. *)
37
(* [abstract_tactic tac] hides the (partial) proof produced by [tac] under
38
a single proof node. The boolean tells if the default tactic is used. *)
39
val abstract_operation : compound_rule -> tactic -> tactic
40
val abstract_tactic : ?dflt:bool -> atomic_tactic_expr -> tactic -> tactic
41
val abstract_tactic_expr : ?dflt:bool -> tactic_expr -> tactic -> tactic
42
val abstract_extended_tactic :
43
?dflt:bool -> string -> typed_generic_argument list -> tactic -> tactic
45
val refiner : rule -> tactic
46
val frontier : transformation_tactic
47
val list_pf : proof_tree -> goal list
48
val unTAC : tactic -> goal sigma -> proof_tree sigma
51
(* Install a hook frontier_map and frontier_mapi call on the new node they create *)
52
val set_solve_hook : (Proof_type.proof_tree -> unit) -> unit
53
(* [frontier_map f n p] applies f on the n-th open subgoal of p and
55
n=1 for first goal, n negative counts from the right *)
57
(proof_tree -> proof_tree) -> int -> proof_tree -> proof_tree
59
(* [frontier_mapi f p] applies (f i) on the i-th open subgoal of p. *)
61
(int -> proof_tree -> proof_tree) -> proof_tree -> proof_tree
65
(* [tclNORMEVAR] forces propagation of evar constraints *)
66
val tclNORMEVAR : tactic
68
(* [tclIDTAC] is the identity tactic without message printing*)
70
val tclIDTAC_MESSAGE : Pp.std_ppcmds -> tactic
72
(* [tclEVARS sigma] changes the current evar map *)
73
val tclEVARS : evar_map -> tactic
75
(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
76
[tac2] to every resulting subgoals *)
77
val tclTHEN : tactic -> tactic -> tactic
79
(* [tclTHENLIST [t1;..;tn]] applies [t1] THEN [t2] ... THEN [tn]. More
80
convenient than [tclTHEN] when [n] is large *)
81
val tclTHENLIST : tactic list -> tactic
83
(* [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
84
[(tac2 i)] to the [i]$^{th}$ resulting subgoal (starting from 1) *)
85
val tclTHEN_i : tactic -> (int -> tactic) -> tactic
87
(* [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
88
to the last resulting subgoal (previously called [tclTHENL]) *)
89
val tclTHENLAST : tactic -> tactic -> tactic
91
(* [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
92
to the first resulting subgoal *)
93
val tclTHENFIRST : tactic -> tactic -> tactic
95
(* [tclTHENS tac1 [|t1 ; ... ; tn|] gls] applies the tactic [tac1] to
96
[gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises
97
an error if the number of resulting subgoals is not [n] *)
98
val tclTHENSV : tactic -> tactic array -> tactic
100
(* Same with a list of tactics *)
101
val tclTHENS : tactic -> tactic list -> tactic
103
(* [tclTHENST] is renamed [tclTHENSFIRSTn]
104
val tclTHENST : tactic -> tactic array -> tactic -> tactic
107
(* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
108
applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
109
the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m]
110
subgoals and [tac2] to the rest of the subgoals in the middle. Raises an
111
error if the number of resulting subgoals is strictly less than [n+m] *)
112
val tclTHENS3PARTS : tactic -> tactic array -> tactic -> tactic array -> tactic
114
(* [tclTHENSLASTn tac1 [t1 ; ... ; tn] tac2 gls] applies [t1],...,[tn] on the
115
last [n] resulting subgoals and [tac2] on the remaining first subgoals *)
116
val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic
118
(* [tclTHENSFIRSTn tac1 [t1 ; ... ; tn] tac2 gls] first applies [tac1], then
119
applies [t1],...,[tn] on the first [n] resulting subgoals and
120
[tac2] for the remaining last subgoals (previously called tclTHENST) *)
121
val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic
123
(* [tclTHENLASTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then,
124
applies [t1],...,[tn] on the last [n] resulting subgoals and leaves
125
unchanged the other subgoals *)
126
val tclTHENLASTn : tactic -> tactic array -> tactic
128
(* [tclTHENFIRSTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then,
129
applies [t1],...,[tn] on the first [n] resulting subgoals and leaves
130
unchanged the other subgoals (previously called [tclTHENSI]) *)
131
val tclTHENFIRSTn : tactic -> tactic array -> tactic
133
(* A special exception for levels for the Fail tactic *)
134
exception FailError of int * Pp.std_ppcmds
136
(* Takes an exception and either raise it at the next
137
level or do nothing. *)
138
val catch_failerror : exn -> unit
140
val tclORELSE0 : tactic -> tactic -> tactic
141
val tclORELSE : tactic -> tactic -> tactic
142
val tclREPEAT : tactic -> tactic
143
val tclREPEAT_MAIN : tactic -> tactic
144
val tclFIRST : tactic list -> tactic
145
val tclSOLVE : tactic list -> tactic
146
val tclTRY : tactic -> tactic
147
val tclTHENTRY : tactic -> tactic -> tactic
148
val tclCOMPLETE : tactic -> tactic
149
val tclAT_LEAST_ONCE : tactic -> tactic
150
val tclFAIL : int -> Pp.std_ppcmds -> tactic
151
val tclDO : int -> tactic -> tactic
152
val tclPROGRESS : tactic -> tactic
153
val tclWEAK_PROGRESS : tactic -> tactic
154
val tclNOTSAMEGOAL : tactic -> tactic
155
val tclINFO : tactic -> tactic
157
(* [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,
158
if it succeeds, applies [tac2] to the resulting subgoals,
159
and if not applies [tac3] to the initial goal [gls] *)
160
val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic
161
val tclIFTHENSELSE : tactic -> tactic list -> tactic ->tactic
162
val tclIFTHENSVELSE : tactic -> tactic array -> tactic ->tactic
164
(* [tclIFTHENTRYELSEMUST tac1 tac2 gls] applies [tac1] then [tac2]. If [tac1]
165
has been successful, then [tac2] may fail. Otherwise, [tac2] must succeed.
166
Equivalent to [(tac1;try tac2)||tac2] *)
168
val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
170
(*s Tactics handling a list of goals. *)
172
type validation_list = proof_tree list -> proof_tree list
174
type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
176
val tclFIRSTLIST : tactic_list list -> tactic_list
177
val tclIDTAC_list : tactic_list
178
val first_goal : 'a list sigma -> 'a sigma
179
val apply_tac_list : tactic -> tactic_list
180
val then_tactic_list : tactic_list -> tactic_list -> tactic_list
181
val tactic_list_tactic : tactic_list -> tactic
182
val goal_goal_list : 'a sigma -> 'a list sigma
185
(*s Functions for handling the state of the proof editor. *)
189
val proof_of_pftreestate : pftreestate -> proof_tree
190
val cursor_of_pftreestate : pftreestate -> int list
191
val is_top_pftreestate : pftreestate -> bool
192
val match_rule : (rule -> bool) -> pftreestate -> bool
193
val evc_of_pftreestate : pftreestate -> evar_map
194
val top_goal_of_pftreestate : pftreestate -> goal sigma
195
val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
197
val traverse : int -> pftreestate -> pftreestate
198
val map_pftreestate :
199
(evar_map ref -> proof_tree -> proof_tree) -> pftreestate -> pftreestate
200
val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate
201
val solve_pftreestate : tactic -> pftreestate -> pftreestate
203
(* a weak version of logical undoing, that is really correct only *)
204
(* if there are no existential variables. *)
205
val weak_undo_pftreestate : pftreestate -> pftreestate
207
val mk_pftreestate : goal -> pftreestate
208
val extract_open_proof : evar_map -> proof_tree -> constr * (int * types) list
209
val extract_open_pftreestate : pftreestate -> constr * Termops.metamap
210
val extract_pftreestate : pftreestate -> constr
211
val first_unproven : pftreestate -> pftreestate
212
val last_unproven : pftreestate -> pftreestate
213
val nth_unproven : int -> pftreestate -> pftreestate
214
val node_prev_unproven : int -> pftreestate -> pftreestate
215
val node_next_unproven : int -> pftreestate -> pftreestate
216
val next_unproven : pftreestate -> pftreestate
217
val prev_unproven : pftreestate -> pftreestate
218
val top_of_tree : pftreestate -> pftreestate
219
val match_rule : (rule -> bool) -> pftreestate -> bool
220
val up_until_matching_rule : (rule -> bool) ->
221
pftreestate -> pftreestate
222
val up_to_matching_rule : (rule -> bool) ->
223
pftreestate -> pftreestate
224
val change_rule : (rule -> rule) -> pftreestate -> pftreestate
225
val change_constraints_pftreestate
226
: evar_map -> pftreestate -> pftreestate
229
(*s Pretty-printers. *)
234
val set_info_printer :
235
(evar_map -> named_context -> proof_tree -> Pp.std_ppcmds) -> unit
added
removed
proofs/refiner.mli
