Source file base.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
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(************************************************************************)
(* Coq Language Server Protocol                                         *)
(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
(* Written by: Emilio J. Gallego Arias                                  *)
(************************************************************************)
(* Status: Experimental                                                 *)
(************************************************************************)

(* This file contains some coq-specific commands, we should instead
   functorialize it so we can share with other OCaml-specific tools *)

module J = Yojson.Safe
module U = Yojson.Safe.Util

let string_field name dict = U.to_string List.(assoc name dict)

let odict_field ~default name dict =
  Option.cata U.to_assoc default (List.assoc_opt name dict)

module Message = struct
  type t =
    | Notification of
        { method_ : string [@key "method"]
        ; params : (string * Yojson.Safe.t) list
        }
    | Request of
        { id : int
        ; method_ : string [@key "method"]
        ; params : (string * Yojson.Safe.t) list
        }

  (** Reify an incoming message *)
  let from_yojson msg =
    try
      let dict = U.to_assoc msg in
      let method_ = string_field "method" dict in
      let params = odict_field ~default:[] "params" dict in
      (match List.assoc_opt "id" dict with
      | None -> Notification { method_; params }
      | Some id ->
        let id = U.to_int id in
        Request { id; method_; params })
      |> Result.ok
    with
    | Not_found -> Error ("missing parameter: " ^ J.to_string msg)
    | U.Type_error (msg, obj) ->
      Error (Format.asprintf "msg: %s; obj: %s" msg (J.to_string obj))

  let method_ = function
    | Notification { method_; _ } | Request { method_; _ } -> method_

  let params = function
    | Notification { params; _ } | Request { params; _ } -> params
end

let mk_reply ~id ~result =
  `Assoc [ ("jsonrpc", `String "2.0"); ("id", `Int id); ("result", result) ]

let mk_request_error ~id ~code ~message =
  `Assoc
    [ ("jsonrpc", `String "2.0")
    ; ("id", `Int id)
    ; ("error", `Assoc [ ("code", `Int code); ("message", `String message) ])
    ]

let mk_notification ~method_ ~params =
  `Assoc
    [ ("jsonrpc", `String "2.0")
    ; ("method", `String method_)
    ; ("params", params)
    ]

module ProgressToken : sig
  type t =
    | String of string
    | Int of int
  [@@deriving yojson]
end = struct
  type t =
    | String of string
    | Int of int

  let of_yojson x =
    match x with
    | `String s -> Result.ok (String s)
    | `Int i -> Result.ok (Int i)
    | _ -> Result.error "failure to parse ProgressToken.t"

  let to_yojson = function
    | String s -> `String s
    | Int i -> `Int i
end

module ProgressParams = struct
  type 'a t =
    { token : ProgressToken.t
    ; value : 'a
    }
  [@@deriving yojson]
end

let mk_progress ~token ~value f =
  let params = ProgressParams.(to_yojson f { token; value }) in
  mk_notification ~method_:"$/progress" ~params

module WorkDoneProgressBegin = struct
  type t =
    { kind : string
    ; title : string
    ; cancellable : bool option [@None]
    ; message : string option [@None]
    ; percentage : int option [@None]
    }
  [@@deriving to_yojson]
end

module WorkDoneProgressReport = struct
  type t =
    { kind : string
    ; cancellable : bool option [@None]
    ; message : string option [@None]
    ; percentage : int option [@None]
    }
  [@@deriving to_yojson]
end

module WorkDoneProgressEnd = struct
  type t = { kind : string } [@@deriving to_yojson]
end