module Agda.Syntax.Abstract.Name
( module Agda.Syntax.Abstract.Name
, IsNoName(..)
) where
import Control.Monad.State
import Data.Foldable (Foldable)
import Data.Traversable (Traversable)
import Data.Typeable (Typeable)
import Data.List
import Data.Function
import Data.Hashable
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Fixity
import Agda.Syntax.Concrete.Name (IsNoName(..))
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Utils.Pretty
import Agda.Utils.Size
import Agda.Utils.Suffix
#include "undefined.h"
import Agda.Utils.Impossible
data Name = Name { nameId :: NameId
, nameConcrete :: C.Name
, nameBindingSite :: Range
, nameFixity :: Fixity'
}
deriving (Typeable)
data QName = QName { qnameModule :: ModuleName
, qnameName :: Name
}
deriving (Typeable)
data QNamed a = QNamed
{ qname :: QName
, qnamed :: a
}
deriving (Typeable, Show, Functor, Foldable, Traversable)
newtype ModuleName = MName { mnameToList :: [Name] }
deriving (Eq, Ord, Typeable)
newtype AmbiguousQName = AmbQ { unAmbQ :: [QName] }
deriving (Typeable, Show)
isAnonymousModuleName :: ModuleName -> Bool
isAnonymousModuleName (MName []) = False
isAnonymousModuleName (MName ms) = isNoName $ last ms
withRangesOf :: ModuleName -> [C.Name] -> ModuleName
MName ms `withRangesOf` ns
| length ms < length ns = __IMPOSSIBLE__
| otherwise = MName $
reverse $ zipWith setRange
(reverse (map getRange ns) ++ repeat noRange)
(reverse ms)
withRangesOfQ :: ModuleName -> C.QName -> ModuleName
m `withRangesOfQ` q = m `withRangesOf` C.qnameParts q
mnameFromList :: [Name] -> ModuleName
mnameFromList = MName
noModuleName :: ModuleName
noModuleName = mnameFromList []
class MkName a where
mkName :: Range -> NameId -> a -> Name
mkName_ :: NameId -> a -> Name
mkName_ = mkName noRange
instance MkName String where
mkName r i s = Name i (C.Name noRange (C.stringNameParts s)) r defaultFixity'
qnameToList :: QName -> [Name]
qnameToList (QName m x) = mnameToList m ++ [x]
qnameFromList :: [Name] -> QName
qnameFromList [] = __IMPOSSIBLE__
qnameFromList xs = QName (mnameFromList $ init xs) (last xs)
qnameToMName :: QName -> ModuleName
qnameToMName = mnameFromList . qnameToList
mnameToQName :: ModuleName -> QName
mnameToQName = qnameFromList . mnameToList
showQNameId :: QName -> String
showQNameId q = show ns ++ "@" ++ show m
where
is = map nameId $ mnameToList (qnameModule q) ++ [qnameName q]
ns = [ n | NameId n _ <- is ]
m = head [ m | NameId _ m <- is ]
qnameToConcrete :: QName -> C.QName
qnameToConcrete (QName m x) =
foldr C.Qual (C.QName $ nameConcrete x) $ map nameConcrete $ mnameToList m
mnameToConcrete :: ModuleName -> C.QName
mnameToConcrete (MName []) = __IMPOSSIBLE__
mnameToConcrete (MName xs) = foldr C.Qual (C.QName $ last cs) $ init cs
where
cs = map nameConcrete xs
toTopLevelModuleName :: ModuleName -> C.TopLevelModuleName
toTopLevelModuleName (MName []) = __IMPOSSIBLE__
toTopLevelModuleName (MName ms) = C.TopLevelModuleName $ map (C.nameToRawName . nameConcrete) ms
qualifyM :: ModuleName -> ModuleName -> ModuleName
qualifyM m1 m2 = mnameFromList $ mnameToList m1 ++ mnameToList m2
qualifyQ :: ModuleName -> QName -> QName
qualifyQ m x = qnameFromList $ mnameToList m ++ qnameToList x
qualify :: ModuleName -> Name -> QName
qualify = QName
qualify_ :: Name -> QName
qualify_ = qualify noModuleName
isOperator :: QName -> Bool
isOperator q = C.isOperator (nameConcrete (qnameName q))
isSubModuleOf :: ModuleName -> ModuleName -> Bool
isSubModuleOf x y = xs /= ys && isPrefixOf ys xs
where
xs = mnameToList x
ys = mnameToList y
isInModule :: QName -> ModuleName -> Bool
isInModule q m = mnameToList m `isPrefixOf` qnameToList q
nextName :: Name -> Name
nextName x = x { nameConcrete = C.Name noRange $ nextSuf ps }
where
C.Name _ ps = nameConcrete x
nextSuf [C.Id s] = [C.Id $ nextStr s]
nextSuf [C.Id s, C.Hole] = [C.Id $ nextStr s, C.Hole]
nextSuf (p : ps) = p : nextSuf ps
nextSuf [] = __IMPOSSIBLE__
nextStr s = case suffixView s of
(s0, suf) -> addSuffix s0 (nextSuffix suf)
instance Eq Name where
(==) = (==) `on` nameId
instance Ord Name where
compare = compare `on` nameId
instance Hashable Name where
hashWithSalt salt = hashWithSalt salt . nameId
instance Eq QName where
(==) = (==) `on` qnameName
instance Ord QName where
compare = compare `on` qnameName
instance Hashable QName where
hashWithSalt salt = hashWithSalt salt . qnameName
instance IsNoName Name where
isNoName = isNoName . nameConcrete
instance Show Name where
show n = show (nameConcrete n)
instance Show ModuleName where
show m = concat $ intersperse "." $ map show $ mnameToList m
instance Show QName where
show q = concat $ intersperse "." $ map show $ qnameToList q
instance Pretty Name where
pretty = pretty . nameConcrete
instance Pretty ModuleName where
pretty = hcat . punctuate (text ".") . map pretty . mnameToList
instance Pretty QName where
pretty = hcat . punctuate (text ".") . map pretty . qnameToList
instance HasRange Name where
getRange = getRange . nameConcrete
instance HasRange ModuleName where
getRange (MName []) = noRange
getRange (MName xs) = getRange xs
instance HasRange QName where
getRange q = getRange (qnameModule q, qnameName q)
instance HasRange AmbiguousQName where
getRange (AmbQ []) = noRange
getRange (AmbQ (c:_)) = getRange c
instance SetRange Name where
setRange r x = x { nameConcrete = setRange r $ nameConcrete x }
instance SetRange QName where
setRange r q = q { qnameModule = setRange r $ qnameModule q
, qnameName = setRange r $ qnameName q
}
instance SetRange ModuleName where
setRange r (MName ns) = MName (map (setRange r) ns)
instance KillRange Name where
killRange x = x { nameConcrete = killRange $ nameConcrete x
, nameBindingSite = noRange
}
instance KillRange ModuleName where
killRange (MName xs) = MName $ killRange xs
instance KillRange QName where
killRange q = q { qnameModule = killRange $ qnameModule q
, qnameName = killRange $ qnameName q
}
instance KillRange AmbiguousQName where
killRange (AmbQ xs) = AmbQ $ killRange xs
instance Sized QName where
size = size . qnameToList
instance Sized ModuleName where
size = size . mnameToList