------------------------------------------------------------------------
-- | 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.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 <- FilePath -> IO Bool
doesFileExistCaseSensitive (FilePath -> IO Bool) -> FilePath -> IO Bool
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> FilePath
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 -> FilePath
filePath AbsolutePath
src
  let localIFile = FilePath -> AbsolutePath -> AbsolutePath
replaceModuleExtension FilePath
".agdai" AbsolutePath
src
  mroot <- libToTCM $ findProjectRoot (takeDirectory fp)
  case mroot of
    Maybe FilePath
Nothing   -> AbsolutePath -> TCM AbsolutePath
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure AbsolutePath
localIFile
    Just FilePath
root -> do
      let buildDir :: FilePath
buildDir = FilePath
root FilePath -> FilePath -> FilePath
</> FilePath
"_build" FilePath -> FilePath -> FilePath
</> FilePath
version FilePath -> FilePath -> FilePath
</> FilePath
"agda"
      fileName <- IO FilePath -> TCMT IO FilePath
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO FilePath -> TCMT IO FilePath)
-> IO FilePath -> TCMT IO FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO FilePath
makeRelativeCanonical FilePath
root (AbsolutePath -> FilePath
filePath AbsolutePath
localIFile)
      let separatedIFile = FilePath -> AbsolutePath
mkAbsolute (FilePath -> AbsolutePath) -> FilePath -> AbsolutePath
forall a b. (a -> b) -> a -> b
$ FilePath
buildDir FilePath -> FilePath -> FilePath
</> FilePath
fileName
      pure separatedIFile

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

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

data FindError
  = NotFound (List1 AbsolutePath)
      -- ^ An Agda module was not found.
      --   We were looking for it in one of the given include directories.
  | Ambiguous (List2 AbsolutePath)
      -- ^ Several matching files were found.
  deriving Int -> FindError -> FilePath -> FilePath
[FindError] -> FilePath -> FilePath
FindError -> FilePath
(Int -> FindError -> FilePath -> FilePath)
-> (FindError -> FilePath)
-> ([FindError] -> FilePath -> FilePath)
-> Show FindError
forall a.
(Int -> a -> FilePath -> FilePath)
-> (a -> FilePath) -> ([a] -> FilePath -> FilePath) -> Show a
$cshowsPrec :: Int -> FindError -> FilePath -> FilePath
showsPrec :: Int -> FindError -> FilePath -> FilePath
$cshow :: FindError -> FilePath
show :: FindError -> FilePath
$cshowList :: [FindError] -> FilePath -> FilePath
showList :: [FindError] -> FilePath -> FilePath
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  List1 AbsolutePath
dirs  -> TopLevelModuleName -> List1 AbsolutePath -> TypeError
FileNotFound TopLevelModuleName
m List1 AbsolutePath
dirs
  Ambiguous List2 AbsolutePath
files -> TopLevelModuleName -> List2 AbsolutePath -> TypeError
AmbiguousTopLevelModuleName TopLevelModuleName
m List2 AbsolutePath
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     <- TCM (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
$ [FilePath] -> IO [AbsolutePath]
fileList [FilePath]
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
          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 (List1 AbsolutePath -> FindError
NotFound List1 AbsolutePath
dirs))
        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 :: [FilePath] -> IO [AbsolutePath]
fileList [FilePath]
exts = (FilePath -> IO AbsolutePath) -> [FilePath] -> 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 FilePath -> IO AbsolutePath
absolute
                    [ AbsolutePath -> FilePath
filePath AbsolutePath
dir FilePath -> FilePath -> FilePath
</> FilePath
file
                    | AbsolutePath
dir  <- List1 AbsolutePath -> [Item (List1 AbsolutePath)]
forall l. IsList l => l -> [Item l]
List1.toList List1 AbsolutePath
dirs
                    , FilePath
file <- (FilePath -> FilePath) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (TopLevelModuleName -> FilePath -> FilePath
moduleNameToFileName TopLevelModuleName
m) [FilePath]
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 List1 AbsolutePath
dirs) -> 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 -> List1 AbsolutePath -> TypeError
ModuleNameDoesntMatchFileName TopLevelModuleName
name List1 AbsolutePath
dirs
        Just TopLevelModuleName
expected -> TopLevelModuleNameWithSourceFile -> TopLevelModuleName -> TypeError
ModuleNameUnexpected (TopLevelModuleName
-> SourceFile -> TopLevelModuleNameWithSourceFile
TopLevelModuleNameWithSourceFile TopLevelModuleName
name SourceFile
src0) 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

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

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

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


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