module Agda.Interaction.Imports where
import Prelude
import Control.Monad.Error
import Control.Monad.Reader
import Control.Monad.State
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 Data.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 Paths_Agda (getDataFileName)
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.Reduce
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Serialise
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Monad.Benchmark (billTop, reimburseTop)
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TheTypeChecker
import Agda.Interaction.FindFile
import Agda.Interaction.Options
import qualified Agda.Interaction.Options.Lenses as Lens
import Agda.Interaction.Highlighting.Precise (HighlightingInfo)
import Agda.Interaction.Highlighting.Generate
import Agda.Interaction.Highlighting.Vim
import Agda.Utils.FileName
import Agda.Utils.Monad
import Agda.Utils.IO.Binary
import Agda.Utils.Pretty
import Agda.Utils.Fresh
import Agda.Utils.Time
import Agda.Utils.Hash
import qualified Agda.Utils.Trie as Trie
#include "../undefined.h"
import Agda.Utils.Impossible
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 ]
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 (iHaskellImports i) (iPatternSyns i)
reportSLn "import.iface.merge" 20 $
" Rebinding primitives " ++ show prim
prim <- Map.fromList <$> mapM rebind prim
modify $ \st -> st { stImportedBuiltins = stImportedBuiltins st `Map.union` prim
}
where
rebind (x, q) = do
PrimImpl _ pf <- lookupPrimitiveFunction x
return (x, Prim $ pf { primFunName = q })
addImportedThings ::
Signature -> BuiltinThings PrimFun -> Set String -> A.PatternSynDefns -> TCM ()
addImportedThings isig ibuiltin hsImports patsyns = do
modify $ \st -> st
{ stImports = unionSignatures [stImports st, isig]
, stImportedBuiltins = Map.union (stImportedBuiltins st) ibuiltin
, stHaskellImports = Set.union (stHaskellImports st) hsImports
, stPatternSynImports = Map.union (stPatternSynImports st) patsyns
}
addSignatureInstances isig
scopeCheckImport :: ModuleName -> TCM (ModuleName, Map ModuleName Scope)
scopeCheckImport x = do
reportSLn "import.scope" 5 $ "Scope checking " ++ show x
verboseS "import.scope" 10 $ do
visited <- Map.keys <$> getVisitedModules
reportSLn "import.scope" 10 $
" visited: " ++ intercalate ", " (map (render . pretty) visited)
i <- reimburseTop Bench.Scoping $ getInterface x
addImport x
return (iModuleName i `withRangesOfQ` mnameToConcrete x, iScope i)
data MaybeWarnings = NoWarnings | SomeWarnings Warnings
hasWarnings :: MaybeWarnings -> Bool
hasWarnings NoWarnings = False
hasWarnings SomeWarnings{} = True
alreadyVisited :: C.TopLevelModuleName ->
TCM (Interface, MaybeWarnings) ->
TCM (Interface, MaybeWarnings)
alreadyVisited x getIface = do
mm <- getVisitedModule x
case mm of
Just mi | not (miWarnings mi) -> do
reportSLn "import.visit" 10 $ " Already visited " ++ render (pretty x)
return (miInterface mi, NoWarnings)
_ -> do
reportSLn "import.visit" 5 $ " Getting interface for " ++ render (pretty x)
r@(i, wt) <- getIface
reportSLn "import.visit" 5 $ " Now we've looked at " ++ render (pretty x)
visitModule $ ModuleInfo
{ miInterface = i
, miWarnings = hasWarnings wt
}
return r
typeCheckMain :: AbsolutePath -> TCM (Interface, MaybeWarnings)
typeCheckMain f = do
reportSLn "import.main" 10 $ "Importing the primitive modules."
libpath <- liftIO $ getDataFileName "lib"
reportSLn "import.main" 20 $ "Library path = " ++ show libpath
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 $
libpath </> "prim" </> "Agda" </> "Primitive.agda"
reportSLn "import.main" 10 $ "Done importing the primitive modules."
typeCheck f
typeCheck :: AbsolutePath -> TCM (Interface, MaybeWarnings)
typeCheck f = do
m <- moduleName f
getInterface' m True
getInterface :: ModuleName -> TCM Interface
getInterface = getInterface_ . toTopLevelModuleName
getInterface_ :: C.TopLevelModuleName -> TCM Interface
getInterface_ x = do
(i, wt) <- getInterface' x False
case wt of
SomeWarnings w -> warningsToError w
NoWarnings -> return i
getInterface' :: C.TopLevelModuleName
-> Bool
-> TCM (Interface, MaybeWarnings)
getInterface' x includeStateChanges =
withIncreasedModuleNestingLevel $
bracket_ (stPragmaOptions <$> get)
(unless includeStateChanges . setPragmaOptions) $ do
setCommandLineOptions . stPersistentOptions . stPersistent =<< get
alreadyVisited x $ addImportCycleCheck x $ do
file <- findFile x
reportSLn "import.iface" 10 $ " Check for cycle"
checkForImportCycle
uptodate <- billTop Bench.Import $ do
ignore <- ignoreInterfaces
cached <- isCached 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 $
" " ++ render (pretty x) ++ " is " ++
(if uptodate then "" else "not ") ++ "up-to-date."
(stateChangesIncluded, (i, wt)) <-
if uptodate then skip file else typeCheckThe file
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
billTop Bench.Highlighting $
ifTopLevelAndHighlightingLevelIs NonInteractive $
highlightFromInterface i file
modify (\s -> s { stCurrentModule = Just $ iModuleName i })
case wt of
SomeWarnings w -> return ()
NoWarnings -> storeDecodedModule i
return (i, wt)
where
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
chaseMsg kind file = do
nesting <- envModuleNestingLevel <$> ask
let s = genericReplicate nesting ' ' ++ kind ++
" " ++ render (pretty x) ++
case file of
Nothing -> "."
Just f -> " (" ++ f ++ ")."
reportSLn "import.chase" 1 s
skip file = do
let ifile = filePath $ toIFile file
h <- fmap snd <$> getInterfaceFileHashes ifile
mm <- getDecodedModule x
(cached, mi) <- billTop 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"
typeCheckThe file
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
typeCheckThe file
else do
unless cached $ chaseMsg "Skipping" (Just ifile)
mapM_ setOptionsFromPragma (iPragmaOptions i)
return (False, (i, NoWarnings))
typeCheckThe file = do
let withMsgs = bracket_
(chaseMsg "Checking" $ Just $ filePath file)
(const $ chaseMsg "Finished" Nothing)
if includeStateChanges then do
r <- withMsgs $ createInterface file x
sig <- getSignature
patsyns <- getPatternSyns
addImportedThings sig Map.empty Set.empty patsyns
setSignature emptySignature
setPatternSyns Map.empty
return (True, r)
else do
ms <- getImportPath
nesting <- asks envModuleNestingLevel
range <- asks envRange
call <- asks envCall
mf <- gets stModuleToSource
vs <- getVisitedModules
ds <- getDecodedModules
opts <- stPersistentOptions . stPersistent <$> get
isig <- getImportedSignature
ibuiltin <- gets stImportedBuiltins
ipatsyns <- getPatternSynImports
ho <- getInteractionOutputCallback
r <- freshTCM $
withImportPath ms $
local (\e -> e { envModuleNestingLevel = nesting
, envRange = range
, envCall = call
}) $ do
setDecodedModules ds
setCommandLineOptions opts
setInteractionOutputCallback ho
modify $ \s -> s { stModuleToSource = mf
}
setVisitedModules vs
addImportedThings isig ibuiltin Set.empty ipatsyns
r <- withMsgs $ createInterface file x
mf <- stModuleToSource <$> get
ds <- getDecodedModules
return (r, do
modify $ \s -> s { 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) ->
skip file
_ -> return (False, r)
highlightFromInterface
:: Interface
-> AbsolutePath
-> TCM ()
highlightFromInterface i file = do
reportSLn "import.iface" 5 $
"Generating syntax info for " ++ filePath file ++
" (read from interface)."
printHighlightingInfo (iHighlighting i)
readInterface :: FilePath -> TCM (Maybe Interface)
readInterface file = do
(s, close) <- liftIO $ readBinaryFile' file
do i <- liftIO . E.evaluate =<< decodeInterface s
liftIO close
return i
`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
createInterface
:: AbsolutePath
-> C.TopLevelModuleName
-> TCM (Interface, MaybeWarnings)
createInterface file mname =
local (\e -> e { envCurrentPath = file }) $ do
modFile <- stModuleToSource <$> get
fileTokenInfo <- billTop Bench.Highlighting $ generateTokenInfo file
modify $ \st -> st { stTokens = fileTokenInfo }
reportSLn "import.iface.create" 5 $
"Creating interface for " ++ render (pretty mname) ++ "."
verboseS "import.iface.create" 10 $ do
visited <- Map.keys <$> getVisitedModules
reportSLn "import.iface.create" 10 $
" visited: " ++ intercalate ", " (map (render . pretty) visited)
previousHsImports <- getHaskellImports
(pragmas, top) <- billTop Bench.Parsing $
liftIO $ parseFile' moduleParser file
pragmas <- concat <$> concreteToAbstract_ pragmas
let getOptions (A.OptionsPragma opts) = Just opts
getOptions _ = Nothing
options = catMaybes $ map getOptions pragmas
mapM_ setOptionsFromPragma options
topLevel <- billTop Bench.Scoping $
concreteToAbstract_ (TopLevel file top)
let ds = topLevelDecls topLevel
billTop Bench.Highlighting $ do
ifTopLevelAndHighlightingLevelIs NonInteractive $ do
printHighlightingInfo fileTokenInfo
mapM_ (\ d -> generateAndPrintSyntaxInfo d Partial) ds
billTop Bench.Typing $ checkDecls ds
unfreezeMetas
verboseS "profile.metas" 10 $ do
MetaId n <- fresh
tickN "metas" (fromIntegral n)
billTop Bench.Highlighting $ do
ifTopLevelAndHighlightingLevelIs NonInteractive $
printHighlightingInfo . stTokens =<< get
modify $ \st ->
st { stTokens = mempty
, stSyntaxInfo = stSyntaxInfo st `mappend` stTokens st
}
whenM (optGenerateVimFile <$> commandLineOptions) $
withScope_ (insideScope topLevel) $ generateVimFile $ filePath file
setScope $ outsideScope topLevel
reportSLn "scope.top" 50 $ "SCOPE " ++ show (insideScope topLevel)
syntaxInfo <- stSyntaxInfo <$> get
i <- billTop Bench.Serialization $ do
buildInterface file topLevel syntaxInfo previousHsImports options
termErrs <- Fold.toList <$> stTermErrs <$> get
unsolvedMetas <- List.nub <$> (mapM getMetaRange =<< getOpenMetas)
unsolvedConstraints <- getAllConstraints
interactionPoints <- getInteractionPoints
ifTopLevelAndHighlightingLevelIs NonInteractive $
printUnsolvedInfo
r <- if and [ null termErrs, null unsolvedMetas, null unsolvedConstraints, null interactionPoints ]
then billTop Bench.Serialization $ do
let ifile = filePath $ toIFile file
writeInterface ifile i
return (i, NoWarnings)
else do
termErr <- if null termErrs then return Nothing else Just <$> do
typeError_ $ TerminationCheckFailed termErrs
return (i, SomeWarnings $ Warnings termErr unsolvedMetas unsolvedConstraints)
verboseS "profile" 1 $ do
stats <- Map.toList <$> getStatistics
case stats of
[] -> return ()
_ -> reportS "profile" 1 $ unlines $
[ "Ticks for " ++ show (pretty mname) ] ++
[ " " ++ s ++ " = " ++ show n
| (s, n) <- sortBy (compare `on` snd) stats ]
return r
buildInterface
:: AbsolutePath
-> TopLevelInfo
-> HighlightingInfo
-> Set String
-> [OptionsPragma]
-> TCM Interface
buildInterface file topLevel syntaxInfo previousHsImports pragmas = do
reportSLn "import.iface" 5 "Building interface..."
let m = topLevelModuleName topLevel
scope' <- getScope
let scope = scope' { scopeCurrent = m }
sig <- getSignature
builtin <- gets stLocalBuiltins
ms <- getImports
mhs <- mapM (\ m -> (m,) <$> moduleHash m) $ Set.toList ms
hsImps <- getHaskellImports
patsyns <- getPatternSyns
h <- liftIO $ hashFile file
let builtin' = Map.mapWithKey (\ x b -> (x,) . primFunName <$> b) builtin
reportSLn "import.iface" 7 " instantiating all meta variables"
i <- instantiateFull $ Interface
{ iSourceHash = h
, iImportedModules = mhs
, iModuleName = m
, iScope = publicModules scope
, iInsideScope = insideScope topLevel
, iSignature = sig
, iBuiltin = builtin'
, iHaskellImports = hsImps `Set.difference` previousHsImports
, iHighlighting = syntaxInfo
, iPragmaOptions = pragmas
, iPatternSyns = patsyns
}
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
safeReadInterface :: FilePath -> TCM (Maybe Interface)
safeReadInterface ifile = do
exist <- liftIO $ doesFileExist ifile
if exist then readInterface ifile
else return Nothing
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