{-# 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
#if !MIN_VERSION_base(4,8,0)
import Control.Applicative
import Data.Foldable
import Data.Monoid
import Data.Traversable
#endif
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
  , 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
# if __GLASGOW_HASKELL__ >= 706
  , (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
#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 #-}

#if MIN_VERSION_transformers(0,5,0) || !MIN_VERSION_transformers(0,4,0)

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

#else

instance Eq1   (Name b) where eq1 = (==)
instance Ord1  (Name b) where compare1 = compare
instance Show b => Show1 (Name b) where showsPrec1 = showsPrec
instance Read b => Read1 (Name b) where readsPrec1 = readsPrec

--instance Eq2 Name   where eq2 = (==)
--instance Ord2 Name  where compare2   = compare
--instance Show2 Name where showsPrec2 = showsPrec
--instance Read2 Name where readsPrec2  = readsPrec

#endif

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 #-}