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

module Mikan.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 Data.Set qualified as Set

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

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

import Mikan.Syntax.Abstract.Name (noModuleName)
import Mikan.Syntax.Position (beginningOfFile)

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

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

import Mikan.Utils.Impossible (__IMPOSSIBLE__)
import Mikan.Interaction.Options.Warnings

-- | 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
. Set TCWarning -> WarningsAndNonFatalErrors
classifyWarnings (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 :: DiagnosticReason -> Bool
isInfectiveWarning DiagnosticReason
d = case DiagnosticReason
d of
      DiagWarning{ _warningName :: DiagnosticReason -> WarningName
_warningName = WarningName
InfectiveImport_ } -> Bool
True
      DiagnosticReason
_ -> 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
. DiagnosticReason -> Bool
isInfectiveWarning (DiagnosticReason -> Bool)
-> (TCWarning -> DiagnosticReason) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeDiagnostic -> DiagnosticReason
forall a. Diagnostic a => a -> DiagnosticReason
diagnosticReason (SomeDiagnostic -> DiagnosticReason)
-> (TCWarning -> SomeDiagnostic) -> TCWarning -> DiagnosticReason
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> SomeDiagnostic
forall diag. TCWarning' diag -> diag
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_ (Getter TCState PragmaOptions -> TCMT IO PragmaOptions
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
Lens' TCState PragmaOptions
Getter TCState PragmaOptions
stPragmaOptions) ((PragmaOptions -> Identity PragmaOptions)
-> TCState -> Identity TCState
Lens' TCState PragmaOptions
stPragmaOptions ((PragmaOptions -> Identity PragmaOptions)
 -> TCState -> Identity TCState)
-> PragmaOptions -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' 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 ()