aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES7
-rw-r--r--lib/explore.ml18
-rw-r--r--lib/explore.mli2
-rw-r--r--lib/pp.ml419
-rw-r--r--lib/pp.mli3
-rw-r--r--parsing/g_tactic.ml426
-rw-r--r--parsing/pptactic.ml27
-rw-r--r--parsing/q_coqast.ml415
-rw-r--r--plugins/funind/functional_principles_proofs.ml3
-rw-r--r--plugins/funind/recdef.ml1
-rw-r--r--plugins/rtauto/proof_search.ml4
-rw-r--r--plugins/rtauto/proof_search.mli2
-rw-r--r--proofs/refiner.ml4
-rw-r--r--proofs/refiner.mli1
-rw-r--r--proofs/tacexpr.ml8
-rw-r--r--tactics/auto.ml296
-rw-r--r--tactics/auto.mli37
-rw-r--r--tactics/eauto.ml4146
-rw-r--r--tactics/eauto.mli4
-rw-r--r--tactics/tacinterp.ml46
-rw-r--r--tactics/tacticals.ml1
-rw-r--r--tactics/tacticals.mli1
22 files changed, 460 insertions, 211 deletions
diff --git a/CHANGES b/CHANGES
index 1fcca5888..e2113ccff 100644
--- a/CHANGES
+++ b/CHANGES
@@ -12,6 +12,13 @@ Vernacular commands
Tactics
- Tactics btauto, a reflexive boolean tautology solver.
+- Still no general "info" tactical, but new specific tactics
+ info_auto, info_eauto, info_trivial which provides information
+ on the proofs found by auto/eauto/trivial. Display of these
+ details could also be activated by Set Info Auto/Eauto/Trivial.
+- Details on everything tried by auto/eauto/trivial during
+ a proof search could be obtained by "debug auto", "debug eauto",
+ "debug trivial" or by a global "Set Debug Auto/Eauto/Trivial".
Program
diff --git a/lib/explore.ml b/lib/explore.ml
index 407bf1e91..e353c9070 100644
--- a/lib/explore.ml
+++ b/lib/explore.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Format
+open Pp
(*s Definition of a search problem. *)
@@ -14,20 +14,20 @@ module type SearchProblem = sig
type state
val branching : state -> state list
val success : state -> bool
- val pp : state -> unit
+ val pp : state -> std_ppcmds
end
module Make = functor(S : SearchProblem) -> struct
type position = int list
- let pp_position p =
+ let msg_with_position p pp =
let rec pp_rec = function
- | [] -> ()
- | [i] -> printf "%d" i
- | i :: l -> pp_rec l; printf ".%d" i
+ | [] -> mt ()
+ | [i] -> int i
+ | i :: l -> pp_rec l ++ str "." ++ int i
in
- open_hbox (); pp_rec p; close_box ()
+ msg_debug (h 0 (pp_rec p) ++ pp)
(*s Depth first search. *)
@@ -40,7 +40,7 @@ module Make = functor(S : SearchProblem) -> struct
let debug_depth_first s =
let rec explore p s =
- pp_position p; S.pp s;
+ msg_with_position p (S.pp s);
if S.success s then s else explore_many 1 p (S.branching s)
and explore_many i p = function
| [] -> raise Not_found
@@ -83,7 +83,7 @@ module Make = functor(S : SearchProblem) -> struct
explore q
| s :: l ->
let ps = i::p in
- pp_position ps; S.pp s;
+ msg_with_position ps (S.pp s);
if S.success s then s else enqueue (succ i) p (push (ps,s) q) l
in
enqueue 1 [] empty [s]
diff --git a/lib/explore.mli b/lib/explore.mli
index e64459f10..a292fd83e 100644
--- a/lib/explore.mli
+++ b/lib/explore.mli
@@ -27,7 +27,7 @@ module type SearchProblem = sig
val success : state -> bool
- val pp : state -> unit
+ val pp : state -> Pp.std_ppcmds
end
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 4fc53270c..ff1973846 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -275,17 +275,15 @@ let pp_dirs ft =
(* pretty print on stdout and stderr *)
(* Special chars for emacs, to detect warnings inside goal output *)
-let emacs_warning_start_string = String.make 1 (Char.chr 254)
-let emacs_warning_end_string = String.make 1 (Char.chr 255)
+let emacs_quote_start = String.make 1 (Char.chr 254)
+let emacs_quote_end = String.make 1 (Char.chr 255)
-let warnstart() =
- if not !print_emacs then mt() else str emacs_warning_start_string
+let emacs_quote strm =
+ if !print_emacs then
+ [< str emacs_quote_start; hov 0 strm; str emacs_quote_end >]
+ else hov 0 strm
-let warnend() =
- if not !print_emacs then mt() else str emacs_warning_end_string
-
-let warnbody strm =
- [< warnstart() ; hov 0 (str "Warning: " ++ strm) ; warnend() >]
+let warnbody strm = emacs_quote (str "Warning: " ++ strm)
(* pretty printing functions WITHOUT FLUSH *)
let pp_with ft strm =
@@ -334,6 +332,9 @@ let msgerr x = msg_with !err_ft x
let msgerrnl x = msgnl_with !err_ft x
let msg_warning x = msg_warning_with !err_ft x
+(* Same specific display in emacs as warning, but without the "Warning:" *)
+let msg_debug x = msgnl (emacs_quote x)
+
let string_of_ppcmds c =
msg_with Format.str_formatter c;
Format.flush_str_formatter ()
diff --git a/lib/pp.mli b/lib/pp.mli
index 2fd62d55a..112d97655 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -114,6 +114,9 @@ val msgerr : std_ppcmds -> unit
val msgerrnl : std_ppcmds -> unit
val msg_warning : std_ppcmds -> unit
+(** Same specific display in emacs as warning, but without the "Warning:" **)
+val msg_debug : std_ppcmds -> unit
+
val string_of_ppcmds : std_ppcmds -> string
(** {6 Location management. } *)
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 7dc166750..ddff97128 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -435,6 +435,16 @@ GEXTEND Gram
[ [ "using"; l = LIST1 constr SEP "," -> l
| -> [] ] ]
;
+ trivial:
+ [ [ IDENT "trivial" -> Off
+ | IDENT "info_trivial" -> Info
+ | IDENT "debug"; IDENT "trivial" -> Debug ] ]
+ ;
+ auto:
+ [ [ IDENT "auto" -> Off
+ | IDENT "info_auto" -> Info
+ | IDENT "debug"; IDENT "auto" -> Debug ] ]
+ ;
eliminator:
[ [ "using"; el = constr_with_bindings -> el ] ]
;
@@ -597,15 +607,13 @@ GEXTEND Gram
-> TacDecompose (l,c)
(* Automation tactic *)
- | IDENT "trivial"; lems = auto_using; db = hintbases ->
- TacTrivial (lems,db)
- | IDENT "auto"; n = OPT int_or_var; lems = auto_using; db = hintbases ->
- TacAuto (n,lems,db)
-
- | IDENT "auto"; IDENT "decomp"; p = OPT natural;
- lems = auto_using -> TacDAuto (None,p,lems)
- | IDENT "auto"; n = OPT int_or_var; IDENT "decomp"; p = OPT natural;
- lems = auto_using -> TacDAuto (n,p,lems)
+ | d = trivial; lems = auto_using; db = hintbases -> TacTrivial (d,lems,db)
+ | d = auto; n = OPT int_or_var; lems = auto_using; db = hintbases ->
+ TacAuto (d,n,lems,db)
+ | d = auto; IDENT "decomp"; p = OPT natural; lems = auto_using ->
+ TacDAuto (d,None,p,lems)
+ | d = auto; n = OPT int_or_var; IDENT "decomp"; p = OPT natural;
+ lems = auto_using -> TacDAuto (d,n,p,lems)
(* Context management *)
| IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacClear (true, l)
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 465d0b76a..1e0f2aef2 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -516,6 +516,11 @@ let pr_auto_using prc = function
| l -> spc () ++
hov 2 (str "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
+let string_of_debug = function
+ | Off -> ""
+ | Debug -> "debug "
+ | Info -> "info_"
+
let pr_then () = str ";"
let ltop = (5,E)
@@ -624,8 +629,8 @@ let rec pr_atom0 = function
| TacAssumption -> str "assumption"
| TacAnyConstructor (false,None) -> str "constructor"
| TacAnyConstructor (true,None) -> str "econstructor"
- | TacTrivial ([],Some []) -> str "trivial"
- | TacAuto (None,[],Some []) -> str "auto"
+ | TacTrivial (d,[],Some []) -> str (string_of_debug d ^ "trivial")
+ | TacAuto (d,None,[],Some []) -> str (string_of_debug d ^ "auto")
| TacReflexivity -> str "reflexivity"
| TacClear (true,[]) -> str "clear"
| t -> str "(" ++ pr_atom1 t ++ str ")"
@@ -738,16 +743,18 @@ and pr_atom1 = function
hov 1 (str "lapply" ++ pr_constrarg c)
(* Automation tactics *)
- | TacTrivial ([],Some []) as x -> pr_atom0 x
- | TacTrivial (lems,db) ->
- hov 0 (str "trivial" ++
+ | TacTrivial (_,[],Some []) as x -> pr_atom0 x
+ | TacTrivial (d,lems,db) ->
+ hov 0 (str (string_of_debug d ^ "trivial") ++
pr_auto_using pr_constr lems ++ pr_hintbases db)
- | TacAuto (None,[],Some []) as x -> pr_atom0 x
- | TacAuto (n,lems,db) ->
- hov 0 (str "auto" ++ pr_opt (pr_or_var int) n ++
+ | TacAuto (_,None,[],Some []) as x -> pr_atom0 x
+ | TacAuto (d,n,lems,db) ->
+ hov 0 (str (string_of_debug d ^ "auto") ++
+ pr_opt (pr_or_var int) n ++
pr_auto_using pr_constr lems ++ pr_hintbases db)
- | TacDAuto (n,p,lems) ->
- hov 1 (str "auto" ++ pr_opt (pr_or_var int) n ++ str "decomp" ++
+ | TacDAuto (d,n,p,lems) ->
+ hov 1 (str (string_of_debug d ^ "auto") ++
+ pr_opt (pr_or_var int) n ++ str "decomp" ++
pr_opt int p ++ pr_auto_using pr_constr lems)
(* Context management *)
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 389118c34..df2597208 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -273,6 +273,11 @@ let mlexpr_of_message_token = function
| Tacexpr.MsgInt n -> <:expr< Tacexpr.MsgInt $mlexpr_of_int n$ >>
| Tacexpr.MsgIdent id -> <:expr< Tacexpr.MsgIdent $mlexpr_of_hyp id$ >>
+let mlexpr_of_debug = function
+ | Tacexpr.Off -> <:expr< Tacexpr.Off >>
+ | Tacexpr.Debug -> <:expr< Tacexpr.Debug >>
+ | Tacexpr.Info -> <:expr< Tacexpr.Info >>
+
let rec mlexpr_of_atomic_tactic = function
(* Basic tactics *)
| Tacexpr.TacIntroPattern pl ->
@@ -399,15 +404,17 @@ let rec mlexpr_of_atomic_tactic = function
| Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_option mlexpr_of_constr c$ >>
(* Automation tactics *)
- | Tacexpr.TacAuto (n,lems,l) ->
+ | Tacexpr.TacAuto (debug,n,lems,l) ->
+ let d = mlexpr_of_debug debug in
let n = mlexpr_of_option (mlexpr_of_or_var mlexpr_of_int) n in
let lems = mlexpr_of_list mlexpr_of_constr lems in
let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in
- <:expr< Tacexpr.TacAuto $n$ $lems$ $l$ >>
- | Tacexpr.TacTrivial (lems,l) ->
+ <:expr< Tacexpr.TacAuto $d$ $n$ $lems$ $l$ >>
+ | Tacexpr.TacTrivial (debug,lems,l) ->
+ let d = mlexpr_of_debug debug in
let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in
let lems = mlexpr_of_list mlexpr_of_constr lems in
- <:expr< Tacexpr.TacTrivial $lems$ $l$ >>
+ <:expr< Tacexpr.TacTrivial $d$ $lems$ $l$ >>
| _ -> failwith "Quotation of atomic tactic expressions: TODO"
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 13b3dabdf..4d5cbe223 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1415,7 +1415,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic =
(* let ids = List.filter (fun id -> not (List.mem id ids)) ids' in *)
(* rewrite *)
(* ) *)
- Eauto.gen_eauto false (false,5) [] (Some [])
+ Eauto.gen_eauto (false,5) [] (Some [])
]
gls
@@ -1493,7 +1493,6 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
(
tclCOMPLETE(
Eauto.eauto_with_bases
- false
(true,5)
[Evd.empty,Lazy.force refl_equal]
[Auto.Hint_db.empty empty_transparent_state false]
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 7613c6765..8eb7d0e8f 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1322,7 +1322,6 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
(eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))
e_assumption;
Eauto.eauto_with_bases
- false
(true,5)
[Evd.empty,Lazy.force refl_equal]
[Auto.Hint_db.empty empty_transparent_state false]
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 2448a2d39..d772279f1 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -510,8 +510,8 @@ let pp_gl gl= cut () ++
let pp =
function
- Incomplete(gl,ctx) -> msgnl (pp_gl gl)
- | _ -> msg (str "<complete>")
+ Incomplete(gl,ctx) -> pp_gl gl ++ fnl ()
+ | _ -> str "<complete>"
let pp_info () =
let count_info =
diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli
index b236aa721..275e94cde 100644
--- a/plugins/rtauto/proof_search.mli
+++ b/plugins/rtauto/proof_search.mli
@@ -38,7 +38,7 @@ val branching: state -> state list
val success: state -> bool
-val pp: state -> unit
+val pp: state -> Pp.std_ppcmds
val pr_form : form -> unit
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 19c09571f..221c46a92 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -416,10 +416,6 @@ let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
let pp_info = ref (fun _ _ _ -> assert false)
let set_info_printer f = pp_info := f
-let tclINFO (tac : tactic) gls =
- msgnl (hov 0 (str "Warning: info is currently not working"));
- tac gls
-
(* Check that holes in arguments have been resolved *)
let check_evars env sigma extsigma gl =
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 75fd6d3d6..9d3d37c22 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -137,7 +137,6 @@ val tclTIMEOUT : int -> tactic -> tactic
val tclWEAK_PROGRESS : tactic -> tactic
val tclPROGRESS : tactic -> tactic
val tclNOTSAMEGOAL : tactic -> tactic
-val tclINFO : tactic -> tactic
(** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,
if it succeeds, applies [tac2] to the resulting subgoals,
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index a044f563f..cec6fd419 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -29,6 +29,8 @@ type split_flag = bool (* true = exists false = split *)
type hidden_flag = bool (* true = internal use false = user-level *)
type letin_flag = bool (* true = use local def false = use Leibniz *)
+type debug = Debug | Info | Off (* for trivial / auto / eauto ... *)
+
type glob_red_flag =
| FBeta
| FIota
@@ -173,9 +175,9 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr =
| TacLApply of 'constr
(* Automation tactics *)
- | TacTrivial of 'constr list * string list option
- | TacAuto of int or_var option * 'constr list * string list option
- | TacDAuto of int or_var option * int option * 'constr list
+ | TacTrivial of debug * 'constr list * string list option
+ | TacAuto of debug * int or_var option * 'constr list * string list option
+ | TacDAuto of debug * int or_var option * int option * 'constr list
(* Context management *)
| TacClear of bool * 'id list
diff --git a/tactics/auto.ml b/tactics/auto.ml
index cfef521c8..cedec80a1 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -879,14 +879,14 @@ let add_hints local dbnames0 h =
let pr_autotactic =
function
- | Res_pf (c,clenv) -> (str"apply " ++ pr_lconstr c)
- | ERes_pf (c,clenv) -> (str"eapply " ++ pr_lconstr c)
- | Give_exact c -> (str"exact " ++ pr_lconstr c)
+ | Res_pf (c,clenv) -> (str"apply " ++ pr_constr c)
+ | ERes_pf (c,clenv) -> (str"eapply " ++ pr_constr c)
+ | Give_exact c -> (str"exact " ++ pr_constr c)
| Res_pf_THEN_trivial_fail (c,clenv) ->
- (str"apply " ++ pr_lconstr c ++ str" ; trivial")
+ (str"apply " ++ pr_constr c ++ str" ; trivial")
| Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c)
| Extern tac ->
- (str "(external) " ++ Pptactic.pr_glob_tactic (Global.env()) tac)
+ (str "(*external*) " ++ Pptactic.pr_glob_tactic (Global.env()) tac)
let pr_hint (id, v) =
(pr_autotactic v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ())
@@ -1099,6 +1099,131 @@ let conclPattern concl pat tac gl =
with PatternMatchingFailure -> error "conclPattern" in
!forward_interp_tactic constr_bindings tac gl
+(***********************************************************)
+(** A debugging / verbosity framework for trivial and auto *)
+(***********************************************************)
+
+(** The following options allow to trigger debugging/verbosity
+ without having to adapt the scripts.
+ Note: if Debug and Info are both activated, Debug take precedence. *)
+
+let global_debug_trivial = ref false
+let global_debug_auto = ref false
+let global_info_trivial = ref false
+let global_info_auto = ref false
+
+let add_option ls refe =
+ let _ = Goptions.declare_bool_option
+ { Goptions.optsync = true;
+ Goptions.optdepr = false;
+ Goptions.optname = String.concat " " ls;
+ Goptions.optkey = ls;
+ Goptions.optread = (fun () -> !refe);
+ Goptions.optwrite = (:=) refe }
+ in ()
+
+let _ =
+ add_option ["Debug";"Trivial"] global_debug_trivial;
+ add_option ["Debug";"Auto"] global_debug_auto;
+ add_option ["Info";"Trivial"] global_info_trivial;
+ add_option ["Info";"Auto"] global_info_auto
+
+let no_dbg () = (Off,0,ref [])
+
+let mk_trivial_dbg debug =
+ let d =
+ if debug = Debug || !global_debug_trivial then Debug
+ else if debug = Info || !global_info_trivial then Info
+ else Off
+ in (d,0,ref [])
+
+(** Note : we start the debug depth of auto at 1 to distinguish it
+ for trivial (whose depth is 0). *)
+
+let mk_auto_dbg debug =
+ let d =
+ if debug = Debug || !global_debug_auto then Debug
+ else if debug = Info || !global_info_auto then Info
+ else Off
+ in (d,1,ref [])
+
+let incr_dbg = function (dbg,depth,trace) -> (dbg,depth+1,trace)
+
+(** A tracing tactic for debug/info trivial/auto *)
+
+let tclLOG (dbg,depth,trace) pp tac =
+ match dbg with
+ | Off -> tac
+ | Debug ->
+ (* For "debug (trivial/auto)", we directly output messages *)
+ let s = String.make depth '*' in
+ begin fun gl ->
+ try
+ let out = tac gl in
+ msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)");
+ out
+ with e ->
+ msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)");
+ raise e
+ end
+ | Info ->
+ (* For "info (trivial/auto)", we store a log trace *)
+ begin fun gl ->
+ try
+ let out = tac gl in
+ trace := (depth, Some pp) :: !trace;
+ out
+ with e ->
+ trace := (depth, None) :: !trace;
+ raise e
+ end
+
+(** For info, from the linear trace information, we reconstitute the part
+ of the proof tree we're interested in. The last executed tactic
+ comes first in the trace (and it should be a successful one).
+ [depth] is the root depth of the tree fragment we're visiting.
+ [keep] means we're in a successful tree fragment (the very last
+ tactic has been successful). *)
+
+let rec cleanup_info_trace depth acc = function
+ | [] -> acc
+ | (d,Some pp) :: l -> cleanup_info_trace d ((d,pp)::acc) l
+ | l -> cleanup_info_trace depth acc (erase_subtree depth l)
+
+and erase_subtree depth = function
+ | [] -> []
+ | (d,_) :: l -> if d = depth then l else erase_subtree depth l
+
+let pr_info_atom (d,pp) =
+ msg_debug (str (String.make d ' ') ++ pp () ++ str ".")
+
+let pr_info_trace = function
+ | (Info,_,{contents=(d,Some pp)::l}) ->
+ List.iter pr_info_atom (cleanup_info_trace d [(d,pp)] l)
+ | _ -> ()
+
+let pr_info_nop = function
+ | (Info,_,_) -> msg_debug (str "idtac.")
+ | _ -> ()
+
+let pr_dbg_header = function
+ | (Off,_,_) -> ()
+ | (Debug,0,_) -> msg_debug (str "(* debug trivial : *)")
+ | (Debug,_,_) -> msg_debug (str "(* debug auto : *)")
+ | (Info,0,_) -> msg_debug (str "(* info trivial : *)")
+ | (Info,_,_) -> msg_debug (str "(* info auto : *)")
+
+let tclTRY_dbg d tac =
+ tclORELSE0
+ (fun gl ->
+ pr_dbg_header d;
+ let out = tac gl in
+ pr_info_trace d;
+ out)
+ (fun gl ->
+ pr_info_nop d;
+ tclIDTAC gl)
+
(**************************************************************************)
(* The Trivial tactic *)
(**************************************************************************)
@@ -1122,17 +1247,20 @@ let exists_evaluable_reference env = function
| EvalConstRef _ -> true
| EvalVarRef v -> try ignore(lookup_named v env); true with Not_found -> false
-let rec trivial_fail_db mod_delta db_list local_db gl =
+let dbg_intro dbg = tclLOG dbg (fun () -> str "intro") intro
+let dbg_assumption dbg = tclLOG dbg (fun () -> str "assumption") assumption
+
+let rec trivial_fail_db dbg mod_delta db_list local_db gl =
let intro_tac =
- tclTHEN intro
+ tclTHEN (dbg_intro dbg)
(fun g'->
let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
- in trivial_fail_db mod_delta db_list (Hint_db.add_list hintl local_db) g')
+ in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list hintl local_db) g')
in
tclFIRST
- (assumption::intro_tac::
- (List.map (fun tac -> tclCOMPLETE tac)
- (trivial_resolve mod_delta db_list local_db (pf_concl gl)))) gl
+ ((dbg_assumption dbg)::intro_tac::
+ (List.map tclCOMPLETE
+ (trivial_resolve dbg mod_delta db_list local_db (pf_concl gl)))) gl
and my_find_search_nodelta db_list local_db hdc concl =
List.map (fun hint -> (None,hint))
@@ -1173,7 +1301,7 @@ and my_find_search_delta db_list local_db hdc concl =
in List.map (fun x -> (Some flags,x)) l)
(local_db::db_list)
-and tac_of_hint db_list local_db concl (flags, ({pat=p; code=t})) =
+and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t})) =
let tactic =
match t with
| Res_pf (c,cl) -> unify_resolve_gen flags (c,cl)
@@ -1182,23 +1310,26 @@ and tac_of_hint db_list local_db concl (flags, ({pat=p; code=t})) =
| Res_pf_THEN_trivial_fail (c,cl) ->
tclTHEN
(unify_resolve_gen flags (c,cl))
- (trivial_fail_db (flags <> None) db_list local_db)
- | Unfold_nth c ->
+ (* With "(debug) trivial", we shouldn't end here, and
+ with "debug auto" we don't display the details of inner trivial *)
+ (trivial_fail_db (no_dbg ()) (flags <> None) db_list local_db)
+ | Unfold_nth c ->
(fun gl ->
if exists_evaluable_reference (pf_env gl) c then
tclPROGRESS (h_reduce (Unfold [all_occurrences_expr,c]) onConcl) gl
else tclFAIL 0 (str"Unbound reference") gl)
| Extern tacast -> conclPattern concl p tacast
- in tactic
+ in
+ tclLOG dbg (fun () -> pr_autotactic t) tactic
-and trivial_resolve mod_delta db_list local_db cl =
+and trivial_resolve dbg mod_delta db_list local_db cl =
try
let head =
try let hdconstr,_ = head_constr_bound cl in
Some (head_of_constr_reference hdconstr)
with Bound -> None
in
- List.map (tac_of_hint db_list local_db cl)
+ List.map (tac_of_hint dbg db_list local_db cl)
(priority
(my_find_search mod_delta db_list local_db head cl))
with Not_found -> []
@@ -1215,52 +1346,59 @@ let make_db_list dbnames =
in
List.map lookup dbnames
-let trivial lems dbnames gl =
+let trivial ?(debug=Off) lems dbnames gl =
let db_list = make_db_list dbnames in
- tclTRY (trivial_fail_db false db_list (make_local_hint_db false lems gl)) gl
+ let d = mk_trivial_dbg debug in
+ tclTRY_dbg d
+ (trivial_fail_db d false db_list (make_local_hint_db false lems gl)) gl
-let full_trivial lems gl =
+let full_trivial ?(debug=Off) lems gl =
let dbnames = Hintdbmap.dom !searchtable in
let dbnames = list_remove "v62" dbnames in
let db_list = List.map (fun x -> searchtable_map x) dbnames in
- tclTRY (trivial_fail_db false db_list (make_local_hint_db false lems gl)) gl
+ let d = mk_trivial_dbg debug in
+ tclTRY_dbg d
+ (trivial_fail_db d false db_list (make_local_hint_db false lems gl)) gl
-let gen_trivial lems = function
- | None -> full_trivial lems
- | Some l -> trivial lems l
+let gen_trivial ?(debug=Off) lems = function
+ | None -> full_trivial ~debug lems
+ | Some l -> trivial ~debug lems l
-let h_trivial lems l =
- Refiner.abstract_tactic (TacTrivial (List.map snd lems,l))
- (gen_trivial lems l)
+let h_trivial ?(debug=Off) lems l =
+ Refiner.abstract_tactic (TacTrivial (debug,List.map snd lems,l))
+ (gen_trivial ~debug lems l)
(**************************************************************************)
(* The classical Auto tactic *)
(**************************************************************************)
-let possible_resolve mod_delta db_list local_db cl =
+let possible_resolve dbg mod_delta db_list local_db cl =
try
let head =
try let hdconstr,_ = head_constr_bound cl in
Some (head_of_constr_reference hdconstr)
with Bound -> None
in
- List.map (tac_of_hint db_list local_db cl)
+ List.map (tac_of_hint dbg db_list local_db cl)
(my_find_search mod_delta db_list local_db head cl)
with Not_found -> []
-let decomp_unary_term_then (id,_,typc) kont1 kont2 gl =
+let dbg_case dbg id =
+ tclLOG dbg (fun () -> str "case " ++ pr_id id) (simplest_case (mkVar id))
+
+let decomp_unary_term_then dbg (id,_,typc) kont1 kont2 gl =
try
let ccl = applist (head_constr typc) in
match Hipattern.match_with_conjunction ccl with
| Some (_,args) ->
- tclTHEN (simplest_case (mkVar id)) (kont1 (List.length args)) gl
+ tclTHEN (dbg_case dbg id) (kont1 (List.length args)) gl
| None ->
kont2 gl
with UserError _ -> kont2 gl
-let decomp_empty_term (id,_,typc) gl =
+let decomp_empty_term dbg (id,_,typc) gl =
if Hipattern.is_empty_type typc then
- simplest_case (mkVar id) gl
+ dbg_case dbg id gl
else
errorlabstrm "Auto.decomp_empty_term" (str "Not an empty type.")
@@ -1272,32 +1410,32 @@ let extend_local_db gl decl db =
empty type) then call the continuation tactic with hint db extended
with the obtained not-further-decomposable hypotheses *)
-let rec decomp_and_register_decl p kont (id,_,_ as decl) db gl =
+let rec decomp_and_register_decl dbg p kont (id,_,_ as decl) db gl =
if p = 0 then
kont (extend_local_db gl decl db) gl
else
tclORELSE0
- (decomp_empty_term decl)
- (decomp_unary_term_then decl (intros_decomp (p-1) kont [] db)
+ (decomp_empty_term dbg decl)
+ (decomp_unary_term_then dbg decl (intros_decomp dbg (p-1) kont [] db)
(kont (extend_local_db gl decl db))) gl
(* Introduce [n] hypotheses, then decompose then with maximum depth [p] and
call the continuation tactic [kont] with the hint db extended
with the so-obtained not-further-decomposable hypotheses *)
-and intros_decomp p kont decls db n =
+and intros_decomp dbg p kont decls db n =
if n = 0 then
- decomp_and_register_decls p kont decls db
+ decomp_and_register_decls dbg p kont decls db
else
- tclTHEN intro (onLastDecl (fun d ->
- (intros_decomp p kont (d::decls) db (n-1))))
+ tclTHEN (dbg_intro dbg) (onLastDecl (fun d ->
+ (intros_decomp dbg p kont (d::decls) db (n-1))))
(* Decompose hypotheses [hyps] with maximum depth [p] and
call the continuation tactic [kont] with the hint db extended
with the so-obtained not-further-decomposable hypotheses *)
-and decomp_and_register_decls p kont decls =
- List.fold_left (decomp_and_register_decl p) kont decls
+and decomp_and_register_decls dbg p kont decls =
+ List.fold_left (decomp_and_register_decl dbg p) kont decls
(* decomp is an natural number giving an indication on decomposition
@@ -1307,53 +1445,60 @@ and decomp_and_register_decls p kont decls =
exception Uplift of tactic list
-let search_gen p n mod_delta db_list local_db =
- let rec search n local_db =
+let search_gen d p n mod_delta db_list local_db =
+ let rec search d n local_db =
if n=0 then (fun gl -> error "BOUND 2") else
- tclORELSE0 assumption
- (tclORELSE0 (intros_decomp p (search n) [] local_db 1)
- (fun gl -> tclFIRST
- (List.map (fun ntac -> tclTHEN ntac (search (n-1) local_db))
- (possible_resolve mod_delta db_list local_db (pf_concl gl))) gl))
+ tclORELSE0 (dbg_assumption d)
+ (tclORELSE0 (intros_decomp d p (search d n) [] local_db 1)
+ (fun gl ->
+ let d' = incr_dbg d in
+ tclFIRST
+ (List.map
+ (fun ntac -> tclTHEN ntac (search d' (n-1) local_db))
+ (possible_resolve d mod_delta db_list local_db (pf_concl gl))) gl))
in
- search n local_db
+ search d n local_db
-let search = search_gen 0
+let search dbg = search_gen dbg 0
let default_search_depth = ref 5
-let delta_auto mod_delta n lems dbnames gl =
+let delta_auto ?(debug=Off) mod_delta n lems dbnames gl =
let db_list = make_db_list dbnames in
- tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl)) gl
+ let d = mk_auto_dbg debug in
+ tclTRY_dbg d
+ (search d n mod_delta db_list (make_local_hint_db false lems gl)) gl
-let auto = delta_auto false
+let auto ?(debug=Off) n = delta_auto ~debug false n
-let new_auto = delta_auto true
+let new_auto ?(debug=Off) n = delta_auto ~debug true n
let default_auto = auto !default_search_depth [] []
-let delta_full_auto mod_delta n lems gl =
+let delta_full_auto ?(debug=Off) mod_delta n lems gl =
let dbnames = Hintdbmap.dom !searchtable in
let dbnames = list_remove "v62" dbnames in
let db_list = List.map (fun x -> searchtable_map x) dbnames in
- tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl)) gl
+ let d = mk_auto_dbg debug in
+ tclTRY_dbg d
+ (search d n mod_delta db_list (make_local_hint_db false lems gl)) gl
-let full_auto = delta_full_auto false
-let new_full_auto = delta_full_auto true
+let full_auto ?(debug=Off) n = delta_full_auto ~debug false n
+let new_full_auto ?(debug=Off) n = delta_full_auto ~debug true n
let default_full_auto gl = full_auto !default_search_depth [] gl
-let gen_auto n lems dbnames =
+let gen_auto ?(debug=Off) n lems dbnames =
let n = match n with None -> !default_search_depth | Some n -> n in
match dbnames with
- | None -> full_auto n lems
- | Some l -> auto n lems l
+ | None -> full_auto ~debug n lems
+ | Some l -> auto ~debug n lems l
let inj_or_var = Option.map (fun n -> ArgArg n)
-let h_auto n lems l =
- Refiner.abstract_tactic (TacAuto (inj_or_var n,List.map snd lems,l))
- (gen_auto n lems l)
+let h_auto ?(debug=Off) n lems l =
+ Refiner.abstract_tactic (TacAuto (debug,inj_or_var n,List.map snd lems,l))
+ (gen_auto ~debug n lems l)
(**************************************************************************)
(* The "destructing Auto" from Eduardo *)
@@ -1363,23 +1508,26 @@ let h_auto n lems l =
one look for an immediate solution *)
let default_search_decomp = ref 20
-let destruct_auto p lems n gl =
- decomp_and_register_decls p (fun local_db gl ->
- search_gen p n false (List.map searchtable_map ["core";"extcore"])
+let destruct_auto d p lems n gl =
+ decomp_and_register_decls d p (fun local_db gl ->
+ search_gen d p n false (List.map searchtable_map ["core";"extcore"])
(add_hint_lemmas false lems local_db gl) gl)
(pf_hyps gl)
(Hint_db.empty empty_transparent_state false)
gl
-let dautomatic des_opt lems n = tclTRY (destruct_auto des_opt lems n)
+let dautomatic ?(debug=Off) des_opt lems n =
+ let d = mk_auto_dbg debug in
+ tclTRY_dbg d (destruct_auto d des_opt lems n)
-let dauto (n,p) lems =
+let dauto ?(debug=Off) (n,p) lems =
let p = match p with Some p -> p | None -> !default_search_decomp in
let n = match n with Some n -> n | None -> !default_search_depth in
- dautomatic p lems n
+ dautomatic ~debug p lems n
let default_dauto = dauto (None,None) []
-let h_dauto (n,p) lems =
- Refiner.abstract_tactic (TacDAuto (inj_or_var n,p,List.map snd lems))
- (dauto (n,p) lems)
+let h_dauto ?(debug=Off) (n,p) lems =
+ Refiner.abstract_tactic
+ (TacDAuto (debug,inj_or_var n,p,List.map snd lems))
+ (dauto ~debug (n,p) lems)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 95de089e0..69a526e5a 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -219,48 +219,61 @@ val conclPattern : constr -> constr_pattern option -> Tacexpr.glob_tactic_expr -
val make_db_list : hint_db_name list -> hint_db list
-val auto : int -> open_constr list -> hint_db_name list -> tactic
+val auto : ?debug:Tacexpr.debug ->
+ int -> open_constr list -> hint_db_name list -> tactic
(** Auto with more delta. *)
-val new_auto : int -> open_constr list -> hint_db_name list -> tactic
+val new_auto : ?debug:Tacexpr.debug ->
+ int -> open_constr list -> hint_db_name list -> tactic
(** auto with default search depth and with the hint database "core" *)
val default_auto : tactic
(** auto with all hint databases except the "v62" compatibility database *)
-val full_auto : int -> open_constr list -> tactic
+val full_auto : ?debug:Tacexpr.debug ->
+ int -> open_constr list -> tactic
(** auto with all hint databases except the "v62" compatibility database
and doing delta *)
-val new_full_auto : int -> open_constr list -> tactic
+val new_full_auto : ?debug:Tacexpr.debug ->
+ int -> open_constr list -> tactic
(** auto with default search depth and with all hint databases
except the "v62" compatibility database *)
val default_full_auto : tactic
(** The generic form of auto (second arg [None] means all bases) *)
-val gen_auto : int option -> open_constr list -> hint_db_name list option -> tactic
+val gen_auto : ?debug:Tacexpr.debug ->
+ int option -> open_constr list -> hint_db_name list option -> tactic
(** The hidden version of auto *)
-val h_auto : int option -> open_constr list -> hint_db_name list option -> tactic
+val h_auto : ?debug:Tacexpr.debug ->
+ int option -> open_constr list -> hint_db_name list option -> tactic
(** Trivial *)
-val trivial : open_constr list -> hint_db_name list -> tactic
-val gen_trivial : open_constr list -> hint_db_name list option -> tactic
-val full_trivial : open_constr list -> tactic
-val h_trivial : open_constr list -> hint_db_name list option -> tactic
+
+val trivial : ?debug:Tacexpr.debug ->
+ open_constr list -> hint_db_name list -> tactic
+val gen_trivial : ?debug:Tacexpr.debug ->
+ open_constr list -> hint_db_name list option -> tactic
+val full_trivial : ?debug:Tacexpr.debug ->
+ open_constr list -> tactic
+val h_trivial : ?debug:Tacexpr.debug ->
+ open_constr list -> hint_db_name list option -> tactic
val pr_autotactic : 'a auto_tactic -> Pp.std_ppcmds
(** Destructing Auto *)
(** DAuto *)
-val dauto : int option * int option -> open_constr list -> tactic
+val dauto : ?debug:Tacexpr.debug ->
+ int option * int option -> open_constr list -> tactic
val default_search_decomp : int ref
val default_dauto : tactic
-val h_dauto : int option * int option -> open_constr list -> tactic
+val h_dauto : ?debug:Tacexpr.debug ->
+ int option * int option -> open_constr list -> tactic
(** Hook for changing the initialization of auto *)
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 4923aa720..a0187434a 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -28,6 +28,7 @@ open Clenv
open Auto
open Glob_term
open Hiddentac
+open Tacexpr
let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_transparent_state }
@@ -172,7 +173,14 @@ type search_state = {
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
@@ -212,6 +220,7 @@ module SearchProblem = struct
if s.depth = 0 then
[]
else
+ 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);
@@ -226,7 +235,8 @@ 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
@@ -238,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 =
@@ -249,73 +259,122 @@ module SearchProblem = struct
(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] }
-
-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 =
- 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
- s.tacres
- with Not_found -> error "eauto: breadth first search failed."
+ localdb = [localdb];
+ prev = if dbg=Info then Init else Unknown;
+ }
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
- 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
+ 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
+ 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 ->
+ 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 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_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
@@ -363,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
@@ -371,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
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 68ec42f4e..5e656139b 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -27,11 +27,11 @@ val registered_e_assumption : tactic
val e_give_exact : ?flags:Unification.unify_flags -> constr -> tactic
-val gen_eauto : bool -> bool * int -> open_constr list ->
+val gen_eauto : ?debug:Tacexpr.debug -> bool * int -> open_constr list ->
hint_db_name list option -> tactic
val eauto_with_bases :
- bool ->
+ ?debug:Tacexpr.debug ->
bool * int ->
open_constr list -> Auto.hint_db list -> Proof_type.tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 81c79f931..b55a9f01f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -175,8 +175,8 @@ let _ =
"intros", TacIntroPattern [];
"assumption", TacAssumption;
"cofix", TacCofix None;
- "trivial", TacTrivial ([],None);
- "auto", TacAuto(None,[],None);
+ "trivial", TacTrivial (Off,[],None);
+ "auto", TacAuto(Off,None,[],None);
"left", TacLeft(false,NoBindings);
"eleft", TacLeft(true,NoBindings);
"right", TacRight(false,NoBindings);
@@ -714,12 +714,12 @@ let rec intern_atomic lf ist x =
(clause_app (intern_hyp_location ist) cls),b)
(* Automation tactics *)
- | TacTrivial (lems,l) -> TacTrivial (List.map (intern_constr ist) lems,l)
- | TacAuto (n,lems,l) ->
- TacAuto (Option.map (intern_or_var ist) n,
+ | TacTrivial (d,lems,l) -> TacTrivial (d,List.map (intern_constr ist) lems,l)
+ | TacAuto (d,n,lems,l) ->
+ TacAuto (d,Option.map (intern_or_var ist) n,
List.map (intern_constr ist) lems,l)
- | TacDAuto (n,p,lems) ->
- TacDAuto (Option.map (intern_or_var ist) n,p,
+ | TacDAuto (d,n,p,lems) ->
+ TacDAuto (d,Option.map (intern_or_var ist) n,p,
List.map (intern_constr ist) lems)
(* Derived basic tactics *)
@@ -1785,14 +1785,6 @@ and eval_tactic ist = function
| TacDo (n,tac) -> tclDO (interp_int_or_var ist n) (interp_tactic ist tac)
| TacTimeout (n,tac) -> tclTIMEOUT (interp_int_or_var ist n) (interp_tactic ist tac)
| TacTry tac -> tclTRY (interp_tactic ist tac)
- | TacInfo tac ->
- let t = (interp_tactic ist tac) in
- tclINFO
- begin
- match tac with
- TacAtom (_,_) -> t
- | _ -> abstract_tactic_expr (TacArg (dloc,Tacexp tac)) t
- end
| TacRepeat tac -> tclREPEAT (interp_tactic ist tac)
| TacOrelse (tac1,tac2) ->
tclORELSE (interp_tactic ist tac1) (interp_tactic ist tac2)
@@ -1800,6 +1792,12 @@ and eval_tactic ist = function
| TacSolve l -> tclSOLVE (List.map (interp_tactic ist) l)
| TacComplete tac -> tclCOMPLETE (interp_tactic ist tac)
| TacArg a -> interp_tactic ist (TacArg a)
+ | TacInfo tac ->
+ msg_warning
+ (str "The general \"info\" tactic is currently not working.\n" ++
+ str "Some specific verbose tactics may exist instead, such as\n" ++
+ str "info_trivial, info_auto, info_eauto.");
+ eval_tactic ist tac
and force_vrec ist gl = function
| VRec (lfun,body) -> val_interp {ist with lfun = !lfun} gl body
@@ -2273,16 +2271,16 @@ and interp_atomic ist gl tac =
(interp_pure_open_constr ist env sigma c) clp
(* Automation tactics *)
- | TacTrivial (lems,l) ->
- Auto.h_trivial
+ | TacTrivial (debug,lems,l) ->
+ Auto.h_trivial ~debug
(interp_auto_lemmas ist env sigma lems)
(Option.map (List.map (interp_hint_base ist)) l)
- | TacAuto (n,lems,l) ->
- Auto.h_auto (Option.map (interp_int_or_var ist) n)
+ | TacAuto (debug,n,lems,l) ->
+ Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n)
(interp_auto_lemmas ist env sigma lems)
(Option.map (List.map (interp_hint_base ist)) l)
- | TacDAuto (n,p,lems) ->
- Auto.h_dauto (Option.map (interp_int_or_var ist) n,p)
+ | TacDAuto (debug,n,p,lems) ->
+ Auto.h_dauto ~debug (Option.map (interp_int_or_var ist) n,p)
(interp_auto_lemmas ist env sigma lems)
(* Derived basic tactics *)
@@ -2646,9 +2644,9 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
| TacLetTac (id,c,clp,b) -> TacLetTac (id,subst_glob_constr subst c,clp,b)
(* Automation tactics *)
- | TacTrivial (lems,l) -> TacTrivial (List.map (subst_glob_constr subst) lems,l)
- | TacAuto (n,lems,l) -> TacAuto (n,List.map (subst_glob_constr subst) lems,l)
- | TacDAuto (n,p,lems) -> TacDAuto (n,p,List.map (subst_glob_constr subst) lems)
+ | TacTrivial (d,lems,l) -> TacTrivial (d,List.map (subst_glob_constr subst) lems,l)
+ | TacAuto (d,n,lems,l) -> TacAuto (d,n,List.map (subst_glob_constr subst) lems,l)
+ | TacDAuto (d,n,p,lems) -> TacDAuto (d,n,p,List.map (subst_glob_constr subst) lems)
(* Derived basic tactics *)
| TacSimpleInductionDestruct (isrec,h) as x -> x
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 2bb9c1cbe..f7b8419c9 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -54,7 +54,6 @@ let tclREPEAT_MAIN = Refiner.tclREPEAT_MAIN
let tclFIRST = Refiner.tclFIRST
let tclSOLVE = Refiner.tclSOLVE
let tclTRY = Refiner.tclTRY
-let tclINFO = Refiner.tclINFO
let tclCOMPLETE = Refiner.tclCOMPLETE
let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE
let tclFAIL = Refiner.tclFAIL
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 42c70eef4..7c13894ec 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -46,7 +46,6 @@ val tclREPEAT_MAIN : tactic -> tactic
val tclFIRST : tactic list -> tactic
val tclSOLVE : tactic list -> tactic
val tclTRY : tactic -> tactic
-val tclINFO : tactic -> tactic
val tclCOMPLETE : tactic -> tactic
val tclAT_LEAST_ONCE : tactic -> tactic
val tclFAIL : int -> std_ppcmds -> tactic
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 00:24:14 +0000