diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-30 09:47:57 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-30 09:47:57 +0000 |
commit | 1e1b6828c29b1344f50f94f9d3a6fce27a885656 (patch) | |
tree | e0b7c5a490f8f650262d6a1457b5c64668bd76a2 /lib | |
parent | 534cbe4f02392c45567ea30d02b53751482ed767 (diff) |
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
Diffstat (limited to 'lib')
-rw-r--r-- | lib/explore.ml | 18 | ||||
-rw-r--r-- | lib/explore.mli | 2 | ||||
-rw-r--r-- | lib/pp.ml4 | 19 | ||||
-rw-r--r-- | lib/pp.mli | 3 |
4 files changed, 23 insertions, 19 deletions
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. } *) |