module Agda.Syntax.Abstract.Name 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 qualified Agda.Syntax.Concrete.Name as C
import Agda.Utils.Fresh
import Agda.Utils.Size
import Agda.Utils.Suffix
import Agda.Syntax.Notation
#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)
instance HasRange ModuleName where
getRange (MName []) = noRange
getRange (MName xs) = getRange xs
isAnonymousModuleName :: ModuleName -> Bool
isAnonymousModuleName (MName []) = False
isAnonymousModuleName (MName ms) = C.isNoName $ nameConcrete $ 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 []
mkName :: Range -> NameId -> String -> Name
mkName r i s = Name i (C.Name noRange (parseName s)) r defaultFixity'
where
parseName "" = []
parseName ('_':s) = C.Hole : parseName s
parseName s = case break (== '_') s of
(s0, s1) -> C.Id s0 : parseName s1
mkName_ :: NameId -> String -> Name
mkName_ = mkName noRange
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
freshName_ :: (MonadState s m, HasFresh NameId s) => String -> m Name
freshName_ = freshName noRange
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
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 Show NameId where
show (NameId x i) = show x ++ "@" ++ show i
instance Eq Name where
x == y = nameId x == nameId y
instance Ord Name where
compare x y = compare (nameId x) (nameId y)
instance Show Name where
show x = show (nameConcrete x)
instance Hashable Name where
hash = hash . nameId
instance Show QName where
show q = concat $ intersperse "." $ map show $ qnameToList q
instance Show ModuleName where
show m = concat $ intersperse "." $ map show $ mnameToList m
instance Eq QName where
(==) = (==) `on` qnameName
instance Ord QName where
compare = compare `on` qnameName
instance Hashable QName where
hash = hash . qnameName
instance HasRange Name where
getRange = getRange . nameConcrete
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 QName where
killRange q = q { qnameModule = killRange $ qnameModule q
, qnameName = killRange $ qnameName q
}
instance KillRange Name where
killRange x = x { nameConcrete = killRange $ nameConcrete x }
instance KillRange ModuleName where
killRange (MName xs) = MName $ killRange xs
instance KillRange AmbiguousQName where
killRange (AmbQ xs) = AmbQ $ killRange xs
instance Sized QName where
size = size . qnameToList
instance Sized ModuleName where
size = size . mnameToList