[wip] Remove handling hook in favor of typed requests.

controller/lsp_core.ml

@@ -428,21 +428,19 @@ let do_changeConfiguration ~io params =
   ()
 
 (* 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_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)
 
 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 fn = petanque_fn in
   let handler ~token ~doc:_ =
-    Petanque_json.Interp.do_request ~token (module S) ~params
+    Petanque_json.Interp.do_request ~fn ~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
@@ -455,7 +453,8 @@ let petanque_handle_doc (module S : Petanque_json.Protocol.Request.S) ~params =
 
 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)
+  let fn = petanque_fn in
+  Rq.Action.now (Petanque_json.Interp.do_request ~fn ~token (module S) ~params)
 
 (* XXX: Deduplicate with Petanque_json.Protocol. *)
 let do_petanque ~token method_ params =
@@ -532,7 +531,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,14 @@ 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
-
 (** [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. *)
 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,10 +2,18 @@ open Protocol
 open Protocol_shell
 module A = Petanque.Agent
 
-let do_request ~token (module R : Protocol.Request.S) ~params =
+let do_request ~fn ~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
+    let res =
+      match R.Handler.handler with
+      | Immediate handler -> handler ~token params
+      | FullDoc { uri; handler } ->
+        let open Coq.Compat.Result.O in
+        let* doc = fn ~token ~uri in
+        handler ~token ~doc params
+    in
+    match res with
     | Ok result -> Ok (R.Handler.Response.to_yojson result)
     | Error err ->
       let message = Petanque.Agent.Error.to_string err in
@@ -29,20 +37,21 @@ let handle_request ~token ~method_ ~params =
   | s when String.equal Premises.method_ s ->
     do_request ~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 : 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 = Obj.magic 0
+        ; 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

petanque/test/basic_api.ml

@@ -25,9 +25,10 @@ let start ~token =
   let _ : _ Result.t = Petanque.Shell.init_agent ~token ~debug ~roots:[] in
   (* Twice to test for #766 *)
   let root, uri = prepare_paths () in
+  let* doc = Petanque.Shell.build_doc ~token ~uri in
   let* () = Petanque.Shell.set_workspace ~token ~debug ~root in
   let* () = Petanque.Shell.set_workspace ~token ~debug ~root in
-  Agent.start ~token ~uri ~thm:"rev_snoc_cons" ()
+  Agent.start ~token ~doc ~thm:"rev_snoc_cons" ()
 
 let extract_st (st : _ Agent.Run_result.t) =
   match st with