2
{-# LANGUAGE DeriveDataTypeable #-}
3
{-# LANGUAGE DeriveFoldable #-}
4
{-# LANGUAGE DeriveFunctor #-}
5
{-# LANGUAGE DeriveTraversable #-}
6
{-# LANGUAGE FlexibleContexts #-}
7
{-# LANGUAGE FlexibleInstances #-}
2
{-# LANGUAGE DeriveDataTypeable #-}
3
{-# LANGUAGE DeriveFoldable #-}
4
{-# LANGUAGE DeriveFunctor #-}
5
{-# LANGUAGE DeriveTraversable #-}
6
{-# LANGUAGE FlexibleContexts #-}
7
{-# LANGUAGE FlexibleInstances #-}
8
8
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
9
{-# LANGUAGE TypeSynonymInstances #-}
10
11
{-| Abstract names carry unique identifiers and stuff.
29
30
import Agda.Syntax.Concrete.Name (IsNoName(..))
30
31
import qualified Agda.Syntax.Concrete.Name as C
32
import Agda.Utils.Fresh
33
-- import Agda.Utils.Function
34
import Agda.Utils.Pretty
33
35
import Agda.Utils.Size
34
36
import Agda.Utils.Suffix
36
#include "../../undefined.h"
38
#include "undefined.h"
37
39
import Agda.Utils.Impossible
39
41
-- | A name is a unique identifier and a suggestion for a concrete name. The
40
42
-- concrete name contains the source location (if any) of the name. The
41
43
-- source location of the binding site is also recorded.
42
data Name = Name { nameId :: NameId
43
, nameConcrete :: C.Name
44
, nameBindingSite :: Range
45
, nameFixity :: Fixity'
44
data Name = Name { nameId :: NameId
45
, nameConcrete :: C.Name
46
, nameBindingSite :: Range
47
, nameFixity :: Fixity'
47
49
deriving (Typeable)
49
51
-- | Qualified names are non-empty lists of names. Equality on qualified names
74
76
-- | Ambiguous qualified names. Used for overloaded constructors.
76
78
-- Invariant: All the names in the list must have the same concrete,
79
-- unqualified name. (This implies that they all have the same 'Range').
77
80
newtype AmbiguousQName = AmbQ { unAmbQ :: [QName] }
78
deriving (Typeable, HasRange, Show)
81
deriving (Typeable, Show)
80
83
-- | A module is anonymous if the qualification path ends in an underscore.
81
84
isAnonymousModuleName :: ModuleName -> Bool
172
174
toTopLevelModuleName :: ModuleName -> C.TopLevelModuleName
173
175
toTopLevelModuleName (MName []) = __IMPOSSIBLE__
174
toTopLevelModuleName (MName ms) = C.TopLevelModuleName (map show ms)
176
toTopLevelModuleName (MName ms) = C.TopLevelModuleName $ map (C.nameToRawName . nameConcrete) ms
176
178
qualifyM :: ModuleName -> ModuleName -> ModuleName
177
179
qualifyM m1 m2 = mnameFromList $ mnameToList m1 ++ mnameToList m2
180
182
qualifyQ m x = qnameFromList $ mnameToList m ++ qnameToList x
182
184
qualify :: ModuleName -> Name -> QName
183
qualify m x = qualifyQ m (qnameFromList [x])
187
-- | Convert a 'Name' to a 'QName' (add no module name).
188
qualify_ :: Name -> QName
189
qualify_ = qualify noModuleName
185
191
-- | Is the name an operator?
196
202
isInModule :: QName -> ModuleName -> Bool
197
203
isInModule q m = mnameToList m `isPrefixOf` qnameToList q
199
freshName :: (MonadState s m, HasFresh NameId s) => Range -> String -> m Name
202
return $ mkName r i s
204
freshNoName :: (MonadState s m, HasFresh NameId s) => Range -> m Name
207
return $ Name i (C.NoName noRange i) r defaultFixity'
209
freshNoName_ :: (MonadState s m, HasFresh NameId s) => m Name
210
freshNoName_ = freshNoName noRange
212
class FreshName a where
213
freshName_ :: (MonadState s m, HasFresh NameId s) => a -> m Name
215
instance FreshName (Range, String) where
216
freshName_ = uncurry freshName
218
instance FreshName String where
219
freshName_ = freshName noRange
221
instance FreshName Range where
222
freshName_ = freshNoName
224
instance FreshName () where
225
freshName_ () = freshNoName_
227
205
-- | Get the next version of the concrete name. For instance, @nextName "x" = "x₁"@.
228
206
-- The name must not be a 'NoName'.
229
207
nextName :: Name -> Name
230
208
nextName x = x { nameConcrete = C.Name noRange $ nextSuf ps }
232
C.Name _ ps = nameConcrete x
233
-- NoName cannot appear here
234
nextSuf [C.Id s] = [C.Id $ nextStr s]
235
nextSuf [C.Id s, C.Hole] = [C.Id $ nextStr s, C.Hole]
236
nextSuf (p : ps) = p : nextSuf ps
237
nextSuf [] = __IMPOSSIBLE__
238
nextStr s = case suffixView s of
239
(s0, suf) -> addSuffix s0 (nextSuffix suf)
210
C.Name _ ps = nameConcrete x
211
-- NoName cannot appear here
212
nextSuf [C.Id s] = [C.Id $ nextStr s]
213
nextSuf [C.Id s, C.Hole] = [C.Id $ nextStr s, C.Hole]
214
nextSuf (p : ps) = p : nextSuf ps
215
nextSuf [] = __IMPOSSIBLE__
216
nextStr s = case suffixView s of
217
(s0, suf) -> addSuffix s0 (nextSuffix suf)
241
219
------------------------------------------------------------------------
242
220
-- * Important instances: Eq, Ord, Hashable
277
254
-- * Show instances
278
255
------------------------------------------------------------------------
257
-- | Only use this @show@ function in debugging! To convert an
258
-- abstract 'Name' into a string use @prettyShow@.
280
259
instance Show Name where
281
show x = show (nameConcrete x) -- ++ "|" ++ show (nameId x)
260
-- Andreas, 2014-10-02: Reverted to nice printing.
261
-- Reason: I do not have time just now to properly fix the
262
-- use of Show Name for pretty printing everywhere, e.g. in
263
-- the Epic backend. But I want to push the fix for Issue 836 now.
264
show n = show (nameConcrete n)
265
-- show n = show (nameConcrete n) ++ "^" ++ show (nameId n)
266
-- show n = applyWhen (isNoName n) (++ show (nameId n)) $ show (nameConcrete n)
268
-- | Only use this @show@ function in debugging! To convert an
269
-- abstract 'ModuleName' into a string use @prettyShow@.
283
270
instance Show ModuleName where
284
271
show m = concat $ intersperse "." $ map show $ mnameToList m
273
-- | Only use this @show@ function in debugging! To convert an
274
-- abstract 'QName' into a string use @prettyShow@.
286
275
instance Show QName where
287
276
show q = concat $ intersperse "." $ map show $ qnameToList q
289
278
------------------------------------------------------------------------
279
-- * Pretty instances
280
------------------------------------------------------------------------
282
instance Pretty Name where
283
pretty = pretty . nameConcrete
285
instance Pretty ModuleName where
286
pretty = hcat . punctuate (text ".") . map pretty . mnameToList
288
instance Pretty QName where
289
pretty = hcat . punctuate (text ".") . map pretty . qnameToList
291
------------------------------------------------------------------------
290
292
-- * Range instances
291
293
------------------------------------------------------------------------
302
304
instance HasRange QName where
303
305
getRange q = getRange (qnameModule q, qnameName q)
307
-- | The range of an @AmbiguousQName@ is the range of any of its
308
-- disambiguations (they are the same concrete name).
309
instance HasRange AmbiguousQName where
310
getRange (AmbQ []) = noRange
311
getRange (AmbQ (c:_)) = getRange c
307
315
instance SetRange Name where
323
331
-- An experiment: what happens if we preserve
324
332
-- the range of the binding site, but kill all
325
333
-- other ranges before serialization?
326
-- , nameBindingSite = noRange
334
-- Andreas, Makoto, 2014-10-18 AIM XX
335
-- Kill all ranges in signature, including nameBindingSite.
336
, nameBindingSite = noRange
329
339
instance KillRange ModuleName where
added
removed
src/full/Agda/Syntax/Abstract/Name.hs
