------------------------------------------------------------------------
-- | 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'_, findFile''
  , findInterfaceFile', findInterfaceFile
  , checkModuleName
  , rootNameModule
  , replaceModuleExtension
  , dropAgdaExtension, hasAgdaExtension, stripAgdaExtension
  ) where

import Prelude hiding (null)

import Control.Monad
import Control.Monad.Except
import Control.Monad.State
import Control.Monad.Trans
import Data.Maybe (catMaybes, fromMaybe, isJust)
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.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 ( registerFileIdWithBuiltin, topLevelModuleName )
import Agda.TypeChecking.Monad.Trace (runPM, setCurrentRange)

import Agda.Version ( version )

import Agda.Utils.Applicative ( (?$>) )
import Agda.Utils.CallStack   ( HasCallStack )
import Agda.Utils.FileId
import Agda.Utils.FileName
import Agda.Utils.List  ( stripSuffix, nubOn )
import Agda.Utils.List1 ( List1, pattern (:|) )
import Agda.Utils.List2 ( List2, pattern List2 )
import qualified Agda.Utils.List1 as List1
import qualified Agda.Utils.List2 as List2
import Agda.Utils.Monad ( ifM, unlessM )
import Agda.Syntax.Common.Pretty ( Pretty(..), prettyShow )
import qualified Agda.Syntax.Common.Pretty as P
import Agda.Utils.Singleton

import Agda.Utils.Impossible

-- This instance isn't producing something pretty.
-- instance Pretty SourceFile where
--   pretty = pretty . srcFileId

-- | File must exist.
newtype InterfaceFile = InterfaceFile { InterfaceFile -> AbsolutePath
intFilePath :: AbsolutePath }

instance Pretty InterfaceFile where
  pretty :: InterfaceFile -> Doc
pretty = AbsolutePath -> Doc
forall a. Pretty a => a -> Doc
pretty (AbsolutePath -> Doc)
-> (InterfaceFile -> AbsolutePath) -> InterfaceFile -> Doc
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
  ex <- String -> IO Bool
doesFileExistCaseSensitive (String -> IO Bool) -> String -> IO Bool
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> String
filePath AbsolutePath
fp
  pure (ex ?$> InterfaceFile fp)

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

toIFile :: HasCallStack => SourceFile -> TCM AbsolutePath
toIFile :: HasCallStack => SourceFile -> TCM AbsolutePath
toIFile (SourceFile FileId
fi) = do
  src <- FileId -> TCM AbsolutePath
forall (m :: * -> *). MonadFileId m => FileId -> m AbsolutePath
fileFromId FileId
fi -- partial function, thus HasCallStack
  let fp = AbsolutePath -> String
filePath AbsolutePath
src
  let localIFile = String -> AbsolutePath -> AbsolutePath
replaceModuleExtension String
".agdai" AbsolutePath
src
  mroot <- libToTCM $ findProjectRoot (takeDirectory fp)
  case mroot of
    Maybe String
Nothing   -> AbsolutePath -> TCM AbsolutePath
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure AbsolutePath
localIFile
    Just String
root -> do
      let buildDir :: String
buildDir = String
root String -> String -> String
</> String
"_build" String -> String -> String
</> String
version String -> String -> String
</> String
"agda"
      fileName <- IO String -> TCMT IO String
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO String -> TCMT IO String) -> IO String -> TCMT IO String
forall a b. (a -> b) -> a -> b
$ String -> String -> IO String
makeRelativeCanonical String
root (AbsolutePath -> String
filePath AbsolutePath
localIFile)
      let separatedIFile = String -> AbsolutePath
mkAbsolute (String -> AbsolutePath) -> String -> AbsolutePath
forall a b. (a -> b) -> a -> b
$ String
buildDir String -> String -> String
</> String
fileName
      pure separatedIFile

replaceModuleExtension :: String -> AbsolutePath -> AbsolutePath
replaceModuleExtension :: String -> AbsolutePath -> AbsolutePath
replaceModuleExtension ext :: String
ext@(Char
'.':String
_) = String -> AbsolutePath
mkAbsolute (String -> AbsolutePath)
-> (AbsolutePath -> String) -> AbsolutePath -> AbsolutePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ext) (String -> String)
-> (AbsolutePath -> String) -> AbsolutePath -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  String -> String
dropAgdaExtension (String -> String)
-> (AbsolutePath -> String) -> AbsolutePath -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> String
filePath
replaceModuleExtension String
ext = String -> AbsolutePath -> AbsolutePath
replaceModuleExtension (Char
'.'Char -> String -> String
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 [AbsolutePath]
      -- ^ The file was not found.
      --   It should have had one of the given file names.
  | Ambiguous (List2 AbsolutePath)
      -- ^ Several matching files were found.
  deriving Int -> FindError -> String -> String
[FindError] -> String -> String
FindError -> String
(Int -> FindError -> String -> String)
-> (FindError -> String)
-> ([FindError] -> String -> String)
-> Show FindError
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> FindError -> String -> String
showsPrec :: Int -> FindError -> String -> String
$cshow :: FindError -> String
show :: FindError -> String
$cshowList :: [FindError] -> String -> String
showList :: [FindError] -> String -> String
Show

-- | 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 = \case
  NotFound  [AbsolutePath]
files -> TopLevelModuleName -> [AbsolutePath] -> TypeError
FileNotFound TopLevelModuleName
m [AbsolutePath]
files
  Ambiguous List2 AbsolutePath
files -> TopLevelModuleName -> List2 AbsolutePath -> TypeError
AmbiguousTopLevelModuleName TopLevelModuleName
m List2 AbsolutePath
files

-- findErrorToTypeError :: MonadFileId m => TopLevelModuleName -> FindError -> m TypeError
-- findErrorToTypeError m = \case
--   NotFound  files -> FileNotFound m <$> mapM srcFilePath files
--   Ambiguous files -> AmbiguousTopLevelModuleName m <$> mapM srcFilePath 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
  mf <- TopLevelModuleName -> TCM (Either FindError SourceFile)
findFile' TopLevelModuleName
m
  case mf of
    Left FindError
err -> TypeError -> TCM SourceFile
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM SourceFile) -> TypeError -> TCM SourceFile
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> FindError -> TypeError
findErrorToTypeError TopLevelModuleName
m FindError
err
    Right SourceFile
f  -> SourceFile -> TCM SourceFile
forall a. a -> TCMT IO a
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
    dirs     <- TCMT IO (List1 AbsolutePath)
forall (m :: * -> *). HasOptions m => m (List1 AbsolutePath)
getIncludeDirs
    modToSrc <- useTC stModuleToSource
    (r, modToSrc) <- liftIO $ runStateT (findFile'' dirs m) modToSrc
    stModuleToSource `setTCLens` modToSrc
    return r

-- | A variant of 'findFile'' which manipulates an extra 'ModuleToSourceId'

findFile'_ ::
     List1 AbsolutePath
       -- ^ Include paths.
  -> TopLevelModuleName
  -> StateT ModuleToSourceId TCM (Either FindError SourceFile)
findFile'_ :: List1 AbsolutePath
-> TopLevelModuleName
-> StateT ModuleToSourceId TCM (Either FindError SourceFile)
findFile'_ List1 AbsolutePath
incs TopLevelModuleName
m = do
  dict <- Lens' TCState FileDictWithBuiltins
-> StateT ModuleToSourceId TCM FileDictWithBuiltins
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (FileDictWithBuiltins -> f FileDictWithBuiltins)
-> TCState -> f TCState
Lens' TCState FileDictWithBuiltins
stFileDict
  m2s  <- get
  (r, ModuleToSource dict' m2s') <- liftIO $
    runStateT (findFile'' incs m) $ ModuleToSource dict m2s
  setTCLens stFileDict dict'
  put m2s'
  return r

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

findFile'' ::
     List1 AbsolutePath
       -- ^ Include paths.
  -> TopLevelModuleName
  -> StateT ModuleToSource IO (Either FindError SourceFile)
findFile'' :: List1 AbsolutePath
-> TopLevelModuleName
-> StateT ModuleToSource IO (Either FindError SourceFile)
findFile'' List1 AbsolutePath
dirs TopLevelModuleName
m = do
  ModuleToSource dict modToSrc <- StateT ModuleToSource IO ModuleToSource
forall s (m :: * -> *). MonadState s m => m s
get
  case Map.lookup m modToSrc of
    Just SourceFile
sf -> Either FindError SourceFile
-> StateT ModuleToSource IO (Either FindError SourceFile)
forall a. a -> StateT ModuleToSource IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either FindError SourceFile
 -> StateT ModuleToSource IO (Either FindError SourceFile))
-> Either FindError SourceFile
-> StateT ModuleToSource IO (Either FindError SourceFile)
forall a b. (a -> b) -> a -> b
$ SourceFile -> Either FindError SourceFile
forall a b. b -> Either a b
Right SourceFile
sf
    Maybe SourceFile
Nothing -> do
      files          <- IO [AbsolutePath] -> StateT ModuleToSource IO [AbsolutePath]
forall a. IO a -> StateT ModuleToSource IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [AbsolutePath] -> StateT ModuleToSource IO [AbsolutePath])
-> IO [AbsolutePath] -> StateT ModuleToSource IO [AbsolutePath]
forall a b. (a -> b) -> a -> b
$ [String] -> IO [AbsolutePath]
fileList [String]
agdaFileExtensions
      existingFiles  <- liftIO $ filterM (doesFileExistCaseSensitive . filePath) files
      case nubOn id existingFiles of
        [AbsolutePath
file]   -> do
          let (FileId
i, FileDictWithBuiltins
dict') = AbsolutePath
-> FileDictWithBuiltins -> (FileId, FileDictWithBuiltins)
registerFileIdWithBuiltin AbsolutePath
file FileDictWithBuiltins
dict
          let src :: SourceFile
src = FileId -> SourceFile
SourceFile FileId
i
          ModuleToSource -> StateT ModuleToSource IO ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (ModuleToSource -> StateT ModuleToSource IO ())
-> ModuleToSource -> StateT ModuleToSource IO ()
forall a b. (a -> b) -> a -> b
$ FileDictWithBuiltins -> ModuleToSourceId -> ModuleToSource
ModuleToSource FileDictWithBuiltins
dict' (ModuleToSourceId -> ModuleToSource)
-> ModuleToSourceId -> ModuleToSource
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName
-> SourceFile -> ModuleToSourceId -> ModuleToSourceId
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TopLevelModuleName
m SourceFile
src ModuleToSourceId
modToSrc
          Either FindError SourceFile
-> StateT ModuleToSource IO (Either FindError SourceFile)
forall a. a -> StateT ModuleToSource IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SourceFile -> Either FindError SourceFile
forall a b. b -> Either a b
Right SourceFile
src)
        []       -> do
          filesShortList <- IO [AbsolutePath] -> StateT ModuleToSource IO [AbsolutePath]
forall a. IO a -> StateT ModuleToSource IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [AbsolutePath] -> StateT ModuleToSource IO [AbsolutePath])
-> IO [AbsolutePath] -> StateT ModuleToSource IO [AbsolutePath]
forall a b. (a -> b) -> a -> b
$ [String] -> IO [AbsolutePath]
fileList ([String] -> IO [AbsolutePath]) -> [String] -> IO [AbsolutePath]
forall a b. (a -> b) -> a -> b
$ List2 String -> [Item (List2 String)]
forall l. IsList l => l -> [Item l]
List2.toList List2 String
parseFileExtsShortList
          return (Left (NotFound filesShortList))
        AbsolutePath
f0:AbsolutePath
f1:[AbsolutePath]
fs -> Either FindError SourceFile
-> StateT ModuleToSource IO (Either FindError SourceFile)
forall a. a -> StateT ModuleToSource IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (FindError -> Either FindError SourceFile
forall a b. a -> Either a b
Left (List2 AbsolutePath -> FindError
Ambiguous (List2 AbsolutePath -> FindError)
-> List2 AbsolutePath -> FindError
forall a b. (a -> b) -> a -> b
$ AbsolutePath
-> AbsolutePath -> [AbsolutePath] -> List2 AbsolutePath
forall a. a -> a -> [a] -> List2 a
List2 AbsolutePath
f0 AbsolutePath
f1 [AbsolutePath]
fs))
  where
    fileList :: [String] -> IO [AbsolutePath]
fileList [String]
exts = (String -> IO AbsolutePath) -> [String] -> IO [AbsolutePath]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM String -> IO AbsolutePath
absolute
                    [ AbsolutePath -> String
filePath AbsolutePath
dir String -> String -> String
</> String
file
                    | AbsolutePath
dir  <- List1 AbsolutePath -> [Item (List1 AbsolutePath)]
forall l. IsList l => l -> [Item l]
List1.toList List1 AbsolutePath
dirs
                    , String
file <- (String -> String) -> [String] -> [String]
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 interface file cannot be found.

findInterfaceFile' :: HasCallStack  -- We are calling partial function toIFile, thus want a call stack.
  => SourceFile                 -- ^ Path to the source file
  -> TCM (Maybe InterfaceFile)  -- ^ Maybe path to the interface file
findInterfaceFile' :: HasCallStack => SourceFile -> TCM (Maybe InterfaceFile)
findInterfaceFile' SourceFile
fp = IO (Maybe InterfaceFile) -> TCM (Maybe InterfaceFile)
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe InterfaceFile) -> TCM (Maybe InterfaceFile))
-> (AbsolutePath -> IO (Maybe InterfaceFile))
-> AbsolutePath
-> TCM (Maybe InterfaceFile)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> IO (Maybe InterfaceFile)
mkInterfaceFile (AbsolutePath -> TCM (Maybe InterfaceFile))
-> TCM AbsolutePath -> TCM (Maybe InterfaceFile)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< HasCallStack => SourceFile -> TCM AbsolutePath
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 :: HasCallStack  -- because of calling a partial function
  => TopLevelModuleName -> TCM (Maybe InterfaceFile)
findInterfaceFile :: HasCallStack => TopLevelModuleName -> TCM (Maybe InterfaceFile)
findInterfaceFile TopLevelModuleName
m = HasCallStack => SourceFile -> TCM (Maybe InterfaceFile)
SourceFile -> TCM (Maybe InterfaceFile)
findInterfaceFile' (SourceFile -> TCM (Maybe InterfaceFile))
-> TCM SourceFile -> TCM (Maybe InterfaceFile)
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
src0 Maybe TopLevelModuleName
mexpected = do
  file <- SourceFile -> TCM AbsolutePath
forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
srcFilePath SourceFile
src0
  findFile' name >>= \case

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

    Left (Ambiguous List2 AbsolutePath
files) -> TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
      TopLevelModuleName -> List2 AbsolutePath -> TypeError
AmbiguousTopLevelModuleName TopLevelModuleName
name List2 AbsolutePath
files

    Right SourceFile
src -> do
      file' <- SourceFile -> TCM AbsolutePath
forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
srcFilePath SourceFile
src
      file  <- liftIO $ absolute $ filePath file
      unlessM (liftIO $ sameFile file file') $
        typeError $ ModuleDefinedInOtherFile name file 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.

  forM_ mexpected \ TopLevelModuleName
expected ->
    Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TopLevelModuleName
name TopLevelModuleName -> TopLevelModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== TopLevelModuleName
expected) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
      TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
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


parseFileExtsShortList :: List2 String
parseFileExtsShortList :: List2 String
parseFileExtsShortList = String -> List1 String -> List2 String
forall a. a -> List1 a -> List2 a
List2.cons String
".agda" List1 String
literateExtsShortList

-- | Remove an Agda file extension from a filepath, if possible.
stripAgdaExtension :: FilePath -> Maybe FilePath
stripAgdaExtension :: String -> Maybe String
stripAgdaExtension = [String] -> String -> Maybe String
stripAnyOfExtensions [String]
agdaFileExtensions

-- | Check if a file path has an Agda extension.
hasAgdaExtension :: FilePath -> Bool
hasAgdaExtension :: String -> Bool
hasAgdaExtension = Maybe String -> Bool
forall a. Maybe a -> Bool
isJust (Maybe String -> Bool)
-> (String -> Maybe String) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe String
stripAgdaExtension

-- | Remove an existing Agda file extension from a file path.
dropAgdaExtension :: FilePath -> FilePath
dropAgdaExtension :: String -> String
dropAgdaExtension = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe String -> String)
-> (String -> Maybe String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe String
stripAgdaExtension


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