diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index 2e63d5a7..3ebe9b0f 100644 --- a/controller/lsp_core.ml +++ b/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 *) diff --git a/petanque/agent.ml b/petanque/agent.ml index a8378a35..d531396e 100644 --- a/petanque/agent.ml +++ b/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 diff --git a/petanque/agent.mli b/petanque/agent.mli index 21b7902a..d0a908e3 100644 --- a/petanque/agent.mli +++ b/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 diff --git a/petanque/json_shell/interp.ml b/petanque/json_shell/interp.ml index 94f13454..623f2ca1 100644 --- a/petanque/json_shell/interp.ml +++ b/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 diff --git a/petanque/json_shell/pet.ml b/petanque/json_shell/pet.ml index 2ac03546..ab1e1216 100644 --- a/petanque/json_shell/pet.ml +++ b/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 diff --git a/petanque/json_shell/protocol.ml b/petanque/json_shell/protocol.ml index 69223560..42a743e8 100644 --- a/petanque/json_shell/protocol.ml +++ b/petanque/json_shell/protocol.ml @@ -1,3 +1,4 @@ +open Lang open Petanque (* Serialization for agent types *) @@ -5,6 +6,15 @@ 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 diff --git a/petanque/json_shell/protocol_shell.ml b/petanque/json_shell/protocol_shell.ml index 55d2be3d..918d482b 100644 --- a/petanque/json_shell/protocol_shell.ml +++ b/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 diff --git a/petanque/json_shell/server.ml b/petanque/json_shell/server.ml index 2a35cb7b..de1b11f9 100644 --- a/petanque/json_shell/server.ml +++ b/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 diff --git a/petanque/shell.ml b/petanque/shell.ml index 490c5012..524e2ed5 100644 --- a/petanque/shell.ml +++ b/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 diff --git a/petanque/shell.mli b/petanque/shell.mli index 2b57dc76..a4409062 100644 --- a/petanque/shell.mli +++ b/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 diff --git a/petanque/test/basic_api.ml b/petanque/test/basic_api.ml index ae4dbc8b..42707098 100644 --- a/petanque/test/basic_api.ml +++ b/petanque/test/basic_api.ml @@ -27,7 +27,10 @@ let start ~token = let root, uri = prepare_paths () 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" () + (* Careful to call [build_doc] before we have set an environment! [pet] and + [pet-server] are careful to always set a default one *) + let* doc = Petanque.Shell.build_doc ~token ~uri in + Agent.start ~token ~doc ~thm:"rev_snoc_cons" () let extract_st (st : _ Agent.Run_result.t) = match st with