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 Agda.TypeChecking.Monad.Debug (reportSDoc)
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
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
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