{-# 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)

-- | A simple wrapper for your expression functor that knows how to name-bind.
-- Create free variables is 'pure', bind them with '>>=', and list free variables with folds.
-- See 'LocScope' for a version with additional annotations between layers.
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

-- * Interface

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 #-}

-- | Substitution as a kind of monadic bind.
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 #-}

-- | Optional substitution as another kind of monadic bind.
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 #-}

-- | Lift an expression functor into the scope functor.
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 #-}

-- | Binds free variables in an expression and returns a binder.
scopeAbstract
  :: (Functor f, Eq a)
  => n
  -- ^ Annotation specific to your expression functor.
  -- Might contain original variable names and types, or might
  -- mark this as a "let" vs a "lambda"
  -> Seq a
  -- ^ Free variables to bind, like the names of function parameters
  -> Scope n f a
  -- ^ The expression to bind in, like the body of a function
  -> 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 #-}

-- | 'scopeAbstract' for a single argument.
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 #-}

-- | Un-bind free variables in an expression. Basically the inverse of
-- 'scopeAbstract'. Take care to match the arity of the binder! ('scopeApply' is safer.)
scopeUnAbstract
  :: Functor f
  => Seq a
  -- ^ The names of the variables you're freeing
  -> Scope n f a
   -- ^ The expression to substitute in (typically a binder)
  -> 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 #-}

-- 'scopeUnAbstract' for a single argument.
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 #-}

-- | Instantiate the bound variables in an expression with other expressions.
-- Take care to match the arity of the binder! ('scopeApply' is safer.)
scopeInstantiate
  :: Functor f
  => Seq (Scope n f a)
  -- ^ Expressions to substitute in place of bound vars
  -> Scope n f a
  -- ^ The expression to substitute in (typically a binder)
  -> 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 #-}

-- | 'scopeInstantiate' for a single argument.
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 #-}

-- | Instantiates the bound variables in an expression with other expressions.
-- Throws errors on mismatched arity, non binder expression, unbound vars, etc.
-- A version of 'scopeInstantiate' that fails loudly instead of silently!
scopeApply
  :: Functor f
  => Seq (Scope n f a)
  -- ^ Expressions to substitute in place of bound vars
  -> Scope n f a
  -- ^ The binder expression to substitute in
  -> 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 #-}

-- | 'scopeApply' for a single argument.
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 #-}