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
89
90
91
92
(************************************************************************)
(* 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)
  | s when String.equal PetAst.method_ s ->
    do_handle ~token (do_request (module PetAst) ~params)
  | s when String.equal AstAtPos.method_ s ->
    do_handle ~token (do_request (module AstAtPos) ~params)
  | _ -> unhandled ~token ~method_