[petanque] Rework protocol file as to expose internal details less.

petanque/json_shell/client.ml

@@ -48,22 +48,22 @@ let get_id () =
   !id_counter
 
 module Wrap (R : Protocol.Request.S) (C : Chans) : sig
-  val call : R.Params_.t -> (R.Response_.t, string) Result.t
+  val call : R.Params.t -> (R.Response.t, string) Result.t
 end = struct
   let trace = C.trace
   let message = C.message
 
   let call params =
     let id = get_id () in
     let method_ = R.method_ in
-    let params = Yojson.Safe.Util.to_assoc (R.Params_.to_yojson params) in
+    let params = Yojson.Safe.Util.to_assoc (R.Params.to_yojson params) in
     let request =
       Lsp.Base.Request.(make ~id ~method_ ~params () |> to_yojson)
     in
     let () = Lsp.Io.send_json C.oc request in
     read_response ~trace ~message C.ic |> fun r ->
     Result.bind r (function
-      | Ok { id = _; result } -> R.Response_.of_yojson result
+      | Ok { id = _; result } -> R.Response.of_yojson result
       | Error { id = _; code = _; message; data = _ } -> Error message)
 end
 

petanque/json_shell/client.mli

@@ -8,9 +8,9 @@ end
 open Protocol
 
 module S (C : Chans) : sig
-  val init : Init.Params_.t -> (Init.Response_.t, string) result
-  val start : Start.Params_.t -> (Start.Response_.t, string) result
-  val run_tac : RunTac.Params_.t -> (RunTac.Response_.t, string) result
-  val goals : Goals.Params_.t -> (Goals.Response_.t, string) result
-  val premises : Premises.Params_.t -> (Premises.Response_.t, string) result
+  val init : Init.Params.t -> (Init.Response.t, string) result
+  val start : Start.Params.t -> (Start.Response.t, string) result
+  val run_tac : RunTac.Params.t -> (RunTac.Response.t, string) result
+  val goals : Goals.Params.t -> (Goals.Response.t, string) result
+  val premises : Premises.Params.t -> (Premises.Response.t, string) result
 end

petanque/json_shell/interp.ml

@@ -2,11 +2,11 @@ open Protocol
 module A = Petanque.Agent
 
 let do_request ~token (module R : Request.S) ~id ~params =
-  match R.Params.of_yojson (`Assoc params) with
+  match R.Handler.Params.of_yojson (`Assoc params) with
   | Ok params -> (
-    match R.handler ~token params with
+    match R.Handler.handler ~token params with
     | Ok result ->
-      let result = R.Response.to_yojson result in
+      let result = R.Handler.Response.to_yojson result in
       Lsp.Base.Response.mk_ok ~id ~result
     | Error err ->
       let message = A.Error.to_string err in

petanque/json_shell/protocol.ml

@@ -3,35 +3,38 @@ 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 type Handler = sig
+  (* Server-side RPC specification *)
+  module Params : sig
+    type t [@@deriving of_yojson]
+  end
+
+  (* Server-side RPC specification *)
+  module Response : sig
+    type t [@@deriving to_yojson]
+  end
+
+  val handler : token:Coq.Limits.Token.t -> Params.t -> Response.t R.t
+end
+
 (* Note that here we follow JSON-RPC / LSP capitalization conventions *)
 module Request = struct
   module type S = sig
     val method_ : string
 
-    (* Would be good to remove this duplicity, but that would complicate the
-       server side setup which now is trivial. *)
-
-    (* Server-side params specification *)
+    (* Protocol params specification *)
     module Params : sig
-      type t [@@deriving of_yojson]
-    end
-
-    (* Client-side params specification *)
-    module Params_ : sig
-      type t [@@deriving to_yojson]
+      type t [@@deriving yojson]
     end
 
-    (* Server-side response specification *)
+    (* Protocol response specification *)
     module Response : sig
-      type t [@@deriving to_yojson]
-    end
-
-    (* Client-side response specification *)
-    module Response_ : sig
-      type t [@@deriving of_yojson]
+      type t [@@deriving yojson]
     end
 
-    val handler : token:Coq.Limits.Token.t -> Params.t -> Response.t R.t
+    module Handler : Handler
   end
 end
 
@@ -47,33 +50,26 @@ module Init = struct
     [@@deriving yojson]
   end
 
-  module Params_ = Params
-
   module Response = struct
-    type t = Env.t [@@deriving yojson]
-  end
-
-  module Response_ = struct
     type t = int [@@deriving yojson]
   end
 
-  let handler ~token { Params.debug; root } = Agent.init ~token ~debug ~root
+  module Handler = struct
+    module Params = Params
+
+    module Response = struct
+      type t = Env.t [@@deriving yojson]
+    end
+
+    let handler ~token { Params.debug; root } = Agent.init ~token ~debug ~root
+  end
 end
 
 (* start RPC *)
 module Start = struct
   let method_ = "petanque/start"
 
   module Params = struct
-    type t =
-      { env : Env.t
-      ; uri : Lsp.JLang.LUri.File.t
-      ; thm : string
-      }
-    [@@deriving yojson]
-  end
-
-  module Params_ = struct
     type t =
       { env : int
       ; uri : Lsp.JLang.LUri.File.t
@@ -83,30 +79,33 @@ module Start = struct
   end
 
   module Response = struct
-    type t = State.t [@@deriving yojson]
-  end
-
-  module Response_ = struct
     type t = int [@@deriving yojson]
   end
 
-  let handler ~token { Params.env; uri; thm } =
-    Agent.start ~token ~env ~uri ~thm
+  module Handler = struct
+    module Params = struct
+      type t =
+        { env : Env.t
+        ; uri : Lsp.JLang.LUri.File.t
+        ; thm : string
+        }
+      [@@deriving yojson]
+    end
+
+    module Response = struct
+      type t = State.t [@@deriving yojson]
+    end
+
+    let handler ~token { Params.env; uri; thm } =
+      Agent.start ~token ~env ~uri ~thm
+  end
 end
 
 (* run_tac RPC *)
 module RunTac = struct
   let method_ = "petanque/run"
 
   module Params = struct
-    type t =
-      { st : State.t
-      ; tac : string
-      }
-    [@@deriving yojson]
-  end
-
-  module Params_ = struct
     type t =
       { st : int
       ; tac : string
@@ -115,56 +114,70 @@ module RunTac = struct
   end
 
   module Response = struct
-    type t = State.t Run_result.t [@@deriving yojson]
-  end
-
-  module Response_ = struct
     type t = int Run_result.t [@@deriving yojson]
   end
 
-  let handler ~token { Params.st; tac } = Agent.run_tac ~token ~st ~tac
+  module Handler = struct
+    module Params = struct
+      type t =
+        { st : State.t
+        ; tac : string
+        }
+      [@@deriving yojson]
+    end
+
+    module Response = struct
+      type t = State.t Run_result.t [@@deriving yojson]
+    end
+
+    let handler ~token { Params.st; tac } = Agent.run_tac ~token ~st ~tac
+  end
 end
 
 (* goals RPC *)
 module Goals = struct
   let method_ = "petanque/goals"
 
   module Params = struct
-    type t = { st : State.t } [@@deriving yojson]
-  end
-
-  module Params_ = struct
     type t = { st : int } [@@deriving yojson]
   end
 
   module Response = struct
     type t = Goals.t [@@deriving yojson]
   end
 
-  module Response_ = Response
+  module Handler = struct
+    module Params = struct
+      type t = { st : State.t } [@@deriving yojson]
+    end
+
+    module Response = Response
 
-  let handler ~token { Params.st } = Agent.goals ~token ~st
+    let handler ~token { Params.st } = Agent.goals ~token ~st
+  end
 end
 
 (* premises RPC *)
 module Premises = struct
   let method_ = "petanque/premises"
 
   module Params = struct
-    type t = { st : State.t } [@@deriving yojson]
-  end
-
-  module Params_ = struct
     type t = { st : int } [@@deriving yojson]
   end
 
   module Response = struct
     type t = string list [@@deriving yojson]
   end
 
-  module Response_ = Response
+  module Handler = struct
+    module Params = struct
+      type t = { st : State.t } [@@deriving yojson]
+    end
+
+    module Response = Response
 
-  let handler ~token { Params.st } = Agent.premises ~token ~st
+    let handler ~token { Params.st } = Agent.premises ~token ~st
+  end
 end
 
 (* Notifications don't get a reply *)

petanque/test/json_api.ml

@@ -13,7 +13,7 @@ let trace ?verbose:_ msg = msgs := Format.asprintf "[trace] %s" msg :: !msgs
 let message ~lvl:_ ~message = msgs := message :: !msgs
 let dump_msgs () = List.iter (Format.eprintf "%s@\n") (List.rev !msgs)
 
-let extract_st (st : Protocol.RunTac.Response_.t) =
+let extract_st (st : Protocol.RunTac.Response.t) =
   match st with
   | Proof_finished st | Current_state st -> st
 

petanque/test/json_api_failure.ml

@@ -13,7 +13,7 @@ let trace ?verbose:_ msg = msgs := Format.asprintf "[trace] %s" msg :: !msgs
 let message ~lvl:_ ~message = msgs := message :: !msgs
 let dump_msgs () = List.iter (Format.eprintf "%s@\n") (List.rev !msgs)
 
-let extract_st (st : Protocol.RunTac.Response_.t) =
+let extract_st (st : Protocol.RunTac.Response.t) =
   match st with
   | Proof_finished st | Current_state st -> st