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 camlp4deps: "parsing/grammar.cma" i*)
11
(* $Id: eauto.ml4 11735 2009-01-02 17:22:31Z herbelin $ *)
34
let e_give_exact ?(flags=Unification.default_unify_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in
35
if occur_existential t1 or occur_existential t2 then
36
tclTHEN (Clenvtac.unify ~flags t1) (exact_check c) gl
39
let assumption id = e_give_exact (mkVar id)
42
tclFIRST (List.map assumption (pf_ids_of_hyps gl)) gl
44
TACTIC EXTEND eassumption
45
| [ "eassumption" ] -> [ e_assumption ]
49
| [ "eexact" constr(c) ] -> [ e_give_exact c ]
52
let e_give_exact_constr = h_eexact
54
let registered_e_assumption gl =
55
tclFIRST (List.map (fun id gl -> e_give_exact_constr (mkVar id) gl)
56
(pf_ids_of_hyps gl)) gl
58
(************************************************************************)
60
(************************************************************************)
64
@ (List.map h_simplest_eapply (List.map mkVar (pf_ids_of_hyps gl)))
65
@ (List.map h_simplest_eapply l)
66
@ (List.map assumption (pf_ids_of_hyps gl))
68
let rec prolog l n gl =
69
if n <= 0 then error "prolog - failure";
70
let prol = (prolog l (n-1)) in
71
(tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl
73
let prolog_tac l n gl =
77
| _ -> error "Prolog called with a non closed argument."
80
with UserError ("Refiner.tclFIRST",_) ->
81
errorlabstrm "Prolog.prolog" (str "Prolog failed.")
84
| [ "prolog" "[" constr_list(l) "]" int_or_var(n) ] -> [ prolog_tac l n ]
90
(***************************************************************************)
91
(* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
92
(***************************************************************************)
94
let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l)
98
let unify_e_resolve flags (c,clenv) gls =
99
let clenv' = connect_clenv gls clenv in
100
let _ = clenv_unique_resolver false ~flags clenv' gls in
101
h_simplest_eapply c gls
103
let unify_e_resolve_nodelta (c,clenv) gls =
104
let clenv' = connect_clenv gls clenv in
105
let _ = clenv_unique_resolver false clenv' gls in
106
h_simplest_eapply c gls
108
let rec e_trivial_fail_db mod_delta db_list local_db goal =
110
registered_e_assumption ::
111
(tclTHEN Tactics.intro
113
let d = pf_last_hyp g' in
114
let hintl = make_resolve_hyp (pf_env g') (project g') d in
115
(e_trivial_fail_db mod_delta db_list
116
(Hint_db.add_list hintl local_db) g'))) ::
117
(List.map fst (e_trivial_resolve mod_delta db_list local_db (pf_concl goal)) )
119
tclFIRST (List.map tclCOMPLETE tacl) goal
121
and e_my_find_search mod_delta =
122
if mod_delta then e_my_find_search_delta
123
else e_my_find_search_nodelta
125
and e_my_find_search_nodelta db_list local_db hdc concl =
126
let hdc = head_of_constr_reference hdc in
128
if occur_existential concl then
129
list_map_append (Hint_db.map_all hdc) (local_db::db_list)
131
list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list)
134
fun {pri=b; pat = p; code=t} ->
138
| Res_pf (term,cl) -> unify_resolve_nodelta (term,cl)
139
| ERes_pf (term,cl) -> unify_e_resolve_nodelta (term,cl)
140
| Give_exact (c) -> e_give_exact_constr c
141
| Res_pf_THEN_trivial_fail (term,cl) ->
142
tclTHEN (unify_e_resolve_nodelta (term,cl))
143
(e_trivial_fail_db false db_list local_db)
144
| Unfold_nth c -> unfold_in_concl [all_occurrences,c]
145
| Extern tacast -> conclPattern concl p tacast
147
(tac,pr_autotactic t))
149
fun gls -> pPNL (pr_autotactic t); Format.print_flush ();
151
with e when Logic.catchable_exception(e) ->
152
(Format.print_string "Fail\n";
153
Format.print_flush ();
157
List.map tac_of_hint hintl
159
and e_my_find_search_delta db_list local_db hdc concl =
160
let hdc = head_of_constr_reference hdc in
162
if occur_existential concl then
163
list_map_append (fun db ->
164
let flags = {auto_unif_flags with modulo_delta = Hint_db.transparent_state db} in
165
List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
167
list_map_append (fun db ->
168
let flags = {auto_unif_flags with modulo_delta = Hint_db.transparent_state db} in
169
List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
172
fun (st, {pri=b; pat = p; code=t}) ->
176
| Res_pf (term,cl) -> unify_resolve st (term,cl)
177
| ERes_pf (term,cl) -> unify_e_resolve st (term,cl)
178
| Give_exact (c) -> e_give_exact ~flags:st c
179
| Res_pf_THEN_trivial_fail (term,cl) ->
180
tclTHEN (unify_e_resolve st (term,cl))
181
(e_trivial_fail_db true db_list local_db)
182
| Unfold_nth c -> unfold_in_concl [all_occurrences,c]
183
| Extern tacast -> conclPattern concl p tacast
185
(tac,pr_autotactic t))
187
fun gls -> pPNL (pr_autotactic t); Format.print_flush ();
189
with e when Logic.catchable_exception(e) ->
190
(Format.print_string "Fail\n";
191
Format.print_flush ();
195
List.map tac_of_hint hintl
197
and e_trivial_resolve mod_delta db_list local_db gl =
200
(e_my_find_search mod_delta db_list local_db
201
(fst (head_constr_bound gl)) gl)
202
with Bound | Not_found -> []
204
let e_possible_resolve mod_delta db_list local_db gl =
206
(e_my_find_search mod_delta db_list local_db
207
(fst (head_constr_bound gl)) gl)
208
with Bound | Not_found -> []
210
let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id))
212
let find_first_goal gls =
213
try first_goal gls with UserError _ -> assert false
215
(*s The following module [SearchProblem] is used to instantiate the generic
216
exploration functor [Explore.Make]. *)
218
type search_state = {
219
depth : int; (*r depth of search before failing *)
220
tacres : goal list sigma * validation;
221
last_tactic : std_ppcmds;
222
dblist : Auto.hint_db list;
223
localdb : Auto.hint_db list }
225
module SearchProblem = struct
227
type state = search_state
229
let success s = (sig_it (fst s.tacres)) = []
231
let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl)
234
let evars = Evarutil.nf_evars (Refiner.project gls) in
235
prlist (pr_ev evars) (sig_it gls)
237
let filter_tactics (glls,v) l =
238
(* let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
239
(* let evars = Evarutil.nf_evars (Refiner.project glls) in *)
240
(* msg (str"Goal:" ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *)
241
let rec aux = function
243
| (tac,pptac) :: tacl ->
245
let (lgls,ptl) = apply_tac_list tac glls in
246
let v' p = v (ptl p) in
247
(* let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
248
(* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *)
249
((lgls,v'),pptac) :: aux tacl
250
with e -> Refiner.catch_failerror e; aux tacl
253
(* Ordering of states is lexicographic on depth (greatest first) then
254
number of remaining goals. *)
256
let d = s'.depth - s.depth in
257
let nbgoals s = List.length (sig_it (fst s.tacres)) in
258
if d <> 0 then d else nbgoals s - nbgoals s'
264
let lg = fst s.tacres in
265
let nbgl = List.length (sig_it lg) in
267
let g = find_first_goal lg in
268
let assumption_tacs =
270
filter_tactics s.tacres
272
(fun id -> (e_give_exact_constr (mkVar id),
273
(str "exact" ++ spc () ++ pr_id id)))
276
List.map (fun (res,pp) -> { depth = s.depth; tacres = res;
277
last_tactic = pp; dblist = s.dblist;
278
localdb = List.tl s.localdb }) l
282
(fun ((lgls,_) as res,pp) ->
283
let g' = first_goal lgls in
285
make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
287
let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
288
{ depth = s.depth; tacres = res;
289
last_tactic = pp; dblist = s.dblist;
290
localdb = ldb :: List.tl s.localdb })
291
(filter_tactics s.tacres [Tactics.intro,(str "intro")])
295
filter_tactics s.tacres (e_possible_resolve false s.dblist (List.hd s.localdb) (pf_concl g))
298
(fun ((lgls,_) as res, pp) ->
299
let nbgl' = List.length (sig_it lgls) in
301
{ depth = s.depth; tacres = res; last_tactic = pp;
302
dblist = s.dblist; localdb = List.tl s.localdb }
304
{ depth = pred s.depth; tacres = res;
305
dblist = s.dblist; last_tactic = pp;
307
list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb })
310
List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
313
msg (hov 0 (str " depth=" ++ int s.depth ++ spc () ++
314
s.last_tactic ++ str "\n"))
318
module Search = Explore.Make(SearchProblem)
320
let make_initial_state n gl dblist localdb =
322
tacres = tclIDTAC gl;
323
last_tactic = (mt ());
325
localdb = [localdb] }
327
let debug_depth_first = Search.debug_depth_first
329
let e_depth_search debug p db_list local_db gl =
331
let tac = if debug then Search.debug_depth_first else Search.depth_first in
332
let s = tac (make_initial_state p gl db_list local_db) in
334
with Not_found -> error "eauto: depth first search failed."
336
let e_breadth_search debug n db_list local_db gl =
339
if debug then Search.debug_breadth_first else Search.breadth_first
341
let s = tac (make_initial_state n gl db_list local_db) in
343
with Not_found -> error "eauto: breadth first search failed."
345
let e_search_auto debug (in_depth,p) lems db_list gl =
346
let local_db = make_local_hint_db true lems gl in
348
e_depth_search debug p db_list local_db gl
350
e_breadth_search debug p db_list local_db gl
354
let eauto_with_bases debug np lems db_list =
355
tclTRY (e_search_auto debug np lems db_list)
357
let eauto debug np lems dbnames =
361
try searchtable_map x
362
with Not_found -> error ("No such Hint database: "^x^"."))
365
tclTRY (e_search_auto debug np lems db_list)
367
let full_eauto debug n lems gl =
368
let dbnames = current_db_names () in
369
let dbnames = list_subtract dbnames ["v62"] in
370
let db_list = List.map searchtable_map dbnames in
371
tclTRY (e_search_auto debug n lems db_list) gl
373
let gen_eauto d np lems = function
374
| None -> full_eauto d np lems
375
| Some l -> eauto d np lems l
377
let make_depth = function
378
| None -> !default_search_depth
379
| Some (ArgArg d) -> d
380
| _ -> error "eauto called with a non closed argument."
382
let make_dimension n = function
383
| None -> (true,make_depth n)
384
| Some (ArgArg d) -> (false,d)
385
| _ -> error "eauto called with a non closed argument."
391
let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases
393
ARGUMENT EXTEND hintbases
394
TYPED AS preident_list_opt
395
PRINTED BY pr_hintbases
396
| [ "with" "*" ] -> [ None ]
397
| [ "with" ne_preident_list(l) ] -> [ Some l ]
401
let pr_constr_coma_sequence prc _ _ = prlist_with_sep pr_coma prc
403
ARGUMENT EXTEND constr_coma_sequence
405
PRINTED BY pr_constr_coma_sequence
406
| [ constr(c) "," constr_coma_sequence(l) ] -> [ c::l ]
407
| [ constr(c) ] -> [ [c] ]
410
let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc
412
ARGUMENT EXTEND auto_using
414
PRINTED BY pr_auto_using
415
| [ "using" constr_coma_sequence(l) ] -> [ l ]
420
| [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
422
[ gen_eauto false (make_dimension n p) lems db ]
425
TACTIC EXTEND new_eauto
426
| [ "new" "auto" int_or_var_opt(n) auto_using(lems)
429
| None -> new_full_auto (make_depth n) lems
431
new_auto (make_depth n) lems l ]
434
TACTIC EXTEND debug_eauto
435
| [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
437
[ gen_eauto true (make_dimension n p) lems db ]
440
TACTIC EXTEND dfs_eauto
441
| [ "dfs" "eauto" int_or_var_opt(p) auto_using(lems)
443
[ gen_eauto false (true, make_depth p) lems db ]
446
let autosimpl db cl =
447
let unfold_of_elts constr (b, elts) =
449
List.map (fun c -> all_occurrences, constr c) elts
452
let unfolds = List.concat (List.map (fun dbname ->
453
let db = searchtable_map dbname in
454
let (ids, csts) = Hint_db.transparent_state db in
455
unfold_of_elts (fun x -> EvalConstRef x) (Cpred.elements csts) @
456
unfold_of_elts (fun x -> EvalVarRef x) (Idpred.elements ids)) db)
457
in unfold_option unfolds cl
459
TACTIC EXTEND autosimpl
460
| [ "autosimpl" hintbases(db) ] ->
461
[ autosimpl (match db with None -> ["core"] | Some x -> "core"::x) None ]
465
| ["unify" constr(x) constr(y) ] -> [ unify x y ]
466
| ["unify" constr(x) constr(y) "with" preident(base) ] -> [
467
unify ~state:(Hint_db.transparent_state (searchtable_map base)) x y ]
added
removed
tactics/eauto.ml4
