module Agda.TypeChecking.Monad.Options where
import Control.Monad.Reader
import Control.Monad.State
import Data.Maybe
import Text.PrettyPrint
import qualified Agda.Utils.IO.Locale as LocIO
import System.Directory
import System.FilePath
import Agda.Syntax.Concrete
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.State
import Agda.Interaction.FindFile
import Agda.Interaction.Options
import Agda.Utils.FileName
import Agda.Utils.Monad
import Agda.Utils.List
import Agda.Utils.Trie (Trie)
import qualified Agda.Utils.Trie as Trie
#include "../../undefined.h"
import Agda.Utils.Impossible
setPragmaOptions :: MonadTCM tcm => PragmaOptions -> tcm ()
setPragmaOptions opts = do
clo <- commandLineOptions
case checkOpts (clo { optPragmaOptions = opts }) of
Left err -> __IMPOSSIBLE__
Right opts -> do
modify $ \s -> s { stPragmaOptions = (optPragmaOptions opts) }
setCommandLineOptions :: MonadTCM tcm => CommandLineOptions -> tcm ()
setCommandLineOptions opts =
case checkOpts opts of
Left err -> __IMPOSSIBLE__
Right opts -> do
incs <- case optIncludeDirs opts of
Right is -> return is
Left is -> do
setIncludeDirs is CurrentDir
getIncludeDirs
modify $ \s ->
s { stPersistentOptions = opts { optIncludeDirs = Right incs }
, stPragmaOptions = optPragmaOptions opts
}
pragmaOptions :: MonadTCM tcm => tcm PragmaOptions
pragmaOptions = liftTCM $ gets stPragmaOptions
commandLineOptions :: MonadTCM tcm => tcm CommandLineOptions
commandLineOptions = liftTCM $ do
p <- gets stPragmaOptions
cl <- gets stPersistentOptions
return $ cl { optPragmaOptions = p }
setOptionsFromPragma :: MonadTCM tcm => OptionsPragma -> tcm ()
setOptionsFromPragma ps = do
opts <- commandLineOptions
case parsePragmaOptions ps opts of
Left err -> typeError $ GenericError err
Right opts' -> setPragmaOptions opts'
enableDisplayForms :: MonadTCM tcm => tcm a -> tcm a
enableDisplayForms =
local $ \e -> e { envDisplayFormsEnabled = True }
disableDisplayForms :: MonadTCM tcm => tcm a -> tcm a
disableDisplayForms =
local $ \e -> e { envDisplayFormsEnabled = False }
displayFormsEnabled :: MonadTCM tcm => tcm Bool
displayFormsEnabled = asks envDisplayFormsEnabled
dontEtaContractImplicit :: MonadTCM tcm => tcm a -> tcm a
dontEtaContractImplicit = local $ \e -> e { envEtaContractImplicit = False }
doEtaContractImplicit :: MonadTCM tcm => tcm a -> tcm a
doEtaContractImplicit = local $ \e -> e { envEtaContractImplicit = True }
shouldEtaContractImplicit :: MonadTCM tcm => tcm Bool
shouldEtaContractImplicit = asks envEtaContractImplicit
dontReifyInteractionPoints :: MonadTCM tcm => tcm a -> tcm a
dontReifyInteractionPoints =
local $ \e -> e { envReifyInteractionPoints = False }
shouldReifyInteractionPoints :: MonadTCM tcm => tcm Bool
shouldReifyInteractionPoints = asks envReifyInteractionPoints
getIncludeDirs :: MonadTCM tcm => tcm [AbsolutePath]
getIncludeDirs = do
incs <- optIncludeDirs <$> commandLineOptions
case incs of
Left _ -> __IMPOSSIBLE__
Right incs -> return incs
data RelativeTo
= ProjectRoot AbsolutePath
| CurrentDir
setIncludeDirs
:: MonadTCM tcm
=> [FilePath]
-> RelativeTo
-> tcm ()
setIncludeDirs incs relativeTo = do
opts <- commandLineOptions
let oldIncs = optIncludeDirs opts
(root, check) <- case relativeTo of
CurrentDir -> do
root <- liftIO (absolute =<< getCurrentDirectory)
return (root, return ())
ProjectRoot f -> do
m <- liftTCM $ moduleName' f
return (projectRoot f m, liftTCM $ checkModuleName m f)
modify $ \s -> s { stPersistentOptions =
(stPersistentOptions s) { optIncludeDirs =
Right $ map (mkAbsolute . (filePath root </>)) $
case incs of
[] -> ["."]
_ -> incs } }
incs <- getIncludeDirs
case oldIncs of
Right incs' | incs' /= incs -> resetState
_ -> return ()
check
setInputFile :: MonadTCM tcm => FilePath -> tcm ()
setInputFile file =
do opts <- commandLineOptions
setCommandLineOptions $
opts { optInputFile = Just file }
getInputFile :: MonadTCM tcm => tcm AbsolutePath
getInputFile =
do mf <- optInputFile <$> commandLineOptions
case mf of
Just file -> liftIO $ absolute file
Nothing -> __IMPOSSIBLE__
hasInputFile :: MonadTCM tcm => tcm Bool
hasInputFile = isJust <$> optInputFile <$> commandLineOptions
proofIrrelevance :: MonadTCM tcm => tcm Bool
proofIrrelevance = optProofIrrelevance <$> pragmaOptions
hasUniversePolymorphism :: MonadTCM tcm => tcm Bool
hasUniversePolymorphism = optUniversePolymorphism <$> pragmaOptions
showImplicitArguments :: MonadTCM tcm => tcm Bool
showImplicitArguments = optShowImplicit <$> pragmaOptions
setShowImplicitArguments :: MonadTCM tcm => Bool -> tcm a -> tcm a
setShowImplicitArguments showImp ret = do
opts <- pragmaOptions
let imp = optShowImplicit opts
setPragmaOptions $ opts { optShowImplicit = showImp }
x <- ret
opts <- pragmaOptions
setPragmaOptions $ opts { optShowImplicit = imp }
return x
ignoreInterfaces :: MonadTCM tcm => tcm Bool
ignoreInterfaces = optIgnoreInterfaces <$> commandLineOptions
positivityCheckEnabled :: MonadTCM tcm => tcm Bool
positivityCheckEnabled = not . optDisablePositivity <$> pragmaOptions
typeInType :: MonadTCM tcm => tcm Bool
typeInType = not . optUniverseCheck <$> pragmaOptions
getVerbosity :: MonadTCM tcm => tcm (Trie String Int)
getVerbosity = optVerbose <$> pragmaOptions
type VerboseKey = String
hasVerbosity :: MonadTCM tcm => VerboseKey -> Int -> tcm Bool
hasVerbosity k n | n < 0 = __IMPOSSIBLE__
| otherwise = do
t <- getVerbosity
let ks = wordsBy (`elem` ".:") k
m = maximum $ 0 : Trie.lookupPath ks t
return (n <= m)
verboseS :: MonadTCM tcm => VerboseKey -> Int -> tcm () -> tcm ()
verboseS k n action = whenM (hasVerbosity k n) action
reportS :: MonadTCM tcm => VerboseKey -> Int -> String -> tcm ()
reportS k n s = verboseS k n $ liftIO $ LocIO.putStr s
reportSLn :: MonadTCM tcm => VerboseKey -> Int -> String -> tcm ()
reportSLn k n s = verboseS k n $ liftIO $ LocIO.putStrLn s >> LocIO.stdoutFlush
reportSDoc :: MonadTCM tcm => VerboseKey -> Int -> tcm Doc -> tcm ()
reportSDoc k n d = verboseS k n $ liftIO . LocIO.print =<< d
verboseBracket :: MonadTCM tcm => VerboseKey -> Int -> String -> tcm a -> tcm a
verboseBracket k n s m = do
v <- hasVerbosity k n
if not v then m
else do
liftIO $ LocIO.putStrLn $ "{ " ++ s
x <- m
liftIO $ LocIO.putStrLn "}"
return x