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 Atom

Defined in Data.Logic.ATP.DefCNF

IsAtom Prop

Defined in Data.Logic.ATP.Prop

IsAtom (Knows Integer)

Defined in Data.Logic.ATP.PropExamples

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

Defined in Data.Logic.ATP.Apply

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

Defined in Data.Logic.ATP.Equate

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

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

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)

Defined in Data.Logic.ATP.Lit

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)

Defined in Data.Logic.ATP.LitWrapper

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)

Defined in Data.Logic.ATP.Prop

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)

Defined in Data.Logic.ATP.Quantified

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.