{-# LANGUAGE CPP #-}
module Agda.TypeChecking.Monad.Options where
import Prelude hiding (mapM)
import Control.Monad.Reader hiding (mapM)
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 %= Lens.mapSafeMode (Lens.getSafeMode opts ||)
clo <- commandLineOptions
let unsafe = unsafePragmaOptions opts
when (Lens.getSafeMode clo && not (null unsafe)) $ warning $ SafeFlagPragma unsafe
ok <- liftIO $ runOptM $ checkOpts (clo { optPragmaOptions = opts })
case ok of
Left err -> __IMPOSSIBLE__
Right opts -> do
stPragmaOptions .= optPragmaOptions opts
updateBenchmarkingStatus
setCommandLineOptions :: CommandLineOptions -> TCM ()
setCommandLineOptions = setCommandLineOptions' CurrentDir
setCommandLineOptions' :: RelativeTo -> CommandLineOptions -> TCM ()
setCommandLineOptions' relativeTo opts = do
z <- liftIO $ runOptM $ checkOpts opts
case z of
Left err -> __IMPOSSIBLE__
Right opts -> do
incs <- case optAbsoluteIncludePaths opts of
[] -> do
opts' <- setLibraryPaths relativeTo opts
let incs = optIncludePaths opts'
setIncludeDirs incs relativeTo
getIncludeDirs
incs -> return incs
modify $ Lens.setCommandLineOptions opts{ optAbsoluteIncludePaths = incs }
setPragmaOptions (optPragmaOptions opts)
updateBenchmarkingStatus
libToTCM :: LibM a -> TCM a
libToTCM m = do
z <- liftIO $ runExceptT m
case z of
Left s -> typeError $ GenericDocError s
Right x -> return x
setLibraryPaths :: RelativeTo -> CommandLineOptions -> TCM CommandLineOptions
setLibraryPaths rel o = setLibraryIncludes =<< addDefaultLibraries rel 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 :: RelativeTo -> CommandLineOptions -> TCM CommandLineOptions
addDefaultLibraries rel o
| or [ not $ null $ optLibraries o
, not $ optUseLibs o
, optShowVersion o ] = pure o
| otherwise = do
root <- getProjectRoot rel
(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 =
local $ \e -> e { envDisplayFormsEnabled = True }
disableDisplayForms :: TCM a -> TCM a
disableDisplayForms =
local $ \e -> e { envDisplayFormsEnabled = False }
displayFormsEnabled :: TCM Bool
displayFormsEnabled = asks envDisplayFormsEnabled
getIncludeDirs :: TCM [AbsolutePath]
getIncludeDirs = do
incs <- optAbsoluteIncludePaths <$> commandLineOptions
case incs of
[] -> __IMPOSSIBLE__
_ -> return incs
data RelativeTo
= ProjectRoot AbsolutePath
| CurrentDir
getProjectRoot :: RelativeTo -> TCM AbsolutePath
getProjectRoot CurrentDir = liftIO (absolute =<< getCurrentDirectory)
getProjectRoot (ProjectRoot f) = do
m <- moduleName' f
return (projectRoot f m)
setIncludeDirs :: [FilePath]
-> RelativeTo
-> TCM ()
setIncludeDirs incs relativeTo = do
oldIncs <- gets Lens.getAbsoluteIncludePaths
root <- getProjectRoot relativeTo
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
[ text "Old include directories:"
, nest 2 $ vcat $ map pretty oldIncs
, text "New include directories:"
, nest 2 $ vcat $ map pretty incs
]
when (oldIncs /= incs) $ do
ho <- getInteractionOutputCallback
resetAllState
setInteractionOutputCallback ho
Lens.putAbsoluteIncludePaths incs
case relativeTo of
CurrentDir -> return ()
ProjectRoot f -> void $ moduleName f
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
proofIrrelevance :: TCM Bool
proofIrrelevance = optProofIrrelevance <$> 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
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` ".:")
{-# 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 :: (MonadReader TCEnv m, HasOptions m) => VerboseKey -> Int -> m () -> m ()
verboseS k n action = whenM (hasVerbosity k n) $ locally 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