Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Logic.ATP.Formulas

Description

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

Synopsis

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
(⊤) :: IsFormula p => p
fromBool :: IsFormula formula => Bool -> formula
prettyBool :: Bool -> Doc
atom_union :: (IsFormula formula, Ord r) => (AtomOf formula -> Set r) -> formula -> Set r

Documentation

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

Basic properties of an atomic formula

Instances

Instances details

IsAtom Atom Source #
Instance details Defined in Data.Logic.ATP.DefCNF
IsAtom Prop Source #
Instance details Defined in Data.Logic.ATP.Prop
IsAtom (Knows Integer) Source #
Instance details Defined in Data.Logic.ATP.PropExamples
(IsPredicate predicate, IsTerm term) => IsAtom (FOLAP predicate term) Source #
Instance details Defined in Data.Logic.ATP.Apply
(IsPredicate predicate, IsTerm term) => IsAtom (FOL predicate term) Source #
Instance details Defined in Data.Logic.ATP.Equate

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

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

Associated Types

type AtomOf formula Source #

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

Methods

true :: formula Source #

The true element

false :: formula Source #

The false element

asBool :: formula -> Maybe Bool Source #

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

atomic :: AtomOf formula -> formula Source #

Build a formula from an atom.

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

Formula analog of iterator foldr.

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

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

Instances

Instances details

IsAtom atom => IsFormula (LFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Lit Associated Types type AtomOf (LFormula atom) Source # Methods true :: LFormula atom Source # false :: LFormula atom Source # asBool :: LFormula atom -> Maybe Bool Source # atomic :: AtomOf (LFormula atom) -> LFormula atom Source # overatoms :: (AtomOf (LFormula atom) -> r -> r) -> LFormula atom -> r -> r Source # onatoms :: (AtomOf (LFormula atom) -> AtomOf (LFormula atom)) -> LFormula atom -> LFormula atom Source #
IsLiteral a => IsFormula (JL a) Source #
Instance details Defined in Data.Logic.ATP.LitWrapper Associated Types type AtomOf (JL a) Source # Methods true :: JL a Source # false :: JL a Source # asBool :: JL a -> Maybe Bool Source # atomic :: AtomOf (JL a) -> JL a Source # overatoms :: (AtomOf (JL a) -> r -> r) -> JL a -> r -> r Source # onatoms :: (AtomOf (JL a) -> AtomOf (JL a)) -> JL a -> JL a Source #
IsAtom atom => IsFormula (PFormula atom) Source #
Instance details Defined in Data.Logic.ATP.Prop Associated Types type AtomOf (PFormula atom) Source # Methods true :: PFormula atom Source # false :: PFormula atom Source # asBool :: PFormula atom -> Maybe Bool Source # atomic :: AtomOf (PFormula atom) -> PFormula atom Source # overatoms :: (AtomOf (PFormula atom) -> r -> r) -> PFormula atom -> r -> r Source # onatoms :: (AtomOf (PFormula atom) -> AtomOf (PFormula atom)) -> PFormula atom -> PFormula atom Source #
(HasApply atom, v ~ TVarOf (TermOf atom)) => IsFormula (QFormula v atom) Source #
Instance details Defined in Data.Logic.ATP.Quantified Associated Types type AtomOf (QFormula v atom) Source # Methods true :: QFormula v atom Source # false :: QFormula v atom Source # asBool :: QFormula v atom -> Maybe Bool Source # atomic :: AtomOf (QFormula v atom) -> QFormula v atom Source # overatoms :: (AtomOf (QFormula v atom) -> r -> r) -> QFormula v atom -> r -> r Source # onatoms :: (AtomOf (QFormula v atom) -> AtomOf (QFormula v atom)) -> QFormula v atom -> QFormula v atom Source #

(⊥) :: IsFormula p => p Source #

(⊤) :: IsFormula p => p Source #

fromBool :: IsFormula formula => Bool -> formula Source #

prettyBool :: Bool -> Doc Source #

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

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