{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Agda.Syntax.Abstract.Name
( module Agda.Syntax.Abstract.Name
, IsNoName(..)
) where
#if MIN_VERSION_base(4,11,0)
import Prelude hiding ((<>))
#endif
import Control.DeepSeq
import Data.Foldable (Foldable, toList)
import Data.Traversable (Traversable)
import Data.Data (Data)
import Data.List
import Data.Function
import Data.Hashable (Hashable(..))
import Data.Void
import Agda.Syntax.Position
import Agda.Syntax.Common
import {-# SOURCE #-} 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.NonemptyList
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 Data
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 :: NonemptyList QName }
deriving (Eq, Ord, Data)
unambiguous :: QName -> AmbiguousQName
unambiguous x = AmbQ (x :! [])
headAmbQ :: AmbiguousQName -> QName
headAmbQ (AmbQ xs) = headNe 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 = isProjP . unArg
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 (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 (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 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
{-# 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
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 (toList 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 (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) =
(killRange4 Name a b c d) { 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) = 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