summaryrefslogtreecommitdiff
path: root/tactics/eauto.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/eauto.ml4')
-rw-r--r--tactics/eauto.ml4270
1 files changed, 183 insertions, 87 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index e0cdbcfa..6981a733 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,8 +8,6 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: eauto.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Pp
open Util
open Names
@@ -19,7 +17,6 @@ open Termops
open Sign
open Reduction
open Proof_type
-open Proof_trees
open Declarations
open Tacticals
open Tacmach
@@ -28,8 +25,9 @@ open Tactics
open Pattern
open Clenv
open Auto
-open Rawterm
+open Glob_term
open Hiddentac
+open Tacexpr
let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_transparent_state }
@@ -71,6 +69,7 @@ let rec prolog l n gl =
(tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl
let prolog_tac l n gl =
+ let l = List.map (prepare_hint (pf_env gl)) l in
let n =
match n with
| ArgArg n -> n
@@ -81,7 +80,7 @@ let prolog_tac l n gl =
errorlabstrm "Prolog.prolog" (str "Prolog failed.")
TACTIC EXTEND prolog
-| [ "prolog" "[" constr_list(l) "]" int_or_var(n) ] -> [ prolog_tac l n ]
+| [ "prolog" "[" open_constr_list(l) "]" int_or_var(n) ] -> [ prolog_tac l n ]
END
open Auto
@@ -95,7 +94,7 @@ let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l)
let unify_e_resolve flags (c,clenv) gls =
let clenv' = connect_clenv gls clenv in
- let _ = clenv_unique_resolver false ~flags clenv' gls in
+ let _ = clenv_unique_resolver ~flags clenv' gls in
h_simplest_eapply c gls
let rec e_trivial_fail_db db_list local_db goal =
@@ -170,24 +169,31 @@ let find_first_goal gls =
type search_state = {
depth : int; (*r depth of search before failing *)
- tacres : goal list sigma * validation;
+ tacres : goal list sigma;
last_tactic : std_ppcmds Lazy.t;
dblist : Auto.hint_db list;
- localdb : Auto.hint_db list }
+ localdb : Auto.hint_db list;
+ prev : prev_search_state
+}
+
+and prev_search_state = (* for info eauto *)
+ | Unknown
+ | Init
+ | State of search_state
module SearchProblem = struct
type state = search_state
- let success s = (sig_it (fst s.tacres)) = []
+ let success s = (sig_it s.tacres) = []
let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl)
let pr_goals gls =
- let evars = Evarutil.nf_evars (Refiner.project gls) in
+ let evars = Evarutil.nf_evar_map (Refiner.project gls) in
prlist (pr_ev evars) (sig_it gls)
- let filter_tactics (glls,v) l =
+ let filter_tactics glls l =
(* let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
(* let evars = Evarutil.nf_evars (Refiner.project glls) in *)
(* msg (str"Goal:" ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *)
@@ -195,26 +201,27 @@ module SearchProblem = struct
| [] -> []
| (tac,pptac) :: tacl ->
try
- let (lgls,ptl) = apply_tac_list tac glls in
- let v' p = v (ptl p) in
+ let lgls = apply_tac_list tac glls in
(* let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
(* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *)
- ((lgls,v'),pptac) :: aux tacl
- with e -> Refiner.catch_failerror e; aux tacl
+ (lgls,pptac) :: aux tacl
+ with e when Errors.noncritical e ->
+ Refiner.catch_failerror e; aux tacl
in aux l
(* Ordering of states is lexicographic on depth (greatest first) then
number of remaining goals. *)
let compare s s' =
let d = s'.depth - s.depth in
- let nbgoals s = List.length (sig_it (fst s.tacres)) in
+ let nbgoals s = List.length (sig_it s.tacres) in
if d <> 0 then d else nbgoals s - nbgoals s'
let branching s =
if s.depth = 0 then
[]
else
- let lg = fst s.tacres in
+ let ps = if s.prev = Unknown then Unknown else State s in
+ let lg = s.tacres in
let nbgl = List.length (sig_it lg) in
assert (nbgl > 0);
let g = find_first_goal lg in
@@ -228,11 +235,12 @@ module SearchProblem = struct
in
List.map (fun (res,pp) -> { depth = s.depth; tacres = res;
last_tactic = pp; dblist = s.dblist;
- localdb = List.tl s.localdb }) l
+ localdb = List.tl s.localdb;
+ prev = ps}) l
in
let intro_tac =
List.map
- (fun ((lgls,_) as res,pp) ->
+ (fun (lgls as res,pp) ->
let g' = first_goal lgls in
let hintl =
make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
@@ -240,7 +248,7 @@ module SearchProblem = struct
let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
{ depth = s.depth; tacres = res;
last_tactic = pp; dblist = s.dblist;
- localdb = ldb :: List.tl s.localdb })
+ localdb = ldb :: List.tl s.localdb; prev = ps })
(filter_tactics s.tacres [Tactics.intro,lazy (str "intro")])
in
let rec_tacs =
@@ -248,82 +256,125 @@ module SearchProblem = struct
filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g))
in
List.map
- (fun ((lgls,_) as res, pp) ->
+ (fun (lgls as res, pp) ->
let nbgl' = List.length (sig_it lgls) in
if nbgl' < nbgl then
- { depth = s.depth; tacres = res; last_tactic = pp;
+ { depth = s.depth; tacres = res; last_tactic = pp; prev = ps;
dblist = s.dblist; localdb = List.tl s.localdb }
else
{ depth = pred s.depth; tacres = res;
- dblist = s.dblist; last_tactic = pp;
+ dblist = s.dblist; last_tactic = pp; prev = ps;
localdb =
list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb })
l
in
List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
- let pp s =
- msg (hov 0 (str " depth=" ++ int s.depth ++ spc () ++
- (Lazy.force s.last_tactic) ++ str "\n"))
+ let pp s = hov 0 (str " depth=" ++ int s.depth ++ spc () ++
+ (Lazy.force s.last_tactic))
end
module Search = Explore.Make(SearchProblem)
-let make_initial_state n gl dblist localdb =
+(** Utilities for debug eauto / info eauto *)
+
+let global_debug_eauto = ref false
+let global_info_eauto = ref false
+
+let _ =
+ Goptions.declare_bool_option
+ { Goptions.optsync = true;
+ Goptions.optdepr = false;
+ Goptions.optname = "Debug Eauto";
+ Goptions.optkey = ["Debug";"Eauto"];
+ Goptions.optread = (fun () -> !global_debug_eauto);
+ Goptions.optwrite = (:=) global_debug_eauto }
+
+let _ =
+ Goptions.declare_bool_option
+ { Goptions.optsync = true;
+ Goptions.optdepr = false;
+ Goptions.optname = "Info Eauto";
+ Goptions.optkey = ["Info";"Eauto"];
+ Goptions.optread = (fun () -> !global_info_eauto);
+ Goptions.optwrite = (:=) global_info_eauto }
+
+let mk_eauto_dbg d =
+ if d = Debug || !global_debug_eauto then Debug
+ else if d = Info || !global_info_eauto then Info
+ else Off
+
+let pr_info_nop = function
+ | Info -> msg_debug (str "idtac.")
+ | _ -> ()
+
+let pr_dbg_header = function
+ | Off -> ()
+ | Debug -> msg_debug (str "(* debug eauto : *)")
+ | Info -> msg_debug (str "(* info eauto : *)")
+
+let pr_info dbg s =
+ if dbg <> Info then ()
+ else
+ let rec loop s =
+ match s.prev with
+ | Unknown | Init -> s.depth
+ | State sp ->
+ let mindepth = loop sp in
+ let indent = String.make (mindepth - sp.depth) ' ' in
+ msg_debug (str indent ++ Lazy.force s.last_tactic ++ str ".");
+ mindepth
+ in
+ ignore (loop s)
+
+(** Eauto main code *)
+
+let make_initial_state dbg n gl dblist localdb =
{ depth = n;
tacres = tclIDTAC gl;
last_tactic = lazy (mt());
dblist = dblist;
- localdb = [localdb] }
+ localdb = [localdb];
+ prev = if dbg=Info then Init else Unknown;
+ }
-let e_depth_search debug p db_list local_db gl =
- try
- let tac = if debug then Search.debug_depth_first else Search.depth_first in
- let s = tac (make_initial_state p gl db_list local_db) in
- s.tacres
- with Not_found -> error "eauto: depth first search failed."
-
-let e_breadth_search debug n db_list local_db gl =
+let e_search_auto debug (in_depth,p) lems db_list gl =
+ let local_db = make_local_hint_db ~ts:full_transparent_state true lems gl in
+ let d = mk_eauto_dbg debug in
+ let tac = match in_depth,d with
+ | (true,Debug) -> Search.debug_depth_first
+ | (true,_) -> Search.depth_first
+ | (false,Debug) -> Search.debug_breadth_first
+ | (false,_) -> Search.breadth_first
+ in
try
- let tac =
- if debug then Search.debug_breadth_first else Search.breadth_first
- in
- let s = tac (make_initial_state n gl db_list local_db) in
+ pr_dbg_header d;
+ let s = tac (make_initial_state d p gl db_list local_db) in
+ pr_info d s;
s.tacres
- with Not_found -> error "eauto: breadth first search failed."
-
-let e_search_auto debug (in_depth,p) lems db_list gl =
- let local_db = make_local_hint_db true lems gl in
- if in_depth then
- e_depth_search debug p db_list local_db gl
- else
- e_breadth_search debug p db_list local_db gl
+ with Not_found ->
+ pr_info_nop d;
+ error "eauto: search failed"
open Evd
-let eauto_with_bases debug np lems db_list =
+let eauto_with_bases ?(debug=Off) np lems db_list =
tclTRY (e_search_auto debug np lems db_list)
-let eauto debug np lems dbnames =
- let db_list =
- List.map
- (fun x ->
- try searchtable_map x
- with Not_found -> error ("No such Hint database: "^x^"."))
- ("core"::dbnames)
- in
+let eauto ?(debug=Off) np lems dbnames =
+ let db_list = make_db_list dbnames in
tclTRY (e_search_auto debug np lems db_list)
-let full_eauto debug n lems gl =
+let full_eauto ?(debug=Off) n lems gl =
let dbnames = current_db_names () in
- let dbnames = list_subtract dbnames ["v62"] in
+ let dbnames = list_remove "v62" dbnames in
let db_list = List.map searchtable_map dbnames in
tclTRY (e_search_auto debug n lems db_list) gl
-let gen_eauto d np lems = function
- | None -> full_eauto d np lems
- | Some l -> eauto d np lems l
+let gen_eauto ?(debug=Off) np lems = function
+ | None -> full_eauto ~debug np lems
+ | Some l -> eauto ~debug np lems l
let make_depth = function
| None -> !default_search_depth
@@ -349,19 +400,20 @@ ARGUMENT EXTEND hintbases
| [ ] -> [ Some [] ]
END
-let pr_constr_coma_sequence prc _ _ = prlist_with_sep pr_comma prc
+let pr_constr_coma_sequence prc _ _ =
+ prlist_with_sep pr_comma (fun (_,c) -> prc c)
ARGUMENT EXTEND constr_coma_sequence
- TYPED AS constr_list
+ TYPED AS open_constr_list
PRINTED BY pr_constr_coma_sequence
-| [ constr(c) "," constr_coma_sequence(l) ] -> [ c::l ]
-| [ constr(c) ] -> [ [c] ]
+| [ open_constr(c) "," constr_coma_sequence(l) ] -> [ c::l ]
+| [ open_constr(c) ] -> [ [c] ]
END
-let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc
+let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using (fun (_,c) -> prc c)
ARGUMENT EXTEND auto_using
- TYPED AS constr_list
+ TYPED AS open_constr_list
PRINTED BY pr_auto_using
| [ "using" constr_coma_sequence(l) ] -> [ l ]
| [ ] -> [ [] ]
@@ -370,7 +422,7 @@ END
TACTIC EXTEND eauto
| [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
hintbases(db) ] ->
- [ gen_eauto false (make_dimension n p) lems db ]
+ [ gen_eauto (make_dimension n p) lems db ]
END
TACTIC EXTEND new_eauto
@@ -378,20 +430,25 @@ TACTIC EXTEND new_eauto
hintbases(db) ] ->
[ match db with
| None -> new_full_auto (make_depth n) lems
- | Some l ->
- new_auto (make_depth n) lems l ]
+ | Some l -> new_auto (make_depth n) lems l ]
END
TACTIC EXTEND debug_eauto
| [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
hintbases(db) ] ->
- [ gen_eauto true (make_dimension n p) lems db ]
+ [ gen_eauto ~debug:Debug (make_dimension n p) lems db ]
+END
+
+TACTIC EXTEND info_eauto
+| [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
+ hintbases(db) ] ->
+ [ gen_eauto ~debug:Info (make_dimension n p) lems db ]
END
TACTIC EXTEND dfs_eauto
| [ "dfs" "eauto" int_or_var_opt(p) auto_using(lems)
hintbases(db) ] ->
- [ gen_eauto false (true, make_depth p) lems db ]
+ [ gen_eauto (true, make_depth p) lems db ]
END
let cons a l = a :: l
@@ -414,19 +471,6 @@ let autounfold db cls gl =
| OnConcl occs -> tac occs None)
cls gl
-let autosimpl db cl =
- let unfold_of_elts constr (b, elts) =
- if not b then
- List.map (fun c -> all_occurrences, constr c) elts
- else []
- in
- let unfolds = List.concat (List.map (fun dbname ->
- let db = searchtable_map dbname in
- let (ids, csts) = Hint_db.transparent_state db in
- unfold_of_elts (fun x -> EvalConstRef x) (Cpred.elements csts) @
- unfold_of_elts (fun x -> EvalVarRef x) (Idpred.elements ids)) db)
- in unfold_option unfolds cl
-
open Extraargs
TACTIC EXTEND autounfold
@@ -520,3 +564,55 @@ END
TACTIC EXTEND convert_concl_no_check
| ["convert_concl_no_check" constr(x) ] -> [ convert_concl_no_check x DEFAULTcast ]
END
+
+
+let pr_hints_path_atom prc _ _ a =
+ match a with
+ | PathAny -> str"."
+ | PathHints grs ->
+ prlist_with_sep pr_spc Printer.pr_global grs
+
+ARGUMENT EXTEND hints_path_atom
+ TYPED AS hints_path_atom
+ PRINTED BY pr_hints_path_atom
+| [ global_list(g) ] -> [ PathHints (List.map Nametab.global g) ]
+| [ "*" ] -> [ PathAny ]
+END
+
+let pr_hints_path prc prx pry c =
+ let rec aux = function
+ | PathAtom a -> pr_hints_path_atom prc prx pry a
+ | PathStar p -> str"(" ++ aux p ++ str")*"
+ | PathSeq (p, p') -> aux p ++ spc () ++ aux p'
+ | PathOr (p, p') -> str "(" ++ aux p ++ str"|" ++ aux p' ++ str")"
+ | PathEmpty -> str"ø"
+ | PathEpsilon -> str"ε"
+ in aux c
+
+ARGUMENT EXTEND hints_path
+ TYPED AS hints_path
+ PRINTED BY pr_hints_path
+| [ "(" hints_path(p) ")" ] -> [ p ]
+| [ "!" hints_path(p) ] -> [ PathStar p ]
+| [ "emp" ] -> [ PathEmpty ]
+| [ "eps" ] -> [ PathEpsilon ]
+| [ hints_path_atom(a) ] -> [ PathAtom a ]
+| [ hints_path(p) "|" hints_path(q) ] -> [ PathOr (p, q) ]
+| [ hints_path(p) ";" hints_path(q) ] -> [ PathSeq (p, q) ]
+END
+
+let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases
+
+ARGUMENT EXTEND opthints
+ TYPED AS preident_list_opt
+ PRINTED BY pr_hintbases
+| [ ":" ne_preident_list(l) ] -> [ Some l ]
+| [ ] -> [ None ]
+END
+
+VERNAC COMMAND EXTEND HintCut
+| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [
+ let entry = HintsCutEntry p in
+ Auto.add_hints (Vernacexpr.use_section_locality ())
+ (match dbnames with None -> ["core"] | Some l -> l) entry ]
+END
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-28 19:10:04 +0000