Source file jFleche.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
(************************************************************************)
(*         *   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 -- LGPL 2.1+                          *)
(* Copyright 2019-2023 Inria -- LGPL 2.1+                               *)
(* Written by: Emilio J. Gallego Arias                                  *)
(************************************************************************)

module Pp = JCoq.Pp

module Config = struct
  module Unicode_completion = struct
    type t = [%import: Fleche.Config.Unicode_completion.t] [@@deriving yojson]
  end

  type t = [%import: Fleche.Config.t] [@@deriving yojson]
end

module Types = struct
  module Point = struct
    type t = [%import: Fleche.Types.Point.t] [@@deriving yojson]
  end

  module Range = struct
    type t = [%import: Fleche.Types.Range.t] [@@deriving yojson]
  end

  module Diagnostic = struct
    module Libnames = Serlib.Ser_libnames

    (* Current Flèche diagnostic is not LSP-standard compliant, this one is *)
    type t =
      { range : Range.t
      ; severity : int
      ; message : string
      }
    [@@deriving yojson]

    let to_yojson
        { Fleche.Types.Diagnostic.range; severity; message; extra = _ } =
      let message = Pp.to_string message in
      to_yojson { range; severity; message }
  end
end

let mk_diagnostics ~uri ~version ld : Yojson.Safe.t =
  let diags = List.map Types.Diagnostic.to_yojson ld in
  let params =
    `Assoc
      [ ("uri", `String uri)
      ; ("version", `Int version)
      ; ("diagnostics", `List diags)
      ]
  in
  Base.mk_notification ~method_:"textDocument/publishDiagnostics" ~params

module Progress = struct
  module Info = struct
    type t =
      [%import:
        (Fleche.Progress.Info.t[@with Fleche.Types.Range.t := Types.Range.t])]
    [@@deriving yojson]
  end

  type t =
    { textDocument : Base.VersionedTextDocument.t
    ; processing : Info.t list
    }
  [@@deriving yojson]
end

let mk_progress ~uri ~version processing =
  let textDocument = { Base.VersionedTextDocument.uri; version } in
  let params = Progress.to_yojson { Progress.textDocument; processing } in
  Base.mk_notification ~method_:"$/coq/fileProgress" ~params

module GoalsAnswer = struct
  type t =
    { textDocument : Base.VersionedTextDocument.t
    ; position : Types.Point.t
    ; goals : string JCoq.Goals.reified_goal JCoq.Goals.goals option
    ; messages : string list
    ; error : string option
    }
  [@@deriving yojson]
end

let mk_goals ~uri ~version ~position ~goals ~messages ~error =
  let f rg = Coq.Goals.map_reified_goal ~f:Pp.to_string rg in
  let goals = Option.map (Coq.Goals.map_goals ~f) goals in
  let messages = List.map Pp.to_string messages in
  let error = Option.map Pp.to_string error in
  GoalsAnswer.to_yojson
    { textDocument = { uri; version }; position; goals; messages; error }

module Location = struct
  type t =
    { uri : string
    ; range : Types.Range.t
    }
  [@@deriving yojson]
end

module SymInfo = struct
  type t =
    { name : string
    ; kind : int
    ; location : Location.t
    }
  [@@deriving yojson]
end

module HoverContents = struct
  type t =
    { kind : string
    ; value : string
    }
  [@@deriving yojson]
end

module HoverInfo = struct
  type t =
    { contents : HoverContents.t
    ; range : Types.Range.t option
    }
  [@@deriving yojson]
end

module LabelDetails = struct
  type t = { detail : string } [@@deriving yojson]
end

module TextEditReplace = struct
  type t =
    { insert : Types.Range.t
    ; replace : Types.Range.t
    ; newText : string
    }
  [@@deriving yojson]
end

module CompletionData = struct
  type t =
    { label : string
    ; insertText : string option
    ; labelDetails : LabelDetails.t option
    ; textEdit : TextEditReplace.t option
    ; commitCharacters : string list option
    }
  [@@deriving yojson]
end