    -- | 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           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         (Source)
    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
      let mode = if CommandLineOptions -> Bool
    optOnlyScopeChecking CommandLineOptions
    opts
                 then Mode
    Imp.ScopeCheck
                 else Mode
    Imp.TypeCheck

      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 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 ()