{-# 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 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.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 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 <- gets 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 %= 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 %= \ imp -> unionSignatures [imp, isig]
stImportedBuiltins %= \ imp -> Map.union imp ibuiltin
stImportedUserWarnings %= \ imp -> Map.union imp userwarn
stPatternSynImports %= \ imp -> Map.union imp patsyns
stImportedDisplayForms %= \ imp -> HMap.unionWith (++) imp display
stTCWarnings %= \ 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 (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 ->
TCM (Interface, MaybeWarnings) ->
TCM (Interface, MaybeWarnings)
alreadyVisited x isMain getIface = do
mm <- getVisitedModule x
case mm of
Just mi | not (miWarnings mi) -> do
reportSLn "import.visit" 10 $ " Already visited " ++ prettyShow x
return (miInterface mi, NoWarnings)
_ -> 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
}
return r
typeCheckMain :: AbsolutePath -> Mode -> TCM (Interface, MaybeWarnings)
typeCheckMain f mode = do
reportSLn "import.main" 10 $ "Importing the primitive modules."
libdir <- liftIO defaultLibDir
reportSLn "import.main" 20 $ "Library dir = " ++ show libdir
_ <- bracket_ (gets $ Lens.getSafeMode) Lens.putSafeMode $ do
Lens.putSafeMode False
bracket_ (gets $ Lens.getPersistentVerbosity) Lens.putPersistentVerbosity $ do
Lens.modifyPersistentVerbosity (Trie.delete [])
withHighlightingLevel None $
getInterface_ =<< do
moduleName $ mkAbsolute $
libdir </> "prim" </> "Agda" </> "Primitive.agda"
reportSLn "import.main" 10 $ "Done importing the primitive modules."
m <- moduleName f
getInterface' m (MainInterface mode)
getInterface :: ModuleName -> TCM Interface
getInterface = getInterface_ . toTopLevelModuleName
getInterface_ :: C.TopLevelModuleName -> TCM Interface
getInterface_ x = do
(i, wt) <- getInterface' x NotMainInterface
case wt of
SomeWarnings w -> tcWarningsToError (filter (notIM . tcWarning) w)
NoWarnings -> return i
where notIM UnsolvedInteractionMetas{} = False
notIM _ = True
getInterface'
:: C.TopLevelModuleName
-> MainInterface
-> TCM (Interface, MaybeWarnings)
getInterface' x isMain = do
withIncreasedModuleNestingLevel $ do
bracket_ (use stPragmaOptions)
(unless (includeStateChanges isMain) . (stPragmaOptions .=)) $ do
setCommandLineOptions . stPersistentOptions . stPersistentState =<< get
alreadyVisited x isMain $ addImportCycleCheck x $ do
file <- findFile x
reportSLn "import.iface" 10 $ " Check for cycle"
checkForImportCycle
uptodate <- Bench.billTo [Bench.Import] $ do
ignore <- ignoreInterfaces
cached <- runMaybeT $ isCached x file
sourceH <- liftIO $ hashFile file
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
else typeCheck x file isMain
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."
unless (visited || stateChangesIncluded) $ do
mergeInterface i
Bench.billTo [Bench.Highlighting] $
ifTopLevelAndHighlightingLevelIs NonInteractive $
highlightFromInterface i file
stCurrentModule .= Just (iModuleName i)
case (isMain, wt) of
(MainInterface ScopeCheck, _) -> return ()
(_, SomeWarnings w) -> return ()
_ -> storeDecodedModule i
return (i, wt)
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
-> TCM (Bool, (Interface, MaybeWarnings))
getStoredInterface x file isMain = do
let fallback = typeCheck x file isMain
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)
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
mapM_ setOptionsFromPragma (iPragmaOptions i)
return (False, (i, NoWarnings))
typeCheck
:: C.TopLevelModuleName
-> AbsolutePath
-> MainInterface
-> TCM (Bool, (Interface, MaybeWarnings))
typeCheck x file isMain = 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
return (True, r)
NotMainInterface -> 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
userwarn <- use stImportedUserWarnings
ipatsyns <- getPatternSynImports
ho <- getInteractionOutputCallback
r <- noCacheForImportedModule $
freshTCM $
withImportPath ms $
local (\e -> e { envModuleNestingLevel = nesting
, envRange = range
, envCall = call
}) $ do
setDecodedModules ds
setCommandLineOptions opts
setInteractionOutputCallback ho
stModuleToSource .= mf
setVisitedModules vs
addImportedThings isig ibuiltin ipatsyns display userwarn []
r <- withMsgs $ createInterface file x isMain
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) ->
getStoredInterface x file isMain
_ -> return (False, r)
chaseMsg
:: String
-> C.TopLevelModuleName
-> Maybe String
-> TCM ()
chaseMsg kind x file = do
indentation <- (`replicate` ' ') <$> asks 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 }
createInterface
:: AbsolutePath
-> C.TopLevelModuleName
-> MainInterface
-> TCM (Interface, MaybeWarnings)
createInterface file mname isMain = Bench.billTo [Bench.TopModule mname] $
local (\e -> e { envCurrentPath = Just file }) $ do
modFile <- use stModuleToSource
fileTokenInfo <- Bench.billTo [Bench.Highlighting] $
generateTokenInfo file
stTokens .= fileTokenInfo
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)
(pragmas, top) <- Bench.billTo [Bench.Parsing] $
runPM $ parseFile' moduleParser file
pragmas <- concat <$> concreteToAbstract_ pragmas
let getOptions (A.OptionsPragma opts) = Just opts
getOptions _ = Nothing
options = catMaybes $ map getOptions 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 <- use 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 <- use stTokens
ifTopLevelAndHighlightingLevelIs NonInteractive $
printHighlightingInfo KeepHighlighting toks
stTokens .= mempty
warnings <- getAllWarnings AllWarnings
unless (null warnings) $ reportSDoc "import.iface.create" 20 $
P.text "collected warnings: " P.<> prettyTCM warnings
unsolved <- getAllUnsolved
unless (null unsolved) $ reportSDoc "import.iface.create" 20 $
P.text "collected unsolved: " P.<> prettyTCM unsolved
let warningInfo = compress $ foldMap warningHighlighting $ unsolved ++ warnings
stSyntaxInfo %= \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
unless (includeStateChanges isMain) $
whenM (optAllowUnsolved <$> pragmaOptions) $ do
withCurrentModule (scopeCurrent scope) $
openMetasToPostulates
stAwakeConstraints .= []
stSleepingConstraints .= []
reportSLn "import.iface.create" 7 $ "Starting serialization."
i <- Bench.billTo [Bench.Serialization, Bench.BuildInterface] $ do
buildInterface file 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, _) -> return ()
(_, MainInterface ScopeCheck) -> return ()
_ -> Bench.billTo [Bench.Serialization] $ do
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 %= 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 <- use 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
errorWarningsOfTCErr :: TCErr -> TCM [TCWarning]
errorWarningsOfTCErr err = case err of
TypeError tcst cls -> case clValue cls of
NonFatalErrors{} -> return []
_ -> localState $ do
put tcst
ws <- getAllWarnings AllWarnings
return $ filter (not . isUnsolvedWarning . tcWarning) ws
_ -> return []
constructIScope :: Interface -> Interface
constructIScope i = billToPure [ Deserialization ] $
i{ iScope = publicModules $ iInsideScope i }
buildInterface
:: AbsolutePath
-> TopLevelInfo
-> [OptionsPragma]
-> TCM Interface
buildInterface file topLevel pragmas = do
reportSLn "import.iface" 5 "Building interface..."
let m = topLevelModuleName topLevel
scope' <- getScope
let scope = scope' { scopeCurrent = m }
builtin <- use stLocalBuiltins
ms <- getImports
mhs <- mapM (\ m -> (m,) <$> moduleHash m) $ Set.toList ms
foreignCode <- use stForeignCode
display <- HMap.filter (not . null) . HMap.map (filter isClosed) <$> use stImportsDisplayForms
(display, sig) <- eliminateDeadCode display =<< getSignature
userwarns <- use stLocalUserWarnings
syntaxInfo <- use stSyntaxInfo
patsyns <- killRange <$> getPatternSyns
h <- liftIO $ hashFile file
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 = h
, iImportedModules = mhs
, iModuleName = m
, iScope = empty
, iInsideScope = topLevelScope topLevel
, iSignature = sig
, iDisplayForms = display
, iUserWarnings = userwarns
, iBuiltin = builtin'
, iForeignCode = foreignCode
, iHighlighting = syntaxInfo
, iPragmaOptions = pragmas
, 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