{-# LANGUAGE UndecidableInstances #-}

-- | Internals.
module Blanks.ScopeW
  ( ScopeWC
  , ScopeW (..)
  , scopeWFree
  , scopeWEmbed
  , scopeWFromInnerBinder
  , scopeWInnerBinder
  , scopeWInnerBinder1
  , scopeWAbstract
  , scopeWAbstract1
  , scopeWUnAbstract
  , scopeWUnAbstract1
  , scopeWInstantiate
  , scopeWInstantiate1
  , scopeWApply
  , scopeWApply1
  , scopeWBind
  , scopeWBindOpt
  , scopeWLift
  , scopeWLiftAnno
  , scopeWHoistAnno
  , scopeWMapAnno
  ) where

import Blanks.Core (BinderScope (..))
import Blanks.NatNewtype (NatNewtype, natNewtypeFrom, natNewtypeTo)
import Blanks.Sub (SubError (..))
import Blanks.Under (UnderScope (..), pattern UnderScopeBinder, pattern UnderScopeBound, pattern UnderScopeEmbed,
                     pattern UnderScopeFree, underScopeShift)
import Control.DeepSeq (NFData (..))
import Data.Bifoldable (bifoldr)
import Data.Bifunctor (bimap, first)
import Data.Bitraversable (bitraverse)
import Data.Functor.Adjunction (Adjunction (..))
import Data.Maybe (fromMaybe)
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq

-- * ScopeW, patterns, and instances

-- | The core internal scope type. (The "w" comes from "wrapper".)
-- We wrap up an 'UnderScope' in some functor and demand that we
-- unwrap it in an adjoint context. In the first case, these functors will be
-- 'Identity', yielding the 'Scope' newtype. In the second case, these
-- functors will be 'Located' and 'Colocated', yielding the 'LocScope' newtype.
newtype ScopeW t n f g a = ScopeW
  { ScopeW t n f g a -> t (UnderScope n f (g a) a)
unScopeW :: t (UnderScope n f (g a) a)
  }

instance NFData (t (UnderScope n f (g a) a)) => NFData (ScopeW t n f g a) where
  rnf :: ScopeW t n f g a -> ()
rnf (ScopeW tu :: t (UnderScope n f (g a) a)
tu) = () -> () -> ()
forall a b. a -> b -> b
seq (t (UnderScope n f (g a) a) -> ()
forall a. NFData a => a -> ()
rnf t (UnderScope n f (g a) a)
tu) ()

instance Eq (t (UnderScope n f (g a) a)) => Eq (ScopeW t n f g a) where
  ScopeW tu :: t (UnderScope n f (g a) a)
tu == :: ScopeW t n f g a -> ScopeW t n f g a -> Bool
== ScopeW tv :: t (UnderScope n f (g a) a)
tv = t (UnderScope n f (g a) a)
tu t (UnderScope n f (g a) a) -> t (UnderScope n f (g a) a) -> Bool
forall a. Eq a => a -> a -> Bool
== t (UnderScope n f (g a) a)
tv

instance Show (t (UnderScope n f (g a) a)) => Show (ScopeW t n f g a) where
  showsPrec :: Int -> ScopeW t n f g a -> ShowS
showsPrec d :: Int
d (ScopeW tu :: t (UnderScope n f (g a) a)
tu) = String -> ShowS
showString "ScopeW " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> t (UnderScope n f (g a) a) -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+1) t (UnderScope n f (g a) a)
tu

instance (Functor t, Functor f, Functor g) => Functor (ScopeW t n f g) where
  fmap :: (a -> b) -> ScopeW t n f g a -> ScopeW t n f g b
fmap f :: a -> b
f (ScopeW tu :: t (UnderScope n f (g a) a)
tu) = t (UnderScope n f (g b) b) -> ScopeW t n f g b
forall (t :: * -> *) n (f :: * -> *) (g :: * -> *) a.
t (UnderScope n f (g a) a) -> ScopeW t n f g a
ScopeW ((UnderScope n f (g a) a -> UnderScope n f (g b) b)
-> t (UnderScope n f (g a) a) -> t (UnderScope n f (g b) b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((g a -> g b)
-> (a -> b) -> UnderScope n f (g a) a -> UnderScope n f (g b) b
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ((a -> b) -> g a -> g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) a -> b
f) t (UnderScope n f (g a) a)
tu)

instance (Foldable t, Foldable f, Foldable g) => Foldable (ScopeW t n f g) where
  foldr :: (a -> b -> b) -> b -> ScopeW t n f g a -> b
foldr f :: a -> b -> b
f z :: b
z (ScopeW tu :: t (UnderScope n f (g a) a)
tu) = (UnderScope n f (g a) a -> b -> b)
-> b -> t (UnderScope n f (g a) a) -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((b -> UnderScope n f (g a) a -> b)
-> UnderScope n f (g a) a -> b -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((g a -> b -> b)
-> (a -> b -> b) -> b -> UnderScope n f (g a) a -> b
forall (p :: * -> * -> *) a c b.
Bifoldable p =>
(a -> c -> c) -> (b -> c -> c) -> c -> p a b -> c
bifoldr ((b -> g a -> b) -> g a -> b -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((a -> b -> b) -> b -> g a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> b -> b
f)) a -> b -> b
f)) b
z t (UnderScope n f (g a) a)
tu

instance (Traversable t, Traversable f, Traversable g) => Traversable (ScopeW t n f g) where
  traverse :: (a -> f b) -> ScopeW t n f g a -> f (ScopeW t n f g b)
traverse f :: a -> f b
f (ScopeW tu :: t (UnderScope n f (g a) a)
tu) = (t (UnderScope n f (g b) b) -> ScopeW t n f g b)
-> f (t (UnderScope n f (g b) b)) -> f (ScopeW t n f g b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap t (UnderScope n f (g b) b) -> ScopeW t n f g b
forall (t :: * -> *) n (f :: * -> *) (g :: * -> *) a.
t (UnderScope n f (g a) a) -> ScopeW t n f g a
ScopeW ((UnderScope n f (g a) a -> f (UnderScope n f (g b) b))
-> t (UnderScope n f (g a) a) -> f (t (UnderScope n f (g b) b))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((g a -> f (g b))
-> (a -> f b)
-> UnderScope n f (g a) a
-> f (UnderScope n f (g b) b)
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 ((a -> f b) -> g a -> f (g 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 b
f) t (UnderScope n f (g a) a)
tu)

type ScopeWC t u n f g = (Adjunction t u, Applicative u, Functor f, NatNewtype (ScopeW t n f g) g)

-- * Smart constructors, shift, and bind

scopeWMod :: ScopeWC t u n f g => (UnderScope n f (g a) a -> u x) -> g a -> x
scopeWMod :: (UnderScope n f (g a) a -> u x) -> g a -> x
scopeWMod f :: UnderScope n f (g a) a -> u x
f = (UnderScope n f (g a) a -> u x) -> t (UnderScope n f (g a) a) -> x
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct UnderScope n f (g a) a -> u x
f (t (UnderScope n f (g a) a) -> x)
-> (g a -> t (UnderScope n f (g a) a)) -> g a -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeW t n f g a -> t (UnderScope n f (g a) a)
forall (t :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeW t n f g a -> t (UnderScope n f (g a) a)
unScopeW (ScopeW t n f g a -> t (UnderScope n f (g a) a))
-> (g a -> ScopeW t n f g a) -> g a -> t (UnderScope n f (g a) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g a -> ScopeW t n f g a
forall (m :: * -> *) (g :: * -> *) a. NatNewtype m g => g a -> m a
natNewtypeFrom
{-# INLINE scopeWMod #-}

scopeWModOpt :: ScopeWC t u n f g => (UnderScope n f (g a) a -> Maybe (u (g a))) -> g a -> g a
scopeWModOpt :: (UnderScope n f (g a) a -> Maybe (u (g a))) -> g a -> g a
scopeWModOpt f :: UnderScope n f (g a) a -> Maybe (u (g a))
f s :: g a
s = (UnderScope n f (g a) a -> u (g a))
-> t (UnderScope n f (g a) a) -> g a
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (u (g a) -> Maybe (u (g a)) -> u (g a)
forall a. a -> Maybe a -> a
fromMaybe (g a -> u (g a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure g a
s) (Maybe (u (g a)) -> u (g a))
-> (UnderScope n f (g a) a -> Maybe (u (g a)))
-> UnderScope n f (g a) a
-> u (g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnderScope n f (g a) a -> Maybe (u (g a))
f) (ScopeW t n f g a -> t (UnderScope n f (g a) a)
forall (t :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeW t n f g a -> t (UnderScope n f (g a) a)
unScopeW (g a -> ScopeW t n f g a
forall (m :: * -> *) (g :: * -> *) a. NatNewtype m g => g a -> m a
natNewtypeFrom g a
s))
{-# INLINE scopeWModOpt #-}

scopeWModM :: (ScopeWC t u n f g, Traversable m) => (UnderScope n f (g a) a -> m (u x)) -> g a -> m x
scopeWModM :: (UnderScope n f (g a) a -> m (u x)) -> g a -> m x
scopeWModM f :: UnderScope n f (g a) a -> m (u x)
f = (UnderScope n f (g a) a -> u (m x))
-> t (UnderScope n f (g a) a) -> m x
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (m (u x) -> u (m x)
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA (m (u x) -> u (m x))
-> (UnderScope n f (g a) a -> m (u x))
-> UnderScope n f (g a) a
-> u (m x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnderScope n f (g a) a -> m (u x)
f) (t (UnderScope n f (g a) a) -> m x)
-> (g a -> t (UnderScope n f (g a) a)) -> g a -> m x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeW t n f g a -> t (UnderScope n f (g a) a)
forall (t :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeW t n f g a -> t (UnderScope n f (g a) a)
unScopeW (ScopeW t n f g a -> t (UnderScope n f (g a) a))
-> (g a -> ScopeW t n f g a) -> g a -> t (UnderScope n f (g a) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g a -> ScopeW t n f g a
forall (m :: * -> *) (g :: * -> *) a. NatNewtype m g => g a -> m a
natNewtypeFrom
{-# INLINE scopeWModM #-}

scopeWBound :: ScopeWC t u n f g => Int -> u (g a)
scopeWBound :: Int -> u (g a)
scopeWBound b :: Int
b = (t (UnderScope n f (g a) a) -> g a)
-> u (t (UnderScope n f (g a) a)) -> u (g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ScopeW t n f g a -> g a
forall (m :: * -> *) (g :: * -> *) a. NatNewtype m g => m a -> g a
natNewtypeTo (ScopeW t n f g a -> g a)
-> (t (UnderScope n f (g a) a) -> ScopeW t n f g a)
-> t (UnderScope n f (g a) a)
-> g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t (UnderScope n f (g a) a) -> ScopeW t n f g a
forall (t :: * -> *) n (f :: * -> *) (g :: * -> *) a.
t (UnderScope n f (g a) a) -> ScopeW t n f g a
ScopeW) (UnderScope n f (g a) a -> u (t (UnderScope n f (g a) a))
forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
a -> u (f a)
unit (Int -> UnderScope n f (g a) a
forall n (f :: * -> *) e a. Int -> UnderScope n f e a
UnderScopeBound Int
b))

scopeWFree :: ScopeWC t u n f g => a -> u (g a)
scopeWFree :: a -> u (g a)
scopeWFree a :: a
a = (t (UnderScope n f (g a) a) -> g a)
-> u (t (UnderScope n f (g a) a)) -> u (g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ScopeW t n f g a -> g a
forall (m :: * -> *) (g :: * -> *) a. NatNewtype m g => m a -> g a
natNewtypeTo (ScopeW t n f g a -> g a)
-> (t (UnderScope n f (g a) a) -> ScopeW t n f g a)
-> t (UnderScope n f (g a) a)
-> g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t (UnderScope n f (g a) a) -> ScopeW t n f g a
forall (t :: * -> *) n (f :: * -> *) (g :: * -> *) a.
t (UnderScope n f (g a) a) -> ScopeW t n f g a
ScopeW) (UnderScope n f (g a) a -> u (t (UnderScope n f (g a) a))
forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
a -> u (f a)
unit (a -> UnderScope n f (g a) a
forall a n (f :: * -> *) e. a -> UnderScope n f e a
UnderScopeFree a
a))

scopeWShift :: ScopeWC t u n f g => Int -> g a -> g a
scopeWShift :: Int -> g a -> g a
scopeWShift = Int -> Int -> g a -> g a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Int -> Int -> g a -> g a
scopeWShiftN 0
{-# INLINE scopeWShift #-}

scopeWShiftN :: ScopeWC t u n f g => Int -> Int -> g a -> g a
scopeWShiftN :: Int -> Int -> g a -> g a
scopeWShiftN c :: Int
c d :: Int
d e :: g a
e =
  let ScopeW tu :: t (UnderScope n f (g a) a)
tu = g a -> ScopeW t n f g a
forall (m :: * -> *) (g :: * -> *) a. NatNewtype m g => g a -> m a
natNewtypeFrom g a
e
  in ScopeW t n f g a -> g a
forall (m :: * -> *) (g :: * -> *) a. NatNewtype m g => m a -> g a
natNewtypeTo (t (UnderScope n f (g a) a) -> ScopeW t n f g a
forall (t :: * -> *) n (f :: * -> *) (g :: * -> *) a.
t (UnderScope n f (g a) a) -> ScopeW t n f g a
ScopeW ((UnderScope n f (g a) a -> UnderScope n f (g a) a)
-> t (UnderScope n f (g a) a) -> t (UnderScope n f (g a) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Int -> Int -> g a -> g a)
-> Int -> Int -> UnderScope n f (g a) a -> UnderScope n f (g a) a
forall (f :: * -> *) e n a.
Functor f =>
(Int -> Int -> e -> e)
-> Int -> Int -> UnderScope n f e a -> UnderScope n f e a
underScopeShift Int -> Int -> g a -> g a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Int -> Int -> g a -> g a
scopeWShiftN Int
c Int
d) t (UnderScope n f (g a) a)
tu))

scopeWBinder :: ScopeWC t u n f g => Int -> n -> g a -> u (g a)
scopeWBinder :: Int -> n -> g a -> u (g a)
scopeWBinder r :: Int
r n :: n
n e :: g a
e = (t (UnderScope n f (g a) a) -> g a)
-> u (t (UnderScope n f (g a) a)) -> u (g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ScopeW t n f g a -> g a
forall (m :: * -> *) (g :: * -> *) a. NatNewtype m g => m a -> g a
natNewtypeTo (ScopeW t n f g a -> g a)
-> (t (UnderScope n f (g a) a) -> ScopeW t n f g a)
-> t (UnderScope n f (g a) a)
-> g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t (UnderScope n f (g a) a) -> ScopeW t n f g a
forall (t :: * -> *) n (f :: * -> *) (g :: * -> *) a.
t (UnderScope n f (g a) a) -> ScopeW t n f g a
ScopeW) (UnderScope n f (g a) a -> u (t (UnderScope n f (g a) a))
forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
a -> u (f a)
unit (Int -> n -> g a -> UnderScope n f (g a) a
forall n e (f :: * -> *) a. Int -> n -> e -> UnderScope n f e a
UnderScopeBinder Int
r n
n g a
e))

scopeWFromInnerBinder :: ScopeWC t u n f g => BinderScope n (g a) -> u (g a)
scopeWFromInnerBinder :: BinderScope n (g a) -> u (g a)
scopeWFromInnerBinder b :: BinderScope n (g a)
b = (t (UnderScope n f (g a) a) -> g a)
-> u (t (UnderScope n f (g a) a)) -> u (g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ScopeW t n f g a -> g a
forall (m :: * -> *) (g :: * -> *) a. NatNewtype m g => m a -> g a
natNewtypeTo (ScopeW t n f g a -> g a)
-> (t (UnderScope n f (g a) a) -> ScopeW t n f g a)
-> t (UnderScope n f (g a) a)
-> g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t (UnderScope n f (g a) a) -> ScopeW t n f g a
forall (t :: * -> *) n (f :: * -> *) (g :: * -> *) a.
t (UnderScope n f (g a) a) -> ScopeW t n f g a
ScopeW) (UnderScope n f (g a) a -> u (t (UnderScope n f (g a) a))
forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
a -> u (f a)
unit (BinderScope n (g a) -> UnderScope n f (g a) a
forall n (f :: * -> *) e a. BinderScope n e -> UnderScope n f e a
UnderBinderScope BinderScope n (g a)
b))

scopeWEmbed :: ScopeWC t u n f g => f (g a) -> u (g a)
scopeWEmbed :: f (g a) -> u (g a)
scopeWEmbed fe :: f (g a)
fe = (t (UnderScope n f (g a) a) -> g a)
-> u (t (UnderScope n f (g a) a)) -> u (g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ScopeW t n f g a -> g a
forall (m :: * -> *) (g :: * -> *) a. NatNewtype m g => m a -> g a
natNewtypeTo (ScopeW t n f g a -> g a)
-> (t (UnderScope n f (g a) a) -> ScopeW t n f g a)
-> t (UnderScope n f (g a) a)
-> g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t (UnderScope n f (g a) a) -> ScopeW t n f g a
forall (t :: * -> *) n (f :: * -> *) (g :: * -> *) a.
t (UnderScope n f (g a) a) -> ScopeW t n f g a
ScopeW) (UnderScope n f (g a) a -> u (t (UnderScope n f (g a) a))
forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
a -> u (f a)
unit (f (g a) -> UnderScope n f (g a) a
forall (f :: * -> *) e n a. f e -> UnderScope n f e a
UnderScopeEmbed f (g a)
fe))

scopeWBind :: ScopeWC t u n f g => (a -> u (g b)) -> g a -> g b
scopeWBind :: (a -> u (g b)) -> g a -> g b
scopeWBind f :: a -> u (g b)
f = (a -> u (g b)) -> Int -> g a -> g b
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a
       b.
ScopeWC t u n f g =>
(a -> u (g b)) -> Int -> g a -> g b
scopeWBindN a -> u (g b)
f 0
{-# INLINE scopeWBind #-}

scopeWBindN :: ScopeWC t u n f g => (a -> u (g b)) -> Int -> g a -> g b
scopeWBindN :: (a -> u (g b)) -> Int -> g a -> g b
scopeWBindN f :: a -> u (g b)
f = (UnderScope n f (g a) a -> u (g b)) -> g a -> g b
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a
       x.
ScopeWC t u n f g =>
(UnderScope n f (g a) a -> u x) -> g a -> x
scopeWMod ((UnderScope n f (g a) a -> u (g b)) -> g a -> g b)
-> (Int -> UnderScope n f (g a) a -> u (g b)) -> Int -> g a -> g b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> UnderScope n f (g a) a -> u (g b)
go where
  go :: Int -> UnderScope n f (g a) a -> u (g b)
go i :: Int
i us :: UnderScope n f (g a) a
us =
    case UnderScope n f (g a) a
us of
      UnderScopeBound b :: Int
b -> Int -> u (g b)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Int -> u (g a)
scopeWBound Int
b
      UnderScopeFree a :: a
a -> (g b -> g b) -> u (g b) -> u (g b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> g b -> g b
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Int -> g a -> g a
scopeWShift Int
i) (a -> u (g b)
f a
a)
      UnderScopeBinder r :: Int
r x :: n
x e :: g a
e -> Int -> n -> g b -> u (g b)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Int -> n -> g a -> u (g a)
scopeWBinder Int
r n
x ((a -> u (g b)) -> Int -> g a -> g b
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a
       b.
ScopeWC t u n f g =>
(a -> u (g b)) -> Int -> g a -> g b
scopeWBindN a -> u (g b)
f (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
r) g a
e)
      UnderScopeEmbed fe :: f (g a)
fe -> f (g b) -> u (g b)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
f (g a) -> u (g a)
scopeWEmbed ((g a -> g b) -> f (g a) -> f (g b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> u (g b)) -> Int -> g a -> g b
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a
       b.
ScopeWC t u n f g =>
(a -> u (g b)) -> Int -> g a -> g b
scopeWBindN a -> u (g b)
f Int
i) f (g a)
fe)

scopeWBindOpt :: ScopeWC t u n f g => (a -> Maybe (u (g a))) -> g a -> g a
scopeWBindOpt :: (a -> Maybe (u (g a))) -> g a -> g a
scopeWBindOpt f :: a -> Maybe (u (g a))
f = (a -> Maybe (u (g a))) -> Int -> g a -> g a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
(a -> Maybe (u (g a))) -> Int -> g a -> g a
scopeWBindOptN a -> Maybe (u (g a))
f 0
{-# INLINE scopeWBindOpt #-}

scopeWBindOptN :: ScopeWC t u n f g => (a -> Maybe (u (g a))) -> Int -> g a -> g a
scopeWBindOptN :: (a -> Maybe (u (g a))) -> Int -> g a -> g a
scopeWBindOptN f :: a -> Maybe (u (g a))
f = (UnderScope n f (g a) a -> Maybe (u (g a))) -> g a -> g a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
(UnderScope n f (g a) a -> Maybe (u (g a))) -> g a -> g a
scopeWModOpt ((UnderScope n f (g a) a -> Maybe (u (g a))) -> g a -> g a)
-> (Int -> UnderScope n f (g a) a -> Maybe (u (g a)))
-> Int
-> g a
-> g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> UnderScope n f (g a) a -> Maybe (u (g a))
go where
  go :: Int -> UnderScope n f (g a) a -> Maybe (u (g a))
go i :: Int
i us :: UnderScope n f (g a) a
us =
    case UnderScope n f (g a) a
us of
      UnderScopeBound _ -> Maybe (u (g a))
forall a. Maybe a
Nothing
      UnderScopeFree a :: a
a -> (u (g a) -> u (g a)) -> Maybe (u (g a)) -> Maybe (u (g a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((g a -> g a) -> u (g a) -> u (g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> g a -> g a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Int -> g a -> g a
scopeWShift Int
i)) (a -> Maybe (u (g a))
f a
a)
      UnderScopeBinder r :: Int
r x :: n
x e :: g a
e -> u (g a) -> Maybe (u (g a))
forall a. a -> Maybe a
Just (Int -> n -> g a -> u (g a)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Int -> n -> g a -> u (g a)
scopeWBinder Int
r n
x ((a -> Maybe (u (g a))) -> Int -> g a -> g a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
(a -> Maybe (u (g a))) -> Int -> g a -> g a
scopeWBindOptN a -> Maybe (u (g a))
f (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
r) g a
e))
      UnderScopeEmbed fe :: f (g a)
fe -> u (g a) -> Maybe (u (g a))
forall a. a -> Maybe a
Just (f (g a) -> u (g a)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
f (g a) -> u (g a)
scopeWEmbed ((g a -> g a) -> f (g a) -> f (g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> Maybe (u (g a))) -> Int -> g a -> g a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
(a -> Maybe (u (g a))) -> Int -> g a -> g a
scopeWBindOptN a -> Maybe (u (g a))
f Int
i) f (g a)
fe))

scopeWLift :: (ScopeWC t u n f g, Monad u, Traversable f) => f a -> u (g a)
scopeWLift :: f a -> u (g a)
scopeWLift fa :: f a
fa = (a -> u (g a)) -> f a -> u (f (g a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> u (g a)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
a -> u (g a)
scopeWFree f a
fa u (f (g a)) -> (f (g a) -> u (g a)) -> u (g a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= f (g a) -> u (g a)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
f (g a) -> u (g a)
scopeWEmbed

-- * Abstraction

scopeWInnerBinder :: (ScopeWC t u n f g, Eq a) => n -> Seq a -> g a -> BinderScope n (g a)
scopeWInnerBinder :: n -> Seq a -> g a -> BinderScope n (g a)
scopeWInnerBinder n :: n
n ks :: Seq a
ks e :: g a
e =
  let r :: Int
r = Seq a -> Int
forall a. Seq a -> Int
Seq.length Seq a
ks
      e' :: g a
e' = Int -> g a -> g a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Int -> g a -> g a
scopeWShift Int
r g a
e
      f :: a -> Maybe (u (g a))
f = (Int -> u (g a)) -> Maybe Int -> Maybe (u (g a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> u (g a)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Int -> u (g a)
scopeWBound (Maybe Int -> Maybe (u (g a)))
-> (a -> Maybe Int) -> a -> Maybe (u (g a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Seq a -> Maybe Int) -> Seq a -> a -> Maybe Int
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> Seq a -> Maybe Int
forall a. Eq a => a -> Seq a -> Maybe Int
Seq.elemIndexL Seq a
ks
      e'' :: g a
e'' = (a -> Maybe (u (g a))) -> g a -> g a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
(a -> Maybe (u (g a))) -> g a -> g a
scopeWBindOpt a -> Maybe (u (g a))
f g a
e'
  in Int -> n -> g a -> BinderScope n (g a)
forall n e. Int -> n -> e -> BinderScope n e
BinderScope Int
r n
n g a
e''

scopeWInnerBinder1 :: (ScopeWC t u n f g, Eq a) => n -> a -> g a -> BinderScope n (g a)
scopeWInnerBinder1 :: n -> a -> g a -> BinderScope n (g a)
scopeWInnerBinder1 n :: n
n = n -> Seq a -> g a -> BinderScope n (g 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 n
n (Seq a -> g a -> BinderScope n (g a))
-> (a -> Seq a) -> a -> g a -> BinderScope n (g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Seq a
forall a. a -> Seq a
Seq.singleton
{-# INLINE scopeWInnerBinder1 #-}

scopeWAbstract :: (ScopeWC t u n f g, Eq a) => n -> Seq a -> g a -> u (g a)
scopeWAbstract :: n -> Seq a -> g a -> u (g a)
scopeWAbstract n :: n
n ks :: Seq a
ks e :: g a
e = BinderScope n (g a) -> u (g a)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
BinderScope n (g a) -> u (g a)
scopeWFromInnerBinder (n -> Seq a -> g a -> BinderScope n (g 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 n
n Seq a
ks g a
e)
{-# INLINE scopeWAbstract #-}

scopeWAbstract1 :: (ScopeWC t u n f g, Eq a) => n -> a -> g a -> u (g a)
scopeWAbstract1 :: n -> a -> g a -> u (g a)
scopeWAbstract1 n :: n
n = n -> Seq a -> g a -> u (g 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 -> g a -> u (g a)) -> (a -> Seq a) -> a -> g a -> u (g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Seq a
forall a. a -> Seq a
Seq.singleton
{-# INLINE scopeWAbstract1 #-}

scopeWUnAbstract :: ScopeWC t u n f g => Seq a -> g a -> g a
scopeWUnAbstract :: Seq a -> g a -> g a
scopeWUnAbstract ks :: Seq a
ks = Seq (u (g a)) -> g a -> g a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Seq (u (g a)) -> g a -> g a
scopeWInstantiate ((a -> u (g a)) -> Seq a -> Seq (u (g a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> u (g a)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
a -> u (g a)
scopeWFree Seq a
ks)
{-# INLINE scopeWUnAbstract #-}

scopeWUnAbstract1 :: ScopeWC t u n f g => a -> g a -> g a
scopeWUnAbstract1 :: a -> g a -> g a
scopeWUnAbstract1 = Seq a -> g a -> g a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Seq a -> g a -> g a
scopeWUnAbstract (Seq a -> g a -> g a) -> (a -> Seq a) -> a -> g a -> g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Seq a
forall a. a -> Seq a
Seq.singleton
{-# INLINE scopeWUnAbstract1 #-}

scopeWInstantiate :: ScopeWC t u n f g => Seq (u (g a)) -> g a -> g a
scopeWInstantiate :: Seq (u (g a)) -> g a -> g a
scopeWInstantiate = Int -> Seq (u (g a)) -> g a -> g a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Int -> Seq (u (g a)) -> g a -> g a
scopeWInstantiateN 0
{-# INLINE scopeWInstantiate #-}

scopeWInstantiate1 :: ScopeWC t u n f g => u (g a) -> g a -> g a
scopeWInstantiate1 :: u (g a) -> g a -> g a
scopeWInstantiate1 = Seq (u (g a)) -> g a -> g a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Seq (u (g a)) -> g a -> g a
scopeWInstantiate (Seq (u (g a)) -> g a -> g a)
-> (u (g a) -> Seq (u (g a))) -> u (g a) -> g a -> g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. u (g a) -> Seq (u (g a))
forall a. a -> Seq a
Seq.singleton
{-# INLINE scopeWInstantiate1 #-}

scopeWInstantiateN :: ScopeWC t u n f g => Int -> Seq (u (g a)) -> g a -> g a
scopeWInstantiateN :: Int -> Seq (u (g a)) -> g a -> g a
scopeWInstantiateN h :: Int
h vs :: Seq (u (g a))
vs = (UnderScope n f (g a) a -> Maybe (u (g a))) -> g a -> g a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
(UnderScope n f (g a) a -> Maybe (u (g a))) -> g a -> g a
scopeWModOpt (Int -> UnderScope n f (g a) a -> Maybe (u (g a))
go Int
h) where
  go :: Int -> UnderScope n f (g a) a -> Maybe (u (g a))
go i :: Int
i us :: UnderScope n f (g a) a
us =
    case UnderScope n f (g a) a
us of
      UnderScopeBound b :: Int
b -> Seq (u (g a))
vs Seq (u (g a)) -> Int -> Maybe (u (g a))
forall a. Seq a -> Int -> Maybe a
Seq.!? (Int
b Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i)
      UnderScopeFree _ -> Maybe (u (g a))
forall a. Maybe a
Nothing
      UnderScopeBinder r :: Int
r n :: n
n e :: g a
e ->
        let vs' :: Seq (u (g a))
vs' = (u (g a) -> u (g a)) -> Seq (u (g a)) -> Seq (u (g a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((g a -> g a) -> u (g a) -> u (g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> g a -> g a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Int -> g a -> g a
scopeWShift Int
r)) Seq (u (g a))
vs
            e' :: g a
e' = Int -> Seq (u (g a)) -> g a -> g a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Int -> Seq (u (g a)) -> g a -> g a
scopeWInstantiateN (Int
r Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i) Seq (u (g a))
vs' g a
e
        in u (g a) -> Maybe (u (g a))
forall a. a -> Maybe a
Just (Int -> n -> g a -> u (g a)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Int -> n -> g a -> u (g a)
scopeWBinder Int
r n
n g a
e')
      UnderScopeEmbed fe :: f (g a)
fe -> u (g a) -> Maybe (u (g a))
forall a. a -> Maybe a
Just (f (g a) -> u (g a)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
f (g a) -> u (g a)
scopeWEmbed ((g a -> g a) -> f (g a) -> f (g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Seq (u (g a)) -> g a -> g a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Int -> Seq (u (g a)) -> g a -> g a
scopeWInstantiateN Int
i Seq (u (g a))
vs) f (g a)
fe))

scopeWApply :: ScopeWC t u n f g => Seq (u (g a)) -> g a -> Either SubError (g a)
scopeWApply :: Seq (u (g a)) -> g a -> Either SubError (g a)
scopeWApply vs :: Seq (u (g a))
vs = (UnderScope n f (g a) a -> Either SubError (u (g a)))
-> g a -> Either SubError (g a)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *)
       (m :: * -> *) a x.
(ScopeWC t u n f g, Traversable m) =>
(UnderScope n f (g a) a -> m (u x)) -> g a -> m x
scopeWModM UnderScope n f (g a) a -> Either SubError (u (g a))
go where
  go :: UnderScope n f (g a) a -> Either SubError (u (g a))
go us :: UnderScope n f (g a) a
us =
    case UnderScope n f (g a) a
us of
      UnderScopeBinder r :: Int
r _ e :: g a
e ->
        let len :: Int
len = Seq (u (g a)) -> Int
forall a. Seq a -> Int
Seq.length Seq (u (g a))
vs
        in if Int
len Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
r
              then u (g a) -> Either SubError (u (g a))
forall a b. b -> Either a b
Right (g a -> u (g a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> g a -> g a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Int -> g a -> g a
scopeWShift (-1) (Seq (u (g a)) -> g a -> g a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Seq (u (g a)) -> g a -> g a
scopeWInstantiate Seq (u (g a))
vs g a
e)))
              else SubError -> Either SubError (u (g a))
forall a b. a -> Either a b
Left (Int -> Int -> SubError
ApplyError Int
len Int
r)
      _ -> SubError -> Either SubError (u (g a))
forall a b. a -> Either a b
Left SubError
NonBinderError

scopeWApply1 :: ScopeWC t u n f g => u (g a) -> g a -> Either SubError (g a)
scopeWApply1 :: u (g a) -> g a -> Either SubError (g a)
scopeWApply1 = Seq (u (g a)) -> g a -> Either SubError (g 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 (Seq (u (g a)) -> g a -> Either SubError (g a))
-> (u (g a) -> Seq (u (g a)))
-> u (g a)
-> g a
-> Either SubError (g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. u (g a) -> Seq (u (g a))
forall a. a -> Seq a
Seq.singleton
{-# INLINE scopeWApply1 #-}

-- * Annotation functions

scopeWLiftAnno :: (NatNewtype (ScopeW t n f g) g, Functor t) => t a -> g a
scopeWLiftAnno :: t a -> g a
scopeWLiftAnno = ScopeW t n f g a -> g a
forall (m :: * -> *) (g :: * -> *) a. NatNewtype m g => m a -> g a
natNewtypeTo (ScopeW t n f g a -> g a)
-> (t a -> ScopeW t n f g a) -> t a -> g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t (UnderScope n f (g a) a) -> ScopeW t n f g a
forall (t :: * -> *) n (f :: * -> *) (g :: * -> *) a.
t (UnderScope n f (g a) a) -> ScopeW t n f g a
ScopeW (t (UnderScope n f (g a) a) -> ScopeW t n f g a)
-> (t a -> t (UnderScope n f (g a) a)) -> t a -> ScopeW t n f g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> UnderScope n f (g a) a) -> t a -> t (UnderScope n f (g a) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> UnderScope n f (g a) a
forall a n (f :: * -> *) e. a -> UnderScope n f e a
UnderScopeFree

scopeWHoistAnno :: (NatNewtype (ScopeW t n f g) g, NatNewtype (ScopeW w n f h) h, Functor t, Functor w, Functor f) => (forall x. t x -> w x) -> g a -> h a
scopeWHoistAnno :: (forall x. t x -> w x) -> g a -> h a
scopeWHoistAnno nat :: forall x. t x -> w x
nat ga :: g a
ga =
  let ScopeW tu :: t (UnderScope n f (g a) a)
tu = g a -> ScopeW t n f g a
forall (m :: * -> *) (g :: * -> *) a. NatNewtype m g => g a -> m a
natNewtypeFrom g a
ga
      s :: ScopeW w n f h a
s = w (UnderScope n f (h a) a) -> ScopeW w n f h a
forall (t :: * -> *) n (f :: * -> *) (g :: * -> *) a.
t (UnderScope n f (g a) a) -> ScopeW t n f g a
ScopeW (t (UnderScope n f (h a) a) -> w (UnderScope n f (h a) a)
forall x. t x -> w x
nat ((UnderScope n f (g a) a -> UnderScope n f (h a) a)
-> t (UnderScope n f (g a) a) -> t (UnderScope n f (h a) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((g a -> h a) -> UnderScope n f (g a) a -> UnderScope n f (h a) a
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((forall x. t x -> w x) -> g a -> h a
forall (t :: * -> *) n (f :: * -> *) (g :: * -> *) (w :: * -> *)
       (h :: * -> *) a.
(NatNewtype (ScopeW t n f g) g, NatNewtype (ScopeW w n f h) h,
 Functor t, Functor w, Functor f) =>
(forall x. t x -> w x) -> g a -> h a
scopeWHoistAnno forall x. t x -> w x
nat)) t (UnderScope n f (g a) a)
tu))
  in ScopeW w n f h a -> h a
forall (m :: * -> *) (g :: * -> *) a. NatNewtype m g => m a -> g a
natNewtypeTo ScopeW w n f h a
s

scopeWMapAnno :: ScopeWC t u n f g => (t a -> t b) -> g a -> g b
scopeWMapAnno :: (t a -> t b) -> g a -> g b
scopeWMapAnno f :: t a -> t b
f = (UnderScope n f (g a) a -> u (g b)) -> g a -> g b
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a
       x.
ScopeWC t u n f g =>
(UnderScope n f (g a) a -> u x) -> g a -> x
scopeWMod UnderScope n f (g a) a -> u (g b)
go where
  go :: UnderScope n f (g a) a -> u (g b)
go us :: UnderScope n f (g a) a
us = case UnderScope n f (g a) a
us of
    UnderScopeBound b :: Int
b -> Int -> u (g b)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Int -> u (g a)
scopeWBound Int
b
    UnderScopeFree a :: a
a -> (t a -> g b) -> u (t a) -> u (g b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ScopeW t n f g b -> g b
forall (m :: * -> *) (g :: * -> *) a. NatNewtype m g => m a -> g a
natNewtypeTo (ScopeW t n f g b -> g b)
-> (t a -> ScopeW t n f g b) -> t a -> g b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t (UnderScope n f (g b) b) -> ScopeW t n f g b
forall (t :: * -> *) n (f :: * -> *) (g :: * -> *) a.
t (UnderScope n f (g a) a) -> ScopeW t n f g a
ScopeW (t (UnderScope n f (g b) b) -> ScopeW t n f g b)
-> (t a -> t (UnderScope n f (g b) b)) -> t a -> ScopeW t n f g b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> UnderScope n f (g b) b) -> t b -> t (UnderScope n f (g b) b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> UnderScope n f (g b) b
forall a n (f :: * -> *) e. a -> UnderScope n f e a
UnderScopeFree (t b -> t (UnderScope n f (g b) b))
-> (t a -> t b) -> t a -> t (UnderScope n f (g b) b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t a -> t b
f) (a -> u (t a)
forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
a -> u (f a)
unit a
a)
    UnderScopeBinder r :: Int
r x :: n
x e :: g a
e -> Int -> n -> g b -> u (g b)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Int -> n -> g a -> u (g a)
scopeWBinder Int
r n
x ((t a -> t b) -> g a -> g b
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a
       b.
ScopeWC t u n f g =>
(t a -> t b) -> g a -> g b
scopeWMapAnno t a -> t b
f g a
e)
    UnderScopeEmbed fe :: f (g a)
fe -> f (g b) -> u (g b)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
f (g a) -> u (g a)
scopeWEmbed ((g a -> g b) -> f (g a) -> f (g b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((t a -> t b) -> g a -> g b
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a
       b.
ScopeWC t u n f g =>
(t a -> t b) -> g a -> g b
scopeWMapAnno t a -> t b
f) f (g a)
fe)