{-# OPTIONS_GHC -Wunused-imports #-}

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

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

import Agda.Syntax.TopLevelModuleName.Boot

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.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 -> TopLevelModuleNameParts
rawModuleNameParts :: TopLevelModuleNameParts
  }
  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
(==) = TopLevelModuleNameParts -> TopLevelModuleNameParts -> Bool
forall a. Eq a => a -> a -> Bool
(==) (TopLevelModuleNameParts -> TopLevelModuleNameParts -> Bool)
-> (RawTopLevelModuleName -> TopLevelModuleNameParts)
-> RawTopLevelModuleName
-> RawTopLevelModuleName
-> 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 = TopLevelModuleNameParts -> TopLevelModuleNameParts -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (TopLevelModuleNameParts -> TopLevelModuleNameParts -> Ordering)
-> (RawTopLevelModuleName -> TopLevelModuleNameParts)
-> RawTopLevelModuleName
-> RawTopLevelModuleName
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` RawTopLevelModuleName -> TopLevelModuleNameParts
rawModuleNameParts

instance Sized RawTopLevelModuleName where
  size :: RawTopLevelModuleName -> Int
size = TopLevelModuleNameParts -> Int
forall a. Sized a => a -> Int
size (TopLevelModuleNameParts -> Int)
-> (RawTopLevelModuleName -> TopLevelModuleNameParts)
-> RawTopLevelModuleName
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RawTopLevelModuleName -> TopLevelModuleNameParts
rawModuleNameParts
  natSize :: RawTopLevelModuleName -> Peano
natSize = TopLevelModuleNameParts -> Peano
forall a. Sized a => a -> Peano
natSize (TopLevelModuleNameParts -> Peano)
-> (RawTopLevelModuleName -> TopLevelModuleNameParts)
-> RawTopLevelModuleName
-> Peano
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RawTopLevelModuleName -> TopLevelModuleNameParts
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
_ 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 Range
forall a. Range' a
noRange TopLevelModuleNameParts
x

instance C.IsNoName RawTopLevelModuleName where
  isNoName :: RawTopLevelModuleName -> Bool
isNoName RawTopLevelModuleName
m = RawTopLevelModuleName -> TopLevelModuleNameParts
rawModuleNameParts RawTopLevelModuleName
m TopLevelModuleNameParts -> TopLevelModuleNameParts -> Bool
forall a. Eq a => a -> a -> Bool
== Text -> TopLevelModuleNameParts
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) = TopLevelModuleNameParts -> ()
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 =
  [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
. TopLevelModuleNameParts -> [Item TopLevelModuleNameParts]
TopLevelModuleNameParts -> [Text]
forall l. IsList l => l -> [Item l]
List1.toList (TopLevelModuleNameParts -> [Text])
-> (RawTopLevelModuleName -> TopLevelModuleNameParts)
-> RawTopLevelModuleName
-> [Text]
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 (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 :: TopLevelModuleNameParts
rawModuleNameParts =
      (Name -> Text) -> NonEmpty Name -> TopLevelModuleNameParts
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 -> TopLevelModuleNameParts)
-> NonEmpty Name -> TopLevelModuleNameParts
forall a b. (a -> b) -> a -> b
$ QName -> NonEmpty 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 []) = RawTopLevelModuleName
forall a. HasCallStack => a
__IMPOSSIBLE__
rawTopLevelModuleNameForModuleName (A.MName [Name]
ms) =
  [Name]
-> RawTopLevelModuleName
-> (List1 Name -> RawTopLevelModuleName)
-> RawTopLevelModuleName
forall a b. [a] -> b -> (List1 a -> b) -> b
List1.ifNull [Name]
ms RawTopLevelModuleName
forall a. HasCallStack => a
__IMPOSSIBLE__ ((List1 Name -> RawTopLevelModuleName) -> RawTopLevelModuleName)
-> (List1 Name -> RawTopLevelModuleName) -> RawTopLevelModuleName
forall a b. (a -> b) -> a -> b
$ \List1 Name
ms ->
  RawTopLevelModuleName
    { rawModuleNameRange :: Range
rawModuleNameRange = List1 Name -> Range
forall a. HasRange a => a -> Range
getRange List1 Name
ms
    , rawModuleNameParts :: TopLevelModuleNameParts
rawModuleNameParts =
        (Name -> Text) -> List1 Name -> TopLevelModuleNameParts
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) 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]
_ []) = RawTopLevelModuleName
forall a. HasCallStack => a
__IMPOSSIBLE__
rawTopLevelModuleNameForModule (C.Mod [Pragma]
_ [Declaration]
ds) =
  case [Declaration] -> ([Declaration], [Declaration])
C.spanAllowedBeforeModule [Declaration]
ds of
    ([Declaration]
_, C.Module Range
_ Erased
_ QName
n Telescope
_ [Declaration]
_ : [Declaration]
_) -> QName -> RawTopLevelModuleName
rawTopLevelModuleNameForQName QName
n
    ([Declaration], [Declaration])
_                           -> RawTopLevelModuleName
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

type TopLevelModuleName = TopLevelModuleName' Range

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

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

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

lensTopLevelModuleNameParts ::
  Lens' TopLevelModuleName TopLevelModuleNameParts
lensTopLevelModuleNameParts :: Lens' TopLevelModuleName TopLevelModuleNameParts
lensTopLevelModuleNameParts TopLevelModuleNameParts -> f TopLevelModuleNameParts
f TopLevelModuleName
m =
  TopLevelModuleNameParts -> f TopLevelModuleNameParts
f (TopLevelModuleName -> TopLevelModuleNameParts
forall range. TopLevelModuleName' range -> TopLevelModuleNameParts
moduleNameParts TopLevelModuleName
m) f TopLevelModuleNameParts
-> (TopLevelModuleNameParts -> TopLevelModuleName)
-> f TopLevelModuleName
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ TopLevelModuleNameParts
xs -> TopLevelModuleName
m{ moduleNameParts = 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
forall range. TopLevelModuleName' range -> range
moduleNameRange TopLevelModuleName
m
  , rawModuleNameParts :: TopLevelModuleNameParts
rawModuleNameParts = TopLevelModuleName -> TopLevelModuleNameParts
forall range. TopLevelModuleName' range -> 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 =
  (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) -> TopLevelModuleNameParts -> 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
forall a. HasRange a => a -> Range
getRange TopLevelModuleName
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) (TopLevelModuleNameParts -> NonEmpty Name)
-> TopLevelModuleNameParts -> NonEmpty Name
forall a b. (a -> b) -> a -> b
$
  TopLevelModuleName -> TopLevelModuleNameParts
forall range. TopLevelModuleName' range -> 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 :: forall range. TopLevelModuleName' range -> TopLevelModuleNameParts
moduleNameParts = TopLevelModuleNameParts
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
$ TopLevelModuleNameParts -> [Text]
forall a. NonEmpty a -> [a]
List1.init TopLevelModuleNameParts
ms) [Char] -> ShowS
</>
  Text -> [Char]
T.unpack (TopLevelModuleNameParts -> Text
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 :: forall range. TopLevelModuleName' range -> TopLevelModuleNameParts
moduleNameParts = TopLevelModuleNameParts
m } =
  [Char] -> AbsolutePath
mkAbsolute ([Char] -> AbsolutePath) -> [Char] -> AbsolutePath
forall a b. (a -> b) -> a -> b
$
    ShowS -> [Char] -> [[Char]]
forall a. (a -> a) -> a -> [a]
iterate ShowS
takeDirectory (AbsolutePath -> [Char]
filePath AbsolutePath
file) [[Char]] -> Int -> [Char]
forall a. HasCallStack => [a] -> Int -> a
!! TopLevelModuleNameParts -> Int
forall a. NonEmpty a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length TopLevelModuleNameParts
m