added apiHEADmaster

1 files changed, 81 insertions, 0 deletions

diff --git a/api/handlers.ml b/api/handlers.ml
new file mode 100644
index 0000000..2b8ac5b
--- /dev/null
+++ b/api/handlers.ml
@@ -0,0 +1,81 @@
+(* Handlers for the different endpoints *)
+
+open Ppx_yojson_conv_lib.Yojson_conv.Primitives
+open Chadprover.Exports
+
+type post_request_data = {
+  data : string;
+} [@@deriving yojson]
+
+type interpretation = {
+  assignment : (string * bool) list option;
+} [@@deriving yojson]
+
+let get_data d = d.data
+
+let health_endpoint _ =
+  {|{"status": "pass"}|}
+  |> Dream.json
+
+let validate_formula_endpoint request =
+  let%lwt body = Dream.body request in
+
+  let input =
+    body
+    |> Yojson.Safe.from_string
+    |> post_request_data_of_yojson
+    |> get_data
+  in
+
+  try
+    input
+    |> parse_input
+    |> Chadprover.To_string.string_of_prop
+    |> fun s -> "{\"is_formula\": true, \"formula\": \"" ^ s ^ "\"}"
+    |> Dream.json
+
+  with _ -> (* TODO: 400 Bad Request, error message *)
+    "{\"is_formula\": false, \"formula\": \"" ^ input ^ "\"}"
+    |> Dream.json
+
+let satisfy_endpoint request =
+  let%lwt body = Dream.body request in
+
+  let input =
+    body
+    |> Yojson.Safe.from_string
+    |> post_request_data_of_yojson
+    |> get_data
+    |> parse_input
+    |> find_satisfying_interpretation
+  in
+
+  { assignment = input; }
+  |> yojson_of_interpretation
+  |> Yojson.Safe.to_string
+  |> Dream.json
+
+let sequent_proof_endpoint request =
+  let%lwt body = Dream.body request in
+
+  let seq_proof =
+    body
+    |> Yojson.Safe.from_string
+    |> post_request_data_of_yojson
+    |> get_data
+    |> parse_input
+    |> get_sequent_calculus_proof
+  in
+
+  let json_string =
+    begin
+      match seq_proof with
+      | None -> {|{"is_provable": "false"}|}
+      | Some tree ->
+          let s = Chadprover.To_string.json_string_of_stree tree in
+          {|{"is_provable": "true", "sequent_proof": |} ^ s ^ "}"
+    end
+  in
+
+  json_string
+  |> Dream.json