{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}

{-| This module deals with finding imported modules and loading their
    interface files.
-}
module Mikan.Interaction.Imports
  ( Mode, pattern ScopeCheck, pattern TypeCheck

  , CheckResult (CheckResult)
  , crModuleInfo
  , crInterface
  , crWarnings
  , crMode
  , crSource

  , Source(..)
  , scopeCheckFileImport
  , parseSource
  , typeCheckMain
  , getNonMainInterface
  , getNonMainModuleInfo
  , getInterface
  , importPrimitiveModules
  , raiseNonFatalErrors

  , MainInterface(..)
  , TCWorkers
  , wantsParallelChecking
  , chaseModule
  , setOptionsFromSourcePragmas

  -- Currently only used by test/api/Issue1168.hs:
  , readInterface
  ) where

import Prelude hiding (null)

import Control.Exception qualified as E
import Control.Monad.Except        ( MonadError(..), ExceptT, runExceptT, withExceptT )
import Control.Monad.IO.Class      ( MonadIO(..) )
import Control.Monad.State         ( MonadState(..), execStateT )
import Control.Monad.Trans.Maybe
import Control.Concurrent
import Control.DeepSeq

import Data.Either
import Data.Monoid
import Data.List (intercalate)
import Data.List qualified as List
import Data.Maybe
import Data.Map (Map)
import Data.Map qualified as Map
import Data.HashMap.Strict qualified as HMap
import Data.ByteString qualified as B
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Text (Text)
import Data.Text qualified as T
import Data.Text.Short qualified as TS
import Data.Text.Lazy qualified as TL

import GHC.Conc

import System.Directory (doesFileExist, removeFile)
import System.FilePath  ( (</>) )
import System.IO
import System.IO.Error (isUserError, isFullError)

import Mikan.Benchmarking

import Mikan.Syntax.Concrete.Definitions qualified as C
import Mikan.Syntax.Abstract qualified as A
import Mikan.Syntax.Concrete qualified as C
import Mikan.Syntax.Concrete.Attribute
import Mikan.Syntax.Concrete.Generic
import Mikan.Syntax.Abstract.Name
import Mikan.Syntax.Common
import Mikan.Syntax.Common.Pretty hiding (Mode)
import Mikan.Syntax.Parser
import Mikan.Syntax.Position
import Mikan.Syntax.Scope.Base
import Mikan.Syntax.Scope.Trimming
import Mikan.Syntax.Scope.UnusedImports (warnUnusedImports)
import Mikan.Syntax.TopLevelModuleName
import Mikan.Syntax.Translation.ConcreteToAbstract
  ( TopLevel( TopLevel )
  , TopLevelInfo( TopLevelInfo, topLevelDecls, topLevelScope)
  , concreteToAbstract_
  )
import Mikan.Syntax.Translation.ConcreteToAbstract qualified as CToA

import Mikan.TypeChecking.InstanceArguments
import Mikan.TypeChecking.Errors.Deferred
import Mikan.TypeChecking.Errors
import Mikan.TypeChecking.Warnings hiding (warnings)
import Mikan.TypeChecking.Reduce
import Mikan.TypeChecking.MetaVars ( openMetasToPostulates )
import Mikan.TypeChecking.Monad.State as S
import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Serialise (decode, encodeFile, decodeInterface, deserializeHashes)
import Mikan.TypeChecking.Primitive
import Mikan.TypeChecking.Pretty as P
import Mikan.TypeChecking.DeadCode
import Mikan.TypeChecking.Monad.Benchmark qualified as Bench

import Mikan.TheTypeChecker

import Mikan.Interaction.BasicOps ( getGoals, prettyGoals )
import Mikan.Interaction.FindFile
import Mikan.Interaction.ReadFile
import Mikan.Interaction.Highlighting.Generate
import Mikan.Interaction.Highlighting.Precise qualified as Highlighting ( convert )
import Mikan.Interaction.Highlighting.Vim
import Mikan.Interaction.Library
import Mikan.Interaction.Options
import Mikan.Interaction.Options.Lenses qualified as Lens
import Mikan.Interaction.Options.Warnings (unsolvedWarnings, WarningName (WarningProblem_))
import Mikan.Interaction.Response
  (RemoveTokenBasedHighlighting(KeepHighlighting))

import Mikan.Utils.CallStack (HasCallStack)
import Mikan.Utils.FileName
import Mikan.Utils.Hash
import Mikan.Utils.Lens
import Mikan.Utils.List ( nubOn )
import Mikan.Utils.Maybe
import Mikan.Utils.Maybe.Strict qualified as Strict
import Mikan.Utils.Monad
import Mikan.Utils.Null
import Mikan.Interaction.Options.ProfileOptions qualified as Profile
import Mikan.Utils.Singleton
import Mikan.Utils.Set1 qualified as Set1
import Mikan.Utils.Trie qualified as Trie
import Mikan.Utils.Impossible
import Mikan.Utils.IORef.Strict
import Mikan.Utils.Tuple.Strict (Pair(..))
import Mikan.Utils.Tuple.Strict qualified as Strict
import Mikan.Utils.Trace (traceMarkerIO, incrementUserEra_)


-- | Whether to ignore interfaces (@.agdai@) other than built-in modules

ignoreInterfaces :: HasOptions m => m Bool
ignoreInterfaces :: forall (m :: * -> *). HasOptions m => m Bool
ignoreInterfaces = CommandLineOptions -> Bool
optIgnoreInterfaces (CommandLineOptions -> Bool) -> m CommandLineOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions

-- | Whether to ignore all interface files (@.agdai@)

ignoreAllInterfaces :: HasOptions m => m Bool
ignoreAllInterfaces :: forall (m :: * -> *). HasOptions m => m Bool
ignoreAllInterfaces = CommandLineOptions -> Bool
optIgnoreAllInterfaces (CommandLineOptions -> Bool) -> m CommandLineOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions

-- | Whether to write interface files (@.agdai@)

writeInterfaces :: HasOptions m => m Bool
writeInterfaces :: forall (m :: * -> *). HasOptions m => m Bool
writeInterfaces = CommandLineOptions -> Bool
optWriteInterfaces (CommandLineOptions -> Bool) -> m CommandLineOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions

-- | The decorated source code.
data Source = Source
  { Source -> Text
srcText        :: Text               -- ^ Source code.
  , Source -> FileType
srcFileType    :: FileType           -- ^ Source file type
  , Source -> SourceFile
srcOrigin      :: SourceFile         -- ^ Source location at the time of its parsing
  , Source -> Module
srcModule      :: C.Module           -- ^ The parsed module.
  , Source -> TopLevelModuleName' Range
srcModuleName  :: TopLevelModuleName -- ^ The top-level module name.
  , Source -> [AgdaLibFile]
srcProjectLibs :: [AgdaLibFile]      -- ^ The .agda-lib file(s) of the project this file belongs to.
  , Source -> Attributes
srcAttributes  :: !Attributes        -- ^ Every encountered attribute.
  }

-- | Parses a source file and prepares the 'Source' record.
parseSource :: SourceFile -> TCM Source
parseSource :: SourceFile -> TCM Source
parseSource SourceFile
sourceFile = Account (BenchPhase (TCMT IO)) -> TCM Source -> TCM Source
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Parsing] (TCM Source -> TCM Source) -> TCM Source -> TCM Source
forall a b. (a -> b) -> a -> b
$ do
  -- Issue #7303:
  -- The parser previously used mdo to avoid the duplicate parsing for the
  -- bootstrapping of the TopLevelModuleName in Range.
  -- But that made ranges blackholes during parsing,
  -- introducing regression #7301, fragility of the API as observed in #7492,
  -- and debugging headaches as ranges could not be showed during parsing.
  -- Now we bite the bullet to parse the source twice,
  -- until a better management of ranges comes about.
  --
  -- (E.g. it is unclear why ranges need the file name/id in place
  -- so early, as all the ranges from one file have the same file id.
  -- It would be sufficient to fill in the file name/id when the mixing
  -- with other files starts, e.g. during scope checking.)

  f <- SourceFile -> TCMT IO AbsolutePath
forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
srcFilePath SourceFile
sourceFile
  traceMarkerIO $ "Loading " <> textPath f
  incrementUserEra_ 1

  -- Read the source text.
  let rf0 = AbsolutePath -> Maybe (TopLevelModuleName' Range) -> RangeFile
mkRangeFile AbsolutePath
f Maybe (TopLevelModuleName' Range)
forall a. Maybe a
Nothing
  setCurrentRange (beginningOfFile rf0) do

  source <- readFileText <$> readFileTCM f

  -- Get the literate markdown option.
  mdOnlyAgdaBlocks <- optMdOnlyAgdaBlocks <$> commandLineOptions

  -- Bootstrapping: parse the module name.
  parsedModName0 <- moduleName f . fst . fst =<< do
    runPMDropWarnings $ parseFile mdOnlyAgdaBlocks moduleParser rf0 source

  -- Now parse again, with module name present to be filled into the ranges.
  let rf = AbsolutePath -> Maybe (TopLevelModuleName' Range) -> RangeFile
mkRangeFile AbsolutePath
f (Maybe (TopLevelModuleName' Range) -> RangeFile)
-> Maybe (TopLevelModuleName' Range) -> RangeFile
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName' Range -> Maybe (TopLevelModuleName' Range)
forall a. a -> Maybe a
Just TopLevelModuleName' Range
parsedModName0
  ((parsedMod, attrs), fileType) <- runPM $ parseFile mdOnlyAgdaBlocks moduleParser rf source
  parsedModName                  <- moduleName f parsedMod

  libs <- getAgdaLibFiles f parsedModName
  return Source
    { srcText        = source
    , srcFileType    = fileType
    , srcOrigin      = sourceFile
    , srcModule      = parsedMod
    , srcModuleName  = parsedModName
    , srcProjectLibs = libs
    , srcAttributes  = attrs
    }

-- | Computes the module name of the top-level module in the given file.
--
-- If no top-level module name is given, then an attempt is made to
-- use the file name as a module name.

moduleName ::
     AbsolutePath
     -- ^ The path to the file.
  -> C.Module
     -- ^ The parsed module.
  -> TCM TopLevelModuleName
moduleName :: AbsolutePath -> Module -> TCM (TopLevelModuleName' Range)
moduleName AbsolutePath
file Module
parsedModule = Account (BenchPhase (TCMT IO))
-> TCM (TopLevelModuleName' Range)
-> TCM (TopLevelModuleName' Range)
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.ModuleName] (TCM (TopLevelModuleName' Range)
 -> TCM (TopLevelModuleName' Range))
-> TCM (TopLevelModuleName' Range)
-> TCM (TopLevelModuleName' Range)
forall a b. (a -> b) -> a -> b
$ do
  let defaultName :: [Char]
defaultName = AbsolutePath -> [Char]
rootNameModule AbsolutePath
file
      raw :: RawTopLevelModuleName
raw         = Module -> RawTopLevelModuleName
rawTopLevelModuleNameForModule Module
parsedModule
  RawTopLevelModuleName -> TCM (TopLevelModuleName' Range)
topLevelModuleName (RawTopLevelModuleName -> TCM (TopLevelModuleName' Range))
-> TCMT IO RawTopLevelModuleName -> TCM (TopLevelModuleName' Range)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< if RawTopLevelModuleName -> Bool
forall a. IsNoName a => a -> Bool
isNoName RawTopLevelModuleName
raw
    then Range
-> TCMT IO RawTopLevelModuleName -> TCMT IO RawTopLevelModuleName
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (AbsolutePath -> Range
rangeFromAbsolutePath AbsolutePath
file) do
      m <- PM QName -> TCM QName
forall a. PM a -> TCM a
runPM ((QName, Attributes) -> QName
forall a b. (a, b) -> a
fst ((QName, Attributes) -> QName)
-> PM (QName, Attributes) -> PM QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser QName -> Text -> PM (QName, Attributes)
forall a. Parser a -> Text -> PM (a, Attributes)
parse Parser QName
moduleNameParser ([Char] -> Text
T.pack [Char]
defaultName))
             TCM QName -> (TCErr -> TCM QName) -> TCM QName
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
_ ->
           TypeError -> TCM QName
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCM QName) -> TypeError -> TCM QName
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> InvalidFileNameReason -> TypeError
InvalidFileName AbsolutePath
file InvalidFileNameReason
DoesNotCorrespondToValidModuleName
      case m of
        C.Qual{} ->
          TypeError -> TCMT IO RawTopLevelModuleName
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCMT IO RawTopLevelModuleName)
-> TypeError -> TCMT IO RawTopLevelModuleName
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> InvalidFileNameReason -> TypeError
InvalidFileName AbsolutePath
file (InvalidFileNameReason -> TypeError)
-> InvalidFileNameReason -> TypeError
forall a b. (a -> b) -> a -> b
$
            Text -> InvalidFileNameReason
RootNameModuleNotAQualifiedModuleName (Text -> InvalidFileNameReason) -> Text -> InvalidFileNameReason
forall a b. (a -> b) -> a -> b
$ [Char] -> Text
T.pack [Char]
defaultName
        C.QName{} ->
          RawTopLevelModuleName -> TCMT IO RawTopLevelModuleName
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (RawTopLevelModuleName -> TCMT IO RawTopLevelModuleName)
-> RawTopLevelModuleName -> TCMT IO RawTopLevelModuleName
forall a b. (a -> b) -> a -> b
$ RawTopLevelModuleName
            { rawModuleNameRange :: Range
rawModuleNameRange = QName -> Range
forall a. HasRange a => a -> Range
getRange QName
m
            , rawModuleNameParts :: TopLevelModuleNameParts
rawModuleNameParts = ShortText -> TopLevelModuleNameParts
forall el coll. Singleton el coll => el -> coll
singleton ([Char] -> ShortText
TS.pack [Char]
defaultName)
            , rawModuleNameInferred :: Bool
rawModuleNameInferred = Bool
True
                -- Andreas, 2025-06-21, issue #7953:
                -- Remember we made up this module name to improve errors.
            }
    else RawTopLevelModuleName -> TCMT IO RawTopLevelModuleName
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return RawTopLevelModuleName
raw


srcDefaultPragmas :: Source -> [OptionsPragma]
srcDefaultPragmas :: Source -> [OptionsPragma]
srcDefaultPragmas Source
src = (AgdaLibFile -> OptionsPragma) -> [AgdaLibFile] -> [OptionsPragma]
forall a b. (a -> b) -> [a] -> [b]
map AgdaLibFile -> OptionsPragma
_libPragmas (Source -> [AgdaLibFile]
srcProjectLibs Source
src)

srcFilePragmas :: Source -> [OptionsPragma]
srcFilePragmas :: Source -> [OptionsPragma]
srcFilePragmas Source
src = [OptionsPragma]
pragmas
  where
  cpragmas :: [Pragma]
cpragmas = Module -> [Pragma]
C.modPragmas (Source -> Module
srcModule Source
src)
  pragmas :: [OptionsPragma]
pragmas = [ OptionsPragma
                { pragmaStrings :: [[Char]]
pragmaStrings = ShortText -> [Char]
TS.unpack (ShortText -> [Char]) -> [ShortText] -> [[Char]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ShortText]
opts
                , pragmaRange :: Range
pragmaRange   = Range
r
                }
            | C.OptionsPragma Range
r [ShortText]
opts <- [Pragma]
cpragmas
            ]

-- | Set options from a 'Source' pragma, using the source
--   ranges of the pragmas for error reporting. Flag to check consistency.
setOptionsFromSourcePragmas :: Bool -> Source -> TCM ()
setOptionsFromSourcePragmas :: Bool -> Source -> TCMT IO ()
setOptionsFromSourcePragmas Bool
checkOpts Source
src = do
  (OptionsPragma -> TCMT IO ()) -> [OptionsPragma] -> TCMT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ OptionsPragma -> TCMT IO ()
setOpts (Source -> [OptionsPragma]
srcDefaultPragmas Source
src)
  (OptionsPragma -> TCMT IO ()) -> [OptionsPragma] -> TCMT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ OptionsPragma -> TCMT IO ()
setOpts (Source -> [OptionsPragma]
srcFilePragmas    Source
src)
  where
    setOpts :: OptionsPragma -> TCMT IO ()
setOpts | Bool
checkOpts = OptionsPragma -> TCMT IO ()
checkAndSetOptionsFromPragma
            | Bool
otherwise = OptionsPragma -> TCMT IO ()
setOptionsFromPragma

-- | Is the aim to type-check the top-level module, or only to
-- scope-check it?

data Mode
  = ScopeCheck
  | TypeCheck
  deriving (Mode -> Mode -> Bool
(Mode -> Mode -> Bool) -> (Mode -> Mode -> Bool) -> Eq Mode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Mode -> Mode -> Bool
== :: Mode -> Mode -> Bool
$c/= :: Mode -> Mode -> Bool
/= :: Mode -> Mode -> Bool
Eq, Int -> Mode -> ShowS
[Mode] -> ShowS
Mode -> [Char]
(Int -> Mode -> ShowS)
-> (Mode -> [Char]) -> ([Mode] -> ShowS) -> Show Mode
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Mode -> ShowS
showsPrec :: Int -> Mode -> ShowS
$cshow :: Mode -> [Char]
show :: Mode -> [Char]
$cshowList :: [Mode] -> ShowS
showList :: [Mode] -> ShowS
Show)

-- | Are we loading the interface for the user-loaded file
--   or for an import?
data MainInterface
  = MainInterface Mode -- ^ For the main file.
                       --
                       --   In this case state changes inflicted by
                       --   'createInterface' are preserved.
  | NotMainInterface   -- ^ For an imported file.
                       --
                       --   In this case state changes inflicted by
                       --   'createInterface' are not preserved.
  deriving (MainInterface -> MainInterface -> Bool
(MainInterface -> MainInterface -> Bool)
-> (MainInterface -> MainInterface -> Bool) -> Eq MainInterface
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MainInterface -> MainInterface -> Bool
== :: MainInterface -> MainInterface -> Bool
$c/= :: MainInterface -> MainInterface -> Bool
/= :: MainInterface -> MainInterface -> Bool
Eq, Int -> MainInterface -> ShowS
[MainInterface] -> ShowS
MainInterface -> [Char]
(Int -> MainInterface -> ShowS)
-> (MainInterface -> [Char])
-> ([MainInterface] -> ShowS)
-> Show MainInterface
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MainInterface -> ShowS
showsPrec :: Int -> MainInterface -> ShowS
$cshow :: MainInterface -> [Char]
show :: MainInterface -> [Char]
$cshowList :: [MainInterface] -> ShowS
showList :: [MainInterface] -> ShowS
Show)

-- | Should state changes inflicted by 'createInterface' be preserved?

includeStateChanges :: MainInterface -> Bool
includeStateChanges :: MainInterface -> Bool
includeStateChanges (MainInterface Mode
_) = Bool
True
includeStateChanges MainInterface
NotMainInterface  = Bool
False

-- | The kind of interface produced by 'createInterface'
moduleCheckMode :: MainInterface -> ModuleCheckMode
moduleCheckMode :: MainInterface -> ModuleCheckMode
moduleCheckMode = \case
    MainInterface Mode
TypeCheck                       -> ModuleCheckMode
ModuleTypeChecked
    MainInterface
NotMainInterface                              -> ModuleCheckMode
ModuleTypeChecked
    MainInterface Mode
ScopeCheck                      -> ModuleCheckMode
ModuleScopeChecked

-- | Merge an interface into the current proof state.
mergeInterface :: Interface -> TCM ()
mergeInterface :: Interface -> TCMT IO ()
mergeInterface Interface
i = do
    let sig :: Signature
sig     = Interface -> Signature
iSignature Interface
i
        builtin :: [(SomeBuiltin, Builtin (PrimitiveId, QName))]
builtin = Map SomeBuiltin (Builtin (PrimitiveId, QName))
-> [(SomeBuiltin, Builtin (PrimitiveId, QName))]
forall k a. Map k a -> [(k, a)]
Map.toAscList (Map SomeBuiltin (Builtin (PrimitiveId, QName))
 -> [(SomeBuiltin, Builtin (PrimitiveId, QName))])
-> Map SomeBuiltin (Builtin (PrimitiveId, QName))
-> [(SomeBuiltin, Builtin (PrimitiveId, QName))]
forall a b. (a -> b) -> a -> b
$ Interface -> Map SomeBuiltin (Builtin (PrimitiveId, QName))
iBuiltin Interface
i
        primOrBi :: (a, Builtin a) -> Either a (a, Builtin pf)
primOrBi = \case
          (a
_, Prim a
x)                     -> a -> Either a (a, Builtin pf)
forall a b. a -> Either a b
Left a
x
          (a
x, Builtin Term
t)                  -> (a, Builtin pf) -> Either a (a, Builtin pf)
forall a b. b -> Either a b
Right (a
x, Term -> Builtin pf
forall pf. Term -> Builtin pf
Builtin Term
t)
        ([(PrimitiveId, QName)]
prim, [(SomeBuiltin, Builtin PrimFun)]
bi') = [Either (PrimitiveId, QName) (SomeBuiltin, Builtin PrimFun)]
-> ([(PrimitiveId, QName)], [(SomeBuiltin, Builtin PrimFun)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either (PrimitiveId, QName) (SomeBuiltin, Builtin PrimFun)]
 -> ([(PrimitiveId, QName)], [(SomeBuiltin, Builtin PrimFun)]))
-> [Either (PrimitiveId, QName) (SomeBuiltin, Builtin PrimFun)]
-> ([(PrimitiveId, QName)], [(SomeBuiltin, Builtin PrimFun)])
forall a b. (a -> b) -> a -> b
$ ((SomeBuiltin, Builtin (PrimitiveId, QName))
 -> Either (PrimitiveId, QName) (SomeBuiltin, Builtin PrimFun))
-> [(SomeBuiltin, Builtin (PrimitiveId, QName))]
-> [Either (PrimitiveId, QName) (SomeBuiltin, Builtin PrimFun)]
forall a b. (a -> b) -> [a] -> [b]
map (SomeBuiltin, Builtin (PrimitiveId, QName))
-> Either (PrimitiveId, QName) (SomeBuiltin, Builtin PrimFun)
forall {a} {a} {pf}. (a, Builtin a) -> Either a (a, Builtin pf)
primOrBi [(SomeBuiltin, Builtin (PrimitiveId, QName))]
builtin
        bi :: BuiltinThings
bi      = [(SomeBuiltin, Builtin PrimFun)] -> BuiltinThings
forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList [(SomeBuiltin, Builtin PrimFun)]
bi'
        warns :: Set TCWarning
warns   = (TCWarning' EncodedDiagnostic -> TCWarning)
-> Set (TCWarning' EncodedDiagnostic) -> Set TCWarning
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic ((EncodedDiagnostic -> SomeDiagnostic)
-> TCWarning' EncodedDiagnostic -> TCWarning
forall a b. (a -> b) -> TCWarning' a -> TCWarning' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap EncodedDiagnostic -> SomeDiagnostic
forall a. Diagnostic a => a -> SomeDiagnostic
toSomeDiagnostic) (Set (TCWarning' EncodedDiagnostic) -> Set TCWarning)
-> Set (TCWarning' EncodedDiagnostic) -> Set TCWarning
forall a b. (a -> b) -> a -> b
$ Interface -> Set (TCWarning' EncodedDiagnostic)
iWarnings Interface
i
    bs <- (TCState -> BuiltinThings) -> TCMT IO BuiltinThings
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC TCState -> BuiltinThings
stBuiltinThings
    reportSLn "import.iface.merge" 10 $ "Merging interface " ++ prettyShow (iTopLevelModuleName i)
    reportSLn "import.iface.merge" 20 $
      "  Current builtins " ++ show (Map.keys bs) ++ "\n" ++
      "  New builtins     " ++ show (Map.keys bi)
    let check (BuiltinName BuiltinId
b) (Builtin Term
x) (Builtin Term
y)
              | Term
x Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
y    = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
              | Bool
otherwise = TypeError -> m ()
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ BuiltinId -> Term -> Term -> TypeError
DuplicateBuiltinBinding BuiltinId
b Term
x Term
y
        check SomeBuiltin
_ Builtin pf
_ Builtin pf
_ = m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
    sequence_ $ Map.intersectionWithKey check bs bi

    addImportedThings
      sig
      (iMetaBindings i)
      bi
      (iPatternSyns i)
      (iDisplayForms i)
      (iUserWarnings i)
      (iPartialDefs i)
      warns
      (iOpaqueBlocks i)
      (iOpaqueNames i)

    reportSLn "import.iface.merge" 50 $
      "  Rebinding primitives " ++ show prim

    forM_ prim \(PrimitiveId
x, QName
q) -> do
      PrimImpl _ pf <- PrimitiveId -> TCM PrimitiveImpl
lookupPrimitiveFunction PrimitiveId
x
      setTCLens (stImportedBuiltins . at (someBuiltin x)) $ Just $ Prim pf{ primFunName = q }

addImportedThings
  :: Signature
  -> RemoteMetaStore
  -> BuiltinThings
  -> A.PatternSynDefns
  -> DisplayForms
  -> UserWarnings      -- ^ Imported user warnings
  -> Set QName             -- ^ Name of imported definitions which are partial
  -> Set TCWarning
  -> Map OpaqueId OpaqueBlock
  -> Map QName OpaqueId
  -> TCM ()
addImportedThings :: Signature
-> RemoteMetaStore
-> BuiltinThings
-> PatternSynDefns
-> DisplayForms
-> UserWarnings
-> Set QName
-> Set TCWarning
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> TCMT IO ()
addImportedThings Signature
isig RemoteMetaStore
metas BuiltinThings
ibuiltin PatternSynDefns
patsyns DisplayForms
display UserWarnings
userwarn
                  Set QName
partialdefs Set TCWarning
warnings Map OpaqueId OpaqueBlock
oblock Map QName OpaqueId
oid = do
  (Signature -> Identity Signature) -> TCState -> Identity TCState
Lens' TCState Signature
stImports              ((Signature -> Identity Signature) -> TCState -> Identity TCState)
-> (Signature -> Signature) -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
`modifyingTC` \ Signature
imp -> Signature -> Signature -> Signature
importSignature Signature
imp Signature
isig
  (RemoteMetaStore -> Identity RemoteMetaStore)
-> TCState -> Identity TCState
Lens' TCState RemoteMetaStore
stImportedMetaStore    ((RemoteMetaStore -> Identity RemoteMetaStore)
 -> TCState -> Identity TCState)
-> (RemoteMetaStore -> RemoteMetaStore) -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
`modifyingTC` RemoteMetaStore -> RemoteMetaStore -> RemoteMetaStore
forall k v. Eq k => HashMap k v -> HashMap k v -> HashMap k v
HMap.union RemoteMetaStore
metas
  (BuiltinThings -> Identity BuiltinThings)
-> TCState -> Identity TCState
Lens' TCState BuiltinThings
stImportedBuiltins     ((BuiltinThings -> Identity BuiltinThings)
 -> TCState -> Identity TCState)
-> (BuiltinThings -> BuiltinThings) -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
`modifyingTC` \ BuiltinThings
imp -> BuiltinThings -> BuiltinThings -> BuiltinThings
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union BuiltinThings
imp BuiltinThings
ibuiltin
  (UserWarnings -> Identity UserWarnings)
-> TCState -> Identity TCState
Lens' TCState UserWarnings
stImportedUserWarnings ((UserWarnings -> Identity UserWarnings)
 -> TCState -> Identity TCState)
-> (UserWarnings -> UserWarnings) -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
`modifyingTC` \ UserWarnings
imp -> UserWarnings -> UserWarnings -> UserWarnings
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union UserWarnings
imp UserWarnings
userwarn
  (Set QName -> Identity (Set QName)) -> TCState -> Identity TCState
Lens' TCState (Set QName)
stImportedPartialDefs  ((Set QName -> Identity (Set QName))
 -> TCState -> Identity TCState)
-> (Set QName -> Set QName) -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
`modifyingTC` \ Set QName
imp -> Set QName -> Set QName -> Set QName
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set QName
imp Set QName
partialdefs
  (PatternSynDefns -> Identity PatternSynDefns)
-> TCState -> Identity TCState
Lens' TCState PatternSynDefns
stPatternSynImports    ((PatternSynDefns -> Identity PatternSynDefns)
 -> TCState -> Identity TCState)
-> (PatternSynDefns -> PatternSynDefns) -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
`modifyingTC` \ PatternSynDefns
imp -> PatternSynDefns -> PatternSynDefns -> PatternSynDefns
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union PatternSynDefns
imp PatternSynDefns
patsyns
  (DisplayForms -> Identity DisplayForms)
-> TCState -> Identity TCState
Lens' TCState DisplayForms
stImportedDisplayForms ((DisplayForms -> Identity DisplayForms)
 -> TCState -> Identity TCState)
-> (DisplayForms -> DisplayForms) -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
`modifyingTC` \ DisplayForms
imp -> (List1 LocalDisplayForm
 -> List1 LocalDisplayForm -> List1 LocalDisplayForm)
-> DisplayForms -> DisplayForms -> DisplayForms
forall k v.
Eq k =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HMap.unionWith List1 LocalDisplayForm
-> List1 LocalDisplayForm -> List1 LocalDisplayForm
forall a. Semigroup a => a -> a -> a
(<>) DisplayForms
imp DisplayForms
display
  (Set TCWarning -> Identity (Set TCWarning))
-> TCState -> Identity TCState
Lens' TCState (Set TCWarning)
stTCWarnings           ((Set TCWarning -> Identity (Set TCWarning))
 -> TCState -> Identity TCState)
-> (Set TCWarning -> Set TCWarning) -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
`modifyingTC` \ Set TCWarning
imp -> Set TCWarning -> Set TCWarning -> Set TCWarning
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set TCWarning
imp Set TCWarning
warnings
  (Map OpaqueId OpaqueBlock -> Identity (Map OpaqueId OpaqueBlock))
-> TCState -> Identity TCState
Lens' TCState (Map OpaqueId OpaqueBlock)
stOpaqueBlocks         ((Map OpaqueId OpaqueBlock -> Identity (Map OpaqueId OpaqueBlock))
 -> TCState -> Identity TCState)
-> (Map OpaqueId OpaqueBlock -> Map OpaqueId OpaqueBlock)
-> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
`modifyingTC` \ Map OpaqueId OpaqueBlock
imp -> Map OpaqueId OpaqueBlock
imp Map OpaqueId OpaqueBlock
-> Map OpaqueId OpaqueBlock -> Map OpaqueId OpaqueBlock
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Map OpaqueId OpaqueBlock
oblock
  (Map QName OpaqueId -> Identity (Map QName OpaqueId))
-> TCState -> Identity TCState
Lens' TCState (Map QName OpaqueId)
stOpaqueIds            ((Map QName OpaqueId -> Identity (Map QName OpaqueId))
 -> TCState -> Identity TCState)
-> (Map QName OpaqueId -> Map QName OpaqueId) -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
`modifyingTC` \ Map QName OpaqueId
imp -> Map QName OpaqueId
imp Map QName OpaqueId -> Map QName OpaqueId -> Map QName OpaqueId
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Map QName OpaqueId
oid

-- | Merges two signatures, assuming the second is being imported into the first
--
-- This is not commutative: `Map.union` is left-biased.
importSignature
  :: Signature
  -- ^ Current signature
  -> Signature
  -- ^ Signature being imported
  -> Signature
  -- ^ Merged signature
importSignature :: Signature -> Signature -> Signature
importSignature (Sig Sections
a HashMap QName Definition
b InstanceTable
c) (Sig Sections
a' HashMap QName Definition
b' InstanceTable
c') =
  Sections -> HashMap QName Definition -> InstanceTable -> Signature
Sig (Sections -> Sections -> Sections
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Sections
a Sections
a')
      (HashMap QName Definition
-> HashMap QName Definition -> HashMap QName Definition
forall k v. Eq k => HashMap k v -> HashMap k v -> HashMap k v
HMap.union HashMap QName Definition
b HashMap QName Definition
b')
      (InstanceTable
c InstanceTable -> InstanceTable -> InstanceTable
forall a. Semigroup a => a -> a -> a
<> InstanceTable
c') -- instances are accumulated

-- | Scope checks the given module, generating an interface or retrieving an existing one.
--   Returns the module name and exported scope from the interface.
scopeCheckFileImport ::
     TopLevelModuleName
  -> TCM (ModuleName, Map ModuleName Scope)
scopeCheckFileImport :: TopLevelModuleName' Range -> TCM (ModuleName, Map ModuleName Scope)
scopeCheckFileImport TopLevelModuleName' Range
top = do
    [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.scope" Int
15 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Scope checking " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ TopLevelModuleName' Range -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName' Range
top
    [Char] -> Int -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"import.scope" Int
30 (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
      visited <- Doc -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (Doc -> [Char]) -> TCMT IO Doc -> TCMT IO [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Doc
forall (m :: * -> *). ReadTCState m => m Doc
getPrettyVisitedModules
      reportSLn "import.scope" 30 $ "  visited: " ++ visited
    -- Since scopeCheckFileImport is called from the scope checker,
    -- we need to reimburse her account.
    i <- Account (BenchPhase (TCMT IO))
-> TCMT IO Interface -> TCMT IO Interface
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [] (TCMT IO Interface -> TCMT IO Interface)
-> TCMT IO Interface -> TCMT IO Interface
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName' Range -> Maybe Source -> TCMT IO Interface
getNonMainInterface TopLevelModuleName' Range
top Maybe Source
forall a. Maybe a
Nothing
    addImport top

    -- Print list of imported modules in current state.
    verboseS "import.iface.imports" 10 do
      imports <- Set.toList <$> useTC stImportedModules
      reportSLn "import.iface.imports" 10 $ intercalate "\n" $
        unwords [prettyShow top, "added, all imports:"] :
        map (\ TopLevelModuleName' Range
x -> [[Char]] -> [Char]
unwords [ [Char]
" ", [Char]
"-", TopLevelModuleName' Range -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName' Range
x ]) imports

    -- If that interface was supposed to raise a warning on import, do so.
    whenJust (iImportWarning i) $ warning . UserWarning

    -- let s = publicModules $ iInsideScope i
    let s = Interface -> Map ModuleName Scope
iScope Interface
i
    return (iModuleName i, s)

-- | The result and associated parameters of a type-checked file,
--   when invoked directly via interaction or a backend.
--   Note that the constructor is not exported.

data CheckResult = CheckResult'
  { CheckResult -> ModuleInfo
crModuleInfo :: ModuleInfo
  , CheckResult -> Source
crSource'    :: Source
  }

-- | Flattened unidirectional pattern for 'CheckResult' for destructuring inside
--   the 'ModuleInfo' field.
pattern CheckResult :: Interface -> Set TCWarning -> ModuleCheckMode -> Source -> CheckResult
pattern $mCheckResult :: forall {r}.
CheckResult
-> (Interface -> Set TCWarning -> ModuleCheckMode -> Source -> r)
-> ((# #) -> r)
-> r
CheckResult { CheckResult -> Interface
crInterface, CheckResult -> Set TCWarning
crWarnings, CheckResult -> ModuleCheckMode
crMode, CheckResult -> Source
crSource } <- CheckResult'
    { crModuleInfo = ModuleInfo
        { miInterface = crInterface
        , miWarnings = crWarnings
        , miMode = crMode
        }
    , crSource' = crSource
    }

-- | The result of a type-checking worker.
data WorkerResult
  -- | Type checking the module, or one of its dependencies, failed.
  = WorkerFailed TCErr
  -- | Elaborating the module succeeded.
  | WorkerSucceeded
    { WorkerResult -> SourceFile
successOrigin  :: SourceFile
      -- ^ This was the 'SourceFile' that we just elaborated.
    , WorkerResult -> [TCM ModuleInfo]
successImports :: [TCM ModuleInfo]
      -- ^ These are the actions for waiting on the result of each of
      -- the module's imports.
    }

-- | Structure necessary for synchronising parallel type-checking workers.
data TCWorkers = Workers
  { TCWorkers
-> MVar (HashMap (TopLevelModuleName' Range) (MVar WorkerResult))
workerThreads    :: !(MVar (HMap.HashMap TopLevelModuleName (MVar WorkerResult)))
    -- ^ Synchronized map containing synchronisation points for each
    -- worker to signal completion.
  , TCWorkers -> IORef DecodedModules
workerModules    :: !(IORef DecodedModules)
    -- ^ The shared 'DecodedModules' where workers can put their results.
  , TCWorkers -> IORef Int
workerStarted    :: !(IORef Int)
    -- ^ How many threads have actually started their work. Used for progress reporting.
  }

-- | If the user has asked for it, prepare the type checker for loading
-- in parallel, and return a 'TCWorkers' instance that can be used to
-- coordinate a number of type-checking tasks.
--
-- The given module name, when encountered, will be treated as the
-- 'MainInterface'.
wantsParallelChecking :: TCM (Maybe TCWorkers)
wantsParallelChecking :: TCM (Maybe TCWorkers)
wantsParallelChecking = (CommandLineOptions -> Parallelism)
-> TCMT IO CommandLineOptions -> TCMT IO Parallelism
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CommandLineOptions -> Parallelism
optParallelChecking TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions TCMT IO Parallelism
-> (Parallelism -> TCM (Maybe TCWorkers)) -> TCM (Maybe TCWorkers)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Parallelism
Sequential -> Maybe TCWorkers -> TCM (Maybe TCWorkers)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe TCWorkers
forall a. Maybe a
Nothing
  Parallel{} -> TCWorkers -> Maybe TCWorkers
forall a. a -> Maybe a
Just (TCWorkers -> Maybe TCWorkers)
-> TCMT IO TCWorkers -> TCM (Maybe TCWorkers)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    -- If we're doing parallel type-checking, we have to synchronise the
    -- interaction callback to make sure we don't end up with mangled logs
    -- (or, worse, mangled Lisp!).
    out <- IO (MVar ()) -> TCMT IO (MVar ())
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (MVar ()) -> TCMT IO (MVar ()))
-> IO (MVar ()) -> TCMT IO (MVar ())
forall a b. (a -> b) -> a -> b
$ () -> IO (MVar ())
forall a. a -> IO (MVar a)
newMVar ()
    cb <- getInteractionOutputCallback
    setInteractionOutputCallback \Response_boot TCErr TCWarning WarningsAndNonFatalErrors
r -> TCMT IO () -> (() -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ (IO () -> TCMT IO ()
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (MVar () -> IO ()
forall a. MVar a -> IO a
takeMVar MVar ()
out)) (IO () -> TCMT IO ()
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCMT IO ()) -> (() -> IO ()) -> () -> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MVar () -> () -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar ()
out) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
      InteractionOutputCallback
cb Response_boot TCErr TCWarning WarningsAndNonFatalErrors
r

    threads <- liftIO $ newMVar mempty
    results <- liftIO . newIORef =<< getDecodedModules
    started <- liftIO $ newIORef 0
    pure Workers
      { workerThreads    = threads
      , workerModules    = results
      , workerStarted    = started
      }

-- | Gets the prefix string to use for reporting the progress message
-- (Checking, Loading, etc.) for the module this worker is responsible
-- for.
-- As a side-effect, updates the 'workerStarted' count.
thisWorkerPrefix :: TCWorkers -> TCM String
thisWorkerPrefix :: TCWorkers -> TCMT IO [Char]
thisWorkerPrefix TCWorkers
workers = do
  -- In general, we don't know ahead-of-time how many modules we will
  -- end up checking (e.g. with --build-library, this fluctuates), but
  -- the number of modules for which we have a result slot is a pretty
  -- good estimate.
  sz <- Int -> [Char]
forall a. Show a => a -> [Char]
show (Int -> [Char])
-> (HashMap (TopLevelModuleName' Range) (MVar WorkerResult) -> Int)
-> HashMap (TopLevelModuleName' Range) (MVar WorkerResult)
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap (TopLevelModuleName' Range) (MVar WorkerResult) -> Int
forall k v. HashMap k v -> Int
HMap.size (HashMap (TopLevelModuleName' Range) (MVar WorkerResult) -> [Char])
-> TCMT
     IO (HashMap (TopLevelModuleName' Range) (MVar WorkerResult))
-> TCMT IO [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO (HashMap (TopLevelModuleName' Range) (MVar WorkerResult))
-> TCMT
     IO (HashMap (TopLevelModuleName' Range) (MVar WorkerResult))
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (MVar (HashMap (TopLevelModuleName' Range) (MVar WorkerResult))
-> IO (HashMap (TopLevelModuleName' Range) (MVar WorkerResult))
forall a. MVar a -> IO a
readMVar (TCWorkers
-> MVar (HashMap (TopLevelModuleName' Range) (MVar WorkerResult))
workerThreads TCWorkers
workers))
  me <- liftIO $ atomicModifyIORef (workerStarted workers) \Int
n -> (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Int -> [Char]
forall a. Show a => a -> [Char]
show (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))
  let
    pad = Int -> Char -> [Char]
forall a. Int -> a -> [a]
replicate ([Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
sz Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
me) Char
' '
    out = [Char]
"(" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
pad [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
me [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"/" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
sz [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
") "
  out `deepseq` pure out

-- | Type-check the given module, using a 'TCWorkers' instance to check
-- its imports in parallel.
--
-- Returns an action which *waits* for completion of type-checking of
-- the given module, and merges its interface (and those of the
-- necessary transitive imports) into the current thread's type-checking
-- state.
--
-- If the given 'MainInterface' indicates that we are checking the main
-- module, its checking will happen in the calling thread, and in the
-- calling TC state. Otherwise, a thread (with isolated TC state) is
-- created to check it.
--
-- Regardless of whether we spawned a new thread or not, checking of the
-- given module will block until all of its imports have been checked.
chaseModule
  :: TCWorkers          -- ^ For synchronization
  -> TopLevelModuleName -- ^ The name of the module to check
  -> MainInterface      -- ^ Are we checking the main module?
  -> Maybe Source       -- ^ Pre-parsed source
  -> TCM (TCM ModuleInfo)
chaseModule :: TCWorkers
-> TopLevelModuleName' Range
-> MainInterface
-> Maybe Source
-> TCM (TCM ModuleInfo)
chaseModule TCWorkers
workers TopLevelModuleName' Range
mod MainInterface
main Maybe Source
msrc = do
  let
    -- This is the generic action for waiting on the result of checking
    -- a module. The MVar is used just for signaling.
    use :: MVar WorkerResult -> TCM ModuleInfo
use MVar WorkerResult
var = IO WorkerResult -> TCMT IO WorkerResult
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (MVar WorkerResult -> IO WorkerResult
forall a. MVar a -> IO a
readMVar MVar WorkerResult
var) TCMT IO WorkerResult
-> (WorkerResult -> TCM ModuleInfo) -> TCM ModuleInfo
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      WorkerFailed TCErr
exc -> TCErr -> TCM ModuleInfo
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
exc
      WorkerSucceeded SourceFile
sf [TCM ModuleInfo]
before -> do
        -- Synchronize the DecodedModules in the TC state of this worker
        -- with the global pool
        DecodedModules -> TCMT IO ()
setDecodedModules (DecodedModules -> TCMT IO ())
-> TCMT IO DecodedModules -> TCMT IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO DecodedModules -> TCMT IO DecodedModules
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IORef DecodedModules -> IO DecodedModules
forall a. IORef a -> IO a
readIORef (TCWorkers -> IORef DecodedModules
workerModules TCWorkers
workers))

        -- Make sure that we actually did produce and/or decode an
        -- interface when the worker responsible for this module
        -- finished
        mi <- TopLevelModuleName' Range -> TCM (Maybe ModuleInfo)
getDecodedModule TopLevelModuleName' Range
mod TCM (Maybe ModuleInfo)
-> (Maybe ModuleInfo -> TCM ModuleInfo) -> TCM ModuleInfo
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Just ModuleInfo
mi -> ModuleInfo -> TCM ModuleInfo
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModuleInfo
mi
          Maybe ModuleInfo
Nothing -> [Char] -> TCM ModuleInfo
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ ([Char] -> TCM ModuleInfo) -> [Char] -> TCM ModuleInfo
forall a b. (a -> b) -> a -> b
$
            [Char]
"internal error: parallel loading had thread responsible for "
            [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Doc -> [Char]
forall a. Show a => a -> [Char]
show (TopLevelModuleName' Range -> Doc
forall a. Pretty a => a -> Doc
Mikan.Syntax.Common.Pretty.pretty TopLevelModuleName' Range
mod)
            [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" marked as ready, but it has not been decoded"

        -- The recompilation avoidance code is actually pretty slow
        -- (because it has to e.g. re-parse options to make sure nothing
        -- has changed). We do not pick up those changes when checking
        -- non-interactively. The recompilation avoidance code is also
        -- responsible for loading the dependencies into the TC state:
        --
        --   loadDecodedModule -> moduleHash -> getInterface -> mergeInterface
        --
        -- Since we're going to be skipping that code entirely (it is
        -- the vast majority of the -j overhead when most of the library
        -- is unchanged), we have to manually "replay" the effect of
        -- loadDecodedModule here.
        -- We first do it for the dependencies (stored by the worker in
        -- the result MVar), and then for the actual interface.

        mi <$ whenNothingM (getVisitedModule mod) do
          sequenceErrors_ before
          mergeInterface (miInterface mi)

          Bench.billTo [Bench.Highlighting] $
            ifTopLevelAndHighlightingLevelIs NonInteractive $
              highlightFromInterface (miInterface mi) sf

          visitModule mi

    has :: IO (Either (MVar WorkerResult) (MVar WorkerResult))
has = MVar (HashMap (TopLevelModuleName' Range) (MVar WorkerResult))
-> (HashMap (TopLevelModuleName' Range) (MVar WorkerResult)
    -> IO
         (HashMap (TopLevelModuleName' Range) (MVar WorkerResult),
          Either (MVar WorkerResult) (MVar WorkerResult)))
-> IO (Either (MVar WorkerResult) (MVar WorkerResult))
forall a b. MVar a -> (a -> IO (a, b)) -> IO b
modifyMVar (TCWorkers
-> MVar (HashMap (TopLevelModuleName' Range) (MVar WorkerResult))
workerThreads TCWorkers
workers) \HashMap (TopLevelModuleName' Range) (MVar WorkerResult)
wmap -> case TopLevelModuleName' Range
-> HashMap (TopLevelModuleName' Range) (MVar WorkerResult)
-> Maybe (MVar WorkerResult)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup TopLevelModuleName' Range
mod HashMap (TopLevelModuleName' Range) (MVar WorkerResult)
wmap of
      Just MVar WorkerResult
var -> (HashMap (TopLevelModuleName' Range) (MVar WorkerResult),
 Either (MVar WorkerResult) (MVar WorkerResult))
-> IO
     (HashMap (TopLevelModuleName' Range) (MVar WorkerResult),
      Either (MVar WorkerResult) (MVar WorkerResult))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HashMap (TopLevelModuleName' Range) (MVar WorkerResult)
wmap, MVar WorkerResult -> Either (MVar WorkerResult) (MVar WorkerResult)
forall a b. a -> Either a b
Left MVar WorkerResult
var)
      Maybe (MVar WorkerResult)
Nothing  -> do
        var <- IO (MVar WorkerResult)
forall a. IO (MVar a)
newEmptyMVar
        let nmap = TopLevelModuleName' Range
-> MVar WorkerResult
-> HashMap (TopLevelModuleName' Range) (MVar WorkerResult)
-> HashMap (TopLevelModuleName' Range) (MVar WorkerResult)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HMap.insert TopLevelModuleName' Range
mod MVar WorkerResult
var HashMap (TopLevelModuleName' Range) (MVar WorkerResult)
wmap
        nmap `seq` pure (nmap, Right var)

  -- In the critical section that holds workerThreads, we just decide
  -- whether to spawn a new thread or not.
  -- If the module already had an entry (Left), we can immediately
  -- return the waiting thunk.
  IO (Either (MVar WorkerResult) (MVar WorkerResult))
-> TCMT IO (Either (MVar WorkerResult) (MVar WorkerResult))
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO (Either (MVar WorkerResult) (MVar WorkerResult))
has TCMT IO (Either (MVar WorkerResult) (MVar WorkerResult))
-> (Either (MVar WorkerResult) (MVar WorkerResult)
    -> TCM (TCM ModuleInfo))
-> TCM (TCM ModuleInfo)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Left MVar WorkerResult
var -> MVar WorkerResult -> TCM ModuleInfo
use MVar WorkerResult
var TCM ModuleInfo -> TCMT IO () -> TCM (TCM ModuleInfo)
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"import.parallel" Int
15 (TCMT IO Doc
"reusing " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TopLevelModuleName' Range -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
P.pretty TopLevelModuleName' Range
mod)

    -- Otherwise, we have to handle spawning the new thread to do
    -- type-checking.
    Right MVar WorkerResult
var -> MVar WorkerResult -> TCM ModuleInfo
use MVar WorkerResult
var TCM ModuleInfo -> TCMT IO () -> TCM (TCM ModuleInfo)
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do
      stack <- Lens' TCEnv [TopLevelModuleName' Range]
-> TCMT IO [TopLevelModuleName' Range]
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC ([TopLevelModuleName' Range] -> f [TopLevelModuleName' Range])
-> TCEnv -> f TCEnv
Lens' TCEnv [TopLevelModuleName' Range]
eImportStack

      let
        -- If this is the call corresponding to checking the main
        -- module, we don't start a new thread.
        -- This is because we want to be in the state from checking the
        -- main module, e.g. for interactive checking.
        --
        -- If we *are* starting a new thread, we must install an
        -- exception handler to catch any TCErrs that make it to the top
        -- level, so that they can propagate back to the main thread
        -- eventually.
        detach TCMT IO ()
cont
          | MainInterface Mode
_ <- MainInterface
main = TCMT IO ()
cont
          | Bool
otherwise = do
            TCMT IO () -> TCMT IO ()
forkTCM (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ (TCMT IO () -> (TCErr -> TCMT IO ()) -> TCMT IO ())
-> (TCErr -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip TCMT IO () -> (TCErr -> TCMT IO ()) -> TCMT IO ()
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError (IO () -> TCMT IO ()
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCMT IO ()) -> (TCErr -> IO ()) -> TCErr -> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MVar WorkerResult -> WorkerResult -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar WorkerResult
var (WorkerResult -> IO ())
-> (TCErr -> WorkerResult) -> TCErr -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCErr -> WorkerResult
WorkerFailed) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
            -- If we're starting a new thread, we also need to parse the source file.
            -- For debugging/profiling/etc., label the thread with the
            -- name of the module that we're checking.
            IO () -> TCMT IO ()
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO do
              let name :: [Char]
name = Doc -> [Char]
forall a. Show a => a -> [Char]
show (TopLevelModuleName' Range -> Doc
forall a. Pretty a => a -> Doc
Mikan.Syntax.Common.Pretty.pretty TopLevelModuleName' Range
mod)
              me <- IO ThreadId
myThreadId
              labelThread me ("TC " <> name)
            TCMT IO ()
cont

      detach do
        reportSDoc "import.parallel" 15 $ "checking " <> P.pretty mod
        src <- maybe (parseSource =<< findFile mod) pure msrc

        -- Now we traverse through all the imports and collect the
        -- "promises" for waiting on them. This will spawn the threads
        -- to check them.
        imports <- flip foldDecl (srcModule src) \case
          C.Import OpenShortHand
opn KwRange
r QName
x Either AsName RawOpenArgs
as ImportDirective
is -> do
            let dec :: NiceDeclaration
dec = OpenShortHand
-> KwRange
-> QName
-> Either AsName RawOpenArgs
-> ImportDirective
-> NiceDeclaration
C.NiceImport OpenShortHand
opn KwRange
r QName
x Either AsName RawOpenArgs
as ImportDirective
is
            Call
-> TCMT IO (Endo [TCM ModuleInfo])
-> TCMT IO (Endo [TCM ModuleInfo])
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (NiceDeclaration -> Call
ScopeCheckDeclaration NiceDeclaration
dec) do

            tl  <- RawTopLevelModuleName -> TCM (TopLevelModuleName' Range)
S.topLevelModuleName (QName -> RawTopLevelModuleName
rawTopLevelModuleNameForQName QName
x)

            -- This is a bit fiddly. 'getInterface' below will push mod
            -- onto the import stack, so if we push it around the entire
            -- thread, we get a spurious cyclic import error.
            --
            -- However, we can't also push tl, because *its* worker
            -- thread would end up pushing it, so *it* would be on the
            -- stack twice, too!
            --
            -- We have to check for import cycles here because GHC does
            -- not seem to always generate the proper "thread blocked
            -- indefinitely on MVar operation".
            act <- locallyTC eImportStack (mod:) do
              locallyTC eImportStack (tl:) checkForImportCycle
              chaseModule workers tl NotMainInterface Nothing

            pure $ Endo (act:)

          Declaration
_ -> Endo [TCM ModuleInfo] -> TCMT IO (Endo [TCM ModuleInfo])
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Endo [TCM ModuleInfo]
forall a. Monoid a => a
mempty

        -- Now we wait for all the dependencies and, when that's done,
        -- we can just type-check the module as usual.
        -- Waiting for the dependencies will have moved us to a TC state
        -- where they have been placed in the DecodedModules map, so the
        -- normal type-checking code will just reuse them when we get
        -- around to actually scope checking the import.
        let !before = Endo [TCM ModuleInfo] -> [TCM ModuleInfo] -> [TCM ModuleInfo]
forall a. Endo a -> a -> a
appEndo Endo [TCM ModuleInfo]
imports []
        sequenceErrors_ before

        prefix <- thisWorkerPrefix workers
        mi <- locallyTC eChasePrefix (const (Just prefix)) $
          getInterface mod main (Just src)

        -- If we have any deferred errors in the state, we can't let the
        -- worker finish successfully: see mikan!137.
        raiseNonFatalErrors (miWarnings mi)

        -- After we're done, update the shared DecodedModules map and
        -- signal our completion.
        liftIO do
          atomicModifyIORef (workerModules workers) \DecodedModules
v -> (TopLevelModuleName' Range
-> ModuleInfo -> DecodedModules -> DecodedModules
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TopLevelModuleName' Range
mod ModuleInfo
mi DecodedModules
v, ())
          putMVar var $ WorkerSucceeded (srcOrigin src) before

-- | Type checks the main file of the interaction.
--   This could be the file loaded in the interacting editor (emacs),
--   or the file passed on the command line.
--
--   First, the primitive modules are imported.
--   Then, @getInterface@ is called to do the main work.
--
--   If the 'Mode' is 'ScopeCheck', then type-checking is not
--   performed, only scope-checking. (This may include type-checking
--   of imported modules.) In this case the generated, partial
--   interface is not stored in the state ('stDecodedModules'). Note,
--   however, that if the file has already been type-checked, then a
--   complete interface is returned.

typeCheckMain
  :: Mode
     -- ^ Should the file be type-checked, or only scope-checked?
  -> Source
     -- ^ The decorated source code.
  -> TCM CheckResult
typeCheckMain :: Mode -> Source -> TCM CheckResult
typeCheckMain Mode
mode Source
src = do
  -- liftIO $ putStrLn $ "This is typeCheckMain " ++ prettyShow f
  -- liftIO . putStrLn . show =<< getVerbosity

  -- For the main interface, we also remember the pragmas from the file
  Bool -> Source -> TCMT IO ()
setOptionsFromSourcePragmas Bool
True Source
src

  -- Import the Agda.Primitive modules
  TCMT IO ()
importPrimitiveModules

  -- Now do the type checking via getInterface.
  TopLevelModuleName' Range -> SourceFile -> TCMT IO ()
checkModuleName' (Source -> TopLevelModuleName' Range
srcModuleName Source
src) (Source -> SourceFile
srcOrigin Source
src)

  mi <- TCM (Maybe TCWorkers)
wantsParallelChecking TCM (Maybe TCWorkers)
-> (Maybe TCWorkers -> TCM ModuleInfo) -> TCM ModuleInfo
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just TCWorkers
workers -> TCM (TCM ModuleInfo) -> TCM ModuleInfo
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (TCM (TCM ModuleInfo) -> TCM ModuleInfo)
-> TCM (TCM ModuleInfo) -> TCM ModuleInfo
forall a b. (a -> b) -> a -> b
$ TCWorkers
-> TopLevelModuleName' Range
-> MainInterface
-> Maybe Source
-> TCM (TCM ModuleInfo)
chaseModule TCWorkers
workers (Source -> TopLevelModuleName' Range
srcModuleName Source
src) (Mode -> MainInterface
MainInterface Mode
mode) (Source -> Maybe Source
forall a. a -> Maybe a
Just Source
src)
    Maybe TCWorkers
Nothing      -> TopLevelModuleName' Range
-> MainInterface -> Maybe Source -> TCM ModuleInfo
getInterface (Source -> TopLevelModuleName' Range
srcModuleName Source
src) (Mode -> MainInterface
MainInterface Mode
mode) (Source -> Maybe Source
forall a. a -> Maybe a
Just Source
src)

  stCurrentModule `setTCLens`
    Strict.Just (iModuleName (miInterface mi) :!: iTopLevelModuleName (miInterface mi))

  return $ CheckResult' mi src

-- Andreas, 2016-07-11, issue 2092
-- The error range should be set to the file with the wrong module name
-- not the importing one (which would be the default).
checkModuleName' :: TopLevelModuleName' Range -> SourceFile -> TCM ()
checkModuleName' :: TopLevelModuleName' Range -> SourceFile -> TCMT IO ()
checkModuleName' TopLevelModuleName' Range
m SourceFile
f =
  TopLevelModuleName' Range -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange TopLevelModuleName' Range
m (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName' Range
-> SourceFile -> Maybe (TopLevelModuleName' Range) -> TCMT IO ()
checkModuleName TopLevelModuleName' Range
m SourceFile
f Maybe (TopLevelModuleName' Range)
forall a. Maybe a
Nothing

-- | Import the primitive modules (unless --no-load-primitives).
importPrimitiveModules :: TCM ()
importPrimitiveModules :: TCMT IO ()
importPrimitiveModules = TCMT IO Bool -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (PragmaOptions -> Bool
optLoadPrimitives (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
  [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.main" Int
10 [Char]
"Importing the primitive modules."
  libdirPrim <- Lens' SessionState AbsolutePath -> TCMT IO AbsolutePath
forall (m :: * -> *) a.
ReadTCState m =>
Lens' SessionState a -> m a
useSession (AbsolutePath -> f AbsolutePath) -> SessionState -> f SessionState
Lens' SessionState AbsolutePath
lensPrimitiveLibDir
  reportSLn "import.main" 20 $ "Library primitive dir = " ++ show libdirPrim
  -- Turn off import-chasing messages.
  -- We have to modify the persistent verbosity setting, since
  -- getInterface resets the current verbosity settings to the persistent ones.

  bracket_ (getsTC Lens.getPersistentVerbosity) Lens.putPersistentVerbosity $ do
    -- set root verbosity to 0
    Lens.modifyPersistentVerbosity
      (Strict.Just . Trie.insert [] 0 . Strict.fromMaybe Trie.empty)

    -- We don't want to generate highlighting information for Agda.Primitive.
    withHighlightingLevel None $
      forM_ (map (filePath libdirPrim </>) $ Set.toList primitiveModules) \ [Char]
f -> do
        sf <- AbsolutePath -> TCMT IO SourceFile
forall (m :: * -> *). MonadFileId m => AbsolutePath -> m SourceFile
srcFromPath ([Char] -> AbsolutePath
mkAbsolute [Char]
f)
        primSource <- parseSource sf
        checkModuleName' (srcModuleName primSource) (srcOrigin primSource)
        void $ getNonMainInterface (srcModuleName primSource) (Just primSource)

  reportSLn "import.main" 10 $ "Done importing the primitive modules."

-- | Tries to return the interface associated to the given (imported) module.
--   The time stamp of the relevant interface file is also returned.
--   Calls itself recursively for the imports of the given module.
--   May type check the module.
--   An error is raised if a warning is encountered.
--
--   Do not use this for the main file, use 'typeCheckMain' instead.

getNonMainInterface
  :: TopLevelModuleName
  -> Maybe Source
     -- ^ Optional: the source code and some information about the source code.
  -> TCM Interface
getNonMainInterface :: TopLevelModuleName' Range -> Maybe Source -> TCMT IO Interface
getNonMainInterface TopLevelModuleName' Range
x Maybe Source
msrc = do
  mi <- TopLevelModuleName' Range -> Maybe Source -> TCM ModuleInfo
getNonMainModuleInfo TopLevelModuleName' Range
x Maybe Source
msrc
  tcWarningsToError (TopLevelModuleNameWithSourceFile x $ miSourceFile mi) $ Set.toAscList $ miWarnings mi
  return (miInterface mi)

getNonMainModuleInfo
  :: TopLevelModuleName
  -> Maybe Source
     -- ^ Optional: the source code and some information about the source code.
  -> TCM ModuleInfo
getNonMainModuleInfo :: TopLevelModuleName' Range -> Maybe Source -> TCM ModuleInfo
getNonMainModuleInfo TopLevelModuleName' Range
x Maybe Source
msrc =
  -- Preserve/restore the current pragma options, which will be mutated when loading
  -- and checking the interface.
  TCMT IO PragmaOptions
-> (PragmaOptions -> TCMT IO ())
-> TCM ModuleInfo
-> TCM ModuleInfo
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 -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> a -> m ()
`setTCLens`) (TCM ModuleInfo -> TCM ModuleInfo)
-> TCM ModuleInfo -> TCM ModuleInfo
forall a b. (a -> b) -> a -> b
$
           TopLevelModuleName' Range
-> MainInterface -> Maybe Source -> TCM ModuleInfo
getInterface TopLevelModuleName' Range
x MainInterface
NotMainInterface Maybe Source
msrc

-- | If the module has already been visited (without warnings), then
-- its interface is returned directly.
--
-- Otherwise the interface is loaded via 'getStoredInterface'.
--
-- If that fails it is created via 'createInterface' or, for non-main modules,
-- 'createInterfaceIsolated'.
-- A such created interface is stored for potential later use.

getInterface
  :: TopLevelModuleName
  -> MainInterface
  -> Maybe Source
     -- ^ Optional: the source code and some information about the source code.
  -> TCM ModuleInfo
getInterface :: TopLevelModuleName' Range
-> MainInterface -> Maybe Source -> TCM ModuleInfo
getInterface TopLevelModuleName' Range
x MainInterface
isMain Maybe Source
msrc = Lens' TCEnv [TopLevelModuleName' Range]
-> ([TopLevelModuleName' Range] -> [TopLevelModuleName' Range])
-> TCM ModuleInfo
-> TCM ModuleInfo
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC ([TopLevelModuleName' Range] -> f [TopLevelModuleName' Range])
-> TCEnv -> f TCEnv
Lens' TCEnv [TopLevelModuleName' Range]
eImportStack (TopLevelModuleName' Range
x TopLevelModuleName' Range
-> [TopLevelModuleName' Range] -> [TopLevelModuleName' Range]
forall a. a -> [a] -> [a]
:) do

  -- We remember but reset the pragma options locally.
  currentOptions <- 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
  -- Issue #3644 (Abel 2020-05-08): Set approximate range for errors in options.
  setCurrentRange (C.modPragmas . srcModule <$> msrc) $ do
    -- Now reset the options
    setCommandLineOptions =<< getsTC (stPersistentOptions . stPersistentState)

  -- Lookup x in the collection of visited modules.
  getVisitedModule x >>= \case

    -- Case: already visited and usable.
    Just ModuleInfo
mi
        -- We can only reuse a sufficiently checked module,
        -- e.g. we cannot import a just scope-checked module when type-checking a module.
      | ModuleInfo -> ModuleCheckMode
miMode ModuleInfo
mi ModuleCheckMode -> ModuleCheckMode -> Bool
forall a. Ord a => a -> a -> Bool
>= MainInterface -> ModuleCheckMode
moduleCheckMode MainInterface
isMain
        -- A module with warnings should never be allowed to be imported from another module.
      , Set TCWarning -> Bool
forall a. Null a => a -> Bool
null (Set TCWarning -> Bool) -> Set TCWarning -> Bool
forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Set TCWarning
miWarnings ModuleInfo
mi -> do
          [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.visit" Int
10 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  Already visited " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ TopLevelModuleName' Range -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName' Range
x
          PragmaOptions -> ModuleInfo -> TCM ModuleInfo
addOptionsCompatibilityWarnings PragmaOptions
currentOptions ModuleInfo
mi

    -- Case: not already visited or unusable.
    Maybe ModuleInfo
_ -> do

      -- Load the module.
      [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.visit" Int
5 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  Getting interface for " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ TopLevelModuleName' Range -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName' Range
x

      file <- case Maybe Source
msrc of
        Maybe Source
Nothing  -> TopLevelModuleName' Range -> TCMT IO SourceFile
findFile TopLevelModuleName' Range
x
        Just Source
src -> do
          -- Andreas, 2021-08-17, issue #5508.
          -- So it happened with @msrc == Just{}@ that the file was not added to @ModuleToSource@,
          -- only with @msrc == Nothing@ (then @findFile@ does it).
          -- As a consequence, the file was added later, but with a file name constructed
          -- from a module name.  As #5508 shows, this can be fatal in case-insensitive file systems.
          -- The file name (with case variant) then no longer maps to the module name.
          -- To prevent this, we register the connection in @ModuleToSource@ here,
          -- where we have the correct spelling of the file name.
          let file :: SourceFile
file = Source -> SourceFile
srcOrigin Source
src
          Lens' SessionState (Map (TopLevelModuleName' Range) SourceFile)
-> (Map (TopLevelModuleName' Range) SourceFile
    -> Map (TopLevelModuleName' Range) SourceFile)
-> TCMT IO ()
forall (m :: * -> *) a.
ModifySession m =>
Lens' SessionState a -> (a -> a) -> m ()
modifySession (Map (TopLevelModuleName' Range) SourceFile
 -> f (Map (TopLevelModuleName' Range) SourceFile))
-> SessionState -> f SessionState
Lens' SessionState (Map (TopLevelModuleName' Range) SourceFile)
lensModuleToSourceId ((Map (TopLevelModuleName' Range) SourceFile
  -> Map (TopLevelModuleName' Range) SourceFile)
 -> TCMT IO ())
-> (Map (TopLevelModuleName' Range) SourceFile
    -> Map (TopLevelModuleName' Range) SourceFile)
-> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName' Range
-> SourceFile
-> Map (TopLevelModuleName' Range) SourceFile
-> Map (TopLevelModuleName' Range) SourceFile
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TopLevelModuleName' Range
x SourceFile
file
          SourceFile -> TCMT IO SourceFile
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceFile
file

      reportSDoc "import.iface" 15 do
        path <- srcFilePath file
        P.text $ List.intercalate "\n" $ map ("  " ++)
          [ "module: " ++ prettyShow x
          , "file:   " ++ prettyShow path
          ]

      reportSLn "import.iface" 15 $ "  Check for cycle"
      checkForImportCycle

      mi <- Bench.billTo [Bench.Import] (getStoredInterface x file msrc)
        `catchExceptT` \ [Char]
reason -> do

            [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
5 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Char]
"  ", TopLevelModuleName' Range -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName' Range
x, [Char]
" is not up-to-date because ", [Char]
reason, [Char]
"."]
            CommandLineOptions -> TCMT IO ()
setCommandLineOptions (CommandLineOptions -> TCMT IO ())
-> (TCState -> CommandLineOptions) -> TCState -> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PersistentTCState -> CommandLineOptions
stPersistentOptions (PersistentTCState -> CommandLineOptions)
-> (TCState -> PersistentTCState) -> TCState -> CommandLineOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState (TCState -> TCMT IO ()) -> TCMT IO TCState -> TCMT IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
            mi <- case MainInterface
isMain of
              MainInterface{}  -> TopLevelModuleName' Range
-> SourceFile -> MainInterface -> Maybe Source -> TCM ModuleInfo
createInterface TopLevelModuleName' Range
x SourceFile
file MainInterface
isMain Maybe Source
msrc
              MainInterface
NotMainInterface -> TopLevelModuleName' Range
-> SourceFile -> Maybe Source -> TCM ModuleInfo
createInterfaceIsolated TopLevelModuleName' Range
x SourceFile
file Maybe Source
msrc

            -- Ensure that the given module name matches the one in the file.
            let topLevelName = Interface -> TopLevelModuleName' Range
iTopLevelModuleName (ModuleInfo -> Interface
miInterface ModuleInfo
mi)
            unless (topLevelName == x) do
              path <- srcFilePath file
              typeError $ OverlappingProjects path topLevelName x

            pure mi

      mi <- addOptionsCompatibilityWarnings currentOptions mi
      reportSLn "import.visit" 5 $ "  Now we've looked at " ++ prettyShow x

      -- Interfaces are not stored if we are only scope-checking, or
      -- if any warnings were encountered.
      when (moduleCheckMode isMain == ModuleTypeChecked && null (miWarnings mi)) do
        storeDecodedModule mi

      reportS "warning.import" 10
        [ "module: " ++ show (moduleNameParts x)
        , "WarningOnImport: " ++ show (iImportWarning (miInterface mi))
        ]

      -- Record the module as visited.
      visitModule mi
      return mi
  where
    addOptionsCompatibilityWarnings :: PragmaOptions -> ModuleInfo -> TCM ModuleInfo
    addOptionsCompatibilityWarnings :: PragmaOptions -> ModuleInfo -> TCM ModuleInfo
addOptionsCompatibilityWarnings PragmaOptions
currentOptions
      mi :: ModuleInfo
mi@ModuleInfo{ miInterface :: ModuleInfo -> Interface
miInterface = Interface
i, miPrimitive :: ModuleInfo -> Bool
miPrimitive = Bool
isPrim, miWarnings :: ModuleInfo -> Set TCWarning
miWarnings = Set TCWarning
ws } = do

      -- Andreas, 2026-02-03, issue #8361, debug printing by @nad.
      -- For testing whether 'isBuiltinModule' is thread-safe.
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"import.iface.builtin" Int
25 do
        isBuiltin <- Maybe IsBuiltinModule -> Bool
forall a. Maybe a -> Bool
isJust (Maybe IsBuiltinModule -> Bool)
-> TCMT IO (Maybe IsBuiltinModule) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FileId -> TCMT IO (Maybe IsBuiltinModule)
forall (m :: * -> *).
ReadTCState m =>
FileId -> m (Maybe IsBuiltinModule)
isBuiltinModule (SourceFile -> FileId
srcFileId (ModuleInfo -> SourceFile
miSourceFile ModuleInfo
mi))
        P.hsep [ "The module", prettyTCM (iTopLevelModuleName i), "is"
               , if isBuiltin then "primitive." else "not primitive."
               ]

      -- Check that imported options are compatible with current ones (issue #2487),
      -- but give primitive modules a pass.
      -- Compute updated warnings if needed.
      ws' <- Set TCWarning -> Maybe (Set TCWarning) -> Set TCWarning
forall a. a -> Maybe a -> a
fromMaybe Set TCWarning
ws (Maybe (Set TCWarning) -> Set TCWarning)
-> TCMT IO (Maybe (Set TCWarning)) -> TCMT IO (Set TCWarning)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MainInterface
-> Bool
-> PragmaOptions
-> Interface
-> TCMT IO (Maybe (Set TCWarning))
getOptionsCompatibilityWarnings MainInterface
isMain Bool
isPrim PragmaOptions
currentOptions Interface
i
      return mi{ miWarnings = ws' }

-- | If checking produced non-benign warnings, error out.
--
raiseNonFatalErrors :: (HasOptions m, MonadTCError m)
  => Set TCWarning  -- ^ E.g. obtained from 'typeCheckMain'.
  -> m ()
raiseNonFatalErrors :: forall (m :: * -> *).
(HasOptions m, MonadTCError m) =>
Set TCWarning -> m ()
raiseNonFatalErrors Set TCWarning
result = do
  m (Set TCWarning) -> (Set1 TCWarning -> m ()) -> m ()
forall (m :: * -> *) a.
Monad m =>
m (Set a) -> (Set1 a -> m ()) -> m ()
Set1.unlessNullM (Set TCWarning -> m (Set TCWarning)
forall (m :: * -> *).
HasOptions m =>
Set TCWarning -> m (Set TCWarning)
applyFlagsToTCWarnings Set TCWarning
result) \ Set1 TCWarning
ws ->
    TypeError -> m ()
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Set1 TCWarning -> TypeError
NonFatalErrors Set1 TCWarning
ws

-- | Check if the options used for checking an imported module are
--   compatible with the current options. Raises Non-fatal errors if
--   not.
checkOptionsCompatible ::
  PragmaOptions -> PragmaOptions -> TopLevelModuleName -> TCM Bool
checkOptionsCompatible :: PragmaOptions
-> PragmaOptions -> TopLevelModuleName' Range -> TCMT IO Bool
checkOptionsCompatible PragmaOptions
current PragmaOptions
imported TopLevelModuleName' Range
importedModule = (StateT Bool (TCMT IO) () -> Bool -> TCMT IO Bool)
-> Bool -> StateT Bool (TCMT IO) () -> TCMT IO Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT Bool (TCMT IO) () -> Bool -> TCMT IO Bool
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT Bool
True (StateT Bool (TCMT IO) () -> TCMT IO Bool)
-> StateT Bool (TCMT IO) () -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ do
  [Char] -> Int -> TCMT IO Doc -> StateT Bool (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"import.iface.options" Int
25 (TCMT IO Doc -> StateT Bool (TCMT IO) ())
-> TCMT IO Doc -> StateT Bool (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
P.nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"current options  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> PragmaOptions -> TCMT IO Doc
forall {m :: * -> *}.
(Applicative m, Semigroup (m Doc), IsString (m Doc)) =>
PragmaOptions -> m Doc
showOptions PragmaOptions
current
  [Char] -> Int -> TCMT IO Doc -> StateT Bool (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"import.iface.options" Int
25 (TCMT IO Doc -> StateT Bool (TCMT IO) ())
-> TCMT IO Doc -> StateT Bool (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
P.nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"imported options =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> PragmaOptions -> TCMT IO Doc
forall {m :: * -> *}.
(Applicative m, Semigroup (m Doc), IsString (m Doc)) =>
PragmaOptions -> m Doc
showOptions PragmaOptions
imported
  [InfectiveCoinfectiveOption]
-> (InfectiveCoinfectiveOption -> StateT Bool (TCMT IO) ())
-> StateT Bool (TCMT IO) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [InfectiveCoinfectiveOption]
infectiveCoinfectiveOptions ((InfectiveCoinfectiveOption -> StateT Bool (TCMT IO) ())
 -> StateT Bool (TCMT IO) ())
-> (InfectiveCoinfectiveOption -> StateT Bool (TCMT IO) ())
-> StateT Bool (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ \InfectiveCoinfectiveOption
opt -> do
    Bool -> StateT Bool (TCMT IO) () -> StateT Bool (TCMT IO) ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (InfectiveCoinfectiveOption
-> PragmaOptions -> PragmaOptions -> Bool
icOptionOK InfectiveCoinfectiveOption
opt PragmaOptions
current PragmaOptions
imported) (StateT Bool (TCMT IO) () -> StateT Bool (TCMT IO) ())
-> StateT Bool (TCMT IO) () -> StateT Bool (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ do
      [Char] -> Int -> TCMT IO Doc -> StateT Bool (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"import.iface.options" Int
25 (TCMT IO Doc -> StateT Bool (TCMT IO) ())
-> TCMT IO Doc -> StateT Bool (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
P.nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"incompatible: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
P.text (InfectiveCoinfectiveOption -> [Char]
icOptionDescription InfectiveCoinfectiveOption
opt)
        TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
", current: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> Bool -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
P.pretty (InfectiveCoinfectiveOption -> PragmaOptions -> Bool
icOptionActive InfectiveCoinfectiveOption
opt PragmaOptions
current)
        TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
", imported: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> Bool -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
P.pretty (InfectiveCoinfectiveOption -> PragmaOptions -> Bool
icOptionActive InfectiveCoinfectiveOption
opt PragmaOptions
imported)
      Bool -> StateT Bool (TCMT IO) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put Bool
False
      Warning -> StateT Bool (TCMT IO) ()
forall (m :: * -> *) e.
(HasCallStack, MonadWarning m, Diagnostic e) =>
e -> m ()
warning (Warning -> StateT Bool (TCMT IO) ())
-> Warning -> StateT Bool (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
        (case InfectiveCoinfectiveOption -> InfectiveCoinfective
icOptionKind InfectiveCoinfectiveOption
opt of
           InfectiveCoinfective
Infective   -> Doc -> Warning
InfectiveImport
           InfectiveCoinfective
Coinfective -> Doc -> Warning
CoInfectiveImport)
        (InfectiveCoinfectiveOption -> TopLevelModuleName' Range -> Doc
icOptionWarning InfectiveCoinfectiveOption
opt TopLevelModuleName' Range
importedModule)
  where
  showOptions :: PragmaOptions -> m Doc
showOptions PragmaOptions
opts =
    [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
P.prettyList ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
    (InfectiveCoinfectiveOption -> m Doc)
-> [InfectiveCoinfectiveOption] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\InfectiveCoinfectiveOption
opt -> ([Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
P.text (InfectiveCoinfectiveOption -> [Char]
icOptionDescription InfectiveCoinfectiveOption
opt) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
": ") m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+>
                 Bool -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
P.pretty (InfectiveCoinfectiveOption -> PragmaOptions -> Bool
icOptionActive InfectiveCoinfectiveOption
opt PragmaOptions
opts))
      [InfectiveCoinfectiveOption]
infectiveCoinfectiveOptions

-- | Compare options and return collected warnings.
-- | Returns `Nothing` if warning collection was skipped.

getOptionsCompatibilityWarnings ::
     MainInterface
  -> Bool           -- ^ Are we looking at a primitvie module?
  -> PragmaOptions
  -> Interface
  -> TCM (Maybe (Set TCWarning))
getOptionsCompatibilityWarnings :: MainInterface
-> Bool
-> PragmaOptions
-> Interface
-> TCMT IO (Maybe (Set TCWarning))
getOptionsCompatibilityWarnings MainInterface
isMain Bool
False PragmaOptions
currentOptions Interface{ PragmaOptions
iOptionsUsed :: PragmaOptions
iOptionsUsed :: Interface -> PragmaOptions
iOptionsUsed, TopLevelModuleName' Range
iTopLevelModuleName :: Interface -> TopLevelModuleName' Range
iTopLevelModuleName :: TopLevelModuleName' Range
iTopLevelModuleName } = do
  TCMT IO Bool
-> TCMT IO (Maybe (Set TCWarning))
-> TCMT IO (Maybe (Set TCWarning))
-> TCMT IO (Maybe (Set TCWarning))
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (PragmaOptions
-> PragmaOptions -> TopLevelModuleName' Range -> TCMT IO Bool
checkOptionsCompatible PragmaOptions
currentOptions PragmaOptions
iOptionsUsed TopLevelModuleName' Range
iTopLevelModuleName)
    {-then-} (Maybe (Set TCWarning) -> TCMT IO (Maybe (Set TCWarning))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Set TCWarning)
forall a. Maybe a
Nothing) -- No warnings to collect because options were compatible.
    {-else-} (Set TCWarning -> Maybe (Set TCWarning)
forall a. a -> Maybe a
Just (Set TCWarning -> Maybe (Set TCWarning))
-> TCMT IO (Set TCWarning) -> TCMT IO (Maybe (Set TCWarning))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MainInterface -> WhichWarnings -> TCMT IO (Set TCWarning)
forall (m :: * -> *).
(MonadWarning m, MonadTCM m) =>
MainInterface -> WhichWarnings -> m (Set TCWarning)
getAllWarnings' MainInterface
isMain WhichWarnings
ErrorWarnings)
-- Options consistency checking is disabled for always-available primitive modules.
getOptionsCompatibilityWarnings MainInterface
_ Bool
True PragmaOptions
_ Interface
_ = Maybe (Set TCWarning) -> TCMT IO (Maybe (Set TCWarning))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Set TCWarning)
forall a. Maybe a
Nothing

-- | Try to get the interface from interface file or cache.

getStoredInterface :: HasCallStack
  => TopLevelModuleName
     -- ^ Module name of file we process.
  -> SourceFile
     -- ^ File we process.
  -> Maybe Source
  -> ExceptT String TCM ModuleInfo
getStoredInterface :: HasCallStack =>
TopLevelModuleName' Range
-> SourceFile
-> Maybe Source
-> ExceptT [Char] (TCMT IO) ModuleInfo
getStoredInterface TopLevelModuleName' Range
x file :: SourceFile
file@(SourceFile FileId
fi) Maybe Source
msrc = do

  -- Check whether interface file exists and is in cache
  --  in the correct version (as testified by the interface file hash).
  --
  -- This is a lazy action which may be skipped if there is no cached interface
  -- and we're ignoring interface files for some reason.
  let getIFileHashesET :: ExceptT [Char] (TCMT IO) (InterfaceFile, (Hash, Hash))
getIFileHashesET = do
        -- Check that the interface file exists and return its hash.
        ifile <- [Char]
-> MaybeT (TCMT IO) InterfaceFile
-> ExceptT [Char] (TCMT IO) InterfaceFile
forall (m :: * -> *) e a.
Functor m =>
e -> MaybeT m a -> ExceptT e m a
maybeToExceptT [Char]
"the interface file could not be found" (MaybeT (TCMT IO) InterfaceFile
 -> ExceptT [Char] (TCMT IO) InterfaceFile)
-> MaybeT (TCMT IO) InterfaceFile
-> ExceptT [Char] (TCMT IO) InterfaceFile
forall a b. (a -> b) -> a -> b
$ TCMT IO (Maybe InterfaceFile) -> MaybeT (TCMT IO) InterfaceFile
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe InterfaceFile) -> MaybeT (TCMT IO) InterfaceFile)
-> TCMT IO (Maybe InterfaceFile) -> MaybeT (TCMT IO) InterfaceFile
forall a b. (a -> b) -> a -> b
$
          HasCallStack => SourceFile -> TCMT IO (Maybe InterfaceFile)
SourceFile -> TCMT IO (Maybe InterfaceFile)
findInterfaceFile' SourceFile
file

        -- Check that the interface file exists and return its hash.
        hashes <- maybeToExceptT "the interface file hash could not be read" $ MaybeT $ liftIO $
          getInterfaceFileHashes ifile

        return (ifile, hashes)

  -- Examine the hash of the interface file. If it is different from the
  -- stored version (in stDecodedModules), or if there is no stored version,
  -- read and decode it. Otherwise use the stored version.
  --
  -- This is a lazy action which may be skipped if the cached or on-disk interface
  -- is invalid, missing, or skipped for some other reason.
  let checkSourceHashET :: Hash -> ExceptT [Char] (TCMT IO) ()
checkSourceHashET Hash
ifaceH = do
        sourceH <- TCMT IO Hash -> ExceptT [Char] (TCMT IO) Hash
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Hash -> ExceptT [Char] (TCMT IO) Hash)
-> TCMT IO Hash -> ExceptT [Char] (TCMT IO) Hash
forall a b. (a -> b) -> a -> b
$ SourceFile -> TCMT IO Hash
hashSourceFile SourceFile
file

        unless (sourceH == ifaceH) $
          throwError $ concat
            [ "the source hash (", show sourceH, ")"
            , " does not match the source hash for the interface (", show ifaceH, ")"
            ]

        reportSLn "import.iface" 5 $ concat ["  ", prettyShow x, " is up-to-date."]

  let
    -- Load or reload the interface file, if possible.
    loadInterfaceFile :: [Char] -> ExceptT [Char] (TCMT IO) ModuleInfo
loadInterfaceFile [Char]
whyNotCached =
      ShowS
-> ExceptT [Char] (TCMT IO) ModuleInfo
-> ExceptT [Char] (TCMT IO) ModuleInfo
forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT (\[Char]
e -> [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Char]
whyNotCached, [Char]
" and ", [Char]
e]) (ExceptT [Char] (TCMT IO) ModuleInfo
 -> ExceptT [Char] (TCMT IO) ModuleInfo)
-> ExceptT [Char] (TCMT IO) ModuleInfo
-> ExceptT [Char] (TCMT IO) ModuleInfo
forall a b. (a -> b) -> a -> b
$ do
      ExceptT [Char] (TCMT IO) Bool
-> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ExceptT [Char] (TCMT IO) Bool
forall (m :: * -> *). HasOptions m => m Bool
ignoreAllInterfaces (ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ())
-> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
        [Char] -> ExceptT [Char] (TCMT IO) ()
forall a. [Char] -> ExceptT [Char] (TCMT IO) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"we're ignoring all interface files"

      ExceptT [Char] (TCMT IO) Bool
-> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ExceptT [Char] (TCMT IO) Bool
forall (m :: * -> *). HasOptions m => m Bool
ignoreInterfaces (ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ())
-> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
        ExceptT [Char] (TCMT IO) (Maybe IsBuiltinModule)
-> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall (m :: * -> *) a. Monad m => m (Maybe a) -> m () -> m ()
whenNothingM (FileId -> ExceptT [Char] (TCMT IO) (Maybe IsBuiltinModule)
forall (m :: * -> *).
ReadTCState m =>
FileId -> m (Maybe IsBuiltinModule)
isBuiltinModule FileId
fi) (ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ())
-> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
            [Char] -> ExceptT [Char] (TCMT IO) ()
forall a. [Char] -> ExceptT [Char] (TCMT IO) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"we're ignoring non-builtin interface files"

      (ifile, hashes) <- ExceptT [Char] (TCMT IO) (InterfaceFile, (Hash, Hash))
getIFileHashesET

      let ifp = AbsolutePath -> [Char]
filePath (AbsolutePath -> [Char]) -> AbsolutePath -> [Char]
forall a b. (a -> b) -> a -> b
$ InterfaceFile -> AbsolutePath
intFilePath (InterfaceFile -> AbsolutePath) -> InterfaceFile -> AbsolutePath
forall a b. (a -> b) -> a -> b
$ InterfaceFile
ifile

      Bench.billTo [Bench.Deserialization] $ do
        checkSourceHashET (fst hashes)

        reportSLn "import.iface" 5 $ "  no stored version, reading " ++ ifp

        i <- maybeToExceptT "bad interface, re-type checking" $ MaybeT $
          readInterface ifile

        -- Ensure that the given module name matches the one in the file.
        let topLevelName = Interface -> TopLevelModuleName' Range
iTopLevelModuleName Interface
i
        unless (topLevelName == x) do
          path <- srcFilePath file
          lift $ typeError $ OverlappingProjects path topLevelName x

        isPrimitiveMod <- isPrimitiveModule fi

        lift $ chaseMsg "Loading " x $ Just ifp
        -- print imported warnings
        reportWarningsForModule x $ iWarnings i

        loadDecodedModule file $ ModuleInfo
          { miInterface = i
          , miWarnings = empty
          , miPrimitive = isPrimitiveMod
          , miMode = ModuleTypeChecked
          , miSourceFile = file
          }

  -- Check if we have cached the module.
  cachedE <- ExceptT [Char] (ExceptT [Char] (TCMT IO)) ModuleInfo
-> ExceptT [Char] (TCMT IO) (Either [Char] ModuleInfo)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT [Char] (ExceptT [Char] (TCMT IO)) ModuleInfo
 -> ExceptT [Char] (TCMT IO) (Either [Char] ModuleInfo))
-> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ModuleInfo
-> ExceptT [Char] (TCMT IO) (Either [Char] ModuleInfo)
forall a b. (a -> b) -> a -> b
$ [Char]
-> MaybeT (ExceptT [Char] (TCMT IO)) ModuleInfo
-> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ModuleInfo
forall (m :: * -> *) e a.
Functor m =>
e -> MaybeT m a -> ExceptT e m a
maybeToExceptT [Char]
"the interface has not been decoded" (MaybeT (ExceptT [Char] (TCMT IO)) ModuleInfo
 -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ModuleInfo)
-> MaybeT (ExceptT [Char] (TCMT IO)) ModuleInfo
-> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ModuleInfo
forall a b. (a -> b) -> a -> b
$ ExceptT [Char] (TCMT IO) (Maybe ModuleInfo)
-> MaybeT (ExceptT [Char] (TCMT IO)) ModuleInfo
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (ExceptT [Char] (TCMT IO) (Maybe ModuleInfo)
 -> MaybeT (ExceptT [Char] (TCMT IO)) ModuleInfo)
-> ExceptT [Char] (TCMT IO) (Maybe ModuleInfo)
-> MaybeT (ExceptT [Char] (TCMT IO)) ModuleInfo
forall a b. (a -> b) -> a -> b
$
      TCM (Maybe ModuleInfo)
-> ExceptT [Char] (TCMT IO) (Maybe ModuleInfo)
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (Maybe ModuleInfo)
 -> ExceptT [Char] (TCMT IO) (Maybe ModuleInfo))
-> TCM (Maybe ModuleInfo)
-> ExceptT [Char] (TCMT IO) (Maybe ModuleInfo)
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName' Range -> TCM (Maybe ModuleInfo)
getDecodedModule TopLevelModuleName' Range
x

  case cachedE of
    Left [Char]
whyNotCached -> [Char] -> ExceptT [Char] (TCMT IO) ModuleInfo
loadInterfaceFile [Char]
whyNotCached

    -- If it's cached ignoreInterfaces has no effect;
    -- to avoid typechecking a file more than once.
    Right ModuleInfo
mi -> do
      (ifile, hashes) <- ExceptT [Char] (TCMT IO) (InterfaceFile, (Hash, Hash))
getIFileHashesET

      let ifp = AbsolutePath -> [Char]
filePath (AbsolutePath -> [Char]) -> AbsolutePath -> [Char]
forall a b. (a -> b) -> a -> b
$ InterfaceFile -> AbsolutePath
intFilePath InterfaceFile
ifile
      let i = ModuleInfo -> Interface
miInterface ModuleInfo
mi

      -- Make sure the hashes match.
      let cachedIfaceHash = Interface -> Hash
iFullHash Interface
i
      let fileIfaceHash = (Hash, Hash) -> Hash
forall a b. (a, b) -> b
snd (Hash, Hash)
hashes
      if cachedIfaceHash /= fileIfaceHash then do
        lift $ dropDecodedModule x
        reportSLn "import.iface" 50 $ "  cached hash = " ++ show cachedIfaceHash
        reportSLn "import.iface" 50 $ "  stored hash = " ++ show fileIfaceHash
        reportSLn "import.iface" 5 $ "  file is newer, re-reading " ++ ifp
        loadInterfaceFile $ concat
          [ "the cached interface hash (", show cachedIfaceHash, ")"
          , " does not match interface file (", show fileIfaceHash, ")"
          ]
       else Bench.billTo [Bench.Deserialization] $ do
        checkSourceHashET (iSourceHash i)

        reportSLn "import.iface" 5 $ "  using stored version of " ++ filePath (intFilePath ifile)
        loadDecodedModule file mi

-- | Report those given warnings that come from the given module.

reportWarningsForModule :: MonadDebug m => TopLevelModuleName -> Set (TCWarning' a) -> m ()
reportWarningsForModule :: forall (m :: * -> *) a.
MonadDebug m =>
TopLevelModuleName' Range -> Set (TCWarning' a) -> m ()
reportWarningsForModule TopLevelModuleName' Range
x Set (TCWarning' a)
warns = do
  [TCWarning' a] -> ([TCWarning' a] -> m ()) -> m ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull ((TCWarning' a -> Bool) -> [TCWarning' a] -> [TCWarning' a]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Maybe (TopLevelModuleName' Range)
-> Maybe (Maybe (TopLevelModuleName' Range))
forall a. a -> Maybe a
Strict.Just (TopLevelModuleName' Range -> Maybe (TopLevelModuleName' Range)
forall a. a -> Maybe a
Just TopLevelModuleName' Range
x) Maybe (Maybe (TopLevelModuleName' Range))
-> Maybe (Maybe (TopLevelModuleName' Range)) -> Bool
forall a. Eq a => a -> a -> Bool
==) (Maybe (Maybe (TopLevelModuleName' Range)) -> Bool)
-> (TCWarning' a -> Maybe (Maybe (TopLevelModuleName' Range)))
-> TCWarning' a
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RangeFile -> Maybe (TopLevelModuleName' Range))
-> Maybe RangeFile -> Maybe (Maybe (TopLevelModuleName' Range))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RangeFile -> Maybe (TopLevelModuleName' Range)
rangeFileName (Maybe RangeFile -> Maybe (Maybe (TopLevelModuleName' Range)))
-> (TCWarning' a -> Maybe RangeFile)
-> TCWarning' a
-> Maybe (Maybe (TopLevelModuleName' Range))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning' a -> Maybe RangeFile
forall a. TCWarning' a -> Maybe RangeFile
tcWarningOrigin) ([TCWarning' a] -> [TCWarning' a])
-> [TCWarning' a] -> [TCWarning' a]
forall a b. (a -> b) -> a -> b
$ Set (TCWarning' a) -> [TCWarning' a]
forall a. Set a -> [a]
Set.toAscList Set (TCWarning' a)
warns) \ [TCWarning' a]
ws ->
    [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
alwaysReportSDoc [Char]
"warning" Int
1 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
      -- Andreas, 2025-08-01, PR #8040
      -- Make sure that imported warnings coming from different modules are separated by an empty line.
      -- E.g. test/Succeed/ImportWarnings
      -- Technique from PR #7473:
      [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
P.vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (TCWarning' a -> [TCMT IO Doc]) -> [TCWarning' a] -> [TCMT IO Doc]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ TCWarning' a
w -> [ TCMT IO Doc
"", TCWarning' a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCWarning' a -> m Doc
P.prettyTCM TCWarning' a
w ]) [TCWarning' a]
ws
      -- Technique from PR #7362:
      -- P.vsep $ map P.prettyTCM ws

-- | Check whether the loaded module is up-to-date
--   and merge into state if this is the case.
--
loadDecodedModule
  :: SourceFile
     -- ^ File we process.
  -> ModuleInfo
     -- ^ The interface we loaded or created.
  -> ExceptT String TCM ModuleInfo
loadDecodedModule :: SourceFile -> ModuleInfo -> ExceptT [Char] (TCMT IO) ModuleInfo
loadDecodedModule sf :: SourceFile
sf@(SourceFile FileId
fi) ModuleInfo
mi = do
  file <- SourceFile -> ExceptT [Char] (TCMT IO) AbsolutePath
forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
srcFilePath SourceFile
sf
  let fp      = AbsolutePath -> [Char]
filePath AbsolutePath
file
  let i       = ModuleInfo -> Interface
miInterface ModuleInfo
mi
  let imports = Interface -> [(TopLevelModuleName' Range, Hash)]
iImportedModules Interface
i
  let name    = Interface -> TopLevelModuleName' Range
iTopLevelModuleName Interface
i

  -- Print imported modules.
  verboseS "import.iface.imports" 5 $ unless (null imports) $
    reportSLn "import.iface.imports" 5 $ intercalate "\n" $
      unwords [ prettyShow name, "imports:" ] :
      map (\ (TopLevelModuleName' Range
x, Hash
hash) -> [[Char]] -> [Char]
unwords [ [Char]
" ", [Char]
"-", TopLevelModuleName' Range -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName' Range
x, [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Char]
"(hash: ", Hash -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Hash
hash, [Char]
")"] ])
        imports

  -- We set the pragma options of the skipped file here, so that
  -- we can check that they are compatible with those of the
  -- imported modules. Also, if the top-level file is skipped we
  -- want the pragmas to apply to interactive commands in the UI.
  -- Jesper, 2021-04-18: Check for changed options in library files!
  -- (see #5250)
  libOptions <- lift $ getLibraryOptions file name
  lift $ mapM_ setOptionsFromPragma (libOptions ++ iFilePragmaOptions i)

  -- Check that options that matter haven't changed compared to
  -- current options (issue #2487).
  whenNothingM (isBuiltinModule fi) do
    current <- useTC stPragmaOptions
    when (recheckBecausePragmaOptionsChanged (iOptionsUsed i) current) $
      throwError "options changed"

  -- If any of the imports are newer we need to re-typecheck.
  badHashMessages <- fmap lefts $ forM imports \ (TopLevelModuleName' Range
impName, Hash
impHash) -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ()
-> ExceptT [Char] (TCMT IO) (Either [Char] ())
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT do
    [Char]
-> Int -> [Char] -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
30 ([Char] -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ())
-> [Char] -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Char]
"Checking that module hash of import ", TopLevelModuleName' Range -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName' Range
impName, [Char]
" matches ", Hash -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Hash
impHash ]
    latestImpHash <- ExceptT [Char] (TCMT IO) Hash
-> ExceptT [Char] (ExceptT [Char] (TCMT IO)) Hash
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ExceptT [Char] (TCMT IO) Hash
 -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) Hash)
-> ExceptT [Char] (TCMT IO) Hash
-> ExceptT [Char] (ExceptT [Char] (TCMT IO)) Hash
forall a b. (a -> b) -> a -> b
$ TCMT IO Hash -> ExceptT [Char] (TCMT IO) Hash
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Hash -> ExceptT [Char] (TCMT IO) Hash)
-> TCMT IO Hash -> ExceptT [Char] (TCMT IO) Hash
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName' Range -> TCMT IO Hash -> TCMT IO Hash
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange TopLevelModuleName' Range
impName (TCMT IO Hash -> TCMT IO Hash) -> TCMT IO Hash -> TCMT IO Hash
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName' Range -> TCMT IO Hash
moduleHash TopLevelModuleName' Range
impName
    reportSLn "import.iface" 30 $ concat ["Done checking module hash of import ", prettyShow impName]
    when (impHash /= latestImpHash) $
      throwError $ concat
        [ "module hash for imported module ", prettyShow impName, " is out of date"
        , " (import cached=", prettyShow impHash, ", latest=", prettyShow latestImpHash, ")"
        ]

  unlessNull badHashMessages (throwError . unlines)

  reportSLn "import.iface" 5 $ prettyShow name ++ ": interface is valid and can be merged into the state."

  lift $ mergeInterface i
  Bench.billTo [Bench.Highlighting] $
    lift $ ifTopLevelAndHighlightingLevelIs NonInteractive $
      highlightFromInterface i sf

  return mi

-- | Run the type checker on a file and create an interface.
--
--   Mostly, this function calls 'createInterface'.
--   But if it is not the main module we check,
--   we do it in a fresh state, suitably initialize,
--   in order to forget some state changes after successful type checking.

createInterfaceIsolated ::
     TopLevelModuleName
     -- ^ Module name of file we process.
  -> SourceFile
     -- ^ File we process.
  -> Maybe Source
     -- ^ Optional: the source code and some information about the source code.
  -> TCM ModuleInfo
createInterfaceIsolated :: TopLevelModuleName' Range
-> SourceFile -> Maybe Source -> TCM ModuleInfo
createInterfaceIsolated TopLevelModuleName' Range
x SourceFile
file Maybe Source
msrc = do
      TCMT IO ()
forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog
      ms          <- Lens' TCEnv [TopLevelModuleName' Range]
-> TCMT IO [TopLevelModuleName' Range]
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC ([TopLevelModuleName' Range] -> f [TopLevelModuleName' Range])
-> TCEnv -> f TCEnv
Lens' TCEnv [TopLevelModuleName' Range]
eImportStack
      pref        <- viewTC eChasePrefix
      range       <- viewTC eRange
      call        <- viewTC eCall
      vs          <- getVisitedModules
      ds          <- getDecodedModules
      opts        <- stPersistentOptions . stPersistentState <$> getTC
      isig        <- useTC stImports
      metas       <- useTC stImportedMetaStore
      ibuiltin    <- useTC stImportedBuiltins
      display     <- useTC stImportsDisplayForms
      userwarn    <- useTC stImportedUserWarnings
      partialdefs <- useTC stImportedPartialDefs
      opaqueblk   <- useTC stOpaqueBlocks
      opaqueid    <- useTC stOpaqueIds
      ipatsyns <- getPatternSynImports
      -- Every interface is treated in isolation. Note: Some changes to
      -- the persistent state may not be preserved if an error other
      -- than a type error or an IO exception is encountered in an
      -- imported module.
      (mi, newDecodedModules) <- (either throwError pure =<<) $
           withoutCache $
           -- The cache should not be used for an imported module, and it
           -- should be restored after the module has been type-checked
           freshTCM $
             localTC (
                -- Andreas, 2014-08-18:
                -- Preserve the range of import statement
                -- for reporting termination errors in
                -- imported modules:
                        set eRange range
                      . set eCall call
                      . set eImportStack ms
                      . set eChasePrefix pref
                     ) do
               setDecodedModules ds
               setCommandLineOptions opts
               setVisitedModules vs
               addImportedThings isig metas ibuiltin ipatsyns display
                 userwarn partialdefs empty opaqueblk opaqueid

               r  <- createInterface x file NotMainInterface msrc
               ds' <- getDecodedModules
               return (r, ds')

      setDecodedModules newDecodedModules

      -- We skip the file which has just been type-checked to
      -- be able to forget some of the local state from
      -- checking the module.
      -- Note that this doesn't actually read the interface
      -- file, only the cached interface. (This comment is not
      -- correct, see
      -- test/Fail/customised/NestedProjectRoots.err.)
      validated <- runExceptT $ loadDecodedModule file mi

      -- NOTE: This attempts to type-check FOREVER if for some
      -- reason it continually fails to validate interface.
      let recheckOnError = \[Char]
msg -> do
            [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
alwaysReportSLn [Char]
"import.iface" Int
1 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Failed to validate just-loaded interface: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
msg
            TopLevelModuleName' Range
-> SourceFile -> Maybe Source -> TCM ModuleInfo
createInterfaceIsolated TopLevelModuleName' Range
x SourceFile
file Maybe Source
msrc

      either recheckOnError pure validated


-- | Formats and outputs the "Checking", "Finished" and "Loading " messages.

chaseMsg
  :: String               -- ^ The prefix, like @Checking@, @Finished@, @Loading @.
  -> TopLevelModuleName   -- ^ The module name.
  -> Maybe String         -- ^ Optionally: the file name.
  -> TCM ()
chaseMsg :: [Char] -> TopLevelModuleName' Range -> Maybe [Char] -> TCMT IO ()
chaseMsg [Char]
kind TopLevelModuleName' Range
x Maybe [Char]
file = do
  indentation <- Lens' TCEnv (Maybe [Char]) -> TCMT IO (Maybe [Char])
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Maybe [Char] -> f (Maybe [Char])) -> TCEnv -> f TCEnv
Lens' TCEnv (Maybe [Char])
eChasePrefix TCMT IO (Maybe [Char])
-> (Maybe [Char] -> TCMT IO [Char]) -> TCMT IO [Char]
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just [Char]
pref -> [Char] -> TCMT IO [Char]
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Char]
pref
    Maybe [Char]
Nothing   -> (Int -> Char -> [Char]
forall a. Int -> a -> [a]
`replicate` Char
' ') (Int -> [Char])
-> ([TopLevelModuleName' Range] -> Int)
-> [TopLevelModuleName' Range]
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int
forall a. Enum a => a -> a
pred (Int -> Int)
-> ([TopLevelModuleName' Range] -> Int)
-> [TopLevelModuleName' Range]
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TopLevelModuleName' Range] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([TopLevelModuleName' Range] -> [Char])
-> TCMT IO [TopLevelModuleName' Range] -> TCMT IO [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCEnv [TopLevelModuleName' Range]
-> TCMT IO [TopLevelModuleName' Range]
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC ([TopLevelModuleName' Range] -> f [TopLevelModuleName' Range])
-> TCEnv -> f TCEnv
Lens' TCEnv [TopLevelModuleName' Range]
eImportStack
  traceImports <- optTraceImports <$> commandLineOptions
  let maybeFile = Maybe [Char] -> [Char] -> ShowS -> [Char]
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe [Char]
file [Char]
"." (ShowS -> [Char]) -> ShowS -> [Char]
forall a b. (a -> b) -> a -> b
$ \ [Char]
f -> [Char]
" (" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
f [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
")."
      vLvl | [Char]
kind [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
"Checking"
             Bool -> Bool -> Bool
&& Integer
traceImports Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 = Int
1
           | [Char]
kind [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
"Finished"
             Bool -> Bool -> Bool
&& Integer
traceImports Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
1 = Int
1
           | [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
List.isPrefixOf [Char]
"Loading" [Char]
kind
             Bool -> Bool -> Bool
&& Integer
traceImports Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
2 = Int
1
           | Bool
otherwise = Int
2
  alwaysReportSLn "import.chase" vLvl $ concat
    [ indentation, kind, " ", prettyShow x, maybeFile ]

-- | Print the highlighting information contained in the given interface.

highlightFromInterface
  :: Interface
  -> SourceFile
     -- ^ The corresponding file.
  -> TCM ()
highlightFromInterface :: Interface -> SourceFile -> TCMT IO ()
highlightFromInterface Interface
i SourceFile
sf = do
  [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"import.iface" Int
5 do
    file <- SourceFile -> TCMT IO AbsolutePath
forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
srcFilePath SourceFile
sf
    P.text $ "Generating syntax info for " ++ filePath file ++
      " (read from interface)."
  RemoveTokenBasedHighlighting -> HighlightingInfo -> TCMT IO ()
forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting (Interface -> HighlightingInfo
iHighlighting Interface
i)

-- | Read interface file corresponding to a module.

readInterface :: InterfaceFile -> TCM (Maybe Interface)
readInterface :: InterfaceFile -> TCMT IO (Maybe Interface)
readInterface InterfaceFile
file = do
    let ifp :: [Char]
ifp = AbsolutePath -> [Char]
filePath (AbsolutePath -> [Char]) -> AbsolutePath -> [Char]
forall a b. (a -> b) -> a -> b
$ InterfaceFile -> AbsolutePath
intFilePath InterfaceFile
file
    bstr <- (IO (Maybe ByteString) -> TCMT IO (Maybe ByteString)
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe ByteString) -> TCMT IO (Maybe ByteString))
-> IO (Maybe ByteString) -> TCMT IO (Maybe ByteString)
forall a b. (a -> b) -> a -> b
$ ByteString -> Maybe ByteString
forall a. a -> Maybe a
Just (ByteString -> Maybe ByteString)
-> IO ByteString -> IO (Maybe ByteString)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> [Char] -> IO ByteString
B.readFile [Char]
ifp) TCMT IO (Maybe ByteString)
-> (TCErr -> TCMT IO (Maybe ByteString))
-> TCMT IO (Maybe ByteString)
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
      IOException Maybe TCState
_ Range
_ IOException
e -> do
        [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
alwaysReportSLn [Char]
"" Int
0 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"IO exception: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ IOException -> [Char]
forall a. Show a => a -> [Char]
show IOException
e
        Maybe ByteString -> TCMT IO (Maybe ByteString)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ByteString
forall a. Maybe a
Nothing   -- Work-around for file locking bug.
                         -- TODO: What does this refer to? Please
                         -- document.
      TCErr
e -> TCErr -> TCMT IO (Maybe ByteString)
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
e
    case bstr of
      Just ByteString
bstr -> MaybeT (TCMT IO) Interface -> TCMT IO (Maybe Interface)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (Interface -> Interface
constructIScope (Interface -> Interface)
-> MaybeT (TCMT IO) Interface -> MaybeT (TCMT IO) Interface
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> ByteString -> MaybeT (TCMT IO) Interface
decodeInterface ByteString
bstr)
      Maybe ByteString
Nothing   -> Maybe Interface -> TCMT IO (Maybe Interface)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Interface
forall a. Maybe a
Nothing


-- | Writes the given interface to the given file.
--
-- The written interface is decoded and returned.

writeInterface :: AbsolutePath -> Interface -> TCM Interface
writeInterface :: AbsolutePath -> Interface -> TCMT IO Interface
writeInterface AbsolutePath
file Interface
i = let fp :: [Char]
fp = AbsolutePath -> [Char]
filePath AbsolutePath
file in do
    [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.write" Int
5  ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
      [Char]
"Writing interface file " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
fp [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"."
    let
      keepWarning :: TCWarning' EncodedDiagnostic -> Bool
keepWarning TCWarning{tcWarningRange :: forall diag. TCWarning' diag -> Range
tcWarningRange = Range
r} = case Range
r of
        Range (Strict.Just RangeFile{ rangeFileName :: RangeFile -> Maybe (TopLevelModuleName' Range)
rangeFileName = Just TopLevelModuleName' Range
f }) Seq IntervalWithoutFile'
_ -> TopLevelModuleName' Range
f TopLevelModuleName' Range -> TopLevelModuleName' Range -> Bool
forall a. Eq a => a -> a -> Bool
== Interface -> TopLevelModuleName' Range
iTopLevelModuleName Interface
i
        Range{}   -> Bool
False
        NoRange{} -> Bool
False

      filteredIface :: Interface
filteredIface = Interface
i
        -- Don't write out private entries in the scope tables. Private
        -- declarations will be stripped out by dead-code (if they are
        -- actually dead).
        { iInsideScope = withoutPrivates $ iInsideScope i
        -- Only serialise warnings that actually come from this module.
        -- Warnings raised in the lib file are picked up in the TC state
        -- of the first module that loads it, but they don't correspond
        -- to any TopLevelModuleName.
        -- If we try to write them out we end up with an unserialisable
        -- RangeFile.
        , iWarnings    = Set.filter keepWarning (iWarnings i)
        }
    filteredIface <- Interface -> TCMT IO Interface
pruneTemporaryInstances Interface
filteredIface
    reportSLn "import.iface.write" 50 $
      "Writing interface file with hash " ++ show (iFullHash filteredIface) ++ "."
    iface <- encodeFile fp filteredIface
    reportSLn "import.iface.write" 5 "Wrote interface file."
    pure iface
  TCMT IO Interface
-> (TCErr -> TCMT IO Interface) -> TCMT IO Interface
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
e -> do
    [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
alwaysReportSLn [Char]
"" Int
1 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
      [Char]
"Failed to write interface " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
fp [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"."
    -- Andreas, 2025-09-12, issue #8098, don't delete when writing failed on a readonly file.
    -- Only delete file when disk is full or Agda had an internal error during serialization.
    case TCErr
e of
      IOException Maybe TCState
_ Range
_ IOException
ioe | Bool -> Bool
not (IOException -> Bool
isUserError IOException
ioe), Bool -> Bool
not (IOException -> Bool
isFullError IOException
ioe)
        -> () -> TCMT IO ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      TCErr
_ -> IO () -> TCMT IO ()
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCMT IO ()) -> IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ IO Bool -> IO () -> IO ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ([Char] -> IO Bool
doesFileExist [Char]
fp) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
removeFile [Char]
fp
    TCErr -> TCMT IO Interface
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
e

-- | Tries to type check a module and write out its interface. The
-- function only writes out an interface file if it does not encounter
-- any warnings.
--
-- If appropriate this function writes out syntax highlighting
-- information.

createInterface ::
     TopLevelModuleName    -- ^ The expected module name.
  -> SourceFile            -- ^ The file to type check.
  -> MainInterface         -- ^ Are we dealing with the main module?
  -> Maybe Source          -- ^ Optional information about the source code.
  -> TCM ModuleInfo
createInterface :: TopLevelModuleName' Range
-> SourceFile -> MainInterface -> Maybe Source -> TCM ModuleInfo
createInterface TopLevelModuleName' Range
mname sf :: SourceFile
sf@(SourceFile FileId
sfi) MainInterface
isMain Maybe Source
msrc = do
  file <- SourceFile -> TCMT IO AbsolutePath
forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
srcFilePath SourceFile
sf
  let
    fp = AbsolutePath -> [Char]
filePath AbsolutePath
file
    onlyScope = ModuleCheckMode
ModuleScopeChecked ModuleCheckMode -> ModuleCheckMode -> Bool
forall a. Eq a => a -> a -> Bool
== MainInterface -> ModuleCheckMode
moduleCheckMode MainInterface
isMain
    checkMsg = if Bool
onlyScope then [Char]
"Reading "
                            else [Char]
"Checking"
    withMsgs = TCMT IO ()
-> (() -> TCMT IO ()) -> TCM ModuleInfo -> TCM ModuleInfo
forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ ([Char] -> TopLevelModuleName' Range -> Maybe [Char] -> TCMT IO ()
chaseMsg [Char]
checkMsg TopLevelModuleName' Range
mname (Maybe [Char] -> TCMT IO ()) -> Maybe [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
fp) ((() -> TCMT IO ()) -> TCM ModuleInfo -> TCM ModuleInfo)
-> (() -> TCMT IO ()) -> TCM ModuleInfo -> TCM ModuleInfo
forall a b. (a -> b) -> a -> b
$ TCMT IO () -> () -> TCMT IO ()
forall a b. a -> b -> a
const (TCMT IO () -> () -> TCMT IO ()) -> TCMT IO () -> () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
      ws <- WhichWarnings -> TCMT IO (Set TCWarning)
forall (m :: * -> *).
(MonadWarning m, MonadTCM m) =>
WhichWarnings -> m (Set TCWarning)
getAllWarnings WhichWarnings
AllWarnings
      let classified = Set TCWarning -> WarningsAndNonFatalErrors
classifyWarnings Set TCWarning
ws
      reportWarningsForModule mname $ tcWarnings classified
      when (null (nonFatalErrors classified)) $ chaseMsg "Finished" mname Nothing

  withMsgs $ Bench.billTo [Bench.TopModule mname] $ localTC (set eCurrentPath (Just sfi)) do

    reportSLn "import.iface.create" 5 $
      "Creating interface for " ++ prettyShow mname ++ "..."
    verboseS "import.iface.create" 10 $ do
      visited <- prettyShow <$> getPrettyVisitedModules
      reportSLn "import.iface.create" 10 $ "  visited: " ++ visited

    src <- maybe (parseSource sf) pure msrc

    srcPath <- srcFilePath $ srcOrigin src

    fileTokenInfo <- Bench.billTo [Bench.Highlighting] $
      generateTokenInfoFromSource
        (let !top = Source -> TopLevelModuleName' Range
srcModuleName Source
src in
         mkRangeFile srcPath (Just top))
        (srcText src)
    stTokens `modifyingTC` (fileTokenInfo <>)

    -- Only check consistency if not main (we check consistency for the main module in
    -- `typeCheckMain`.
    let checkConsistency | MainInterface{} <- MainInterface
isMain = Bool
False
                         | Bool
otherwise                 = Bool
True
    setOptionsFromSourcePragmas checkConsistency src

    verboseS "import.iface.create" 15 $ do
      nestingLevel      <- asksTC (pred . length . view eImportStack)
      highlightingLevel <- viewTC eHighlightingLevel
      reportSLn "import.iface.create" 15 $ unlines
        [ "  nesting      level: " ++ show nestingLevel
        , "  highlighting level: " ++ show highlightingLevel
        ]

    -- Scope checking.
    reportSLn "import.iface.create" 7 $ prettyShow mname ++ ": Starting scope checking."
    topLevel <- Bench.billTo [Bench.Scoping] $ do
      let topDecls = Module -> [Declaration]
C.modDecls (Module -> [Declaration]) -> Module -> [Declaration]
forall a b. (a -> b) -> a -> b
$ Source -> Module
srcModule Source
src
      concreteToAbstract_ (TopLevel (srcOrigin src) mname topDecls)
    reportSLn "import.iface.create" 7 $ prettyShow mname ++ ": Finished scope checking."

    let ds    = TopLevelInfo -> [Declaration]
topLevelDecls TopLevelInfo
topLevel
        scope = TopLevelInfo -> ScopeInfo
topLevelScope TopLevelInfo
topLevel

    -- Highlighting from scope checker.
    reportSLn "import.iface.highlight" 15 $ prettyShow mname ++ ": Starting highlighting from scope."
    Bench.billTo [Bench.Highlighting] $ do
      -- Generate and print approximate syntax highlighting info.
      ifTopLevelAndHighlightingLevelIs NonInteractive $
        printHighlightingInfo KeepHighlighting fileTokenInfo
      ifTopLevelAndHighlightingLevelIsOr NonInteractive onlyScope $
        mapM_ (\ Declaration
d -> Declaration -> Level -> Bool -> TCMT IO ()
generateAndPrintSyntaxInfo Declaration
d Level
Partial Bool
onlyScope) ds
    reportSLn "import.iface.highlight" 15 $ prettyShow mname ++ ": Finished highlighting from scope."


    -- Type checking.

    -- Now that all the options are in we can check if caching should
    -- be on.
    activateLoadedFileCache

    -- invalidate cache if pragmas change, TODO move
    cachingStarts
    opts <- useTC stPragmaOptions
    me <- readFromCachedLog
    case me of
      Just (Pragmas PragmaOptions
opts', PostScopeState
_) | PragmaOptions
opts PragmaOptions -> PragmaOptions -> Bool
forall a. Eq a => a -> a -> Bool
== PragmaOptions
opts'
        -> () -> TCMT IO ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Maybe (TypeCheckAction, PostScopeState)
_ -> do
        [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"cache" Int
10 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"pragma changed: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> [Char]
forall a. Show a => a -> [Char]
show (Maybe (TypeCheckAction, PostScopeState) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (TypeCheckAction, PostScopeState)
me)
        TCMT IO ()
forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog
    writeToCurrentLog $ Pragmas opts

    -- copy trimming doesn't currently play nice with caching, since
    -- 'ScopeCopyRef's can be buried deep within an expression (e.g. a
    -- module telescope, see Issue8202).
    -- this call to clobberLiveNames 'knows' about every copy, so it has
    -- the effect of entirely disabling trimming for the top-level
    -- module.
    ifTopLevelAndHighlightingLevelIs None clobberLiveNames

    if onlyScope
      then do
        reportSLn "import.iface.create" 7 $ prettyShow mname ++ ": Skipping type checking."
        cacheCurrentLog
      else do
        reportSLn "import.iface.create" 7 $ prettyShow mname ++ ": Starting type checking."
        Bench.billTo [Bench.Typing] $ mapM_ checkDeclCached ds `finally_` cacheCurrentLog
        reportSLn "import.iface.create" 7 $ prettyShow mname ++ ": Finished type checking."

    -- Ulf, 2013-11-09: Since we're rethrowing the error, leave it up to the
    -- code that handles that error to reset the state.
    -- Ulf, 2013-11-13: Errors are now caught and highlighted in InteractionTop.
    -- catchError_ (checkDecls ds) $ \e -> do
    --   ifTopLevelAndHighlightingLevelIs NonInteractive $
    --     printErrorInfo e
    --   throwError e

    unfreezeMetas

    -- Profiling: Count number of metas.
    whenProfile Profile.Metas $ do
      m <- fresh
      tickN "metas" (metaId m)

    -- Generate unused imports warning.
    warnUnusedImports

    -- Highlighting from type checker.
    reportSLn "import.iface.highlight" 15 $ prettyShow mname ++ ": Starting highlighting from type info."
    Bench.billTo [Bench.Highlighting] $ do

      -- Move any remaining token highlighting to stSyntaxInfo.
      toks <- useTC stTokens
      ifTopLevelAndHighlightingLevelIs NonInteractive $
        printHighlightingInfo KeepHighlighting toks
      stTokens `setTCLens` mempty

      -- Grabbing warnings and unsolved metas to highlight them
      warnings <- getAllWarnings AllWarnings
      unless (null warnings) $ reportSDoc "import.iface.highlight" 20 $
        "collected warnings: " <> prettyTCM warnings
      unsolved <- getAllUnsolvedWarnings
      unless (null unsolved) $ reportSDoc "import.iface.highlight" 20 $
        "collected unsolved: " <> prettyTCM unsolved
      let warningInfo =
            HighlightingInfoBuilder -> HighlightingInfo
forall a b. Convert a b => a -> b
Highlighting.convert (HighlightingInfoBuilder -> HighlightingInfo)
-> HighlightingInfoBuilder -> HighlightingInfo
forall a b. (a -> b) -> a -> b
$ (TCWarning -> HighlightingInfoBuilder)
-> Set TCWarning -> HighlightingInfoBuilder
forall m a. Monoid m => (a -> m) -> Set a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap TCWarning -> HighlightingInfoBuilder
warningHighlighting (Set TCWarning -> HighlightingInfoBuilder)
-> Set TCWarning -> HighlightingInfoBuilder
forall a b. (a -> b) -> a -> b
$ [TCWarning] -> Set TCWarning
forall a. Ord a => [a] -> Set a
Set.fromList [TCWarning]
unsolved Set TCWarning -> Set TCWarning -> Set TCWarning
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set TCWarning
warnings

      stSyntaxInfo `modifyingTC` \HighlightingInfo
inf -> (HighlightingInfo
inf HighlightingInfo -> HighlightingInfo -> HighlightingInfo
forall a. Monoid a => a -> a -> a
`mappend` HighlightingInfo
toks) HighlightingInfo -> HighlightingInfo -> HighlightingInfo
forall a. Monoid a => a -> a -> a
`mappend` HighlightingInfo
warningInfo

      whenM (optGenerateVimFile <$> commandLineOptions) $
        -- Generate Vim file.
        evalWithScope scope $ generateVimFile $ filePath $ srcPath
    reportSLn "import.iface.create" 15 $ prettyShow mname ++ ": Finished highlighting from type info."

    setScope scope
    reportSLn "scope.top" 90 $ "SCOPE " ++ show scope

    -- TODO: It would be nice if unsolved things were highlighted
    -- after every mutual block.

    openMetas <- getOpenMetas
    unless (null openMetas) $ do
      reportSLn "import.metas" 10 $ prettyShow mname ++ ": We have unsolved metas."
      reportSDoc "import.metas" 10 $ prettyGoals =<< getGoals

    ifTopLevelAndHighlightingLevelIs NonInteractive printUnsolvedInfo

    -- Andreas, 2016-08-03, issue #964
    -- When open metas are allowed,
    -- permanently freeze them now by turning them into postulates.
    -- This will enable serialization.
    -- savedMetaStore <- useTC stMetaStore
    unless (includeStateChanges isMain) $
      -- Andreas, 2018-11-15, re issue #3393:
      -- We do not get here when checking the main module
      -- (then includeStateChanges is True).
      whenM (optAllowUnsolved <$> pragmaOptions) $ do
        reportSLn "import.iface.create" 7 $ prettyShow mname ++ ": Turning unsolved metas (if any) into postulates."
        withCurrentModule (scope ^. scopeCurrent) openMetasToPostulates
        -- Clear constraints as they might refer to what
        -- they think are open metas.
        stAwakeConstraints    `setTCLens` []
        stSleepingConstraints `setTCLens` []

    -- Serialization.
    reportSLn "import.iface.create" 7 $ prettyShow mname ++ ": Starting serialization."
    i <- Bench.billTo [Bench.Serialization, Bench.BuildInterface] $
      buildInterface src topLevel

    reportS "tc.top" 101 $
      "Signature:" :
      [ unlines
          [ prettyShow q
          , "  type: " ++ show (defType def)
          , "  def:  " ++ show cc
          ]
      | (q, def) <- HMap.toList $ iSignature i ^. sigDefinitions,
        Function{ funCompiled = cc } <- [theDef def]
      ]
    reportSLn "import.iface.create" 7 $ prettyShow mname ++ ": Finished serialization."

    mallWarnings <- getAllWarnings' isMain ErrorWarnings

    isWritingInterfaces <- writeInterfaces

    reportSLn "import.iface.create" 7 $ prettyShow mname ++ ": Considering writing to interface file."
    finalIface <- constructIScope <$> case (null mallWarnings, isMain, isWritingInterfaces) of
      (Bool
False, MainInterface
_, Bool
_) -> do
        -- Andreas, 2018-11-15, re issue #3393
        -- The following is not sufficient to fix #3393
        -- since the replacement of metas by postulates did not happen.
        -- -- | not (allowUnsolved && all (isUnsolvedWarning . tcWarning) allWarnings) -> do
        [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName' Range -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName' Range
mname [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": We have warnings, skipping writing interface file."
        Interface -> TCMT IO Interface
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Interface
i
      (Bool
True, MainInterface Mode
ScopeCheck , Bool
_) -> do
        [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName' Range -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName' Range
mname [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": We are just scope-checking, skipping writing interface file."
        Interface -> TCMT IO Interface
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Interface
i
      (Bool
_, MainInterface
_, Bool
False) -> do
        [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName' Range -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName' Range
mname [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": We are not writing any interfaces, skipping writing interface file."
        Interface -> TCMT IO Interface
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Interface
i
      (Bool
True, MainInterface
_, Bool
_) -> Account (BenchPhase (TCMT IO))
-> TCMT IO Interface -> TCMT IO Interface
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Serialization] (TCMT IO Interface -> TCMT IO Interface)
-> TCMT IO Interface -> TCMT IO Interface
forall a b. (a -> b) -> a -> b
$ do
        [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName' Range -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName' Range
mname [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": Actually calling writeInterface."
        -- The file was successfully type-checked (and no warnings were
        -- encountered), so the interface should be written out.
        ifile <- HasCallStack => SourceFile -> TCMT IO AbsolutePath
SourceFile -> TCMT IO AbsolutePath
toIFile SourceFile
sf
        serializedIface <- writeInterface ifile i
        reportSLn "import.iface.create" 7 $ prettyShow mname ++ ": Finished writing to interface file."
        pure serializedIface

    -- -- Restore the open metas, as we might continue in interaction mode.
    -- Actually, we do not serialize the metas if checking the MainInterface
    -- stMetaStore `setTCLens` savedMetaStore

    -- Profiling: Print statistics.
    printStatistics (Just mname) =<< getStatistics

    -- Get the statistics of the current module
    -- and add it to the accumulated statistics.
    localStatistics <- getStatistics
    lensAccumStatistics `modifyingTC` (<>) localStatistics
    reportSLn "import.iface" 25 $ prettyShow mname ++ ": Added statistics to the accumulated statistics."

    isPrimitiveMod <- isPrimitiveModule sfi

    return ModuleInfo
      { miInterface = finalIface
      , miWarnings = mallWarnings
      , miPrimitive = isPrimitiveMod
      , miMode = moduleCheckMode isMain
      , miSourceFile = sf
      }

-- | Expert version of 'getAllWarnings'; if 'isMain' is a
-- 'MainInterface', the warnings definitely include also unsolved
-- warnings.

getAllWarnings' :: (MonadWarning m, MonadTCM m) => MainInterface -> WhichWarnings -> m (Set TCWarning)
getAllWarnings' :: forall (m :: * -> *).
(MonadWarning m, MonadTCM m) =>
MainInterface -> WhichWarnings -> m (Set TCWarning)
getAllWarnings' MainInterface{}  = Set WarningName -> WhichWarnings -> m (Set TCWarning)
forall (m :: * -> *).
(MonadWarning m, MonadTCM m) =>
Set WarningName -> WhichWarnings -> m (Set TCWarning)
getAllWarningsPreserving Set WarningName
unsolvedWarnings
getAllWarnings' MainInterface
NotMainInterface = Set WarningName -> WhichWarnings -> m (Set TCWarning)
forall (m :: * -> *).
(MonadWarning m, MonadTCM m) =>
Set WarningName -> WhichWarnings -> m (Set TCWarning)
getAllWarningsPreserving Set WarningName
forall a. Set a
Set.empty

-- Andreas, issue 964: not checking null interactionPoints
-- anymore; we want to serialize with open interaction points now!

-- | Reconstruct the 'iScope' (not serialized)
--   from the 'iInsideScope' (serialized).

constructIScope :: Interface -> Interface
constructIScope :: Interface -> Interface
constructIScope Interface
i = [Phase] -> Interface -> Interface
forall a. [Phase] -> a -> a
billToPure [ Phase
Deserialization ] (Interface -> Interface) -> Interface -> Interface
forall a b. (a -> b) -> a -> b
$
  Interface
i{ iScope = publicModules $ iInsideScope i }

isSourceCodeWarning :: TCWarning -> Bool
isSourceCodeWarning :: TCWarning -> Bool
isSourceCodeWarning TCWarning
w = case SomeDiagnostic -> DiagnosticReason
forall a. Diagnostic a => a -> DiagnosticReason
diagnosticReason (TCWarning -> SomeDiagnostic
forall diag. TCWarning' diag -> diag
tcWarning TCWarning
w) of
  DiagWarning { _warningName :: DiagnosticReason -> WarningName
_warningName = WarningName
WarningProblem_ } -> Bool
False
  DiagnosticReason
_ -> Bool
True

-- | Builds an interface for the current module, which should already
--   have been successfully type checked.
buildInterface
  :: Source
     -- ^ 'Source' for the current module.
  -> TopLevelInfo
     -- ^ 'TopLevelInfo' scope information for the current module.
  -> TCM Interface
buildInterface :: Source -> TopLevelInfo -> TCMT IO Interface
buildInterface Source
src TopLevelInfo
topLevel = do
    [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
5 [Char]
"Building interface..."
    let mname :: ModuleName
mname = TopLevelInfo -> ModuleName
CToA.topLevelModuleName TopLevelInfo
topLevel
        source :: Text
source   = Source -> Text
srcText Source
src
        fileType :: FileType
fileType = Source -> FileType
srcFileType Source
src
        defPragmas :: [OptionsPragma]
defPragmas = Source -> [OptionsPragma]
srcDefaultPragmas Source
src
        filePragmas :: [OptionsPragma]
filePragmas  = Source -> [OptionsPragma]
srcFilePragmas Source
src

    -- Andreas, 2014-05-03: killRange did not result in significant reduction
    -- of .agdai file size, and lost a few seconds performance on library-test.
    -- Andreas, Makoto, 2014-10-18 AIM XX: repeating the experiment
    -- with discarding also the nameBindingSite in QName:
    -- Saves 10% on serialization time (and file size)!
    --
    -- NOTE: We no longer discard all nameBindingSites (but the commit
    -- that introduced this change seems to have made Agda a bit
    -- faster and interface file sizes a bit smaller, at least for the
    -- standard library).
    !mhs <- (TopLevelModuleName' Range
 -> TCMT IO (TopLevelModuleName' Range, Hash))
-> [TopLevelModuleName' Range]
-> TCMT IO [(TopLevelModuleName' Range, Hash)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\TopLevelModuleName' Range
top -> (TopLevelModuleName' Range
top,) (Hash -> (TopLevelModuleName' Range, Hash))
-> TCMT IO Hash -> TCMT IO (TopLevelModuleName' Range, Hash)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TopLevelModuleName' Range -> TCMT IO Hash
moduleHash TopLevelModuleName' Range
top) ([TopLevelModuleName' Range]
 -> TCMT IO [(TopLevelModuleName' Range, Hash)])
-> (Set (TopLevelModuleName' Range) -> [TopLevelModuleName' Range])
-> Set (TopLevelModuleName' Range)
-> TCMT IO [(TopLevelModuleName' Range, Hash)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (TopLevelModuleName' Range) -> [TopLevelModuleName' Range]
forall a. Set a -> [a]
Set.toAscList (Set (TopLevelModuleName' Range)
 -> TCMT IO [(TopLevelModuleName' Range, Hash)])
-> TCMT IO (Set (TopLevelModuleName' Range))
-> TCMT IO [(TopLevelModuleName' Range, Hash)]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Lens' TCState (Set (TopLevelModuleName' Range))
-> TCMT IO (Set (TopLevelModuleName' Range))
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Set (TopLevelModuleName' Range)
 -> f (Set (TopLevelModuleName' Range)))
-> TCState -> f TCState
Lens' TCState (Set (TopLevelModuleName' Range))
stImportedModules
    !foreignCode <- useTC stForeignCode

    let !scope = TopLevelInfo -> ScopeInfo
topLevelScope TopLevelInfo
topLevel

    (!solvedMetas, !definitions, !displayForms) <- eliminateDeadCode scope
    !sig <- set sigDefinitions definitions <$> getSignature

    -- Andreas, 2015-02-09 kill ranges in pattern synonyms before
    -- serialization to avoid error locations pointing to external files
    -- when expanding a pattern synonym.
    !patsyns <- killRange <$> getPatternSyns

    !userwarns   <- useTC stLocalUserWarnings
    !importwarn  <- useTC stWarningOnImport
    !syntaxInfo  <- useTC stSyntaxInfo
    !optionsUsed <- useTC stPragmaOptions
    !partialDefs <- useTC stLocalPartialDefs

    -- Only serialise the opaque blocks actually defined in this
    -- top-level module.
    !opaqueBlocks' <- useTC stOpaqueBlocks
    !opaqueIds' <- useTC stOpaqueIds
    let
      !mh = TopLevelModuleName' Range -> ModuleNameHash
forall range. TopLevelModuleName' range -> ModuleNameHash
moduleNameId (Source -> TopLevelModuleName' Range
srcModuleName Source
src)
      !opaqueBlocks = (OpaqueId -> OpaqueBlock -> Bool)
-> Map OpaqueId OpaqueBlock -> Map OpaqueId OpaqueBlock
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\(OpaqueId Hash
_ ModuleNameHash
mod) OpaqueBlock
_ -> ModuleNameHash
mod ModuleNameHash -> ModuleNameHash -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleNameHash
mh) Map OpaqueId OpaqueBlock
opaqueBlocks'
      isLocal QName
qnm = case QName -> NameId
forall a. HasNameId a => a -> NameId
nameId QName
qnm of
        NameId Hash
_ ModuleNameHash
mh' -> ModuleNameHash
mh' ModuleNameHash -> ModuleNameHash -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleNameHash
mh
      !opaqueIds = (QName -> OpaqueId -> Bool)
-> Map QName OpaqueId -> Map QName OpaqueId
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\QName
qnm (OpaqueId Hash
_ ModuleNameHash
mod) -> QName -> Bool
isLocal QName
qnm Bool -> Bool -> Bool
|| ModuleNameHash
mod ModuleNameHash -> ModuleNameHash -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleNameHash
mh) Map QName OpaqueId
opaqueIds'

    !builtin  <- Map.mapWithKey (\ SomeBuiltin
x Builtin PrimFun
b -> SomeBuiltin -> PrimFun -> (PrimitiveId, QName)
primName SomeBuiltin
x (PrimFun -> (PrimitiveId, QName))
-> Builtin PrimFun -> Builtin (PrimitiveId, QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Builtin PrimFun
b) <$> useTC stLocalBuiltins
    !warnings <- Set.filter isSourceCodeWarning <$> getAllWarnings AllWarnings

    let !i = Interface
          { iSourceHash :: Hash
iSourceHash           = Text -> Hash
hashText Text
source
          , iSource :: Text
iSource               = Text
source
          , iFileType :: FileType
iFileType             = FileType
fileType
          , iImportedModules :: [(TopLevelModuleName' Range, Hash)]
iImportedModules      = [(TopLevelModuleName' Range, Hash)]
mhs
          , iModuleName :: ModuleName
iModuleName           = ModuleName
mname
          , iTopLevelModuleName :: TopLevelModuleName' Range
iTopLevelModuleName   = Source -> TopLevelModuleName' Range
srcModuleName Source
src
          , iScope :: Map ModuleName Scope
iScope                = Map ModuleName Scope
forall a. Null a => a
empty -- publicModules scope
          , iInsideScope :: ScopeInfo
iInsideScope          = ScopeInfo
scope
          , iSignature :: Signature
iSignature            = Signature
sig
          , iMetaBindings :: RemoteMetaStore
iMetaBindings         = RemoteMetaStore
solvedMetas
          , iDisplayForms :: DisplayForms
iDisplayForms         = DisplayForms
displayForms
          , iUserWarnings :: UserWarnings
iUserWarnings         = UserWarnings
userwarns
          , iImportWarning :: Maybe ShortText
iImportWarning        = Maybe ShortText
importwarn
          , iBuiltin :: Map SomeBuiltin (Builtin (PrimitiveId, QName))
iBuiltin              = Map SomeBuiltin (Builtin (PrimitiveId, QName))
builtin
          , iForeignCode :: Map ShortText ForeignCodeStack
iForeignCode          = Map ShortText ForeignCodeStack
foreignCode
          , iHighlighting :: HighlightingInfo
iHighlighting         = HighlightingInfo
syntaxInfo
          , iDefaultPragmaOptions :: [OptionsPragma]
iDefaultPragmaOptions = [OptionsPragma]
defPragmas
          , iFilePragmaOptions :: [OptionsPragma]
iFilePragmaOptions    = [OptionsPragma]
filePragmas
          , iOptionsUsed :: PragmaOptions
iOptionsUsed          = PragmaOptions
optionsUsed
          , iPatternSyns :: PatternSynDefns
iPatternSyns          = PatternSynDefns
patsyns
          , iWarnings :: Set (TCWarning' EncodedDiagnostic)
iWarnings             = (TCWarning -> TCWarning' EncodedDiagnostic)
-> Set TCWarning -> Set (TCWarning' EncodedDiagnostic)
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (EncodedDiagnostic -> Maybe EncodedDiagnostic -> EncodedDiagnostic
forall a. a -> Maybe a -> a
fromMaybe EncodedDiagnostic
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe EncodedDiagnostic -> EncodedDiagnostic)
-> (SomeDiagnostic -> Maybe EncodedDiagnostic)
-> SomeDiagnostic
-> EncodedDiagnostic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeDiagnostic -> Maybe EncodedDiagnostic
forall a. Diagnostic a => SomeDiagnostic -> Maybe a
fromSomeDiagnostic (SomeDiagnostic -> EncodedDiagnostic)
-> TCWarning -> TCWarning' EncodedDiagnostic
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) Set TCWarning
warnings
          , iPartialDefs :: Set QName
iPartialDefs          = Set QName
partialDefs
          , iOpaqueBlocks :: Map OpaqueId OpaqueBlock
iOpaqueBlocks         = Map OpaqueId OpaqueBlock
opaqueBlocks
          , iOpaqueNames :: Map QName OpaqueId
iOpaqueNames          = Map QName OpaqueId
opaqueIds
          }
    !i <-
      ifM (optSaveMetas <$> pragmaOptions)
        (return i)
        (do reportSLn "import.iface" 7
              "  instantiating all metavariables in interface"
            Bench.billTo [Bench.InterfaceInstantiateFull] $ liftReduce $ instantiateFull' i)
    reportSLn "import.iface" 7 "  interface complete"
    return i

    where
      primName :: SomeBuiltin -> PrimFun -> (PrimitiveId, QName)
primName (PrimitiveName PrimitiveId
x) PrimFun
b = (PrimitiveId
x, PrimFun -> QName
primFunName PrimFun
b)
      primName (BuiltinName BuiltinId
x)   PrimFun
b = (PrimitiveId, QName)
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Returns (iSourceHash, iFullHash)
--   We do not need to check that the file exist because we only
--   accept @InterfaceFile@ as an input and not arbitrary @AbsolutePath@!
getInterfaceFileHashes :: InterfaceFile -> IO (Maybe (Hash, Hash))
getInterfaceFileHashes :: InterfaceFile -> IO (Maybe (Hash, Hash))
getInterfaceFileHashes InterfaceFile
fp = do
  let ifile :: [Char]
ifile = AbsolutePath -> [Char]
filePath (AbsolutePath -> [Char]) -> AbsolutePath -> [Char]
forall a b. (a -> b) -> a -> b
$ InterfaceFile -> AbsolutePath
intFilePath InterfaceFile
fp
  h    <- [Char] -> IOMode -> IO Handle
openBinaryFile [Char]
ifile IOMode
ReadMode
  bstr <- B.hGetSome h (2 * hashSize)
  hClose h
  deserializeHashes bstr

moduleHash :: TopLevelModuleName -> TCM Hash
moduleHash :: TopLevelModuleName' Range -> TCMT IO Hash
moduleHash TopLevelModuleName' Range
m = Interface -> Hash
iFullHash (Interface -> Hash) -> TCMT IO Interface -> TCMT IO Hash
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TopLevelModuleName' Range -> Maybe Source -> TCMT IO Interface
getNonMainInterface TopLevelModuleName' Range
m Maybe Source
forall a. Maybe a
Nothing