[petanque] Add TCP/IP pet-server

petanque/README.md

@@ -33,7 +33,7 @@ have three options:
 See the contributing guide for instructions on how to perform the last
 two.
 
-## Using `petanque`
+## Running `petanque` JSON shell
 
 You can use `petanque` in 2 different ways:
 
@@ -68,3 +68,47 @@ Please use one line per json input. json input examples are:
 
 Seems to work! (TM) (Famous last words)
 
+## Running `pet-server`
+
+After building Petanque, you can launch a TCP server with:
+```
+dune exec -- pet-server
+```
+
+Default address is 127.0.0.1 and default port is 8765.
+
+```
+❯ dune exec -- pet-server --help
+PET(1)                            Pet Manual                            PET(1)
+
+NAME
+       pet - Petanque Server
+
+SYNOPSIS
+       pet [--address=ADDRESS] [--backlog=BACKLOG] [--port=PORT] [OPTION]…
+
+DESCRIPTION
+       Launch a petanque server to interact with Coq
+
+USAGE
+       See the documentation on the project's webpage for more information
+
+OPTIONS
+       -a ADDRESS, --address=ADDRESS (absent=127.0.0.1)
+           address to listen to
+
+       -b BACKLOG, --backlog=BACKLOG (absent=10)
+           socket backlog
+
+       -p PORT, --port=PORT (absent=8765)
+           port to listen to
+
+COMMON OPTIONS
+       --help[=FMT] (default=auto)
+           Show this help in format FMT. The value FMT must be one of auto,
+           pager, groff or plain. With auto, the format is pager or plain
+           whenever the TERM env var is dumb or undefined.
+
+       --version
+           Show version information.
+```

petanque/json_shell/dune

@@ -1,7 +1,19 @@
-(executable
- (name pet)
- (public_name pet)
- (modules :standard)
+(library
+ (name petanque_json)
+ (public_name coq-lsp.petanque.json)
+ (modules :standard \ pet server)
  (preprocess
   (staged_pps ppx_import ppx_deriving_yojson))
- (libraries cmdliner lsp petanque))
+ (libraries petanque lsp))
+
+(executables
+ (names pet)
+ (public_names pet)
+ (modules pet)
+ (libraries cmdliner petanque_json))
+
+(executables
+ (names server)
+ (public_names pet-server)
+ (modules server)
+ (libraries logs.lwt lwt.unix petanque_json))

petanque/json_shell/pet.ml

@@ -1,5 +1,3 @@
-open Cmdliner
-
 (** example input / output sequence:
 
 {{{
@@ -25,6 +23,7 @@ open Cmdliner
  *)
 
 let rec loop () : unit =
+  let open Petanque_json in
   let token = Coq.Limits.Token.create () in
   try
     let line = read_line () in
@@ -49,6 +48,8 @@ let rec loop () : unit =
 
 let pet_main () = loop ()
 
+open Cmdliner
+
 let pet_cmd : unit Cmd.t =
   let doc = "Petanque Coq Environment" in
   let man =

petanque/json_shell/server.ml

@@ -0,0 +1,101 @@
+open Lwt
+open Lwt.Syntax
+
+let run_cmd line =
+  let open Petanque_json in
+  let token = Coq.Limits.Token.create () in
+  try
+    let json = Yojson.Safe.from_string line in
+    match Protocol.Command.of_yojson json with
+    | Error msg -> raise (Failure msg)
+    | Ok cmd ->
+      let answer = Interp.interp ~token cmd in
+      Yojson.Safe.to_string (Protocol.Answer.to_yojson answer)
+  with
+  | End_of_file ->
+    "Error: End of file" (* if the input does not match the format. *)
+  | Scanf.Scan_failure msg (* if a conversion to a number is not possible. *)
+  | Failure msg (* if the format string is invalid. *)
+  | Invalid_argument msg -> "Error: " ^ msg
+
+let rec handle_connection ic oc () =
+  let* line = Lwt_io.read_line_opt ic in
+  match line with
+  | Some line ->
+    let* () = Logs_lwt.info (fun m -> m "Received: %s" line) in
+    let reply = run_cmd line in
+    let* () = Logs_lwt.info (fun m -> m "Reply: %s" reply) in
+    Lwt_io.write_line oc reply >>= handle_connection ic oc
+  | None ->
+    let* () = Logs_lwt.info (fun m -> m "Connection closed") in
+    Lwt_io.write_line oc "Connection closed" >>= return
+
+let accept_connection conn =
+  let fd, _ = conn in
+  let ic = Lwt_io.of_fd ~mode:Lwt_io.Input fd in
+  let oc = Lwt_io.of_fd ~mode:Lwt_io.Output fd in
+  let* () = Logs_lwt.info (fun m -> m "New connection") in
+  Lwt.on_failure (handle_connection ic oc ()) (fun e ->
+      Logs.err (fun m -> m "%s" (Printexc.to_string e)));
+  return ()
+
+let create_socket ~address ~port ~backlog =
+  let open Lwt_unix in
+  let sock = socket PF_INET SOCK_STREAM 0 in
+  ( bind sock @@ ADDR_INET (Unix.inet_addr_of_string address, port) |> fun x ->
+    ignore x );
+  listen sock backlog;
+  sock
+
+let create_server sock =
+  let rec serve () =
+    let* conn = Lwt_unix.accept sock in
+    let* () = accept_connection conn in
+    serve ()
+  in
+  serve
+
+let pet_main address port backlog =
+  let () = Logs.set_reporter (Logs.format_reporter ()) in
+  let () = Logs.set_level (Some Logs.Info) in
+  let sock = create_socket ~address ~port ~backlog in
+  let serve = create_server sock in
+  Lwt_main.run @@ serve ()
+
+open Cmdliner
+
+let address =
+  let doc = "address to listen to" in
+  Arg.(
+    value & opt string "127.0.0.1"
+    & info [ "a"; "address" ] ~docv:"ADDRESS" ~doc)
+
+let port =
+  let doc = "port to listen to" in
+  Arg.(value & opt int 8765 & info [ "p"; "port" ] ~docv:"PORT" ~doc)
+
+let backlog =
+  let doc = "socket backlog" in
+  Arg.(value & opt int 10 & info [ "b"; "backlog" ] ~docv:"BACKLOG" ~doc)
+
+let pet_cmd : unit Cmd.t =
+  let doc = "Petanque Server" in
+  let man =
+    [ `S "DESCRIPTION"
+    ; `P "Launch a petanque server to interact with Coq"
+    ; `S "USAGE"
+    ; `P
+        "See\n\
+        \    the\n\
+        \  documentation on the project's webpage for more information"
+    ]
+  in
+  let version = Fleche.Version.server in
+  let pet_term = Term.(const pet_main $ address $ port $ backlog) in
+  Cmd.(v (Cmd.info "pet" ~version ~doc ~man) pet_term)
+
+let main () =
+  let ecode = Cmd.eval pet_cmd in
+  exit ecode
+
+let () = main ()