4 files changed, 132 insertions, 0 deletions
diff --git a/api/dune b/api/dune
new file mode 100644
index 0000000..9e9e824
--- /dev/null
+++ b/api/dune
@@ -0,0 +1,4 @@
+(library
+ (name api)
+ (libraries chadprover dream)
+ (preprocess (pps lwt_ppx ppx_yojson_conv)))
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
diff --git a/api/routes.ml b/api/routes.ml
new file mode 100644
index 0000000..74b78ae
--- /dev/null
+++ b/api/routes.ml
@@ -0,0 +1,21 @@
+(* Define the routes for our api *)
+
+open Handlers
+
+let routes = [
+
+  Dream.get "/health"
+    health_endpoint;
+
+  Dream.post "/validate_formula"
+    validate_formula_endpoint;
+
+  Dream.post "/satisfy"
+    satisfy_endpoint;
+
+  Dream.post "/sequent_proof"
+    sequent_proof_endpoint;
+
+  (* /tableau_calculus_proof *)
+
+]
diff --git a/api/startapp.ml b/api/startapp.ml
new file mode 100644
index 0000000..3b459d5
--- /dev/null
+++ b/api/startapp.ml
@@ -0,0 +1,26 @@
+
+(* Middleware to enable CORS for testing purposes *)
+let cors_middleware handler request =
+  let handlers =
+    [
+      "Allow", "OPTIONS, GET, HEAD, POST";
+      "Access-Control-Allow-Origin", "*";
+      "Access-Control-Allow-Methods", "OPTIONS, GET, HEAD, POST";
+      "Access-Control-Allow-Headers", "Content-Type";
+      "Access-Control-Max-Age", "86400"
+    ]
+  in
+
+  let%lwt res = handler request in
+  handlers
+  |> List.map (fun (key, value) -> Dream.add_header res key value)
+  |> ignore;
+  Lwt.return res
+
+  (* Create and start the app *)
+let startapp () =
+  Dream.run
+  @@ Dream.logger
+  (* @@ Dream.origin_referrer_check *)
+  @@ cors_middleware (* TODO: remove *)
+  @@ Dream.router Routes.routes