module Agda.TypeChecking.Monad.Options where
import Control.Applicative
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.Except ( MonadError(catchError) )
import Agda.Utils.FileName
import Agda.Utils.Monad
import Agda.Utils.Lens
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
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 = use stPragmaOptions
commandLineOptions = do
p <- use stPragmaOptions
cl <- stPersistentOptions . stPersistentState <$> 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"