Merge pull request #18 from imandra-ai/john/decoders

Make the project compatible with Decoder 0.7, add a `make format` command

Author: hesterjeng

Makefile

@@ -34,4 +34,7 @@ _opam:
 opam-install-deps: _opam
 	opam install ./imandra-http-api-client.opam -y --deps-only
 
+format:
+	@dune build @fmt --auto-promote
+
 .PHONY: all clean watch tests

bin/dune

@@ -2,9 +2,6 @@
 
 (executables
  (names test_http_api_eval test_http_api_instance test_http_api_verify)
- (public_names
-  test_http_api_eval
-  test_http_api_instance
-  test_http_api_verify)
+ (public_names test_http_api_eval test_http_api_instance test_http_api_verify)
  (libraries containers imandra_http_api_client)
  (modules test_http_api_eval test_http_api_instance test_http_api_verify))

src/api.ml

@@ -454,11 +454,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

@@ -150,17 +150,17 @@ module Decoders : functor (D : Decoders.Decode.S) -> sig
   module Request : sig
     module Hints : sig
       module Induct : sig
-        val structural : (D.value, Request.Hints.Induct.t) D.t_let
+        val structural : Request.Hints.Induct.t D.decoder
 
-        val functional : (D.value, Request.Hints.Induct.t) D.t_let
+        val functional : Request.Hints.Induct.t D.decoder
 
-        val t : (D.value, Request.Hints.Induct.t) D.t_let
+        val t : Request.Hints.Induct.t D.decoder
       end
 
       module Method : sig
-        val unroll : (D.value, Request.Hints.Method.unroll) D.t_let
+        val unroll : Request.Hints.Method.unroll D.decoder
 
-        val ext_solver : (D.value, Request.Hints.Method.ext_solver) D.t_let
+        val ext_solver : Request.Hints.Method.ext_solver D.decoder
 
         val t : Request.Hints.Method.t D.decoder
       end

src/imandra_http_api_client.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

src/imandra_http_api_client.mli

@@ -85,22 +85,21 @@ module D : sig
     module Hints : sig
       module Induct : sig
         val structural :
-          (Yojson.Basic.t, Api.Request.Hints.Induct.t) Decoders.Decoder.t
+          Api.Request.Hints.Induct.t Decoders_yojson.Basic.Decode.decoder
 
         val functional :
-          (Yojson.Basic.t, Api.Request.Hints.Induct.t) Decoders.Decoder.t
+          Api.Request.Hints.Induct.t Decoders_yojson.Basic.Decode.decoder
 
-        val t : (Yojson.Basic.t, Api.Request.Hints.Induct.t) Decoders.Decoder.t
+        val t : Api.Request.Hints.Induct.t Decoders_yojson.Basic.Decode.decoder
       end
 
       module Method : sig
         val unroll :
-          (Yojson.Basic.t, Api.Request.Hints.Method.unroll) Decoders.Decoder.t
+          Api.Request.Hints.Method.unroll Decoders_yojson.Basic.Decode.decoder
 
         val ext_solver :
-          ( Yojson.Basic.t,
-            Api.Request.Hints.Method.ext_solver )
-          Decoders.Decoder.t
+          Api.Request.Hints.Method.ext_solver
+          Decoders_yojson.Basic.Decode.decoder
 
         val t : Api.Request.Hints.Method.t Decoders_yojson.Basic.Decode.decoder
       end
@@ -164,46 +163,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