------------------------------------------------------------------------
-- Top-level module names
------------------------------------------------------------------------

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

------------------------------------------------------------------------
-- Raw top-level module names

-- | A top-level module name has one or more name parts.

type TopLevelModuleNameParts = List1 Text

-- | Raw top-level module names (with linear-time comparisons).

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
"_"

-- | The 'Range' is not forced.

instance NFData RawTopLevelModuleName where
  rnf :: RawTopLevelModuleName -> ()
rnf (RawTopLevelModuleName Range
_ TopLevelModuleNameParts
x) = forall a. NFData a => a -> ()
rnf TopLevelModuleNameParts
x

-- | Turns a raw top-level module name into a string.

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

-- | Hashes a raw top-level module name.

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

-- | Turns a qualified name into a 'RawTopLevelModuleName'. The
-- qualified name is assumed to represent a top-level module name.

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
  }

-- | Computes the 'RawTopLevelModuleName' corresponding to the given
-- module name, which is assumed to represent a top-level module name.
--
-- Precondition: The module name must be well-formed.

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
    }

-- | Computes the top-level module name.
--
-- Precondition: The 'C.Module' has to be well-formed.
-- This means that there are only allowed declarations before the
-- first module declaration, typically import declarations.
-- See 'spanAllowedBeforeModule'.

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__

------------------------------------------------------------------------
-- Top-level module names

-- | Top-level module names (with constant-time comparisons).

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

-- | The 'Range' is not forced.

instance NFData TopLevelModuleName where
  rnf :: TopLevelModuleName -> ()
rnf (TopLevelModuleName Range
_ ModuleNameHash
x TopLevelModuleNameParts
y) = forall a. NFData a => a -> ()
rnf (ModuleNameHash
x, TopLevelModuleNameParts
y)

-- | A lens focusing on the 'moduleNameParts'.

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 }

-- | Converts a top-level module name to a raw top-level module name.

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
  }

-- | Converts a raw top-level module name and a hash to a top-level
-- module name.
--
-- This function does not ensure that there are no hash collisions,
-- that is taken care of by
-- 'Agda.TypeChecking.Monad.State.topLevelModuleName'.

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
  }

-- | A corresponding 'C.QName'. The range of each 'Name' part is the
-- whole range of the 'TopLevelModuleName'.

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

-- | Turns a top-level module name into a file name with the given
-- suffix.

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

-- | Finds the current project's \"root\" directory, given a project
-- file and the corresponding top-level module name.
--
-- Example: If the module \"A.B.C\" is located in the file
-- \"/foo/A/B/C.agda\", then the root is \"/foo/\".
--
-- Precondition: The module name must be well-formed.

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