Partial disentangling of Ltac codebase.

9 files changed, 504 insertions, 9 deletions

diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml
index 55463afd01..588709873e 100644
--- a/tactics/ftactic.ml
+++ b/tactics/ftactic.ml
@@ -99,8 +99,6 @@ end
 module Ftac = Monad.Make(Self)
 module List = Ftac.List
 
-let debug_prompt = Tactic_debug.debug_prompt
-
 module Notations =
 struct
   let (>>=) = bind
diff --git a/tactics/ftactic.mli b/tactics/ftactic.mli
index fd05a44698..19041f1698 100644
--- a/tactics/ftactic.mli
+++ b/tactics/ftactic.mli
@@ -70,11 +70,6 @@ val (<*>) : unit t -> 'a t -> 'a t
 
 module List : Monad.ListS with type 'a t := 'a t
 
-(** {5 Debug} *)
-
-val debug_prompt :
-  int -> Tacexpr.glob_tactic_expr -> (Tactic_debug.debug_info -> 'a t) -> 'a t
-
 (** {5 Notations} *)
 
 module Notations :
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4
index 72cfb01a57..6b6dc7b21a 100644
--- a/tactics/g_rewrite.ml4
+++ b/tactics/g_rewrite.ml4
@@ -261,3 +261,7 @@ TACTIC EXTEND setoid_transitivity
   [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity (Some t) ]
 | [ "setoid_etransitivity" ] -> [ setoid_transitivity None ]
 END
+
+VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY
+  [ "Print" "Rewrite" "HintDb" preident(s) ] -> [ Pp.msg_notice (Autorewrite.print_rewrite_hintdb s) ]
+END
diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib
index 0d73cc27aa..73f11d0be0 100644
--- a/tactics/hightactics.mllib
+++ b/tactics/hightactics.mllib
@@ -1,5 +1,6 @@
 Extraargs
 Coretactics
+Autorewrite
 Extratactics
 Eauto
 G_auto
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index bf5f9ddc86..32f7c3c61c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -44,6 +44,8 @@ open Sigma.Notations
 open Proofview.Notations
 open Context.Named.Declaration
 
+let ltac_trace_info = Tactic_debug.ltac_trace_info
+
 let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit ->
   let Val.Dyn (t, _) = v in
   match Val.eq t (val_tag wit) with
@@ -1200,7 +1202,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
           let ist = { ist with extra = TacStore.set ist.extra f_debug v } in
           value_interp ist >>= fun v -> return (name_vfun appl v)
         in
-	Ftactic.debug_prompt lev tac eval
+	Tactic_debug.debug_prompt lev tac eval
   | _ -> value_interp ist >>= fun v -> return (name_vfun appl v)
       
 
@@ -2199,3 +2201,16 @@ let lift_constr_tac_to_ml_tac vars tac =
     tac args ist
   end } in
   tac
+
+let vernac_debug b =
+  set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
+
+let _ =
+  let open Goptions in
+  declare_bool_option
+    { optsync  = false;
+      optdepr  = false;
+      optname  = "Ltac debug";
+      optkey   = ["Ltac";"Debug"];
+      optread  = (fun () -> get_debug () != Tactic_debug.DebugOff);
+      optwrite = vernac_debug }
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index c5da3494cb..31327873e9 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -14,6 +14,8 @@ open Genarg
 open Redexpr
 open Misctypes
 
+val ltac_trace_info : ltac_trace Exninfo.t
+
 module Value :
 sig
   type t = Val.t
diff --git a/tactics/tactic_debug.ml b/tactics/tactic_debug.ml
new file mode 100644
index 0000000000..e991eb86dc
--- /dev/null
+++ b/tactics/tactic_debug.ml
@@ -0,0 +1,400 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Util
+open Names
+open Pp
+open Tacexpr
+open Termops
+open Nameops
+open Proofview.Notations
+
+let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make ()
+
+let prtac x =
+  Pptactic.pr_glob_tactic (Global.env()) x
+let prmatchpatt env sigma hyp =
+  Pptactic.pr_match_pattern (Printer.pr_constr_pattern_env env sigma) hyp
+let prmatchrl rl =
+  Pptactic.pr_match_rule false (Pptactic.pr_glob_tactic (Global.env()))
+    (fun (_,p) -> Printer.pr_constr_pattern p) rl
+
+(* 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 *)
+
+(* Debug information *)
+type debug_info =
+  | DebugOn of int
+  | DebugOff
+
+(* An exception handler *)
+let explain_logic_error = ref (fun e -> mt())
+
+let explain_logic_error_no_anomaly = ref (fun e -> mt())
+
+let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl())
+let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl())
+
+(* Prints the goal *)
+
+let db_pr_goal gl =
+  let env = Proofview.Goal.env gl in
+  let concl = Proofview.Goal.concl gl in
+  let penv = print_named_context env in
+  let pc = print_constr_env env concl in
+    str"  " ++ hv 0 (penv ++ fnl () ++
+                   str "============================" ++ fnl ()  ++
+                   str" "  ++ pc) ++ fnl ()
+
+let db_pr_goal =
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  let pg = db_pr_goal gl in
+  Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg))
+  end }
+
+
+(* Prints the commands *)
+let help () =
+  msg_tac_debug (str "Commands: <Enter> = Continue" ++ fnl() ++
+         str "          h/? = Help" ++ fnl() ++
+         str "          r <num> = Run <num> times" ++ fnl() ++
+         str "          r <string> = Run up to next idtac <string>" ++ fnl() ++
+         str "          s = Skip" ++ fnl() ++
+         str "          x = Exit")
+
+(* Prints the goal and the command to be executed *)
+let goal_com tac =
+  Proofview.tclTHEN
+    db_pr_goal
+    (Proofview.tclLIFT (msg_tac_debug (str "Going to execute:" ++ fnl () ++ 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.ref 0)
+let skip = Proofview.NonLogical.run (Proofview.NonLogical.ref 0)
+let breakpoint = Proofview.NonLogical.run (Proofview.NonLogical.ref None)
+
+let rec drop_spaces inst i =
+  if String.length inst > i && inst.[i] == ' ' then drop_spaces inst (i+1)
+  else i
+
+let possibly_unquote s =
+  if String.length s >= 2 && s.[0] == '"' && s.[String.length s - 1] == '"' then
+    String.sub s 1 (String.length s - 2)
+  else
+    s
+
+(* (Re-)initialize debugger *)
+let db_initialize =
+  let open Proofview.NonLogical in
+  (skip:=0) >> (skipped:=0) >> (breakpoint:=None)
+
+let int_of_string s =
+  try Proofview.NonLogical.return (int_of_string s)
+  with e -> Proofview.NonLogical.raise e
+
+let string_get s i =
+  try Proofview.NonLogical.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 =
+  let open Proofview.NonLogical in
+  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
+        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
+      invalid_arg "run_com"
+  else
+    invalid_arg "run_com"
+
+(* Prints the run counter *)
+let run ini =
+  let open Proofview.NonLogical in
+  if not ini then
+    begin
+      Proofview.NonLogical.print_notice (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 =
+  (* spiwack: avoid overriding by the open below *)
+  let runtrue = run true in
+  begin
+    let open Proofview.NonLogical in
+    Proofview.NonLogical.print_notice (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 (e, info) -> match e with
+        | End_of_file -> exit
+        | e -> raise ~info e
+      end
+    >>= fun inst ->
+    match inst with
+    | ""  -> return (DebugOn (level+1))
+    | "s" -> return (DebugOff)
+    | "x" -> Proofview.NonLogical.print_char '\b' >> exit
+    | "h"| "?" ->
+      begin
+        help () >>
+        prompt level
+      end
+    | _ ->
+        Proofview.NonLogical.catch (run_com inst >> runtrue >> return (DebugOn (level+1)))
+          begin function (e, info) -> match e with
+            | Failure _ | Invalid_argument _ -> prompt level
+            | e -> raise ~info e
+          end
+  end
+
+(* Prints the state and waits for an instruction *)
+(* 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 =
+  (* spiwack: avoid overriding by the open below *)
+  let runfalse = run false in
+  let open Proofview.NonLogical in
+  let (>=) = Proofview.tclBIND in
+  (* What to print and to do next *)
+  let newlevel =
+    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(runfalse >> return (DebugOn (lev+1)))
+    else Proofview.tclLIFT begin
+      (!skip >>= fun s -> skip:=s-1) >>
+      runfalse >>
+      !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 *)
+  Proofview.tclOR
+    (f newlevel)
+    begin fun (reraise, info) ->
+      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 ~info reraise)
+    end
+
+let is_debug db =
+  let open Proofview.NonLogical in
+  !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 =
+  let open Proofview.NonLogical in
+  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 =
+  let open Proofview.NonLogical in
+  is_debug debug >>= fun db ->
+  if db then
+  begin
+    msg_tac_debug (str "Pattern rule " ++ int num ++ str ":" ++ fnl () ++
+      str "|" ++ spc () ++ prmatchrl r)
+  end
+  else return ()
+
+(* Prints the hypothesis pattern identifier if it exists *)
+let hyp_bound = function
+  | Anonymous -> str " (unbound)"
+  | Name id -> str " (bound to " ++ pr_id id ++ str ")"
+
+(* Prints a matched hypothesis *)
+let db_matched_hyp debug env (id,_,c) ido =
+  let open Proofview.NonLogical in
+  is_debug debug >>= fun db ->
+  if db then
+    msg_tac_debug (str "Hypothesis " ++ pr_id id ++ hyp_bound ido ++
+                str " has been matched: " ++ print_constr_env env c)
+  else return ()
+
+(* Prints the matched conclusion *)
+let db_matched_concl debug env c =
+  let open Proofview.NonLogical in
+  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 =
+  let open Proofview.NonLogical in
+  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 sigma (na,hyp) =
+  let open Proofview.NonLogical in
+  is_debug debug >>= fun db ->
+  if db then
+    msg_tac_debug (str "The pattern hypothesis" ++ hyp_bound na ++
+                str " cannot match: " ++
+           prmatchpatt env sigma hyp)
+  else return ()
+
+(* Prints a matching failure message for a rule *)
+let db_matching_failure debug =
+  let open Proofview.NonLogical in
+  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 =
+  let open Proofview.NonLogical in
+  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 =
+  let open Proofview.NonLogical in
+  is_debug debug >>= fun db ->
+  if db then
+  begin
+    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 =
+  let open Proofview.NonLogical in
+  !breakpoint >>= fun opt_breakpoint ->
+  match debug with
+  | DebugOn lev when not (CList.is_empty s) && is_breakpoint opt_breakpoint s ->
+      breakpoint:=None
+  | _ ->
+      return ()
+
+(** Extrating traces *)
+
+let is_defined_ltac trace =
+  let rec aux = function
+  | (_, Tacexpr.LtacNameCall f) :: tail ->
+      not (Tacenv.is_ltac_for_ml_tactic f)
+  | (_, Tacexpr.LtacAtomCall _) :: tail ->
+      false
+  | _ :: tail -> aux tail
+  | [] -> false in
+  aux (List.rev trace)
+
+let explain_ltac_call_trace last trace loc =
+  let calls = last :: List.rev_map snd trace in
+  let pr_call ck = match ck with
+  | Tacexpr.LtacNotationCall kn -> quote (KerName.print kn)
+  | Tacexpr.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst)
+  | Tacexpr.LtacMLCall t ->
+      quote (Pptactic.pr_glob_tactic (Global.env()) t)
+  | Tacexpr.LtacVarCall (id,t) ->
+      quote (Nameops.pr_id id) ++ strbrk " (bound to " ++
+        Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
+  | Tacexpr.LtacAtomCall te ->
+      quote (Pptactic.pr_glob_tactic (Global.env())
+              (Tacexpr.TacAtom (Loc.ghost,te)))
+  | Tacexpr.LtacConstrInterp (c, { Pretyping.ltac_constrs = vars }) ->
+      quote (Printer.pr_glob_constr_env (Global.env()) c) ++
+        (if not (Id.Map.is_empty vars) then
+          strbrk " (with " ++
+            prlist_with_sep pr_comma
+            (fun (id,c) ->
+                pr_id id ++ str ":=" ++ Printer.pr_lconstr_under_binders c)
+            (List.rev (Id.Map.bindings vars)) ++ str ")"
+        else mt())
+  in
+  match calls with
+  | [] -> mt ()
+  | _ ->
+    let kind_of_last_call = match List.last calls with
+    | Tacexpr.LtacConstrInterp _ -> ", last term evaluation failed."
+    | _ -> ", last call failed."
+    in
+    hov 0 (str "In nested Ltac calls to " ++
+           pr_enum pr_call calls ++ strbrk kind_of_last_call)
+
+let skip_extensions trace =
+  let rec aux = function
+  | (_,Tacexpr.LtacNameCall f as tac) :: _ 
+      when Tacenv.is_ltac_for_ml_tactic f -> [tac]
+  | (_,(Tacexpr.LtacNotationCall _ | Tacexpr.LtacMLCall _) as tac)
+      :: _ -> [tac]
+  | t :: tail -> t :: aux tail
+  | [] -> [] in
+  List.rev (aux (List.rev trace))
+
+let extract_ltac_trace trace eloc =
+  let trace = skip_extensions trace in
+  let (loc,c),tail = List.sep_last trace in
+  if is_defined_ltac trace then
+    (* We entered a user-defined tactic,
+       we display the trace with location of the call *)
+    let msg = hov 0 (explain_ltac_call_trace c tail eloc ++ fnl()) in
+    Some msg, loc
+  else
+    (* We entered a primitive tactic, we don't display trace but
+       report on the finest location *)
+    let best_loc =
+      if not (Loc.is_ghost eloc) then eloc else
+        (* trace is with innermost call coming first *)
+        let rec aux = function
+        | (loc,_)::tail when not (Loc.is_ghost loc) -> loc
+        | _::tail -> aux tail
+        | [] -> Loc.ghost in
+        aux trace in
+    None, best_loc
diff --git a/tactics/tactic_debug.mli b/tactics/tactic_debug.mli
new file mode 100644
index 0000000000..523398e75a
--- /dev/null
+++ b/tactics/tactic_debug.mli
@@ -0,0 +1,80 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Environ
+open Pattern
+open Names
+open Tacexpr
+open Term
+open Evd
+
+(** TODO: Move those definitions somewhere sensible *)
+
+val ltac_trace_info : ltac_trace Exninfo.t
+
+(** 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 *)
+
+(** Debug information *)
+type debug_info =
+  | DebugOn of int
+  | DebugOff
+
+(** Prints the state and waits *)
+val debug_prompt :
+  int -> glob_tactic_expr -> (debug_info -> 'a Proofview.tactic) -> 'a Proofview.tactic
+
+(** Initializes debugger *)
+val db_initialize : unit Proofview.NonLogical.t
+
+(** Prints a constr *)
+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 Proofview.NonLogical.t
+
+(** Prints a matched hypothesis *)
+val db_matched_hyp :
+  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 Proofview.NonLogical.t
+
+(** Prints a success message when the goal has been matched *)
+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 -> evar_map -> 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 Proofview.NonLogical.t
+
+(** Prints an evaluation failure message for a rule *)
+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
+
+(** For use in the Ltac debugger: some exception that are usually
+   consider anomalies are acceptable because they are caught later in
+   the process that is being debugged.  One should not require
+   from users that they report these anomalies. *)
+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 Proofview.NonLogical.t
+
+(** Prints a logic failure message for a rule *)
+val db_breakpoint : debug_info ->
+  Id.t Loc.located message_token list -> unit Proofview.NonLogical.t
+
+val extract_ltac_trace :
+  Tacexpr.ltac_trace -> Loc.t -> Pp.std_ppcmds option * Loc.t
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 2c5edc20ed..fd7fab0c58 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -21,8 +21,8 @@ Hints
 Auto
 Tacintern
 Tactic_matching
+Tactic_debug
 Tacinterp
 Evar_tactics
 Term_dnet
-Autorewrite
 Tactic_option