{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Agda.Syntax.Concrete.Name where
#if MIN_VERSION_base(4,11,0)
import Prelude hiding ((<>))
#endif
import Control.DeepSeq
import Data.ByteString.Char8 (ByteString)
import Data.Function
import qualified Data.List as List
import Data.Data (Data)
import GHC.Generics (Generic)
import System.FilePath
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Utils.FileName
import Agda.Utils.Pretty
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
data Name
= Name Range [NamePart]
| NoName Range NameId
deriving Data
isOpenMixfix :: Name -> Bool
isOpenMixfix n = case n of
Name _ (x : xs@(_:_)) -> x == Hole || last xs == Hole
_ -> False
instance Underscore Name where
underscore = NoName noRange __IMPOSSIBLE__
isUnderscore NoName{} = True
isUnderscore (Name _ [Id x]) = isUnderscore x
isUnderscore _ = False
data NamePart
= Hole
| Id RawName
deriving (Data, Generic)
instance Eq Name where
Name _ xs == Name _ ys = xs == ys
NoName _ i == NoName _ j = i == j
_ == _ = False
instance Ord Name where
compare (Name _ xs) (Name _ ys) = compare xs ys
compare (NoName _ i) (NoName _ j) = compare i j
compare (NoName {}) (Name {}) = LT
compare (Name {}) (NoName {}) = GT
instance Eq NamePart where
Hole == Hole = True
Id s1 == Id s2 = s1 == s2
_ == _ = False
instance Ord NamePart where
compare Hole Hole = EQ
compare Hole (Id {}) = LT
compare (Id {}) Hole = GT
compare (Id s1) (Id s2) = compare s1 s2
data QName
= Qual Name QName
| QName Name
deriving (Data, Eq, Ord)
instance Underscore QName where
underscore = QName underscore
isUnderscore (QName x) = isUnderscore x
isUnderscore Qual{} = False
data TopLevelModuleName = TopLevelModuleName
{ moduleNameRange :: Range
, moduleNameParts :: [String]
}
deriving (Show, Data)
instance Eq TopLevelModuleName where (==) = (==) `on` moduleNameParts
instance Ord TopLevelModuleName where compare = compare `on` moduleNameParts
instance Sized TopLevelModuleName where size = size . moduleNameParts
nameToRawName :: Name -> RawName
nameToRawName = prettyShow
nameParts :: Name -> [NamePart]
nameParts (Name _ ps) = ps
nameParts (NoName _ _) = [Id "_"]
nameStringParts :: Name -> [RawName]
nameStringParts n = [ s | Id s <- nameParts n ]
stringNameParts :: String -> [NamePart]
stringNameParts "_" = [Id "_"]
stringNameParts s = loop s where
loop "" = []
loop ('_':s) = Hole : loop s
loop s | (x, s') <- break (== '_') s = Id (stringToRawName x) : loop s'
class NumHoles a where
numHoles :: a -> Int
instance NumHoles [NamePart] where
numHoles = length . filter (== Hole)
instance NumHoles Name where
numHoles NoName{} = 0
numHoles (Name _ parts) = numHoles parts
instance NumHoles QName where
numHoles (QName x) = numHoles x
numHoles (Qual _ x) = numHoles x
isOperator :: Name -> Bool
isOperator (NoName {}) = False
isOperator (Name _ ps) = length ps > 1
isHole :: NamePart -> Bool
isHole Hole = True
isHole _ = False
isPrefix, isPostfix, isInfix, isNonfix :: Name -> Bool
isPrefix x = not (isHole (head xs)) && isHole (last xs) where xs = nameParts x
isPostfix x = isHole (head xs) && not (isHole (last xs)) where xs = nameParts x
isInfix x = isHole (head xs) && isHole (last xs) where xs = nameParts x
isNonfix x = not (isHole (head xs)) && not (isHole (last xs)) where xs = nameParts x
qualify :: QName -> Name -> QName
qualify (QName m) x = Qual m (QName x)
qualify (Qual m m') x = Qual m $ qualify m' x
unqualify :: QName -> Name
unqualify q = unqualify' q `withRangeOf` q
where
unqualify' (QName x) = x
unqualify' (Qual _ x) = unqualify' x
qnameParts :: QName -> [Name]
qnameParts (Qual x q) = x : qnameParts q
qnameParts (QName x) = [x]
isQualified :: QName -> Bool
isQualified Qual{} = True
isQualified QName{} = False
toTopLevelModuleName :: QName -> TopLevelModuleName
toTopLevelModuleName q = TopLevelModuleName (getRange q) $ map prettyShow $ qnameParts q
moduleNameToFileName :: TopLevelModuleName -> String -> FilePath
moduleNameToFileName (TopLevelModuleName _ []) ext = __IMPOSSIBLE__
moduleNameToFileName (TopLevelModuleName _ ms) ext =
joinPath (init ms) </> last ms <.> ext
projectRoot :: AbsolutePath -> TopLevelModuleName -> AbsolutePath
projectRoot file (TopLevelModuleName _ m) =
mkAbsolute $
foldr (.) id (replicate (length m - 1) takeDirectory) $
takeDirectory $
filePath file
noName_ :: Name
noName_ = noName noRange
noName :: Range -> Name
noName r = NoName r (NameId 0 0)
class IsNoName a where
isNoName :: a -> Bool
instance IsNoName String where
isNoName = isUnderscore
instance IsNoName ByteString where
isNoName = isUnderscore
instance IsNoName Name where
isNoName (NoName _ _) = True
isNoName (Name _ [Hole]) = True
isNoName (Name _ []) = True
isNoName (Name _ [Id x]) = isNoName x
isNoName _ = False
instance IsNoName QName where
isNoName (QName x) = isNoName x
isNoName Qual{} = False
instance Show Name where
show = prettyShow
instance Show NamePart where
show = prettyShow
instance Show QName where
show = prettyShow
instance Pretty Name where
pretty (Name _ xs) = hcat $ map pretty xs
pretty (NoName _ _) = text $ "_"
instance Pretty NamePart where
pretty Hole = text $ "_"
pretty (Id s) = text $ rawNameToString s
instance Pretty QName where
pretty (Qual m x)
| isUnderscore m = pretty x
| otherwise = pretty m <> pretty "." <> pretty x
pretty (QName x) = pretty x
instance Pretty TopLevelModuleName where
pretty (TopLevelModuleName _ ms) = text $ List.intercalate "." ms
instance HasRange Name where
getRange (Name r ps) = r
getRange (NoName r _) = r
instance HasRange QName where
getRange (QName x) = getRange x
getRange (Qual n x) = fuseRange n x
instance HasRange TopLevelModuleName where
getRange = moduleNameRange
instance SetRange Name where
setRange r (Name _ ps) = Name r ps
setRange r (NoName _ i) = NoName r i
instance SetRange QName where
setRange r (QName x) = QName (setRange r x)
setRange r (Qual n x) = Qual (setRange r n) (setRange r x)
instance SetRange TopLevelModuleName where
setRange r (TopLevelModuleName _ x) = TopLevelModuleName r x
instance KillRange QName where
killRange (QName x) = QName $ killRange x
killRange (Qual n x) = killRange n `Qual` killRange x
instance KillRange Name where
killRange (Name r ps) = Name (killRange r) ps
killRange (NoName r i) = NoName (killRange r) i
instance KillRange TopLevelModuleName where
killRange (TopLevelModuleName _ x) = TopLevelModuleName noRange x
instance NFData Name where
rnf (Name _ ns) = rnf ns
rnf (NoName _ n) = rnf n
instance NFData NamePart where
rnf Hole = ()
rnf (Id s) = rnf s
instance NFData QName where
rnf (Qual a b) = rnf a `seq` rnf b
rnf (QName a) = rnf a