Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Logic.ATP.Equate

Description

ATOM with a distinguished Equate predicate.

Synopsis

class HasApply atom => HasEquate atom where
- equate :: TermOf atom -> TermOf atom -> atom
- foldEquate :: (TermOf atom -> TermOf atom -> r) -> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
(.=.) :: (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
- = R predicate [term]
- | Equals term term
type EqAtom = FOL Predicate FTerm

Documentation

class HasApply atom => HasEquate atom where Source #

Atoms that support equality must be an instance of HasEquate

Methods

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.

Instances

Instances details

(IsPredicate predicate, IsTerm term) => HasEquate (FOL predicate term) Source #
Instance details Defined in Data.Logic.ATP.Equate Methods equate :: TermOf (FOL predicate term) -> TermOf (FOL predicate term) -> FOL predicate term Source # foldEquate :: (TermOf (FOL predicate term) -> TermOf (FOL predicate term) -> r) -> (PredOf (FOL predicate term) -> [TermOf (FOL predicate term)] -> r) -> FOL predicate term -> r Source #

(.=.) :: (IsFormula formula, HasEquate atom, atom ~ AtomOf formula) => TermOf atom -> TermOf atom -> formula infix 6 Source #

Combine equate and atomic to build a formula from two terms.

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 #

Implementation of overterms for HasEquate types.

ontermsEq :: HasEquate atom => (TermOf atom -> TermOf atom) -> atom -> atom Source #

Implementation of onterms for HasEquate types.

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.

Constructors

R predicate [term]
Equals term term

Instances

Instances details

IsFirstOrder EqFormula Source #
Instance details Defined in Data.Logic.ATP.FOL
IsFirstOrder Formula Source #
Instance details Defined in Data.Logic.ATP.Skolem
MonadFail m => Unify m (SkAtom, SkAtom) Source #
Instance details Defined in Data.Logic.ATP.Unif Associated Types type UTermOf (SkAtom, SkAtom) Source # Methods unify' :: (SkAtom, SkAtom) -> StateT (Map (TVarOf (UTermOf (SkAtom, SkAtom))) (UTermOf (SkAtom, SkAtom))) m () Source #
(IsPredicate predicate, IsTerm term) => HasApply (FOL predicate term) Source #
Instance details Defined in Data.Logic.ATP.Equate Associated Types type PredOf (FOL predicate term) Source # type TermOf (FOL predicate term) Source # Methods applyPredicate :: PredOf (FOL predicate term) -> [TermOf (FOL predicate term)] -> FOL predicate term Source # foldApply' :: (FOL predicate term -> r) -> (PredOf (FOL predicate term) -> [TermOf (FOL predicate term)] -> r) -> FOL predicate term -> r Source # overterms :: (TermOf (FOL predicate term) -> r -> r) -> r -> FOL predicate term -> r Source # onterms :: (TermOf (FOL predicate term) -> TermOf (FOL predicate term)) -> FOL predicate term -> FOL predicate term Source #
(IsPredicate predicate, IsTerm term) => HasEquate (FOL predicate term) Source #
Instance details Defined in Data.Logic.ATP.Equate Methods equate :: TermOf (FOL predicate term) -> TermOf (FOL predicate term) -> FOL predicate term Source # foldEquate :: (TermOf (FOL predicate term) -> TermOf (FOL predicate term) -> r) -> (PredOf (FOL predicate term) -> [TermOf (FOL predicate term)] -> r) -> FOL predicate term -> r Source #
(IsPredicate predicate, IsTerm term) => IsAtom (FOL predicate term) Source #
Instance details Defined in Data.Logic.ATP.Equate
(IsPredicate predicate, IsTerm term) => HasFixity (FOL predicate term) Source #
Instance details Defined in Data.Logic.ATP.Equate Methods precedence :: FOL predicate term -> Precedence Source # associativity :: FOL predicate term -> Associativity Source #
(Data predicate, Data term) => Data (FOL predicate term) Source #
Instance details Defined in Data.Logic.ATP.Equate Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FOL predicate term -> c (FOL predicate term) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (FOL predicate term) # toConstr :: FOL predicate term -> Constr # dataTypeOf :: FOL predicate term -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (FOL predicate term)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (FOL predicate term)) # gmapT :: (forall b. Data b => b -> b) -> FOL predicate term -> FOL predicate term # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FOL predicate term -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FOL predicate term -> r # gmapQ :: (forall d. Data d => d -> u) -> FOL predicate term -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> FOL predicate term -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> FOL predicate term -> m (FOL predicate term) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FOL predicate term -> m (FOL predicate term) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FOL predicate term -> m (FOL predicate term) #
(Read predicate, Read term) => Read (FOL predicate term) Source #
Instance details Defined in Data.Logic.ATP.Equate Methods readsPrec :: Int -> ReadS (FOL predicate term) # readList :: ReadS [FOL predicate term] # readPrec :: ReadPrec (FOL predicate term) # readListPrec :: ReadPrec [FOL predicate term] #
(IsPredicate predicate, IsTerm term, Show predicate, Show term) => Show (FOL predicate term) Source #
Instance details Defined in Data.Logic.ATP.Equate Methods showsPrec :: Int -> FOL predicate term -> ShowS # show :: FOL predicate term -> String # showList :: [FOL predicate term] -> ShowS #
(Eq predicate, Eq term) => Eq (FOL predicate term) Source #
Instance details Defined in Data.Logic.ATP.Equate Methods (==) :: FOL predicate term -> FOL predicate term -> Bool # (/=) :: FOL predicate term -> FOL predicate term -> Bool #
(Ord predicate, Ord term) => Ord (FOL predicate term) Source #
Instance details Defined in Data.Logic.ATP.Equate Methods compare :: FOL predicate term -> FOL predicate term -> Ordering # (<) :: FOL predicate term -> FOL predicate term -> Bool # (<=) :: FOL predicate term -> FOL predicate term -> Bool # (>) :: FOL predicate term -> FOL predicate term -> Bool # (>=) :: FOL predicate term -> FOL predicate term -> Bool # max :: FOL predicate term -> FOL predicate term -> FOL predicate term # min :: FOL predicate term -> FOL predicate term -> FOL predicate term #
(HasApply (FOL predicate term), HasEquate (FOL predicate term), IsTerm term) => Pretty (FOL predicate term) Source #
Instance details Defined in Data.Logic.ATP.Equate Methods pPrintPrec :: PrettyLevel -> Rational -> FOL predicate term -> Doc # pPrint :: FOL predicate term -> Doc # pPrintList :: PrettyLevel -> [FOL predicate term] -> Doc #
type PredOf (FOL predicate term) Source #
Instance details Defined in Data.Logic.ATP.Equate type PredOf (FOL predicate term) = predicate
type TermOf (FOL predicate term) Source #
Instance details Defined in Data.Logic.ATP.Equate type TermOf (FOL predicate term) = term
type UTermOf (SkAtom, SkAtom) Source #
Instance details Defined in Data.Logic.ATP.Unif type UTermOf (SkAtom, SkAtom) = TermOf SkAtom

type EqAtom = FOL Predicate FTerm Source #

An atom type with equality predicate