Data.Logic.ATP.TH

ATP instances for the template haskell type Type, and the conjunction of such types, [Type]. In these instances, almost every role is played by Type. It might a case where the tagged package could be used to advantage. A list represents conjunction, but there is no disjunction operation, nor any derived from it like implication or equivalence.

Documentation

unfoldApply :: Type -> [Type] -> (Type, [Type])

Helper function to interpret a type application: unfoldApply (AppT (AppT (AppT (VarT (mkName "a")) StarT) ListT) ArrowT) -> (VarT (mkName "a"), [StarT, ListT, ArrowT]) The inverse is uncurry . foldl AppT.

expandBindings :: Map Pred Pred -> Pred -> Pred

Orphan instances

IsString Type

Methods

fromString :: String -> Type

HasEquate Type

Methods

equate :: TermOf Type -> TermOf Type -> Type

foldEquate :: (TermOf Type -> TermOf Type -> r) -> (PredOf Type -> [TermOf Type] -> r) -> Type -> r

IsPredicate Type

HasApply Type

Associated Types

type PredOf Type :: *

type TermOf Type :: *

Methods

applyPredicate :: PredOf Type -> [TermOf Type] -> Type

foldApply' :: (Type -> r) -> (PredOf Type -> [TermOf Type] -> r) -> Type -> r

overterms :: (TermOf Type -> r -> r) -> r -> Type -> r

onterms :: (TermOf Type -> TermOf Type) -> Type -> Type

IsVariable Type

Methods

variant :: Type -> Set Type -> Type

prefix :: String -> Type -> Type

IsFunction Type

IsTerm Type

Associated Types

type TVarOf Type :: *

type FunOf Type :: *

Methods

vt :: TVarOf Type -> Type

fApp :: FunOf Type -> [Type] -> Type

foldTerm :: (TVarOf Type -> r) -> (FunOf Type -> [Type] -> r) -> Type -> r

IsLiteral Type

Methods

naiveNegate :: Type -> Type

foldNegation :: (Type -> r) -> (Type -> r) -> Type -> r

foldLiteral' :: (Type -> r) -> (Type -> r) -> (Bool -> r) -> (AtomOf Type -> r) -> Type -> r

JustLiteral Type

IsAtom Type

IsFormula Type

Associated Types

type AtomOf Type :: *

Methods

true :: Type

false :: Type

asBool :: Type -> Maybe Bool

atomic :: AtomOf Type -> Type

overatoms :: (AtomOf Type -> r -> r) -> Type -> r -> r

onatoms :: (AtomOf Type -> AtomOf Type) -> Type -> Type

HasFixity Type

Methods

precedence :: Type -> Precedence

associativity :: Type -> Associativity

Pretty Type

Methods

pPrintPrec :: PrettyLevel -> Rational -> Type -> Doc

pPrint :: Type -> Doc

pPrintList :: PrettyLevel -> [Type] -> Doc

Monad m => Unify m Type

Associated Types

type UTermOf Type :: *

Methods

unify' :: Type -> StateT (Map (TVarOf (UTermOf Type)) (UTermOf Type)) m ()

Monad m => Unify m [Type]

Associated Types

type UTermOf [Type] :: *

Methods

unify' :: [Type] -> StateT (Map (TVarOf (UTermOf [Type])) (UTermOf [Type])) m ()