did a bunch of stuff

2 files changed, 26 insertions, 0 deletions

diff --git a/bin/dune b/bin/dune
new file mode 100644
index 0000000..5e8e55c
--- /dev/null
+++ b/bin/dune
@@ -0,0 +1,4 @@
+(executable
+ (public_name power_prover)
+ (name main)
+ (libraries power_prover))
diff --git a/bin/main.ml b/bin/main.ml
new file mode 100644
index 0000000..eed1a7a
--- /dev/null
+++ b/bin/main.ml
@@ -0,0 +1,22 @@
+open Power_prover.Datatypes
+
+let show_example p i =
+  print_endline ("Proposition p:     " ^ (string_of_prop p));
+  print_endline ("p in NNF:          " ^ (string_of_prop (to_nnf p)));
+  print_endline ("Interpretation i:  " ^ (string_of_interpr i));
+  print_endline ("p under i:         " ^ (string_of_prop (interpret p i)) ^ "\n");;
+
+let p1 = Not(Not(Not(And(Lit "a", Lit "b"))));;
+let p2 = Iff(Not(Implies(Or(Lit "a", Lit "b"), And(Lit "b", Lit "c"))), True);;
+let i1 = [("a", false); ("b", true); ("c", false)];;
+let i2 = [("a", false); ("b", false)];;
+let i3 = [("c", true)];;
+
+let () =
+  show_example p1 i1;
+  show_example p1 i2;
+  show_example p1 i3;
+
+  show_example p2 i1;
+  show_example p2 i2;
+  show_example p2 i3;;