package coq-lsp

  1. Overview
  2. Docs
package coq-lsp
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file interp.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
(************************************************************************)
(* Coq Petanque                                                         *)
(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
(* Copyright 2019-2024 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
(************************************************************************)

module Req = Request
open Protocol
module A = Petanque.Agent

(* Payload specialized to json / string *)
type json_rpc_result = (Yojson.Safe.t, string) Req.R.t

(* These types ares basically duplicated with controller/request.ml; move to a
   common lib (lsp?) *)
module Action = struct
  type t =
    | Now of (token:Coq.Limits.Token.t -> json_rpc_result)
    | Doc of
        { uri : Lang.LUri.File.t
        ; handler :
            token:Coq.Limits.Token.t -> doc:Fleche.Doc.t -> json_rpc_result
        }
    | Pos of
        { uri : Lang.LUri.File.t
        ; point : int * int
        ; handler :
               token:Coq.Limits.Token.t
            -> doc:Fleche.Doc.t
            -> point:int * int
            -> json_rpc_result
        }
end
(* End of controller/request.ml *)

let of_pet_err e = Req.R.map_error ~f:Petanque.Agent.Error.to_string e

(* Basically a functor from R.Handler.t to Action.t, but closing over params *)
let do_request (module R : Protocol.Request.S) ~params =
  let of_pet res = Result.map R.Handler.Response.to_yojson res |> of_pet_err in
  let handler params =
    match R.Handler.handler with
    | Immediate handler ->
      Action.Now (fun ~token -> handler ~token params |> of_pet)
    | FullDoc { uri_fn; handler } ->
      let uri = uri_fn params in
      let handler ~token ~doc = handler ~token ~doc params |> of_pet in
      Action.Doc { uri; handler }
    | PosInDoc { uri_fn; pos_fn; handler } ->
      let uri = uri_fn params in
      let point = pos_fn params in
      let handler ~token ~doc ~point =
        handler ~token ~doc ~point params |> of_pet
      in
      Action.Pos { uri; point; handler }
  in
  match R.Handler.Params.of_yojson (`Assoc params) with
  | Ok params -> handler params
  | Error message ->
    (* JSON-RPC Parse error *)
    let code = -32700 in
    Action.Now (fun ~token:_ -> Error (Req.Error.make code message))

type 'a handle = token:Coq.Limits.Token.t -> Action.t -> 'a

let handle_request ~(do_handle : 'a handle) ~unhandled ~token ~method_ ~params =
  match method_ with
  | s when String.equal GetStateAtPos.method_ s ->
    do_handle ~token (do_request (module GetStateAtPos) ~params)
  | s when String.equal GetRootState.method_ s ->
    do_handle ~token (do_request (module GetRootState) ~params)
  | s when String.equal Start.method_ s ->
    do_handle ~token (do_request (module Start) ~params)
  | s when String.equal RunTac.method_ s ->
    do_handle ~token (do_request (module RunTac) ~params)
  | s when String.equal Goals.method_ s ->
    do_handle ~token (do_request (module Goals) ~params)
  | s when String.equal Premises.method_ s ->
    do_handle ~token (do_request (module Premises) ~params)
  | s when String.equal StateEqual.method_ s ->
    do_handle ~token (do_request (module StateEqual) ~params)
  | s when String.equal StateHash.method_ s ->
    do_handle ~token (do_request (module StateHash) ~params)
  | s when String.equal StateProofEqual.method_ s ->
    do_handle ~token (do_request (module StateProofEqual) ~params)
  | s when String.equal StateProofHash.method_ s ->
    do_handle ~token (do_request (module StateProofHash) ~params)
  | _ -> unhandled ~token ~method_
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct