blob: 30e909be9af2b5988c98c4c21486ef15a5d82c1e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
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
|