{-# LANGUAGE CPP #-}
{-# LANGUAGE Rank2Types #-}
#ifdef __GLASGOW_HASKELL__
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE DeriveGeneric #-}
#endif

-----------------------------------------------------------------------------
-- |
-- Copyright   :  (C) 2012-2013 Edward Kmett
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
-- Stability   :  experimental
-- Portability :  portable
--
-- This is the work-horse of the @bound@ library.
--
-- 'Scope' provides a single generalized de Bruijn level
-- and is often used inside of the definition of binders.
----------------------------------------------------------------------------
module Bound.Scope
  ( Scope(..)
  -- * Abstraction
  , abstract, abstract1, abstractEither
  -- * Instantiation
  , instantiate, instantiate1, instantiateEither
  -- * Traditional de Bruijn
  , fromScope
  , toScope
  -- * Bound variable manipulation
  , splat
  , bindings
  , mapBound
  , mapScope
  , liftMBound
  , liftMScope
  , foldMapBound
  , foldMapScope
  , traverseBound_
  , traverseScope_
  , mapMBound_
  , mapMScope_
  , traverseBound
  , traverseScope
  , mapMBound
  , mapMScope
  , serializeScope
  , deserializeScope
  , hoistScope
  , bitraverseScope
  , bitransverseScope
  , transverseScope
  , instantiateVars
  ) where

import Bound.Class
import Bound.Var
import Control.Applicative
import Control.DeepSeq
import Control.Monad hiding (mapM, mapM_)
import Control.Monad.Morph
import Data.Bifunctor
import Data.Bifoldable
import qualified Data.Binary as Binary
import Data.Binary (Binary)
import Data.Bitraversable
import Data.Bytes.Get
import Data.Bytes.Put
import Data.Bytes.Serial
import Data.Foldable
import Data.Functor.Classes
import Data.Hashable (Hashable (..))
import Data.Hashable.Lifted (Hashable1(..), hashWithSalt1)
import Data.Monoid
import qualified Data.Serialize as Serialize
import Data.Serialize (Serialize)
import Data.Traversable
import Prelude hiding (foldr, mapM, mapM_)
import Data.Data
#if defined(__GLASGOW_HASKELL__)
import GHC.Generics ( Generic, Generic1 )
#endif

-- $setup
-- >>> import Bound.Var

-------------------------------------------------------------------------------
-- Scopes
-------------------------------------------------------------------------------

-- | @'Scope' b f a@ is an @f@ expression with bound variables in @b@,
-- and free variables in @a@
--
-- We store bound variables as their generalized de Bruijn
-- representation in that we're allowed to 'lift' (using 'F') an entire
-- tree rather than only succ individual variables, but we're still
-- only allowed to do so once per 'Scope'. Weakening trees permits
-- /O(1)/ weakening and permits more sharing opportunities. Here the
-- deBruijn 0 is represented by the 'B' constructor of 'Var', while the
-- de Bruijn 'succ' (which may be applied to an entire tree!) is handled
-- by 'F'.
--
-- NB: equality and comparison quotient out the distinct 'F' placements
-- allowed by the generalized de Bruijn representation and return the
-- same result as a traditional de Bruijn representation would.
--
-- Logically you can think of this as if the shape were the traditional
-- @f (Var b a)@, but the extra @f a@ inside permits us a cheaper 'lift'.
--
newtype Scope b f a = Scope { Scope b f a -> f (Var b (f a))
unscope :: f (Var b (f a)) }
#if defined(__GLASGOW_HASKELL__)
  deriving ((forall x. Scope b f a -> Rep (Scope b f a) x)
-> (forall x. Rep (Scope b f a) x -> Scope b f a)
-> Generic (Scope b f a)
forall x. Rep (Scope b f a) x -> Scope b f a
forall x. Scope b f a -> Rep (Scope b f a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall b (f :: * -> *) a x. Rep (Scope b f a) x -> Scope b f a
forall b (f :: * -> *) a x. Scope b f a -> Rep (Scope b f a) x
$cto :: forall b (f :: * -> *) a x. Rep (Scope b f a) x -> Scope b f a
$cfrom :: forall b (f :: * -> *) a x. Scope b f a -> Rep (Scope b f a) x
Generic)
#endif
deriving instance Functor f => Generic1 (Scope b f)

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

instance Functor f => Functor (Scope b f) where
  fmap :: (a -> b) -> Scope b f a -> Scope b f b
fmap a -> b
f (Scope f (Var b (f a))
a) = f (Var b (f b)) -> Scope b f b
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope ((Var b (f a) -> Var b (f b)) -> f (Var b (f a)) -> f (Var b (f b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f a -> f b) -> Var b (f a) -> Var b (f b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f)) f (Var b (f a))
a)
  {-# INLINE fmap #-}

-- | @'toList'@ is provides a list (with duplicates) of the free variables
instance Foldable f => Foldable (Scope b f) where
  foldMap :: (a -> m) -> Scope b f a -> m
foldMap a -> m
f (Scope f (Var b (f a))
a) = (Var b (f a) -> m) -> f (Var b (f a)) -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((f a -> m) -> Var b (f a) -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((a -> m) -> f a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f)) f (Var b (f a))
a
  {-# INLINE foldMap #-}

instance Traversable f => Traversable (Scope b f) where
  traverse :: (a -> f b) -> Scope b f a -> f (Scope b f b)
traverse a -> f b
f (Scope f (Var b (f a))
a) = f (Var b (f b)) -> Scope b f b
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope (f (Var b (f b)) -> Scope b f b)
-> f (f (Var b (f b))) -> f (Scope b f b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var b (f a) -> f (Var b (f b)))
-> f (Var b (f a)) -> f (f (Var b (f b)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((f a -> f (f b)) -> Var b (f a) -> f (Var b (f 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 (f 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 (f a))
a
  {-# INLINE traverse #-}

instance (Functor f, Monad f) => Applicative (Scope b f) where
  pure :: a -> Scope b f a
pure a
a = f (Var b (f a)) -> Scope b f a
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope (Var b (f a) -> f (Var b (f a))
forall (m :: * -> *) a. Monad m => a -> m a
return (f a -> Var b (f a)
forall b a. a -> Var b a
F (a -> f a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a)))
  {-# INLINE pure #-}
  <*> :: Scope b f (a -> b) -> Scope b f a -> Scope b f b
(<*>) = Scope b f (a -> b) -> Scope b f a -> Scope b f b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
  {-# INLINE (<*>) #-}

-- | The monad permits substitution on free variables, while preserving
-- bound variables
instance Monad f => Monad (Scope b f) where
  Scope f (Var b (f a))
e >>= :: Scope b f a -> (a -> Scope b f b) -> Scope b f b
>>= a -> Scope b f b
f = f (Var b (f b)) -> Scope b f b
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope (f (Var b (f b)) -> Scope b f b) -> f (Var b (f b)) -> Scope b f b
forall a b. (a -> b) -> a -> b
$ f (Var b (f a))
e f (Var b (f a))
-> (Var b (f a) -> f (Var b (f b))) -> f (Var b (f b))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Var b (f a)
v -> case Var b (f a)
v of
    B b
b -> Var b (f b) -> f (Var b (f b))
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> Var b (f b)
forall b a. b -> Var b a
B b
b)
    F f a
ea -> f a
ea f a -> (a -> f (Var b (f b))) -> f (Var b (f b))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Scope b f b -> f (Var b (f b))
forall b (f :: * -> *) a. Scope b f a -> f (Var b (f a))
unscope (Scope b f b -> f (Var b (f b)))
-> (a -> Scope b f b) -> a -> f (Var b (f b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Scope b f b
f
  {-# INLINE (>>=) #-}

instance MonadTrans (Scope b) where
  lift :: m a -> Scope b m a
lift m a
m = m (Var b (m a)) -> Scope b m a
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope (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))
  {-# INLINE lift #-}

instance MFunctor (Scope b) where
  hoist :: (forall a. m a -> n a) -> Scope b m b -> Scope b n b
hoist = (forall a. m a -> n a) -> Scope b m b -> Scope b n b
forall (f :: * -> *) (g :: * -> *) b a.
Functor f =>
(forall x. f x -> g x) -> Scope b f a -> Scope b g a
hoistScope
  {-# INLINE hoist #-}

instance (Monad f, Eq b, Eq1 f, Eq a) => Eq  (Scope b f a) where == :: Scope b f a -> Scope b f a -> Bool
(==) = Scope b f a -> Scope b f a -> Bool
forall (f :: * -> *) a. (Eq1 f, Eq a) => f a -> f a -> Bool
eq1
instance (Monad f, Ord b, Ord1 f, Ord a) => Ord  (Scope b f a) where compare :: Scope b f a -> Scope b f a -> Ordering
compare = Scope b f a -> Scope b f a -> Ordering
forall (f :: * -> *) a. (Ord1 f, Ord a) => f a -> f a -> Ordering
compare1

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

instance (Read b, Read1 f, Read a) => Read  (Scope b f a) where readsPrec :: Int -> ReadS (Scope b f a)
readsPrec = Int -> ReadS (Scope b f a)
forall (f :: * -> *) a. (Read1 f, Read a) => Int -> ReadS (f a)
readsPrec1
instance (Show b, Show1 f, Show a) => Show (Scope b f a) where showsPrec :: Int -> Scope b f a -> ShowS
showsPrec = Int -> Scope b f a -> ShowS
forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1

instance (Monad f, Eq b, Eq1 f) => Eq1 (Scope b f) where
  liftEq :: (a -> b -> Bool) -> Scope b f a -> Scope b f b -> Bool
liftEq a -> b -> Bool
f Scope b f a
m Scope b f 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) (Scope b f a -> f (Var b a)
forall (f :: * -> *) b a. Monad f => Scope b f a -> f (Var b a)
fromScope Scope b f a
m) (Scope b f b -> f (Var b b)
forall (f :: * -> *) b a. Monad f => Scope b f a -> f (Var b a)
fromScope Scope b f b
n)

instance (Monad f, Ord b, Ord1 f) => Ord1 (Scope b f) where
  liftCompare :: (a -> b -> Ordering) -> Scope b f a -> Scope b f b -> Ordering
liftCompare a -> b -> Ordering
f Scope b f a
m Scope b f 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) (Scope b f a -> f (Var b a)
forall (f :: * -> *) b a. Monad f => Scope b f a -> f (Var b a)
fromScope Scope b f a
m) (Scope b f b -> f (Var b b)
forall (f :: * -> *) b a. Monad f => Scope b f a -> f (Var b a)
fromScope Scope b f b
n)

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

instance (Read b, Read1 f) => Read1 (Scope b f) where
  liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (Scope b f a)
liftReadsPrec Int -> ReadS a
f ReadS [a]
g = (String -> ReadS (Scope b f a)) -> Int -> ReadS (Scope b f a)
forall a. (String -> ReadS a) -> Int -> ReadS a
readsData ((String -> ReadS (Scope b f a)) -> Int -> ReadS (Scope b f a))
-> (String -> ReadS (Scope b f a)) -> Int -> ReadS (Scope b f a)
forall a b. (a -> b) -> a -> b
$ (Int -> ReadS (f (Var b (f a))))
-> String
-> (f (Var b (f a)) -> Scope b f a)
-> String
-> ReadS (Scope b f a)
forall a t.
(Int -> ReadS a) -> String -> (a -> t) -> String -> ReadS t
readsUnaryWith ((Int -> ReadS (Var b (f a)))
-> ReadS [Var b (f a)] -> Int -> ReadS (f (Var b (f a)))
forall (f :: * -> *) a.
Read1 f =>
(Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (f a)
liftReadsPrec ((Int -> ReadS (f a)) -> ReadS [f a] -> Int -> ReadS (Var b (f a))
forall (f :: * -> *) a.
Read1 f =>
(Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (f a)
liftReadsPrec Int -> ReadS (f a)
f' ReadS [f a]
g') ((Int -> ReadS (f a)) -> ReadS [f a] -> ReadS [Var b (f a)]
forall (f :: * -> *) a.
Read1 f =>
(Int -> ReadS a) -> ReadS [a] -> ReadS [f a]
liftReadList Int -> ReadS (f a)
f' ReadS [f a]
g')) String
"Scope" f (Var b (f a)) -> Scope b f a
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope where
    f' :: Int -> ReadS (f a)
f' = (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (f 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 [f a]
g' = (Int -> ReadS a) -> ReadS [a] -> ReadS [f a]
forall (f :: * -> *) a.
Read1 f =>
(Int -> ReadS a) -> ReadS [a] -> ReadS [f a]
liftReadList Int -> ReadS a
f ReadS [a]
g

instance Bound (Scope b) where
  Scope f (Var b (f a))
m >>>= :: Scope b f a -> (a -> f c) -> Scope b f c
>>>= a -> f c
f = f (Var b (f c)) -> Scope b f c
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope ((Var b (f a) -> Var b (f c)) -> f (Var b (f a)) -> f (Var b (f c))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((f a -> f c) -> Var b (f a) -> Var b (f c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (f a -> (a -> f c) -> f c
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> f c
f)) f (Var b (f a))
m)
  {-# INLINE (>>>=) #-}

--  {-# INLINE hashWithSalt1 #-}

instance (Hashable b, Monad f, Hashable1 f) => Hashable1 (Scope b f) where
  liftHashWithSalt :: (Int -> a -> Int) -> Int -> Scope b f a -> Int
liftHashWithSalt Int -> a -> Int
h Int
s Scope b f 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 (Scope b f a -> f (Var b a)
forall (f :: * -> *) b a. Monad f => Scope b f a -> f (Var b a)
fromScope Scope b f a
m)
  {-# INLINE liftHashWithSalt #-}

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

instance NFData (f (Var b (f a))) => NFData (Scope b f a) where
  rnf :: Scope b f a -> ()
rnf Scope b f a
scope = f (Var b (f a)) -> ()
forall a. NFData a => a -> ()
rnf (Scope b f a -> f (Var b (f a))
forall b (f :: * -> *) a. Scope b f a -> f (Var b (f a))
unscope Scope b f a
scope)

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

-- | Capture some free variables in an expression to yield
-- a 'Scope' with bound variables in @b@
--
-- >>> :m + Data.List
-- >>> abstract (`elemIndex` "bar") "barry"
-- Scope [B 0,B 1,B 2,B 2,F "y"]
abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f a
abstract :: (a -> Maybe b) -> f a -> Scope b f a
abstract a -> Maybe b
f f a
e = f (Var b (f a)) -> Scope b f a
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope ((a -> Var b (f a)) -> f a -> f (Var b (f a))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM a -> Var b (f 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 abstract #-}

-- | Abstract over a single variable
--
-- >>> abstract1 'x' "xyz"
-- Scope [B (),F "y",F "z"]
abstract1 :: (Monad f, Eq a) => a -> f a -> Scope () f a
abstract1 :: a -> f a -> Scope () f a
abstract1 a
a = (a -> Maybe ()) -> f a -> Scope () f a
forall (f :: * -> *) a b.
Monad f =>
(a -> Maybe b) -> f a -> Scope b f a
abstract (\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 abstract1 #-}

-- | Capture some free variables in an expression to yield
-- a 'Scope' with bound variables in @b@. Optionally change the
-- types of the remaining free variables.
abstractEither :: Monad f => (a -> Either b c) -> f a -> Scope b f c
abstractEither :: (a -> Either b c) -> f a -> Scope b f c
abstractEither a -> Either b c
f f a
e = f (Var b (f c)) -> Scope b f c
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope ((a -> Var b (f c)) -> f a -> f (Var b (f c))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM a -> Var b (f 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')

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

-- | Enter a scope, instantiating all bound variables
--
-- >>> :m + Data.List
-- >>> instantiate (\x -> [toEnum (97 + x)]) $ abstract (`elemIndex` "bar") "barry"
-- "abccy"
instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a
instantiate :: (b -> f a) -> Scope b f a -> f a
instantiate b -> f a
k Scope b f a
e = Scope b f a -> f (Var b (f a))
forall b (f :: * -> *) a. Scope b f a -> f (Var b (f a))
unscope Scope b f a
e f (Var b (f a)) -> (Var b (f a) -> f a) -> f a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Var b (f a)
v -> case Var b (f a)
v of
  B b
b -> b -> f a
k b
b
  F f a
a -> f a
a
{-# INLINE instantiate #-}

-- | Enter a 'Scope' that binds one variable, instantiating it
--
-- >>> instantiate1 "x" $ Scope [B (),F "y",F "z"]
-- "xyz"
instantiate1 :: Monad f => f a -> Scope n f a -> f a
instantiate1 :: f a -> Scope n f a -> f a
instantiate1 f a
e = (n -> f a) -> Scope n f a -> f a
forall (f :: * -> *) b a.
Monad f =>
(b -> f a) -> Scope b f a -> f a
instantiate (f a -> n -> f a
forall a b. a -> b -> a
const f a
e)
{-# INLINE instantiate1 #-}

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

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

-- | @'fromScope'@ quotients out the possible placements of 'F' in 'Scope'
-- by distributing them all to the leaves. This yields a more traditional
-- de Bruijn indexing scheme for bound variables.
--
-- Since,
--
-- @'fromScope' '.' 'toScope' ≡ 'id'@
--
-- we know that
--
-- @'fromScope' '.' 'toScope' '.' 'fromScope' ≡ 'fromScope'@
--
-- and therefore @('toScope' . 'fromScope')@ is idempotent.
fromScope :: Monad f => Scope b f a -> f (Var b a)
fromScope :: Scope b f a -> f (Var b a)
fromScope (Scope f (Var b (f a))
s) = f (Var b (f a))
s f (Var b (f a)) -> (Var b (f a) -> f (Var b a)) -> f (Var b a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Var b (f a)
v -> case Var b (f a)
v of
  F f a
e -> (a -> Var b a) -> f a -> f (Var b a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM a -> Var b a
forall b a. a -> Var b a
F f a
e
  B b
b -> Var b a -> f (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)
{-# INLINE fromScope #-}

-- | Convert from traditional de Bruijn to generalized de Bruijn indices.
--
-- This requires a full tree traversal
toScope :: Monad f => f (Var b a) -> Scope b f a
toScope :: f (Var b a) -> Scope b f a
toScope f (Var b a)
e = f (Var b (f a)) -> Scope b f a
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope ((Var b a -> Var b (f a)) -> f (Var b a) -> f (Var b (f a))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((a -> f a) -> Var b a -> Var b (f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> f a
forall (m :: * -> *) a. Monad m => a -> m a
return) f (Var b a)
e)
{-# INLINE toScope #-}

-------------------------------------------------------------------------------
-- Exotic Traversals of Bound Variables (not exported by default)
-------------------------------------------------------------------------------

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

-- | Return a list of occurences of the variables bound by this 'Scope'.
bindings :: Foldable f => Scope b f a -> [b]
bindings :: Scope b f a -> [b]
bindings (Scope f (Var b (f a))
s) = (Var b (f a) -> [b] -> [b]) -> [b] -> f (Var b (f a)) -> [b]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Var b (f a) -> [b] -> [b]
forall a a. Var a a -> [a] -> [a]
f [] f (Var b (f 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 bindings #-}

-- | Perform a change of variables on bound variables.
mapBound :: Functor f => (b -> b') -> Scope b f a -> Scope b' f a
mapBound :: (b -> b') -> Scope b f a -> Scope b' f a
mapBound b -> b'
f (Scope f (Var b (f a))
s) = f (Var b' (f a)) -> Scope b' f a
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope ((Var b (f a) -> Var b' (f a))
-> f (Var b (f a)) -> f (Var b' (f a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Var b (f a) -> Var b' (f a)
forall a. Var b a -> Var b' a
f' f (Var b (f 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 mapBound #-}

-- | Perform a change of variables, reassigning both bound and free variables.
mapScope :: Functor f => (b -> d) -> (a -> c) -> Scope b f a -> Scope d f c
mapScope :: (b -> d) -> (a -> c) -> Scope b f a -> Scope d f c
mapScope b -> d
f a -> c
g (Scope f (Var b (f a))
s) = f (Var d (f c)) -> Scope d f c
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope (f (Var d (f c)) -> Scope d f c) -> f (Var d (f c)) -> Scope d f c
forall a b. (a -> b) -> a -> b
$ (Var b (f a) -> Var d (f c)) -> f (Var b (f a)) -> f (Var d (f c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> d) -> (f a -> f c) -> Var b (f a) -> Var d (f 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) -> f a -> f c
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> c
g)) f (Var b (f a))
s
{-# INLINE mapScope #-}

-- | Perform a change of variables on bound variables given only a 'Monad'
-- instance
liftMBound :: Monad m => (b -> b') -> Scope b m a -> Scope b' m a
liftMBound :: (b -> b') -> Scope b m a -> Scope b' m a
liftMBound b -> b'
f (Scope m (Var b (m a))
s) = m (Var b' (m a)) -> Scope b' m a
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope ((Var b (m a) -> Var b' (m a))
-> m (Var b (m a)) -> m (Var b' (m a))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Var b (m a) -> Var b' (m a)
forall a. Var b a -> Var b' a
f' m (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 liftMBound #-}

-- | A version of 'mapScope' that can be used when you only have the 'Monad'
-- instance
liftMScope :: Monad m => (b -> d) -> (a -> c) -> Scope b m a -> Scope d m c
liftMScope :: (b -> d) -> (a -> c) -> Scope b m a -> Scope d m c
liftMScope b -> d
f a -> c
g (Scope m (Var b (m a))
s) = m (Var d (m c)) -> Scope d m c
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope (m (Var d (m c)) -> Scope d m c) -> m (Var d (m c)) -> Scope d m c
forall a b. (a -> b) -> a -> b
$ (Var b (m a) -> Var d (m c)) -> m (Var b (m a)) -> m (Var d (m c))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((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 (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM a -> c
g)) m (Var b (m a))
s
{-# INLINE liftMScope #-}

-- | Obtain a result by collecting information from bound variables
foldMapBound :: (Foldable f, Monoid r) => (b -> r) -> Scope b f a -> r
foldMapBound :: (b -> r) -> Scope b f a -> r
foldMapBound b -> r
f (Scope f (Var b (f a))
s) = (Var b (f a) -> r) -> f (Var b (f a)) -> r
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Var b (f a) -> r
forall a. Var b a -> r
f' f (Var b (f 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 foldMapBound #-}

-- | Obtain a result by collecting information from both bound and free
-- variables
foldMapScope :: (Foldable f, Monoid r) =>
                (b -> r) -> (a -> r) -> Scope b f a -> r
foldMapScope :: (b -> r) -> (a -> r) -> Scope b f a -> r
foldMapScope b -> r
f a -> r
g (Scope f (Var b (f a))
s) = (Var b (f a) -> r) -> f (Var b (f a)) -> r
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((b -> r) -> (f a -> r) -> Var b (f 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) -> f a -> r
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> r
g)) f (Var b (f a))
s
{-# INLINE foldMapScope #-}

-- | 'traverse_' the bound variables in a 'Scope'.
traverseBound_ :: (Applicative g, Foldable f) =>
                  (b -> g d) -> Scope b f a -> g ()
traverseBound_ :: (b -> g d) -> Scope b f a -> g ()
traverseBound_ b -> g d
f (Scope f (Var b (f a))
s) = (Var b (f a) -> g ()) -> f (Var b (f a)) -> g ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ Var b (f a) -> g ()
forall a. Var b a -> g ()
f' f (Var b (f 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 traverseBound_ #-}

-- | 'traverse' both the variables bound by this scope and any free variables.
traverseScope_ :: (Applicative g, Foldable f) =>
                  (b -> g d) -> (a -> g c) -> Scope b f a -> g ()
traverseScope_ :: (b -> g d) -> (a -> g c) -> Scope b f a -> g ()
traverseScope_ b -> g d
f a -> g c
g (Scope f (Var b (f a))
s) = (Var b (f a) -> g ()) -> f (Var b (f a)) -> g ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ ((b -> g d) -> (f a -> g ()) -> Var b (f 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) -> f 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 (f a))
s
{-# INLINE traverseScope_ #-}

-- | mapM_ over the variables bound by this scope
mapMBound_ :: (Monad g, Foldable f) => (b -> g d) -> Scope b f a -> g ()
mapMBound_ :: (b -> g d) -> Scope b f a -> g ()
mapMBound_ b -> g d
f (Scope f (Var b (f a))
s) = (Var b (f a) -> g ()) -> f (Var b (f a)) -> g ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Var b (f a) -> g ()
forall a. Var b a -> g ()
f' f (Var b (f a))
s where
  f' :: Var b a -> g ()
f' (B b
a) = do d
_ <- b -> g d
f b
a; () -> g ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  f' Var b a
_     = () -> g ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
{-# INLINE mapMBound_ #-}

-- | A 'traverseScope_' that can be used when you only have a 'Monad'
-- instance
mapMScope_ :: (Monad m, Foldable f) =>
              (b -> m d) -> (a -> m c) -> Scope b f a -> m ()
mapMScope_ :: (b -> m d) -> (a -> m c) -> Scope b f a -> m ()
mapMScope_ b -> m d
f a -> m c
g (Scope f (Var b (f a))
s) = (Var b (f a) -> m ()) -> f (Var b (f a)) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((b -> m d) -> (f a -> m ()) -> Var b (f a) -> m ()
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bifoldable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f ()
bimapM_ b -> m d
f ((a -> m c) -> f a -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ a -> m c
g)) f (Var b (f a))
s
{-# INLINE mapMScope_ #-}

-- | 'traverse' the bound variables in a 'Scope'.
traverseBound :: (Applicative g, Traversable f) =>
                 (b -> g c) -> Scope b f a -> g (Scope c f a)
traverseBound :: (b -> g c) -> Scope b f a -> g (Scope c f a)
traverseBound b -> g c
f (Scope f (Var b (f a))
s) = f (Var c (f a)) -> Scope c f a
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope (f (Var c (f a)) -> Scope c f a)
-> g (f (Var c (f a))) -> g (Scope c f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var b (f a) -> g (Var c (f a)))
-> f (Var b (f a)) -> g (f (Var c (f a)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Var b (f a) -> g (Var c (f a))
forall a. Var b a -> g (Var c a)
f' f (Var b (f 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 traverseBound #-}

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

-- | mapM over both bound and free variables
mapMBound :: (Monad m, Traversable f) =>
             (b -> m c) -> Scope b f a -> m (Scope c f a)
mapMBound :: (b -> m c) -> Scope b f a -> m (Scope c f a)
mapMBound b -> m c
f (Scope f (Var b (f a))
s) = (f (Var c (f a)) -> Scope c f a)
-> m (f (Var c (f a))) -> m (Scope c f a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM f (Var c (f a)) -> Scope c f a
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope ((Var b (f a) -> m (Var c (f a)))
-> f (Var b (f a)) -> m (f (Var c (f a)))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Var b (f a) -> m (Var c (f a))
forall a. Var b a -> m (Var c a)
f' f (Var b (f a))
s) where
  f' :: Var b a -> m (Var c a)
f' (B b
b) = (c -> Var c a) -> m c -> m (Var c a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM c -> Var c a
forall b a. b -> Var b a
B (b -> m c
f b
b)
  f' (F a
a) = Var c a -> m (Var c a)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Var c a
forall b a. a -> Var b a
F a
a)
{-# INLINE mapMBound #-}

-- | A 'traverseScope' that can be used when you only have a 'Monad'
-- instance
mapMScope :: (Monad m, Traversable f) =>
             (b -> m d) -> (a -> m c) -> Scope b f a -> m (Scope d f c)
mapMScope :: (b -> m d) -> (a -> m c) -> Scope b f a -> m (Scope d f c)
mapMScope b -> m d
f a -> m c
g (Scope f (Var b (f a))
s) = (f (Var d (f c)) -> Scope d f c)
-> m (f (Var d (f c))) -> m (Scope d f c)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM f (Var d (f c)) -> Scope d f c
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope ((Var b (f a) -> m (Var d (f c)))
-> f (Var b (f a)) -> m (f (Var d (f c)))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((b -> m d) -> (f a -> m (f c)) -> Var b (f a) -> m (Var d (f 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)
bimapM b -> m d
f ((a -> m c) -> f a -> m (f c)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> m c
g)) f (Var b (f a))
s)
{-# INLINE mapMScope #-}

serializeScope :: (Serial1 f, MonadPut m) => (b -> m ()) -> (v -> m ()) -> Scope b f v -> m ()
serializeScope :: (b -> m ()) -> (v -> m ()) -> Scope b f v -> m ()
serializeScope b -> m ()
pb v -> m ()
pv (Scope f (Var b (f v))
body) = (Var b (f v) -> m ()) -> f (Var b (f v)) -> m ()
forall (f :: * -> *) (m :: * -> *) a.
(Serial1 f, MonadPut m) =>
(a -> m ()) -> f a -> m ()
serializeWith ((b -> m ()) -> (f v -> m ()) -> Var b (f v) -> m ()
forall (f :: * -> * -> *) (m :: * -> *) a b.
(Serial2 f, MonadPut m) =>
(a -> m ()) -> (b -> m ()) -> f a b -> m ()
serializeWith2 b -> m ()
pb ((f v -> m ()) -> Var b (f v) -> m ())
-> (f v -> m ()) -> Var b (f v) -> m ()
forall a b. (a -> b) -> a -> b
$ (v -> m ()) -> f v -> m ()
forall (f :: * -> *) (m :: * -> *) a.
(Serial1 f, MonadPut m) =>
(a -> m ()) -> f a -> m ()
serializeWith v -> m ()
pv) f (Var b (f v))
body
{-# INLINE serializeScope #-}

deserializeScope :: (Serial1 f, MonadGet m) => m b -> m v -> m (Scope b f v)
deserializeScope :: m b -> m v -> m (Scope b f v)
deserializeScope m b
gb m v
gv = (f (Var b (f v)) -> Scope b f v)
-> m (f (Var b (f v))) -> m (Scope b f v)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM f (Var b (f v)) -> Scope b f v
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope (m (f (Var b (f v))) -> m (Scope b f v))
-> m (f (Var b (f v))) -> m (Scope b f v)
forall a b. (a -> b) -> a -> b
$ m (Var b (f v)) -> m (f (Var b (f v)))
forall (f :: * -> *) (m :: * -> *) a.
(Serial1 f, MonadGet m) =>
m a -> m (f a)
deserializeWith (m b -> m (f v) -> m (Var b (f v))
forall (f :: * -> * -> *) (m :: * -> *) a b.
(Serial2 f, MonadGet m) =>
m a -> m b -> m (f a b)
deserializeWith2 m b
gb (m (f v) -> m (Var b (f v))) -> m (f v) -> m (Var b (f v))
forall a b. (a -> b) -> a -> b
$ m v -> m (f v)
forall (f :: * -> *) (m :: * -> *) a.
(Serial1 f, MonadGet m) =>
m a -> m (f a)
deserializeWith m v
gv)
{-# INLINE deserializeScope #-}

-- | This allows you to 'bitraverse' a 'Scope'.
bitraverseScope :: (Bitraversable t, Applicative f) => (k -> f k') -> (a -> f a') -> Scope b (t k) a -> f (Scope b (t k') a')
bitraverseScope :: (k -> f k')
-> (a -> f a') -> Scope b (t k) a -> f (Scope b (t k') a')
bitraverseScope k -> f k'
f = (forall a a'. (a -> f a') -> t k a -> f (t k' a'))
-> (a -> f a') -> Scope b (t k) a -> f (Scope b (t k') a')
forall (f :: * -> *) (t :: * -> *) (u :: * -> *) c c' b.
Applicative f =>
(forall a a'. (a -> f a') -> t a -> f (u a'))
-> (c -> f c') -> Scope b t c -> f (Scope b u c')
bitransverseScope ((k -> f k') -> (a -> f a') -> t k a -> f (t k' a')
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 -> f k'
f)
{-# INLINE bitraverseScope #-}

-- | This is a higher-order analogue of 'traverse'.
transverseScope :: (Applicative f, Monad f, Traversable g)
                => (forall r. g r -> f (h r))
                -> Scope b g a -> f (Scope b h a)
transverseScope :: (forall r. g r -> f (h r)) -> Scope b g a -> f (Scope b h a)
transverseScope forall r. g r -> f (h r)
tau (Scope g (Var b (g a))
e) = h (Var b (h a)) -> Scope b h a
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope (h (Var b (h a)) -> Scope b h a)
-> f (h (Var b (h a))) -> f (Scope b h a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (g (Var b (h a)) -> f (h (Var b (h a)))
forall r. g r -> f (h r)
tau (g (Var b (h a)) -> f (h (Var b (h a))))
-> f (g (Var b (h a))) -> f (h (Var b (h a)))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Var b (g a) -> f (Var b (h a)))
-> g (Var b (g a)) -> f (g (Var b (h a)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((g a -> f (h a)) -> Var b (g a) -> f (Var b (h a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse g a -> f (h a)
forall r. g r -> f (h r)
tau) g (Var b (g a))
e)

bitransverseScope :: Applicative f => (forall a a'. (a -> f a') -> t a -> f (u a')) -> (c -> f c') -> Scope b t c -> f (Scope b u c')
bitransverseScope :: (forall a a'. (a -> f a') -> t a -> f (u a'))
-> (c -> f c') -> Scope b t c -> f (Scope b u c')
bitransverseScope forall a a'. (a -> f a') -> t a -> f (u a')
tau c -> f c'
f = (u (Var b (u c')) -> Scope b u c')
-> f (u (Var b (u c'))) -> f (Scope b u c')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap u (Var b (u c')) -> Scope b u c'
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope (f (u (Var b (u c'))) -> f (Scope b u c'))
-> (Scope b t c -> f (u (Var b (u c'))))
-> Scope b t c
-> f (Scope b u c')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var b (t c) -> f (Var b (u c')))
-> t (Var b (t c)) -> f (u (Var b (u c')))
forall a a'. (a -> f a') -> t a -> f (u a')
tau ((t c -> f (u c')) -> Var b (t c) -> f (Var b (u c'))
forall (p :: * -> * -> *) (f :: * -> *) a a' b.
(Choice p, Applicative f) =>
p a (f a') -> p (Var b a) (f (Var b a'))
_F ((c -> f c') -> t c -> f (u c')
forall a a'. (a -> f a') -> t a -> f (u a')
tau c -> f c'
f)) (t (Var b (t c)) -> f (u (Var b (u c'))))
-> (Scope b t c -> t (Var b (t c)))
-> Scope b t c
-> f (u (Var b (u c')))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Scope b t c -> t (Var b (t c))
forall b (f :: * -> *) a. Scope b f a -> f (Var b (f a))
unscope
{-# INLINE bitransverseScope #-}

-- | instantiate bound variables using a list of new variables
instantiateVars :: Monad t => [a] -> Scope Int t a -> t a
instantiateVars :: [a] -> Scope Int t a -> t a
instantiateVars [a]
as = (Int -> t a) -> Scope Int t a -> t a
forall (f :: * -> *) b a.
Monad f =>
(b -> f a) -> Scope b f a -> f a
instantiate ([t a]
vs [t a] -> Int -> t a
forall a. [a] -> Int -> a
!!) where
  vs :: [t a]
vs = (a -> t a) -> [a] -> [t a]
forall a b. (a -> b) -> [a] -> [b]
map a -> t a
forall (m :: * -> *) a. Monad m => a -> m a
return [a]
as
{-# INLINE instantiateVars #-}

-- | Lift a natural transformation from @f@ to @g@ into one between scopes.
hoistScope :: Functor f => (forall x. f x -> g x) -> Scope b f a -> Scope b g a
hoistScope :: (forall x. f x -> g x) -> Scope b f a -> Scope b g a
hoistScope forall x. f x -> g x
t (Scope f (Var b (f a))
b) = g (Var b (g a)) -> Scope b g a
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope (g (Var b (g a)) -> Scope b g a) -> g (Var b (g a)) -> Scope b g a
forall a b. (a -> b) -> a -> b
$ f (Var b (g a)) -> g (Var b (g a))
forall x. f x -> g x
t ((f a -> g a) -> Var b (f a) -> Var b (g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f a -> g a
forall x. f x -> g x
t (Var b (f a) -> Var b (g a)) -> f (Var b (f a)) -> f (Var b (g a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Var b (f a))
b)
{-# INLINE hoistScope #-}

instance (Serial b, Serial1 f) => Serial1 (Scope b f) where
  serializeWith :: (a -> m ()) -> Scope b f a -> m ()
serializeWith = (b -> m ()) -> (a -> m ()) -> Scope b f a -> m ()
forall (f :: * -> *) (m :: * -> *) b v.
(Serial1 f, MonadPut m) =>
(b -> m ()) -> (v -> m ()) -> Scope b f v -> m ()
serializeScope b -> m ()
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
serialize
  deserializeWith :: m a -> m (Scope b f a)
deserializeWith = m b -> m a -> m (Scope b f a)
forall (f :: * -> *) (m :: * -> *) b v.
(Serial1 f, MonadGet m) =>
m b -> m v -> m (Scope b f v)
deserializeScope m b
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
deserialize

instance (Serial b, Serial1 f, Serial a) => Serial (Scope b f a) where
  serialize :: Scope b f a -> m ()
serialize = (b -> m ()) -> (a -> m ()) -> Scope b f a -> m ()
forall (f :: * -> *) (m :: * -> *) b v.
(Serial1 f, MonadPut m) =>
(b -> m ()) -> (v -> m ()) -> Scope b f v -> m ()
serializeScope b -> m ()
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
serialize a -> m ()
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
serialize
  deserialize :: m (Scope b f a)
deserialize = m b -> m a -> m (Scope b f a)
forall (f :: * -> *) (m :: * -> *) b v.
(Serial1 f, MonadGet m) =>
m b -> m v -> m (Scope b f v)
deserializeScope m b
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
deserialize m a
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
deserialize

instance (Binary b, Serial1 f, Binary a) => Binary (Scope b f a) where
  put :: Scope b f a -> Put
put = (b -> Put) -> (a -> Put) -> Scope b f a -> Put
forall (f :: * -> *) (m :: * -> *) b v.
(Serial1 f, MonadPut m) =>
(b -> m ()) -> (v -> m ()) -> Scope b f v -> m ()
serializeScope b -> Put
forall t. Binary t => t -> Put
Binary.put a -> Put
forall t. Binary t => t -> Put
Binary.put
  get :: Get (Scope b f a)
get = Get b -> Get a -> Get (Scope b f a)
forall (f :: * -> *) (m :: * -> *) b v.
(Serial1 f, MonadGet m) =>
m b -> m v -> m (Scope b f v)
deserializeScope Get b
forall t. Binary t => Get t
Binary.get Get a
forall t. Binary t => Get t
Binary.get

instance (Serialize b, Serial1 f, Serialize a) => Serialize (Scope b f a) where
  put :: Putter (Scope b f a)
put = (b -> PutM ()) -> (a -> PutM ()) -> Putter (Scope b f a)
forall (f :: * -> *) (m :: * -> *) b v.
(Serial1 f, MonadPut m) =>
(b -> m ()) -> (v -> m ()) -> Scope b f v -> m ()
serializeScope b -> PutM ()
forall t. Serialize t => Putter t
Serialize.put a -> PutM ()
forall t. Serialize t => Putter t
Serialize.put
  get :: Get (Scope b f a)
get = Get b -> Get a -> Get (Scope b f a)
forall (f :: * -> *) (m :: * -> *) b v.
(Serial1 f, MonadGet m) =>
m b -> m v -> m (Scope b f v)
deserializeScope Get b
forall t. Serialize t => Get t
Serialize.get Get a
forall t. Serialize t => Get t
Serialize.get

#ifdef __GLASGOW_HASKELL__
deriving instance (Typeable b, Typeable f, Data a, Data (f (Var b (f a)))) => Data (Scope b f a)
#endif