{-# LANGUAGE CPP #-}

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

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

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

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

import Prelude hiding (null)

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

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

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

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

import Agda.Benchmarking

import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Concrete as C
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.Translation.ConcreteToAbstract

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

import Agda.TheTypeChecker

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

import Agda.Utils.FileName
import Agda.Utils.Lens
import Agda.Utils.Maybe
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.IO.Binary
import Agda.Utils.Pretty hiding (Mode)
import Agda.Utils.Hash
import qualified Agda.Utils.Trie as Trie

import Agda.Utils.Impossible

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

ignoreInterfaces :: HasOptions m => m Bool
ignoreInterfaces :: 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 :: 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  :: C.TopLevelModuleName  -- ^ The top-level module name.
  , Source -> [AgdaLibFile]
srcProjectLibs :: [AgdaLibFile]         -- ^ The .agda-lib file(s) of the project this file belongs to.
  }

-- | 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
  Text
source                <- PM Text -> TCM Text
forall a. PM a -> TCM a
runPM (PM Text -> TCM Text) -> PM Text -> TCM Text
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> PM Text
readFilePM AbsolutePath
f
  (Module
parsedMod, FileType
fileType) <- PM (Module, FileType) -> TCM (Module, FileType)
forall a. PM a -> TCM a
runPM (PM (Module, FileType) -> TCM (Module, FileType))
-> PM (Module, FileType) -> TCM (Module, FileType)
forall a b. (a -> b) -> a -> b
$
                           Parser Module -> AbsolutePath -> String -> PM (Module, FileType)
forall a.
Show a =>
Parser a -> AbsolutePath -> String -> PM (a, FileType)
parseFile Parser Module
moduleParser AbsolutePath
f (String -> PM (Module, FileType))
-> String -> PM (Module, FileType)
forall a b. (a -> b) -> a -> b
$ Text -> String
TL.unpack Text
source
  TopLevelModuleName
parsedModName         <- AbsolutePath -> Module -> TCM TopLevelModuleName
moduleName AbsolutePath
f Module
parsedMod
  [AgdaLibFile]
libs <- String -> TCM [AgdaLibFile]
getAgdaLibFiles (String -> TCM [AgdaLibFile]) -> String -> TCM [AgdaLibFile]
forall a b. (a -> b) -> a -> b
$ String -> String
takeDirectory (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> String
filePath AbsolutePath
f
  Source -> TCM Source
forall (m :: * -> *) a. Monad m => a -> m a
return Source :: Text
-> FileType
-> SourceFile
-> Module
-> TopLevelModuleName
-> [AgdaLibFile]
-> Source
Source
    { srcText :: Text
srcText        = Text
source
    , srcFileType :: FileType
srcFileType    = FileType
fileType
    , srcOrigin :: SourceFile
srcOrigin      = SourceFile
sourceFile
    , srcModule :: Module
srcModule      = Module
parsedMod
    , srcModuleName :: TopLevelModuleName
srcModuleName  = TopLevelModuleName
parsedModName
    , srcProjectLibs :: [AgdaLibFile]
srcProjectLibs = [AgdaLibFile]
libs
    }

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
opts | C.OptionsPragma Range
_ OptionsPragma
opts <- [Pragma]
cpragmas ]

srcPragmas :: Source -> [OptionsPragma]
srcPragmas :: Source -> [OptionsPragma]
srcPragmas Source
src = Source -> [OptionsPragma]
srcDefaultPragmas Source
src [OptionsPragma] -> [OptionsPragma] -> [OptionsPragma]
forall a. [a] -> [a] -> [a]
++ Source -> [OptionsPragma]
srcFilePragmas Source
src

-- | Set options from a 'Source' pragma, using the source
--   ranges of the pragmas for error reporting.
setOptionsFromSourcePragmas :: Source -> TCM ()
setOptionsFromSourcePragmas :: Source -> TCM ()
setOptionsFromSourcePragmas Source
src =
  [Pragma] -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (Module -> [Pragma]
C.modPragmas (Module -> [Pragma]) -> (Source -> Module) -> Source -> [Pragma]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Source -> Module
srcModule (Source -> [Pragma]) -> Source -> [Pragma]
forall a b. (a -> b) -> a -> b
$ Source
src) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    (OptionsPragma -> TCM ()) -> [OptionsPragma] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ OptionsPragma -> TCM ()
setOptionsFromPragma (Source -> [OptionsPragma]
srcPragmas Source
src)

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

data Mode
  = ScopeCheck
  | TypeCheck
  deriving (Mode -> Mode -> Bool
(Mode -> Mode -> Bool) -> (Mode -> Mode -> Bool) -> Eq Mode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Mode -> Mode -> Bool
$c/= :: Mode -> Mode -> Bool
== :: Mode -> Mode -> Bool
$c== :: Mode -> Mode -> Bool
Eq, Int -> Mode -> String -> String
[Mode] -> String -> String
Mode -> String
(Int -> Mode -> String -> String)
-> (Mode -> String) -> ([Mode] -> String -> String) -> Show Mode
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Mode] -> String -> String
$cshowList :: [Mode] -> String -> String
show :: Mode -> String
$cshow :: Mode -> String
showsPrec :: Int -> Mode -> String -> String
$cshowsPrec :: Int -> Mode -> String -> String
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
/= :: MainInterface -> MainInterface -> Bool
$c/= :: MainInterface -> MainInterface -> Bool
== :: MainInterface -> MainInterface -> Bool
$c== :: MainInterface -> MainInterface -> Bool
Eq, Int -> MainInterface -> String -> String
[MainInterface] -> String -> String
MainInterface -> String
(Int -> MainInterface -> String -> String)
-> (MainInterface -> String)
-> ([MainInterface] -> String -> String)
-> Show MainInterface
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [MainInterface] -> String -> String
$cshowList :: [MainInterface] -> String -> String
show :: MainInterface -> String
$cshow :: MainInterface -> String
showsPrec :: Int -> MainInterface -> String -> String
$cshowsPrec :: Int -> MainInterface -> String -> String
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 :: [(String, Builtin (String, QName))]
builtin = Map String (Builtin (String, QName))
-> [(String, Builtin (String, QName))]
forall k a. Map k a -> [(k, a)]
Map.toAscList (Map String (Builtin (String, QName))
 -> [(String, Builtin (String, QName))])
-> Map String (Builtin (String, QName))
-> [(String, Builtin (String, QName))]
forall a b. (a -> b) -> a -> b
$ Interface -> Map String (Builtin (String, QName))
iBuiltin Interface
i
        prim :: [(String, QName)]
prim    = [ (String, QName)
x | (String
_,Prim (String, QName)
x) <- [(String, Builtin (String, QName))]
builtin ]
        bi :: Map String (Builtin PrimFun)
bi      = [(String, Builtin PrimFun)] -> Map String (Builtin PrimFun)
forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList [ (String
x, Term -> Builtin PrimFun
forall pf. Term -> Builtin pf
Builtin Term
t) | (String
x, Builtin Term
t) <- [(String, Builtin (String, QName))]
builtin ]
                    -- Andreas, 2021-08-19: this seeming identity filters out the @Prim@s
                    -- and converts the type.
        warns :: [TCWarning]
warns   = Interface -> [TCWarning]
iWarnings Interface
i
    Map String (Builtin PrimFun)
bs <- (TCState -> Map String (Builtin PrimFun))
-> TCMT IO (Map String (Builtin PrimFun))
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC TCState -> Map String (Builtin PrimFun)
stBuiltinThings
    String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface.merge" Int
10 String
"Merging interface"
    String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface.merge" Int
20 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$
      String
"  Current builtins " String -> String -> String
forall a. [a] -> [a] -> [a]
++ OptionsPragma -> String
forall a. Show a => a -> String
show (Map String (Builtin PrimFun) -> OptionsPragma
forall k a. Map k a -> [k]
Map.keys Map String (Builtin PrimFun)
bs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String
"  New builtins     " String -> String -> String
forall a. [a] -> [a] -> [a]
++ OptionsPragma -> String
forall a. Show a => a -> String
show (Map String (Builtin PrimFun) -> OptionsPragma
forall k a. Map k a -> [k]
Map.keys Map String (Builtin PrimFun)
bi)
    let check :: String -> Builtin pf -> Builtin pf -> m ()
check String
b (Builtin Term
x) (Builtin Term
y)
              | Term
x Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
y    = () -> m ()
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
$ String -> Term -> Term -> TypeError
DuplicateBuiltinBinding String
b Term
x Term
y
        check String
_ Builtin pf
_ Builtin pf
_ = m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
    Map String (TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ (Map String (TCM ()) -> TCM ()) -> Map String (TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ (String -> Builtin PrimFun -> Builtin PrimFun -> TCM ())
-> Map String (Builtin PrimFun)
-> Map String (Builtin PrimFun)
-> Map String (TCM ())
forall k a b c.
Ord k =>
(k -> a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWithKey String -> Builtin PrimFun -> Builtin PrimFun -> TCM ()
forall (m :: * -> *) pf pf.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> Builtin pf -> Builtin pf -> m ()
check Map String (Builtin PrimFun)
bs Map String (Builtin PrimFun)
bi
    Signature
-> Map String (Builtin PrimFun)
-> PatternSynDefns
-> DisplayForms
-> Map QName Text
-> Set QName
-> [TCWarning]
-> TCM ()
addImportedThings Signature
sig Map String (Builtin PrimFun)
bi
      (Interface -> PatternSynDefns
iPatternSyns Interface
i)
      (Interface -> DisplayForms
iDisplayForms Interface
i)
      (Interface -> Map QName Text
iUserWarnings Interface
i)
      (Interface -> Set QName
iPartialDefs Interface
i)
      [TCWarning]
warns
    String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface.merge" Int
20 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$
      String
"  Rebinding primitives " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(String, QName)] -> String
forall a. Show a => a -> String
show [(String, QName)]
prim
    ((String, QName) -> TCM ()) -> [(String, QName)] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String, QName) -> TCM ()
rebind [(String, QName)]
prim
    TCMT IO (Maybe ConfluenceCheck)
-> (ConfluenceCheck -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (PragmaOptions -> Maybe ConfluenceCheck
optConfluenceCheck (PragmaOptions -> Maybe ConfluenceCheck)
-> TCMT IO PragmaOptions -> TCMT IO (Maybe ConfluenceCheck)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) ((ConfluenceCheck -> TCM ()) -> TCM ())
-> (ConfluenceCheck -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ConfluenceCheck
confChk -> do
      String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface.confluence" Int
20 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ String
"  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' (HashMap QName [RewriteRule]) Signature
-> HashMap QName [RewriteRule]
forall o i. o -> Lens' i o -> i
^. Lens' (HashMap QName [RewriteRule]) Signature
sigRewriteRules
    where
        rebind :: (String, QName) -> TCM ()
rebind (String
x, QName
q) = do
            PrimImpl Type
_ PrimFun
pf <- String -> TCM PrimitiveImpl
lookupPrimitiveFunction String
x
            Lens' (Map String (Builtin PrimFun)) TCState
stImportedBuiltins Lens' (Map String (Builtin PrimFun)) TCState
-> (Map String (Builtin PrimFun) -> Map String (Builtin PrimFun))
-> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` String
-> Builtin PrimFun
-> Map String (Builtin PrimFun)
-> Map String (Builtin PrimFun)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
x (PrimFun -> Builtin PrimFun
forall pf. pf -> Builtin pf
Prim PrimFun
pf{ primFunName :: QName
primFunName = QName
q })

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

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

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

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

    -- let s = publicModules $ iInsideScope i
    let s :: Map ModuleName Scope
s = Interface -> Map ModuleName Scope
iScope Interface
i
    (ModuleName, Map ModuleName Scope)
-> TCM (ModuleName, Map ModuleName Scope)
forall (m :: * -> *) a. Monad m => a -> m a
return (Interface -> ModuleName
iModuleName Interface
i ModuleName -> QName -> ModuleName
`withRangesOfQ` ModuleName -> QName
mnameToConcrete ModuleName
x, Map ModuleName Scope
s)

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

alreadyVisited :: C.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 String (TCMT IO) ModuleInfo -> MaybeT (TCMT IO) ModuleInfo
forall (m :: * -> *) e a. Functor m => ExceptT e m a -> MaybeT m a
exceptToMaybeT (ExceptT String (TCMT IO) ModuleInfo
 -> MaybeT (TCMT IO) ModuleInfo)
-> ExceptT String (TCMT IO) ModuleInfo
-> MaybeT (TCMT IO) ModuleInfo
forall a b. (a -> b) -> a -> b
$ do
    ModuleInfo
mi <- String
-> MaybeT (TCMT IO) ModuleInfo
-> ExceptT String (TCMT IO) ModuleInfo
forall (m :: * -> *) e a.
Functor m =>
e -> MaybeT m a -> ExceptT e m a
maybeToExceptT String
"interface has not been visited in this context" (MaybeT (TCMT IO) ModuleInfo
 -> ExceptT String (TCMT IO) ModuleInfo)
-> MaybeT (TCMT IO) ModuleInfo
-> ExceptT String (TCMT IO) ModuleInfo
forall a b. (a -> b) -> a -> b
$ TCMT IO (Maybe ModuleInfo) -> MaybeT (TCMT IO) ModuleInfo
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe ModuleInfo) -> MaybeT (TCMT IO) ModuleInfo)
-> TCMT IO (Maybe ModuleInfo) -> MaybeT (TCMT IO) ModuleInfo
forall a b. (a -> b) -> a -> b
$
      TopLevelModuleName -> TCMT IO (Maybe ModuleInfo)
forall (m :: * -> *).
ReadTCState m =>
TopLevelModuleName -> m (Maybe ModuleInfo)
getVisitedModule TopLevelModuleName
x

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

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

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

    TCM ModuleInfo -> ExceptT String (TCMT IO) ModuleInfo
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM ModuleInfo -> ExceptT String (TCMT IO) ModuleInfo)
-> TCM ModuleInfo -> ExceptT String (TCMT IO) ModuleInfo
forall a b. (a -> b) -> a -> b
$ ModuleInfo -> TCM ModuleInfo
processResultingModule ModuleInfo
mi

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

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

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

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

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

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

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


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

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

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

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

typeCheckMain
  :: Mode
     -- ^ Should the file be type-checked, or only scope-checked?
  -> Source
     -- ^ The decorated source code.
  -> TCM CheckResult
typeCheckMain :: Mode -> Source -> TCM CheckResult
typeCheckMain Mode
mode Source
src = do
  -- liftIO $ putStrLn $ "This is typeCheckMain " ++ prettyShow f
  -- liftIO . putStrLn . show =<< getVerbosity
  String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.main" Int
10 String
"Importing the primitive modules."
  String
libdirPrim <- IO String -> TCMT IO String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO String
getPrimitiveLibDir
  String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.main" Int
20 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ String
"Library primitive dir = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
libdirPrim
  -- Turn off import-chasing messages.
  -- We have to modify the persistent verbosity setting, since
  -- getInterface resets the current verbosity settings to the persistent ones.
  TCMT IO PersistentVerbosity
-> (PersistentVerbosity -> TCM ()) -> TCM () -> TCM ()
forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ ((TCState -> PersistentVerbosity) -> TCMT IO PersistentVerbosity
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC TCState -> PersistentVerbosity
forall a. LensPersistentVerbosity a => a -> PersistentVerbosity
Lens.getPersistentVerbosity) PersistentVerbosity -> TCM ()
forall (m :: * -> *). MonadTCState m => PersistentVerbosity -> m ()
Lens.putPersistentVerbosity (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    (PersistentVerbosity -> PersistentVerbosity) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(PersistentVerbosity -> PersistentVerbosity) -> m ()
Lens.modifyPersistentVerbosity (OptionsPragma -> PersistentVerbosity -> PersistentVerbosity
forall k v. Ord k => [k] -> Trie k v -> Trie k v
Trie.delete [])  -- set root verbosity to 0

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

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

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

  -- For the main interface, we also remember the pragmas from the file
  Source -> TCM ()
setOptionsFromSourcePragmas Source
src

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

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

  CheckResult -> TCM CheckResult
forall (m :: * -> *) a. Monad m => a -> m a
return (CheckResult -> TCM CheckResult) -> CheckResult -> TCM CheckResult
forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Source -> CheckResult
CheckResult' ModuleInfo
mi Source
src
  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
  :: C.TopLevelModuleName
  -> Maybe Source
     -- ^ Optional: the source code and some information about the source code.
  -> TCM Interface
getNonMainInterface :: TopLevelModuleName -> Maybe Source -> TCMT IO Interface
getNonMainInterface TopLevelModuleName
x Maybe Source
msrc = do
  -- Preserve/restore the current pragma options, which will be mutated when loading
  -- and checking the interface.
  ModuleInfo
mi <- 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' PragmaOptions TCState -> TCMT IO PragmaOptions
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' PragmaOptions TCState
stPragmaOptions) (Lens' PragmaOptions TCState
stPragmaOptions Lens' PragmaOptions TCState -> PragmaOptions -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> 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
  [TCWarning] -> TCM ()
tcWarningsToError ([TCWarning] -> TCM ()) -> [TCWarning] -> TCM ()
forall a b. (a -> b) -> a -> b
$ ModuleInfo -> [TCWarning]
miWarnings ModuleInfo
mi
  Interface -> TCMT IO Interface
forall (m :: * -> *) a. Monad m => a -> m a
return (ModuleInfo -> Interface
miInterface ModuleInfo
mi)

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

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

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

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

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

      let recheck :: String -> TCM ModuleInfo
recheck = \String
reason -> do
            String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface" Int
5 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ OptionsPragma -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"  ", TopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow TopLevelModuleName
x, String
" is not up-to-date because ", String
reason, String
"."]
            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
            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

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

-- | Check if the options used for checking an imported module are
--   compatible with the current options. Raises Non-fatal errors if
--   not.
checkOptionsCompatible :: PragmaOptions -> PragmaOptions -> ModuleName -> TCM Bool
checkOptionsCompatible :: PragmaOptions -> PragmaOptions -> ModuleName -> TCM Bool
checkOptionsCompatible PragmaOptions
current PragmaOptions
imported ModuleName
importedModule = (StateT Bool (TCMT IO) () -> Bool -> TCM Bool)
-> Bool -> StateT Bool (TCMT IO) () -> TCM Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT Bool (TCMT IO) () -> Bool -> TCM Bool
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT Bool
True (StateT Bool (TCMT IO) () -> TCM Bool)
-> StateT Bool (TCMT IO) () -> TCM Bool
forall a b. (a -> b) -> a -> b
$ do
  String -> Int -> TCMT IO Doc -> StateT Bool (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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
  String -> Int -> TCMT IO Doc -> StateT Bool (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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
  [(PragmaOptions -> Bool, String)]
-> ((PragmaOptions -> Bool, String) -> StateT Bool (TCMT IO) ())
-> StateT Bool (TCMT IO) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(PragmaOptions -> Bool, String)]
coinfectiveOptions (((PragmaOptions -> Bool, String) -> StateT Bool (TCMT IO) ())
 -> StateT Bool (TCMT IO) ())
-> ((PragmaOptions -> Bool, String) -> StateT Bool (TCMT IO) ())
-> StateT Bool (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ \ (PragmaOptions -> Bool
opt, String
optName) -> do
    Bool -> StateT Bool (TCMT IO) () -> StateT Bool (TCMT IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (PragmaOptions -> Bool
opt PragmaOptions
current Bool -> Bool -> Bool
`implies` PragmaOptions -> Bool
opt 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 (String -> ModuleName -> Warning
CoInfectiveImport String
optName ModuleName
importedModule)
  [(PragmaOptions -> Bool, String)]
-> ((PragmaOptions -> Bool, String) -> StateT Bool (TCMT IO) ())
-> StateT Bool (TCMT IO) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(PragmaOptions -> Bool, String)]
infectiveOptions (((PragmaOptions -> Bool, String) -> StateT Bool (TCMT IO) ())
 -> StateT Bool (TCMT IO) ())
-> ((PragmaOptions -> Bool, String) -> StateT Bool (TCMT IO) ())
-> StateT Bool (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ \ (PragmaOptions -> Bool
opt, String
optName) -> do
    Bool -> StateT Bool (TCMT IO) () -> StateT Bool (TCMT IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (PragmaOptions -> Bool
opt PragmaOptions
imported Bool -> Bool -> Bool
`implies` PragmaOptions -> Bool
opt PragmaOptions
current) (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 (String -> ModuleName -> Warning
InfectiveImport String
optName ModuleName
importedModule)
  where
    implies :: Bool -> Bool -> Bool
    Bool
p implies :: Bool -> Bool -> Bool
`implies` Bool
q = Bool
p Bool -> Bool -> Bool
forall a. Ord a => a -> a -> Bool
<= Bool
q

    showOptions :: PragmaOptions -> m Doc
showOptions PragmaOptions
opts = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
P.prettyList (((PragmaOptions -> Bool, String) -> m Doc)
-> [(PragmaOptions -> Bool, String)] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (PragmaOptions -> Bool
o, String
n) -> (String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
P.text String
n 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 (PragmaOptions -> Bool
o PragmaOptions
opts))
                                 ([(PragmaOptions -> Bool, String)]
coinfectiveOptions [(PragmaOptions -> Bool, String)]
-> [(PragmaOptions -> Bool, String)]
-> [(PragmaOptions -> Bool, String)]
forall a. [a] -> [a] -> [a]
++ [(PragmaOptions -> Bool, String)]
infectiveOptions))


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

getOptionsCompatibilityWarnings :: MainInterface -> Bool -> PragmaOptions -> Interface -> TCM (Maybe [TCWarning])
getOptionsCompatibilityWarnings :: MainInterface
-> Bool
-> PragmaOptions
-> Interface
-> TCMT IO (Maybe [TCWarning])
getOptionsCompatibilityWarnings MainInterface
isMain Bool
isPrim PragmaOptions
currentOptions Interface
i = MaybeT (TCMT IO) [TCWarning] -> TCMT IO (Maybe [TCWarning])
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (TCMT IO) [TCWarning] -> TCMT IO (Maybe [TCWarning]))
-> MaybeT (TCMT IO) [TCWarning] -> TCMT IO (Maybe [TCWarning])
forall a b. (a -> b) -> a -> b
$ ExceptT String (TCMT IO) [TCWarning]
-> MaybeT (TCMT IO) [TCWarning]
forall (m :: * -> *) e a. Functor m => ExceptT e m a -> MaybeT m a
exceptToMaybeT (ExceptT String (TCMT IO) [TCWarning]
 -> MaybeT (TCMT IO) [TCWarning])
-> ExceptT String (TCMT IO) [TCWarning]
-> MaybeT (TCMT IO) [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 String (TCMT IO) () -> ExceptT String (TCMT IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
isPrim (ExceptT String (TCMT IO) () -> ExceptT String (TCMT IO) ())
-> ExceptT String (TCMT IO) () -> ExceptT String (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
    String -> ExceptT String (TCMT IO) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"Options consistency checking disabled for always-available primitive module"
  ExceptT String (TCMT IO) Bool
-> ExceptT String (TCMT IO) () -> ExceptT String (TCMT IO) ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (TCM Bool -> ExceptT String (TCMT IO) Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Bool -> ExceptT String (TCMT IO) Bool)
-> TCM Bool -> ExceptT String (TCMT IO) Bool
forall a b. (a -> b) -> a -> b
$ PragmaOptions -> PragmaOptions -> ModuleName -> TCM Bool
checkOptionsCompatible PragmaOptions
currentOptions (Interface -> PragmaOptions
iOptionsUsed Interface
i) (Interface -> ModuleName
iModuleName Interface
i)) (ExceptT String (TCMT IO) () -> ExceptT String (TCMT IO) ())
-> ExceptT String (TCMT IO) () -> ExceptT String (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
    String -> ExceptT String (TCMT IO) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"No warnings to collect because options were compatible"
  TCMT IO [TCWarning] -> ExceptT String (TCMT IO) [TCWarning]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO [TCWarning] -> ExceptT String (TCMT IO) [TCWarning])
-> TCMT IO [TCWarning] -> ExceptT String (TCMT IO) [TCWarning]
forall a b. (a -> b) -> a -> b
$ MainInterface -> WhichWarnings -> TCMT IO [TCWarning]
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m) =>
MainInterface -> WhichWarnings -> m [TCWarning]
getAllWarnings' MainInterface
isMain WhichWarnings
ErrorWarnings

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

getStoredInterface
  :: C.TopLevelModuleName
     -- ^ Module name of file we process.
  -> SourceFile
     -- ^ File we process.
  -> Maybe Source
  -> ExceptT String TCM ModuleInfo
getStoredInterface :: TopLevelModuleName
-> SourceFile
-> Maybe Source
-> ExceptT String (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 String (TCMT IO) (InterfaceFile, (Hash, Hash))
getIFileHashesET = do
        -- Check that the interface file exists and return its hash.
        InterfaceFile
ifile <- String
-> MaybeT (TCMT IO) InterfaceFile
-> ExceptT String (TCMT IO) InterfaceFile
forall (m :: * -> *) e a.
Functor m =>
e -> MaybeT m a -> ExceptT e m a
maybeToExceptT String
"the interface file could not be found" (MaybeT (TCMT IO) InterfaceFile
 -> ExceptT String (TCMT IO) InterfaceFile)
-> MaybeT (TCMT IO) InterfaceFile
-> ExceptT String (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.
        (Hash, Hash)
hashes <- String
-> MaybeT (TCMT IO) (Hash, Hash)
-> ExceptT String (TCMT IO) (Hash, Hash)
forall (m :: * -> *) e a.
Functor m =>
e -> MaybeT m a -> ExceptT e m a
maybeToExceptT String
"the interface file hash could not be read" (MaybeT (TCMT IO) (Hash, Hash)
 -> ExceptT String (TCMT IO) (Hash, Hash))
-> MaybeT (TCMT IO) (Hash, Hash)
-> ExceptT String (TCMT IO) (Hash, Hash)
forall a b. (a -> b) -> a -> b
$ TCMT IO (Maybe (Hash, Hash)) -> MaybeT (TCMT IO) (Hash, Hash)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe (Hash, Hash)) -> MaybeT (TCMT IO) (Hash, Hash))
-> TCMT IO (Maybe (Hash, Hash)) -> MaybeT (TCMT IO) (Hash, Hash)
forall a b. (a -> b) -> a -> b
$ IO (Maybe (Hash, Hash)) -> TCMT IO (Maybe (Hash, Hash))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe (Hash, Hash)) -> TCMT IO (Maybe (Hash, Hash)))
-> IO (Maybe (Hash, Hash)) -> TCMT IO (Maybe (Hash, Hash))
forall a b. (a -> b) -> a -> b
$
          InterfaceFile -> IO (Maybe (Hash, Hash))
getInterfaceFileHashes InterfaceFile
ifile

        (InterfaceFile, (Hash, Hash))
-> ExceptT String (TCMT IO) (InterfaceFile, (Hash, Hash))
forall (m :: * -> *) a. Monad m => a -> m a
return (InterfaceFile
ifile, (Hash, Hash)
hashes)

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

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

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

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

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

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

      -- Make sure the hashes match.
      let cachedIfaceHash :: Hash
cachedIfaceHash = Interface -> Hash
iFullHash Interface
i
      let fileIfaceHash :: Hash
fileIfaceHash = (Hash, Hash) -> Hash
forall a b. (a, b) -> b
snd (Hash, Hash)
hashes
      Bool -> ExceptT String (TCMT IO) () -> ExceptT String (TCMT IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Hash
cachedIfaceHash Hash -> Hash -> Bool
forall a. Eq a => a -> a -> Bool
== Hash
fileIfaceHash) (ExceptT String (TCMT IO) () -> ExceptT String (TCMT IO) ())
-> ExceptT String (TCMT IO) () -> ExceptT String (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ do
        TCM () -> ExceptT String (TCMT IO) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> ExceptT String (TCMT IO) ())
-> TCM () -> ExceptT String (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> TCM ()
dropDecodedModule TopLevelModuleName
x
        String -> Int -> String -> ExceptT String (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface" Int
50 (String -> ExceptT String (TCMT IO) ())
-> String -> ExceptT String (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ String
"  cached hash = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Hash -> String
forall a. Show a => a -> String
show Hash
cachedIfaceHash
        String -> Int -> String -> ExceptT String (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface" Int
50 (String -> ExceptT String (TCMT IO) ())
-> String -> ExceptT String (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ String
"  stored hash = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Hash -> String
forall a. Show a => a -> String
show Hash
fileIfaceHash
        String -> Int -> String -> ExceptT String (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface" Int
5 (String -> ExceptT String (TCMT IO) ())
-> String -> ExceptT String (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ String
"  file is newer, re-reading " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ifp
        String -> ExceptT String (TCMT IO) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> ExceptT String (TCMT IO) ())
-> String -> ExceptT String (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ OptionsPragma -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ String
"the cached interface hash (", Hash -> String
forall a. Show a => a -> String
show Hash
cachedIfaceHash, String
")"
          , String
" does not match interface file (", Hash -> String
forall a. Show a => a -> String
show Hash
fileIfaceHash, String
")"
          ]

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

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

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

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

      (InterfaceFile
ifile, (Hash, Hash)
hashes) <- ExceptT String (TCMT IO) (InterfaceFile, (Hash, Hash))
getIFileHashesET

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

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

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

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

        -- Ensure that the given module name matches the one in the file.
        let topLevelName :: TopLevelModuleName
topLevelName = ModuleName -> TopLevelModuleName
toTopLevelModuleName (ModuleName -> TopLevelModuleName)
-> ModuleName -> TopLevelModuleName
forall a b. (a -> b) -> a -> b
$ Interface -> ModuleName
iModuleName Interface
i
        Bool -> ExceptT String (TCMT IO) () -> ExceptT String (TCMT IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TopLevelModuleName
topLevelName TopLevelModuleName -> TopLevelModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== TopLevelModuleName
x) (ExceptT String (TCMT IO) () -> ExceptT String (TCMT IO) ())
-> ExceptT String (TCMT IO) () -> ExceptT String (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
          -- Andreas, 2014-03-27 This check is now done in the scope checker.
          -- checkModuleName topLevelName file
          TCM () -> ExceptT String (TCMT IO) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> ExceptT String (TCMT IO) ())
-> TCM () -> ExceptT String (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ AbsolutePath
-> TopLevelModuleName -> TopLevelModuleName -> TypeError
OverlappingProjects (SourceFile -> AbsolutePath
srcFilePath SourceFile
file) TopLevelModuleName
topLevelName TopLevelModuleName
x

        Bool
isPrimitiveModule <- TCM Bool -> ExceptT String (TCMT IO) Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Bool -> ExceptT String (TCMT IO) Bool)
-> TCM Bool -> ExceptT String (TCMT IO) Bool
forall a b. (a -> b) -> a -> b
$ String -> TCM Bool
forall (m :: * -> *). MonadIO m => String -> m Bool
Lens.isPrimitiveModule (AbsolutePath -> String
filePath (AbsolutePath -> String) -> AbsolutePath -> String
forall a b. (a -> b) -> a -> b
$ SourceFile -> AbsolutePath
srcFilePath SourceFile
file)

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

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


loadDecodedModule
  :: SourceFile
     -- ^ File we process.
  -> ModuleInfo
  -> ExceptT String TCM ModuleInfo
loadDecodedModule :: SourceFile -> ModuleInfo -> ExceptT String (TCMT IO) ModuleInfo
loadDecodedModule SourceFile
file ModuleInfo
mi = do
  let fp :: String
fp = AbsolutePath -> String
filePath (AbsolutePath -> String) -> AbsolutePath -> String
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
  String -> Int -> String -> ExceptT String (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface" Int
5 (String -> ExceptT String (TCMT IO) ())
-> String -> ExceptT String (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ String
"  imports: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(ModuleName, Hash)] -> String
forall a. Pretty a => a -> String
prettyShow (Interface -> [(ModuleName, Hash)]
iImportedModules Interface
i)

  -- We set the pragma options of the skipped file here, so that
  -- we can check that they are compatible with those of the
  -- imported modules. Also, if the top-level file is skipped we
  -- want the pragmas to apply to interactive commands in the UI.
  -- Jesper, 2021-04-18: Check for changed options in library files!
  -- (see #5250)
  [OptionsPragma]
libOptions <- TCMT IO [OptionsPragma] -> ExceptT String (TCMT IO) [OptionsPragma]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO [OptionsPragma]
 -> ExceptT String (TCMT IO) [OptionsPragma])
-> TCMT IO [OptionsPragma]
-> ExceptT String (TCMT IO) [OptionsPragma]
forall a b. (a -> b) -> a -> b
$ String -> TCMT IO [OptionsPragma]
getLibraryOptions (String -> TCMT IO [OptionsPragma])
-> String -> TCMT IO [OptionsPragma]
forall a b. (a -> b) -> a -> b
$ String -> String
takeDirectory String
fp
  TCM () -> ExceptT String (TCMT IO) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> ExceptT String (TCMT IO) ())
-> TCM () -> ExceptT String (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ (OptionsPragma -> TCM ()) -> [OptionsPragma] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ OptionsPragma -> TCM ()
setOptionsFromPragma ([OptionsPragma]
libOptions [OptionsPragma] -> [OptionsPragma] -> [OptionsPragma]
forall a. [a] -> [a] -> [a]
++ Interface -> [OptionsPragma]
iFilePragmaOptions Interface
i)

  -- Check that options that matter haven't changed compared to
  -- current options (issue #2487)
  ExceptT String (TCMT IO) Bool
-> ExceptT String (TCMT IO) () -> ExceptT String (TCMT IO) ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (TCM Bool -> ExceptT String (TCMT IO) Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Bool -> ExceptT String (TCMT IO) Bool)
-> TCM Bool -> ExceptT String (TCMT IO) Bool
forall a b. (a -> b) -> a -> b
$ String -> TCM Bool
forall (m :: * -> *). MonadIO m => String -> m Bool
Lens.isBuiltinModule String
fp) (ExceptT String (TCMT IO) () -> ExceptT String (TCMT IO) ())
-> ExceptT String (TCMT IO) () -> ExceptT String (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ do
    PragmaOptions
currentOptions <- Lens' PragmaOptions TCState
-> ExceptT String (TCMT IO) PragmaOptions
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' PragmaOptions TCState
stPragmaOptions
    let disagreements :: OptionsPragma
disagreements =
          [ String
optName | (PragmaOptions -> RestartCodomain
opt, String
optName) <- [(PragmaOptions -> RestartCodomain, String)]
restartOptions,
                      PragmaOptions -> RestartCodomain
opt PragmaOptions
currentOptions RestartCodomain -> RestartCodomain -> Bool
forall a. Eq a => a -> a -> Bool
/= PragmaOptions -> RestartCodomain
opt (Interface -> PragmaOptions
iOptionsUsed Interface
i) ]
    Bool -> ExceptT String (TCMT IO) () -> ExceptT String (TCMT IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (OptionsPragma -> Bool
forall a. Null a => a -> Bool
null OptionsPragma
disagreements) (ExceptT String (TCMT IO) () -> ExceptT String (TCMT IO) ())
-> ExceptT String (TCMT IO) () -> ExceptT String (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ do
      String -> Int -> String -> ExceptT String (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface.options" Int
4 (String -> ExceptT String (TCMT IO) ())
-> String -> ExceptT String (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ OptionsPragma -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ String
"  Changes in the following options in "
        , String -> String
forall a. Pretty a => a -> String
prettyShow String
fp
        , String
", re-typechecking: "
        , OptionsPragma -> String
forall a. Pretty a => a -> String
prettyShow OptionsPragma
disagreements
        ]
      String -> ExceptT String (TCMT IO) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"options changed"

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

  OptionsPragma
-> (OptionsPragma -> ExceptT String (TCMT IO) ())
-> ExceptT String (TCMT IO) ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull OptionsPragma
badHashMessages (String -> ExceptT String (TCMT IO) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> ExceptT String (TCMT IO) ())
-> (OptionsPragma -> String)
-> OptionsPragma
-> ExceptT String (TCMT IO) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OptionsPragma -> String
unlines)

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

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

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

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

      [TopLevelModuleName]
ms          <- TCM [TopLevelModuleName]
getImportPath
      Range
range       <- (TCEnv -> Range) -> TCMT IO Range
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Range
envRange
      Maybe (Closure Call)
call        <- (TCEnv -> Maybe (Closure Call)) -> TCMT IO (Maybe (Closure Call))
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe (Closure Call)
envCall
      Map TopLevelModuleName AbsolutePath
mf          <- Lens' (Map TopLevelModuleName AbsolutePath) TCState
-> TCMT IO (Map TopLevelModuleName AbsolutePath)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map TopLevelModuleName AbsolutePath) TCState
stModuleToSource
      VisitedModules
vs          <- TCMT IO VisitedModules
forall (m :: * -> *). ReadTCState m => m VisitedModules
getVisitedModules
      VisitedModules
ds          <- TCMT IO VisitedModules
getDecodedModules
      CommandLineOptions
opts        <- PersistentTCState -> CommandLineOptions
stPersistentOptions (PersistentTCState -> CommandLineOptions)
-> (TCState -> PersistentTCState) -> TCState -> CommandLineOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState (TCState -> CommandLineOptions)
-> TCMT IO TCState -> TCMT IO CommandLineOptions
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
      Signature
isig        <- Lens' Signature TCState -> TCMT IO Signature
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' Signature TCState
stImports
      Map String (Builtin PrimFun)
ibuiltin    <- Lens' (Map String (Builtin PrimFun)) TCState
-> TCMT IO (Map String (Builtin PrimFun))
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map String (Builtin PrimFun)) TCState
stImportedBuiltins
      DisplayForms
display     <- Lens' DisplayForms TCState -> TCMT IO DisplayForms
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' DisplayForms TCState
stImportsDisplayForms
      Map QName Text
userwarn    <- Lens' (Map QName Text) TCState -> TCMT IO (Map QName Text)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map QName Text) TCState
stImportedUserWarnings
      Set QName
partialdefs <- Lens' (Set QName) TCState -> TCMT IO (Set QName)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Set QName) TCState
stImportedPartialDefs
      PatternSynDefns
ipatsyns <- TCMT IO PatternSynDefns
forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getPatternSynImports
      InteractionOutputCallback
ho       <- TCMT IO InteractionOutputCallback
forall (m :: * -> *). ReadTCState m => m InteractionOutputCallback
getInteractionOutputCallback
      -- Every interface is treated in isolation. Note: Some changes to
      -- the persistent state may not be preserved if an error other
      -- than a type error or an IO exception is encountered in an
      -- imported module.
      (ModuleInfo
mi, Map TopLevelModuleName AbsolutePath
newModToSource, VisitedModules
newDecodedModules) <- ((TCErr
 -> TCMT
      IO
      (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
-> ((ModuleInfo, Map TopLevelModuleName AbsolutePath,
     VisitedModules)
    -> TCMT
         IO
         (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
-> Either
     TCErr
     (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
-> TCMT
     IO
     (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either TCErr
-> TCMT
     IO
     (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
-> TCMT
     IO
     (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either
   TCErr
   (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
 -> TCMT
      IO
      (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
-> TCMT
     IO
     (Either
        TCErr
        (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
-> TCMT
     IO
     (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) (TCMT
   IO
   (Either
      TCErr
      (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
 -> TCMT
      IO
      (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
-> TCMT
     IO
     (Either
        TCErr
        (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
-> TCMT
     IO
     (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
forall a b. (a -> b) -> a -> b
$
           TCMT
  IO
  (Either
     TCErr
     (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
-> TCMT
     IO
     (Either
        TCErr
        (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
forall (m :: * -> *) a.
(MonadTCState m, ReadTCState m) =>
m a -> m a
withoutCache (TCMT
   IO
   (Either
      TCErr
      (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
 -> TCMT
      IO
      (Either
         TCErr
         (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)))
-> TCMT
     IO
     (Either
        TCErr
        (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
-> TCMT
     IO
     (Either
        TCErr
        (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
forall a b. (a -> b) -> a -> b
$
           -- The cache should not be used for an imported module, and it
           -- should be restored after the module has been type-checked
           TCMT
  IO
  (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
-> TCMT
     IO
     (Either
        TCErr
        (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
forall a. TCM a -> TCM (Either TCErr a)
freshTCM (TCMT
   IO
   (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
 -> TCMT
      IO
      (Either
         TCErr
         (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)))
-> TCMT
     IO
     (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
-> TCMT
     IO
     (Either
        TCErr
        (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
forall a b. (a -> b) -> a -> b
$
             [TopLevelModuleName]
-> TCMT
     IO
     (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
-> TCMT
     IO
     (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
forall a. [TopLevelModuleName] -> TCM a -> TCM a
withImportPath [TopLevelModuleName]
ms (TCMT
   IO
   (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
 -> TCMT
      IO
      (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
-> TCMT
     IO
     (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
-> TCMT
     IO
     (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
forall a b. (a -> b) -> a -> b
$
             (TCEnv -> TCEnv)
-> TCMT
     IO
     (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
-> TCMT
     IO
     (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\TCEnv
e -> TCEnv
e
                              -- Andreas, 2014-08-18:
                              -- Preserve the range of import statement
                              -- for reporting termination errors in
                              -- imported modules:
                            { envRange :: Range
envRange              = Range
range
                            , envCall :: Maybe (Closure Call)
envCall               = Maybe (Closure Call)
call
                            }) (TCMT
   IO
   (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
 -> TCMT
      IO
      (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
-> TCMT
     IO
     (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
-> TCMT
     IO
     (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
forall a b. (a -> b) -> a -> b
$ do
               VisitedModules -> TCM ()
setDecodedModules VisitedModules
ds
               CommandLineOptions -> TCM ()
setCommandLineOptions CommandLineOptions
opts
               InteractionOutputCallback -> TCM ()
setInteractionOutputCallback InteractionOutputCallback
ho
               Lens' (Map TopLevelModuleName AbsolutePath) TCState
stModuleToSource Lens' (Map TopLevelModuleName AbsolutePath) TCState
-> Map TopLevelModuleName AbsolutePath -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` Map TopLevelModuleName AbsolutePath
mf
               VisitedModules -> TCM ()
setVisitedModules VisitedModules
vs
               Signature
-> Map String (Builtin PrimFun)
-> PatternSynDefns
-> DisplayForms
-> Map QName Text
-> Set QName
-> [TCWarning]
-> TCM ()
addImportedThings Signature
isig Map String (Builtin PrimFun)
ibuiltin PatternSynDefns
ipatsyns DisplayForms
display Map QName Text
userwarn Set QName
partialdefs []

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

      Lens' (Map TopLevelModuleName AbsolutePath) TCState
stModuleToSource Lens' (Map TopLevelModuleName AbsolutePath) TCState
-> Map TopLevelModuleName AbsolutePath -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` Map TopLevelModuleName AbsolutePath
newModToSource
      VisitedModules -> TCM ()
setDecodedModules VisitedModules
newDecodedModules

      -- We skip the file which has just been type-checked to
      -- be able to forget some of the local state from
      -- checking the module.
      -- Note that this doesn't actually read the interface
      -- file, only the cached interface. (This comment is not
      -- correct, see
      -- test/Fail/customised/NestedProjectRoots.err.)
      Either String ModuleInfo
validated <- ExceptT String (TCMT IO) ModuleInfo
-> TCM (Either String ModuleInfo)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT String (TCMT IO) ModuleInfo
 -> TCM (Either String ModuleInfo))
-> ExceptT String (TCMT IO) ModuleInfo
-> TCM (Either String ModuleInfo)
forall a b. (a -> b) -> a -> b
$ SourceFile -> ModuleInfo -> ExceptT String (TCMT IO) ModuleInfo
loadDecodedModule SourceFile
file ModuleInfo
mi

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

      (String -> TCM ModuleInfo)
-> (ModuleInfo -> TCM ModuleInfo)
-> Either String ModuleInfo
-> TCM ModuleInfo
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either String -> TCM ModuleInfo
recheckOnError ModuleInfo -> TCM ModuleInfo
forall (f :: * -> *) a. Applicative f => a -> f a
pure Either String ModuleInfo
validated


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

chaseMsg
  :: String               -- ^ The prefix, like @Checking@, @Finished@, @Loading @.
  -> C.TopLevelModuleName -- ^ The module name.
  -> Maybe String         -- ^ Optionally: the file name.
  -> TCM ()
chaseMsg :: String -> TopLevelModuleName -> Maybe String -> TCM ()
chaseMsg String
kind TopLevelModuleName
x Maybe String
file = do
  String
indentation <- (Int -> Char -> String
forall a. Int -> a -> [a]
`replicate` Char
' ') (Int -> String) -> TCMT IO Int -> TCMT IO String
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 (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)
  let maybeFile :: String
maybeFile = Maybe String -> String -> (String -> String) -> String
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe String
file String
"." ((String -> String) -> String) -> (String -> String) -> String
forall a b. (a -> b) -> a -> b
$ \ String
f -> String
" (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")."
      vLvl :: Int
vLvl | String
kind String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"Checking" = Int
1
           | Bool
otherwise          = Int
2
  String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.chase" Int
vLvl (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ OptionsPragma -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ String
indentation, String
kind, String
" ", TopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow TopLevelModuleName
x, String
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
  String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface" Int
5 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$
    String
"Generating syntax info for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ AbsolutePath -> String
filePath (SourceFile -> AbsolutePath
srcFilePath SourceFile
file) String -> String -> String
forall a. [a] -> [a] -> [a]
++
    String
" (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 :: String
ifp = AbsolutePath -> String
filePath (AbsolutePath -> String) -> AbsolutePath -> String
forall a b. (a -> b) -> a -> b
$ InterfaceFile -> AbsolutePath
intFilePath InterfaceFile
file
    -- Decode the interface file
    (ByteString
s, IO ()
close) <- IO (ByteString, IO ()) -> TCMT IO (ByteString, IO ())
forall (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
$ String -> IO (ByteString, IO ())
readBinaryFile' String
ifp
    do  Maybe Interface
mi <- IO (Maybe Interface) -> TCMT IO (Maybe Interface)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe Interface) -> TCMT IO (Maybe Interface))
-> (Maybe Interface -> IO (Maybe Interface))
-> Maybe Interface
-> TCMT IO (Maybe Interface)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Interface -> IO (Maybe Interface)
forall a. a -> IO a
E.evaluate (Maybe Interface -> TCMT IO (Maybe Interface))
-> TCMT IO (Maybe Interface) -> TCMT IO (Maybe Interface)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ByteString -> TCMT IO (Maybe Interface)
decodeInterface ByteString
s

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

        Maybe Interface -> TCMT IO (Maybe Interface)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Interface -> TCMT IO (Maybe Interface))
-> Maybe Interface -> TCMT IO (Maybe Interface)
forall a b. (a -> b) -> a -> b
$ Interface -> Interface
constructIScope (Interface -> Interface) -> Maybe Interface -> Maybe Interface
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Interface
mi
      -- Catch exceptions and close
      TCMT IO (Maybe Interface)
-> (TCErr -> TCMT IO (Maybe Interface))
-> TCMT IO (Maybe Interface)
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
e -> IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO ()
close TCM () -> TCMT IO (Maybe Interface) -> TCMT IO (Maybe Interface)
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 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 TCState
_ Range
_ IOException
e -> do
        String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"" Int
0 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ String
"IO exception: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ IOException -> String
forall a. Show a => a -> String
show IOException
e
        Maybe a -> TCMT IO (Maybe 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 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 :: String
fp = AbsolutePath -> String
filePath AbsolutePath
file in do
    String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface.write" Int
5  (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$
      String
"Writing interface file " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fp String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."
    -- Andreas, 2015-07-13
    -- After QName memoization (AIM XXI), scope serialization might be cheap enough.
    -- -- Andreas, Makoto, 2014-10-18 AIM XX:
    -- -- iInsideScope is bloating the interface files, so we do not serialize it?
    -- i <- return $
    --   i { iInsideScope  = emptyScopeInfo
    --     }
    -- [Old: Andreas, 2016-02-02 this causes issue #1804, so don't do it:]
    -- Andreas, 2020-05-13, #1804, #4647: removed private declarations
    -- only when we actually write the interface.
    let filteredIface :: Interface
filteredIface = Interface
i { iInsideScope :: ScopeInfo
iInsideScope  = ScopeInfo -> ScopeInfo
withoutPrivates (ScopeInfo -> ScopeInfo) -> ScopeInfo -> ScopeInfo
forall a b. (a -> b) -> a -> b
$ Interface -> ScopeInfo
iInsideScope Interface
i }
    String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface.write" Int
50 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$
      String
"Writing interface file with hash " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Hash -> String
forall a. Show a => a -> String
show (Interface -> Hash
iFullHash Interface
filteredIface) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."
    ByteString
encodedIface <- String -> Interface -> TCM ByteString
encodeFile String
fp Interface
filteredIface
    String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface.write" Int
5 String
"Wrote interface file."
#if __GLASGOW_HASKELL__ >= 804
    Interface -> Maybe Interface -> Interface
forall a. a -> Maybe a -> a
fromMaybe Interface
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Interface -> Interface)
-> TCMT IO (Maybe Interface) -> TCMT IO Interface
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Account (BenchPhase (TCMT IO))
-> TCMT IO (Maybe Interface) -> TCMT IO (Maybe Interface)
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Deserialization] (ByteString -> TCMT IO (Maybe Interface)
forall a. EmbPrj a => ByteString -> TCM (Maybe a)
decode ByteString
encodedIface))
#else
    return filteredIface
#endif
  TCMT IO Interface
-> (TCErr -> TCMT IO Interface) -> TCMT IO Interface
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
e -> do
    String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"" Int
1 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$
      String
"Failed to write interface " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fp String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."
    IO () -> TCM ()
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 (String -> IO Bool
doesFileExist String
fp) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
removeFile String
fp
    TCErr -> TCMT IO Interface
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
  :: C.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 :: String
fp = AbsolutePath -> String
filePath (AbsolutePath -> String) -> AbsolutePath -> String
forall a b. (a -> b) -> a -> b
$ SourceFile -> AbsolutePath
srcFilePath SourceFile
file
  let checkMsg :: String
checkMsg = case MainInterface
isMain of
                   MainInterface Mode
ScopeCheck -> String
"Reading "
                   MainInterface
_                        -> String
"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_
       (String -> TopLevelModuleName -> Maybe String -> TCM ()
chaseMsg String
checkMsg TopLevelModuleName
x (Maybe String -> TCM ()) -> Maybe String -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
fp)
       (TCM () -> () -> TCM ()
forall a b. a -> b -> a
const (TCM () -> () -> TCM ()) -> TCM () -> () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do [TCWarning]
ws <- WhichWarnings -> TCMT IO [TCWarning]
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m) =>
WhichWarnings -> m [TCWarning]
getAllWarnings WhichWarnings
AllWarnings
                   let classified :: WarningsAndNonFatalErrors
classified = [TCWarning] -> WarningsAndNonFatalErrors
classifyWarnings [TCWarning]
ws
                   let wa' :: [TCWarning]
wa' = (TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
forall a. (a -> Bool) -> [a] -> [a]
filter ((AbsolutePath -> Maybe AbsolutePath
forall a. a -> Maybe a
Strict.Just (SourceFile -> AbsolutePath
srcFilePath SourceFile
file) Maybe AbsolutePath -> Maybe AbsolutePath -> Bool
forall a. Eq a => a -> a -> Bool
==) (Maybe AbsolutePath -> Bool)
-> (TCWarning -> Maybe AbsolutePath) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Maybe AbsolutePath
tcWarningOrigin) (WarningsAndNonFatalErrors -> [TCWarning]
tcWarnings WarningsAndNonFatalErrors
classified)
                   Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([TCWarning] -> Bool
forall a. Null a => a -> Bool
null [TCWarning]
wa') (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
                     String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"warning" Int
1 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
P.vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCWarning -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
P.prettyTCM (TCWarning -> TCMT IO Doc) -> [TCWarning] -> [TCMT IO Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TCWarning]
wa'
                   Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([TCWarning] -> Bool
forall a. Null a => a -> Bool
null (WarningsAndNonFatalErrors -> [TCWarning]
nonFatalErrors WarningsAndNonFatalErrors
classified)) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> TopLevelModuleName -> Maybe String -> TCM ()
chaseMsg String
"Finished" TopLevelModuleName
x Maybe String
forall a. Maybe a
Nothing)

  TCM ModuleInfo -> TCM ModuleInfo
withMsgs (TCM ModuleInfo -> TCM ModuleInfo)
-> TCM ModuleInfo -> TCM ModuleInfo
forall a b. (a -> b) -> a -> b
$
    Account (BenchPhase (TCMT IO)) -> TCM ModuleInfo -> TCM ModuleInfo
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [TopLevelModuleName -> Phase
Bench.TopModule TopLevelModuleName
mname] (TCM ModuleInfo -> TCM ModuleInfo)
-> TCM ModuleInfo -> TCM ModuleInfo
forall a b. (a -> b) -> a -> b
$
    (TCEnv -> TCEnv) -> TCM ModuleInfo -> TCM ModuleInfo
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\TCEnv
e -> TCEnv
e { envCurrentPath :: Maybe AbsolutePath
envCurrentPath = AbsolutePath -> Maybe AbsolutePath
forall a. a -> Maybe a
Just (SourceFile -> AbsolutePath
srcFilePath SourceFile
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

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

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

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

    HighlightingInfo
fileTokenInfo <- Account (BenchPhase (TCMT IO))
-> TCMT IO HighlightingInfo -> TCMT IO HighlightingInfo
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Highlighting] (TCMT IO HighlightingInfo -> TCMT IO HighlightingInfo)
-> TCMT IO HighlightingInfo -> TCMT IO HighlightingInfo
forall a b. (a -> b) -> a -> b
$
      AbsolutePath -> String -> TCMT IO HighlightingInfo
generateTokenInfoFromSource AbsolutePath
srcPath (Text -> String
TL.unpack (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$ Source -> Text
srcText Source
src)
    Lens' HighlightingInfo TCState
stTokens Lens' HighlightingInfo TCState
-> (HighlightingInfo -> HighlightingInfo) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` (HighlightingInfo
fileTokenInfo HighlightingInfo -> HighlightingInfo -> HighlightingInfo
forall a. Semigroup a => a -> a -> a
<>)

    Source -> TCM ()
setOptionsFromSourcePragmas Source
src

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

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

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

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


    -- Type checking.

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

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

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

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

    TCM ()
unfreezeMetas

    -- Profiling: Count number of metas.
    String -> Int -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => String -> Int -> m () -> m ()
verboseS String
"profile.metas" Int
10 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      MetaId Int
n <- TCMT IO MetaId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
      String -> Integer -> TCM ()
forall (m :: * -> *).
MonadStatistics m =>
String -> Integer -> m ()
tickN String
"metas" (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n)

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

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

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

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

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

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

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

    [MetaId]
openMetas           <- TCMT IO [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas
    Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([MetaId] -> Bool
forall a. Null a => a -> Bool
null [MetaId]
openMetas) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.metas" Int
10 String
"We have unsolved metas."
      String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.metas" Int
10 (String -> TCM ()) -> TCMT IO String -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Goals -> TCMT IO String
showGoals (Goals -> TCMT IO String) -> TCMT IO Goals -> TCMT IO String
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Goals
getGoals

    HighlightingLevel -> TCM () -> TCM ()
forall (tcm :: * -> *).
MonadTCEnv tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive TCM ()
printUnsolvedInfo

    -- Andreas, 2016-08-03, issue #964
    -- When open metas are allowed,
    -- permanently freeze them now by turning them into postulates.
    -- This will enable serialization.
    -- savedMetaStore <- useTC stMetaStore
    Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (MainInterface -> Bool
includeStateChanges MainInterface
isMain) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
      -- Andreas, 2018-11-15, re issue #3393:
      -- We do not get here when checking the main module
      -- (then includeStateChanges is True).
      TCM Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (PragmaOptions -> Bool
optAllowUnsolved (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface.create" Int
7 String
"Turning unsolved metas (if any) into postulates."
        ModuleName -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
withCurrentModule (ScopeInfo
scope ScopeInfo -> Lens' ModuleName ScopeInfo -> ModuleName
forall o i. o -> Lens' i o -> i
^. Lens' ModuleName ScopeInfo
scopeCurrent) TCM ()
openMetasToPostulates
        -- Clear constraints as they might refer to what
        -- they think are open metas.
        Lens' Constraints TCState
stAwakeConstraints    Lens' Constraints TCState -> Constraints -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` []
        Lens' Constraints TCState
stSleepingConstraints Lens' Constraints TCState -> Constraints -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` []

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

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

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

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

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

    -- Profiling: Print statistics.
    Int -> Maybe TopLevelModuleName -> Statistics -> TCM ()
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m, HasOptions m) =>
Int -> Maybe TopLevelModuleName -> Statistics -> m ()
printStatistics Int
30 (TopLevelModuleName -> Maybe TopLevelModuleName
forall a. a -> Maybe a
Just TopLevelModuleName
mname) (Statistics -> TCM ()) -> TCMT IO Statistics -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Statistics
forall (m :: * -> *). ReadTCState m => m Statistics
getStatistics

    -- Get the statistics of the current module
    -- and add it to the accumulated statistics.
    Statistics
localStatistics <- TCMT IO Statistics
forall (m :: * -> *). ReadTCState m => m Statistics
getStatistics
    Lens' Statistics TCState
lensAccumStatistics Lens' Statistics TCState -> (Statistics -> Statistics) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` (Integer -> Integer -> Integer)
-> Statistics -> Statistics -> Statistics
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) Statistics
localStatistics
    String -> Int -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => String -> Int -> m () -> m ()
verboseS String
"profile" Int
1 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface" Int
5 String
"Accumulated statistics."

    Bool
isPrimitiveModule <- String -> TCM Bool
forall (m :: * -> *). MonadIO m => String -> m Bool
Lens.isPrimitiveModule (AbsolutePath -> String
filePath AbsolutePath
srcPath)

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

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

getAllWarnings' :: (MonadFail m, ReadTCState m, MonadWarning m) => MainInterface -> WhichWarnings -> m [TCWarning]
getAllWarnings' :: MainInterface -> WhichWarnings -> m [TCWarning]
getAllWarnings' (MainInterface Mode
_) = Set WarningName -> WhichWarnings -> m [TCWarning]
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m) =>
Set WarningName -> WhichWarnings -> m [TCWarning]
getAllWarningsPreserving Set WarningName
unsolvedWarnings
getAllWarnings' MainInterface
NotMainInterface  = Set WarningName -> WhichWarnings -> m [TCWarning]
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m) =>
Set WarningName -> WhichWarnings -> m [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 = Account -> Interface -> Interface
forall a. Account -> a -> a
billToPure [ Phase
Deserialization ] (Interface -> Interface) -> Interface -> Interface
forall a b. (a -> b) -> a -> b
$
  Interface
i{ iScope :: Map ModuleName Scope
iScope = ScopeInfo -> Map ModuleName Scope
publicModules (ScopeInfo -> Map ModuleName Scope)
-> ScopeInfo -> Map ModuleName Scope
forall a b. (a -> b) -> a -> b
$ Interface -> ScopeInfo
iInsideScope Interface
i }

-- | Builds an interface for the current module, which should already
-- have been successfully type checked.

buildInterface
  :: Source
     -- ^ 'Source' for the current module.
  -> TopLevelInfo
     -- ^ 'TopLevelInfo' scope information for the current module.
  -> TCM Interface
buildInterface :: Source -> TopLevelInfo -> TCMT IO Interface
buildInterface Source
src TopLevelInfo
topLevel = do
    String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface" Int
5 String
"Building interface..."
    let mname :: ModuleName
mname = TopLevelInfo -> ModuleName
topLevelModuleName TopLevelInfo
topLevel
        source :: Text
source   = Source -> Text
srcText Source
src
        fileType :: FileType
fileType = Source -> FileType
srcFileType Source
src
        defPragmas :: [OptionsPragma]
defPragmas = Source -> [OptionsPragma]
srcDefaultPragmas Source
src
        filePragmas :: [OptionsPragma]
filePragmas  = Source -> [OptionsPragma]
srcFilePragmas Source
src
    -- Andreas, 2014-05-03: killRange did not result in significant reduction
    -- of .agdai file size, and lost a few seconds performance on library-test.
    -- Andreas, Makoto, 2014-10-18 AIM XX: repeating the experiment
    -- with discarding also the nameBindingSite in QName:
    -- Saves 10% on serialization time (and file size)!
    --
    -- NOTE: We no longer discard all nameBindingSites (but the commit
    -- that introduced this change seems to have made Agda a bit
    -- faster and interface file sizes a bit smaller, at least for the
    -- standard library).
    Map String (Builtin PrimFun)
builtin     <- Lens' (Map String (Builtin PrimFun)) TCState
-> TCMT IO (Map String (Builtin PrimFun))
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map String (Builtin PrimFun)) TCState
stLocalBuiltins
    Set ModuleName
ms          <- TCM (Set ModuleName)
getImports
    [(ModuleName, Hash)]
mhs         <- (ModuleName -> TCMT IO (ModuleName, Hash))
-> [ModuleName] -> TCMT IO [(ModuleName, Hash)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ ModuleName
m -> (ModuleName
m,) (Hash -> (ModuleName, Hash))
-> TCMT IO Hash -> TCMT IO (ModuleName, Hash)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> TCMT IO Hash
moduleHash ModuleName
m) ([ModuleName] -> TCMT IO [(ModuleName, Hash)])
-> [ModuleName] -> TCMT IO [(ModuleName, Hash)]
forall a b. (a -> b) -> a -> b
$ Set ModuleName -> [ModuleName]
forall a. Set a -> [a]
Set.toList Set ModuleName
ms
    Map String [ForeignCode]
foreignCode <- Lens' (Map String [ForeignCode]) TCState
-> TCMT IO (Map String [ForeignCode])
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map String [ForeignCode]) TCState
stForeignCode
    -- Ulf, 2016-04-12:
    -- Non-closed display forms are not applicable outside the module anyway,
    -- and should be dead-code eliminated (#1928).
    DisplayForms
origDisplayForms <- ([LocalDisplayForm] -> Bool) -> DisplayForms -> DisplayForms
forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
HMap.filter (Bool -> Bool
not (Bool -> Bool)
-> ([LocalDisplayForm] -> Bool) -> [LocalDisplayForm] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [LocalDisplayForm] -> Bool
forall a. Null a => a -> Bool
null) (DisplayForms -> DisplayForms)
-> (DisplayForms -> DisplayForms) -> DisplayForms -> DisplayForms
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([LocalDisplayForm] -> [LocalDisplayForm])
-> DisplayForms -> DisplayForms
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HMap.map ((LocalDisplayForm -> Bool)
-> [LocalDisplayForm] -> [LocalDisplayForm]
forall a. (a -> Bool) -> [a] -> [a]
filter LocalDisplayForm -> Bool
forall a. Open a -> Bool
isClosed) (DisplayForms -> DisplayForms)
-> TCMT IO DisplayForms -> TCMT IO DisplayForms
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' DisplayForms TCState -> TCMT IO DisplayForms
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' DisplayForms TCState
stImportsDisplayForms
    -- TODO: Kill some ranges?
    (DisplayForms
display, Signature
sig) <- DisplayForms -> Signature -> TCM (DisplayForms, Signature)
eliminateDeadCode DisplayForms
origDisplayForms (Signature -> TCM (DisplayForms, Signature))
-> TCMT IO Signature -> TCM (DisplayForms, Signature)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Signature
forall (m :: * -> *). ReadTCState m => m Signature
getSignature
    Map QName Text
userwarns      <- Lens' (Map QName Text) TCState -> TCMT IO (Map QName Text)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map QName Text) TCState
stLocalUserWarnings
    Maybe Text
importwarn     <- Lens' (Maybe Text) TCState -> TCMT IO (Maybe Text)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Maybe Text) TCState
stWarningOnImport
    HighlightingInfo
syntaxInfo     <- Lens' HighlightingInfo TCState -> TCMT IO HighlightingInfo
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' HighlightingInfo TCState
stSyntaxInfo
    PragmaOptions
optionsUsed    <- Lens' PragmaOptions TCState -> TCMT IO PragmaOptions
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' PragmaOptions TCState
stPragmaOptions
    Set QName
partialDefs    <- Lens' (Set QName) TCState -> TCMT IO (Set QName)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Set QName) TCState
stLocalPartialDefs

    -- Andreas, 2015-02-09 kill ranges in pattern synonyms before
    -- serialization to avoid error locations pointing to external files
    -- when expanding a pattern synonym.
    PatternSynDefns
patsyns <- PatternSynDefns -> PatternSynDefns
forall a. KillRange a => KillRangeT a
killRange (PatternSynDefns -> PatternSynDefns)
-> TCMT IO PatternSynDefns -> TCMT IO PatternSynDefns
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PatternSynDefns
forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getPatternSyns
    let builtin' :: Map String (Builtin (String, QName))
builtin' = (String -> Builtin PrimFun -> Builtin (String, QName))
-> Map String (Builtin PrimFun)
-> Map String (Builtin (String, QName))
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey (\ String
x Builtin PrimFun
b -> (String
x,) (QName -> (String, QName))
-> (PrimFun -> QName) -> PrimFun -> (String, QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimFun -> QName
primFunName (PrimFun -> (String, QName))
-> Builtin PrimFun -> Builtin (String, QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Builtin PrimFun
b) Map String (Builtin PrimFun)
builtin
    [TCWarning]
warnings <- WhichWarnings -> TCMT IO [TCWarning]
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m) =>
WhichWarnings -> m [TCWarning]
getAllWarnings WhichWarnings
AllWarnings
    String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface" Int
7 String
"  instantiating all meta variables"
    -- Note that the meta-variables in the definitions in "sig" have
    -- already been instantiated (by eliminateDeadCode).
    Interface
i <- Interface -> TCMT IO Interface
forall (m :: * -> *). MonadReduce m => Interface -> m Interface
instantiateFullExceptForDefinitions Interface :: Hash
-> Text
-> FileType
-> [(ModuleName, Hash)]
-> ModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> DisplayForms
-> Map QName Text
-> Maybe Text
-> Map String (Builtin (String, QName))
-> Map String [ForeignCode]
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Interface
Interface
      { iSourceHash :: Hash
iSourceHash      = Text -> Hash
hashText Text
source
      , iSource :: Text
iSource          = Text
source
      , iFileType :: FileType
iFileType        = FileType
fileType
      , iImportedModules :: [(ModuleName, Hash)]
iImportedModules = [(ModuleName, Hash)]
mhs
      , iModuleName :: ModuleName
iModuleName      = ModuleName
mname
      , iScope :: Map ModuleName Scope
iScope           = Map ModuleName Scope
forall a. Null a => a
empty -- publicModules scope
      , iInsideScope :: ScopeInfo
iInsideScope     = TopLevelInfo -> ScopeInfo
topLevelScope TopLevelInfo
topLevel
      , iSignature :: Signature
iSignature       = Signature
sig
      , iDisplayForms :: DisplayForms
iDisplayForms    = DisplayForms
display
      , iUserWarnings :: Map QName Text
iUserWarnings    = Map QName Text
userwarns
      , iImportWarning :: Maybe Text
iImportWarning   = Maybe Text
importwarn
      , iBuiltin :: Map String (Builtin (String, QName))
iBuiltin         = Map String (Builtin (String, QName))
builtin'
      , iForeignCode :: Map String [ForeignCode]
iForeignCode     = Map String [ForeignCode]
foreignCode
      , iHighlighting :: HighlightingInfo
iHighlighting    = HighlightingInfo
syntaxInfo
      , iDefaultPragmaOptions :: [OptionsPragma]
iDefaultPragmaOptions = [OptionsPragma]
defPragmas
      , iFilePragmaOptions :: [OptionsPragma]
iFilePragmaOptions    = [OptionsPragma]
filePragmas
      , iOptionsUsed :: PragmaOptions
iOptionsUsed     = PragmaOptions
optionsUsed
      , iPatternSyns :: PatternSynDefns
iPatternSyns     = PatternSynDefns
patsyns
      , iWarnings :: [TCWarning]
iWarnings        = [TCWarning]
warnings
      , iPartialDefs :: Set QName
iPartialDefs     = Set QName
partialDefs
      }
    String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface" Int
7 String
"  interface complete"
    Interface -> TCMT IO Interface
forall (m :: * -> *) a. Monad m => a -> m a
return Interface
i

-- | 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 :: String
ifile = AbsolutePath -> String
filePath (AbsolutePath -> String) -> AbsolutePath -> String
forall a b. (a -> b) -> a -> b
$ InterfaceFile -> AbsolutePath
intFilePath InterfaceFile
fp
  (ByteString
s, IO ()
close) <- String -> IO (ByteString, IO ())
readBinaryFile' String
ifile
  let hs :: Maybe (Hash, Hash)
hs = ByteString -> Maybe (Hash, Hash)
decodeHashes ByteString
s
  Hash -> ((Hash, Hash) -> Hash) -> Maybe (Hash, Hash) -> Hash
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Hash
0 ((Hash -> Hash -> Hash) -> (Hash, Hash) -> Hash
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Hash -> Hash -> Hash
forall a. Num a => a -> a -> a
(+)) Maybe (Hash, Hash)
hs Hash -> IO () -> IO ()
`seq` IO ()
close
  Maybe (Hash, Hash) -> IO (Maybe (Hash, Hash))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Hash, Hash)
hs

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