{-# LANGUAGE DeriveAnyClass #-}

-- | Internals.
module Blanks.Under
  ( UnderScope (..)
  , pattern UnderScopeBound
  , pattern UnderScopeFree
  , pattern UnderScopeBinder
  , pattern UnderScopeEmbed
  , underScopeShift
  ) where

import Blanks.Core (BinderScope (..), BoundScope (..), EmbedScope (..), FreeScope (..))
import Control.DeepSeq (NFData)
import Data.Bifoldable (Bifoldable (..))
import Data.Bifunctor (Bifunctor (..))
import Data.Bitraversable (Bitraversable (..))
import GHC.Generics (Generic)

data UnderScope n f e a
  = UnderBoundScope !BoundScope
  | UnderFreeScope !(FreeScope a)
  | UnderBinderScope !(BinderScope n e)
  | UnderEmbedScope !(EmbedScope f e)
  deriving stock (UnderScope n f e a -> UnderScope n f e a -> Bool
(UnderScope n f e a -> UnderScope n f e a -> Bool)
-> (UnderScope n f e a -> UnderScope n f e a -> Bool)
-> Eq (UnderScope n f e a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall n (f :: * -> *) e a.
(Eq a, Eq n, Eq e, Eq (f e)) =>
UnderScope n f e a -> UnderScope n f e a -> Bool
/= :: UnderScope n f e a -> UnderScope n f e a -> Bool
$c/= :: forall n (f :: * -> *) e a.
(Eq a, Eq n, Eq e, Eq (f e)) =>
UnderScope n f e a -> UnderScope n f e a -> Bool
== :: UnderScope n f e a -> UnderScope n f e a -> Bool
$c== :: forall n (f :: * -> *) e a.
(Eq a, Eq n, Eq e, Eq (f e)) =>
UnderScope n f e a -> UnderScope n f e a -> Bool
Eq, Int -> UnderScope n f e a -> ShowS
[UnderScope n f e a] -> ShowS
UnderScope n f e a -> String
(Int -> UnderScope n f e a -> ShowS)
-> (UnderScope n f e a -> String)
-> ([UnderScope n f e a] -> ShowS)
-> Show (UnderScope n f e a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall n (f :: * -> *) e a.
(Show a, Show n, Show e, Show (f e)) =>
Int -> UnderScope n f e a -> ShowS
forall n (f :: * -> *) e a.
(Show a, Show n, Show e, Show (f e)) =>
[UnderScope n f e a] -> ShowS
forall n (f :: * -> *) e a.
(Show a, Show n, Show e, Show (f e)) =>
UnderScope n f e a -> String
showList :: [UnderScope n f e a] -> ShowS
$cshowList :: forall n (f :: * -> *) e a.
(Show a, Show n, Show e, Show (f e)) =>
[UnderScope n f e a] -> ShowS
show :: UnderScope n f e a -> String
$cshow :: forall n (f :: * -> *) e a.
(Show a, Show n, Show e, Show (f e)) =>
UnderScope n f e a -> String
showsPrec :: Int -> UnderScope n f e a -> ShowS
$cshowsPrec :: forall n (f :: * -> *) e a.
(Show a, Show n, Show e, Show (f e)) =>
Int -> UnderScope n f e a -> ShowS
Show, a -> UnderScope n f e b -> UnderScope n f e a
(a -> b) -> UnderScope n f e a -> UnderScope n f e b
(forall a b. (a -> b) -> UnderScope n f e a -> UnderScope n f e b)
-> (forall a b. a -> UnderScope n f e b -> UnderScope n f e a)
-> Functor (UnderScope n f e)
forall a b. a -> UnderScope n f e b -> UnderScope n f e a
forall a b. (a -> b) -> UnderScope n f e a -> UnderScope n f e b
forall n (f :: * -> *) e a b.
a -> UnderScope n f e b -> UnderScope n f e a
forall n (f :: * -> *) e a b.
(a -> b) -> UnderScope n f e a -> UnderScope n f e b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> UnderScope n f e b -> UnderScope n f e a
$c<$ :: forall n (f :: * -> *) e a b.
a -> UnderScope n f e b -> UnderScope n f e a
fmap :: (a -> b) -> UnderScope n f e a -> UnderScope n f e b
$cfmap :: forall n (f :: * -> *) e a b.
(a -> b) -> UnderScope n f e a -> UnderScope n f e b
Functor, (forall x. UnderScope n f e a -> Rep (UnderScope n f e a) x)
-> (forall x. Rep (UnderScope n f e a) x -> UnderScope n f e a)
-> Generic (UnderScope n f e a)
forall x. Rep (UnderScope n f e a) x -> UnderScope n f e a
forall x. UnderScope n f e a -> Rep (UnderScope n f e a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall n (f :: * -> *) e a x.
Rep (UnderScope n f e a) x -> UnderScope n f e a
forall n (f :: * -> *) e a x.
UnderScope n f e a -> Rep (UnderScope n f e a) x
$cto :: forall n (f :: * -> *) e a x.
Rep (UnderScope n f e a) x -> UnderScope n f e a
$cfrom :: forall n (f :: * -> *) e a x.
UnderScope n f e a -> Rep (UnderScope n f e a) x
Generic)
  deriving anyclass (UnderScope n f e a -> ()
(UnderScope n f e a -> ()) -> NFData (UnderScope n f e a)
forall a. (a -> ()) -> NFData a
forall n (f :: * -> *) e a.
(NFData a, NFData n, NFData e, NFData (f e)) =>
UnderScope n f e a -> ()
rnf :: UnderScope n f e a -> ()
$crnf :: forall n (f :: * -> *) e a.
(NFData a, NFData n, NFData e, NFData (f e)) =>
UnderScope n f e a -> ()
NFData)

pattern UnderScopeBound :: Int -> UnderScope n f e a
pattern $bUnderScopeBound :: Int -> UnderScope n f e a
$mUnderScopeBound :: forall r n (f :: * -> *) e a.
UnderScope n f e a -> (Int -> r) -> (Void# -> r) -> r
UnderScopeBound i = UnderBoundScope (BoundScope i)

pattern UnderScopeFree :: a -> UnderScope n f e a
pattern $bUnderScopeFree :: a -> UnderScope n f e a
$mUnderScopeFree :: forall r a n (f :: * -> *) e.
UnderScope n f e a -> (a -> r) -> (Void# -> r) -> r
UnderScopeFree a = UnderFreeScope (FreeScope a)

pattern UnderScopeBinder :: Int -> n -> e -> UnderScope n f e a
pattern $bUnderScopeBinder :: Int -> n -> e -> UnderScope n f e a
$mUnderScopeBinder :: forall r n e (f :: * -> *) a.
UnderScope n f e a -> (Int -> n -> e -> r) -> (Void# -> r) -> r
UnderScopeBinder i n e = UnderBinderScope (BinderScope i n e)

pattern UnderScopeEmbed :: f e -> UnderScope n f e a
pattern $bUnderScopeEmbed :: f e -> UnderScope n f e a
$mUnderScopeEmbed :: forall r (f :: * -> *) e n a.
UnderScope n f e a -> (f e -> r) -> (Void# -> r) -> r
UnderScopeEmbed fe = UnderEmbedScope (EmbedScope fe)

{-# COMPLETE UnderScopeBound, UnderScopeFree, UnderScopeBinder, UnderScopeEmbed #-}

instance Functor f => Bifunctor (UnderScope n f) where
  bimap :: (a -> b) -> (c -> d) -> UnderScope n f a c -> UnderScope n f b d
bimap _ _ (UnderBoundScope (BoundScope b :: Int
b)) = BoundScope -> UnderScope n f b d
forall n (f :: * -> *) e a. BoundScope -> UnderScope n f e a
UnderBoundScope (Int -> BoundScope
BoundScope Int
b)
  bimap _ g :: c -> d
g (UnderFreeScope (FreeScope a :: c
a)) = FreeScope d -> UnderScope n f b d
forall n (f :: * -> *) e a. FreeScope a -> UnderScope n f e a
UnderFreeScope (d -> FreeScope d
forall a. a -> FreeScope a
FreeScope (c -> d
g c
a))
  bimap f :: a -> b
f _ (UnderBinderScope (BinderScope i :: Int
i x :: n
x e :: a
e)) = BinderScope n b -> UnderScope n f b d
forall n (f :: * -> *) e a. BinderScope n e -> UnderScope n f e a
UnderBinderScope (Int -> n -> b -> BinderScope n b
forall n e. Int -> n -> e -> BinderScope n e
BinderScope Int
i n
x (a -> b
f a
e))
  bimap f :: a -> b
f _ (UnderEmbedScope (EmbedScope fe :: f a
fe)) = EmbedScope f b -> UnderScope n f b d
forall n (f :: * -> *) e a. EmbedScope f e -> UnderScope n f e a
UnderEmbedScope (f b -> EmbedScope f b
forall (f :: * -> *) e. f e -> EmbedScope f e
EmbedScope ((a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f f a
fe))

instance Foldable f => Bifoldable (UnderScope n f) where
  bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> UnderScope n f a b -> c
bifoldr _ _ z :: c
z (UnderBoundScope _) = c
z
  bifoldr _ g :: b -> c -> c
g z :: c
z (UnderFreeScope (FreeScope a :: b
a)) = b -> c -> c
g b
a c
z
  bifoldr f :: a -> c -> c
f _ z :: c
z (UnderBinderScope (BinderScope _ _ e :: a
e)) = a -> c -> c
f a
e c
z
  bifoldr f :: a -> c -> c
f _ z :: c
z (UnderEmbedScope (EmbedScope fe :: f a
fe)) = (a -> c -> c) -> c -> f a -> c
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> c -> c
f c
z f a
fe

instance Traversable f => Bitraversable (UnderScope n f) where
  bitraverse :: (a -> f c)
-> (b -> f d) -> UnderScope n f a b -> f (UnderScope n f c d)
bitraverse _ _ (UnderBoundScope (BoundScope b :: Int
b)) = UnderScope n f c d -> f (UnderScope n f c d)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BoundScope -> UnderScope n f c d
forall n (f :: * -> *) e a. BoundScope -> UnderScope n f e a
UnderBoundScope (Int -> BoundScope
BoundScope Int
b))
  bitraverse _ g :: b -> f d
g (UnderFreeScope (FreeScope a :: b
a)) = (d -> UnderScope n f c d) -> f d -> f (UnderScope n f c d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (FreeScope d -> UnderScope n f c d
forall n (f :: * -> *) e a. FreeScope a -> UnderScope n f e a
UnderFreeScope (FreeScope d -> UnderScope n f c d)
-> (d -> FreeScope d) -> d -> UnderScope n f c d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. d -> FreeScope d
forall a. a -> FreeScope a
FreeScope) (b -> f d
g b
a)
  bitraverse f :: a -> f c
f _ (UnderBinderScope (BinderScope i :: Int
i x :: n
x e :: a
e)) = (c -> UnderScope n f c d) -> f c -> f (UnderScope n f c d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (BinderScope n c -> UnderScope n f c d
forall n (f :: * -> *) e a. BinderScope n e -> UnderScope n f e a
UnderBinderScope (BinderScope n c -> UnderScope n f c d)
-> (c -> BinderScope n c) -> c -> UnderScope n f c d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> n -> c -> BinderScope n c
forall n e. Int -> n -> e -> BinderScope n e
BinderScope Int
i n
x) (a -> f c
f a
e)
  bitraverse f :: a -> f c
f _ (UnderEmbedScope (EmbedScope fe :: f a
fe)) = (f c -> UnderScope n f c d) -> f (f c) -> f (UnderScope n f c d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (EmbedScope f c -> UnderScope n f c d
forall n (f :: * -> *) e a. EmbedScope f e -> UnderScope n f e a
UnderEmbedScope (EmbedScope f c -> UnderScope n f c d)
-> (f c -> EmbedScope f c) -> f c -> UnderScope n f c d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f c -> EmbedScope f c
forall (f :: * -> *) e. f e -> EmbedScope f e
EmbedScope) ((a -> f c) -> f a -> f (f c)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f c
f f a
fe)

underScopeShift :: Functor f => (Int -> Int -> e -> e) -> Int -> Int -> UnderScope n f e a -> UnderScope n f e a
underScopeShift :: (Int -> Int -> e -> e)
-> Int -> Int -> UnderScope n f e a -> UnderScope n f e a
underScopeShift recShift :: Int -> Int -> e -> e
recShift c :: Int
c d :: Int
d us :: UnderScope n f e a
us =
  case UnderScope n f e a
us of
    UnderBoundScope (BoundScope b :: Int
b) ->
      if Int
b Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
c
        then UnderScope n f e a
us
        else BoundScope -> UnderScope n f e a
forall n (f :: * -> *) e a. BoundScope -> UnderScope n f e a
UnderBoundScope (Int -> BoundScope
BoundScope (Int
b Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
d))
    UnderFreeScope _ -> UnderScope n f e a
us
    UnderBinderScope (BinderScope i :: Int
i x :: n
x e :: e
e) -> BinderScope n e -> UnderScope n f e a
forall n (f :: * -> *) e a. BinderScope n e -> UnderScope n f e a
UnderBinderScope (Int -> n -> e -> BinderScope n e
forall n e. Int -> n -> e -> BinderScope n e
BinderScope Int
i n
x (Int -> Int -> e -> e
recShift (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i) Int
d e
e))
    UnderEmbedScope (EmbedScope fe :: f e
fe) -> EmbedScope f e -> UnderScope n f e a
forall n (f :: * -> *) e a. EmbedScope f e -> UnderScope n f e a
UnderEmbedScope (f e -> EmbedScope f e
forall (f :: * -> *) e. f e -> EmbedScope f e
EmbedScope ((e -> e) -> f e -> f e
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Int -> e -> e
recShift Int
c Int
d) f e
fe))