{-# LANGUAGE CPP                   #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE UndecidableInstances  #-}
-- | 'ScopeH' scope, which allows substitute 'f' into 'g' to get new 'g'.
--
-- Compare following signatures:
--
-- @
-- 'instantiate1'  :: ... => m a -> 'Scope'  b   m a -> m a
-- 'instantiate1H' :: ... => m a -> 'ScopeH' b f m a -> f a
-- @
--
-- 'ScopeH' variant allows to encode e.g. Hindley-Milner types, where
-- we diffentiate between @Poly@ and @Mono@-morphic types.
--
-- @
-- specialise :: Poly a -> Mono a -> Poly a
-- specialise (Forall p) m = 'instantiate1H' m p
-- specialise _          _ = error "ill-kinded"
-- @
--
-- Another applications are /bidirectional/ type-systems or representing
-- normal forms with /normal/ and  /neutral/ terms,
-- aka /introduction/ and /elimination/ terms.
--
-- Look into @examples/@ directory for /System F/ and /Bidirectional STLC/
-- implemented with a help of 'ScopeH'.
--
module Bound.ScopeH (
    ScopeH (..),
    -- * Abstraction
    abstractH, abstract1H, abstractHEither,
    -- ** Name
    abstractHName, abstract1HName,
    -- * Instantiation
    instantiateH, instantiate1H, instantiateHEither,
    -- * Lifting
    liftScopeH,
    -- * Traditional de Bruijn
    fromScopeH,
    toScopeH,
    -- * Bound variable manipulation
    lowerScopeH,
    convertFromScope,
    splatH,
    bindingsH,
    mapBoundH,
    mapScopeH,
    foldMapBoundH,
    foldMapScopeH,
    traverseBoundH_,
    traverseScopeH_,
    traverseBoundH,
    traverseScopeH,
    bitraverseScopeH,
    bitransverseScopeH,
    ) where

import Bound                (Scope (..), Var (..))
import Bound.Name           (Name (..))
import Control.DeepSeq      (NFData (..))
import Control.Monad.Module (Module (..), LiftedModule (..))
import Data.Bifoldable      (bifoldMap, bitraverse_)
import Data.Bifunctor       (bimap)
import Data.Bitraversable   (Bitraversable (..))
import Data.Foldable        (traverse_)
import Data.Functor.Classes
import Data.Hashable        (Hashable (..))
import Data.Hashable.Lifted (Hashable1 (..), hashWithSalt1)

-- | @'ScopeH' b f m a@ is a @f@ expression abstracted over @g@,
-- with bound variables in @b@, and free variables in @a@.
--
-- @
-- 'Scope' b f a ~ 'ScopeH' n f f a
-- 'ScopeT' b t f a ~ 'ScopeH' b (t f) f a
-- @
--
newtype ScopeH b f m a = ScopeH { ScopeH b f m a -> f (Var b (m a))
unscopeH :: f (Var b (m a)) }

instance (Functor f, Monad m) => Module (ScopeH b f m) m where
    ScopeH f (Var b (m a))
s >>== :: ScopeH b f m a -> (a -> m b) -> ScopeH b f m b
>>== a -> m b
k = f (Var b (m b)) -> ScopeH b f m b
forall b (f :: * -> *) (m :: * -> *) a.
f (Var b (m a)) -> ScopeH b f m a
ScopeH (f (Var b (m b)) -> ScopeH b f m b)
-> f (Var b (m b)) -> ScopeH b f m b
forall a b. (a -> b) -> a -> b
$ (Var b (m a) -> Var b (m b)) -> f (Var b (m a)) -> f (Var b (m b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((m a -> m b) -> Var b (m a) -> Var b (m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> m b
k)) f (Var b (m a))
s

instance LiftedModule f m => LiftedModule (ScopeH b f m) m where
    mlift :: m a -> ScopeH b f m a
mlift = m a -> ScopeH b f m a
forall (f :: * -> *) (m :: * -> *) a b.
LiftedModule f m =>
m a -> ScopeH b f m a
liftScopeH

-------------------------------------------------------------------------------
-- Instances
-------------------------------------------------------------------------------

instance (Functor f, Functor m) => Functor (ScopeH b f m) where
   fmap :: (a -> b) -> ScopeH b f m a -> ScopeH b f m b
fmap a -> b
f (ScopeH f (Var b (m a))
a) = f (Var b (m b)) -> ScopeH b f m b
forall b (f :: * -> *) (m :: * -> *) a.
f (Var b (m a)) -> ScopeH b f m a
ScopeH (f (Var b (m b)) -> ScopeH b f m b)
-> f (Var b (m b)) -> ScopeH b f m b
forall a b. (a -> b) -> a -> b
$ (Var b (m a) -> Var b (m b)) -> f (Var b (m a)) -> f (Var b (m b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((m a -> m b) -> Var b (m a) -> Var b (m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f)) f (Var b (m a))
a

instance (Foldable f, Foldable m) => Foldable (ScopeH b f m) where
    foldMap :: (a -> m) -> ScopeH b f m a -> m
foldMap a -> m
f (ScopeH f (Var b (m a))
a) = (Var b (m a) -> m) -> f (Var b (m a)) -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((m a -> m) -> Var b (m a) -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((a -> m) -> m a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f)) f (Var b (m a))
a
    foldr :: (a -> b -> b) -> b -> ScopeH b f m a -> b
foldr a -> b -> b
f b
z (ScopeH f (Var b (m a))
a) = (Var b (m a) -> b -> b) -> b -> f (Var b (m a)) -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((b -> Var b (m a) -> b) -> Var b (m a) -> b -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((m a -> b -> b) -> b -> Var b (m a) -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((b -> m a -> b) -> m a -> b -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((a -> b -> b) -> b -> m a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> b -> b
f))))  b
z f (Var b (m a))
a

instance (Traversable f, Traversable m) => Traversable (ScopeH b f m) where
    traverse :: (a -> f b) -> ScopeH b f m a -> f (ScopeH b f m b)
traverse a -> f b
f (ScopeH f (Var b (m a))
a) = f (Var b (m b)) -> ScopeH b f m b
forall b (f :: * -> *) (m :: * -> *) a.
f (Var b (m a)) -> ScopeH b f m a
ScopeH (f (Var b (m b)) -> ScopeH b f m b)
-> f (f (Var b (m b))) -> f (ScopeH b f m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var b (m a) -> f (Var b (m b)))
-> f (Var b (m a)) -> f (f (Var b (m b)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((m a -> f (m b)) -> Var b (m a) -> f (Var b (m b))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((a -> f b) -> m a -> f (m b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f)) f (Var b (m a))
a

instance (Hashable b, Module f m, Hashable1 f, Hashable1 m) => Hashable1 (ScopeH b f m) where
    liftHashWithSalt :: (Int -> a -> Int) -> Int -> ScopeH b f m a -> Int
liftHashWithSalt Int -> a -> Int
h Int
s ScopeH b f m a
m = (Int -> Var b a -> Int) -> Int -> f (Var b a) -> Int
forall (t :: * -> *) a.
Hashable1 t =>
(Int -> a -> Int) -> Int -> t a -> Int
liftHashWithSalt ((Int -> a -> Int) -> Int -> Var b a -> Int
forall (t :: * -> *) a.
Hashable1 t =>
(Int -> a -> Int) -> Int -> t a -> Int
liftHashWithSalt Int -> a -> Int
h) Int
s (ScopeH b f m a -> f (Var b a)
forall (f :: * -> *) (m :: * -> *) b a.
Module f m =>
ScopeH b f m a -> f (Var b a)
fromScopeH ScopeH b f m a
m)
    {-# INLINE liftHashWithSalt #-}

instance (Hashable b, Module f m, Hashable1 f, Hashable1 m, Hashable a) => Hashable (ScopeH b f m a) where
    hashWithSalt :: Int -> ScopeH b f m a -> Int
hashWithSalt Int
n ScopeH b f m a
m = Int -> f (Var b a) -> Int
forall (f :: * -> *) a.
(Hashable1 f, Hashable a) =>
Int -> f a -> Int
hashWithSalt1 Int
n (ScopeH b f m a -> f (Var b a)
forall (f :: * -> *) (m :: * -> *) b a.
Module f m =>
ScopeH b f m a -> f (Var b a)
fromScopeH ScopeH b f m a
m)
    {-# INLINE hashWithSalt #-}

instance NFData (f (Var b (m a))) => NFData (ScopeH b f m a) where
  rnf :: ScopeH b f m a -> ()
rnf ScopeH b f m a
scope = f (Var b (m a)) -> ()
forall a. NFData a => a -> ()
rnf (ScopeH b f m a -> f (Var b (m a))
forall b (f :: * -> *) (m :: * -> *) a.
ScopeH b f m a -> f (Var b (m a))
unscopeH ScopeH b f m a
scope)

instance (Module f m, Eq b, Eq1 f, Eq1 m, Eq a) => Eq  (ScopeH b f m a) where == :: ScopeH b f m a -> ScopeH b f m a -> Bool
(==) = ScopeH b f m a -> ScopeH b f m a -> Bool
forall (f :: * -> *) a. (Eq1 f, Eq a) => f a -> f a -> Bool
eq1
instance (Module f m, Ord b, Ord1 f, Ord1 m, Ord a) => Ord  (ScopeH b f m a) where compare :: ScopeH b f m a -> ScopeH b f m a -> Ordering
compare = ScopeH b f m a -> ScopeH b f m a -> Ordering
forall (f :: * -> *) a. (Ord1 f, Ord a) => f a -> f a -> Ordering
compare1
instance (Show b, Show1 f, Show1 m, Show a) => Show (ScopeH b f m a) where showsPrec :: Int -> ScopeH b f m a -> ShowS
showsPrec = Int -> ScopeH b f m a -> ShowS
forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1
instance (Read b, Read1 f, Read1 m, Read a) => Read (ScopeH b f m a) where readsPrec :: Int -> ReadS (ScopeH b f m a)
readsPrec = Int -> ReadS (ScopeH b f m a)
forall (f :: * -> *) a. (Read1 f, Read a) => Int -> ReadS (f a)
readsPrec1

-------------------------------------------------------------------------------
-- * transformers 0.5 Data.Functor.Classes
-------------------------------------------------------------------------------

instance (Module f m, Eq b, Eq1 f, Eq1 m) => Eq1 (ScopeH b f m) where
  liftEq :: (a -> b -> Bool) -> ScopeH b f m a -> ScopeH b f m b -> Bool
liftEq a -> b -> Bool
f ScopeH b f m a
m ScopeH b f m b
n = (Var b a -> Var b b -> Bool) -> f (Var b a) -> f (Var b b) -> Bool
forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq ((a -> b -> Bool) -> Var b a -> Var b b -> Bool
forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
f) (ScopeH b f m a -> f (Var b a)
forall (f :: * -> *) (m :: * -> *) b a.
Module f m =>
ScopeH b f m a -> f (Var b a)
fromScopeH ScopeH b f m a
m) (ScopeH b f m b -> f (Var b b)
forall (f :: * -> *) (m :: * -> *) b a.
Module f m =>
ScopeH b f m a -> f (Var b a)
fromScopeH ScopeH b f m b
n)

instance (Module f m, Ord b, Ord1 f, Ord1 m) => Ord1 (ScopeH b f m) where
  liftCompare :: (a -> b -> Ordering)
-> ScopeH b f m a -> ScopeH b f m b -> Ordering
liftCompare a -> b -> Ordering
f ScopeH b f m a
m ScopeH b f m b
n = (Var b a -> Var b b -> Ordering)
-> f (Var b a) -> f (Var b b) -> Ordering
forall (f :: * -> *) a b.
Ord1 f =>
(a -> b -> Ordering) -> f a -> f b -> Ordering
liftCompare ((a -> b -> Ordering) -> Var b a -> Var b b -> Ordering
forall (f :: * -> *) a b.
Ord1 f =>
(a -> b -> Ordering) -> f a -> f b -> Ordering
liftCompare a -> b -> Ordering
f) (ScopeH b f m a -> f (Var b a)
forall (f :: * -> *) (m :: * -> *) b a.
Module f m =>
ScopeH b f m a -> f (Var b a)
fromScopeH ScopeH b f m a
m) (ScopeH b f m b -> f (Var b b)
forall (f :: * -> *) (m :: * -> *) b a.
Module f m =>
ScopeH b f m a -> f (Var b a)
fromScopeH ScopeH b f m b
n)

instance (Show b, Show1 f, Show1 m) => Show1 (ScopeH b f m) where
    liftShowsPrec :: (Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> ScopeH b f m a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl Int
d (ScopeH f (Var b (m a))
x) = (Int -> f (Var b (m a)) -> ShowS)
-> String -> Int -> f (Var b (m a)) -> ShowS
forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith
        ((Int -> Var b (m a) -> ShowS)
-> ([Var b (m a)] -> ShowS) -> Int -> f (Var b (m a)) -> ShowS
forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
liftShowsPrec ((Int -> m a -> ShowS)
-> ([m a] -> ShowS) -> Int -> Var b (m a) -> ShowS
forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
liftShowsPrec Int -> m a -> ShowS
sp' [m a] -> ShowS
sl') ((Int -> m a -> ShowS) -> ([m a] -> ShowS) -> [Var b (m a)] -> ShowS
forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [f a] -> ShowS
liftShowList Int -> m a -> ShowS
sp' [m a] -> ShowS
sl'))
        String
"ScopeH" Int
d f (Var b (m a))
x
      where
        sp' :: Int -> m a -> ShowS
sp' = (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> m a -> ShowS
forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl
        sl' :: [m a] -> ShowS
sl' = (Int -> a -> ShowS) -> ([a] -> ShowS) -> [m a] -> ShowS
forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [f a] -> ShowS
liftShowList Int -> a -> ShowS
sp [a] -> ShowS
sl

instance (Read b, Read1 f, Read1 m) => Read1 (ScopeH b f m) where
    liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (ScopeH b f m a)
liftReadsPrec Int -> ReadS a
f ReadS [a]
g = (String -> ReadS (ScopeH b f m a)) -> Int -> ReadS (ScopeH b f m a)
forall a. (String -> ReadS a) -> Int -> ReadS a
readsData ((String -> ReadS (ScopeH b f m a))
 -> Int -> ReadS (ScopeH b f m a))
-> (String -> ReadS (ScopeH b f m a))
-> Int
-> ReadS (ScopeH b f m a)
forall a b. (a -> b) -> a -> b
$ (Int -> ReadS (f (Var b (m a))))
-> String
-> (f (Var b (m a)) -> ScopeH b f m a)
-> String
-> ReadS (ScopeH b f m a)
forall a t.
(Int -> ReadS a) -> String -> (a -> t) -> String -> ReadS t
readsUnaryWith
        ((Int -> ReadS (Var b (m a)))
-> ReadS [Var b (m a)] -> Int -> ReadS (f (Var b (m a)))
forall (f :: * -> *) a.
Read1 f =>
(Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (f a)
liftReadsPrec ((Int -> ReadS (m a)) -> ReadS [m a] -> Int -> ReadS (Var b (m a))
forall (f :: * -> *) a.
Read1 f =>
(Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (f a)
liftReadsPrec Int -> ReadS (m a)
f' ReadS [m a]
g') ((Int -> ReadS (m a)) -> ReadS [m a] -> ReadS [Var b (m a)]
forall (f :: * -> *) a.
Read1 f =>
(Int -> ReadS a) -> ReadS [a] -> ReadS [f a]
liftReadList Int -> ReadS (m a)
f' ReadS [m a]
g'))
        String
"ScopeH" f (Var b (m a)) -> ScopeH b f m a
forall b (f :: * -> *) (m :: * -> *) a.
f (Var b (m a)) -> ScopeH b f m a
ScopeH
      where
        f' :: Int -> ReadS (m a)
f' = (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (m a)
forall (f :: * -> *) a.
Read1 f =>
(Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (f a)
liftReadsPrec Int -> ReadS a
f ReadS [a]
g
        g' :: ReadS [m a]
g' = (Int -> ReadS a) -> ReadS [a] -> ReadS [m a]
forall (f :: * -> *) a.
Read1 f =>
(Int -> ReadS a) -> ReadS [a] -> ReadS [f a]
liftReadList Int -> ReadS a
f ReadS [a]
g

-------------------------------------------------------------------------------
-- Abstraction
-------------------------------------------------------------------------------

-- | Capture some free variables in an expression to yield a 'ScopeH' with bound variables in @b@.
abstractH :: (Functor f, Monad m) => (a -> Maybe b) -> f a -> ScopeH b f m a
abstractH :: (a -> Maybe b) -> f a -> ScopeH b f m a
abstractH a -> Maybe b
f f a
e = f (Var b (m a)) -> ScopeH b f m a
forall b (f :: * -> *) (m :: * -> *) a.
f (Var b (m a)) -> ScopeH b f m a
ScopeH ((a -> Var b (m a)) -> f a -> f (Var b (m a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Var b (m a)
forall (m :: * -> *). Monad m => a -> Var b (m a)
k f a
e) where
    k :: a -> Var b (m a)
k a
y = case a -> Maybe b
f a
y of
        Just b
z  -> b -> Var b (m a)
forall b a. b -> Var b a
B b
z
        Maybe b
Nothing -> m a -> Var b (m a)
forall b a. a -> Var b a
F (a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
y)
{-# INLINE abstractH #-}

-- | Abstract over a single variable.
abstract1H :: (Functor f, Monad m, Eq a) => a -> f a -> ScopeH () f m a
abstract1H :: a -> f a -> ScopeH () f m a
abstract1H a
a = (a -> Maybe ()) -> f a -> ScopeH () f m a
forall (f :: * -> *) (m :: * -> *) a b.
(Functor f, Monad m) =>
(a -> Maybe b) -> f a -> ScopeH b f m a
abstractH (\a
b -> if a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b then () -> Maybe ()
forall a. a -> Maybe a
Just () else Maybe ()
forall a. Maybe a
Nothing)
{-# INLINE abstract1H #-}

-- | Capture some free variables in an expression to yield a 'ScopeH' with bound variables in @b@. Optionally change the types of the remaining free variables.
abstractHEither :: (Functor f,  Monad m) => (a -> Either b c) -> f a -> ScopeH b f m c
abstractHEither :: (a -> Either b c) -> f a -> ScopeH b f m c
abstractHEither a -> Either b c
f f a
e = f (Var b (m c)) -> ScopeH b f m c
forall b (f :: * -> *) (m :: * -> *) a.
f (Var b (m a)) -> ScopeH b f m a
ScopeH ((a -> Var b (m c)) -> f a -> f (Var b (m c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Var b (m c)
forall (m :: * -> *). Monad m => a -> Var b (m c)
k f a
e) where
    k :: a -> Var b (m c)
k a
y = case a -> Either b c
f a
y of
        Left b
z -> b -> Var b (m c)
forall b a. b -> Var b a
B b
z
        Right c
y' -> m c -> Var b (m c)
forall b a. a -> Var b a
F (c -> m c
forall (m :: * -> *) a. Monad m => a -> m a
return c
y')
{-# INLINE abstractHEither #-}

-------------------------------------------------------------------------------
-- Abstraction with Name
-------------------------------------------------------------------------------

-- | Abstraction, capturing named bound variables.
abstractHName :: (Functor f, Monad m) => (a -> Maybe b) -> f a -> ScopeH (Name a b) f m a
abstractHName :: (a -> Maybe b) -> f a -> ScopeH (Name a b) f m a
abstractHName a -> Maybe b
f f a
t = f (Var (Name a b) (m a)) -> ScopeH (Name a b) f m a
forall b (f :: * -> *) (m :: * -> *) a.
f (Var b (m a)) -> ScopeH b f m a
ScopeH ((a -> Var (Name a b) (m a)) -> f a -> f (Var (Name a b) (m a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Var (Name a b) (m a)
forall (m :: * -> *). Monad m => a -> Var (Name a b) (m a)
k f a
t) where
    k :: a -> Var (Name a b) (m a)
k a
a = case a -> Maybe b
f a
a of
        Just b
b  -> Name a b -> Var (Name a b) (m a)
forall b a. b -> Var b a
B (a -> b -> Name a b
forall n b. n -> b -> Name n b
Name a
a b
b)
        Maybe b
Nothing -> m a -> Var (Name a b) (m a)
forall b a. a -> Var b a
F (a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a)
{-# INLINE abstractHName #-}

-- | Abstract over a single variable
abstract1HName :: (Functor f, Monad m, Eq a) => a -> f a -> ScopeH (Name a ()) f m a
abstract1HName :: a -> f a -> ScopeH (Name a ()) f m a
abstract1HName a
a = (a -> Maybe ()) -> f a -> ScopeH (Name a ()) f m a
forall (f :: * -> *) (m :: * -> *) a b.
(Functor f, Monad m) =>
(a -> Maybe b) -> f a -> ScopeH (Name a b) f m a
abstractHName (\a
b -> if a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b then () -> Maybe ()
forall a. a -> Maybe a
Just () else Maybe ()
forall a. Maybe a
Nothing)
{-# INLINE abstract1HName #-}

-------------------------------------------------------------------------------
-- Instantiation
-------------------------------------------------------------------------------

-- | Enter a 'ScopeH', instantiating all bound variables
instantiateH :: Module f m => (b -> m a) -> ScopeH b f m a -> f a
instantiateH :: (b -> m a) -> ScopeH b f m a -> f a
instantiateH b -> m a
k (ScopeH f (Var b (m a))
e) = f (Var b (m a))
e f (Var b (m a)) -> (Var b (m a) -> m a) -> f a
forall (f :: * -> *) (m :: * -> *) a b.
Module f m =>
f a -> (a -> m b) -> f b
>>== \Var b (m a)
v -> case Var b (m a)
v of
    B b
b -> b -> m a
k b
b
    F m a
a -> m a
a
{-# INLINE instantiateH #-}

-- | Enter a 'ScopeH' that binds one variable, instantiating it
instantiate1H :: Module f m => m a -> ScopeH b f m a -> f a
instantiate1H :: m a -> ScopeH b f m a -> f a
instantiate1H m a
e = (b -> m a) -> ScopeH b f m a -> f a
forall (f :: * -> *) (m :: * -> *) b a.
Module f m =>
(b -> m a) -> ScopeH b f m a -> f a
instantiateH (m a -> b -> m a
forall a b. a -> b -> a
const m a
e)
{-# INLINE instantiate1H #-}

-- | Enter a 'ScopeH', and instantiate all bound and free variables in one go.
instantiateHEither :: Module f m => (Either b a -> m c) -> ScopeH b f m a -> f c
instantiateHEither :: (Either b a -> m c) -> ScopeH b f m a -> f c
instantiateHEither Either b a -> m c
f (ScopeH f (Var b (m a))
e) = f (Var b (m a))
e f (Var b (m a)) -> (Var b (m a) -> m c) -> f c
forall (f :: * -> *) (m :: * -> *) a b.
Module f m =>
f a -> (a -> m b) -> f b
>>== \Var b (m a)
v -> case Var b (m a)
v of
    B b
b  -> Either b a -> m c
f (b -> Either b a
forall a b. a -> Either a b
Left b
b)
    F m a
ea -> m a
ea m a -> (a -> m c) -> m c
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Either b a -> m c
f (Either b a -> m c) -> (a -> Either b a) -> a -> m c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either b a
forall a b. b -> Either a b
Right
{-# INLINE instantiateHEither #-}

-------------------------------------------------------------------------------
-- Lifting
-------------------------------------------------------------------------------

-- |
--
-- @since 0.0.2
liftScopeH:: forall f m a b. LiftedModule f m => m a -> ScopeH b f m a
liftScopeH :: m a -> ScopeH b f m a
liftScopeH m a
m = f (Var b (m a)) -> ScopeH b f m a
forall b (f :: * -> *) (m :: * -> *) a.
f (Var b (m a)) -> ScopeH b f m a
ScopeH (m (Var b (m a)) -> f (Var b (m a))
forall (f :: * -> *) (m :: * -> *) a.
LiftedModule f m =>
m a -> f a
mlift (Var b (m a) -> m (Var b (m a))
forall (m :: * -> *) a. Monad m => a -> m a
return (m a -> Var b (m a)
forall b a. a -> Var b a
F m a
m) :: m (Var b (m a))))
{-# INLINE liftScopeH #-}

-------------------------------------------------------------------------------
-- Traditional de Bruijn
-------------------------------------------------------------------------------

-- | Convert to traditional de Bruijn.
fromScopeH :: Module f m => ScopeH b f m a -> f (Var b a)
fromScopeH :: ScopeH b f m a -> f (Var b a)
fromScopeH (ScopeH f (Var b (m a))
s) = f (Var b (m a))
s f (Var b (m a)) -> (Var b (m a) -> m (Var b a)) -> f (Var b a)
forall (f :: * -> *) (m :: * -> *) a b.
Module f m =>
f a -> (a -> m b) -> f b
>>== \Var b (m a)
v -> case Var b (m a)
v of
    F m a
e -> (a -> Var b a) -> m a -> m (Var b a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Var b a
forall b a. a -> Var b a
F m a
e
    B b
b -> Var b a -> m (Var b a)
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> Var b a
forall b a. b -> Var b a
B b
b)

-- | Convert from traditional de Bruijn to generalized de Bruijn indices.
toScopeH :: (Functor f, Monad m) => f (Var b a) -> ScopeH b f m a
toScopeH :: f (Var b a) -> ScopeH b f m a
toScopeH f (Var b a)
e = f (Var b (m a)) -> ScopeH b f m a
forall b (f :: * -> *) (m :: * -> *) a.
f (Var b (m a)) -> ScopeH b f m a
ScopeH ((Var b a -> Var b (m a)) -> f (Var b a) -> f (Var b (m a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> m a) -> Var b a -> Var b (m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return) f (Var b a)
e)

-- | Convert to 'Scope'.
lowerScopeH
    :: (Functor f, Functor f)
    => (forall x. f x -> h x)
    -> (forall x. m x -> h x)
    -> ScopeH b f m a -> Scope b h a
lowerScopeH :: (forall x. f x -> h x)
-> (forall x. m x -> h x) -> ScopeH b f m a -> Scope b h a
lowerScopeH forall x. f x -> h x
f forall x. m x -> h x
m (ScopeH f (Var b (m a))
x) = h (Var b (h a)) -> Scope b h a
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope (f (Var b (h a)) -> h (Var b (h a))
forall x. f x -> h x
f ((Var b (m a) -> Var b (h a)) -> f (Var b (m a)) -> f (Var b (h a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((m a -> h a) -> Var b (m a) -> Var b (h a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap m a -> h a
forall x. m x -> h x
m) f (Var b (m a))
x))

convertFromScope :: Scope b f a -> ScopeH b f f a
convertFromScope :: Scope b f a -> ScopeH b f f a
convertFromScope (Scope f (Var b (f a))
x) = f (Var b (f a)) -> ScopeH b f f a
forall b (f :: * -> *) (m :: * -> *) a.
f (Var b (m a)) -> ScopeH b f m a
ScopeH f (Var b (f a))
x

-------------------------------------------------------------------------------
-- Extras
-------------------------------------------------------------------------------

-- | Perform substitution on both bound and free variables in a 'ScopeH'.
splatH :: Module f m => (a -> m c) -> (b -> m c) -> ScopeH b f m a -> f c
splatH :: (a -> m c) -> (b -> m c) -> ScopeH b f m a -> f c
splatH a -> m c
f b -> m c
unbind (ScopeH f (Var b (m a))
e) = f (Var b (m a))
e f (Var b (m a)) -> (Var b (m a) -> m c) -> f c
forall (f :: * -> *) (m :: * -> *) a b.
Module f m =>
f a -> (a -> m b) -> f b
>>== \Var b (m a)
v -> case Var b (m a)
v of
    B b
b -> b -> m c
unbind b
b
    F m a
ea -> m a
ea m a -> (a -> m c) -> m c
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> m c
f
{-# INLINE splatH #-}

-- | Return a list of occurences of the variables bound by this 'ScopeH'.
bindingsH :: Foldable f => ScopeH b f m a -> [b]
bindingsH :: ScopeH b f m a -> [b]
bindingsH (ScopeH f (Var b (m a))
s) = (Var b (m a) -> [b] -> [b]) -> [b] -> f (Var b (m a)) -> [b]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Var b (m a) -> [b] -> [b]
forall a a. Var a a -> [a] -> [a]
f [] f (Var b (m a))
s where
    f :: Var a a -> [a] -> [a]
f (B a
v) [a]
vs = a
v a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
vs
    f Var a a
_ [a]
vs     = [a]
vs
{-# INLINE bindingsH #-}

-- | Perform a change of variables on bound variables.
mapBoundH :: Functor f => (b -> b') -> ScopeH b f m a -> ScopeH b' f m a
mapBoundH :: (b -> b') -> ScopeH b f m a -> ScopeH b' f m a
mapBoundH b -> b'
f (ScopeH f (Var b (m a))
s) = f (Var b' (m a)) -> ScopeH b' f m a
forall b (f :: * -> *) (m :: * -> *) a.
f (Var b (m a)) -> ScopeH b f m a
ScopeH ((Var b (m a) -> Var b' (m a))
-> f (Var b (m a)) -> f (Var b' (m a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Var b (m a) -> Var b' (m a)
forall a. Var b a -> Var b' a
f' f (Var b (m a))
s) where
    f' :: Var b a -> Var b' a
f' (B b
b) = b' -> Var b' a
forall b a. b -> Var b a
B (b -> b'
f b
b)
    f' (F a
a) = a -> Var b' a
forall b a. a -> Var b a
F a
a
{-# INLINE mapBoundH #-}

-- | Perform a change of variables, reassigning both bound and free variables.
mapScopeH
    :: (Functor f, Functor m)
    => (b -> d) -> (a -> c)
    -> ScopeH b f m a -> ScopeH d f m c
mapScopeH :: (b -> d) -> (a -> c) -> ScopeH b f m a -> ScopeH d f m c
mapScopeH b -> d
f a -> c
g (ScopeH f (Var b (m a))
s) = f (Var d (m c)) -> ScopeH d f m c
forall b (f :: * -> *) (m :: * -> *) a.
f (Var b (m a)) -> ScopeH b f m a
ScopeH (f (Var d (m c)) -> ScopeH d f m c)
-> f (Var d (m c)) -> ScopeH d f m c
forall a b. (a -> b) -> a -> b
$ (Var b (m a) -> Var d (m c)) -> f (Var b (m a)) -> f (Var d (m c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> d) -> (m a -> m c) -> Var b (m a) -> Var d (m c)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap b -> d
f ((a -> c) -> m a -> m c
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> c
g)) f (Var b (m a))
s
{-# INLINE mapScopeH #-}

-- | Obtain a result by collecting information from bound variables
foldMapBoundH :: (Foldable f, Monoid r) => (b -> r) -> ScopeH b f m a -> r
foldMapBoundH :: (b -> r) -> ScopeH b f m a -> r
foldMapBoundH b -> r
f (ScopeH f (Var b (m a))
s) = (Var b (m a) -> r) -> f (Var b (m a)) -> r
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Var b (m a) -> r
forall a. Var b a -> r
f' f (Var b (m a))
s where
    f' :: Var b a -> r
f' (B b
a) = b -> r
f b
a
    f' Var b a
_     = r
forall a. Monoid a => a
mempty
{-# INLINE foldMapBoundH #-}

-- | Obtain a result by collecting information from both bound and free
-- variables
foldMapScopeH
    :: (Foldable f, Foldable m, Monoid r)
    => (b -> r) -> (a -> r)
    -> ScopeH b f m a -> r
foldMapScopeH :: (b -> r) -> (a -> r) -> ScopeH b f m a -> r
foldMapScopeH b -> r
f a -> r
g (ScopeH f (Var b (m a))
s) = (Var b (m a) -> r) -> f (Var b (m a)) -> r
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((b -> r) -> (m a -> r) -> Var b (m a) -> r
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap b -> r
f ((a -> r) -> m a -> r
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> r
g)) f (Var b (m a))
s
{-# INLINE foldMapScopeH #-}

-- | 'traverse_' the bound variables in a 'Scope'.
traverseBoundH_ :: (Applicative g, Foldable f) => (b -> g d) -> ScopeH b f m a -> g ()
traverseBoundH_ :: (b -> g d) -> ScopeH b f m a -> g ()
traverseBoundH_ b -> g d
f (ScopeH f (Var b (m a))
s) = (Var b (m a) -> g ()) -> f (Var b (m a)) -> g ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ Var b (m a) -> g ()
forall a. Var b a -> g ()
f' f (Var b (m a))
s where
    f' :: Var b a -> g ()
f' (B b
a) = () () -> g d -> g ()
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ b -> g d
f b
a
    f' Var b a
_     = () -> g ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
{-# INLINE traverseBoundH_ #-}

-- | 'traverse_' both the variables bound by this scope and any free variables.
traverseScopeH_
    :: (Applicative g, Foldable f, Foldable m)
    => (b -> g d) -> (a -> g c)
    -> ScopeH b f m a -> g ()
traverseScopeH_ :: (b -> g d) -> (a -> g c) -> ScopeH b f m a -> g ()
traverseScopeH_ b -> g d
f a -> g c
g (ScopeH f (Var b (m a))
s) = (Var b (m a) -> g ()) -> f (Var b (m a)) -> g ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ ((b -> g d) -> (m a -> g ()) -> Var b (m a) -> g ()
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bifoldable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f ()
bitraverse_ b -> g d
f ((a -> g c) -> m a -> g ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ a -> g c
g)) f (Var b (m a))
s
{-# INLINE traverseScopeH_ #-}

-- | 'traverse' the bound variables in a 'Scope'.
traverseBoundH
    :: (Applicative g, Traversable f)
    => (b -> g c) -> ScopeH b f m a -> g (ScopeH c f m a)
traverseBoundH :: (b -> g c) -> ScopeH b f m a -> g (ScopeH c f m a)
traverseBoundH b -> g c
f (ScopeH f (Var b (m a))
s) = f (Var c (m a)) -> ScopeH c f m a
forall b (f :: * -> *) (m :: * -> *) a.
f (Var b (m a)) -> ScopeH b f m a
ScopeH (f (Var c (m a)) -> ScopeH c f m a)
-> g (f (Var c (m a))) -> g (ScopeH c f m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var b (m a) -> g (Var c (m a)))
-> f (Var b (m a)) -> g (f (Var c (m a)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Var b (m a) -> g (Var c (m a))
forall a. Var b a -> g (Var c a)
f' f (Var b (m a))
s where
    f' :: Var b a -> g (Var c a)
f' (B b
b) = c -> Var c a
forall b a. b -> Var b a
B (c -> Var c a) -> g c -> g (Var c a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> g c
f b
b
    f' (F a
a) = Var c a -> g (Var c a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> Var c a
forall b a. a -> Var b a
F a
a)
{-# INLINE traverseBoundH #-}

-- | 'traverse' both bound and free variables
traverseScopeH
    :: (Applicative g, Traversable f, Traversable m)
    => (b -> g d) -> (a -> g c)
    -> ScopeH b f m a -> g (ScopeH d f m c)
traverseScopeH :: (b -> g d) -> (a -> g c) -> ScopeH b f m a -> g (ScopeH d f m c)
traverseScopeH b -> g d
f a -> g c
g (ScopeH f (Var b (m a))
s) = f (Var d (m c)) -> ScopeH d f m c
forall b (f :: * -> *) (m :: * -> *) a.
f (Var b (m a)) -> ScopeH b f m a
ScopeH (f (Var d (m c)) -> ScopeH d f m c)
-> g (f (Var d (m c))) -> g (ScopeH d f m c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var b (m a) -> g (Var d (m c)))
-> f (Var b (m a)) -> g (f (Var d (m c)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((b -> g d) -> (m a -> g (m c)) -> Var b (m a) -> g (Var d (m c))
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 b -> g d
f ((a -> g c) -> m a -> g (m c)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> g c
g)) f (Var b (m a))
s
{-# INLINE traverseScopeH #-}

bitraverseScopeH
    :: (Applicative g, Bitraversable f, Bitraversable m)
    => (k -> g k')
    -> (l -> g l')
    -> (a -> g a')
    -> ScopeH b (f k) (m l) a
    -> g (ScopeH b (f k') (m l') a')
bitraverseScopeH :: (k -> g k')
-> (l -> g l')
-> (a -> g a')
-> ScopeH b (f k) (m l) a
-> g (ScopeH b (f k') (m l') a')
bitraverseScopeH k -> g k'
k l -> g l'
l = (forall x x'. (x -> g x') -> f k x -> g (f k' x'))
-> (forall x x'. (x -> g x') -> m l x -> g (m l' x'))
-> (a -> g a')
-> ScopeH b (f k) (m l) a
-> g (ScopeH b (f k') (m l') a')
forall (g :: * -> *) (f :: * -> *) (f' :: * -> *) (m :: * -> *)
       (m' :: * -> *) a a' b.
Applicative g =>
(forall x x'. (x -> g x') -> f x -> g (f' x'))
-> (forall x x'. (x -> g x') -> m x -> g (m' x'))
-> (a -> g a')
-> ScopeH b f m a
-> g (ScopeH b f' m' a')
bitransverseScopeH ((k -> g k') -> (x -> g x') -> f k x -> g (f k' x')
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 k -> g k'
k) ((l -> g l') -> (x -> g x') -> m l x -> g (m l' x')
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 l -> g l'
l)
{-# INLINE bitraverseScopeH #-}

bitransverseScopeH
    :: Applicative g
    => (forall x x'. (x -> g x') -> f x -> g (f' x'))  -- ^ 'traverse'-like for @f@
    -> (forall x x'. (x -> g x') -> m x -> g (m' x'))  -- ^ 'traverse'-like for @m@
    -> (a -> g a')
    -> ScopeH b f m a
    -> g (ScopeH b f' m' a')
bitransverseScopeH :: (forall x x'. (x -> g x') -> f x -> g (f' x'))
-> (forall x x'. (x -> g x') -> m x -> g (m' x'))
-> (a -> g a')
-> ScopeH b f m a
-> g (ScopeH b f' m' a')
bitransverseScopeH forall x x'. (x -> g x') -> f x -> g (f' x')
tauF forall x x'. (x -> g x') -> m x -> g (m' x')
tauM a -> g a'
f = (f' (Var b (m' a')) -> ScopeH b f' m' a')
-> g (f' (Var b (m' a'))) -> g (ScopeH b f' m' a')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f' (Var b (m' a')) -> ScopeH b f' m' a'
forall b (f :: * -> *) (m :: * -> *) a.
f (Var b (m a)) -> ScopeH b f m a
ScopeH (g (f' (Var b (m' a'))) -> g (ScopeH b f' m' a'))
-> (ScopeH b f m a -> g (f' (Var b (m' a'))))
-> ScopeH b f m a
-> g (ScopeH b f' m' a')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var b (m a) -> g (Var b (m' a')))
-> f (Var b (m a)) -> g (f' (Var b (m' a')))
forall x x'. (x -> g x') -> f x -> g (f' x')
tauF ((m a -> g (m' a')) -> Var b (m a) -> g (Var b (m' a'))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((a -> g a') -> m a -> g (m' a')
forall x x'. (x -> g x') -> m x -> g (m' x')
tauM a -> g a'
f)) (f (Var b (m a)) -> g (f' (Var b (m' a'))))
-> (ScopeH b f m a -> f (Var b (m a)))
-> ScopeH b f m a
-> g (f' (Var b (m' a')))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeH b f m a -> f (Var b (m a))
forall b (f :: * -> *) (m :: * -> *) a.
ScopeH b f m a -> f (Var b (m a))
unscopeH
{-# INLINE bitransverseScopeH #-}