{-# LANGUAGE DeriveDataTypeable #-}
module Agda.Syntax.Abstract.Name
( module Agda.Syntax.Abstract.Name
, IsNoName(..)
) where
import Control.DeepSeq
import Data.Data (Data)
import Data.Foldable (Foldable)
import Data.Function
import Data.Hashable (Hashable(..))
import Data.List
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
import Data.Maybe
import Data.Traversable (Traversable)
import Data.Void
import Agda.Syntax.Position
import Agda.Syntax.Common
import {-# SOURCE #-} Agda.Syntax.Fixity
import Agda.Syntax.Concrete.Name (IsNoName(..), NumHoles(..), NameInScope(..), LensInScope(..))
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Pretty
import Agda.Utils.Size
import Agda.Utils.Impossible
data Name = Name
{ nameId :: !NameId
, nameConcrete :: C.Name
, nameBindingSite :: Range
, nameFixity :: Fixity'
, nameIsRecordName :: Bool
} deriving Data
uglyShowName :: Name -> String
uglyShowName (Name i c _ _ _) = show (i,c)
data QName = QName { qnameModule :: ModuleName
, qnameName :: Name
}
deriving Data
data QNamed a = QNamed
{ qname :: QName
, qnamed :: a
}
deriving (Functor, Foldable, Traversable)
newtype ModuleName = MName { mnameToList :: [Name] }
deriving (Eq, Ord, Data)
newtype AmbiguousQName = AmbQ { unAmbQ :: NonEmpty QName }
deriving (Eq, Ord, Data)
unambiguous :: QName -> AmbiguousQName
unambiguous x = AmbQ (x :| [])
headAmbQ :: AmbiguousQName -> QName
headAmbQ (AmbQ xs) = NonEmpty.head xs
isAmbiguous :: AmbiguousQName -> Bool
isAmbiguous (AmbQ (_ :| xs)) = not (null xs)
getUnambiguous :: AmbiguousQName -> Maybe QName
getUnambiguous (AmbQ (x :| [])) = Just x
getUnambiguous _ = Nothing
class IsProjP a where
isProjP :: a -> Maybe (ProjOrigin, AmbiguousQName)
instance IsProjP a => IsProjP (Arg a) where
isProjP p = case isProjP $ unArg p of
Just (ProjPostfix , f)
| getHiding p /= NotHidden -> Nothing
x -> x
instance IsProjP a => IsProjP (Named n a) where
isProjP = isProjP . namedThing
instance IsProjP Void where
isProjP _ = __IMPOSSIBLE__
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 InScope (C.stringNameParts s)) r noFixity' False
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 (getRange ms) $ 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 = C.isOperator . nameConcrete . qnameName
isLeParentModuleOf :: ModuleName -> ModuleName -> Bool
isLeParentModuleOf = isPrefixOf `on` mnameToList
isLtParentModuleOf :: ModuleName -> ModuleName -> Bool
isLtParentModuleOf x y = isJust $ (stripPrefixBy (==) `on` mnameToList) x y
isLeChildModuleOf :: ModuleName -> ModuleName -> Bool
isLeChildModuleOf = flip isLeParentModuleOf
isLtChildModuleOf :: ModuleName -> ModuleName -> Bool
isLtChildModuleOf = flip isLtParentModuleOf
isInModule :: QName -> ModuleName -> Bool
isInModule q m = mnameToList m `isPrefixOf` qnameToList q
nextName :: Name -> Name
nextName x = x { nameConcrete = C.nextName (nameConcrete x) }
sameRoot :: Name -> Name -> Bool
sameRoot = C.sameRoot `on` nameConcrete
instance Eq Name where
(==) = (==) `on` nameId
instance Ord Name where
compare = compare `on` nameId
instance Hashable Name where
{-# INLINE hashWithSalt #-}
hashWithSalt salt = hashWithSalt salt . nameId
instance Eq QName where
(==) = (==) `on` qnameName
instance Ord QName where
compare = compare `on` qnameName
instance Hashable QName where
{-# INLINE hashWithSalt #-}
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 = numHoles . headAmbQ
lensQNameName :: Lens' Name QName
lensQNameName f (QName m n) = QName m <$> f n
instance LensFixity' Name where
lensFixity' f n = f (nameFixity n) <&> \ fix' -> n { nameFixity = fix' }
instance LensFixity' QName where
lensFixity' = lensQNameName . lensFixity'
instance LensFixity Name where
lensFixity = lensFixity' . lensFixity
instance LensFixity QName where
lensFixity = lensFixity' . lensFixity
instance LensInScope Name where
lensInScope f n@Name{ nameConcrete = x } =
(\y -> n { nameConcrete = y }) <$> lensInScope f x
instance LensInScope QName where
lensInScope f q@QName{ qnameName = n } =
(\n' -> q { qnameName = n' }) <$> lensInScope f n
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
nameToArgName :: Name -> ArgName
nameToArgName = stringToArgName . prettyShow
namedArgName :: NamedArg Name -> ArgName
namedArgName x = fromMaybe (nameToArgName $ namedArg x) $ bareNameOf x
instance Pretty Name where
pretty = pretty . nameConcrete
instance Pretty ModuleName where
pretty = hcat . punctuate "." . map pretty . mnameToList
instance Pretty QName where
pretty = hcat . punctuate "." . map pretty . qnameToList
instance Pretty AmbiguousQName where
pretty (AmbQ qs) = hcat $ punctuate " | " $ map pretty (NonEmpty.toList qs)
instance Pretty a => Pretty (QNamed a) where
pretty (QNamed a b) = pretty a <> "." <> 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 (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 (zipWith setRange rs ns)
where
rs = replicate (length ns - 1) noRange ++ [r]
instance KillRange Name where
killRange (Name a b c d e) =
(killRange4 Name a b c d e) { nameBindingSite = c }
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 c) = rnf a `seq` rnf b `seq` rnf c
instance NFData QName where
rnf (QName a b) = rnf a `seq` rnf b
instance NFData ModuleName where
rnf (MName a) = rnf a