{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
#if __GLASGOW_HASKELL__ >= 805
{-# LANGUAGE QuantifiedConstraints #-}
#endif
{-# LANGUAGE UndecidableInstances #-}
module Bound.ScopeT (
ScopeT (..),
(>>>>=),
abstractT, abstract1T, abstractTEither,
abstractTName, abstract1TName,
instantiateT, instantiate1T, instantiateTEither,
liftScopeT,
fromScopeT,
toScopeT,
lowerScopeT,
splatT,
bindingsT,
mapBoundT,
mapScopeT,
foldMapBoundT,
foldMapScopeT,
traverseBoundT_,
traverseScopeT_,
traverseBoundT,
traverseScopeT,
bitransverseScopeT,
) where
import Bound (Bound (..), Scope (..), Var (..))
import Bound.Name (Name (..))
import Control.DeepSeq (NFData (..))
import Control.Monad.Module (Module (..), LiftedModule (..))
import Data.Bifoldable (bifoldMap, bitraverse_)
import Data.Bifunctor (bimap)
import Data.Bitraversable (Bitraversable (..))
import Data.Foldable (traverse_)
import Data.Functor.Classes
import Data.Hashable (Hashable (..))
import Data.Hashable.Lifted (Hashable1 (..), hashWithSalt1)
newtype ScopeT b t f a = ScopeT { ScopeT b t f a -> t f (Var b (f a))
unscopeT :: t f (Var b (f a)) }
instance (Functor (t f), Functor f) => Functor (ScopeT b t f) where
fmap :: (a -> b) -> ScopeT b t f a -> ScopeT b t f b
fmap a -> b
f (ScopeT t f (Var b (f a))
a) = t f (Var b (f b)) -> ScopeT b t f b
forall b (t :: (* -> *) -> * -> *) (f :: * -> *) a.
t f (Var b (f a)) -> ScopeT b t f a
ScopeT (t f (Var b (f b)) -> ScopeT b t f b)
-> t f (Var b (f b)) -> ScopeT b t f b
forall a b. (a -> b) -> a -> b
$ (Var b (f a) -> Var b (f b))
-> t f (Var b (f a)) -> t f (Var b (f b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f a -> f b) -> Var b (f a) -> Var b (f b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f)) t f (Var b (f a))
a
instance (Foldable (t f), Foldable f) => Foldable (ScopeT b t f) where
foldMap :: (a -> m) -> ScopeT b t f a -> m
foldMap a -> m
f (ScopeT t f (Var b (f a))
a) = (Var b (f a) -> m) -> t f (Var b (f a)) -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((f a -> m) -> Var b (f a) -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((a -> m) -> f a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f)) t f (Var b (f a))
a
foldr :: (a -> b -> b) -> b -> ScopeT b t f a -> b
foldr a -> b -> b
f b
z (ScopeT t f (Var b (f a))
a) = (Var b (f a) -> b -> b) -> b -> t f (Var b (f a)) -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((b -> Var b (f a) -> b) -> Var b (f a) -> b -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((f a -> b -> b) -> b -> Var b (f a) -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((b -> f a -> b) -> f a -> b -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((a -> b -> b) -> b -> f a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> b -> b
f)))) b
z t f (Var b (f a))
a
instance (Traversable (t f), Traversable f) => Traversable (ScopeT b t f) where
traverse :: (a -> f b) -> ScopeT b t f a -> f (ScopeT b t f b)
traverse a -> f b
f (ScopeT t f (Var b (f a))
a) = t f (Var b (f b)) -> ScopeT b t f b
forall b (t :: (* -> *) -> * -> *) (f :: * -> *) a.
t f (Var b (f a)) -> ScopeT b t f a
ScopeT (t f (Var b (f b)) -> ScopeT b t f b)
-> f (t f (Var b (f b))) -> f (ScopeT b t f b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var b (f a) -> f (Var b (f b)))
-> t f (Var b (f a)) -> f (t f (Var b (f b)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((f a -> f (f b)) -> Var b (f a) -> f (Var b (f b))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((a -> f b) -> f a -> f (f b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f)) t f (Var b (f a))
a
(>>>>=) :: (Monad f, Functor (t f)) => ScopeT b t f a -> (a -> f c) -> ScopeT b t f c
ScopeT t f (Var b (f a))
m >>>>= :: ScopeT b t f a -> (a -> f c) -> ScopeT b t f c
>>>>= a -> f c
k = t f (Var b (f c)) -> ScopeT b t f c
forall b (t :: (* -> *) -> * -> *) (f :: * -> *) a.
t f (Var b (f a)) -> ScopeT b t f a
ScopeT (t f (Var b (f c)) -> ScopeT b t f c)
-> t f (Var b (f c)) -> ScopeT b t f c
forall a b. (a -> b) -> a -> b
$ (Var b (f a) -> Var b (f c))
-> t f (Var b (f a)) -> t f (Var b (f c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f a -> f c) -> Var b (f a) -> Var b (f c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (f a -> (a -> f c) -> f c
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> f c
k)) t f (Var b (f a))
m
{-# INLINE (>>>>=) #-}
#if __GLASGOW_HASKELL__ >= 805
instance (forall f. Functor f => Functor (t f)) => Bound (ScopeT n t) where
>>>= :: ScopeT n t f a -> (a -> f c) -> ScopeT n t f c
(>>>=) = ScopeT n t f a -> (a -> f c) -> ScopeT n t f c
forall (f :: * -> *) (t :: (* -> *) -> * -> *) b a c.
(Monad f, Functor (t f)) =>
ScopeT b t f a -> (a -> f c) -> ScopeT b t f c
(>>>>=)
#endif
instance (Monad f, Functor (t f)) => Module (ScopeT b t f) f where
>>== :: ScopeT b t f a -> (a -> f b) -> ScopeT b t f b
(>>==) = ScopeT b t f a -> (a -> f b) -> ScopeT b t f b
forall (f :: * -> *) (t :: (* -> *) -> * -> *) b a c.
(Monad f, Functor (t f)) =>
ScopeT b t f a -> (a -> f c) -> ScopeT b t f c
(>>>>=)
instance (Monad f, Monad (t f)) => LiftedModule (ScopeT b t f) f where
mlift :: f a -> ScopeT b t f a
mlift = f a -> ScopeT b t f a
forall (t :: (* -> *) -> * -> *) (f :: * -> *) a b.
Monad (t f) =>
f a -> ScopeT b t f a
liftScopeT
instance (Hashable b, Bound t, Monad f, Hashable1 f, Hashable1 (t f)) => Hashable1 (ScopeT b t f) where
liftHashWithSalt :: (Int -> a -> Int) -> Int -> ScopeT b t f a -> Int
liftHashWithSalt Int -> a -> Int
h Int
s ScopeT b t f a
m = (Int -> Var b a -> Int) -> Int -> t f (Var b a) -> Int
forall (t :: * -> *) a.
Hashable1 t =>
(Int -> a -> Int) -> Int -> t a -> Int
liftHashWithSalt ((Int -> a -> Int) -> Int -> Var b a -> Int
forall (t :: * -> *) a.
Hashable1 t =>
(Int -> a -> Int) -> Int -> t a -> Int
liftHashWithSalt Int -> a -> Int
h) Int
s (ScopeT b t f a -> t f (Var b a)
forall (t :: (* -> *) -> * -> *) (f :: * -> *) b a.
(Bound t, Monad f) =>
ScopeT b t f a -> t f (Var b a)
fromScopeT ScopeT b t f a
m)
{-# INLINE liftHashWithSalt #-}
instance (Hashable b, Bound t, Monad f, Hashable1 f, Hashable1 (t f), Hashable a) => Hashable (ScopeT b t f a) where
hashWithSalt :: Int -> ScopeT b t f a -> Int
hashWithSalt Int
n ScopeT b t f a
m = Int -> t f (Var b a) -> Int
forall (f :: * -> *) a.
(Hashable1 f, Hashable a) =>
Int -> f a -> Int
hashWithSalt1 Int
n (ScopeT b t f a -> t f (Var b a)
forall (t :: (* -> *) -> * -> *) (f :: * -> *) b a.
(Bound t, Monad f) =>
ScopeT b t f a -> t f (Var b a)
fromScopeT ScopeT b t f a
m)
{-# INLINE hashWithSalt #-}
instance NFData (t f (Var b (f a))) => NFData (ScopeT b t f a) where
rnf :: ScopeT b t f a -> ()
rnf ScopeT b t f a
scope = t f (Var b (f a)) -> ()
forall a. NFData a => a -> ()
rnf (ScopeT b t f a -> t f (Var b (f a))
forall b (t :: (* -> *) -> * -> *) (f :: * -> *) a.
ScopeT b t f a -> t f (Var b (f a))
unscopeT ScopeT b t f a
scope)
instance (Monad f, Bound t, Eq b, Eq1 (t f), Eq1 f, Eq a) => Eq (ScopeT b t f a) where == :: ScopeT b t f a -> ScopeT b t f a -> Bool
(==) = ScopeT b t f a -> ScopeT b t f a -> Bool
forall (f :: * -> *) a. (Eq1 f, Eq a) => f a -> f a -> Bool
eq1
instance (Monad f, Bound t, Ord b, Ord1 (t f), Ord1 f, Ord a) => Ord (ScopeT b t f a) where compare :: ScopeT b t f a -> ScopeT b t f a -> Ordering
compare = ScopeT b t f a -> ScopeT b t f a -> Ordering
forall (f :: * -> *) a. (Ord1 f, Ord a) => f a -> f a -> Ordering
compare1
instance (Show b, Show1 (t f), Show1 f, Show a) => Show (ScopeT b t f a) where showsPrec :: Int -> ScopeT b t f a -> ShowS
showsPrec = Int -> ScopeT b t f a -> ShowS
forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1
instance (Read b, Read1 (t f), Read1 f, Read a) => Read (ScopeT b t f a) where readsPrec :: Int -> ReadS (ScopeT b t f a)
readsPrec = Int -> ReadS (ScopeT b t f a)
forall (f :: * -> *) a. (Read1 f, Read a) => Int -> ReadS (f a)
readsPrec1
instance (Monad f, Bound t, Eq b, Eq1 (t f), Eq1 f) => Eq1 (ScopeT b t f) where
liftEq :: (a -> b -> Bool) -> ScopeT b t f a -> ScopeT b t f b -> Bool
liftEq a -> b -> Bool
f ScopeT b t f a
m ScopeT b t f b
n = (Var b a -> Var b b -> Bool)
-> t f (Var b a) -> t f (Var b b) -> Bool
forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq ((a -> b -> Bool) -> Var b a -> Var b b -> Bool
forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
f) (ScopeT b t f a -> t f (Var b a)
forall (t :: (* -> *) -> * -> *) (f :: * -> *) b a.
(Bound t, Monad f) =>
ScopeT b t f a -> t f (Var b a)
fromScopeT ScopeT b t f a
m) (ScopeT b t f b -> t f (Var b b)
forall (t :: (* -> *) -> * -> *) (f :: * -> *) b a.
(Bound t, Monad f) =>
ScopeT b t f a -> t f (Var b a)
fromScopeT ScopeT b t f b
n)
instance (Monad f, Bound t, Ord b, Ord1 (t f), Ord1 f) => Ord1 (ScopeT b t f) where
liftCompare :: (a -> b -> Ordering)
-> ScopeT b t f a -> ScopeT b t f b -> Ordering
liftCompare a -> b -> Ordering
f ScopeT b t f a
m ScopeT b t f b
n = (Var b a -> Var b b -> Ordering)
-> t f (Var b a) -> t f (Var b b) -> Ordering
forall (f :: * -> *) a b.
Ord1 f =>
(a -> b -> Ordering) -> f a -> f b -> Ordering
liftCompare ((a -> b -> Ordering) -> Var b a -> Var b b -> Ordering
forall (f :: * -> *) a b.
Ord1 f =>
(a -> b -> Ordering) -> f a -> f b -> Ordering
liftCompare a -> b -> Ordering
f) (ScopeT b t f a -> t f (Var b a)
forall (t :: (* -> *) -> * -> *) (f :: * -> *) b a.
(Bound t, Monad f) =>
ScopeT b t f a -> t f (Var b a)
fromScopeT ScopeT b t f a
m) (ScopeT b t f b -> t f (Var b b)
forall (t :: (* -> *) -> * -> *) (f :: * -> *) b a.
(Bound t, Monad f) =>
ScopeT b t f a -> t f (Var b a)
fromScopeT ScopeT b t f b
n)
instance (Show b, Show1 (t f), Show1 f) => Show1 (ScopeT b t f) where
liftShowsPrec :: (Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> ScopeT b t f a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl Int
d (ScopeT t f (Var b (f a))
x) = (Int -> t f (Var b (f a)) -> ShowS)
-> String -> Int -> t f (Var b (f a)) -> ShowS
forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith
((Int -> Var b (f a) -> ShowS)
-> ([Var b (f a)] -> ShowS) -> Int -> t f (Var b (f a)) -> ShowS
forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
liftShowsPrec ((Int -> f a -> ShowS)
-> ([f a] -> ShowS) -> Int -> Var b (f a) -> ShowS
forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
liftShowsPrec Int -> f a -> ShowS
sp' [f a] -> ShowS
sl') ((Int -> f a -> ShowS) -> ([f a] -> ShowS) -> [Var b (f a)] -> ShowS
forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [f a] -> ShowS
liftShowList Int -> f a -> ShowS
sp' [f a] -> ShowS
sl'))
String
"ScopeT" Int
d t f (Var b (f a))
x
where
sp' :: Int -> f a -> ShowS
sp' = (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl
sl' :: [f a] -> ShowS
sl' = (Int -> a -> ShowS) -> ([a] -> ShowS) -> [f a] -> ShowS
forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [f a] -> ShowS
liftShowList Int -> a -> ShowS
sp [a] -> ShowS
sl
instance (Read b, Read1 (t f), Read1 f) => Read1 (ScopeT b t f) where
liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (ScopeT b t f a)
liftReadsPrec Int -> ReadS a
f ReadS [a]
g = (String -> ReadS (ScopeT b t f a)) -> Int -> ReadS (ScopeT b t f a)
forall a. (String -> ReadS a) -> Int -> ReadS a
readsData ((String -> ReadS (ScopeT b t f a))
-> Int -> ReadS (ScopeT b t f a))
-> (String -> ReadS (ScopeT b t f a))
-> Int
-> ReadS (ScopeT b t f a)
forall a b. (a -> b) -> a -> b
$ (Int -> ReadS (t f (Var b (f a))))
-> String
-> (t f (Var b (f a)) -> ScopeT b t f a)
-> String
-> ReadS (ScopeT b t f a)
forall a t.
(Int -> ReadS a) -> String -> (a -> t) -> String -> ReadS t
readsUnaryWith
((Int -> ReadS (Var b (f a)))
-> ReadS [Var b (f a)] -> Int -> ReadS (t f (Var b (f a)))
forall (f :: * -> *) a.
Read1 f =>
(Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (f a)
liftReadsPrec ((Int -> ReadS (f a)) -> ReadS [f a] -> Int -> ReadS (Var b (f a))
forall (f :: * -> *) a.
Read1 f =>
(Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (f a)
liftReadsPrec Int -> ReadS (f a)
f' ReadS [f a]
g') ((Int -> ReadS (f a)) -> ReadS [f a] -> ReadS [Var b (f a)]
forall (f :: * -> *) a.
Read1 f =>
(Int -> ReadS a) -> ReadS [a] -> ReadS [f a]
liftReadList Int -> ReadS (f a)
f' ReadS [f a]
g'))
String
"ScopeT" t f (Var b (f a)) -> ScopeT b t f a
forall b (t :: (* -> *) -> * -> *) (f :: * -> *) a.
t f (Var b (f a)) -> ScopeT b t f a
ScopeT
where
f' :: Int -> ReadS (f a)
f' = (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (f a)
forall (f :: * -> *) a.
Read1 f =>
(Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (f a)
liftReadsPrec Int -> ReadS a
f ReadS [a]
g
g' :: ReadS [f a]
g' = (Int -> ReadS a) -> ReadS [a] -> ReadS [f a]
forall (f :: * -> *) a.
Read1 f =>
(Int -> ReadS a) -> ReadS [a] -> ReadS [f a]
liftReadList Int -> ReadS a
f ReadS [a]
g
abstractT :: (Functor (t f), Monad f) => (a -> Maybe b) -> t f a -> ScopeT b t f a
abstractT :: (a -> Maybe b) -> t f a -> ScopeT b t f a
abstractT a -> Maybe b
f t f a
e = t f (Var b (f a)) -> ScopeT b t f a
forall b (t :: (* -> *) -> * -> *) (f :: * -> *) a.
t f (Var b (f a)) -> ScopeT b t f a
ScopeT ((a -> Var b (f a)) -> t f a -> t f (Var b (f a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Var b (f a)
forall (m :: * -> *). Monad m => a -> Var b (m a)
k t f a
e) where
k :: a -> Var b (m a)
k a
y = case a -> Maybe b
f a
y of
Just b
z -> b -> Var b (m a)
forall b a. b -> Var b a
B b
z
Maybe b
Nothing -> m a -> Var b (m a)
forall b a. a -> Var b a
F (a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
y)
{-# INLINE abstractT #-}
abstract1T :: (Functor (t f), Monad f, Eq a) => a -> t f a -> ScopeT () t f a
abstract1T :: a -> t f a -> ScopeT () t f a
abstract1T a
a = (a -> Maybe ()) -> t f a -> ScopeT () t f a
forall (t :: (* -> *) -> * -> *) (f :: * -> *) a b.
(Functor (t f), Monad f) =>
(a -> Maybe b) -> t f a -> ScopeT b t f a
abstractT (\a
b -> if a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b then () -> Maybe ()
forall a. a -> Maybe a
Just () else Maybe ()
forall a. Maybe a
Nothing)
{-# INLINE abstract1T #-}
abstractTEither :: (Functor (t f), Monad f) => (a -> Either b c) -> t f a -> ScopeT b t f c
abstractTEither :: (a -> Either b c) -> t f a -> ScopeT b t f c
abstractTEither a -> Either b c
f t f a
e = t f (Var b (f c)) -> ScopeT b t f c
forall b (t :: (* -> *) -> * -> *) (f :: * -> *) a.
t f (Var b (f a)) -> ScopeT b t f a
ScopeT ((a -> Var b (f c)) -> t f a -> t f (Var b (f c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Var b (f c)
forall (m :: * -> *). Monad m => a -> Var b (m c)
k t f a
e) where
k :: a -> Var b (m c)
k a
y = case a -> Either b c
f a
y of
Left b
z -> b -> Var b (m c)
forall b a. b -> Var b a
B b
z
Right c
y' -> m c -> Var b (m c)
forall b a. a -> Var b a
F (c -> m c
forall (m :: * -> *) a. Monad m => a -> m a
return c
y')
{-# INLINE abstractTEither #-}
abstractTName :: (Functor (t f), Monad f) => (a -> Maybe b) -> t f a -> ScopeT (Name a b) t f a
abstractTName :: (a -> Maybe b) -> t f a -> ScopeT (Name a b) t f a
abstractTName a -> Maybe b
f t f a
t = t f (Var (Name a b) (f a)) -> ScopeT (Name a b) t f a
forall b (t :: (* -> *) -> * -> *) (f :: * -> *) a.
t f (Var b (f a)) -> ScopeT b t f a
ScopeT ((a -> Var (Name a b) (f a)) -> t f a -> t f (Var (Name a b) (f a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Var (Name a b) (f a)
forall (m :: * -> *). Monad m => a -> Var (Name a b) (m a)
k t f a
t) where
k :: a -> Var (Name a b) (m a)
k a
a = case a -> Maybe b
f a
a of
Just b
b -> Name a b -> Var (Name a b) (m a)
forall b a. b -> Var b a
B (a -> b -> Name a b
forall n b. n -> b -> Name n b
Name a
a b
b)
Maybe b
Nothing -> m a -> Var (Name a b) (m a)
forall b a. a -> Var b a
F (a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a)
{-# INLINE abstractTName #-}
abstract1TName :: (Functor (t f), Monad f, Eq a) => a -> t f a -> ScopeT (Name a ()) t f a
abstract1TName :: a -> t f a -> ScopeT (Name a ()) t f a
abstract1TName a
a = (a -> Maybe ()) -> t f a -> ScopeT (Name a ()) t f a
forall (t :: (* -> *) -> * -> *) (f :: * -> *) a b.
(Functor (t f), Monad f) =>
(a -> Maybe b) -> t f a -> ScopeT (Name a b) t f a
abstractTName (\a
b -> if a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b then () -> Maybe ()
forall a. a -> Maybe a
Just () else Maybe ()
forall a. Maybe a
Nothing)
{-# INLINE abstract1TName #-}
instantiateT :: (Bound t, Monad f) => (b -> f a) -> ScopeT b t f a -> t f a
instantiateT :: (b -> f a) -> ScopeT b t f a -> t f a
instantiateT b -> f a
k (ScopeT t f (Var b (f a))
e) = t f (Var b (f a))
e t f (Var b (f a)) -> (Var b (f a) -> f a) -> t f a
forall (t :: (* -> *) -> * -> *) (f :: * -> *) a c.
(Bound t, Monad f) =>
t f a -> (a -> f c) -> t f c
>>>= \Var b (f a)
v -> case Var b (f a)
v of
B b
b -> b -> f a
k b
b
F f a
a -> f a
a
{-# INLINE instantiateT #-}
instantiate1T :: (Bound t, Monad f) => f a -> ScopeT b t f a -> t f a
instantiate1T :: f a -> ScopeT b t f a -> t f a
instantiate1T f a
e = (b -> f a) -> ScopeT b t f a -> t f a
forall (t :: (* -> *) -> * -> *) (f :: * -> *) b a.
(Bound t, Monad f) =>
(b -> f a) -> ScopeT b t f a -> t f a
instantiateT (f a -> b -> f a
forall a b. a -> b -> a
const f a
e)
{-# INLINE instantiate1T #-}
instantiateTEither :: (Bound t, Monad f) => (Either b a -> f c) -> ScopeT b t f a -> t f c
instantiateTEither :: (Either b a -> f c) -> ScopeT b t f a -> t f c
instantiateTEither Either b a -> f c
f (ScopeT t f (Var b (f a))
e) = t f (Var b (f a))
e t f (Var b (f a)) -> (Var b (f a) -> f c) -> t f c
forall (t :: (* -> *) -> * -> *) (f :: * -> *) a c.
(Bound t, Monad f) =>
t f a -> (a -> f c) -> t f c
>>>= \Var b (f a)
v -> case Var b (f a)
v of
B b
b -> Either b a -> f c
f (b -> Either b a
forall a b. a -> Either a b
Left b
b)
F f a
ea -> f a
ea f a -> (a -> f c) -> f c
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Either b a -> f c
f (Either b a -> f c) -> (a -> Either b a) -> a -> f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either b a
forall a b. b -> Either a b
Right
{-# INLINE instantiateTEither #-}
liftScopeT:: forall t f a b. (Monad (t f)) => f a -> ScopeT b t f a
liftScopeT :: f a -> ScopeT b t f a
liftScopeT = t f (Var b (f a)) -> ScopeT b t f a
forall b (t :: (* -> *) -> * -> *) (f :: * -> *) a.
t f (Var b (f a)) -> ScopeT b t f a
ScopeT (t f (Var b (f a)) -> ScopeT b t f a)
-> (f a -> t f (Var b (f a))) -> f a -> ScopeT b t f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var b (f a) -> t f (Var b (f a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Var b (f a) -> t f (Var b (f a)))
-> (f a -> Var b (f a)) -> f a -> t f (Var b (f a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> Var b (f a)
forall b a. a -> Var b a
F
{-# INLINE liftScopeT #-}
fromScopeT :: (Bound t, Monad f) => ScopeT b t f a -> t f (Var b a)
fromScopeT :: ScopeT b t f a -> t f (Var b a)
fromScopeT (ScopeT t f (Var b (f a))
s) = t f (Var b (f a))
s t f (Var b (f a)) -> (Var b (f a) -> f (Var b a)) -> t f (Var b a)
forall (t :: (* -> *) -> * -> *) (f :: * -> *) a c.
(Bound t, Monad f) =>
t f a -> (a -> f c) -> t f c
>>>= \Var b (f a)
v -> case Var b (f a)
v of
F f a
e -> (a -> Var b a) -> f a -> f (Var b a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Var b a
forall b a. a -> Var b a
F f a
e
B b
b -> Var b a -> f (Var b a)
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> Var b a
forall b a. b -> Var b a
B b
b)
toScopeT :: (Functor (t f), Monad f) => t f (Var b a) -> ScopeT b t f a
toScopeT :: t f (Var b a) -> ScopeT b t f a
toScopeT t f (Var b a)
e = t f (Var b (f a)) -> ScopeT b t f a
forall b (t :: (* -> *) -> * -> *) (f :: * -> *) a.
t f (Var b (f a)) -> ScopeT b t f a
ScopeT ((Var b a -> Var b (f a)) -> t f (Var b a) -> t f (Var b (f a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> f a) -> Var b a -> Var b (f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> f a
forall (m :: * -> *) a. Monad m => a -> m a
return) t f (Var b a)
e)
lowerScopeT
:: (Functor (t f), Functor f)
=> (forall x. t f x -> g x)
-> (forall x. f x -> g x)
-> ScopeT b t f a -> Scope b g a
lowerScopeT :: (forall x. t f x -> g x)
-> (forall x. f x -> g x) -> ScopeT b t f a -> Scope b g a
lowerScopeT forall x. t f x -> g x
tf forall x. f x -> g x
f (ScopeT t f (Var b (f a))
x) = g (Var b (g a)) -> Scope b g a
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope (t f (Var b (g a)) -> g (Var b (g a))
forall x. t f x -> g x
tf ((Var b (f a) -> Var b (g a))
-> t f (Var b (f a)) -> t f (Var b (g a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f a -> g a) -> Var b (f a) -> Var b (g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f a -> g a
forall x. f x -> g x
f) t f (Var b (f a))
x))
splatT :: (Bound t, Monad f) => (a -> f c) -> (b -> f c) -> ScopeT b t f a -> t f c
splatT :: (a -> f c) -> (b -> f c) -> ScopeT b t f a -> t f c
splatT a -> f c
f b -> f c
unbind (ScopeT t f (Var b (f a))
e) = t f (Var b (f a))
e t f (Var b (f a)) -> (Var b (f a) -> f c) -> t f c
forall (t :: (* -> *) -> * -> *) (f :: * -> *) a c.
(Bound t, Monad f) =>
t f a -> (a -> f c) -> t f c
>>>= \Var b (f a)
v -> case Var b (f a)
v of
B b
b -> b -> f c
unbind b
b
F f a
ea -> f a
ea f a -> (a -> f c) -> f c
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> f c
f
{-# INLINE splatT #-}
bindingsT :: Foldable (t f) => ScopeT b t f a -> [b]
bindingsT :: ScopeT b t f a -> [b]
bindingsT (ScopeT t f (Var b (f a))
s) = (Var b (f a) -> [b] -> [b]) -> [b] -> t f (Var b (f a)) -> [b]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Var b (f a) -> [b] -> [b]
forall a a. Var a a -> [a] -> [a]
f [] t f (Var b (f a))
s where
f :: Var a a -> [a] -> [a]
f (B a
v) [a]
vs = a
v a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
vs
f Var a a
_ [a]
vs = [a]
vs
{-# INLINE bindingsT #-}
mapBoundT :: Functor (t f) => (b -> b') -> ScopeT b t f a -> ScopeT b' t f a
mapBoundT :: (b -> b') -> ScopeT b t f a -> ScopeT b' t f a
mapBoundT b -> b'
f (ScopeT t f (Var b (f a))
s) = t f (Var b' (f a)) -> ScopeT b' t f a
forall b (t :: (* -> *) -> * -> *) (f :: * -> *) a.
t f (Var b (f a)) -> ScopeT b t f a
ScopeT ((Var b (f a) -> Var b' (f a))
-> t f (Var b (f a)) -> t f (Var b' (f a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Var b (f a) -> Var b' (f a)
forall a. Var b a -> Var b' a
f' t f (Var b (f a))
s) where
f' :: Var b a -> Var b' a
f' (B b
b) = b' -> Var b' a
forall b a. b -> Var b a
B (b -> b'
f b
b)
f' (F a
a) = a -> Var b' a
forall b a. a -> Var b a
F a
a
{-# INLINE mapBoundT #-}
mapScopeT
:: (Functor (t f), Functor f)
=> (b -> d) -> (a -> c)
-> ScopeT b t f a -> ScopeT d t f c
mapScopeT :: (b -> d) -> (a -> c) -> ScopeT b t f a -> ScopeT d t f c
mapScopeT b -> d
f a -> c
g (ScopeT t f (Var b (f a))
s) = t f (Var d (f c)) -> ScopeT d t f c
forall b (t :: (* -> *) -> * -> *) (f :: * -> *) a.
t f (Var b (f a)) -> ScopeT b t f a
ScopeT (t f (Var d (f c)) -> ScopeT d t f c)
-> t f (Var d (f c)) -> ScopeT d t f c
forall a b. (a -> b) -> a -> b
$ (Var b (f a) -> Var d (f c))
-> t f (Var b (f a)) -> t f (Var d (f c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> d) -> (f a -> f c) -> Var b (f a) -> Var d (f c)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap b -> d
f ((a -> c) -> f a -> f c
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> c
g)) t f (Var b (f a))
s
{-# INLINE mapScopeT #-}
foldMapBoundT :: (Foldable (t f), Monoid r) => (b -> r) -> ScopeT b t f a -> r
foldMapBoundT :: (b -> r) -> ScopeT b t f a -> r
foldMapBoundT b -> r
f (ScopeT t f (Var b (f a))
s) = (Var b (f a) -> r) -> t f (Var b (f a)) -> r
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Var b (f a) -> r
forall a. Var b a -> r
f' t f (Var b (f a))
s where
f' :: Var b a -> r
f' (B b
a) = b -> r
f b
a
f' Var b a
_ = r
forall a. Monoid a => a
mempty
{-# INLINE foldMapBoundT #-}
foldMapScopeT
:: (Foldable f, Foldable (t f), Monoid r)
=> (b -> r) -> (a -> r)
-> ScopeT b t f a -> r
foldMapScopeT :: (b -> r) -> (a -> r) -> ScopeT b t f a -> r
foldMapScopeT b -> r
f a -> r
g (ScopeT t f (Var b (f a))
s) = (Var b (f a) -> r) -> t f (Var b (f a)) -> r
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((b -> r) -> (f a -> r) -> Var b (f a) -> r
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap b -> r
f ((a -> r) -> f a -> r
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> r
g)) t f (Var b (f a))
s
{-# INLINE foldMapScopeT #-}
traverseBoundT_ :: (Applicative g, Foldable (t f)) => (b -> g d) -> ScopeT b t f a -> g ()
traverseBoundT_ :: (b -> g d) -> ScopeT b t f a -> g ()
traverseBoundT_ b -> g d
f (ScopeT t f (Var b (f a))
s) = (Var b (f a) -> g ()) -> t f (Var b (f a)) -> g ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ Var b (f a) -> g ()
forall a. Var b a -> g ()
f' t f (Var b (f a))
s where
f' :: Var b a -> g ()
f' (B b
a) = () () -> g d -> g ()
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ b -> g d
f b
a
f' Var b a
_ = () -> g ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
{-# INLINE traverseBoundT_ #-}
traverseScopeT_
:: (Applicative g, Foldable f, Foldable (t f))
=> (b -> g d) -> (a -> g c)
-> ScopeT b t f a -> g ()
traverseScopeT_ :: (b -> g d) -> (a -> g c) -> ScopeT b t f a -> g ()
traverseScopeT_ b -> g d
f a -> g c
g (ScopeT t f (Var b (f a))
s) = (Var b (f a) -> g ()) -> t f (Var b (f a)) -> g ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ ((b -> g d) -> (f a -> g ()) -> Var b (f a) -> g ()
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bifoldable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f ()
bitraverse_ b -> g d
f ((a -> g c) -> f a -> g ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ a -> g c
g)) t f (Var b (f a))
s
{-# INLINE traverseScopeT_ #-}
traverseBoundT
:: (Applicative g, Traversable (t f))
=> (b -> g c) -> ScopeT b t f a -> g (ScopeT c t f a)
traverseBoundT :: (b -> g c) -> ScopeT b t f a -> g (ScopeT c t f a)
traverseBoundT b -> g c
f (ScopeT t f (Var b (f a))
s) = t f (Var c (f a)) -> ScopeT c t f a
forall b (t :: (* -> *) -> * -> *) (f :: * -> *) a.
t f (Var b (f a)) -> ScopeT b t f a
ScopeT (t f (Var c (f a)) -> ScopeT c t f a)
-> g (t f (Var c (f a))) -> g (ScopeT c t f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var b (f a) -> g (Var c (f a)))
-> t f (Var b (f a)) -> g (t f (Var c (f a)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Var b (f a) -> g (Var c (f a))
forall a. Var b a -> g (Var c a)
f' t f (Var b (f a))
s where
f' :: Var b a -> g (Var c a)
f' (B b
b) = c -> Var c a
forall b a. b -> Var b a
B (c -> Var c a) -> g c -> g (Var c a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> g c
f b
b
f' (F a
a) = Var c a -> g (Var c a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> Var c a
forall b a. a -> Var b a
F a
a)
{-# INLINE traverseBoundT #-}
traverseScopeT
:: (Applicative g, Traversable f, Traversable (t f))
=> (b -> g d) -> (a -> g c)
-> ScopeT b t f a -> g (ScopeT d t f c)
traverseScopeT :: (b -> g d) -> (a -> g c) -> ScopeT b t f a -> g (ScopeT d t f c)
traverseScopeT b -> g d
f a -> g c
g (ScopeT t f (Var b (f a))
s) = t f (Var d (f c)) -> ScopeT d t f c
forall b (t :: (* -> *) -> * -> *) (f :: * -> *) a.
t f (Var b (f a)) -> ScopeT b t f a
ScopeT (t f (Var d (f c)) -> ScopeT d t f c)
-> g (t f (Var d (f c))) -> g (ScopeT d t f c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var b (f a) -> g (Var d (f c)))
-> t f (Var b (f a)) -> g (t f (Var d (f c)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((b -> g d) -> (f a -> g (f c)) -> Var b (f a) -> g (Var d (f c))
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse b -> g d
f ((a -> g c) -> f a -> g (f c)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> g c
g)) t f (Var b (f a))
s
{-# INLINE traverseScopeT #-}
bitransverseScopeT
:: Applicative f
=> (forall x x'. (x -> f x') -> t s x -> f (t' s' x'))
-> (forall x x'. (x -> f x') -> s x -> f (s' x'))
-> (a -> f a')
-> ScopeT b t s a
-> f (ScopeT b t' s' a')
bitransverseScopeT :: (forall x x'. (x -> f x') -> t s x -> f (t' s' x'))
-> (forall x x'. (x -> f x') -> s x -> f (s' x'))
-> (a -> f a')
-> ScopeT b t s a
-> f (ScopeT b t' s' a')
bitransverseScopeT forall x x'. (x -> f x') -> t s x -> f (t' s' x')
tauT forall x x'. (x -> f x') -> s x -> f (s' x')
tauS a -> f a'
f = (t' s' (Var b (s' a')) -> ScopeT b t' s' a')
-> f (t' s' (Var b (s' a'))) -> f (ScopeT b t' s' a')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap t' s' (Var b (s' a')) -> ScopeT b t' s' a'
forall b (t :: (* -> *) -> * -> *) (f :: * -> *) a.
t f (Var b (f a)) -> ScopeT b t f a
ScopeT (f (t' s' (Var b (s' a'))) -> f (ScopeT b t' s' a'))
-> (ScopeT b t s a -> f (t' s' (Var b (s' a'))))
-> ScopeT b t s a
-> f (ScopeT b t' s' a')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var b (s a) -> f (Var b (s' a')))
-> t s (Var b (s a)) -> f (t' s' (Var b (s' a')))
forall x x'. (x -> f x') -> t s x -> f (t' s' x')
tauT ((s a -> f (s' a')) -> Var b (s a) -> f (Var b (s' a'))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((a -> f a') -> s a -> f (s' a')
forall x x'. (x -> f x') -> s x -> f (s' x')
tauS a -> f a'
f)) (t s (Var b (s a)) -> f (t' s' (Var b (s' a'))))
-> (ScopeT b t s a -> t s (Var b (s a)))
-> ScopeT b t s a
-> f (t' s' (Var b (s' a')))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeT b t s a -> t s (Var b (s a))
forall b (t :: (* -> *) -> * -> *) (f :: * -> *) a.
ScopeT b t f a -> t f (Var b (f a))
unscopeT
{-# INLINE bitransverseScopeT #-}