module Agda.TypeChecking.Monad.Options where
import Prelude hiding (mapM)
import Control.Applicative
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 Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Monad.Benchmark
import 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
hasUniversePolymorphism :: HasOptions m => m Bool
hasUniversePolymorphism = optUniversePolymorphism <$> pragmaOptions
sharedFun :: HasOptions m => m (Term -> Term)
sharedFun = do
sharing <- optSharing <$> commandLineOptions
return $ if sharing then shared_ else id
shared :: HasOptions m => Term -> m Term
shared v = ($ v) <$> sharedFun
sharedType :: HasOptions m => Type -> m Type
sharedType (El s v) = El s <$> shared v
enableCaching :: TCM Bool
enableCaching = optCaching <$> commandLineOptions
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
typeInType :: HasOptions m => m Bool
typeInType = not . optUniverseCheck <$> pragmaOptions
etaEnabled :: TCM Bool
etaEnabled = optEta <$> pragmaOptions
maxInstanceSearchDepth :: TCM Int
maxInstanceSearchDepth = optInstanceSearchDepth <$> 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 = last $ 0 : Trie.lookupPath ks t
return (n <= m)
hasExactVerbosity :: HasOptions m => VerboseKey -> Int -> m Bool
hasExactVerbosity k n =
(Just n ==) . Trie.lookup (wordsBy (`elem` ".:") k) <$> getVerbosity
whenExactVerbosity :: MonadTCM tcm => VerboseKey -> Int -> tcm () -> tcm ()
whenExactVerbosity k n = whenM $ liftTCM $ hasExactVerbosity k n
verboseS :: HasOptions m => VerboseKey -> Int -> m () -> m ()
verboseS k n action = whenM (hasVerbosity k n) action