blob: 08446d0112f64bb29f06962f1123012255265653 (
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
|
(***********************************************************************)
(* 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 Pp
open Printer
(* 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
| DebugOff
| Exit
(* Prints the goal if it exists *)
let db_pr_goal = function
| None -> mSGNL [< 'sTR "No goal" >]
| Some g ->
mSGNL [<'sTR ("Goal:"); 'fNL; Proof_trees.pr_goal (Tacmach.sig_it g) >]
(* Prints the commands *)
let help () =
mSGNL [< 'sTR "Commands: <Enter>=Continue, h=Help, s=Skip, x=Exit" >]
(* Prints the state and waits for an instruction *)
let debug_prompt goalopt tac_ast =
db_pr_goal goalopt;
mSG [< 'sTR "Going to execute:"; 'fNL; (gentacpr tac_ast); 'fNL >];
(* 'sTR "Commands: <Enter>=Continue, s=Skip, x=Exit" >];*)
(* mSG [< 'sTR "Going to execute:"; 'fNL; (gentacpr tac_ast); 'fNL; 'fNL;
'sTR "----<Enter>=Continue----s=Skip----x=Exit----" >];*)
let rec prompt () =
mSG [<'fNL; 'sTR "TcDebug > " >];
flush stdout;
let inst = read_line () in
(* mSGNL [<>];*)
match inst with
| "" -> DebugOn
| "s" -> DebugOff
| "x" -> Exit
| "h" ->
begin
help ();
prompt ()
end
| _ -> prompt () in
prompt ()
(* Prints a constr *)
let db_constr debug env c =
if debug = DebugOn then
mSGNL [< 'sTR "Evaluated term --> "; prterm_env env c >]
(* Prints a matched hypothesis *)
let db_matched_hyp debug env (id,c) =
if debug = DebugOn then
mSGNL [< 'sTR "Matched hypothesis --> "; 'sTR (id^": ");
prterm_env env c >]
(* Prints the matched conclusion *)
let db_matched_concl debug env c =
if debug = DebugOn then
mSGNL [< 'sTR "Matched goal --> "; prterm_env env c >]
|