module Agda.Syntax.Concrete.Name where
import Control.DeepSeq
import Control.Applicative
import Data.ByteString.Char8 (ByteString)
import Data.List
import Data.Typeable (Typeable)
import GHC.Generics (Generic)
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 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, 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 (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 = 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]
toTopLevelModuleName :: QName -> TopLevelModuleName
toTopLevelModuleName = TopLevelModuleName . map prettyShow . 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 = 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) = 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 Arbitrary Name where
arbitrary = oneof
[ Name <$> arbitrary <*> parts
, NoName <$> arbitrary <*> arbitrary
]
where
parts = do
parts <- listOf1 (elements ["x", "y", "z"])
startWithHole <- arbitrary
endWithHole <- arbitrary
return $
(if startWithHole then (Hole :) else id) $
(if endWithHole then (++ [Hole]) else id) $
intersperse Hole (map Id parts)
instance CoArbitrary NamePart
instance CoArbitrary Name where
coarbitrary (Name _ ns) = variant 0 . coarbitrary ns
coarbitrary (NoName _ i) = variant 1 . coarbitrary i
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
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