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
(* $Id: tacticals.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
32
(******************************************)
34
(******************************************)
36
(*************************************************)
37
(* Tacticals re-exported from the Refiner module.*)
38
(*************************************************)
40
let tclNORMEVAR = tclNORMEVAR
41
let tclIDTAC = tclIDTAC
42
let tclIDTAC_MESSAGE = tclIDTAC_MESSAGE
43
let tclORELSE0 = tclORELSE0
44
let tclORELSE = tclORELSE
46
let tclTHENLIST = tclTHENLIST
47
let tclTHEN_i = tclTHEN_i
48
let tclTHENFIRST = tclTHENFIRST
49
let tclTHENLAST = tclTHENLAST
50
let tclTHENS = tclTHENS
51
let tclTHENSV = Refiner.tclTHENSV
52
let tclTHENSFIRSTn = Refiner.tclTHENSFIRSTn
53
let tclTHENSLASTn = Refiner.tclTHENSLASTn
54
let tclTHENFIRSTn = Refiner.tclTHENFIRSTn
55
let tclTHENLASTn = Refiner.tclTHENLASTn
56
let tclREPEAT = Refiner.tclREPEAT
57
let tclREPEAT_MAIN = tclREPEAT_MAIN
58
let tclFIRST = Refiner.tclFIRST
59
let tclSOLVE = Refiner.tclSOLVE
60
let tclTRY = Refiner.tclTRY
61
let tclINFO = Refiner.tclINFO
62
let tclCOMPLETE = Refiner.tclCOMPLETE
63
let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE
64
let tclFAIL = Refiner.tclFAIL
65
let tclDO = Refiner.tclDO
66
let tclPROGRESS = Refiner.tclPROGRESS
67
let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS
68
let tclNOTSAMEGOAL = Refiner.tclNOTSAMEGOAL
69
let tclTHENTRY = tclTHENTRY
70
let tclIFTHENELSE = tclIFTHENELSE
71
let tclIFTHENSELSE = tclIFTHENSELSE
72
let tclIFTHENSVELSE = tclIFTHENSVELSE
73
let tclIFTHENTRYELSEMUST = tclIFTHENTRYELSEMUST
77
(* [rclTHENSEQ [t1;..;tn] is equivalent to t1;..;tn *)
78
let tclTHENSEQ = tclTHENLIST
80
(* map_tactical f [x1..xn] = (f x1);(f x2);...(f xn) *)
81
(* tclMAP f [x1..xn] = (f x1);(f x2);...(f xn) *)
83
List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC
85
(* apply a tactic to the nth element of the signature *)
87
let tclNTH_HYP m (tac : constr->tactic) gl =
88
tac (try mkVar(let (id,_,_) = List.nth (pf_hyps gl) (m-1) in id)
89
with Failure _ -> error "No such assumption.") gl
91
let tclNTH_DECL m tac gl =
92
tac (try List.nth (pf_hyps gl) (m-1)
93
with Failure _ -> error "No such assumption.") gl
95
(* apply a tactic to the last element of the signature *)
97
let tclLAST_HYP = tclNTH_HYP 1
99
let tclLAST_DECL = tclNTH_DECL 1
101
let tclLAST_NHYPS n tac gl =
102
tac (try list_firstn n (pf_ids_of_hyps gl)
103
with Failure _ -> error "No such assumptions.") gl
105
let tclTRY_sign (tac : constr->tactic) sign gl =
106
let rec arec = function
107
| [] -> tclFAIL 0 (str "No applicable hypothesis.")
108
| [s] -> tac (mkVar s) (*added in order to get useful error messages *)
109
| (s::sl) -> tclORELSE (tac (mkVar s)) (arec sl)
111
arec (ids_of_named_context sign) gl
113
let tclTRY_HYPS (tac : constr->tactic) gl =
114
tclTRY_sign tac (pf_hyps gl) gl
116
(***************************************)
117
(* Clause Tacticals *)
118
(***************************************)
120
(* The following functions introduce several tactic combinators and
121
functions useful for working with clauses. A clause is either None
122
or (Some id), where id is an identifier. This type is useful for
123
defining tactics that may be used either to transform the
124
conclusion (None) or to transform a hypothesis id (Some id). --
128
(* The type of clauses *)
130
type simple_clause = identifier gsimple_clause
131
type clause = identifier gclause
133
let allClauses = { onhyps=None; concl_occs=all_occurrences_expr }
134
let allHyps = { onhyps=None; concl_occs=no_occurrences_expr }
135
let onConcl = { onhyps=Some[]; concl_occs=all_occurrences_expr }
137
{ onhyps=Some[((all_occurrences_expr,id),InHyp)]; concl_occs=no_occurrences_expr }
139
let simple_clause_list_of cl gls =
143
let f id = Some((all_occurrences_expr,id),InHyp) in
144
List.map f (pf_ids_of_hyps gls)
146
List.map (fun h -> Some h) l in
147
if cl.concl_occs = all_occurrences_expr then None::hyps else hyps
151
let tryClauses tac cl gls =
152
let rec firstrec = function
153
| [] -> tclFAIL 0 (str "no applicable hypothesis")
154
| [cls] -> tac cls (* added in order to get a useful error message *)
155
| cls::tl -> (tclORELSE (tac cls) (firstrec tl))
157
let hyps = simple_clause_list_of cl gls in
161
let onClauses tac cl gls =
162
let hyps = simple_clause_list_of cl gls in
165
(* AND-branch reverse order*)
166
let onClausesLR tac cl gls =
167
let hyps = simple_clause_list_of cl gls in
168
tclMAP tac (List.rev hyps) gls
170
(* A clause corresponding to the |n|-th hypothesis or None *)
172
let nth_clause n gl =
176
let id = List.nth (List.rev (pf_ids_of_hyps gl)) (-n-1) in
179
let id = List.nth (pf_ids_of_hyps gl) (n-1) in
182
(* Gets the conclusion or the type of a given hypothesis *)
184
let clause_type cls gl =
185
match simple_clause_of cls with
186
| None -> pf_concl gl
187
| Some ((_,id),_) -> pf_get_hyp_typ gl id
189
(* Functions concerning matching of clausal environments *)
191
let pf_is_matching gls pat n =
192
is_matching_conv (pf_env gls) (project gls) pat n
194
let pf_matches gls pat n =
195
matches_conv (pf_env gls) (project gls) pat n
197
(* [OnCL clausefinder clausetac]
198
* executes the clausefinder to find the clauses, and then executes the
199
* clausetac on the clause so obtained. *)
201
let onCL cfind cltac gl = cltac (cfind gl) gl
204
(* [OnHyps hypsfinder hypstac]
205
* idem [OnCL] but only for hypotheses, not for conclusion *)
207
let onHyps find tac gl = tac (find gl) gl
211
(* Create a clause list with all the hypotheses from the context, occuring
215
fst (list_split_at (fun (hyp,_,_) -> hyp = id) (pf_hyps gl))
218
(* Create a singleton clause list with the last hypothesis from then context *)
220
let lastHyp gl = List.hd (pf_ids_of_hyps gl)
223
(* Create a clause list with the n last hypothesis from then context *)
226
try list_firstn n (pf_hyps gl)
227
with Failure "firstn" -> error "Not enough hypotheses in the goal."
230
let onClause t cls gl = t cls gl
231
let tryAllClauses tac = tryClauses tac allClauses
232
let onAllClauses tac = onClauses tac allClauses
233
let onAllClausesLR tac = onClausesLR tac allClauses
234
let onNthLastHyp n tac gls = tac (nth_clause n gls) gls
237
tryClauses (function Some((_,id),_) -> tac id | _ -> assert false) allHyps
238
let onNLastHyps n tac = onHyps (nLastHyps n) (tclMAP tac)
239
let onLastHyp tac gls = tac (lastHyp gls) gls
241
let clauseTacThen tac continuation =
242
(fun cls -> (tclTHEN (tac cls) continuation))
244
let if_tac pred tac1 tac2 gl =
245
if pred gl then tac1 gl else tac2 gl
247
let ifOnClause pred tac1 tac2 cls gl =
248
if pred (cls,clause_type cls gl) then
253
let ifOnHyp pred tac1 tac2 id gl =
254
if pred (id,pf_get_hyp_typ gl id) then
259
(***************************************)
260
(* Elimination Tacticals *)
261
(***************************************)
263
(* The following tacticals allow to apply a tactic to the
264
branches generated by the application of an elimination
267
Two auxiliary types --branch_args and branch_assumptions-- are
268
used to keep track of some information about the ``branches'' of
272
ity : inductive; (* the type we were eliminating on *)
273
largs : constr list; (* its arguments *)
274
branchnum : int; (* the branch number *)
275
pred : constr; (* the predicate we used *)
276
nassums : int; (* the number of assumptions to be introduced *)
277
branchsign : bool list; (* the signature of the branch.
278
true=recursive argument, false=constant *)
279
branchnames : intro_pattern_expr located list}
281
type branch_assumptions = {
282
ba : branch_args; (* the branch args *)
283
assums : named_context} (* the list of assumptions introduced *)
285
let fix_empty_or_and_pattern nv l =
286
(* 1- The syntax does not distinguish between "[ ]" for one clause with no
287
names and "[ ]" for no clause at all *)
288
(* 2- More generally, we admit "[ ]" for any disjunctive pattern of
290
if l = [[]] then list_make nv [] else l
292
let check_or_and_pattern_size loc names n =
293
if List.length names <> n then
295
user_err_loc (loc,"",str "Expects a conjunctive pattern.")
297
user_err_loc (loc,"",str "Expects a disjunctive pattern with " ++ int n
300
let compute_induction_names n = function
303
| Some (loc,IntroOrAndPattern names) ->
304
let names = fix_empty_or_and_pattern n names in
305
check_or_and_pattern_size loc names n;
308
user_err_loc (loc,"",str "Disjunctive/conjunctive introduction pattern expected.")
310
let compute_construtor_signatures isrec (_,k as ity) =
311
let rec analrec c recargs =
312
match kind_of_term c, recargs with
313
| Prod (_,_,c), recarg::rest ->
314
let b = match dest_recarg recarg with
315
| Norec | Imbr _ -> false
316
| Mrec j -> isrec & j=k
317
in b :: (analrec c rest)
318
| LetIn (_,_,_,c), rest -> false :: (analrec c rest)
320
| _ -> anomaly "compute_construtor_signatures"
322
let (mib,mip) = Global.lookup_inductive ity in
323
let n = mib.mind_nparams in
325
Array.map (fun c -> snd (decompose_prod_n_assum n c)) mip.mind_nf_lc in
326
let lrecargs = dest_subterms mip.mind_recargs in
327
array_map2 analrec lc lrecargs
329
let elimination_sort_of_goal gl =
330
pf_apply Retyping.get_sort_family_of gl (pf_concl gl)
332
let elimination_sort_of_hyp id gl =
333
pf_apply Retyping.get_sort_family_of gl (pf_get_hyp_typ gl id)
335
let elimination_sort_of_clause = function
336
| None -> elimination_sort_of_goal
337
| Some id -> elimination_sort_of_hyp id
339
(* Find the right elimination suffix corresponding to the sort of the goal *)
340
(* c should be of type A1->.. An->B with B an inductive definition *)
342
let general_elim_then_using mk_elim
343
isrec allnames tac predicate (indbindings,elimbindings)
345
let elim = mk_elim ind gl in
346
(* applying elimination_scheme just a little modified *)
347
let indclause' = clenv_match_args indbindings indclause in
348
let elimclause = mk_clenv_from gl (elim,pf_type_of gl elim) in
350
match kind_of_term (last_arg elimclause.templval.Evd.rebus) with
352
| _ -> anomaly "elimination"
355
let p, _ = decompose_app elimclause.templtyp.Evd.rebus in
356
match kind_of_term p with
360
match kind_of_term elim with
361
| Const kn -> string_of_con kn
362
| Var id -> string_of_id id
365
error ("The elimination combinator " ^ name_elim ^ " is unknown.")
367
let elimclause' = clenv_fchain indmv elimclause indclause' in
368
let elimclause' = clenv_match_args elimbindings elimclause' in
369
let branchsigns = compute_construtor_signatures isrec ind in
370
let brnames = compute_induction_names (Array.length branchsigns) allnames in
371
let after_tac ce i gl =
372
let (hd,largs) = decompose_app ce.templtyp.Evd.rebus in
373
let ba = { branchsign = branchsigns.(i);
374
branchnames = brnames.(i);
377
(fun acc b -> if b then acc+2 else acc+1)
381
largs = List.map (clenv_nf_meta ce) largs;
382
pred = clenv_nf_meta ce hd }
386
let branchtacs ce = Array.init (Array.length branchsigns) (after_tac ce) in
389
| None -> elimclause'
391
clenv_unify true Reduction.CONV (mkMeta pmv) p elimclause'
393
elim_res_pf_THEN_i elimclause' branchtacs gl
395
(* computing the case/elim combinators *)
397
let gl_make_elim ind gl =
398
Indrec.lookup_eliminator ind (elimination_sort_of_goal gl)
400
let gl_make_case_dep ind gl =
401
pf_apply Indrec.make_case_dep gl ind (elimination_sort_of_goal gl)
403
let gl_make_case_nodep ind gl =
404
pf_apply Indrec.make_case_nodep gl ind (elimination_sort_of_goal gl)
406
let elimination_then_using tac predicate bindings c gl =
407
let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
408
let indclause = mk_clenv_from gl (c,t) in
409
general_elim_then_using gl_make_elim
410
true None tac predicate bindings ind indclause gl
412
let case_then_using =
413
general_elim_then_using gl_make_case_dep false
415
let case_nodep_then_using =
416
general_elim_then_using gl_make_case_nodep false
418
let elimination_then tac = elimination_then_using tac None
419
let simple_elimination_then tac = elimination_then tac ([],[])
422
let make_elim_branch_assumptions ba gl =
423
let rec makerec (assums,cargs,constargs,recargs,indargs) lb lc =
428
| ((true::tl), ((idrec,_,_ as recarg)::(idind,_,_ as indarg)::idtl)) ->
429
makerec (recarg::indarg::assums,
433
idind::indargs) tl idtl
434
| ((false::tl), ((id,_,_ as constarg)::idtl)) ->
435
makerec (constarg::assums,
440
| (_, _) -> anomaly "make_elim_branch_assumptions"
442
makerec ([],[],[],[],[]) ba.branchsign
443
(try list_firstn ba.nassums (pf_hyps gl)
444
with Failure _ -> anomaly "make_elim_branch_assumptions")
446
let elim_on_ba tac ba gl = tac (make_elim_branch_assumptions ba gl) gl
448
let make_case_branch_assumptions ba gl =
449
let rec makerec (assums,cargs,constargs,recargs) p_0 p_1 =
454
| ((true::tl), ((idrec,_,_ as recarg)::idtl)) ->
455
makerec (recarg::assums,
459
| ((false::tl), ((id,_,_ as constarg)::idtl)) ->
460
makerec (constarg::assums,
463
id::constargs) tl idtl
464
| (_, _) -> anomaly "make_case_branch_assumptions"
466
makerec ([],[],[],[]) ba.branchsign
467
(try list_firstn ba.nassums (pf_hyps gl)
468
with Failure _ -> anomaly "make_case_branch_assumptions")
470
let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl
added
removed
tactics/tacticals.ml
