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.Fresh
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, HasRange, 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 show 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 m x = qualifyQ m (qnameFromList [x])
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
freshName :: (MonadState s m, HasFresh NameId s) => Range -> String -> m Name
freshName r s = do
i <- fresh
return $ mkName r i s
freshNoName :: (MonadState s m, HasFresh NameId s) => Range -> m Name
freshNoName r =
do i <- fresh
return $ Name i (C.NoName noRange i) r defaultFixity'
freshNoName_ :: (MonadState s m, HasFresh NameId s) => m Name
freshNoName_ = freshNoName noRange
class FreshName a where
freshName_ :: (MonadState s m, HasFresh NameId s) => a -> m Name
instance FreshName (Range, String) where
freshName_ = uncurry freshName
instance FreshName String where
freshName_ = freshName noRange
instance FreshName Range where
freshName_ = freshNoName
instance FreshName () where
freshName_ () = freshNoName_
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 x = show (nameConcrete x)
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 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 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
}
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