Safe Haskell | None |
---|---|
Language | Haskell98 |
Support for equality.
- class Predicate p => AtomEq atom p term | atom -> term, atom -> p where
- foldAtomEq :: (p -> [term] -> r) -> (Bool -> r) -> (term -> term -> r) -> atom -> r
- equals :: term -> term -> atom
- applyEq' :: p -> [term] -> atom
- applyEq :: AtomEq atom p term => p -> [term] -> atom
- data PredicateName p
- zipAtomsEq :: AtomEq atom p term => (p -> [term] -> p -> [term] -> Maybe r) -> (Bool -> Bool -> Maybe r) -> (term -> term -> term -> term -> Maybe r) -> atom -> atom -> Maybe r
- apply0 :: AtomEq atom p term => p -> atom
- apply1 :: AtomEq atom p a => p -> a -> atom
- apply2 :: AtomEq atom p a => p -> a -> a -> atom
- apply3 :: AtomEq atom p a => p -> a -> a -> a -> atom
- apply4 :: AtomEq atom p a => p -> a -> a -> a -> a -> atom
- apply5 :: AtomEq atom p a => p -> a -> a -> a -> a -> a -> atom
- apply6 :: AtomEq atom p a => p -> a -> a -> a -> a -> a -> a -> atom
- apply7 :: AtomEq atom p a => p -> a -> a -> a -> a -> a -> a -> a -> atom
- pApp :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> [term] -> formula
- pApp0 :: forall formula atom term v p. (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> formula
- pApp1 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> formula
- pApp2 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> formula
- pApp3 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> formula
- pApp4 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> term -> formula
- pApp5 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> term -> term -> formula
- pApp6 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> term -> term -> term -> formula
- pApp7 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> term -> term -> term -> term -> formula
- showFirstOrderFormulaEq :: forall fof atom v p term. (FirstOrderFormula fof atom v, AtomEq atom p term, Show term, Show v, Show p) => fof -> String
- (.=.) :: (FirstOrderFormula fof atom v, AtomEq atom p term) => term -> term -> fof
- (≡) :: (FirstOrderFormula fof atom v, AtomEq atom p term) => term -> term -> fof
- (.!=.) :: (FirstOrderFormula fof atom v, AtomEq atom p term) => term -> term -> fof
- (≢) :: (FirstOrderFormula fof atom v, AtomEq atom p term) => term -> term -> fof
- fromAtomEq :: (AtomEq atom1 p1 term1, Term term1 v1 f1, AtomEq atom2 p2 term2, Term term2 v2 f2, Constants atom2) => (v1 -> v2) -> (p1 -> p2) -> (f1 -> f2) -> atom1 -> atom2
- showAtomEq :: forall atom term v p f. (AtomEq atom p term, Term term v f, Show v, Show p, Show f) => atom -> String
- prettyAtomEq :: (AtomEq atom p term, Term term v f) => (v -> Doc) -> (p -> Doc) -> (f -> Doc) -> Int -> atom -> Doc
- varAtomEq :: forall atom term v p f. (AtomEq atom p term, Term term v f) => atom -> Set v
- substAtomEq :: (AtomEq atom p term, Constants atom, Term term v f) => Map v term -> atom -> atom
- funcsAtomEq :: (AtomEq atom p term, Term term v f, Ord f) => atom -> Set (f, Int)
Documentation
class Predicate p => AtomEq atom p term | atom -> term, atom -> p where Source
Its not safe to make Atom a superclass of AtomEq, because the Atom methods will fail on AtomEq instances.
foldAtomEq :: (p -> [term] -> r) -> (Bool -> r) -> (term -> term -> r) -> atom -> r Source
applyEq :: AtomEq atom p term => p -> [term] -> atom Source
applyEq' with an arity check - clients should always call this.
data PredicateName p Source
A way to represent any predicate's name. Frequently the equality predicate has no standalone representation in the p type, it is just a constructor in the atom type, or even the formula type.
Eq p => Eq (PredicateName p) Source | |
Ord p => Ord (PredicateName p) Source | |
Show p => Show (PredicateName p) Source | |
(Pretty p, Ord p) => Pretty (PredicateName p) Source |
zipAtomsEq :: AtomEq atom p term => (p -> [term] -> p -> [term] -> Maybe r) -> (Bool -> Bool -> Maybe r) -> (term -> term -> term -> term -> Maybe r) -> atom -> atom -> Maybe r Source
pApp :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> [term] -> formula Source
pApp0 :: forall formula atom term v p. (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> formula Source
Versions of pApp specialized for different argument counts.
pApp1 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> formula Source
pApp2 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> formula Source
pApp3 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> formula Source
pApp4 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> term -> formula Source
pApp5 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> term -> term -> formula Source
pApp6 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> term -> term -> term -> formula Source
pApp7 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> term -> term -> term -> term -> formula Source
showFirstOrderFormulaEq :: forall fof atom v p term. (FirstOrderFormula fof atom v, AtomEq atom p term, Show term, Show v, Show p) => fof -> String Source
(.=.) :: (FirstOrderFormula fof atom v, AtomEq atom p term) => term -> term -> fof infix 5 Source
(≡) :: (FirstOrderFormula fof atom v, AtomEq atom p term) => term -> term -> fof infix 5 Source
(.!=.) :: (FirstOrderFormula fof atom v, AtomEq atom p term) => term -> term -> fof infix 5 Source
(≢) :: (FirstOrderFormula fof atom v, AtomEq atom p term) => term -> term -> fof infix 5 Source
fromAtomEq :: (AtomEq atom1 p1 term1, Term term1 v1 f1, AtomEq atom2 p2 term2, Term term2 v2 f2, Constants atom2) => (v1 -> v2) -> (p1 -> p2) -> (f1 -> f2) -> atom1 -> atom2 Source
showAtomEq :: forall atom term v p f. (AtomEq atom p term, Term term v f, Show v, Show p, Show f) => atom -> String Source
prettyAtomEq :: (AtomEq atom p term, Term term v f) => (v -> Doc) -> (p -> Doc) -> (f -> Doc) -> Int -> atom -> Doc Source
varAtomEq :: forall atom term v p f. (AtomEq atom p term, Term term v f) => atom -> Set v Source
Return the variables that occur in an instance of AtomEq.