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
module R = struct
(** We want to replace the string by a proper diagnostic we can send to the
client *)
type 'a t =
| Ok of 'a
| Error of string
let map ~f = function
| Ok x -> Ok (f x)
| Error e -> Error e
end
module Util = struct
(** Builds a string that contains the right white-space padding between two
points *)
let build_whitespace prev cur =
let l_p, c_p, o_p = Lang.Point.(prev.line, prev.character, prev.offset) in
let l_c, c_c, o_c = Lang.Point.(cur.line, cur.character, cur.offset) in
let nl = l_c - l_p in
let nc, padding = if l_p = l_c then (c_c - c_p, 0) else (c_c, o_c - o_p) in
String.make padding ' ' ^ String.make nl '\n' ^ String.make nc ' '
let ~raw ~(range : Lang.Range.t) =
let start = range.start.offset in
let length = range.end_.offset - start in
let length =
if String.length raw < start + length then String.length raw - start
else length
in
String.sub raw start length
end
module Markdown = struct
let gen l = String.make (String.length l) ' '
let rec md_map_lines coq l =
match l with
| [] -> []
| l :: ls ->
let code_marker = if coq then [ "```" ] else [ "```coq"; "```rocq" ] in
let check l c = List.exists (String.equal c) l in
if check code_marker l then gen l :: md_map_lines (not coq) ls
else (if coq then l else gen l) :: md_map_lines coq ls
let process text =
let lines = String.split_on_char '\n' text in
let lines = md_map_lines false lines in
String.concat "\n" lines
end
module LaTeX = struct
let gen l = String.make (String.length l) ' '
let rec tex_map_lines coq l =
match l with
| [] -> []
| l :: ls ->
let code_marker =
if coq then [ "\\end{rocq}"; "\\end{coq}" ]
else [ "\\begin{rocq}"; "\\begin{coq}" ]
in
let check l c = List.exists (String.equal c) l in
if check code_marker l then gen l :: tex_map_lines (not coq) ls
else (if coq then l else gen l) :: tex_map_lines coq ls
let process text =
let lines = String.split_on_char '\n' text in
let lines = tex_map_lines false lines in
String.concat "\n" lines
end
module WaterProof = struct
open Fleche_waterproof.Json
let wp_error msg = R.Error (Format.asprintf "Waterproof parsing: %s" msg)
let code_block block =
match block with
| { CAst.v = Assoc dict; _ } -> (
match find "type" dict with
| Some { CAst.v = String "code"; _ } -> (
match find "text" dict with
| Some { CAst.v = String coq_span; range } -> Some (range, coq_span)
| _ -> None)
| _ -> None)
| _ -> None
let new_to_space = function
| '\n' -> ' '
| x -> x
let coq_block_to_span (contents, last_point) (range, coq) =
let range_text = Util.build_whitespace last_point range.Lang.Range.start in
let last_point = range.Lang.Range.end_ in
let coq = String.map new_to_space coq in
(contents ^ range_text ^ coq, last_point)
let block_pos (range, _) = Format.asprintf "%a" Lang.Range.pp range
let waterproof_debug = false
let from_blocks blocks =
let start_point = Lang.Point.{ line = 0; character = 0; offset = 0 } in
let code_blocks = List.filter_map code_block blocks in
let code_pos = List.map block_pos code_blocks in
let contents, _ =
List.fold_left coq_block_to_span ("", start_point) code_blocks
in
(if waterproof_debug then
let code_pos = String.concat "\n" code_pos in
Io.Log.trace "waterproof" "pos:\n%s\nContents:\n%s" code_pos contents);
R.Ok contents
let from_json json =
match json with
| CAst.{ v = Assoc dict; _ } -> (
match find "blocks" dict with
| None -> wp_error "blocks field not found"
| Some blocks -> (
match blocks with
| { CAst.v = List blocks; _ } -> from_blocks blocks
| _ -> wp_error "blocks not a list"))
| _ -> wp_error "top-level object not a dictionary"
let process raw =
let lexbuf = Lexing.from_string raw in
match Fleche_waterproof.(Ljson.prog Tjson.read) lexbuf with
| None -> R.Ok ""
| Some json -> from_json json
| exception _ -> wp_error "parsing failed"
end
let process_contents ~uri ~languageId ~raw =
let ext = Lang.LUri.File.extension uri in
match (languageId, ext) with
| "coq", _ | "rocq", _ -> R.Ok raw
| "latex", _ -> R.Ok (LaTeX.process raw)
| "markdown", _ -> R.Ok (Markdown.process raw)
| _, ".wpn" -> WaterProof.process raw
| _, _ ->
let msg =
Format.asprintf "unknown format: %s for %a" languageId Lang.LUri.File.pp
uri
in
R.Error msg
type t =
{ raw : string (** That's the original, unprocessed document text *)
; text : string
(** That's the text to be sent to the prover, already processed, encoded
in UTF-8 *)
; last : Lang.Point.t (** Last point of [text] *)
; lines : string Array.t (** [text] split in lines *)
}
let get_last_text text =
let offset = String.length text in
let lines = String.split_on_char '\n' text |> Array.of_list in
let n_lines = Array.length lines in
let last_line = if n_lines < 1 then "" else Array.get lines (n_lines - 1) in
let character = Lang.Utf.length_utf16 last_line in
(Lang.Point.{ line = n_lines - 1; character; offset }, lines)
let make ~uri ~languageId ~raw =
match process_contents ~uri ~languageId ~raw with
| R.Error e -> R.Error e
| R.Ok text ->
let last, lines = get_last_text text in
R.Ok { raw; text; last; lines }
let make_raw ~raw =
let text = raw in
let last, lines = get_last_text text in
{ raw; text; last; lines }
let ~contents:{ raw; _ } ~range = Util.extract_raw ~raw ~range