package why3find

  1. Overview
  2. Docs
A Why3 Package Manager

Install

dune-project
 Dependency

Authors

Maintainers

Sources

why3find-1.3.0.tar.gz
md5=435da830a513fd91ec5411c91126b763
sha512=fd8b04eb16d569c0dc9e5595a40b174d7858121b080c81d459b2f28fb3af1ebc32ef408859d5c1c5f45c61790625c027c2ecfc3d45e597943543de7212bab8d6

doc/src/why3find.utils/lsp.ml.html

Source file lsp.ml

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
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

(* -------------------------------------------------------------------------- *)
(* --- Language Server Base Protocol                                      --- *)
(* -------------------------------------------------------------------------- *)

type response = (Json.t,Json.t) result
type callback = response -> unit

type message =
  | Notify of { meth: string; param: Json.t }
  | Request of { meth: string; param: Json.t; callback: callback }

type server = {
  mutable shutdown : bool ; (* has been shutdown *)
  mutable processing : bool ; (* processing a request *)
  queue : message Queue.t ; (* pending notifications *)
  callbacks : (string, callback) Hashtbl.t ;
  channel : Rpc.channel ;
}

(* -------------------------------------------------------------------------- *)
(* --- Decoding Json-RPC                                                  --- *)
(* -------------------------------------------------------------------------- *)

type handler = (server -> Json.t -> Json.t)
let protocol : (string, handler) Hashtbl.t = Hashtbl.create 0

let json_header = "jsonrpc", `String "2.0"
let json_rpc msg : Json.t = `Assoc ( json_header :: msg )

let send_response { channel } ~id ~result =
  if not @@ Json.is_empty id then
    Rpc.push channel @@ Json.to_string @@ json_rpc [
      "id", id ;
      "result", result
    ]

let send_error { channel } ~id ~code ~msg =
  if not @@ Json.is_empty id then
    Rpc.push channel @@ Json.to_string @@ json_rpc [
      "id", id ;
      "error", `Assoc [
        "code", `Int code ;
        "message", `String msg ;
      ]]

let send_notification { channel } meth params =
  Rpc.push channel @@ Json.to_string @@ json_rpc [
    "method", `String meth ;
    "params", params ;
  ]

let rqid = ref 0
let make_id () = incr rqid ; Printf.sprintf "#%d" !rqid

let send_request server meth params callback =
  let id = make_id () in
  Hashtbl.replace server.callbacks id callback ;
  Rpc.push server.channel @@ Json.to_string @@ json_rpc [
    "id", `String id ;
    "method", `String meth ;
    "params", params ;
  ]

let send_message ch = function
  | Notify { meth = m ; param = p } ->
    send_notification ch m p
  | Request { meth = m ; param = p ; callback = fn } ->
    send_request ch m p fn

let flush server =
  begin
    server.processing <- false ;
    Queue.iter (send_message server) server.queue ;
    Queue.clear server.queue ;
    Rpc.flush server.channel ;
  end

let jresponse rq =
  if Json.mfield "result" rq
  then Ok (Json.jfield "result" rq)
  else Error (Json.jfield "error" rq)

let process_request server ~id ~meth ~params =
  begin
    server.processing <- true ;
    match Hashtbl.find protocol meth server params with
    | result ->
      send_response server ~id ~result
    | exception Not_found ->
      if not @@ String.starts_with ~prefix:"$/" meth then
        Log.error "Unsupported method: %s" meth ;
      (* still error the request if there is an id *)
      send_error server ~id ~code:(-32601) ~msg:meth
    | exception Invalid_argument msg ->
      Log.error "Invalid parameters (%s:%s)" meth msg ;
      send_error server ~id ~code:(-32602) ~msg
    | exception Failure msg ->
      Log.error "Internal error (%s:%s)" meth msg ;
      send_error server ~id ~code:(-32603) ~msg
    | exception err ->
      let msg = Printexc.to_string err in
      Log.error "Internal error (%s:%s)" meth msg ;
      send_error server ~id ~code:(-32603) ~msg
  end

let process_response server ~id ~result =
  begin
    server.processing <- true ;
    match Hashtbl.find server.callbacks id with
    | exception Not_found -> ()
    | fn ->
      Hashtbl.remove server.callbacks id ; fn result
  end

let process server =
  Rpc.yield server.channel ;
  if server.processing then false
  else
    match Rpc.pull server.channel with
    | None -> false
    | Some data ->
      try
        let rq = Json.of_string data in
        begin
          if Json.mfield "method" rq then
            let id = Json.jfield "id" rq in
            let meth = Json.jfield "method" rq |> Json.jstring in
            let params = Json.jfield "params" rq in
            process_request server ~id ~meth ~params
          else
            let id = Json.jfield "id" rq |> Json.jstring in
            let result = jresponse rq in
            process_response server ~id ~result
        end ;
        flush server ; true
      with Invalid_argument msg ->
        Log.error "Invalid message (%s)" msg ;
        send_error server ~id:(`Int 0) ~code:(-32700) ~msg ;
        flush server ; true

let yield { channel } = Rpc.yield channel

(* -------------------------------------------------------------------------- *)
(* --- Decoding LSP Messages                                              --- *)
(* -------------------------------------------------------------------------- *)

let register ?(force=false) name fn =
  if not force && Hashtbl.mem protocol name then
    Log.error "Already registered method or notification: %s" name
  else
    Hashtbl.add protocol name fn

let ignore name = register name (fun _ _ -> `Null)

let notify server meth param =
  if server.processing then
    Queue.push (Notify { meth ; param }) server.queue
  else
    send_notification server meth param

let error meth = function Ok _ -> () | Error data ->
  Format.eprintf "[%s] ERROR: %a@." meth Json.pretty data

let send server meth ?(callback = error meth) param =
  if server.processing then
    Queue.push (Request { meth ; param ; callback }) server.queue
  else
    send_request server meth param callback

(* -------------------------------------------------------------------------- *)
(* --- Handling Transport I/O                                             --- *)
(* -------------------------------------------------------------------------- *)

let shutdown server = server.shutdown <- true

let running { shutdown ; processing ; channel } =
  not shutdown || processing || Rpc.processing channel

let establish transport =
  let channel = Rpc.establish transport in
  Log.message "why3find language server started." ; {
    channel ;
    shutdown = false ;
    processing = false ;
    queue = Queue.create () ;
    callbacks = Hashtbl.create 0 ;
  }

(* -------------------------------------------------------------------------- *)
(* ---  Default LSP Behavior (refined in lspserver)                       --- *)
(* -------------------------------------------------------------------------- *)

let () = register "initialize"
    begin fun _channel _params -> `Assoc [ "capabilities", `Assoc [] ] end

let () = register "shutdown"
    begin fun server _data -> shutdown server ; `Null end

let () = register "exit"
    begin fun server _data -> shutdown server ; `Null end

let () = ignore "initialized"
let () = ignore "$/setTrace"

(* -------------------------------------------------------------------------- *)
(* --- Capabilities                                                       --- *)
(* -------------------------------------------------------------------------- *)

type capability = Capability of { id: string ; meth: string }

let jregistration id meth param : Json.t =
  Json.assoc [
    "id", `String id ;
    "method", `String meth ;
    "registerOptions", param ;
  ]

let register_capability server meth param =
  let id = make_id () in
  send server "client/registerCapability" @@ Json.assoc [
    "registrations", `List [ jregistration id meth param ]
  ] ;
  Capability { id ; meth }

let unregister_capability server = function Capability { id ; meth } ->
  send server "client/unregisterCapability" @@ Json.assoc [
    "unregisterations", `List [ jregistration id meth `Null ]
  ]

(* -------------------------------------------------------------------------- *)