{-# 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)
import Data.Traversable (Traversable)
import Data.Data (Data)
import Data.List
import Data.Function
import Data.Hashable (Hashable(..))
import Data.Set (Set)
import qualified Data.Set as Set
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.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.NonemptyList
import Agda.Utils.Pretty
import Agda.Utils.Size
#include "undefined.h"
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 :: 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 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 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.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
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
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 (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