proof_checker/lib/kernel/formula.ml

type t =
  | Relation of string * Term.t list
  | Equal of Term.t * Term.t
  | Bottom
  | Neg of t
  | Conj of t * t
  | Disj of t * t
  | Impl of t * t
  | Iff of t * t
  | Forall of t
  | Exists of t

let rec match_term t phi psi =
  match (phi, psi) with
  | Relation (r1, ts1), Relation (r2, ts2) ->
      if r1 = r2 && List.length ts1 = List.length ts2 then
        List.map2 (Term.match_term t) ts1 ts2
        |> List.fold_left Term.merge_result NoneSubst
      else MatchErr
  | Equal (t1, s1), Equal (t2, s2) ->
      Term.(merge_result (match_term t t1 t2) (match_term t s1 s2))
  | Bottom, Bottom -> NoneSubst
  | Neg phi, Neg psi -> match_term t phi psi
  | Conj (phi1, psi1), Conj (phi2, psi2) ->
      Term.merge_result (match_term t phi1 phi2) (match_term t psi1 psi2)
  | Disj (phi1, psi1), Disj (phi2, psi2) ->
      Term.merge_result (match_term t phi1 phi2) (match_term t psi1 psi2)
  | Impl (phi1, psi1), Impl (phi2, psi2) ->
      Term.merge_result (match_term t phi1 phi2) (match_term t psi1 psi2)
  | Iff (phi1, psi1), Iff (phi2, psi2) ->
      Term.merge_result (match_term t phi1 phi2) (match_term t psi1 psi2)
  | Forall phi, Forall psi -> match_term (Term.inc_var t) phi psi
  | Exists phi, Exists psi -> match_term (Term.inc_var t) phi psi
  | _ -> MatchErr

let rec occurs t = function
  | Relation (_, ts) -> List.exists (Term.occurs t) ts
  | Equal (t1, t2) -> Term.occurs t t1 || Term.occurs t t2
  | Bottom -> false
  | Neg phi -> occurs t phi
  | Conj (phi, psi) -> occurs t phi || occurs t psi
  | Disj (phi, psi) -> occurs t phi || occurs t psi
  | Impl (phi, psi) -> occurs t phi || occurs t psi
  | 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