module Agda.Syntax.Abstract.Name
( module Agda.Syntax.Abstract.Name
, IsNoName(..)
) where
import Control.DeepSeq
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(..), NumHoles(..))
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
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, Functor, Foldable, Traversable)
newtype ModuleName = MName { mnameToList :: [Name] }
deriving (Eq, Ord, Typeable)
newtype AmbiguousQName = AmbQ { unAmbQ :: [QName] }
deriving (Eq, Ord, Typeable)
class IsProjP a where
isProjP :: a -> Maybe (ProjOrigin, AmbiguousQName)
instance IsProjP a => IsProjP (Arg a) where
isProjP = isProjP . unArg
instance IsProjP a => IsProjP (Named n a) where
isProjP = isProjP . namedThing
isAnonymousModuleName :: ModuleName -> Bool
isAnonymousModuleName (MName []) = False
isAnonymousModuleName (MName ms) = isNoName $ last ms
withRangesOf :: ModuleName -> [C.Name] -> ModuleName
MName ms `withRangesOf` ns = if m < n then __IMPOSSIBLE__ else MName $
zipWith setRange (replicate (m n) noRange ++ map getRange ns) ms
where
m = length ms
n = length ns
withRangesOfQ :: ModuleName -> C.QName -> ModuleName
m `withRangesOfQ` q = m `withRangesOf` C.qnameParts q
mnameFromList :: [Name] -> ModuleName
mnameFromList = MName
noModuleName :: ModuleName
noModuleName = mnameFromList []
commonParentModule :: ModuleName -> ModuleName -> ModuleName
commonParentModule m1 m2 =
mnameFromList $ commonPrefix (mnameToList m1) (mnameToList m2)
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 noFixity'
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 NumHoles Name where
numHoles = numHoles . nameConcrete
instance NumHoles QName where
numHoles = numHoles . qnameName
instance NumHoles AmbiguousQName where
numHoles (AmbQ qs) = numHoles $ fromMaybe __IMPOSSIBLE__ $ headMaybe qs
deriving instance Show a => Show (QNamed a)
deriving instance Show AmbiguousQName
instance Show Name where
show = prettyShow
instance Show ModuleName where
show = prettyShow
instance Show QName where
show = prettyShow
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 Pretty AmbiguousQName where
pretty (AmbQ qs) = hcat $ punctuate (text " | ") $ map pretty qs
instance Pretty a => Pretty (QNamed a) where
pretty (QNamed a b) = pretty a <> text "." <> pretty b
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 (Name a b c d) = killRange4 Name a b c d
instance KillRange ModuleName where
killRange (MName xs) = MName $ killRange xs
instance KillRange QName where
killRange (QName a b) = killRange2 QName a b
instance KillRange AmbiguousQName where
killRange (AmbQ xs) = AmbQ $ killRange xs
instance Sized QName where
size = size . qnameToList
instance Sized ModuleName where
size = size . mnameToList
instance NFData Name where
rnf (Name _ a _ b) = rnf a `seq` rnf b
instance NFData QName where
rnf (QName a b) = rnf a `seq` rnf b
instance NFData ModuleName where
rnf (MName a) = rnf a