{-# LANGUAGE CPP #-}
module Agda.Interaction.Imports where
import Prelude hiding (null)
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
import Data.Function (on)
import qualified Data.Map as Map
import qualified Data.List as List
import qualified Data.Set as Set
import qualified Data.Foldable as Fold (toList)
import qualified Data.List as List
import Data.Maybe
import Data.Monoid (mempty, mappend)
import Data.Map (Map)
import Data.Set (Set)
import Data.Text.Lazy (Text)
import qualified Data.Text.Lazy as T
import System.Directory (doesFileExist, getModificationTime, removeFile)
import System.FilePath ((</>))
import qualified Text.PrettyPrint.Boxes as Boxes
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.Syntax.Internal
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Warnings
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.DeadCode
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TheTypeChecker
import Agda.Interaction.FindFile
import {-# SOURCE #-} Agda.Interaction.InteractionTop (showOpenMetas)
import Agda.Interaction.Options
import qualified Agda.Interaction.Options.Lenses as Lens
import Agda.Interaction.Highlighting.Precise
(HighlightingInfo, compress)
import Agda.Interaction.Highlighting.Generate
import Agda.Interaction.Highlighting.Vim
import Agda.Interaction.Response
(RemoveTokenBasedHighlighting(KeepHighlighting))
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.FileName
import Agda.Utils.Lens
import Agda.Utils.Maybe
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.IO.Binary
import Agda.Utils.Pretty hiding (Mode)
import Agda.Utils.Time
import Agda.Utils.Hash
import qualified Agda.Utils.HashMap as HMap
import qualified Agda.Utils.Trie as Trie
#include "undefined.h"
import Agda.Utils.Impossible
data SourceInfo = SourceInfo
{ siSource :: Text
, siFileType :: FileType
, siModule :: C.Module
, siModuleName :: C.TopLevelModuleName
}
sourceInfo :: AbsolutePath -> TCM SourceInfo
sourceInfo f = Bench.billTo [Bench.Parsing] $ do
source <- runPM $ readFilePM f
(parsedMod, fileType) <- runPM $
parseFile moduleParser f $ T.unpack source
moduleName <- moduleName f parsedMod
return $ SourceInfo { siSource = source
, siFileType = fileType
, siModule = parsedMod
, siModuleName = moduleName
}
data Mode
= ScopeCheck
| TypeCheck
deriving (Eq, Show)
data MainInterface
= MainInterface Mode
| NotMainInterface
deriving (Eq, Show)
includeStateChanges :: MainInterface -> Bool
includeStateChanges (MainInterface _) = True
includeStateChanges NotMainInterface = False
mergeInterface :: Interface -> TCM ()
mergeInterface i = do
let sig = iSignature i
builtin = Map.toList $ iBuiltin i
prim = [ x | (_,Prim x) <- builtin ]
bi = Map.fromList [ (x,Builtin t) | (x,Builtin t) <- builtin ]
warns = iWarnings i
bs <- getsTC stBuiltinThings
reportSLn "import.iface.merge" 10 $ "Merging interface"
reportSLn "import.iface.merge" 20 $
" Current builtins " ++ show (Map.keys bs) ++ "\n" ++
" New builtins " ++ show (Map.keys bi)
let check b = case (b1, b2) of
(Builtin x, Builtin y)
| x == y -> return ()
| otherwise -> typeError $ DuplicateBuiltinBinding b x y
_ -> __IMPOSSIBLE__
where
Just b1 = Map.lookup b bs
Just b2 = Map.lookup b bi
mapM_ check (map fst $ Map.toList $ Map.intersection bs bi)
addImportedThings sig bi (iPatternSyns i) (iDisplayForms i) (iUserWarnings i) warns
reportSLn "import.iface.merge" 20 $
" Rebinding primitives " ++ show prim
mapM_ rebind prim
where
rebind (x, q) = do
PrimImpl _ pf <- lookupPrimitiveFunction x
stImportedBuiltins `modifyTCLens` Map.insert x (Prim pf{ primFunName = q })
addImportedThings ::
Signature -> BuiltinThings PrimFun ->
A.PatternSynDefns -> DisplayForms -> Map A.QName String -> [TCWarning] -> TCM ()
addImportedThings isig ibuiltin patsyns display userwarn warnings = do
stImports `modifyTCLens` \ imp -> unionSignatures [imp, isig]
stImportedBuiltins `modifyTCLens` \ imp -> Map.union imp ibuiltin
stImportedUserWarnings `modifyTCLens` \ imp -> Map.union imp userwarn
stPatternSynImports `modifyTCLens` \ imp -> Map.union imp patsyns
stImportedDisplayForms `modifyTCLens` \ imp -> HMap.unionWith (++) imp display
stTCWarnings `modifyTCLens` \ imp -> List.union imp warnings
addImportedInstances isig
scopeCheckImport :: ModuleName -> TCM (ModuleName, Map ModuleName Scope)
scopeCheckImport x = do
reportSLn "import.scope" 5 $ "Scope checking " ++ prettyShow x
verboseS "import.scope" 10 $ do
visited <- Map.keys <$> getVisitedModules
reportSLn "import.scope" 10 $
" visited: " ++ List.intercalate ", " (map prettyShow visited)
i <- Bench.billTo [] $ getInterface x
addImport x
let s = iScope i
return (iModuleName i `withRangesOfQ` mnameToConcrete x, s)
data MaybeWarnings' a = NoWarnings | SomeWarnings a
deriving (Show, Functor, Foldable, Traversable)
type MaybeWarnings = MaybeWarnings' [TCWarning]
applyFlagsToMaybeWarnings :: MaybeWarnings -> TCM MaybeWarnings
applyFlagsToMaybeWarnings mw = do
w' <- traverse applyFlagsToTCWarnings 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 = not . null
alreadyVisited :: C.TopLevelModuleName ->
MainInterface ->
PragmaOptions ->
TCM (Interface, MaybeWarnings) ->
TCM (Interface, MaybeWarnings)
alreadyVisited x isMain currentOptions getIface = do
mm <- getVisitedModule x
case mm of
Just mi | not (miWarnings mi) -> do
reportSLn "import.visit" 10 $ " Already visited " ++ prettyShow x
let i = miInterface mi
optsCompat <- if miPrimitive mi then return True else do
ifM (asksTC envCheckOptionConsistency)
(checkOptionsCompatible currentOptions (iOptionsUsed i)
(iModuleName i))
(return True)
if optsCompat then return (i , NoWarnings) else do
wt <- getMaybeWarnings' isMain ErrorWarnings
return (i, wt)
_ -> do
reportSLn "import.visit" 5 $ " Getting interface for " ++ prettyShow x
r@(i, wt) <- getIface
reportSLn "import.visit" 5 $ " Now we've looked at " ++ prettyShow x
unless (isMain == MainInterface ScopeCheck) $
visitModule $ ModuleInfo
{ miInterface = i
, miWarnings = hasWarnings wt
, miPrimitive = False
}
return r
typeCheckMain
:: AbsolutePath
-> Mode
-> SourceInfo
-> TCM (Interface, MaybeWarnings)
typeCheckMain f mode si = do
reportSLn "import.main" 10 $ "Importing the primitive modules."
libdir <- liftIO defaultLibDir
let libdirPrim = libdir </> "prim"
reportSLn "import.main" 20 $ "Library dir = " ++ show libdir
bracket_ (getsTC Lens.getPersistentVerbosity) Lens.putPersistentVerbosity $ do
Lens.modifyPersistentVerbosity (Trie.delete [])
withHighlightingLevel None $ withoutOptionsChecking $
forM_ (Set.map (libdirPrim </>) Lens.primitiveModules) $ \f -> do
let file = mkAbsolute f
si <- sourceInfo file
checkModuleName' (siModuleName si) file
_ <- getInterface_ (siModuleName si) (Just si)
mapVisitedModule (siModuleName si) (\ m -> m { miPrimitive = True })
reportSLn "import.main" 10 $ "Done importing the primitive modules."
checkModuleName' (siModuleName si) f
getInterface' (siModuleName si) (MainInterface mode) (Just si)
where
checkModuleName' m f =
(if null r then id else traceCall (SetRange r)) $
checkModuleName m f Nothing
where
r = getRange m
getInterface :: ModuleName -> TCM Interface
getInterface m = getInterface_ (toTopLevelModuleName m) Nothing
getInterface_
:: C.TopLevelModuleName
-> Maybe SourceInfo
-> TCM Interface
getInterface_ x msi = do
(i, wt) <- getInterface' x NotMainInterface msi
case wt of
SomeWarnings w -> tcWarningsToError (filter (notIM . tcWarning) w)
NoWarnings -> return i
where notIM UnsolvedInteractionMetas{} = False
notIM _ = True
getInterface'
:: C.TopLevelModuleName
-> MainInterface
-> Maybe SourceInfo
-> TCM (Interface, MaybeWarnings)
getInterface' x isMain msi = do
withIncreasedModuleNestingLevel $ do
bracket_ (useTC stPragmaOptions)
(unless (includeStateChanges isMain) . (stPragmaOptions `setTCLens`)) $ do
when (includeStateChanges isMain) $ do
pragmas <- concreteOptionsToOptionPragmas
(fst $ maybe __IMPOSSIBLE__ siModule msi)
mapM_ setOptionsFromPragma pragmas
currentOptions <- useTC stPragmaOptions
setCommandLineOptions . stPersistentOptions . stPersistentState =<< getTC
alreadyVisited x isMain currentOptions $ addImportCycleCheck x $ do
file <- findFile x
reportSLn "import.iface" 10 $ " Check for cycle"
checkForImportCycle
uptodate <- Bench.billTo [Bench.Import] $ do
ignore <- (ignoreInterfaces `and2M`
(not <$> Lens.isBuiltinModule (filePath file)))
`or2M` ignoreAllInterfaces
cached <- runMaybeT $ isCached x file
sourceH <- case msi of
Nothing -> liftIO $ hashTextFile file
Just si -> return $ hashText (siSource si)
ifaceH <-
case cached of
Nothing -> fmap fst <$> getInterfaceFileHashes (filePath $ toIFile file)
Just i -> return $ Just $ iSourceHash i
let unchanged = Just sourceH == ifaceH
return $ unchanged && (not ignore || isJust cached)
reportSLn "import.iface" 5 $
" " ++ prettyShow x ++ " is " ++
(if uptodate then "" else "not ") ++ "up-to-date."
(stateChangesIncluded, (i, wt)) <- do
let maySkip = True
if uptodate && maySkip
then getStoredInterface x file isMain msi
else typeCheck x file isMain msi
let topLevelName = toTopLevelModuleName $ iModuleName i
unless (topLevelName == x) $ do
typeError $ OverlappingProjects file topLevelName x
visited <- isVisited x
reportSLn "import.iface" 5 $ if visited then " We've been here. Don't merge."
else " New module. Let's check it out."
wt' <- ifM (not <$> asksTC envCheckOptionConsistency)
(return wt) $ do
optComp <- checkOptionsCompatible currentOptions (iOptionsUsed i) (iModuleName i)
if optComp then return wt else getMaybeWarnings' isMain ErrorWarnings
unless (visited || stateChangesIncluded) $ do
mergeInterface i
Bench.billTo [Bench.Highlighting] $
ifTopLevelAndHighlightingLevelIs NonInteractive $
highlightFromInterface i file
stCurrentModule `setTCLens` Just (iModuleName i)
case (isMain, wt') of
(MainInterface ScopeCheck, _) -> return ()
(_, SomeWarnings w) -> return ()
_ -> storeDecodedModule i
return (i, wt')
checkOptionsCompatible :: PragmaOptions -> PragmaOptions -> ModuleName -> TCM Bool
checkOptionsCompatible current imported importedModule = flip execStateT True $ do
reportSDoc "import.iface.options" 5 $ P.nest 2 $ "current options =" P.<+> showOptions current
reportSDoc "import.iface.options" 5 $ P.nest 2 $ "imported options =" P.<+> showOptions imported
forM_ coinfectiveOptions $ \ (opt, optName) -> do
unless ((opt current) `implies` (opt imported)) $ do
put False
warning (CoInfectiveImport optName importedModule)
forM_ infectiveOptions $ \ (opt, optName) -> do
unless ((opt imported) `implies` (opt current)) $ do
put False
warning (InfectiveImport optName importedModule)
where
implies :: Bool -> Bool -> Bool
p `implies` q = p <= q
showOptions opts = P.prettyList (map (\ (o, n) -> P.text n P.<> ": " P.<+> (P.pretty $ o opts))
(coinfectiveOptions ++ infectiveOptions))
isCached
:: C.TopLevelModuleName
-> AbsolutePath
-> MaybeT TCM Interface
isCached x file = do
let ifile = filePath $ toIFile file
guardM $ liftIO $ doesFileExistCaseSensitive ifile
mi <- MaybeT $ getDecodedModule x
h <- MaybeT $ fmap snd <$> getInterfaceFileHashes ifile
guard $ iFullHash mi == h
return mi
getStoredInterface
:: C.TopLevelModuleName
-> AbsolutePath
-> MainInterface
-> Maybe SourceInfo
-> TCM (Bool, (Interface, MaybeWarnings))
getStoredInterface x file isMain msi = do
let fallback = typeCheck x file isMain msi
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
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)
mapM_ setOptionsFromPragma (iPragmaOptions i)
optionsChanged <-ifM ((not <$> asksTC envCheckOptionConsistency) `or2M`
Lens.isBuiltinModule (filePath file))
(return False) $ do
currentOptions <- useTC stPragmaOptions
let disagreements =
[ optName | (opt, optName) <- restartOptions,
(opt currentOptions) /= (opt (iOptionsUsed i))]
if null disagreements then return False else do
reportSLn "import.iface.options" 4 $ " Changes in the following options in " ++ prettyShow (filePath file) ++ ", re-typechecking: " ++ prettyShow disagreements
return True
if optionsChanged then fallback else do
hs <- map iFullHash <$> mapM getInterface (map fst $ iImportedModules i)
if hs /= map snd (iImportedModules i)
then do
fallback
else do
unless cached $ do
chaseMsg "Loading " x $ Just ifile
let ws = filter ((Strict.Just file ==) . tcWarningOrigin) (iWarnings i)
unless (null ws) $ reportSDoc "warning" 1 $ P.vcat $ P.prettyTCM <$> ws
return (False, (i, NoWarnings))
typeCheck
:: C.TopLevelModuleName
-> AbsolutePath
-> MainInterface
-> Maybe SourceInfo
-> TCM (Bool, (Interface, MaybeWarnings))
typeCheck x file isMain msi = do
unless (includeStateChanges isMain) cleanCachedLog
let checkMsg = case isMain of
MainInterface ScopeCheck -> "Reading "
_ -> "Checking"
withMsgs = bracket_
(chaseMsg checkMsg x $ Just $ filePath file)
(const $ do ws <- getAllWarnings AllWarnings
let (we, wa) = classifyWarnings ws
let wa' = filter ((Strict.Just file ==) . tcWarningOrigin) wa
unless (null wa') $
reportSDoc "warning" 1 $ P.vcat $ P.prettyTCM <$> wa'
when (null we) $ chaseMsg "Finished" x Nothing)
case isMain of
MainInterface _ -> do
r <- withMsgs $ createInterface file x isMain msi
return (True, r)
NotMainInterface -> do
ms <- getImportPath
nesting <- asksTC envModuleNestingLevel
range <- asksTC envRange
call <- asksTC envCall
mf <- useTC stModuleToSource
vs <- getVisitedModules
ds <- getDecodedModules
opts <- stPersistentOptions . stPersistentState <$> getTC
isig <- useTC stImports
ibuiltin <- useTC stImportedBuiltins
display <- useTC stImportsDisplayForms
userwarn <- useTC stImportedUserWarnings
ipatsyns <- getPatternSynImports
ho <- getInteractionOutputCallback
r <- withoutCache $
freshTCM $
withImportPath ms $
localTC (\e -> e { envModuleNestingLevel = nesting
, envRange = range
, envCall = call
}) $ do
setDecodedModules ds
setCommandLineOptions opts
setInteractionOutputCallback ho
stModuleToSource `setTCLens` mf
setVisitedModules vs
addImportedThings isig ibuiltin ipatsyns display userwarn []
r <- withMsgs $ createInterface file x isMain msi
mf <- useTC stModuleToSource
ds <- getDecodedModules
return (r, do
stModuleToSource `setTCLens` 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) ->
getStoredInterface x file isMain msi
_ -> return (False, r)
chaseMsg
:: String
-> C.TopLevelModuleName
-> Maybe String
-> TCM ()
chaseMsg kind x file = do
indentation <- (`replicate` ' ') <$> asksTC envModuleNestingLevel
let maybeFile = caseMaybe file "." $ \ f -> " (" ++ f ++ ")."
vLvl | kind == "Checking" = 1
| otherwise = 2
reportSLn "import.chase" vLvl $ concat $
[ indentation, kind, " ", prettyShow x, maybeFile ]
highlightFromInterface
:: Interface
-> AbsolutePath
-> TCM ()
highlightFromInterface i file = do
reportSLn "import.iface" 5 $
"Generating syntax info for " ++ filePath file ++
" (read from interface)."
printHighlightingInfo KeepHighlighting (iHighlighting i)
readInterface :: FilePath -> TCM (Maybe Interface)
readInterface file = do
(s, close) <- liftIO $ readBinaryFile' file
do mi <- liftIO . E.evaluate =<< decodeInterface s
liftIO close
return $ constructIScope <$> mi
`catchError` \e -> liftIO close >> handler e
`catchError` handler
where
handler e = case e of
IOException _ _ e -> do
reportSLn "" 0 $ "IO exception: " ++ show e
return Nothing
_ -> throwError e
writeInterface :: FilePath -> Interface -> TCM ()
writeInterface file i = do
reportSLn "import.iface.write" 5 $ "Writing interface file " ++ file ++ "."
encodeFile file i
reportSLn "import.iface.write" 5 $ "Wrote interface file."
reportSLn "import.iface.write" 50 $ " hash = " ++ show (iFullHash i) ++ ""
`catchError` \e -> do
reportSLn "" 1 $
"Failed to write interface " ++ file ++ "."
liftIO $
whenM (doesFileExist file) $ removeFile file
throwError e
removePrivates :: ScopeInfo -> ScopeInfo
removePrivates si = si { scopeModules = restrictPrivate <$> scopeModules si }
concreteOptionsToOptionPragmas :: [C.Pragma] -> TCM [OptionsPragma]
concreteOptionsToOptionPragmas p = do
pragmas <- concat <$> concreteToAbstract_ p
let getOptions (A.OptionsPragma opts) = Just opts
getOptions _ = Nothing
return $ mapMaybe getOptions pragmas
createInterface
:: AbsolutePath
-> C.TopLevelModuleName
-> MainInterface
-> Maybe SourceInfo
-> TCM (Interface, MaybeWarnings)
createInterface file mname isMain msi =
Bench.billTo [Bench.TopModule mname] $
localTC (\e -> e { envCurrentPath = Just file }) $ do
reportSLn "import.iface.create" 5 $
"Creating interface for " ++ prettyShow mname ++ "."
verboseS "import.iface.create" 10 $ do
visited <- Map.keys <$> getVisitedModules
reportSLn "import.iface.create" 10 $
" visited: " ++ List.intercalate ", " (map prettyShow visited)
(source, fileType, (pragmas, top)) <- do
si <- case msi of
Nothing -> sourceInfo file
Just si -> return si
case si of
SourceInfo {..} -> return (siSource, siFileType, siModule)
modFile <- useTC stModuleToSource
fileTokenInfo <- Bench.billTo [Bench.Highlighting] $
generateTokenInfoFromSource
file (T.unpack source)
stTokens `setTCLens` fileTokenInfo
options <- concreteOptionsToOptionPragmas pragmas
mapM_ setOptionsFromPragma options
reportSLn "import.iface.create" 7 $ "Starting scope checking."
topLevel <- Bench.billTo [Bench.Scoping] $
concreteToAbstract_ (TopLevel file mname top)
reportSLn "import.iface.create" 7 $ "Finished scope checking."
let ds = topLevelDecls topLevel
scope = topLevelScope topLevel
reportSLn "import.iface.create" 7 $ "Starting highlighting from scope."
Bench.billTo [Bench.Highlighting] $ do
ifTopLevelAndHighlightingLevelIs NonInteractive $
printHighlightingInfo KeepHighlighting fileTokenInfo
let onlyScope = isMain == MainInterface ScopeCheck
ifTopLevelAndHighlightingLevelIsOr NonInteractive onlyScope $
mapM_ (\ d -> generateAndPrintSyntaxInfo d Partial onlyScope) ds
reportSLn "import.iface.create" 7 $ "Finished highlighting from scope."
activateLoadedFileCache
cachingStarts
opts <- useTC stPragmaOptions
me <- readFromCachedLog
case me of
Just (Pragmas opts', _) | opts == opts'
-> return ()
_ -> do
reportSLn "cache" 10 $ "pragma changed: " ++ show (isJust me)
cleanCachedLog
writeToCurrentLog $ Pragmas opts
case isMain of
MainInterface ScopeCheck -> do
reportSLn "import.iface.create" 7 $ "Skipping type checking."
cacheCurrentLog
_ -> do
reportSLn "import.iface.create" 7 $ "Starting type checking."
Bench.billTo [Bench.Typing] $ mapM_ checkDeclCached ds `finally_` cacheCurrentLog
reportSLn "import.iface.create" 7 $ "Finished type checking."
unfreezeMetas
verboseS "profile.metas" 10 $ do
MetaId n <- fresh
tickN "metas" (fromIntegral n)
reportSLn "import.iface.create" 7 $ "Starting highlighting from type info."
Bench.billTo [Bench.Highlighting] $ do
toks <- useTC stTokens
ifTopLevelAndHighlightingLevelIs NonInteractive $
printHighlightingInfo KeepHighlighting toks
stTokens `setTCLens` mempty
warnings <- getAllWarnings AllWarnings
unless (null warnings) $ reportSDoc "import.iface.create" 20 $
"collected warnings: " P.<> prettyTCM warnings
unsolved <- getAllUnsolved
unless (null unsolved) $ reportSDoc "import.iface.create" 20 $
"collected unsolved: " P.<> prettyTCM unsolved
let warningInfo = compress $ foldMap warningHighlighting $ unsolved ++ warnings
stSyntaxInfo `modifyTCLens` \inf -> (inf `mappend` toks) `mappend` warningInfo
whenM (optGenerateVimFile <$> commandLineOptions) $
withScope_ scope $ generateVimFile $ filePath file
reportSLn "import.iface.create" 7 $ "Finished highlighting from type info."
setScope scope
reportSLn "scope.top" 50 $ "SCOPE " ++ show scope
openMetas <- getOpenMetas
unless (null openMetas) $ do
reportSLn "import.metas" 10 "We have unsolved metas."
reportSLn "import.metas" 10 . unlines =<< showOpenMetas
ifTopLevelAndHighlightingLevelIs NonInteractive $
printUnsolvedInfo
allowUnsolved <- optAllowUnsolved <$> pragmaOptions
unless (includeStateChanges isMain) $
when allowUnsolved $ do
reportSLn "import.iface.create" 7 $ "Turning unsolved metas (if any) into postulates."
withCurrentModule (scopeCurrent scope) $
openMetasToPostulates
stAwakeConstraints `setTCLens` []
stSleepingConstraints `setTCLens` []
reportSLn "import.iface.create" 7 $ "Starting serialization."
i <- Bench.billTo [Bench.Serialization, Bench.BuildInterface] $ do
buildInterface source fileType topLevel options
reportSLn "tc.top" 101 $ unlines $
"Signature:" :
[ unlines
[ prettyShow x
, " type: " ++ show (defType def)
, " def: " ++ show cc
]
| (x, def) <- HMap.toList $ iSignature i ^. sigDefinitions,
Function{ funCompiled = cc } <- [theDef def]
]
reportSLn "import.iface.create" 7 $ "Finished serialization."
mallWarnings <- getMaybeWarnings' isMain ErrorWarnings
reportSLn "import.iface.create" 7 $ "Considering writing to interface file."
case (mallWarnings, isMain) of
(SomeWarnings allWarnings, _) -> do
reportSLn "import.iface.create" 7 $ "We have warnings, skipping writing interface file."
return ()
(_, MainInterface ScopeCheck) -> do
reportSLn "import.iface.create" 7 $ "We are just scope-checking, skipping writing interface file."
return ()
_ -> Bench.billTo [Bench.Serialization] $ do
reportSLn "import.iface.create" 7 $ "Actually calling writeInterface."
let ifile = filePath $ toIFile file
writeInterface ifile i
reportSLn "import.iface.create" 7 $ "Finished (or skipped) writing to interface file."
printStatistics 30 (Just mname) =<< getStatistics
localStatistics <- getStatistics
lensAccumStatistics `modifyTCLens` Map.unionWith (+) localStatistics
verboseS "profile" 1 $ do
reportSLn "import.iface" 5 $ "Accumulated statistics."
return $ first constructIScope (i, mallWarnings)
getUniqueMetasRanges :: [MetaId] -> TCM [Range]
getUniqueMetasRanges = fmap List.nub . mapM getMetaRange
getUnsolvedMetas :: TCM [Range]
getUnsolvedMetas = do
openMetas <- getOpenMetas
interactionMetas <- getInteractionMetas
getUniqueMetasRanges (openMetas List.\\ interactionMetas)
getAllUnsolved :: TCM [TCWarning]
getAllUnsolved = do
unsolvedInteractions <- getUniqueMetasRanges =<< getInteractionMetas
unsolvedConstraints <- getAllConstraints
unsolvedMetas <- getUnsolvedMetas
let checkNonEmpty c rs = c rs <$ guard (not $ null rs)
mapM warning_ $ catMaybes
[ checkNonEmpty UnsolvedInteractionMetas unsolvedInteractions
, checkNonEmpty UnsolvedMetaVariables unsolvedMetas
, checkNonEmpty UnsolvedConstraints unsolvedConstraints ]
getAllWarnings :: WhichWarnings -> TCM [TCWarning]
getAllWarnings = getAllWarnings' NotMainInterface
getAllWarnings' :: MainInterface -> WhichWarnings -> TCM [TCWarning]
getAllWarnings' isMain ww = do
unsolved <- getAllUnsolved
collectedTCWarnings <- useTC stTCWarnings
let showWarn w = classifyWarning w <= ww &&
not (null unsolved && onlyShowIfUnsolved w)
fmap (filter (showWarn . tcWarning))
$ applyFlagsToTCWarnings' isMain $ reverse
$ unsolved ++ collectedTCWarnings
getMaybeWarnings :: WhichWarnings -> TCM MaybeWarnings
getMaybeWarnings = getMaybeWarnings' NotMainInterface
getMaybeWarnings' :: MainInterface -> WhichWarnings -> TCM MaybeWarnings
getMaybeWarnings' isMain ww = do
allWarnings <- getAllWarnings' isMain ww
return $ if null allWarnings
then NoWarnings
else SomeWarnings allWarnings
getAllWarningsOfTCErr :: TCErr -> TCM [TCWarning]
getAllWarningsOfTCErr err = case err of
TypeError tcst cls -> case clValue cls of
NonFatalErrors{} -> return []
_ -> localTCState $ do
putTC tcst
ws <- getAllWarnings AllWarnings
return $ filter (not . isUnsolvedWarning . tcWarning) ws
_ -> return []
constructIScope :: Interface -> Interface
constructIScope i = billToPure [ Deserialization ] $
i{ iScope = publicModules $ iInsideScope i }
buildInterface
:: Text
-> FileType
-> TopLevelInfo
-> [OptionsPragma]
-> TCM Interface
buildInterface source fileType topLevel pragmas = do
reportSLn "import.iface" 5 "Building interface..."
let m = topLevelModuleName topLevel
scope' <- getScope
let scope = scope' { scopeCurrent = m }
builtin <- useTC stLocalBuiltins
ms <- getImports
mhs <- mapM (\ m -> (m,) <$> moduleHash m) $ Set.toList ms
foreignCode <- useTC stForeignCode
display <- HMap.filter (not . null) . HMap.map (filter isClosed) <$> useTC stImportsDisplayForms
(display, sig) <- eliminateDeadCode display =<< getSignature
userwarns <- useTC stLocalUserWarnings
syntaxInfo <- useTC stSyntaxInfo
optionsUsed <- useTC stPragmaOptions
patsyns <- killRange <$> getPatternSyns
let builtin' = Map.mapWithKey (\ x b -> (x,) . primFunName <$> b) builtin
warnings <- getAllWarnings AllWarnings
reportSLn "import.iface" 7 " instantiating all meta variables"
i <- instantiateFull $ Interface
{ iSourceHash = hashText source
, iSource = source
, iFileType = fileType
, iImportedModules = mhs
, iModuleName = m
, iScope = empty
, iInsideScope = topLevelScope topLevel
, iSignature = sig
, iDisplayForms = display
, iUserWarnings = userwarns
, iBuiltin = builtin'
, iForeignCode = foreignCode
, iHighlighting = syntaxInfo
, iPragmaOptions = pragmas
, iOptionsUsed = optionsUsed
, iPatternSyns = patsyns
, iWarnings = warnings
}
reportSLn "import.iface" 7 " interface complete"
return i
getInterfaceFileHashes :: FilePath -> TCM (Maybe (Hash, Hash))
getInterfaceFileHashes ifile = do
exist <- liftIO $ doesFileExist ifile
if not exist then return Nothing else do
(s, close) <- liftIO $ readBinaryFile' ifile
let hs = decodeHashes s
liftIO $ maybe 0 (uncurry (+)) hs `seq` close
return hs
moduleHash :: ModuleName -> TCM Hash
moduleHash m = iFullHash <$> getInterface m
isNewerThan :: FilePath -> FilePath -> IO Bool
isNewerThan new old = do
newExist <- doesFileExist new
oldExist <- doesFileExist old
if not (newExist && oldExist)
then return newExist
else do
newT <- getModificationTime new
oldT <- getModificationTime old
return $ newT >= oldT