Source file `client.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
module Lsp = Fleche_lsp
open Petanque_json

(* Client wrap *)
module type Chans = sig
  val ic : in_channel
  val oc : Format.formatter
  val trace : ?verbose:string -> string -> unit
  val message : lvl:int -> message:string -> unit
end

(* Display incoming requests *)
let display_requests = false

let maybe_display_request method_ =
  if display_requests then Format.eprintf "received request: %s@\n%!" method_

let do_trace ~trace params =
  match Lsp.Base.TraceParams.of_yojson (`Assoc params) with
  | Ok { message; verbose } -> trace ?verbose message
  | Error _ -> ()

let do_message ~message params =
  match Lsp.Base.MessageParams.of_yojson (`Assoc params) with
  | Ok { type_; message = msg } -> message ~lvl:type_ ~message:msg
  | Error _ -> ()

(* Read until we find a response *)
let rec read_response ~trace ~message ic =
  match Lsp.Io.read_message ic with
  | Some (Ok (Lsp.Base.Message.Response r)) -> Ok r
  | Some (Ok (Notification { method_; params }))
    when String.equal method_ Lsp.Base.TraceParams.method_ ->
    do_trace ~trace params;
    read_response ~trace ~message ic
  | Some (Ok (Notification { method_; params }))
    when String.equal method_ Lsp.Base.MessageParams.method_ ->
    do_message ~message params;
    read_response ~trace ~message ic
  | Some (Ok (Request { method_; _ })) | Some (Ok (Notification { method_; _ }))
    ->
    maybe_display_request method_;
    read_response ~trace ~message ic
  | Some (Error err) -> Error err
  | None -> assert false (* not in our testing setup *)

let id_counter = ref 0

let get_id () =
  incr id_counter;
  !id_counter

module Wrap (R : Protocol.Request.S) (C : Chans) : sig
  val call : R.Params.t -> (R.Response.t, string) Result.t
end = struct
  let trace = C.trace
  let message = C.message

  let call params =
    let id = get_id () in
    let method_ = R.method_ in
    let params = Yojson.Safe.Util.to_assoc (R.Params.to_yojson params) in
    let request = Lsp.Base.Request.make ~id ~method_ ~params () in
    let () = Lsp.Io.send_message C.oc (Lsp.Base.Message.Request request) in
    read_response ~trace ~message C.ic |> fun r ->
    Result.bind r (function
      | Ok { id = _; result } -> R.Response.of_yojson result
      | Error { id = _; code = _; message; data = _ } -> Error message)
end

module S (C : Chans) = struct
  open Protocol
  open Protocol_shell

  (* Shell calls (they do have an equivalent version in LSP) *)
  let set_workspace =
    let module M = Wrap (SetWorkspace) (C) in
    M.call

  let toc =
    let module M = Wrap (TableOfContents) (C) in
    M.call

  (* Standard calls *)
  let get_root_state =
    let module M = Wrap (GetRootState) (C) in
    M.call

  let get_state_at_pos =
    let module M = Wrap (GetStateAtPos) (C) in
    M.call

  let start =
    let module M = Wrap (Start) (C) in
    M.call

  let run =
    let module M = Wrap (RunTac) (C) in
    M.call

  let goals =
    let module M = Wrap (Goals) (C) in
    M.call

  let premises =
    let module M = Wrap (Premises) (C) in
    M.call

  let state_equal =
    let module M = Wrap (StateEqual) (C) in
    M.call

  let state_hash =
    let module M = Wrap (StateHash) (C) in
    M.call

  let state_proof_equal =
    let module M = Wrap (StateProofEqual) (C) in
    M.call

  let state_proof_hash =
    let module M = Wrap (StateProofHash) (C) in
    M.call
end