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

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

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

import Prelude hiding (null)

import Control.Monad               ( forM, forM_, void )
import Control.Monad.Except
import Control.Monad.IO.Class      ( MonadIO(..) )
import Control.Monad.State
import Control.Monad.Trans.Maybe
import qualified Control.Exception as E

#if __GLASGOW_HASKELL__ < 808
import Control.Monad.Fail (MonadFail)
#endif

import Data.Either
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.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.Parser
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.Syntax.TopLevelModuleName
import Agda.Syntax.Translation.ConcreteToAbstract as CToA

import Agda.TypeChecking.Errors
import Agda.TypeChecking.Warnings hiding (warnings)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Rewriting.Confluence ( checkConfluenceOfRules )
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 Agda.Interaction.Highlighting.Precise  ( 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.FileName
import Agda.Utils.Lens
import Agda.Utils.Maybe
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.IO.Binary
import Agda.Syntax.Common.Pretty hiding (Mode)
import qualified Agda.Utils.ProfileOptions as Profile
import Agda.Utils.Hash
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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
sourceFile@(SourceFile AbsolutePath
f) = forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.Parsing] forall a b. (a -> b) -> a -> b
$ do
  (Text
source, FileType
fileType, Module
parsedMod, Attributes
attrs, TopLevelModuleName
parsedModName) <- mdo
    -- This piece of code uses mdo because the top-level module name
    -- (parsedModName) is obtained from the parser's result, but it is
    -- also used by the parser.
    let rf :: RangeFile
rf = AbsolutePath -> Maybe TopLevelModuleName -> RangeFile
mkRangeFile AbsolutePath
f (forall a. a -> Maybe a
Just TopLevelModuleName
parsedModName)
    Text
source                         <- forall a. PM a -> TCM a
runPM forall a b. (a -> b) -> a -> b
$ RangeFile -> PM Text
readFilePM RangeFile
rf
    ((Module
parsedMod, Attributes
attrs), FileType
fileType) <- forall a. PM a -> TCM a
runPM forall a b. (a -> b) -> a -> b
$
                                      forall a.
Show a =>
Parser a -> RangeFile -> [Char] -> PM ((a, Attributes), FileType)
parseFile Parser Module
moduleParser RangeFile
rf forall a b. (a -> b) -> a -> b
$
                                      Text -> [Char]
TL.unpack Text
source
    TopLevelModuleName
parsedModName                  <- AbsolutePath -> Module -> TCM TopLevelModuleName
moduleName AbsolutePath
f Module
parsedMod
    forall (m :: * -> *) a. Monad m => a -> m a
return (Text
source, FileType
fileType, Module
parsedMod, Attributes
attrs, TopLevelModuleName
parsedModName)
  [AgdaLibFile]
libs <- AbsolutePath -> TopLevelModuleName -> TCM [AgdaLibFile]
getAgdaLibFiles AbsolutePath
f TopLevelModuleName
parsedModName
  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
    }

srcDefaultPragmas :: Source -> [OptionsPragma]
srcDefaultPragmas :: Source -> [OptionsPragma]
srcDefaultPragmas Source
src = 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.
setOptionsFromSourcePragmas :: Source -> TCM ()
setOptionsFromSourcePragmas :: Source -> TCM ()
setOptionsFromSourcePragmas Source
src = do
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ OptionsPragma -> TCM ()
setOptionsFromPragma (Source -> [OptionsPragma]
srcDefaultPragmas Source
src)
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ OptionsPragma -> TCM ()
setOptionsFromPragma (Source -> [OptionsPragma]
srcFilePragmas    Source
src)

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

data Mode
  = ScopeCheck
  | TypeCheck
  deriving (Mode -> Mode -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Mode -> Mode -> Bool
$c/= :: Mode -> Mode -> Bool
== :: Mode -> Mode -> Bool
$c== :: Mode -> Mode -> Bool
Eq, Int -> Mode -> ShowS
[Mode] -> ShowS
Mode -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Mode] -> ShowS
$cshowList :: [Mode] -> ShowS
show :: Mode -> [Char]
$cshow :: Mode -> [Char]
showsPrec :: Int -> Mode -> ShowS
$cshowsPrec :: Int -> 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MainInterface -> MainInterface -> Bool
$c/= :: MainInterface -> MainInterface -> Bool
== :: MainInterface -> MainInterface -> Bool
$c== :: MainInterface -> MainInterface -> Bool
Eq, Int -> MainInterface -> ShowS
[MainInterface] -> ShowS
MainInterface -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [MainInterface] -> ShowS
$cshowList :: [MainInterface] -> ShowS
show :: MainInterface -> [Char]
$cshow :: MainInterface -> [Char]
showsPrec :: Int -> MainInterface -> ShowS
$cshowsPrec :: Int -> 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 = forall k a. Map k a -> [(k, a)]
Map.toAscList forall a b. (a -> b) -> a -> b
$ Interface -> BuiltinThings (PrimitiveId, QName)
iBuiltin Interface
i
        primOrBi :: (a, Builtin a) -> Either a (a, Builtin pf)
primOrBi = \case
          (a
_, Prim a
x)                     -> forall a b. a -> Either a b
Left a
x
          (a
x, Builtin Term
t)                  -> forall a b. b -> Either a b
Right (a
x, forall pf. Term -> Builtin pf
Builtin Term
t)
          (a
x, BuiltinRewriteRelations Set QName
xs) -> forall a b. b -> Either a b
Right (a
x, forall pf. Set QName -> Builtin pf
BuiltinRewriteRelations Set QName
xs)
        ([(PrimitiveId, QName)]
prim, [(SomeBuiltin, Builtin PrimFun)]
bi') = forall a b. [Either a b] -> ([a], [b])
partitionEithers forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall {a} {a} {pf}. (a, Builtin a) -> Either a (a, Builtin pf)
primOrBi [(SomeBuiltin, Builtin (PrimitiveId, QName))]
builtin
        bi :: Map SomeBuiltin (Builtin PrimFun)
bi      = forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList [(SomeBuiltin, Builtin PrimFun)]
bi'
        warns :: [TCWarning]
warns   = Interface -> [TCWarning]
iWarnings Interface
i
    Map SomeBuiltin (Builtin PrimFun)
bs <- forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC TCState -> Map SomeBuiltin (Builtin PrimFun)
stBuiltinThings
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.merge" Int
10 [Char]
"Merging interface"
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.merge" Int
20 forall a b. (a -> b) -> a -> b
$
      [Char]
"  Current builtins " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall k a. Map k a -> [k]
Map.keys Map SomeBuiltin (Builtin PrimFun)
bs) forall a. [a] -> [a] -> [a]
++ [Char]
"\n" forall a. [a] -> [a] -> [a]
++
      [Char]
"  New builtins     " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (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 forall a. Eq a => a -> a -> Bool
== Term
y    = forall (m :: * -> *) a. Monad m => a -> m a
return ()
              | Bool
otherwise = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError 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) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
        check SomeBuiltin
_ Builtin pf
_ Builtin pf
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
    forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ forall a b. (a -> b) -> a -> b
$ forall k a b c.
Ord k =>
(k -> a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWithKey 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
-> Map QName Text
-> Set QName
-> [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 -> Map QName Text
iUserWarnings Interface
i)
      (Interface -> Set QName
iPartialDefs Interface
i)
      [TCWarning]
warns
      (Interface -> Map OpaqueId OpaqueBlock
iOpaqueBlocks Interface
i)
      (Interface -> Map QName OpaqueId
iOpaqueNames Interface
i)
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.merge" Int
20 forall a b. (a -> b) -> a -> b
$
      [Char]
"  Rebinding primitives " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [(PrimitiveId, QName)]
prim
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (PrimitiveId, QName) -> TCM ()
rebind [(PrimitiveId, QName)]
prim
    forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (PragmaOptions -> Maybe ConfluenceCheck
optConfluenceCheck forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) forall a b. (a -> b) -> a -> b
$ \ConfluenceCheck
confChk -> do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.confluence" Int
20 forall a b. (a -> b) -> a -> b
$ [Char]
"  Checking confluence of imported rewrite rules"
      ConfluenceCheck -> [RewriteRule] -> TCM ()
checkConfluenceOfRules ConfluenceCheck
confChk forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall k v. HashMap k v -> [v]
HMap.elems forall a b. (a -> b) -> a -> b
$ Signature
sig forall o i. o -> Lens' o i -> i
^. Lens' Signature (HashMap QName [RewriteRule])
sigRewriteRules
    where
        rebind :: (PrimitiveId, QName) -> TCM ()
rebind (PrimitiveId
x, QName
q) = do
            PrimImpl Type
_ PrimFun
pf <- PrimitiveId -> TCM PrimitiveImpl
lookupPrimitiveFunction PrimitiveId
x
            Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
stImportedBuiltins forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
x) (forall pf. pf -> Builtin pf
Prim PrimFun
pf{ primFunName :: QName
primFunName = QName
q })

addImportedThings
  :: Signature
  -> RemoteMetaStore
  -> BuiltinThings PrimFun
  -> A.PatternSynDefns
  -> DisplayForms
  -> Map A.QName Text      -- ^ Imported user warnings
  -> Set QName             -- ^ Name of imported definitions which are partial
  -> [TCWarning]
  -> Map OpaqueId OpaqueBlock
  -> Map QName OpaqueId
  -> TCM ()
addImportedThings :: Signature
-> RemoteMetaStore
-> Map SomeBuiltin (Builtin PrimFun)
-> PatternSynDefns
-> DisplayForms
-> Map QName Text
-> Set QName
-> [TCWarning]
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> TCM ()
addImportedThings Signature
isig RemoteMetaStore
metas Map SomeBuiltin (Builtin PrimFun)
ibuiltin PatternSynDefns
patsyns DisplayForms
display Map QName Text
userwarn
                  Set QName
partialdefs [TCWarning]
warnings Map OpaqueId OpaqueBlock
oblock Map QName OpaqueId
oid = do
  Lens' TCState Signature
stImports              forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` \ Signature
imp -> [Signature] -> Signature
unionSignatures [Signature
imp, Signature
isig]
  Lens' TCState RemoteMetaStore
stImportedMetaStore    forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` forall k v.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k v -> HashMap k v
HMap.union RemoteMetaStore
metas
  Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
stImportedBuiltins     forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` \ Map SomeBuiltin (Builtin PrimFun)
imp -> 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
  Lens' TCState (Map QName Text)
stImportedUserWarnings forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` \ Map QName Text
imp -> forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map QName Text
imp Map QName Text
userwarn
  Lens' TCState (Set QName)
stImportedPartialDefs  forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` \ Set QName
imp -> forall a. Ord a => Set a -> Set a -> Set a
Set.union Set QName
imp Set QName
partialdefs
  Lens' TCState PatternSynDefns
stPatternSynImports    forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` \ PatternSynDefns
imp -> forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union PatternSynDefns
imp PatternSynDefns
patsyns
  Lens' TCState DisplayForms
stImportedDisplayForms forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` \ DisplayForms
imp -> forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HMap.unionWith forall a. [a] -> [a] -> [a]
(++) DisplayForms
imp DisplayForms
display
  Lens' TCState [TCWarning]
stTCWarnings           forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` \ [TCWarning]
imp -> [TCWarning]
imp forall a. Eq a => [a] -> [a] -> [a]
`List.union` [TCWarning]
warnings
  Lens' TCState (Map OpaqueId OpaqueBlock)
stOpaqueBlocks         forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` \ Map OpaqueId OpaqueBlock
imp -> Map OpaqueId OpaqueBlock
imp forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Map OpaqueId OpaqueBlock
oblock
  Lens' TCState (Map QName OpaqueId)
stOpaqueIds            forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` \ Map QName OpaqueId
imp -> Map QName OpaqueId
imp forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Map QName OpaqueId
oid
  Signature -> TCM ()
addImportedInstances Signature
isig

-- | Scope checks the given module. A proper version of the module
-- name (with correct definition sites) is returned.

scopeCheckImport ::
  TopLevelModuleName -> ModuleName ->
  TCM (ModuleName, Map ModuleName Scope)
scopeCheckImport :: TopLevelModuleName
-> ModuleName -> TCM (ModuleName, Map ModuleName Scope)
scopeCheckImport TopLevelModuleName
top ModuleName
x = do
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.scope" Int
5 forall a b. (a -> b) -> a -> b
$ [Char]
"Scope checking " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow ModuleName
x
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"import.scope" Int
10 forall a b. (a -> b) -> a -> b
$ do
      [Char]
visited <- forall a. Pretty a => a -> [Char]
prettyShow forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m Doc
getPrettyVisitedModules
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.scope" Int
10 forall a b. (a -> b) -> a -> b
$ [Char]
"  visited: " forall a. [a] -> [a] -> [a]
++ [Char]
visited
    -- Since scopeCheckImport is called from the scope checker,
    -- we need to reimburse her account.
    Interface
i <- forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [] forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> Maybe Source -> TCMT IO Interface
getNonMainInterface TopLevelModuleName
top forall a. Maybe a
Nothing
    TopLevelModuleName -> TCM ()
addImport TopLevelModuleName
top

    -- If that interface was supposed to raise a warning on import, do so.
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (Interface -> Maybe Text
iImportWarning Interface
i) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning 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
    forall (m :: * -> *) a. Monad m => a -> m a
return (Interface -> ModuleName
iModuleName Interface
i ModuleName -> QName -> ModuleName
`withRangesOfQ` ModuleName -> QName
mnameToConcrete ModuleName
x, 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 = forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM TCM ModuleInfo
loadAndRecordVisited (ModuleCheckMode -> TCM (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 -> TCM (Maybe ModuleInfo)
existingWithoutWarnings ModuleCheckMode
mode = forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) e a. Functor m => ExceptT e m a -> MaybeT m a
exceptToMaybeT forall a b. (a -> b) -> a -> b
$ do
    ModuleInfo
mi <- forall (m :: * -> *) e a.
Functor m =>
e -> MaybeT m a -> ExceptT e m a
maybeToExceptT [Char]
"interface has not been visited in this context" forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *).
ReadTCState m =>
TopLevelModuleName -> m (Maybe ModuleInfo)
getVisitedModule TopLevelModuleName
x

    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ModuleInfo -> ModuleCheckMode
miMode ModuleInfo
mi forall a. Ord a => a -> a -> Bool
< ModuleCheckMode
mode) forall a b. (a -> b) -> a -> b
$
      forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"previously-visited interface was not sufficiently checked"

    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null forall a b. (a -> b) -> a -> b
$ ModuleInfo -> [TCWarning]
miWarnings ModuleInfo
mi) forall a b. (a -> b) -> a -> b
$
      forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"previously-visited interface had warnings"

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

    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift 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 -> [TCWarning]
miWarnings = [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
    [TCWarning]
wt <- forall a. a -> Maybe a -> a
fromMaybe [TCWarning]
ws forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (MainInterface
-> Bool -> PragmaOptions -> Interface -> TCM (Maybe [TCWarning])
getOptionsCompatibilityWarnings MainInterface
isMain Bool
isPrim PragmaOptions
currentOptions Interface
i)

    forall (m :: * -> *) a. Monad m => a -> m a
return ModuleInfo
mi { miWarnings :: [TCWarning]
miWarnings = [TCWarning]
wt }

  loadAndRecordVisited :: TCM ModuleInfo
  loadAndRecordVisited :: TCM ModuleInfo
loadAndRecordVisited = do
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.visit" Int
5 forall a b. (a -> b) -> a -> b
$ [Char]
"  Getting interface for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
x
    ModuleInfo
mi <- ModuleInfo -> TCM ModuleInfo
processResultingModule forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM ModuleInfo
getModule
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.visit" Int
5 forall a b. (a -> b) -> a -> b
$ [Char]
"  Now we've looked at " forall a. [a] -> [a] -> [a]
++ 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, ModuleInfo -> [TCWarning]
miWarnings ModuleInfo
mi) of
      (MainInterface Mode
ScopeCheck, [TCWarning]
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      (MainInterface
_, TCWarning
_:[TCWarning]
_)                      -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      (MainInterface, [TCWarning])
_                             -> ModuleInfo -> TCM ()
storeDecodedModule ModuleInfo
mi

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

    ModuleInfo -> TCM ()
visitModule ModuleInfo
mi
    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 -> [TCWarning] -> ModuleCheckMode -> Source -> CheckResult
pattern $mCheckResult :: forall {r}.
CheckResult
-> (Interface -> [TCWarning] -> ModuleCheckMode -> Source -> r)
-> ((# #) -> r)
-> r
CheckResult { CheckResult -> Interface
crInterface, CheckResult -> [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
  Source -> TCM ()
setOptionsFromSourcePragmas Source
src
  Bool
loadPrims <- PragmaOptions -> Bool
optLoadPrimitives forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions

  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
loadPrims forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.main" Int
10 [Char]
"Importing the primitive modules."
    [Char]
libdirPrim <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO [Char]
getPrimitiveLibDir
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.main" Int
20 forall a b. (a -> b) -> a -> b
$ [Char]
"Library primitive dir = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [Char]
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.

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

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

    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.main" Int
10 forall a b. (a -> b) -> a -> b
$ [Char]
"Done importing the primitive modules."

  -- 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) (forall a. a -> Maybe a
Just Source
src)

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

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

-- | 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
  -- Preserve/restore the current pragma options, which will be mutated when loading
  -- and checking the interface.
  ModuleInfo
mi <- forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ (forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState PragmaOptions
stPragmaOptions) (Lens' TCState PragmaOptions
stPragmaOptions forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens`) forall a b. (a -> b) -> a -> b
$
          TopLevelModuleName
-> MainInterface -> Maybe Source -> TCM ModuleInfo
getInterface TopLevelModuleName
x MainInterface
NotMainInterface Maybe Source
msrc
  [TCWarning] -> TCM ()
tcWarningsToError forall a b. (a -> b) -> a -> b
$ ModuleInfo -> [TCWarning]
miWarnings ModuleInfo
mi
  forall (m :: * -> *) a. Monad m => a -> m a
return (ModuleInfo -> Interface
miInterface ModuleInfo
mi)

-- | 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 =
  forall a. TopLevelModuleName -> TCM a -> TCM a
addImportCycleCheck TopLevelModuleName
x 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 <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState PragmaOptions
stPragmaOptions
     forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (Module -> [Pragma]
C.modPragmas forall b c a. (b -> c) -> (a -> b) -> a -> c
. Source -> Module
srcModule forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Source
msrc) forall a b. (a -> b) -> a -> b
$
       -- Now reset the options
       CommandLineOptions -> TCM ()
setCommandLineOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. PersistentTCState -> CommandLineOptions
stPersistentOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadTCState m => m TCState
getTC

     TopLevelModuleName
-> MainInterface
-> PragmaOptions
-> TCM ModuleInfo
-> TCM ModuleInfo
alreadyVisited TopLevelModuleName
x MainInterface
isMain PragmaOptions
currentOptions 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
          forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
modifyTCLens Lens' TCState ModuleToSource
stModuleToSource forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TopLevelModuleName
x (SourceFile -> AbsolutePath
srcFilePath SourceFile
file)
          forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceFile
file
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
15 forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
"\n" forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ([Char]
"  " forall a. [a] -> [a] -> [a]
++)
        [ [Char]
"module: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
x
        , [Char]
"file:   " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow SourceFile
file
        ]

      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
10 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 <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.Import] forall a b. (a -> b) -> a -> b
$ do
        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
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
5 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Char]
"  ", forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
x, [Char]
" is not up-to-date because ", [Char]
reason, [Char]
"."]
            CommandLineOptions -> TCM ()
setCommandLineOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. PersistentTCState -> CommandLineOptions
stPersistentOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadTCState m => m TCState
getTC
            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

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

-- | 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 = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT Bool
True forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"import.iface.options" Int
5 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
P.nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"current options  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> forall {m :: * -> *}.
(Applicative m, Semigroup (m Doc), IsString (m Doc)) =>
PragmaOptions -> m Doc
showOptions PragmaOptions
current
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"import.iface.options" Int
5 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
P.nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"imported options =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> forall {m :: * -> *}.
(Applicative m, Semigroup (m Doc), IsString (m Doc)) =>
PragmaOptions -> m Doc
showOptions PragmaOptions
imported
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [InfectiveCoinfectiveOption]
infectiveCoinfectiveOptions forall a b. (a -> b) -> a -> b
$ \InfectiveCoinfectiveOption
opt -> do
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (InfectiveCoinfectiveOption
-> PragmaOptions -> PragmaOptions -> Bool
icOptionOK InfectiveCoinfectiveOption
opt PragmaOptions
current PragmaOptions
imported) forall a b. (a -> b) -> a -> b
$ do
      forall s (m :: * -> *). MonadState s m => s -> m ()
put Bool
False
      forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning 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 =
    forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
P.prettyList forall a b. (a -> b) -> a -> b
$
    forall a b. (a -> b) -> [a] -> [b]
map (\InfectiveCoinfectiveOption
opt -> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
P.text (InfectiveCoinfectiveOption -> [Char]
icOptionDescription InfectiveCoinfectiveOption
opt) forall a. Semigroup a => a -> a -> a
<> m Doc
": ") forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+>
                 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 [TCWarning])
getOptionsCompatibilityWarnings :: MainInterface
-> Bool -> PragmaOptions -> Interface -> TCM (Maybe [TCWarning])
getOptionsCompatibilityWarnings MainInterface
isMain Bool
isPrim PragmaOptions
currentOptions Interface
i = forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) e a. Functor m => ExceptT e m a -> MaybeT m a
exceptToMaybeT 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.
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
isPrim forall a b. (a -> b) -> a -> b
$
    forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"Options consistency checking disabled for always-available primitive module"
  forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift 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)) forall a b. (a -> b) -> a -> b
$
    forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"No warnings to collect because options were compatible"
  forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) =>
MainInterface -> WhichWarnings -> m [TCWarning]
getAllWarnings' MainInterface
isMain WhichWarnings
ErrorWarnings

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

getStoredInterface
  :: TopLevelModuleName
     -- ^ Module name of file we process.
  -> SourceFile
     -- ^ File we process.
  -> Maybe Source
  -> ExceptT String TCM ModuleInfo
getStoredInterface :: TopLevelModuleName
-> SourceFile
-> Maybe Source
-> ExceptT [Char] (TCMT IO) ModuleInfo
getStoredInterface TopLevelModuleName
x SourceFile
file 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 <- forall (m :: * -> *) e a.
Functor m =>
e -> MaybeT m a -> ExceptT e m a
maybeToExceptT [Char]
"the interface file could not be found" forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$
          SourceFile -> TCM (Maybe InterfaceFile)
findInterfaceFile' SourceFile
file

        -- Check that the interface file exists and return its hash.
        (Hash, Hash)
hashes <- forall (m :: * -> *) e a.
Functor m =>
e -> MaybeT m a -> ExceptT e m a
maybeToExceptT [Char]
"the interface file hash could not be read" forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
          InterfaceFile -> IO (Maybe (Hash, Hash))
getInterfaceFileHashes InterfaceFile
ifile

        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 -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ AbsolutePath -> IO Hash
hashTextFile (SourceFile -> AbsolutePath
srcFilePath SourceFile
file)
                    Just Source
src -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Text -> Hash
hashText (Source -> Text
srcText Source
src)

        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Hash
sourceH forall a. Eq a => a -> a -> Bool
== Hash
ifaceH) forall a b. (a -> b) -> a -> b
$
          forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            [ [Char]
"the source hash (", forall a. Show a => a -> [Char]
show Hash
sourceH, [Char]
")"
            , [Char]
" does not match the source hash for the interface (", forall a. Show a => a -> [Char]
show Hash
ifaceH, [Char]
")"
            ]

        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
5 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Char]
"  ", forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
x, [Char]
" is up-to-date."]

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

  case Either [Char] ModuleInfo
cachedE of
    -- 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 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 = forall a b. (a, b) -> b
snd (Hash, Hash)
hashes
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Hash
cachedIfaceHash forall a. Eq a => a -> a -> Bool
== Hash
fileIfaceHash) forall a b. (a -> b) -> a -> b
$ do
        forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> TCM ()
dropDecodedModule TopLevelModuleName
x
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
50 forall a b. (a -> b) -> a -> b
$ [Char]
"  cached hash = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Hash
cachedIfaceHash
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
50 forall a b. (a -> b) -> a -> b
$ [Char]
"  stored hash = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Hash
fileIfaceHash
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
5 forall a b. (a -> b) -> a -> b
$ [Char]
"  file is newer, re-reading " forall a. [a] -> [a] -> [a]
++ [Char]
ifp
        forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ [Char]
"the cached interface hash (", forall a. Show a => a -> [Char]
show Hash
cachedIfaceHash, [Char]
")"
          , [Char]
" does not match interface file (", forall a. Show a => a -> [Char]
show Hash
fileIfaceHash, [Char]
")"
          ]

      forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.Deserialization] forall a b. (a -> b) -> a -> b
$ do
        Hash -> ExceptT [Char] (TCMT IO) ()
checkSourceHashET (Interface -> Hash
iSourceHash Interface
i)

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

    Left [Char]
whyNotCached -> forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> ExceptT e m a -> ExceptT e' m a
withExceptT (\[Char]
e -> forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Char]
whyNotCached, [Char]
" and ", [Char]
e]) forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM forall (m :: * -> *). HasOptions m => m Bool
ignoreAllInterfaces forall a b. (a -> b) -> a -> b
$
        forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"we're ignoring all interface files"

      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM forall (m :: * -> *). HasOptions m => m Bool
ignoreInterfaces forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadIO m => [Char] -> m Bool
Lens.isBuiltinModule (AbsolutePath -> [Char]
filePath forall a b. (a -> b) -> a -> b
$ SourceFile -> AbsolutePath
srcFilePath SourceFile
file)) forall a b. (a -> b) -> a -> b
$
            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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. InterfaceFile -> AbsolutePath
intFilePath forall a b. (a -> b) -> a -> b
$ InterfaceFile
ifile)

      forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.Deserialization] forall a b. (a -> b) -> a -> b
$ do
        Hash -> ExceptT [Char] (TCMT IO) ()
checkSourceHashET (forall a b. (a, b) -> a
fst (Hash, Hash)
hashes)

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

        Interface
i <- forall (m :: * -> *) e a.
Functor m =>
e -> MaybeT m a -> ExceptT e m a
maybeToExceptT [Char]
"bad interface, re-type checking" forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$
          InterfaceFile -> TCM (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
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TopLevelModuleName
topLevelName forall a. Eq a => a -> a -> Bool
== TopLevelModuleName
x) forall a b. (a -> b) -> a -> b
$
          -- Andreas, 2014-03-27 This check is now done in the scope checker.
          -- checkModuleName topLevelName file
          forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ AbsolutePath
-> TopLevelModuleName -> TopLevelModuleName -> TypeError
OverlappingProjects (SourceFile -> AbsolutePath
srcFilePath SourceFile
file) TopLevelModuleName
topLevelName TopLevelModuleName
x

        Bool
isPrimitiveModule <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadIO m => [Char] -> m Bool
Lens.isPrimitiveModule (AbsolutePath -> [Char]
filePath forall a b. (a -> b) -> a -> b
$ SourceFile -> AbsolutePath
srcFilePath SourceFile
file)

        forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ [Char] -> TopLevelModuleName -> Maybe [Char] -> TCM ()
chaseMsg [Char]
"Loading " TopLevelModuleName
x forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [Char]
ifp
        -- print imported warnings
        let ws :: [TCWarning]
ws = forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. a -> Maybe a
Strict.Just (forall a. a -> Maybe a
Just TopLevelModuleName
x) forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                         forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RangeFile -> Maybe TopLevelModuleName
rangeFileName forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> SrcFile
tcWarningOrigin) forall a b. (a -> b) -> a -> b
$
                 Interface -> [TCWarning]
iWarnings Interface
i
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null [TCWarning]
ws) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
alwaysReportSDoc [Char]
"warning" Int
1 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
P.vcat forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
P.prettyTCM forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TCWarning]
ws

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


loadDecodedModule
  :: SourceFile
     -- ^ File we process.
  -> ModuleInfo
  -> ExceptT String TCM ModuleInfo
loadDecodedModule :: SourceFile -> ModuleInfo -> ExceptT [Char] (TCMT IO) ModuleInfo
loadDecodedModule SourceFile
file ModuleInfo
mi = do
  let fp :: [Char]
fp = AbsolutePath -> [Char]
filePath forall a b. (a -> b) -> a -> b
$ SourceFile -> AbsolutePath
srcFilePath SourceFile
file
  let i :: Interface
i = ModuleInfo -> Interface
miInterface ModuleInfo
mi

  -- Check that it's the right version
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
5 forall a b. (a -> b) -> a -> b
$ [Char]
"  imports: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow (Interface -> [(TopLevelModuleName, Hash)]
iImportedModules Interface
i)

  -- 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 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ AbsolutePath -> TopLevelModuleName -> TCM [OptionsPragma]
getLibraryOptions
    (SourceFile -> AbsolutePath
srcFilePath SourceFile
file)
    (Interface -> TopLevelModuleName
iTopLevelModuleName Interface
i)
  forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ OptionsPragma -> TCM ()
setOptionsFromPragma ([OptionsPragma]
libOptions forall a. [a] -> [a] -> [a]
++ Interface -> [OptionsPragma]
iFilePragmaOptions Interface
i)

  -- Check that options that matter haven't changed compared to
  -- current options (issue #2487)
  forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadIO m => [Char] -> m Bool
Lens.isBuiltinModule [Char]
fp) forall a b. (a -> b) -> a -> b
$ do
    PragmaOptions
current <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState PragmaOptions
stPragmaOptions
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (PragmaOptions -> PragmaOptions -> Bool
recheckBecausePragmaOptionsChanged (Interface -> PragmaOptions
iOptionsUsed Interface
i) PragmaOptions
current) forall a b. (a -> b) -> a -> b
$
      forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"options changed"

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

  forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull [[Char]]
badHashMessages (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Char]] -> [Char]
unlines)

  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
5 [Char]
"  New module. Let's check it out."
  forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Interface -> TCM ()
mergeInterface Interface
i
  forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.Highlighting] forall a b. (a -> b) -> a -> b
$
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *).
MonadTCEnv tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive forall a b. (a -> b) -> a -> b
$
      Interface -> SourceFile -> TCM ()
highlightFromInterface Interface
i SourceFile
file

  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
      forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog

      [TopLevelModuleName]
ms          <- TCM [TopLevelModuleName]
getImportPath
      Range
range       <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Range
envRange
      Maybe (Closure Call)
call        <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe (Closure Call)
envCall
      ModuleToSource
mf          <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState ModuleToSource
stModuleToSource
      VisitedModules
vs          <- forall (m :: * -> *). ReadTCState m => m VisitedModules
getVisitedModules
      VisitedModules
ds          <- TCM VisitedModules
getDecodedModules
      CommandLineOptions
opts        <- PersistentTCState -> CommandLineOptions
stPersistentOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCState m => m TCState
getTC
      Signature
isig        <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState Signature
stImports
      RemoteMetaStore
metas       <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState RemoteMetaStore
stImportedMetaStore
      Map SomeBuiltin (Builtin PrimFun)
ibuiltin    <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
stImportedBuiltins
      DisplayForms
display     <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState DisplayForms
stImportsDisplayForms
      Map QName Text
userwarn    <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState (Map QName Text)
stImportedUserWarnings
      Set QName
partialdefs <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState (Set QName)
stImportedPartialDefs
      Map OpaqueId OpaqueBlock
opaqueblk   <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState (Map OpaqueId OpaqueBlock)
stOpaqueBlocks
      Map QName OpaqueId
opaqueid    <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState (Map QName OpaqueId)
stOpaqueIds
      PatternSynDefns
ipatsyns <- forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getPatternSynImports
      InteractionOutputCallback
ho       <- 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) <- (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) forall a b. (a -> b) -> a -> b
$
           forall (m :: * -> *) a.
(MonadTCState m, ReadTCState m) =>
m a -> m a
withoutCache 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
           forall a. TCM a -> TCM (Either TCErr a)
freshTCM forall a b. (a -> b) -> a -> b
$
             forall a. [TopLevelModuleName] -> TCM a -> TCM a
withImportPath [TopLevelModuleName]
ms forall a b. (a -> b) -> a -> b
$
             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
envRange              = Range
range
                            , envCall :: Maybe (Closure Call)
envCall               = Maybe (Closure Call)
call
                            }) forall a b. (a -> b) -> a -> b
$ do
               VisitedModules -> TCM ()
setDecodedModules VisitedModules
ds
               CommandLineOptions -> TCM ()
setCommandLineOptions CommandLineOptions
opts
               InteractionOutputCallback -> TCM ()
setInteractionOutputCallback InteractionOutputCallback
ho
               Lens' TCState ModuleToSource
stModuleToSource 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
-> Map QName Text
-> Set QName
-> [TCWarning]
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> TCM ()
addImportedThings Signature
isig RemoteMetaStore
metas Map SomeBuiltin (Builtin PrimFun)
ibuiltin PatternSynDefns
ipatsyns DisplayForms
display
                 Map QName Text
userwarn Set QName
partialdefs [] 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' <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState ModuleToSource
stModuleToSource
               VisitedModules
ds' <- TCM VisitedModules
getDecodedModules
               forall (m :: * -> *) a. Monad m => a -> m a
return (ModuleInfo
r, ModuleToSource
mf', VisitedModules
ds')

      Lens' TCState ModuleToSource
stModuleToSource 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 <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT 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
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
alwaysReportSLn [Char]
"import.iface" Int
1 forall a b. (a -> b) -> a -> b
$ [Char]
"Failed to validate just-loaded interface: " forall a. [a] -> [a] -> [a]
++ [Char]
msg
            TopLevelModuleName -> SourceFile -> Maybe Source -> TCM ModuleInfo
createInterfaceIsolated TopLevelModuleName
x SourceFile
file Maybe Source
msrc

      forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either [Char] -> TCM ModuleInfo
recheckOnError 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 <- (forall a. Int -> a -> [a]
`replicate` Char
' ') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC (forall a. Enum a => a -> a
pred forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEnv -> [TopLevelModuleName]
envImportPath)
  Integer
traceImports <- CommandLineOptions -> Integer
optTraceImports forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  let maybeFile :: [Char]
maybeFile = forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe [Char]
file [Char]
"." forall a b. (a -> b) -> a -> b
$ \ [Char]
f -> [Char]
" (" forall a. [a] -> [a] -> [a]
++ [Char]
f forall a. [a] -> [a] -> [a]
++ [Char]
")."
      vLvl :: Int
vLvl | [Char]
kind forall a. Eq a => a -> a -> Bool
== [Char]
"Checking"
             Bool -> Bool -> Bool
&& Integer
traceImports forall a. Ord a => a -> a -> Bool
> Integer
0 = Int
1
           | [Char]
kind forall a. Eq a => a -> a -> Bool
== [Char]
"Finished"
             Bool -> Bool -> Bool
&& Integer
traceImports forall a. Ord a => a -> a -> Bool
> Integer
1 = Int
1
           | forall a. Eq a => [a] -> [a] -> Bool
List.isPrefixOf [Char]
"Loading" [Char]
kind
             Bool -> Bool -> Bool
&& Integer
traceImports forall a. Ord a => a -> a -> Bool
> Integer
2 = Int
1
           | Bool
otherwise = Int
2
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
alwaysReportSLn [Char]
"import.chase" Int
vLvl forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ [Char]
indentation, [Char]
kind, [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
file = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
5 forall a b. (a -> b) -> a -> b
$
    [Char]
"Generating syntax info for " forall a. [a] -> [a] -> [a]
++ AbsolutePath -> [Char]
filePath (SourceFile -> AbsolutePath
srcFilePath SourceFile
file) forall a. [a] -> [a] -> [a]
++
    [Char]
" (read from interface)."
  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 -> TCM (Maybe Interface)
readInterface InterfaceFile
file = do
    let ifp :: [Char]
ifp = AbsolutePath -> [Char]
filePath forall a b. (a -> b) -> a -> b
$ InterfaceFile -> AbsolutePath
intFilePath InterfaceFile
file
    -- Decode the interface file
    (ByteString
s, IO ()
close) <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ [Char] -> IO (ByteString, IO ())
readBinaryFile' [Char]
ifp
    do  Maybe Interface
mi <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> IO a
E.evaluate forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ByteString -> TCM (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.
        forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO ()
close

        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Interface -> Interface
constructIScope forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Interface
mi
      -- Catch exceptions and close
      forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
e -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO ()
close forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall {a}. TCErr -> TCMT IO (Maybe a)
handler TCErr
e
  -- Catch exceptions
  forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` forall {a}. TCErr -> TCMT IO (Maybe a)
handler
  where
    handler :: TCErr -> TCMT IO (Maybe a)
handler = \case
      IOException TCState
_ Range
_ IOException
e -> do
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
alwaysReportSLn [Char]
"" Int
0 forall a b. (a -> b) -> a -> b
$ [Char]
"IO exception: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show IOException
e
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing   -- Work-around for file locking bug.
                         -- TODO: What does this refer to? Please
                         -- document.
      TCErr
e -> 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
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.write" Int
5  forall a b. (a -> b) -> a -> b
$
      [Char]
"Writing interface file " forall a. [a] -> [a] -> [a]
++ [Char]
fp 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 :: ScopeInfo
iInsideScope  = ScopeInfo -> ScopeInfo
withoutPrivates forall a b. (a -> b) -> a -> b
$ Interface -> ScopeInfo
iInsideScope Interface
i }
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.write" Int
50 forall a b. (a -> b) -> a -> b
$
      [Char]
"Writing interface file with hash " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Interface -> Hash
iFullHash Interface
filteredIface) forall a. [a] -> [a] -> [a]
++ [Char]
"."
    ByteString
encodedIface <- [Char] -> Interface -> TCM ByteString
encodeFile [Char]
fp Interface
filteredIface
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.write" Int
5 [Char]
"Wrote interface file."
    forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.Deserialization] (forall a. EmbPrj a => ByteString -> TCM (Maybe a)
decode ByteString
encodedIface))
  forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
e -> do
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
alwaysReportSLn [Char]
"" Int
1 forall a b. (a -> b) -> a -> b
$
      [Char]
"Failed to write interface " forall a. [a] -> [a] -> [a]
++ [Char]
fp forall a. [a] -> [a] -> [a]
++ [Char]
"."
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ([Char] -> IO Bool
doesFileExist [Char]
fp) forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
removeFile [Char]
fp
    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 SourceFile
file MainInterface
isMain Maybe Source
msrc = do
  let x :: TopLevelModuleName
x = TopLevelModuleName
mname
  let fp :: [Char]
fp = AbsolutePath -> [Char]
filePath forall a b. (a -> b) -> a -> b
$ SourceFile -> AbsolutePath
srcFilePath SourceFile
file
  let checkMsg :: [Char]
checkMsg = case MainInterface
isMain of
                   MainInterface Mode
ScopeCheck -> [Char]
"Reading "
                   MainInterface
_                        -> [Char]
"Checking"
      withMsgs :: TCM ModuleInfo -> TCM ModuleInfo
withMsgs = forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_
       ([Char] -> TopLevelModuleName -> Maybe [Char] -> TCM ()
chaseMsg [Char]
checkMsg TopLevelModuleName
x forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [Char]
fp)
       (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ do [TCWarning]
ws <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) =>
WhichWarnings -> m [TCWarning]
getAllWarnings WhichWarnings
AllWarnings
                   let classified :: WarningsAndNonFatalErrors
classified = [TCWarning] -> WarningsAndNonFatalErrors
classifyWarnings [TCWarning]
ws
                   let wa' :: [TCWarning]
wa' = forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. a -> Maybe a
Strict.Just (forall a. a -> Maybe a
Just TopLevelModuleName
mname) forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                                     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RangeFile -> Maybe TopLevelModuleName
rangeFileName forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> SrcFile
tcWarningOrigin) forall a b. (a -> b) -> a -> b
$
                             WarningsAndNonFatalErrors -> [TCWarning]
tcWarnings WarningsAndNonFatalErrors
classified
                   forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null [TCWarning]
wa') forall a b. (a -> b) -> a -> b
$
                     forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
alwaysReportSDoc [Char]
"warning" Int
1 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
P.vcat forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
P.prettyTCM forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TCWarning]
wa'
                   forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Null a => a -> Bool
null (WarningsAndNonFatalErrors -> [TCWarning]
nonFatalErrors WarningsAndNonFatalErrors
classified)) forall a b. (a -> b) -> a -> b
$ [Char] -> TopLevelModuleName -> Maybe [Char] -> TCM ()
chaseMsg [Char]
"Finished" TopLevelModuleName
x forall a. Maybe a
Nothing)

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

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

    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
5 forall a b. (a -> b) -> a -> b
$
      [Char]
"Creating interface for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
mname forall a. [a] -> [a] -> [a]
++ [Char]
"."
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"import.iface.create" Int
10 forall a b. (a -> b) -> a -> b
$ do
      [Char]
visited <- forall a. Pretty a => a -> [Char]
prettyShow forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m Doc
getPrettyVisitedModules
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
10 forall a b. (a -> b) -> a -> b
$ [Char]
"  visited: " forall a. [a] -> [a] -> [a]
++ [Char]
visited

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

    let srcPath :: AbsolutePath
srcPath = SourceFile -> AbsolutePath
srcFilePath forall a b. (a -> b) -> a -> b
$ Source -> SourceFile
srcOrigin Source
src

    HighlightingInfo
fileTokenInfo <- forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.Highlighting] 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 (forall a. a -> Maybe a
Just TopLevelModuleName
top))
        (Text -> [Char]
TL.unpack forall a b. (a -> b) -> a -> b
$ Source -> Text
srcText Source
src)
    Lens' TCState HighlightingInfo
stTokens forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` (HighlightingInfo
fileTokenInfo forall a. Semigroup a => a -> a -> a
<>)

    Source -> TCM ()
setOptionsFromSourcePragmas Source
src
    Attributes -> TCM ()
checkAttributes (Source -> Attributes
srcAttributes Source
src)
    Maybe Int
syntactic <- PragmaOptions -> Maybe Int
optSyntacticEquality forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
    forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\TCEnv
env -> TCEnv
env { envSyntacticEqualityFuel :: Maybe Int
envSyntacticEqualityFuel = Maybe Int
syntactic }) forall a b. (a -> b) -> a -> b
$ do

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

    -- Scope checking.
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 [Char]
"Starting scope checking."
    TopLevelInfo
topLevel <- forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.Scoping] forall a b. (a -> b) -> a -> b
$ do
      let topDecls :: [Declaration]
topDecls = Module -> [Declaration]
C.modDecls forall a b. (a -> b) -> a -> b
$ Source -> Module
srcModule Source
src
      forall c. ToAbstract c => c -> ScopeM (AbsOfCon c)
concreteToAbstract_ (forall a. AbsolutePath -> TopLevelModuleName -> a -> TopLevel a
TopLevel AbsolutePath
srcPath TopLevelModuleName
mname [Declaration]
topDecls)
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 [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.
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 [Char]
"Starting highlighting from scope."
    forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.Highlighting] forall a b. (a -> b) -> a -> b
$ do
      -- Generate and print approximate syntax highlighting info.
      forall (tcm :: * -> *).
MonadTCEnv tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting HighlightingInfo
fileTokenInfo
      forall (tcm :: * -> *).
MonadTCEnv tcm =>
HighlightingLevel -> Bool -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIsOr HighlightingLevel
NonInteractive Bool
onlyScope forall a b. (a -> b) -> a -> b
$
        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
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 [Char]
"Finished highlighting from scope."


    -- Type checking.

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

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

    if Bool
onlyScope
      then do
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 [Char]
"Skipping type checking."
        forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cacheCurrentLog
      else do
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 [Char]
"Starting type checking."
        forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.Typing] forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Declaration -> TCM ()
checkDeclCached [Declaration]
ds forall a b. TCM a -> TCM b -> TCM a
`finally_` forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cacheCurrentLog
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 [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.
    forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Metas forall a b. (a -> b) -> a -> b
$ do
      MetaId
m <- forall i (m :: * -> *). MonadFresh i m => m i
fresh
      forall (m :: * -> *).
MonadStatistics m =>
[Char] -> Integer -> m ()
tickN [Char]
"metas" (forall a b. (Integral a, Num b) => a -> b
fromIntegral (MetaId -> Hash
metaId MetaId
m))

    -- Highlighting from type checker.
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 [Char]
"Starting highlighting from type info."
    forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.Highlighting] forall a b. (a -> b) -> a -> b
$ do

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

      -- Grabbing warnings and unsolved metas to highlight them
      [TCWarning]
warnings <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) =>
WhichWarnings -> m [TCWarning]
getAllWarnings WhichWarnings
AllWarnings
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null [TCWarning]
warnings) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"import.iface.create" Int
20 forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"collected warnings: " forall a. Semigroup a => a -> a -> a
<> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [TCWarning]
warnings
      [TCWarning]
unsolved <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) =>
m [TCWarning]
getAllUnsolvedWarnings
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null [TCWarning]
unsolved) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"import.iface.create" Int
20 forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"collected unsolved: " forall a. Semigroup a => a -> a -> a
<> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [TCWarning]
unsolved
      let warningInfo :: HighlightingInfo
warningInfo =
            forall a b. Convert a b => a -> b
convert forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap TCWarning -> HighlightingInfoBuilder
warningHighlighting forall a b. (a -> b) -> a -> b
$ [TCWarning]
unsolved forall a. [a] -> [a] -> [a]
++ [TCWarning]
warnings

      Lens' TCState HighlightingInfo
stSyntaxInfo forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` \HighlightingInfo
inf -> (HighlightingInfo
inf forall a. Monoid a => a -> a -> a
`mappend` HighlightingInfo
toks) forall a. Monoid a => a -> a -> a
`mappend` HighlightingInfo
warningInfo

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

    ScopeInfo -> TCM ()
setScope ScopeInfo
scope
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"scope.top" Int
50 forall a b. (a -> b) -> a -> b
$ [Char]
"SCOPE " forall a. [a] -> [a] -> [a]
++ 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           <- forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null [MetaId]
openMetas) forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.metas" Int
10 [Char]
"We have unsolved metas."
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.metas" Int
10 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Goals -> TCMT IO [Char]
showGoals forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM Goals
getGoals

    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
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (MainInterface -> Bool
includeStateChanges MainInterface
isMain) 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).
      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (PragmaOptions -> Bool
optAllowUnsolved forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 [Char]
"Turning unsolved metas (if any) into postulates."
        forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
withCurrentModule (ScopeInfo
scope forall o i. o -> Lens' o i -> i
^. Lens' ScopeInfo ModuleName
scopeCurrent) TCM ()
openMetasToPostulates
        -- Clear constraints as they might refer to what
        -- they think are open metas.
        Lens' TCState Constraints
stAwakeConstraints    forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens` []
        Lens' TCState Constraints
stSleepingConstraints forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens` []

    -- Serialization.
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 [Char]
"Starting serialization."
    Interface
i <- forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.Serialization, Phase
Bench.BuildInterface] forall a b. (a -> b) -> a -> b
$
      Source -> TopLevelInfo -> TCMT IO Interface
buildInterface Source
src TopLevelInfo
topLevel

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

    [TCWarning]
mallWarnings <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) =>
MainInterface -> WhichWarnings -> m [TCWarning]
getAllWarnings' MainInterface
isMain WhichWarnings
ErrorWarnings

    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 [Char]
"Considering writing to interface file."
    Interface
finalIface <- Interface -> Interface
constructIScope forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> case ([TCWarning]
mallWarnings, MainInterface
isMain) of
      (TCWarning
_:[TCWarning]
_, 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
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 [Char]
"We have warnings, skipping writing interface file."
        forall (m :: * -> *) a. Monad m => a -> m a
return Interface
i
      ([], MainInterface Mode
ScopeCheck) -> do
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 [Char]
"We are just scope-checking, skipping writing interface file."
        forall (m :: * -> *) a. Monad m => a -> m a
return Interface
i
      ([], MainInterface
_) -> forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.Serialization] forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 [Char]
"Actually calling writeInterface."
        -- The file was successfully type-checked (and no warnings were
        -- encountered), so the interface should be written out.
        AbsolutePath
ifile <- SourceFile -> TCM AbsolutePath
toIFile SourceFile
file
        Interface
serializedIface <- AbsolutePath -> Interface -> TCMT IO Interface
writeInterface AbsolutePath
ifile Interface
i
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.create" Int
7 [Char]
"Finished writing to interface file."
        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.
    forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m, HasOptions m) =>
Maybe TopLevelModuleName -> Statistics -> m ()
printStatistics (forall a. a -> Maybe a
Just TopLevelModuleName
mname) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). ReadTCState m => m Statistics
getStatistics

    -- Get the statistics of the current module
    -- and add it to the accumulated statistics.
    Statistics
localStatistics <- forall (m :: * -> *). ReadTCState m => m Statistics
getStatistics
    Lens' TCState Statistics
lensAccumStatistics forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith forall a. Num a => a -> a -> a
(+) Statistics
localStatistics
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
5 [Char]
"Accumulated statistics."

    Bool
isPrimitiveModule <- forall (m :: * -> *). MonadIO m => [Char] -> m Bool
Lens.isPrimitiveModule (AbsolutePath -> [Char]
filePath AbsolutePath
srcPath)

    forall (m :: * -> *) a. Monad m => a -> m a
return ModuleInfo
      { miInterface :: Interface
miInterface = Interface
finalIface
      , miWarnings :: [TCWarning]
miWarnings = [TCWarning]
mallWarnings
      , miPrimitive :: Bool
miPrimitive = Bool
isPrimitiveModule
      , 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' :: (MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) => MainInterface -> WhichWarnings -> m [TCWarning]
getAllWarnings' :: forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) =>
MainInterface -> WhichWarnings -> m [TCWarning]
getAllWarnings' (MainInterface Mode
_) = forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) =>
Set WarningName -> WhichWarnings -> m [TCWarning]
getAllWarningsPreserving Set WarningName
unsolvedWarnings
getAllWarnings' MainInterface
NotMainInterface  = forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) =>
Set WarningName -> WhichWarnings -> m [TCWarning]
getAllWarningsPreserving 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 = forall a. Account -> a -> a
billToPure [ Phase
Deserialization ] forall a b. (a -> b) -> a -> b
$
  Interface
i{ iScope :: Map ModuleName Scope
iScope = ScopeInfo -> Map ModuleName Scope
publicModules forall a b. (a -> b) -> a -> b
$ Interface -> ScopeInfo
iInsideScope Interface
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
    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).
    Map SomeBuiltin (Builtin PrimFun)
builtin     <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
stLocalBuiltins
    [(TopLevelModuleName, Hash)]
mhs         <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\TopLevelModuleName
top -> (TopLevelModuleName
top,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TopLevelModuleName -> TCMT IO Hash
moduleHash TopLevelModuleName
top) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                   forall a. Set a -> [a]
Set.toAscList forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
                   forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR Lens' TCState (Set TopLevelModuleName)
stImportedModules
    Map [Char] ForeignCodeStack
foreignCode <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState (Map [Char] ForeignCodeStack)
stForeignCode
    -- Ulf, 2016-04-12:
    -- Non-closed display forms are not applicable outside the module anyway,
    -- and should be dead-code eliminated (#1928).
    DisplayForms
origDisplayForms <- forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
HMap.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Null a => a -> Bool
null) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HMap.map (forall a. (a -> Bool) -> [a] -> [a]
filter forall a. Open a -> Bool
isClosed) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState DisplayForms
stImportsDisplayForms
    -- TODO: Kill some ranges?
    let scope :: ScopeInfo
scope = TopLevelInfo -> ScopeInfo
topLevelScope TopLevelInfo
topLevel
    -- Andreas, Oskar, 2023-10-19, issue #6931:
    -- To not delete module telescopes of empty public modules,
    -- we need to pass the public modules to the dead-code elimination
    -- (to be mined for additional roots for the reachability analysis).
    (DisplayForms
display, Signature
sig, RemoteMetaStore
solvedMetas) <-
      forall a.
Map ModuleName a
-> Map SomeBuiltin (Builtin PrimFun)
-> DisplayForms
-> Signature
-> LocalMetaStore
-> TCMT IO (DisplayForms, Signature, RemoteMetaStore)
eliminateDeadCode (ScopeInfo -> Map ModuleName Scope
publicModules ScopeInfo
scope) Map SomeBuiltin (Builtin PrimFun)
builtin DisplayForms
origDisplayForms forall (m :: * -> *) a b c.
Monad m =>
(a -> b -> m c) -> (m a, m b) -> m c
==<<
        (forall (m :: * -> *). ReadTCState m => m Signature
getSignature, forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR Lens' TCState LocalMetaStore
stSolvedMetaStore)
    Map QName Text
userwarns   <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState (Map QName Text)
stLocalUserWarnings
    Maybe Text
importwarn  <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState (Maybe Text)
stWarningOnImport
    HighlightingInfo
syntaxInfo  <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState HighlightingInfo
stSyntaxInfo
    PragmaOptions
optionsUsed <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState PragmaOptions
stPragmaOptions
    Set QName
partialDefs <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState (Set QName)
stLocalPartialDefs

    -- Only serialise the opaque blocks actually defined in this
    -- top-level module.
    Map OpaqueId OpaqueBlock
opaqueBlocks' <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState (Map OpaqueId OpaqueBlock)
stOpaqueBlocks
    Map QName OpaqueId
opaqueIds' <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState (Map QName OpaqueId)
stOpaqueIds
    let
      mh :: ModuleNameHash
mh = forall range. TopLevelModuleName' range -> ModuleNameHash
moduleNameId (Source -> TopLevelModuleName
srcModuleName Source
src)
      opaqueBlocks :: Map OpaqueId OpaqueBlock
opaqueBlocks = forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\(OpaqueId Hash
_ ModuleNameHash
mod) OpaqueBlock
_ -> ModuleNameHash
mod forall a. Eq a => a -> a -> Bool
== ModuleNameHash
mh) Map OpaqueId OpaqueBlock
opaqueBlocks'
      opaqueIds :: Map QName OpaqueId
opaqueIds    = forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\QName
_ (OpaqueId Hash
_ ModuleNameHash
mod) -> ModuleNameHash
mod forall a. Eq a => a -> a -> Bool
== ModuleNameHash
mh) Map QName OpaqueId
opaqueIds'

    -- 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 <- forall a. KillRange a => KillRangeT a
killRange forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getPatternSyns
    let builtin' :: BuiltinThings (PrimitiveId, QName)
builtin' = 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Builtin PrimFun
b) Map SomeBuiltin (Builtin PrimFun)
builtin
    [TCWarning]
warnings <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) =>
WhichWarnings -> m [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           = 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
display
          , iUserWarnings :: Map QName Text
iUserWarnings    = Map QName Text
userwarns
          , iImportWarning :: Maybe Text
iImportWarning   = Maybe Text
importwarn
          , iBuiltin :: BuiltinThings (PrimitiveId, QName)
iBuiltin         = BuiltinThings (PrimitiveId, QName)
builtin'
          , iForeignCode :: Map [Char] ForeignCodeStack
iForeignCode     = Map [Char] 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 :: [TCWarning]
iWarnings        = [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 <-
      forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (PragmaOptions -> Bool
optSaveMetas forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)
        (forall (m :: * -> *) a. Monad m => a -> m a
return Interface
i)
        (do forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
7
              [Char]
"  instantiating all meta variables"
            -- Note that the meta-variables in the definitions in
            -- "sig" have already been instantiated (by
            -- eliminateDeadCode).
            forall (m :: * -> *). MonadReduce m => Interface -> m Interface
instantiateFullExceptForDefinitions Interface
i)
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
7 [Char]
"  interface complete"
    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 = 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 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
  forall b a. b -> (a -> b) -> Maybe a -> b
maybe Hash
0 (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Num a => a -> a -> a
(+)) Maybe (Hash, Hash)
hs seq :: forall a b. a -> b -> b
`seq` IO ()
close
  forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Hash, Hash)
hs

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