diff options
| author | filip <“filip.rabiega@gmail.com”> | 2024-08-16 14:11:00 +0200 |
|---|---|---|
| committer | filip <“filip.rabiega@gmail.com”> | 2024-08-16 14:11:00 +0200 |
| commit | 69de932f9116b30adfd689d38e35ace63aef0e2d (patch) | |
| tree | f7e8621889d313e70186ef255fcf04fe0d55d4c3 /bin/main.ml | |
| parent | 2e893fd0df7dae8c4ae843d4a23acb098dd97aff (diff) | |
| download | chadprover-69de932f9116b30adfd689d38e35ace63aef0e2d.tar.gz chadprover-69de932f9116b30adfd689d38e35ace63aef0e2d.tar.bz2 chadprover-69de932f9116b30adfd689d38e35ace63aef0e2d.zip | |
Diffstat (limited to 'bin/main.ml')
| -rw-r--r-- | bin/main.ml | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/bin/main.ml b/bin/main.ml index 19dd333..10a6bc3 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -1,4 +1,16 @@ +(* Entry point for this web application *) + +(* open Chadprover.Types *) +open Chadprover.To_string +(* open Chadprover.Lib_utils *) +open Chadprover.Lexing.Lexer +open Chadprover.Parsing.Parser +(* open Chadprover.Satisfiability.Satisfiable *) + let () = - Dream.run (fun _ -> - Dream.html "Sup yall!" - ) + let lex_result = lex "(p > (q > (p > p)))" in (* "a & b & c = z > x & y | c" *) + let parse_result = parse lex_result in + let proof = Chadprover.Sequent_calculus.Sequent_proof.prove_sequent (Seq([], [parse_result])) in + print string_of_stree proof + +let () = Api.Startapp.startapp () |