← Back to branch summary

~ubuntu-branches/ubuntu/trusty/agda/trusty

« 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, Kiwamu Okabe, Iain Lane
  • Date: 2013-04-10 11:46:43 UTC
  • mfrom: (4.1.5 experimental)
  • Revision ID: package-import@ubuntu.com-20130410114643-prunhsz59f0fhrdn
Tags: 2.3.2-1
[ Kiwamu Okabe ]
* New patch: Extend haskell-src-exts dependency and fix type miss.

[ Iain Lane ]
* [dfbca48] Imported Upstream version 2.3.2
* [7746bcc] Remove all patches — all upstream.
* [2cdb691] Update build-deps to match control file
* [868ebf4] agda-mode no longer depends on haskell-mode or GHCi.
  Remove dependency and update .el file accordingly
* [9e0ba22] Add agda-bin package here, as the separate package has been
  removed
* [75a240f] agda-mode needs to depend on agda-bin
* [d290f95] Allow Quickcheck up to 2.7. Fix haskeline build-dep.
* [79190e6] Add missing geniplate and parallel BDs

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/Syntax/Abstract/Name.hs
1
 
{-# LANGUAGE CPP, DeriveDataTypeable, GeneralizedNewtypeDeriving, FlexibleContexts #-}
 
1
{-# LANGUAGE CPP,
 
2
  DeriveDataTypeable, GeneralizedNewtypeDeriving,
 
3
  DeriveFunctor, DeriveFoldable, DeriveTraversable,
 
4
  FlexibleContexts #-}
2
5
 
3
6
{-| Abstract names should carry unique identifiers and stuff. Not right now though.
4
7
-}
5
8
module Agda.Syntax.Abstract.Name where
6
9
 
7
10
import Control.Monad.State
8
 
import Data.Generics (Typeable, Data)
 
11
 
 
12
import Data.Foldable (Foldable)
 
13
import Data.Traversable (Traversable)
 
14
import Data.Typeable (Typeable)
9
15
import Data.List
10
16
import Data.Function
 
17
import Data.Hashable
11
18
 
12
19
import Agda.Syntax.Position
13
20
import Agda.Syntax.Common
31
38
                 , nameBindingSite :: Range
32
39
                 , nameFixity      :: Fixity'
33
40
                 }
34
 
    deriving (Typeable, Data)
 
41
    deriving (Typeable)
35
42
 
36
43
-- | Qualified names are non-empty lists of names. Equality on qualified names
37
44
--   are just equality on the last name, i.e. the module part is just
42
49
data QName = QName { qnameModule :: ModuleName
43
50
                   , qnameName   :: Name
44
51
                   }
45
 
    deriving (Typeable, Data)
 
52
    deriving (Typeable)
 
53
 
 
54
-- | Something preceeded by a qualified name.
 
55
data QNamed a = QNamed
 
56
  { qname  :: QName
 
57
  , qnamed :: a
 
58
  }
 
59
  deriving (Typeable, Show, Functor, Foldable, Traversable)
46
60
 
47
61
-- | A module name is just a qualified name.
48
62
--
49
63
-- The 'SetRange' instance for module names sets all individual ranges
50
64
-- to the given one.
51
65
newtype ModuleName = MName { mnameToList :: [Name] }
52
 
  deriving (Eq, Ord, Typeable, Data)
 
66
  deriving (Eq, Ord, Typeable)
53
67
 
54
68
-- | Ambiguous qualified names. Used for overloaded constructors.
55
69
--
56
70
-- Invariant: All the names in the list must have the same concrete,
57
71
-- unqualified name.
58
72
newtype AmbiguousQName = AmbQ { unAmbQ :: [QName] }
59
 
  deriving (Typeable, Data, HasRange, Show)
 
73
  deriving (Typeable, HasRange, Show)
60
74
 
61
75
instance HasRange ModuleName where
62
76
  getRange (MName []) = noRange
63
77
  getRange (MName xs) = getRange xs
64
78
 
 
79
-- | A module is anonymous if the qualification path ends in an underscore.
 
80
isAnonymousModuleName :: ModuleName -> Bool
 
81
isAnonymousModuleName (MName []) = False
 
82
isAnonymousModuleName (MName ms) = C.isNoName $ nameConcrete $ last ms
 
83
 
65
84
-- | Sets the ranges of the individual names in the module name to
66
85
-- match those of the corresponding concrete names. If the concrete
67
86
-- names are fewer than the number of module name name parts, then the
68
87
-- initial name parts get the range 'noRange'.
69
88
--
 
89
-- @C.D.E \`withRangesOf\` [A, B]@ returns @C.D.E@ but with ranges set
70
90
-- as follows:
71
91
--
72
92
-- * @C@: 'noRange'.
193
212
freshNoName_ :: (MonadState s m, HasFresh NameId s) => m Name
194
213
freshNoName_ = freshNoName noRange
195
214
 
 
215
-- | Get the next version of the concrete name. For instance, @nextName "x" = "x₁"@.
196
216
--   The name must not be a 'NoName'.
197
217
nextName :: Name -> Name
198
218
nextName x = x { nameConcrete = C.Name noRange $ nextSuf ps }
219
238
instance Show Name where
220
239
  show x = show (nameConcrete x) -- ++ "|" ++ show (nameId x)
221
240
 
 
241
instance Hashable Name where
 
242
  {-# INLINE hash #-}
 
243
  hash = hash . nameId
 
244
 
222
245
instance Show QName where
223
246
  show q = concat $ intersperse "." $ map show $ qnameToList q
224
247
 
231
254
instance Ord QName where
232
255
  compare = compare `on` qnameName
233
256
 
 
257
instance Hashable QName where
 
258
  {-# INLINE hash #-}
 
259
  hash = hash . qnameName
 
260
 
234
261
instance HasRange Name where
235
262
  getRange = getRange . nameConcrete
236
263