api/handlers.ml


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
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