blob: 422e58502d65cb9e9bf7a0dcb71d9c03aade1fbb (
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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
open Ast
open Names
open Constrextern
open Pp
open Pptactic
open Printer
open Tacexpr
open Termops
let pr_glob_tactic x =
(if !Options.v7 then pr_glob_tactic else Pptacticnew.pr_glob_tactic (Global.env())) x
(* 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())
(* Prints the goal *)
let db_pr_goal g =
msgnl (str "Goal:" ++ fnl () ++ Proof_trees.pr_goal (Tacmach.sig_it g))
(* Prints the commands *)
let help () =
msgnl (str "Commands: <Enter>=Continue" ++ fnl() ++
str " h/?=Help" ++ fnl() ++
str " r<num>=Run <num> times" ++ fnl() ++
str " s=Skip" ++ fnl() ++
str " x=Exit")
(* Prints the goal and the command to be executed *)
let goal_com g tac =
begin
db_pr_goal g;
msg (str "Going to execute:" ++ fnl () ++ pr_glob_tactic tac ++ fnl ())
end
(* Gives the number of a run command *)
let run_com inst =
if (String.get inst 0)='r' then
let num = int_of_string (String.sub inst 1 ((String.length inst)-1)) in
if num>0 then num
else raise (Invalid_argument "run_com")
else
raise (Invalid_argument "run_com")
let allskip = ref 0
let skip = ref 0
(* Prints the run counter *)
let run ini =
if not ini then
for i=1 to 2 do
print_char (Char.chr 8);print_char (Char.chr 13)
done;
msg (str "Executed expressions: " ++ int (!allskip - !skip) ++
fnl() ++ fnl())
(* Prints the prompt *)
let rec prompt level =
begin
msg (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ");
flush stdout;
let inst = read_line () in
match inst with
| "" -> true
| "s" -> false
| "x" -> print_char (Char.chr 8);skip:=0;allskip:=0;raise Sys.Break
| "h"| "?" ->
begin
help ();
prompt level
end
| _ ->
(try let ctr=run_com inst in skip:=ctr;allskip:=ctr;run true;true
with Failure _ | Invalid_argument _ -> prompt level)
end
(* Prints the state and waits for an instruction *)
let debug_prompt lev g tac f =
(* What to print and to do next *)
let continue =
if !skip = 0 then (goal_com g tac; prompt lev)
else (decr skip; run false; if !skip=0 then allskip:=0; true) in
(* What to execute *)
try f (if continue then DebugOn (lev+1) else DebugOff)
with e ->
skip:=0; allskip:=0;
if Logic.catchable_exception e then
ppnl (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error e);
raise e
(* Prints a constr *)
let db_constr debug env c =
if debug <> DebugOff & !skip = 0 then
msgnl (str "Evaluated term: " ++ prterm_env env c)
(* Prints the pattern rule *)
let db_pattern_rule debug num r =
if debug <> DebugOff & !skip = 0 then
begin
msgnl (str "Pattern rule " ++ int num ++ str ":");
msgnl (str "|" ++ spc () ++
pr_match_rule false Printer.pr_pattern pr_glob_tactic r)
end
(* Prints the hypothesis pattern identifier if it exists *)
let hyp_bound = function
| Anonymous -> " (unbound)"
| Name id -> " (bound to "^(Names.string_of_id id)^")"
(* Prints a matched hypothesis *)
let db_matched_hyp debug env (id,c) ido =
if debug <> DebugOff & !skip = 0 then
msgnl (str "Hypothesis " ++
str ((Names.string_of_id id)^(hyp_bound ido)^
" has been matched: ") ++ prterm_env env c)
(* Prints the matched conclusion *)
let db_matched_concl debug env c =
if debug <> DebugOff & !skip = 0 then
msgnl (str "Conclusion has been matched: " ++ prterm_env env c)
(* Prints a success message when the goal has been matched *)
let db_mc_pattern_success debug =
if debug <> DebugOff & !skip = 0 then
msgnl (str "The goal has been successfully matched!" ++ fnl() ++
str "Let us execute the right-hand side part..." ++ fnl())
let pp_match_pattern env = function
| Term c -> Term (extern_pattern env (names_of_rel_context env) c)
| Subterm (o,c) ->
Subterm (o,(extern_pattern env (names_of_rel_context env) c))
(* Prints a failure message for an hypothesis pattern *)
let db_hyp_pattern_failure debug env (na,hyp) =
if debug <> DebugOff & !skip = 0 then
msgnl (str ("The pattern hypothesis"^(hyp_bound na)^
" cannot match: ") ++
pr_match_pattern
(Printer.pr_pattern_env env (names_of_rel_context env))
hyp)
(* Prints a matching failure message for a rule *)
let db_matching_failure debug =
if debug <> DebugOff & !skip = 0 then
msgnl (str "This rule has failed due to matching errors!" ++ fnl() ++
str "Let us try the next one...")
(* Prints an evaluation failure message for a rule *)
let db_eval_failure debug s =
if debug <> DebugOff & !skip = 0 then
let s = if s="" then "no message" else "message \""^s^"\"" in
msgnl
(str "This rule has failed due to \"Fail\" tactic (" ++
str s ++ str ", level 0)!" ++ fnl() ++ str "Let us try the next one...")
(* Prints a logic failure message for a rule *)
let db_logic_failure debug err =
if debug <> DebugOff & !skip = 0 then
begin
msgnl (!explain_logic_error err);
msgnl (str "This rule has failed due to a logic error!" ++ fnl() ++
str "Let us try the next one...")
end
|
