{-# LANGUAGE CPP #-}

{-| This module deals with finding imported modules and loading their
    interface files.
-}
module Agda.Interaction.Imports where

import Prelude hiding (null)

import Control.Arrow
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Trans.Maybe
import qualified Control.Exception as E

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.Monoid (mempty, mappend)
import Data.Map (Map)
import qualified Data.HashMap.Strict as HMap
import Data.Text.Lazy (Text)
import qualified Data.Text.Lazy as T

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

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
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  ( compress )
import Agda.Interaction.Highlighting.Vim
import Agda.Interaction.Options
import qualified Agda.Interaction.Options.Lenses as Lens
import Agda.Interaction.Response
  (RemoveTokenBasedHighlighting(KeepHighlighting))

import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.FileName
import Agda.Utils.Lens
import Agda.Utils.List
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

-- | Some information about the source code.

data SourceInfo = SourceInfo
  { SourceInfo -> Text
siSource     :: Text                  -- ^ Source code.
  , SourceInfo -> FileType
siFileType   :: FileType              -- ^ Source file type
  , SourceInfo -> Module
siModule     :: C.Module              -- ^ The parsed module.
  , SourceInfo -> TopLevelModuleName
siModuleName :: C.TopLevelModuleName  -- ^ The top-level module name.
  }

-- | Computes a 'SourceInfo' record for the given file.

sourceInfo :: SourceFile -> TCM SourceInfo
sourceInfo :: SourceFile -> TCM SourceInfo
sourceInfo (SourceFile AbsolutePath
f) = Account Phase -> TCM SourceInfo -> TCM SourceInfo
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Parsing] (TCM SourceInfo -> TCM SourceInfo)
-> TCM SourceInfo -> TCM SourceInfo
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
T.unpack Text
source
  TopLevelModuleName
moduleName            <- AbsolutePath -> Module -> TCM TopLevelModuleName
moduleName AbsolutePath
f Module
parsedMod
  SourceInfo -> TCM SourceInfo
forall (m :: * -> *) a. Monad m => a -> m a
return SourceInfo :: Text -> FileType -> Module -> TopLevelModuleName -> SourceInfo
SourceInfo
    { siSource :: Text
siSource     = Text
source
    , siFileType :: FileType
siFileType   = FileType
fileType
    , siModule :: Module
siModule     = Module
parsedMod
    , siModuleName :: TopLevelModuleName
siModuleName = TopLevelModuleName
moduleName
    }

-- | 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 -> ShowS
[Mode] -> ShowS
Mode -> String
(Int -> Mode -> ShowS)
-> (Mode -> String) -> ([Mode] -> ShowS) -> Show Mode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Mode] -> ShowS
$cshowList :: [Mode] -> ShowS
show :: Mode -> String
$cshow :: Mode -> String
showsPrec :: Int -> Mode -> ShowS
$cshowsPrec :: Int -> Mode -> ShowS
Show)

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

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

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

-- | 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.toList (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 pf)
bi      = [(String, Builtin pf)] -> Map String (Builtin pf)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (String
x,Term -> Builtin pf
forall pf. Term -> Builtin pf
Builtin Term
t) | (String
x,Builtin Term
t) <- [(String, Builtin (String, QName))]
builtin ]
        warns :: [TCWarning]
warns   = Interface -> [TCWarning]
iWarnings Interface
i
    BuiltinThings PrimFun
bs <- (TCState -> BuiltinThings PrimFun)
-> TCMT IO (BuiltinThings PrimFun)
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC TCState -> BuiltinThings 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 -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show (BuiltinThings PrimFun -> [String]
forall k a. Map k a -> [k]
Map.keys BuiltinThings PrimFun
bs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
      String
"  New builtins     " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show (Map String (Builtin Any) -> [String]
forall k a. Map k a -> [k]
Map.keys Map String (Builtin Any)
forall pf. Map String (Builtin pf)
bi)
    let check :: String -> m ()
check String
b = case (Builtin PrimFun
b1, Builtin Any
forall pf. Builtin pf
b2) of
            (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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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
            (Builtin PrimFun, Builtin Any)
_ -> m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
          where
            Just Builtin PrimFun
b1 = String -> BuiltinThings PrimFun -> Maybe (Builtin PrimFun)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
b BuiltinThings PrimFun
bs
            Just Builtin pf
b2 = String -> Map String (Builtin pf) -> Maybe (Builtin pf)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
b Map String (Builtin pf)
forall pf. Map String (Builtin pf)
bi
    (String -> TCM ()) -> [String] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> TCM ()
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m ()
check (((String, Builtin PrimFun) -> String)
-> [(String, Builtin PrimFun)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Builtin PrimFun) -> String
forall a b. (a, b) -> a
fst ([(String, Builtin PrimFun)] -> [String])
-> [(String, Builtin PrimFun)] -> [String]
forall a b. (a -> b) -> a -> b
$ BuiltinThings PrimFun -> [(String, Builtin PrimFun)]
forall k a. Map k a -> [(k, a)]
Map.toList (BuiltinThings PrimFun -> [(String, Builtin PrimFun)])
-> BuiltinThings PrimFun -> [(String, Builtin PrimFun)]
forall a b. (a -> b) -> a -> b
$ BuiltinThings PrimFun
-> Map String (Builtin Any) -> BuiltinThings PrimFun
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection BuiltinThings PrimFun
bs Map String (Builtin Any)
forall pf. Map String (Builtin pf)
bi)
    Signature
-> BuiltinThings PrimFun
-> PatternSynDefns
-> DisplayForms
-> Map QName String
-> Set QName
-> [TCWarning]
-> TCM ()
addImportedThings Signature
sig BuiltinThings PrimFun
forall pf. Map String (Builtin pf)
bi (Interface -> PatternSynDefns
iPatternSyns Interface
i) (Interface -> DisplayForms
iDisplayForms Interface
i) (Interface -> Map QName String
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 -> ShowS
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 Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (PragmaOptions -> Bool
optConfluenceCheck (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      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"
      [RewriteRule] -> TCM ()
checkConfluenceOfRules ([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' (BuiltinThings PrimFun) TCState
stImportedBuiltins Lens' (BuiltinThings PrimFun) TCState
-> (BuiltinThings PrimFun -> BuiltinThings PrimFun) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` String
-> Builtin PrimFun
-> BuiltinThings PrimFun
-> BuiltinThings 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 String    -- ^ Imported user warnings
  -> Set QName             -- ^ Name of imported definitions which are partial
  -> [TCWarning]
  -> TCM ()
addImportedThings :: Signature
-> BuiltinThings PrimFun
-> PatternSynDefns
-> DisplayForms
-> Map QName String
-> Set QName
-> [TCWarning]
-> TCM ()
addImportedThings Signature
isig BuiltinThings PrimFun
ibuiltin PatternSynDefns
patsyns DisplayForms
display Map QName String
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' (BuiltinThings PrimFun) TCState
stImportedBuiltins     Lens' (BuiltinThings PrimFun) TCState
-> (BuiltinThings PrimFun -> BuiltinThings PrimFun) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` \ BuiltinThings PrimFun
imp -> BuiltinThings PrimFun
-> BuiltinThings PrimFun -> BuiltinThings PrimFun
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union BuiltinThings PrimFun
imp BuiltinThings PrimFun
ibuiltin
  Lens' (Map QName String) TCState
stImportedUserWarnings Lens' (Map QName String) TCState
-> (Map QName String -> Map QName String) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` \ Map QName String
imp -> Map QName String -> Map QName String -> Map QName String
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map QName String
imp Map QName String
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] -> [TCWarning] -> [TCWarning]
forall a. Eq a => [a] -> [a] -> [a]
List.union [TCWarning]
imp [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 -> ShowS
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
      [TopLevelModuleName]
visited <- Map TopLevelModuleName ModuleInfo -> [TopLevelModuleName]
forall k a. Map k a -> [k]
Map.keys (Map TopLevelModuleName ModuleInfo -> [TopLevelModuleName])
-> TCMT IO (Map TopLevelModuleName ModuleInfo)
-> TCMT IO [TopLevelModuleName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Map TopLevelModuleName ModuleInfo)
getVisitedModules
      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 -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
", " ((TopLevelModuleName -> String) -> [TopLevelModuleName] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map TopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow [TopLevelModuleName]
visited)
    -- Since scopeCheckImport is called from the scope checker,
    -- we need to reimburse her account.
    Interface
i <- Account Phase -> TCMT IO Interface -> TCMT IO Interface
forall a (m :: * -> *) c. MonadBench a m => Account a -> 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
$ ModuleName -> TCMT IO Interface
getInterface ModuleName
x
    ModuleName -> TCM ()
addImport ModuleName
x

    -- If that interface was supposed to raise a warning on import, do so.
    Maybe String -> (String -> TCM ()) -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (Interface -> Maybe String
iImportWarning Interface
i) ((String -> TCM ()) -> TCM ()) -> (String -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Warning -> TCM ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning (Warning -> TCM ()) -> (String -> Warning) -> String -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> 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)

data MaybeWarnings' a = NoWarnings | SomeWarnings a
  deriving (Int -> MaybeWarnings' a -> ShowS
[MaybeWarnings' a] -> ShowS
MaybeWarnings' a -> String
(Int -> MaybeWarnings' a -> ShowS)
-> (MaybeWarnings' a -> String)
-> ([MaybeWarnings' a] -> ShowS)
-> Show (MaybeWarnings' a)
forall a. Show a => Int -> MaybeWarnings' a -> ShowS
forall a. Show a => [MaybeWarnings' a] -> ShowS
forall a. Show a => MaybeWarnings' a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MaybeWarnings' a] -> ShowS
$cshowList :: forall a. Show a => [MaybeWarnings' a] -> ShowS
show :: MaybeWarnings' a -> String
$cshow :: forall a. Show a => MaybeWarnings' a -> String
showsPrec :: Int -> MaybeWarnings' a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> MaybeWarnings' a -> ShowS
Show, a -> MaybeWarnings' b -> MaybeWarnings' a
(a -> b) -> MaybeWarnings' a -> MaybeWarnings' b
(forall a b. (a -> b) -> MaybeWarnings' a -> MaybeWarnings' b)
-> (forall a b. a -> MaybeWarnings' b -> MaybeWarnings' a)
-> Functor MaybeWarnings'
forall a b. a -> MaybeWarnings' b -> MaybeWarnings' a
forall a b. (a -> b) -> MaybeWarnings' a -> MaybeWarnings' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> MaybeWarnings' b -> MaybeWarnings' a
$c<$ :: forall a b. a -> MaybeWarnings' b -> MaybeWarnings' a
fmap :: (a -> b) -> MaybeWarnings' a -> MaybeWarnings' b
$cfmap :: forall a b. (a -> b) -> MaybeWarnings' a -> MaybeWarnings' b
Functor, MaybeWarnings' a -> Bool
(a -> m) -> MaybeWarnings' a -> m
(a -> b -> b) -> b -> MaybeWarnings' a -> b
(forall m. Monoid m => MaybeWarnings' m -> m)
-> (forall m a. Monoid m => (a -> m) -> MaybeWarnings' a -> m)
-> (forall m a. Monoid m => (a -> m) -> MaybeWarnings' a -> m)
-> (forall a b. (a -> b -> b) -> b -> MaybeWarnings' a -> b)
-> (forall a b. (a -> b -> b) -> b -> MaybeWarnings' a -> b)
-> (forall b a. (b -> a -> b) -> b -> MaybeWarnings' a -> b)
-> (forall b a. (b -> a -> b) -> b -> MaybeWarnings' a -> b)
-> (forall a. (a -> a -> a) -> MaybeWarnings' a -> a)
-> (forall a. (a -> a -> a) -> MaybeWarnings' a -> a)
-> (forall a. MaybeWarnings' a -> [a])
-> (forall a. MaybeWarnings' a -> Bool)
-> (forall a. MaybeWarnings' a -> Int)
-> (forall a. Eq a => a -> MaybeWarnings' a -> Bool)
-> (forall a. Ord a => MaybeWarnings' a -> a)
-> (forall a. Ord a => MaybeWarnings' a -> a)
-> (forall a. Num a => MaybeWarnings' a -> a)
-> (forall a. Num a => MaybeWarnings' a -> a)
-> Foldable MaybeWarnings'
forall a. Eq a => a -> MaybeWarnings' a -> Bool
forall a. Num a => MaybeWarnings' a -> a
forall a. Ord a => MaybeWarnings' a -> a
forall m. Monoid m => MaybeWarnings' m -> m
forall a. MaybeWarnings' a -> Bool
forall a. MaybeWarnings' a -> Int
forall a. MaybeWarnings' a -> [a]
forall a. (a -> a -> a) -> MaybeWarnings' a -> a
forall m a. Monoid m => (a -> m) -> MaybeWarnings' a -> m
forall b a. (b -> a -> b) -> b -> MaybeWarnings' a -> b
forall a b. (a -> b -> b) -> b -> MaybeWarnings' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: MaybeWarnings' a -> a
$cproduct :: forall a. Num a => MaybeWarnings' a -> a
sum :: MaybeWarnings' a -> a
$csum :: forall a. Num a => MaybeWarnings' a -> a
minimum :: MaybeWarnings' a -> a
$cminimum :: forall a. Ord a => MaybeWarnings' a -> a
maximum :: MaybeWarnings' a -> a
$cmaximum :: forall a. Ord a => MaybeWarnings' a -> a
elem :: a -> MaybeWarnings' a -> Bool
$celem :: forall a. Eq a => a -> MaybeWarnings' a -> Bool
length :: MaybeWarnings' a -> Int
$clength :: forall a. MaybeWarnings' a -> Int
null :: MaybeWarnings' a -> Bool
$cnull :: forall a. MaybeWarnings' a -> Bool
toList :: MaybeWarnings' a -> [a]
$ctoList :: forall a. MaybeWarnings' a -> [a]
foldl1 :: (a -> a -> a) -> MaybeWarnings' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> MaybeWarnings' a -> a
foldr1 :: (a -> a -> a) -> MaybeWarnings' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> MaybeWarnings' a -> a
foldl' :: (b -> a -> b) -> b -> MaybeWarnings' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> MaybeWarnings' a -> b
foldl :: (b -> a -> b) -> b -> MaybeWarnings' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> MaybeWarnings' a -> b
foldr' :: (a -> b -> b) -> b -> MaybeWarnings' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> MaybeWarnings' a -> b
foldr :: (a -> b -> b) -> b -> MaybeWarnings' a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> MaybeWarnings' a -> b
foldMap' :: (a -> m) -> MaybeWarnings' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> MaybeWarnings' a -> m
foldMap :: (a -> m) -> MaybeWarnings' a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> MaybeWarnings' a -> m
fold :: MaybeWarnings' m -> m
$cfold :: forall m. Monoid m => MaybeWarnings' m -> m
Foldable, Functor MaybeWarnings'
Foldable MaybeWarnings'
Functor MaybeWarnings'
-> Foldable MaybeWarnings'
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> MaybeWarnings' a -> f (MaybeWarnings' b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    MaybeWarnings' (f a) -> f (MaybeWarnings' a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> MaybeWarnings' a -> m (MaybeWarnings' b))
-> (forall (m :: * -> *) a.
    Monad m =>
    MaybeWarnings' (m a) -> m (MaybeWarnings' a))
-> Traversable MaybeWarnings'
(a -> f b) -> MaybeWarnings' a -> f (MaybeWarnings' b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
MaybeWarnings' (m a) -> m (MaybeWarnings' a)
forall (f :: * -> *) a.
Applicative f =>
MaybeWarnings' (f a) -> f (MaybeWarnings' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> MaybeWarnings' a -> m (MaybeWarnings' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> MaybeWarnings' a -> f (MaybeWarnings' b)
sequence :: MaybeWarnings' (m a) -> m (MaybeWarnings' a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
MaybeWarnings' (m a) -> m (MaybeWarnings' a)
mapM :: (a -> m b) -> MaybeWarnings' a -> m (MaybeWarnings' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> MaybeWarnings' a -> m (MaybeWarnings' b)
sequenceA :: MaybeWarnings' (f a) -> f (MaybeWarnings' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
MaybeWarnings' (f a) -> f (MaybeWarnings' a)
traverse :: (a -> f b) -> MaybeWarnings' a -> f (MaybeWarnings' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> MaybeWarnings' a -> f (MaybeWarnings' b)
$cp2Traversable :: Foldable MaybeWarnings'
$cp1Traversable :: Functor MaybeWarnings'
Traversable)
type MaybeWarnings = MaybeWarnings' [TCWarning]

applyFlagsToMaybeWarnings :: MaybeWarnings -> TCM MaybeWarnings
applyFlagsToMaybeWarnings :: MaybeWarnings -> TCM MaybeWarnings
applyFlagsToMaybeWarnings MaybeWarnings
mw = do
  MaybeWarnings
w' <- ([TCWarning] -> TCMT IO [TCWarning])
-> MaybeWarnings -> TCM MaybeWarnings
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse [TCWarning] -> TCMT IO [TCWarning]
applyFlagsToTCWarnings MaybeWarnings
mw
  MaybeWarnings -> TCM MaybeWarnings
forall (m :: * -> *) a. Monad m => a -> m a
return (MaybeWarnings -> TCM MaybeWarnings)
-> MaybeWarnings -> TCM MaybeWarnings
forall a b. (a -> b) -> a -> b
$ if MaybeWarnings -> Bool
forall a. Null a => a -> Bool
null MaybeWarnings
w' then MaybeWarnings
forall a. MaybeWarnings' a
NoWarnings else MaybeWarnings
w'

instance Null a => Null (MaybeWarnings' a) where
  empty :: MaybeWarnings' a
empty = MaybeWarnings' a
forall a. MaybeWarnings' a
NoWarnings
  null :: MaybeWarnings' a -> Bool
null MaybeWarnings' a
mws = case MaybeWarnings' a
mws of
    MaybeWarnings' a
NoWarnings      -> Bool
True
    SomeWarnings a
ws -> a -> Bool
forall a. Null a => a -> Bool
null a
ws

hasWarnings :: MaybeWarnings -> Bool
hasWarnings :: MaybeWarnings -> Bool
hasWarnings = Bool -> Bool
not (Bool -> Bool) -> (MaybeWarnings -> Bool) -> MaybeWarnings -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MaybeWarnings -> Bool
forall a. Null a => a -> Bool
null

-- | 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 (unless the 'MainInterface' is @'MainInterface'
-- 'ScopeCheck'@).

alreadyVisited :: C.TopLevelModuleName ->
                  MainInterface ->
                  PragmaOptions ->
                  TCM (Interface, MaybeWarnings) ->
                  TCM (Interface, MaybeWarnings)
alreadyVisited :: TopLevelModuleName
-> MainInterface
-> PragmaOptions
-> TCM (Interface, MaybeWarnings)
-> TCM (Interface, MaybeWarnings)
alreadyVisited TopLevelModuleName
x MainInterface
isMain PragmaOptions
currentOptions TCM (Interface, MaybeWarnings)
getIface = do
    Maybe ModuleInfo
mm <- TopLevelModuleName -> TCM (Maybe ModuleInfo)
getVisitedModule TopLevelModuleName
x
    case Maybe ModuleInfo
mm of
        -- A module with warnings should never be allowed to be
        -- imported from another module.
        Just ModuleInfo
mi | Bool -> Bool
not (ModuleInfo -> Bool
miWarnings ModuleInfo
mi) -> do
          String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.visit" Int
10 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ String
"  Already visited " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow TopLevelModuleName
x
          let i :: Interface
i = ModuleInfo -> Interface
miInterface ModuleInfo
mi
          -- Check that imported options are compatible with current ones,
          -- but give primitive modules a pass
          Bool
optsCompat <- if ModuleInfo -> Bool
miPrimitive ModuleInfo
mi then Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else
            TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((TCEnv -> Bool) -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envCheckOptionConsistency)
            {-then-} (PragmaOptions -> PragmaOptions -> ModuleName -> TCMT IO Bool
checkOptionsCompatible PragmaOptions
currentOptions (Interface -> PragmaOptions
iOptionsUsed Interface
i)
                                             (Interface -> ModuleName
iModuleName Interface
i))
            {-else-} (Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
          if Bool
optsCompat then (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall (m :: * -> *) a. Monad m => a -> m a
return (Interface
i , MaybeWarnings
forall a. MaybeWarnings' a
NoWarnings) else do
            MaybeWarnings
wt <- MainInterface -> WhichWarnings -> TCM MaybeWarnings
getMaybeWarnings' MainInterface
isMain WhichWarnings
ErrorWarnings
            (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall (m :: * -> *) a. Monad m => a -> m a
return (Interface
i, MaybeWarnings
wt)
        Maybe ModuleInfo
_ -> 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 -> ShowS
forall a. [a] -> [a] -> [a]
++ TopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow TopLevelModuleName
x
          r :: (Interface, MaybeWarnings)
r@(Interface
i, MaybeWarnings
wt) <- TCM (Interface, MaybeWarnings)
getIface
          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 -> ShowS
forall a. [a] -> [a] -> [a]
++ TopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow TopLevelModuleName
x
          Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (MainInterface
isMain MainInterface -> MainInterface -> Bool
forall a. Eq a => a -> a -> Bool
== Mode -> MainInterface
MainInterface Mode
ScopeCheck) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
            ModuleInfo -> TCM ()
visitModule ModuleInfo :: Interface -> Bool -> Bool -> ModuleInfo
ModuleInfo
              { miInterface :: Interface
miInterface  = Interface
i
              , miWarnings :: Bool
miWarnings   = MaybeWarnings -> Bool
hasWarnings MaybeWarnings
wt
              , miPrimitive :: Bool
miPrimitive  = Bool
False -- will be updated later for primitive modules
              }
          (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall (m :: * -> *) a. Monad m => a -> m a
return (Interface, MaybeWarnings)
r

-- | 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
  :: SourceFile
     -- ^ The path to the file.
  -> Mode
     -- ^ Should the file be type-checked, or only scope-checked?
  -> SourceInfo
     -- ^ Information about the source code.
  -> TCM (Interface, MaybeWarnings)
typeCheckMain :: SourceFile -> Mode -> SourceInfo -> TCM (Interface, MaybeWarnings)
typeCheckMain SourceFile
f Mode
mode SourceInfo
si = 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
libdir <- IO String -> TCMT IO String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO String
defaultLibDir
  let libdirPrim :: String
libdirPrim = String
libdir String -> ShowS
</> String
"prim"
  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 dir = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
libdir
  -- 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 ()
Lens.putPersistentVerbosity (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    (PersistentVerbosity -> PersistentVerbosity) -> TCM ()
Lens.modifyPersistentVerbosity ([String] -> 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
$ TCM () -> TCM ()
forall a. TCM a -> TCM a
withoutOptionsChecking (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_ (ShowS -> Set String -> Set String
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (String
libdirPrim String -> ShowS
</>) Set String
Lens.primitiveModules) ((String -> TCM ()) -> TCM ()) -> (String -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \String
f -> do
        let file :: SourceFile
file = AbsolutePath -> SourceFile
SourceFile (AbsolutePath -> SourceFile) -> AbsolutePath -> SourceFile
forall a b. (a -> b) -> a -> b
$ String -> AbsolutePath
mkAbsolute String
f
        SourceInfo
si <- SourceFile -> TCM SourceInfo
sourceInfo SourceFile
file
        TopLevelModuleName -> SourceFile -> TCM ()
checkModuleName' (SourceInfo -> TopLevelModuleName
siModuleName SourceInfo
si) SourceFile
file
        Interface
_ <- TopLevelModuleName -> Maybe SourceInfo -> TCMT IO Interface
getInterface_ (SourceInfo -> TopLevelModuleName
siModuleName SourceInfo
si) (SourceInfo -> Maybe SourceInfo
forall a. a -> Maybe a
Just SourceInfo
si)
        -- record that the just visited module is primitive
        TopLevelModuleName -> (ModuleInfo -> ModuleInfo) -> TCM ()
mapVisitedModule (SourceInfo -> TopLevelModuleName
siModuleName SourceInfo
si) (\ ModuleInfo
m -> ModuleInfo
m { miPrimitive :: Bool
miPrimitive = Bool
True })

  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' (SourceInfo -> TopLevelModuleName
siModuleName SourceInfo
si) SourceFile
f
  TopLevelModuleName
-> MainInterface
-> Maybe SourceInfo
-> TCM (Interface, MaybeWarnings)
getInterface' (SourceInfo -> TopLevelModuleName
siModuleName SourceInfo
si) (Mode -> MainInterface
MainInterface Mode
mode) (SourceInfo -> Maybe SourceInfo
forall a. a -> Maybe a
Just SourceInfo
si)
  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).
    (if Range -> Bool
forall a. Null a => a -> Bool
null Range
r then TCM () -> TCM ()
forall a. a -> a
id else Call -> TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (Range -> Call
SetRange Range
r)) (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
    where
    r :: Range
r = TopLevelModuleName -> Range
forall t. HasRange t => t -> Range
getRange TopLevelModuleName
m

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

getInterface :: ModuleName -> TCM Interface
getInterface :: ModuleName -> TCMT IO Interface
getInterface ModuleName
m = TopLevelModuleName -> Maybe SourceInfo -> TCMT IO Interface
getInterface_ (ModuleName -> TopLevelModuleName
toTopLevelModuleName ModuleName
m) Maybe SourceInfo
forall a. Maybe a
Nothing

-- | See 'getInterface'.

getInterface_
  :: C.TopLevelModuleName
  -> Maybe SourceInfo
     -- ^ Optional information about the source code.
  -> TCM Interface
getInterface_ :: TopLevelModuleName -> Maybe SourceInfo -> TCMT IO Interface
getInterface_ TopLevelModuleName
x Maybe SourceInfo
msi = do
  (Interface
i, MaybeWarnings
wt) <- TopLevelModuleName
-> MainInterface
-> Maybe SourceInfo
-> TCM (Interface, MaybeWarnings)
getInterface' TopLevelModuleName
x MainInterface
NotMainInterface Maybe SourceInfo
msi
  case MaybeWarnings
wt of
    SomeWarnings [TCWarning]
w  -> [TCWarning] -> TCMT IO Interface
forall a. [TCWarning] -> TCM a
tcWarningsToError ((TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
forall a. (a -> Bool) -> [a] -> [a]
filter (Warning -> Bool
notIM (Warning -> Bool) -> (TCWarning -> Warning) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning) [TCWarning]
w)
    MaybeWarnings
NoWarnings      -> Interface -> TCMT IO Interface
forall (m :: * -> *) a. Monad m => a -> m a
return Interface
i
   -- filter out unsolved interaction points for imported module so
   -- that we get the right error message (see test case Fail/Issue1296)
   where notIM :: Warning -> Bool
notIM UnsolvedInteractionMetas{} = Bool
False
         notIM Warning
_                          = Bool
True


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

getInterface'
  :: C.TopLevelModuleName
  -> MainInterface
  -> Maybe SourceInfo
     -- ^ Optional information about the source code.
  -> TCM (Interface, MaybeWarnings)
getInterface' :: TopLevelModuleName
-> MainInterface
-> Maybe SourceInfo
-> TCM (Interface, MaybeWarnings)
getInterface' TopLevelModuleName
x MainInterface
isMain Maybe SourceInfo
msi =
  TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a. TCM a -> TCM a
withIncreasedModuleNestingLevel (TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings))
-> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a b. (a -> b) -> a -> b
$
    -- Preserve the pragma options unless we are checking the main
    -- interface.
    TCMT IO PragmaOptions
-> (PragmaOptions -> TCM ())
-> TCM (Interface, MaybeWarnings)
-> TCM (Interface, MaybeWarnings)
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)
             (Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (MainInterface -> Bool
includeStateChanges MainInterface
isMain) (TCM () -> TCM ())
-> (PragmaOptions -> TCM ()) -> PragmaOptions -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Lens' PragmaOptions TCState
stPragmaOptions Lens' PragmaOptions TCState -> PragmaOptions -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens`)) (TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings))
-> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a b. (a -> b) -> a -> b
$ do
     -- We remember but reset the pragma options locally
     -- For the main interface, we also remember the pragmas from the file
     Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (MainInterface -> Bool
includeStateChanges MainInterface
isMain) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
       [[String]]
pragmas <- [Pragma] -> TCM [[String]]
concreteOptionsToOptionPragmas
                    (Module -> [Pragma]
forall a b. (a, b) -> a
fst (Module -> [Pragma]) -> Module -> [Pragma]
forall a b. (a -> b) -> a -> b
$ Module -> (SourceInfo -> Module) -> Maybe SourceInfo -> Module
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Module
forall a. HasCallStack => a
__IMPOSSIBLE__ SourceInfo -> Module
siModule Maybe SourceInfo
msi)
       ([String] -> TCM ()) -> [[String]] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [String] -> TCM ()
setOptionsFromPragma [[String]]
pragmas
     PragmaOptions
currentOptions <- Lens' PragmaOptions TCState -> TCMT IO PragmaOptions
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' PragmaOptions TCState
stPragmaOptions
     -- 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 (Interface, MaybeWarnings)
-> TCM (Interface, MaybeWarnings)
alreadyVisited TopLevelModuleName
x MainInterface
isMain PragmaOptions
currentOptions (TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings))
-> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName
-> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a. TopLevelModuleName -> TCM a -> TCM a
addImportCycleCheck TopLevelModuleName
x (TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings))
-> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a b. (a -> b) -> a -> b
$ do
      SourceFile
file <- TopLevelModuleName -> TCM SourceFile
findFile TopLevelModuleName
x  -- requires source to exist

      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

      Bool
uptodate <- Account Phase -> TCMT IO Bool -> TCMT IO Bool
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Import] (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ do
        Bool
ignore <- (TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
ignoreInterfaces TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M`
                    (Bool -> Bool
not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> TCMT IO Bool
Lens.isBuiltinModule (AbsolutePath -> String
filePath (AbsolutePath -> String) -> AbsolutePath -> String
forall a b. (a -> b) -> a -> b
$ SourceFile -> AbsolutePath
srcFilePath SourceFile
file)))
                  TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
ignoreAllInterfaces
        Maybe Interface
cached <- MaybeT TCM Interface -> TCM (Maybe Interface)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT TCM Interface -> TCM (Maybe Interface))
-> MaybeT TCM Interface -> TCM (Maybe Interface)
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> SourceFile -> MaybeT TCM Interface
isCached TopLevelModuleName
x SourceFile
file
          -- If it's cached ignoreInterfaces has no effect;
          -- to avoid typechecking a file more than once.
        Hash
sourceH <- case Maybe SourceInfo
msi of
                     Maybe SourceInfo
Nothing -> IO Hash -> TCMT IO Hash
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Hash -> TCMT IO Hash) -> IO Hash -> TCMT IO Hash
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> IO Hash
hashTextFile (SourceFile -> AbsolutePath
srcFilePath SourceFile
file)
                     Just SourceInfo
si -> Hash -> TCMT IO Hash
forall (m :: * -> *) a. Monad m => a -> m a
return (Hash -> TCMT IO Hash) -> Hash -> TCMT IO Hash
forall a b. (a -> b) -> a -> b
$ Text -> Hash
hashText (SourceInfo -> Text
siSource SourceInfo
si)
        Maybe Hash
ifaceH  <- case Maybe Interface
cached of
            Maybe Interface
Nothing -> do
              AbsolutePath
mifile <- SourceFile -> TCM AbsolutePath
toIFile SourceFile
file
              ((Hash, Hash) -> Hash) -> Maybe (Hash, Hash) -> Maybe Hash
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Hash, Hash) -> Hash
forall a b. (a, b) -> a
fst (Maybe (Hash, Hash) -> Maybe Hash)
-> TCMT IO (Maybe (Hash, Hash)) -> TCMT IO (Maybe Hash)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AbsolutePath -> TCMT IO (Maybe (Hash, Hash))
getInterfaceFileHashes AbsolutePath
mifile
            Just Interface
i  -> Maybe Hash -> TCMT IO (Maybe Hash)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Hash -> TCMT IO (Maybe Hash))
-> Maybe Hash -> TCMT IO (Maybe Hash)
forall a b. (a -> b) -> a -> b
$ Hash -> Maybe Hash
forall a. a -> Maybe a
Just (Hash -> Maybe Hash) -> Hash -> Maybe Hash
forall a b. (a -> b) -> a -> b
$ Interface -> Hash
iSourceHash Interface
i
        let unchanged :: Bool
unchanged = Hash -> Maybe Hash
forall a. a -> Maybe a
Just Hash
sourceH Maybe Hash -> Maybe Hash -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Hash
ifaceH
        Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ Bool
unchanged Bool -> Bool -> Bool
&& (Bool -> Bool
not Bool
ignore Bool -> Bool -> Bool
|| Maybe Interface -> Bool
forall a. Maybe a -> Bool
isJust Maybe Interface
cached)

      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
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow TopLevelModuleName
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is " String -> ShowS
forall a. [a] -> [a] -> [a]
++
        (if Bool
uptodate then String
"" else String
"not ") String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"up-to-date."

      (Bool
stateChangesIncluded, (Interface
i, MaybeWarnings
wt)) <- do
        -- -- 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.
        let maySkip :: Bool
maySkip = Bool
True

        if Bool
uptodate Bool -> Bool -> Bool
&& Bool
maySkip
          then TopLevelModuleName
-> SourceFile
-> MainInterface
-> Maybe SourceInfo
-> TCMT IO (Bool, (Interface, MaybeWarnings))
getStoredInterface TopLevelModuleName
x SourceFile
file MainInterface
isMain Maybe SourceInfo
msi
          else TopLevelModuleName
-> SourceFile
-> MainInterface
-> Maybe SourceInfo
-> TCMT IO (Bool, (Interface, MaybeWarnings))
typeCheck          TopLevelModuleName
x SourceFile
file MainInterface
isMain Maybe SourceInfo
msi

      -- 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 -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TopLevelModuleName
topLevelName TopLevelModuleName -> TopLevelModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== TopLevelModuleName
x) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        -- Andreas, 2014-03-27 This check is now done in the scope checker.
        -- checkModuleName topLevelName file
        TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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
visited <- TopLevelModuleName -> TCMT IO Bool
isVisited TopLevelModuleName
x
      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
$ if Bool
visited then String
"  We've been here. Don't merge."
                                   else String
"  New module. Let's check it out."

      -- Check that imported module options are consistent with
      -- current options (issue #2487)
      -- compute updated warnings if needed
      MaybeWarnings
wt' <- TCMT IO Bool
-> TCM MaybeWarnings -> TCM MaybeWarnings -> TCM MaybeWarnings
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Bool -> Bool
not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Bool) -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envCheckOptionConsistency)
                 {- then -} (MaybeWarnings -> TCM MaybeWarnings
forall (m :: * -> *) a. Monad m => a -> m a
return MaybeWarnings
wt) {- else -} (TCM MaybeWarnings -> TCM MaybeWarnings)
-> TCM MaybeWarnings -> TCM MaybeWarnings
forall a b. (a -> b) -> a -> b
$ do
        Bool
optComp <- PragmaOptions -> PragmaOptions -> ModuleName -> TCMT IO Bool
checkOptionsCompatible PragmaOptions
currentOptions (Interface -> PragmaOptions
iOptionsUsed Interface
i) (Interface -> ModuleName
iModuleName Interface
i)
        -- we might have aquired some more warnings when consistency checking
        if Bool
optComp then MaybeWarnings -> TCM MaybeWarnings
forall (m :: * -> *) a. Monad m => a -> m a
return MaybeWarnings
wt else MainInterface -> WhichWarnings -> TCM MaybeWarnings
getMaybeWarnings' MainInterface
isMain WhichWarnings
ErrorWarnings

      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
visited Bool -> Bool -> Bool
|| Bool
stateChangesIncluded) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        Interface -> TCM ()
mergeInterface Interface
i
        Account Phase -> TCM () -> TCM ()
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Highlighting] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
          HighlightingLevel -> TCM () -> TCM ()
forall (tcm :: * -> *).
MonadTCM 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

      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 Interface
i)

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

      String -> Int -> [String] -> TCM ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Int -> a -> m ()
reportS String
"warning.import" Int
10
        [ String
"module: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show (TopLevelModuleName -> [String]
C.moduleNameParts TopLevelModuleName
x)
        , String
"WarningOnImport: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe String -> String
forall a. Show a => a -> String
show (Interface -> Maybe String
iImportWarning Interface
i)
        ]
      (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall (m :: * -> *) a. Monad m => a -> m a
return (Interface
i, MaybeWarnings
wt')

-- | 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 -> TCMT IO Bool
checkOptionsCompatible PragmaOptions
current PragmaOptions
imported ModuleName
importedModule = (StateT Bool TCM () -> Bool -> TCMT IO Bool)
-> Bool -> StateT Bool TCM () -> TCMT IO Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT Bool TCM () -> Bool -> TCMT IO Bool
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT Bool
True (StateT Bool TCM () -> TCMT IO Bool)
-> StateT Bool TCM () -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ do
  String -> Int -> TCM Doc -> StateT Bool TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"import.iface.options" Int
5 (TCM Doc -> StateT Bool TCM ()) -> TCM Doc -> StateT Bool TCM ()
forall a b. (a -> b) -> a -> b
$ Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
P.nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"current options  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> PragmaOptions -> TCM Doc
forall (m :: * -> *).
(Monad m, Semigroup (m Doc), IsString (m Doc)) =>
PragmaOptions -> m Doc
showOptions PragmaOptions
current
  String -> Int -> TCM Doc -> StateT Bool TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"import.iface.options" Int
5 (TCM Doc -> StateT Bool TCM ()) -> TCM Doc -> StateT Bool TCM ()
forall a b. (a -> b) -> a -> b
$ Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
P.nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"imported options =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> PragmaOptions -> TCM Doc
forall (m :: * -> *).
(Monad m, Semigroup (m Doc), IsString (m Doc)) =>
PragmaOptions -> m Doc
showOptions PragmaOptions
imported
  [(PragmaOptions -> Bool, String)]
-> ((PragmaOptions -> Bool, String) -> StateT Bool TCM ())
-> StateT Bool TCM ()
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 TCM ())
 -> StateT Bool TCM ())
-> ((PragmaOptions -> Bool, String) -> StateT Bool TCM ())
-> StateT Bool TCM ()
forall a b. (a -> b) -> a -> b
$ \ (PragmaOptions -> Bool
opt, String
optName) -> do
    Bool -> StateT Bool TCM () -> StateT Bool TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (PragmaOptions -> Bool
opt PragmaOptions
current Bool -> Bool -> Bool
`implies` PragmaOptions -> Bool
opt PragmaOptions
imported) (StateT Bool TCM () -> StateT Bool TCM ())
-> StateT Bool TCM () -> StateT Bool TCM ()
forall a b. (a -> b) -> a -> b
$ do
      Bool -> StateT Bool TCM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put Bool
False
      Warning -> StateT Bool TCM ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning (String -> ModuleName -> Warning
CoInfectiveImport String
optName ModuleName
importedModule)
  [(PragmaOptions -> Bool, String)]
-> ((PragmaOptions -> Bool, String) -> StateT Bool TCM ())
-> StateT Bool TCM ()
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 TCM ())
 -> StateT Bool TCM ())
-> ((PragmaOptions -> Bool, String) -> StateT Bool TCM ())
-> StateT Bool TCM ()
forall a b. (a -> b) -> a -> b
$ \ (PragmaOptions -> Bool
opt, String
optName) -> do
    Bool -> StateT Bool TCM () -> StateT Bool TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (PragmaOptions -> Bool
opt PragmaOptions
imported Bool -> Bool -> Bool
`implies` PragmaOptions -> Bool
opt PragmaOptions
current) (StateT Bool TCM () -> StateT Bool TCM ())
-> StateT Bool TCM () -> StateT Bool TCM ()
forall a b. (a -> b) -> a -> b
$ do
      Bool -> StateT Bool TCM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put Bool
False
      Warning -> StateT Bool TCM ()
forall (m :: * -> *). 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 :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[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 :: * -> *). Monad 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. (Monad m, Pretty a) => a -> m Doc
P.pretty (Bool -> m Doc) -> Bool -> m Doc
forall a b. (a -> b) -> a -> b
$ 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))

-- | Check whether interface file exists and is in cache
--   in the correct version (as testified by the interface file hash).

isCached
  :: C.TopLevelModuleName
     -- ^ Module name of file we process.
  -> SourceFile
     -- ^ File we process.
  -> MaybeT TCM Interface

isCached :: TopLevelModuleName -> SourceFile -> MaybeT TCM Interface
isCached TopLevelModuleName
x SourceFile
file = do
  InterfaceFile
ifile <- TCMT IO (Maybe InterfaceFile) -> MaybeT TCM InterfaceFile
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe InterfaceFile) -> MaybeT TCM InterfaceFile)
-> TCMT IO (Maybe InterfaceFile) -> MaybeT TCM InterfaceFile
forall a b. (a -> b) -> a -> b
$ SourceFile -> TCMT IO (Maybe InterfaceFile)
findInterfaceFile' SourceFile
file

  -- Check that we have cached the module.
  Interface
mi <- TCM (Maybe Interface) -> MaybeT TCM Interface
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCM (Maybe Interface) -> MaybeT TCM Interface)
-> TCM (Maybe Interface) -> MaybeT TCM Interface
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> TCM (Maybe Interface)
getDecodedModule TopLevelModuleName
x

  -- Check that the interface file exists and return its hash.
  Hash
h  <- TCMT IO (Maybe Hash) -> MaybeT TCM Hash
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe Hash) -> MaybeT TCM Hash)
-> TCMT IO (Maybe Hash) -> MaybeT TCM Hash
forall a b. (a -> b) -> a -> b
$ ((Hash, Hash) -> Hash) -> Maybe (Hash, Hash) -> Maybe Hash
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Hash, Hash) -> Hash
forall a b. (a, b) -> b
snd (Maybe (Hash, Hash) -> Maybe Hash)
-> TCMT IO (Maybe (Hash, Hash)) -> TCMT IO (Maybe Hash)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InterfaceFile -> TCMT IO (Maybe (Hash, Hash))
getInterfaceFileHashes' InterfaceFile
ifile

  -- Make sure the hashes match.
  Bool -> MaybeT TCM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> MaybeT TCM ()) -> Bool -> MaybeT TCM ()
forall a b. (a -> b) -> a -> b
$ Interface -> Hash
iFullHash Interface
mi Hash -> Hash -> Bool
forall a. Eq a => a -> a -> Bool
== Hash
h

  Interface -> MaybeT TCM Interface
forall (m :: * -> *) a. Monad m => a -> m a
return Interface
mi

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

getStoredInterface
  :: C.TopLevelModuleName
     -- ^ Module name of file we process.
  -> SourceFile
     -- ^ File we process.
  -> MainInterface
  -> Maybe SourceInfo
     -- ^ Optional information about the source code.
  -> TCM (Bool, (Interface, MaybeWarnings))
     -- ^ @Bool@ is: do we have to merge the interface?
getStoredInterface :: TopLevelModuleName
-> SourceFile
-> MainInterface
-> Maybe SourceInfo
-> TCMT IO (Bool, (Interface, MaybeWarnings))
getStoredInterface TopLevelModuleName
x SourceFile
file MainInterface
isMain Maybe SourceInfo
msi = do
  let fp :: String
fp = AbsolutePath -> String
filePath (AbsolutePath -> String) -> AbsolutePath -> String
forall a b. (a -> b) -> a -> b
$ SourceFile -> AbsolutePath
srcFilePath SourceFile
file
  -- If something goes wrong (interface outdated etc.)
  -- we revert to fresh type checking.
  let fallback :: TCMT IO (Bool, (Interface, MaybeWarnings))
fallback = TopLevelModuleName
-> SourceFile
-> MainInterface
-> Maybe SourceInfo
-> TCMT IO (Bool, (Interface, MaybeWarnings))
typeCheck TopLevelModuleName
x SourceFile
file MainInterface
isMain Maybe SourceInfo
msi

  -- 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.
  AbsolutePath
ifile <- SourceFile -> TCM AbsolutePath
toIFile SourceFile
file
  let ifp :: String
ifp = AbsolutePath -> String
filePath AbsolutePath
ifile
  Maybe Hash
h <- ((Hash, Hash) -> Hash) -> Maybe (Hash, Hash) -> Maybe Hash
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Hash, Hash) -> Hash
forall a b. (a, b) -> b
snd (Maybe (Hash, Hash) -> Maybe Hash)
-> TCMT IO (Maybe (Hash, Hash)) -> TCMT IO (Maybe Hash)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AbsolutePath -> TCMT IO (Maybe (Hash, Hash))
getInterfaceFileHashes AbsolutePath
ifile
  Maybe Interface
mm <- TopLevelModuleName -> TCM (Maybe Interface)
getDecodedModule TopLevelModuleName
x
  (Bool
cached, Maybe Interface
mi) <- Account Phase
-> TCMT IO (Bool, Maybe Interface)
-> TCMT IO (Bool, Maybe Interface)
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Deserialization] (TCMT IO (Bool, Maybe Interface)
 -> TCMT IO (Bool, Maybe Interface))
-> TCMT IO (Bool, Maybe Interface)
-> TCMT IO (Bool, Maybe Interface)
forall a b. (a -> b) -> a -> b
$ case Maybe Interface
mm of
    Just Interface
mi ->
      if Hash -> Maybe Hash
forall a. a -> Maybe a
Just (Interface -> Hash
iFullHash Interface
mi) Maybe Hash -> Maybe Hash -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe Hash
h
      then do
        TopLevelModuleName -> TCM ()
dropDecodedModule TopLevelModuleName
x
        String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface" Int
50 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ String
"  cached hash = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Hash -> String
forall a. Show a => a -> String
show (Interface -> Hash
iFullHash Interface
mi)
        String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface" Int
50 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ String
"  stored hash = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe Hash -> String
forall a. Show a => a -> String
show Maybe Hash
h
        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
"  file is newer, re-reading " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
ifp
        (Bool
False,) (Maybe Interface -> (Bool, Maybe Interface))
-> TCM (Maybe Interface) -> TCMT IO (Bool, Maybe Interface)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AbsolutePath -> TCM (Maybe Interface)
readInterface AbsolutePath
ifile
      else 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
"  using stored version of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
ifp
        (Bool, Maybe Interface) -> TCMT IO (Bool, Maybe Interface)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, Interface -> Maybe Interface
forall a. a -> Maybe a
Just Interface
mi)
    Maybe Interface
Nothing -> 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
"  no stored version, reading " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
ifp
      (Bool
False,) (Maybe Interface -> (Bool, Maybe Interface))
-> TCM (Maybe Interface) -> TCMT IO (Bool, Maybe Interface)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AbsolutePath -> TCM (Maybe Interface)
readInterface AbsolutePath
ifile

  -- Check that it's the right version
  case Maybe Interface
mi of
    Maybe Interface
Nothing       -> do
      String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface" Int
5 String
"  bad interface, re-type checking"
      TCMT IO (Bool, (Interface, MaybeWarnings))
fallback
    Just Interface
i        -> 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
"  imports: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(ModuleName, Hash)] -> String
forall a. Show a => a -> String
show (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.
      ([String] -> TCM ()) -> [[String]] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [String] -> TCM ()
setOptionsFromPragma (Interface -> [[String]]
iPragmaOptions Interface
i)

      -- Check that options that matter haven't changed compared to
      -- current options (issue #2487)
      Bool
optionsChanged <-TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((Bool -> Bool
not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Bool) -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envCheckOptionConsistency) TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M`
                            String -> TCMT IO Bool
Lens.isBuiltinModule String
fp)
                       {-then-} (Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) {-else-} (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ do
        PragmaOptions
currentOptions <- Lens' PragmaOptions TCState -> TCMT IO PragmaOptions
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' PragmaOptions TCState
stPragmaOptions
        let disagreements :: [String]
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) ]
        if [String] -> Bool
forall a. Null a => a -> Bool
null [String]
disagreements then Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False else do
          String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface.options" Int
4 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            [ String
"  Changes in the following options in "
            , ShowS
forall a. Pretty a => a -> String
prettyShow String
fp
            , String
", re-typechecking: "
            , [String] -> String
forall a. Pretty a => a -> String
prettyShow [String]
disagreements
            ]
          Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

      if Bool
optionsChanged then TCMT IO (Bool, (Interface, MaybeWarnings))
fallback else do

        [Hash]
hs <- (Interface -> Hash) -> [Interface] -> [Hash]
forall a b. (a -> b) -> [a] -> [b]
map Interface -> Hash
iFullHash ([Interface] -> [Hash]) -> TCMT IO [Interface] -> TCMT IO [Hash]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ModuleName -> TCMT IO Interface)
-> [ModuleName] -> TCMT IO [Interface]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ModuleName -> TCMT IO Interface
getInterface (((ModuleName, Hash) -> ModuleName)
-> [(ModuleName, Hash)] -> [ModuleName]
forall a b. (a -> b) -> [a] -> [b]
map (ModuleName, Hash) -> ModuleName
forall a b. (a, b) -> a
fst ([(ModuleName, Hash)] -> [ModuleName])
-> [(ModuleName, Hash)] -> [ModuleName]
forall a b. (a -> b) -> a -> b
$ Interface -> [(ModuleName, Hash)]
iImportedModules Interface
i)

        -- If any of the imports are newer we need to retype check
        if [Hash]
hs [Hash] -> [Hash] -> Bool
forall a. Eq a => a -> a -> Bool
/= ((ModuleName, Hash) -> Hash) -> [(ModuleName, Hash)] -> [Hash]
forall a b. (a -> b) -> [a] -> [b]
map (ModuleName, Hash) -> Hash
forall a b. (a, b) -> b
snd (Interface -> [(ModuleName, Hash)]
iImportedModules Interface
i)
          then TCMT IO (Bool, (Interface, MaybeWarnings))
fallback
          else do
            Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
cached (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
              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 -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([TCWarning] -> Bool
forall a. Null a => a -> Bool
null [TCWarning]
ws) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"warning" Int
1 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
P.vcat ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCWarning -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
P.prettyTCM (TCWarning -> TCM Doc) -> [TCWarning] -> [TCM Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TCWarning]
ws

            (Bool, (Interface, MaybeWarnings))
-> TCMT IO (Bool, (Interface, MaybeWarnings))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, (Interface
i, MaybeWarnings
forall a. MaybeWarnings' a
NoWarnings))

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

typeCheck
  :: C.TopLevelModuleName
     -- ^ Module name of file we process.
  -> SourceFile
     -- ^ File we process.
  -> MainInterface
  -> Maybe SourceInfo
     -- ^ Optional information about the source code.
  -> TCM (Bool, (Interface, MaybeWarnings))
     -- ^ @Bool@ is: do we have to merge the interface?
typeCheck :: TopLevelModuleName
-> SourceFile
-> MainInterface
-> Maybe SourceInfo
-> TCMT IO (Bool, (Interface, MaybeWarnings))
typeCheck TopLevelModuleName
x SourceFile
file MainInterface
isMain Maybe SourceInfo
msi = do
  let fp :: String
fp = AbsolutePath -> String
filePath (AbsolutePath -> String) -> AbsolutePath -> String
forall a b. (a -> b) -> a -> b
$ SourceFile -> AbsolutePath
srcFilePath SourceFile
file
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (MainInterface -> Bool
includeStateChanges MainInterface
isMain) TCM ()
forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog
  let checkMsg :: String
checkMsg = case MainInterface
isMain of
                   MainInterface Mode
ScopeCheck -> String
"Reading "
                   MainInterface
_                        -> String
"Checking"
      withMsgs :: TCMT IO b -> TCMT IO b
withMsgs = TCM () -> (() -> TCM ()) -> TCMT IO b -> TCMT IO b
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]
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 -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"warning" Int
1 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
P.vcat ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCWarning -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
P.prettyTCM (TCWarning -> TCM Doc) -> [TCWarning] -> [TCM 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)

  -- Do the type checking.

  case MainInterface
isMain of
    MainInterface Mode
_ -> do
      (Interface, MaybeWarnings)
r <- TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a. TCM a -> TCM a
withMsgs (TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings))
-> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a b. (a -> b) -> a -> b
$ SourceFile
-> TopLevelModuleName
-> MainInterface
-> Maybe SourceInfo
-> TCM (Interface, MaybeWarnings)
createInterface SourceFile
file TopLevelModuleName
x MainInterface
isMain Maybe SourceInfo
msi
      (Bool, (Interface, MaybeWarnings))
-> TCMT IO (Bool, (Interface, MaybeWarnings))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, (Interface, MaybeWarnings)
r)

    MainInterface
NotMainInterface -> do
      [TopLevelModuleName]
ms          <- TCMT IO [TopLevelModuleName]
getImportPath
      Int
nesting     <- (TCEnv -> Int) -> TCMT IO Int
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Int
envModuleNestingLevel
      Range
range       <- (TCEnv -> Range) -> TCMT IO Range
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Range
envRange
      Maybe (Closure Call)
call        <- (TCEnv -> Maybe (Closure Call)) -> TCMT IO (Maybe (Closure Call))
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe (Closure Call)
envCall
      ModuleToSource
mf          <- Lens' ModuleToSource TCState -> TCMT IO ModuleToSource
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' ModuleToSource TCState
stModuleToSource
      Map TopLevelModuleName ModuleInfo
vs          <- TCMT IO (Map TopLevelModuleName ModuleInfo)
getVisitedModules
      DecodedModules
ds          <- TCM DecodedModules
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
      BuiltinThings PrimFun
ibuiltin    <- Lens' (BuiltinThings PrimFun) TCState
-> TCMT IO (BuiltinThings PrimFun)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (BuiltinThings 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 String
userwarn    <- Lens' (Map QName String) TCState -> TCMT IO (Map QName String)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map QName String) 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       <- TCM 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.
      Either TCErr ((Interface, MaybeWarnings), TCM ())
r <- TCMT IO (Either TCErr ((Interface, MaybeWarnings), TCM ()))
-> TCMT IO (Either TCErr ((Interface, MaybeWarnings), TCM ()))
forall (m :: * -> *) a.
(MonadTCState m, ReadTCState m) =>
m a -> m a
withoutCache (TCMT IO (Either TCErr ((Interface, MaybeWarnings), TCM ()))
 -> TCMT IO (Either TCErr ((Interface, MaybeWarnings), TCM ())))
-> TCMT IO (Either TCErr ((Interface, MaybeWarnings), TCM ()))
-> TCMT IO (Either TCErr ((Interface, MaybeWarnings), TCM ()))
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
           TCM ((Interface, MaybeWarnings), TCM ())
-> TCMT IO (Either TCErr ((Interface, MaybeWarnings), TCM ()))
forall a. TCM a -> TCM (Either TCErr a)
freshTCM (TCM ((Interface, MaybeWarnings), TCM ())
 -> TCMT IO (Either TCErr ((Interface, MaybeWarnings), TCM ())))
-> TCM ((Interface, MaybeWarnings), TCM ())
-> TCMT IO (Either TCErr ((Interface, MaybeWarnings), TCM ()))
forall a b. (a -> b) -> a -> b
$
             [TopLevelModuleName]
-> TCM ((Interface, MaybeWarnings), TCM ())
-> TCM ((Interface, MaybeWarnings), TCM ())
forall a. [TopLevelModuleName] -> TCM a -> TCM a
withImportPath [TopLevelModuleName]
ms (TCM ((Interface, MaybeWarnings), TCM ())
 -> TCM ((Interface, MaybeWarnings), TCM ()))
-> TCM ((Interface, MaybeWarnings), TCM ())
-> TCM ((Interface, MaybeWarnings), TCM ())
forall a b. (a -> b) -> a -> b
$
             (TCEnv -> TCEnv)
-> TCM ((Interface, MaybeWarnings), TCM ())
-> TCM ((Interface, MaybeWarnings), TCM ())
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\TCEnv
e -> TCEnv
e { envModuleNestingLevel :: Int
envModuleNestingLevel = Int
nesting
                              -- 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
                            }) (TCM ((Interface, MaybeWarnings), TCM ())
 -> TCM ((Interface, MaybeWarnings), TCM ()))
-> TCM ((Interface, MaybeWarnings), TCM ())
-> TCM ((Interface, MaybeWarnings), TCM ())
forall a b. (a -> b) -> a -> b
$ do
               DecodedModules -> TCM ()
setDecodedModules DecodedModules
ds
               CommandLineOptions -> TCM ()
setCommandLineOptions CommandLineOptions
opts
               InteractionOutputCallback -> TCM ()
setInteractionOutputCallback InteractionOutputCallback
ho
               Lens' ModuleToSource TCState
stModuleToSource Lens' ModuleToSource TCState -> ModuleToSource -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` ModuleToSource
mf
               Map TopLevelModuleName ModuleInfo -> TCM ()
setVisitedModules Map TopLevelModuleName ModuleInfo
vs
               Signature
-> BuiltinThings PrimFun
-> PatternSynDefns
-> DisplayForms
-> Map QName String
-> Set QName
-> [TCWarning]
-> TCM ()
addImportedThings Signature
isig BuiltinThings PrimFun
ibuiltin PatternSynDefns
ipatsyns DisplayForms
display Map QName String
userwarn Set QName
partialdefs []

               (Interface, MaybeWarnings)
r  <- TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a. TCM a -> TCM a
withMsgs (TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings))
-> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a b. (a -> b) -> a -> b
$ SourceFile
-> TopLevelModuleName
-> MainInterface
-> Maybe SourceInfo
-> TCM (Interface, MaybeWarnings)
createInterface SourceFile
file TopLevelModuleName
x MainInterface
isMain Maybe SourceInfo
msi
               ModuleToSource
mf <- Lens' ModuleToSource TCState -> TCMT IO ModuleToSource
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' ModuleToSource TCState
stModuleToSource
               DecodedModules
ds <- TCM DecodedModules
getDecodedModules
               ((Interface, MaybeWarnings), TCM ())
-> TCM ((Interface, MaybeWarnings), TCM ())
forall (m :: * -> *) a. Monad m => a -> m a
return ((Interface, MaybeWarnings)
r, do
                  Lens' ModuleToSource TCState
stModuleToSource Lens' ModuleToSource TCState -> ModuleToSource -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` ModuleToSource
mf
                  DecodedModules -> TCM ()
setDecodedModules DecodedModules
ds
                  case (Interface, MaybeWarnings)
r of
                    (Interface
i, MaybeWarnings
NoWarnings) -> Interface -> TCM ()
storeDecodedModule Interface
i
                    (Interface, MaybeWarnings)
_               -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                  )

      case Either TCErr ((Interface, MaybeWarnings), TCM ())
r of
          Left TCErr
err          -> TCErr -> TCMT IO (Bool, (Interface, MaybeWarnings))
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
          Right ((Interface, MaybeWarnings)
r, TCM ()
update) -> do
            TCM ()
update
            case (Interface, MaybeWarnings)
r of
              (Interface
_, MaybeWarnings
NoWarnings) ->
                -- 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.)
                TopLevelModuleName
-> SourceFile
-> MainInterface
-> Maybe SourceInfo
-> TCMT IO (Bool, (Interface, MaybeWarnings))
getStoredInterface TopLevelModuleName
x SourceFile
file MainInterface
isMain Maybe SourceInfo
msi
              (Interface, MaybeWarnings)
_ -> (Bool, (Interface, MaybeWarnings))
-> TCMT IO (Bool, (Interface, MaybeWarnings))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, (Interface, MaybeWarnings)
r)

-- | 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 TCEnv -> Int
envModuleNestingLevel
  let maybeFile :: String
maybeFile = Maybe String -> String -> ShowS -> String
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe String
file String
"." (ShowS -> String) -> ShowS -> String
forall a b. (a -> b) -> a -> b
$ \ String
f -> String
" (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
f String -> ShowS
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
$ [String] -> 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 -> ShowS
forall a. [a] -> [a] -> [a]
++ AbsolutePath -> String
filePath (SourceFile -> AbsolutePath
srcFilePath SourceFile
file) String -> ShowS
forall a. [a] -> [a] -> [a]
++
    String
" (read from interface)."
  RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
forall (tcm :: * -> *).
(MonadTCM tcm, ReadTCState tcm) =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> tcm ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting (Interface -> HighlightingInfo
iHighlighting Interface
i)

-- | Read interface file corresponding to a module.

readInterface :: AbsolutePath -> TCM (Maybe Interface)
readInterface :: AbsolutePath -> TCM (Maybe Interface)
readInterface AbsolutePath
file = MaybeT TCM Interface -> TCM (Maybe Interface)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT TCM Interface -> TCM (Maybe Interface))
-> MaybeT TCM Interface -> TCM (Maybe Interface)
forall a b. (a -> b) -> a -> b
$ do
  InterfaceFile
ifile <- TCMT IO (Maybe InterfaceFile) -> MaybeT TCM InterfaceFile
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe InterfaceFile) -> MaybeT TCM InterfaceFile)
-> TCMT IO (Maybe InterfaceFile) -> MaybeT TCM InterfaceFile
forall a b. (a -> b) -> a -> b
$ IO (Maybe InterfaceFile) -> TCMT IO (Maybe InterfaceFile)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe InterfaceFile) -> TCMT IO (Maybe InterfaceFile))
-> IO (Maybe InterfaceFile) -> TCMT IO (Maybe InterfaceFile)
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> IO (Maybe InterfaceFile)
mkInterfaceFile AbsolutePath
file
  TCM (Maybe Interface) -> MaybeT TCM Interface
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCM (Maybe Interface) -> MaybeT TCM Interface)
-> TCM (Maybe Interface) -> MaybeT TCM Interface
forall a b. (a -> b) -> a -> b
$ InterfaceFile -> TCM (Maybe Interface)
readInterface' InterfaceFile
ifile

readInterface' :: InterfaceFile -> TCM (Maybe Interface)
readInterface' :: InterfaceFile -> TCM (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) -> TCM (Maybe Interface)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe Interface) -> TCM (Maybe Interface))
-> (Maybe Interface -> IO (Maybe Interface))
-> Maybe Interface
-> TCM (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 -> TCM (Maybe Interface))
-> TCM (Maybe Interface) -> TCM (Maybe Interface)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ByteString -> TCM (Maybe Interface)
decodeInterface ByteString
s

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

        Maybe Interface -> TCM (Maybe Interface)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Interface -> TCM (Maybe Interface))
-> Maybe Interface -> TCM (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
      TCM (Maybe Interface)
-> (TCErr -> TCM (Maybe Interface)) -> TCM (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 () -> TCM (Maybe Interface) -> TCM (Maybe Interface)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TCErr -> TCM (Maybe Interface)
forall (m :: * -> *) a.
(MonadDebug m, MonadError TCErr m) =>
TCErr -> m (Maybe a)
handler TCErr
e
  -- Catch exceptions
  TCM (Maybe Interface)
-> (TCErr -> TCM (Maybe Interface)) -> TCM (Maybe Interface)
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` TCErr -> TCM (Maybe Interface)
forall (m :: * -> *) a.
(MonadDebug m, MonadError TCErr m) =>
TCErr -> m (Maybe a)
handler
  where
    handler :: TCErr -> m (Maybe a)
handler TCErr
e = case TCErr
e of
      IOException TCState
_ Range
_ IOException
e -> do
        String -> Int -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"" Int
0 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"IO exception: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ IOException -> String
forall a. Show a => a -> String
show IOException
e
        Maybe a -> m (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
_ -> TCErr -> m (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 -> ShowS
forall a. [a] -> [a] -> [a]
++ String
fp String -> ShowS
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
    --     }
    -- Andreas, 2016-02-02 this causes issue #1804, so don't do it:
    -- i <- return $
    --   i { iInsideScope  = removePrivates $ iInsideScope 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 -> ShowS
forall a. [a] -> [a] -> [a]
++ Hash -> String
forall a. Show a => a -> String
show (Interface -> Hash
iFullHash Interface
i) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
    ByteString
i' <- String -> Interface -> TCM ByteString
encodeFile String
fp Interface
i
    String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface.write" Int
5 String
"Wrote interface file."
    Maybe Interface
i <-
#if __GLASGOW_HASKELL__ >= 804
      Account Phase -> TCM (Maybe Interface) -> TCM (Maybe Interface)
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Deserialization] (ByteString -> TCM (Maybe Interface)
forall a. EmbPrj a => ByteString -> TCM (Maybe a)
decode ByteString
i')
#else
      return (Just i)
#endif
    case Maybe Interface
i of
      Just Interface
i  -> Interface -> TCMT IO Interface
forall (m :: * -> *) a. Monad m => a -> m a
return Interface
i
      Maybe Interface
Nothing -> TCMT IO Interface
forall a. HasCallStack => a
__IMPOSSIBLE__
  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 -> ShowS
forall a. [a] -> [a] -> [a]
++ String
fp String -> ShowS
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

removePrivates :: ScopeInfo -> ScopeInfo
removePrivates :: ScopeInfo -> ScopeInfo
removePrivates = Lens' (Map ModuleName Scope) ScopeInfo
-> LensMap (Map ModuleName Scope) ScopeInfo
forall i o. Lens' i o -> LensMap i o
over Lens' (Map ModuleName Scope) ScopeInfo
scopeModules LensMap (Map ModuleName Scope) ScopeInfo
-> LensMap (Map ModuleName Scope) ScopeInfo
forall a b. (a -> b) -> a -> b
$ (Scope -> Scope) -> Map ModuleName Scope -> Map ModuleName Scope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Scope -> Scope
restrictPrivate

concreteOptionsToOptionPragmas :: [C.Pragma] -> TCM [OptionsPragma]
concreteOptionsToOptionPragmas :: [Pragma] -> TCM [[String]]
concreteOptionsToOptionPragmas [Pragma]
p = do
  [Pragma]
pragmas <- [[Pragma]] -> [Pragma]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Pragma]] -> [Pragma]) -> TCMT IO [[Pragma]] -> TCMT IO [Pragma]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pragma] -> TCMT IO [[Pragma]]
forall c a. ToAbstract c a => c -> ScopeM a
concreteToAbstract_ [Pragma]
p
  -- identity for top-level pragmas at the moment
  let getOptions :: Pragma -> Maybe [String]
getOptions (A.OptionsPragma [String]
opts) = [String] -> Maybe [String]
forall a. a -> Maybe a
Just [String]
opts
      getOptions Pragma
_                      = Maybe [String]
forall a. Maybe a
Nothing
  [[String]] -> TCM [[String]]
forall (m :: * -> *) a. Monad m => a -> m a
return ([[String]] -> TCM [[String]]) -> [[String]] -> TCM [[String]]
forall a b. (a -> b) -> a -> b
$ (Pragma -> Maybe [String]) -> [Pragma] -> [[String]]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Pragma -> Maybe [String]
getOptions [Pragma]
pragmas

-- | 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
  :: SourceFile            -- ^ The file to type check.
  -> C.TopLevelModuleName  -- ^ The expected module name.
  -> MainInterface         -- ^ Are we dealing with the main module?
  -> Maybe SourceInfo      -- ^ Optional information about the source code.
  -> TCM (Interface, MaybeWarnings)
createInterface :: SourceFile
-> TopLevelModuleName
-> MainInterface
-> Maybe SourceInfo
-> TCM (Interface, MaybeWarnings)
createInterface SourceFile
file TopLevelModuleName
mname MainInterface
isMain Maybe SourceInfo
msi =
  Account Phase
-> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [TopLevelModuleName -> Phase
Bench.TopModule TopLevelModuleName
mname] (TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings))
-> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a b. (a -> b) -> a -> b
$
  (TCEnv -> TCEnv)
-> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
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 (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings))
-> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
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
5 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$
      String
"Creating interface for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow TopLevelModuleName
mname String -> ShowS
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
      [TopLevelModuleName]
visited <- Map TopLevelModuleName ModuleInfo -> [TopLevelModuleName]
forall k a. Map k a -> [k]
Map.keys (Map TopLevelModuleName ModuleInfo -> [TopLevelModuleName])
-> TCMT IO (Map TopLevelModuleName ModuleInfo)
-> TCMT IO [TopLevelModuleName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Map TopLevelModuleName ModuleInfo)
getVisitedModules
      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 -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
", " ((TopLevelModuleName -> String) -> [TopLevelModuleName] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map TopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow [TopLevelModuleName]
visited)

    (Text
source, FileType
fileType, ([Pragma]
pragmas, [Declaration]
top)) <- do
      SourceInfo
si <- case Maybe SourceInfo
msi of
        Maybe SourceInfo
Nothing -> SourceFile -> TCM SourceInfo
sourceInfo SourceFile
file
        Just SourceInfo
si -> SourceInfo -> TCM SourceInfo
forall (m :: * -> *) a. Monad m => a -> m a
return SourceInfo
si
      case SourceInfo
si of
        SourceInfo {Module
Text
FileType
TopLevelModuleName
siModuleName :: TopLevelModuleName
siModule :: Module
siFileType :: FileType
siSource :: Text
siModuleName :: SourceInfo -> TopLevelModuleName
siModule :: SourceInfo -> Module
siFileType :: SourceInfo -> FileType
siSource :: SourceInfo -> Text
..} -> (Text, FileType, Module) -> TCMT IO (Text, FileType, Module)
forall (m :: * -> *) a. Monad m => a -> m a
return (Text
siSource, FileType
siFileType, Module
siModule)

    ModuleToSource
modFile       <- Lens' ModuleToSource TCState -> TCMT IO ModuleToSource
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' ModuleToSource TCState
stModuleToSource
    HighlightingInfo
fileTokenInfo <- Account Phase
-> TCMT IO HighlightingInfo -> TCMT IO HighlightingInfo
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [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
                         (SourceFile -> AbsolutePath
srcFilePath SourceFile
file) (Text -> String
T.unpack Text
source)
    Lens' HighlightingInfo TCState
stTokens Lens' HighlightingInfo TCState -> HighlightingInfo -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` HighlightingInfo
fileTokenInfo

    [[String]]
options <- [Pragma] -> TCM [[String]]
concreteOptionsToOptionPragmas [Pragma]
pragmas
    ([String] -> TCM ()) -> [[String]] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [String] -> TCM ()
setOptionsFromPragma [[String]]
options


    -- 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 Phase -> TCMT IO TopLevelInfo -> TCMT IO TopLevelInfo
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Scoping] (TCMT IO TopLevelInfo -> TCMT IO TopLevelInfo)
-> TCMT IO TopLevelInfo -> TCMT IO TopLevelInfo
forall a b. (a -> b) -> a -> b
$
      TopLevel [Declaration] -> TCMT IO TopLevelInfo
forall c a. ToAbstract c a => c -> ScopeM a
concreteToAbstract_ (AbsolutePath
-> TopLevelModuleName -> [Declaration] -> TopLevel [Declaration]
forall a. AbsolutePath -> TopLevelModuleName -> a -> TopLevel a
TopLevel (SourceFile -> AbsolutePath
srcFilePath SourceFile
file) TopLevelModuleName
mname [Declaration]
top)
    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 Phase -> TCM () -> TCM ()
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [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 :: * -> *).
MonadTCM tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
forall (tcm :: * -> *).
(MonadTCM tcm, ReadTCState tcm) =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> tcm ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting HighlightingInfo
fileTokenInfo
      let onlyScope :: Bool
onlyScope = MainInterface
isMain MainInterface -> MainInterface -> Bool
forall a. Eq a => a -> a -> Bool
== Mode -> MainInterface
MainInterface Mode
ScopeCheck
      HighlightingLevel -> Bool -> TCM () -> TCM ()
forall (tcm :: * -> *).
MonadTCM 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 :: * -> *). (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 -> ShowS
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

    case MainInterface
isMain of
      MainInterface Mode
ScopeCheck -> 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
      MainInterface
_ -> 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 Phase -> TCM () -> TCM ()
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [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 Phase -> TCM () -> TCM ()
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [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 :: * -> *).
MonadTCM tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
forall (tcm :: * -> *).
(MonadTCM tcm, ReadTCState tcm) =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> tcm ()
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]
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 -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"import.iface.create" Int
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
        TCM Doc
"collected warnings: " TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> [TCWarning] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [TCWarning]
warnings
      [TCWarning]
unsolved <- TCMT IO [TCWarning]
getAllUnsolved
      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 -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"import.iface.create" Int
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
        TCM Doc
"collected unsolved: " TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> [TCWarning] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [TCWarning]
unsolved
      let warningInfo :: HighlightingInfo
warningInfo = File -> HighlightingInfo
compress (File -> HighlightingInfo) -> File -> HighlightingInfo
forall a b. (a -> b) -> a -> b
$ (TCWarning -> File) -> [TCWarning] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap TCWarning -> File
warningHighlighting ([TCWarning] -> File) -> [TCWarning] -> File
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

      TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (CommandLineOptions -> Bool
optGenerateVimFile (CommandLineOptions -> Bool)
-> TCMT IO CommandLineOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        -- Generate Vim file.
        ScopeInfo -> TCM () -> TCM ()
forall (m :: * -> *) a. ReadTCState m => ScopeInfo -> m a -> m a
withScope_ ScopeInfo
scope (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ 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
$ SourceFile -> AbsolutePath
srcFilePath (SourceFile -> AbsolutePath) -> SourceFile -> AbsolutePath
forall a b. (a -> b) -> a -> b
$ SourceFile
file
    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 -> ShowS
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 :: * -> *).
MonadTCM 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
allowUnsolved <- PragmaOptions -> Bool
optAllowUnsolved (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
    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).
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
allowUnsolved (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 Phase -> TCMT IO Interface -> TCMT IO Interface
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Serialization, Phase
Bench.BuildInterface] (TCMT IO Interface -> TCMT IO Interface)
-> TCMT IO Interface -> TCMT IO Interface
forall a b. (a -> b) -> a -> b
$
      Text -> FileType -> TopLevelInfo -> [[String]] -> TCMT IO Interface
buildInterface Text
source FileType
fileType TopLevelInfo
topLevel [[String]]
options

    String -> Int -> [String] -> TCM ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Int -> a -> m ()
reportS String
"tc.top" Int
101 ([String] -> TCM ()) -> [String] -> TCM ()
forall a b. (a -> b) -> a -> b
$
      String
"Signature:" String -> [String] -> [String]
forall a. a -> [a] -> [a]
:
      [ [String] -> String
unlines
          [ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
x
          , String
"  type: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show (Definition -> Type
defType Definition
def)
          , String
"  def:  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe CompiledClauses -> String
forall a. Show a => a -> String
show Maybe CompiledClauses
cc
          ]
      | (QName
x, 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."

    MaybeWarnings
mallWarnings <- MainInterface -> WhichWarnings -> TCM MaybeWarnings
getMaybeWarnings' 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
i <- case (MaybeWarnings
mallWarnings, MainInterface
isMain) of
      (SomeWarnings [TCWarning]
allWarnings, 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
      (MaybeWarnings
_, 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
      (MaybeWarnings, MainInterface)
_ -> Account Phase -> TCMT IO Interface -> TCMT IO Interface
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [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
        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 (or skipped) writing to interface file."

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

    (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings))
-> (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a b. (a -> b) -> a -> b
$ (Interface -> Interface)
-> (Interface, MaybeWarnings) -> (Interface, MaybeWarnings)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first Interface -> Interface
constructIScope (Interface
i, MaybeWarnings
mallWarnings)

getUniqueMetasRanges :: [MetaId] -> TCM [Range]
getUniqueMetasRanges :: [MetaId] -> TCM [Range]
getUniqueMetasRanges = ([Range] -> [Range]) -> TCM [Range] -> TCM [Range]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Range -> Range) -> [Range] -> [Range]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn Range -> Range
forall a. a -> a
id) (TCM [Range] -> TCM [Range])
-> ([MetaId] -> TCM [Range]) -> [MetaId] -> TCM [Range]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaId -> TCMT IO Range) -> [MetaId] -> TCM [Range]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM MetaId -> TCMT IO Range
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Range
getMetaRange

getUnsolvedMetas :: TCM [Range]
getUnsolvedMetas :: TCM [Range]
getUnsolvedMetas = do
  [MetaId]
openMetas            <- TCMT IO [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas
  [MetaId]
interactionMetas     <- TCMT IO [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getInteractionMetas
  [MetaId] -> TCM [Range]
getUniqueMetasRanges ([MetaId]
openMetas [MetaId] -> [MetaId] -> [MetaId]
forall a. Eq a => [a] -> [a] -> [a]
List.\\ [MetaId]
interactionMetas)

getAllUnsolved :: TCM [TCWarning]
getAllUnsolved :: TCMT IO [TCWarning]
getAllUnsolved = do
  [Range]
unsolvedInteractions <- [MetaId] -> TCM [Range]
getUniqueMetasRanges ([MetaId] -> TCM [Range]) -> TCMT IO [MetaId] -> TCM [Range]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getInteractionMetas
  Constraints
unsolvedConstraints  <- TCMT IO Constraints
forall (m :: * -> *). ReadTCState m => m Constraints
getAllConstraints
  [Range]
unsolvedMetas        <- TCM [Range]
getUnsolvedMetas

  let checkNonEmpty :: (a -> a) -> a -> f a
checkNonEmpty a -> a
c a
rs = a -> a
c a
rs a -> f () -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> f ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ a -> Bool
forall a. Null a => a -> Bool
null a
rs)

  (Warning -> TCMT IO TCWarning) -> [Warning] -> TCMT IO [TCWarning]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Warning -> TCMT IO TCWarning
forall (m :: * -> *). MonadWarning m => Warning -> m TCWarning
warning_ ([Warning] -> TCMT IO [TCWarning])
-> [Warning] -> TCMT IO [TCWarning]
forall a b. (a -> b) -> a -> b
$ [Maybe Warning] -> [Warning]
forall a. [Maybe a] -> [a]
catMaybes
                [ ([Range] -> Warning) -> [Range] -> Maybe Warning
forall (f :: * -> *) a a.
(Alternative f, Null a) =>
(a -> a) -> a -> f a
checkNonEmpty [Range] -> Warning
UnsolvedInteractionMetas [Range]
unsolvedInteractions
                , ([Range] -> Warning) -> [Range] -> Maybe Warning
forall (f :: * -> *) a a.
(Alternative f, Null a) =>
(a -> a) -> a -> f a
checkNonEmpty [Range] -> Warning
UnsolvedMetaVariables    [Range]
unsolvedMetas
                , (Constraints -> Warning) -> Constraints -> Maybe Warning
forall (f :: * -> *) a a.
(Alternative f, Null a) =>
(a -> a) -> a -> f a
checkNonEmpty Constraints -> Warning
UnsolvedConstraints      Constraints
unsolvedConstraints ]


-- | Collect all warnings that have accumulated in the state.

getAllWarnings :: WhichWarnings -> TCM [TCWarning]
getAllWarnings :: WhichWarnings -> TCMT IO [TCWarning]
getAllWarnings = MainInterface -> WhichWarnings -> TCMT IO [TCWarning]
getAllWarnings' MainInterface
NotMainInterface

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

getAllWarnings' :: MainInterface -> WhichWarnings -> TCM [TCWarning]
getAllWarnings' :: MainInterface -> WhichWarnings -> TCMT IO [TCWarning]
getAllWarnings' MainInterface
isMain WhichWarnings
ww = do
  [TCWarning]
unsolved            <- TCMT IO [TCWarning]
getAllUnsolved
  [TCWarning]
collectedTCWarnings <- Lens' [TCWarning] TCState -> TCMT IO [TCWarning]
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' [TCWarning] TCState
stTCWarnings

  let showWarn :: Warning -> Bool
showWarn Warning
w = Warning -> WhichWarnings
classifyWarning Warning
w WhichWarnings -> WhichWarnings -> Bool
forall a. Ord a => a -> a -> Bool
<= WhichWarnings
ww Bool -> Bool -> Bool
&&
                    Bool -> Bool
not ([TCWarning] -> Bool
forall a. Null a => a -> Bool
null [TCWarning]
unsolved Bool -> Bool -> Bool
&& Warning -> Bool
onlyShowIfUnsolved Warning
w)

  ([TCWarning] -> [TCWarning])
-> TCMT IO [TCWarning] -> TCMT IO [TCWarning]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
forall a. (a -> Bool) -> [a] -> [a]
filter (Warning -> Bool
showWarn (Warning -> Bool) -> (TCWarning -> Warning) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning))
    (TCMT IO [TCWarning] -> TCMT IO [TCWarning])
-> TCMT IO [TCWarning] -> TCMT IO [TCWarning]
forall a b. (a -> b) -> a -> b
$ MainInterface -> [TCWarning] -> TCMT IO [TCWarning]
applyFlagsToTCWarnings' MainInterface
isMain ([TCWarning] -> TCMT IO [TCWarning])
-> [TCWarning] -> TCMT IO [TCWarning]
forall a b. (a -> b) -> a -> b
$ [TCWarning] -> [TCWarning]
forall a. [a] -> [a]
reverse
    ([TCWarning] -> [TCWarning]) -> [TCWarning] -> [TCWarning]
forall a b. (a -> b) -> a -> b
$ [TCWarning]
unsolved [TCWarning] -> [TCWarning] -> [TCWarning]
forall a. [a] -> [a] -> [a]
++ [TCWarning]
collectedTCWarnings

getMaybeWarnings :: WhichWarnings -> TCM MaybeWarnings
getMaybeWarnings :: WhichWarnings -> TCM MaybeWarnings
getMaybeWarnings = MainInterface -> WhichWarnings -> TCM MaybeWarnings
getMaybeWarnings' MainInterface
NotMainInterface

getMaybeWarnings' :: MainInterface -> WhichWarnings -> TCM MaybeWarnings
getMaybeWarnings' :: MainInterface -> WhichWarnings -> TCM MaybeWarnings
getMaybeWarnings' MainInterface
isMain WhichWarnings
ww = do
  [TCWarning]
allWarnings <- MainInterface -> WhichWarnings -> TCMT IO [TCWarning]
getAllWarnings' MainInterface
isMain WhichWarnings
ww
  MaybeWarnings -> TCM MaybeWarnings
forall (m :: * -> *) a. Monad m => a -> m a
return (MaybeWarnings -> TCM MaybeWarnings)
-> MaybeWarnings -> TCM MaybeWarnings
forall a b. (a -> b) -> a -> b
$ if [TCWarning] -> Bool
forall a. Null a => a -> Bool
null [TCWarning]
allWarnings
    -- Andreas, issue 964: not checking null interactionPoints
    -- anymore; we want to serialize with open interaction points now!
           then MaybeWarnings
forall a. MaybeWarnings' a
NoWarnings
           else [TCWarning] -> MaybeWarnings
forall a. a -> MaybeWarnings' a
SomeWarnings [TCWarning]
allWarnings

getAllWarningsOfTCErr :: TCErr -> TCM [TCWarning]
getAllWarningsOfTCErr :: TCErr -> TCMT IO [TCWarning]
getAllWarningsOfTCErr TCErr
err = case TCErr
err of
  TypeError TCState
tcst Closure TypeError
cls -> case Closure TypeError -> TypeError
forall a. Closure a -> a
clValue Closure TypeError
cls of
    NonFatalErrors{} -> [TCWarning] -> TCMT IO [TCWarning]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    TypeError
_ -> TCMT IO [TCWarning] -> TCMT IO [TCWarning]
forall a. TCM a -> TCM a
localTCState (TCMT IO [TCWarning] -> TCMT IO [TCWarning])
-> TCMT IO [TCWarning] -> TCMT IO [TCWarning]
forall a b. (a -> b) -> a -> b
$ do
      TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
tcst
      [TCWarning]
ws <- WhichWarnings -> TCMT IO [TCWarning]
getAllWarnings WhichWarnings
AllWarnings
      -- We filter out the unsolved(Metas/Constraints) to stay
      -- true to the previous error messages.
      [TCWarning] -> TCMT IO [TCWarning]
forall (m :: * -> *) a. Monad m => a -> m a
return ([TCWarning] -> TCMT IO [TCWarning])
-> [TCWarning] -> TCMT IO [TCWarning]
forall a b. (a -> b) -> a -> b
$ (TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (TCWarning -> Bool) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Warning -> Bool
isUnsolvedWarning (Warning -> Bool) -> (TCWarning -> Warning) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning) [TCWarning]
ws
  TCErr
_ -> [TCWarning] -> TCMT IO [TCWarning]
forall (m :: * -> *) a. Monad m => a -> m a
return []

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

constructIScope :: Interface -> Interface
constructIScope :: Interface -> Interface
constructIScope Interface
i = Account Phase -> Interface -> Interface
forall a. Account Phase -> 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
  :: Text
     -- ^ Source code.
  -> FileType
     -- ^ Agda file? Literate Agda file?
  -> TopLevelInfo
     -- ^ 'TopLevelInfo' for the current module.
  -> [OptionsPragma]
     -- ^ Options set in @OPTIONS@ pragmas.
  -> TCM Interface
buildInterface :: Text -> FileType -> TopLevelInfo -> [[String]] -> TCMT IO Interface
buildInterface Text
source FileType
fileType TopLevelInfo
topLevel [[String]]
pragmas = do
    String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"import.iface" Int
5 String
"Building interface..."
    let m :: ModuleName
m = TopLevelInfo -> ModuleName
topLevelModuleName TopLevelInfo
topLevel
    ScopeInfo
scope'  <- TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
    let scope :: ScopeInfo
scope = Lens' ModuleName ScopeInfo -> LensSet ModuleName ScopeInfo
forall i o. Lens' i o -> LensSet i o
set Lens' ModuleName ScopeInfo
scopeCurrent ModuleName
m ScopeInfo
scope'
    -- 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).
    BuiltinThings PrimFun
builtin     <- Lens' (BuiltinThings PrimFun) TCState
-> TCMT IO (BuiltinThings PrimFun)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (BuiltinThings 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
display <- ([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
display (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 String
userwarns      <- Lens' (Map QName String) TCState -> TCMT IO (Map QName String)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map QName String) TCState
stLocalUserWarnings
    Maybe String
importwarn     <- Lens' (Maybe String) TCState -> TCMT IO (Maybe String)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Maybe String) 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))
-> BuiltinThings 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) BuiltinThings PrimFun
builtin
    [TCWarning]
warnings <- WhichWarnings -> TCMT IO [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"
    Interface
i <- Interface -> TCMT IO Interface
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Interface :: Hash
-> Text
-> FileType
-> [(ModuleName, Hash)]
-> ModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> DisplayForms
-> Map QName String
-> Maybe String
-> Map String (Builtin (String, QName))
-> Map String [ForeignCode]
-> HighlightingInfo
-> [[String]]
-> 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
m
      , 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 String
iUserWarnings    = Map QName String
userwarns
      , iImportWarning :: Maybe String
iImportWarning   = Maybe String
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
      , iPragmaOptions :: [[String]]
iPragmaOptions   = [[String]]
pragmas
      , 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 :: AbsolutePath -> TCM (Maybe (Hash, Hash))
getInterfaceFileHashes :: AbsolutePath -> TCMT IO (Maybe (Hash, Hash))
getInterfaceFileHashes AbsolutePath
fp = MaybeT TCM (Hash, Hash) -> TCMT IO (Maybe (Hash, Hash))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT TCM (Hash, Hash) -> TCMT IO (Maybe (Hash, Hash)))
-> MaybeT TCM (Hash, Hash) -> TCMT IO (Maybe (Hash, Hash))
forall a b. (a -> b) -> a -> b
$ do
  InterfaceFile
mifile <- TCMT IO (Maybe InterfaceFile) -> MaybeT TCM InterfaceFile
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe InterfaceFile) -> MaybeT TCM InterfaceFile)
-> TCMT IO (Maybe InterfaceFile) -> MaybeT TCM InterfaceFile
forall a b. (a -> b) -> a -> b
$ IO (Maybe InterfaceFile) -> TCMT IO (Maybe InterfaceFile)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe InterfaceFile) -> TCMT IO (Maybe InterfaceFile))
-> IO (Maybe InterfaceFile) -> TCMT IO (Maybe InterfaceFile)
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> IO (Maybe InterfaceFile)
mkInterfaceFile AbsolutePath
fp
  TCMT IO (Maybe (Hash, Hash)) -> MaybeT TCM (Hash, Hash)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe (Hash, Hash)) -> MaybeT TCM (Hash, Hash))
-> TCMT IO (Maybe (Hash, Hash)) -> MaybeT TCM (Hash, Hash)
forall a b. (a -> b) -> a -> b
$ InterfaceFile -> TCMT IO (Maybe (Hash, Hash))
getInterfaceFileHashes' InterfaceFile
mifile

getInterfaceFileHashes' :: InterfaceFile -> TCM (Maybe (Hash, Hash))
getInterfaceFileHashes' :: InterfaceFile -> TCMT 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) <- 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
ifile
  let hs :: Maybe (Hash, Hash)
hs = ByteString -> Maybe (Hash, Hash)
decodeHashes ByteString
s
  IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ 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) -> TCMT 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
<$> ModuleName -> TCMT IO Interface
getInterface ModuleName
m

-- | True if the first file is newer than the second file. If a file doesn't
-- exist it is considered to be infinitely old.
isNewerThan :: FilePath -> FilePath -> IO Bool
isNewerThan :: String -> String -> IO Bool
isNewerThan String
new String
old = do
    Bool
newExist <- String -> IO Bool
doesFileExist String
new
    Bool
oldExist <- String -> IO Bool
doesFileExist String
old
    if Bool -> Bool
not (Bool
newExist Bool -> Bool -> Bool
&& Bool
oldExist)
        then Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
newExist
        else do
            UTCTime
newT <- String -> IO UTCTime
getModificationTime String
new
            UTCTime
oldT <- String -> IO UTCTime
getModificationTime String
old
            Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ UTCTime
newT UTCTime -> UTCTime -> Bool
forall a. Ord a => a -> a -> Bool
>= UTCTime
oldT