added a functional parser

10 files changed, 621 insertions, 0 deletions

diff --git a/lib/lexing/headers.ml b/lib/lexing/headers.ml
new file mode 100644
index 0000000..2452eec
--- /dev/null
+++ b/lib/lexing/headers.ml
@@ -0,0 +1,23 @@
+(* Types for lexing *)
+
+open Types
+
+(* Exceptions to aid control flow for lexer *)
+exception Not_In_Alphabet of char
+exception No_Transition of int * char
+
+(* Tagged Deterministice Finite Automaton *)
+type tdfa = {
+  alphabet : char list;
+  start_state: int;
+  register_init : tok; (* initial contents of the single register for this TDFA *)
+  delta : int * char -> int * (tok -> tok)
+}
+
+(* Description of a possible state that the TDFA could be in *)
+type tdfa_state = {
+  state_id : int;         (* current state *)
+  register : tok;         (* contents of register *)
+  tokens : tok list;      (* tokens emitted so far *)
+  to_parse : char list;   (* characters left to parse *)
+}
diff --git a/lib/lexing/lexer.ml b/lib/lexing/lexer.ml
new file mode 100644
index 0000000..af24e49
--- /dev/null
+++ b/lib/lexing/lexer.ml
@@ -0,0 +1,97 @@
+(* Lexer for transforming an input string into a list of tokens *)
+
+open Types
+open Headers
+open Utils
+
+(*
+  Ordered lexer rules:
+
+  true            => TRUE         [1,2,3,4]
+  false           => FALSE        [5,6,7,8,9]
+  [a-zA-Z]+ as s  => LIT s        [10]
+  ¬               => NOT          [11]
+  ∧               => AND          [12]
+  ∨               => OR           [13]
+  →               => IMPLIES      [14]
+  ↔               => IFF          [15]
+  (               => LEFT_PAREN   [16]
+  )               => RIGHT_PAREN  [17]
+  [ \t\n]         => SKIP         [18]
+*)
+
+(* Define a TDFA *)
+let my_tdfa : tdfa =
+  let my_alphabet =
+    let lowercase = List.init 26 (fun i -> Char.chr (Char.code 'a' + i)) in
+    let uppercase = List.init 26 (fun i -> Char.chr (Char.code 'A' + i)) in
+    ['!'; '&'; '|'; '>'; '='; '('; ')'; ' '; '\t'; '\n'] @ lowercase @ uppercase
+  in
+
+  let my_delta (i, c) =
+    if
+      not (List.mem c my_alphabet)
+    then
+      raise (Not_In_Alphabet c)
+    else
+      let append_lit = function
+          | LIT s -> LIT (s ^ Char.escaped c)
+          | _ -> LIT (Char.escaped c)
+      in
+
+      let is_ltr c =
+        let ascii = Char.code c in
+        (65 <= ascii && ascii <= 90) || (97 <= ascii && ascii <= 122)
+      in
+
+      match i, c with
+      | 0, '!'                  -> 11, (fun _ -> NOT)
+      | 0, '&'                  -> 12, (fun _ -> AND)
+      | 0, '|'                  -> 13, (fun _ -> OR)
+      | 0, '>'                  -> 14, (fun _ -> IMPLIES)
+      | 0, '='                  -> 15, (fun _ -> IFF)
+      | 0, '('                  -> 16, (fun _ -> LEFT_PAREN)
+      | 0, ')'                  -> 17, (fun _ -> RIGHT_PAREN)
+      | 0, ' '                  -> 18, (fun _ -> SKIP)
+      | 0, '\t'                 -> 18, (fun _ -> SKIP)
+      | 0, '\n'                 -> 18, (fun _ -> SKIP)
+      | 0, 't'                  -> 1, append_lit
+      | 0, 'f'                  -> 5, append_lit
+      | 0, c when is_ltr c      -> 10, append_lit
+      | 1, 'r'                  -> 2, append_lit
+      | 1, c when is_ltr c      -> 10, append_lit
+      | 2, 'u'                  -> 3, append_lit
+      | 2, c when is_ltr c      -> 10, append_lit
+      | 3, 'e'                  -> 4, (fun _ -> TRUE)
+      | 3, c when is_ltr c      -> 10, append_lit
+      | 4, c when is_ltr c      -> 10, (fun _ -> (LIT ("true" ^ Char.escaped c)))
+      | 5, 'a'                  -> 6, append_lit
+      | 5, c when is_ltr c      -> 10, append_lit
+      | 6, 'l'                  -> 7, append_lit
+      | 6, c when is_ltr c      -> 10, append_lit
+      | 7, 's'                  -> 8, append_lit
+      | 7, c when is_ltr c      -> 10, append_lit
+      | 8, 'e'                  -> 9, (fun _ -> FALSE)
+      | 8, c when is_ltr c      -> 10, append_lit
+      | 9, c when is_ltr c      -> 10, (fun _ -> (LIT ("false" ^ Char.escaped c)))
+      | 10, c when is_ltr c     -> 10, append_lit
+      | _                       -> raise (No_Transition (i, c))
+  in
+
+  {
+    alphabet = my_alphabet;
+    start_state = 0;
+    register_init = SKIP;
+    delta = my_delta
+  }
+
+
+let lex (s : string) : tok list =
+  let to_parse = s |> String.to_seq |> List.of_seq in
+  let initial_tdfa_state = {
+    state_id = my_tdfa.start_state;
+    register = my_tdfa.register_init;
+    tokens = [];
+    to_parse = to_parse
+  } in
+  driver my_tdfa initial_tdfa_state
diff --git a/lib/lexing/utils.ml b/lib/lexing/utils.ml
new file mode 100644
index 0000000..aa218f5
--- /dev/null
+++ b/lib/lexing/utils.ml
@@ -0,0 +1,36 @@
+open Types
+open Headers
+
+(* Function for stepping through a TDFA computation *)
+let step (automaton : tdfa) (state : tdfa_state) : tdfa_state =
+  match state.to_parse with
+  | [] -> state
+  | c :: cs ->
+    try
+      let next_state_id, f = automaton.delta (state.state_id, c) in
+      let next_tok = f state.register in
+      {
+        state_id = next_state_id;
+        register = next_tok;
+        tokens = state.tokens;
+        to_parse = cs
+      }
+    with (No_Transition (_, c)) ->
+      let token_to_add = state.register in
+      let next_state_id, f = automaton.delta (0, c) in
+      let next_tok = f SKIP in
+      {
+        state_id = next_state_id;
+        register = next_tok;
+        tokens = if token_to_add <> SKIP then token_to_add :: state.tokens else state.tokens;
+        to_parse = cs
+      }
+
+(* Driver to perform a TDFA computation *)
+let rec driver (automaton : tdfa) (state: tdfa_state) : tok list =
+  if
+    state.to_parse = []
+  then
+    List.rev (state.register :: state.tokens) (* ensure that final tag is emitted *)
+  else
+    driver automaton (step automaton state)
diff --git a/lib/lib_utils.ml b/lib/lib_utils.ml
new file mode 100644
index 0000000..e9a67b8
--- /dev/null
+++ b/lib/lib_utils.ml
@@ -0,0 +1,93 @@
+(* Utility functions for dealing with our new data types *)
+
+open Types
+
+
+(* Converts an interpretation to a substitution *)
+let rec sub_of_interpr = function
+  | [] -> []
+  | (s, b) :: tl -> (s, if b then True else False) :: (sub_of_interpr tl);;
+
+(* Removes instances of True or False literals via simplification *)
+let rec simplify_true_false = function
+  | True -> True
+  | False -> False
+  | Lit symbol -> Lit symbol
+  | Not p ->
+    (match simplify_true_false p with
+    | True -> False
+    | False -> True
+    | Not p' -> p'
+    | p' -> Not(p'))
+  | And (p1, p2) ->
+    (match simplify_true_false p1, simplify_true_false p2 with
+    | False, _ -> False
+    | _, False -> False
+    | True, p2' -> p2'
+    | p1', True -> p1'
+    | p1', p2' -> And(p1', p2'))
+  | Or (p1, p2) ->
+    (match simplify_true_false p1, simplify_true_false p2 with
+    | True, _ -> True
+    | _, True -> True
+    | False, p2' -> p2'
+    | p1', False -> p1'
+    | p1', p2' -> Or(p1', p2'))
+  | Implies (p1, p2) ->
+    (match simplify_true_false p1, simplify_true_false p2 with
+    | False, _ -> True
+    | True, p2' -> p2'
+    | p1', p2' -> Implies(p1', p2'))
+  | Iff (p1, p2) ->
+    (match simplify_true_false p1, simplify_true_false p2 with
+    | True, p2' -> p2'
+    | p1', True -> p1'
+    | False, p2' -> simplify_true_false (Not(p2'))
+    | p1', False -> simplify_true_false (Not(p1'))
+    | p1', p2' -> Iff(p1', p2'));;
+
+(* Finds a symbol in a list of substitutions and returns the value to substitute for that symbol *)
+let rec replace sub symbol =
+  match sub with
+  | [] -> Lit symbol
+  | (s, value) :: sub -> if s = symbol then value else replace sub symbol;;
+
+(* Substitutes propositions for symbols as specified by the sub argument *)
+let rec substitute (prop : proposition) (sub : substitution) =
+  match prop with
+  | True -> True
+  | False -> False
+  | Lit s -> replace sub s
+  | Not p -> Not (substitute p sub)
+  | And(p1, p2) -> And(substitute p1 sub, substitute p2 sub)
+  | Or(p1, p2) -> Or(substitute p1 sub, substitute p2 sub)
+  | Implies(p1, p2) -> Implies(substitute p1 sub, substitute p2 sub)
+  | Iff(p1, p2) -> And(substitute p1 sub, substitute p2 sub);;
+
+(* Converts a proposition to negation normal form *)
+let to_nnf prop =
+  let rec to_nnf = function
+    | True -> True
+    | False -> False
+    | Lit symbol -> Lit symbol
+    | Not p ->
+      (match to_nnf p with
+      | And(p1, p2) -> Or(to_nnf (Not(p1)), to_nnf (Not(p2)))
+      | Or(p1, p2) -> And(to_nnf (Not(p1)), to_nnf (Not(p2)))
+      | p' -> simplify_true_false (Not p'))
+    | And(p1, p2) -> And(to_nnf p1, to_nnf p2)
+    | Or(p1, p2) -> Or(to_nnf p1, to_nnf p2)
+    | Implies(p1, p2) -> to_nnf (Or(Not(p1), p2))
+    | Iff(p1, p2) -> to_nnf (And(Implies(p1, p2), Implies(p2, p1)))
+  in
+  simplify_true_false (to_nnf prop);;
+
+(* Applies an interpretation to a proposition and returns the resulting proposition *)
+let interpret prop i = simplify_true_false (substitute prop (sub_of_interpr i));;
+
+(* Tests whether a proposition holds under a given interpretation *)
+let test_interpretation prop i =
+  match interpret prop i with
+  | True -> Some true
+  | False -> Some false
+  | _ -> None;; (* return None if cannot be determined *)
diff --git a/lib/parsing/headers.ml b/lib/parsing/headers.ml
new file mode 100644
index 0000000..8d63381
--- /dev/null
+++ b/lib/parsing/headers.ml
@@ -0,0 +1,74 @@
+(* Useful types for parsing *)
+
+open Types
+
+exception Parse_Error of string
+
+type terminal = tok
+
+type nonterminal = S | E | E' | F | F' | G | G' | H | H' | I
+
+type symbol = Nt of nonterminal | Tm of terminal
+
+type production = nonterminal * (symbol list)
+
+(* possible actions to take when LL parsing *)
+type action =
+  | PREDICT of production
+  | MATCH of tok
+  | ACCEPT
+  | REJECT
+
+(* takes in top stack symbol and the next input token and selects action to take *)
+type table = symbol -> tok -> action
+
+(* mutable abstract syntax tree *)
+type ast =
+  | Br of symbol * (ast ref) list
+  | Lf of symbol
+
+(* parsing state *)
+type state = {
+  stack : symbol list;
+  ast_stack : ast ref list; (* list of ast refs corresponding to symbols on the stack *)
+  input : tok list;
+  finished : bool;
+  accepted : bool
+}
+
+(* convert ast to proposition *)
+let rec prop_of_ast (tree : ast) : proposition =
+  match tree with
+  | Lf (Tm TRUE) -> True
+  | Lf (Tm FALSE) -> False
+  | Lf (Tm (LIT s)) -> Lit s
+  | Br (Nt S, e_ref :: _) -> prop_of_ast !e_ref
+  | Br (Nt I, _ :: e_ref :: _ :: _) -> prop_of_ast !e_ref (* I ::= LEFT_PAREN E RIGHT_PAREN *)
+  | Br (Nt I, _ :: i_ref :: _) -> let inner_prop = prop_of_ast !i_ref in Not(inner_prop) (* I ::=  NOT I *)
+  | Br (Nt I, [some_ref]) -> (* I ::= TRUE | FALSE | LIT s *)
+    begin
+      match !some_ref with
+      | Lf (Tm TRUE) -> True
+      | Lf (Tm FALSE) -> False
+      | Lf (Tm (LIT s)) -> Lit s
+      | _ -> failwith "some bug"
+    end
+  | Br (Nt a, b_ref :: a'_ref :: _) -> (* A ::= B A' *)
+    begin
+      match !a'_ref with
+      | Lf _ -> prop_of_ast !b_ref (* A' ::= eps *)
+      | Br (_, _ :: tl) -> (* A' ::=  CONNECTOR B A' *)
+        let left = prop_of_ast !b_ref in
+        let right = prop_of_ast (Br(Nt a, tl)) in
+        begin
+          match a with
+          | E -> Iff(left, right)
+          | F -> Implies(left, right)
+          | G -> Or(left, right)
+          | H -> And(left, right)
+          | _ -> failwith "a bug!"
+        end
+      | _ -> failwith "another bug"
+    end
+  | _ -> failwith "found a bug!"
+  
\ No newline at end of file
diff --git a/lib/parsing/parser.ml b/lib/parsing/parser.ml
new file mode 100644
index 0000000..e56411b
--- /dev/null
+++ b/lib/parsing/parser.ml
@@ -0,0 +1,81 @@
+open Types
+open Headers
+open Utils
+
+let my_productions : production list = (* currently not in use *)
+  [
+    (S, [Nt E; Tm (LIT "$")]);    (* S ::= E $ *)
+    (E, [Nt F; Nt E']);
+    (E', [Tm IFF; Nt F; Nt E']);
+    (E', []);
+    (F, [Nt G; Nt F']);
+    (F', [Tm IMPLIES; Nt G; Nt F']);
+    (F', []);
+    (G, [Nt H; Nt G']);
+    (G', [Tm OR; Nt H; Nt G']);
+    (G', []);
+    (H, [Nt I; Nt H']);
+    (H', [Tm AND; Nt I; Nt H']);
+    (H', []);
+    (I, [Tm NOT; Nt I]);
+    (I, [Tm LEFT_PAREN; Nt E; Tm RIGHT_PAREN]);
+    (I, [Tm TRUE]);
+    (I, [Tm FALSE]);
+    (I, [Tm (LIT "any string")])
+  ]
+
+
+let my_action_table (sym : symbol) (tk : tok) : action =
+  let predict_if_in_first tk prod =
+    match tk with
+    | TRUE -> PREDICT prod
+    | FALSE -> PREDICT prod
+    | LIT _ -> PREDICT prod
+    | NOT -> PREDICT prod
+    | LEFT_PAREN -> PREDICT prod
+    | _ -> REJECT
+  in
+
+  let predict_if_in_follow tk follow prod =
+    if List.mem tk follow then
+      PREDICT prod
+    else
+      REJECT
+  in
+
+  match sym, tk with
+  | Tm (LIT "$"), LIT "$" -> ACCEPT
+  | Tm t, tk -> if t = tk then MATCH t else REJECT
+  | Nt S, tk -> predict_if_in_first tk (S, [Nt E; Tm (LIT "$")])
+  | Nt E, tk -> predict_if_in_first tk (E, [Nt F; Nt E'])
+  | Nt E', IFF -> PREDICT (E', [Tm IFF; Nt F; Nt E'])
+  | Nt E', tk -> predict_if_in_follow tk [LIT "$"; RIGHT_PAREN] (E', [])
+  | Nt F, tk -> predict_if_in_first tk (F, [Nt G; Nt F'])
+  | Nt F', IMPLIES -> PREDICT (F', [Tm IMPLIES; Nt G; Nt F'])
+  | Nt F', tk -> predict_if_in_follow tk [IFF; LIT "$"; RIGHT_PAREN] (F', [])
+  | Nt G, tk -> predict_if_in_first tk (G, [Nt H; Nt G'])
+  | Nt G', OR -> PREDICT (G', [Tm OR; Nt H; Nt G'])
+  | Nt G', tk -> predict_if_in_follow tk [IMPLIES; IFF; LIT "$"; RIGHT_PAREN] (G', [])
+  | Nt H, tk -> predict_if_in_first tk (H, [Nt I; Nt H'])
+  | Nt H', AND -> PREDICT (H', [Tm AND; Nt I; Nt H'])
+  | Nt H', tk -> predict_if_in_follow tk [OR; IMPLIES; IFF; LIT "$"; RIGHT_PAREN] (H', [])
+  | Nt I, NOT -> PREDICT (I, [Tm NOT; Nt I]);
+  | Nt I, LEFT_PAREN -> PREDICT (I, [Tm LEFT_PAREN; Nt E; Tm RIGHT_PAREN]);
+  | Nt I, TRUE -> PREDICT (I, [Tm TRUE]);
+  | Nt I, FALSE -> PREDICT (I, [Tm FALSE]);
+  | Nt I, LIT s when s <> "$" -> PREDICT (I, [Tm (LIT s)])
+  | _ -> REJECT
+
+
+let parse (input : tok list) =
+  let root = ref (Lf (Nt S)) in
+  let initial_parse_state = {
+    stack = [Nt S];
+    ast_stack = [root]; (* list of ast refs corresponding to symbols on the stack *)
+    input = input @ [LIT "$"];
+    finished = false;
+    accepted = false
+  } in
+  driver initial_parse_state my_action_table;
+  (* print_endline (string_of_ast (!root)); *)
+  prop_of_ast !root
diff --git a/lib/parsing/utils.ml b/lib/parsing/utils.ml
new file mode 100644
index 0000000..61211f0
--- /dev/null
+++ b/lib/parsing/utils.ml
@@ -0,0 +1,69 @@
+open Headers
+open To_string
+
+(* to string functions for debugging *)
+let string_of_nt = function
+  | S -> "S"
+  | E -> "E"
+  | E' -> "E'"
+  | F -> "F"
+  | F' -> "F'"
+  | G -> "G"
+  | G' -> "G'"
+  | H -> "H"
+  | H' -> "H'"
+  | I -> "I"
+
+let string_of_symbol = function
+  | Tm x -> string_of_tok x
+  | Nt x -> string_of_nt x
+
+let rec string_of_symbols = function
+  | [] -> ""
+  | sym :: xs -> "[" ^ string_of_symbol sym ^ "] " ^ string_of_symbols xs
+
+let print_state st =
+  print_endline ("stack: " ^ (string_of_symbols st.stack));
+  print_endline (" input: " ^ (string_of_tokens st.input))
+
+let rec string_of_ast = function
+  | Br (sym, ars) -> "Br(" ^ string_of_symbol sym ^ "| " ^ (String.concat ", " (List.map (fun ar -> string_of_ast !ar) ars))  ^ ")"
+  | Lf sym -> "(" ^ string_of_symbol sym ^ ")"
+
+(* step through parse states *)
+let step (parse_state : state) (action_table : table) =
+  (*print_state parse_state; currently printing the trace *)
+  match parse_state.stack, parse_state.ast_stack, parse_state.input with
+  | x::xs, t::ts, i::is -> (
+      match action_table x i with
+      | ACCEPT -> {stack = xs; ast_stack = ts; input = is; finished = true; accepted = true}
+      | REJECT -> {stack = xs; ast_stack = ts; input = is; finished = true; accepted = false}
+      | MATCH _ -> {stack = xs; ast_stack = ts; input = is; finished = false; accepted = false}
+      | PREDICT (_, l) ->
+        let update_ast_ref sym = (* for each symbol in the production, create an ast ref *)
+          let new_lf = ref (Lf sym) in
+          (match !t with
+          | Lf t_sym -> t := Br (t_sym, [new_lf])
+          | Br (t_sym, l) -> t := Br(t_sym, l @ [new_lf]));
+          new_lf
+        in
+        {
+          stack = l @ xs; (* add production symbols to symbol stack *)
+          ast_stack = List.map update_ast_ref l @ ts; (* update t's contents and add new refs to ast_stack *)
+          input = i :: is;
+          finished = false;
+          accepted = false
+        }
+    )
+  | xs, ts, is -> {stack = xs; ast_stack = ts; input = is; finished = true; accepted = false}
+
+(* driver function to perform multistepping *)
+let rec driver (parse_state : state) (action_table : table) : unit =
+  if parse_state.finished then
+    if parse_state.accepted then
+      ()
+    else
+      raise (Parse_Error "Input rejected")
+  else
+    driver (step parse_state action_table) action_table
+  
\ No newline at end of file
diff --git a/lib/sequent_calculus/sequents.ml b/lib/sequent_calculus/sequents.ml
new file mode 100644
index 0000000..0b4a33a
--- /dev/null
+++ b/lib/sequent_calculus/sequents.ml
@@ -0,0 +1,72 @@
+
+(* Sequent Calculus *)
+
+open Types
+open To_string
+
+
+type seq = Seq of proposition list * proposition list;; (* sequent *)
+
+type stree = (* tree of sequents *)
+  | Taut (* tautology of the form A, Gamma => A, Delta *)
+  | Br of stree * stree
+
+let string_of_seq (Seq (p1, p2)) =
+  let rec string_of_prop_list = function
+    | [] -> ""
+    | p :: ps -> (string_of_prop p) ^ ", " ^ (string_of_prop_list ps)
+  in
+  (string_of_prop_list p1) ^ "⇒" ^ (string_of_prop_list p2);;
+
+(* let rec reduce_seq s =
+  let rec not_lhs (Seq(p1s, p2s)) =
+    match p1s with
+    | [] -> Seq(p1s, p2s), None, false
+    | p::ps ->
+      (match p with
+      | Not(p') -> Seq(ps, p'::p2s), None, true
+      | _ -> let Seq(ps', p2s), _, found = not_lhs (Seq(ps, p2s)) in Seq(p::ps', p2s), None, found)
+  in
+  let rec not_rhs (Seq(p1s, p2s)) =
+    match p2s with
+    | [] -> Seq(p1s, p2s), None, false
+    | p::ps ->
+      (match p with
+      | Not(p') -> Seq(p'::p1s, ps), None, true
+      | _ -> let Seq(p1s, ps'), _, found = not_rhs (Seq(p1s, ps)) in Seq(p1s, p::ps'), None, found)
+  in
+  let rec and_lhs (Seq(p1s, p2s)) =
+    match p1s with
+    | [] -> Seq(p1s, p2s), None, false
+    | p::ps ->
+      (match p with
+      | And(p1, p2) -> Seq(p1::p2::ps, p2s), None, true
+      | _ -> let Seq(p1s, ps'), _, found = and_lhs (Seq(p1s, ps)) in Seq(p1s, p::ps'), None, found)
+  in
+  let rec and_rhs (Seq(p1s, p2s)) =
+    match p2s with
+    | [] -> Seq(p1s, p2s), None, false
+    | p::ps ->
+      (match p with
+      | And(p1, p2) -> Seq(p1s, p1::ps), Some (Seq(p1s, p2::ps)), true
+      | _ ->
+        (match and_rhs (Seq(p1s, ps)) with
+        | Seq(p1s, ps'), None, found -> Seq(p1s, p2s), None, false
+        | Seq(p1s, ps'), Some (Seq(p1s', ps'')), found -> Seq(p1s, p::ps'), Some (Seq(p1s', p::ps'')), true))
+  in
+  match s with
+  | Seq  *)
+
+  (*
+  Steps (repeat in this order):
+  - reduce AND on LHS
+  - reduce OR on RHS
+  - reduce NOT on LHS
+  - reduce NOT on RHS
+  - reduce -> (RHS)
+  - reduce <-> (both)
+  - reduce OR (LHS)
+  - reduce AND (RHS)
+  - reduce -> (LHS)
+  *)
+  
\ No newline at end of file
diff --git a/lib/to_string.ml b/lib/to_string.ml
new file mode 100644
index 0000000..30e909b
--- /dev/null
+++ b/lib/to_string.ml
@@ -0,0 +1,44 @@
+open Types
+
+let rec string_of_prop = function
+  | True -> "True"
+  | False -> "False"
+  | Lit symbol -> symbol
+  | Not p -> "¬" ^ (string_of_prop p)
+  | And (p1, p2) -> "(" ^ (string_of_prop p1) ^ " ∧ " ^ (string_of_prop p2) ^ ")"
+  | Or (p1, p2) -> "(" ^ (string_of_prop p1) ^ " ∨ " ^ (string_of_prop p2) ^ ")"
+  | Implies (p1, p2) -> "(" ^ (string_of_prop p1) ^ " → " ^ (string_of_prop p2) ^ ")"
+  | Iff (p1, p2) -> "(" ^ (string_of_prop p1) ^ " ↔ " ^ (string_of_prop p2) ^ ")";;
+
+  let string_of_sub sub =
+    let rec stringify = function
+      | [] -> ""
+      | (s, value) :: [] -> "(" ^ s ^ ": " ^ (string_of_prop value) ^ ")"
+      | (s, value) :: tl -> "(" ^ s ^ ": " ^ (string_of_prop value) ^ "), " ^ (stringify tl)
+    in "[" ^ (stringify sub) ^ "]";;
+
+let string_of_interpr (i : interpretation) =
+  let rec stringify = function
+    | [] -> ""
+    | (s, value) :: [] -> "(" ^ s ^ ": " ^ (string_of_bool value) ^ ")"
+    | (s, value) :: tl -> "(" ^ s ^ ": " ^ (string_of_bool value) ^ "), " ^ (stringify tl)
+  in "[" ^ (stringify i) ^ "]";;
+
+let print_prop prop = print_endline (string_of_prop prop);;
+
+let string_of_tok = function
+  | TRUE -> "TRUE"
+  | FALSE -> "FALSE"
+  | LIT s -> "LIT " ^ s
+  | NOT -> "NOT"
+  | AND -> "AND"
+  | OR -> "OR"
+  | IMPLIES -> "IMPLIES"
+  | IFF -> "IFF"
+  | LEFT_PAREN -> "LEFT_PAREN"
+  | RIGHT_PAREN -> "RIGHT_PAREN"
+  | SKIP -> "SKIP"
+
+let rec string_of_tokens = function
+  | [] -> ""
+  | t :: ts -> "[" ^ string_of_tok t ^ "] " ^ string_of_tokens ts
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