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

1 files changed, 145 insertions, 68 deletions

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 ()