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
module type Point = sig
type t
val in_range : ?range:Lang.Range.t -> t -> bool
val gt_range : ?range:Lang.Range.t -> t -> bool
type offset_table = string
val to_offset : t -> offset_table -> int
val to_string : t -> string
end
module LineCol : Point with type t = int * int = struct
type t = int * int
type offset_table = string
let line_length offset text =
match String.index_from_opt text offset '\n' with
| Some l -> l - offset
| None -> String.length text - offset
let rec to_offset cur lc (l, c) text =
Io.Log.trace "to_offset"
(Format.asprintf "cur: %d | lc: %d | l: %d c: %d" cur lc l c);
if lc = l then cur + c
else
let ll = line_length cur text + 1 in
to_offset (cur + ll) (lc + 1) (l, c) text
let to_offset (l, c) text = to_offset 0 0 (l, c) text
let to_string (l, c) = "(" ^ string_of_int l ^ "," ^ string_of_int c ^ ")"
let debug_in_range = false
let debug_in_range hdr line col line1 col1 line2 col2 =
if debug_in_range then
Io.Log.trace hdr
(Format.asprintf "(%d, %d) in (%d,%d)-(%d,%d)" line col line1 col1 line2
col2)
let in_range ?range (line, col) =
match range with
| None -> false
| Some r ->
let line1 = r.Lang.Range.start.line in
let col1 = r.start.character in
let line2 = r.end_.line in
let col2 = r.end_.character in
debug_in_range "in_range" line col line1 col1 line2 col2;
(line1 < line && line < line2)
||
if line1 = line && line2 = line then col1 <= col && col < col2
else (line1 = line && col1 <= col) || (line2 = line && col < col2)
let gt_range ?range (line, col) =
match range with
| None -> false
| Some r ->
let line1 = r.Lang.Range.start.line in
let col1 = r.start.character in
let line2 = r.end_.line in
let col2 = r.end_.character in
debug_in_range "gt_range" line col line1 col1 line2 col2;
line < line1 || (line = line1 && col < col1)
end
module Offset : Point with type t = int = struct
type t = int
type offset_table = string
let in_range ?range point =
match range with
| None -> false
| Some range ->
range.Lang.Range.start.offset <= point
&& point < range.Lang.Range.end_.offset
let gt_range ?range point =
match range with
| None -> false
| Some range -> point < range.Lang.Range.start.offset
let to_offset off _ = off
let to_string off = string_of_int off
end
type approx =
| Exact
| PrevIfEmpty
| Prev
module type S = sig
module P : Point
type ('a, 'r) query = doc:Doc.t -> point:P.t -> 'a -> 'r option
val node : (approx, Doc.Node.t) query
val range : (approx, Lang.Range.t) query
val ast : (approx, Doc.Node.Ast.t) query
val goals : (approx, Coq.Goals.reified_pp) query
val messages : (approx, Doc.Node.Message.t list) query
val info : (approx, Doc.Node.Info.t) query
val completion : (string, string list) query
val in_state : st:Coq.State.t -> f:('a -> 'b option) -> 'a -> 'b option
end
let some x = Some x
let obind x f = Option.bind f x
module Make (P : Point) : S with module P := P = struct
type ('a, 'r) query = doc:Doc.t -> point:P.t -> 'a -> 'r option
let find ~doc ~point approx =
let rec find prev l =
match l with
| [] -> prev
| node :: xs -> (
let range = node.Doc.Node.range in
match approx with
| Exact -> if P.in_range ~range point then Some node else find None xs
| PrevIfEmpty ->
if P.gt_range ~range point then prev else find (Some node) xs
| Prev ->
if P.gt_range ~range point || P.in_range ~range point then prev
else find (Some node) xs)
in
find None doc.Doc.nodes
let node = find
let pr_goal st =
let ppx env sigma x =
let { Coq.Protect.E.r; feedback } =
Coq.Print.pr_letype_env ~goal_concl_style:true env sigma x
in
Io.Log.feedback feedback;
match r with
| Coq.Protect.R.Completed (Ok pr) -> pr
| Coq.Protect.R.Completed (Error _pr) -> Pp.str "printer failed!"
| Interrupted -> Pp.str "printer interrupted!"
in
let lemmas = Coq.State.lemmas ~st in
Option.map (Coq.Goals.reify ~ppx) lemmas
let range ~doc ~point approx =
let node = find ~doc ~point approx in
Option.map Doc.Node.range node
let ast ~doc ~point approx =
let node = find ~doc ~point approx in
Option.bind node Doc.Node.ast
let in_state ~st ~f node =
match Coq.State.in_state ~st ~f node with
| { r = Coq.Protect.R.Completed (Result.Ok res); feedback } ->
Io.Log.feedback feedback;
res
| { r = Coq.Protect.R.Completed (Result.Error _) | Coq.Protect.R.Interrupted
; feedback
} ->
Io.Log.feedback feedback;
None
let goals ~doc ~point approx =
find ~doc ~point approx
|> obind (fun node ->
let st = node.Doc.Node.state in
in_state ~st ~f:pr_goal st)
let messages ~doc ~point approx =
find ~doc ~point approx |> Option.map Doc.Node.messages
let info ~doc ~point approx =
find ~doc ~point approx |> Option.map Doc.Node.info
let pr_extref gr =
match gr with
| Globnames.TrueGlobal gr -> Printer.pr_global gr
| Globnames.Abbrev kn -> Names.KerName.print kn
let to_qualid p = try Some (Libnames.qualid_of_string p) with _ -> None
let completion ~doc ~point prefix =
find ~doc ~point Exact
|> obind (fun node ->
in_state ~st:node.Doc.Node.state prefix ~f:(fun prefix ->
to_qualid prefix
|> obind (fun p ->
Nametab.completion_canditates p
|> List.map (fun x -> Pp.string_of_ppcmds (pr_extref x))
|> some)))
end
module LC = Make (LineCol)
module O = Make (Offset)