------------------------------------------------------------------------
-- | Functions which map between module names and file names.
--
-- Note that file name lookups are cached in the 'TCState'. The code
-- assumes that no Agda source files are added or removed from the
-- include directories while the code is being type checked.
------------------------------------------------------------------------

module Agda.Interaction.FindFile
  ( SourceFile(..), InterfaceFile(intFilePath)
  , toIFile, mkInterfaceFile
  , FindError(..), findErrorToTypeError
  , findFile, findFile', findFile''
  , findInterfaceFile', findInterfaceFile
  , checkModuleName
  , moduleName
  , rootNameModule
  , replaceModuleExtension
  ) where

import Prelude hiding (null)

import Control.Monad
import Control.Monad.Except
import Control.Monad.Trans
import Data.Maybe (catMaybes)
import qualified Data.Map as Map
import qualified Data.Text as T
import System.FilePath

import Agda.Interaction.Library ( findProjectRoot )

import Agda.Syntax.Concrete
import Agda.Syntax.Parser
import Agda.Syntax.Parser.Literate (literateExtsShortList)
import Agda.Syntax.Position
import Agda.Syntax.TopLevelModuleName

import Agda.Interaction.Options ( optLocalInterfaces )

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Benchmark (billTo)
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import {-# SOURCE #-} Agda.TypeChecking.Monad.Options
  (getIncludeDirs, libToTCM)
import Agda.TypeChecking.Monad.State (topLevelModuleName)
import Agda.TypeChecking.Warnings (runPM)

import Agda.Version ( version )

import Agda.Utils.Applicative ( (?$>) )
import Agda.Utils.FileName
import Agda.Utils.List  ( stripSuffix, nubOn )
import Agda.Utils.List1 ( List1, pattern (:|) )
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Monad ( ifM, unlessM )
import Agda.Utils.Pretty ( Pretty(..), prettyShow )
import Agda.Utils.Singleton

import Agda.Utils.Impossible

-- | Type aliases for source files and interface files.
--   We may only produce one of these if we know for sure that the file
--   does exist. We can always output an @AbsolutePath@ if we are not sure.

-- TODO: do not export @SourceFile@ and force users to check the
-- @AbsolutePath@ does exist.
newtype SourceFile    = SourceFile    { SourceFile -> AbsolutePath
srcFilePath :: AbsolutePath } deriving (SourceFile -> SourceFile -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SourceFile -> SourceFile -> Bool
$c/= :: SourceFile -> SourceFile -> Bool
== :: SourceFile -> SourceFile -> Bool
$c== :: SourceFile -> SourceFile -> Bool
Eq, Eq SourceFile
SourceFile -> SourceFile -> Bool
SourceFile -> SourceFile -> Ordering
SourceFile -> SourceFile -> SourceFile
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SourceFile -> SourceFile -> SourceFile
$cmin :: SourceFile -> SourceFile -> SourceFile
max :: SourceFile -> SourceFile -> SourceFile
$cmax :: SourceFile -> SourceFile -> SourceFile
>= :: SourceFile -> SourceFile -> Bool
$c>= :: SourceFile -> SourceFile -> Bool
> :: SourceFile -> SourceFile -> Bool
$c> :: SourceFile -> SourceFile -> Bool
<= :: SourceFile -> SourceFile -> Bool
$c<= :: SourceFile -> SourceFile -> Bool
< :: SourceFile -> SourceFile -> Bool
$c< :: SourceFile -> SourceFile -> Bool
compare :: SourceFile -> SourceFile -> Ordering
$ccompare :: SourceFile -> SourceFile -> Ordering
Ord)
newtype InterfaceFile = InterfaceFile { InterfaceFile -> AbsolutePath
intFilePath :: AbsolutePath }

instance Pretty SourceFile    where pretty :: SourceFile -> Doc
pretty = forall a. Pretty a => a -> Doc
pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceFile -> AbsolutePath
srcFilePath
instance Pretty InterfaceFile where pretty :: InterfaceFile -> Doc
pretty = forall a. Pretty a => a -> Doc
pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. InterfaceFile -> AbsolutePath
intFilePath

-- | Makes an interface file from an AbsolutePath candidate.
--   If the file does not exist, then fail by returning @Nothing@.

mkInterfaceFile
  :: AbsolutePath             -- ^ Path to the candidate interface file
  -> IO (Maybe InterfaceFile) -- ^ Interface file iff it exists
mkInterfaceFile :: AbsolutePath -> IO (Maybe InterfaceFile)
mkInterfaceFile AbsolutePath
fp = do
  Bool
ex <- String -> IO Bool
doesFileExistCaseSensitive forall a b. (a -> b) -> a -> b
$ AbsolutePath -> String
filePath AbsolutePath
fp
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
ex forall (f :: * -> *) a. Alternative f => Bool -> a -> f a
?$> AbsolutePath -> InterfaceFile
InterfaceFile AbsolutePath
fp)

-- | Converts an Agda file name to the corresponding interface file
--   name. Note that we do not guarantee that the file exists.

toIFile :: SourceFile -> TCM AbsolutePath
toIFile :: SourceFile -> TCM AbsolutePath
toIFile (SourceFile AbsolutePath
src) = do
  let fp :: String
fp = AbsolutePath -> String
filePath AbsolutePath
src
  Maybe String
mroot <- forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (CommandLineOptions -> Bool
optLocalInterfaces forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions)
               {- then -} (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing)
               {- else -} (forall a. LibM a -> TCM a
libToTCM forall a b. (a -> b) -> a -> b
$ String -> LibM (Maybe String)
findProjectRoot (String -> String
takeDirectory String
fp))
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ String -> AbsolutePath -> AbsolutePath
replaceModuleExtension String
".agdai" forall a b. (a -> b) -> a -> b
$ case Maybe String
mroot of
    Maybe String
Nothing   -> AbsolutePath
src
    Just String
root ->
      let buildDir :: String
buildDir = String
root String -> String -> String
</> String
"_build" String -> String -> String
</> String
version String -> String -> String
</> String
"agda"
          fileName :: String
fileName = String -> String -> String
makeRelative String
root String
fp
      in String -> AbsolutePath
mkAbsolute forall a b. (a -> b) -> a -> b
$ String
buildDir String -> String -> String
</> String
fileName

replaceModuleExtension :: String -> AbsolutePath -> AbsolutePath
replaceModuleExtension :: String -> AbsolutePath -> AbsolutePath
replaceModuleExtension ext :: String
ext@(Char
'.':String
_) = String -> AbsolutePath
mkAbsolute forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. [a] -> [a] -> [a]
++ String
ext) forall b c a. (b -> c) -> (a -> b) -> a -> c
.  String -> String
dropAgdaExtension forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> String
filePath
replaceModuleExtension String
ext = String -> AbsolutePath -> AbsolutePath
replaceModuleExtension (Char
'.'forall a. a -> [a] -> [a]
:String
ext)

-- | Errors which can arise when trying to find a source file.
--
-- Invariant: All paths are absolute.

data FindError
  = NotFound [SourceFile]
    -- ^ The file was not found. It should have had one of the given
    -- file names.
  | Ambiguous [SourceFile]
    -- ^ Several matching files were found.
    --
    -- Invariant: The list of matching files has at least two
    -- elements.

-- | Given the module name which the error applies to this function
-- converts a 'FindError' to a 'TypeError'.

findErrorToTypeError :: TopLevelModuleName -> FindError -> TypeError
findErrorToTypeError :: TopLevelModuleName -> FindError -> TypeError
findErrorToTypeError TopLevelModuleName
m (NotFound  [SourceFile]
files) = TopLevelModuleName -> [AbsolutePath] -> TypeError
FileNotFound TopLevelModuleName
m (forall a b. (a -> b) -> [a] -> [b]
map SourceFile -> AbsolutePath
srcFilePath [SourceFile]
files)
findErrorToTypeError TopLevelModuleName
m (Ambiguous [SourceFile]
files) =
  TopLevelModuleName -> [AbsolutePath] -> TypeError
AmbiguousTopLevelModuleName TopLevelModuleName
m (forall a b. (a -> b) -> [a] -> [b]
map SourceFile -> AbsolutePath
srcFilePath [SourceFile]
files)

-- | Finds the source file corresponding to a given top-level module
-- name. The returned paths are absolute.
--
-- Raises an error if the file cannot be found.

findFile :: TopLevelModuleName -> TCM SourceFile
findFile :: TopLevelModuleName -> TCM SourceFile
findFile TopLevelModuleName
m = do
  Either FindError SourceFile
mf <- TopLevelModuleName -> TCM (Either FindError SourceFile)
findFile' TopLevelModuleName
m
  case Either FindError SourceFile
mf of
    Left FindError
err -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> FindError -> TypeError
findErrorToTypeError TopLevelModuleName
m FindError
err
    Right SourceFile
f  -> forall (m :: * -> *) a. Monad m => a -> m a
return SourceFile
f

-- | Tries to find the source file corresponding to a given top-level
--   module name. The returned paths are absolute.
--
--   SIDE EFFECT:  Updates 'stModuleToSource'.
findFile' :: TopLevelModuleName -> TCM (Either FindError SourceFile)
findFile' :: TopLevelModuleName -> TCM (Either FindError SourceFile)
findFile' TopLevelModuleName
m = do
    [AbsolutePath]
dirs         <- forall (m :: * -> *). HasOptions m => m [AbsolutePath]
getIncludeDirs
    ModuleToSource
modFile      <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' ModuleToSource TCState
stModuleToSource
    (Either FindError SourceFile
r, ModuleToSource
modFile) <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ [AbsolutePath]
-> TopLevelModuleName
-> ModuleToSource
-> IO (Either FindError SourceFile, ModuleToSource)
findFile'' [AbsolutePath]
dirs TopLevelModuleName
m ModuleToSource
modFile
    Lens' ModuleToSource TCState
stModuleToSource forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` ModuleToSource
modFile
    forall (m :: * -> *) a. Monad m => a -> m a
return Either FindError SourceFile
r

-- | A variant of 'findFile'' which does not require 'TCM'.

findFile''
  :: [AbsolutePath]
  -- ^ Include paths.
  -> TopLevelModuleName
  -> ModuleToSource
  -- ^ Cached invocations of 'findFile'''. An updated copy is returned.
  -> IO (Either FindError SourceFile, ModuleToSource)
findFile'' :: [AbsolutePath]
-> TopLevelModuleName
-> ModuleToSource
-> IO (Either FindError SourceFile, ModuleToSource)
findFile'' [AbsolutePath]
dirs TopLevelModuleName
m ModuleToSource
modFile =
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TopLevelModuleName
m ModuleToSource
modFile of
    Just AbsolutePath
f  -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (AbsolutePath -> SourceFile
SourceFile AbsolutePath
f), ModuleToSource
modFile)
    Maybe AbsolutePath
Nothing -> do
      [SourceFile]
files          <- [String] -> IO [SourceFile]
fileList [String]
acceptableFileExts
      [SourceFile]
filesShortList <- [String] -> IO [SourceFile]
fileList [String]
parseFileExtsShortList
      [SourceFile]
existingFiles  <-
        forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (String -> IO Bool
doesFileExistCaseSensitive forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> String
filePath forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceFile -> AbsolutePath
srcFilePath) [SourceFile]
files
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn forall a. a -> a
id [SourceFile]
existingFiles of
        []     -> (forall a b. a -> Either a b
Left ([SourceFile] -> FindError
NotFound [SourceFile]
filesShortList), ModuleToSource
modFile)
        [SourceFile
file] -> (forall a b. b -> Either a b
Right SourceFile
file, forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TopLevelModuleName
m (SourceFile -> AbsolutePath
srcFilePath SourceFile
file) ModuleToSource
modFile)
        [SourceFile]
files  -> (forall a b. a -> Either a b
Left ([SourceFile] -> FindError
Ambiguous [SourceFile]
existingFiles), ModuleToSource
modFile)
  where
    fileList :: [String] -> IO [SourceFile]
fileList [String]
exts = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AbsolutePath -> SourceFile
SourceFile forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO AbsolutePath
absolute)
                    [ AbsolutePath -> String
filePath AbsolutePath
dir String -> String -> String
</> String
file
                    | AbsolutePath
dir  <- [AbsolutePath]
dirs
                    , String
file <- forall a b. (a -> b) -> [a] -> [b]
map (TopLevelModuleName -> String -> String
moduleNameToFileName TopLevelModuleName
m) [String]
exts
                    ]

-- | Finds the interface file corresponding to a given top-level
-- module file. The returned paths are absolute.
--
-- Raises 'Nothing' if the the interface file cannot be found.

findInterfaceFile'
  :: SourceFile                 -- ^ Path to the source file
  -> TCM (Maybe InterfaceFile)  -- ^ Maybe path to the interface file
findInterfaceFile' :: SourceFile -> TCM (Maybe InterfaceFile)
findInterfaceFile' SourceFile
fp = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> IO (Maybe InterfaceFile)
mkInterfaceFile forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SourceFile -> TCM AbsolutePath
toIFile SourceFile
fp

-- | Finds the interface file corresponding to a given top-level
-- module file. The returned paths are absolute.
--
-- Raises an error if the source file cannot be found, and returns
-- 'Nothing' if the source file can be found but not the interface
-- file.

findInterfaceFile :: TopLevelModuleName -> TCM (Maybe InterfaceFile)
findInterfaceFile :: TopLevelModuleName -> TCM (Maybe InterfaceFile)
findInterfaceFile TopLevelModuleName
m = SourceFile -> TCM (Maybe InterfaceFile)
findInterfaceFile' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TopLevelModuleName -> TCM SourceFile
findFile TopLevelModuleName
m

-- | Ensures that the module name matches the file name. The file
-- corresponding to the module name (according to the include path)
-- has to be the same as the given file name.

checkModuleName
  :: TopLevelModuleName
     -- ^ The name of the module.
  -> SourceFile
     -- ^ The file from which it was loaded.
  -> Maybe TopLevelModuleName
     -- ^ The expected name, coming from an import statement.
  -> TCM ()
checkModuleName :: TopLevelModuleName
-> SourceFile -> Maybe TopLevelModuleName -> TCMT IO ()
checkModuleName TopLevelModuleName
name (SourceFile AbsolutePath
file) Maybe TopLevelModuleName
mexpected = do
  TopLevelModuleName -> TCM (Either FindError SourceFile)
findFile' TopLevelModuleName
name forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case

    Left (NotFound [SourceFile]
files)  -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$
      case Maybe TopLevelModuleName
mexpected of
        Maybe TopLevelModuleName
Nothing -> TopLevelModuleName -> [AbsolutePath] -> TypeError
ModuleNameDoesntMatchFileName TopLevelModuleName
name (forall a b. (a -> b) -> [a] -> [b]
map SourceFile -> AbsolutePath
srcFilePath [SourceFile]
files)
        Just TopLevelModuleName
expected -> TopLevelModuleName -> TopLevelModuleName -> TypeError
ModuleNameUnexpected TopLevelModuleName
name TopLevelModuleName
expected

    Left (Ambiguous [SourceFile]
files) -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$
      TopLevelModuleName -> [AbsolutePath] -> TypeError
AmbiguousTopLevelModuleName TopLevelModuleName
name (forall a b. (a -> b) -> [a] -> [b]
map SourceFile -> AbsolutePath
srcFilePath [SourceFile]
files)

    Right SourceFile
src -> do
      let file' :: AbsolutePath
file' = SourceFile -> AbsolutePath
srcFilePath SourceFile
src
      AbsolutePath
file <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO AbsolutePath
absolute (AbsolutePath -> String
filePath AbsolutePath
file)
      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ AbsolutePath -> AbsolutePath -> IO Bool
sameFile AbsolutePath
file AbsolutePath
file') forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> AbsolutePath -> AbsolutePath -> TypeError
ModuleDefinedInOtherFile TopLevelModuleName
name AbsolutePath
file AbsolutePath
file'

  -- Andreas, 2020-09-28, issue #4671:  In any case, make sure
  -- that we do not end up with a mismatch between expected
  -- and actual module name.

  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Maybe TopLevelModuleName
mexpected forall a b. (a -> b) -> a -> b
$ \ TopLevelModuleName
expected ->
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TopLevelModuleName
name forall a. Eq a => a -> a -> Bool
== TopLevelModuleName
expected) forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ AbsolutePath
-> TopLevelModuleName -> TopLevelModuleName -> TypeError
OverlappingProjects AbsolutePath
file TopLevelModuleName
name TopLevelModuleName
expected
      -- OverlappingProjects is the correct error for
      -- test/Fail/customized/NestedProjectRoots
      -- -- typeError $ ModuleNameUnexpected name expected


-- | Computes the module name of the top-level module in the given
-- file.
--
-- If no top-level module name is given, then an attempt is made to
-- use the file name as a module name.

-- TODO: Perhaps it makes sense to move this procedure to some other
-- module.

moduleName
  :: AbsolutePath
     -- ^ The path to the file.
  -> Module
     -- ^ The parsed module.
  -> TCM TopLevelModuleName
moduleName :: AbsolutePath -> Module -> TCM TopLevelModuleName
moduleName AbsolutePath
file Module
parsedModule = forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
billTo [Phase
Bench.ModuleName] forall a b. (a -> b) -> a -> b
$ do
  let defaultName :: String
defaultName = AbsolutePath -> String
rootNameModule AbsolutePath
file
      raw :: RawTopLevelModuleName
raw         = Module -> RawTopLevelModuleName
rawTopLevelModuleNameForModule Module
parsedModule
  RawTopLevelModuleName -> TCM TopLevelModuleName
topLevelModuleName forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< if forall a. IsNoName a => a -> Bool
isNoName RawTopLevelModuleName
raw
    then do
      QName
m <- forall a. PM a -> TCM a
runPM (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Parser a -> String -> PM (a, CohesionAttributes)
parse Parser QName
moduleNameParser String
defaultName)
             forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
_ ->
           forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
             String
"The file name " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow AbsolutePath
file forall a. [a] -> [a] -> [a]
++
             String
" is invalid because it does not correspond to a valid module name."
      case QName
m of
        Qual {} ->
          forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
            String
"The file name " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow AbsolutePath
file forall a. [a] -> [a] -> [a]
++ String
" is invalid because " forall a. [a] -> [a] -> [a]
++
            String
defaultName forall a. [a] -> [a] -> [a]
++ String
" is not an unqualified module name."
        QName {} ->
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ RawTopLevelModuleName
            { rawModuleNameRange :: Range
rawModuleNameRange = forall a. HasRange a => a -> Range
getRange QName
m
            , rawModuleNameParts :: TopLevelModuleNameParts
rawModuleNameParts = forall el coll. Singleton el coll => el -> coll
singleton (String -> Text
T.pack String
defaultName)
            }
    else forall (m :: * -> *) a. Monad m => a -> m a
return RawTopLevelModuleName
raw

parseFileExtsShortList :: [String]
parseFileExtsShortList :: [String]
parseFileExtsShortList = String
".agda" forall a. a -> [a] -> [a]
: [String]
literateExtsShortList

dropAgdaExtension :: String -> String
dropAgdaExtension :: String -> String
dropAgdaExtension String
s = case forall a. [Maybe a] -> [a]
catMaybes [ forall a. Eq a => Suffix a -> Suffix a -> Maybe (Suffix a)
stripSuffix String
ext String
s
                                     | String
ext <- [String]
acceptableFileExts ] of
    [String
name] -> String
name
    [String]
_      -> forall a. HasCallStack => a
__IMPOSSIBLE__

rootNameModule :: AbsolutePath -> String
rootNameModule :: AbsolutePath -> String
rootNameModule = String -> String
dropAgdaExtension forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> (String, String)
splitFileName forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> String
filePath