{-# LANGUAGE UndecidableInstances #-}

module Blanks.LocScope
  ( LocScope (..)
  , pattern LocScopeBound
  , pattern LocScopeFree
  , pattern LocScopeBinder
  , pattern LocScopeEmbed
  , locScopeLocation
  , locScopeFree
  , locScopeEmbed
  , locScopeFromInnerBinder
  , locScopeBind
  , locScopeBindOpt
  , locScopeLift
  , locScopeInnerBinder
  , locScopeInnerBinder1
  , locScopeAbstract
  , locScopeAbstract1
  , locScopeUnAbstract
  , locScopeUnAbstract1
  , locScopeInstantiate
  , locScopeInstantiate1
  , locScopeApply
  , locScopeApply1
  , locScopeLiftAnno
  , locScopeHoistAnno
  , locScopeMapAnno
  ) where

import Blanks.Core (BinderScope)
import Blanks.Located (Colocated, Located (..), askColocated)
import Blanks.NatNewtype (NatNewtype)
import Blanks.ScopeW (ScopeW (..), scopeWAbstract, scopeWAbstract1, scopeWApply, scopeWApply1, scopeWBind,
                      scopeWBindOpt, scopeWEmbed, scopeWFree, scopeWFromInnerBinder, scopeWHoistAnno, scopeWInnerBinder,
                      scopeWInnerBinder1, scopeWInstantiate, scopeWInstantiate1, scopeWLift, scopeWLiftAnno,
                      scopeWMapAnno, 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.Writer (MonadWriter (..))
import Data.Sequence (Seq)

-- | A 'Scope' annotated with some information between constructors.
newtype LocScope l n f a = LocScope
  { LocScope l n f a -> ScopeW (Located l) n f (LocScope l n f) a
unLocScope :: ScopeW (Located l) n f (LocScope l n f) a
  } deriving stock (a -> LocScope l n f b -> LocScope l n f a
(a -> b) -> LocScope l n f a -> LocScope l n f b
(forall a b. (a -> b) -> LocScope l n f a -> LocScope l n f b)
-> (forall a b. a -> LocScope l n f b -> LocScope l n f a)
-> Functor (LocScope l n f)
forall a b. a -> LocScope l n f b -> LocScope l n f a
forall a b. (a -> b) -> LocScope l n f a -> LocScope l n f b
forall l n (f :: * -> *) a b.
Functor f =>
a -> LocScope l n f b -> LocScope l n f a
forall l n (f :: * -> *) a b.
Functor f =>
(a -> b) -> LocScope l n f a -> LocScope l 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 -> LocScope l n f b -> LocScope l n f a
$c<$ :: forall l n (f :: * -> *) a b.
Functor f =>
a -> LocScope l n f b -> LocScope l n f a
fmap :: (a -> b) -> LocScope l n f a -> LocScope l n f b
$cfmap :: forall l n (f :: * -> *) a b.
Functor f =>
(a -> b) -> LocScope l n f a -> LocScope l n f b
Functor, LocScope l n f a -> Bool
(a -> m) -> LocScope l n f a -> m
(a -> b -> b) -> b -> LocScope l n f a -> b
(forall m. Monoid m => LocScope l n f m -> m)
-> (forall m a. Monoid m => (a -> m) -> LocScope l n f a -> m)
-> (forall m a. Monoid m => (a -> m) -> LocScope l n f a -> m)
-> (forall a b. (a -> b -> b) -> b -> LocScope l n f a -> b)
-> (forall a b. (a -> b -> b) -> b -> LocScope l n f a -> b)
-> (forall b a. (b -> a -> b) -> b -> LocScope l n f a -> b)
-> (forall b a. (b -> a -> b) -> b -> LocScope l n f a -> b)
-> (forall a. (a -> a -> a) -> LocScope l n f a -> a)
-> (forall a. (a -> a -> a) -> LocScope l n f a -> a)
-> (forall a. LocScope l n f a -> [a])
-> (forall a. LocScope l n f a -> Bool)
-> (forall a. LocScope l n f a -> Int)
-> (forall a. Eq a => a -> LocScope l n f a -> Bool)
-> (forall a. Ord a => LocScope l n f a -> a)
-> (forall a. Ord a => LocScope l n f a -> a)
-> (forall a. Num a => LocScope l n f a -> a)
-> (forall a. Num a => LocScope l n f a -> a)
-> Foldable (LocScope l n f)
forall a. Eq a => a -> LocScope l n f a -> Bool
forall a. Num a => LocScope l n f a -> a
forall a. Ord a => LocScope l n f a -> a
forall m. Monoid m => LocScope l n f m -> m
forall a. LocScope l n f a -> Bool
forall a. LocScope l n f a -> Int
forall a. LocScope l n f a -> [a]
forall a. (a -> a -> a) -> LocScope l n f a -> a
forall m a. Monoid m => (a -> m) -> LocScope l n f a -> m
forall b a. (b -> a -> b) -> b -> LocScope l n f a -> b
forall a b. (a -> b -> b) -> b -> LocScope l n f a -> b
forall l n (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> LocScope l n f a -> Bool
forall l n (f :: * -> *) a.
(Foldable f, Num a) =>
LocScope l n f a -> a
forall l n (f :: * -> *) a.
(Foldable f, Ord a) =>
LocScope l n f a -> a
forall l n (f :: * -> *) m.
(Foldable f, Monoid m) =>
LocScope l n f m -> m
forall l n (f :: * -> *) a. Foldable f => LocScope l n f a -> Bool
forall l n (f :: * -> *) a. Foldable f => LocScope l n f a -> Int
forall l n (f :: * -> *) a. Foldable f => LocScope l n f a -> [a]
forall l n (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> LocScope l n f a -> a
forall l n (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> LocScope l n f a -> m
forall l n (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> LocScope l n f a -> b
forall l n (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> LocScope l 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 :: LocScope l n f a -> a
$cproduct :: forall l n (f :: * -> *) a.
(Foldable f, Num a) =>
LocScope l n f a -> a
sum :: LocScope l n f a -> a
$csum :: forall l n (f :: * -> *) a.
(Foldable f, Num a) =>
LocScope l n f a -> a
minimum :: LocScope l n f a -> a
$cminimum :: forall l n (f :: * -> *) a.
(Foldable f, Ord a) =>
LocScope l n f a -> a
maximum :: LocScope l n f a -> a
$cmaximum :: forall l n (f :: * -> *) a.
(Foldable f, Ord a) =>
LocScope l n f a -> a
elem :: a -> LocScope l n f a -> Bool
$celem :: forall l n (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> LocScope l n f a -> Bool
length :: LocScope l n f a -> Int
$clength :: forall l n (f :: * -> *) a. Foldable f => LocScope l n f a -> Int
null :: LocScope l n f a -> Bool
$cnull :: forall l n (f :: * -> *) a. Foldable f => LocScope l n f a -> Bool
toList :: LocScope l n f a -> [a]
$ctoList :: forall l n (f :: * -> *) a. Foldable f => LocScope l n f a -> [a]
foldl1 :: (a -> a -> a) -> LocScope l n f a -> a
$cfoldl1 :: forall l n (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> LocScope l n f a -> a
foldr1 :: (a -> a -> a) -> LocScope l n f a -> a
$cfoldr1 :: forall l n (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> LocScope l n f a -> a
foldl' :: (b -> a -> b) -> b -> LocScope l n f a -> b
$cfoldl' :: forall l n (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> LocScope l n f a -> b
foldl :: (b -> a -> b) -> b -> LocScope l n f a -> b
$cfoldl :: forall l n (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> LocScope l n f a -> b
foldr' :: (a -> b -> b) -> b -> LocScope l n f a -> b
$cfoldr' :: forall l n (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> LocScope l n f a -> b
foldr :: (a -> b -> b) -> b -> LocScope l n f a -> b
$cfoldr :: forall l n (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> LocScope l n f a -> b
foldMap' :: (a -> m) -> LocScope l n f a -> m
$cfoldMap' :: forall l n (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> LocScope l n f a -> m
foldMap :: (a -> m) -> LocScope l n f a -> m
$cfoldMap :: forall l n (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> LocScope l n f a -> m
fold :: LocScope l n f m -> m
$cfold :: forall l n (f :: * -> *) m.
(Foldable f, Monoid m) =>
LocScope l n f m -> m
Foldable, Functor (LocScope l n f)
Foldable (LocScope l n f)
(Functor (LocScope l n f), Foldable (LocScope l n f)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> LocScope l n f a -> f (LocScope l n f b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    LocScope l n f (f a) -> f (LocScope l n f a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> LocScope l n f a -> m (LocScope l n f b))
-> (forall (m :: * -> *) a.
    Monad m =>
    LocScope l n f (m a) -> m (LocScope l n f a))
-> Traversable (LocScope l n f)
(a -> f b) -> LocScope l n f a -> f (LocScope l n f b)
forall l n (f :: * -> *). Traversable f => Functor (LocScope l n f)
forall l n (f :: * -> *).
Traversable f =>
Foldable (LocScope l n f)
forall l n (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
LocScope l n f (m a) -> m (LocScope l n f a)
forall l n (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
LocScope l n f (f a) -> f (LocScope l n f a)
forall l n (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> LocScope l n f a -> m (LocScope l n f b)
forall l n (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> LocScope l n f a -> f (LocScope l 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 =>
LocScope l n f (m a) -> m (LocScope l n f a)
forall (f :: * -> *) a.
Applicative f =>
LocScope l n f (f a) -> f (LocScope l n f a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LocScope l n f a -> m (LocScope l n f b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LocScope l n f a -> f (LocScope l n f b)
sequence :: LocScope l n f (m a) -> m (LocScope l n f a)
$csequence :: forall l n (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
LocScope l n f (m a) -> m (LocScope l n f a)
mapM :: (a -> m b) -> LocScope l n f a -> m (LocScope l n f b)
$cmapM :: forall l n (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> LocScope l n f a -> m (LocScope l n f b)
sequenceA :: LocScope l n f (f a) -> f (LocScope l n f a)
$csequenceA :: forall l n (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
LocScope l n f (f a) -> f (LocScope l n f a)
traverse :: (a -> f b) -> LocScope l n f a -> f (LocScope l n f b)
$ctraverse :: forall l n (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> LocScope l n f a -> f (LocScope l n f b)
$cp2Traversable :: forall l n (f :: * -> *).
Traversable f =>
Foldable (LocScope l n f)
$cp1Traversable :: forall l n (f :: * -> *). Traversable f => Functor (LocScope l n f)
Traversable)

instance NatNewtype (ScopeW (Located l) n f (LocScope l n f)) (LocScope l n f)

instance (NFData l, NFData n, NFData a, NFData (f (LocScope l n f a))) => NFData (LocScope l n f a) where
  rnf :: LocScope l n f a -> ()
rnf (LocScope s :: ScopeW (Located l) n f (LocScope l n f) a
s) = () -> () -> ()
forall a b. a -> b -> b
seq (ScopeW (Located l) n f (LocScope l n f) a -> ()
forall a. NFData a => a -> ()
rnf ScopeW (Located l) n f (LocScope l n f) a
s) ()

pattern LocScopeBound :: l -> Int -> LocScope l n f a
pattern $bLocScopeBound :: l -> Int -> LocScope l n f a
$mLocScopeBound :: forall r l n (f :: * -> *) a.
LocScope l n f a -> (l -> Int -> r) -> (Void# -> r) -> r
LocScopeBound l b = LocScope (ScopeW (Located l (UnderScopeBound b)))

pattern LocScopeFree :: l -> a -> LocScope l n f a
pattern $bLocScopeFree :: l -> a -> LocScope l n f a
$mLocScopeFree :: forall r l a n (f :: * -> *).
LocScope l n f a -> (l -> a -> r) -> (Void# -> r) -> r
LocScopeFree l a = LocScope (ScopeW (Located l (UnderScopeFree a)))

pattern LocScopeBinder :: l -> Int -> n -> LocScope l n f a -> LocScope l n f a
pattern $bLocScopeBinder :: l -> Int -> n -> LocScope l n f a -> LocScope l n f a
$mLocScopeBinder :: forall r l n (f :: * -> *) a.
LocScope l n f a
-> (l -> Int -> n -> LocScope l n f a -> r) -> (Void# -> r) -> r
LocScopeBinder l i n e = LocScope (ScopeW (Located l (UnderScopeBinder i n e)))

pattern LocScopeEmbed :: l -> f (LocScope l n f a) -> LocScope l n f a
pattern $bLocScopeEmbed :: l -> f (LocScope l n f a) -> LocScope l n f a
$mLocScopeEmbed :: forall r l (f :: * -> *) n a.
LocScope l n f a
-> (l -> f (LocScope l n f a) -> r) -> (Void# -> r) -> r
LocScopeEmbed l fe = LocScope (ScopeW (Located l (UnderScopeEmbed fe)))

{-# COMPLETE LocScopeBound, LocScopeFree, LocScopeBinder, LocScopeEmbed #-}

-- | Extract the location (annotation) from this scope.
locScopeLocation :: LocScope l n f a -> l
locScopeLocation :: LocScope l n f a -> l
locScopeLocation s :: LocScope l n f a
s =
  case LocScope l n f a
s of
    LocScopeBound l :: l
l _ -> l
l
    LocScopeFree l :: l
l _ -> l
l
    LocScopeBinder l :: l
l _ _ _ -> l
l
    LocScopeEmbed l :: l
l _ -> l
l

instance (Monoid l, Functor f) => Applicative (LocScope l n f) where
  pure :: a -> LocScope l n f a
pure = l -> a -> LocScope l n f a
forall l a n (f :: * -> *). l -> a -> LocScope l n f a
LocScopeFree l
forall a. Monoid a => a
mempty
  <*> :: LocScope l n f (a -> b) -> LocScope l n f a -> LocScope l n f b
(<*>) = LocScope l n f (a -> b) -> LocScope l n f a -> LocScope l n f b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance (Monoid l, Functor f) => Monad (LocScope l n f) where
  return :: a -> LocScope l n f a
return = a -> LocScope l n f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  s :: LocScope l n f a
s >>= :: LocScope l n f a -> (a -> LocScope l n f b) -> LocScope l n f b
>>= f :: a -> LocScope l n f b
f = (a -> Colocated l (LocScope l n f b))
-> LocScope l n f a -> LocScope l n f b
forall (f :: * -> *) a l n b.
Functor f =>
(a -> Colocated l (LocScope l n f b))
-> LocScope l n f a -> LocScope l n f b
locScopeBind a -> Colocated l (LocScope l n f b)
go LocScope l n f a
s where
    go :: a -> Colocated l (LocScope l n f b)
go a :: a
a = (l -> LocScope l n f b)
-> Colocated l l -> Colocated l (LocScope l n f b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\l1 :: l
l1 -> let LocScope (ScopeW (Located l2 :: l
l2 b :: UnderScope n f (LocScope l n f b) b
b)) = a -> LocScope l n f b
f a
a in ScopeW (Located l) n f (LocScope l n f) b -> LocScope l n f b
forall l n (f :: * -> *) a.
ScopeW (Located l) n f (LocScope l n f) a -> LocScope l n f a
LocScope (Located l (UnderScope n f (LocScope l n f b) b)
-> ScopeW (Located l) n f (LocScope l n f) b
forall (t :: * -> *) n (f :: * -> *) (g :: * -> *) a.
t (UnderScope n f (g a) a) -> ScopeW t n f g a
ScopeW (l
-> UnderScope n f (LocScope l n f b) b
-> Located l (UnderScope n f (LocScope l n f b) b)
forall l a. l -> a -> Located l a
Located (l
l1 l -> l -> l
forall a. Semigroup a => a -> a -> a
<> l
l2) UnderScope n f (LocScope l n f b) b
b))) Colocated l l
forall l. Colocated l l
askColocated

instance (Monoid l, Functor f) => MonadWriter l (LocScope l n f) where
  writer :: (a, l) -> LocScope l n f a
writer (a :: a
a, l :: l
l) = l -> a -> LocScope l n f a
forall l a n (f :: * -> *). l -> a -> LocScope l n f a
LocScopeFree l
l a
a
  tell :: l -> LocScope l n f ()
tell l :: l
l = l -> () -> LocScope l n f ()
forall l a n (f :: * -> *). l -> a -> LocScope l n f a
LocScopeFree l
l ()
  listen :: LocScope l n f a -> LocScope l n f (a, l)
listen = (Located l a -> Located l (a, l))
-> LocScope l n f a -> LocScope l n f (a, l)
forall (f :: * -> *) l a b n.
Functor f =>
(Located l a -> Located l b)
-> LocScope l n f a -> LocScope l n f b
locScopeMapAnno (\(Located l :: l
l a :: a
a) -> l -> (a, l) -> Located l (a, l)
forall l a. l -> a -> Located l a
Located l
l (a
a, l
l))
  pass :: LocScope l n f (a, l -> l) -> LocScope l n f a
pass = (Located l (a, l -> l) -> Located l a)
-> LocScope l n f (a, l -> l) -> LocScope l n f a
forall (f :: * -> *) l a b n.
Functor f =>
(Located l a -> Located l b)
-> LocScope l n f a -> LocScope l n f b
locScopeMapAnno (\(Located l :: l
l (a :: a
a, f :: l -> l
f)) -> l -> a -> Located l a
forall l a. l -> a -> Located l a
Located (l -> l
f l
l) a
a)

instance (Eq (f (LocScope l n f a)), Eq l, Eq n, Eq a) => Eq (LocScope l n f a) where
  LocScope su :: ScopeW (Located l) n f (LocScope l n f) a
su == :: LocScope l n f a -> LocScope l n f a -> Bool
== LocScope sv :: ScopeW (Located l) n f (LocScope l n f) a
sv = ScopeW (Located l) n f (LocScope l n f) a
su ScopeW (Located l) n f (LocScope l n f) a
-> ScopeW (Located l) n f (LocScope l n f) a -> Bool
forall a. Eq a => a -> a -> Bool
== ScopeW (Located l) n f (LocScope l n f) a
sv

instance (Show (f (LocScope l n f a)), Show l, Show n, Show a) => Show (LocScope l n f a) where
  showsPrec :: Int -> LocScope l n f a -> ShowS
showsPrec d :: Int
d (LocScope (ScopeW tu :: Located l (UnderScope n f (LocScope l n f a) a)
tu)) = String -> ShowS
showString "LocScope " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Located l (UnderScope n f (LocScope l 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) Located l (UnderScope n f (LocScope l n f a) a)
tu

-- * Interface

locScopeFree :: Functor f => a -> Colocated l (LocScope l n f a)
locScopeFree :: a -> Colocated l (LocScope l n f a)
locScopeFree = a -> Colocated l (LocScope l n f a)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
a -> u (g a)
scopeWFree
{-# INLINE locScopeFree #-}

locScopeEmbed :: Functor f => f (LocScope l n f a) -> Colocated l (LocScope l n f a)
locScopeEmbed :: f (LocScope l n f a) -> Colocated l (LocScope l n f a)
locScopeEmbed = f (LocScope l n f a) -> Colocated l (LocScope l n f a)
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
f (g a) -> u (g a)
scopeWEmbed
{-# INLINE locScopeEmbed #-}

locScopeFromInnerBinder :: Functor f => BinderScope n (LocScope l n f a) -> Colocated l (LocScope l n f a)
locScopeFromInnerBinder :: BinderScope n (LocScope l n f a) -> Colocated l (LocScope l n f a)
locScopeFromInnerBinder = BinderScope n (LocScope l n f a) -> Colocated l (LocScope l 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 locScopeFromInnerBinder #-}

locScopeBind :: Functor f => (a -> Colocated l (LocScope l n f b)) -> LocScope l n f a -> LocScope l n f b
locScopeBind :: (a -> Colocated l (LocScope l n f b))
-> LocScope l n f a -> LocScope l n f b
locScopeBind = (a -> Colocated l (LocScope l n f b))
-> LocScope l n f a -> LocScope l 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
{-# INLINE locScopeBind #-}

locScopeBindOpt :: Functor f => (a -> Maybe (Colocated l (LocScope l n f a))) -> LocScope l n f a -> LocScope l n f a
locScopeBindOpt :: (a -> Maybe (Colocated l (LocScope l n f a)))
-> LocScope l n f a -> LocScope l n f a
locScopeBindOpt = (a -> Maybe (Colocated l (LocScope l n f a)))
-> LocScope l n f a -> LocScope l 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
{-# INLINE locScopeBindOpt #-}

locScopeLift :: Traversable f => f a -> Colocated l (LocScope l n f a)
locScopeLift :: f a -> Colocated l (LocScope l n f a)
locScopeLift = f a -> Colocated l (LocScope l 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 locScopeLift #-}

locScopeInnerBinder :: (Functor f, Eq a) => n -> Seq a -> LocScope l n f a -> BinderScope n (LocScope l n f a)
locScopeInnerBinder :: n -> Seq a -> LocScope l n f a -> BinderScope n (LocScope l n f a)
locScopeInnerBinder = n -> Seq a -> LocScope l n f a -> BinderScope n (LocScope l 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 locScopeInnerBinder #-}

locScopeInnerBinder1 :: (Functor f, Eq a) => n -> a -> LocScope l n f a -> BinderScope n (LocScope l n f a)
locScopeInnerBinder1 :: n -> a -> LocScope l n f a -> BinderScope n (LocScope l n f a)
locScopeInnerBinder1 = n -> a -> LocScope l n f a -> BinderScope n (LocScope l 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 locScopeInnerBinder1 #-}

locScopeAbstract :: (Functor f, Eq a) => n -> Seq a -> LocScope l n f a -> Colocated l (LocScope l n f a)
locScopeAbstract :: n -> Seq a -> LocScope l n f a -> Colocated l (LocScope l n f a)
locScopeAbstract = n -> Seq a -> LocScope l n f a -> Colocated l (LocScope l 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
{-# INLINE locScopeAbstract #-}

locScopeAbstract1 :: (Functor f, Eq a) => n -> a -> LocScope l n f a -> Colocated l (LocScope l n f a)
locScopeAbstract1 :: n -> a -> LocScope l n f a -> Colocated l (LocScope l n f a)
locScopeAbstract1 = n -> a -> LocScope l n f a -> Colocated l (LocScope l 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
{-# INLINE locScopeAbstract1 #-}

locScopeUnAbstract :: Functor f => Seq a -> LocScope l n f a -> LocScope l n f a
locScopeUnAbstract :: Seq a -> LocScope l n f a -> LocScope l n f a
locScopeUnAbstract = Seq a -> LocScope l n f a -> LocScope l n f a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
Seq a -> g a -> g a
scopeWUnAbstract
{-# INLINE locScopeUnAbstract #-}

locScopeUnAbstract1 :: Functor f => a -> LocScope l n f a -> LocScope l n f a
locScopeUnAbstract1 :: a -> LocScope l n f a -> LocScope l n f a
locScopeUnAbstract1 = a -> LocScope l n f a -> LocScope l n f a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
a -> g a -> g a
scopeWUnAbstract1
{-# INLINE locScopeUnAbstract1 #-}

locScopeInstantiate :: Functor f => Seq (Colocated l (LocScope l n f a)) -> LocScope l n f a -> LocScope l n f a
locScopeInstantiate :: Seq (Colocated l (LocScope l n f a))
-> LocScope l n f a -> LocScope l n f a
locScopeInstantiate = Seq (Colocated l (LocScope l n f a))
-> LocScope l n f a -> LocScope l 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
{-# INLINE locScopeInstantiate #-}

locScopeInstantiate1 :: Functor f => Colocated l (LocScope l n f a) -> LocScope l n f a -> LocScope l n f a
locScopeInstantiate1 :: Colocated l (LocScope l n f a)
-> LocScope l n f a -> LocScope l n f a
locScopeInstantiate1 = Colocated l (LocScope l n f a)
-> LocScope l n f a -> LocScope l n f a
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a.
ScopeWC t u n f g =>
u (g a) -> g a -> g a
scopeWInstantiate1
{-# INLINE locScopeInstantiate1 #-}

locScopeApply :: Functor f => Seq (Colocated l (LocScope l n f a)) -> LocScope l n f a -> Either SubError (LocScope l n f a)
locScopeApply :: Seq (Colocated l (LocScope l n f a))
-> LocScope l n f a -> Either SubError (LocScope l n f a)
locScopeApply = Seq (Colocated l (LocScope l n f a))
-> LocScope l n f a -> Either SubError (LocScope l 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
{-# INLINE locScopeApply #-}

locScopeApply1 :: Functor f => Colocated l (LocScope l n f a) -> LocScope l n f a -> Either SubError (LocScope l n f a)
locScopeApply1 :: Colocated l (LocScope l n f a)
-> LocScope l n f a -> Either SubError (LocScope l n f a)
locScopeApply1 = Colocated l (LocScope l n f a)
-> LocScope l n f a -> Either SubError (LocScope l 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
{-# INLINE locScopeApply1 #-}

locScopeLiftAnno :: Located l a -> LocScope l n f a
locScopeLiftAnno :: Located l a -> LocScope l n f a
locScopeLiftAnno = Located l a -> LocScope l n f a
forall (t :: * -> *) n (f :: * -> *) (g :: * -> *) a.
(NatNewtype (ScopeW t n f g) g, Functor t) =>
t a -> g a
scopeWLiftAnno
{-# INLINE locScopeLiftAnno #-}

-- Need an explicit type sig and forall to use this in the hoist below
mapLocatedForall :: (l -> x) -> (forall z. Located l z -> Located x z)
mapLocatedForall :: (l -> x) -> forall z. Located l z -> Located x z
mapLocatedForall f :: l -> x
f (Located l :: l
l z :: z
z) = x -> z -> Located x z
forall l a. l -> a -> Located l a
Located (l -> x
f l
l) z
z

locScopeHoistAnno :: Functor f => (l -> x) -> LocScope l n f a -> LocScope x n f a
locScopeHoistAnno :: (l -> x) -> LocScope l n f a -> LocScope x n f a
locScopeHoistAnno f :: l -> x
f = (forall x. Located l x -> Located x x)
-> LocScope l n f a -> LocScope x n f 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 ((l -> x) -> forall x. Located l x -> Located x x
forall l x. (l -> x) -> forall z. Located l z -> Located x z
mapLocatedForall l -> x
f)
{-# INLINE locScopeHoistAnno #-}

locScopeMapAnno :: Functor f => (Located l a -> Located l b) -> LocScope l n f a -> LocScope l n f b
locScopeMapAnno :: (Located l a -> Located l b)
-> LocScope l n f a -> LocScope l n f b
locScopeMapAnno = (Located l a -> Located l b)
-> LocScope l n f a -> LocScope l n f b
forall (t :: * -> *) (u :: * -> *) n (f :: * -> *) (g :: * -> *) a
       b.
ScopeWC t u n f g =>
(t a -> t b) -> g a -> g b
scopeWMapAnno
{-# INLINE locScopeMapAnno #-}