{-# LANGUAGE CPP #-}
module Agda.TypeChecking.Monad.Options where
import Prelude hiding (mapM)
import Control.Monad.Reader hiding (mapM)
import Control.Monad.Writer
import Control.Monad.State hiding (mapM)
import Data.Maybe
import Data.Traversable
import System.Directory
import System.FilePath
import Agda.Syntax.Internal
import Agda.Syntax.Common
import Agda.Syntax.Concrete
import {-# SOURCE #-} Agda.TypeChecking.Monad.Debug
import {-# SOURCE #-} Agda.TypeChecking.Errors
import Agda.TypeChecking.Warnings
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Monad.Benchmark
import {-# SOURCE #-} Agda.Interaction.FindFile
import Agda.Interaction.Options
import qualified Agda.Interaction.Options.Lenses as Lens
import Agda.Interaction.Response
import Agda.Interaction.Library
import Agda.Utils.Except ( MonadError(catchError) )
import Agda.Utils.FileName
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Pretty
import Agda.Utils.Trie (Trie)
import qualified Agda.Utils.Trie as Trie
import Agda.Utils.Except
import Agda.Utils.Either
#include "undefined.h"
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 = 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 :: TCM a -> TCM a
enableDisplayForms =
localTC $ \e -> e { envDisplayFormsEnabled = True }
disableDisplayForms :: TCM a -> TCM a
disableDisplayForms =
localTC $ \e -> e { envDisplayFormsEnabled = False }
displayFormsEnabled :: TCM Bool
displayFormsEnabled = asksTC envDisplayFormsEnabled
getIncludeDirs :: TCM [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 :: TCM 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 :: TCM Bool
enableCaching = optCaching <$> pragmaOptions
showImplicitArguments :: TCM Bool
showImplicitArguments = optShowImplicit <$> pragmaOptions
showIrrelevantArguments :: TCM Bool
showIrrelevantArguments = optShowIrrelevant <$> pragmaOptions
withShowAllArguments :: TCM a -> TCM a
withShowAllArguments = withShowAllArguments' True
withShowAllArguments' :: Bool -> TCM a -> TCM a
withShowAllArguments' yes = withPragmaOptions $ \ opts ->
opts { optShowImplicit = yes, optShowIrrelevant = yes }
withPragmaOptions :: (PragmaOptions -> PragmaOptions) -> TCM a -> TCM a
withPragmaOptions f cont = do
opts <- pragmaOptions
setPragmaOptions $ f opts
x <- cont
setPragmaOptions opts
return x
ignoreInterfaces :: TCM Bool
ignoreInterfaces = optIgnoreInterfaces <$> commandLineOptions
ignoreAllInterfaces :: TCM Bool
ignoreAllInterfaces = optIgnoreAllInterfaces <$> commandLineOptions
positivityCheckEnabled :: TCM Bool
positivityCheckEnabled = not . optDisablePositivity <$> pragmaOptions
{-# SPECIALIZE typeInType :: TCM Bool #-}
typeInType :: HasOptions m => m Bool
typeInType = not . optUniverseCheck <$> pragmaOptions
etaEnabled :: TCM Bool
etaEnabled = optEta <$> pragmaOptions
maxInstanceSearchDepth :: TCM Int
maxInstanceSearchDepth = optInstanceSearchDepth <$> pragmaOptions
maxInversionDepth :: TCM Int
maxInversionDepth = optInversionMaxDepth <$> pragmaOptions
{-# SPECIALIZE getVerbosity :: TCM (Trie String Int) #-}
getVerbosity :: HasOptions m => m (Trie String Int)
getVerbosity = optVerbose <$> pragmaOptions
type VerboseKey = String
parseVerboseKey :: VerboseKey -> [String]
parseVerboseKey = wordsBy (`elem` (".:" :: String))
{-# SPECIALIZE hasVerbosity :: VerboseKey -> Int -> TCM Bool #-}
hasVerbosity :: HasOptions m => VerboseKey -> Int -> m Bool
hasVerbosity k n | n < 0 = __IMPOSSIBLE__
| otherwise = do
t <- getVerbosity
let ks = parseVerboseKey k
m = last $ 0 : Trie.lookupPath ks t
return (n <= m)
{-# SPECIALIZE hasExactVerbosity :: VerboseKey -> Int -> TCM Bool #-}
hasExactVerbosity :: HasOptions m => VerboseKey -> Int -> m Bool
hasExactVerbosity k n =
(Just n ==) . Trie.lookup (parseVerboseKey k) <$> getVerbosity
{-# SPECIALIZE whenExactVerbosity :: VerboseKey -> Int -> TCM () -> TCM () #-}
whenExactVerbosity :: MonadTCM tcm => VerboseKey -> Int -> tcm () -> tcm ()
whenExactVerbosity k n = whenM $ liftTCM $ hasExactVerbosity k n
{-# SPECIALIZE verboseS :: VerboseKey -> Int -> TCM () -> TCM () #-}
{-# SPECIALIZE verboseS :: MonadTCM tcm => VerboseKey -> Int -> tcm () -> tcm () #-}
verboseS :: (MonadTCEnv m, HasOptions m) => VerboseKey -> Int -> m () -> m ()
verboseS k n action = whenM (hasVerbosity k n) $ locallyTC eIsDebugPrinting (const True) action
verbosity :: VerboseKey -> Lens' Int TCState
verbosity k = stPragmaOptions . verbOpt . Trie.valueAt (parseVerboseKey k) . defaultTo 0
where
verbOpt :: Lens' (Trie String Int) PragmaOptions
verbOpt f opts = f (optVerbose opts) <&> \ v -> opts { optVerbose = v }
defaultTo :: Eq a => a -> Lens' a (Maybe a)
defaultTo x f m = f (fromMaybe x m) <&> \ v -> if v == x then Nothing else Just v