Safe Haskell | None |
---|---|
Language | Haskell98 |
ATOM with a distinguished Equate predicate.
- class HasApply atom => HasEquate atom where
- (.=.) :: (IsFormula formula, HasEquate atom, atom ~ AtomOf formula) => TermOf atom -> TermOf atom -> formula
- zipEquates :: (HasEquate atom1, HasEquate atom2, PredOf atom1 ~ PredOf atom2) => (TermOf atom1 -> TermOf atom1 -> TermOf atom2 -> TermOf atom2 -> Maybe r) -> (PredOf atom1 -> [(TermOf atom1, TermOf atom2)] -> Maybe r) -> atom1 -> atom2 -> Maybe r
- prettyEquate :: IsTerm term => PrettyLevel -> Rational -> term -> term -> Doc
- overtermsEq :: HasEquate atom => (TermOf atom -> r -> r) -> r -> atom -> r
- ontermsEq :: HasEquate atom => (TermOf atom -> TermOf atom) -> atom -> atom
- showApplyAndEquate :: (HasEquate atom, Show (TermOf atom)) => atom -> String
- showEquate :: Show term => term -> term -> String
- convertEquate :: (HasEquate atom1, HasEquate atom2) => (PredOf atom1 -> PredOf atom2) -> (TermOf atom1 -> TermOf atom2) -> atom1 -> atom2
- precedenceEquate :: HasEquate atom => atom -> Precedence
- associativityEquate :: HasEquate atom => atom -> Associativity
- data FOL predicate term
- type EqAtom = FOL Predicate FTerm
Documentation
class HasApply atom => HasEquate atom where Source
Atoms that support equality must be an instance of HasEquate
equate :: TermOf atom -> TermOf atom -> atom Source
Create an equate predicate
foldEquate :: (TermOf atom -> TermOf atom -> r) -> (PredOf atom -> [TermOf atom] -> r) -> atom -> r Source
Analyze whether a predicate is an equate or a regular apply.
(IsPredicate predicate, IsTerm term) => HasEquate (FOL predicate term) Source |
(.=.) :: (IsFormula formula, HasEquate atom, atom ~ AtomOf formula) => TermOf atom -> TermOf atom -> formula infix 6 Source
zipEquates :: (HasEquate atom1, HasEquate atom2, PredOf atom1 ~ PredOf atom2) => (TermOf atom1 -> TermOf atom1 -> TermOf atom2 -> TermOf atom2 -> Maybe r) -> (PredOf atom1 -> [(TermOf atom1, TermOf atom2)] -> Maybe r) -> atom1 -> atom2 -> Maybe r Source
Zip two atoms that support equality
prettyEquate :: IsTerm term => PrettyLevel -> Rational -> term -> term -> Doc Source
Format the infix equality predicate applied to two terms.
overtermsEq :: HasEquate atom => (TermOf atom -> r -> r) -> r -> atom -> r Source
showApplyAndEquate :: (HasEquate atom, Show (TermOf atom)) => atom -> String Source
Implementation of Show for HasEquate
types
showEquate :: Show term => term -> term -> String Source
convertEquate :: (HasEquate atom1, HasEquate atom2) => (PredOf atom1 -> PredOf atom2) -> (TermOf atom1 -> TermOf atom2) -> atom1 -> atom2 Source
Convert between HasEquate atom types.
precedenceEquate :: HasEquate atom => atom -> Precedence Source
associativityEquate :: HasEquate atom => atom -> Associativity Source
data FOL predicate term Source
Instance of an atom type with a distinct equality predicate.
IsFirstOrder EqFormula Source | |
IsFirstOrder Formula Source | |
(Eq predicate, Eq term) => Eq (FOL predicate term) Source | |
(Data predicate, Data term) => Data (FOL predicate term) Source | |
(Ord predicate, Ord term) => Ord (FOL predicate term) Source | |
(Read predicate, Read term) => Read (FOL predicate term) Source | |
(IsPredicate predicate, IsTerm term, Show predicate, Show term) => Show (FOL predicate term) Source | |
(HasApply (FOL predicate term), HasEquate (FOL predicate term), IsTerm term) => Pretty (FOL predicate term) Source | |
(IsPredicate predicate, IsTerm term) => HasFixity (FOL predicate term) Source | |
(IsPredicate predicate, IsTerm term) => IsAtom (FOL predicate term) Source | |
(IsPredicate predicate, IsTerm term) => HasApply (FOL predicate term) Source | |
(IsPredicate predicate, IsTerm term) => HasEquate (FOL predicate term) Source | |
Unify (SkAtom, SkAtom) Source | |
type PredOf (FOL predicate term) = predicate Source | |
type TermOf (FOL predicate term) = term Source | |
type UTermOf (SkAtom, SkAtom) = TermOf SkAtom Source |