-- | 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
  FilePath
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.
  [AgdaLibFile]
ls <- LibM [AgdaLibFile] -> TCM [AgdaLibFile]
forall a. LibM a -> TCM a
libToTCM (LibM [AgdaLibFile] -> TCM [AgdaLibFile])
-> LibM [AgdaLibFile] -> TCM [AgdaLibFile]
forall a b. (a -> b) -> a -> b
$ FilePath -> LibM [AgdaLibFile]
getAgdaLibFile FilePath
cwd
  libFile :: AgdaLibFile
libFile@AgdaLibFile{ _libIncludes :: AgdaLibFile -> [FilePath]
_libIncludes = [FilePath]
paths
                     , _libPragmas :: AgdaLibFile -> OptionsPragma
_libPragmas  = OptionsPragma
libOpts } <- case [AgdaLibFile]
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__

  OptionsPragma -> TCM ()
checkAndSetOptionsFromPragma OptionsPragma
libOpts

  -- Import the primitive modules
  TCM ()
Imp.importPrimitiveModules

  -- Find all modules in the include paths of the library.
  [FilePath]
files <- [FilePath] -> [FilePath]
forall a. Ord a => [a] -> [a]
sort ([FilePath] -> [FilePath])
-> ([[FileInfo]] -> [FilePath]) -> [[FileInfo]] -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FileInfo -> FilePath) -> [FileInfo] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map FileInfo -> FilePath
Find.infoPath ([FileInfo] -> [FilePath])
-> ([[FileInfo]] -> [FileInfo]) -> [[FileInfo]] -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[FileInfo]] -> [FileInfo]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[FileInfo]] -> [FilePath])
-> TCMT IO [[FileInfo]] -> TCMT IO [FilePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FilePath]
-> (FilePath -> TCMT IO [FileInfo]) -> TCMT IO [[FileInfo]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [FilePath]
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.)

  CommandLineOptions
opts <- TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  let mode :: Mode
mode = if CommandLineOptions -> Bool
optOnlyScopeChecking CommandLineOptions
opts
             then Mode
Imp.ScopeCheck
             else Mode
Imp.TypeCheck

  [FilePath] -> (FilePath -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [FilePath]
files \ FilePath
inputFile -> do
    AbsolutePath
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)
    SourceFile
sf :: SourceFile
      <- AbsolutePath -> TCMT IO SourceFile
forall (m :: * -> *). MonadFileId m => AbsolutePath -> m SourceFile
srcFromPath AbsolutePath
path
    Source
src :: Source
      <- SourceFile -> TCM Source
Imp.parseSource SourceFile
sf
    let
      m :: TopLevelModuleName
      m :: TopLevelModuleName
m = Source -> TopLevelModuleName
Imp.srcModuleName Source
src
    Range -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (AbsolutePath -> Range
forall a. BeginningOfFile a => a -> Range
beginningOfFile AbsolutePath
path) do
      TopLevelModuleName
-> SourceFile -> Maybe TopLevelModuleName -> TCM ()
checkModuleName TopLevelModuleName
m (Source -> SourceFile
Imp.srcOrigin Source
src) Maybe TopLevelModuleName
forall a. Maybe a
Nothing
      ()
_ <- ModuleName -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
withCurrentModule ModuleName
noModuleName
           (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> TCM () -> TCM ()
forall a. TopLevelModuleName -> TCM a -> TCM a
withTopLevelModule TopLevelModuleName
m
           (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> Source -> TCM ()
checkModule TopLevelModuleName
m Source
src
      () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  -- Print accumulated warnings
  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 :: * -> *).
(ReadTCState 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

checkModule :: TopLevelModuleName -> Imp.Source -> TCM ()
checkModule :: TopLevelModuleName -> Source -> TCM ()
checkModule TopLevelModuleName
m Source
src = do
  ModuleInfo
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 :: 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
  [TCWarning] -> TCM ()
tcWarningsToError [TCWarning]
warns
  () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()