← 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, d5cf60f
  • Date: 2015-05-20 13:08:33 UTC
  • mfrom: (1.1.7)
  • Revision ID: package-import@ubuntu.com-20150520130833-cdcmhagwsouna237
Tags: 2.4.2.2-2
[d5cf60f] Depend on ${shlibs:Depends}, to get libc (& maybe other) deps

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/Syntax/Concrete/Name.hs
1
 
{-# LANGUAGE CPP #-}
2
 
{-# LANGUAGE DeriveDataTypeable #-}
3
 
{-# LANGUAGE FlexibleInstances #-}
4
 
{-# LANGUAGE PatternGuards #-}
 
1
{-# LANGUAGE CPP                  #-}
 
2
{-# LANGUAGE DeriveDataTypeable   #-}
 
3
{-# LANGUAGE FlexibleInstances    #-}
 
4
{-# LANGUAGE PatternGuards        #-}
5
5
{-# LANGUAGE TypeSynonymInstances #-}
6
6
 
7
7
{-| Names in the concrete syntax are just strings (or lists of strings for
26
26
import Agda.Utils.FileName
27
27
import Agda.Utils.Pretty
28
28
 
29
 
#include "../../undefined.h"
 
29
#include "undefined.h"
30
30
import Agda.Utils.Impossible
31
31
 
32
32
{-| A name is a non-empty list of alternating 'Id's and 'Hole's. A normal name
69
69
instance Eq Name where
70
70
    Name _ xs  == Name _ ys  = xs == ys
71
71
    NoName _ i == NoName _ j = i == j
72
 
    _          == _          = False
 
72
    _          == _          = False
73
73
 
74
74
instance Ord Name where
75
75
    compare (Name _ xs)  (Name _ ys)  = compare xs ys
156
156
 
157
157
-- | @qualify A.B x == A.B.x@
158
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
 
159
qualify (QName m) x     = Qual m (QName x)
 
160
qualify (Qual m m') x   = Qual m $ qualify m' x
161
161
 
162
162
-- | @unqualify A.B.x == x@
163
163
--
241
241
-- no instance for TopLevelModuleName
242
242
 
243
243
------------------------------------------------------------------------
 
244
-- * Showing names
244
245
------------------------------------------------------------------------
245
246
 
 
247
-- TODO: 'Show' should output Haskell-parseable representations.
 
248
-- The following instances are deprecated, and Pretty should be used
 
249
-- instead.  Later, simply derive Show for these types:
 
250
 
246
251
instance Show Name where
247
252
    show (Name _ xs)  = concatMap show xs
248
253
    show (NoName _ _) = "_"
256
260
    show (Qual m x) = show m ++ "." ++ show x
257
261
    show (QName x)  = show x
258
262
 
 
263
------------------------------------------------------------------------
 
264
-- * Printing names
 
265
------------------------------------------------------------------------
 
266
 
 
267
instance Pretty Name where
 
268
    pretty (Name _ xs)  = hcat $ map pretty xs
 
269
    pretty (NoName _ _) = text $ "_"
 
270
 
 
271
instance Pretty NamePart where
 
272
    pretty Hole   = text $ "_"
 
273
    pretty (Id s) = text $ rawNameToString s
 
274
 
 
275
instance Pretty QName where
 
276
    pretty (Qual m x) = pretty m <> pretty "." <> pretty x
 
277
    pretty (QName x)  = pretty x
 
278
 
259
279
instance Pretty TopLevelModuleName where
260
280
  pretty (TopLevelModuleName ms) = text $ intercalate "." ms
261
281
 
279
299
 
280
300
instance HasRange QName where
281
301
    getRange (QName  x) = getRange x
282
 
    getRange (Qual n x) = fuseRange n x
 
302
    getRange (Qual n x) = fuseRange n x
283
303
 
284
304
instance SetRange Name where
285
305
  setRange r (Name _ ps)  = Name r ps