diff options
Diffstat (limited to 'lib/to_string.ml')
-rw-r--r-- | lib/to_string.ml | 44 |
1 files changed, 44 insertions, 0 deletions
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 |