/
Name.hs
239 lines (205 loc) · 7.09 KB
/
Name.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
{-# LANGUAGE CPP #-}
#ifdef __GLASGOW_HASKELL__
{-# LANGUAGE DeriveDataTypeable #-}
# if __GLASGOW_HASKELL__ >= 704
{-# LANGUAGE DeriveGeneric #-}
# endif
#endif
-----------------------------------------------------------------------------
-- |
-- Module : Bound.Name
-- 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
, instantiateName
, instantiate1Name
) where
import Bound.Scope
import Bound.Var
import Control.Applicative
import Control.Comonad
import Control.Monad (liftM, liftM2)
import Data.Foldable
import Data.Traversable
import Data.Monoid
import Data.Bifunctor
import Data.Bifoldable
import qualified Data.Binary as Binary
import Data.Binary (Binary)
import Data.Bitraversable
import Data.Bytes.Serial
#ifdef __GLASGOW_HASKELL__
import Data.Data
# if __GLASGOW_HASKELL__ >= 704
import GHC.Generics
# endif
#endif
import Data.Hashable
import Data.Hashable.Extras
import Data.Profunctor
import qualified Data.Serialize as Serialize
import Data.Serialize (Serialize)
import Prelude.Extras
-------------------------------------------------------------------------------
-- 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
( Show
, Read
#ifdef __GLASGOW_HASKELL__
, Typeable
, Data
# if __GLASGOW_HASKELL__ >= 704
, Generic
# endif
#endif
)
-- | Extract the 'name'.
name :: Name n b -> n
name (Name 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 = dimap (\(Name n a) -> (n, a)) (fmap (uncurry Name))
{-# INLINE _Name #-}
-------------------------------------------------------------------------------
-- Instances
-------------------------------------------------------------------------------
instance Eq b => Eq (Name n b) where
Name _ a == Name _ b = a == b
{-# INLINE (==) #-}
instance Hashable2 Name where
hashWithSalt2 m (Name _ a) = hashWithSalt m a
{-# INLINE hashWithSalt2 #-}
instance Hashable1 (Name n) where
hashWithSalt1 m (Name _ a) = hashWithSalt m a
{-# INLINE hashWithSalt1 #-}
instance Hashable a => Hashable (Name n a) where
hashWithSalt m (Name _ a) = hashWithSalt m a
{-# INLINE hashWithSalt #-}
instance Ord b => Ord (Name n b) where
Name _ a `compare` Name _ b = compare a b
{-# INLINE compare #-}
instance Functor (Name n) where
fmap f (Name n a) = Name n (f a)
{-# INLINE fmap #-}
instance Foldable (Name n) where
foldMap f (Name _ a) = f a
{-# INLINE foldMap #-}
instance Traversable (Name n) where
traverse f (Name n a) = Name n <$> f a
{-# INLINE traverse #-}
instance Bifunctor Name where
bimap f g (Name n a) = Name (f n) (g a)
{-# INLINE bimap #-}
instance Bifoldable Name where
bifoldMap f g (Name n a) = f n `mappend` g a
{-# INLINE bifoldMap #-}
instance Bitraversable Name where
bitraverse f g (Name n a) = Name <$> f n <*> g a
{-# INLINE bitraverse #-}
instance Comonad (Name n) where
extract (Name _ b) = b
{-# INLINE extract #-}
extend f w@(Name n _) = Name n (f w)
{-# INLINE extend #-}
instance Eq1 (Name b) where
(==#) = (==)
{-# INLINE (==#) #-}
instance Ord1 (Name b) where
compare1 = compare
{-# INLINE compare1 #-}
instance Show b => Show1 (Name b) where showsPrec1 = showsPrec
instance Read b => Read1 (Name b) where readsPrec1 = readsPrec
-- these are slightly too restrictive, but still safe
instance Eq2 Name where
(==##) = (==)
{-# INLINE (==##) #-}
instance Ord2 Name where
compare2 = compare
{-# INLINE compare2 #-}
instance Show2 Name where showsPrec2 = showsPrec
instance Read2 Name where readsPrec2 = readsPrec
instance Serial2 Name where
serializeWith2 pb pf (Name b a) = pb b >> pf a
{-# INLINE serializeWith2 #-}
deserializeWith2 gb gf = liftM2 Name gb gf
{-# INLINE deserializeWith2 #-}
instance Serial b => Serial1 (Name b) where
serializeWith = serializeWith2 serialize
{-# INLINE serializeWith #-}
deserializeWith = deserializeWith2 deserialize
{-# INLINE deserializeWith #-}
instance (Serial b, Serial a) => Serial (Name b a) where
serialize = serializeWith2 serialize serialize
{-# INLINE serialize #-}
deserialize = deserializeWith2 deserialize deserialize
{-# INLINE deserialize #-}
instance (Binary b, Binary a) => Binary (Name b a) where
put = serializeWith2 Binary.put Binary.put
get = deserializeWith2 Binary.get Binary.get
instance (Serialize b, Serialize a) => Serialize (Name b a) where
put = serializeWith2 Serialize.put Serialize.put
get = deserializeWith2 Serialize.get Serialize.get
-------------------------------------------------------------------------------
-- Abstraction
-------------------------------------------------------------------------------
-- | Abstraction, capturing named bound variables.
abstractName :: Monad f => (a -> Maybe b) -> f a -> Scope (Name a b) f a
abstractName f t = Scope (liftM k t) where
k a = case f a of
Just b -> B (Name a b)
Nothing -> F (return a)
{-# INLINE abstractName #-}
-- | Abstract over a single variable
abstract1Name :: (Monad f, Eq a) => a -> f a -> Scope (Name a ()) f a
abstract1Name a = abstractName (\b -> if a == b then Just () else Nothing)
{-# INLINE abstract1Name #-}
-------------------------------------------------------------------------------
-- 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 k e = unscope e >>= \v -> case v of
B b -> k (extract b)
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 = instantiate1
{-# INLINE instantiate1Name #-}