feat: Eio conversion of reset, status, history

bin/dune

@@ -1,10 +1,25 @@
 (include_subdirs no)
 
 (executables
- (names test_http_api_eval test_http_api_instance test_http_api_verify)
+ (names
+  test_http_api_eval
+  test_http_api_instance
+  test_http_api_verify
+  test_eio)
  (public_names
   test_http_api_eval
   test_http_api_instance
-  test_http_api_verify)
- (libraries containers imandra_http_api_client eio eio_main lwt_eio)
- (modules test_http_api_eval test_http_api_instance test_http_api_verify))
+  test_http_api_verify
+  test_eio)
+ (libraries
+  containers
+  cohttp-eio
+  eio
+  imandra_http_api_client
+  eio_main
+  lwt_eio)
+ (modules
+  test_http_api_eval
+  test_http_api_instance
+  test_http_api_verify
+  test_eio))

bin/test_eio.ml

@@ -0,0 +1,30 @@
+module Log = (val Logs.src_log (Logs.Src.create "imandra-http-api-local"))
+
+let () =
+  let open Imandra_http_api_client in
+  Logs.set_reporter (Logs.format_reporter ());
+  Logs.set_level (Some Logs.Debug);
+  let config = Main_eio.Config.make ~base_uri:"http://127.0.0.1:3000" () in
+
+  let response http ~sw =
+    Log.debug (fun k -> k "Sending query to server...");
+    let result = Main_eio.reset config http ~sw in
+    match result with
+    | Ok st ->
+      Log.app (fun k ->
+          k "Got ok response: %a"
+            CCFormat.(some Api.Response.pp_capture)
+            st.capture)
+    | Error err ->
+      (match err with
+      | `Error_decoding_response err ->
+        Log.err (fun k ->
+            k "Decoding error: %a@." Decoders_yojson.Basic.Decode.pp_error err)
+      | `Error_response (code, _err) ->
+        Log.err (fun k ->
+            k "Error response: Code = %s" (Cohttp.Code.string_of_status code)))
+  in
+
+  Eio_main.run @@ fun env ->
+  let http = Cohttp_eio.Client.make ~https:None env#net in
+  Eio.Switch.run @@ fun sw -> response http ~sw

bin/test_http_api_eval.ml

@@ -1,4 +1,4 @@
-module Client = Imandra_http_api_client
+module Client = Imandra_http_api_client.Main
 module Api = Imandra_http_api_client.Api
 
 module Log = (val Logs.src_log (Logs.Src.create "imandra-http-api-local"))

bin/test_http_api_instance.ml

@@ -1,4 +1,4 @@
-module Client = Imandra_http_api_client
+module Client = Imandra_http_api_client.Main
 module Api = Imandra_http_api_client.Api
 
 let () = Printexc.record_backtrace true

bin/test_http_api_verify.ml

@@ -1,4 +1,4 @@
-module Client = Imandra_http_api_client
+module Client = Imandra_http_api_client.Main
 module Api = Imandra_http_api_client.Api
 
 let () = Printexc.record_backtrace true

src/api.ml

@@ -99,6 +99,7 @@ module Response = struct
     stderr: string;
     raw_stdio: string option;
   }
+  [@@deriving show]
 
   type model = {
     syntax: src_syntax;
@@ -454,11 +455,11 @@ module Encoders (E : D.Encode.S) = struct
     let eval_req_src (x : Request.eval_req_src) =
       obj [ "syntax", src_syntax x.syntax; "src", string x.src ]
 
-    let decomp_req_src (x : Request.decomp_req_src) = 
+    let decomp_req_src (x : Request.decomp_req_src) =
       obj
         ([ "name", string x.name; "prune", bool x.prune ]
-        |> append_opt_key "assuming" string x.assuming 
-        |> append_opt_key "max_rounds" int x.max_rounds 
+        |> append_opt_key "assuming" string x.assuming
+        |> append_opt_key "max_rounds" int x.max_rounds
         |> append_opt_key "stop_at" int x.stop_at)
   end
 

src/api.mli

@@ -91,6 +91,8 @@ module Response : sig
     raw_stdio: string option;
   }
 
+  val pp_capture : Format.formatter -> capture -> unit
+
   type model = {
     syntax: src_syntax;
     src: string;

src/dune

@@ -1,6 +1,8 @@
 (library
  (name imandra_http_api_client)
  (public_name imandra-http-api-client)
+ (preprocess
+  (pps ppx_deriving.show))
  (flags
   (:standard -w -27))
  (libraries

src/imandra_http_api_client.ml → src/main.ml

@@ -33,7 +33,7 @@ let default_headers (c : Config.t) =
 let make_body enc x =
   Decoders_yojson.Basic.Encode.encode_string enc x |> Cohttp_lwt.Body.of_string
 
-let read_response dec s=
+let read_response dec s =
   match
     Decoders_yojson.Basic.Decode.decode_string (D.Response.with_capture dec) s
   with
@@ -48,7 +48,7 @@ let read_error s =
   | Error e -> Error (`Error_decoding_response e)
 
 let read (dec : 'a Decoders_yojson.Basic.Decode.decoder) (resp, body) :
-    ('a Api.Response.with_capture, [> error ]) Lwt_result.t =
+    ('a Api.Response.with_capture, [> error ]) CCResult.t Lwt.t =
   let open Lwt.Syntax in
   let* body = Cohttp_lwt.Body.to_string body in
   let status = Cohttp.Response.status resp in

src/imandra_http_api_client.mli → src/main.mli

@@ -164,46 +164,55 @@ val read_error :
 val read :
   'a Decoders_yojson.Basic.Decode.decoder ->
   Cohttp.Response.t * Cohttp_lwt.Body.t ->
-  ('a Api.Response.with_capture, [> error] ) Lwt_result.t
+  ('a Api.Response.with_capture, [> error ]) Lwt_result.t
 
 val eval :
   Config.t ->
   Api.Request.eval_req_src ->
-  (Api.Response.eval_result Api.Response.with_capture, [> error]) result Lwt.t
+  (Api.Response.eval_result Api.Response.with_capture, [> error ]) result Lwt.t
 
 val get_history :
-  Config.t -> (string Api.Response.with_capture, [> error]) result Lwt.t
+  Config.t -> (string Api.Response.with_capture, [> error ]) result Lwt.t
 
 val get_status :
-  Config.t -> (string Api.Response.with_capture, [> error]) result Lwt.t
+  Config.t -> (string Api.Response.with_capture, [> error ]) result Lwt.t
 
 val instance_by_name :
   Config.t ->
   Api.Request.instance_req_name ->
-  (Api.Response.instance_result Api.Response.with_capture, [> error]) result Lwt.t
+  (Api.Response.instance_result Api.Response.with_capture, [> error ]) result
+  Lwt.t
 
 val instance_by_src :
   Config.t ->
   Api.Request.instance_req_src ->
-  (Api.Response.instance_result Api.Response.with_capture, [> error]) result Lwt.t
+  (Api.Response.instance_result Api.Response.with_capture, [> error ]) result
+  Lwt.t
 
 val reset :
-  Config.t -> unit -> (unit Api.Response.with_capture, [> error]) result Lwt.t
+  Config.t -> unit -> (unit Api.Response.with_capture, [> error ]) result Lwt.t
 
 val shutdown :
-  Config.t -> unit -> (string Api.Response.with_capture, [> error]) result Lwt.t
+  Config.t ->
+  unit ->
+  (string Api.Response.with_capture, [> error ]) result Lwt.t
 
 val verify_by_name :
   Config.t ->
   Api.Request.verify_req_name ->
-  (Api.Response.verify_result Api.Response.with_capture, [> error]) result Lwt.t
+  (Api.Response.verify_result Api.Response.with_capture, [> error ]) result
+  Lwt.t
 
 val verify_by_src :
   Config.t ->
   Api.Request.verify_req_src ->
-  (Api.Response.verify_result Api.Response.with_capture, [> error]) result Lwt.t
+  (Api.Response.verify_result Api.Response.with_capture, [> error ]) result
+  Lwt.t
 
 val decompose :
   Config.t ->
   Api.Request.decomp_req_src ->
-  (Yojson.Basic.t Api.Response.decompose_result Api.Response.with_capture, [> error]) result Lwt.t
+  ( Yojson.Basic.t Api.Response.decompose_result Api.Response.with_capture,
+    [> error ] )
+  result
+  Lwt.t

src/main_eio.ml

@@ -0,0 +1,93 @@
+module Config = struct
+  type t = {
+    base_uri: Uri.t;
+    auth_token: string option;
+  }
+
+  let make ?auth_token ~base_uri () =
+    { base_uri = Uri.of_string base_uri; auth_token }
+end
+
+module E = Api.Encoders (Decoders_yojson.Basic.Encode)
+module D = Api.Decoders (Decoders_yojson.Basic.Decode)
+
+type error =
+  [ `Error_response of
+    Cohttp.Code.status_code * Api.Response.error Api.Response.with_capture
+  | `Error_decoding_response of Decoders_yojson.Basic.Decode.error
+  ]
+
+let build_uri (c : Config.t) path = Uri.with_path c.base_uri path
+
+let default_headers (c : Config.t) =
+  let other_headers = [] in
+  let auth_header =
+    match c.auth_token with
+    | None -> []
+    | Some t -> [ "Authorization", Format.asprintf "Bearer %s" t ]
+  in
+  other_headers @ auth_header
+
+let make_body enc x : Cohttp_eio.Body.t =
+  Decoders_yojson.Basic.Encode.encode_string enc x |> Cohttp_eio.Body.of_string
+
+let read_response dec (s : Cohttp_eio.Body.t) =
+  match
+    Decoders_yojson.Basic.Decode.decode_string
+      (D.Response.with_capture dec)
+      (s |> Eio.Flow.read_all)
+  with
+  | Ok err -> Ok err
+  | Error e -> Error (`Error_decoding_response e)
+
+let read_error (s : Cohttp_eio.Body.t) =
+  match
+    Decoders_yojson.Basic.Decode.decode_string
+      D.Response.(with_capture error)
+      (s |> Eio.Flow.read_all)
+  with
+  | Ok err -> Ok err
+  | Error e -> Error (`Error_decoding_response e)
+
+let read (dec : 'a Decoders_yojson.Basic.Decode.decoder)
+    ((resp, body) : Http.Response.t * Cohttp_eio.Body.t) =
+  let status = Cohttp.Response.status resp in
+  if status = `OK then
+    read_response dec body |> CCResult.flat_map (fun ok -> Ok ok)
+  else
+    read_error body
+    |> CCResult.flat_map (fun err -> Error (`Error_response (status, err)))
+
+(* let net =
+   let open Eio.Std in
+   let net = Eio_mock.Net.make "mocknet" in
+   Eio_mock.Net.on_getaddrinfo net
+     [ `Return [ `Tcp (Eio.Net.Ipaddr.V4.loopback, 443) ] ];
+   let conn = Eio_mock.Flow.make "connection" in
+   Eio_mock.Net.on_connect net [ `Return conn ];
+   net *)
+
+(* let eval (c : Config.t) (req : Api.Request.eval_req_src) ~sw cl =
+   let uri = build_uri c "/eval/by-src" in
+   let headers = default_headers c |> Cohttp.Header.of_list in
+   let body = make_body E.Request.eval_req_src req in
+   (* let res = Cohttp_eio.Client.call ~headers ~body cl `POST uri ~sw in *)
+   let res = Cohttp_eio.Client.get ~headers cl ~sw uri in
+   read D.Response.eval_result res *)
+let get_history (c : Config.t) cl ~sw =
+  let uri = build_uri c "/history" in
+  let headers = default_headers c |> Cohttp.Header.of_list in
+  let res = Cohttp_eio.Client.get cl ~sw uri ~headers in
+  read Decoders_yojson.Basic.Decode.string res
+
+let get_status (c : Config.t) cl ~sw =
+  let uri = build_uri c "/status" in
+  let headers = default_headers c |> Cohttp.Header.of_list in
+  let res = Cohttp_eio.Client.get cl ~sw uri ~headers in
+  read Decoders_yojson.Basic.Decode.string res
+
+let reset (c : Config.t) cl ~sw =
+  let uri = build_uri c "/reset" in
+  let headers = default_headers c |> Cohttp.Header.of_list in
+  let res = Cohttp_eio.Client.call cl ~sw `POST uri ~headers in
+  read D.Response.reset_result res

tests/decompose.ml

@@ -1,4 +1,4 @@
-module Client = Imandra_http_api_client
+module Client = Imandra_http_api_client.Main
 
 let tests (module Log : Logs.LOG) : unit Alcotest_lwt.test_case list =
   [

tests/evaluation.ml

@@ -1,4 +1,4 @@
-module Client = Imandra_http_api_client
+module Client = Imandra_http_api_client.Main
 
 let tests (module Log : Logs.LOG) : unit Alcotest_lwt.test_case list =
   [

tests/instance.ml

@@ -1,4 +1,4 @@
-module Client = Imandra_http_api_client
+module Client = Imandra_http_api_client.Main
 
 let tests (module Log : Logs.LOG) : unit Alcotest_lwt.test_case list =
   [

tests/verification.ml

@@ -1,4 +1,4 @@
-module Client = Imandra_http_api_client
+module Client = Imandra_http_api_client.Main
 
 let tests (module Log : Logs.LOG) : unit Alcotest_lwt.test_case list =
   [