Safe Haskell	None
Language	Haskell2010

Language.PTS.Bound

Contents

Variable
Scope (simple)
ScopeH
Module

Description

Bound "prelude" for Language.PTS.

Synopsis

class Bound (t :: (* -> *) -> * -> *) where
data Var b a
- = B b
- | F a
unvar :: (b -> r) -> (a -> r) -> Var b a -> r
newtype Scope b (f :: * -> *) a = Scope {
- unscope :: f (Var b a)
}
fromScope :: Scope b f a -> f (Var b a)
toScope :: f (Var b a) -> Scope b f a
abstract :: Functor f => (a -> Maybe b) -> f a -> Scope b f a
abstract1Sym :: Functor f => Sym -> f Sym -> Scope IrrSym f Sym
instantiate1 :: Monad f => f a -> Scope n f a -> f a
instantiate1return :: Functor f => a -> Scope IrrSym f a -> f a
instantiate2 :: Monad f => f a -> f a -> Scope IrrSym2 f a -> f a
instantiate2return :: Functor f => a -> a -> Scope IrrSym2 f a -> f a
instantiate3 :: Monad f => f a -> f a -> f a -> Scope IrrSym3 f a -> f a
instantiate3return :: Functor f => a -> a -> a -> Scope IrrSym3 f a -> f a
bindings :: Foldable f => Scope b f a -> [b]
transverseScope :: Functor f => (forall r. g r -> f (h r)) -> Scope b g a -> f (Scope b h a)
liftS :: Functor m => m a -> Scope n m a
unusedScope :: Traversable m => Scope n m a -> Maybe (m a)
newtype ScopeH b (f :: * -> *) (m :: * -> *) a = ScopeH {
- unscopeH :: f (Var b (m a))
}
fromScopeH :: Module f m => ScopeH b f m a -> f (Var b a)
abstractH :: (Functor f, Monad m) => (a -> Maybe b) -> f a -> ScopeH b f m a
abstractHEither :: (Functor f, Monad m) => (a -> Either b c) -> f a -> ScopeH b f m c
abstract1HSym :: (Functor f, Monad m) => Sym -> f Sym -> ScopeH IrrSym f m Sym
abstract2HSym :: (Functor f, Monad m) => Sym -> Sym -> f Sym -> ScopeH IrrSym2 f m Sym
abstract3HSym :: (Functor f, Monad m) => Sym -> Sym -> Sym -> f Sym -> ScopeH IrrSym3 f m Sym
instantiate1H :: Module f m => m a -> ScopeH b f m a -> f a
instantiate1Hreturn :: Module f m => a -> ScopeH IrrSym f m a -> f a
instantiate2H :: Module f m => m a -> m a -> ScopeH IrrSym2 f m a -> f a
instantiate2Hreturn :: Module f m => a -> a -> ScopeH IrrSym2 f m a -> f a
instantiate3H :: Module f m => m a -> m a -> m a -> ScopeH IrrSym3 f m a -> f a
instantiate3Hreturn :: Module f m => a -> a -> a -> ScopeH IrrSym3 f m a -> f a
instantiateHEither :: Module f m => (Either b a -> m c) -> ScopeH b f m a -> f c
bindingsH :: Foldable f => ScopeH b f m a -> [b]
liftH :: (Functor f, Monad m) => f a -> ScopeH n f m a
class (Functor f, Monad m) => Module (f :: * -> *) (m :: * -> *) where

Documentation

class Bound (t :: (* -> *) -> * -> *) where #

Methods

(>>>=) :: Monad f => t f a -> (a -> f c) -> t f c #

Instances

Bound ListT
Instance details Defined in Bound.Class Methods (>>>=) :: Monad f => ListT f a -> (a -> f c) -> ListT f c #
Bound MaybeT
Instance details Defined in Bound.Class Methods (>>>=) :: Monad f => MaybeT f a -> (a -> f c) -> MaybeT f c #
Bound (IdentityT :: (* -> ) -> -> *)
Instance details Defined in Bound.Class Methods (>>>=) :: Monad f => IdentityT f a -> (a -> f c) -> IdentityT f c #
Error e => Bound (ErrorT e)
Instance details Defined in Bound.Class Methods (>>>=) :: Monad f => ErrorT e f a -> (a -> f c) -> ErrorT e f c #
Bound (StateT s)
Instance details Defined in Bound.Class Methods (>>>=) :: Monad f => StateT s f a -> (a -> f c) -> StateT s f c #
Monoid w => Bound (WriterT w)
Instance details Defined in Bound.Class Methods (>>>=) :: Monad f => WriterT w f a -> (a -> f c) -> WriterT w f c #
Bound (Scope b)
Instance details Defined in Bound.Scope Methods (>>>=) :: Monad f => Scope b f a -> (a -> f c) -> Scope b f c #
Bound (Scope b)
Instance details Defined in Bound.Scope.Simple Methods (>>>=) :: Monad f => Scope b f a -> (a -> f c) -> Scope b f c #
Bound (ContT c)
Instance details Defined in Bound.Class Methods (>>>=) :: Monad f => ContT c f a -> (a -> f c0) -> ContT c f c0 #
Bound (ReaderT r :: (* -> ) -> -> *)
Instance details Defined in Bound.Class Methods (>>>=) :: Monad f => ReaderT r f a -> (a -> f c) -> ReaderT r f c #
Monoid w => Bound (RWST r w s)
Instance details Defined in Bound.Class Methods (>>>=) :: Monad f => RWST r w s f a -> (a -> f c) -> RWST r w s f c #

Variable

data Var b a #

Constructors

B b
F a

Instances

Bitraversable Var
Instance details Defined in Bound.Var Methods bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> Var a b -> f (Var c d) Source #
Bifoldable Var
Instance details Defined in Bound.Var Methods bifold :: Monoid m => Var m m -> m Source # bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> Var a b -> m Source # bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> Var a b -> c Source # bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> Var a b -> c Source #
Bifunctor Var
Instance details Defined in Bound.Var Methods bimap :: (a -> b) -> (c -> d) -> Var a c -> Var b d Source # first :: (a -> b) -> Var a c -> Var b c Source # second :: (b -> c) -> Var a b -> Var a c Source #
Eq2 Var
Instance details Defined in Bound.Var Methods liftEq2 :: (a -> b -> Bool) -> (c -> d -> Bool) -> Var a c -> Var b d -> Bool Source #
Ord2 Var
Instance details Defined in Bound.Var Methods liftCompare2 :: (a -> b -> Ordering) -> (c -> d -> Ordering) -> Var a c -> Var b d -> Ordering Source #
Read2 Var
Instance details Defined in Bound.Var Methods liftReadsPrec2 :: (Int -> ReadS a) -> ReadS [a] -> (Int -> ReadS b) -> ReadS [b] -> Int -> ReadS (Var a b) Source # liftReadList2 :: (Int -> ReadS a) -> ReadS [a] -> (Int -> ReadS b) -> ReadS [b] -> ReadS [Var a b] Source # liftReadPrec2 :: ReadPrec a -> ReadPrec [a] -> ReadPrec b -> ReadPrec [b] -> ReadPrec (Var a b) Source # liftReadListPrec2 :: ReadPrec a -> ReadPrec [a] -> ReadPrec b -> ReadPrec [b] -> ReadPrec [Var a b] Source #
Show2 Var
Instance details Defined in Bound.Var Methods liftShowsPrec2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> Int -> Var a b -> ShowS Source # liftShowList2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> [Var a b] -> ShowS Source #
Hashable2 Var
Instance details Defined in Bound.Var Methods liftHashWithSalt2 :: (Int -> a -> Int) -> (Int -> b -> Int) -> Int -> Var a b -> Int
Serial2 Var
Instance details Defined in Bound.Var Methods serializeWith2 :: MonadPut m => (a -> m ()) -> (b -> m ()) -> Var a b -> m () deserializeWith2 :: MonadGet m => m a -> m b -> m (Var a b)
Monad (Var b)
Instance details Defined in Bound.Var Methods (>>=) :: Var b a -> (a -> Var b b0) -> Var b b0 Source # (>>) :: Var b a -> Var b b0 -> Var b b0 Source # return :: a -> Var b a Source # fail :: String -> Var b a Source #
Functor (Var b)
Instance details Defined in Bound.Var Methods fmap :: (a -> b0) -> Var b a -> Var b b0 Source # (<$) :: a -> Var b b0 -> Var b a Source #
Applicative (Var b)
Instance details Defined in Bound.Var Methods pure :: a -> Var b a Source # (<>) :: Var b (a -> b0) -> Var b a -> Var b b0 Source # liftA2 :: (a -> b0 -> c) -> Var b a -> Var b b0 -> Var b c Source # (>) :: Var b a -> Var b b0 -> Var b b0 Source # (<*) :: Var b a -> Var b b0 -> Var b a Source #
Foldable (Var b)
Instance details Defined in Bound.Var Methods fold :: Monoid m => Var b m -> m Source # foldMap :: Monoid m => (a -> m) -> Var b a -> m Source # foldr :: (a -> b0 -> b0) -> b0 -> Var b a -> b0 Source # foldr' :: (a -> b0 -> b0) -> b0 -> Var b a -> b0 Source # foldl :: (b0 -> a -> b0) -> b0 -> Var b a -> b0 Source # foldl' :: (b0 -> a -> b0) -> b0 -> Var b a -> b0 Source # foldr1 :: (a -> a -> a) -> Var b a -> a Source # foldl1 :: (a -> a -> a) -> Var b a -> a Source # toList :: Var b a -> [a] Source # null :: Var b a -> Bool Source # length :: Var b a -> Int Source # elem :: Eq a => a -> Var b a -> Bool Source # maximum :: Ord a => Var b a -> a Source # minimum :: Ord a => Var b a -> a Source # sum :: Num a => Var b a -> a Source # product :: Num a => Var b a -> a Source #
Traversable (Var b)
Instance details Defined in Bound.Var Methods traverse :: Applicative f => (a -> f b0) -> Var b a -> f (Var b b0) Source # sequenceA :: Applicative f => Var b (f a) -> f (Var b a) Source # mapM :: Monad m => (a -> m b0) -> Var b a -> m (Var b b0) Source # sequence :: Monad m => Var b (m a) -> m (Var b a) Source #
Eq b => Eq1 (Var b)
Instance details Defined in Bound.Var Methods liftEq :: (a -> b0 -> Bool) -> Var b a -> Var b b0 -> Bool Source #
Ord b => Ord1 (Var b)
Instance details Defined in Bound.Var Methods liftCompare :: (a -> b0 -> Ordering) -> Var b a -> Var b b0 -> Ordering Source #
Read b => Read1 (Var b)
Instance details Defined in Bound.Var Methods liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (Var b a) Source # liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [Var b a] Source # liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (Var b a) Source # liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [Var b a] Source #
Show b => Show1 (Var b)
Instance details Defined in Bound.Var Methods liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Var b a -> ShowS Source # liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Var b a] -> ShowS Source #
Hashable b => Hashable1 (Var b)
Instance details Defined in Bound.Var Methods liftHashWithSalt :: (Int -> a -> Int) -> Int -> Var b a -> Int
Serial b => Serial1 (Var b)
Instance details Defined in Bound.Var Methods serializeWith :: MonadPut m => (a -> m ()) -> Var b a -> m () deserializeWith :: MonadGet m => m a -> m (Var b a)
PrettyPrec a => PrettyPrec1 (Var a) Source #
Instance details Defined in Language.PTS.Pretty Methods liftPpp :: (Prec -> a0 -> PrettyM Doc) -> Prec -> Var a a0 -> PrettyM Doc Source #
Generic1 (Var b :: * -> *)
Instance details Defined in Bound.Var Associated Types type Rep1 (Var b) :: k -> * Source # Methods from1 :: Var b a -> Rep1 (Var b) a Source # to1 :: Rep1 (Var b) a -> Var b a Source #
(Eq b, Eq a) => Eq (Var b a)
Instance details Defined in Bound.Var Methods (==) :: Var b a -> Var b a -> Bool Source # (/=) :: Var b a -> Var b a -> Bool Source #
(Data b, Data a) => Data (Var b a)
Instance details Defined in Bound.Var Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> Var b a -> c (Var b a) Source # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Var b a) Source # toConstr :: Var b a -> Constr Source # dataTypeOf :: Var b a -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Var b a)) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Var b a)) Source # gmapT :: (forall b0. Data b0 => b0 -> b0) -> Var b a -> Var b a Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var b a -> r Source # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var b a -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Var b a -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Var b a -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Var b a -> m (Var b a) Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Var b a -> m (Var b a) Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Var b a -> m (Var b a) Source #
(Ord b, Ord a) => Ord (Var b a)
Instance details Defined in Bound.Var Methods compare :: Var b a -> Var b a -> Ordering Source # (<) :: Var b a -> Var b a -> Bool Source # (<=) :: Var b a -> Var b a -> Bool Source # (>) :: Var b a -> Var b a -> Bool Source # (>=) :: Var b a -> Var b a -> Bool Source # max :: Var b a -> Var b a -> Var b a Source # min :: Var b a -> Var b a -> Var b a Source #
(Read b, Read a) => Read (Var b a)
Instance details Defined in Bound.Var Methods readsPrec :: Int -> ReadS (Var b a) Source # readList :: ReadS [Var b a] Source # readPrec :: ReadPrec (Var b a) Source # readListPrec :: ReadPrec [Var b a] Source #
(Show b, Show a) => Show (Var b a)
Instance details Defined in Bound.Var Methods showsPrec :: Int -> Var b a -> ShowS Source # show :: Var b a -> String Source # showList :: [Var b a] -> ShowS Source #
Generic (Var b a)
Instance details Defined in Bound.Var Associated Types type Rep (Var b a) :: * -> * Source # Methods from :: Var b a -> Rep (Var b a) x Source # to :: Rep (Var b a) x -> Var b a Source #
(Binary b, Binary a) => Binary (Var b a)
Instance details Defined in Bound.Var Methods put :: Var b a -> Put Source # get :: Get (Var b a) Source # putList :: [Var b a] -> Put Source #
(NFData a, NFData b) => NFData (Var b a)
Instance details Defined in Bound.Var Methods rnf :: Var b a -> () Source #
(Hashable b, Hashable a) => Hashable (Var b a)
Instance details Defined in Bound.Var Methods hashWithSalt :: Int -> Var b a -> Int hash :: Var b a -> Int
(Serial b, Serial a) => Serial (Var b a)
Instance details Defined in Bound.Var Methods serialize :: MonadPut m => Var b a -> m () deserialize :: MonadGet m => m (Var b a)
(Serialize b, Serialize a) => Serialize (Var b a)
Instance details Defined in Bound.Var Methods put :: Putter (Var b a) get :: Get (Var b a)
(PrettyPrec a, PrettyPrec b) => PrettyPrec (Var a b) Source #
Instance details Defined in Language.PTS.Pretty Methods ppp :: Prec -> Var a b -> PrettyM Doc Source #
type Rep1 (Var b :: * -> *)
Instance details Defined in Bound.Var type Rep1 (Var b :: * -> *) = D1 (MetaData "Var" "Bound.Var" "bound-2.0.1-b2119def9c5a269bc73b65a6a2993a468736abb7bf396de0d95b9467a5bdf60e" False) (C1 (MetaCons "B" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 b)) :+: C1 (MetaCons "F" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) Par1))
type Rep (Var b a)
Instance details Defined in Bound.Var type Rep (Var b a) = D1 (MetaData "Var" "Bound.Var" "bound-2.0.1-b2119def9c5a269bc73b65a6a2993a468736abb7bf396de0d95b9467a5bdf60e" False) (C1 (MetaCons "B" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 b)) :+: C1 (MetaCons "F" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a)))

unvar :: (b -> r) -> (a -> r) -> Var b a -> r #

Scope (simple)

newtype Scope b (f :: * -> *) a #

Constructors

Scope
Fields unscope :: f (Var b a)

Instances

MonadTrans (Scope b)
Instance details Defined in Bound.Scope.Simple Methods lift :: Monad m => m a -> Scope b m a Source #
Bound (Scope b)
Instance details Defined in Bound.Scope.Simple Methods (>>>=) :: Monad f => Scope b f a -> (a -> f c) -> Scope b f c #
MFunctor (Scope b :: (* -> ) -> -> *)
Instance details Defined in Bound.Scope.Simple Methods hoist :: Monad m => (forall a. m a -> n a) -> Scope b m b0 -> Scope b n b0
Functor f => Generic1 (Scope b f :: * -> *)
Instance details Defined in Bound.Scope.Simple Associated Types type Rep1 (Scope b f) :: k -> * Source # Methods from1 :: Scope b f a -> Rep1 (Scope b f) a Source # to1 :: Rep1 (Scope b f) a -> Scope b f a Source #
Monad f => Monad (Scope b f)
Instance details Defined in Bound.Scope.Simple Methods (>>=) :: Scope b f a -> (a -> Scope b f b0) -> Scope b f b0 Source # (>>) :: Scope b f a -> Scope b f b0 -> Scope b f b0 Source # return :: a -> Scope b f a Source # fail :: String -> Scope b f a Source #
Functor f => Functor (Scope b f)
Instance details Defined in Bound.Scope.Simple Methods fmap :: (a -> b0) -> Scope b f a -> Scope b f b0 Source # (<$) :: a -> Scope b f b0 -> Scope b f a Source #
Monad f => Applicative (Scope b f)
Instance details Defined in Bound.Scope.Simple Methods pure :: a -> Scope b f a Source # (<>) :: Scope b f (a -> b0) -> Scope b f a -> Scope b f b0 Source # liftA2 :: (a -> b0 -> c) -> Scope b f a -> Scope b f b0 -> Scope b f c Source # (>) :: Scope b f a -> Scope b f b0 -> Scope b f b0 Source # (<*) :: Scope b f a -> Scope b f b0 -> Scope b f a Source #
Foldable f => Foldable (Scope b f)
Instance details Defined in Bound.Scope.Simple Methods fold :: Monoid m => Scope b f m -> m Source # foldMap :: Monoid m => (a -> m) -> Scope b f a -> m Source # foldr :: (a -> b0 -> b0) -> b0 -> Scope b f a -> b0 Source # foldr' :: (a -> b0 -> b0) -> b0 -> Scope b f a -> b0 Source # foldl :: (b0 -> a -> b0) -> b0 -> Scope b f a -> b0 Source # foldl' :: (b0 -> a -> b0) -> b0 -> Scope b f a -> b0 Source # foldr1 :: (a -> a -> a) -> Scope b f a -> a Source # foldl1 :: (a -> a -> a) -> Scope b f a -> a Source # toList :: Scope b f a -> [a] Source # null :: Scope b f a -> Bool Source # length :: Scope b f a -> Int Source # elem :: Eq a => a -> Scope b f a -> Bool Source # maximum :: Ord a => Scope b f a -> a Source # minimum :: Ord a => Scope b f a -> a Source # sum :: Num a => Scope b f a -> a Source # product :: Num a => Scope b f a -> a Source #
Traversable f => Traversable (Scope b f)
Instance details Defined in Bound.Scope.Simple Methods traverse :: Applicative f0 => (a -> f0 b0) -> Scope b f a -> f0 (Scope b f b0) Source # sequenceA :: Applicative f0 => Scope b f (f0 a) -> f0 (Scope b f a) Source # mapM :: Monad m => (a -> m b0) -> Scope b f a -> m (Scope b f b0) Source # sequence :: Monad m => Scope b f (m a) -> m (Scope b f a) Source #
(Eq b, Eq1 f) => Eq1 (Scope b f)
Instance details Defined in Bound.Scope.Simple Methods liftEq :: (a -> b0 -> Bool) -> Scope b f a -> Scope b f b0 -> Bool Source #
(Ord b, Ord1 f) => Ord1 (Scope b f)
Instance details Defined in Bound.Scope.Simple Methods liftCompare :: (a -> b0 -> Ordering) -> Scope b f a -> Scope b f b0 -> Ordering Source #
(Read b, Read1 f) => Read1 (Scope b f)
Instance details Defined in Bound.Scope.Simple Methods liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (Scope b f a) Source # liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [Scope b f a] Source # liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (Scope b f a) Source # liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [Scope b f a] Source #
(Show b, Show1 f) => Show1 (Scope b f)
Instance details Defined in Bound.Scope.Simple Methods liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Scope b f a -> ShowS Source # liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Scope b f a] -> ShowS Source #
(Hashable b, Hashable1 f) => Hashable1 (Scope b f)
Instance details Defined in Bound.Scope.Simple Methods liftHashWithSalt :: (Int -> a -> Int) -> Int -> Scope b f a -> Int
(Serial b, Serial1 f) => Serial1 (Scope b f)
Instance details Defined in Bound.Scope.Simple Methods serializeWith :: MonadPut m => (a -> m ()) -> Scope b f a -> m () deserializeWith :: MonadGet m => m a -> m (Scope b f a)
(Eq b, Eq1 f, Eq a) => Eq (Scope b f a)
Instance details Defined in Bound.Scope.Simple Methods (==) :: Scope b f a -> Scope b f a -> Bool Source # (/=) :: Scope b f a -> Scope b f a -> Bool Source #
(Typeable b, Typeable f, Data a, Data (f (Var b a))) => Data (Scope b f a)
Instance details Defined in Bound.Scope.Simple Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> Scope b f a -> c (Scope b f a) Source # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Scope b f a) Source # toConstr :: Scope b f a -> Constr Source # dataTypeOf :: Scope b f a -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Scope b f a)) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Scope b f a)) Source # gmapT :: (forall b0. Data b0 => b0 -> b0) -> Scope b f a -> Scope b f a Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Scope b f a -> r Source # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Scope b f a -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Scope b f a -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Scope b f a -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Scope b f a -> m (Scope b f a) Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Scope b f a -> m (Scope b f a) Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Scope b f a -> m (Scope b f a) Source #
(Ord b, Ord1 f, Ord a) => Ord (Scope b f a)
Instance details Defined in Bound.Scope.Simple Methods compare :: Scope b f a -> Scope b f a -> Ordering Source # (<) :: Scope b f a -> Scope b f a -> Bool Source # (<=) :: Scope b f a -> Scope b f a -> Bool Source # (>) :: Scope b f a -> Scope b f a -> Bool Source # (>=) :: Scope b f a -> Scope b f a -> Bool Source # max :: Scope b f a -> Scope b f a -> Scope b f a Source # min :: Scope b f a -> Scope b f a -> Scope b f a Source #
(Read b, Read1 f, Read a) => Read (Scope b f a)
Instance details Defined in Bound.Scope.Simple Methods readsPrec :: Int -> ReadS (Scope b f a) Source # readList :: ReadS [Scope b f a] Source # readPrec :: ReadPrec (Scope b f a) Source # readListPrec :: ReadPrec [Scope b f a] Source #
(Show b, Show1 f, Show a) => Show (Scope b f a)
Instance details Defined in Bound.Scope.Simple Methods showsPrec :: Int -> Scope b f a -> ShowS Source # show :: Scope b f a -> String Source # showList :: [Scope b f a] -> ShowS Source #
Generic (Scope b f a)
Instance details Defined in Bound.Scope.Simple Associated Types type Rep (Scope b f a) :: * -> * Source # Methods from :: Scope b f a -> Rep (Scope b f a) x Source # to :: Rep (Scope b f a) x -> Scope b f a Source #
(Binary b, Serial1 f, Binary a) => Binary (Scope b f a)
Instance details Defined in Bound.Scope.Simple Methods put :: Scope b f a -> Put Source # get :: Get (Scope b f a) Source # putList :: [Scope b f a] -> Put Source #
NFData (f (Var b a)) => NFData (Scope b f a)
Instance details Defined in Bound.Scope.Simple Methods rnf :: Scope b f a -> () Source #
(Hashable b, Hashable1 f, Hashable a) => Hashable (Scope b f a)
Instance details Defined in Bound.Scope.Simple Methods hashWithSalt :: Int -> Scope b f a -> Int hash :: Scope b f a -> Int
(Serial b, Serial1 f, Serial a) => Serial (Scope b f a)
Instance details Defined in Bound.Scope.Simple Methods serialize :: MonadPut m => Scope b f a -> m () deserialize :: MonadGet m => m (Scope b f a)
(Serialize b, Serial1 f, Serialize a) => Serialize (Scope b f a)
Instance details Defined in Bound.Scope.Simple Methods put :: Putter (Scope b f a) get :: Get (Scope b f a)
type Rep1 (Scope b f :: * -> *)
Instance details Defined in Bound.Scope.Simple type Rep1 (Scope b f :: * -> *) = D1 (MetaData "Scope" "Bound.Scope.Simple" "bound-2.0.1-b2119def9c5a269bc73b65a6a2993a468736abb7bf396de0d95b9467a5bdf60e" True) (C1 (MetaCons "Scope" PrefixI True) (S1 (MetaSel (Just "unscope") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (f :.: Rec1 (Var b))))
type Rep (Scope b f a)
Instance details Defined in Bound.Scope.Simple type Rep (Scope b f a) = D1 (MetaData "Scope" "Bound.Scope.Simple" "bound-2.0.1-b2119def9c5a269bc73b65a6a2993a468736abb7bf396de0d95b9467a5bdf60e" True) (C1 (MetaCons "Scope" PrefixI True) (S1 (MetaSel (Just "unscope") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (f (Var b a)))))

fromScope :: Scope b f a -> f (Var b a) #

toScope :: f (Var b a) -> Scope b f a #

abstract :: Functor f => (a -> Maybe b) -> f a -> Scope b f a #

abstract1Sym :: Functor f => Sym -> f Sym -> Scope IrrSym f Sym Source #

instantiate1 :: Monad f => f a -> Scope n f a -> f a #

instantiate1return :: Functor f => a -> Scope IrrSym f a -> f a Source #

instantiate2 :: Monad f => f a -> f a -> Scope IrrSym2 f a -> f a Source #

instantiate2return :: Functor f => a -> a -> Scope IrrSym2 f a -> f a Source #

instantiate3 :: Monad f => f a -> f a -> f a -> Scope IrrSym3 f a -> f a Source #

instantiate3return :: Functor f => a -> a -> a -> Scope IrrSym3 f a -> f a Source #

bindings :: Foldable f => Scope b f a -> [b] #

transverseScope :: Functor f => (forall r. g r -> f (h r)) -> Scope b g a -> f (Scope b h a) #

liftS :: Functor m => m a -> Scope n m a Source #

unusedScope :: Traversable m => Scope n m a -> Maybe (m a) Source #

ScopeH

newtype ScopeH b (f :: * -> *) (m :: * -> *) a #

Constructors

ScopeH
Fields unscopeH :: f (Var b (m a))

Instances

(Functor f, Functor m) => Functor (ScopeH b f m)
Instance details Defined in Bound.ScopeH Methods fmap :: (a -> b0) -> ScopeH b f m a -> ScopeH b f m b0 Source # (<$) :: a -> ScopeH b f m b0 -> ScopeH b f m a Source #
(Foldable f, Foldable m) => Foldable (ScopeH b f m)
Instance details Defined in Bound.ScopeH Methods fold :: Monoid m0 => ScopeH b f m m0 -> m0 Source # foldMap :: Monoid m0 => (a -> m0) -> ScopeH b f m a -> m0 Source # foldr :: (a -> b0 -> b0) -> b0 -> ScopeH b f m a -> b0 Source # foldr' :: (a -> b0 -> b0) -> b0 -> ScopeH b f m a -> b0 Source # foldl :: (b0 -> a -> b0) -> b0 -> ScopeH b f m a -> b0 Source # foldl' :: (b0 -> a -> b0) -> b0 -> ScopeH b f m a -> b0 Source # foldr1 :: (a -> a -> a) -> ScopeH b f m a -> a Source # foldl1 :: (a -> a -> a) -> ScopeH b f m a -> a Source # toList :: ScopeH b f m a -> [a] Source # null :: ScopeH b f m a -> Bool Source # length :: ScopeH b f m a -> Int Source # elem :: Eq a => a -> ScopeH b f m a -> Bool Source # maximum :: Ord a => ScopeH b f m a -> a Source # minimum :: Ord a => ScopeH b f m a -> a Source # sum :: Num a => ScopeH b f m a -> a Source # product :: Num a => ScopeH b f m a -> a Source #
(Traversable f, Traversable m) => Traversable (ScopeH b f m)
Instance details Defined in Bound.ScopeH Methods traverse :: Applicative f0 => (a -> f0 b0) -> ScopeH b f m a -> f0 (ScopeH b f m b0) Source # sequenceA :: Applicative f0 => ScopeH b f m (f0 a) -> f0 (ScopeH b f m a) Source # mapM :: Monad m0 => (a -> m0 b0) -> ScopeH b f m a -> m0 (ScopeH b f m b0) Source # sequence :: Monad m0 => ScopeH b f m (m0 a) -> m0 (ScopeH b f m a) Source #
(Module f m, Eq b, Eq1 f, Eq1 m) => Eq1 (ScopeH b f m)
Instance details Defined in Bound.ScopeH Methods liftEq :: (a -> b0 -> Bool) -> ScopeH b f m a -> ScopeH b f m b0 -> Bool Source #
(Module f m, Ord b, Ord1 f, Ord1 m) => Ord1 (ScopeH b f m)
Instance details Defined in Bound.ScopeH Methods liftCompare :: (a -> b0 -> Ordering) -> ScopeH b f m a -> ScopeH b f m b0 -> Ordering Source #
(Read b, Read1 f, Read1 m) => Read1 (ScopeH b f m)
Instance details Defined in Bound.ScopeH Methods liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (ScopeH b f m a) Source # liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [ScopeH b f m a] Source # liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (ScopeH b f m a) Source # liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [ScopeH b f m a] Source #
(Show b, Show1 f, Show1 m) => Show1 (ScopeH b f m)
Instance details Defined in Bound.ScopeH Methods liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> ScopeH b f m a -> ShowS Source # liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [ScopeH b f m a] -> ShowS Source #
(Hashable b, Module f m, Hashable1 f, Hashable1 m) => Hashable1 (ScopeH b f m)
Instance details Defined in Bound.ScopeH Methods liftHashWithSalt :: (Int -> a -> Int) -> Int -> ScopeH b f m a -> Int
(Functor f, Monad m) => Module (ScopeH b f m) m
Instance details Defined in Bound.ScopeH Methods (>>==) :: ScopeH b f m a -> (a -> m b0) -> ScopeH b f m b0 #
(Module f m, Eq b, Eq1 f, Eq1 m, Eq a) => Eq (ScopeH b f m a)
Instance details Defined in Bound.ScopeH Methods (==) :: ScopeH b f m a -> ScopeH b f m a -> Bool Source # (/=) :: ScopeH b f m a -> ScopeH b f m a -> Bool Source #
(Module f m, Ord b, Ord1 f, Ord1 m, Ord a) => Ord (ScopeH b f m a)
Instance details Defined in Bound.ScopeH Methods compare :: ScopeH b f m a -> ScopeH b f m a -> Ordering Source # (<) :: ScopeH b f m a -> ScopeH b f m a -> Bool Source # (<=) :: ScopeH b f m a -> ScopeH b f m a -> Bool Source # (>) :: ScopeH b f m a -> ScopeH b f m a -> Bool Source # (>=) :: ScopeH b f m a -> ScopeH b f m a -> Bool Source # max :: ScopeH b f m a -> ScopeH b f m a -> ScopeH b f m a Source # min :: ScopeH b f m a -> ScopeH b f m a -> ScopeH b f m a Source #
(Read b, Read1 f, Read1 m, Read a) => Read (ScopeH b f m a)
Instance details Defined in Bound.ScopeH Methods readsPrec :: Int -> ReadS (ScopeH b f m a) Source # readList :: ReadS [ScopeH b f m a] Source # readPrec :: ReadPrec (ScopeH b f m a) Source # readListPrec :: ReadPrec [ScopeH b f m a] Source #
(Show b, Show1 f, Show1 m, Show a) => Show (ScopeH b f m a)
Instance details Defined in Bound.ScopeH Methods showsPrec :: Int -> ScopeH b f m a -> ShowS Source # show :: ScopeH b f m a -> String Source # showList :: [ScopeH b f m a] -> ShowS Source #
NFData (f (Var b (m a))) => NFData (ScopeH b f m a)
Instance details Defined in Bound.ScopeH Methods rnf :: ScopeH b f m a -> () Source #
(Hashable b, Module f m, Hashable1 f, Hashable1 m, Hashable a) => Hashable (ScopeH b f m a)
Instance details Defined in Bound.ScopeH Methods hashWithSalt :: Int -> ScopeH b f m a -> Int hash :: ScopeH b f m a -> Int

fromScopeH :: Module f m => ScopeH b f m a -> f (Var b a) #

abstractH :: (Functor f, Monad m) => (a -> Maybe b) -> f a -> ScopeH b f m a #

abstractHEither :: (Functor f, Monad m) => (a -> Either b c) -> f a -> ScopeH b f m c #

abstract1HSym :: (Functor f, Monad m) => Sym -> f Sym -> ScopeH IrrSym f m Sym Source #

Abstract over a single variable

abstract2HSym :: (Functor f, Monad m) => Sym -> Sym -> f Sym -> ScopeH IrrSym2 f m Sym Source #

Abstract over two variables

abstract3HSym :: (Functor f, Monad m) => Sym -> Sym -> Sym -> f Sym -> ScopeH IrrSym3 f m Sym Source #

Abstract over tree variables

instantiate1H :: Module f m => m a -> ScopeH b f m a -> f a #

instantiate1Hreturn :: Module f m => a -> ScopeH IrrSym f m a -> f a Source #

instantiate2H :: Module f m => m a -> m a -> ScopeH IrrSym2 f m a -> f a Source #

instantiate2Hreturn :: Module f m => a -> a -> ScopeH IrrSym2 f m a -> f a Source #

instantiate3H :: Module f m => m a -> m a -> m a -> ScopeH IrrSym3 f m a -> f a Source #

instantiate3Hreturn :: Module f m => a -> a -> a -> ScopeH IrrSym3 f m a -> f a Source #

instantiateHEither :: Module f m => (Either b a -> m c) -> ScopeH b f m a -> f c #

bindingsH :: Foldable f => ScopeH b f m a -> [b] #

liftH :: (Functor f, Monad m) => f a -> ScopeH n f m a Source #

Module

class (Functor f, Monad m) => Module (f :: * -> *) (m :: * -> *) where #

Minimal complete definition

(>>==)

Methods

(>>==) :: f a -> (a -> m b) -> f b #

Instances

Monad m => Module m Identity
Instance details Defined in Control.Monad.Module Methods (>>==) :: m a -> (a -> Identity b) -> m b #
Module (TermChk s) (TermInf s) #
Instance details Defined in Language.PTS.Term Methods (>>==) :: TermChk s a -> (a -> TermInf s b) -> TermChk s b #
Module (TermInf s) (TermInf s) #
Instance details Defined in Language.PTS.Term Methods (>>==) :: TermInf s a -> (a -> TermInf s b) -> TermInf s b #
Monad m => Module (Scope b m) m
Instance details Defined in Control.Monad.Module Methods (>>==) :: Scope b m a -> (a -> m b0) -> Scope b m b0 #
(PrettyPrec err, AsErr err, Specification s) => Module (ValueIntro err s) (ValueElim err s) #
Instance details Defined in Language.PTS.Value Methods (>>==) :: ValueIntro err s a -> (a -> ValueElim err s b) -> ValueIntro err s b #
(Functor f, Monad m) => Module (ScopeH b f m) m
Instance details Defined in Bound.ScopeH Methods (>>==) :: ScopeH b f m a -> (a -> m b0) -> ScopeH b f m b0 #