Makes the Ltac debugger usable again.

This is just a port of the existing design. Basing the tactics on an IO monad
may allow to simplify things a bit.

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

8 files changed, 351 insertions, 150 deletions

diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index 26583b0be5..c9cdfc2ad6 100644
--- a/bootstrap/Monads.v
+++ b/bootstrap/Monads.v
@@ -30,7 +30,6 @@ Extract Inductive prod => "(*)" [
 ].
 
 (*** Sum ***)
-Print sum.
 Extract Inductive sum => "Util.union" [
   "Util.Inl"
   "Util.Inr"
@@ -44,6 +43,26 @@ Extract Inlined Constant Exception => exn.
 Parameter tactic_failure : Exception -> Exception.
 Extract Inlined Constant tactic_failure => "(fun e -> Proof_errors.TacticFailure e)".
 
+(*** Basic integers ***)
+
+Parameter Int : Set.
+Extract Inlined Constant Int => int.
+
+(*** Char ***)
+
+Parameter Char : Set.
+Extract Inlined Constant Char => char.
+
+(*** Primitive strings ***)
+
+Parameter String : Set.
+Extract Inlined Constant String => string.
+
+(*** Pretty printer ***)
+
+Parameter Ppcmds : Set.
+Extract Inlined Constant Ppcmds => "Pp.std_ppcmds".
+
 (*** Monoids ***)
 
 Module Monoid.
@@ -162,8 +181,13 @@ Module IOBase.
  Extract Constant catch => "fun s h () -> try s () with Proof_errors.Exception e -> h e ()".
  Extraction Implicit catch [A].
 
- Parameter Int : Set.
- Extract Constant Int => int.
+ Parameter read_line : T String.
+ Extract Constant read_line => "fun () -> try Pervasives.read_line () with e -> raise e ()".
+ Parameter print_char : Char -> T unit.
+ Extract Constant print_char => "fun c () -> print_char c".
+ Parameter print : Ppcmds -> T unit.
+ Extract Constant print => "fun s () -> try Pp.pp s; Pp.pp_flush () with e -> raise e ()".
+
  Parameter timeout: forall A, Int -> T A -> T A.
  Extract Constant timeout => "fun n t () ->
     let timeout_handler _ = Pervasives.raise (Proof_errors.Exception Proof_errors.Timeout) in
@@ -193,9 +217,13 @@ Module IO.
    set : forall {A:Set}, Ref A -> A -> T unit;
    get : forall {A:Set}, Ref A -> T A;
 
+   read_line : T String;
+   print_char : Char -> T unit;
+   print : Ppcmds -> T unit;
+
    raise : forall {A:Set}, Exception -> T A;
    catch : forall {A:Set}, T A -> (Exception -> T A) -> T A;
-   timeout : forall {A:Set}, IOBase.Int -> T A -> T A
+   timeout : forall {A:Set}, Int -> T A -> T A
  }.
 
  Definition T : Set -> Set := IOBase.T.
@@ -213,6 +241,10 @@ Module IO.
    set := IOBase.set;
    get := IOBase.get;
 
+   read_line := IOBase.read_line;
+   print_char := IOBase.print_char;
+   print := IOBase.print;
+
    raise := IOBase.raise;
    catch := IOBase.catch;
    timeout := IOBase.timeout
@@ -550,6 +582,10 @@ Module NonLogical.
  Definition timeout {a:Set} n (x:t a) : t a := Eval compute in IO.timeout _ _ NonLogicalIO n x.
  Extraction Implicit timeout [a].
 
+ Definition read_line : t String := Eval compute in IO.read_line _ _ NonLogicalIO.
+ Definition print_char (c:Char) : t unit := Eval compute in IO.print_char _ _ NonLogicalIO c.
+ Definition print (s:Ppcmds) : t unit := Eval compute in IO.print _ _ NonLogicalIO s.
+
  (* /!\ The extracted code for [run] performs effects. /!\ *)
  Parameter run : forall a:Set, t a -> a.
  Extract Constant run => "fun x -> try x () with Proof_errors.Exception e -> Pervasives.raise e".
@@ -572,7 +608,6 @@ Module Logical.
 
  Definition set (s:LogicalState) : t unit := Eval compute in set _ _ LogicalStateM s.
  Definition get : t LogicalState := Eval compute in get _ _ LogicalStateM.
- Print Environment.lift.
  Definition put (m:LogicalMessageType) : t unit := Eval compute in State.lift _ _ LogicalMonadEnv (Environment.lift _ _ (put _ _ LogicalWriter m)).
  Definition current : t LogicalEnvironment := Eval compute in State.lift _ _ LogicalMonadEnv (current _ _ LogicalReader).
 
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 9496b51ea8..3e05b60f0d 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -575,3 +575,7 @@ module Goal = struct
   let hyps = lift Goal.hyps
   let env = lift Goal.env
 end
+
+module NonLogical = Proofview_monad.NonLogical
+
+let tclLIFT = Proofview_monad.Logical.lift
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 136a44332e..5caffa8bdc 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -290,3 +290,34 @@ module Goal : sig
   (* [lift Goal.env] *)
   val env : Environ.env glist tactic
 end
+
+
+module NonLogical : sig
+
+  type +'a t
+  type 'a ref
+
+  val ret : 'a -> 'a t
+  val bind : 'a t -> ('a -> 'b t) -> 'b t
+  val ignore : 'a t -> unit t
+  val seq : unit t -> 'a t -> 'a t
+
+  val new_ref : 'a -> 'a ref t
+  val set : 'a ref -> 'a -> unit t
+  val get : 'a ref -> 'a t
+
+  val read_line : string t
+  val print_char : char -> unit t
+  val print : Pp.std_ppcmds -> unit t
+
+  val raise : exn -> 'a t
+  val catch : 'a t -> (exn -> 'a t) -> 'a t
+  val timeout : int -> 'a t -> 'a t
+
+
+  (* [run] performs effects. *)
+  val run : 'a t -> 'a
+
+end
+
+val tclLIFT : 'a NonLogical.t -> 'a tactic
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index 577aa2ddb0..4220958700 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -57,10 +57,21 @@ module IOBase =
   
   let catch = fun s h () -> try s () with Proof_errors.Exception e -> h e ()
   
-  type coq_Int = int
+  (** val read_line : string coq_T **)
+  
+  let read_line = fun () -> try Pervasives.read_line () with e -> raise e ()
+  
+  (** val print_char : char -> unit coq_T **)
+  
+  let print_char = fun c () -> print_char c
+  
+  (** val print :
+      Pp.std_ppcmds -> unit coq_T **)
+  
+  let print = fun s () -> try Pp.pp s; Pp.pp_flush () with e -> raise e ()
   
   (** val timeout :
-      coq_Int -> 'a1 coq_T -> 'a1 coq_T **)
+      int -> 'a1 coq_T -> 'a1 coq_T **)
   
   let timeout = fun n t () ->
     let timeout_handler _ = Pervasives.raise (Proof_errors.Exception Proof_errors.Timeout) in
@@ -143,12 +154,26 @@ module NonLogical =
   let catch s h =
     IOBase.catch s h
   
-  (** val timeout :
-      IOBase.coq_Int -> 'a1 t -> 'a1 t **)
+  (** val timeout : int -> 'a1 t -> 'a1 t **)
   
   let timeout n x =
     IOBase.timeout n x
   
+  (** val read_line : string t **)
+  
+  let read_line =
+    IOBase.read_line
+  
+  (** val print_char : char -> unit t **)
+  
+  let print_char c =
+    IOBase.print_char c
+  
+  (** val print : Pp.std_ppcmds -> unit t **)
+  
+  let print s =
+    IOBase.print s
+  
   (** val run : 'a1 t -> 'a1 **)
   
   let run = fun x -> try x () with Proof_errors.Exception e -> Pervasives.raise e
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
index 02550aebc0..bdebe658c1 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -27,6 +27,10 @@ module NonLogical : sig
   val set : 'a ref -> 'a -> unit t
   val get : 'a ref -> 'a t
 
+  val read_line : string t
+  val print_char : char -> unit t
+  val print : Pp.std_ppcmds -> unit t
+
   val raise : exn -> 'a t
   val catch : 'a t -> (exn -> 'a t) -> 'a t
   val timeout : int -> 'a t -> 'a t
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 1b49f9ff85..dc48cfc3bc 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -16,6 +16,14 @@ let (prtac, tactic_printer) = Hook.make ()
 let (prmatchpatt, match_pattern_printer) = Hook.make ()
 let (prmatchrl, match_rule_printer) = Hook.make ()
 
+(* Notations *)
+let return = Proofview.NonLogical.ret
+let (>>=) = Proofview.NonLogical.bind
+let (>>) = Proofview.NonLogical.seq
+let (:=) = Proofview.NonLogical.set
+let (!) = Proofview.NonLogical.get
+let raise = Proofview.NonLogical.raise
+
 (* This module intends to be a beginning of debugger for tactic expressions.
    Currently, it is quite simple and we can hope to have, in the future, a more
    complete panel of commands dedicated to a proof assistant framework *)
@@ -30,20 +38,26 @@ let explain_logic_error = ref (fun e -> mt())
 
 let explain_logic_error_no_anomaly = ref (fun e -> mt())
 
-let msg_tac_debug s = Pp.ppnl s; Pp.pp_flush ()
+let msg_tac_debug s = Proofview.NonLogical.print (s++fnl())
 
 (* Prints the goal *)
 
-let db_pr_goal g =
-  let env = Refiner.pf_env g in
+let db_pr_goal =
+  let (>>=) = Goal.bind in
+  Goal.env >>= fun env ->
+  Goal.concl >>= fun concl ->
   let penv = print_named_context env in
-  let pc = print_constr_env env (Goal.V82.concl (Refiner.project g) (Refiner.sig_it g)) in
-  str"  " ++ hv 0 (penv ++ fnl () ++
+  let pc = print_constr_env env concl in
+  Goal.return begin
+    str"  " ++ hv 0 (penv ++ fnl () ++
                    str "============================" ++ fnl ()  ++
                    str" "  ++ pc) ++ fnl ()
+  end
 
-let db_pr_goal g =
-  msg_tac_debug (str "Goal:" ++ fnl () ++ db_pr_goal g)
+let db_pr_goal =
+  let (>>=) = Proofview.Notations.(>>=) in
+  Proofview.Goal.lift db_pr_goal >>= fun pg ->
+  Proofview.tclLIFT (msg_tac_debug (str "Goal:" ++ fnl () ++ pg))
 
 
 (* Prints the commands *)
@@ -56,15 +70,17 @@ let help () =
          str "          x = Exit")
 
 (* Prints the goal and the command to be executed *)
-let goal_com g tac =
-  begin
-    db_pr_goal g;
-    msg_tac_debug (str "Going to execute:" ++ fnl () ++ Hook.get prtac tac)
-  end
-
-let skipped = ref 0
-let skip = ref 0
-let breakpoint = ref None
+let goal_com tac =
+  Proofview.tclTHEN
+    db_pr_goal
+    (Proofview.tclLIFT (msg_tac_debug (str "Going to execute:" ++ fnl () ++ Hook.get prtac tac)))
+
+(* [run (new_ref _)] gives us a ref shared among [NonLogical.t]
+   expressions. It avoids parametrizing everything over a
+   reference. *)
+let skipped = Proofview.NonLogical.run (Proofview.NonLogical.new_ref 0)
+let skip = Proofview.NonLogical.run (Proofview.NonLogical.new_ref 0)
+let breakpoint = Proofview.NonLogical.run (Proofview.NonLogical.new_ref None)
 
 let rec drop_spaces inst i =
   if String.length inst > i && inst.[i] == ' ' then drop_spaces inst (i+1)
@@ -77,19 +93,28 @@ let possibly_unquote s =
     s
 
 (* (Re-)initialize debugger *)
-let db_initialize () =
-  skip:=0;skipped:=0;breakpoint:=None
+let db_initialize =
+  (skip:=0) >> (skipped:=0) >> (breakpoint:=None)
+
+let int_of_string s =
+  try return (int_of_string s)
+  with e -> Proofview.NonLogical.raise e
+
+let string_get s i =
+  try return (String.get s i)
+  with e -> Proofview.NonLogical.raise e
 
 (* Gives the number of steps or next breakpoint of a run command *)
 let run_com inst =
-  if (String.get inst 0) == 'r' then
+  string_get inst 0 >>= fun first_char ->
+  if first_char ='r' then
     let i = drop_spaces inst 1 in
     if String.length inst > i then
       let s = String.sub inst i (String.length inst - i) in
       if inst.[0] >= '0' && inst.[0] <= '9' then
-        let num = int_of_string s in
-        if num<0 then invalid_arg "run_com";
-        skip:=num;skipped:=0
+        int_of_string s >>= fun num ->
+        (if num<0 then invalid_arg "run_com" else return ()) >>
+        (skip:=num) >> (skipped:=0)
       else
         breakpoint:=Some (possibly_unquote s)
     else
@@ -100,69 +125,106 @@ let run_com inst =
 (* Prints the run counter *)
 let run ini =
   if not ini then
-  begin
-    for _i = 1 to 2 do
-      print_char (Char.chr 8);print_char (Char.chr 13)
-    done;
-    msg_tac_debug (str "Executed expressions: " ++ int !skipped ++ fnl())
-  end;
-  incr skipped
+    begin
+      Proofview.NonLogical.print (str"\b\r\b\r") >>
+      !skipped >>= fun skipped ->
+      msg_tac_debug (str "Executed expressions: " ++ int skipped ++ fnl())
+    end >>
+    !skipped >>= fun x ->
+    skipped := x+1
+  else
+    return ()
 
 (* Prints the prompt *)
 let rec prompt level =
   begin
-    pp (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ");
-    flush stdout;
-    let exit () = skip:=0;skipped:=0;raise Sys.Break in
-    let inst = try read_line () with End_of_file -> exit () in
+    Proofview.NonLogical.print (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >>
+    let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in
+    Proofview.NonLogical.catch Proofview.NonLogical.read_line
+      begin function
+        | End_of_file -> exit
+        | e -> raise e
+      end
+    >>= fun inst ->
     match inst with
-    | ""  -> DebugOn (level+1)
-    | "s" -> DebugOff
-    | "x" -> print_char (Char.chr 8); exit ()
+    | ""  -> return (DebugOn (level+1))
+    | "s" -> return (DebugOff)
+    | "x" -> Proofview.NonLogical.print_char '\b' >> exit
     | "h"| "?" ->
       begin
-        help ();
+        help () >>
         prompt level
       end
     | _ ->
-      (try run_com inst;run true;DebugOn (level+1)
-       with Failure _ | Invalid_argument _ -> prompt level)
+        Proofview.NonLogical.catch (run_com inst >> run true >> return (DebugOn (level+1)))
+          begin function
+            | Failure _ | Invalid_argument _ -> prompt level
+            | e -> raise e
+          end
   end
 
 (* Prints the state and waits for an instruction *)
-let debug_prompt lev g tac f =
+(* spiwack: the only reason why we need to take the continuation [f]
+   as an argument rather than returning the new level directly seems to
+   be that [f] is wrapped in with "explain_logic_error". I don't think
+   it serves any purpose in the current design, so we could just drop
+   that. *)
+let debug_prompt lev tac f =
+  let (>=) = Proofview.tclBIND in
   (* What to print and to do next *)
   let newlevel =
-    if Int.equal !skip 0 then
-      if Option.is_empty !breakpoint then (goal_com g tac; prompt lev)
-      else (run false; DebugOn (lev+1))
-    else (decr skip; run false; if Int.equal !skip 0 then skipped:=0; DebugOn (lev+1)) in
+    Proofview.tclLIFT !skip >= fun initial_skip ->
+    if Int.equal initial_skip 0 then
+      Proofview.tclLIFT !breakpoint >= fun breakpoint ->
+      if Option.is_empty breakpoint then Proofview.tclTHEN (goal_com tac) (Proofview.tclLIFT (prompt lev))
+      else Proofview.tclLIFT(run false >> return (DebugOn (lev+1)))
+    else Proofview.tclLIFT begin
+      (!skip >>= fun s -> skip:=s-1) >>
+      run false >>
+      !skip >>= fun new_skip ->
+      (if Int.equal new_skip 0 then skipped:=0 else return ()) >>
+      return (DebugOn (lev+1))
+    end in
+  newlevel >= fun newlevel ->
   (* What to execute *)
-  try f newlevel
-  with reraise ->
-    skip:=0; skipped:=0;
-    if Logic.catchable_exception reraise then
-      msg_tac_debug
-        (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error reraise);
-    raise reraise
-
-let is_debug db = match db, !breakpoint with
-| DebugOff, _ -> false
-| _, Some _ -> false
-| _ -> Int.equal !skip 0
+  Proofview.tclOR
+    (f newlevel)
+    begin fun reraise ->
+      Proofview.tclTHEN
+        (Proofview.tclLIFT begin
+          (skip:=0) >> (skipped:=0) >>
+            if Logic.catchable_exception reraise then
+              msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ Pervasives.(!) explain_logic_error reraise)
+            else return ()
+        end)
+        (Proofview.tclZERO reraise)
+    end
+
+let is_debug db =
+  !breakpoint >>= fun breakpoint ->
+  match db, breakpoint with
+  | DebugOff, _ -> return false
+  | _, Some _ -> return false
+  | _ ->
+      !skip >>= fun skip ->
+      return (Int.equal skip 0)
 
 (* Prints a constr *)
 let db_constr debug env c =
-  if is_debug debug then
+  is_debug debug >>= fun db ->
+  if db then
     msg_tac_debug (str "Evaluated term: " ++ print_constr_env env c)
+  else return ()
 
 (* Prints the pattern rule *)
 let db_pattern_rule debug num r =
-  if is_debug debug then
+  is_debug debug >>= fun db ->
+  if db then
   begin
     msg_tac_debug (str "Pattern rule " ++ int num ++ str ":" ++ fnl () ++
       str "|" ++ spc () ++ Hook.get prmatchrl r)
   end
+  else return ()
 
 (* Prints the hypothesis pattern identifier if it exists *)
 let hyp_bound = function
@@ -171,59 +233,74 @@ let hyp_bound = function
 
 (* Prints a matched hypothesis *)
 let db_matched_hyp debug env (id,_,c) ido =
-  if is_debug debug then
+  is_debug debug >>= fun db ->
+  if db then
     msg_tac_debug (str "Hypothesis " ++
            str ((Names.Id.to_string id)^(hyp_bound ido)^
                 " has been matched: ") ++ print_constr_env env c)
+  else return ()
 
 (* Prints the matched conclusion *)
 let db_matched_concl debug env c =
-  if is_debug debug then
+  is_debug debug >>= fun db ->
+  if db then
     msg_tac_debug (str "Conclusion has been matched: " ++ print_constr_env env c)
+  else return ()
 
 (* Prints a success message when the goal has been matched *)
 let db_mc_pattern_success debug =
-  if is_debug debug then
+  is_debug debug >>= fun db ->
+  if db then
     msg_tac_debug (str "The goal has been successfully matched!" ++ fnl() ++
            str "Let us execute the right-hand side part..." ++ fnl())
+  else return ()
 
 (* Prints a failure message for an hypothesis pattern *)
 let db_hyp_pattern_failure debug env (na,hyp) =
-  if is_debug debug then
+  is_debug debug >>= fun db ->
+  if db then
     msg_tac_debug (str ("The pattern hypothesis"^(hyp_bound na)^
                 " cannot match: ") ++
            Hook.get prmatchpatt env hyp)
+  else return ()
 
 (* Prints a matching failure message for a rule *)
 let db_matching_failure debug =
-  if is_debug debug then
+  is_debug debug >>= fun db ->
+  if db then
     msg_tac_debug (str "This rule has failed due to matching errors!" ++ fnl() ++
            str "Let us try the next one...")
+  else return ()
 
 (* Prints an evaluation failure message for a rule *)
 let db_eval_failure debug s =
-  if is_debug debug then
+  is_debug debug >>= fun db ->
+  if db then
     let s = str "message \"" ++ s ++ str "\"" in
     msg_tac_debug
       (str "This rule has failed due to \"Fail\" tactic (" ++
        s ++ str ", level 0)!" ++ fnl() ++ str "Let us try the next one...")
+  else return ()
 
 (* Prints a logic failure message for a rule *)
 let db_logic_failure debug err =
-  if is_debug debug then
+  is_debug debug >>= fun db ->
+  if db then
   begin
-    msg_tac_debug (!explain_logic_error err);
+    msg_tac_debug (Pervasives.(!) explain_logic_error err) >>
     msg_tac_debug (str "This rule has failed due to a logic error!" ++ fnl() ++
            str "Let us try the next one...")
   end
+  else return ()
 
 let is_breakpoint brkname s = match brkname, s with
   | Some s, MsgString s'::_ -> String.equal s s'
   | _ -> false
 
 let db_breakpoint debug s =
+  !breakpoint >>= fun opt_breakpoint ->
   match debug with
-  | DebugOn lev when not (List.is_empty s) && is_breakpoint !breakpoint s ->
+  | DebugOn lev when not (List.is_empty s) && is_breakpoint opt_breakpoint s ->
       breakpoint:=None
   | _ ->
-      ()
+      return ()
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 3b9858f16e..1ae1a3905c 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -31,37 +31,37 @@ type debug_info =
 
 (** Prints the state and waits *)
 val debug_prompt :
-  int -> goal sigma -> glob_tactic_expr -> (debug_info -> 'a) -> 'a
+  int -> glob_tactic_expr -> (debug_info -> 'a Proofview.tactic) -> 'a Proofview.tactic
 
 (** Initializes debugger *)
-val db_initialize : unit -> unit
+val db_initialize : unit Proofview.NonLogical.t
 
 (** Prints a constr *)
-val db_constr : debug_info -> env -> constr -> unit
+val db_constr : debug_info -> env -> constr -> unit Proofview.NonLogical.t
 
 (** Prints the pattern rule *)
 val db_pattern_rule :
-  debug_info -> int -> (Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit
+  debug_info -> int -> (Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t
 
 (** Prints a matched hypothesis *)
 val db_matched_hyp :
-  debug_info -> env -> Id.t * constr option * constr -> Name.t -> unit
+  debug_info -> env -> Id.t * constr option * constr -> Name.t -> unit Proofview.NonLogical.t
 
 (** Prints the matched conclusion *)
-val db_matched_concl : debug_info -> env -> constr -> unit
+val db_matched_concl : debug_info -> env -> constr -> unit Proofview.NonLogical.t
 
 (** Prints a success message when the goal has been matched *)
-val db_mc_pattern_success : debug_info -> unit
+val db_mc_pattern_success : debug_info -> unit Proofview.NonLogical.t
 
 (** Prints a failure message for an hypothesis pattern *)
 val db_hyp_pattern_failure :
-  debug_info -> env -> Name.t * constr_pattern match_pattern -> unit
+  debug_info -> env -> Name.t * constr_pattern match_pattern -> unit Proofview.NonLogical.t
 
 (** Prints a matching failure message for a rule *)
-val db_matching_failure : debug_info -> unit
+val db_matching_failure : debug_info -> unit Proofview.NonLogical.t
 
 (** Prints an evaluation failure message for a rule *)
-val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit
+val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit Proofview.NonLogical.t
 
 (** An exception handler *)
 val explain_logic_error: (exn -> Pp.std_ppcmds) ref
@@ -73,8 +73,8 @@ val explain_logic_error: (exn -> Pp.std_ppcmds) ref
 val explain_logic_error_no_anomaly : (exn -> Pp.std_ppcmds) ref
 
 (** Prints a logic failure message for a rule *)
-val db_logic_failure : debug_info -> exn -> unit
+val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t
 
 (** Prints a logic failure message for a rule *)
 val db_breakpoint : debug_info ->
-  Id.t Loc.located message_token list -> unit
+  Id.t Loc.located message_token list -> unit Proofview.NonLogical.t
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 73fb292ed8..668b47e16e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -46,11 +46,9 @@ open Taccoerce
 open Proofview.Notations
 
 let safe_msgnl s =
-  let _ =
-    try ppnl s with any ->
-    ppnl (str "bug in the debugger: an exception is raised while printing debug information")
-  in
-  pp_flush () 
+  Proofview.NonLogical.catch
+    (Proofview.NonLogical.print (s++fnl()))
+    (fun _ -> Proofview.NonLogical.print (str "bug in the debugger: an exception is raised while printing debug information"++fnl()))
 
 type value = tlevel generic_argument
 
@@ -309,7 +307,7 @@ let get_debug () = !debug
 let debugging_step ist pp = match curr_debug ist with
   | DebugOn lev ->
       safe_msgnl (str "Level " ++ int lev ++ str": " ++ pp () ++ fnl())
-  | _ -> ()
+  | _ -> Proofview.NonLogical.ret ()
 
 let debugging_exception_step ist signal_anomaly e pp =
   let explain_exc =
@@ -525,7 +523,10 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
   let (evd,c) =
     catch_error trace (understand_ltac flags sigma env vars kind) c
   in
-  db_constr (curr_debug ist) env c;
+  (* spiwack: to avoid unnecessary modifications of tacinterp, as this
+     function already use effect, I call [run] hoping it doesn't mess
+     up with any assumption. *)
+  Proofview.NonLogical.run (db_constr (curr_debug ist) env c);
   (evd,c)
 
 let constr_flags = {
@@ -692,8 +693,11 @@ let interp_may_eval f ist gl = function
 	f ist gl c
      with reraise ->
        let reraise = Errors.push reraise in
-       debugging_exception_step ist false reraise (fun () ->
-         str"interpretation of term " ++ pr_glob_constr_env (pf_env gl) (fst c));
+       (* spiwack: to avoid unnecessary modifications of tacinterp, as this
+          function already use effect, I call [run] hoping it doesn't mess
+          up with any assumption. *)
+       Proofview.NonLogical.run (debugging_exception_step ist false reraise (fun () ->
+         str"interpretation of term " ++ pr_glob_constr_env (pf_env gl) (fst c)));
        raise reraise
 
 (* Interprets a constr expression possibly to first evaluate *)
@@ -703,12 +707,17 @@ let interp_constr_may_eval ist gl c =
       interp_may_eval pf_interp_constr ist gl c
     with reraise ->
       let reraise = Errors.push reraise in
-      debugging_exception_step ist false reraise
-        (fun () -> str"evaluation of term");
+      (* spiwack: to avoid unnecessary modifications of tacinterp, as this
+          function already use effect, I call [run] hoping it doesn't mess
+          up with any assumption. *)
+       Proofview.NonLogical.run (debugging_exception_step ist false reraise (fun () -> str"evaluation of term"));
       raise reraise
   in
   begin
-    db_constr (curr_debug ist) (pf_env gl) csr;
+    (* spiwack: to avoid unnecessary modifications of tacinterp, as this
+       function already use effect, I call [run] hoping it doesn't mess
+       up with any assumption. *)
+    Proofview.NonLogical.run (db_constr (curr_debug ist) (pf_env gl) csr);
     sigma , csr
   end
 
@@ -1083,10 +1092,12 @@ let rec val_interp ist (tac:glob_tactic_expr) : typed_generic_argument Proofview
     (Proofview.Goal.return (of_tacvalue v))
   in check_for_interrupt ();
   match curr_debug ist with
-      (* arnaud: todo: debug
   | DebugOn lev ->
-      debug_prompt lev gl tac (fun v -> value_interp {ist with debug=v})
-      *)
+        let eval v =
+          let ist = { ist with extra = TacStore.set ist.extra f_debug v } in
+          value_interp ist
+        in
+	debug_prompt lev tac eval
   | _ -> value_interp ist
       
 
@@ -1096,10 +1107,12 @@ and eval_tactic ist = function
       catch_error_tac (push_trace(loc,call) ist) (interp_atomic ist t)
   | TacFun _ | TacLetIn _ -> assert false
   | TacMatchGoal _ | TacMatch _ -> assert false
-  | TacId s -> Proofview.V82.tactic begin fun gl ->
-    let res = tclIDTAC_MESSAGE (interp_message_nl ist gl s) gl in
-    db_breakpoint (curr_debug ist) s; res
-  end
+  | TacId s ->
+      Proofview.tclTHEN
+        (Proofview.V82.tactic begin fun gl ->
+          tclIDTAC_MESSAGE (interp_message_nl ist gl s) gl
+        end)
+        (Proofview.tclLIFT (db_breakpoint (curr_debug ist) s))
   | TacFail (n,s) ->
       Proofview.V82.tactic begin fun gl ->
         tclFAIL (interp_int_or_var ist n) (interp_message ist gl s) gl
@@ -1241,17 +1254,18 @@ and interp_app loc ist fv largs =
                  it's intended to, or anything meaningful for that
                  matter. *)
               let e = Errors.push e in
-              (* arnaud: todo: debugging: debugging_exception_step ist false e (fun () -> str "evaluation"); *)
+              Proofview.tclLIFT (debugging_exception_step ist false e (fun () -> str "evaluation")) <*>
 	      Proofview.tclZERO e
             end
         end >>== fun v ->
-        (* arnaud: todo: debugging:
-          (* No errors happened, we propagate the trace *)
-          let v = append_trace trace v in
-        debugging_step ist
-	  (fun () ->
-	    str"evaluation returns"++fnl()++pr_value (Some (pf_env gl)) v);
-        *)
+        (* No errors happened, we propagate the trace *)
+        let v = append_trace trace v in
+        Proofview.Goal.env >>== fun env ->
+        Proofview.tclLIFT begin
+          debugging_step ist
+	    (fun () ->
+	      str"evaluation returns"++fnl()++pr_value (Some env) v)
+        end <*>
         if List.is_empty lval then (Proofview.Goal.return v) else interp_app loc ist v lval
       else
         Proofview.Goal.return (of_tacvalue (VFun(trace,newlfun,lvar,body)))
@@ -1344,14 +1358,14 @@ and interp_match_goal ist lz lr lmr =
     match_next_pattern (match_subterm_gen app c csr) in
   let rec apply_match_goal ist env nrs lex lpt =
     begin
-      let () = match lex with
-      | r :: _ -> db_pattern_rule (curr_debug ist) nrs r
-      | _ -> ()
-      in
+      begin match lex with
+      | r :: _ -> Proofview.tclLIFT (db_pattern_rule (curr_debug ist) nrs r)
+      | _ -> Proofview.tclUNIT ()
+      end <*>
       match lpt with
       | (All t)::tl ->
 	  begin
-            db_mc_pattern_success (curr_debug ist);
+            Proofview.tclLIFT (db_mc_pattern_success (curr_debug ist)) <*>
             Proofview.tclORELSE (eval_with_fail ist lz t)
               begin function
                 | e when is_match_catchable e ->
@@ -1369,20 +1383,20 @@ and interp_match_goal ist lz lr lmr =
               in
                             begin match matches with
               | None ->
-                db_matching_failure (curr_debug ist);
+                Proofview.tclLIFT (db_matching_failure (curr_debug ist)) <*>
                 apply_match_goal ist env (nrs+1) (List.tl lex) tl
               | Some lmatch ->
                 Proofview.tclORELSE
                   begin
-                    db_matched_concl (curr_debug ist) env concl;
+                    Proofview.tclLIFT (db_matched_concl (curr_debug ist) env concl) <*>
                     apply_hyps_context ist env lz mt Id.Map.empty lmatch mhyps hyps
                   end
                  begin function
                    | e when is_match_catchable e ->
-                       ((match e with
+                       (Proofview.tclLIFT (match e with
                        | PatternMatchingFailure -> db_matching_failure (curr_debug ist)
                        | Eval_fail s -> db_eval_failure (curr_debug ist) s
-                       | _ -> db_logic_failure (curr_debug ist) e);
+                       | _ -> db_logic_failure (curr_debug ist) e) <*>
                         apply_match_goal ist env (nrs+1) (List.tl lex) tl)
                    | e -> Proofview.tclZERO e
                  end
@@ -1421,11 +1435,11 @@ and apply_hyps_context ist env lz mt lctxt lgmatch mhyps hyps =
 	in
         let rec match_next_pattern next = match IStream.peek next with
         | None ->
-          db_hyp_pattern_failure (curr_debug ist) env (hypname, pat);
+          Proofview.tclLIFT (db_hyp_pattern_failure (curr_debug ist) env (hypname, pat)) <*>
           Proofview.tclZERO PatternMatchingFailure
         | Some (s, next) ->
           let lids, hyp_match = s.e_ctx in
-          db_matched_hyp (curr_debug ist) env hyp_match hypname;
+          Proofview.tclLIFT (db_matched_hyp (curr_debug ist) env hyp_match hypname) <*>
           Proofview.tclORELSE
             begin
               let id_match = pi1 hyp_match in
@@ -1446,8 +1460,8 @@ and apply_hyps_context ist env lz mt lctxt lgmatch mhyps hyps =
     | [] ->
         let lfun = lfun +++ ist.lfun in
         let lfun = extend_values_with_bindings lmatch lfun in
-        db_mc_pattern_success (curr_debug ist);
-        eval_with_fail {ist with lfun } lz mt
+        Proofview.tclLIFT (db_mc_pattern_success (curr_debug ist)) <*>
+        eval_with_fail {ist with lfun=lfun} lz mt
   in
   apply_hyps_context_rec lctxt lgmatch hyps mhyps
 
@@ -1564,7 +1578,13 @@ and interp_match ist lz constr lmr =
           with PatternMatchingFailure -> None
         in
         Proofview.tclORELSE begin match matches with
-        | None -> Proofview.tclZERO PatternMatchingFailure
+        | None -> let e = PatternMatchingFailure in
+                  (Proofview.Goal.env >>= fun env ->
+                  Proofview.tclLIFT begin
+                    debugging_exception_step ist false e (fun () ->
+                      str "matching with pattern" ++ fnl () ++
+                        pr_constr_pattern_env env c)
+                  end) <*> Proofview.tclZERO e
         | Some lmatch ->
            Proofview.tclORELSE
              begin
@@ -1573,16 +1593,18 @@ and interp_match ist lz constr lmr =
              end
              begin function
                | e ->
-                   (* arnaud: todo: debugging
+                   (Proofview.Goal.env >>= fun env ->
+                    Proofview.tclLIFT begin
                       debugging_exception_step ist false e (fun () ->
-                      str "rule body for pattern" ++
-                      pr_constr_pattern_env (pf_env g) c);*)
+                        str "rule body for pattern" ++
+                          pr_constr_pattern_env env c)
+                    end) <*>
                    Proofview.tclZERO e
              end
         end
         begin function 
           | e when is_match_catchable e ->
-              debugging_step ist (fun () -> str "switching to the next rule");
+              Proofview.tclLIFT (debugging_step ist (fun () -> str "switching to the next rule")) <*>
               apply_match ist csr tl
           | e -> Proofview.tclZERO e
         end
@@ -1605,8 +1627,8 @@ and interp_match ist lz constr lmr =
              it's intended to, or anything meaningful for that
              matter. *)
           let e = Errors.push e in
-          debugging_exception_step ist true e
-            (fun () -> str "evaluation of the matched expression");
+          Proofview.tclLIFT (debugging_exception_step ist true e
+          (fun () -> str "evaluation of the matched expression")) <*>
           Proofview.tclZERO e
     end
   end >>== fun csr ->
@@ -1617,11 +1639,11 @@ and interp_match ist lz constr lmr =
     (apply_match ist csr ilr)
     begin function
       | e ->
-          debugging_exception_step ist true e (fun () -> str "match expression");
+          Proofview.tclLIFT (debugging_exception_step ist true e (fun () -> str "match expression")) <*>
           Proofview.tclZERO e
     end >>== fun res ->
-  debugging_step ist (fun () ->
-    str "match expression returns " ++ pr_value (Some env) res);
+  Proofview.tclLIFT (debugging_step ist (fun () ->
+    str "match expression returns " ++ pr_value (Some env) res)) <*>
   (Proofview.Goal.return res)
 
 (* Interprets tactic expressions : returns a "constr" *)
@@ -1630,11 +1652,12 @@ and interp_ltac_constr ist e =
       (val_interp ist e)
       begin function
         | Not_found ->
-            (* arnaud: todo: debugging
-            debugging_step ist (fun () ->
-              str "evaluation failed for" ++ fnl() ++
-                Pptactic.pr_glob_tactic (pf_env gl) e);
-            *)
+            (Proofview.Goal.env >>= fun env ->
+            Proofview.tclLIFT begin
+              debugging_step ist (fun () ->
+                str "evaluation failed for" ++ fnl() ++
+                  Pptactic.pr_glob_tactic env e)
+            end) <*>
             Proofview.tclZERO Not_found
         | e -> Proofview.tclZERO e
       end
@@ -1643,10 +1666,12 @@ and interp_ltac_constr ist e =
   let result = Value.normalize result in
   try
     let cresult = coerce_to_closed_constr env result in
-    debugging_step ist (fun () ->
-      Pptactic.pr_glob_tactic env e ++ fnl() ++
-        str " has value " ++ fnl() ++
-        pr_constr_env env cresult);
+    Proofview.tclLIFT begin
+      debugging_step ist (fun () ->
+        Pptactic.pr_glob_tactic env e ++ fnl() ++
+          str " has value " ++ fnl() ++
+          pr_constr_env env cresult)
+    end <*>
     (Proofview.Goal.return cresult)
   with CannotCoerceTo _ ->
     Proofview.Goal.env >>== fun env ->
@@ -2177,8 +2202,8 @@ let default_ist () =
   { lfun = Id.Map.empty; extra = extra }
 
 let eval_tactic t =
-  Proofview.tclUNIT () >= fun () -> (* delay for [db_initialize] and [default_ist] *)
-  db_initialize ();
+  Proofview.tclUNIT () >= fun () -> (* delay for [default_ist] *)
+  Proofview.tclLIFT db_initialize <*>
   interp_tactic (default_ist ()) t
 
 (* globalization + interpretation *)