aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/tactic_debug.ml
blob: e1c9fed637e8fe7c022cd7f907aef4aa8414cf05 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
(************************************************************************)
(*  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 e =
  CErrors.print (fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null)))

let explain_logic_error_no_anomaly e =
  CErrors.print_no_report
    (fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null)))

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 ": " ++ 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 (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) :: _ -> not (Tacenv.is_ltac_for_ml_tactic f)
  | (_, Tacexpr.LtacNotationCall f) :: _ -> true
  | (_, Tacexpr.LtacAtomCall _) :: _ -> 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 (Pptactic.pr_alias_key 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 ()
  | [a] -> hov 0 (str "Ltac call to " ++ pr_call a ++ str " failed.")
  | _ ->
    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 _ as tac) :: (_,Tacexpr.LtacMLCall _) :: _ ->
     (* Case of an ML defined tactic with entry of the form <<"foo" args>> *)
     (* see tacextend.mlp *)
     [tac]
  | (_,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 finer_loc loc1 loc2 = Loc.merge loc1 loc2 = loc2 in
    let best_loc =
      (* trace is with innermost call coming first *)
      let rec aux best_loc = function
        | (loc,_)::tail ->
           if Loc.is_ghost best_loc ||
              not (Loc.is_ghost loc) && finer_loc loc best_loc
           then
             aux loc tail
           else
             aux best_loc tail
        | [] -> best_loc in
        aux eloc trace in
    None, best_loc

let get_ltac_trace (_, info) =
  let ltac_trace = Exninfo.get info ltac_trace_info in
  let loc = Option.default Loc.ghost (Loc.get_loc info) in
  match ltac_trace with
  | None -> None
  | Some trace -> Some (extract_ltac_trace trace loc)

let () = ExplainErr.register_additional_error_info get_ltac_trace