module Agda.TypeChecking.Monad.Options where
import Control.Monad.Error
import Control.Monad.Reader
import Control.Monad.State
import Data.Maybe
import Text.PrettyPrint
import System.Directory
import System.FilePath
import System.IO
import Agda.Syntax.Concrete
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.State
import Agda.Interaction.EmacsCommand as Emacs
import Agda.Interaction.FindFile
import Agda.Interaction.Options
import Agda.Utils.FileName
import Agda.Utils.Monad
import Agda.Utils.List
import Agda.Utils.String
import Agda.Utils.Trie (Trie)
import qualified Agda.Utils.Trie as Trie
#include "../../undefined.h"
import Agda.Utils.Impossible
setPragmaOptions :: PragmaOptions -> TCM ()
setPragmaOptions opts = do
clo <- commandLineOptions
let unsafe = unsafePragmaOptions opts
when (optSafe clo && not (null unsafe)) $ typeError (SafeFlagPragma unsafe)
case checkOpts (clo { optPragmaOptions = opts }) of
Left err -> __IMPOSSIBLE__
Right opts -> do
modify $ \s -> s { stPragmaOptions = (optPragmaOptions opts) }
setCommandLineOptions :: 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 { stPersistent = (stPersistent s) {
stPersistentOptions = opts { optIncludeDirs = Right incs }
}
, stPragmaOptions = optPragmaOptions opts
}
pragmaOptions :: TCM PragmaOptions
pragmaOptions = gets stPragmaOptions
commandLineOptions :: TCM CommandLineOptions
commandLineOptions = do
p <- stPragmaOptions <$> get
cl <- stPersistentOptions . stPersistent <$> get
return $ cl { optPragmaOptions = p }
setOptionsFromPragma :: OptionsPragma -> TCM ()
setOptionsFromPragma ps = do
opts <- commandLineOptions
case parsePragmaOptions ps opts 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
dontEtaContractImplicit :: TCM a -> TCM a
dontEtaContractImplicit = local $ \e -> e { envEtaContractImplicit = False }
doEtaContractImplicit :: MonadTCM tcm => tcm a -> tcm a
doEtaContractImplicit = local $ \e -> e { envEtaContractImplicit = True }
shouldEtaContractImplicit :: TCM Bool
shouldEtaContractImplicit = asks envEtaContractImplicit
dontReifyInteractionPoints :: TCM a -> TCM a
dontReifyInteractionPoints =
local $ \e -> e { envReifyInteractionPoints = False }
shouldReifyInteractionPoints :: TCM Bool
shouldReifyInteractionPoints = asks envReifyInteractionPoints
getIncludeDirs :: TCM [AbsolutePath]
getIncludeDirs = do
incs <- optIncludeDirs <$> commandLineOptions
case incs of
Left _ -> __IMPOSSIBLE__
Right incs -> return incs
data RelativeTo
= ProjectRoot AbsolutePath
| CurrentDir
setIncludeDirs
:: [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 <- moduleName' f
return (projectRoot f m, checkModuleName m f)
let setIncs incs = modify $ \s ->
s { stPersistent =
(stPersistent s) { stPersistentOptions =
(stPersistentOptions $ stPersistent s)
{ optIncludeDirs = Right incs
}
}
}
setIncs (map (mkAbsolute . (filePath root </>)) $
case incs of
[] -> ["."]
_ -> incs)
incs <- getIncludeDirs
case oldIncs of
Right incs' | incs' /= incs -> do
ho <- stInteractionOutputCallback <$> get
resetAllState
modify $ \st -> st { stInteractionOutputCallback = ho }
setIncs incs
_ -> return ()
check
setInputFile :: FilePath -> TCM ()
setInputFile file =
do opts <- commandLineOptions
setCommandLineOptions $
opts { optInputFile = Just file }
getInputFile :: TCM AbsolutePath
getInputFile =
do mf <- optInputFile <$> commandLineOptions
case mf of
Just file -> liftIO $ absolute file
Nothing -> __IMPOSSIBLE__
hasInputFile :: TCM Bool
hasInputFile = isJust <$> optInputFile <$> commandLineOptions
proofIrrelevance :: TCM Bool
proofIrrelevance = optProofIrrelevance <$> pragmaOptions
hasUniversePolymorphism :: TCM Bool
hasUniversePolymorphism = optUniversePolymorphism <$> pragmaOptions
showImplicitArguments :: TCM Bool
showImplicitArguments = optShowImplicit <$> pragmaOptions
showIrrelevantArguments :: TCM Bool
showIrrelevantArguments = optShowIrrelevant <$> pragmaOptions
withShowAllArguments :: TCM a -> TCM a
withShowAllArguments ret = do
opts <- pragmaOptions
let imp = optShowImplicit opts
irr = optShowIrrelevant opts
setPragmaOptions $ opts { optShowImplicit = True, optShowIrrelevant = True }
x <- ret
opts <- pragmaOptions
setPragmaOptions $ opts { optShowImplicit = imp, optShowIrrelevant = irr }
return x
ignoreInterfaces :: TCM Bool
ignoreInterfaces = optIgnoreInterfaces <$> commandLineOptions
positivityCheckEnabled :: TCM Bool
positivityCheckEnabled = not . optDisablePositivity <$> pragmaOptions
typeInType :: TCM Bool
typeInType = not . optUniverseCheck <$> pragmaOptions
getVerbosity :: TCM (Trie String Int)
getVerbosity = optVerbose <$> pragmaOptions
type VerboseKey = String
hasVerbosity :: 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)
emacsifyDebugMessage :: String
-> TCM String
emacsifyDebugMessage s =
ifM (envEmacs <$> ask)
(return $ Emacs.response $
L [ A "agda2-verbose"
, A (quote s)
])
(return s)
displayDebugMessage :: String -> TCM ()
displayDebugMessage s =
liftIO . putStr =<< emacsifyDebugMessage s
verboseS :: VerboseKey -> Int -> TCM () -> TCM ()
verboseS k n action = whenM (hasVerbosity k n) action
reportS :: VerboseKey -> Int -> String -> TCM ()
reportS k n s = verboseS k n $ displayDebugMessage s
reportSLn :: VerboseKey -> Int -> String -> TCM ()
reportSLn k n s = verboseS k n $ do
displayDebugMessage (s ++ "\n")
liftIO $ hFlush stdout
reportSDoc :: VerboseKey -> Int -> TCM Doc -> TCM ()
reportSDoc k n d = verboseS k n $ do
displayDebugMessage . (++ "\n") . show =<< do
d `catchError` \ err ->
(\ s -> (sep $ map text
[ "Printing debug message"
, k ++ ":" ++show n
, "failed due to error:" ]) $$
(nest 2 $ text s)) <$> prettyError err
verboseBracket :: VerboseKey -> Int -> String -> TCM a -> TCM a
verboseBracket k n s m = do
v <- hasVerbosity k n
if not v then m
else do
displayDebugMessage $ "{ " ++ s ++ "\n"
x <- m `finally` displayDebugMessage "}\n"
return x