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

module Agda.Interaction.BuildLibrary (buildLibrary, printAccumulatedWarnings) where

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

import           Data.Functor                     (void)
import           Data.List                        (sort)
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           Agda.Interaction.Imports         (TCWorkers, Source, MainInterface(..))
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.Syntax.Position             (beginningOfFile)

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 <- sort . 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
  par <- Imp.wantsParallelChecking

  checks <- forM files \ FilePath
inputFile -> do
    path :: AbsolutePath
      <- 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)
    sf :: SourceFile
      <- srcFromPath path
    src :: Source
      <- Imp.parseSource sf
    let
      m :: TopLevelModuleName
      m = Source -> TopLevelModuleName
Imp.srcModuleName Source
src
    setCurrentRange (beginningOfFile path) do
      checkModuleName m (Imp.srcOrigin src) Nothing
      withCurrentModule noModuleName
           $ withTopLevelModule m
           $ checkModule par m src

  sequence_ checks
  printAccumulatedWarnings

printAccumulatedWarnings :: TCM ()
printAccumulatedWarnings :: TCM ()
printAccumulatedWarnings = do
  TCMT IO (Set TCWarning) -> (Set TCWarning -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
m a -> (a -> m ()) -> m ()
unlessNullM (WarningsAndNonFatalErrors -> Set TCWarning
tcWarnings (WarningsAndNonFatalErrors -> Set TCWarning)
-> (Set TCWarning -> WarningsAndNonFatalErrors)
-> Set TCWarning
-> Set TCWarning
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCWarning] -> WarningsAndNonFatalErrors
classifyWarnings ([TCWarning] -> WarningsAndNonFatalErrors)
-> (Set TCWarning -> [TCWarning])
-> Set TCWarning
-> WarningsAndNonFatalErrors
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set TCWarning -> [TCWarning]
forall a. Set a -> [a]
Set.toAscList (Set TCWarning -> Set TCWarning)
-> TCMT IO (Set TCWarning) -> TCMT IO (Set TCWarning)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WhichWarnings -> TCMT IO (Set TCWarning)
forall (m :: * -> *).
(MonadWarning m, MonadTCM m) =>
WhichWarnings -> m (Set TCWarning)
getAllWarnings WhichWarnings
AllWarnings) ((Set TCWarning -> TCM ()) -> TCM ())
-> (Set TCWarning -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ 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

postCheckModule :: TopLevelModuleName -> Source -> ModuleInfo -> TCM ()
postCheckModule :: TopLevelModuleName -> Source -> ModuleInfo -> TCM ()
postCheckModule TopLevelModuleName
m Source
src ModuleInfo
mi = do
  -- Here we ignore InfectiveImport warnings since we don't have an actual parent module that can
  -- be infected.
  let
    isInfectiveWarning :: Warning -> Bool
isInfectiveWarning InfectiveImport{} = Bool
True
    isInfectiveWarning Warning
_                 = Bool
False
    warns :: [TCWarning]
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
  TopLevelModuleNameWithSourceFile -> [TCWarning] -> TCM ()
tcWarningsToError (TopLevelModuleName
-> SourceFile -> TopLevelModuleNameWithSourceFile
TopLevelModuleNameWithSourceFile TopLevelModuleName
m (Source -> SourceFile
Imp.srcOrigin Source
src)) [TCWarning]
warns

checkModule :: Maybe TCWorkers -> TopLevelModuleName -> Source -> TCM (TCM ())
checkModule :: Maybe TCWorkers -> TopLevelModuleName -> Source -> TCMT IO (TCM ())
checkModule (Just TCWorkers
w) TopLevelModuleName
m Source
src = TCMT IO PragmaOptions
-> (PragmaOptions -> TCM ())
-> TCMT IO (TCM ())
-> TCMT IO (TCM ())
forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ (Lens' TCState PragmaOptions -> TCMT IO PragmaOptions
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
Lens' TCState PragmaOptions
stPragmaOptions) ((PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
Lens' TCState PragmaOptions
stPragmaOptions Lens' TCState PragmaOptions -> PragmaOptions -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens`) do
  Bool -> Source -> TCM ()
Imp.setOptionsFromSourcePragmas Bool
True Source
src
  mip <- TCWorkers
-> TopLevelModuleName
-> MainInterface
-> Maybe Source
-> TCM (TCM ModuleInfo)
Imp.chaseModule TCWorkers
w TopLevelModuleName
m MainInterface
NotMainInterface (Source -> Maybe Source
forall a. a -> Maybe a
Just Source
src)
  pure $ mip >>= postCheckModule m src

checkModule Maybe TCWorkers
Nothing 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)
  postCheckModule m src mi
  pure $ pure ()