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

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

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

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

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

import Prelude hiding (null)

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 qualified Control.Exception as E

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

import System.Directory (doesFileExist, removeFile)
import System.FilePath  ( (</>) )

import Agda.Benchmarking

import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Concrete.Attribute
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common
import Agda.Syntax.Common.Pretty hiding (Mode)
import Agda.Syntax.Parser
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.Syntax.TopLevelModuleName
import Agda.Syntax.Translation.ConcreteToAbstract
  ( TopLevel( TopLevel )
  , TopLevelInfo( TopLevelInfo, topLevelDecls, topLevelScope)
  , checkAttributes, concreteToAbstract_
  )
import qualified Agda.Syntax.Translation.ConcreteToAbstract as CToA

import Agda.TypeChecking.InstanceArguments
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Warnings hiding (warnings)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Rewriting.Confluence ( checkConfluenceOfRules, sortRulesOfSymbol )
import Agda.TypeChecking.MetaVars ( openMetasToPostulates )
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Serialise
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Pretty as P
import Agda.TypeChecking.DeadCode
import qualified Agda.TypeChecking.Monad.Benchmark as Bench

import Agda.TheTypeChecker

import Agda.Interaction.BasicOps ( getGoals, showGoals )
import Agda.Interaction.FindFile
import Agda.Interaction.Highlighting.Generate
import qualified Agda.Interaction.Highlighting.Precise as Highlighting ( convert )
import Agda.Interaction.Highlighting.Vim
import Agda.Interaction.Library
import Agda.Interaction.Options
import qualified Agda.Interaction.Options.Lenses as Lens
import Agda.Interaction.Options.Warnings (unsolvedWarnings)
import Agda.Interaction.Response
  (RemoveTokenBasedHighlighting(KeepHighlighting))

import Agda.Utils.CallStack (HasCallStack)
import Agda.Utils.FileName
import Agda.Utils.Hash
import Agda.Utils.IO.Binary
import Agda.Utils.Lens
import Agda.Utils.List ( nubOn )
import Agda.Utils.Maybe
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Null
import qualified Agda.Utils.ProfileOptions as Profile
import Agda.Utils.Singleton
import qualified Agda.Utils.Set1 as Set1
import qualified Agda.Utils.Trie as Trie

import Agda.Utils.Impossible

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

-- | The decorated source code.

data Source = Source
  { Source -> Text
srcText        :: TL.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
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.)

  AbsolutePath
f <- SourceFile -> TCMT IO AbsolutePath
forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
srcFilePath SourceFile
sourceFile

  -- Read the source text.
  let rf0 :: RangeFile
rf0 = AbsolutePath -> Maybe TopLevelModuleName -> RangeFile
mkRangeFile AbsolutePath
f Maybe TopLevelModuleName
forall a. Maybe a
Nothing
  Range -> TCM Source -> TCM Source
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (RangeFile -> Range
forall a. BeginningOfFile a => a -> Range
beginningOfFile RangeFile
rf0) do

  Text
source <- PM Text -> TCM Text
forall a. PM a -> TCM a
runPM (PM Text -> TCM Text) -> PM Text -> TCM Text
forall a b. (a -> b) -> a -> b
$ RangeFile -> PM Text
readFilePM RangeFile
rf0
  let txt :: [Char]
txt = Text -> [Char]
TL.unpack Text
source

  -- Bootstrapping: parse the module name.
  TopLevelModuleName
parsedModName0 <- AbsolutePath -> Module -> TCM TopLevelModuleName
moduleName AbsolutePath
f (Module -> TCM TopLevelModuleName)
-> (((Module, Attributes), FileType) -> Module)
-> ((Module, Attributes), FileType)
-> TCM TopLevelModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Module, Attributes) -> Module
forall a b. (a, b) -> a
fst ((Module, Attributes) -> Module)
-> (((Module, Attributes), FileType) -> (Module, Attributes))
-> ((Module, Attributes), FileType)
-> Module
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Module, Attributes), FileType) -> (Module, Attributes)
forall a b. (a, b) -> a
fst (((Module, Attributes), FileType) -> TCM TopLevelModuleName)
-> TCMT IO ((Module, Attributes), FileType)
-> TCM TopLevelModuleName
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
    PM ((Module, Attributes), FileType)
-> TCMT IO ((Module, Attributes), FileType)
forall a. PM a -> TCM a
runPMDropWarnings (PM ((Module, Attributes), FileType)
 -> TCMT IO ((Module, Attributes), FileType))
-> PM ((Module, Attributes), FileType)
-> TCMT IO ((Module, Attributes), FileType)
forall a b. (a -> b) -> a -> b
$ Parser Module
-> RangeFile -> [Char] -> PM ((Module, Attributes), FileType)
forall a.
Show a =>
Parser a -> RangeFile -> [Char] -> PM ((a, Attributes), FileType)
parseFile Parser Module
moduleParser RangeFile
rf0 [Char]
txt

  -- Now parse again, with module name present to be filled into the ranges.
  let rf :: RangeFile
rf = AbsolutePath -> Maybe TopLevelModuleName -> RangeFile
mkRangeFile AbsolutePath
f (Maybe TopLevelModuleName -> RangeFile)
-> Maybe TopLevelModuleName -> RangeFile
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> Maybe TopLevelModuleName
forall a. a -> Maybe a
Just TopLevelModuleName
parsedModName0
  ((Module
parsedMod, Attributes
attrs), FileType
fileType) <- PM ((Module, Attributes), FileType)
-> TCMT IO ((Module, Attributes), FileType)
forall a. PM a -> TCM a
runPM (PM ((Module, Attributes), FileType)
 -> TCMT IO ((Module, Attributes), FileType))
-> PM ((Module, Attributes), FileType)
-> TCMT IO ((Module, Attributes), FileType)
forall a b. (a -> b) -> a -> b
$ Parser Module
-> RangeFile -> [Char] -> PM ((Module, Attributes), FileType)
forall a.
Show a =>
Parser a -> RangeFile -> [Char] -> PM ((a, Attributes), FileType)
parseFile Parser Module
moduleParser RangeFile
rf [Char]
txt
  TopLevelModuleName
parsedModName                  <- AbsolutePath -> Module -> TCM TopLevelModuleName
moduleName AbsolutePath
f Module
parsedMod

  [AgdaLibFile]
libs <- AbsolutePath -> TopLevelModuleName -> TCM [AgdaLibFile]
getAgdaLibFiles AbsolutePath
f TopLevelModuleName
parsedModName
  Source -> TCM Source
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Source
    { srcText :: Text
srcText        = Text
source
    , srcFileType :: FileType
srcFileType    = FileType
fileType
    , srcOrigin :: SourceFile
srcOrigin      = SourceFile
sourceFile
    , srcModule :: Module
srcModule      = Module
parsedMod
    , srcModuleName :: TopLevelModuleName
srcModuleName  = TopLevelModuleName
parsedModName
    , srcProjectLibs :: [AgdaLibFile]
srcProjectLibs = [AgdaLibFile]
libs
    , srcAttributes :: Attributes
srcAttributes  = Attributes
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
moduleName AbsolutePath
file Module
parsedModule = Account (BenchPhase (TCMT IO))
-> TCM TopLevelModuleName -> TCM TopLevelModuleName
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.ModuleName] (TCM TopLevelModuleName -> TCM TopLevelModuleName)
-> TCM TopLevelModuleName -> TCM TopLevelModuleName
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
topLevelModuleName (RawTopLevelModuleName -> TCM TopLevelModuleName)
-> TCMT IO RawTopLevelModuleName -> TCM TopLevelModuleName
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
      QName
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 -> [Char] -> PM (QName, Attributes)
forall a. Parser a -> [Char] -> PM (a, Attributes)
parse Parser QName
moduleNameParser [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 :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> 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 QName
m of
        C.Qual{} ->
          TypeError -> TCMT IO RawTopLevelModuleName
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> 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 = Text -> TopLevelModuleNameParts
forall el coll. Singleton el coll => el -> coll
singleton ([Char] -> Text
T.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 = [[Char]]
opts
                , pragmaRange :: Range
pragmaRange   = Range
r
                }
            | C.OptionsPragma Range
r [[Char]]
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 -> TCM ()
setOptionsFromSourcePragmas Bool
checkOpts Source
src = do
  (OptionsPragma -> TCM ()) -> [OptionsPragma] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ OptionsPragma -> TCM ()
setOpts (Source -> [OptionsPragma]
srcDefaultPragmas Source
src)
  (OptionsPragma -> TCM ()) -> [OptionsPragma] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ OptionsPragma -> TCM ()
setOpts (Source -> [OptionsPragma]
srcFilePragmas    Source
src)
  where
    setOpts :: OptionsPragma -> TCM ()
setOpts | Bool
checkOpts = OptionsPragma -> TCM ()
checkAndSetOptionsFromPragma
            | Bool
otherwise = OptionsPragma -> TCM ()
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 -> TCM ()
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)
          (a
x, BuiltinRewriteRelations Set QName
xs) -> (a, Builtin pf) -> Either a (a, Builtin pf)
forall a b. b -> Either a b
Right (a
x, Set QName -> Builtin pf
forall pf. Set QName -> Builtin pf
BuiltinRewriteRelations Set QName
xs)
        ([(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 :: Map SomeBuiltin (Builtin PrimFun)
bi      = [(SomeBuiltin, Builtin PrimFun)]
-> Map SomeBuiltin (Builtin PrimFun)
forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList [(SomeBuiltin, Builtin PrimFun)]
bi'
        warns :: Set TCWarning
warns   = Interface -> Set TCWarning
iWarnings Interface
i
    Map SomeBuiltin (Builtin PrimFun)
bs <- (TCState -> Map SomeBuiltin (Builtin PrimFun))
-> TCMT IO (Map SomeBuiltin (Builtin PrimFun))
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC TCState -> Map SomeBuiltin (Builtin PrimFun)
stBuiltinThings
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.merge" Int
10 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Merging interface " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (Interface -> TopLevelModuleName
iTopLevelModuleName Interface
i)
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.merge" Int
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$
      [Char]
"  Current builtins " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [SomeBuiltin] -> [Char]
forall a. Show a => a -> [Char]
show (Map SomeBuiltin (Builtin PrimFun) -> [SomeBuiltin]
forall k a. Map k a -> [k]
Map.keys Map SomeBuiltin (Builtin PrimFun)
bs) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++
      [Char]
"  New builtins     " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [SomeBuiltin] -> [Char]
forall a. Show a => a -> [Char]
show (Map SomeBuiltin (Builtin PrimFun) -> [SomeBuiltin]
forall k a. Map k a -> [k]
Map.keys Map SomeBuiltin (Builtin PrimFun)
bi)
    let check :: SomeBuiltin -> Builtin pf -> Builtin pf -> m ()
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 :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> 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
_ (BuiltinRewriteRelations Set QName
xs) (BuiltinRewriteRelations Set QName
ys) = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        check SomeBuiltin
_ Builtin pf
_ Builtin pf
_ = m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
    Map SomeBuiltin (TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ (Map SomeBuiltin (TCM ()) -> TCM ())
-> Map SomeBuiltin (TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ (SomeBuiltin -> Builtin PrimFun -> Builtin PrimFun -> TCM ())
-> Map SomeBuiltin (Builtin PrimFun)
-> Map SomeBuiltin (Builtin PrimFun)
-> Map SomeBuiltin (TCM ())
forall k a b c.
Ord k =>
(k -> a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWithKey SomeBuiltin -> Builtin PrimFun -> Builtin PrimFun -> TCM ()
forall {m :: * -> *} {pf} {pf}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
SomeBuiltin -> Builtin pf -> Builtin pf -> m ()
check Map SomeBuiltin (Builtin PrimFun)
bs Map SomeBuiltin (Builtin PrimFun)
bi
    Signature
-> RemoteMetaStore
-> Map SomeBuiltin (Builtin PrimFun)
-> PatternSynDefns
-> DisplayForms
-> UserWarnings
-> Set QName
-> Set TCWarning
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> TCM ()
addImportedThings
      Signature
sig
      (Interface -> RemoteMetaStore
iMetaBindings Interface
i)
      Map SomeBuiltin (Builtin PrimFun)
bi
      (Interface -> PatternSynDefns
iPatternSyns Interface
i)
      (Interface -> DisplayForms
iDisplayForms Interface
i)
      (Interface -> UserWarnings
iUserWarnings Interface
i)
      (Interface -> Set QName
iPartialDefs Interface
i)
      Set TCWarning
warns
      (Interface -> Map OpaqueId OpaqueBlock
iOpaqueBlocks Interface
i)
      (Interface -> Map QName OpaqueId
iOpaqueNames Interface
i)
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.merge" Int
50 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$
      [Char]
"  Rebinding primitives " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [(PrimitiveId, QName)] -> [Char]
forall a. Show a => a -> [Char]
show [(PrimitiveId, QName)]
prim
    ((PrimitiveId, QName) -> TCM ())
-> [(PrimitiveId, QName)] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (PrimitiveId, QName) -> TCM ()
rebind [(PrimitiveId, QName)]
prim
    TCMT IO (Maybe ConfluenceCheck)
-> (ConfluenceCheck -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (PragmaOptions -> Maybe ConfluenceCheck
optConfluenceCheck (PragmaOptions -> Maybe ConfluenceCheck)
-> TCMT IO PragmaOptions -> TCMT IO (Maybe ConfluenceCheck)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) \ ConfluenceCheck
confChk -> do
      let rews :: [RewriteRule]
rews = [[RewriteRule]] -> [RewriteRule]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[RewriteRule]] -> [RewriteRule])
-> [[RewriteRule]] -> [RewriteRule]
forall a b. (a -> b) -> a -> b
$ HashMap QName [RewriteRule] -> [[RewriteRule]]
forall k v. HashMap k v -> [v]
HMap.elems (HashMap QName [RewriteRule] -> [[RewriteRule]])
-> HashMap QName [RewriteRule] -> [[RewriteRule]]
forall a b. (a -> b) -> a -> b
$ Signature
sig Signature
-> Lens' Signature (HashMap QName [RewriteRule])
-> HashMap QName [RewriteRule]
forall o i. o -> Lens' o i -> i
^. (HashMap QName [RewriteRule] -> f (HashMap QName [RewriteRule]))
-> Signature -> f Signature
Lens' Signature (HashMap QName [RewriteRule])
sigRewriteRules
      [Char] -> Int -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"import.iface.confluence" Int
20 do
        if [RewriteRule] -> Bool
forall a. Null a => a -> Bool
null [RewriteRule]
rews then [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"" Int
1 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  No rewrite rules imported"
        else do
          [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"" Int
1 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
P.vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (TCMT IO Doc -> TCMT IO Doc) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (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
"Checking confluence of imported rewrite rules" TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
:
            (RewriteRule -> TCMT IO Doc) -> [RewriteRule] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((TCMT IO Doc
"-" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+>) (TCMT IO Doc -> TCMT IO Doc)
-> (RewriteRule -> TCMT IO Doc) -> RewriteRule -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (QName -> TCMT IO Doc)
-> (RewriteRule -> QName) -> RewriteRule -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteRule -> QName
rewName) [RewriteRule]
rews

      -- Andreas, 2025-06-28, PR #7934 and issue #7969:
      -- Global confluence checker requires rules to be sorted
      -- according to the generality of their lhs
      Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when (ConfluenceCheck
confChk ConfluenceCheck -> ConfluenceCheck -> Bool
forall a. Eq a => a -> a -> Bool
== ConfluenceCheck
GlobalConfluenceCheck) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        [QName] -> (QName -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ((QName -> QName) -> [QName] -> [QName]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn QName -> QName
forall a. a -> a
id ([QName] -> [QName]) -> [QName] -> [QName]
forall a b. (a -> b) -> a -> b
$ (RewriteRule -> QName) -> [RewriteRule] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map RewriteRule -> QName
rewHead [RewriteRule]
rews) QName -> TCM ()
sortRulesOfSymbol
      ConfluenceCheck -> [RewriteRule] -> TCM ()
checkConfluenceOfRules ConfluenceCheck
confChk [RewriteRule]
rews
    where
        rebind :: (PrimitiveId, QName) -> TCM ()
rebind (PrimitiveId
x, QName
q) = do
            PrimImpl Type
_ PrimFun
pf <- PrimitiveId -> TCM PrimitiveImpl
lookupPrimitiveFunction PrimitiveId
x
            (Map SomeBuiltin (Builtin PrimFun)
 -> f (Map SomeBuiltin (Builtin PrimFun)))
-> TCState -> f TCState
Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
stImportedBuiltins Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
-> (Map SomeBuiltin (Builtin PrimFun)
    -> Map SomeBuiltin (Builtin PrimFun))
-> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` SomeBuiltin
-> Builtin PrimFun
-> Map SomeBuiltin (Builtin PrimFun)
-> Map SomeBuiltin (Builtin PrimFun)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
x) (PrimFun -> Builtin PrimFun
forall pf. pf -> Builtin pf
Prim PrimFun
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
-> Map SomeBuiltin (Builtin PrimFun)
-> PatternSynDefns
-> DisplayForms
-> UserWarnings
-> Set QName
-> Set TCWarning
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> TCM ()
addImportedThings Signature
isig RemoteMetaStore
metas Map SomeBuiltin (Builtin PrimFun)
ibuiltin PatternSynDefns
patsyns DisplayForms
display UserWarnings
userwarn
                  Set QName
partialdefs Set TCWarning
warnings Map OpaqueId OpaqueBlock
oblock Map QName OpaqueId
oid = do
  (Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stImports              Lens' TCState Signature -> (Signature -> Signature) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` \ Signature
imp -> Signature -> Signature -> Signature
unionSignature Signature
imp Signature
isig
  (RemoteMetaStore -> f RemoteMetaStore) -> TCState -> f TCState
Lens' TCState RemoteMetaStore
stImportedMetaStore    Lens' TCState RemoteMetaStore
-> (RemoteMetaStore -> RemoteMetaStore) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` RemoteMetaStore -> RemoteMetaStore -> RemoteMetaStore
forall k v. Eq k => HashMap k v -> HashMap k v -> HashMap k v
HMap.union RemoteMetaStore
metas
  (Map SomeBuiltin (Builtin PrimFun)
 -> f (Map SomeBuiltin (Builtin PrimFun)))
-> TCState -> f TCState
Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
stImportedBuiltins     Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
-> (Map SomeBuiltin (Builtin PrimFun)
    -> Map SomeBuiltin (Builtin PrimFun))
-> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` \ Map SomeBuiltin (Builtin PrimFun)
imp -> Map SomeBuiltin (Builtin PrimFun)
-> Map SomeBuiltin (Builtin PrimFun)
-> Map SomeBuiltin (Builtin PrimFun)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map SomeBuiltin (Builtin PrimFun)
imp Map SomeBuiltin (Builtin PrimFun)
ibuiltin
  (UserWarnings -> f UserWarnings) -> TCState -> f TCState
Lens' TCState UserWarnings
stImportedUserWarnings Lens' TCState UserWarnings
-> (UserWarnings -> UserWarnings) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` \ 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 -> f (Set QName)) -> TCState -> f TCState
Lens' TCState (Set QName)
stImportedPartialDefs  Lens' TCState (Set QName) -> (Set QName -> Set QName) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` \ 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 -> f PatternSynDefns) -> TCState -> f TCState
Lens' TCState PatternSynDefns
stPatternSynImports    Lens' TCState PatternSynDefns
-> (PatternSynDefns -> PatternSynDefns) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` \ 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 -> f DisplayForms) -> TCState -> f TCState
Lens' TCState DisplayForms
stImportedDisplayForms Lens' TCState DisplayForms
-> (DisplayForms -> DisplayForms) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` \ DisplayForms
imp -> ([LocalDisplayForm] -> [LocalDisplayForm] -> [LocalDisplayForm])
-> DisplayForms -> DisplayForms -> DisplayForms
forall k v.
Eq k =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HMap.unionWith [LocalDisplayForm] -> [LocalDisplayForm] -> [LocalDisplayForm]
forall a. [a] -> [a] -> [a]
(++) DisplayForms
imp DisplayForms
display
  (Set TCWarning -> f (Set TCWarning)) -> TCState -> f TCState
Lens' TCState (Set TCWarning)
stTCWarnings           Lens' TCState (Set TCWarning)
-> (Set TCWarning -> Set TCWarning) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` \ 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 -> f (Map OpaqueId OpaqueBlock))
-> TCState -> f TCState
Lens' TCState (Map OpaqueId OpaqueBlock)
stOpaqueBlocks         Lens' TCState (Map OpaqueId OpaqueBlock)
-> (Map OpaqueId OpaqueBlock -> Map OpaqueId OpaqueBlock) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` \ 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 -> f (Map QName OpaqueId))
-> TCState -> f TCState
Lens' TCState (Map QName OpaqueId)
stOpaqueIds            Lens' TCState (Map QName OpaqueId)
-> (Map QName OpaqueId -> Map QName OpaqueId) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` \ 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

-- | Scope checks the given module, generating an interface or retrieving an existing one.
--   Returns the module name and exported scope from the interface.
--
scopeCheckImport ::
     TopLevelModuleName
  -> TCM (ModuleName, Map ModuleName Scope)
scopeCheckImport :: TopLevelModuleName -> TCM (ModuleName, Map ModuleName Scope)
scopeCheckImport TopLevelModuleName
top = do
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.scope" Int
15 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Scope checking " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
top
    [Char] -> Int -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"import.scope" Int
30 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      [Char]
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
      [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.scope" Int
30 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  visited: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
visited
    -- Since scopeCheckImport is called from the scope checker,
    -- we need to reimburse her account.
    Interface
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 -> Maybe Source -> TCMT IO Interface
getNonMainInterface TopLevelModuleName
top Maybe Source
forall a. Maybe a
Nothing
    TopLevelModuleName -> TCM ()
addImport TopLevelModuleName
top

    -- Print list of imported modules in current state.
    [Char] -> Int -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"import.iface.imports" Int
10 do
      [TopLevelModuleName]
imports <- Set TopLevelModuleName -> [TopLevelModuleName]
forall a. Set a -> [a]
Set.toList (Set TopLevelModuleName -> [TopLevelModuleName])
-> TCMT IO (Set TopLevelModuleName) -> TCMT IO [TopLevelModuleName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState (Set TopLevelModuleName)
-> TCMT IO (Set TopLevelModuleName)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Set TopLevelModuleName -> f (Set TopLevelModuleName))
-> TCState -> f TCState
Lens' TCState (Set TopLevelModuleName)
stImportedModules
      [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.imports" Int
10 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
        [[Char]] -> [Char]
unwords [TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
top, [Char]
"added, all imports:"] [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
:
        (TopLevelModuleName -> [Char]) -> [TopLevelModuleName] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (\ TopLevelModuleName
x -> [[Char]] -> [Char]
unwords [ [Char]
" ", [Char]
"-", TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
x ]) [TopLevelModuleName]
imports

    -- Print list of transitively imported modules in current state.
    [Char] -> Int -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"import.iface.imports" Int
20 do
      [TopLevelModuleName]
imports <- Set TopLevelModuleName -> [TopLevelModuleName]
forall a. Set a -> [a]
Set.toList (Set TopLevelModuleName -> [TopLevelModuleName])
-> TCMT IO (Set TopLevelModuleName) -> TCMT IO [TopLevelModuleName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState (Set TopLevelModuleName)
-> TCMT IO (Set TopLevelModuleName)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Set TopLevelModuleName -> f (Set TopLevelModuleName))
-> TCState -> f TCState
Lens' TCState (Set TopLevelModuleName)
stImportedModulesTransitive
      [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.imports" Int
10 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
        [[Char]] -> [Char]
unwords [TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
top, [Char]
"added, all transitive imports:"] [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
:
        (TopLevelModuleName -> [Char]) -> [TopLevelModuleName] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (\ TopLevelModuleName
x -> [[Char]] -> [Char]
unwords [ [Char]
" ", [Char]
"-", TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
x ]) [TopLevelModuleName]
imports

    -- If that interface was supposed to raise a warning on import, do so.
    Maybe Text -> (Text -> TCM ()) -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (Interface -> Maybe Text
iImportWarning Interface
i) ((Text -> TCM ()) -> TCM ()) -> (Text -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> (Text -> Warning) -> Text -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Warning
UserWarning

    -- let s = publicModules $ iInsideScope i
    let s :: Map ModuleName Scope
s = Interface -> Map ModuleName Scope
iScope Interface
i
    (ModuleName, Map ModuleName Scope)
-> TCM (ModuleName, Map ModuleName Scope)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Interface -> ModuleName
iModuleName Interface
i, Map ModuleName Scope
s)

-- | If the module has already been visited (without warnings), then
-- its interface is returned directly. Otherwise the computation is
-- used to find the interface and the computed interface is stored for
-- potential later use.

alreadyVisited :: TopLevelModuleName ->
                  MainInterface ->
                  PragmaOptions ->
                  TCM ModuleInfo ->
                  TCM ModuleInfo
alreadyVisited :: TopLevelModuleName
-> MainInterface
-> PragmaOptions
-> TCM ModuleInfo
-> TCM ModuleInfo
alreadyVisited TopLevelModuleName
x MainInterface
isMain PragmaOptions
currentOptions TCM ModuleInfo
getModule =
  case MainInterface
isMain of
    MainInterface Mode
TypeCheck                       -> ModuleCheckMode -> TCM ModuleInfo
useExistingOrLoadAndRecordVisited ModuleCheckMode
ModuleTypeChecked
    MainInterface
NotMainInterface                              -> ModuleCheckMode -> TCM ModuleInfo
useExistingOrLoadAndRecordVisited ModuleCheckMode
ModuleTypeChecked
    MainInterface Mode
ScopeCheck                      -> ModuleCheckMode -> TCM ModuleInfo
useExistingOrLoadAndRecordVisited ModuleCheckMode
ModuleScopeChecked
  where
  useExistingOrLoadAndRecordVisited :: ModuleCheckMode -> TCM ModuleInfo
  useExistingOrLoadAndRecordVisited :: ModuleCheckMode -> TCM ModuleInfo
useExistingOrLoadAndRecordVisited ModuleCheckMode
mode = TCM ModuleInfo -> TCMT IO (Maybe ModuleInfo) -> TCM ModuleInfo
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM TCM ModuleInfo
loadAndRecordVisited (ModuleCheckMode -> TCMT IO (Maybe ModuleInfo)
existingWithoutWarnings ModuleCheckMode
mode)

  -- Case: already visited.
  --
  -- A module with warnings should never be allowed to be
  -- imported from another module.
  existingWithoutWarnings :: ModuleCheckMode -> TCM (Maybe ModuleInfo)
  existingWithoutWarnings :: ModuleCheckMode -> TCMT IO (Maybe ModuleInfo)
existingWithoutWarnings ModuleCheckMode
mode = MaybeT (TCMT IO) ModuleInfo -> TCMT IO (Maybe ModuleInfo)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (TCMT IO) ModuleInfo -> TCMT IO (Maybe ModuleInfo))
-> MaybeT (TCMT IO) ModuleInfo -> TCMT IO (Maybe ModuleInfo)
forall a b. (a -> b) -> a -> b
$ ExceptT [Char] (TCMT IO) ModuleInfo -> MaybeT (TCMT IO) ModuleInfo
forall (m :: * -> *) e a. Functor m => ExceptT e m a -> MaybeT m a
exceptToMaybeT (ExceptT [Char] (TCMT IO) ModuleInfo
 -> MaybeT (TCMT IO) ModuleInfo)
-> ExceptT [Char] (TCMT IO) ModuleInfo
-> MaybeT (TCMT IO) ModuleInfo
forall a b. (a -> b) -> a -> b
$ do
    ModuleInfo
mi <- [Char]
-> MaybeT (TCMT IO) ModuleInfo
-> ExceptT [Char] (TCMT IO) ModuleInfo
forall (m :: * -> *) e a.
Functor m =>
e -> MaybeT m a -> ExceptT e m a
maybeToExceptT [Char]
"interface has not been visited in this context" (MaybeT (TCMT IO) ModuleInfo
 -> ExceptT [Char] (TCMT IO) ModuleInfo)
-> MaybeT (TCMT IO) ModuleInfo
-> ExceptT [Char] (TCMT IO) ModuleInfo
forall a b. (a -> b) -> a -> b
$ TCMT IO (Maybe ModuleInfo) -> MaybeT (TCMT IO) ModuleInfo
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe ModuleInfo) -> MaybeT (TCMT IO) ModuleInfo)
-> TCMT IO (Maybe ModuleInfo) -> MaybeT (TCMT IO) ModuleInfo
forall a b. (a -> b) -> a -> b
$
      TopLevelModuleName -> TCMT IO (Maybe ModuleInfo)
forall (m :: * -> *).
ReadTCState m =>
TopLevelModuleName -> m (Maybe ModuleInfo)
getVisitedModule TopLevelModuleName
x

    Bool -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when (ModuleInfo -> ModuleCheckMode
miMode ModuleInfo
mi ModuleCheckMode -> ModuleCheckMode -> Bool
forall a. Ord a => a -> a -> Bool
< ModuleCheckMode
mode) (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]
"previously-visited interface was not sufficiently checked"

    Bool -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (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) (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]
"previously-visited interface had warnings"

    [Char] -> Int -> [Char] -> ExceptT [Char] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.visit" Int
10 ([Char] -> ExceptT [Char] (TCMT IO) ())
-> [Char] -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  Already visited " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
x

    TCM ModuleInfo -> ExceptT [Char] (TCMT IO) 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 ModuleInfo -> ExceptT [Char] (TCMT IO) ModuleInfo)
-> TCM ModuleInfo -> ExceptT [Char] (TCMT IO) ModuleInfo
forall a b. (a -> b) -> a -> b
$ ModuleInfo -> TCM ModuleInfo
processResultingModule ModuleInfo
mi

  processResultingModule :: ModuleInfo -> TCM ModuleInfo
  processResultingModule :: ModuleInfo -> TCM ModuleInfo
processResultingModule ModuleInfo
mi = do
    let ModuleInfo { miInterface :: ModuleInfo -> Interface
miInterface = Interface
i, miPrimitive :: ModuleInfo -> Bool
miPrimitive = Bool
isPrim, miWarnings :: ModuleInfo -> Set TCWarning
miWarnings = Set TCWarning
ws } = ModuleInfo
mi

    -- Check that imported options are compatible with current ones (issue #2487),
    -- but give primitive modules a pass
    -- compute updated warnings if needed
    Set TCWarning
wt <- 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

    ModuleInfo -> TCM ModuleInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleInfo
mi { miWarnings = wt }

  loadAndRecordVisited :: TCM ModuleInfo
  loadAndRecordVisited :: TCM ModuleInfo
loadAndRecordVisited = do
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.visit" Int
5 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  Getting interface for " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
x
    ModuleInfo
mi <- ModuleInfo -> TCM ModuleInfo
processResultingModule (ModuleInfo -> TCM ModuleInfo) -> TCM ModuleInfo -> TCM ModuleInfo
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM ModuleInfo
getModule
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.visit" Int
5 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  Now we've looked at " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
x

    -- Interfaces are not stored if we are only scope-checking, or
    -- if any warnings were encountered.
    case (MainInterface
isMain, 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) of
      (MainInterface Mode
ScopeCheck, Bool
_) -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      (MainInterface
_, Bool
False)                    -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      (MainInterface, Bool)
_                             -> ModuleInfo -> TCM ()
storeDecodedModule ModuleInfo
mi

    [Char] -> Int -> [[Char]] -> TCM ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> Int -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [[Char]] -> m ()
reportS [Char]
"warning.import" Int
10
      [ [Char]
"module: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ TopLevelModuleNameParts -> [Char]
forall a. Show a => a -> [Char]
show (TopLevelModuleName -> TopLevelModuleNameParts
forall range. TopLevelModuleName' range -> TopLevelModuleNameParts
moduleNameParts TopLevelModuleName
x)
      , [Char]
"WarningOnImport: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe Text -> [Char]
forall a. Show a => a -> [Char]
show (Interface -> Maybe Text
iImportWarning (ModuleInfo -> Interface
miInterface ModuleInfo
mi))
      ]

    ModuleInfo -> TCM ()
visitModule ModuleInfo
mi
    ModuleInfo -> TCM ModuleInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleInfo
mi


-- | 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
    }

-- | 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 -> TCM ()
setOptionsFromSourcePragmas Bool
True Source
src

  -- Import the Agda.Primitive modules
  TCM ()
importPrimitiveModules

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

  ModuleInfo
mi <- TopLevelModuleName
-> MainInterface -> Maybe Source -> TCM ModuleInfo
getInterface (Source -> TopLevelModuleName
srcModuleName Source
src) (Mode -> MainInterface
MainInterface Mode
mode) (Source -> Maybe Source
forall a. a -> Maybe a
Just Source
src)

  (Maybe (ModuleName, TopLevelModuleName)
 -> f (Maybe (ModuleName, TopLevelModuleName)))
-> TCState -> f TCState
Lens' TCState (Maybe (ModuleName, TopLevelModuleName))
stCurrentModule Lens' TCState (Maybe (ModuleName, TopLevelModuleName))
-> Maybe (ModuleName, TopLevelModuleName) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens'`
    (ModuleName, TopLevelModuleName)
-> Maybe (ModuleName, TopLevelModuleName)
forall a. a -> Maybe a
Just ( Interface -> ModuleName
iModuleName (ModuleInfo -> Interface
miInterface ModuleInfo
mi)
         , Interface -> TopLevelModuleName
iTopLevelModuleName (ModuleInfo -> Interface
miInterface ModuleInfo
mi)
         )

  CheckResult -> TCM CheckResult
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CheckResult -> TCM CheckResult) -> CheckResult -> TCM CheckResult
forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Source -> CheckResult
CheckResult' ModuleInfo
mi Source
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 -> SourceFile -> TCM ()
checkModuleName' TopLevelModuleName
m SourceFile
f =
  TopLevelModuleName -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange TopLevelModuleName
m (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName
-> SourceFile -> Maybe TopLevelModuleName -> TCM ()
checkModuleName TopLevelModuleName
m SourceFile
f Maybe TopLevelModuleName
forall a. Maybe a
Nothing

-- | Import the primitive modules (unless --no-load-primitives).
importPrimitiveModules :: TCM ()
importPrimitiveModules :: TCM ()
importPrimitiveModules = TCMT IO Bool -> TCM () -> TCM ()
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) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.main" Int
10 [Char]
"Importing the primitive modules."
  AbsolutePath
libdirPrim <- Lens' TCState AbsolutePath -> TCMT IO AbsolutePath
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (AbsolutePath -> f AbsolutePath) -> TCState -> f TCState
Lens' TCState AbsolutePath
stPrimitiveLibDir
  [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.main" Int
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Library primitive dir = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ AbsolutePath -> [Char]
forall a. Show a => a -> [Char]
show AbsolutePath
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.

  TCMT IO PersistentVerbosity
-> (PersistentVerbosity -> TCM ()) -> TCM () -> TCM ()
forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ ((TCState -> PersistentVerbosity) -> TCMT IO PersistentVerbosity
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC TCState -> PersistentVerbosity
forall a. LensPersistentVerbosity a => a -> PersistentVerbosity
Lens.getPersistentVerbosity) PersistentVerbosity -> TCM ()
forall (m :: * -> *). MonadTCState m => PersistentVerbosity -> m ()
Lens.putPersistentVerbosity (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    (PersistentVerbosity -> PersistentVerbosity) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(PersistentVerbosity -> PersistentVerbosity) -> m ()
Lens.modifyPersistentVerbosity
      (Trie VerboseKeyItem Int -> PersistentVerbosity
forall a. a -> Maybe a
Strict.Just (Trie VerboseKeyItem Int -> PersistentVerbosity)
-> (PersistentVerbosity -> Trie VerboseKeyItem Int)
-> PersistentVerbosity
-> PersistentVerbosity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VerboseKeyItem]
-> Int -> Trie VerboseKeyItem Int -> Trie VerboseKeyItem Int
forall k v. Ord k => [k] -> v -> Trie k v -> Trie k v
Trie.insert [] Int
0 (Trie VerboseKeyItem Int -> Trie VerboseKeyItem Int)
-> (PersistentVerbosity -> Trie VerboseKeyItem Int)
-> PersistentVerbosity
-> Trie VerboseKeyItem Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Trie VerboseKeyItem Int
-> PersistentVerbosity -> Trie VerboseKeyItem Int
forall a. a -> Maybe a -> a
Strict.fromMaybe Trie VerboseKeyItem Int
forall a. Null a => a
Trie.empty)
      -- set root verbosity to 0

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

  [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.main" Int
10 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"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 -> Maybe Source -> TCMT IO Interface
getNonMainInterface TopLevelModuleName
x Maybe Source
msrc = do
  ModuleInfo
mi <- TopLevelModuleName -> Maybe Source -> TCM ModuleInfo
getNonMainModuleInfo TopLevelModuleName
x Maybe Source
msrc
  [TCWarning] -> TCM ()
tcWarningsToError ([TCWarning] -> TCM ()) -> [TCWarning] -> TCM ()
forall a b. (a -> b) -> a -> b
$ Set TCWarning -> [TCWarning]
forall a. Set a -> [a]
Set.toAscList (Set TCWarning -> [TCWarning]) -> Set TCWarning -> [TCWarning]
forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Set TCWarning
miWarnings ModuleInfo
mi
  Interface -> TCMT IO Interface
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ModuleInfo -> Interface
miInterface ModuleInfo
mi)

getNonMainModuleInfo
  :: TopLevelModuleName
  -> Maybe Source
     -- ^ Optional: the source code and some information about the source code.
  -> TCM ModuleInfo
getNonMainModuleInfo :: TopLevelModuleName -> Maybe Source -> TCM ModuleInfo
getNonMainModuleInfo TopLevelModuleName
x Maybe Source
msrc =
  -- Preserve/restore the current pragma options, which will be mutated when loading
  -- and checking the interface.
  TCMT IO PragmaOptions
-> (PragmaOptions -> TCM ()) -> TCM ModuleInfo -> TCM ModuleInfo
forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ (Lens' TCState PragmaOptions -> TCMT IO PragmaOptions
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
Lens' TCState PragmaOptions
stPragmaOptions) ((PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
Lens' TCState PragmaOptions
stPragmaOptions Lens' TCState PragmaOptions -> PragmaOptions -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens`) (TCM ModuleInfo -> TCM ModuleInfo)
-> TCM ModuleInfo -> TCM ModuleInfo
forall a b. (a -> b) -> a -> b
$
           TopLevelModuleName
-> MainInterface -> Maybe Source -> TCM ModuleInfo
getInterface TopLevelModuleName
x MainInterface
NotMainInterface Maybe Source
msrc

-- | A more precise variant of 'getNonMainInterface'. If warnings are
-- encountered then they are returned instead of being turned into
-- errors.

getInterface
  :: TopLevelModuleName
  -> MainInterface
  -> Maybe Source
     -- ^ Optional: the source code and some information about the source code.
  -> TCM ModuleInfo
getInterface :: TopLevelModuleName
-> MainInterface -> Maybe Source -> TCM ModuleInfo
getInterface TopLevelModuleName
x MainInterface
isMain Maybe Source
msrc =
  TopLevelModuleName -> TCM ModuleInfo -> TCM ModuleInfo
forall a. TopLevelModuleName -> TCM a -> TCM a
addImportCycleCheck TopLevelModuleName
x (TCM ModuleInfo -> TCM ModuleInfo)
-> TCM ModuleInfo -> TCM ModuleInfo
forall a b. (a -> b) -> a -> b
$ do
     -- We remember but reset the pragma options locally
     -- Issue #3644 (Abel 2020-05-08): Set approximate range for errors in options
     PragmaOptions
currentOptions <- Lens' TCState PragmaOptions -> TCMT IO PragmaOptions
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
Lens' TCState PragmaOptions
stPragmaOptions
     Maybe [Pragma] -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (Module -> [Pragma]
C.modPragmas (Module -> [Pragma]) -> (Source -> Module) -> Source -> [Pragma]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Source -> Module
srcModule (Source -> [Pragma]) -> Maybe Source -> Maybe [Pragma]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Source
msrc) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
       -- Now reset the options
       CommandLineOptions -> TCM ()
setCommandLineOptions (CommandLineOptions -> TCM ())
-> (TCState -> CommandLineOptions) -> TCState -> TCM ()
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 -> TCM ()) -> TCMT IO TCState -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC

     TopLevelModuleName
-> MainInterface
-> PragmaOptions
-> TCM ModuleInfo
-> TCM ModuleInfo
alreadyVisited TopLevelModuleName
x MainInterface
isMain PragmaOptions
currentOptions (TCM ModuleInfo -> TCM ModuleInfo)
-> TCM ModuleInfo -> TCM ModuleInfo
forall a b. (a -> b) -> a -> b
$ do
      SourceFile
file <- case Maybe Source
msrc of
        Maybe Source
Nothing  -> TopLevelModuleName -> TCMT IO SourceFile
findFile TopLevelModuleName
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' TCState (Map TopLevelModuleName SourceFile)
-> (Map TopLevelModuleName SourceFile
    -> Map TopLevelModuleName SourceFile)
-> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
modifyTCLens (Map TopLevelModuleName SourceFile
 -> f (Map TopLevelModuleName SourceFile))
-> TCState -> f TCState
Lens' TCState (Map TopLevelModuleName SourceFile)
stModuleToSourceId ((Map TopLevelModuleName SourceFile
  -> Map TopLevelModuleName SourceFile)
 -> TCM ())
-> (Map TopLevelModuleName SourceFile
    -> Map TopLevelModuleName SourceFile)
-> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName
-> SourceFile
-> Map TopLevelModuleName SourceFile
-> Map TopLevelModuleName SourceFile
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TopLevelModuleName
x SourceFile
file
          SourceFile -> TCMT IO SourceFile
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceFile
file
      [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"import.iface" Int
15 do
        AbsolutePath
path <- SourceFile -> TCMT IO AbsolutePath
forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
srcFilePath SourceFile
file
        [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
P.text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
"\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ ShowS -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char]
"  " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++)
          [ [Char]
"module: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
x
          , [Char]
"file:   " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ AbsolutePath -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow AbsolutePath
path
          ]

      [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
15 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  Check for cycle"
      TCM ()
checkForImportCycle

      -- -- Andreas, 2014-10-20 AIM XX:
      -- -- Always retype-check the main file to get the iInsideScope
      -- -- which is no longer serialized.
      -- let maySkip = isMain == NotMainInterface
      -- Andreas, 2015-07-13: Serialize iInsideScope again.
      -- Andreas, 2020-05-13 issue #4647: don't skip if reload because of top-level command
      Either [Char] ModuleInfo
stored <- ExceptT [Char] (TCMT IO) ModuleInfo
-> TCMT IO (Either [Char] ModuleInfo)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT [Char] (TCMT IO) ModuleInfo
 -> TCMT IO (Either [Char] ModuleInfo))
-> ExceptT [Char] (TCMT IO) ModuleInfo
-> TCMT IO (Either [Char] ModuleInfo)
forall a b. (a -> b) -> a -> b
$ Account (BenchPhase (ExceptT [Char] (TCMT IO)))
-> ExceptT [Char] (TCMT IO) ModuleInfo
-> ExceptT [Char] (TCMT IO) ModuleInfo
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (ExceptT [Char] (TCMT IO))
Phase
Bench.Import] (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
        HasCallStack =>
TopLevelModuleName
-> SourceFile
-> Maybe Source
-> ExceptT [Char] (TCMT IO) ModuleInfo
TopLevelModuleName
-> SourceFile
-> Maybe Source
-> ExceptT [Char] (TCMT IO) ModuleInfo
getStoredInterface TopLevelModuleName
x SourceFile
file Maybe Source
msrc

      let recheck :: [Char] -> TCM ModuleInfo
recheck = \[Char]
reason -> do
            [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
5 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Char]
"  ", TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
x, [Char]
" is not up-to-date because ", [Char]
reason, [Char]
"."]
            CommandLineOptions -> TCM ()
setCommandLineOptions (CommandLineOptions -> TCM ())
-> (TCState -> CommandLineOptions) -> TCState -> TCM ()
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 -> TCM ()) -> TCMT IO TCState -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
            ModuleInfo
modl <- case MainInterface
isMain of
              MainInterface Mode
_ -> TopLevelModuleName
-> SourceFile -> MainInterface -> Maybe Source -> TCM ModuleInfo
createInterface TopLevelModuleName
x SourceFile
file MainInterface
isMain Maybe Source
msrc
              MainInterface
NotMainInterface -> TopLevelModuleName -> SourceFile -> Maybe Source -> TCM ModuleInfo
createInterfaceIsolated TopLevelModuleName
x SourceFile
file Maybe Source
msrc

            -- Ensure that the given module name matches the one in the file.
            let topLevelName :: TopLevelModuleName
topLevelName = Interface -> TopLevelModuleName
iTopLevelModuleName (ModuleInfo -> Interface
miInterface ModuleInfo
modl)
            Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (TopLevelModuleName
topLevelName TopLevelModuleName -> TopLevelModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== TopLevelModuleName
x) do
              AbsolutePath
path <- SourceFile -> TCMT IO AbsolutePath
forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
srcFilePath SourceFile
file
              TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ AbsolutePath
-> TopLevelModuleName -> TopLevelModuleName -> TypeError
OverlappingProjects AbsolutePath
path TopLevelModuleName
topLevelName TopLevelModuleName
x

            ModuleInfo -> TCM ModuleInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleInfo
modl

      ([Char] -> TCM ModuleInfo)
-> (ModuleInfo -> TCM ModuleInfo)
-> Either [Char] ModuleInfo
-> TCM ModuleInfo
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either [Char] -> TCM ModuleInfo
recheck ModuleInfo -> TCM ModuleInfo
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Either [Char] ModuleInfo
stored

-- | If checking produced non-benign warnings, error out.
--
raiseNonFatalErrors :: (HasOptions m, MonadTCError m)
  => CheckResult  -- ^ E.g. obtained from 'typeCheckMain'.
  -> m ()
raiseNonFatalErrors :: forall (m :: * -> *).
(HasOptions m, MonadTCError m) =>
CheckResult -> m ()
raiseNonFatalErrors CheckResult
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 (CheckResult -> Set TCWarning
crWarnings CheckResult
result)) ((Set1 TCWarning -> m ()) -> m ())
-> (Set1 TCWarning -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ Set1 TCWarning
ws ->
    TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> 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 -> TCMT IO Bool
checkOptionsCompatible PragmaOptions
current PragmaOptions
imported TopLevelModuleName
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
      Bool -> StateT Bool (TCMT IO) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put Bool
False
      Warning -> StateT Bool (TCMT IO) ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> 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 -> Doc
icOptionWarning InfectiveCoinfectiveOption
opt TopLevelModuleName
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 -> PragmaOptions -> Interface -> TCM (Maybe (Set TCWarning))
getOptionsCompatibilityWarnings :: MainInterface
-> Bool
-> PragmaOptions
-> Interface
-> TCMT IO (Maybe (Set TCWarning))
getOptionsCompatibilityWarnings MainInterface
isMain Bool
isPrim PragmaOptions
currentOptions Interface
i = MaybeT (TCMT IO) (Set TCWarning) -> TCMT IO (Maybe (Set TCWarning))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (TCMT IO) (Set TCWarning)
 -> TCMT IO (Maybe (Set TCWarning)))
-> MaybeT (TCMT IO) (Set TCWarning)
-> TCMT IO (Maybe (Set TCWarning))
forall a b. (a -> b) -> a -> b
$ ExceptT [Char] (TCMT IO) (Set TCWarning)
-> MaybeT (TCMT IO) (Set TCWarning)
forall (m :: * -> *) e a. Functor m => ExceptT e m a -> MaybeT m a
exceptToMaybeT (ExceptT [Char] (TCMT IO) (Set TCWarning)
 -> MaybeT (TCMT IO) (Set TCWarning))
-> ExceptT [Char] (TCMT IO) (Set TCWarning)
-> MaybeT (TCMT IO) (Set TCWarning)
forall a b. (a -> b) -> a -> b
$ do
  -- We're just dropping these reasons-for-skipping messages for now.
  -- They weren't logged before, but they're nice for documenting the early returns.
  Bool -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when Bool
isPrim (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]
"Options consistency checking disabled for always-available primitive module"
  ExceptT [Char] (TCMT IO) Bool
-> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (TCMT IO Bool -> ExceptT [Char] (TCMT IO) Bool
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 Bool -> ExceptT [Char] (TCMT IO) Bool)
-> TCMT IO Bool -> ExceptT [Char] (TCMT IO) Bool
forall a b. (a -> b) -> a -> b
$ PragmaOptions
-> PragmaOptions -> TopLevelModuleName -> TCMT IO Bool
checkOptionsCompatible PragmaOptions
currentOptions (Interface -> PragmaOptions
iOptionsUsed Interface
i)
                  (Interface -> TopLevelModuleName
iTopLevelModuleName Interface
i)) (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]
"No warnings to collect because options were compatible"
  TCMT IO (Set TCWarning) -> ExceptT [Char] (TCMT IO) (Set TCWarning)
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 (Set TCWarning)
 -> ExceptT [Char] (TCMT IO) (Set TCWarning))
-> TCMT IO (Set TCWarning)
-> ExceptT [Char] (TCMT IO) (Set TCWarning)
forall a b. (a -> b) -> a -> b
$ MainInterface -> WhichWarnings -> TCMT IO (Set TCWarning)
forall (m :: * -> *).
(ReadTCState m, MonadWarning m, MonadTCM m) =>
MainInterface -> WhichWarnings -> m (Set TCWarning)
getAllWarnings' MainInterface
isMain WhichWarnings
ErrorWarnings

-- | 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
-> SourceFile
-> Maybe Source
-> ExceptT [Char] (TCMT IO) ModuleInfo
getStoredInterface TopLevelModuleName
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.
        InterfaceFile
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.
        (Hash, Hash)
hashes <- [Char]
-> MaybeT (TCMT IO) (Hash, Hash)
-> ExceptT [Char] (TCMT IO) (Hash, Hash)
forall (m :: * -> *) e a.
Functor m =>
e -> MaybeT m a -> ExceptT e m a
maybeToExceptT [Char]
"the interface file hash could not be read" (MaybeT (TCMT IO) (Hash, Hash)
 -> ExceptT [Char] (TCMT IO) (Hash, Hash))
-> MaybeT (TCMT IO) (Hash, Hash)
-> ExceptT [Char] (TCMT IO) (Hash, Hash)
forall a b. (a -> b) -> a -> b
$ TCMT IO (Maybe (Hash, Hash)) -> MaybeT (TCMT IO) (Hash, Hash)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe (Hash, Hash)) -> MaybeT (TCMT IO) (Hash, Hash))
-> TCMT IO (Maybe (Hash, Hash)) -> MaybeT (TCMT IO) (Hash, Hash)
forall a b. (a -> b) -> a -> b
$ IO (Maybe (Hash, Hash)) -> TCMT IO (Maybe (Hash, Hash))
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe (Hash, Hash)) -> TCMT IO (Maybe (Hash, Hash)))
-> IO (Maybe (Hash, Hash)) -> TCMT IO (Maybe (Hash, Hash))
forall a b. (a -> b) -> a -> b
$
          InterfaceFile -> IO (Maybe (Hash, Hash))
getInterfaceFileHashes InterfaceFile
ifile

        (InterfaceFile, (Hash, Hash))
-> ExceptT [Char] (TCMT IO) (InterfaceFile, (Hash, Hash))
forall a. a -> ExceptT [Char] (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (InterfaceFile
ifile, (Hash, Hash)
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
        Hash
sourceH <- case Maybe Source
msrc of
                    Maybe Source
Nothing -> do
                      AbsolutePath
path <- SourceFile -> ExceptT [Char] (TCMT IO) AbsolutePath
forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
srcFilePath SourceFile
file
                      IO Hash -> ExceptT [Char] (TCMT IO) Hash
forall a. IO a -> ExceptT [Char] (TCMT IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Hash -> ExceptT [Char] (TCMT IO) Hash)
-> IO Hash -> ExceptT [Char] (TCMT IO) Hash
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> IO Hash
hashTextFile AbsolutePath
path
                    Just Source
src -> Hash -> ExceptT [Char] (TCMT IO) Hash
forall a. a -> ExceptT [Char] (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Hash -> ExceptT [Char] (TCMT IO) Hash)
-> Hash -> ExceptT [Char] (TCMT IO) Hash
forall a b. (a -> b) -> a -> b
$ Text -> Hash
hashText (Source -> Text
srcText Source
src)

        Bool -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Hash
sourceH Hash -> Hash -> Bool
forall a. Eq a => a -> a -> Bool
== Hash
ifaceH) (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] -> ExceptT [Char] (TCMT IO) ())
-> [Char] -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            [ [Char]
"the source hash (", Hash -> [Char]
forall a. Show a => a -> [Char]
show Hash
sourceH, [Char]
")"
            , [Char]
" does not match the source hash for the interface (", Hash -> [Char]
forall a. Show a => a -> [Char]
show Hash
ifaceH, [Char]
")"
            ]

        [Char] -> Int -> [Char] -> ExceptT [Char] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
5 ([Char] -> ExceptT [Char] (TCMT IO) ())
-> [Char] -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Char]
"  ", TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
x, [Char]
" 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"

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

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

      Account (BenchPhase (ExceptT [Char] (TCMT IO)))
-> ExceptT [Char] (TCMT IO) ModuleInfo
-> ExceptT [Char] (TCMT IO) ModuleInfo
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (ExceptT [Char] (TCMT IO))
Phase
Bench.Deserialization] (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
        Hash -> ExceptT [Char] (TCMT IO) ()
checkSourceHashET ((Hash, Hash) -> Hash
forall a b. (a, b) -> a
fst (Hash, Hash)
hashes)

        [Char] -> Int -> [Char] -> ExceptT [Char] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
5 ([Char] -> ExceptT [Char] (TCMT IO) ())
-> [Char] -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  no stored version, reading " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
ifp

        Interface
i <- [Char]
-> MaybeT (TCMT IO) Interface -> ExceptT [Char] (TCMT IO) Interface
forall (m :: * -> *) e a.
Functor m =>
e -> MaybeT m a -> ExceptT e m a
maybeToExceptT [Char]
"bad interface, re-type checking" (MaybeT (TCMT IO) Interface -> ExceptT [Char] (TCMT IO) Interface)
-> MaybeT (TCMT IO) Interface -> ExceptT [Char] (TCMT IO) Interface
forall a b. (a -> b) -> a -> b
$ TCMT IO (Maybe Interface) -> MaybeT (TCMT IO) Interface
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe Interface) -> MaybeT (TCMT IO) Interface)
-> TCMT IO (Maybe Interface) -> MaybeT (TCMT IO) Interface
forall a b. (a -> b) -> a -> b
$
          InterfaceFile -> TCMT IO (Maybe Interface)
readInterface InterfaceFile
ifile

        -- Ensure that the given module name matches the one in the file.
        let topLevelName :: TopLevelModuleName
topLevelName = Interface -> TopLevelModuleName
iTopLevelModuleName Interface
i
        Bool -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (TopLevelModuleName
topLevelName TopLevelModuleName -> TopLevelModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== TopLevelModuleName
x) do
          AbsolutePath
path <- SourceFile -> ExceptT [Char] (TCMT IO) AbsolutePath
forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
srcFilePath SourceFile
file
          TCM () -> ExceptT [Char] (TCMT IO) ()
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 () -> ExceptT [Char] (TCMT IO) ())
-> TCM () -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ AbsolutePath
-> TopLevelModuleName -> TopLevelModuleName -> TypeError
OverlappingProjects AbsolutePath
path TopLevelModuleName
topLevelName TopLevelModuleName
x

        Bool
isPrimitiveMod <- FileId -> ExceptT [Char] (TCMT IO) Bool
forall (m :: * -> *). ReadTCState m => FileId -> m Bool
isPrimitiveModule FileId
fi

        TCM () -> ExceptT [Char] (TCMT IO) ()
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 () -> ExceptT [Char] (TCMT IO) ())
-> TCM () -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char] -> TopLevelModuleName -> Maybe [Char] -> TCM ()
chaseMsg [Char]
"Loading " TopLevelModuleName
x (Maybe [Char] -> TCM ()) -> Maybe [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
ifp
        -- print imported warnings
        TopLevelModuleName -> Set TCWarning -> ExceptT [Char] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
TopLevelModuleName -> Set TCWarning -> m ()
reportWarningsForModule TopLevelModuleName
x (Set TCWarning -> ExceptT [Char] (TCMT IO) ())
-> Set TCWarning -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ Interface -> Set TCWarning
iWarnings Interface
i

        SourceFile -> ModuleInfo -> ExceptT [Char] (TCMT IO) ModuleInfo
loadDecodedModule SourceFile
file (ModuleInfo -> ExceptT [Char] (TCMT IO) ModuleInfo)
-> ModuleInfo -> ExceptT [Char] (TCMT IO) ModuleInfo
forall a b. (a -> b) -> a -> b
$ ModuleInfo
          { miInterface :: Interface
miInterface = Interface
i
          , miWarnings :: Set TCWarning
miWarnings = Set TCWarning
forall a. Null a => a
empty
          , miPrimitive :: Bool
miPrimitive = Bool
isPrimitiveMod
          , miMode :: ModuleCheckMode
miMode = ModuleCheckMode
ModuleTypeChecked
          }

  -- Check if we have cached the module.
  Either [Char] ModuleInfo
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
$
      TCMT IO (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 (TCMT IO (Maybe ModuleInfo)
 -> ExceptT [Char] (TCMT IO) (Maybe ModuleInfo))
-> TCMT IO (Maybe ModuleInfo)
-> ExceptT [Char] (TCMT IO) (Maybe ModuleInfo)
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> TCMT IO (Maybe ModuleInfo)
getDecodedModule TopLevelModuleName
x

  case Either [Char] ModuleInfo
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
      (InterfaceFile
ifile, (Hash, Hash)
hashes) <- ExceptT [Char] (TCMT IO) (InterfaceFile, (Hash, Hash))
getIFileHashesET

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

      -- Make sure the hashes match.
      let cachedIfaceHash :: Hash
cachedIfaceHash = Interface -> Hash
iFullHash Interface
i
      let fileIfaceHash :: Hash
fileIfaceHash = (Hash, Hash) -> Hash
forall a b. (a, b) -> b
snd (Hash, Hash)
hashes
      if Hash
cachedIfaceHash Hash -> Hash -> Bool
forall a. Eq a => a -> a -> Bool
/= Hash
fileIfaceHash then do
        TCM () -> ExceptT [Char] (TCMT IO) ()
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 () -> ExceptT [Char] (TCMT IO) ())
-> TCM () -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> TCM ()
dropDecodedModule TopLevelModuleName
x
        [Char] -> Int -> [Char] -> ExceptT [Char] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
50 ([Char] -> ExceptT [Char] (TCMT IO) ())
-> [Char] -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  cached hash = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Hash -> [Char]
forall a. Show a => a -> [Char]
show Hash
cachedIfaceHash
        [Char] -> Int -> [Char] -> ExceptT [Char] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
50 ([Char] -> ExceptT [Char] (TCMT IO) ())
-> [Char] -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  stored hash = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Hash -> [Char]
forall a. Show a => a -> [Char]
show Hash
fileIfaceHash
        [Char] -> Int -> [Char] -> ExceptT [Char] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
5 ([Char] -> ExceptT [Char] (TCMT IO) ())
-> [Char] -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  file is newer, re-reading " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
ifp
        [Char] -> ExceptT [Char] (TCMT IO) ModuleInfo
loadInterfaceFile ([Char] -> ExceptT [Char] (TCMT IO) ModuleInfo)
-> [Char] -> ExceptT [Char] (TCMT IO) ModuleInfo
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ [Char]
"the cached interface hash (", Hash -> [Char]
forall a. Show a => a -> [Char]
show Hash
cachedIfaceHash, [Char]
")"
          , [Char]
" does not match interface file (", Hash -> [Char]
forall a. Show a => a -> [Char]
show Hash
fileIfaceHash, [Char]
")"
          ]
       else Account (BenchPhase (ExceptT [Char] (TCMT IO)))
-> ExceptT [Char] (TCMT IO) ModuleInfo
-> ExceptT [Char] (TCMT IO) ModuleInfo
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (ExceptT [Char] (TCMT IO))
Phase
Bench.Deserialization] (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
        Hash -> ExceptT [Char] (TCMT IO) ()
checkSourceHashET (Interface -> Hash
iSourceHash Interface
i)

        [Char] -> Int -> [Char] -> ExceptT [Char] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
5 ([Char] -> ExceptT [Char] (TCMT IO) ())
-> [Char] -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  using stored version of " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ AbsolutePath -> [Char]
filePath (InterfaceFile -> AbsolutePath
intFilePath InterfaceFile
ifile)
        SourceFile -> ModuleInfo -> ExceptT [Char] (TCMT IO) ModuleInfo
loadDecodedModule SourceFile
file ModuleInfo
mi

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

reportWarningsForModule :: MonadDebug m => TopLevelModuleName -> Set TCWarning -> m ()
reportWarningsForModule :: forall (m :: * -> *).
MonadDebug m =>
TopLevelModuleName -> Set TCWarning -> m ()
reportWarningsForModule TopLevelModuleName
x Set TCWarning
warns = do
  [TCWarning] -> ([TCWarning] -> m ()) -> m ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull ((TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Maybe TopLevelModuleName -> Maybe (Maybe TopLevelModuleName)
forall a. a -> Maybe a
Strict.Just (TopLevelModuleName -> Maybe TopLevelModuleName
forall a. a -> Maybe a
Just TopLevelModuleName
x) Maybe (Maybe TopLevelModuleName)
-> Maybe (Maybe TopLevelModuleName) -> Bool
forall a. Eq a => a -> a -> Bool
==) (Maybe (Maybe TopLevelModuleName) -> Bool)
-> (TCWarning -> Maybe (Maybe TopLevelModuleName))
-> TCWarning
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RangeFile -> Maybe TopLevelModuleName)
-> Maybe RangeFile -> Maybe (Maybe TopLevelModuleName)
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
rangeFileName (Maybe RangeFile -> Maybe (Maybe TopLevelModuleName))
-> (TCWarning -> Maybe RangeFile)
-> TCWarning
-> Maybe (Maybe TopLevelModuleName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Maybe RangeFile
tcWarningOrigin) ([TCWarning] -> [TCWarning]) -> [TCWarning] -> [TCWarning]
forall a b. (a -> b) -> a -> b
$ Set TCWarning -> [TCWarning]
forall a. Set a -> [a]
Set.toAscList Set TCWarning
warns) \ [TCWarning]
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
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
P.vsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (TCWarning -> TCMT IO Doc) -> [TCWarning] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map TCWarning -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
P.prettyTCM [TCWarning]
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
  AbsolutePath
file <- SourceFile -> ExceptT [Char] (TCMT IO) AbsolutePath
forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
srcFilePath SourceFile
sf
  let fp :: [Char]
fp      = AbsolutePath -> [Char]
filePath AbsolutePath
file
  let i :: Interface
i       = ModuleInfo -> Interface
miInterface ModuleInfo
mi
  let imports :: [(TopLevelModuleName, Hash)]
imports = Interface -> [(TopLevelModuleName, Hash)]
iImportedModules Interface
i
  let name :: TopLevelModuleName
name    = Interface -> TopLevelModuleName
iTopLevelModuleName Interface
i

  -- Print imported modules.
  [Char]
-> Int
-> ExceptT [Char] (TCMT IO) ()
-> ExceptT [Char] (TCMT IO) ()
forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"import.iface.imports" Int
5 (ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ())
-> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ Bool -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless ([(TopLevelModuleName, Hash)] -> Bool
forall a. Null a => a -> Bool
null [(TopLevelModuleName, Hash)]
imports) (ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ())
-> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
    [Char] -> Int -> [Char] -> ExceptT [Char] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.imports" Int
5 ([Char] -> ExceptT [Char] (TCMT IO) ())
-> [Char] -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
      [[Char]] -> [Char]
unwords [ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
name, [Char]
"imports:" ] [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
:
      ((TopLevelModuleName, Hash) -> [Char])
-> [(TopLevelModuleName, Hash)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (\ (TopLevelModuleName
x, Hash
hash) -> [[Char]] -> [Char]
unwords [ [Char]
" ", [Char]
"-", TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
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]
")"] ])
        [(TopLevelModuleName, Hash)]
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)
  [OptionsPragma]
libOptions <- TCMT IO [OptionsPragma] -> ExceptT [Char] (TCMT IO) [OptionsPragma]
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 [OptionsPragma]
 -> ExceptT [Char] (TCMT IO) [OptionsPragma])
-> TCMT IO [OptionsPragma]
-> ExceptT [Char] (TCMT IO) [OptionsPragma]
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> TopLevelModuleName -> TCMT IO [OptionsPragma]
getLibraryOptions AbsolutePath
file TopLevelModuleName
name
  TCM () -> ExceptT [Char] (TCMT IO) ()
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 () -> ExceptT [Char] (TCMT IO) ())
-> TCM () -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ (OptionsPragma -> TCM ()) -> [OptionsPragma] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ OptionsPragma -> TCM ()
setOptionsFromPragma ([OptionsPragma]
libOptions [OptionsPragma] -> [OptionsPragma] -> [OptionsPragma]
forall a. [a] -> [a] -> [a]
++ Interface -> [OptionsPragma]
iFilePragmaOptions Interface
i)

  -- Check that options that matter haven't changed compared to
  -- current options (issue #2487).
  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) do
    PragmaOptions
current <- Lens' TCState PragmaOptions
-> ExceptT [Char] (TCMT IO) PragmaOptions
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
Lens' TCState PragmaOptions
stPragmaOptions
    Bool -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when (PragmaOptions -> PragmaOptions -> Bool
recheckBecausePragmaOptionsChanged (Interface -> PragmaOptions
iOptionsUsed Interface
i) PragmaOptions
current) (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]
"options changed"

  -- If any of the imports are newer we need to re-typecheck.
  [[Char]]
badHashMessages <- ([Either [Char] ()] -> [[Char]])
-> ExceptT [Char] (TCMT IO) [Either [Char] ()]
-> ExceptT [Char] (TCMT IO) [[Char]]
forall a b.
(a -> b)
-> ExceptT [Char] (TCMT IO) a -> ExceptT [Char] (TCMT IO) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Either [Char] ()] -> [[Char]]
forall a b. [Either a b] -> [a]
lefts (ExceptT [Char] (TCMT IO) [Either [Char] ()]
 -> ExceptT [Char] (TCMT IO) [[Char]])
-> ExceptT [Char] (TCMT IO) [Either [Char] ()]
-> ExceptT [Char] (TCMT IO) [[Char]]
forall a b. (a -> b) -> a -> b
$ [(TopLevelModuleName, Hash)]
-> ((TopLevelModuleName, Hash)
    -> ExceptT [Char] (TCMT IO) (Either [Char] ()))
-> ExceptT [Char] (TCMT IO) [Either [Char] ()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(TopLevelModuleName, Hash)]
imports \ (TopLevelModuleName
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 -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
impName, [Char]
" matches ", Hash -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Hash
impHash ]
    Hash
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
$ TCM 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 (TCM Hash -> ExceptT [Char] (TCMT IO) Hash)
-> TCM Hash -> ExceptT [Char] (TCMT IO) Hash
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> TCM Hash -> TCM Hash
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange TopLevelModuleName
impName (TCM Hash -> TCM Hash) -> TCM Hash -> TCM Hash
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> TCM Hash
moduleHash TopLevelModuleName
impName
    [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]
"Done checking module hash of import ", TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
impName]
    Bool
-> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ()
-> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when (Hash
impHash Hash -> Hash -> Bool
forall a. Eq a => a -> a -> Bool
/= Hash
latestImpHash) (ExceptT [Char] (ExceptT [Char] (TCMT IO)) ()
 -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ())
-> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ()
-> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ()
forall a b. (a -> b) -> a -> b
$
      [Char] -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ()
forall a. [Char] -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ([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]
"module hash for imported module ", TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
impName, [Char]
" is out of date"
        , [Char]
" (import cached=", Hash -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Hash
impHash, [Char]
", latest=", Hash -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Hash
latestImpHash, [Char]
")"
        ]

  [[Char]]
-> ([[Char]] -> ExceptT [Char] (TCMT IO) ())
-> ExceptT [Char] (TCMT IO) ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull [[Char]]
badHashMessages ([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] -> ExceptT [Char] (TCMT IO) ())
-> ([[Char]] -> [Char]) -> [[Char]] -> ExceptT [Char] (TCMT IO) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Char]] -> [Char]
unlines)

  [Char] -> Int -> [Char] -> ExceptT [Char] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
5 ([Char] -> ExceptT [Char] (TCMT IO) ())
-> [Char] -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
name [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": interface is valid and can be merged into the state."
  TCM () -> ExceptT [Char] (TCMT IO) ()
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 () -> ExceptT [Char] (TCMT IO) ())
-> TCM () -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ Interface -> TCM ()
mergeInterface Interface
i
  Account (BenchPhase (ExceptT [Char] (TCMT IO)))
-> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (ExceptT [Char] (TCMT IO))
Phase
Bench.Highlighting] (ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ())
-> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
    TCM () -> ExceptT [Char] (TCMT IO) ()
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 () -> ExceptT [Char] (TCMT IO) ())
-> TCM () -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ HighlightingLevel -> TCM () -> TCM ()
forall (tcm :: * -> *).
MonadTCEnv tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
      Interface -> SourceFile -> TCM ()
highlightFromInterface Interface
i SourceFile
sf

  ModuleInfo -> ExceptT [Char] (TCMT IO) ModuleInfo
forall a. a -> ExceptT [Char] (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleInfo
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 -> SourceFile -> Maybe Source -> TCM ModuleInfo
createInterfaceIsolated TopLevelModuleName
x SourceFile
file Maybe Source
msrc = do
      TCM ()
forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog

      [TopLevelModuleName]
ms          <- TCMT IO [TopLevelModuleName]
getImportPath
      Range
range       <- (TCEnv -> Range) -> TCMT IO Range
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Range
envRange
      Maybe (Closure Call)
call        <- (TCEnv -> Maybe (Closure Call)) -> TCMT IO (Maybe (Closure Call))
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe (Closure Call)
envCall
      ModuleToSource
mf          <- Lens' TCState ModuleToSource -> TCMT IO ModuleToSource
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (ModuleToSource -> f ModuleToSource) -> TCState -> f TCState
Lens' TCState ModuleToSource
stModuleToSource
      VisitedModules
vs          <- TCMT IO VisitedModules
forall (m :: * -> *). ReadTCState m => m VisitedModules
getVisitedModules
      VisitedModules
ds          <- TCMT IO VisitedModules
getDecodedModules
      CommandLineOptions
opts        <- PersistentTCState -> CommandLineOptions
stPersistentOptions (PersistentTCState -> CommandLineOptions)
-> (TCState -> PersistentTCState) -> TCState -> CommandLineOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState (TCState -> CommandLineOptions)
-> TCMT IO TCState -> TCMT IO CommandLineOptions
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
      Signature
isig        <- Lens' TCState Signature -> TCMT IO Signature
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stImports
      RemoteMetaStore
metas       <- Lens' TCState RemoteMetaStore -> TCMT IO RemoteMetaStore
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (RemoteMetaStore -> f RemoteMetaStore) -> TCState -> f TCState
Lens' TCState RemoteMetaStore
stImportedMetaStore
      Map SomeBuiltin (Builtin PrimFun)
ibuiltin    <- Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
-> TCMT IO (Map SomeBuiltin (Builtin PrimFun))
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Map SomeBuiltin (Builtin PrimFun)
 -> f (Map SomeBuiltin (Builtin PrimFun)))
-> TCState -> f TCState
Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
stImportedBuiltins
      DisplayForms
display     <- Lens' TCState DisplayForms -> TCMT IO DisplayForms
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (DisplayForms -> f DisplayForms) -> TCState -> f TCState
Lens' TCState DisplayForms
stImportsDisplayForms
      UserWarnings
userwarn    <- Lens' TCState UserWarnings -> TCMT IO UserWarnings
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (UserWarnings -> f UserWarnings) -> TCState -> f TCState
Lens' TCState UserWarnings
stImportedUserWarnings
      Set QName
partialdefs <- Lens' TCState (Set QName) -> TCMT IO (Set QName)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Set QName -> f (Set QName)) -> TCState -> f TCState
Lens' TCState (Set QName)
stImportedPartialDefs
      Map OpaqueId OpaqueBlock
opaqueblk   <- Lens' TCState (Map OpaqueId OpaqueBlock)
-> TCMT IO (Map OpaqueId OpaqueBlock)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Map OpaqueId OpaqueBlock -> f (Map OpaqueId OpaqueBlock))
-> TCState -> f TCState
Lens' TCState (Map OpaqueId OpaqueBlock)
stOpaqueBlocks
      Map QName OpaqueId
opaqueid    <- Lens' TCState (Map QName OpaqueId) -> TCMT IO (Map QName OpaqueId)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Map QName OpaqueId -> f (Map QName OpaqueId))
-> TCState -> f TCState
Lens' TCState (Map QName OpaqueId)
stOpaqueIds
      PatternSynDefns
ipatsyns <- TCMT IO PatternSynDefns
forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getPatternSynImports
      InteractionOutputCallback
ho       <- TCMT IO InteractionOutputCallback
forall (m :: * -> *). ReadTCState m => m InteractionOutputCallback
getInteractionOutputCallback
      -- 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.
      (ModuleInfo
mi, ModuleToSource
newModToSource, VisitedModules
newDecodedModules) <- ((TCErr -> TCMT IO (ModuleInfo, ModuleToSource, VisitedModules))
-> ((ModuleInfo, ModuleToSource, VisitedModules)
    -> TCMT IO (ModuleInfo, ModuleToSource, VisitedModules))
-> Either TCErr (ModuleInfo, ModuleToSource, VisitedModules)
-> TCMT IO (ModuleInfo, ModuleToSource, VisitedModules)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either TCErr -> TCMT IO (ModuleInfo, ModuleToSource, VisitedModules)
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (ModuleInfo, ModuleToSource, VisitedModules)
-> TCMT IO (ModuleInfo, ModuleToSource, VisitedModules)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either TCErr (ModuleInfo, ModuleToSource, VisitedModules)
 -> TCMT IO (ModuleInfo, ModuleToSource, VisitedModules))
-> TCMT
     IO (Either TCErr (ModuleInfo, ModuleToSource, VisitedModules))
-> TCMT IO (ModuleInfo, ModuleToSource, VisitedModules)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) (TCMT
   IO (Either TCErr (ModuleInfo, ModuleToSource, VisitedModules))
 -> TCMT IO (ModuleInfo, ModuleToSource, VisitedModules))
-> TCMT
     IO (Either TCErr (ModuleInfo, ModuleToSource, VisitedModules))
-> TCMT IO (ModuleInfo, ModuleToSource, VisitedModules)
forall a b. (a -> b) -> a -> b
$
           TCMT IO (Either TCErr (ModuleInfo, ModuleToSource, VisitedModules))
-> TCMT
     IO (Either TCErr (ModuleInfo, ModuleToSource, VisitedModules))
forall (m :: * -> *) a.
(MonadTCState m, ReadTCState m) =>
m a -> m a
withoutCache (TCMT
   IO (Either TCErr (ModuleInfo, ModuleToSource, VisitedModules))
 -> TCMT
      IO (Either TCErr (ModuleInfo, ModuleToSource, VisitedModules)))
-> TCMT
     IO (Either TCErr (ModuleInfo, ModuleToSource, VisitedModules))
-> TCMT
     IO (Either TCErr (ModuleInfo, ModuleToSource, VisitedModules))
forall a b. (a -> b) -> a -> b
$
           -- The cache should not be used for an imported module, and it
           -- should be restored after the module has been type-checked
           TCMT IO (ModuleInfo, ModuleToSource, VisitedModules)
-> TCMT
     IO (Either TCErr (ModuleInfo, ModuleToSource, VisitedModules))
forall a. TCM a -> TCM (Either TCErr a)
freshTCM (TCMT IO (ModuleInfo, ModuleToSource, VisitedModules)
 -> TCMT
      IO (Either TCErr (ModuleInfo, ModuleToSource, VisitedModules)))
-> TCMT IO (ModuleInfo, ModuleToSource, VisitedModules)
-> TCMT
     IO (Either TCErr (ModuleInfo, ModuleToSource, VisitedModules))
forall a b. (a -> b) -> a -> b
$
             [TopLevelModuleName]
-> TCMT IO (ModuleInfo, ModuleToSource, VisitedModules)
-> TCMT IO (ModuleInfo, ModuleToSource, VisitedModules)
forall a. [TopLevelModuleName] -> TCM a -> TCM a
withImportPath [TopLevelModuleName]
ms (TCMT IO (ModuleInfo, ModuleToSource, VisitedModules)
 -> TCMT IO (ModuleInfo, ModuleToSource, VisitedModules))
-> TCMT IO (ModuleInfo, ModuleToSource, VisitedModules)
-> TCMT IO (ModuleInfo, ModuleToSource, VisitedModules)
forall a b. (a -> b) -> a -> b
$
             (TCEnv -> TCEnv)
-> TCMT IO (ModuleInfo, ModuleToSource, VisitedModules)
-> TCMT IO (ModuleInfo, ModuleToSource, VisitedModules)
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\TCEnv
e -> TCEnv
e
                              -- Andreas, 2014-08-18:
                              -- Preserve the range of import statement
                              -- for reporting termination errors in
                              -- imported modules:
                            { envRange              = range
                            , envCall               = call
                            }) (TCMT IO (ModuleInfo, ModuleToSource, VisitedModules)
 -> TCMT IO (ModuleInfo, ModuleToSource, VisitedModules))
-> TCMT IO (ModuleInfo, ModuleToSource, VisitedModules)
-> TCMT IO (ModuleInfo, ModuleToSource, VisitedModules)
forall a b. (a -> b) -> a -> b
$ do
               VisitedModules -> TCM ()
setDecodedModules VisitedModules
ds
               CommandLineOptions -> TCM ()
setCommandLineOptions CommandLineOptions
opts
               InteractionOutputCallback -> TCM ()
setInteractionOutputCallback InteractionOutputCallback
ho
               (ModuleToSource -> f ModuleToSource) -> TCState -> f TCState
Lens' TCState ModuleToSource
stModuleToSource Lens' TCState ModuleToSource -> ModuleToSource -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens` ModuleToSource
mf
               VisitedModules -> TCM ()
setVisitedModules VisitedModules
vs
               Signature
-> RemoteMetaStore
-> Map SomeBuiltin (Builtin PrimFun)
-> PatternSynDefns
-> DisplayForms
-> UserWarnings
-> Set QName
-> Set TCWarning
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> TCM ()
addImportedThings Signature
isig RemoteMetaStore
metas Map SomeBuiltin (Builtin PrimFun)
ibuiltin PatternSynDefns
ipatsyns DisplayForms
display
                 UserWarnings
userwarn Set QName
partialdefs Set TCWarning
forall a. Null a => a
empty Map OpaqueId OpaqueBlock
opaqueblk Map QName OpaqueId
opaqueid

               ModuleInfo
r  <- TopLevelModuleName
-> SourceFile -> MainInterface -> Maybe Source -> TCM ModuleInfo
createInterface TopLevelModuleName
x SourceFile
file MainInterface
NotMainInterface Maybe Source
msrc
               ModuleToSource
mf' <- Lens' TCState ModuleToSource -> TCMT IO ModuleToSource
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (ModuleToSource -> f ModuleToSource) -> TCState -> f TCState
Lens' TCState ModuleToSource
stModuleToSource
               VisitedModules
ds' <- TCMT IO VisitedModules
getDecodedModules
               (ModuleInfo, ModuleToSource, VisitedModules)
-> TCMT IO (ModuleInfo, ModuleToSource, VisitedModules)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ModuleInfo
r, ModuleToSource
mf', VisitedModules
ds')

      (ModuleToSource -> f ModuleToSource) -> TCState -> f TCState
Lens' TCState ModuleToSource
stModuleToSource Lens' TCState ModuleToSource -> ModuleToSource -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens` ModuleToSource
newModToSource
      VisitedModules -> TCM ()
setDecodedModules VisitedModules
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.)
      Either [Char] ModuleInfo
validated <- ExceptT [Char] (TCMT IO) ModuleInfo
-> TCMT IO (Either [Char] ModuleInfo)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT [Char] (TCMT IO) ModuleInfo
 -> TCMT IO (Either [Char] ModuleInfo))
-> ExceptT [Char] (TCMT IO) ModuleInfo
-> TCMT IO (Either [Char] ModuleInfo)
forall a b. (a -> b) -> a -> b
$ SourceFile -> ModuleInfo -> ExceptT [Char] (TCMT IO) ModuleInfo
loadDecodedModule SourceFile
file ModuleInfo
mi

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

      ([Char] -> TCM ModuleInfo)
-> (ModuleInfo -> TCM ModuleInfo)
-> Either [Char] ModuleInfo
-> TCM ModuleInfo
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either [Char] -> TCM ModuleInfo
recheckOnError ModuleInfo -> TCM ModuleInfo
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Either [Char] ModuleInfo
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 -> Maybe [Char] -> TCM ()
chaseMsg [Char]
kind TopLevelModuleName
x Maybe [Char]
file = do
  [Char]
indentation <- (Int -> Char -> [Char]
forall a. Int -> a -> [a]
`replicate` Char
' ') (Int -> [Char]) -> TCMT IO Int -> TCMT IO [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Int) -> TCMT IO Int
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC (Int -> Int
forall a. Enum a => a -> a
pred (Int -> Int) -> (TCEnv -> Int) -> TCEnv -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TopLevelModuleName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([TopLevelModuleName] -> Int)
-> (TCEnv -> [TopLevelModuleName]) -> TCEnv -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEnv -> [TopLevelModuleName]
envImportPath)
  Integer
traceImports <- CommandLineOptions -> Integer
optTraceImports (CommandLineOptions -> Integer)
-> TCMT IO CommandLineOptions -> TCMT IO Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  let maybeFile :: [Char]
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 :: Int
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
  [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
alwaysReportSLn [Char]
"import.chase" Int
vLvl ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ [Char]
indentation, [Char]
kind, [Char]
" ", TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
x, [Char]
maybeFile ]

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

highlightFromInterface
  :: Interface
  -> SourceFile
     -- ^ The corresponding file.
  -> TCM ()
highlightFromInterface :: Interface -> SourceFile -> TCM ()
highlightFromInterface Interface
i SourceFile
sf = do
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"import.iface" Int
5 do
    AbsolutePath
file <- SourceFile -> TCMT IO AbsolutePath
forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
srcFilePath SourceFile
sf
    [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
P.text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Generating syntax info for " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ AbsolutePath -> [Char]
filePath AbsolutePath
file [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++
      [Char]
" (read from interface)."
  RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
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
    -- Decode the interface file
    (ByteString
s, IO ()
close) <- IO (ByteString, IO ()) -> TCMT IO (ByteString, IO ())
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ByteString, IO ()) -> TCMT IO (ByteString, IO ()))
-> IO (ByteString, IO ()) -> TCMT IO (ByteString, IO ())
forall a b. (a -> b) -> a -> b
$ [Char] -> IO (ByteString, IO ())
readBinaryFile' [Char]
ifp
    do  Maybe Interface
mi <- IO (Maybe Interface) -> TCMT IO (Maybe Interface)
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe Interface) -> TCMT IO (Maybe Interface))
-> (Maybe Interface -> IO (Maybe Interface))
-> Maybe Interface
-> TCMT IO (Maybe Interface)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Interface -> IO (Maybe Interface)
forall a. a -> IO a
E.evaluate (Maybe Interface -> TCMT IO (Maybe Interface))
-> TCMT IO (Maybe Interface) -> TCMT IO (Maybe Interface)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ByteString -> TCMT IO (Maybe Interface)
decodeInterface ByteString
s

        -- Close the file. Note
        -- ⑴ that evaluate ensures that i is evaluated to WHNF (before
        --   the next IO operation is executed), and
        -- ⑵ that decode returns Nothing if an error is encountered,
        -- so it is safe to close the file here.
        IO () -> TCM ()
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO ()
close

        Maybe Interface -> TCMT IO (Maybe Interface)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Interface -> TCMT IO (Maybe Interface))
-> Maybe Interface -> TCMT IO (Maybe Interface)
forall a b. (a -> b) -> a -> b
$ Interface -> Interface
constructIScope (Interface -> Interface) -> Maybe Interface -> Maybe Interface
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Interface
mi
      -- Catch exceptions and close
      TCMT IO (Maybe Interface)
-> (TCErr -> TCMT IO (Maybe Interface))
-> TCMT IO (Maybe 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 -> IO () -> TCM ()
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO ()
close TCM () -> TCMT IO (Maybe Interface) -> TCMT IO (Maybe Interface)
forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TCErr -> TCMT IO (Maybe Interface)
forall {a}. TCErr -> TCMT IO (Maybe a)
handler TCErr
e
  -- Catch exceptions
  TCMT IO (Maybe Interface)
-> (TCErr -> TCMT IO (Maybe Interface))
-> TCMT IO (Maybe 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 -> TCMT IO (Maybe Interface)
forall {a}. TCErr -> TCMT IO (Maybe a)
handler
  where
    handler :: TCErr -> TCMT IO (Maybe a)
handler = \case
      IOException Maybe TCState
_ Range
_ IOException
e -> do
        [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
alwaysReportSLn [Char]
"" Int
0 ([Char] -> TCM ()) -> [Char] -> TCM ()
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 a -> TCMT IO (Maybe a)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
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 a)
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
e

-- | 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] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.write" Int
5  ([Char] -> TCM ()) -> [Char] -> TCM ()
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]
"."
    -- Andreas, 2015-07-13
    -- After QName memoization (AIM XXI), scope serialization might be cheap enough.
    -- -- Andreas, Makoto, 2014-10-18 AIM XX:
    -- -- iInsideScope is bloating the interface files, so we do not serialize it?
    -- i <- return $
    --   i { iInsideScope  = emptyScopeInfo
    --     }
    -- [Old: Andreas, 2016-02-02 this causes issue #1804, so don't do it:]
    -- Andreas, 2020-05-13, #1804, #4647: removed private declarations
    -- only when we actually write the interface.
    let
      filteredIface :: Interface
filteredIface = Interface
i { iInsideScope = withoutPrivates $ iInsideScope i }
    Interface
filteredIface <- Interface -> TCMT IO Interface
pruneTemporaryInstances Interface
filteredIface
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.write" Int
50 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$
      [Char]
"Writing interface file with hash " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Hash -> [Char]
forall a. Show a => a -> [Char]
show (Interface -> Hash
iFullHash Interface
filteredIface) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"."
    ByteString
encodedIface <- [Char] -> Interface -> TCM ByteString
encodeFile [Char]
fp Interface
filteredIface
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.write" Int
5 [Char]
"Wrote interface file."
    Interface -> Maybe Interface -> Interface
forall a. a -> Maybe a -> a
fromMaybe Interface
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Interface -> Interface)
-> TCMT IO (Maybe Interface) -> TCMT IO Interface
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Account (BenchPhase (TCMT IO))
-> TCMT IO (Maybe Interface) -> TCMT IO (Maybe Interface)
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Deserialization] (ByteString -> TCMT IO (Maybe Interface)
forall a. EmbPrj a => ByteString -> TCM (Maybe a)
decode ByteString
encodedIface))
  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] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
alwaysReportSLn [Char]
"" Int
1 ([Char] -> TCM ()) -> [Char] -> TCM ()
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]
"."
    IO () -> TCM ()
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
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
-> SourceFile -> MainInterface -> Maybe Source -> TCM ModuleInfo
createInterface TopLevelModuleName
mname sf :: SourceFile
sf@(SourceFile FileId
sfi) MainInterface
isMain Maybe Source
msrc = do
  AbsolutePath
file <- SourceFile -> TCMT IO AbsolutePath
forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
srcFilePath SourceFile
sf
  let fp :: [Char]
fp = AbsolutePath -> [Char]
filePath AbsolutePath
file
  let checkMsg :: [Char]
checkMsg = case MainInterface
isMain of
                   MainInterface Mode
ScopeCheck -> [Char]
"Reading "
                   MainInterface
_                        -> [Char]
"Checking"
      withMsgs :: TCM ModuleInfo -> TCM ModuleInfo
withMsgs = TCM () -> (() -> TCM ()) -> TCM ModuleInfo -> TCM ModuleInfo
forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_
       ([Char] -> TopLevelModuleName -> Maybe [Char] -> TCM ()
chaseMsg [Char]
checkMsg TopLevelModuleName
mname (Maybe [Char] -> TCM ()) -> Maybe [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
fp)
       (TCM () -> () -> TCM ()
forall a b. a -> b -> a
const (TCM () -> () -> TCM ()) -> TCM () -> () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do Set TCWarning
ws <- WhichWarnings -> TCMT IO (Set TCWarning)
forall (m :: * -> *).
(ReadTCState m, MonadWarning m, MonadTCM m) =>
WhichWarnings -> m (Set TCWarning)
getAllWarnings WhichWarnings
AllWarnings
                   let classified :: WarningsAndNonFatalErrors
classified = [TCWarning] -> WarningsAndNonFatalErrors
classifyWarnings ([TCWarning] -> WarningsAndNonFatalErrors)
-> [TCWarning] -> WarningsAndNonFatalErrors
forall a b. (a -> b) -> a -> b
$ Set TCWarning -> [TCWarning]
forall a. Set a -> [a]
Set.toAscList Set TCWarning
ws
                   TopLevelModuleName -> Set TCWarning -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
TopLevelModuleName -> Set TCWarning -> m ()
reportWarningsForModule TopLevelModuleName
mname (Set TCWarning -> TCM ()) -> Set TCWarning -> TCM ()
forall a b. (a -> b) -> a -> b
$ WarningsAndNonFatalErrors -> Set TCWarning
tcWarnings WarningsAndNonFatalErrors
classified
                   Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when (Set TCWarning -> Bool
forall a. Null a => a -> Bool
null (WarningsAndNonFatalErrors -> Set TCWarning
nonFatalErrors WarningsAndNonFatalErrors
classified)) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> TopLevelModuleName -> Maybe [Char] -> TCM ()
chaseMsg [Char]
"Finished" TopLevelModuleName
mname Maybe [Char]
forall a. Maybe a
Nothing)

  TCM ModuleInfo -> TCM ModuleInfo
withMsgs (TCM ModuleInfo -> TCM ModuleInfo)
-> TCM ModuleInfo -> TCM ModuleInfo
forall a b. (a -> b) -> a -> b
$
    Account (BenchPhase (TCMT IO)) -> TCM ModuleInfo -> TCM ModuleInfo
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [TopLevelModuleName -> Phase
Bench.TopModule TopLevelModuleName
mname] (TCM ModuleInfo -> TCM ModuleInfo)
-> TCM ModuleInfo -> TCM ModuleInfo
forall a b. (a -> b) -> a -> b
$
    (TCEnv -> TCEnv) -> TCM ModuleInfo -> TCM ModuleInfo
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envCurrentPath = Just sfi }) do

    let onlyScope :: Bool
onlyScope = MainInterface
isMain MainInterface -> MainInterface -> Bool
forall a. Eq a => a -> a -> Bool
== Mode -> MainInterface
MainInterface Mode
ScopeCheck

    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
5 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$
      [Char]
"Creating interface for " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
mname [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"..."
    [Char] -> Int -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"import.iface.create" Int
10 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      [Char]
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
      [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
10 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  visited: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
visited

    Source
src <- TCM Source -> (Source -> TCM Source) -> Maybe Source -> TCM Source
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (SourceFile -> TCM Source
parseSource SourceFile
sf) Source -> TCM Source
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Source
msrc

    AbsolutePath
srcPath <- SourceFile -> TCMT IO AbsolutePath
forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
srcFilePath (SourceFile -> TCMT IO AbsolutePath)
-> SourceFile -> TCMT IO AbsolutePath
forall a b. (a -> b) -> a -> b
$ Source -> SourceFile
srcOrigin Source
src

    HighlightingInfo
fileTokenInfo <- Account (BenchPhase (TCMT IO))
-> TCMT IO HighlightingInfo -> TCMT IO HighlightingInfo
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Highlighting] (TCMT IO HighlightingInfo -> TCMT IO HighlightingInfo)
-> TCMT IO HighlightingInfo -> TCMT IO HighlightingInfo
forall a b. (a -> b) -> a -> b
$
      RangeFile -> [Char] -> TCMT IO HighlightingInfo
generateTokenInfoFromSource
        (let !top :: TopLevelModuleName
top = Source -> TopLevelModuleName
srcModuleName Source
src in
         AbsolutePath -> Maybe TopLevelModuleName -> RangeFile
mkRangeFile AbsolutePath
srcPath (TopLevelModuleName -> Maybe TopLevelModuleName
forall a. a -> Maybe a
Just TopLevelModuleName
top))
        (Text -> [Char]
TL.unpack (Text -> [Char]) -> Text -> [Char]
forall a b. (a -> b) -> a -> b
$ Source -> Text
srcText Source
src)
    (HighlightingInfo -> f HighlightingInfo) -> TCState -> f TCState
Lens' TCState HighlightingInfo
stTokens Lens' TCState HighlightingInfo
-> (HighlightingInfo -> HighlightingInfo) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` (HighlightingInfo
fileTokenInfo HighlightingInfo -> HighlightingInfo -> HighlightingInfo
forall a. Semigroup a => a -> a -> a
<>)

    -- Only check consistency if not main (we check consistency for the main module in
    -- `typeCheckMain`.
    let checkConsistency :: Bool
checkConsistency | MainInterface{} <- MainInterface
isMain = Bool
False
                         | Bool
otherwise                 = Bool
True
    Bool -> Source -> TCM ()
setOptionsFromSourcePragmas Bool
checkConsistency Source
src
    Attributes -> TCM ()
checkAttributes (Source -> Attributes
srcAttributes Source
src)
    Maybe Int
syntactic <- PragmaOptions -> Maybe Int
optSyntacticEquality (PragmaOptions -> Maybe Int)
-> TCMT IO PragmaOptions -> TCMT IO (Maybe Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
    (TCEnv -> TCEnv) -> TCM ModuleInfo -> TCM ModuleInfo
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\TCEnv
env -> TCEnv
env { envSyntacticEqualityFuel = syntactic }) (TCM ModuleInfo -> TCM ModuleInfo)
-> TCM ModuleInfo -> TCM ModuleInfo
forall a b. (a -> b) -> a -> b
$ do

    [Char] -> Int -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"import.iface.create" Int
15 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      Int
nestingLevel      <- (TCEnv -> Int) -> TCMT IO Int
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC (Int -> Int
forall a. Enum a => a -> a
pred (Int -> Int) -> (TCEnv -> Int) -> TCEnv -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TopLevelModuleName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([TopLevelModuleName] -> Int)
-> (TCEnv -> [TopLevelModuleName]) -> TCEnv -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEnv -> [TopLevelModuleName]
envImportPath)
      HighlightingLevel
highlightingLevel <- (TCEnv -> HighlightingLevel) -> TCMT IO HighlightingLevel
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> HighlightingLevel
envHighlightingLevel
      [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
15 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines
        [ [Char]
"  nesting      level: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
nestingLevel
        , [Char]
"  highlighting level: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ HighlightingLevel -> [Char]
forall a. Show a => a -> [Char]
show HighlightingLevel
highlightingLevel
        ]

    -- Scope checking.
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
mname [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": Starting scope checking."
    TopLevelInfo
topLevel <- Account (BenchPhase (TCMT IO))
-> TCMT IO TopLevelInfo -> TCMT IO TopLevelInfo
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Scoping] (TCMT IO TopLevelInfo -> TCMT IO TopLevelInfo)
-> TCMT IO TopLevelInfo -> TCMT IO TopLevelInfo
forall a b. (a -> b) -> a -> b
$ do
      let topDecls :: [Declaration]
topDecls = Module -> [Declaration]
C.modDecls (Module -> [Declaration]) -> Module -> [Declaration]
forall a b. (a -> b) -> a -> b
$ Source -> Module
srcModule Source
src
      TopLevel [Declaration]
-> ScopeM (AbsOfCon (TopLevel [Declaration]))
forall c. ToAbstract c => c -> ScopeM (AbsOfCon c)
concreteToAbstract_ (SourceFile
-> TopLevelModuleName -> [Declaration] -> TopLevel [Declaration]
forall a. SourceFile -> TopLevelModuleName -> a -> TopLevel a
TopLevel (Source -> SourceFile
srcOrigin Source
src) TopLevelModuleName
mname [Declaration]
topDecls)
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
mname [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": Finished scope checking."

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

    -- Highlighting from scope checker.
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.highlight" Int
15 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
mname [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": Starting highlighting from scope."
    Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Highlighting] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      -- Generate and print approximate syntax highlighting info.
      HighlightingLevel -> TCM () -> TCM ()
forall (tcm :: * -> *).
MonadTCEnv tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting HighlightingInfo
fileTokenInfo
      HighlightingLevel -> Bool -> TCM () -> TCM ()
forall (tcm :: * -> *).
MonadTCEnv tcm =>
HighlightingLevel -> Bool -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIsOr HighlightingLevel
NonInteractive Bool
onlyScope (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        (Declaration -> TCM ()) -> [Declaration] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ Declaration
d -> Declaration -> Level -> Bool -> TCM ()
generateAndPrintSyntaxInfo Declaration
d Level
Partial Bool
onlyScope) [Declaration]
ds
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.highlight" Int
15 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
mname [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": Finished highlighting from scope."


    -- Type checking.

    -- Now that all the options are in we can check if caching should
    -- be on.
    TCM ()
forall (m :: * -> *).
(HasOptions m, MonadDebug m, MonadTCState m) =>
m ()
activateLoadedFileCache

    -- invalidate cache if pragmas change, TODO move
    TCM ()
forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
m ()
cachingStarts
    PragmaOptions
opts <- Lens' TCState PragmaOptions -> TCMT IO PragmaOptions
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
Lens' TCState PragmaOptions
stPragmaOptions
    Maybe (TypeCheckAction, PostScopeState)
me <- TCMT IO (Maybe (TypeCheckAction, PostScopeState))
forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
m (Maybe (TypeCheckAction, PostScopeState))
readFromCachedLog
    case Maybe (TypeCheckAction, PostScopeState)
me of
      Just (Pragmas PragmaOptions
opts', PostScopeState
_) | PragmaOptions
opts PragmaOptions -> PragmaOptions -> Bool
forall a. Eq a => a -> a -> Bool
== PragmaOptions
opts'
        -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Maybe (TypeCheckAction, PostScopeState)
_ -> do
        [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"cache" Int
10 ([Char] -> TCM ()) -> [Char] -> TCM ()
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)
        TCM ()
forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog
    TypeCheckAction -> TCM ()
forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
TypeCheckAction -> m ()
writeToCurrentLog (TypeCheckAction -> TCM ()) -> TypeCheckAction -> TCM ()
forall a b. (a -> b) -> a -> b
$ PragmaOptions -> TypeCheckAction
Pragmas PragmaOptions
opts

    if Bool
onlyScope
      then do
        [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
mname [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": Skipping type checking."
        TCM ()
forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cacheCurrentLog
      else do
        [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
mname [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": Starting type checking."
        Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Typing] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ (Declaration -> TCM ()) -> [Declaration] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Declaration -> TCM ()
checkDeclCached [Declaration]
ds TCM () -> TCM () -> TCM ()
forall a b. TCM a -> TCM b -> TCM a
`finally_` TCM ()
forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cacheCurrentLog
        [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
mname [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": 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

    TCM ()
unfreezeMetas

    -- Profiling: Count number of metas.
    ProfileOption -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Metas (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      MetaId
m <- TCMT IO MetaId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
      [Char] -> Integer -> TCM ()
forall (m :: * -> *).
MonadStatistics m =>
[Char] -> Integer -> m ()
tickN [Char]
"metas" (Hash -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (MetaId -> Hash
metaId MetaId
m))

    -- Highlighting from type checker.
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.highlight" Int
15 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
mname [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": Starting highlighting from type info."
    Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Highlighting] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do

      -- Move any remaining token highlighting to stSyntaxInfo.
      HighlightingInfo
toks <- Lens' TCState HighlightingInfo -> TCMT IO HighlightingInfo
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (HighlightingInfo -> f HighlightingInfo) -> TCState -> f TCState
Lens' TCState HighlightingInfo
stTokens
      HighlightingLevel -> TCM () -> TCM ()
forall (tcm :: * -> *).
MonadTCEnv tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting HighlightingInfo
toks
      (HighlightingInfo -> f HighlightingInfo) -> TCState -> f TCState
Lens' TCState HighlightingInfo
stTokens Lens' TCState HighlightingInfo -> HighlightingInfo -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens` HighlightingInfo
forall a. Monoid a => a
mempty

      -- Grabbing warnings and unsolved metas to highlight them
      Set TCWarning
warnings <- WhichWarnings -> TCMT IO (Set TCWarning)
forall (m :: * -> *).
(ReadTCState m, MonadWarning m, MonadTCM m) =>
WhichWarnings -> m (Set TCWarning)
getAllWarnings WhichWarnings
AllWarnings
      Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Set TCWarning -> Bool
forall a. Null a => a -> Bool
null Set TCWarning
warnings) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"import.iface.highlight" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"collected warnings: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> Set TCWarning -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Set TCWarning -> m Doc
prettyTCM Set TCWarning
warnings
      [TCWarning]
unsolved <- TCMT IO [TCWarning]
forall (m :: * -> *).
(ReadTCState m, MonadWarning m, MonadTCM m) =>
m [TCWarning]
getAllUnsolvedWarnings
      Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless ([TCWarning] -> Bool
forall a. Null a => a -> Bool
null [TCWarning]
unsolved) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"import.iface.highlight" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"collected unsolved: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> [TCWarning] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [TCWarning] -> m Doc
prettyTCM [TCWarning]
unsolved
      let warningInfo :: HighlightingInfo
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

      (HighlightingInfo -> f HighlightingInfo) -> TCState -> f TCState
Lens' TCState HighlightingInfo
stSyntaxInfo Lens' TCState HighlightingInfo
-> (HighlightingInfo -> HighlightingInfo) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` \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

      TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (CommandLineOptions -> Bool
optGenerateVimFile (CommandLineOptions -> Bool)
-> TCMT IO CommandLineOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        -- Generate Vim file.
        ScopeInfo -> TCM () -> TCM ()
forall (m :: * -> *) a. ReadTCState m => ScopeInfo -> m a -> m a
withScope_ ScopeInfo
scope (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> TCM ()
generateVimFile ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> [Char]
filePath (AbsolutePath -> [Char]) -> AbsolutePath -> [Char]
forall a b. (a -> b) -> a -> b
$ AbsolutePath
srcPath
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
15 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
mname [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": Finished highlighting from type info."

    ScopeInfo -> TCM ()
setScope ScopeInfo
scope
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"scope.top" Int
50 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"SCOPE " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ScopeInfo -> [Char]
forall a. Show a => a -> [Char]
show ScopeInfo
scope

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

    [MetaId]
openMetas <- TCMT IO [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas
    Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless ([MetaId] -> Bool
forall a. Null a => a -> Bool
null [MetaId]
openMetas) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.metas" Int
10 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
mname [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": We have unsolved metas."
      [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.metas" Int
10 ([Char] -> TCM ()) -> TCMT IO [Char] -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Goals -> TCMT IO [Char]
showGoals (Goals -> TCMT IO [Char]) -> TCMT IO Goals -> TCMT IO [Char]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Goals
getGoals

    HighlightingLevel -> TCM () -> TCM ()
forall (tcm :: * -> *).
MonadTCEnv tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive TCM ()
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
    Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (MainInterface -> Bool
includeStateChanges MainInterface
isMain) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
      -- Andreas, 2018-11-15, re issue #3393:
      -- We do not get here when checking the main module
      -- (then includeStateChanges is True).
      TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (PragmaOptions -> Bool
optAllowUnsolved (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) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
mname [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": Turning unsolved metas (if any) into postulates."
        ModuleName -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
withCurrentModule (ScopeInfo
scope ScopeInfo -> Lens' ScopeInfo ModuleName -> ModuleName
forall o i. o -> Lens' o i -> i
^. (ModuleName -> f ModuleName) -> ScopeInfo -> f ScopeInfo
Lens' ScopeInfo ModuleName
scopeCurrent) TCM ()
openMetasToPostulates
        -- Clear constraints as they might refer to what
        -- they think are open metas.
        (Constraints -> f Constraints) -> TCState -> f TCState
Lens' TCState Constraints
stAwakeConstraints    Lens' TCState Constraints -> Constraints -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens` []
        (Constraints -> f Constraints) -> TCState -> f TCState
Lens' TCState Constraints
stSleepingConstraints Lens' TCState Constraints -> Constraints -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens` []

    -- Serialization.
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
mname [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": Starting serialization."
    Interface
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 [BenchPhase (TCMT IO)
Phase
Bench.Serialization, BenchPhase (TCMT IO)
Phase
Bench.BuildInterface] (TCMT IO Interface -> TCMT IO Interface)
-> TCMT IO Interface -> TCMT IO Interface
forall a b. (a -> b) -> a -> b
$
      Source -> TopLevelInfo -> TCMT IO Interface
buildInterface Source
src TopLevelInfo
topLevel

    [Char] -> Int -> [[Char]] -> TCM ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> Int -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [[Char]] -> m ()
reportS [Char]
"tc.top" Int
101 ([[Char]] -> TCM ()) -> [[Char]] -> TCM ()
forall a b. (a -> b) -> a -> b
$
      [Char]
"Signature:" [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
:
      [ [[Char]] -> [Char]
unlines
          [ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
q
          , [Char]
"  type: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show (Definition -> Type
defType Definition
def)
          , [Char]
"  def:  " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe CompiledClauses -> [Char]
forall a. Show a => a -> [Char]
show Maybe CompiledClauses
cc
          ]
      | (QName
q, Definition
def) <- HashMap QName Definition -> [(QName, Definition)]
forall k v. HashMap k v -> [(k, v)]
HMap.toList (HashMap QName Definition -> [(QName, Definition)])
-> HashMap QName Definition -> [(QName, Definition)]
forall a b. (a -> b) -> a -> b
$ Interface -> Signature
iSignature Interface
i Signature
-> Lens' Signature (HashMap QName Definition)
-> HashMap QName Definition
forall o i. o -> Lens' o i -> i
^. (HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature
Lens' Signature (HashMap QName Definition)
sigDefinitions,
        Function{ funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Maybe CompiledClauses
cc } <- [Definition -> Defn
theDef Definition
def]
      ]
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
mname [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": Finished serialization."

    Set TCWarning
mallWarnings <- MainInterface -> WhichWarnings -> TCMT IO (Set TCWarning)
forall (m :: * -> *).
(ReadTCState m, MonadWarning m, MonadTCM m) =>
MainInterface -> WhichWarnings -> m (Set TCWarning)
getAllWarnings' MainInterface
isMain WhichWarnings
ErrorWarnings

    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
mname [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": Considering writing to interface file."
    Interface
finalIface <- Interface -> Interface
constructIScope (Interface -> Interface) -> TCMT IO Interface -> TCMT IO Interface
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> case (Set TCWarning -> Bool
forall a. Null a => a -> Bool
null Set TCWarning
mallWarnings, MainInterface
isMain) of
      (Bool
False, MainInterface
_) -> 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] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
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) -> do
        [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
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
True, MainInterface
_) -> 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] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
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.
        AbsolutePath
ifile <- HasCallStack => SourceFile -> TCMT IO AbsolutePath
SourceFile -> TCMT IO AbsolutePath
toIFile SourceFile
sf
        Interface
serializedIface <- AbsolutePath -> Interface -> TCMT IO Interface
writeInterface AbsolutePath
ifile Interface
i
        [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
mname [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": Finished writing to interface file."
        Interface -> TCMT IO Interface
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Interface
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.
    Maybe TopLevelModuleName -> Statistics -> TCM ()
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m, HasOptions m) =>
Maybe TopLevelModuleName -> Statistics -> m ()
printStatistics (TopLevelModuleName -> Maybe TopLevelModuleName
forall a. a -> Maybe a
Just TopLevelModuleName
mname) (Statistics -> TCM ()) -> TCMT IO Statistics -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Statistics
forall (m :: * -> *). ReadTCState m => m Statistics
getStatistics

    -- Get the statistics of the current module
    -- and add it to the accumulated statistics.
    Statistics
localStatistics <- TCMT IO Statistics
forall (m :: * -> *). ReadTCState m => m Statistics
getStatistics
    (Statistics -> f Statistics) -> TCState -> f TCState
Lens' TCState Statistics
lensAccumStatistics Lens' TCState Statistics -> (Statistics -> Statistics) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` (Integer -> Integer -> Integer)
-> Statistics -> Statistics -> Statistics
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) Statistics
localStatistics
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
25 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
mname [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": Added statistics to the accumulated statistics."

    Bool
isPrimitiveMod <- FileId -> TCMT IO Bool
forall (m :: * -> *). ReadTCState m => FileId -> m Bool
isPrimitiveModule FileId
sfi

    ModuleInfo -> TCM ModuleInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleInfo
      { miInterface :: Interface
miInterface = Interface
finalIface
      , miWarnings :: Set TCWarning
miWarnings = Set TCWarning
mallWarnings
      , miPrimitive :: Bool
miPrimitive = Bool
isPrimitiveMod
      , miMode :: ModuleCheckMode
miMode = MainInterface -> ModuleCheckMode
moduleCheckMode MainInterface
isMain
      }

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

getAllWarnings' :: (ReadTCState m, MonadWarning m, MonadTCM m) => MainInterface -> WhichWarnings -> m (Set TCWarning)
getAllWarnings' :: forall (m :: * -> *).
(ReadTCState m, MonadWarning m, MonadTCM m) =>
MainInterface -> WhichWarnings -> m (Set TCWarning)
getAllWarnings' (MainInterface Mode
_) = Set WarningName -> WhichWarnings -> m (Set TCWarning)
forall (m :: * -> *).
(ReadTCState 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 :: * -> *).
(ReadTCState 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 }

-- | 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] -> TCM ()
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).
    ![(TopLevelModuleName, Hash)]
mhs <- (TopLevelModuleName -> TCMT IO (TopLevelModuleName, Hash))
-> [TopLevelModuleName] -> TCMT IO [(TopLevelModuleName, 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
top -> (TopLevelModuleName
top,) (Hash -> (TopLevelModuleName, Hash))
-> TCM Hash -> TCMT IO (TopLevelModuleName, Hash)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TopLevelModuleName -> TCM Hash
moduleHash TopLevelModuleName
top) ([TopLevelModuleName] -> TCMT IO [(TopLevelModuleName, Hash)])
-> (Set TopLevelModuleName -> [TopLevelModuleName])
-> Set TopLevelModuleName
-> TCMT IO [(TopLevelModuleName, Hash)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set TopLevelModuleName -> [TopLevelModuleName]
forall a. Set a -> [a]
Set.toAscList (Set TopLevelModuleName -> TCMT IO [(TopLevelModuleName, Hash)])
-> TCMT IO (Set TopLevelModuleName)
-> TCMT IO [(TopLevelModuleName, Hash)]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Lens' TCState (Set TopLevelModuleName)
-> TCMT IO (Set TopLevelModuleName)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Set TopLevelModuleName -> f (Set TopLevelModuleName))
-> TCState -> f TCState
Lens' TCState (Set TopLevelModuleName)
stImportedModules
    !Map Text ForeignCodeStack
foreignCode <- Lens' TCState (Map Text ForeignCodeStack)
-> TCMT IO (Map Text ForeignCodeStack)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Map Text ForeignCodeStack -> f (Map Text ForeignCodeStack))
-> TCState -> f TCState
Lens' TCState (Map Text ForeignCodeStack)
stForeignCode

    let !scope :: ScopeInfo
scope = TopLevelInfo -> ScopeInfo
topLevelScope TopLevelInfo
topLevel

    (!RemoteMetaStore
solvedMetas, !HashMap QName Definition
definitions, !DisplayForms
displayForms) <- ScopeInfo
-> TCM (RemoteMetaStore, HashMap QName Definition, DisplayForms)
eliminateDeadCode ScopeInfo
scope
    !Signature
sig <- Lens' Signature (HashMap QName Definition)
-> LensSet Signature (HashMap QName Definition)
forall o i. Lens' o i -> LensSet o i
set (HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature
Lens' Signature (HashMap QName Definition)
sigDefinitions HashMap QName Definition
definitions (Signature -> Signature) -> TCMT IO Signature -> TCMT IO Signature
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Signature
forall (m :: * -> *). ReadTCState m => m Signature
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.
    !PatternSynDefns
patsyns <- PatternSynDefns -> PatternSynDefns
forall a. KillRange a => KillRangeT a
killRange (PatternSynDefns -> PatternSynDefns)
-> TCMT IO PatternSynDefns -> TCMT IO PatternSynDefns
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PatternSynDefns
forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getPatternSyns

    !UserWarnings
userwarns   <- Lens' TCState UserWarnings -> TCMT IO UserWarnings
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (UserWarnings -> f UserWarnings) -> TCState -> f TCState
Lens' TCState UserWarnings
stLocalUserWarnings
    !Maybe Text
importwarn  <- Lens' TCState (Maybe Text) -> TCMT IO (Maybe Text)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Maybe Text -> f (Maybe Text)) -> TCState -> f TCState
Lens' TCState (Maybe Text)
stWarningOnImport
    !HighlightingInfo
syntaxInfo  <- Lens' TCState HighlightingInfo -> TCMT IO HighlightingInfo
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (HighlightingInfo -> f HighlightingInfo) -> TCState -> f TCState
Lens' TCState HighlightingInfo
stSyntaxInfo
    !PragmaOptions
optionsUsed <- Lens' TCState PragmaOptions -> TCMT IO PragmaOptions
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
Lens' TCState PragmaOptions
stPragmaOptions
    !Set QName
partialDefs <- Lens' TCState (Set QName) -> TCMT IO (Set QName)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Set QName -> f (Set QName)) -> TCState -> f TCState
Lens' TCState (Set QName)
stLocalPartialDefs

    -- Only serialise the opaque blocks actually defined in this
    -- top-level module.
    !Map OpaqueId OpaqueBlock
opaqueBlocks' <- Lens' TCState (Map OpaqueId OpaqueBlock)
-> TCMT IO (Map OpaqueId OpaqueBlock)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Map OpaqueId OpaqueBlock -> f (Map OpaqueId OpaqueBlock))
-> TCState -> f TCState
Lens' TCState (Map OpaqueId OpaqueBlock)
stOpaqueBlocks
    !Map QName OpaqueId
opaqueIds' <- Lens' TCState (Map QName OpaqueId) -> TCMT IO (Map QName OpaqueId)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Map QName OpaqueId -> f (Map QName OpaqueId))
-> TCState -> f TCState
Lens' TCState (Map QName OpaqueId)
stOpaqueIds
    let
      !mh :: ModuleNameHash
mh = TopLevelModuleName -> ModuleNameHash
forall range. TopLevelModuleName' range -> ModuleNameHash
moduleNameId (Source -> TopLevelModuleName
srcModuleName Source
src)
      !opaqueBlocks :: Map OpaqueId OpaqueBlock
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 -> Bool
isLocal QName
qnm = case Name -> NameId
nameId (QName -> Name
qnameName QName
qnm) of
        NameId Hash
_ ModuleNameHash
mh' -> ModuleNameHash
mh' ModuleNameHash -> ModuleNameHash -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleNameHash
mh
      !opaqueIds :: Map QName OpaqueId
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'

    !Map SomeBuiltin (Builtin (PrimitiveId, QName))
builtin  <- (SomeBuiltin -> Builtin PrimFun -> Builtin (PrimitiveId, QName))
-> Map SomeBuiltin (Builtin PrimFun)
-> Map SomeBuiltin (Builtin (PrimitiveId, QName))
forall k a b. (k -> a -> b) -> Map k a -> Map k b
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) (Map SomeBuiltin (Builtin PrimFun)
 -> Map SomeBuiltin (Builtin (PrimitiveId, QName)))
-> TCMT IO (Map SomeBuiltin (Builtin PrimFun))
-> TCMT IO (Map SomeBuiltin (Builtin (PrimitiveId, QName)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
-> TCMT IO (Map SomeBuiltin (Builtin PrimFun))
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Map SomeBuiltin (Builtin PrimFun)
 -> f (Map SomeBuiltin (Builtin PrimFun)))
-> TCState -> f TCState
Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
stLocalBuiltins
    !Set TCWarning
warnings <- (TCWarning -> Bool) -> Set TCWarning -> Set TCWarning
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (WarningName -> Bool
isSourceCodeWarning (WarningName -> Bool)
-> (TCWarning -> WarningName) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Warning -> WarningName
warningName (Warning -> WarningName)
-> (TCWarning -> Warning) -> TCWarning -> WarningName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning) (Set TCWarning -> Set TCWarning)
-> TCMT IO (Set TCWarning) -> TCMT IO (Set TCWarning)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WhichWarnings -> TCMT IO (Set TCWarning)
forall (m :: * -> *).
(ReadTCState m, MonadWarning m, MonadTCM m) =>
WhichWarnings -> m (Set TCWarning)
getAllWarnings WhichWarnings
AllWarnings

    let !i :: Interface
i = Interface
          { iSourceHash :: Hash
iSourceHash           = Text -> Hash
hashText Text
source
          , iSource :: Text
iSource               = Text
source
          , iFileType :: FileType
iFileType             = FileType
fileType
          , iImportedModules :: [(TopLevelModuleName, Hash)]
iImportedModules      = [(TopLevelModuleName, Hash)]
mhs
          , iModuleName :: ModuleName
iModuleName           = ModuleName
mname
          , iTopLevelModuleName :: TopLevelModuleName
iTopLevelModuleName   = Source -> TopLevelModuleName
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 Text
iImportWarning        = Maybe Text
importwarn
          , iBuiltin :: Map SomeBuiltin (Builtin (PrimitiveId, QName))
iBuiltin              = Map SomeBuiltin (Builtin (PrimitiveId, QName))
builtin
          , iForeignCode :: Map Text ForeignCodeStack
iForeignCode          = Map Text 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
iWarnings             = 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
          }
    !Interface
i <-
      TCMT IO Bool
-> TCMT IO Interface -> TCMT IO Interface -> TCMT IO Interface
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (PragmaOptions -> Bool
optSaveMetas (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)
        (Interface -> TCMT IO Interface
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Interface
i)
        (do [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
7
              [Char]
"  instantiating all metavariables in interface"
            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.InterfaceInstantiateFull] (TCMT IO Interface -> TCMT IO Interface)
-> TCMT IO Interface -> TCMT IO Interface
forall a b. (a -> b) -> a -> b
$ ReduceM Interface -> TCMT IO Interface
forall a. ReduceM a -> TCMT IO a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (ReduceM Interface -> TCMT IO Interface)
-> ReduceM Interface -> TCMT IO Interface
forall a b. (a -> b) -> a -> b
$ Interface -> ReduceM Interface
forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Interface
i)
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
7 [Char]
"  interface complete"
    Interface -> TCMT IO Interface
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Interface
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
  (ByteString
s, IO ()
close) <- [Char] -> IO (ByteString, IO ())
readBinaryFile' [Char]
ifile
  let hs :: Maybe (Hash, Hash)
hs = ByteString -> Maybe (Hash, Hash)
decodeHashes ByteString
s
  Hash -> ((Hash, Hash) -> Hash) -> Maybe (Hash, Hash) -> Hash
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Hash
0 ((Hash -> Hash -> Hash) -> (Hash, Hash) -> Hash
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Hash -> Hash -> Hash
forall a. Num a => a -> a -> a
(+)) Maybe (Hash, Hash)
hs Hash -> IO () -> IO ()
forall a b. a -> b -> b
`seq` IO ()
close
  Maybe (Hash, Hash) -> IO (Maybe (Hash, Hash))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Hash, Hash)
hs

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