[petanque] Add a JSON-RPC shell

compiler/fcc.ml

@@ -25,10 +25,6 @@ let fcc_main int_backend roots display debug plugins files coqlib coqcorelib
 
 (****************************************************************************)
 (* Specific to fcc *)
-let roots : string list Term.t =
-  let doc = "Workspace(s) root(s)" in
-  Arg.(value & opt_all string [] & info [ "root" ] ~docv:"ROOTS" ~doc)
-
 let display : Args.Display.t Term.t =
   let doc = "Verbosity display settings" in
   let dparse =

coq/args.ml

@@ -89,3 +89,7 @@ let int_backend =
     value
     & opt (enum [ ("Coq", Limits.Coq); ("Mp", Limits.Mp) ]) Limits.Coq
     & info [ "int_backend" ] ~docv:"INT_BACKEND" ~doc)
+
+let roots : string list Term.t =
+  let doc = "Workspace(s) root(s)" in
+  Arg.(value & opt_all string [] & info [ "root" ] ~docv:"ROOTS" ~doc)

coq/args.mli

@@ -17,3 +17,4 @@ val bt : Bool.t Term.t
 val ml_include_path : string list Term.t
 val ri_from : (string option * string) list Term.t
 val int_backend : Limits.backend Term.t
+val roots : string list Term.t

lsp/base.ml

@@ -22,6 +22,7 @@
 module J = Yojson.Safe
 module U = Yojson.Safe.Util
 
+let int_field name dict = U.to_int List.(assoc name dict)
 let string_field name dict = U.to_string List.(assoc name dict)
 
 let odict_field ~default name dict =
@@ -63,6 +64,40 @@ module Message = struct
     | Notification { params; _ } | Request { params; _ } -> params
 end
 
+module Response = struct
+  type t =
+    | Ok of
+        { id : int
+        ; result : Yojson.Safe.t
+        }
+    | Error of
+        { id : int
+        ; code : int
+        ; message : string
+        ; data : Yojson.Safe.t option
+        }
+
+  let of_yojson msg =
+    try
+      let dict = U.to_assoc msg in
+      let id = int_field "id" dict in
+      (match List.assoc_opt "error" dict with
+      | Some error ->
+        let error = U.to_assoc error in
+        let code = int_field "message" error in
+        let message = string_field "message" error in
+        let data = None in
+        Error { id; code; message; data }
+      | None ->
+        let result = List.assoc "result" dict in
+        Ok { id; result })
+      |> Result.ok
+    with
+    | Not_found -> Error ("missing parameter: " ^ J.to_string msg)
+    | U.Type_error (msg, obj) ->
+      Error (Format.asprintf "msg: %s; obj: %s" msg (J.to_string obj))
+end
+
 let mk_reply ~id ~result =
   `Assoc [ ("jsonrpc", `String "2.0"); ("id", `Int id); ("result", result) ]
 
@@ -73,6 +108,14 @@ let mk_request_error ~id ~code ~message =
     ; ("error", `Assoc [ ("code", `Int code); ("message", `String message) ])
     ]
 
+let mk_request ~method_ ~id ~params =
+  `Assoc
+    [ ("jsonrpc", `String "2.0")
+    ; ("id", `Int id)
+    ; ("method", `String method_)
+    ; ("params", params)
+    ]
+
 let mk_notification ~method_ ~params =
   `Assoc
     [ ("jsonrpc", `String "2.0")

lsp/base.mli

@@ -35,6 +35,27 @@ module Message : sig
   val params : t -> (string * Yojson.Safe.t) list
 end
 
+(* Request response *)
+module Response : sig
+  type t =
+    | Ok of
+        { id : int
+        ; result : Yojson.Safe.t
+        }
+    | Error of
+        { id : int
+        ; code : int
+        ; message : string
+        ; data : Yojson.Safe.t option
+        }
+
+  val of_yojson : Yojson.Safe.t -> (t, string) Result.t
+end
+
+(** Build request *)
+val mk_request :
+  method_:string -> id:int -> params:Yojson.Safe.t -> Yojson.Safe.t
+
 (** Build notification *)
 val mk_notification : method_:string -> params:Yojson.Safe.t -> Yojson.Safe.t
 

lsp/io.ml

@@ -157,3 +157,11 @@ let rec read_request ic =
     | Error msg ->
       trace "read_request" ("error: " ^ msg);
       read_request ic)
+
+let read_response ic =
+  match read_raw_request ic with
+  | None -> None (* EOF *)
+  | Some com ->
+    if Fleche.Debug.read then trace_object "read" com;
+    Some (Base.Response.of_yojson com)
+  | exception ReadError err -> Some (Error err)

lsp/io.mli

@@ -23,9 +23,12 @@ val set_log_fn : (Yojson.Safe.t -> unit) -> unit
 (** Read a JSON-RPC request from channel *)
 val read_raw_request : in_channel -> Yojson.Safe.t option
 
-(** [None] signals [EOF] *)
+(** [None] signals [EOF], else [ReadError] *)
 val read_request : in_channel -> Base.Message.t option
 
+(** [None] signals [EOF] *)
+val read_response : in_channel -> (Base.Response.t, string) Result.t option
+
 exception ReadError of string
 
 (** Send a JSON-RPC request to channel *)

lsp/jCoq.ml

@@ -50,13 +50,20 @@ module Goals = struct
 
     let to_ { Coq.Goals.goals; stack; bullet; shelf; given_up } =
       { goals; stack; bullet; shelf; given_up }
+
+    let of_ { goals; stack; bullet; shelf; given_up } =
+      { Coq.Goals.goals; stack; bullet; shelf; given_up }
   end
 
   type ('a, 'pp) goals = ('a, 'pp) Coq.Goals.goals
 
   let goals_to_yojson f pp g = Goals_.to_ g |> Goals_.to_yojson f pp
 
-  type 'pp reified_pp = ('pp reified_goal, 'pp) goals [@@deriving to_yojson]
+  let goals_of_yojson f pp j =
+    let open Ppx_deriving_yojson_runtime in
+    Goals_.of_yojson f pp j >|= Goals_.of_
+
+  type 'pp reified_pp = ('pp reified_goal, 'pp) goals [@@deriving yojson]
 end
 
 module Ast = struct

petanque/README.md

@@ -35,5 +35,52 @@ two.
 
 ## Using `petanque`
 
-To use `petanque`, you need to some form of shell, or you can just
-call the API directly from your OCaml program.
+You can use `petanque` in 2 different ways:
+
+- call the API directly from your OCaml program
+- use the provided `pet` JSON-RPC shell
+
+to execute the `pet` JSON-RPC shell do:
+```
+make
+dune exec -- rlwrap %{bin:pet}
+```
+
+`rlwrap` is just a convenience, if your dune version is too old and
+don't recognize the `%{bin:pet}` form, you can just do `dune exec -- pet`.
+
+### Petanque options
+
+Petanque can be initalized from the command line by passing the `--root` parameter to it:
+```
+make
+dune exec -- rlwrap %{bin:pet} --root=/absolute/path/to/my/project
+```
+
+NOTE: If you use this option, you should not call `Init`!
+
+### A first example:
+
+Please use one line per json input. json input examples are:
+```json
+["Init",{"debug": false,"root":"file:///home/egallego/research/coq-lsp/examples/"}]
+["Init",["Ok",1]]
+
+["Start",{"env":1,"uri": "file:///home/egallego/research/coq-lsp/examples/ex0.v","thm":"addnC"}]
+["Start",["Ok",1]]
+
+["Run_tac", {"st": 1, "tac": "induction n."}]
+["Run_tac", ["Ok", 2]]
+
+["Run_tac", {"st": 2, "tac": "simpl."}]
+["Run_tac", 3]
+
+["Run_tac", {"st": 3, "tac": "auto."}]
+["Run_tac",4]
+
+["Premises", {"st": 2}]
+["Premises", ...]
+```
+
+Seems to work! (TM) (Famous last words)
+

petanque/agent.ml

@@ -33,6 +33,14 @@ module Error = struct
     | Coq msg -> Format.asprintf "Coq: %s" msg
     | Anomaly msg -> Format.asprintf "Anomaly: %s" msg
     | Theorem_not_found msg -> Format.asprintf "Theorem_not_found: %s" msg
+
+  (* JSON-RPC server reserved codes *)
+  let to_code = function
+    | Interrupted -> -32001
+    | Parsing _ -> -32002
+    | Coq _ -> -32003
+    | Anomaly _ -> -32004
+    | Theorem_not_found _ -> -32005
 end
 
 module R = struct

petanque/agent.mli

@@ -29,6 +29,7 @@ module Error : sig
     | Theorem_not_found of string
 
   val to_string : t -> string
+  val to_code : t -> int
 end
 
 (** Petanque results *)

petanque/json_shell/dune

@@ -0,0 +1,13 @@
+(library
+ (name petanque_json)
+ (public_name coq-lsp.petanque.json)
+ (modules :standard \ pet)
+ (preprocess
+  (staged_pps ppx_import ppx_deriving_yojson))
+ (libraries cmdliner lsp petanque))
+
+(executable
+ (name pet)
+ (public_name pet)
+ (modules pet)
+ (libraries petanque_json))

petanque/json_shell/interp.ml

@@ -0,0 +1,42 @@
+open Protocol
+module A = Petanque.Agent
+
+let do_request ~token (module R : Request.S) ~id ~params =
+  match R.Params.of_yojson (`Assoc params) with
+  | Ok params -> (
+    match R.handler ~token params with
+    | Ok result ->
+      let result = R.Response.to_yojson result in
+      Lsp.Base.mk_reply ~id ~result
+    | Error err ->
+      let message = A.Error.to_string err in
+      let code = A.Error.to_code err in
+      Lsp.Base.mk_request_error ~id ~code ~message)
+  | Error message ->
+    (* JSON-RPC Parse error *)
+    let code = -32700 in
+    Lsp.Base.mk_request_error ~id ~code ~message
+
+let handle_request ~token ~id ~method_ ~params =
+  match method_ with
+  | s when String.equal Init.method_ s ->
+    do_request ~token (module Init) ~id ~params
+  | s when String.equal Start.method_ s ->
+    do_request ~token (module Start) ~id ~params
+  | s when String.equal RunTac.method_ s ->
+    do_request ~token (module RunTac) ~id ~params
+  | s when String.equal Goals.method_ s ->
+    do_request ~token (module Goals) ~id ~params
+  | s when String.equal Premises.method_ s ->
+    do_request ~token (module Premises) ~id ~params
+  | _ ->
+    (* JSON-RPC method not found *)
+    let code = -32601 in
+    let message = "method not found" in
+    Lsp.Base.mk_request_error ~id ~code ~message
+
+let interp ~token (r : Lsp.Base.Message.t) : Yojson.Safe.t option =
+  match r with
+  | Request { id; method_; params } ->
+    Some (handle_request ~token ~id ~method_ ~params)
+  | Notification { method_ = _; params = _ } -> None

petanque/json_shell/jAgent.ml

@@ -0,0 +1,25 @@
+(* Serialization for agent types *)
+
+(* Implement State.t and Env.t serialization methods *)
+module State = Obj_map.Make (Petanque.Agent.State)
+module Env = Obj_map.Make (Petanque.Agent.Env)
+
+(* The typical protocol dance *)
+
+module Result = struct
+  include Result
+
+  type ('a, 'e) t = [%import: ('a, 'e) Result.t] [@@deriving yojson]
+end
+
+module Error = struct
+  type t = [%import: Petanque.Agent.Error.t] [@@deriving yojson]
+end
+
+module R = struct
+  type 'a t = [%import: 'a Petanque.Agent.R.t] [@@deriving yojson]
+end
+
+module Goals = struct
+  type t = string Lsp.JCoq.Goals.reified_pp option [@@deriving yojson]
+end

petanque/json_shell/obj_map.ml

@@ -0,0 +1,43 @@
+module type Obj = sig
+  type t
+  (* Not yet *)
+  (* val equal : t -> t -> bool *)
+end
+
+module type S = sig
+  type t [@@deriving yojson]
+end
+
+module Make (O : Obj) : S with type t = O.t = struct
+  type t = O.t
+  type _t = int [@@deriving yojson]
+
+  module Memo = Hashtbl.Make (Int)
+
+  let memo = Memo.create 1000
+
+  let dump_memo () =
+    let keys = Memo.to_seq_keys memo |> List.of_seq in
+    Format.(eprintf "@[size: %d@]@\n%!" (List.length keys));
+    Format.(eprintf "@[<v>%a@]@\n%!" (pp_print_list pp_print_int) keys)
+
+  let last_id = ref 0
+
+  let mk_id _ =
+    incr last_id;
+    !last_id
+
+  let of_obj (s : O.t) : int =
+    let id = mk_id s in
+    let () = Memo.add memo id s in
+    id
+
+  let to_obj (id : int) : O.t =
+    try Memo.find memo id
+    with Not_found ->
+      dump_memo ();
+      raise Not_found
+
+  let of_yojson json = _t_of_yojson json |> Result.map to_obj
+  let to_yojson st : Yojson.Safe.t = of_obj st |> _t_to_yojson
+end