{-# LANGUAGE CPP #-}
#ifdef __GLASGOW_HASKELL__
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE Trustworthy #-}
#endif

-----------------------------------------------------------------------------
-- |
-- Copyright   :  (C) 2012 Edward Kmett
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
-- Stability   :  experimental
-- Portability :  portable
--
-- The problem with locally nameless approaches is that original names are
-- often useful for error reporting, or to allow for the user in an interactive
-- theorem prover to convey some hint about the domain. A @'Name' n b@ is a value
-- @b@ supplemented with a (discardable) name that may be useful for error
-- reporting purposes. In particular, this name does not participate in
-- comparisons for equality.
--
-- This module is /not/ exported from "Bound" by default. You need to explicitly
-- import it, due to the fact that 'Name' is a pretty common term in other
-- people's code.
----------------------------------------------------------------------------
module Bound.Name
  ( Name(..)
  , _Name
  , name
  , abstractName
  , abstract1Name
  , abstractEitherName
  , instantiateName
  , instantiate1Name
  , instantiateEitherName
  ) where

import Bound.Scope
import Bound.Var
import Control.Comonad
import Control.DeepSeq
import Control.Monad (liftM, liftM2)
import Data.Bifunctor
import Data.Bifoldable
import qualified Data.Binary as Binary
import Data.Binary (Binary)
import Data.Bitraversable
import Data.Bytes.Serial
import Data.Functor.Classes
#ifdef __GLASGOW_HASKELL__
import Data.Data
import GHC.Generics
#endif
import Data.Hashable (Hashable(..))
import Data.Hashable.Lifted (Hashable1(..), Hashable2(..))
import Data.Profunctor
import qualified Data.Serialize as Serialize
import Data.Serialize (Serialize)

-------------------------------------------------------------------------------
-- Names
-------------------------------------------------------------------------------

-- |
-- We track the choice of 'Name' @n@ as a forgettable property that does /not/ affect
-- the result of ('==') or 'compare'.
--
-- To compare names rather than values, use @('Data.Function.on' 'compare' 'name')@ instead.
data Name n b = Name n b deriving
  ( Int -> Name n b -> ShowS
[Name n b] -> ShowS
Name n b -> String
(Int -> Name n b -> ShowS)
-> (Name n b -> String) -> ([Name n b] -> ShowS) -> Show (Name n b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall n b. (Show n, Show b) => Int -> Name n b -> ShowS
forall n b. (Show n, Show b) => [Name n b] -> ShowS
forall n b. (Show n, Show b) => Name n b -> String
showList :: [Name n b] -> ShowS
$cshowList :: forall n b. (Show n, Show b) => [Name n b] -> ShowS
show :: Name n b -> String
$cshow :: forall n b. (Show n, Show b) => Name n b -> String
showsPrec :: Int -> Name n b -> ShowS
$cshowsPrec :: forall n b. (Show n, Show b) => Int -> Name n b -> ShowS
Show
  , ReadPrec [Name n b]
ReadPrec (Name n b)
Int -> ReadS (Name n b)
ReadS [Name n b]
(Int -> ReadS (Name n b))
-> ReadS [Name n b]
-> ReadPrec (Name n b)
-> ReadPrec [Name n b]
-> Read (Name n b)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall n b. (Read n, Read b) => ReadPrec [Name n b]
forall n b. (Read n, Read b) => ReadPrec (Name n b)
forall n b. (Read n, Read b) => Int -> ReadS (Name n b)
forall n b. (Read n, Read b) => ReadS [Name n b]
readListPrec :: ReadPrec [Name n b]
$creadListPrec :: forall n b. (Read n, Read b) => ReadPrec [Name n b]
readPrec :: ReadPrec (Name n b)
$creadPrec :: forall n b. (Read n, Read b) => ReadPrec (Name n b)
readList :: ReadS [Name n b]
$creadList :: forall n b. (Read n, Read b) => ReadS [Name n b]
readsPrec :: Int -> ReadS (Name n b)
$creadsPrec :: forall n b. (Read n, Read b) => Int -> ReadS (Name n b)
Read
#ifdef __GLASGOW_HASKELL__
  , Typeable (Name n b)
DataType
Constr
Typeable (Name n b)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Name n b -> c (Name n b))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Name n b))
-> (Name n b -> Constr)
-> (Name n b -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Name n b)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Name n b)))
-> ((forall b. Data b => b -> b) -> Name n b -> Name n b)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Name n b -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Name n b -> r)
-> (forall u. (forall d. Data d => d -> u) -> Name n b -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Name n b -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Name n b -> m (Name n b))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Name n b -> m (Name n b))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Name n b -> m (Name n b))
-> Data (Name n b)
Name n b -> DataType
Name n b -> Constr
(forall b. Data b => b -> b) -> Name n b -> Name n b
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Name n b -> c (Name n b)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Name n b)
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Name n b))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Name n b -> u
forall u. (forall d. Data d => d -> u) -> Name n b -> [u]
forall n b. (Data n, Data b) => Typeable (Name n b)
forall n b. (Data n, Data b) => Name n b -> DataType
forall n b. (Data n, Data b) => Name n b -> Constr
forall n b.
(Data n, Data b) =>
(forall b. Data b => b -> b) -> Name n b -> Name n b
forall n b u.
(Data n, Data b) =>
Int -> (forall d. Data d => d -> u) -> Name n b -> u
forall n b u.
(Data n, Data b) =>
(forall d. Data d => d -> u) -> Name n b -> [u]
forall n b r r'.
(Data n, Data b) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Name n b -> r
forall n b r r'.
(Data n, Data b) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Name n b -> r
forall n b (m :: * -> *).
(Data n, Data b, Monad m) =>
(forall d. Data d => d -> m d) -> Name n b -> m (Name n b)
forall n b (m :: * -> *).
(Data n, Data b, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Name n b -> m (Name n b)
forall n b (c :: * -> *).
(Data n, Data b) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Name n b)
forall n b (c :: * -> *).
(Data n, Data b) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Name n b -> c (Name n b)
forall n b (t :: * -> *) (c :: * -> *).
(Data n, Data b, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Name n b))
forall n b (t :: * -> * -> *) (c :: * -> *).
(Data n, Data b, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Name n b))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Name n b -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Name n b -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Name n b -> m (Name n b)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Name n b -> m (Name n b)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Name n b)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Name n b -> c (Name n b)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Name n b))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Name n b))
$cName :: Constr
$tName :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Name n b -> m (Name n b)
$cgmapMo :: forall n b (m :: * -> *).
(Data n, Data b, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Name n b -> m (Name n b)
gmapMp :: (forall d. Data d => d -> m d) -> Name n b -> m (Name n b)
$cgmapMp :: forall n b (m :: * -> *).
(Data n, Data b, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Name n b -> m (Name n b)
gmapM :: (forall d. Data d => d -> m d) -> Name n b -> m (Name n b)
$cgmapM :: forall n b (m :: * -> *).
(Data n, Data b, Monad m) =>
(forall d. Data d => d -> m d) -> Name n b -> m (Name n b)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Name n b -> u
$cgmapQi :: forall n b u.
(Data n, Data b) =>
Int -> (forall d. Data d => d -> u) -> Name n b -> u
gmapQ :: (forall d. Data d => d -> u) -> Name n b -> [u]
$cgmapQ :: forall n b u.
(Data n, Data b) =>
(forall d. Data d => d -> u) -> Name n b -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Name n b -> r
$cgmapQr :: forall n b r r'.
(Data n, Data b) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Name n b -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Name n b -> r
$cgmapQl :: forall n b r r'.
(Data n, Data b) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Name n b -> r
gmapT :: (forall b. Data b => b -> b) -> Name n b -> Name n b
$cgmapT :: forall n b.
(Data n, Data b) =>
(forall b. Data b => b -> b) -> Name n b -> Name n b
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Name n b))
$cdataCast2 :: forall n b (t :: * -> * -> *) (c :: * -> *).
(Data n, Data b, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Name n b))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Name n b))
$cdataCast1 :: forall n b (t :: * -> *) (c :: * -> *).
(Data n, Data b, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Name n b))
dataTypeOf :: Name n b -> DataType
$cdataTypeOf :: forall n b. (Data n, Data b) => Name n b -> DataType
toConstr :: Name n b -> Constr
$ctoConstr :: forall n b. (Data n, Data b) => Name n b -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Name n b)
$cgunfold :: forall n b (c :: * -> *).
(Data n, Data b) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Name n b)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Name n b -> c (Name n b)
$cgfoldl :: forall n b (c :: * -> *).
(Data n, Data b) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Name n b -> c (Name n b)
$cp1Data :: forall n b. (Data n, Data b) => Typeable (Name n b)
Data
  , (forall x. Name n b -> Rep (Name n b) x)
-> (forall x. Rep (Name n b) x -> Name n b) -> Generic (Name n b)
forall x. Rep (Name n b) x -> Name n b
forall x. Name n b -> Rep (Name n b) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall n b x. Rep (Name n b) x -> Name n b
forall n b x. Name n b -> Rep (Name n b) x
$cto :: forall n b x. Rep (Name n b) x -> Name n b
$cfrom :: forall n b x. Name n b -> Rep (Name n b) x
Generic
  , (forall a. Name n a -> Rep1 (Name n) a)
-> (forall a. Rep1 (Name n) a -> Name n a) -> Generic1 (Name n)
forall a. Rep1 (Name n) a -> Name n a
forall a. Name n a -> Rep1 (Name n) a
forall n a. Rep1 (Name n) a -> Name n a
forall n a. Name n a -> Rep1 (Name n) a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cto1 :: forall n a. Rep1 (Name n) a -> Name n a
$cfrom1 :: forall n a. Name n a -> Rep1 (Name n) a
Generic1
#endif
  )

-- | Extract the 'name'.
name :: Name n b -> n
name :: Name n b -> n
name (Name n
n b
_) = n
n
{-# INLINE name #-}

-- |
--
-- This provides an 'Iso' that can be used to access the parts of a 'Name'.
--
-- @
-- '_Name' :: Iso ('Name' n a) ('Name' m b) (n, a) (m, b)
-- @
_Name :: (Profunctor p, Functor f) => p (n, a) (f (m,b)) -> p (Name n a) (f (Name m b))
_Name :: p (n, a) (f (m, b)) -> p (Name n a) (f (Name m b))
_Name = (Name n a -> (n, a))
-> (f (m, b) -> f (Name m b))
-> p (n, a) (f (m, b))
-> p (Name n a) (f (Name m b))
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (\(Name n
n a
a) -> (n
n, a
a)) (((m, b) -> Name m b) -> f (m, b) -> f (Name m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((m -> b -> Name m b) -> (m, b) -> Name m b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry m -> b -> Name m b
forall n b. n -> b -> Name n b
Name))
{-# INLINE _Name #-}

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

instance Eq b => Eq (Name n b) where
  Name n
_ b
a == :: Name n b -> Name n b -> Bool
== Name n
_ b
b = b
a b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
b
  {-# INLINE (==) #-}

instance Hashable2 Name where
  liftHashWithSalt2 :: (Int -> a -> Int) -> (Int -> b -> Int) -> Int -> Name a b -> Int
liftHashWithSalt2 Int -> a -> Int
_ Int -> b -> Int
h Int
s (Name a
_ b
a) = Int -> b -> Int
h Int
s b
a
  {-# INLINE liftHashWithSalt2 #-}

instance Hashable1 (Name n) where
  liftHashWithSalt :: (Int -> a -> Int) -> Int -> Name n a -> Int
liftHashWithSalt Int -> a -> Int
h Int
s (Name n
_ a
a) = Int -> a -> Int
h Int
s a
a
  {-# INLINE liftHashWithSalt #-}

instance Hashable a => Hashable (Name n a) where
  hashWithSalt :: Int -> Name n a -> Int
hashWithSalt Int
m (Name n
_ a
a) = Int -> a -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
m a
a
  {-# INLINE hashWithSalt #-}

instance Ord b => Ord (Name n b) where
  Name n
_ b
a compare :: Name n b -> Name n b -> Ordering
`compare` Name n
_ b
b = b -> b -> Ordering
forall a. Ord a => a -> a -> Ordering
compare b
a b
b
  {-# INLINE compare #-}

instance Functor (Name n) where
  fmap :: (a -> b) -> Name n a -> Name n b
fmap a -> b
f (Name n
n a
a) = n -> b -> Name n b
forall n b. n -> b -> Name n b
Name n
n (a -> b
f a
a)
  {-# INLINE fmap #-}

instance Foldable (Name n) where
  foldMap :: (a -> m) -> Name n a -> m
foldMap a -> m
f (Name n
_ a
a) = a -> m
f a
a
  {-# INLINE foldMap #-}

instance Traversable (Name n) where
  traverse :: (a -> f b) -> Name n a -> f (Name n b)
traverse a -> f b
f (Name n
n a
a) = n -> b -> Name n b
forall n b. n -> b -> Name n b
Name n
n (b -> Name n b) -> f b -> f (Name n b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
a
  {-# INLINE traverse #-}

instance Bifunctor Name where
  bimap :: (a -> b) -> (c -> d) -> Name a c -> Name b d
bimap a -> b
f c -> d
g (Name a
n c
a) = b -> d -> Name b d
forall n b. n -> b -> Name n b
Name (a -> b
f a
n) (c -> d
g c
a)
  {-# INLINE bimap #-}

instance Bifoldable Name where
  bifoldMap :: (a -> m) -> (b -> m) -> Name a b -> m
bifoldMap a -> m
f b -> m
g (Name a
n b
a) = a -> m
f a
n m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` b -> m
g b
a
  {-# INLINE bifoldMap #-}

instance Bitraversable Name where
  bitraverse :: (a -> f c) -> (b -> f d) -> Name a b -> f (Name c d)
bitraverse a -> f c
f b -> f d
g (Name a
n b
a) = c -> d -> Name c d
forall n b. n -> b -> Name n b
Name (c -> d -> Name c d) -> f c -> f (d -> Name c d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f c
f a
n f (d -> Name c d) -> f d -> f (Name c d)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> f d
g b
a
  {-# INLINE bitraverse #-}

instance Comonad (Name n) where
  extract :: Name n a -> a
extract (Name n
_ a
b) = a
b
  {-# INLINE extract #-}
  extend :: (Name n a -> b) -> Name n a -> Name n b
extend Name n a -> b
f w :: Name n a
w@(Name n
n a
_) = n -> b -> Name n b
forall n b. n -> b -> Name n b
Name n
n (Name n a -> b
f Name n a
w)
  {-# INLINE extend #-}

instance Eq2 Name where
  liftEq2 :: (a -> b -> Bool)
-> (c -> d -> Bool) -> Name a c -> Name b d -> Bool
liftEq2 a -> b -> Bool
_ c -> d -> Bool
g (Name a
_ c
b) (Name b
_ d
d) = c -> d -> Bool
g c
b d
d

instance Ord2 Name where
  liftCompare2 :: (a -> b -> Ordering)
-> (c -> d -> Ordering) -> Name a c -> Name b d -> Ordering
liftCompare2 a -> b -> Ordering
_ c -> d -> Ordering
g (Name a
_ c
b) (Name b
_ d
d) = c -> d -> Ordering
g c
b d
d

instance Show2 Name where
  liftShowsPrec2 :: (Int -> a -> ShowS)
-> ([a] -> ShowS)
-> (Int -> b -> ShowS)
-> ([b] -> ShowS)
-> Int
-> Name a b
-> ShowS
liftShowsPrec2 Int -> a -> ShowS
f [a] -> ShowS
_ Int -> b -> ShowS
h [b] -> ShowS
_ Int
d (Name a
a b
b) = (Int -> a -> ShowS)
-> (Int -> b -> ShowS) -> String -> Int -> a -> b -> ShowS
forall a b.
(Int -> a -> ShowS)
-> (Int -> b -> ShowS) -> String -> Int -> a -> b -> ShowS
showsBinaryWith Int -> a -> ShowS
f Int -> b -> ShowS
h String
"Name" Int
d a
a b
b

instance Read2 Name where
  liftReadsPrec2 :: (Int -> ReadS a)
-> ReadS [a]
-> (Int -> ReadS b)
-> ReadS [b]
-> Int
-> ReadS (Name a b)
liftReadsPrec2 Int -> ReadS a
f ReadS [a]
_ Int -> ReadS b
h ReadS [b]
_ = (String -> ReadS (Name a b)) -> Int -> ReadS (Name a b)
forall a. (String -> ReadS a) -> Int -> ReadS a
readsData ((String -> ReadS (Name a b)) -> Int -> ReadS (Name a b))
-> (String -> ReadS (Name a b)) -> Int -> ReadS (Name a b)
forall a b. (a -> b) -> a -> b
$ (Int -> ReadS a)
-> (Int -> ReadS b)
-> String
-> (a -> b -> Name a b)
-> String
-> ReadS (Name a b)
forall a b t.
(Int -> ReadS a)
-> (Int -> ReadS b) -> String -> (a -> b -> t) -> String -> ReadS t
readsBinaryWith Int -> ReadS a
f Int -> ReadS b
h String
"Name" a -> b -> Name a b
forall n b. n -> b -> Name n b
Name

instance Eq1 (Name b) where
  liftEq :: (a -> b -> Bool) -> Name b a -> Name b b -> Bool
liftEq a -> b -> Bool
f (Name b
_ a
b) (Name b
_ b
d) = a -> b -> Bool
f a
b b
d

instance Ord1 (Name b) where
  liftCompare :: (a -> b -> Ordering) -> Name b a -> Name b b -> Ordering
liftCompare a -> b -> Ordering
f (Name b
_ a
b) (Name b
_ b
d) = a -> b -> Ordering
f a
b b
d

instance Show b => Show1 (Name b) where
  liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Name b a -> ShowS
liftShowsPrec Int -> a -> ShowS
f [a] -> ShowS
_ Int
d (Name b
a a
b) = (Int -> b -> ShowS)
-> (Int -> a -> ShowS) -> String -> Int -> b -> a -> ShowS
forall a b.
(Int -> a -> ShowS)
-> (Int -> b -> ShowS) -> String -> Int -> a -> b -> ShowS
showsBinaryWith Int -> b -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int -> a -> ShowS
f String
"Name" Int
d b
a a
b

instance Read b => Read1 (Name b) where
  liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (Name b a)
liftReadsPrec Int -> ReadS a
f ReadS [a]
_ = (String -> ReadS (Name b a)) -> Int -> ReadS (Name b a)
forall a. (String -> ReadS a) -> Int -> ReadS a
readsData ((String -> ReadS (Name b a)) -> Int -> ReadS (Name b a))
-> (String -> ReadS (Name b a)) -> Int -> ReadS (Name b a)
forall a b. (a -> b) -> a -> b
$ (Int -> ReadS b)
-> (Int -> ReadS a)
-> String
-> (b -> a -> Name b a)
-> String
-> ReadS (Name b a)
forall a b t.
(Int -> ReadS a)
-> (Int -> ReadS b) -> String -> (a -> b -> t) -> String -> ReadS t
readsBinaryWith Int -> ReadS b
forall a. Read a => Int -> ReadS a
readsPrec Int -> ReadS a
f String
"Name" b -> a -> Name b a
forall n b. n -> b -> Name n b
Name

instance Serial2 Name where
  serializeWith2 :: (a -> m ()) -> (b -> m ()) -> Name a b -> m ()
serializeWith2 a -> m ()
pb b -> m ()
pf (Name a
b b
a) = a -> m ()
pb a
b m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> b -> m ()
pf b
a
  {-# INLINE serializeWith2 #-}

  deserializeWith2 :: m a -> m b -> m (Name a b)
deserializeWith2 = (a -> b -> Name a b) -> m a -> m b -> m (Name a b)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 a -> b -> Name a b
forall n b. n -> b -> Name n b
Name
  {-# INLINE deserializeWith2 #-}

instance Serial b => Serial1 (Name b) where
  serializeWith :: (a -> m ()) -> Name b a -> m ()
serializeWith = (b -> m ()) -> (a -> m ()) -> Name b a -> m ()
forall (f :: * -> * -> *) (m :: * -> *) a b.
(Serial2 f, MonadPut m) =>
(a -> m ()) -> (b -> m ()) -> f a b -> m ()
serializeWith2 b -> m ()
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
serialize
  {-# INLINE serializeWith #-}
  deserializeWith :: m a -> m (Name b a)
deserializeWith = m b -> m a -> m (Name b a)
forall (f :: * -> * -> *) (m :: * -> *) a b.
(Serial2 f, MonadGet m) =>
m a -> m b -> m (f a b)
deserializeWith2 m b
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
deserialize
  {-# INLINE deserializeWith #-}

instance (Serial b, Serial a) => Serial (Name b a) where
  serialize :: Name b a -> m ()
serialize = (b -> m ()) -> (a -> m ()) -> Name b a -> m ()
forall (f :: * -> * -> *) (m :: * -> *) a b.
(Serial2 f, MonadPut m) =>
(a -> m ()) -> (b -> m ()) -> f a b -> m ()
serializeWith2 b -> m ()
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
serialize a -> m ()
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
serialize
  {-# INLINE serialize #-}
  deserialize :: m (Name b a)
deserialize = m b -> m a -> m (Name b a)
forall (f :: * -> * -> *) (m :: * -> *) a b.
(Serial2 f, MonadGet m) =>
m a -> m b -> m (f a b)
deserializeWith2 m b
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
deserialize m a
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
deserialize
  {-# INLINE deserialize #-}

instance (Binary b, Binary a) => Binary (Name b a) where
  put :: Name b a -> Put
put = (b -> Put) -> (a -> Put) -> Name b a -> Put
forall (f :: * -> * -> *) (m :: * -> *) a b.
(Serial2 f, MonadPut m) =>
(a -> m ()) -> (b -> m ()) -> f a b -> m ()
serializeWith2 b -> Put
forall t. Binary t => t -> Put
Binary.put a -> Put
forall t. Binary t => t -> Put
Binary.put
  get :: Get (Name b a)
get = Get b -> Get a -> Get (Name b a)
forall (f :: * -> * -> *) (m :: * -> *) a b.
(Serial2 f, MonadGet m) =>
m a -> m b -> m (f a b)
deserializeWith2 Get b
forall t. Binary t => Get t
Binary.get Get a
forall t. Binary t => Get t
Binary.get

instance (Serialize b, Serialize a) => Serialize (Name b a) where
  put :: Putter (Name b a)
put = (b -> PutM ()) -> (a -> PutM ()) -> Putter (Name b a)
forall (f :: * -> * -> *) (m :: * -> *) a b.
(Serial2 f, MonadPut m) =>
(a -> m ()) -> (b -> m ()) -> f a b -> m ()
serializeWith2 b -> PutM ()
forall t. Serialize t => Putter t
Serialize.put a -> PutM ()
forall t. Serialize t => Putter t
Serialize.put
  get :: Get (Name b a)
get = Get b -> Get a -> Get (Name b a)
forall (f :: * -> * -> *) (m :: * -> *) a b.
(Serial2 f, MonadGet m) =>
m a -> m b -> m (f a b)
deserializeWith2 Get b
forall t. Serialize t => Get t
Serialize.get Get a
forall t. Serialize t => Get t
Serialize.get

instance (NFData b, NFData a) => NFData (Name b a) where
  rnf :: Name b a -> ()
rnf (Name b
a a
b) = b -> ()
forall a. NFData a => a -> ()
rnf b
a () -> () -> ()
`seq` a -> ()
forall a. NFData a => a -> ()
rnf a
b

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

-- | Abstraction, capturing named bound variables.
abstractName :: Monad f => (a -> Maybe b) -> f a -> Scope (Name a b) f a
abstractName :: (a -> Maybe b) -> f a -> Scope (Name a b) f a
abstractName a -> Maybe b
f f a
t = f (Var (Name a b) (f a)) -> Scope (Name a b) f a
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope ((a -> Var (Name a b) (f a)) -> f a -> f (Var (Name a b) (f a))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM a -> Var (Name a b) (f 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 abstractName #-}

-- | Abstract over a single variable
abstract1Name :: (Monad f, Eq a) => a -> f a -> Scope (Name a ()) f a
abstract1Name :: a -> f a -> Scope (Name a ()) f a
abstract1Name a
a = (a -> Maybe ()) -> f a -> Scope (Name a ()) f a
forall (f :: * -> *) a b.
Monad f =>
(a -> Maybe b) -> f a -> Scope (Name a b) f a
abstractName (\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 abstract1Name #-}

-- | Capture some free variables in an expression to yield
-- a 'Scope' with named bound variables. Optionally change the
-- types of the remaining free variables.
abstractEitherName :: Monad f => (a -> Either b c) -> f a -> Scope (Name a b) f c
abstractEitherName :: (a -> Either b c) -> f a -> Scope (Name a b) f c
abstractEitherName a -> Either b c
f f a
e = f (Var (Name a b) (f c)) -> Scope (Name a b) f c
forall b (f :: * -> *) a. f (Var b (f a)) -> Scope b f a
Scope ((a -> Var (Name a b) (f c)) -> f a -> f (Var (Name a b) (f c))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM a -> Var (Name a b) (f c)
forall (m :: * -> *). Monad m => a -> Var (Name a b) (m c)
k f a
e) where
  k :: a -> Var (Name a b) (m c)
k a
y = case a -> Either b c
f a
y of
    Left b
z -> Name a b -> Var (Name a b) (m c)
forall b a. b -> Var b a
B (a -> b -> Name a b
forall n b. n -> b -> Name n b
Name a
y b
z)
    Right c
y' -> m c -> Var (Name a 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, but discarding (comonadic)
-- meta data, like its name
instantiateName :: (Monad f, Comonad n) => (b -> f a) -> Scope (n b) f a -> f a
instantiateName :: (b -> f a) -> Scope (n b) f a -> f a
instantiateName b -> f a
k Scope (n b) f a
e = Scope (n b) f a -> f (Var (n b) (f a))
forall b (f :: * -> *) a. Scope b f a -> f (Var b (f a))
unscope Scope (n b) f a
e f (Var (n b) (f a)) -> (Var (n b) (f a) -> f a) -> f a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Var (n b) (f a)
v -> case Var (n b) (f a)
v of
  B n b
b -> b -> f a
k (n b -> b
forall (w :: * -> *) a. Comonad w => w a -> a
extract n b
b)
  F f a
a -> f a
a
{-# INLINE instantiateName #-}

-- | Enter a 'Scope' that binds one (named) variable, instantiating it.
--
-- @'instantiate1Name' = 'instantiate1'@
instantiate1Name :: Monad f => f a -> Scope n f a -> f a
instantiate1Name :: f a -> Scope n f a -> f a
instantiate1Name = f a -> Scope n f a -> f a
forall (f :: * -> *) a n. Monad f => f a -> Scope n f a -> f a
instantiate1
{-# INLINE instantiate1Name #-}

instantiateEitherName :: (Monad f, Comonad n) => (Either b a -> f c) -> Scope (n b) f a -> f c
instantiateEitherName :: (Either b a -> f c) -> Scope (n b) f a -> f c
instantiateEitherName Either b a -> f c
k Scope (n b) f a
e = Scope (n b) f a -> f (Var (n b) (f a))
forall b (f :: * -> *) a. Scope b f a -> f (Var b (f a))
unscope Scope (n b) f a
e f (Var (n b) (f a)) -> (Var (n b) (f a) -> f c) -> f c
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Var (n b) (f a)
v -> case Var (n b) (f a)
v of
  B n b
b -> Either b a -> f c
k (b -> Either b a
forall a b. a -> Either a b
Left (n b -> b
forall (w :: * -> *) a. Comonad w => w a -> a
extract n b
b))
  F f a
a -> f a
a 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
k (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 instantiateEitherName #-}