Data.Logic.ATP.Formulas

The IsFormula class contains definitions for the boolean true and false values, and methods for traversing the atoms of a formula.

Documentation

class (Ord atom, Show atom, HasFixity atom, Pretty atom) => IsAtom atom

Basic properties of an atomic formula

Instances

IsAtom Prop

IsAtom Atom

IsAtom (Knows Integer)

(IsPredicate predicate, IsTerm term) => IsAtom (FOLAP predicate term)

(IsPredicate predicate, IsTerm term) => IsAtom (FOL predicate term)

class (Pretty formula, HasFixity formula, IsAtom (AtomOf formula)) => IsFormula formula where

Class associating a formula type with its atom (atomic formula) type.

Minimal complete definition

true, false, asBool, atomic, overatoms, onatoms

Associated Types

type AtomOf formula

AtomOf is a function that maps the formula type to the associated atomic formula type

Methods

true :: formula

The true element

false :: formula

The false element

asBool :: formula -> Maybe Bool

If the arugment is true or false return the corresponding Bool, otherwise return Nothing.

atomic :: AtomOf formula -> formula

Build a formula from an atom.

overatoms :: (AtomOf formula -> r -> r) -> formula -> r -> r

Formula analog of iterator foldr.

onatoms :: (AtomOf formula -> AtomOf formula) -> formula -> formula

Apply a function to the atoms, otherwise keeping structure (new sig)

Instances

IsAtom atom => IsFormula (LFormula atom)

Associated Types

type AtomOf (LFormula atom) :: *

Methods

true :: LFormula atom

false :: LFormula atom

asBool :: LFormula atom -> Maybe Bool

atomic :: AtomOf (LFormula atom) -> LFormula atom

overatoms :: (AtomOf (LFormula atom) -> r -> r) -> LFormula atom -> r -> r

onatoms :: (AtomOf (LFormula atom) -> AtomOf (LFormula atom)) -> LFormula atom -> LFormula atom

IsLiteral a => IsFormula (JL a)

Associated Types

type AtomOf (JL a) :: *

Methods

true :: JL a

false :: JL a

asBool :: JL a -> Maybe Bool

atomic :: AtomOf (JL a) -> JL a

overatoms :: (AtomOf (JL a) -> r -> r) -> JL a -> r -> r

onatoms :: (AtomOf (JL a) -> AtomOf (JL a)) -> JL a -> JL a

IsAtom atom => IsFormula (PFormula atom)

Associated Types

type AtomOf (PFormula atom) :: *

Methods

true :: PFormula atom

false :: PFormula atom

asBool :: PFormula atom -> Maybe Bool

atomic :: AtomOf (PFormula atom) -> PFormula atom

overatoms :: (AtomOf (PFormula atom) -> r -> r) -> PFormula atom -> r -> r

onatoms :: (AtomOf (PFormula atom) -> AtomOf (PFormula atom)) -> PFormula atom -> PFormula atom

(HasApply atom, (~) * v (TVarOf (TermOf atom))) => IsFormula (QFormula v atom)

Associated Types

type AtomOf (QFormula v atom) :: *

Methods

true :: QFormula v atom

false :: QFormula v atom

asBool :: QFormula v atom -> Maybe Bool

atomic :: AtomOf (QFormula v atom) -> QFormula v atom

overatoms :: (AtomOf (QFormula v atom) -> r -> r) -> QFormula v atom -> r -> r

onatoms :: (AtomOf (QFormula v atom) -> AtomOf (QFormula v atom)) -> QFormula v atom -> QFormula v atom

(⊥) :: IsFormula p => p

(⊤) :: IsFormula p => p

fromBool :: IsFormula formula => Bool -> formula

prettyBool :: Bool -> Doc

atom_union :: (IsFormula formula, Ord r) => (AtomOf formula -> Set r) -> formula -> Set r

Special case of a union of the results of a function over the atoms.