blob: d9c5d528a787362c2f8da551821551f8b167cb5f (
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
|
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 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; '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
| _ -> prompt () in
prompt ()
(* 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 >]
|
