module Agda.TypeChecking.Monad.Options where
import Prelude hiding (mapM)
import Control.Monad.Reader hiding (mapM)
import Control.Monad.Writer
import Data.Maybe
import System.Directory
import System.FilePath
import {-# SOURCE #-} Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Warnings
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Monad.Benchmark
import Agda.Interaction.Options
import qualified Agda.Interaction.Options.Lenses as Lens
import Agda.Interaction.Library
import Agda.Utils.FileName
import Agda.Utils.Maybe
import Agda.Utils.Pretty
import Agda.Utils.Except
import Agda.Utils.Impossible
setPragmaOptions :: PragmaOptions -> TCM ()
setPragmaOptions opts = do
stPragmaOptions `modifyTCLens` Lens.mapSafeMode (Lens.getSafeMode opts ||)
clo <- commandLineOptions
let unsafe = unsafePragmaOptions opts
when (Lens.getSafeMode opts && not (null unsafe)) $ warning $ SafeFlagPragma unsafe
ok <- liftIO $ runOptM $ checkOpts (clo { optPragmaOptions = opts })
case ok of
Left err -> __IMPOSSIBLE__
Right opts -> do
stPragmaOptions `setTCLens` optPragmaOptions opts
updateBenchmarkingStatus
setCommandLineOptions :: CommandLineOptions -> TCM ()
setCommandLineOptions opts = do
root <- liftIO (absolute =<< getCurrentDirectory)
setCommandLineOptions' root opts
setCommandLineOptions'
:: AbsolutePath
-> CommandLineOptions
-> TCM ()
setCommandLineOptions' root opts = do
z <- liftIO $ runOptM $ checkOpts opts
case z of
Left err -> __IMPOSSIBLE__
Right opts -> do
incs <- case optAbsoluteIncludePaths opts of
[] -> do
opts' <- setLibraryPaths root opts
let incs = optIncludePaths opts'
setIncludeDirs incs root
getIncludeDirs
incs -> return incs
modifyTC $ Lens.setCommandLineOptions opts{ optAbsoluteIncludePaths = incs }
setPragmaOptions (optPragmaOptions opts)
updateBenchmarkingStatus
libToTCM :: LibM a -> TCM a
libToTCM m = do
(z, warns) <- liftIO $ runWriterT $ runExceptT m
unless (null warns) $ warnings $ map LibraryWarning warns
case z of
Left s -> typeError $ GenericDocError s
Right x -> return x
setLibraryPaths
:: AbsolutePath
-> CommandLineOptions
-> TCM CommandLineOptions
setLibraryPaths root o =
setLibraryIncludes =<< addDefaultLibraries root o
setLibraryIncludes :: CommandLineOptions -> TCM CommandLineOptions
setLibraryIncludes o
| or [ not $ optUseLibs o
, optShowVersion o ] = pure o
| otherwise = do
let libs = optLibraries o
installed <- libToTCM $ getInstalledLibraries (optOverrideLibrariesFile o)
paths <- libToTCM $ libraryIncludePaths (optOverrideLibrariesFile o) installed libs
return o{ optIncludePaths = paths ++ optIncludePaths o }
addDefaultLibraries
:: AbsolutePath
-> CommandLineOptions
-> TCM CommandLineOptions
addDefaultLibraries root o
| or [ not $ null $ optLibraries o
, not $ optUseLibs o
, optShowVersion o ] = pure o
| otherwise = do
(libs, incs) <- libToTCM $ getDefaultLibraries (filePath root) (optDefaultLibs o)
return o{ optIncludePaths = incs ++ optIncludePaths o, optLibraries = libs }
setOptionsFromPragma :: OptionsPragma -> TCM ()
setOptionsFromPragma ps = do
opts <- commandLineOptions
z <- liftIO $ runOptM (parsePragmaOptions ps opts)
case z of
Left err -> typeError $ GenericError err
Right opts' -> setPragmaOptions opts'
enableDisplayForms :: MonadTCEnv m => m a -> m a
enableDisplayForms =
localTC $ \e -> e { envDisplayFormsEnabled = True }
disableDisplayForms :: MonadTCEnv m => m a -> m a
disableDisplayForms =
localTC $ \e -> e { envDisplayFormsEnabled = False }
displayFormsEnabled :: MonadTCEnv m => m Bool
displayFormsEnabled = asksTC envDisplayFormsEnabled
getIncludeDirs :: HasOptions m => m [AbsolutePath]
getIncludeDirs = do
incs <- optAbsoluteIncludePaths <$> commandLineOptions
case incs of
[] -> __IMPOSSIBLE__
_ -> return incs
setIncludeDirs :: [FilePath]
-> AbsolutePath
-> TCM ()
setIncludeDirs incs root = do
oldIncs <- getsTC Lens.getAbsoluteIncludePaths
incs <- return $ if null incs then ["."] else incs
incs <- return $ map (mkAbsolute . (filePath root </>)) incs
libdir <- liftIO $ defaultLibDir
let primdir = mkAbsolute $ libdir </> "prim"
incs <- return $ incs ++ [primdir]
reportSDoc "setIncludeDirs" 10 $ return $ vcat
[ "Old include directories:"
, nest 2 $ vcat $ map pretty oldIncs
, "New include directories:"
, nest 2 $ vcat $ map pretty incs
]
when (oldIncs /= incs) $ do
ho <- getInteractionOutputCallback
tcWarnings <- useTC stTCWarnings
resetAllState
setTCLens stTCWarnings tcWarnings
setInteractionOutputCallback ho
Lens.putAbsoluteIncludePaths incs
setInputFile :: FilePath -> TCM ()
setInputFile file =
do opts <- commandLineOptions
setCommandLineOptions $
opts { optInputFile = Just file }
getInputFile :: TCM AbsolutePath
getInputFile = fromMaybeM __IMPOSSIBLE__ $
getInputFile'
getInputFile' :: TCM (Maybe AbsolutePath)
getInputFile' = mapM (liftIO . absolute) =<< do
optInputFile <$> commandLineOptions
hasInputFile :: HasOptions m => m Bool
hasInputFile = isJust <$> optInputFile <$> commandLineOptions
isPropEnabled :: HasOptions m => m Bool
isPropEnabled = optProp <$> pragmaOptions
{-# SPECIALIZE hasUniversePolymorphism :: TCM Bool #-}
hasUniversePolymorphism :: HasOptions m => m Bool
hasUniversePolymorphism = optUniversePolymorphism <$> pragmaOptions
enableCaching :: HasOptions m => m Bool
enableCaching = optCaching <$> pragmaOptions
showImplicitArguments :: HasOptions m => m Bool
showImplicitArguments = optShowImplicit <$> pragmaOptions
showIrrelevantArguments :: HasOptions m => m Bool
showIrrelevantArguments = optShowIrrelevant <$> pragmaOptions
withShowAllArguments :: ReadTCState m => m a -> m a
withShowAllArguments = withShowAllArguments' True
withShowAllArguments' :: ReadTCState m => Bool -> m a -> m a
withShowAllArguments' yes = withPragmaOptions $ \ opts ->
opts { optShowImplicit = yes, optShowIrrelevant = yes }
withPragmaOptions :: ReadTCState m => (PragmaOptions -> PragmaOptions) -> m a -> m a
withPragmaOptions = locallyTCState stPragmaOptions
ignoreInterfaces :: HasOptions m => m Bool
ignoreInterfaces = optIgnoreInterfaces <$> commandLineOptions
ignoreAllInterfaces :: HasOptions m => m Bool
ignoreAllInterfaces = optIgnoreAllInterfaces <$> commandLineOptions
positivityCheckEnabled :: HasOptions m => m Bool
positivityCheckEnabled = not . optDisablePositivity <$> pragmaOptions
{-# SPECIALIZE typeInType :: TCM Bool #-}
typeInType :: HasOptions m => m Bool
typeInType = not . optUniverseCheck <$> pragmaOptions
etaEnabled :: HasOptions m => m Bool
etaEnabled = optEta <$> pragmaOptions
maxInstanceSearchDepth :: HasOptions m => m Int
maxInstanceSearchDepth = optInstanceSearchDepth <$> pragmaOptions
maxInversionDepth :: HasOptions m => m Int
maxInversionDepth = optInversionMaxDepth <$> pragmaOptions