108 lines
3.7 KiB
OCaml
108 lines
3.7 KiB
OCaml
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 None
|
||
else MatchErr
|
||
| Equal (t1, s1), Equal (t2, s2) ->
|
||
Term.(merge_result (match_term t t1 t2) (match_term t s1 s2))
|
||
| Bottom, Bottom -> None
|
||
| 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
|