diff options
Diffstat (limited to 'lib/to_string.ml')
| -rw-r--r-- | lib/to_string.ml | 24 |
1 files changed, 20 insertions, 4 deletions
diff --git a/lib/to_string.ml b/lib/to_string.ml index 30e909b..5d74adf 100644 --- a/lib/to_string.ml +++ b/lib/to_string.ml @@ -1,3 +1,5 @@ +(* Various to_string and print functions *) + open Types let rec string_of_prop = function @@ -8,23 +10,24 @@ let rec string_of_prop = function | 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) ^ ")";; + | 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) ^ "]";; + 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) ^ "]";; + in "[" ^ (stringify i) ^ "]" -let print_prop prop = print_endline (string_of_prop prop);; +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" @@ -42,3 +45,16 @@ let string_of_tok = function 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)) ^ "]]" |