added a functional parser

1 files changed, 32 insertions, 0 deletions

diff --git a/lib/types.ml b/lib/types.ml
new file mode 100644
index 0000000..bf6a34d
--- /dev/null
+++ b/lib/types.ml
@@ -0,0 +1,32 @@
+(* Data types useful for our theorem prover *)
+
+(* logical proposition *)
+type proposition =
+  | True
+  | False
+  | Lit of string
+  | Not of proposition
+  | And of proposition * proposition
+  | Or of proposition * proposition
+  | Implies of proposition * proposition
+  | Iff of proposition * proposition
+
+(* interpretation of propositional symbols *)
+type interpretation = (string * bool) list
+
+(* allows us to substitute any proposition for any atomic literal *)
+type substitution = (string * proposition) list
+
+(* tokens used by lexer and parser *)
+type tok =
+  | TRUE
+  | FALSE
+  | LIT of string
+  | NOT
+  | AND
+  | OR
+  | IMPLIES
+  | IFF
+  | LEFT_PAREN
+  | RIGHT_PAREN
+  | SKIP