[lsp] [petanque] Remove handling hook in favor of more typed requests.

controller/lsp_core.ml

@@ -427,49 +427,35 @@ let do_changeConfiguration ~io params =
   Rq_init.do_settings settings;
   ()
 
-(* Petanque bridge *)
-let petanque_init () =
-  let fn ~token:_ uri =
-    match Fleche.Theory.find_doc ~uri with
-    | Some doc -> Ok doc
-    | None ->
-      let msg = Format.asprintf "lsp_core: document not found" in
-      Error (Petanque.Agent.Error.System msg)
-  in
-  Petanque.Agent.fn := fn
-
-let petanque_handle_doc (module S : Petanque_json.Protocol.Request.S) ~params =
-  (* XXX fixme: doc is now retrieved by petanque callback, but we could use
-     this *)
-  let handler ~token ~doc:_ =
-    Petanque_json.Interp.do_request ~token (module S) ~params
-  in
-  (* XXX: The below wouldn't work due to params having uri in an incorrect
-     format, do_document_request expects the uri to be in the textDocument
-     field *)
-  let textDocument = string_field "uri" params in
-  let params =
-    ("textDocument", `Assoc [ ("uri", `String textDocument) ]) :: params
-  in
-  do_document_request ~postpone:true ~params ~handler
-
-let petanque_handle_now ~token (module S : Petanque_json.Protocol.Request.S)
-    ~params =
-  Rq.Action.now (Petanque_json.Interp.do_request ~token (module S) ~params)
+(* EJGA: Note that our current configuration allow petanque calls to be
+   interrupted, this can become an issue with LSP. For now, clients must choose
+   a trade-off (we could disable interruption on petanque call, but that brings
+   other downsides)
+
+   The only real solution is to wait for OCaml 5.x support, so we can server
+   read-only queries without interrupting the main Coq thread. *)
+let petanque_handle ~token (module R : Petanque_json.Protocol.Request.S) ~params
+    =
+  let open Petanque_json in
+  match Interp.do_request (module R) ~params with
+  | Interp.Action.Now handler -> Rq.Action.now (handler ~token)
+  | Interp.Action.Doc { uri; handler } ->
+    (* Request document execution if not ready *)
+    let postpone = true in
+    Rq.Action.(Data (DocRequest { uri; postpone; handler }))
 
-(* XXX: Deduplicate with Petanque_json.Protocol. *)
 let do_petanque ~token method_ params =
   (* For now we do a manual brigde *)
   let open Petanque_json.Protocol in
   match method_ with
   | s when String.equal Start.method_ s ->
-    petanque_handle_doc (module Start) ~params
+    petanque_handle ~token (module Start) ~params
   | s when String.equal RunTac.method_ s ->
-    petanque_handle_now ~token (module RunTac) ~params
+    petanque_handle ~token (module RunTac) ~params
   | s when String.equal Goals.method_ s ->
-    petanque_handle_now ~token (module Goals) ~params
+    petanque_handle ~token (module Goals) ~params
   | s when String.equal Premises.method_ s ->
-    petanque_handle_now ~token (module Premises) ~params
+    petanque_handle ~token (module Premises) ~params
   | _ ->
     (* EJGA: should we allow this system to compose better with other LSP
        extensions? *)
@@ -532,7 +518,6 @@ let lsp_init_process ~ofn ~io ~cmdline ~debug msg : Init_effect.t =
         dirs
     in
     List.iter (log_workspace ~io) workspaces;
-    petanque_init ();
     Success workspaces
   | LSP.Message.Request { id; _ } ->
     (* per spec *)

petanque/agent.ml

@@ -101,17 +101,12 @@ let protect_to_result (r : _ Coq.Protect.E.t) : (_, _) Result.t =
     Error (Error.Anomaly (Pp.string_of_ppcmds msg))
   | { r = Completed (Ok r); feedback = _ } -> Ok r
 
-let fn = ref (fun ~token:_ _uri -> Error (Error.System "No handler for fn"))
-
-let start ~token ~uri ?pre_commands ~thm () =
-  match !fn ~token uri with
-  | Ok doc ->
-    let open Coq.Compat.Result.O in
-    let* node = find_thm ~doc ~thm in
-    (* Usually single shot, so we don't memoize *)
-    let memo = false in
-    execute_precommands ~token ~memo ~pre_commands ~node |> protect_to_result
-  | Error err -> Error err
+let start ~token ~doc ?pre_commands ~thm () =
+  let open Coq.Compat.Result.O in
+  let* node = find_thm ~doc ~thm in
+  (* Usually single shot, so we don't memoize *)
+  let memo = false in
+  execute_precommands ~token ~memo ~pre_commands ~node |> protect_to_result
 
 let proof_finished { Coq.Goals.goals; stack; shelf; given_up; _ } =
   List.for_all CList.is_empty [ goals; shelf; given_up ] && CList.is_empty stack

petanque/agent.mli

@@ -40,16 +40,34 @@ module Run_result : sig
     | Current_state of 'a
 end
 
-val fn : (token:Coq.Limits.Token.t -> Lang.LUri.File.t -> Fleche.Doc.t R.t) ref
+(** Protocol notes:
 
-(** [start ~token ~fn ~uri ~pre_commands ~thm] start a new proof for theorem
-    [thm] in file [uri] under [fn]. [token] can be used to interrupt the
-    computation. Returns the proof state or error otherwise. [pre_commands] is a
-    string of dot-separated Coq commands that will be executed before the proof
-    starts. *)
+    The idea is that the types of the functions here have a direct translation
+    to the JSON-RPC (or any other) protocol.
+
+    Thus, types here correspond to types in the wire, except for cases where the
+    protocol layer performs an implicit mapping on types.
+
+    So far, the mappings are:
+
+    - [uri] <-> [Doc.t]
+    - [int] <-> [State.t]
+
+    The [State.t] mapping is easy to do at the protocol level with a simple
+    mapping, however [uri -> Doc.t] may need to yield to the document manager to
+    build the corresponding [doc]. This is very convenient for users, but
+    introduces a little bit more machinery.
+
+    We could imagine a future where [State.t] need to be managed asynchronously,
+    then the same approach that we use for [Doc.t] could happen. *)
+
+(** [start ~token ~doc ~pre_commands ~thm] start a new proof for theorem [thm]
+    in file [uri] under [fn]. [token] can be used to interrupt the computation.
+    Returns the proof state or error otherwise. [pre_commands] is a string of
+    dot-separated Coq commands that will be executed before the proof starts. *)
 val start :
      token:Coq.Limits.Token.t
-  -> uri:Lang.LUri.File.t
+  -> doc:Fleche.Doc.t
   -> ?pre_commands:string
   -> thm:string
   -> unit

petanque/json_shell/interp.ml

@@ -2,47 +2,83 @@ open Protocol
 open Protocol_shell
 module A = Petanque.Agent
 
-let do_request ~token (module R : Protocol.Request.S) ~params =
-  match R.Handler.Params.of_yojson (`Assoc params) with
-  | Ok params -> (
-    match R.Handler.handler ~token params with
-    | Ok result -> Ok (R.Handler.Response.to_yojson result)
-    | Error err ->
+(* These types ares basically duplicated with controller/request.ml; move to a
+   common lib (lsp?) *)
+type r = (Yojson.Safe.t, int * string) Result.t
+
+module Action = struct
+  type 'a t =
+    | Now of (token:Coq.Limits.Token.t -> r)
+    | Doc of
+        { uri : Lang.LUri.File.t
+        ; handler : token:Coq.Limits.Token.t -> doc:Fleche.Doc.t -> r
+        }
+end
+(* End of controller/request.ml *)
+
+let of_pet_err res =
+  Result.map_error
+    (fun err ->
       let message = Petanque.Agent.Error.to_string err in
       let code = Petanque.Agent.Error.to_code err in
-      Error (code, message))
+      (code, message))
+    res
+
+(* 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 }
+  in
+  match R.Handler.Params.of_yojson (`Assoc params) with
+  | Ok params -> handler params
   | Error message ->
     (* JSON-RPC Parse error *)
     let code = -32700 in
-    Error (code, message)
+    Action.Now (fun ~token:_ -> Error (code, message))
+
+let do_handle ~fn ~token (module R : Protocol.Request.S) ~params =
+  match do_request (module R) ~params with
+  | Action.Now handler -> handler ~token
+  | Action.Doc { uri; handler } ->
+    let open Coq.Compat.Result.O in
+    let* doc = fn ~token ~uri |> of_pet_err in
+    handler ~token ~doc
 
 let handle_request ~token ~method_ ~params =
   match method_ with
   | s when String.equal SetWorkspace.method_ s ->
-    do_request ~token (module SetWorkspace) ~params
+    do_handle ~token (module SetWorkspace) ~params
   | s when String.equal Start.method_ s ->
-    do_request ~token (module Start) ~params
+    do_handle ~token (module Start) ~params
   | s when String.equal RunTac.method_ s ->
-    do_request ~token (module RunTac) ~params
+    do_handle ~token (module RunTac) ~params
   | s when String.equal Goals.method_ s ->
-    do_request ~token (module Goals) ~params
+    do_handle ~token (module Goals) ~params
   | s when String.equal Premises.method_ s ->
-    do_request ~token (module Premises) ~params
+    do_handle ~token (module Premises) ~params
   | _ ->
-    (* JSON-RPC method not found *)
-    let code = -32601 in
-    let message = "method not found" in
-    Error (code, message)
+    fun ~fn:_ ->
+      (* JSON-RPC method not found *)
+      let code = -32601 in
+      let message = "method not found" in
+      Error (code, message)
 
-let request ~token ~id ~method_ ~params =
-  match handle_request ~token ~method_ ~params with
+let request ~fn ~token ~id ~method_ ~params =
+  match handle_request ~fn ~token ~method_ ~params with
   | Ok result -> Lsp.Base.Response.mk_ok ~id ~result
   | Error (code, message) -> Lsp.Base.Response.mk_error ~id ~code ~message
 
-let interp ~token (r : Lsp.Base.Message.t) : Lsp.Base.Message.t option =
+let interp ~fn ~token (r : Lsp.Base.Message.t) : Lsp.Base.Message.t option =
   match r with
   | Request { id; method_; params } ->
-    let response = request ~token ~id ~method_ ~params in
+    let response = request ~fn ~token ~id ~method_ ~params in
     Some (Lsp.Base.Message.response response)
   | Notification { method_; params = _ } ->
     let message = "unhandled notification: " ^ method_ in

petanque/json_shell/pet.ml

@@ -28,8 +28,10 @@ let send_message msg =
 (* Format.fprintf Format.std_formatter "@[%a@]@\n%!" Yojson.Safe.pretty_print
    msg *)
 
+let fn = Petanque.Shell.build_doc
+
 let interp ~token request =
-  match Interp.interp ~token request with
+  match Interp.interp ~fn ~token request with
   | None -> ()
   | Some message -> send_message message
 

petanque/json_shell/protocol.ml

@@ -1,10 +1,20 @@
+open Lang
 open Petanque
 
 (* Serialization for agent types *)
 open JAgent
 
 (* RPC-side server mappings, internal; we could split this in a different module
    eventually as to make this clearer. *)
+module HType = struct
+  type ('p, 'r) t =
+    | Immediate of (token:Coq.Limits.Token.t -> 'p -> 'r R.t)
+    | FullDoc of
+        { uri_fn : 'p -> LUri.File.t
+        ; handler : token:Coq.Limits.Token.t -> doc:Fleche.Doc.t -> 'p -> 'r R.t
+        }
+end
+
 module type Handler = sig
   (* Server-side RPC specification *)
   module Params : sig
@@ -16,7 +26,7 @@ module type Handler = sig
     type t [@@deriving to_yojson]
   end
 
-  val handler : token:Coq.Limits.Token.t -> Params.t -> Response.t R.t
+  val handler : (Params.t, Response.t) HType.t
 end
 
 (* Note that here we follow JSON-RPC / LSP capitalization conventions *)
@@ -69,8 +79,13 @@ module Start = struct
       type t = State.t [@@deriving yojson]
     end
 
-    let handler ~token { Params.uri; pre_commands; thm } =
-      Agent.start ~token ~uri ?pre_commands ~thm ()
+    let handler =
+      HType.FullDoc
+        { uri_fn = (fun { Params.uri; _ } -> uri)
+        ; handler =
+            (fun ~token ~doc { Params.uri = _; pre_commands; thm } ->
+              Agent.start ~token ~doc ?pre_commands ~thm ())
+        }
   end
 end
 
@@ -107,8 +122,10 @@ module RunTac = struct
       type t = State.t Run_result.t [@@deriving yojson]
     end
 
-    let handler ~token { Params.memo; st; tac } =
-      Agent.run ~token ?memo ~st ~tac ()
+    let handler =
+      HType.Immediate
+        (fun ~token { Params.memo; st; tac } ->
+          Agent.run ~token ?memo ~st ~tac ())
   end
 end
 
@@ -131,7 +148,8 @@ module Goals = struct
 
     module Response = Response
 
-    let handler ~token { Params.st } = Agent.goals ~token ~st
+    let handler =
+      HType.Immediate (fun ~token { Params.st } -> Agent.goals ~token ~st)
   end
 end
 
@@ -154,6 +172,7 @@ module Premises = struct
 
     module Response = Response
 
-    let handler ~token { Params.st } = Agent.premises ~token ~st
+    let handler =
+      HType.Immediate (fun ~token { Params.st } -> Agent.premises ~token ~st)
   end
 end

petanque/json_shell/protocol_shell.ml

@@ -21,7 +21,9 @@ module SetWorkspace = struct
       type t = unit [@@deriving yojson]
     end
 
-    let handler ~token { Params.debug; root } =
-      Petanque.Shell.set_workspace ~token ~debug ~root
+    let handler =
+      Protocol.HType.Immediate
+        (fun ~token { Params.debug; root } ->
+          Petanque.Shell.set_workspace ~token ~debug ~root)
   end
 end

petanque/json_shell/server.ml

@@ -9,6 +9,8 @@ let rq_info (r : Lsp.Base.Message.t) =
   | Response (Ok { id; _ } | Error { id; _ }) ->
     Format.asprintf "response for: %d" id
 
+let fn = Petanque.Shell.build_doc
+
 let rec handle_connection ~token ic oc () =
   try
     let* request = Lwt_io.read_line ic in
@@ -23,7 +25,7 @@ let rec handle_connection ~token ic oc () =
       let* () = Logs_lwt.info (fun m -> m "Received: %s" (rq_info request)) in
       (* request could be a notification, so maybe we don't have to do a
          reply! *)
-      match Interp.interp ~token request with
+      match Interp.interp ~fn ~token request with
       | None -> handle_connection ~token ic oc ()
       | Some reply ->
         let* () = Logs_lwt.info (fun m -> m "Sent reply") in

petanque/shell.ml

@@ -79,9 +79,7 @@ let setup_doc ~token env uri =
     Ok (Fleche.Doc.check ~io ~token ~target ~doc ())
   | Error err -> Error err
 
-let fn ~token uri =
-  let env = Option.get !env in
-  setup_doc ~token env uri
+let build_doc ~token ~uri = setup_doc ~token (Option.get !env) uri
 
 (* Flèche LSP backend handles the conversion at the protocol level *)
 let to_uri uri = Lang.LUri.of_string uri |> Lang.LUri.File.of_uri
@@ -97,5 +95,4 @@ let set_roots ~token ~debug ~roots =
 let init_agent ~token ~debug ~roots =
   init_st := Some (init_coq ~debug);
   Fleche.Io.CallBack.set io;
-  Agent.fn := fn;
   set_roots ~token ~debug ~roots

petanque/shell.mli

@@ -18,3 +18,8 @@ val set_workspace :
   -> debug:bool
   -> root:Lang.LUri.File.t
   -> unit Agent.R.t
+
+val build_doc :
+     token:Coq.Limits.Token.t
+  -> uri:Lang.LUri.File.t
+  -> (Fleche.Doc.t, Agent.Error.t) Result.t