module Agda.Syntax.Concrete.Name where
import Control.DeepSeq
import Control.Applicative
import Data.ByteString.Char8 (ByteString)
import qualified Data.ByteString.Char8 as ByteString
import Data.List
import Data.Typeable (Typeable)
import System.FilePath
import Test.QuickCheck
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Utils.FileName
import Agda.Utils.Pretty
#include "undefined.h"
import Agda.Utils.Impossible
data Name
= Name !Range [NamePart]
| NoName !Range NameId
deriving (Typeable)
instance NFData Name
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 (Typeable)
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 (Typeable, Eq, Ord)
instance Underscore QName where
underscore = QName underscore
isUnderscore (QName x) = isUnderscore x
isUnderscore Qual{} = False
newtype TopLevelModuleName
= TopLevelModuleName { moduleNameParts :: [String] }
deriving (Show, Eq, Ord, Typeable)
nameToRawName :: Name -> RawName
nameToRawName = show
nameParts :: Name -> [NamePart]
nameParts (Name _ ps) = ps
nameParts (NoName _ _) = [Hole]
nameStringParts :: Name -> [RawName]
nameStringParts n = [ s | Id s <- nameParts n ]
stringNameParts :: String -> [NamePart]
stringNameParts "" = []
stringNameParts ('_':s) = Hole : stringNameParts s
stringNameParts s | (x, s') <- break (== '_') s = Id (stringToRawName x) : stringNameParts s'
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]
toTopLevelModuleName :: QName -> TopLevelModuleName
toTopLevelModuleName = TopLevelModuleName . map show . qnameParts
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 _ = False
instance IsNoName QName where
isNoName (QName x) = isNoName x
isNoName Qual{} = False
instance Show Name where
show (Name _ xs) = concatMap show xs
show (NoName _ _) = "_"
instance Show NamePart where
show Hole = "_"
show (Id s) = rawNameToString s
instance Show QName where
show (Qual m x) = show m ++ "." ++ show x
show (QName x) = show x
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) = pretty m <> pretty "." <> pretty x
pretty (QName x) = pretty x
instance Pretty TopLevelModuleName where
pretty (TopLevelModuleName ms) = text $ intercalate "." ms
instance Arbitrary TopLevelModuleName where
arbitrary = TopLevelModuleName <$> listOf1 (listOf1 $ elements "AB")
instance CoArbitrary TopLevelModuleName where
coarbitrary (TopLevelModuleName m) = coarbitrary m
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 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 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