| Safe Haskell | None |
|---|
Data.Logic.Classes.Literal
- class (Negatable lit, Constants lit, HasFixity atom, Formula lit atom, Ord lit) => Literal lit atom | lit -> atom where
- foldLiteral :: (lit -> r) -> (Bool -> r) -> (atom -> r) -> lit -> r
- zipLiterals :: Literal lit atom => (lit -> lit -> Maybe r) -> (Bool -> Bool -> Maybe r) -> (atom -> atom -> Maybe r) -> lit -> lit -> Maybe r
- fromFirstOrder :: forall formula atom v lit atom2. (Formula lit atom2, FirstOrderFormula formula atom v, Literal lit atom2) => (atom -> atom2) -> formula -> Failing lit
- fromLiteral :: forall lit atom v fof atom2. (Literal lit atom, FirstOrderFormula fof atom2 v) => (atom -> atom2) -> lit -> fof
- toPropositional :: forall lit atom pf atom2. (Literal lit atom, PropositionalFormula pf atom2) => (atom -> atom2) -> lit -> pf
- prettyLit :: forall lit atom v. Literal lit atom => (Int -> atom -> Doc) -> (v -> Doc) -> Int -> lit -> Doc
- foldAtomsLiteral :: Literal lit atom => (r -> atom -> r) -> r -> lit -> r
Documentation
class (Negatable lit, Constants lit, HasFixity atom, Formula lit atom, Ord lit) => Literal lit atom | lit -> atom whereSource
Literals are the building blocks of the clause and implicative normal |forms. They support negation and must include True and False elements.
Methods
foldLiteral :: (lit -> r) -> (Bool -> r) -> (atom -> r) -> lit -> rSource
Instances
| (Negatable (Formula atom), Constants (Formula atom), Formula (Formula atom) atom, Ord (Formula atom), Pretty atom, HasFixity atom, Ord atom) => Literal (Formula atom) atom | |
| (Negatable (Formula atom), Constants (Formula atom), Formula (Formula atom) atom, Ord (Formula atom), HasFixity atom, Pretty atom, Ord atom) => Literal (Formula atom) atom | |
| (Negatable (Formula FOLEQ), Constants (Formula FOLEQ), HasFixity FOLEQ, Ord (Formula FOLEQ), Formula (Formula FOLEQ) FOLEQ) => Literal (Formula FOLEQ) FOLEQ | |
| (Negatable (Formula v p f), Constants (Formula v p f), HasFixity (Predicate p (PTerm v f)), Ord (Formula v p f), Constants p, Ord v, Ord p, Ord f, Constants (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f))) => Literal (Formula v p f) (Predicate p (PTerm v f)) |
zipLiterals :: Literal lit atom => (lit -> lit -> Maybe r) -> (Bool -> Bool -> Maybe r) -> (atom -> atom -> Maybe r) -> lit -> lit -> Maybe rSource
fromFirstOrder :: forall formula atom v lit atom2. (Formula lit atom2, FirstOrderFormula formula atom v, Literal lit atom2) => (atom -> atom2) -> formula -> Failing litSource
Just like Logic.FirstOrder.convertFOF except it rejects anything with a construct unsupported in a normal logic formula, i.e. quantifiers and formula combinators other than negation.
fromLiteral :: forall lit atom v fof atom2. (Literal lit atom, FirstOrderFormula fof atom2 v) => (atom -> atom2) -> lit -> fofSource
toPropositional :: forall lit atom pf atom2. (Literal lit atom, PropositionalFormula pf atom2) => (atom -> atom2) -> lit -> pfSource
prettyLit :: forall lit atom v. Literal lit atom => (Int -> atom -> Doc) -> (v -> Doc) -> Int -> lit -> DocSource
foldAtomsLiteral :: Literal lit atom => (r -> atom -> r) -> r -> lit -> rSource