← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/Syntax/Abstract/Name.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/Syntax/Abstract/Name.hs
1
 
{-# LANGUAGE CPP,
2
 
  DeriveDataTypeable, GeneralizedNewtypeDeriving,
3
 
  DeriveFunctor, DeriveFoldable, DeriveTraversable,
4
 
  FlexibleContexts #-}
 
1
{-# LANGUAGE CPP #-}
 
2
{-# LANGUAGE DeriveDataTypeable #-}
 
3
{-# LANGUAGE DeriveFoldable #-}
 
4
{-# LANGUAGE DeriveFunctor #-}
 
5
{-# LANGUAGE DeriveTraversable #-}
 
6
{-# LANGUAGE FlexibleContexts #-}
 
7
{-# LANGUAGE FlexibleInstances #-}
 
8
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
5
9
 
6
 
{-| Abstract names should carry unique identifiers and stuff. Not right now though.
 
10
{-| Abstract names carry unique identifiers and stuff.
7
11
-}
8
 
module Agda.Syntax.Abstract.Name where
 
12
module Agda.Syntax.Abstract.Name
 
13
  ( module Agda.Syntax.Abstract.Name
 
14
  , IsNoName(..)
 
15
  ) where
9
16
 
10
17
import Control.Monad.State
11
18
 
19
26
import Agda.Syntax.Position
20
27
import Agda.Syntax.Common
21
28
import Agda.Syntax.Fixity
 
29
import Agda.Syntax.Concrete.Name (IsNoName(..))
22
30
import qualified Agda.Syntax.Concrete.Name as C
23
31
 
24
32
import Agda.Utils.Fresh
25
33
import Agda.Utils.Size
26
34
import Agda.Utils.Suffix
27
35
 
28
 
import Agda.Syntax.Notation
29
 
 
30
36
#include "../../undefined.h"
31
37
import Agda.Utils.Impossible
32
38
 
72
78
newtype AmbiguousQName = AmbQ { unAmbQ :: [QName] }
73
79
  deriving (Typeable, HasRange, Show)
74
80
 
75
 
instance HasRange ModuleName where
76
 
  getRange (MName []) = noRange
77
 
  getRange (MName xs) = getRange xs
78
 
 
79
81
-- | A module is anonymous if the qualification path ends in an underscore.
80
82
isAnonymousModuleName :: ModuleName -> Bool
81
83
isAnonymousModuleName (MName []) = False
82
 
isAnonymousModuleName (MName ms) = C.isNoName $ nameConcrete $ last ms
 
84
isAnonymousModuleName (MName ms) = isNoName $ last ms
83
85
 
84
86
-- | Sets the ranges of the individual names in the module name to
85
87
-- match those of the corresponding concrete names. If the concrete
118
120
noModuleName :: ModuleName
119
121
noModuleName = mnameFromList []
120
122
 
121
 
 
122
 
mkName :: Range -> NameId -> String -> Name
123
 
mkName r i s = Name i (C.Name noRange (parseName s)) r defaultFixity'
124
 
  where
125
 
    parseName ""      = []
126
 
    parseName ('_':s) = C.Hole : parseName s
127
 
    parseName s = case break (== '_') s of
128
 
      (s0, s1)  -> C.Id s0 : parseName s1
129
 
 
130
 
mkName_ :: NameId -> String -> Name
131
 
mkName_ = mkName noRange
 
123
-- | Make a 'Name' from some kind of string.
 
124
class MkName a where
 
125
  -- | The 'Range' sets the /definition site/ of the name, not the use site.
 
126
  mkName :: Range -> NameId -> a -> Name
 
127
 
 
128
  mkName_ :: NameId -> a -> Name
 
129
  mkName_ = mkName noRange
 
130
 
 
131
instance MkName String where
 
132
  mkName r i s = Name i (C.Name noRange (C.stringNameParts s)) r defaultFixity'
 
133
 
132
134
 
133
135
qnameToList :: QName -> [Name]
134
136
qnameToList (QName m x) = mnameToList m ++ [x]
201
201
  i <- fresh
202
202
  return $ mkName r i s
203
203
 
204
 
freshName_ :: (MonadState s m, HasFresh NameId s) => String -> m Name
205
 
freshName_ = freshName noRange
206
 
 
207
204
freshNoName :: (MonadState s m, HasFresh NameId s) => Range -> m Name
208
205
freshNoName r =
209
206
    do  i <- fresh
212
209
freshNoName_ :: (MonadState s m, HasFresh NameId s) => m Name
213
210
freshNoName_ = freshNoName noRange
214
211
 
 
212
-- | Create a fresh name from @a@.
 
213
class FreshName a where
 
214
  freshName_ :: (MonadState s m, HasFresh NameId s) => a -> m Name
 
215
 
 
216
instance FreshName (Range, String) where
 
217
  freshName_ = uncurry freshName
 
218
 
 
219
instance FreshName String where
 
220
  freshName_ = freshName noRange
 
221
 
 
222
instance FreshName Range where
 
223
  freshName_ = freshNoName
 
224
 
 
225
instance FreshName () where
 
226
  freshName_ () = freshNoName_
 
227
 
215
228
-- | Get the next version of the concrete name. For instance, @nextName "x" = "x₁"@.
216
229
--   The name must not be a 'NoName'.
217
230
nextName :: Name -> Name
226
239
        nextStr s = case suffixView s of
227
240
            (s0, suf) -> addSuffix s0 (nextSuffix suf)
228
241
 
229
 
instance Show NameId where
230
 
  show (NameId x i) = show x ++ "@" ++ show i
 
242
------------------------------------------------------------------------
 
243
-- * Important instances: Eq, Ord, Hashable
 
244
--
 
245
--   For the identity and comparing of names, only the 'NameId' matters!
 
246
------------------------------------------------------------------------
231
247
 
232
248
instance Eq Name where
233
 
  x == y  = nameId x == nameId y
 
249
  (==) = (==) `on` nameId
234
250
 
235
251
instance Ord Name where
236
 
  compare x y = compare (nameId x) (nameId y)
237
 
 
238
 
instance Show Name where
239
 
  show x = show (nameConcrete x) -- ++ "|" ++ show (nameId x)
 
252
  compare = compare `on` nameId
240
253
 
241
254
instance Hashable Name where
242
255
  {-# INLINE hashWithSalt #-}
243
 
  hashWithSalt salt = (hashWithSalt salt) . nameId
244
 
 
245
 
instance Show QName where
246
 
  show q = concat $ intersperse "." $ map show $ qnameToList q
247
 
 
248
 
instance Show ModuleName where
249
 
  show m = concat $ intersperse "." $ map show $ mnameToList m
 
256
  hashWithSalt salt = hashWithSalt salt . nameId
250
257
 
251
258
instance Eq QName where
252
259
  (==) = (==) `on` qnameName
256
263
 
257
264
instance Hashable QName where
258
265
  {-# INLINE hashWithSalt #-}
259
 
  hashWithSalt salt = (hashWithSalt salt) . qnameName
 
266
  hashWithSalt salt = hashWithSalt salt . qnameName
 
267
 
 
268
------------------------------------------------------------------------
 
269
-- * IsNoName instances (checking for "_")
 
270
------------------------------------------------------------------------
 
271
 
 
272
-- | An abstract name is empty if its concrete name is empty.
 
273
instance IsNoName Name where
 
274
  isNoName = isNoName . nameConcrete
 
275
 
 
276
------------------------------------------------------------------------
 
277
-- * Show instances
 
278
------------------------------------------------------------------------
 
279
 
 
280
instance Show Name where
 
281
  show x = show (nameConcrete x) -- ++ "|" ++ show (nameId x)
 
282
 
 
283
instance Show ModuleName where
 
284
  show m = concat $ intersperse "." $ map show $ mnameToList m
 
285
 
 
286
instance Show QName where
 
287
  show q = concat $ intersperse "." $ map show $ qnameToList q
 
288
 
 
289
------------------------------------------------------------------------
 
290
-- * Range instances
 
291
------------------------------------------------------------------------
 
292
 
 
293
-- ** HasRange
260
294
 
261
295
instance HasRange Name where
262
296
  getRange = getRange . nameConcrete
263
297
 
 
298
instance HasRange ModuleName where
 
299
  getRange (MName []) = noRange
 
300
  getRange (MName xs) = getRange xs
 
301
 
264
302
instance HasRange QName where
265
303
  getRange q = getRange (qnameModule q, qnameName q)
266
304
 
 
305
-- ** SetRange
 
306
 
267
307
instance SetRange Name where
268
308
  setRange r x = x { nameConcrete = setRange r $ nameConcrete x }
269
309
 
275
315
instance SetRange ModuleName where
276
316
  setRange r (MName ns) = MName (map (setRange r) ns)
277
317
 
 
318
-- ** KillRange
 
319
 
 
320
instance KillRange Name where
 
321
  killRange x = x { nameConcrete = killRange $ nameConcrete x
 
322
                  -- Andreas, 2014-03-30
 
323
                  -- An experiment: what happens if we preserve
 
324
                  -- the range of the binding site, but kill all
 
325
                  -- other ranges before serialization?
 
326
                  -- , nameBindingSite = noRange
 
327
                  }
 
328
 
 
329
instance KillRange ModuleName where
 
330
  killRange (MName xs) = MName $ killRange xs
 
331
 
278
332
instance KillRange QName where
279
333
  killRange q = q { qnameModule = killRange $ qnameModule q
280
334
                  , qnameName   = killRange $ qnameName   q
281
335
                  }
282
336
 
283
 
instance KillRange Name where
284
 
  killRange x = x { nameConcrete = killRange $ nameConcrete x }
285
 
 
286
 
instance KillRange ModuleName where
287
 
  killRange (MName xs) = MName $ killRange xs
288
 
 
289
337
instance KillRange AmbiguousQName where
290
338
  killRange (AmbQ xs) = AmbQ $ killRange xs
291
339
 
 
340
------------------------------------------------------------------------
 
341
-- * Sized instances
 
342
------------------------------------------------------------------------
 
343
 
292
344
instance Sized QName where
293
345
  size = size . qnameToList
294
346