1 2{-| Abstract names carry unique identifiers and stuff. 3-} 4module Agda.Syntax.Abstract.Name 5 ( module Agda.Syntax.Abstract.Name 6 , IsNoName(..) 7 , FreshNameMode(..) 8 ) where 9 10import Prelude hiding (length) 11 12import Control.DeepSeq 13 14import Data.Data (Data) 15import Data.Foldable (length) 16import Data.Function 17import Data.Hashable (Hashable(..)) 18import qualified Data.List as List 19import Data.Maybe 20import Data.Void 21 22import Agda.Syntax.Position 23import Agda.Syntax.Common 24import Agda.Syntax.Concrete.Name (IsNoName(..), NumHoles(..), NameInScope(..), LensInScope(..), FreshNameMode(..)) 25import qualified Agda.Syntax.Concrete.Name as C 26 27import Agda.Utils.Functor 28import Agda.Utils.Lens 29import qualified Agda.Utils.List as L 30import Agda.Utils.List1 (List1, pattern (:|), (<|)) 31import qualified Agda.Utils.List1 as List1 32import Agda.Utils.Pretty 33import Agda.Utils.Size 34 35import Agda.Utils.Impossible 36 37-- | A name is a unique identifier and a suggestion for a concrete name. The 38-- concrete name contains the source location (if any) of the name. The 39-- source location of the binding site is also recorded. 40data Name = Name 41 { nameId :: !NameId 42 , nameConcrete :: C.Name -- ^ The concrete name used for this instance 43 , nameCanonical :: C.Name -- ^ The concrete name in the original definition (needed by primShowQName, see #4735) 44 , nameBindingSite :: Range 45 , nameFixity :: Fixity' 46 , nameIsRecordName :: Bool 47 -- ^ Is this the name of the invisible record variable `self`? 48 -- Should not be printed or displayed in the context, see issue #3584. 49 } deriving Data 50 51-- | Useful for debugging scoping problems 52uglyShowName :: Name -> String 53uglyShowName x = show (nameId x, nameConcrete x) 54 55-- | Qualified names are non-empty lists of names. Equality on qualified names 56-- are just equality on the last name, i.e. the module part is just 57-- for show. 58-- 59-- The 'SetRange' instance for qualified names sets all individual 60-- ranges (including those of the module prefix) to the given one. 61data QName = QName { qnameModule :: ModuleName 62 , qnameName :: Name 63 } 64 deriving Data 65 66-- | Something preceeded by a qualified name. 67data QNamed a = QNamed 68 { qname :: QName 69 , qnamed :: a 70 } 71 deriving (Functor, Foldable, Traversable) 72 73-- | A module name is just a qualified name. 74-- 75-- The 'SetRange' instance for module names sets all individual ranges 76-- to the given one. 77newtype ModuleName = MName { mnameToList :: [Name] } 78 deriving (Eq, Ord, Data) 79 80-- | Ambiguous qualified names. Used for overloaded constructors. 81-- 82-- Invariant: All the names in the list must have the same concrete, 83-- unqualified name. (This implies that they all have the same 'Range'). 84newtype AmbiguousQName = AmbQ { unAmbQ :: List1 QName } 85 deriving (Eq, Ord, Data, NFData) 86 87-- | A singleton "ambiguous" name. 88unambiguous :: QName -> AmbiguousQName 89unambiguous x = AmbQ (x :| []) 90 91-- | Get the first of the ambiguous names. 92headAmbQ :: AmbiguousQName -> QName 93headAmbQ (AmbQ xs) = List1.head xs 94 95-- | Is a name ambiguous. 96isAmbiguous :: AmbiguousQName -> Bool 97isAmbiguous (AmbQ (_ :| xs)) = not (null xs) 98 99-- | Get the name if unambiguous. 100getUnambiguous :: AmbiguousQName -> Maybe QName 101getUnambiguous (AmbQ (x :| [])) = Just x 102getUnambiguous _ = Nothing 103 104-- | A name suffix 105data Suffix 106 = NoSuffix 107 | Suffix !Integer 108 deriving (Data, Show, Eq, Ord) 109 110instance NFData Suffix where 111 rnf NoSuffix = () 112 rnf (Suffix _) = () 113 114-- | Check whether we are a projection pattern. 115class IsProjP a where 116 isProjP :: a -> Maybe (ProjOrigin, AmbiguousQName) 117 118instance IsProjP a => IsProjP (Arg a) where 119 isProjP p = case isProjP $ unArg p of 120 Just (ProjPostfix , f) 121 | getHiding p /= NotHidden -> Nothing 122 x -> x 123 124instance IsProjP a => IsProjP (Named n a) where 125 isProjP = isProjP . namedThing 126 127instance IsProjP Void where 128 isProjP _ = __IMPOSSIBLE__ 129 130-- | A module is anonymous if the qualification path ends in an underscore. 131isAnonymousModuleName :: ModuleName -> Bool 132isAnonymousModuleName (MName mms) = maybe False isNoName $ L.lastMaybe mms 133 134-- | Sets the ranges of the individual names in the module name to 135-- match those of the corresponding concrete names. If the concrete 136-- names are fewer than the number of module name name parts, then the 137-- initial name parts get the range 'noRange'. 138-- 139-- @C.D.E \`withRangesOf\` [A, B]@ returns @C.D.E@ but with ranges set 140-- as follows: 141-- 142-- * @C@: 'noRange'. 143-- 144-- * @D@: the range of @A@. 145-- 146-- * @E@: the range of @B@. 147-- 148-- Precondition: The number of module name name parts has to be at 149-- least as large as the length of the list. 150 151withRangesOf :: ModuleName -> List1 C.Name -> ModuleName 152MName ms `withRangesOf` ns = if m < n then __IMPOSSIBLE__ else MName $ 153 zipWith setRange (replicate (m - n) noRange ++ map getRange (List1.toList ns)) ms 154 where 155 m = length ms 156 n = length ns 157 158-- | Like 'withRangesOf', but uses the name parts (qualifier + name) 159-- of the qualified name as the list of concrete names. 160 161withRangesOfQ :: ModuleName -> C.QName -> ModuleName 162m `withRangesOfQ` q = m `withRangesOf` C.qnameParts q 163 164mnameFromList :: [Name] -> ModuleName 165mnameFromList = MName 166 167mnameFromList1 :: List1 Name -> ModuleName 168mnameFromList1 = MName . List1.toList 169 170mnameToList1 :: ModuleName -> List1 Name 171mnameToList1 (MName ns) = List1.ifNull ns __IMPOSSIBLE__ id 172 173noModuleName :: ModuleName 174noModuleName = mnameFromList [] 175 176commonParentModule :: ModuleName -> ModuleName -> ModuleName 177commonParentModule m1 m2 = 178 mnameFromList $ L.commonPrefix (mnameToList m1) (mnameToList m2) 179 180-- | Make a 'Name' from some kind of string. 181class MkName a where 182 -- | The 'Range' sets the /definition site/ of the name, not the use site. 183 mkName :: Range -> NameId -> a -> Name 184 185 mkName_ :: NameId -> a -> Name 186 mkName_ = mkName noRange 187 188instance MkName String where 189 mkName r i s = makeName i (C.Name noRange InScope (C.stringNameParts s)) r noFixity' False 190 191makeName :: NameId -> C.Name -> Range -> Fixity' -> Bool -> Name 192makeName i c r f rec = Name i c c r f rec 193 194qnameToList0 :: QName -> [Name] 195qnameToList0 = List1.toList . qnameToList 196 197qnameToList :: QName -> List1 Name 198qnameToList (QName m x) = mnameToList m `List1.snoc` x 199 200qnameFromList :: List1 Name -> QName 201qnameFromList xs = QName (mnameFromList $ List1.init xs) (List1.last xs) 202 203qnameToMName :: QName -> ModuleName 204qnameToMName = mnameFromList1 . qnameToList 205 206mnameToQName :: ModuleName -> QName 207mnameToQName = qnameFromList . mnameToList1 208 209showQNameId :: QName -> String 210showQNameId q = show ns ++ "@" ++ show m 211 where 212 is = map nameId $ mnameToList (qnameModule q) ++ [qnameName q] 213 ns = [ n | NameId n _ <- is ] 214 m = head [ m | NameId _ m <- is ] 215 216-- | Turn a qualified name into a concrete name. This should only be used as a 217-- fallback when looking up the right concrete name in the scope fails. 218qnameToConcrete :: QName -> C.QName 219qnameToConcrete (QName m x) = -- Use the canonical name here (#5048) 220 foldr (C.Qual . nameConcrete) (C.QName $ nameCanonical x) (mnameToList m) 221 222mnameToConcrete :: ModuleName -> C.QName 223mnameToConcrete (MName []) = __IMPOSSIBLE__ -- C.QName C.noName_ -- should never happen? 224mnameToConcrete (MName (x:xs)) = foldr C.Qual (C.QName $ List1.last cs) $ List1.init cs 225 where 226 cs = fmap nameConcrete (x :| xs) 227 228-- | Computes the 'TopLevelModuleName' corresponding to the given 229-- module name, which is assumed to represent a top-level module name. 230-- 231-- Precondition: The module name must be well-formed. 232 233toTopLevelModuleName :: ModuleName -> C.TopLevelModuleName 234toTopLevelModuleName (MName []) = __IMPOSSIBLE__ 235toTopLevelModuleName (MName ms) = List1.ifNull ms __IMPOSSIBLE__ {-else-} $ \ ms1 -> 236 C.TopLevelModuleName (getRange ms1) $ fmap (C.nameToRawName . nameConcrete) ms1 237 238qualifyM :: ModuleName -> ModuleName -> ModuleName 239qualifyM m1 m2 = mnameFromList $ mnameToList m1 ++ mnameToList m2 240 241qualifyQ :: ModuleName -> QName -> QName 242qualifyQ m x = qnameFromList $ mnameToList m `List1.prepend` qnameToList x 243 244qualify :: ModuleName -> Name -> QName 245qualify = QName 246 247-- | Convert a 'Name' to a 'QName' (add no module name). 248qualify_ :: Name -> QName 249qualify_ = qualify noModuleName 250 251-- | Is the name an operator? 252 253isOperator :: QName -> Bool 254isOperator = C.isOperator . nameConcrete . qnameName 255 256-- | Is the first module a weak parent of the second? 257isLeParentModuleOf :: ModuleName -> ModuleName -> Bool 258isLeParentModuleOf = List.isPrefixOf `on` mnameToList 259 260-- | Is the first module a proper parent of the second? 261isLtParentModuleOf :: ModuleName -> ModuleName -> Bool 262isLtParentModuleOf x y = 263 isJust $ (L.stripPrefixBy (==) `on` mnameToList) x y 264 265-- | Is the first module a weak child of the second? 266isLeChildModuleOf :: ModuleName -> ModuleName -> Bool 267isLeChildModuleOf = flip isLeParentModuleOf 268 269-- | Is the first module a proper child of the second? 270isLtChildModuleOf :: ModuleName -> ModuleName -> Bool 271isLtChildModuleOf = flip isLtParentModuleOf 272 273isInModule :: QName -> ModuleName -> Bool 274isInModule q m = mnameToList m `List.isPrefixOf` qnameToList0 q 275 276-- | Get the next version of the concrete name. For instance, @nextName "x" = "x₁"@. 277-- The name must not be a 'NoName'. 278nextName :: C.FreshNameMode -> Name -> Name 279nextName freshNameMode x = x { nameConcrete = C.nextName freshNameMode (nameConcrete x) } 280 281sameRoot :: Name -> Name -> Bool 282sameRoot = C.sameRoot `on` nameConcrete 283 284------------------------------------------------------------------------ 285-- * Important instances: Eq, Ord, Hashable 286-- 287-- For the identity and comparing of names, only the 'NameId' matters! 288------------------------------------------------------------------------ 289 290instance Eq Name where 291 (==) = (==) `on` nameId 292 293instance Ord Name where 294 compare = compare `on` nameId 295 296instance Hashable Name where 297 {-# INLINE hashWithSalt #-} 298 hashWithSalt salt = hashWithSalt salt . nameId 299 300instance Eq QName where 301 (==) = (==) `on` qnameName 302 303instance Ord QName where 304 compare = compare `on` qnameName 305 306instance Hashable QName where 307 {-# INLINE hashWithSalt #-} 308 hashWithSalt salt = hashWithSalt salt . qnameName 309 310------------------------------------------------------------------------ 311-- * IsNoName instances (checking for "_") 312------------------------------------------------------------------------ 313 314-- | An abstract name is empty if its concrete name is empty. 315instance IsNoName Name where 316 isNoName = isNoName . nameConcrete 317 318instance NumHoles Name where 319 numHoles = numHoles . nameConcrete 320 321instance NumHoles QName where 322 numHoles = numHoles . qnameName 323 324-- | We can have an instance for ambiguous names as all share a common concrete name. 325instance NumHoles AmbiguousQName where 326 numHoles = numHoles . headAmbQ 327 328------------------------------------------------------------------------ 329-- * name lenses 330------------------------------------------------------------------------ 331 332lensQNameName :: Lens' Name QName 333lensQNameName f (QName m n) = QName m <$> f n 334 335------------------------------------------------------------------------ 336-- * LensFixity' instances 337------------------------------------------------------------------------ 338 339instance LensFixity' Name where 340 lensFixity' f n = f (nameFixity n) <&> \ fix' -> n { nameFixity = fix' } 341 342instance LensFixity' QName where 343 lensFixity' = lensQNameName . lensFixity' 344 345------------------------------------------------------------------------ 346-- * LensFixity instances 347------------------------------------------------------------------------ 348 349instance LensFixity Name where 350 lensFixity = lensFixity' . lensFixity 351 352instance LensFixity QName where 353 lensFixity = lensFixity' . lensFixity 354 355------------------------------------------------------------------------ 356-- * LensInScope instances 357------------------------------------------------------------------------ 358 359instance LensInScope Name where 360 lensInScope f n@Name{ nameConcrete = x } = 361 (\y -> n { nameConcrete = y }) <$> lensInScope f x 362 363instance LensInScope QName where 364 lensInScope f q@QName{ qnameName = n } = 365 (\n' -> q { qnameName = n' }) <$> lensInScope f n 366 367------------------------------------------------------------------------ 368-- * Show instances (only for debug printing!) 369-- 370-- | Use 'prettyShow' to print names to the user. 371------------------------------------------------------------------------ 372 373deriving instance Show Name 374deriving instance Show ModuleName 375deriving instance Show QName 376deriving instance Show a => Show (QNamed a) 377deriving instance Show AmbiguousQName 378 379nameToArgName :: Name -> ArgName 380nameToArgName = stringToArgName . prettyShow 381 382namedArgName :: NamedArg Name -> ArgName 383namedArgName x = fromMaybe (nameToArgName $ namedArg x) $ bareNameOf x 384 385------------------------------------------------------------------------ 386-- * Pretty instances 387------------------------------------------------------------------------ 388 389instance Pretty Name where 390 pretty = pretty . nameConcrete 391 392instance Pretty ModuleName where 393 pretty = hcat . punctuate "." . map pretty . mnameToList 394 395instance Pretty QName where 396 pretty = hcat . punctuate "." . map pretty . qnameToList0 . useCanonical 397 where 398 -- #4735: When printing a fully qualified name (as done by primShowQName) we need to 399 -- use the origincal concrete name, not the possibly renamed concrete name in 'nameConcrete'. 400 useCanonical q = q { qnameName = (qnameName q) { nameConcrete = nameCanonical (qnameName q) } } 401 402instance Pretty AmbiguousQName where 403 pretty (AmbQ qs) = hcat $ punctuate " | " $ map pretty $ List1.toList qs 404 405instance Pretty a => Pretty (QNamed a) where 406 pretty (QNamed a b) = pretty a <> "." <> pretty b 407 408------------------------------------------------------------------------ 409-- * Range instances 410------------------------------------------------------------------------ 411 412-- ** HasRange 413 414instance HasRange Name where 415 getRange = getRange . nameConcrete 416 417instance HasRange ModuleName where 418 getRange (MName []) = noRange 419 getRange (MName xs) = getRange xs 420 421instance HasRange QName where 422 getRange q = getRange (qnameModule q, qnameName q) 423 424-- | The range of an @AmbiguousQName@ is the range of any of its 425-- disambiguations (they are the same concrete name). 426instance HasRange AmbiguousQName where 427 getRange (AmbQ (c :| _)) = getRange c 428 429-- ** SetRange 430 431instance SetRange Name where 432 setRange r x = x { nameConcrete = setRange r $ nameConcrete x } 433 434instance SetRange QName where 435 setRange r q = q { qnameModule = setRange r $ qnameModule q 436 , qnameName = setRange r $ qnameName q 437 } 438 439instance SetRange ModuleName where 440 setRange r (MName ns) = MName (zipWith setRange rs ns) 441 where 442 -- Put the range only on the last name. Otherwise 443 -- we get overlapping jump-to-definition links for all 444 -- the parts (See #2666). 445 rs = replicate (length ns - 1) noRange ++ [r] 446 447-- ** KillRange 448 449instance KillRange Name where 450 killRange (Name a b c d e f) = 451 (killRange6 Name a b c d e f) { nameBindingSite = d } 452 -- Andreas, 2017-07-25, issue #2649 453 -- Preserve the nameBindingSite for error message. 454 -- 455 -- Older remarks: 456 -- 457 -- Andreas, 2014-03-30 458 -- An experiment: what happens if we preserve 459 -- the range of the binding site, but kill all 460 -- other ranges before serialization? 461 -- 462 -- Andreas, Makoto, 2014-10-18 AIM XX 463 -- Kill all ranges in signature, including nameBindingSite. 464 465instance KillRange ModuleName where 466 killRange (MName xs) = MName $ killRange xs 467 468instance KillRange QName where 469 killRange (QName a b) = killRange2 QName a b 470 -- killRange q = q { qnameModule = killRange $ qnameModule q 471 -- , qnameName = killRange $ qnameName q 472 -- } 473 474instance KillRange AmbiguousQName where 475 killRange (AmbQ xs) = AmbQ $ killRange xs 476 477------------------------------------------------------------------------ 478-- * Sized instances 479------------------------------------------------------------------------ 480 481instance Sized QName where 482 size = size . qnameToList 483 484instance Sized ModuleName where 485 size = size . mnameToList 486 487------------------------------------------------------------------------ 488-- * NFData instances 489------------------------------------------------------------------------ 490 491-- | The range is not forced. 492 493instance NFData Name where 494 rnf (Name _ a b _ c d) = rnf (a, b, c, d) 495 496instance NFData QName where 497 rnf (QName a b) = rnf a `seq` rnf b 498 499instance NFData ModuleName where 500 rnf (MName a) = rnf a 501