{-# LANGUAGE UndecidableInstances #-}
module Blanks.Scope
( Scope (..)
, pattern ScopeBound
, pattern ScopeFree
, pattern ScopeBinder
, pattern ScopeEmbed
, scopeWFromInnerBinder
, scopeBind
, scopeBindOpt
, scopeLift
, scopeInnerBinder
, scopeInnerBinder1
, scopeAbstract
, scopeAbstract1
, scopeUnAbstract
, scopeUnAbstract1
, scopeInstantiate
, scopeInstantiate1
, scopeApply
, scopeApply1
) where
import Blanks.Core (BinderScope)
import Blanks.NatNewtype (NatNewtype)
import Blanks.ScopeW (ScopeW (ScopeW), scopeWAbstract, scopeWAbstract1, scopeWApply, scopeWApply1, scopeWBind,
scopeWBindOpt, scopeWFromInnerBinder, scopeWInnerBinder, scopeWInnerBinder1, scopeWInstantiate,
scopeWInstantiate1, scopeWLift, scopeWUnAbstract, scopeWUnAbstract1)
import Blanks.Sub (SubError)
import Blanks.Under (pattern UnderScopeBinder, pattern UnderScopeBound, pattern UnderScopeEmbed, pattern UnderScopeFree)
import Control.DeepSeq (NFData (..))
import Control.Monad (ap)
import Control.Monad.Identity (Identity (..))
import Data.Sequence (Seq)
newtype Scope n f a = Scope
{ Scope n f a -> ScopeW Identity n f (Scope n f) a
unScope :: ScopeW Identity n f (Scope n f) a
} deriving stock (a -> Scope n f b -> Scope n f a
(a -> b) -> Scope n f a -> Scope n f b
(forall a b. (a -> b) -> Scope n f a -> Scope n f b)
-> (forall a b. a -> Scope n f b -> Scope n f a)
-> Functor (Scope n f)
forall a b. a -> Scope n f b -> Scope n f a
forall a b. (a -> b) -> Scope n f a -> Scope n f b
forall n (f :: * -> *) a b.
Functor f =>
a -> Scope n f b -> Scope n f a
forall n (f :: * -> *) a b.
Functor f =>
(a -> b) -> Scope n f a -> Scope n f b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Scope n f b -> Scope n f a
$c<$ :: forall n (f :: * -> *) a b.
Functor f =>
a -> Scope n f b -> Scope n f a
fmap :: (a -> b) -> Scope n f a -> Scope n f b
$cfmap :: forall n (f :: * -> *) a b.
Functor f =>
(a -> b) -> Scope n f a -> Scope n f b
Functor, Scope n f a -> Bool
(a -> m) -> Scope n f a -> m
(a -> b -> b) -> b -> Scope n f a -> b
(forall m. Monoid m => Scope n f m -> m)
-> (forall m a. Monoid m => (a -> m) -> Scope n f a -> m)
-> (forall m a. Monoid m => (a -> m) -> Scope n f a -> m)
-> (forall a b. (a -> b -> b) -> b -> Scope n f a -> b)
-> (forall a b. (a -> b -> b) -> b -> Scope n f a -> b)
-> (forall b a. (b -> a -> b) -> b -> Scope n f a -> b)
-> (forall b a. (b -> a -> b) -> b -> Scope n f a -> b)
-> (forall a. (a -> a -> a) -> Scope n f a -> a)
-> (forall a. (a -> a -> a) -> Scope n f a -> a)
-> (forall a. Scope n f a -> [a])
-> (forall a. Scope n f a -> Bool)
-> (forall a. Scope n f a -> Int)
-> (forall a. Eq a => a -> Scope n f a -> Bool)
-> (forall a. Ord a => Scope n f a -> a)
-> (forall a. Ord a => Scope n f a -> a)
-> (forall a. Num a => Scope n f a -> a)
-> (forall a. Num a => Scope n f a -> a)
-> Foldable (Scope n f)
forall a. Eq a => a -> Scope n f a -> Bool
forall a. Num a => Scope n f a -> a
forall a. Ord a => Scope n f a -> a
forall m. Monoid m => Scope n f m -> m
forall a. Scope n f a -> Bool
forall a. Scope n f a -> Int
forall a. Scope n f a -> [a]
forall a. (a -> a -> a) -> Scope n f a -> a
forall m a. Monoid m => (a -> m) -> Scope n f a -> m
forall b a. (b -> a -> b) -> b -> Scope n f a -> b
forall a b. (a -> b -> b) -> b -> Scope n f a -> b
forall n (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> Scope n f a -> Bool
forall n (f :: * -> *) a. (Foldable f, Num a) => Scope n f a -> a
forall n (f :: * -> *) a. (Foldable f, Ord a) => Scope n f a -> a
forall n (f :: * -> *) m.
(Foldable f, Monoid m) =>
Scope n f m -> m
forall n (f :: * -> *) a. Foldable f => Scope n f a -> Bool
forall n (f :: * -> *) a. Foldable f => Scope n f a -> Int
forall n (f :: * -> *) a. Foldable f => Scope n f a -> [a]
forall n (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Scope n f a -> a
forall n (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Scope n f a -> m
forall n (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Scope n f a -> b
forall n (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Scope n f a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Scope n f a -> a
$cproduct :: forall n (f :: * -> *) a. (Foldable f, Num a) => Scope n f a -> a
sum :: Scope n f a -> a
$csum :: forall n (f :: * -> *) a. (Foldable f, Num a) => Scope n f a -> a
minimum :: Scope n f a -> a
$cminimum :: forall n (f :: * -> *) a. (Foldable f, Ord a) => Scope n f a -> a
maximum :: Scope n f a -> a
$cmaximum :: forall n (f :: * -> *) a. (Foldable f, Ord a) => Scope n f a -> a
elem :: a -> Scope n f a -> Bool
$celem :: forall n (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> Scope n f a -> Bool
length :: Scope n f a -> Int
$clength :: forall n (f :: * -> *) a. Foldable f => Scope n f a -> Int
null :: Scope n f a -> Bool
$cnull :: forall n (f :: * -> *) a. Foldable f => Scope n f a -> Bool
toList :: Scope n f a -> [a]
$ctoList :: forall n (f :: * -> *) a. Foldable f => Scope n f a -> [a]
foldl1 :: (a -> a -> a) -> Scope n f a -> a
$cfoldl1 :: forall n (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Scope n f a -> a
foldr1 :: (a -> a -> a) -> Scope n f a -> a
$cfoldr1 :: forall n (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Scope n f a -> a
foldl' :: (b -> a -> b) -> b -> Scope n f a -> b
$cfoldl' :: forall n (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Scope n f a -> b
foldl :: (b -> a -> b) -> b -> Scope n f a -> b
$cfoldl :: forall n (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Scope n f a -> b
foldr' :: (a -> b -> b) -> b -> Scope n f a -> b
$cfoldr' :: forall n (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Scope n f a -> b
foldr :: (a -> b -> b) -> b -> Scope n f a -> b
$cfoldr :: forall n (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Scope n f a -> b
foldMap' :: (a -> m) -> Scope n f a -> m
$cfoldMap' :: forall n (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Scope n f a -> m
foldMap :: (a -> m) -> Scope n f a -> m
$cfoldMap :: forall n (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Scope n f a -> m
fold :: Scope n f m -> m
$cfold :: forall n (f :: * -> *) m.
(Foldable f, Monoid m) =>
Scope n f m -> m
Foldable, Functor (Scope n f)
Foldable (Scope n f)
(Functor (Scope n f), Foldable (Scope n f)) =>
(forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Scope n f a -> f (Scope n f b))
-> (forall (f :: * -> *) a.
Applicative f =>
Scope n f (f a) -> f (Scope n f a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Scope n f a -> m (Scope n f b))
-> (forall (m :: * -> *) a.
Monad m =>
Scope n f (m a) -> m (Scope n f a))
-> Traversable (Scope n f)
(a -> f b) -> Scope n f a -> f (Scope n f b)
forall n (f :: * -> *). Traversable f => Functor (Scope n f)
forall n (f :: * -> *). Traversable f => Foldable (Scope n f)
forall n (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
Scope n f (m a) -> m (Scope n f a)
forall n (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
Scope n f (f a) -> f (Scope n f a)
forall n (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> Scope n f a -> m (Scope n f b)
forall n (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> Scope n f a -> f (Scope n f b)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
Scope n f (m a) -> m (Scope n f a)
forall (f :: * -> *) a.
Applicative f =>
Scope n f (f a) -> f (Scope n f a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Scope n f a -> m (Scope n f b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Scope n f a -> f (Scope n f b)
sequence :: Scope n f (m a) -> m (Scope n f a)
$csequence :: forall n (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
Scope n f (m a) -> m (Scope n f a)
mapM :: (a -> m b) -> Scope n f a -> m (Scope n f b)
$cmapM :: forall n (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> Scope n f a -> m (Scope n f b)
sequenceA :: Scope n f (f a) -> f (Scope n f a)
$csequenceA :: forall n (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
Scope n f (f a) -> f (Scope n f a)
traverse :: (a -> f b) -> Scope n f a -> f (Scope n f b)
$ctraverse :: forall n (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> Scope n f a -> f (Scope n f b)
$cp2Traversable :: forall n (f :: * -> *). Traversable f => Foldable (Scope n f)
$cp1Traversable :: forall n (f :: * -> *). Traversable f => Functor (Scope n f)
Traversable)
instance NatNewtype (ScopeW Identity n f (Scope n f)) (Scope n f)
instance (NFData n, NFData a, NFData (f (Scope n f a))) => NFData (Scope n f a) where
rnf :: Scope n f a -> ()
rnf (Scope s :: ScopeW Identity n f (Scope n f) a
s) = () -> () -> ()
forall a b. a -> b -> b
seq (ScopeW Identity n f (Scope n f) a -> ()
forall a. NFData a => a -> ()
rnf ScopeW Identity n f (Scope n f) a
s) ()
pattern ScopeBound :: Int -> Scope n f a
pattern $bScopeBound :: Int -> Scope n f a
$mScopeBound :: forall r n (f :: * -> *) a.
Scope n f a -> (Int -> r) -> (Void# -> r) -> r
ScopeBound b = Scope (ScopeW (Identity (UnderScopeBound b)))
pattern ScopeFree :: a -> Scope n f a
pattern $bScopeFree :: a -> Scope n f a
$mScopeFree :: forall r a n (f :: * -> *).
Scope n f a -> (a -> r) -> (Void# -> r) -> r
ScopeFree a = Scope (ScopeW (Identity (UnderScopeFree a)))
pattern ScopeBinder :: Int -> n -> Scope n f a -> Scope n f a
pattern $bScopeBinder :: Int -> n -> Scope n f a -> Scope n f a
$mScopeBinder :: forall r n (f :: * -> *) a.
Scope n f a -> (Int -> n -> Scope n f a -> r) -> (Void# -> r) -> r
ScopeBinder i n e = Scope (ScopeW (Identity (UnderScopeBinder i n e)))
pattern ScopeEmbed :: f (Scope n f a) -> Scope n f a
pattern $bScopeEmbed :: f (Scope n f a) -> Scope n f a
$mScopeEmbed :: forall r (f :: * -> *) n a.
Scope n f a -> (f (Scope n f a) -> r) -> (Void# -> r) -> r
ScopeEmbed fe = Scope (ScopeW (Identity (UnderScopeEmbed fe)))
{-# COMPLETE ScopeBound, ScopeFree, ScopeBinder, ScopeEmbed #-}
instance Functor f => Applicative (Scope n f) where
pure :: a -> Scope n f a
pure = a -> Scope n f a
forall a n (f :: * -> *). a -> Scope n f a
ScopeFree
<*> :: Scope n f (a -> b) -> Scope n f a -> Scope n f b
(<*>) = Scope n f (a -> b) -> Scope n f a -> Scope n f b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Functor f => Monad (Scope n f) where
return :: a -> Scope n f a
return = a -> Scope n f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
s :: Scope n f a
s >>= :: Scope n f a -> (a -> Scope n f b) -> Scope n f b
>>= f :: a -> Scope n f b
f = (a -> Scope n f b) -> Scope n f a -> Scope n f b
forall (f :: * -> *) a n b.
Functor f =>
(a -> Scope n f b) -> Scope n f a -> Scope n f b
scopeBind a -> Scope n f b
f Scope n f a
s
instance (Eq (f (Scope n f a)), Eq n, Eq a) => Eq (Scope n f a) where
Scope su :: ScopeW Identity n f (Scope n f) a
su == :: Scope n f a -> Scope n f a -> Bool
== Scope sv :: ScopeW Identity n f (Scope n f) a
sv = ScopeW Identity n f (Scope n f) a
su ScopeW Identity n f (Scope n f) a
-> ScopeW Identity n f (Scope n f) a -> Bool
forall a. Eq a => a -> a -> Bool
== ScopeW Identity n f (Scope n f) a
sv
instance (Show (f (Scope n f a)), Show n, Show a) => Show (Scope n f a) where
showsPrec :: Int -> Scope n f a -> ShowS
showsPrec d :: Int
d (Scope (ScopeW tu :: Identity (UnderScope n f (Scope n f a) a)
tu)) = String -> ShowS
showString "Scope " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Identity (UnderScope n f (Scope n f a) a) -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+1) Identity (UnderScope n f (Scope n f a) a)
tu
scopeFromInnerBinder :: Functor f => BinderScope n (Scope n f a) -> Scope n f a
scopeFromInnerBinder :: BinderScope n (Scope n f a) -> Scope n f a
scopeFromInnerBinder = Identity (Scope n f a) -> Scope n f a
forall a. Identity a -> a
runIdentity (Identity (Scope n f a) -> Scope n f a)
-> (BinderScope n (Scope n f a) -> Identity (Scope n f a))
-> BinderScope n (Scope n f a)
-> Scope n f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BinderScope n (Scope n f a) -> Identity (Scope n f a)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
BinderScope n (g a) -> u (g a)
scopeWFromInnerBinder
{-# INLINE scopeFromInnerBinder #-}
scopeBind :: Functor f => (a -> Scope n f b) -> Scope n f a -> Scope n f b
scopeBind :: (a -> Scope n f b) -> Scope n f a -> Scope n f b
scopeBind f :: a -> Scope n f b
f = (a -> Identity (Scope n f b)) -> Scope n f a -> Scope n f b
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a
b.
ScopeWC t u n f g =>
(a -> u (g b)) -> g a -> g b
scopeWBind (Scope n f b -> Identity (Scope n f b)
forall a. a -> Identity a
Identity (Scope n f b -> Identity (Scope n f b))
-> (a -> Scope n f b) -> a -> Identity (Scope n f b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Scope n f b
f)
{-# INLINE scopeBind #-}
scopeBindOpt :: Functor f => (a -> Maybe (Scope n f a)) -> Scope n f a -> Scope n f a
scopeBindOpt :: (a -> Maybe (Scope n f a)) -> Scope n f a -> Scope n f a
scopeBindOpt f :: a -> Maybe (Scope n f a)
f = (a -> Maybe (Identity (Scope n f a))) -> Scope n f a -> Scope n f a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
(a -> Maybe (u (g a))) -> g a -> g a
scopeWBindOpt ((Scope n f a -> Identity (Scope n f a))
-> Maybe (Scope n f a) -> Maybe (Identity (Scope n f a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Scope n f a -> Identity (Scope n f a)
forall a. a -> Identity a
Identity (Maybe (Scope n f a) -> Maybe (Identity (Scope n f a)))
-> (a -> Maybe (Scope n f a))
-> a
-> Maybe (Identity (Scope n f a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe (Scope n f a)
f)
{-# INLINE scopeBindOpt #-}
scopeLift :: Traversable f => f a -> Scope n f a
scopeLift :: f a -> Scope n f a
scopeLift = Identity (Scope n f a) -> Scope n f a
forall a. Identity a -> a
runIdentity (Identity (Scope n f a) -> Scope n f a)
-> (f a -> Identity (Scope n f a)) -> f a -> Scope n f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> Identity (Scope n f a)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
(ScopeWC t u n f g, Monad u, Traversable f) =>
f a -> u (g a)
scopeWLift
{-# INLINE scopeLift #-}
scopeInnerBinder :: (Functor f, Eq a) => n -> Seq a -> Scope n f a -> BinderScope n (Scope n f a)
scopeInnerBinder :: n -> Seq a -> Scope n f a -> BinderScope n (Scope n f a)
scopeInnerBinder = n -> Seq a -> Scope n f a -> BinderScope n (Scope n f a)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
(ScopeWC t u n f g, Eq a) =>
n -> Seq a -> g a -> BinderScope n (g a)
scopeWInnerBinder
{-# INLINE scopeInnerBinder #-}
scopeInnerBinder1 :: (Functor f, Eq a) => n -> a -> Scope n f a -> BinderScope n (Scope n f a)
scopeInnerBinder1 :: n -> a -> Scope n f a -> BinderScope n (Scope n f a)
scopeInnerBinder1 = n -> a -> Scope n f a -> BinderScope n (Scope n f a)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
(ScopeWC t u n f g, Eq a) =>
n -> a -> g a -> BinderScope n (g a)
scopeWInnerBinder1
{-# INLINE scopeInnerBinder1 #-}
scopeAbstract
:: (Functor f, Eq a)
=> n
-> Seq a
-> Scope n f a
-> Scope n f a
scopeAbstract :: n -> Seq a -> Scope n f a -> Scope n f a
scopeAbstract n :: n
n ks :: Seq a
ks = Identity (Scope n f a) -> Scope n f a
forall a. Identity a -> a
runIdentity (Identity (Scope n f a) -> Scope n f a)
-> (Scope n f a -> Identity (Scope n f a))
-> Scope n f a
-> Scope n f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. n -> Seq a -> Scope n f a -> Identity (Scope n f a)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
(ScopeWC t u n f g, Eq a) =>
n -> Seq a -> g a -> u (g a)
scopeWAbstract n
n Seq a
ks
{-# INLINE scopeAbstract #-}
scopeAbstract1 :: (Functor f, Eq a) => n -> a -> Scope n f a -> Scope n f a
scopeAbstract1 :: n -> a -> Scope n f a -> Scope n f a
scopeAbstract1 n :: n
n k :: a
k = Identity (Scope n f a) -> Scope n f a
forall a. Identity a -> a
runIdentity (Identity (Scope n f a) -> Scope n f a)
-> (Scope n f a -> Identity (Scope n f a))
-> Scope n f a
-> Scope n f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. n -> a -> Scope n f a -> Identity (Scope n f a)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
(ScopeWC t u n f g, Eq a) =>
n -> a -> g a -> u (g a)
scopeWAbstract1 n
n a
k
{-# INLINE scopeAbstract1 #-}
scopeUnAbstract
:: Functor f
=> Seq a
-> Scope n f a
-> Scope n f a
scopeUnAbstract :: Seq a -> Scope n f a -> Scope n f a
scopeUnAbstract = Seq a -> Scope n f a -> Scope n f a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Seq a -> g a -> g a
scopeWUnAbstract
{-# INLINE scopeUnAbstract #-}
scopeUnAbstract1 :: Functor f => a -> Scope n f a -> Scope n f a
scopeUnAbstract1 :: a -> Scope n f a -> Scope n f a
scopeUnAbstract1 = a -> Scope n f a -> Scope n f a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
a -> g a -> g a
scopeWUnAbstract1
{-# INLINE scopeUnAbstract1 #-}
scopeInstantiate
:: Functor f
=> Seq (Scope n f a)
-> Scope n f a
-> Scope n f a
scopeInstantiate :: Seq (Scope n f a) -> Scope n f a -> Scope n f a
scopeInstantiate vs :: Seq (Scope n f a)
vs = Seq (Identity (Scope n f a)) -> Scope n f a -> Scope n f a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Seq (u (g a)) -> g a -> g a
scopeWInstantiate ((Scope n f a -> Identity (Scope n f a))
-> Seq (Scope n f a) -> Seq (Identity (Scope n f a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Scope n f a -> Identity (Scope n f a)
forall a. a -> Identity a
Identity Seq (Scope n f a)
vs)
{-# INLINE scopeInstantiate #-}
scopeInstantiate1 :: Functor f => Scope n f a -> Scope n f a -> Scope n f a
scopeInstantiate1 :: Scope n f a -> Scope n f a -> Scope n f a
scopeInstantiate1 v :: Scope n f a
v = Identity (Scope n f a) -> Scope n f a -> Scope n f a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
u (g a) -> g a -> g a
scopeWInstantiate1 (Scope n f a -> Identity (Scope n f a)
forall a. a -> Identity a
Identity Scope n f a
v)
{-# INLINE scopeInstantiate1 #-}
scopeApply
:: Functor f
=> Seq (Scope n f a)
-> Scope n f a
-> Either SubError (Scope n f a)
scopeApply :: Seq (Scope n f a) -> Scope n f a -> Either SubError (Scope n f a)
scopeApply vs :: Seq (Scope n f a)
vs = Seq (Identity (Scope n f a))
-> Scope n f a -> Either SubError (Scope n f a)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Seq (u (g a)) -> g a -> Either SubError (g a)
scopeWApply ((Scope n f a -> Identity (Scope n f a))
-> Seq (Scope n f a) -> Seq (Identity (Scope n f a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Scope n f a -> Identity (Scope n f a)
forall a. a -> Identity a
Identity Seq (Scope n f a)
vs)
{-# INLINE scopeApply #-}
scopeApply1 :: Functor f => Scope n f a -> Scope n f a -> Either SubError (Scope n f a)
scopeApply1 :: Scope n f a -> Scope n f a -> Either SubError (Scope n f a)
scopeApply1 v :: Scope n f a
v = Identity (Scope n f a)
-> Scope n f a -> Either SubError (Scope n f a)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
u (g a) -> g a -> Either SubError (g a)
scopeWApply1 (Scope n f a -> Identity (Scope n f a)
forall a. a -> Identity a
Identity Scope n f a
v)
{-# INLINE scopeApply1 #-}