-- | Type-check all files of a library (option @--build-library@).

module Agda.Interaction.BuildLibrary (buildLibrary) where

import           Control.Monad.Except             (throwError)
import           Control.Monad.IO.Class           (liftIO)

import           Data.Functor                     (void)
import qualified Data.Set as Set

import           System.Directory                 (getCurrentDirectory)
import           System.FilePath                  ( (</>) )
import qualified System.FilePath.Find             as Find

import           Agda.Interaction.FindFile        (hasAgdaExtension, checkModuleName)
import qualified Agda.Interaction.Imports         as Imp
import           Agda.Interaction.Library         (pattern AgdaLibFile, _libIncludes, _libPragmas, getAgdaLibFile)
import           Agda.Interaction.Options         (optOnlyScopeChecking)

import           Agda.Syntax.Abstract.Name        (noModuleName)

import           Agda.TypeChecking.Monad
import           Agda.TypeChecking.Pretty         (prettyTCM, text, vsep)
import           Agda.TypeChecking.Pretty.Warning (getAllWarnings, tcWarningsToError)
import           Agda.TypeChecking.Warnings       (pattern AllWarnings, classifyWarnings)

import           Agda.Utils.FileName              (absolute)
import           Agda.Utils.Functor               ()
import           Agda.Utils.IO.Directory          (findWithInfo)
import           Agda.Utils.Monad                 (forM, forM_, unless, bracket_)
import           Agda.Utils.Null                  (unlessNullM)
import           Agda.Utils.String                (delimiter)

import           Agda.Utils.Impossible            (__IMPOSSIBLE__)

-- | Find @.agda-lib@ file from current directory
--   and build all modules located in the @include@ paths
--   and their subdirectories of the library.
--
buildLibrary :: TCM ()
buildLibrary :: TCM ()
buildLibrary = do
  cwd <- IO FilePath -> TCMT IO FilePath
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO FilePath
getCurrentDirectory

  -- Read the library file.
  ls <- libToTCM $ getAgdaLibFile cwd
  libFile@AgdaLibFile{ _libIncludes = paths
                     , _libPragmas  = libOpts } <- case ls of
    [AgdaLibFile
l] -> AgdaLibFile -> TCMT IO AgdaLibFile
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure AgdaLibFile
l
    []  -> TCErr -> TCMT IO AgdaLibFile
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCErr -> TCMT IO AgdaLibFile) -> TCErr -> TCMT IO AgdaLibFile
forall a b. (a -> b) -> a -> b
$ FilePath -> TCErr
GenericException FilePath
"No library found to build"
    [AgdaLibFile]
_   -> TCMT IO AgdaLibFile
forall a. HasCallStack => a
__IMPOSSIBLE__

  checkAndSetOptionsFromPragma libOpts

  -- Import the primitive modules
  Imp.importPrimitiveModules

  -- Find all modules in the include paths of the library.
  files <- map Find.infoPath . concat <$> forM paths \ FilePath
path -> do
    IO [FileInfo] -> TCMT IO [FileInfo]
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [FileInfo] -> TCMT IO [FileInfo])
-> IO [FileInfo] -> TCMT IO [FileInfo]
forall a b. (a -> b) -> a -> b
$ RecursionPredicate
-> RecursionPredicate -> FilePath -> IO [FileInfo]
findWithInfo (Bool -> RecursionPredicate
forall a. a -> FindClause a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True) (FilePath -> Bool
hasAgdaExtension (FilePath -> Bool) -> FindClause FilePath -> RecursionPredicate
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FindClause FilePath
Find.filePath) FilePath
path

  -- Call the type-checker on all these modules.
  -- (Code copied from Agda.Main.)

  opts <- commandLineOptions
  let mode = if CommandLineOptions -> Bool
optOnlyScopeChecking CommandLineOptions
opts
             then Mode
Imp.ScopeCheck
             else Mode
Imp.TypeCheck

  forM_ files \ FilePath
inputFile -> do
    sf <- AbsolutePath -> TCMT IO SourceFile
forall (m :: * -> *). MonadFileId m => AbsolutePath -> m SourceFile
srcFromPath (AbsolutePath -> TCMT IO SourceFile)
-> TCMT IO AbsolutePath -> TCMT IO SourceFile
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO AbsolutePath -> TCMT IO AbsolutePath
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (FilePath -> IO AbsolutePath
absolute FilePath
inputFile)
    src <- Imp.parseSource sf
    let m = Source -> TopLevelModuleName
Imp.srcModuleName Source
src
    checkModuleName m (Imp.srcOrigin src) Nothing
    void $ withCurrentModule noModuleName
         $ withTopLevelModule m
         $ checkModule m src
    return ()

  -- Print accumulated warnings
  unlessNullM (tcWarnings . classifyWarnings . Set.toAscList <$> getAllWarnings AllWarnings) $ \ Set TCWarning
ws -> do
    let banner :: TCMT IO Doc
banner = FilePath -> TCMT IO Doc
forall (m :: * -> *). Applicative m => FilePath -> m Doc
text (FilePath -> TCMT IO Doc) -> FilePath -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ FilePath
"\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
delimiter FilePath
"All done; warnings encountered"
    FilePath -> VerboseLevel -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
FilePath -> VerboseLevel -> TCMT IO Doc -> m ()
alwaysReportSDoc FilePath
"warning" VerboseLevel
1 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
      [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (TCMT IO Doc
banner TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
:) ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (TCWarning -> TCMT IO Doc) -> [TCWarning] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map TCWarning -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
prettyTCM ([TCWarning] -> [TCMT IO Doc]) -> [TCWarning] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ Set TCWarning -> [TCWarning]
forall a. Set a -> [a]
Set.toAscList Set TCWarning
ws

checkModule :: TopLevelModuleName -> Imp.Source -> TCM ()
checkModule :: TopLevelModuleName -> Source -> TCM ()
checkModule TopLevelModuleName
m Source
src = do
  mi <- TopLevelModuleName -> Maybe Source -> TCM ModuleInfo
Imp.getNonMainModuleInfo TopLevelModuleName
m (Source -> Maybe Source
forall a. a -> Maybe a
Just Source
src)
  -- Here we ignore InfectiveImport warnings since we don't have an actual parent module that can
  -- be infected.
  let isInfectiveWarning InfectiveImport{} = Bool
True
      isInfectiveWarning Warning
_                 = Bool
False
      warns = (TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (TCWarning -> Bool) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Warning -> Bool
isInfectiveWarning (Warning -> Bool) -> (TCWarning -> Warning) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning) ([TCWarning] -> [TCWarning]) -> [TCWarning] -> [TCWarning]
forall a b. (a -> b) -> a -> b
$ Set TCWarning -> [TCWarning]
forall a. Set a -> [a]
Set.toAscList (Set TCWarning -> [TCWarning]) -> Set TCWarning -> [TCWarning]
forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Set TCWarning
miWarnings ModuleInfo
mi
  tcWarningsToError warns
  return ()