pretty printing

lib/formula.ml

@@ -44,3 +44,65 @@ let rec occurs t = function
   | Iff (phi, psi) -> occurs t phi || occurs t psi
   | Forall phi -> occurs (Term.inc_var t) phi
   | Exists phi -> occurs (Term.inc_var t) phi
+
+type precedence =
+  | Atomic
+  | Negation
+  | Conjunction
+  | Disjunction
+  | Implication
+  | Biconditional
+  | Quantifier
+
+let precedence_of = function
+  | Relation _ | Equal _ | Bottom -> Atomic
+  | Neg _ -> Negation
+  | Conj _ -> Conjunction
+  | Disj _ -> Disjunction
+  | Impl _ -> Implication
+  | Iff _ -> Biconditional
+  | Forall _ | Exists _ -> Quantifier
+
+open Format
+
+let fresh_var_name used_names =
+  let base_names = [ "x"; "y"; "z"; "w"; "u"; "v" ] in
+  let rec find_name i =
+    let name =
+      if i < List.length base_names then List.nth base_names i
+      else sprintf "x%d" (i - List.length base_names + 1)
+    in
+    if List.mem name used_names then find_name (i + 1) else name
+  in
+  find_name 0
+
+let to_string formula =
+  let rec aux depth binders parent_precedence formula =
+    let current_precedence = precedence_of formula in
+    let step = aux depth binders current_precedence in
+
+    let inner_string =
+      match formula with
+      | Relation (r, terms) ->
+          sprintf "%s(%s)" r
+            (String.concat ", " (List.map (Term.to_string ~binders) terms))
+      | Equal (t1, t2) ->
+          sprintf "%s = %s"
+            (Term.to_string ~binders t1)
+            (Term.to_string ~binders t2)
+      | Bottom -> "⊥"
+      | Neg f -> sprintf "¬%s" (aux depth binders Negation f)
+      | Conj (f1, f2) -> sprintf "%s ∧ %s" (step f1) (step f2)
+      | Disj (f1, f2) -> sprintf "%s ∨ %s" (step f1) (step f2)
+      | Impl (f1, f2) -> sprintf "%s → %s" (step f1) (step f2)
+      | Iff (f1, f2) -> sprintf "%s ↔ %s" (step f1) (step f2)
+      | Forall f | Exists f ->
+          let new_var = fresh_var_name binders in
+          let quantifier = if Forall f = formula then "∀" else "∃" in
+          sprintf "%s%s.%s" quantifier new_var
+            (aux (depth + 1) (new_var :: binders) Quantifier f)
+    in
+    if parent_precedence < current_precedence then "(" ^ inner_string ^ ")"
+    else inner_string
+  in
+  aux 0 [] Quantifier formula

lib/formula.mli

@@ -12,3 +12,4 @@ type t =
 
 val match_term : Term.t -> t -> t -> Term.match_result
 val occurs : Term.t -> t -> bool
+val to_string : t -> string

lib/term.ml

@@ -40,3 +40,16 @@ let rec inc_var = function
 let rec occurs t = function
   | Function (_, ts) -> List.exists (occurs t) ts
   | s -> t = s
+
+exception UnboundVariable
+
+let to_string ~binders =
+  let open Format in
+  let rec aux = function
+    | Var v -> ( try List.nth binders v with _ -> raise UnboundVariable)
+    | Const c -> c
+    | Free f -> f
+    | Function (f, args) ->
+        sprintf "%s(%s)" f (String.concat ", " (List.map aux args))
+  in
+  aux

lib/term.mli

@@ -12,3 +12,7 @@ val merge_result : match_result -> match_result -> match_result
 val match_term : t -> t -> t -> match_result
 val inc_var : t -> t
 val occurs : t -> t -> bool
+
+exception UnboundVariable
+
+val to_string : binders:string list -> t -> string