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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** Ltac debugger interface; clients should register hooks to interact
with their provided interface. *)
module Action = struct
type t =
| StepIn
| StepOver
| StepOut
| Continue
| Skip
| Interrupt
| Help
| UpdBpts of ((string * int) * bool) list
| Configd
| GetStack
| GetVars of int
| RunCnt of int
| RunBreakpoint of string
| Command of string
| Failed
| Ignore (* do nothing, read another command *)
(* XXX: Could we move this to the CString utility library? *)
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
let parse_complex inst : (t, string) result =
if 'r' = String.get inst 0 then
let arg = String.(trim (sub inst 1 (length inst - 1))) in
if arg <> "" then
match int_of_string_opt arg with
| Some num ->
if num < 0 then
Error "number must be positive"
else
Ok (RunCnt num)
| None ->
Ok (RunBreakpoint (possibly_unquote arg))
else
Error ("invalid input: " ^ inst)
else
Error ("invalid input: " ^ inst)
(* XXX: Should be moved to the clients *)
let parse inst : (t, string) result =
match inst with
| "" -> Ok StepIn
| "s" -> Ok Skip
| "x" -> Ok Interrupt
| "h"| "?" -> Ok Help
| _ -> parse_complex inst
end
module Answer = struct
type t =
| Prompt of Pp.t
| Goal of Pp.t
| Output of Pp.t
| Init
| Stack of (string * (string * int list) option) list
| Vars of (string * Pp.t) list
end
module Intf = struct
type t =
{ read_cmd : unit -> Action.t
(** request a debugger command from the client *)
; submit_answer : Answer.t -> unit
(** receive a debugger answer from Ltac *)
; isTerminal : bool
(** whether the debugger is running as a terminal (non-visual) *)
}
let ltac_debug_ref : t option ref = ref None
let set hooks = ltac_debug_ref := Some hooks
let get () = !ltac_debug_ref
end
|
