module Agda.Interaction.Imports where
import Prelude hiding (catch)
import Control.Monad.Error
import Control.Monad.State
import qualified Control.Exception as E
import qualified Data.Map as Map
import qualified Data.List as List
import qualified Data.Set as Set
import qualified Data.ByteString.Lazy as BS
import Data.Generics
import Data.List
import Data.Map (Map)
import Data.Set (Set)
import System.Directory
import System.Time
import qualified Agda.Utils.IO.Locale as LocIO
import System.FilePath hiding (splitPath)
import Agda.Syntax.Position
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Parser
import Agda.Syntax.Scope.Base
import Agda.Syntax.Scope.Monad
import Agda.Syntax.Translation.ConcreteToAbstract
import Agda.Syntax.Internal
import Agda.Termination.TermCheck
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Serialise
import Agda.TypeChecking.Primitive
import Agda.TypeChecker
import Agda.Interaction.FindFile
import Agda.Interaction.Options
import Agda.Interaction.Highlighting.Precise (HighlightingInfo)
import Agda.Interaction.Highlighting.Generate
import Agda.Interaction.Highlighting.Vim
import qualified Agda.Interaction.Highlighting.Range as R
import Agda.Utils.FileName
import Agda.Utils.Monad
import Agda.Utils.IO.Binary
import Agda.Utils.Pretty
import Agda.Utils.Impossible
#include "../undefined.h"
data RelativeTo
= ProjectRoot
| CurrentDir
moduleName :: FilePath -> TCM C.TopLevelModuleName
moduleName file = do
file <- liftIO (absolute file)
m <- moduleName' file
checkModuleName m file
return m
moduleName' :: AbsolutePath -> TCM C.TopLevelModuleName
moduleName' file = liftIO $ do
C.topLevelModuleName <$> parseFile' moduleParser file
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 <- getBuiltinThings
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)
case Map.toList $ Map.intersection bs bi of
[] -> return ()
(b, Builtin x):_ -> typeError $ DuplicateBuiltinBinding b x x
(_, Prim{}):_ -> __IMPOSSIBLE__
addImportedThings sig bi (iHaskellImports 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 = do
PrimImpl _ pf <- lookupPrimitiveFunction x
return (x, Prim pf)
addImportedThings ::
Signature -> BuiltinThings PrimFun -> Set String -> TCM ()
addImportedThings isig ibuiltin hsImports =
modify $ \st -> st
{ stImports = unionSignatures [stImports st, isig]
, stImportedBuiltins = Map.union (stImportedBuiltins st) ibuiltin
, stHaskellImports = Set.union (stHaskellImports st) hsImports
}
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
liftIO $ LocIO.putStrLn $
" visited: " ++ intercalate ", " (map (render . pretty) visited)
i <- fst <$> getInterface x
addImport x
return (iModuleName i `withRangesOfQ` mnameToConcrete x, iScope i)
alreadyVisited :: C.TopLevelModuleName ->
TCM (Interface, Either Warnings ClockTime) ->
TCM (Interface, Either Warnings ClockTime)
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, Right $ miTimeStamp mi)
_ -> 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)
case wt of
Left _ -> do
t <- liftIO getClockTime
visitModule $ ModuleInfo
{ miInterface = i
, miWarnings = True
, miTimeStamp = t
}
Right t ->
visitModule $ ModuleInfo
{ miInterface = i
, miWarnings = False
, miTimeStamp = t
}
return r
data Warnings = Warnings
{ terminationProblems :: [([QName], [R.Range])]
, unsolvedMetaVariables :: [Range]
, unsolvedConstraints :: Constraints
}
warningsToError :: Warnings -> TypeError
warningsToError (Warnings [] [] []) = __IMPOSSIBLE__
warningsToError (Warnings _ w@(_:_) _) = UnsolvedMetas w
warningsToError (Warnings _ _ w@(_:_)) = UnsolvedConstraints w
warningsToError (Warnings w@(_:_) _ _) = TerminationCheckFailed w
typeCheck :: FilePath
-> RelativeTo
-> Maybe [AbsolutePath]
-> TCM (Interface, Maybe Warnings)
typeCheck f relativeTo oldIncs = do
f <- liftIO (absolute f)
m <- moduleName' f
makeIncludeDirsAbsolute =<< case relativeTo of
CurrentDir -> liftIO (absolute =<< getCurrentDirectory)
ProjectRoot -> return $ C.projectRoot f m
incs <- getIncludeDirs
case oldIncs of
Just incs' | incs' /= incs -> resetState
_ -> return ()
checkModuleName m f
(i, wt) <- getInterface' m True
return (i, case wt of
Left w -> Just w
Right _ -> Nothing)
getInterface :: ModuleName -> TCM (Interface, ClockTime)
getInterface x = do
(i, wt) <- getInterface' (toTopLevelModuleName x) False
case wt of
Left w -> typeError $ warningsToError w
Right t -> return (i, t)
getInterface' :: C.TopLevelModuleName
-> Bool
-> TCM (Interface, Either Warnings ClockTime)
getInterface' x includeStateChanges =
bracket (stPragmaOptions <$> get)
(unless includeStateChanges .
setCommandLineOptions PragmaOptions) $ \_ -> do
setCommandLineOptions PersistentOptions . stPersistentOptions =<< get
alreadyVisited x $ addImportCycleCheck x $ do
file <- findFile x
reportSLn "import.iface" 10 $ " Check for cycle"
checkForImportCycle
uptodate <- ifM ignoreInterfaces
(return False)
(liftIO $ filePath (toIFile file)
`isNewerThan`
filePath file)
reportSLn "import.iface" 5 $
" " ++ render (pretty x) ++ " is " ++
(if uptodate then "" else "not ") ++ "up-to-date."
(stateChangesIncluded, (i, wt)) <-
if uptodate then skip x file else typeCheck file
let topLevelName = toTopLevelModuleName $ iModuleName i
unless (topLevelName == x) $ do
checkModuleName topLevelName file
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) $ mergeInterface i
modify (\s -> s { stCurrentModule = Just $ iModuleName i })
case wt of
Left w -> return ()
Right t -> storeDecodedModule i t
return (i, wt)
where
skip x file = do
let ifile = filePath $ toIFile file
t <- liftIO $ getModificationTime ifile
mm <- getDecodedModule x
(cached, mi) <- case mm of
Just (mi, mt) ->
if mt < t
then do dropDecodedModule x
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"
typeCheck file
Just i -> do
reportSLn "import.iface" 5 $ " imports: " ++ show (iImportedModules i)
ts <- map snd <$> mapM getInterface (iImportedModules i)
if any (> t) ts
then do
typeCheck file
else do
reportSLn "" 1 $
"Skipping " ++ render (pretty x) ++
" (" ++ (if cached then "cached" else ifile) ++ ")."
return (False, (i, Right t))
typeCheck file = do
reportSLn "" 1 $ "Checking " ++ render (pretty x) ++ " (" ++ filePath file ++ ")."
if includeStateChanges then do
r <- createInterface file x
sig <- getSignature
addImportedThings sig Map.empty Set.empty
setSignature emptySignature
return (True, r)
else do
ms <- getImportPath
mf <- stModuleToSource <$> get
vs <- getVisitedModules
ds <- getDecodedModules
opts <- stPersistentOptions <$> get
trace <- getTrace
isig <- getImportedSignature
ibuiltin <- gets stImportedBuiltins
r <- liftIO $ runTCM $
withImportPath ms $ do
setDecodedModules ds
setTrace trace
setCommandLineOptions PersistentOptions opts
modify $ \s -> s { stModuleToSource = mf }
setVisitedModules vs
addImportedThings isig ibuiltin Set.empty
r <- createInterface file x
mf <- stModuleToSource <$> get
vs <- getVisitedModules
ds <- getDecodedModules
isig <- getImportedSignature
ibuiltin <- gets stImportedBuiltins
hsImports <- getHaskellImports
return (r, do
modify $ \s -> s { stModuleToSource = mf }
setVisitedModules vs
setDecodedModules ds
addImportedThings isig ibuiltin hsImports)
case r of
Left err -> throwError err
Right (result, update) -> do
update
return (False, result)
readInterface :: FilePath -> TCM (Maybe Interface)
readInterface file = do
(s, close) <- liftIO $ readBinaryFile' file
do i <- liftIO . E.evaluate =<< decode s
liftIO close
return i
`catchError` \e -> liftIO close >> handler e
`catchError` handler
where
handler e = case errError e of
IOException _ e -> do
liftIO $ LocIO.putStrLn $ "IO exception: " ++ show e
return Nothing
_ -> throwError e
writeInterface :: FilePath -> Interface -> TCM ClockTime
writeInterface file i = do
encodeFile file i
liftIO $ getModificationTime file
`catchError` \e -> do
reportSLn "" 1 $
"Failed to write interface " ++ file ++ "."
liftIO $
whenM (doesFileExist file) $ removeFile file
throwError e
createInterface
:: AbsolutePath
-> C.TopLevelModuleName
-> TCM (Interface, Either Warnings ClockTime)
createInterface file mname = do
reportSLn "import.iface.create" 5 $
"Creating interface for " ++ render (pretty mname) ++ "."
verboseS "import.iface.create" 10 $ do
visited <- Map.keys <$> getVisitedModules
liftIO $ LocIO.putStrLn $
" visited: " ++ intercalate ", " (map (render . pretty) visited)
previousHsImports <- getHaskellImports
(pragmas, top) <- liftIO $ parseFile' moduleParser file
pragmas <- concat <$> concreteToAbstract_ pragmas
setOptionsFromPragmas pragmas
topLevel <- concreteToAbstract_ (TopLevel top)
termErrs <- catchError (do
checkDecls (topLevelDecls topLevel)
termErrs <- ifM (optTerminationCheck <$> commandLineOptions)
(termDecls $ topLevelDecls topLevel)
(return [])
mapM_ (\e -> reportSLn "term.warn.no" 2
(show (fst e) ++
" does NOT pass the termination checker."))
termErrs
return termErrs
) (\e -> do
case rStart $ getRange e of
Just (Pn { srcFile = Just f }) | f == file -> do
syntaxInfo <- generateSyntaxInfo file (Just e) topLevel []
modFile <- stModuleToSource <$> get
case errHighlighting e of
Just _ -> __IMPOSSIBLE__
Nothing ->
throwError $ e { errHighlighting =
Just (syntaxInfo, modFile) }
_ -> throwError e
)
syntaxInfo <- generateSyntaxInfo file Nothing topLevel termErrs
whenM (optGenerateVimFile <$> commandLineOptions) $
withScope_ (insideScope topLevel) $ generateVimFile $ filePath file
unsolvedMetas <- List.nub <$> (mapM getMetaRange =<< getOpenMetas)
unless (null unsolvedMetas) $ do
unsolvedOK <- optAllowUnsolved <$> commandLineOptions
unless unsolvedOK $
typeError $ UnsolvedMetas unsolvedMetas
unsolvedConstraints <- getConstraints
unless (null unsolvedConstraints) $ do
unsolvedOK <- optAllowUnsolved <$> commandLineOptions
unless unsolvedOK $
typeError $ UnsolvedConstraints unsolvedConstraints
setScope $ outsideScope topLevel
reportSLn "scope.top" 50 $ "SCOPE " ++ show (insideScope topLevel)
i <- buildInterface topLevel syntaxInfo previousHsImports
if and [ null termErrs, null unsolvedMetas, null unsolvedConstraints ]
then do
t <- writeInterface (filePath $ toIFile file) i
return (i, Right t)
else
return (i, Left $ Warnings termErrs unsolvedMetas unsolvedConstraints)
buildInterface :: TopLevelInfo
-> HighlightingInfo
-> Set String
-> TCM Interface
buildInterface topLevel syntaxInfo previousHsImports = do
reportSLn "import.iface" 5 "Building interface..."
scope' <- getScope
let scope = scope' { scopeCurrent = m }
sig <- getSignature
builtin <- gets stLocalBuiltins
ms <- getImports
hsImps <- getHaskellImports
let builtin' = Map.mapWithKey (\x b -> fmap (const x) b) builtin
reportSLn "import.iface" 7 " instantiating all meta variables"
i <- instantiateFull $ Interface
{ iImportedModules = Set.toList ms
, iModuleName = m
, iScope = publicModules scope
, iInsideScope = insideScope topLevel
, iSignature = sig
, iBuiltin = builtin'
, iHaskellImports = Set.difference hsImps
previousHsImports
, iHighlighting = syntaxInfo
}
reportSLn "import.iface" 7 " interface complete"
return i
where m = topLevelModuleName topLevel
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