summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Monad/Options.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Monad/Options.hs')
-rw-r--r--src/full/Agda/TypeChecking/Monad/Options.hs69
1 files changed, 33 insertions, 36 deletions
diff --git a/src/full/Agda/TypeChecking/Monad/Options.hs b/src/full/Agda/TypeChecking/Monad/Options.hs
index 88a25d4..3086fd2 100644
--- a/src/full/Agda/TypeChecking/Monad/Options.hs
+++ b/src/full/Agda/TypeChecking/Monad/Options.hs
@@ -1,5 +1,4 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleContexts #-}
module Agda.TypeChecking.Monad.Options where
@@ -17,12 +16,13 @@ import System.Directory
import System.FilePath
import Agda.Syntax.Internal
+import Agda.Syntax.Common
import Agda.Syntax.Concrete
import {-# SOURCE #-} Agda.TypeChecking.Errors
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Monad.Benchmark
-import Agda.Interaction.FindFile
+import {-# SOURCE #-} Agda.Interaction.FindFile
import Agda.Interaction.Options
import qualified Agda.Interaction.Options.Lenses as Lens
import Agda.Interaction.Response
@@ -83,7 +83,7 @@ setCommandLineOptions' relativeTo opts = do
getIncludeDirs
incs -> return incs
modify $ Lens.setCommandLineOptions opts{ optAbsoluteIncludePaths = incs }
- . Lens.setPragmaOptions (optPragmaOptions opts)
+ setPragmaOptions (optPragmaOptions opts)
updateBenchmarkingStatus
libToTCM :: LibM a -> TCM a
@@ -106,11 +106,11 @@ setLibraryIncludes o = do
addDefaultLibraries :: RelativeTo -> CommandLineOptions -> TCM CommandLineOptions
addDefaultLibraries rel o
| or [ not $ null $ optLibraries o
- , not $ optDefaultLibs o
+ , not $ optUseLibs o
, optShowVersion o ] = pure o
| otherwise = do
root <- getProjectRoot rel
- (libs, incs) <- libToTCM $ getDefaultLibraries (filePath root)
+ (libs, incs) <- libToTCM $ getDefaultLibraries (filePath root) (optDefaultLibs o)
return o{ optIncludePaths = incs ++ optIncludePaths o, optLibraries = libs }
class (Functor m, Applicative m, Monad m) => HasOptions m where
@@ -149,27 +149,6 @@ disableDisplayForms =
displayFormsEnabled :: TCM Bool
displayFormsEnabled = asks envDisplayFormsEnabled
--- | Don't eta contract implicit
-dontEtaContractImplicit :: TCM a -> TCM a
-dontEtaContractImplicit = local $ \e -> e { envEtaContractImplicit = False }
-
--- | Do eta contract implicit
-{-# SPECIALIZE doEtaContractImplicit :: TCM a -> TCM a #-}
-doEtaContractImplicit :: MonadTCM tcm => tcm a -> tcm a
-doEtaContractImplicit = local $ \e -> e { envEtaContractImplicit = True }
-
-{-# SPECIALIZE shouldEtaContractImplicit :: TCM Bool #-}
-shouldEtaContractImplicit :: MonadReader TCEnv m => m Bool
-shouldEtaContractImplicit = asks envEtaContractImplicit
-
--- | Don't reify interaction points
-dontReifyInteractionPoints :: TCM a -> TCM a
-dontReifyInteractionPoints =
- local $ \e -> e { envReifyInteractionPoints = False }
-
-shouldReifyInteractionPoints :: TCM Bool
-shouldReifyInteractionPoints = asks envReifyInteractionPoints
-
-- | Gets the include directories.
--
-- Precondition: 'optAbsoluteIncludePaths' must be nonempty (i.e.
@@ -195,7 +174,7 @@ data RelativeTo
getProjectRoot :: RelativeTo -> TCM AbsolutePath
getProjectRoot CurrentDir = liftIO (absolute =<< getCurrentDirectory)
getProjectRoot (ProjectRoot f) = do
- m <- moduleName' f
+ Ranged _ m <- moduleName' f
return (projectRoot f m)
-- | Makes the given directories absolute and stores them as include
@@ -214,11 +193,6 @@ setIncludeDirs incs relativeTo = do
oldIncs <- gets Lens.getAbsoluteIncludePaths
root <- getProjectRoot relativeTo
- check <- case relativeTo of
- CurrentDir -> return (return ())
- ProjectRoot f -> do
- m <- moduleName' f
- return (checkModuleName m f)
-- Add the current dir if no include path is given
incs <- return $ if null incs then ["."] else incs
@@ -247,7 +221,24 @@ setIncludeDirs incs relativeTo = do
setInteractionOutputCallback ho
Lens.putAbsoluteIncludePaths incs
- check
+
+ -- Andreas, 2016-07-11 (reconstructing semantics):
+ --
+ -- Check that the module name of the project root
+ -- is still correct wrt. to the changed include path.
+ --
+ -- E.g. if the include path was "/" and file "/A/B" was named "module A.B",
+ -- and then the include path changes to "/A/", the module name
+ -- becomes invalid; correct would then be "module B".
+
+ case relativeTo of
+ CurrentDir -> return ()
+ ProjectRoot f -> void $ moduleName f
+ -- Andreas, 2016-07-12 WAS:
+ -- do
+ -- Ranged _ m <- moduleName' f
+ -- checkModuleName m f Nothing
+
setInputFile :: FilePath -> TCM ()
setInputFile file =
@@ -301,11 +292,14 @@ showIrrelevantArguments = optShowIrrelevant <$> pragmaOptions
-- | Switch on printing of implicit and irrelevant arguments.
-- E.g. for reification in with-function generation.
withShowAllArguments :: TCM a -> TCM a
-withShowAllArguments ret = do
+withShowAllArguments = withShowAllArguments' True
+
+withShowAllArguments' :: Bool -> TCM a -> TCM a
+withShowAllArguments' yes ret = do
opts <- pragmaOptions
let imp = optShowImplicit opts
irr = optShowIrrelevant opts
- setPragmaOptions $ opts { optShowImplicit = True, optShowIrrelevant = True }
+ setPragmaOptions $ opts { optShowImplicit = yes, optShowIrrelevant = yes }
x <- ret
opts <- pragmaOptions
setPragmaOptions $ opts { optShowImplicit = imp, optShowIrrelevant = irr }
@@ -336,6 +330,9 @@ typeInType = not . optUniverseCheck <$> pragmaOptions
etaEnabled :: TCM Bool
etaEnabled = optEta <$> pragmaOptions
+maxInstanceSearchDepth :: TCM Int
+maxInstanceSearchDepth = optInstanceSearchDepth <$> pragmaOptions
+
------------------------------------------------------------------------
-- Verbosity
@@ -362,7 +359,7 @@ hasVerbosity k n | n < 0 = __IMPOSSIBLE__
| otherwise = do
t <- getVerbosity
let ks = wordsBy (`elem` ".:") k
- m = maximum $ 0 : Trie.lookupPath ks t
+ m = last $ 0 : Trie.lookupPath ks t
return (n <= m)
-- | Displays a debug message in a suitable way.