module Agda.Syntax.TopLevelModuleName where
import Control.DeepSeq
import Data.Function
import Data.Hashable
import qualified Data.List as List
import Data.Text (Text)
import qualified Data.Text as T
import GHC.Generics (Generic)
import System.FilePath
import qualified Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Position
import Agda.Utils.BiMap (HasTag(..))
import Agda.Utils.FileName
import Agda.Utils.Hash
import Agda.Utils.Impossible
import Agda.Utils.Lens
import Agda.Utils.List1 (List1)
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Pretty
import Agda.Utils.Singleton
import Agda.Utils.Size
type TopLevelModuleNameParts = List1 Text
data RawTopLevelModuleName = RawTopLevelModuleName
{ RawTopLevelModuleName -> Range
rawModuleNameRange :: Range
, RawTopLevelModuleName -> TopLevelModuleNameParts
rawModuleNameParts :: TopLevelModuleNameParts
}
deriving (Int -> RawTopLevelModuleName -> ShowS
[RawTopLevelModuleName] -> ShowS
RawTopLevelModuleName -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [RawTopLevelModuleName] -> ShowS
$cshowList :: [RawTopLevelModuleName] -> ShowS
show :: RawTopLevelModuleName -> [Char]
$cshow :: RawTopLevelModuleName -> [Char]
showsPrec :: Int -> RawTopLevelModuleName -> ShowS
$cshowsPrec :: Int -> RawTopLevelModuleName -> ShowS
Show, forall x. Rep RawTopLevelModuleName x -> RawTopLevelModuleName
forall x. RawTopLevelModuleName -> Rep RawTopLevelModuleName x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep RawTopLevelModuleName x -> RawTopLevelModuleName
$cfrom :: forall x. RawTopLevelModuleName -> Rep RawTopLevelModuleName x
Generic)
instance Eq RawTopLevelModuleName where
== :: RawTopLevelModuleName -> RawTopLevelModuleName -> Bool
(==) = forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` RawTopLevelModuleName -> TopLevelModuleNameParts
rawModuleNameParts
instance Ord RawTopLevelModuleName where
compare :: RawTopLevelModuleName -> RawTopLevelModuleName -> Ordering
compare = forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` RawTopLevelModuleName -> TopLevelModuleNameParts
rawModuleNameParts
instance Sized RawTopLevelModuleName where
size :: RawTopLevelModuleName -> Int
size = forall a. Sized a => a -> Int
size forall b c a. (b -> c) -> (a -> b) -> a -> c
. RawTopLevelModuleName -> TopLevelModuleNameParts
rawModuleNameParts
instance Pretty RawTopLevelModuleName where
pretty :: RawTopLevelModuleName -> Doc
pretty = [Char] -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. RawTopLevelModuleName -> [Char]
rawTopLevelModuleNameToString
instance HasRange RawTopLevelModuleName where
getRange :: RawTopLevelModuleName -> Range
getRange = RawTopLevelModuleName -> Range
rawModuleNameRange
instance SetRange RawTopLevelModuleName where
setRange :: Range -> RawTopLevelModuleName -> RawTopLevelModuleName
setRange Range
r (RawTopLevelModuleName Range
_ TopLevelModuleNameParts
x) = Range -> TopLevelModuleNameParts -> RawTopLevelModuleName
RawTopLevelModuleName Range
r TopLevelModuleNameParts
x
instance KillRange RawTopLevelModuleName where
killRange :: RawTopLevelModuleName -> RawTopLevelModuleName
killRange (RawTopLevelModuleName Range
_ TopLevelModuleNameParts
x) =
Range -> TopLevelModuleNameParts -> RawTopLevelModuleName
RawTopLevelModuleName forall a. Range' a
noRange TopLevelModuleNameParts
x
instance C.IsNoName RawTopLevelModuleName where
isNoName :: RawTopLevelModuleName -> Bool
isNoName RawTopLevelModuleName
m = RawTopLevelModuleName -> TopLevelModuleNameParts
rawModuleNameParts RawTopLevelModuleName
m forall a. Eq a => a -> a -> Bool
== forall el coll. Singleton el coll => el -> coll
singleton Text
"_"
instance NFData RawTopLevelModuleName where
rnf :: RawTopLevelModuleName -> ()
rnf (RawTopLevelModuleName Range
_ TopLevelModuleNameParts
x) = forall a. NFData a => a -> ()
rnf TopLevelModuleNameParts
x
rawTopLevelModuleNameToString :: RawTopLevelModuleName -> String
rawTopLevelModuleNameToString :: RawTopLevelModuleName -> [Char]
rawTopLevelModuleNameToString =
forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
"." forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall a b. (a -> b) -> [a] -> [b]
map Text -> [Char]
T.unpack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l. IsList l => l -> [Item l]
List1.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. RawTopLevelModuleName -> TopLevelModuleNameParts
rawModuleNameParts
hashRawTopLevelModuleName :: RawTopLevelModuleName -> ModuleNameHash
hashRawTopLevelModuleName :: RawTopLevelModuleName -> ModuleNameHash
hashRawTopLevelModuleName =
Word64 -> ModuleNameHash
ModuleNameHash forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Word64
hashString forall b c a. (b -> c) -> (a -> b) -> a -> c
. RawTopLevelModuleName -> [Char]
rawTopLevelModuleNameToString
rawTopLevelModuleNameForQName :: C.QName -> RawTopLevelModuleName
rawTopLevelModuleNameForQName :: QName -> RawTopLevelModuleName
rawTopLevelModuleNameForQName QName
q = RawTopLevelModuleName
{ rawModuleNameRange :: Range
rawModuleNameRange = forall a. HasRange a => a -> Range
getRange QName
q
, rawModuleNameParts :: TopLevelModuleNameParts
rawModuleNameParts =
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char] -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
C.nameToRawName) forall a b. (a -> b) -> a -> b
$ QName -> List1 Name
C.qnameParts QName
q
}
rawTopLevelModuleNameForModuleName ::
A.ModuleName -> RawTopLevelModuleName
rawTopLevelModuleNameForModuleName :: ModuleName -> RawTopLevelModuleName
rawTopLevelModuleNameForModuleName (A.MName []) = forall a. HasCallStack => a
__IMPOSSIBLE__
rawTopLevelModuleNameForModuleName (A.MName [Name]
ms) =
forall a b. [a] -> b -> (List1 a -> b) -> b
List1.ifNull [Name]
ms forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ \List1 Name
ms ->
RawTopLevelModuleName
{ rawModuleNameRange :: Range
rawModuleNameRange = forall a. HasRange a => a -> Range
getRange List1 Name
ms
, rawModuleNameParts :: TopLevelModuleNameParts
rawModuleNameParts =
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char] -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
C.nameToRawName forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
A.nameConcrete) List1 Name
ms
}
rawTopLevelModuleNameForModule :: C.Module -> RawTopLevelModuleName
rawTopLevelModuleNameForModule :: Module -> RawTopLevelModuleName
rawTopLevelModuleNameForModule (C.Mod [Pragma]
_ []) = forall a. HasCallStack => a
__IMPOSSIBLE__
rawTopLevelModuleNameForModule (C.Mod [Pragma]
_ [Declaration]
ds) =
case [Declaration] -> ([Declaration], [Declaration])
C.spanAllowedBeforeModule [Declaration]
ds of
([Declaration]
_, C.Module Range
_ QName
n Telescope
_ [Declaration]
_ : [Declaration]
_) -> QName -> RawTopLevelModuleName
rawTopLevelModuleNameForQName QName
n
([Declaration], [Declaration])
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
data TopLevelModuleName = TopLevelModuleName
{ TopLevelModuleName -> Range
moduleNameRange :: Range
, TopLevelModuleName -> ModuleNameHash
moduleNameId :: {-# UNPACK #-} !ModuleNameHash
, TopLevelModuleName -> TopLevelModuleNameParts
moduleNameParts :: TopLevelModuleNameParts
}
deriving (Int -> TopLevelModuleName -> ShowS
[TopLevelModuleName] -> ShowS
TopLevelModuleName -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [TopLevelModuleName] -> ShowS
$cshowList :: [TopLevelModuleName] -> ShowS
show :: TopLevelModuleName -> [Char]
$cshow :: TopLevelModuleName -> [Char]
showsPrec :: Int -> TopLevelModuleName -> ShowS
$cshowsPrec :: Int -> TopLevelModuleName -> ShowS
Show, forall x. Rep TopLevelModuleName x -> TopLevelModuleName
forall x. TopLevelModuleName -> Rep TopLevelModuleName x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TopLevelModuleName x -> TopLevelModuleName
$cfrom :: forall x. TopLevelModuleName -> Rep TopLevelModuleName x
Generic)
instance HasTag TopLevelModuleName where
type Tag TopLevelModuleName = ModuleNameHash
tag :: TopLevelModuleName -> Maybe (Tag TopLevelModuleName)
tag = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. TopLevelModuleName -> ModuleNameHash
moduleNameId
instance Eq TopLevelModuleName where
== :: TopLevelModuleName -> TopLevelModuleName -> Bool
(==) = forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` TopLevelModuleName -> ModuleNameHash
moduleNameId
instance Ord TopLevelModuleName where
compare :: TopLevelModuleName -> TopLevelModuleName -> Ordering
compare = forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` TopLevelModuleName -> ModuleNameHash
moduleNameId
instance Hashable TopLevelModuleName where
hashWithSalt :: Int -> TopLevelModuleName -> Int
hashWithSalt Int
salt = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt forall b c a. (b -> c) -> (a -> b) -> a -> c
. TopLevelModuleName -> ModuleNameHash
moduleNameId
instance Sized TopLevelModuleName where
size :: TopLevelModuleName -> Int
size = forall a. Sized a => a -> Int
size forall b c a. (b -> c) -> (a -> b) -> a -> c
. TopLevelModuleName -> RawTopLevelModuleName
rawTopLevelModuleName
instance Pretty TopLevelModuleName where
pretty :: TopLevelModuleName -> Doc
pretty = forall a. Pretty a => a -> Doc
pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. TopLevelModuleName -> RawTopLevelModuleName
rawTopLevelModuleName
instance HasRange TopLevelModuleName where
getRange :: TopLevelModuleName -> Range
getRange = TopLevelModuleName -> Range
moduleNameRange
instance SetRange TopLevelModuleName where
setRange :: Range -> TopLevelModuleName -> TopLevelModuleName
setRange Range
r (TopLevelModuleName Range
_ ModuleNameHash
h TopLevelModuleNameParts
x) = Range
-> ModuleNameHash -> TopLevelModuleNameParts -> TopLevelModuleName
TopLevelModuleName Range
r ModuleNameHash
h TopLevelModuleNameParts
x
instance KillRange TopLevelModuleName where
killRange :: TopLevelModuleName -> TopLevelModuleName
killRange (TopLevelModuleName Range
_ ModuleNameHash
h TopLevelModuleNameParts
x) = Range
-> ModuleNameHash -> TopLevelModuleNameParts -> TopLevelModuleName
TopLevelModuleName forall a. Range' a
noRange ModuleNameHash
h TopLevelModuleNameParts
x
instance NFData TopLevelModuleName where
rnf :: TopLevelModuleName -> ()
rnf (TopLevelModuleName Range
_ ModuleNameHash
x TopLevelModuleNameParts
y) = forall a. NFData a => a -> ()
rnf (ModuleNameHash
x, TopLevelModuleNameParts
y)
lensTopLevelModuleNameParts ::
Lens' TopLevelModuleNameParts TopLevelModuleName
lensTopLevelModuleNameParts :: Lens' TopLevelModuleNameParts TopLevelModuleName
lensTopLevelModuleNameParts TopLevelModuleNameParts -> f TopLevelModuleNameParts
f TopLevelModuleName
m =
TopLevelModuleNameParts -> f TopLevelModuleNameParts
f (TopLevelModuleName -> TopLevelModuleNameParts
moduleNameParts TopLevelModuleName
m) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ TopLevelModuleNameParts
xs -> TopLevelModuleName
m{ moduleNameParts :: TopLevelModuleNameParts
moduleNameParts = TopLevelModuleNameParts
xs }
rawTopLevelModuleName :: TopLevelModuleName -> RawTopLevelModuleName
rawTopLevelModuleName :: TopLevelModuleName -> RawTopLevelModuleName
rawTopLevelModuleName TopLevelModuleName
m = RawTopLevelModuleName
{ rawModuleNameRange :: Range
rawModuleNameRange = TopLevelModuleName -> Range
moduleNameRange TopLevelModuleName
m
, rawModuleNameParts :: TopLevelModuleNameParts
rawModuleNameParts = TopLevelModuleName -> TopLevelModuleNameParts
moduleNameParts TopLevelModuleName
m
}
unsafeTopLevelModuleName ::
RawTopLevelModuleName -> ModuleNameHash -> TopLevelModuleName
unsafeTopLevelModuleName :: RawTopLevelModuleName -> ModuleNameHash -> TopLevelModuleName
unsafeTopLevelModuleName RawTopLevelModuleName
m ModuleNameHash
h = TopLevelModuleName
{ moduleNameRange :: Range
moduleNameRange = RawTopLevelModuleName -> Range
rawModuleNameRange RawTopLevelModuleName
m
, moduleNameParts :: TopLevelModuleNameParts
moduleNameParts = RawTopLevelModuleName -> TopLevelModuleNameParts
rawModuleNameParts RawTopLevelModuleName
m
, moduleNameId :: ModuleNameHash
moduleNameId = ModuleNameHash
h
}
topLevelModuleNameToQName :: TopLevelModuleName -> C.QName
topLevelModuleNameToQName :: TopLevelModuleName -> QName
topLevelModuleNameToQName TopLevelModuleName
m =
forall a b. (a -> b -> b) -> (a -> b) -> List1 a -> b
List1.foldr Name -> QName -> QName
C.Qual Name -> QName
C.QName forall a b. (a -> b) -> a -> b
$
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Range -> NameInScope -> NameParts -> Name
C.Name (forall a. HasRange a => a -> Range
getRange TopLevelModuleName
m) NameInScope
C.NotInScope forall b c a. (b -> c) -> (a -> b) -> a -> c
.
[Char] -> NameParts
C.stringNameParts forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Char]
T.unpack) forall a b. (a -> b) -> a -> b
$
TopLevelModuleName -> TopLevelModuleNameParts
moduleNameParts TopLevelModuleName
m
moduleNameToFileName :: TopLevelModuleName -> String -> FilePath
moduleNameToFileName :: TopLevelModuleName -> ShowS
moduleNameToFileName TopLevelModuleName{ moduleNameParts :: TopLevelModuleName -> TopLevelModuleNameParts
moduleNameParts = TopLevelModuleNameParts
ms } [Char]
ext =
[[Char]] -> [Char]
joinPath (forall a b. (a -> b) -> [a] -> [b]
map Text -> [Char]
T.unpack forall a b. (a -> b) -> a -> b
$ forall a. NonEmpty a -> [a]
List1.init TopLevelModuleNameParts
ms) [Char] -> ShowS
</>
Text -> [Char]
T.unpack (forall a. NonEmpty a -> a
List1.last TopLevelModuleNameParts
ms) [Char] -> ShowS
<.> [Char]
ext
projectRoot :: AbsolutePath -> TopLevelModuleName -> AbsolutePath
projectRoot :: AbsolutePath -> TopLevelModuleName -> AbsolutePath
projectRoot AbsolutePath
file TopLevelModuleName{ moduleNameParts :: TopLevelModuleName -> TopLevelModuleNameParts
moduleNameParts = TopLevelModuleNameParts
m } =
[Char] -> AbsolutePath
mkAbsolute forall a b. (a -> b) -> a -> b
$
forall a. (a -> a) -> a -> [a]
iterate ShowS
takeDirectory (AbsolutePath -> [Char]
filePath AbsolutePath
file) forall a. [a] -> Int -> a
!! forall (t :: * -> *) a. Foldable t => t a -> Int
length TopLevelModuleNameParts
m