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

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

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

  , Source(..)
  , scopeCheckImport
  , parseSource
  , typeCheckMain
  , raiseNonFatalErrors

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

import Prelude hiding (null)

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

import Data.Either
import 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.InstanceArguments
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 qualified Agda.Interaction.Highlighting.Precise as Highlighting ( convert )
import Agda.Interaction.Highlighting.Vim
import Agda.Interaction.Library
import Agda.Interaction.Options
import qualified Agda.Interaction.Options.Lenses as Lens
import Agda.Interaction.Options.Warnings (unsolvedWarnings)
import Agda.Interaction.Response
  (RemoveTokenBasedHighlighting(KeepHighlighting))

import Agda.Utils.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.Set1 as Set1
import qualified Agda.Utils.Trie as Trie

import Agda.Utils.Impossible

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

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

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

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

-- | The decorated source code.

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

-- | Parses a source file and prepares the 'Source' record.

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

  -- Read the source text.
  let rf0 :: RangeFile
rf0 = AbsolutePath -> Maybe TopLevelModuleName -> RangeFile
mkRangeFile AbsolutePath
f Maybe TopLevelModuleName
forall a. Maybe a
Nothing
  source <- PM Text -> TCM Text
forall a. PM a -> TCM a
runPM (PM Text -> TCM Text) -> PM Text -> TCM Text
forall a b. (a -> b) -> a -> b
$ RangeFile -> PM Text
readFilePM RangeFile
rf0
  let txt = Text -> [Char]
TL.unpack Text
source

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

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

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

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

srcFilePragmas :: Source -> [OptionsPragma]
srcFilePragmas :: Source -> [OptionsPragma]
srcFilePragmas Source
src = [OptionsPragma]
pragmas
  where
  cpragmas :: [Pragma]
cpragmas = Module -> [Pragma]
C.modPragmas (Source -> Module
srcModule Source
src)
  pragmas :: [OptionsPragma]
pragmas = [ OptionsPragma
                { pragmaStrings :: [[Char]]
pragmaStrings = [[Char]]
opts
                , pragmaRange :: Range
pragmaRange   = Range
r
                }
            | C.OptionsPragma Range
r [[Char]]
opts <- [Pragma]
cpragmas
            ]

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

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

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

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

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

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

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

-- | Merge an interface into the current proof state.
mergeInterface :: Interface -> TCM ()
mergeInterface :: Interface -> TCM ()
mergeInterface Interface
i = do
    let sig :: Signature
sig     = Interface -> Signature
iSignature Interface
i
        builtin :: [(SomeBuiltin, Builtin (PrimitiveId, QName))]
builtin = Map SomeBuiltin (Builtin (PrimitiveId, QName))
-> [(SomeBuiltin, Builtin (PrimitiveId, QName))]
forall k a. Map k a -> [(k, a)]
Map.toAscList (Map SomeBuiltin (Builtin (PrimitiveId, QName))
 -> [(SomeBuiltin, Builtin (PrimitiveId, QName))])
-> Map SomeBuiltin (Builtin (PrimitiveId, QName))
-> [(SomeBuiltin, Builtin (PrimitiveId, QName))]
forall a b. (a -> b) -> a -> b
$ Interface -> Map SomeBuiltin (Builtin (PrimitiveId, QName))
iBuiltin Interface
i
        primOrBi :: (a, Builtin a) -> Either a (a, Builtin pf)
primOrBi = \case
          (a
_, Prim a
x)                     -> a -> Either a (a, Builtin pf)
forall a b. a -> Either a b
Left a
x
          (a
x, Builtin Term
t)                  -> (a, Builtin pf) -> Either a (a, Builtin pf)
forall a b. b -> Either a b
Right (a
x, Term -> Builtin pf
forall pf. Term -> Builtin pf
Builtin Term
t)
          (a
x, BuiltinRewriteRelations Set QName
xs) -> (a, Builtin pf) -> Either a (a, Builtin pf)
forall a b. b -> Either a b
Right (a
x, Set QName -> Builtin pf
forall pf. Set QName -> Builtin pf
BuiltinRewriteRelations Set QName
xs)
        ([(PrimitiveId, QName)]
prim, [(SomeBuiltin, Builtin PrimFun)]
bi') = [Either (PrimitiveId, QName) (SomeBuiltin, Builtin PrimFun)]
-> ([(PrimitiveId, QName)], [(SomeBuiltin, Builtin PrimFun)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either (PrimitiveId, QName) (SomeBuiltin, Builtin PrimFun)]
 -> ([(PrimitiveId, QName)], [(SomeBuiltin, Builtin PrimFun)]))
-> [Either (PrimitiveId, QName) (SomeBuiltin, Builtin PrimFun)]
-> ([(PrimitiveId, QName)], [(SomeBuiltin, Builtin PrimFun)])
forall a b. (a -> b) -> a -> b
$ ((SomeBuiltin, Builtin (PrimitiveId, QName))
 -> Either (PrimitiveId, QName) (SomeBuiltin, Builtin PrimFun))
-> [(SomeBuiltin, Builtin (PrimitiveId, QName))]
-> [Either (PrimitiveId, QName) (SomeBuiltin, Builtin PrimFun)]
forall a b. (a -> b) -> [a] -> [b]
map (SomeBuiltin, Builtin (PrimitiveId, QName))
-> Either (PrimitiveId, QName) (SomeBuiltin, Builtin PrimFun)
forall {a} {a} {pf}. (a, Builtin a) -> Either a (a, Builtin pf)
primOrBi [(SomeBuiltin, Builtin (PrimitiveId, QName))]
builtin
        bi :: Map SomeBuiltin (Builtin PrimFun)
bi      = [(SomeBuiltin, Builtin PrimFun)]
-> Map SomeBuiltin (Builtin PrimFun)
forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList [(SomeBuiltin, Builtin PrimFun)]
bi'
        warns :: Set TCWarning
warns   = Interface -> Set TCWarning
iWarnings Interface
i
    bs <- (TCState -> Map SomeBuiltin (Builtin PrimFun))
-> TCMT IO (Map SomeBuiltin (Builtin PrimFun))
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC TCState -> Map SomeBuiltin (Builtin PrimFun)
stBuiltinThings
    reportSLn "import.iface.merge" 10 "Merging interface"
    reportSLn "import.iface.merge" 20 $
      "  Current builtins " ++ show (Map.keys bs) ++ "\n" ++
      "  New builtins     " ++ show (Map.keys bi)
    let check (BuiltinName BuiltinId
b) (Builtin Term
x) (Builtin Term
y)
              | Term
x Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
y    = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
              | Bool
otherwise = TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ BuiltinId -> Term -> Term -> TypeError
DuplicateBuiltinBinding BuiltinId
b Term
x Term
y
        check SomeBuiltin
_ (BuiltinRewriteRelations Set QName
xs) (BuiltinRewriteRelations Set QName
ys) = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        check SomeBuiltin
_ Builtin pf
_ Builtin pf
_ = m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
    sequence_ $ Map.intersectionWithKey check bs bi
    addImportedThings
      sig
      (iMetaBindings i)
      bi
      (iPatternSyns i)
      (iDisplayForms i)
      (iUserWarnings i)
      (iPartialDefs i)
      warns
      (iOpaqueBlocks i)
      (iOpaqueNames i)
    reportSLn "import.iface.merge" 50 $
      "  Rebinding primitives " ++ show prim
    mapM_ rebind prim
    whenJustM (optConfluenceCheck <$> pragmaOptions) $ \ConfluenceCheck
confChk -> do
      [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.confluence" Int
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  Checking confluence of imported rewrite rules"
      ConfluenceCheck -> [RewriteRule] -> TCM ()
checkConfluenceOfRules ConfluenceCheck
confChk ([RewriteRule] -> TCM ()) -> [RewriteRule] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [[RewriteRule]] -> [RewriteRule]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[RewriteRule]] -> [RewriteRule])
-> [[RewriteRule]] -> [RewriteRule]
forall a b. (a -> b) -> a -> b
$ HashMap QName [RewriteRule] -> [[RewriteRule]]
forall k v. HashMap k v -> [v]
HMap.elems (HashMap QName [RewriteRule] -> [[RewriteRule]])
-> HashMap QName [RewriteRule] -> [[RewriteRule]]
forall a b. (a -> b) -> a -> b
$ Signature
sig Signature
-> Lens' Signature (HashMap QName [RewriteRule])
-> HashMap QName [RewriteRule]
forall o i. o -> Lens' o i -> i
^. (HashMap QName [RewriteRule] -> f (HashMap QName [RewriteRule]))
-> Signature -> f Signature
Lens' Signature (HashMap QName [RewriteRule])
sigRewriteRules
    where
        rebind :: (PrimitiveId, QName) -> TCM ()
rebind (PrimitiveId
x, QName
q) = do
            PrimImpl _ pf <- PrimitiveId -> TCM PrimitiveImpl
lookupPrimitiveFunction PrimitiveId
x
            stImportedBuiltins `modifyTCLens` Map.insert (someBuiltin x) (Prim pf{ primFunName = q })

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

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

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

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

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

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

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

    when (miMode mi < mode) $
      throwError "previously-visited interface was not sufficiently checked"

    unless (null $ miWarnings mi) $
      throwError "previously-visited interface had warnings"

    reportSLn "import.visit" 10 $ "  Already visited " ++ prettyShow x

    lift $ processResultingModule mi

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

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

    return mi { miWarnings = wt }

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

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

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

    visitModule mi
    return mi


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

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

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

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

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

  -- For the main interface, we also remember the pragmas from the file
  Bool -> Source -> TCM ()
setOptionsFromSourcePragmas Bool
True Source
src
  loadPrims <- PragmaOptions -> Bool
optLoadPrimitives (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions

  when loadPrims $ do
    reportSLn "import.main" 10 "Importing the primitive modules."
    libdirPrim <- liftIO getPrimitiveLibDir
    reportSLn "import.main" 20 $ "Library primitive dir = " ++ show libdirPrim
    -- Turn off import-chasing messages.
    -- We have to modify the persistent verbosity setting, since
    -- getInterface resets the current verbosity settings to the persistent ones.

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

      -- We don't want to generate highlighting information for Agda.Primitive.
      withHighlightingLevel None $
        forM_ (Set.map (libdirPrim </>) Lens.primitiveModules) $ \[Char]
f -> do
          primSource <- SourceFile -> TCM Source
parseSource (AbsolutePath -> SourceFile
SourceFile (AbsolutePath -> SourceFile) -> AbsolutePath -> SourceFile
forall a b. (a -> b) -> a -> b
$ [Char] -> AbsolutePath
mkAbsolute [Char]
f)
          checkModuleName' (srcModuleName primSource) (srcOrigin primSource)
          void $ getNonMainInterface (srcModuleName primSource) (Just primSource)

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

  -- Now do the type checking via getInterface.
  checkModuleName' (srcModuleName src) (srcOrigin src)

  mi <- getInterface (srcModuleName src) (MainInterface mode) (Just src)

  stCurrentModule `setTCLens'`
    Just ( iModuleName (miInterface mi)
         , iTopLevelModuleName (miInterface mi)
         )

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

-- | 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.
  mi <- TCMT IO PragmaOptions
-> (PragmaOptions -> TCM ()) -> TCM ModuleInfo -> TCM ModuleInfo
forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ (Lens' TCState PragmaOptions -> TCMT IO PragmaOptions
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
Lens' TCState PragmaOptions
stPragmaOptions) ((PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
Lens' TCState PragmaOptions
stPragmaOptions Lens' TCState PragmaOptions -> PragmaOptions -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens`) (TCM ModuleInfo -> TCM ModuleInfo)
-> TCM ModuleInfo -> TCM ModuleInfo
forall a b. (a -> b) -> a -> b
$
          TopLevelModuleName
-> MainInterface -> Maybe Source -> TCM ModuleInfo
getInterface TopLevelModuleName
x MainInterface
NotMainInterface Maybe Source
msrc
  tcWarningsToError $ Set.toAscList $ miWarnings mi
  return (miInterface 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 =
  TopLevelModuleName -> TCM ModuleInfo -> TCM ModuleInfo
forall a. TopLevelModuleName -> TCM a -> TCM a
addImportCycleCheck TopLevelModuleName
x (TCM ModuleInfo -> TCM ModuleInfo)
-> TCM ModuleInfo -> TCM ModuleInfo
forall a b. (a -> b) -> a -> b
$ do
     -- We remember but reset the pragma options locally
     -- Issue #3644 (Abel 2020-05-08): Set approximate range for errors in options
     currentOptions <- Lens' TCState PragmaOptions -> TCMT IO PragmaOptions
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
Lens' TCState PragmaOptions
stPragmaOptions
     setCurrentRange (C.modPragmas . srcModule <$> msrc) $
       -- Now reset the options
       setCommandLineOptions . stPersistentOptions . stPersistentState =<< getTC

     alreadyVisited x isMain currentOptions $ do
      file <- case msrc of
        Maybe Source
Nothing  -> TopLevelModuleName -> TCMT IO SourceFile
findFile TopLevelModuleName
x
        Just Source
src -> do
          -- Andreas, 2021-08-17, issue #5508.
          -- So it happened with @msrc == Just{}@ that the file was not added to @ModuleToSource@,
          -- only with @msrc == Nothing@ (then @findFile@ does it).
          -- As a consequence, the file was added later, but with a file name constructed
          -- from a module name.  As #5508 shows, this can be fatal in case-insensitive file systems.
          -- The file name (with case variant) then no longer maps to the module name.
          -- To prevent this, we register the connection in @ModuleToSource@ here,
          -- where we have the correct spelling of the file name.
          let file :: SourceFile
file = Source -> SourceFile
srcOrigin Source
src
          Lens' TCState (Map TopLevelModuleName AbsolutePath)
-> (Map TopLevelModuleName AbsolutePath
    -> Map TopLevelModuleName AbsolutePath)
-> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
modifyTCLens (Map TopLevelModuleName AbsolutePath
 -> f (Map TopLevelModuleName AbsolutePath))
-> TCState -> f TCState
Lens' TCState (Map TopLevelModuleName AbsolutePath)
stModuleToSource ((Map TopLevelModuleName AbsolutePath
  -> Map TopLevelModuleName AbsolutePath)
 -> TCM ())
-> (Map TopLevelModuleName AbsolutePath
    -> Map TopLevelModuleName AbsolutePath)
-> TCM ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName
-> AbsolutePath
-> Map TopLevelModuleName AbsolutePath
-> Map TopLevelModuleName AbsolutePath
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TopLevelModuleName
x (SourceFile -> AbsolutePath
srcFilePath SourceFile
file)
          SourceFile -> TCMT IO SourceFile
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceFile
file
      reportSLn "import.iface" 15 $ List.intercalate "\n" $ map ("  " ++)
        [ "module: " ++ prettyShow x
        , "file:   " ++ prettyShow file
        ]

      reportSLn "import.iface" 10 $ "  Check for cycle"
      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
      stored <- runExceptT $ Bench.billTo [Bench.Import] $ do
        getStoredInterface x file msrc

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

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

            return modl

      either recheck pure stored

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

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

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

getOptionsCompatibilityWarnings :: MainInterface -> Bool -> PragmaOptions -> Interface -> TCM (Maybe (Set TCWarning))
getOptionsCompatibilityWarnings :: MainInterface
-> Bool
-> PragmaOptions
-> Interface
-> TCMT IO (Maybe (Set TCWarning))
getOptionsCompatibilityWarnings MainInterface
isMain Bool
isPrim PragmaOptions
currentOptions Interface
i = MaybeT (TCMT IO) (Set TCWarning) -> TCMT IO (Maybe (Set TCWarning))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (TCMT IO) (Set TCWarning)
 -> TCMT IO (Maybe (Set TCWarning)))
-> MaybeT (TCMT IO) (Set TCWarning)
-> TCMT IO (Maybe (Set TCWarning))
forall a b. (a -> b) -> a -> b
$ ExceptT [Char] (TCMT IO) (Set TCWarning)
-> MaybeT (TCMT IO) (Set TCWarning)
forall (m :: * -> *) e a. Functor m => ExceptT e m a -> MaybeT m a
exceptToMaybeT (ExceptT [Char] (TCMT IO) (Set TCWarning)
 -> MaybeT (TCMT IO) (Set TCWarning))
-> ExceptT [Char] (TCMT IO) (Set TCWarning)
-> MaybeT (TCMT IO) (Set TCWarning)
forall a b. (a -> b) -> a -> b
$ do
  -- We're just dropping these reasons-for-skipping messages for now.
  -- They weren't logged before, but they're nice for documenting the early returns.
  Bool -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when Bool
isPrim (ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ())
-> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
    [Char] -> ExceptT [Char] (TCMT IO) ()
forall a. [Char] -> ExceptT [Char] (TCMT IO) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"Options consistency checking disabled for always-available primitive module"
  ExceptT [Char] (TCMT IO) Bool
-> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (TCMT IO Bool -> ExceptT [Char] (TCMT IO) Bool
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Bool -> ExceptT [Char] (TCMT IO) Bool)
-> TCMT IO Bool -> ExceptT [Char] (TCMT IO) Bool
forall a b. (a -> b) -> a -> b
$ PragmaOptions
-> PragmaOptions -> TopLevelModuleName -> TCMT IO Bool
checkOptionsCompatible PragmaOptions
currentOptions (Interface -> PragmaOptions
iOptionsUsed Interface
i)
                  (Interface -> TopLevelModuleName
iTopLevelModuleName Interface
i)) (ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ())
-> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
    [Char] -> ExceptT [Char] (TCMT IO) ()
forall a. [Char] -> ExceptT [Char] (TCMT IO) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"No warnings to collect because options were compatible"
  TCMT IO (Set TCWarning) -> ExceptT [Char] (TCMT IO) (Set TCWarning)
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO (Set TCWarning)
 -> ExceptT [Char] (TCMT IO) (Set TCWarning))
-> TCMT IO (Set TCWarning)
-> ExceptT [Char] (TCMT IO) (Set TCWarning)
forall a b. (a -> b) -> a -> b
$ MainInterface -> WhichWarnings -> TCMT IO (Set TCWarning)
forall (m :: * -> *).
(ReadTCState m, MonadWarning m, MonadTCM m) =>
MainInterface -> WhichWarnings -> m (Set TCWarning)
getAllWarnings' MainInterface
isMain WhichWarnings
ErrorWarnings

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

getStoredInterface
  :: 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.
        ifile <- [Char]
-> MaybeT (TCMT IO) InterfaceFile
-> ExceptT [Char] (TCMT IO) InterfaceFile
forall (m :: * -> *) e a.
Functor m =>
e -> MaybeT m a -> ExceptT e m a
maybeToExceptT [Char]
"the interface file could not be found" (MaybeT (TCMT IO) InterfaceFile
 -> ExceptT [Char] (TCMT IO) InterfaceFile)
-> MaybeT (TCMT IO) InterfaceFile
-> ExceptT [Char] (TCMT IO) InterfaceFile
forall a b. (a -> b) -> a -> b
$ TCMT IO (Maybe InterfaceFile) -> MaybeT (TCMT IO) InterfaceFile
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe InterfaceFile) -> MaybeT (TCMT IO) InterfaceFile)
-> TCMT IO (Maybe InterfaceFile) -> MaybeT (TCMT IO) InterfaceFile
forall a b. (a -> b) -> a -> b
$
          SourceFile -> TCMT IO (Maybe InterfaceFile)
findInterfaceFile' SourceFile
file

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

        return (ifile, hashes)

  -- Examine the hash of the interface file. If it is different from the
  -- stored version (in stDecodedModules), or if there is no stored version,
  -- read and decode it. Otherwise use the stored version.
  --
  -- This is a lazy action which may be skipped if the cached or on-disk interface
  -- is invalid, missing, or skipped for some other reason.
  let checkSourceHashET :: Hash -> ExceptT [Char] (TCMT IO) ()
checkSourceHashET Hash
ifaceH = do
        sourceH <- case Maybe Source
msrc of
                    Maybe Source
Nothing -> IO Hash -> ExceptT [Char] (TCMT IO) Hash
forall a. IO a -> ExceptT [Char] (TCMT IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Hash -> ExceptT [Char] (TCMT IO) Hash)
-> IO Hash -> ExceptT [Char] (TCMT IO) Hash
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> IO Hash
hashTextFile (SourceFile -> AbsolutePath
srcFilePath SourceFile
file)
                    Just Source
src -> Hash -> ExceptT [Char] (TCMT IO) Hash
forall a. a -> ExceptT [Char] (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Hash -> ExceptT [Char] (TCMT IO) Hash)
-> Hash -> ExceptT [Char] (TCMT IO) Hash
forall a b. (a -> b) -> a -> b
$ Text -> Hash
hashText (Source -> Text
srcText Source
src)

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

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

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

      ExceptT [Char] (TCMT IO) Bool
-> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ExceptT [Char] (TCMT IO) Bool
forall (m :: * -> *). HasOptions m => m Bool
ignoreInterfaces (ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ())
-> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
        ExceptT [Char] (TCMT IO) Bool
-> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (TCMT IO Bool -> ExceptT [Char] (TCMT IO) Bool
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Bool -> ExceptT [Char] (TCMT IO) Bool)
-> TCMT IO Bool -> ExceptT [Char] (TCMT IO) Bool
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Bool
forall (m :: * -> *). MonadIO m => [Char] -> m Bool
Lens.isBuiltinModule (AbsolutePath -> [Char]
filePath (AbsolutePath -> [Char]) -> AbsolutePath -> [Char]
forall a b. (a -> b) -> a -> b
$ SourceFile -> AbsolutePath
srcFilePath SourceFile
file)) (ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ())
-> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
            [Char] -> ExceptT [Char] (TCMT IO) ()
forall a. [Char] -> ExceptT [Char] (TCMT IO) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"we're ignoring non-builtin interface files"

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

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

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

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

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

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

        isPrimitiveModule <- lift $ Lens.isPrimitiveModule (filePath $ srcFilePath file)

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

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

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

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

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

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

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

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

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

reportWarningsForModule :: MonadDebug m => TopLevelModuleName -> Set TCWarning -> m ()
reportWarningsForModule :: forall (m :: * -> *).
MonadDebug m =>
TopLevelModuleName -> Set TCWarning -> m ()
reportWarningsForModule TopLevelModuleName
x Set TCWarning
warns = do
  [TCWarning] -> ([TCWarning] -> m ()) -> m ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull ((TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Maybe TopLevelModuleName -> Maybe (Maybe TopLevelModuleName)
forall a. a -> Maybe a
Strict.Just (TopLevelModuleName -> Maybe TopLevelModuleName
forall a. a -> Maybe a
Just TopLevelModuleName
x) Maybe (Maybe TopLevelModuleName)
-> Maybe (Maybe TopLevelModuleName) -> Bool
forall a. Eq a => a -> a -> Bool
==) (Maybe (Maybe TopLevelModuleName) -> Bool)
-> (TCWarning -> Maybe (Maybe TopLevelModuleName))
-> TCWarning
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RangeFile -> Maybe TopLevelModuleName)
-> Maybe RangeFile -> Maybe (Maybe TopLevelModuleName)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RangeFile -> Maybe TopLevelModuleName
rangeFileName (Maybe RangeFile -> Maybe (Maybe TopLevelModuleName))
-> (TCWarning -> Maybe RangeFile)
-> TCWarning
-> Maybe (Maybe TopLevelModuleName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Maybe RangeFile
tcWarningOrigin) ([TCWarning] -> [TCWarning]) -> [TCWarning] -> [TCWarning]
forall a b. (a -> b) -> a -> b
$ Set TCWarning -> [TCWarning]
forall a. Set a -> [a]
Set.toAscList Set TCWarning
warns) \ [TCWarning]
ws ->
    [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
alwaysReportSDoc [Char]
"warning" Int
1 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
P.vsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (TCWarning -> TCMT IO Doc) -> [TCWarning] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map TCWarning -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
P.prettyTCM [TCWarning]
ws


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 (AbsolutePath -> [Char]) -> AbsolutePath -> [Char]
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
  [Char] -> Int -> [Char] -> ExceptT [Char] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
5 ([Char] -> ExceptT [Char] (TCMT IO) ())
-> [Char] -> ExceptT [Char] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  imports: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [(TopLevelModuleName, Hash)] -> [Char]
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)
  libOptions <- TCMT IO [OptionsPragma] -> ExceptT [Char] (TCMT IO) [OptionsPragma]
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO [OptionsPragma]
 -> ExceptT [Char] (TCMT IO) [OptionsPragma])
-> TCMT IO [OptionsPragma]
-> ExceptT [Char] (TCMT IO) [OptionsPragma]
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> TopLevelModuleName -> TCMT IO [OptionsPragma]
getLibraryOptions
    (SourceFile -> AbsolutePath
srcFilePath SourceFile
file)
    (Interface -> TopLevelModuleName
iTopLevelModuleName Interface
i)
  lift $ mapM_ setOptionsFromPragma (libOptions ++ iFilePragmaOptions i)

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

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

  unlessNull badHashMessages (throwError . unlines)

  reportSLn "import.iface" 5 "  New module. Let's check it out."
  lift $ mergeInterface i
  Bench.billTo [Bench.Highlighting] $
    lift $ ifTopLevelAndHighlightingLevelIs NonInteractive $
      highlightFromInterface i file

  return mi

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

createInterfaceIsolated
  :: TopLevelModuleName
     -- ^ Module name of file we process.
  -> SourceFile
     -- ^ File we process.
  -> Maybe Source
     -- ^ Optional: the source code and some information about the source code.
  -> TCM ModuleInfo
createInterfaceIsolated :: TopLevelModuleName -> SourceFile -> Maybe Source -> TCM ModuleInfo
createInterfaceIsolated TopLevelModuleName
x SourceFile
file Maybe Source
msrc = do
      TCM ()
forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog

      ms          <- TCM [TopLevelModuleName]
getImportPath
      range       <- asksTC envRange
      call        <- asksTC envCall
      mf          <- useTC stModuleToSource
      vs          <- getVisitedModules
      ds          <- getDecodedModules
      opts        <- stPersistentOptions . stPersistentState <$> getTC
      isig        <- useTC stImports
      metas       <- useTC stImportedMetaStore
      ibuiltin    <- useTC stImportedBuiltins
      display     <- useTC stImportsDisplayForms
      userwarn    <- useTC stImportedUserWarnings
      partialdefs <- useTC stImportedPartialDefs
      opaqueblk   <- useTC stOpaqueBlocks
      opaqueid    <- useTC stOpaqueIds
      ipatsyns <- getPatternSynImports
      ho       <- 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.
      (mi, newModToSource, newDecodedModules) <- (either throwError pure =<<) $
           withoutCache $
           -- The cache should not be used for an imported module, and it
           -- should be restored after the module has been type-checked
           freshTCM $
             withImportPath ms $
             localTC (\TCEnv
e -> TCEnv
e
                              -- Andreas, 2014-08-18:
                              -- Preserve the range of import statement
                              -- for reporting termination errors in
                              -- imported modules:
                            { envRange              = range
                            , envCall               = call
                            }) $ do
               setDecodedModules ds
               setCommandLineOptions opts
               setInteractionOutputCallback ho
               stModuleToSource `setTCLens` mf
               setVisitedModules vs
               addImportedThings isig metas ibuiltin ipatsyns display
                 userwarn partialdefs empty opaqueblk opaqueid

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

      stModuleToSource `setTCLens` newModToSource
      setDecodedModules newDecodedModules

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

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

      either recheckOnError pure validated


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

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

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

highlightFromInterface
  :: Interface
  -> SourceFile
     -- ^ The corresponding file.
  -> TCM ()
highlightFromInterface :: Interface -> SourceFile -> TCM ()
highlightFromInterface Interface
i SourceFile
file = do
  [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface" Int
5 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$
    [Char]
"Generating syntax info for " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ AbsolutePath -> [Char]
filePath (SourceFile -> AbsolutePath
srcFilePath SourceFile
file) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++
    [Char]
" (read from interface)."
  RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting (Interface -> HighlightingInfo
iHighlighting Interface
i)

-- | Read interface file corresponding to a module.

readInterface :: InterfaceFile -> TCM (Maybe Interface)
readInterface :: InterfaceFile -> TCMT IO (Maybe Interface)
readInterface InterfaceFile
file = do
    let ifp :: [Char]
ifp = AbsolutePath -> [Char]
filePath (AbsolutePath -> [Char]) -> AbsolutePath -> [Char]
forall a b. (a -> b) -> a -> b
$ InterfaceFile -> AbsolutePath
intFilePath InterfaceFile
file
    -- Decode the interface file
    (s, close) <- IO (ByteString, IO ()) -> TCMT IO (ByteString, IO ())
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ByteString, IO ()) -> TCMT IO (ByteString, IO ()))
-> IO (ByteString, IO ()) -> TCMT IO (ByteString, IO ())
forall a b. (a -> b) -> a -> b
$ [Char] -> IO (ByteString, IO ())
readBinaryFile' [Char]
ifp
    do  mi <- liftIO . E.evaluate =<< decodeInterface 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.
        liftIO close

        return $ constructIScope <$> mi
      -- Catch exceptions and close
      `catchError` \TCErr
e -> IO () -> TCM ()
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO ()
close TCM () -> TCMT IO (Maybe Interface) -> TCMT IO (Maybe Interface)
forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TCErr -> TCMT IO (Maybe Interface)
forall {a}. TCErr -> TCMT IO (Maybe a)
handler TCErr
e
  -- Catch exceptions
  TCMT IO (Maybe Interface)
-> (TCErr -> TCMT IO (Maybe Interface))
-> TCMT IO (Maybe Interface)
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` TCErr -> TCMT IO (Maybe Interface)
forall {a}. TCErr -> TCMT IO (Maybe a)
handler
  where
    handler :: TCErr -> TCMT IO (Maybe a)
handler = \case
      IOException Maybe TCState
_ Range
_ IOException
e -> do
        [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
alwaysReportSLn [Char]
"" Int
0 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"IO exception: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ IOException -> [Char]
forall a. Show a => a -> [Char]
show IOException
e
        Maybe a -> TCMT IO (Maybe a)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing   -- Work-around for file locking bug.
                         -- TODO: What does this refer to? Please
                         -- document.
      TCErr
e -> TCErr -> TCMT IO (Maybe a)
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
e

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

writeInterface :: AbsolutePath -> Interface -> TCM Interface
writeInterface :: AbsolutePath -> Interface -> TCMT IO Interface
writeInterface AbsolutePath
file Interface
i = let fp :: [Char]
fp = AbsolutePath -> [Char]
filePath AbsolutePath
file in do
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"import.iface.write" Int
5  ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$
      [Char]
"Writing interface file " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
fp [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"."
    -- Andreas, 2015-07-13
    -- After QName memoization (AIM XXI), scope serialization might be cheap enough.
    -- -- Andreas, Makoto, 2014-10-18 AIM XX:
    -- -- iInsideScope is bloating the interface files, so we do not serialize it?
    -- i <- return $
    --   i { iInsideScope  = emptyScopeInfo
    --     }
    -- [Old: Andreas, 2016-02-02 this causes issue #1804, so don't do it:]
    -- Andreas, 2020-05-13, #1804, #4647: removed private declarations
    -- only when we actually write the interface.
    let
      filteredIface :: Interface
filteredIface = Interface
i { iInsideScope = withoutPrivates $ iInsideScope i }
    filteredIface <- Interface -> TCMT IO Interface
pruneTemporaryInstances Interface
filteredIface
    reportSLn "import.iface.write" 50 $
      "Writing interface file with hash " ++ show (iFullHash filteredIface) ++ "."
    encodedIface <- encodeFile fp filteredIface
    reportSLn "import.iface.write" 5 "Wrote interface file."
    fromMaybe __IMPOSSIBLE__ <$> (Bench.billTo [Bench.Deserialization] (decode encodedIface))
  TCMT IO Interface
-> (TCErr -> TCMT IO Interface) -> TCMT IO Interface
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
e -> do
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
alwaysReportSLn [Char]
"" Int
1 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$
      [Char]
"Failed to write interface " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
fp [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"."
    IO () -> TCM ()
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$
      IO Bool -> IO () -> IO ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ([Char] -> IO Bool
doesFileExist [Char]
fp) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
removeFile [Char]
fp
    TCErr -> TCMT IO Interface
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
e

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

createInterface
  :: TopLevelModuleName    -- ^ The expected module name.
  -> SourceFile            -- ^ The file to type check.
  -> MainInterface         -- ^ Are we dealing with the main module?
  -> Maybe Source      -- ^ Optional information about the source code.
  -> TCM ModuleInfo
createInterface :: TopLevelModuleName
-> SourceFile -> MainInterface -> Maybe Source -> TCM ModuleInfo
createInterface TopLevelModuleName
mname SourceFile
file MainInterface
isMain Maybe Source
msrc = do
  let x :: TopLevelModuleName
x = TopLevelModuleName
mname
  let fp :: [Char]
fp = AbsolutePath -> [Char]
filePath (AbsolutePath -> [Char]) -> AbsolutePath -> [Char]
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 = TCM () -> (() -> TCM ()) -> TCM ModuleInfo -> TCM ModuleInfo
forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_
       ([Char] -> TopLevelModuleName -> Maybe [Char] -> TCM ()
chaseMsg [Char]
checkMsg TopLevelModuleName
x (Maybe [Char] -> TCM ()) -> Maybe [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
fp)
       (TCM () -> () -> TCM ()
forall a b. a -> b -> a
const (TCM () -> () -> TCM ()) -> TCM () -> () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do ws <- WhichWarnings -> TCMT IO (Set TCWarning)
forall (m :: * -> *).
(ReadTCState m, MonadWarning m, MonadTCM m) =>
WhichWarnings -> m (Set TCWarning)
getAllWarnings WhichWarnings
AllWarnings
                   let classified = [TCWarning] -> WarningsAndNonFatalErrors
classifyWarnings ([TCWarning] -> WarningsAndNonFatalErrors)
-> [TCWarning] -> WarningsAndNonFatalErrors
forall a b. (a -> b) -> a -> b
$ Set TCWarning -> [TCWarning]
forall a. Set a -> [a]
Set.toAscList Set TCWarning
ws
                   reportWarningsForModule mname $ tcWarnings classified
                   when (null (nonFatalErrors classified)) $ chaseMsg "Finished" x Nothing)

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

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

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

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

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

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

    -- Only check consistency if not main (we check consistency for the main module in
    -- `typeCheckMain`.
    let checkConsistency | MainInterface{} <- MainInterface
isMain = Bool
False
                         | Bool
otherwise                 = Bool
True
    setOptionsFromSourcePragmas checkConsistency src
    checkAttributes (srcAttributes src)
    syntactic <- optSyntacticEquality <$> pragmaOptions
    localTC (\TCEnv
env -> TCEnv
env { envSyntacticEqualityFuel = syntactic }) $ do

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

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

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

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


    -- Type checking.

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

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

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

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

    unfreezeMetas

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

    -- Highlighting from type checker.
    reportSLn "import.iface.create" 7 "Starting highlighting from type info."
    Bench.billTo [Bench.Highlighting] $ do

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

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

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

      whenM (optGenerateVimFile <$> commandLineOptions) $
        -- Generate Vim file.
        withScope_ scope $ generateVimFile $ filePath $ srcPath
    reportSLn "import.iface.create" 7 "Finished highlighting from type info."

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

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

    openMetas           <- getOpenMetas
    unless (null openMetas) $ do
      reportSLn "import.metas" 10 "We have unsolved metas."
      reportSLn "import.metas" 10 =<< showGoals =<< getGoals

    ifTopLevelAndHighlightingLevelIs NonInteractive printUnsolvedInfo

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

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

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

    mallWarnings <- getAllWarnings' isMain ErrorWarnings

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

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

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

    -- Get the statistics of the current module
    -- and add it to the accumulated statistics.
    localStatistics <- getStatistics
    lensAccumStatistics `modifyTCLens` Map.unionWith (+) localStatistics
    reportSLn "import.iface" 5 "Accumulated statistics."

    isPrimitiveModule <- Lens.isPrimitiveModule (filePath srcPath)

    return ModuleInfo
      { miInterface = finalIface
      , miWarnings = mallWarnings
      , miPrimitive = isPrimitiveModule
      , miMode = moduleCheckMode isMain
      }

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

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

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

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

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

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

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

    let !scope = TopLevelInfo -> ScopeInfo
topLevelScope TopLevelInfo
topLevel

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

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

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

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

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

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

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

-- | Returns (iSourceHash, iFullHash)
--   We do not need to check that the file exist because we only
--   accept @InterfaceFile@ as an input and not arbitrary @AbsolutePath@!
getInterfaceFileHashes :: InterfaceFile -> IO (Maybe (Hash, Hash))
getInterfaceFileHashes :: InterfaceFile -> IO (Maybe (Hash, Hash))
getInterfaceFileHashes InterfaceFile
fp = do
  let ifile :: [Char]
ifile = AbsolutePath -> [Char]
filePath (AbsolutePath -> [Char]) -> AbsolutePath -> [Char]
forall a b. (a -> b) -> a -> b
$ InterfaceFile -> AbsolutePath
intFilePath InterfaceFile
fp
  (s, close) <- [Char] -> IO (ByteString, IO ())
readBinaryFile' [Char]
ifile
  let hs = ByteString -> Maybe (Hash, Hash)
decodeHashes ByteString
s
  maybe 0 (uncurry (+)) hs `seq` close
  return hs

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