module Agda.TypeChecking.Monad.Options where
import Control.Applicative
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 Paths_Agda (getDataFileName)
import Agda.Syntax.Concrete
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.State
import Agda.Interaction.FindFile
import Agda.Interaction.Options
import qualified Agda.Interaction.Options.Lenses as Lens
import Agda.Interaction.Response
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 :: 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 absolutePathes -> return absolutePathes
Left relativePathes -> do
setIncludeDirs relativePathes CurrentDir
getIncludeDirs
modify $ Lens.setCommandLineOptions opts{ optIncludeDirs = Right incs }
. Lens.setPragmaOptions (optPragmaOptions opts)
class (Functor m, Applicative m, Monad m) => HasOptions m where
pragmaOptions :: m PragmaOptions
commandLineOptions :: m CommandLineOptions
instance MonadIO m => HasOptions (TCMT m) where
pragmaOptions = gets stPragmaOptions
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 :: MonadReader TCEnv m => m 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
oldIncs <- gets Lens.getIncludeDirs
(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)
incs <- return $ if null incs then ["."] else incs
incs <- return $ map (mkAbsolute . (filePath root </>)) incs
libdir <- liftIO $ getDataFileName ("lib")
let primdir = mkAbsolute $ libdir </> "prim"
incs <- return $ incs ++ [primdir]
Lens.putIncludeDirs $ Right $ incs
case oldIncs of
Right incs' | incs' /= incs -> do
ho <- getInteractionOutputCallback
resetAllState
setInteractionOutputCallback ho
Lens.putIncludeDirs $ Right 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 :: HasOptions m => m 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 :: HasOptions m => m (Trie String Int)
getVerbosity = optVerbose <$> pragmaOptions
type VerboseKey = String
hasVerbosity :: HasOptions m => VerboseKey -> Int -> m 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)
displayDebugMessage :: MonadTCM tcm
=> Int
-> String
-> tcm ()
displayDebugMessage n s = liftTCM $
appInteractionOutputCallback (Resp_RunningInfo n s)
verboseS :: MonadTCM tcm => VerboseKey -> Int -> tcm () -> tcm ()
verboseS k n action = whenM (liftTCM $ hasVerbosity k n) action
reportS :: MonadTCM tcm => VerboseKey -> Int -> String -> tcm ()
reportS k n s = liftTCM $ verboseS k n $ displayDebugMessage n s
reportSLn :: MonadTCM tcm => VerboseKey -> Int -> String -> tcm ()
reportSLn k n s = verboseS k n $
displayDebugMessage n (s ++ "\n")
reportSDoc :: MonadTCM tcm => VerboseKey -> Int -> TCM Doc -> tcm ()
reportSDoc k n d = liftTCM $ verboseS k n $ do
displayDebugMessage n . (++ "\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 :: MonadTCM tcm => VerboseKey -> Int -> String -> TCM a -> tcm a
verboseBracket k n s m = liftTCM $ ifNotM (hasVerbosity k n) m $ do
displayDebugMessage n $ "{ " ++ s ++ "\n"
m `finally` displayDebugMessage n "}\n"