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
let init_coq ~debug =
let load_module = Dynlink.loadfile in
let load_plugin = Coq.Loader.plugin_handler None in
let vm, warnings = (true, None) in
Coq.Init.(coq_init { debug; load_module; load_plugin; vm; warnings })
let cmdline : Coq.Workspace.CmdLine.t =
{ coqlib = Coq.Args.coqlib_dyn
; findlib_config = None
; ocamlpath = []
; vo_load_path = []
; args = []
; require_libraries = []
}
let setup_workspace ~token ~init ~debug ~root =
let dir = Lang.LUri.File.to_string_file root in
(let open Coq.Compat.Result.O in
let+ workspace = Coq.Workspace.guess ~token ~debug ~cmdline ~dir in
let files = Coq.Files.make () in
Fleche.Doc.Env.make ~init ~workspace ~files)
|> Result.map_error (fun msg -> Petanque.Agent.Error.(make_request (coq msg)))
let trace_stderr hdr ?verbose:_ msg =
Format.eprintf "@[[trace] %s | %s @]@\n%!" hdr msg
let trace_ref = ref trace_stderr
let message_stderr ~lvl:_ ~message =
Format.eprintf "@[[message] %s @]@\n%!" message
let message_ref = ref message_stderr
let io =
let trace hdr ?verbose msg = !trace_ref hdr ?verbose msg in
let message ~lvl ~message = !message_ref ~lvl ~message in
let diagnostics ~uri:_ ~version:_ _diags = () in
let fileProgress ~uri:_ ~version:_ _pinfo = () in
let perfData ~uri:_ ~version:_ _perf = () in
let serverVersion _ = () in
let serverStatus _ = () in
let execInfo ~uri:_ ~version:_ ~range:_ = () in
{ Fleche.Io.CallBack.trace
; message
; diagnostics
; fileProgress
; perfData
; serverVersion
; serverStatus
; execInfo
}
let init_st = ref None
let env = ref None
let set_workspace ~token ~debug ~root =
let init = Option.get !init_st in
let open Coq.Compat.Result.O in
let+ env_ = setup_workspace ~token ~init ~debug ~root in
env := Some env_
let pp_diag fmt { Lang.Diagnostic.message; _ } =
Format.fprintf fmt "%a" Pp.pp_with message
let print_diags (doc : Fleche.Doc.t) =
let d = Fleche.Doc.diags doc in
Format.(eprintf "@[<v>%a@]" (pp_print_list pp_diag) d)
let read_raw ~uri =
let file = Lang.LUri.File.to_string_file uri in
try Ok Coq.Compat.Ocaml_414.In_channel.(with_open_text file input_all)
with Sys_error err -> Error Petanque.Agent.Error.(make_request (system err))
let languageId = "rocq"
let setup_doc ~token env uri =
match read_raw ~uri with
| Ok raw ->
let doc = Fleche.Doc.create ~token ~env ~uri ~languageId ~version:0 ~raw in
print_diags doc;
let target = Fleche.Doc.Target.End in
Ok (Fleche.Doc.check ~io ~token ~target ~doc ())
| Error err -> Error err
let build_doc ~token ~uri = setup_doc ~token (Option.get !env) uri
let to_uri uri : _ Request.R.t =
Lang.LUri.of_string uri |> Lang.LUri.File.of_uri
|> Result.map_error (fun msg ->
Petanque.Agent.Error.(make_request (system msg)))
let uri_of_path path = Format.asprintf "file:///%s" path |> to_uri
let set_roots ~token ~debug ~roots =
let root =
match roots with
| [] -> Sys.getcwd ()
| root :: _ -> root
in
let open Coq.Compat.Result.O in
let* root = uri_of_path root in
set_workspace ~token ~debug ~root
let init_agent ~token ~debug ~roots =
init_st := Some (init_coq ~debug);
Fleche.Io.CallBack.set io;
set_roots ~token ~debug ~roots
let toc_to_info (name, node) =
let open Coq.Compat.Option.O in
let+ ast = Fleche.Doc.Node.ast node in
(name, ast.Fleche.Doc.Node.Ast.ast_info)
let get_toc ~token:_ ~(doc : Fleche.Doc.t) :
(string * Lang.Ast.Info.t list option) list Petanque.Agent.R.t =
let { Fleche.Doc.toc; _ } = doc in
let toc = CString.Map.bindings toc |> List.filter_map toc_to_info in
Ok toc