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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
|
(* Various to_string and print functions *)
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 string_of_x x = x |> string_of_x |> print_endline
let print_prop prop = print 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
let string_of_seq (Seq (p1s, p2s)) =
let p1_string = String.concat ", " (List.map string_of_prop p1s) in
let p2_string = String.concat ", " (List.map string_of_prop p2s) in
p1_string ^ " ⇒ " ^ p2_string
let rec string_of_stree = function
| Concl(s, []) -> "[" ^ string_of_seq s ^ "]"
| Concl(s, trees) -> "Seq(" ^ string_of_seq s ^ "| " ^ (String.concat "; " (List.map string_of_stree trees)) ^ ")"
let rec json_string_of_stree = function
| Concl(s, []) -> "[\"" ^ string_of_seq s ^ "\", []]"
| Concl(s, trees) -> "[\"" ^ string_of_seq s ^ "\", [" ^ (String.concat ", " (List.map json_string_of_stree trees)) ^ "]]"
|
