info_trivial, info_auto, info_eauto, and debug (trivial|auto)

 To mitigate the lack of a general "info" tactical, let's
 introduce some specialized tactics info_trivial, info_auto
 and info_eauto that display the basic tactics used when
 solving a goal.

 We also add tactics "debug trivial" and "debug auto" which
 display every basic tactics attempted by trivial or auto.

 Triggering the "info" or "debug" mode for auto, eauto, trivial
 can also be done now via global options, such as Set Debug Auto
 or Set Info Eauto. In case both debug and info modes are
 activated, the debug mode takes precedence.

 NB: it would be nice to name these tactics "info xxx" instead
 of "info_xxx", but I don't see how to implement a "info eauto"
 in eauto.ml4 (hence by TACTIC EXTEND) while keeping
 a generic "info foo" tactic in g_ltac.ml4 (useful to display
 a nice message about the unavailability of the general info).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15103 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 45 insertions, 23 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 7dc166750c..ddff97128e 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 465d0b76a8..1e0f2aef2a 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 389118c346..df25972082 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"