module Data.Logic.ATP.Formulas
( IsAtom
, IsFormula(AtomOf, true, false, asBool, atomic, overatoms, onatoms)
, (⊥), (⊤)
, fromBool
, prettyBool
, atom_union
) where
import Data.Logic.ATP.Pretty (Doc, HasFixity, Pretty, text)
import Data.Set as Set (Set, empty, union)
import Prelude hiding (negate)
class (Ord atom, Show atom, HasFixity atom, Pretty atom) => IsAtom atom
class (Pretty formula, HasFixity formula, IsAtom (AtomOf formula)) => IsFormula formula where
type AtomOf formula
true :: formula
false :: formula
asBool :: formula -> Maybe Bool
atomic :: AtomOf formula -> formula
overatoms :: (AtomOf formula -> r -> r) -> formula -> r -> r
onatoms :: (AtomOf formula -> AtomOf formula) -> formula -> formula
(⊤) :: IsFormula p => p
(⊤) = true
(⊥) :: IsFormula p => p
(⊥) = false
fromBool :: IsFormula formula => Bool -> formula
fromBool True = true
fromBool False = false
prettyBool :: Bool -> Doc
prettyBool True = text "⊤"
prettyBool False = text "⊥"
atom_union :: (IsFormula formula, Ord r) => (AtomOf formula -> Set r) -> formula -> Set r
atom_union f fm = overatoms (\h t -> Set.union (f h) t) fm Set.empty