{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -Wunused-matches #-}

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

module Agda.Syntax.TopLevelModuleName
  ( module Agda.Syntax.TopLevelModuleName
  , module Agda.Syntax.TopLevelModuleName.Boot
  ) where

import Agda.Syntax.TopLevelModuleName.Boot
import Agda.Syntax.Abstract.Name (isNoName)

import Control.DeepSeq

import Data.Function (on)
import qualified Data.List as List
import qualified Data.Text as T

import GHC.Generics (Generic)

import System.FilePath

import qualified Agda.Syntax.Abstract.Name as A
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Position

import Agda.Utils.FileName
import Agda.Utils.Function (iterate')
import Agda.Utils.Hash
import Agda.Utils.Impossible
import Agda.Utils.Lens
import qualified Agda.Utils.List1 as List1
import Agda.Syntax.Common.Pretty
import Agda.Utils.Singleton
import Agda.Utils.Size

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

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

data RawTopLevelModuleName = RawTopLevelModuleName
  { RawTopLevelModuleName -> Range
rawModuleNameRange :: Range
  , RawTopLevelModuleName -> NonEmpty Text
rawModuleNameParts :: TopLevelModuleNameParts
  , RawTopLevelModuleName -> Bool
rawModuleNameInferred :: !Bool
      -- ^ Was this module name constructed from a file name
      --   rather than declared in the file?
  }
  deriving (Int -> RawTopLevelModuleName -> ShowS
[RawTopLevelModuleName] -> ShowS
RawTopLevelModuleName -> [Char]
(Int -> RawTopLevelModuleName -> ShowS)
-> (RawTopLevelModuleName -> [Char])
-> ([RawTopLevelModuleName] -> ShowS)
-> Show RawTopLevelModuleName
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RawTopLevelModuleName -> ShowS
showsPrec :: Int -> RawTopLevelModuleName -> ShowS
$cshow :: RawTopLevelModuleName -> [Char]
show :: RawTopLevelModuleName -> [Char]
$cshowList :: [RawTopLevelModuleName] -> ShowS
showList :: [RawTopLevelModuleName] -> ShowS
Show, (forall x. RawTopLevelModuleName -> Rep RawTopLevelModuleName x)
-> (forall x. Rep RawTopLevelModuleName x -> RawTopLevelModuleName)
-> Generic RawTopLevelModuleName
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
$cfrom :: forall x. RawTopLevelModuleName -> Rep RawTopLevelModuleName x
from :: forall x. RawTopLevelModuleName -> Rep RawTopLevelModuleName x
$cto :: forall x. Rep RawTopLevelModuleName x -> RawTopLevelModuleName
to :: forall x. Rep RawTopLevelModuleName x -> RawTopLevelModuleName
Generic)

instance Eq RawTopLevelModuleName where
  == :: RawTopLevelModuleName -> RawTopLevelModuleName -> Bool
(==) = NonEmpty Text -> NonEmpty Text -> Bool
forall a. Eq a => a -> a -> Bool
(==) (NonEmpty Text -> NonEmpty Text -> Bool)
-> (RawTopLevelModuleName -> NonEmpty Text)
-> RawTopLevelModuleName
-> RawTopLevelModuleName
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` RawTopLevelModuleName -> NonEmpty Text
rawModuleNameParts

instance Ord RawTopLevelModuleName where
  compare :: RawTopLevelModuleName -> RawTopLevelModuleName -> Ordering
compare = NonEmpty Text -> NonEmpty Text -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (NonEmpty Text -> NonEmpty Text -> Ordering)
-> (RawTopLevelModuleName -> NonEmpty Text)
-> RawTopLevelModuleName
-> RawTopLevelModuleName
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` RawTopLevelModuleName -> NonEmpty Text
rawModuleNameParts

instance Sized RawTopLevelModuleName where
  size :: RawTopLevelModuleName -> Int
size = NonEmpty Text -> Int
forall a. Sized a => a -> Int
size (NonEmpty Text -> Int)
-> (RawTopLevelModuleName -> NonEmpty Text)
-> RawTopLevelModuleName
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RawTopLevelModuleName -> NonEmpty Text
rawModuleNameParts
  natSize :: RawTopLevelModuleName -> Peano
natSize = NonEmpty Text -> Peano
forall a. Sized a => a -> Peano
natSize (NonEmpty Text -> Peano)
-> (RawTopLevelModuleName -> NonEmpty Text)
-> RawTopLevelModuleName
-> Peano
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RawTopLevelModuleName -> NonEmpty Text
rawModuleNameParts

instance Pretty RawTopLevelModuleName where
  pretty :: RawTopLevelModuleName -> Doc
pretty = [Char] -> Doc
forall a. [Char] -> Doc a
text ([Char] -> Doc)
-> (RawTopLevelModuleName -> [Char])
-> RawTopLevelModuleName
-> Doc
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
_ NonEmpty Text
x Bool
z) = Range -> NonEmpty Text -> Bool -> RawTopLevelModuleName
RawTopLevelModuleName Range
r NonEmpty Text
x Bool
z

instance KillRange RawTopLevelModuleName where
  killRange :: RawTopLevelModuleName -> RawTopLevelModuleName
killRange (RawTopLevelModuleName Range
_ NonEmpty Text
x Bool
z) =
    Range -> NonEmpty Text -> Bool -> RawTopLevelModuleName
RawTopLevelModuleName Range
forall a. Range' a
noRange NonEmpty Text
x Bool
z

instance C.IsNoName RawTopLevelModuleName where
  isNoName :: RawTopLevelModuleName -> Bool
isNoName RawTopLevelModuleName
m = RawTopLevelModuleName -> NonEmpty Text
rawModuleNameParts RawTopLevelModuleName
m NonEmpty Text -> NonEmpty Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text -> NonEmpty Text
forall el coll. Singleton el coll => el -> coll
singleton Text
"_"

-- | The 'Range' is not forced.

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

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

rawTopLevelModuleNameToString :: RawTopLevelModuleName -> String
rawTopLevelModuleNameToString :: RawTopLevelModuleName -> [Char]
rawTopLevelModuleNameToString =
  [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
"." ([[Char]] -> [Char])
-> (RawTopLevelModuleName -> [[Char]])
-> RawTopLevelModuleName
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  (Text -> [Char]) -> [Text] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Text -> [Char]
T.unpack ([Text] -> [[Char]])
-> (RawTopLevelModuleName -> [Text])
-> RawTopLevelModuleName
-> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty Text -> [Item (NonEmpty Text)]
NonEmpty Text -> [Text]
forall l. IsList l => l -> [Item l]
List1.toList (NonEmpty Text -> [Text])
-> (RawTopLevelModuleName -> NonEmpty Text)
-> RawTopLevelModuleName
-> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RawTopLevelModuleName -> NonEmpty Text
rawModuleNameParts

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

hashRawTopLevelModuleName :: RawTopLevelModuleName -> ModuleNameHash
hashRawTopLevelModuleName :: RawTopLevelModuleName -> ModuleNameHash
hashRawTopLevelModuleName =
  Word64 -> ModuleNameHash
ModuleNameHash (Word64 -> ModuleNameHash)
-> (RawTopLevelModuleName -> Word64)
-> RawTopLevelModuleName
-> ModuleNameHash
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Word64
hashString ([Char] -> Word64)
-> (RawTopLevelModuleName -> [Char])
-> RawTopLevelModuleName
-> Word64
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 = QName -> Range
forall a. HasRange a => a -> Range
getRange QName
q
  , rawModuleNameParts :: NonEmpty Text
rawModuleNameParts =
      (Name -> Text) -> NonEmpty Name -> NonEmpty Text
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char] -> Text
T.pack ([Char] -> Text) -> (Name -> [Char]) -> Name -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
C.nameToRawName) (NonEmpty Name -> NonEmpty Text) -> NonEmpty Name -> NonEmpty Text
forall a b. (a -> b) -> a -> b
$ QName -> NonEmpty Name
C.qnameParts QName
q
  , rawModuleNameInferred :: Bool
rawModuleNameInferred = QName -> Bool
forall a. IsNoName a => a -> Bool
C.isNoName 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 x :: ModuleName
x@(A.MName [Name]
ms) =
  [Name]
-> RawTopLevelModuleName
-> (NonEmpty Name -> RawTopLevelModuleName)
-> RawTopLevelModuleName
forall a b. [a] -> b -> (List1 a -> b) -> b
List1.ifNull [Name]
ms RawTopLevelModuleName
forall a. HasCallStack => a
__IMPOSSIBLE__ ((NonEmpty Name -> RawTopLevelModuleName) -> RawTopLevelModuleName)
-> (NonEmpty Name -> RawTopLevelModuleName)
-> RawTopLevelModuleName
forall a b. (a -> b) -> a -> b
$ \NonEmpty Name
ms ->
  RawTopLevelModuleName
    { rawModuleNameRange :: Range
rawModuleNameRange = NonEmpty Name -> Range
forall a. HasRange a => a -> Range
getRange NonEmpty Name
ms
    , rawModuleNameParts :: NonEmpty Text
rawModuleNameParts =
        (Name -> Text) -> NonEmpty Name -> NonEmpty Text
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char] -> Text
T.pack ([Char] -> Text) -> (Name -> [Char]) -> Name -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
C.nameToRawName (Name -> [Char]) -> (Name -> Name) -> Name -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
A.nameConcrete) NonEmpty Name
ms
    , rawModuleNameInferred :: Bool
rawModuleNameInferred = ModuleName -> Bool
forall a. IsNoName a => a -> Bool
isNoName ModuleName
x
    }

-- | Retrieves the top-level module name.

rawTopLevelModuleNameForModule :: C.Module -> RawTopLevelModuleName
rawTopLevelModuleNameForModule :: Module -> RawTopLevelModuleName
rawTopLevelModuleNameForModule (C.Mod QName
n [Pragma]
_pragmas [Declaration]
_decls) = QName -> RawTopLevelModuleName
rawTopLevelModuleNameForQName QName
n

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

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

type TopLevelModuleName = TopLevelModuleName' Range

instance Sized TopLevelModuleName where
  size :: TopLevelModuleName' Range -> Int
size = RawTopLevelModuleName -> Int
forall a. Sized a => a -> Int
size (RawTopLevelModuleName -> Int)
-> (TopLevelModuleName' Range -> RawTopLevelModuleName)
-> TopLevelModuleName' Range
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TopLevelModuleName' Range -> RawTopLevelModuleName
rawTopLevelModuleName
  natSize :: TopLevelModuleName' Range -> Peano
natSize = RawTopLevelModuleName -> Peano
forall a. Sized a => a -> Peano
natSize (RawTopLevelModuleName -> Peano)
-> (TopLevelModuleName' Range -> RawTopLevelModuleName)
-> TopLevelModuleName' Range
-> Peano
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TopLevelModuleName' Range -> RawTopLevelModuleName
rawTopLevelModuleName

instance Pretty TopLevelModuleName where
  pretty :: TopLevelModuleName' Range -> Doc
pretty = RawTopLevelModuleName -> Doc
forall a. Pretty a => a -> Doc
pretty (RawTopLevelModuleName -> Doc)
-> (TopLevelModuleName' Range -> RawTopLevelModuleName)
-> TopLevelModuleName' Range
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TopLevelModuleName' Range -> RawTopLevelModuleName
rawTopLevelModuleName

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

lensTopLevelModuleNameParts ::
  Lens' TopLevelModuleName TopLevelModuleNameParts
lensTopLevelModuleNameParts :: Lens' (TopLevelModuleName' Range) (NonEmpty Text)
lensTopLevelModuleNameParts NonEmpty Text -> f (NonEmpty Text)
f TopLevelModuleName' Range
m =
  NonEmpty Text -> f (NonEmpty Text)
f (TopLevelModuleName' Range -> NonEmpty Text
forall range. TopLevelModuleName' range -> NonEmpty Text
moduleNameParts TopLevelModuleName' Range
m) f (NonEmpty Text)
-> (NonEmpty Text -> TopLevelModuleName' Range)
-> f (TopLevelModuleName' Range)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ NonEmpty Text
xs -> TopLevelModuleName' Range
m{ moduleNameParts = xs }

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

rawTopLevelModuleName :: TopLevelModuleName -> RawTopLevelModuleName
rawTopLevelModuleName :: TopLevelModuleName' Range -> RawTopLevelModuleName
rawTopLevelModuleName TopLevelModuleName' Range
m = RawTopLevelModuleName
  { rawModuleNameRange :: Range
rawModuleNameRange = TopLevelModuleName' Range -> Range
forall range. TopLevelModuleName' range -> range
moduleNameRange TopLevelModuleName' Range
m
  , rawModuleNameParts :: NonEmpty Text
rawModuleNameParts = TopLevelModuleName' Range -> NonEmpty Text
forall range. TopLevelModuleName' range -> NonEmpty Text
moduleNameParts TopLevelModuleName' Range
m
  , rawModuleNameInferred :: Bool
rawModuleNameInferred = TopLevelModuleName' Range -> Bool
forall range. TopLevelModuleName' range -> Bool
moduleNameInferred TopLevelModuleName' Range
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' Range
unsafeTopLevelModuleName RawTopLevelModuleName
m ModuleNameHash
h = TopLevelModuleName
  { moduleNameRange :: Range
moduleNameRange = RawTopLevelModuleName -> Range
rawModuleNameRange RawTopLevelModuleName
m
  , moduleNameParts :: NonEmpty Text
moduleNameParts = RawTopLevelModuleName -> NonEmpty Text
rawModuleNameParts RawTopLevelModuleName
m
  , moduleNameId :: ModuleNameHash
moduleNameId    = ModuleNameHash
h
  , moduleNameInferred :: Bool
moduleNameInferred = RawTopLevelModuleName -> Bool
rawModuleNameInferred RawTopLevelModuleName
m
  }

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

topLevelModuleNameToQName :: TopLevelModuleName -> C.QName
topLevelModuleNameToQName :: TopLevelModuleName' Range -> QName
topLevelModuleNameToQName TopLevelModuleName' Range
m =
  (Name -> QName -> QName)
-> (Name -> QName) -> NonEmpty Name -> QName
forall a b. (a -> b -> b) -> (a -> b) -> List1 a -> b
List1.foldr Name -> QName -> QName
C.Qual Name -> QName
C.QName (NonEmpty Name -> QName) -> NonEmpty Name -> QName
forall a b. (a -> b) -> a -> b
$
  (Text -> Name) -> NonEmpty Text -> NonEmpty Name
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Range -> NameInScope -> NameParts -> Name
C.Name (TopLevelModuleName' Range -> Range
forall a. HasRange a => a -> Range
getRange TopLevelModuleName' Range
m) NameInScope
C.NotInScope (NameParts -> Name) -> (Text -> NameParts) -> Text -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        [Char] -> NameParts
C.stringNameParts ([Char] -> NameParts) -> (Text -> [Char]) -> Text -> NameParts
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Char]
T.unpack) (NonEmpty Text -> NonEmpty Name) -> NonEmpty Text -> NonEmpty Name
forall a b. (a -> b) -> a -> b
$
  TopLevelModuleName' Range -> NonEmpty Text
forall range. TopLevelModuleName' range -> NonEmpty Text
moduleNameParts TopLevelModuleName' Range
m

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

moduleNameToFileName :: TopLevelModuleName -> String -> FilePath
moduleNameToFileName :: TopLevelModuleName' Range -> ShowS
moduleNameToFileName TopLevelModuleName{ moduleNameParts :: forall range. TopLevelModuleName' range -> NonEmpty Text
moduleNameParts = NonEmpty Text
ms } [Char]
ext =
  [[Char]] -> [Char]
joinPath ((Text -> [Char]) -> [Text] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Text -> [Char]
T.unpack ([Text] -> [[Char]]) -> [Text] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ NonEmpty Text -> [Text]
forall a. NonEmpty a -> [a]
List1.init NonEmpty Text
ms) [Char] -> ShowS
</>
  Text -> [Char]
T.unpack (NonEmpty Text -> Text
forall a. NonEmpty a -> a
List1.last NonEmpty Text
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' Range -> AbsolutePath
projectRoot AbsolutePath
file TopLevelModuleName{ moduleNameParts :: forall range. TopLevelModuleName' range -> NonEmpty Text
moduleNameParts = NonEmpty Text
m } =
  [Char] -> AbsolutePath
mkAbsolute ([Char] -> AbsolutePath) -> [Char] -> AbsolutePath
forall a b. (a -> b) -> a -> b
$ Int -> ShowS -> ShowS
forall i a. Integral i => i -> (a -> a) -> a -> a
iterate' (NonEmpty Text -> Int
forall a. NonEmpty a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty Text
m) ShowS
takeDirectory ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> [Char]
filePath AbsolutePath
file