← 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/Concrete/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/Concrete/Name.hs
1
 
{-# LANGUAGE CPP, DeriveDataTypeable #-}
 
1
{-# LANGUAGE CPP #-}
 
2
{-# LANGUAGE DeriveDataTypeable #-}
 
3
{-# LANGUAGE FlexibleInstances #-}
 
4
{-# LANGUAGE PatternGuards #-}
 
5
{-# LANGUAGE TypeSynonymInstances #-}
2
6
 
3
7
{-| Names in the concrete syntax are just strings (or lists of strings for
4
8
    qualified names).
5
9
-}
6
10
module Agda.Syntax.Concrete.Name where
7
11
 
 
12
import Control.DeepSeq
8
13
import Control.Applicative
9
14
 
 
15
import Data.ByteString.Char8 (ByteString)
 
16
import qualified Data.ByteString.Char8 as ByteString
10
17
import Data.List
11
 
import Data.Maybe
12
18
import Data.Typeable (Typeable)
13
19
 
14
20
import System.FilePath
31
37
    Equality and ordering on @Name@s are defined to ignore range so same names
32
38
    in different locations are equal.
33
39
-}
34
 
data Name = Name !Range [NamePart]
35
 
          | NoName !Range NameId
36
 
    deriving (Typeable)
37
 
 
38
 
data NamePart = Hole | Id String
39
 
    deriving (Typeable)
40
 
 
41
 
noName_ :: Name
42
 
noName_ = noName noRange
43
 
 
44
 
noName :: Range -> Name
45
 
noName r = NoName r (NameId 0 0)
46
 
 
47
 
isNoName :: Name -> Bool
48
 
isNoName (NoName _ _)    = True
49
 
isNoName (Name _ [Hole]) = True   -- TODO: Track down where these come from
50
 
isNoName (Name _ [])     = True
51
 
isNoName _               = False
52
 
 
53
 
 
54
 
isOperator :: Name -> Bool
55
 
isOperator (NoName {}) = False
56
 
isOperator (Name _ ps) = length ps > 1
57
 
 
58
 
nameParts :: Name -> [NamePart]
59
 
nameParts (Name _ ps)  = ps
60
 
nameParts (NoName _ _) = [Hole]
61
 
 
62
 
nameStringParts :: Name -> [String]
63
 
nameStringParts n = [ s | Id s <- nameParts n ]
64
 
 
65
 
qualify :: QName -> Name -> QName
66
 
qualify (QName m) x     = Qual m (QName x)
67
 
qualify (Qual m m') x   = Qual m $ qualify m' x
68
 
 
69
 
--
70
 
unqualify :: QName -> Name
71
 
unqualify q = unqualify' q `withRangeOf` q
72
 
  where
73
 
  unqualify' (QName x)  = x
74
 
  unqualify' (Qual _ x) = unqualify' x
75
 
 
76
 
qnameParts :: QName -> [Name]
77
 
qnameParts (Qual x q) = x : qnameParts q
78
 
qnameParts (QName x)  = [x]
79
 
 
 
40
data Name
 
41
  = Name !Range [NamePart]  -- ^ A (mixfix) identifier.
 
42
  | NoName !Range NameId    -- ^ @_@.
 
43
  deriving (Typeable)
 
44
 
 
45
instance NFData Name
 
46
 
 
47
instance Underscore Name where
 
48
  underscore = NoName noRange __IMPOSSIBLE__
 
49
  isUnderscore NoName{}        = True
 
50
  isUnderscore (Name _ [Id x]) = isUnderscore x
 
51
  isUnderscore _               = False
 
52
 
 
53
-- | Mixfix identifiers are composed of words and holes,
 
54
--   e.g. @_+_@ or @if_then_else_@ or @[_/_]@.
 
55
data NamePart
 
56
  = Hole       -- ^ @_@ part.
 
57
  | Id RawName  -- ^ Identifier part.
 
58
  deriving (Typeable)
 
59
 
 
60
-- | Define equality on @Name@ to ignore range so same names in different
 
61
--   locations are equal.
80
62
--
81
63
--   Is there a reason not to do this? -Jeff
82
64
--
122
95
--     equality. We will have to define an equality instance to
123
96
--     non-generative namespaces (as well as having some sort of
124
97
--     lookup table for namespace names).
125
 
data QName = Qual  Name QName
126
 
           | QName Name
 
98
data QName
 
99
  = Qual  Name QName -- ^ @A.rest@.
 
100
  | QName Name       -- ^ @x@.
127
101
  deriving (Typeable, Eq, Ord)
128
102
 
 
103
instance Underscore QName where
 
104
  underscore = QName underscore
 
105
  isUnderscore (QName x) = isUnderscore x
 
106
  isUnderscore Qual{}    = False
 
107
 
 
108
-- | Top-level module names.  Used in connection with the file system.
129
109
--
 
110
--   Invariant: The list must not be empty.
130
111
 
131
112
newtype TopLevelModuleName
132
113
  = TopLevelModuleName { moduleNameParts :: [String] }
133
114
  deriving (Show, Eq, Ord, Typeable)
134
115
 
 
116
------------------------------------------------------------------------
 
117
-- * Operations on 'Name' and 'NamePart'
 
118
------------------------------------------------------------------------
 
119
 
 
120
nameToRawName :: Name -> RawName
 
121
nameToRawName = show
 
122
 
 
123
nameParts :: Name -> [NamePart]
 
124
nameParts (Name _ ps)  = ps
 
125
nameParts (NoName _ _) = [Hole]
 
126
 
 
127
nameStringParts :: Name -> [RawName]
 
128
nameStringParts n = [ s | Id s <- nameParts n ]
 
129
 
 
130
-- | Parse a string to parts of a concrete name.
 
131
 
 
132
stringNameParts :: String -> [NamePart]
 
133
stringNameParts ""                              = []
 
134
stringNameParts ('_':s)                         = Hole : stringNameParts s
 
135
stringNameParts s | (x, s') <- break (== '_') s = Id (stringToRawName x) : stringNameParts s'
 
136
 
 
137
-- | Is the name an operator?
 
138
 
 
139
isOperator :: Name -> Bool
 
140
isOperator (NoName {}) = False
 
141
isOperator (Name _ ps) = length ps > 1
 
142
 
 
143
isHole :: NamePart -> Bool
 
144
isHole Hole = True
 
145
isHole _    = False
 
146
 
 
147
isPrefix, isPostfix, isInfix, isNonfix :: Name -> Bool
 
148
isPrefix  x = not (isHole (head xs)) &&      isHole (last xs)  where xs = nameParts x
 
149
isPostfix x =      isHole (head xs)  && not (isHole (last xs)) where xs = nameParts x
 
150
isInfix   x =      isHole (head xs)  &&      isHole (last xs)  where xs = nameParts x
 
151
isNonfix  x = not (isHole (head xs)) && not (isHole (last xs)) where xs = nameParts x
 
152
 
 
153
------------------------------------------------------------------------
 
154
-- * Operations on qualified names
 
155
------------------------------------------------------------------------
 
156
 
 
157
-- | @qualify A.B x == A.B.x@
 
158
qualify :: QName -> Name -> QName
 
159
qualify (QName m) x     = Qual m (QName x)
 
160
qualify (Qual m m') x   = Qual m $ qualify m' x
 
161
 
 
162
-- | @unqualify A.B.x == x@
 
163
--
 
164
-- The range is preserved.
 
165
unqualify :: QName -> Name
 
166
unqualify q = unqualify' q `withRangeOf` q
 
167
  where
 
168
  unqualify' (QName x)  = x
 
169
  unqualify' (Qual _ x) = unqualify' x
 
170
 
 
171
-- | @qnameParts A.B.x = [A, B, x]@
 
172
qnameParts :: QName -> [Name]
 
173
qnameParts (Qual x q) = x : qnameParts q
 
174
qnameParts (QName x)  = [x]
 
175
 
 
176
------------------------------------------------------------------------
 
177
-- * Operations on 'TopLevelModuleName'
 
178
------------------------------------------------------------------------
 
179
 
135
180
-- | Turns a qualified name into a 'TopLevelModuleName'. The qualified
136
181
-- name is assumed to represent a top-level module name.
137
182
 
163
206
  takeDirectory $
164
207
  filePath file
165
208
 
166
 
isHole :: NamePart -> Bool
167
 
isHole Hole = True
168
 
isHole _    = False
169
 
 
170
 
isPrefix, isPostfix, isInfix, isNonfix :: Name -> Bool
171
 
isPrefix  x = not (isHole (head xs)) &&      isHole (last xs)  where xs = nameParts x
172
 
isPostfix x =      isHole (head xs)  && not (isHole (last xs)) where xs = nameParts x
173
 
isInfix   x =      isHole (head xs)  &&      isHole (last xs)  where xs = nameParts x
174
 
isNonfix  x = not (isHole (head xs)) && not (isHole (last xs)) where xs = nameParts x
 
209
------------------------------------------------------------------------
 
210
-- * No name stuff
 
211
------------------------------------------------------------------------
 
212
 
 
213
-- | @noName_ = 'noName' 'noRange'@
 
214
noName_ :: Name
 
215
noName_ = noName noRange
 
216
 
 
217
-- | @noName r = 'Name' r ['Hole']@
 
218
noName :: Range -> Name
 
219
noName r = NoName r (NameId 0 0)
 
220
 
 
221
-- | Check whether a name is the empty name "_".
 
222
class IsNoName a where
 
223
  isNoName :: a -> Bool
 
224
 
 
225
instance IsNoName String where
 
226
  isNoName = isUnderscore
 
227
 
 
228
instance IsNoName ByteString where
 
229
  isNoName = isUnderscore
 
230
 
 
231
instance IsNoName Name where
 
232
  isNoName (NoName _ _)    = True
 
233
  isNoName (Name _ [Hole]) = True   -- TODO: Track down where these come from
 
234
  isNoName (Name _ [])     = True
 
235
  isNoName _               = False
 
236
 
 
237
instance IsNoName QName where
 
238
  isNoName (QName x) = isNoName x
 
239
  isNoName Qual{}    = False        -- M.A._ does not qualify as empty name
 
240
 
 
241
-- no instance for TopLevelModuleName
 
242
 
 
243
------------------------------------------------------------------------
 
244
-- * Printing names
 
245
------------------------------------------------------------------------
175
246
 
176
247
instance Show Name where
177
248
    show (Name _ xs)  = concatMap show xs
179
250
 
180
251
instance Show NamePart where
181
252
    show Hole   = "_"
182
 
    show (Id s) = s
 
253
    show (Id s) = rawNameToString s
183
254
 
184
255
instance Show QName where
185
256
    show (Qual m x) = show m ++ "." ++ show x
188
259
instance Pretty TopLevelModuleName where
189
260
  pretty (TopLevelModuleName ms) = text $ intercalate "." ms
190
261
 
 
262
------------------------------------------------------------------------
 
263
-- * QuickCheck instances
 
264
------------------------------------------------------------------------
 
265
 
191
266
instance Arbitrary TopLevelModuleName where
192
267
  arbitrary = TopLevelModuleName <$> listOf1 (listOf1 $ elements "AB")
193
268
 
194
269
instance CoArbitrary TopLevelModuleName where
195
270
  coarbitrary (TopLevelModuleName m) = coarbitrary m
196
271
 
 
272
------------------------------------------------------------------------
 
273
-- * Range instances
 
274
------------------------------------------------------------------------
 
275
 
197
276
instance HasRange Name where
198
277
    getRange (Name r ps)  = r
199
278
    getRange (NoName r _) = r