module Agda.Syntax.Concrete.Name where
import Control.Applicative
import Data.List
import Data.Maybe
import Data.Generics (Typeable, Data)
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, Data)
data NamePart = Hole | Id String
deriving (Typeable, Data)
noName_ :: Name
noName_ = noName noRange
noName :: Range -> Name
noName r = NoName r (NameId 0 0)
isNoName :: Name -> Bool
isNoName (NoName _ _) = True
isNoName (Name _ [Hole]) = True
isNoName (Name _ []) = True
isNoName _ = False
isOperator :: Name -> Bool
isOperator (NoName {}) = False
isOperator (Name _ ps) = length ps > 1
nameParts :: Name -> [NamePart]
nameParts (Name _ ps) = ps
nameParts (NoName _ _) = [Hole]
nameStringParts :: Name -> [String]
nameStringParts n = [ s | Id s <- nameParts n ]
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]
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, Data, Eq, Ord)
newtype TopLevelModuleName
= TopLevelModuleName { moduleNameParts :: [String] }
deriving (Show, Eq, Ord, Typeable, Data)
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
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
instance Show Name where
show (Name _ xs) = concatMap show xs
show (NoName _ _) = "_"
instance Show NamePart where
show Hole = "_"
show (Id s) = s
instance Show QName where
show (Qual m x) = show m ++ "." ++ show x
show (QName x) = show 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 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