Merge pull request #770 from ejgallego/petanque_http

[petanque] Improvements on protocol handling

CHANGES.md

@@ -39,6 +39,9 @@
  - [petanque] New parameter `pre_commands` to `start` which allows
    instrumenting the goal before starting the proof (@ejgallego, Alex
    Sanchez-Stern #769)
+ - [petanque] New `http_headers={yes,no}` parameter for `pet` json
+   shell, plus some improvements on protocol handling (@ejgallego,
+   #770)
 
 # coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_...
 ----------------------------------------------------

petanque/agent.ml

@@ -12,10 +12,13 @@ module State = struct
 
   let hash = Coq.State.hash
   let equal = Coq.State.equal
+  let name = "state"
 end
 
 module Env = struct
   type t = Fleche.Doc.Env.t
+
+  let name = "env"
 end
 
 (** Petanque errors *)

petanque/agent.mli

@@ -10,13 +10,16 @@
 module State : sig
   type t
 
+  val name : string
   val hash : t -> int
   val equal : t -> t -> bool
 end
 
 module Env : sig
   (** Coq Workspaces / project enviroments *)
   type t
+
+  val name : string
 end
 
 (** Petanque errors *)

petanque/json_shell/interp.ml

@@ -35,12 +35,16 @@ let handle_request ~token ~id ~method_ ~params =
     let message = "method not found" in
     Lsp.Base.Response.mk_error ~id ~code ~message
 
-let interp ~token (r : Lsp.Base.Message.t) : Lsp.Base.Response.t option =
+let interp ~token (r : Lsp.Base.Message.t) : Lsp.Base.Message.t option =
   match r with
   | Request { id; method_; params } ->
     let response = handle_request ~token ~id ~method_ ~params in
-    Some response
-  | Notification { method_ = _; params = _ } -> None
-  | Response _ ->
-    (* XXX: to implement *)
-    None
+    Some (Lsp.Base.Message.response response)
+  | Notification { method_; params = _ } ->
+    let message = "unhandled notification: " ^ method_ in
+    let log = Trace.(make Params.{ message; verbose = None }) in
+    Some log
+  | Response (Ok { id; _ }) | Response (Error { id; _ }) ->
+    let message = "unhandled response: " ^ string_of_int id in
+    let log = Trace.(make Params.{ message; verbose = None }) in
+    Some log

petanque/json_shell/obj_map.ml

@@ -1,4 +1,6 @@
 module type Obj = sig
+  val name : string
+
   type t
   (* Not yet *)
   (* val equal : t -> t -> bool *)
@@ -32,12 +34,13 @@ module Make (O : Obj) : S with type t = O.t = struct
     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 to_obj (id : int) : (O.t, _) Result.t =
+    match Memo.find_opt memo id with
+    | Some v -> Ok v
+    | None ->
+      if false then dump_memo ();
+      Error (Format.asprintf "key %d for object %s not found" id O.name)
 
-  let of_yojson json = _t_of_yojson json |> Result.map to_obj
+  let of_yojson json = _t_of_yojson json |> fun r -> Result.bind r to_obj
   let to_yojson st : Yojson.Safe.t = of_obj st |> _t_to_yojson
 end

petanque/json_shell/pet.ml

@@ -1,16 +1,40 @@
 (* json rpc server *)
 open Petanque_json
 
+let use_http_headers = ref true
+
+let read_json inc =
+  match Yojson.Safe.from_channel inc with
+  | json -> Ok json
+  | exception Yojson.Json_error err -> Error err
+
+let read_message inc =
+  if !use_http_headers then Lsp.Io.read_message inc
+  else
+    try
+      match read_json inc with
+      | Error err -> Some (Error err)
+      | Ok json -> Some (Lsp.Base.Message.of_yojson json)
+    with End_of_file -> None
+
+let send_message msg =
+  if !use_http_headers then (
+    Lsp.Io.send_message Format.std_formatter msg;
+    Format.pp_print_flush Format.std_formatter ())
+  else
+    let msg = Lsp.Base.Message.to_yojson msg in
+    Format.fprintf Format.std_formatter "@[%s@]@\n%!"
+      (Yojson.Safe.to_string ?std:None msg)
+(* Format.fprintf Format.std_formatter "@[%a@]@\n%!" Yojson.Safe.pretty_print
+   msg *)
+
 let interp ~token request =
   match Interp.interp ~token request with
   | None -> ()
-  | Some response ->
-    let message = Lsp.Base.Message.response response in
-    Lsp.Io.send_message Format.std_formatter message;
-    Format.pp_print_flush Format.std_formatter ()
+  | Some message -> send_message message
 
 let rec loop ~token : unit =
-  match Lsp.Io.read_message stdin with
+  match read_message stdin with
   | None -> () (* EOF *)
   | Some (Ok request) ->
     interp ~token request;
@@ -21,40 +45,43 @@ let rec loop ~token : unit =
 
 let trace_notification hdr ?extra msg =
   let module M = Protocol.Trace in
-  let method_ = M.method_ in
   let message = Format.asprintf "[%s] %s" hdr msg in
   let params = { M.Params.message; verbose = extra } in
-  let params = M.Params.to_yojson params |> Yojson.Safe.Util.to_assoc in
-  let notification =
-    Lsp.Base.(Notification.(make ~method_ ~params () |> Message.notification))
-  in
-  Lsp.Io.send_message Format.std_formatter notification
+  let notification = M.make params in
+  send_message notification
 
 let message_notification ~lvl ~message =
   let module M = Protocol.Message in
-  let method_ = M.method_ in
   let type_ = Fleche.Io.Level.to_int lvl in
-  let params = M.Params.({ type_; message } |> to_yojson) in
-  let params = Yojson.Safe.Util.to_assoc params in
-  let notification =
-    Lsp.Base.(Notification.(make ~method_ ~params () |> Message.notification))
-  in
-  Lsp.Io.send_message Format.std_formatter notification
+  let params = M.Params.{ type_; message } in
+  let notification = M.make params in
+  send_message notification
 
 let trace_enabled = true
 
-let pet_main debug roots =
+let pet_main debug roots http_headers =
   Coq.Limits.start ();
   (* Don't trace for now *)
   if trace_enabled then (
     Petanque.Agent.trace_ref := trace_notification;
     Petanque.Agent.message_ref := message_notification);
   let token = Coq.Limits.Token.create () in
   let () = Utils.set_roots ~token ~debug ~roots in
+  use_http_headers := http_headers;
   loop ~token
 
 open Cmdliner
 
+let http_headers : bool Term.t =
+  let docv = "{yes|no}" in
+  let opts = [ ("yes", true); ("no", false) ] in
+  let absent = "yes" in
+  let doc =
+    "whether http-headers CONTENT-LENGHT are used in the JSON-RPC encoding"
+  in
+  Arg.(
+    value & opt (enum opts) true & info [ "http_headers" ] ~docv ~doc ~absent)
+
 let pet_cmd : unit Cmd.t =
   let doc = "Petanque Coq Environment" in
   let man =
@@ -66,7 +93,7 @@ let pet_cmd : unit Cmd.t =
   in
   let version = Fleche.Version.server in
   let pet_term =
-    Term.(const pet_main $ Coq.Args.debug $ Coq.Args.roots)
+    Term.(const pet_main $ Coq.Args.debug $ Coq.Args.roots $ http_headers)
     (* const pet_main $ roots $ display $ debug $ plugins $ file $ coqlib *)
     (* $ coqcorelib $ ocamlpath $ rload_path $ load_path $ rifrom) *)
   in

petanque/json_shell/protocol.ml

@@ -206,6 +206,10 @@ module Trace = struct
       }
     [@@deriving yojson]
   end
+
+  let make params =
+    let params = Params.to_yojson params |> Yojson.Safe.Util.to_assoc in
+    Lsp.Base.Message.Notification { method_; params }
 end
 
 (* Message notification *)
@@ -219,4 +223,8 @@ module Message = struct
       }
     [@@deriving yojson]
   end
+
+  let make params =
+    let params = Params.to_yojson params |> Yojson.Safe.Util.to_assoc in
+    Lsp.Base.Message.Notification { method_; params }
 end

petanque/json_shell/server.ml

@@ -29,7 +29,7 @@ let rec handle_connection ~token ic oc () =
         let* () = Logs_lwt.info (fun m -> m "Sent reply") in
         let* () =
           Lwt_io.fprintl oc
-            (Yojson.Safe.to_string (Lsp.Base.Response.to_yojson reply))
+            (Yojson.Safe.to_string (Lsp.Base.Message.to_yojson reply))
         in
         handle_connection ~token ic oc ())
   with End_of_file -> return ()