summaryrefslogtreecommitdiff
path: root/src/full/Agda/Interaction/Imports.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Interaction/Imports.hs')
-rw-r--r--src/full/Agda/Interaction/Imports.hs560
1 files changed, 357 insertions, 203 deletions
diff --git a/src/full/Agda/Interaction/Imports.hs b/src/full/Agda/Interaction/Imports.hs
index 9dbc00a..eca6614 100644
--- a/src/full/Agda/Interaction/Imports.hs
+++ b/src/full/Agda/Interaction/Imports.hs
@@ -1,9 +1,4 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE TupleSections #-}
-
-#if __GLASGOW_HASKELL__ >= 710
-{-# LANGUAGE FlexibleContexts #-}
-#endif
+{-# LANGUAGE CPP #-}
{-| This module deals with finding imported modules and loading their
interface files.
@@ -16,8 +11,14 @@ import Control.Arrow
import Control.DeepSeq
import Control.Monad.Reader
import Control.Monad.State
+import Control.Monad.Trans.Maybe
import qualified Control.Exception as E
+#if __GLASGOW_HASKELL__ <= 708
+import Data.Foldable ( Foldable )
+import Data.Traversable ( Traversable, traverse )
+#endif
+
import Data.Function (on)
import qualified Data.Map as Map
import qualified Data.List as List
@@ -47,10 +48,12 @@ import Agda.Syntax.Internal
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Reduce
+import Agda.TypeChecking.MetaVars ( openMetasToPostulates )
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Serialise
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Primitive
+import Agda.TypeChecking.Pretty as P
import Agda.TypeChecking.Rewriting (killCtxId)
import Agda.TypeChecking.DeadCode
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
@@ -68,6 +71,7 @@ import Agda.Interaction.Highlighting.Vim
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.FileName
import Agda.Utils.Lens
+import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.IO.Binary
@@ -123,13 +127,13 @@ addImportedThings ::
Set String -> -- UHC backend imports
A.PatternSynDefns -> DisplayForms -> TCM ()
addImportedThings isig ibuiltin hsImports hsImportsUHC patsyns display = do
- stImports %= \imp -> unionSignatures [imp, over sigRewriteRules killCtxId isig]
- stImportedBuiltins %= \imp -> Map.union imp ibuiltin
- stHaskellImports %= \imp -> Set.union imp hsImports
- stHaskellImportsUHC %= \imp -> Set.union imp hsImportsUHC
- stPatternSynImports %= \imp -> Map.union imp patsyns
- stImportedDisplayForms %= \imp -> HMap.unionWith (++) imp display
- addSignatureInstances isig
+ stImports %= \ imp -> unionSignatures [imp, over sigRewriteRules killCtxId isig]
+ stImportedBuiltins %= \ imp -> Map.union imp ibuiltin
+ stHaskellImports %= \ imp -> Set.union imp hsImports
+ stHaskellImportsUHC %= \ imp -> Set.union imp hsImportsUHC
+ stPatternSynImports %= \ imp -> Map.union imp patsyns
+ stImportedDisplayForms %= \ imp -> HMap.unionWith (++) imp display
+ addImportedInstances isig
-- | Scope checks the given module. A proper version of the module
-- name (with correct definition sites) is returned.
@@ -149,11 +153,23 @@ scopeCheckImport x = do
let s = iScope i
return (iModuleName i `withRangesOfQ` mnameToConcrete x, s)
-data MaybeWarnings = NoWarnings | SomeWarnings Warnings
+data MaybeWarnings' a = NoWarnings | SomeWarnings a
+ deriving (Functor, Foldable, Traversable)
+type MaybeWarnings = MaybeWarnings' [TCWarning]
+
+applyFlagsToMaybeWarnings :: IgnoreFlags -> MaybeWarnings -> TCM MaybeWarnings
+applyFlagsToMaybeWarnings r mw = do
+ w' <- traverse (applyFlagsToTCWarnings r) mw
+ return $ if null w' then NoWarnings else w'
+
+instance Null a => Null (MaybeWarnings' a) where
+ empty = NoWarnings
+ null mws = case mws of
+ NoWarnings -> True
+ SomeWarnings ws -> null ws
hasWarnings :: MaybeWarnings -> Bool
-hasWarnings NoWarnings = False
-hasWarnings SomeWarnings{} = True
+hasWarnings = not . null
-- | If the module has already been visited (without warnings), then
-- its interface is returned directly. Otherwise the computation is
@@ -232,8 +248,13 @@ getInterface_ :: C.TopLevelModuleName -> TCM Interface
getInterface_ x = do
(i, wt) <- getInterface' x NotMainInterface
case wt of
- SomeWarnings w -> warningsToError w
+ SomeWarnings w -> tcWarningsToError (filter (notIM . tcWarning) w)
NoWarnings -> return i
+ -- filter out unsolved interaction points for imported module so
+ -- that we get the right error message (see test case Fail/Issue1296)
+ where notIM UnsolvedInteractionMetas{} = False
+ notIM _ = True
+
-- | A more precise variant of 'getInterface'. If warnings are
-- encountered then they are returned instead of being turned into
@@ -244,6 +265,7 @@ getInterface'
-> MainInterface
-- ^ If type checking is necessary,
-- should all state changes inflicted by 'createInterface' be preserved?
+ -- Yes, if we are the 'MainInterface'. No, if we are 'NotMainInterface'.
-> TCM (Interface, MaybeWarnings)
getInterface' x isMain = do
withIncreasedModuleNestingLevel $ do
@@ -261,8 +283,9 @@ getInterface' x isMain = do
uptodate <- Bench.billTo [Bench.Import] $ do
ignore <- ignoreInterfaces
- cached <- isCached file -- if it's cached ignoreInterfaces has no effect
- -- to avoid typechecking a file more than once
+ cached <- runMaybeT $ isCached x file
+ -- If it's cached ignoreInterfaces has no effect;
+ -- to avoid typechecking a file more than once.
sourceH <- liftIO $ hashFile file
ifaceH <-
case cached of
@@ -282,7 +305,9 @@ getInterface' x isMain = do
-- let maySkip = isMain == NotMainInterface
-- Andreas, 2015-07-13: Serialize iInsideScope again.
let maySkip = True
- if uptodate && maySkip then skip file else typeCheckThe file
+ if uptodate && maySkip
+ then getStoredInterface x file includeStateChanges
+ else typeCheck x file includeStateChanges
-- Ensure that the given module name matches the one in the file.
let topLevelName = toTopLevelModuleName $ iModuleName i
@@ -312,158 +337,219 @@ getInterface' x isMain = do
where
includeStateChanges = isMain == MainInterface
- isCached file = do
- let ifile = filePath $ toIFile file
- exist <- liftIO $ doesFileExistCaseSensitive ifile
- if not exist
- then return Nothing
- else do
- h <- fmap snd <$> getInterfaceFileHashes ifile
- mm <- getDecodedModule x
- return $ case mm of
- Just mi | Just (iFullHash mi) == h -> Just mi
- _ -> Nothing
-
- -- Formats the "Checking", "Finished" and "Skipping" messages.
- chaseMsg kind file = do
- nesting <- envModuleNestingLevel <$> ask
- let s = genericReplicate nesting ' ' ++ kind ++
- " " ++ prettyShow x ++
- case file of
- Nothing -> "."
- Just f -> " (" ++ f ++ ")."
- reportSLn "import.chase" 1 s
-
- skip file = do
- -- 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.
- let ifile = filePath $ toIFile file
- h <- fmap snd <$> getInterfaceFileHashes ifile
- mm <- getDecodedModule x
- (cached, mi) <- Bench.billTo [Bench.Deserialization] $ case mm of
- Just mi ->
- if Just (iFullHash mi) /= h
- then do dropDecodedModule x
- reportSLn "import.iface" 50 $ " cached hash = " ++ show (iFullHash mi)
- reportSLn "import.iface" 50 $ " stored hash = " ++ show h
- reportSLn "import.iface" 5 $ " file is newer, re-reading " ++ ifile
- (False,) <$> readInterface ifile
- else do reportSLn "import.iface" 5 $ " using stored version of " ++ ifile
- return (True, Just mi)
- Nothing -> do
- reportSLn "import.iface" 5 $ " no stored version, reading " ++ ifile
- (False,) <$> readInterface ifile
-
- -- Check that it's the right version
- case mi of
- Nothing -> do
- reportSLn "import.iface" 5 $ " bad interface, re-type checking"
- typeCheckThe file
- Just i -> do
-
- reportSLn "import.iface" 5 $ " imports: " ++ show (iImportedModules i)
-
- hs <- map iFullHash <$> mapM getInterface (map fst $ iImportedModules i)
-
- -- If any of the imports are newer we need to retype check
- if hs /= map snd (iImportedModules i)
- then do
- -- liftIO close -- Close the interface file. See above.
- typeCheckThe file
- else do
- unless cached $ chaseMsg "Skipping" (Just ifile)
- -- We set the pragma options of the skipped file here,
- -- because if the top-level file is skipped we want the
- -- pragmas to apply to interactive commands in the UI.
- mapM_ setOptionsFromPragma (iPragmaOptions i)
- return (False, (i, NoWarnings))
-
- typeCheckThe file = do
- unless includeStateChanges cleanCachedLog
- let withMsgs = bracket_
- (chaseMsg "Checking" $ Just $ filePath file)
- (const $ chaseMsg "Finished" Nothing)
-
- -- Do the type checking.
-
- if includeStateChanges then do
- r <- withMsgs $ createInterface file x
-
- -- Merge the signature with the signature for imported
- -- things.
- sig <- getSignature
- patsyns <- getPatternSyns
- display <- use stImportsDisplayForms
- addImportedThings sig Map.empty Set.empty Set.empty patsyns display
- setSignature emptySignature
- setPatternSyns Map.empty
-
- return (True, r)
- else do
- ms <- getImportPath
- nesting <- asks envModuleNestingLevel
- range <- asks envRange
- call <- asks envCall
- mf <- use stModuleToSource
- vs <- getVisitedModules
- ds <- getDecodedModules
- opts <- stPersistentOptions . stPersistentState <$> get
- isig <- getImportedSignature
- ibuiltin <- use stImportedBuiltins
- display <- use stImportsDisplayForms
- ipatsyns <- getPatternSynImports
- ho <- getInteractionOutputCallback
- -- Every interface is treated in isolation. Note: Changes
- -- to stDecodedModules are not preserved if an error is
- -- encountered in an imported module.
- -- Andreas, 2014-03-23: freshTCM spawns a new TCM computation
- -- with initial state and environment
- -- but on the same Benchmark accounts.
- r <- freshTCM $
- withImportPath ms $
- local (\e -> e { envModuleNestingLevel = nesting
- -- Andreas, 2014-08-18:
- -- Preserve the range of import statement
- -- for reporting termination errors in
- -- imported modules:
- , envRange = range
- , envCall = call
- }) $ do
- setDecodedModules ds
- setCommandLineOptions opts
- setInteractionOutputCallback ho
- stModuleToSource .= mf
- setVisitedModules vs
- addImportedThings isig ibuiltin Set.empty Set.empty ipatsyns display
-
- r <- withMsgs $ createInterface file x
- mf <- use stModuleToSource
- ds <- getDecodedModules
- return (r, do
- stModuleToSource .= mf
- setDecodedModules ds
- case r of
- (i, NoWarnings) -> storeDecodedModule i
- _ -> return ()
- )
-
- case r of
- Left err -> throwError err
- Right (r, update) -> do
- update
- case r of
- (_, 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.
- skip file
- _ -> return (False, r)
-
--- | Print the highlighting information contained in the given
--- interface.
+-- | 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.
+ -> AbsolutePath
+ -- ^ File we process.
+ -> MaybeT TCM Interface
+
+isCached x file = do
+ let ifile = filePath $ toIFile file
+
+ -- Make sure the file exists in the case sensitive spelling.
+ guardM $ liftIO $ doesFileExistCaseSensitive ifile
+
+ -- Check that we have cached the module.
+ mi <- MaybeT $ getDecodedModule x
+
+ -- Check that the interface file exists and return its hash.
+ h <- MaybeT $ fmap snd <$> getInterfaceFileHashes ifile
+
+ -- Make sure the hashes match.
+ guard $ iFullHash mi == h
+
+ return mi
+
+
+-- | Try to get the interface from interface file or cache.
+
+getStoredInterface
+ :: C.TopLevelModuleName
+ -- ^ Module name of file we process.
+ -> AbsolutePath
+ -- ^ File we process.
+ -> Bool
+ -- ^ If type checking is necessary,
+ -- should all state changes inflicted by 'createInterface' be preserved?
+ -- @True@, if we are the 'MainInterface'. @False@, if we are 'NotMainInterface'.
+ -> TCM (Bool, (Interface, MaybeWarnings))
+ -- ^ @Bool@ is: do we have to merge the interface?
+getStoredInterface x file includeStateChanges = do
+ -- If something goes wrong (interface outdated etc.)
+ -- we revert to fresh type checking.
+ let fallback = typeCheck x file includeStateChanges
+
+ -- 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.
+ let ifile = filePath $ toIFile file
+ h <- fmap snd <$> getInterfaceFileHashes ifile
+ mm <- getDecodedModule x
+ (cached, mi) <- Bench.billTo [Bench.Deserialization] $ case mm of
+ Just mi ->
+ if Just (iFullHash mi) /= h
+ then do
+ dropDecodedModule x
+ reportSLn "import.iface" 50 $ " cached hash = " ++ show (iFullHash mi)
+ reportSLn "import.iface" 50 $ " stored hash = " ++ show h
+ reportSLn "import.iface" 5 $ " file is newer, re-reading " ++ ifile
+ (False,) <$> readInterface ifile
+ else do
+ reportSLn "import.iface" 5 $ " using stored version of " ++ ifile
+ return (True, Just mi)
+ Nothing -> do
+ reportSLn "import.iface" 5 $ " no stored version, reading " ++ ifile
+ (False,) <$> readInterface ifile
+
+ -- Check that it's the right version
+ case mi of
+ Nothing -> do
+ reportSLn "import.iface" 5 $ " bad interface, re-type checking"
+ fallback
+ Just i -> do
+ reportSLn "import.iface" 5 $ " imports: " ++ show (iImportedModules i)
+
+ hs <- map iFullHash <$> mapM getInterface (map fst $ iImportedModules i)
+
+ -- If any of the imports are newer we need to retype check
+ if hs /= map snd (iImportedModules i)
+ then do
+ -- liftIO close -- Close the interface file. See above.
+ fallback
+ else do
+ unless cached $ chaseMsg "Skipping" x $ Just ifile
+ -- We set the pragma options of the skipped file here,
+ -- because if the top-level file is skipped we want the
+ -- pragmas to apply to interactive commands in the UI.
+ mapM_ setOptionsFromPragma (iPragmaOptions i)
+ return (False, (i, 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.
+ -> AbsolutePath
+ -- ^ File we process.
+ -> Bool
+ -- ^ If type checking is necessary,
+ -- should all state changes inflicted by 'createInterface' be preserved?
+ -- @True@, if we are the 'MainInterface'. @False@, if we are 'NotMainInterface'.
+ -> TCM (Bool, (Interface, MaybeWarnings))
+ -- ^ @Bool@ is: do we have to merge the interface?
+typeCheck x file includeStateChanges = do
+ unless includeStateChanges cleanCachedLog
+ let withMsgs = bracket_
+ (chaseMsg "Checking" x $ Just $ filePath file)
+ (const $ do ws <- getAllWarnings' AllWarnings RespectFlags
+ let (we, wa) = classifyWarnings ws
+ unless (null wa) $ reportSDoc "warning" 1
+ $ P.vcat $ P.prettyTCM <$> wa
+ unless (not $ null we) $ chaseMsg "Finished" x Nothing)
+
+ -- Do the type checking.
+
+ if includeStateChanges then do
+ r <- withMsgs $ createInterface file x includeStateChanges
+
+ -- Merge the signature with the signature for imported
+ -- things.
+ reportSLn "import.iface" 40 $ "Merging with state changes included."
+ sig <- getSignature
+ patsyns <- getPatternSyns
+ display <- use stImportsDisplayForms
+ addImportedThings sig Map.empty Set.empty Set.empty patsyns display
+ setSignature emptySignature
+ setPatternSyns Map.empty
+
+ return (True, r)
+ else do
+ ms <- getImportPath
+ nesting <- asks envModuleNestingLevel
+ range <- asks envRange
+ call <- asks envCall
+ mf <- use stModuleToSource
+ vs <- getVisitedModules
+ ds <- getDecodedModules
+ opts <- stPersistentOptions . stPersistentState <$> get
+ isig <- use stImports
+ ibuiltin <- use stImportedBuiltins
+ display <- use stImportsDisplayForms
+ ipatsyns <- getPatternSynImports
+ ho <- getInteractionOutputCallback
+ -- Every interface is treated in isolation. Note: Changes
+ -- to stDecodedModules are not preserved if an error is
+ -- encountered in an imported module.
+ -- Andreas, 2014-03-23: freshTCM spawns a new TCM computation
+ -- with initial state and environment
+ -- but on the same Benchmark accounts.
+ r <- freshTCM $
+ withImportPath ms $
+ local (\e -> e { envModuleNestingLevel = nesting
+ -- Andreas, 2014-08-18:
+ -- Preserve the range of import statement
+ -- for reporting termination errors in
+ -- imported modules:
+ , envRange = range
+ , envCall = call
+ }) $ do
+ setDecodedModules ds
+ setCommandLineOptions opts
+ setInteractionOutputCallback ho
+ stModuleToSource .= mf
+ setVisitedModules vs
+ addImportedThings isig ibuiltin Set.empty Set.empty ipatsyns display
+
+ r <- withMsgs $ createInterface file x includeStateChanges
+ mf <- use stModuleToSource
+ ds <- getDecodedModules
+ return (r, do
+ stModuleToSource .= mf
+ setDecodedModules ds
+ case r of
+ (i, NoWarnings) -> storeDecodedModule i
+ _ -> return ()
+ )
+
+ case r of
+ Left err -> throwError err
+ Right (r, update) -> do
+ update
+ case r of
+ (_, 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.
+ getStoredInterface x file includeStateChanges
+ _ -> return (False, r)
+
+
+-- | Formats and outputs the "Checking", "Finished" and "Skipping" messages.
+
+chaseMsg
+ :: String -- ^ The prefix, like @Checking@, @Finished@, @Skipping@.
+ -> C.TopLevelModuleName -- ^ The module name.
+ -> Maybe String -- ^ Optionally: the file name.
+ -> TCM ()
+chaseMsg kind x file = do
+ indentation <- (`replicate` ' ') <$> asks envModuleNestingLevel
+ let maybeFile = caseMaybe file "." $ \ f -> " (" ++ f ++ ")."
+ reportSLn "import.chase" 1 $ concat $
+ [ indentation, kind, " ", prettyShow x, maybeFile ]
+
+
+-- | Print the highlighting information contained in the given interface.
highlightFromInterface
:: Interface
@@ -476,6 +562,7 @@ highlightFromInterface i file = do
" (read from interface)."
printHighlightingInfo (iHighlighting i)
+
readInterface :: FilePath -> TCM (Maybe Interface)
readInterface file = do
-- Decode the interface file
@@ -503,8 +590,7 @@ readInterface file = do
-- document.
_ -> throwError e
--- | Writes the given interface to the given file. Returns the file's
--- new modification time stamp, or 'Nothing' if the write failed.
+-- | Writes the given interface to the given file.
writeInterface :: FilePath -> Interface -> TCM ()
writeInterface file i = do
@@ -543,8 +629,9 @@ removePrivates si = si { scopeModules = restrictPrivate <$> scopeModules si }
createInterface
:: AbsolutePath -- ^ The file to type check.
-> C.TopLevelModuleName -- ^ The expected module name.
+ -> Bool
-> TCM (Interface, MaybeWarnings)
-createInterface file mname =
+createInterface file mname isMain =
local (\e -> e { envCurrentPath = Just file }) $ do
modFile <- use stModuleToSource
fileTokenInfo <- Bench.billTo [Bench.Highlighting] $
@@ -563,7 +650,7 @@ createInterface file mname =
-- Parsing.
(pragmas, top) <- Bench.billTo [Bench.Parsing] $
- liftIO $ parseFile' moduleParser file
+ runPM $ parseFile' moduleParser file
pragmas <- concat <$> concreteToAbstract_ pragmas
-- identity for top-level pragmas at the moment
@@ -576,7 +663,7 @@ createInterface file mname =
-- Scope checking.
reportSLn "import.iface.create" 7 $ "Starting scope checking."
topLevel <- Bench.billTo [Bench.Scoping] $
- concreteToAbstract_ (TopLevel file top)
+ concreteToAbstract_ (TopLevel file mname top)
reportSLn "import.iface.create" 7 $ "Finished scope checking."
let ds = topLevelDecls topLevel
@@ -643,10 +730,35 @@ createInterface file mname =
setScope scope
reportSLn "scope.top" 50 $ "SCOPE " ++ show scope
+ -- TODO: It would be nice if unsolved things were highlighted
+ -- after every mutual block.
+
+ openMetas <- getOpenMetas
+ unless (null openMetas) $ do
+ reportSLn "import.metas" 10 "We have unsolved metas."
+ reportSLn "import.metas" 10 . unlines =<< showOpenMetas
+
+ ifTopLevelAndHighlightingLevelIs NonInteractive $
+ printUnsolvedInfo
+
+ -- Andreas, 2016-08-03, issue #964
+ -- When open metas are allowed,
+ -- permanently freeze them now by turning them into postulates.
+ -- This will enable serialization.
+ -- savedMetaStore <- use stMetaStore
+ unless isMain $
+ whenM (optAllowUnsolved <$> pragmaOptions) $ do
+ withCurrentModule (scopeCurrent scope) $
+ openMetasToPostulates
+ -- Clear constraints as they might refer to what
+ -- they think are open metas.
+ stAwakeConstraints .= []
+ stSleepingConstraints .= []
+
-- Serialization.
reportSLn "import.iface.create" 7 $ "Starting serialization."
syntaxInfo <- use stSyntaxInfo
- i <- Bench.billTo [Bench.Serialization] $ do
+ i <- Bench.billTo [Bench.Serialization, Bench.BuildInterface] $ do
buildInterface file topLevel syntaxInfo previousHsImports previousHsImportsUHC options
reportSLn "tc.top" 101 $ concat $
@@ -658,31 +770,22 @@ createInterface file mname =
]
reportSLn "import.iface.create" 7 $ "Finished serialization."
- -- TODO: It would be nice if unsolved things were highlighted
- -- after every mutual block.
-
- openMetas <- getOpenMetas
- unless (null openMetas) $ do
- reportSLn "import.metas" 10 "We have unsolved metas."
- reportSLn "import.metas" 10 . unlines =<< showOpenMetas
- unsolvedMetas <- List.nub <$> mapM getMetaRange openMetas
- unsolvedConstraints <- getAllConstraints
- interactionPoints <- getInteractionPoints
+ mallWarnings <- getAllWarnings ErrorWarnings
+ $ if isMain then IgnoreFlags else RespectFlags
- ifTopLevelAndHighlightingLevelIs NonInteractive $
- printUnsolvedInfo
+ reportSLn "import.iface.create" 7 $ "Considering writing to interface file."
+ case mallWarnings of
+ SomeWarnings allWarnings -> return ()
+ NoWarnings -> Bench.billTo [Bench.Serialization] $ do
+ -- The file was successfully type-checked (and no warnings were
+ -- encountered), so the interface should be written out.
+ let ifile = filePath $ toIFile file
+ writeInterface ifile i
+ reportSLn "import.iface.create" 7 $ "Finished (or skipped) writing to interface file."
- reportSLn "import.iface.create" 7 $ "Starting writing to interface file."
- r <- if and [ null unsolvedMetas, null unsolvedConstraints, null interactionPoints ]
- then Bench.billTo [Bench.Serialization] $ do
- -- The file was successfully type-checked (and no warnings were
- -- encountered), so the interface should be written out.
- let ifile = filePath $ toIFile file
- writeInterface ifile i
- return (i, NoWarnings)
- else do
- return (i, SomeWarnings $ Warnings unsolvedMetas unsolvedConstraints)
- reportSLn "import.iface.create" 7 $ "Finished 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 .= savedMetaStore
-- Profiling: Print statistics.
printStatistics 30 (Just mname) =<< getStatistics
@@ -694,7 +797,58 @@ createInterface file mname =
verboseS "profile" 1 $ do
reportSLn "import.iface" 5 $ "Accumulated statistics."
- return $ first constructIScope r
+ return $ first constructIScope (i, mallWarnings)
+
+-- | Collect all warnings that have accumulated in the state.
+-- Depending on the argument, we either respect the flags passed
+-- in by the user, or not (for instance when deciding if we are
+-- writing an interface file or not)
+
+data WhichWarnings = ErrorWarnings | AllWarnings
+ -- ^ order of constructors important for derived Ord instance
+ deriving (Eq, Ord)
+
+classifyWarning :: Warning -> WhichWarnings
+classifyWarning w = case w of
+ OldBuiltin{} -> AllWarnings
+ EmptyRewritePragma -> AllWarnings
+ TerminationIssue{} -> ErrorWarnings
+ NotStrictlyPositive{} -> ErrorWarnings
+ UnsolvedMetaVariables{} -> ErrorWarnings
+ UnsolvedInteractionMetas{} -> ErrorWarnings
+ UnsolvedConstraints{} -> ErrorWarnings
+ ParseWarning{} -> ErrorWarnings
+
+classifyWarnings :: [TCWarning] -> ([TCWarning], [TCWarning])
+classifyWarnings = partition $ (< AllWarnings) . classifyWarning . tcWarning
+
+getAllWarnings' :: WhichWarnings -> IgnoreFlags -> TCM [TCWarning]
+getAllWarnings' ww ifs = do
+ openMetas <- getOpenMetas
+ interactionMetas <- getInteractionMetas
+ let getUniqueMetas = fmap List.nub . mapM getMetaRange
+ unsolvedInteractions <- getUniqueMetas interactionMetas
+ unsolvedMetas <- getUniqueMetas (openMetas List.\\ interactionMetas)
+ unsolvedConstraints <- getAllConstraints
+ collectedTCWarnings <- use stTCWarnings
+
+ unsolved <- mapM warning_
+ [ UnsolvedInteractionMetas unsolvedInteractions
+ , UnsolvedMetaVariables unsolvedMetas
+ , UnsolvedConstraints unsolvedConstraints ]
+
+ fmap (filter ((<= ww) . classifyWarning . tcWarning))
+ $ applyFlagsToTCWarnings ifs $ reverse
+ $ unsolved ++ collectedTCWarnings
+
+getAllWarnings :: WhichWarnings -> IgnoreFlags -> TCM MaybeWarnings
+getAllWarnings ww ifs = do
+ allWarnings <- getAllWarnings' ww ifs
+ return $ if null allWarnings
+ -- Andreas, issue 964: not checking null interactionPoints
+ -- anymore; we want to serialize with open interaction points now!
+ then NoWarnings
+ else SomeWarnings allWarnings
-- constructIScope :: ScopeInfo -> Map ModuleName Scope
constructIScope :: Interface -> Interface
@@ -740,7 +894,7 @@ buildInterface file topLevel syntaxInfo previousHsImports previousHsImportsUHC p
-- Ulf, 2016-04-12:
-- Non-closed display forms are not applicable outside the module anyway,
-- and should be dead-code eliminated (#1928).
- display <- HMap.filter (not . null) . HMap.map (filter isClosed) <$> use stImportsDisplayForms
+ display <- HMap.filter (not . null) . HMap.map (filter isGlobal) <$> use stImportsDisplayForms
-- TODO: Kill some ranges?
(display, sig) <- eliminateDeadCode display =<< getSignature
-- Andreas, 2015-02-09 kill ranges in pattern synonyms before