{-# LANGUAGE CPP #-}
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
data SourceInfo = SourceInfo
{ siSource :: Text
, siFileType :: FileType
, siModule :: C.Module
, siModuleName :: C.TopLevelModuleName
}
sourceInfo :: SourceFile -> TCM SourceInfo
sourceInfo (SourceFile 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) (iPartialDefs i) warns
reportSLn "import.iface.merge" 20 $
" Rebinding primitives " ++ show prim
mapM_ rebind prim
whenM (optConfluenceCheck <$> pragmaOptions) $ do
reportSLn "import.iface.confluence" 20 $ " Checking confluence of imported rewrite rules"
checkConfluenceOfRules $ concat $ HMap.elems $ sig ^. sigRewriteRules
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
-> Set QName
-> [TCWarning]
-> TCM ()
addImportedThings isig ibuiltin patsyns display userwarn partialdefs warnings = do
stImports `modifyTCLens` \ imp -> unionSignatures [imp, isig]
stImportedBuiltins `modifyTCLens` \ imp -> Map.union imp ibuiltin
stImportedUserWarnings `modifyTCLens` \ imp -> Map.union imp userwarn
stImportedPartialDefs `modifyTCLens` \ imp -> Set.union imp partialdefs
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
whenJust (iImportWarning i) $ warning . UserWarning
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
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
:: SourceFile
-> 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 = SourceFile $ 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 =
withIncreasedModuleNestingLevel $
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 $ srcFilePath file)))
`or2M` ignoreAllInterfaces
cached <- runMaybeT $ isCached x file
sourceH <- case msi of
Nothing -> liftIO $ hashTextFile (srcFilePath file)
Just si -> return $ hashText (siSource si)
ifaceH <- case cached of
Nothing -> do
mifile <- toIFile file
fmap fst <$> getInterfaceFileHashes mifile
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) $
typeError $ OverlappingProjects (srcFilePath 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
reportS "warning.import" 10
[ "module: " ++ show (C.moduleNameParts x)
, "WarningOnImport: " ++ show (iImportWarning 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.pretty $ o opts))
(coinfectiveOptions ++ infectiveOptions))
isCached
:: C.TopLevelModuleName
-> SourceFile
-> MaybeT TCM Interface
isCached x file = do
ifile <- MaybeT $ findInterfaceFile' file
mi <- MaybeT $ getDecodedModule x
h <- MaybeT $ fmap snd <$> getInterfaceFileHashes' ifile
guard $ iFullHash mi == h
return mi
getStoredInterface
:: C.TopLevelModuleName
-> SourceFile
-> MainInterface
-> Maybe SourceInfo
-> TCM (Bool, (Interface, MaybeWarnings))
getStoredInterface x file isMain msi = do
let fp = filePath $ srcFilePath file
let fallback = typeCheck x file isMain msi
ifile <- toIFile file
let ifp = filePath ifile
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 " ++ ifp
(False,) <$> readInterface ifile
else do
reportSLn "import.iface" 5 $ " using stored version of " ++ ifp
return (True, Just mi)
Nothing -> do
reportSLn "import.iface" 5 $ " no stored version, reading " ++ ifp
(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 fp)
(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 $ concat
[ " Changes in the following options in "
, prettyShow fp
, ", 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 fallback
else do
unless cached $ do
chaseMsg "Loading " x $ Just ifp
let ws = filter ((Strict.Just (srcFilePath file) ==) . tcWarningOrigin) (iWarnings i)
unless (null ws) $ reportSDoc "warning" 1 $ P.vcat $ P.prettyTCM <$> ws
return (False, (i, NoWarnings))
typeCheck
:: C.TopLevelModuleName
-> SourceFile
-> MainInterface
-> Maybe SourceInfo
-> TCM (Bool, (Interface, MaybeWarnings))
typeCheck x file isMain msi = do
let fp = filePath $ srcFilePath file
unless (includeStateChanges isMain) cleanCachedLog
let checkMsg = case isMain of
MainInterface ScopeCheck -> "Reading "
_ -> "Checking"
withMsgs = bracket_
(chaseMsg checkMsg x $ Just fp)
(const $ do ws <- getAllWarnings AllWarnings
let classified = classifyWarnings ws
let wa' = filter ((Strict.Just (srcFilePath file) ==) . tcWarningOrigin) (tcWarnings classified)
unless (null wa') $
reportSDoc "warning" 1 $ P.vcat $ P.prettyTCM <$> wa'
when (null (nonFatalErrors classified)) $ 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
partialdefs <- useTC stImportedPartialDefs
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 partialdefs []
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
-> SourceFile
-> TCM ()
highlightFromInterface i file = do
reportSLn "import.iface" 5 $
"Generating syntax info for " ++ filePath (srcFilePath file) ++
" (read from interface)."
printHighlightingInfo KeepHighlighting (iHighlighting i)
readInterface :: AbsolutePath -> TCM (Maybe Interface)
readInterface file = runMaybeT $ do
ifile <- MaybeT $ liftIO $ mkInterfaceFile file
MaybeT $ readInterface' ifile
readInterface' :: InterfaceFile -> TCM (Maybe Interface)
readInterface' file = do
let ifp = filePath $ intFilePath file
(s, close) <- liftIO $ readBinaryFile' ifp
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 :: AbsolutePath -> Interface -> TCM Interface
writeInterface file i = let fp = filePath file in do
reportSLn "import.iface.write" 5 $
"Writing interface file " ++ fp ++ "."
reportSLn "import.iface.write" 50 $
"Writing interface file with hash" ++ show (iFullHash i) ++ "."
i' <- encodeFile fp i
reportSLn "import.iface.write" 5 "Wrote interface file."
i <-
#if __GLASGOW_HASKELL__ >= 804
Bench.billTo [Bench.Deserialization] (decode i')
#else
return (Just i)
#endif
case i of
Just i -> return i
Nothing -> __IMPOSSIBLE__
`catchError` \e -> do
reportSLn "" 1 $
"Failed to write interface " ++ fp ++ "."
liftIO $
whenM (doesFileExist fp) $ removeFile fp
throwError e
removePrivates :: ScopeInfo -> ScopeInfo
removePrivates = over scopeModules $ fmap restrictPrivate
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
:: SourceFile
-> C.TopLevelModuleName
-> MainInterface
-> Maybe SourceInfo
-> TCM (Interface, MaybeWarnings)
createInterface file mname isMain msi =
Bench.billTo [Bench.TopModule mname] $
localTC (\e -> e { envCurrentPath = Just (srcFilePath 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
(srcFilePath 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 (srcFilePath 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: " <> prettyTCM warnings
unsolved <- getAllUnsolved
unless (null unsolved) $ reportSDoc "import.iface.create" 20 $
"collected unsolved: " <> prettyTCM unsolved
let warningInfo = compress $ foldMap warningHighlighting $ unsolved ++ warnings
stSyntaxInfo `modifyTCLens` \inf -> (inf `mappend` toks) `mappend` warningInfo
whenM (optGenerateVimFile <$> commandLineOptions) $
withScope_ scope $ generateVimFile $ filePath $ srcFilePath $ 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 =<< showGoals =<< getGoals
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 (scope ^. scopeCurrent) openMetasToPostulates
stAwakeConstraints `setTCLens` []
stSleepingConstraints `setTCLens` []
reportSLn "import.iface.create" 7 "Starting serialization."
i <- Bench.billTo [Bench.Serialization, Bench.BuildInterface] $
buildInterface source fileType topLevel options
reportS "tc.top" 101 $
"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."
i <- case (mallWarnings, isMain) of
(SomeWarnings allWarnings, _) -> do
reportSLn "import.iface.create" 7 "We have warnings, skipping writing interface file."
return i
(_, MainInterface ScopeCheck) -> do
reportSLn "import.iface.create" 7 "We are just scope-checking, skipping writing interface file."
return i
_ -> Bench.billTo [Bench.Serialization] $ do
reportSLn "import.iface.create" 7 "Actually calling writeInterface."
ifile <- 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 $ reportSLn "import.iface" 5 "Accumulated statistics."
return $ first constructIScope (i, mallWarnings)
getUniqueMetasRanges :: [MetaId] -> TCM [Range]
getUniqueMetasRanges = fmap (nubOn id) . 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 = set scopeCurrent m scope'
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
importwarn <- useTC stWarningOnImport
syntaxInfo <- useTC stSyntaxInfo
optionsUsed <- useTC stPragmaOptions
partialDefs <- useTC stLocalPartialDefs
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
, iImportWarning = importwarn
, iBuiltin = builtin'
, iForeignCode = foreignCode
, iHighlighting = syntaxInfo
, iPragmaOptions = pragmas
, iOptionsUsed = optionsUsed
, iPatternSyns = patsyns
, iWarnings = warnings
, iPartialDefs = partialDefs
}
reportSLn "import.iface" 7 " interface complete"
return i
getInterfaceFileHashes :: AbsolutePath -> TCM (Maybe (Hash, Hash))
getInterfaceFileHashes fp = runMaybeT $ do
mifile <- MaybeT $ liftIO $ mkInterfaceFile fp
MaybeT $ getInterfaceFileHashes' mifile
getInterfaceFileHashes' :: InterfaceFile -> TCM (Maybe (Hash, Hash))
getInterfaceFileHashes' fp = do
let ifile = filePath $ intFilePath fp
(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