module Agda.TypeChecking.Monad.Options where
import Control.Arrow ( (&&&) )
import Control.Monad ( unless, when )
import Control.Monad.IO.Class ( MonadIO(..) )
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Writer
import qualified Data.Graph as Graph
import Data.List (sort)
import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map
import System.Directory
import System.FilePath
import Agda.Syntax.Common
import Agda.Syntax.Concrete (TopLevelModuleName)
import qualified Agda.Syntax.Concrete as C
import qualified Agda.Syntax.Abstract as A
import Agda.TypeChecking.Monad.Debug (reportSDoc)
import Agda.TypeChecking.Warnings
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Imports
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.Library
import Agda.Utils.FileName
import Agda.Utils.Functor
import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as G
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Pretty
import Agda.Utils.Tuple
import Agda.Utils.WithDefault
import Agda.Utils.Impossible
setPragmaOptions :: PragmaOptions -> TCM ()
setPragmaOptions :: PragmaOptions -> TCM ()
setPragmaOptions PragmaOptions
opts = do
Lens' PragmaOptions TCState
stPragmaOptions Lens' PragmaOptions TCState
-> (PragmaOptions -> PragmaOptions) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` (SafeMode -> SafeMode) -> PragmaOptions -> PragmaOptions
forall a. LensSafeMode a => (SafeMode -> SafeMode) -> a -> a
Lens.mapSafeMode (PragmaOptions -> SafeMode
forall a. LensSafeMode a => a -> SafeMode
Lens.getSafeMode PragmaOptions
opts SafeMode -> SafeMode -> SafeMode
||)
CommandLineOptions
clo <- TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
let unsafe :: [String]
unsafe = CommandLineOptions -> PragmaOptions -> [String]
unsafePragmaOptions CommandLineOptions
clo PragmaOptions
opts
SafeMode -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => SafeMode -> f () -> f ()
when (PragmaOptions -> SafeMode
forall a. LensSafeMode a => a -> SafeMode
Lens.getSafeMode PragmaOptions
opts SafeMode -> SafeMode -> SafeMode
&& SafeMode -> SafeMode
not ([String] -> SafeMode
forall (t :: * -> *) a. Foldable t => t a -> SafeMode
null [String]
unsafe)) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ [String] -> Warning
SafeFlagPragma [String]
unsafe
OptM CommandLineOptions
-> TCMT IO (Either String CommandLineOptions)
forall (m :: * -> *) opts.
Monad m =>
OptM opts -> m (Either String opts)
runOptM (Flag CommandLineOptions
checkOpts CommandLineOptions
clo{ optPragmaOptions :: PragmaOptions
optPragmaOptions = PragmaOptions
opts }) TCMT IO (Either String CommandLineOptions)
-> (Either String CommandLineOptions -> TCM ()) -> TCM ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Left String
err -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
Right CommandLineOptions
opts -> do
Lens' PragmaOptions TCState
stPragmaOptions Lens' PragmaOptions TCState -> PragmaOptions -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` CommandLineOptions -> PragmaOptions
optPragmaOptions CommandLineOptions
opts
TCM ()
updateBenchmarkingStatus
setCommandLineOptions :: CommandLineOptions -> TCM ()
setCommandLineOptions :: CommandLineOptions -> TCM ()
setCommandLineOptions CommandLineOptions
opts = do
AbsolutePath
root <- IO AbsolutePath -> TCMT IO AbsolutePath
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (String -> IO AbsolutePath
absolute (String -> IO AbsolutePath) -> IO String -> IO AbsolutePath
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO String
getCurrentDirectory)
AbsolutePath -> CommandLineOptions -> TCM ()
setCommandLineOptions' AbsolutePath
root CommandLineOptions
opts
setCommandLineOptions'
:: AbsolutePath
-> CommandLineOptions
-> TCM ()
setCommandLineOptions' :: AbsolutePath -> CommandLineOptions -> TCM ()
setCommandLineOptions' AbsolutePath
root CommandLineOptions
opts = do
OptM CommandLineOptions
-> TCMT IO (Either String CommandLineOptions)
forall (m :: * -> *) opts.
Monad m =>
OptM opts -> m (Either String opts)
runOptM (Flag CommandLineOptions
checkOpts CommandLineOptions
opts) TCMT IO (Either String CommandLineOptions)
-> (Either String CommandLineOptions -> TCM ()) -> TCM ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Left String
err -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
Right CommandLineOptions
opts -> do
[AbsolutePath]
incs <- case CommandLineOptions -> [AbsolutePath]
optAbsoluteIncludePaths CommandLineOptions
opts of
[] -> do
CommandLineOptions
opts' <- AbsolutePath -> CommandLineOptions -> TCMT IO CommandLineOptions
setLibraryPaths AbsolutePath
root CommandLineOptions
opts
let incs :: [String]
incs = CommandLineOptions -> [String]
optIncludePaths CommandLineOptions
opts'
[String] -> AbsolutePath -> TCM ()
setIncludeDirs [String]
incs AbsolutePath
root
TCMT IO [AbsolutePath]
forall (m :: * -> *). HasOptions m => m [AbsolutePath]
getIncludeDirs
[AbsolutePath]
incs -> [AbsolutePath] -> TCMT IO [AbsolutePath]
forall (m :: * -> *) a. Monad m => a -> m a
return [AbsolutePath]
incs
(TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> TCM ()) -> (TCState -> TCState) -> TCM ()
forall a b. (a -> b) -> a -> b
$ CommandLineOptions -> TCState -> TCState
forall a. LensCommandLineOptions a => CommandLineOptions -> a -> a
Lens.setCommandLineOptions CommandLineOptions
opts{ optAbsoluteIncludePaths :: [AbsolutePath]
optAbsoluteIncludePaths = [AbsolutePath]
incs }
PragmaOptions -> TCM ()
setPragmaOptions (CommandLineOptions -> PragmaOptions
optPragmaOptions CommandLineOptions
opts)
TCM ()
updateBenchmarkingStatus
libToTCM :: LibM a -> TCM a
libToTCM :: LibM a -> TCM a
libToTCM LibM a
m = do
Map String ProjectConfig
cachedConfs <- Lens' (Map String ProjectConfig) TCState
-> TCMT IO (Map String ProjectConfig)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map String ProjectConfig) TCState
stProjectConfigs
Map String AgdaLibFile
cachedLibs <- Lens' (Map String AgdaLibFile) TCState
-> TCMT IO (Map String AgdaLibFile)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map String AgdaLibFile) TCState
stAgdaLibFiles
((Either Doc a
z, [LibWarning]
warns), (Map String ProjectConfig
cachedConfs', Map String AgdaLibFile
cachedLibs')) <- IO
((Either Doc a, [LibWarning]),
(Map String ProjectConfig, Map String AgdaLibFile))
-> TCMT
IO
((Either Doc a, [LibWarning]),
(Map String ProjectConfig, Map String AgdaLibFile))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO
((Either Doc a, [LibWarning]),
(Map String ProjectConfig, Map String AgdaLibFile))
-> TCMT
IO
((Either Doc a, [LibWarning]),
(Map String ProjectConfig, Map String AgdaLibFile)))
-> IO
((Either Doc a, [LibWarning]),
(Map String ProjectConfig, Map String AgdaLibFile))
-> TCMT
IO
((Either Doc a, [LibWarning]),
(Map String ProjectConfig, Map String AgdaLibFile))
forall a b. (a -> b) -> a -> b
$
(StateT
(Map String ProjectConfig, Map String AgdaLibFile)
IO
(Either Doc a, [LibWarning])
-> (Map String ProjectConfig, Map String AgdaLibFile)
-> IO
((Either Doc a, [LibWarning]),
(Map String ProjectConfig, Map String AgdaLibFile))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
`runStateT` (Map String ProjectConfig
cachedConfs, Map String AgdaLibFile
cachedLibs)) (StateT
(Map String ProjectConfig, Map String AgdaLibFile)
IO
(Either Doc a, [LibWarning])
-> IO
((Either Doc a, [LibWarning]),
(Map String ProjectConfig, Map String AgdaLibFile)))
-> StateT
(Map String ProjectConfig, Map String AgdaLibFile)
IO
(Either Doc a, [LibWarning])
-> IO
((Either Doc a, [LibWarning]),
(Map String ProjectConfig, Map String AgdaLibFile))
forall a b. (a -> b) -> a -> b
$ WriterT
[LibWarning]
(StateT (Map String ProjectConfig, Map String AgdaLibFile) IO)
(Either Doc a)
-> StateT
(Map String ProjectConfig, Map String AgdaLibFile)
IO
(Either Doc a, [LibWarning])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT
[LibWarning]
(StateT (Map String ProjectConfig, Map String AgdaLibFile) IO)
(Either Doc a)
-> StateT
(Map String ProjectConfig, Map String AgdaLibFile)
IO
(Either Doc a, [LibWarning]))
-> WriterT
[LibWarning]
(StateT (Map String ProjectConfig, Map String AgdaLibFile) IO)
(Either Doc a)
-> StateT
(Map String ProjectConfig, Map String AgdaLibFile)
IO
(Either Doc a, [LibWarning])
forall a b. (a -> b) -> a -> b
$ LibM a
-> WriterT
[LibWarning]
(StateT (Map String ProjectConfig, Map String AgdaLibFile) IO)
(Either Doc a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT LibM a
m
Lens' (Map String ProjectConfig) TCState
-> (Map String ProjectConfig -> Map String ProjectConfig) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
modifyTCLens Lens' (Map String ProjectConfig) TCState
stProjectConfigs ((Map String ProjectConfig -> Map String ProjectConfig) -> TCM ())
-> (Map String ProjectConfig -> Map String ProjectConfig) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Map String ProjectConfig
-> Map String ProjectConfig -> Map String ProjectConfig
forall a b. a -> b -> a
const Map String ProjectConfig
cachedConfs'
Lens' (Map String AgdaLibFile) TCState
-> (Map String AgdaLibFile -> Map String AgdaLibFile) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
modifyTCLens Lens' (Map String AgdaLibFile) TCState
stAgdaLibFiles ((Map String AgdaLibFile -> Map String AgdaLibFile) -> TCM ())
-> (Map String AgdaLibFile -> Map String AgdaLibFile) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Map String AgdaLibFile
-> Map String AgdaLibFile -> Map String AgdaLibFile
forall a b. a -> b -> a
const Map String AgdaLibFile
cachedLibs'
SafeMode -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => SafeMode -> f () -> f ()
unless ([LibWarning] -> SafeMode
forall (t :: * -> *) a. Foldable t => t a -> SafeMode
null [LibWarning]
warns) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Warning] -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
[Warning] -> m ()
warnings ([Warning] -> TCM ()) -> [Warning] -> TCM ()
forall a b. (a -> b) -> a -> b
$ (LibWarning -> Warning) -> [LibWarning] -> [Warning]
forall a b. (a -> b) -> [a] -> [b]
map LibWarning -> Warning
LibraryWarning [LibWarning]
warns
case Either Doc a
z of
Left Doc
s -> TypeError -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM a) -> TypeError -> TCM a
forall a b. (a -> b) -> a -> b
$ Doc -> TypeError
GenericDocError Doc
s
Right a
x -> a -> TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
getAgdaLibFiles :: FilePath -> TCM [AgdaLibFile]
getAgdaLibFiles :: String -> TCM [AgdaLibFile]
getAgdaLibFiles String
root = do
SafeMode
useLibs <- CommandLineOptions -> SafeMode
optUseLibs (CommandLineOptions -> SafeMode)
-> TCMT IO CommandLineOptions -> TCMT IO SafeMode
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
if | SafeMode
useLibs -> LibM [AgdaLibFile] -> TCM [AgdaLibFile]
forall a. LibM a -> TCM a
libToTCM (LibM [AgdaLibFile] -> TCM [AgdaLibFile])
-> LibM [AgdaLibFile] -> TCM [AgdaLibFile]
forall a b. (a -> b) -> a -> b
$ [AgdaLibFile] -> LibErrorIO [AgdaLibFile] -> LibM [AgdaLibFile]
forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
mkLibM [] (LibErrorIO [AgdaLibFile] -> LibM [AgdaLibFile])
-> LibErrorIO [AgdaLibFile] -> LibM [AgdaLibFile]
forall a b. (a -> b) -> a -> b
$ String -> LibErrorIO [AgdaLibFile]
getAgdaLibFiles' String
root
| SafeMode
otherwise -> [AgdaLibFile] -> TCM [AgdaLibFile]
forall (m :: * -> *) a. Monad m => a -> m a
return []
getLibraryOptions :: FilePath -> TCM [OptionsPragma]
getLibraryOptions :: String -> TCM [[String]]
getLibraryOptions String
root = (AgdaLibFile -> [String]) -> [AgdaLibFile] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map AgdaLibFile -> [String]
_libPragmas ([AgdaLibFile] -> [[String]])
-> TCM [AgdaLibFile] -> TCM [[String]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> TCM [AgdaLibFile]
getAgdaLibFiles String
root
setLibraryPaths
:: AbsolutePath
-> CommandLineOptions
-> TCM CommandLineOptions
setLibraryPaths :: AbsolutePath -> CommandLineOptions -> TCMT IO CommandLineOptions
setLibraryPaths AbsolutePath
root CommandLineOptions
o =
CommandLineOptions -> TCMT IO CommandLineOptions
setLibraryIncludes (CommandLineOptions -> TCMT IO CommandLineOptions)
-> TCMT IO CommandLineOptions -> TCMT IO CommandLineOptions
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< AbsolutePath -> CommandLineOptions -> TCMT IO CommandLineOptions
addDefaultLibraries AbsolutePath
root CommandLineOptions
o
setLibraryIncludes :: CommandLineOptions -> TCM CommandLineOptions
setLibraryIncludes :: CommandLineOptions -> TCMT IO CommandLineOptions
setLibraryIncludes CommandLineOptions
o
| SafeMode -> SafeMode
not (CommandLineOptions -> SafeMode
optUseLibs CommandLineOptions
o) = CommandLineOptions -> TCMT IO CommandLineOptions
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandLineOptions
o
| SafeMode
otherwise = do
let libs :: [String]
libs = CommandLineOptions -> [String]
optLibraries CommandLineOptions
o
[AgdaLibFile]
installed <- LibM [AgdaLibFile] -> TCM [AgdaLibFile]
forall a. LibM a -> TCM a
libToTCM (LibM [AgdaLibFile] -> TCM [AgdaLibFile])
-> LibM [AgdaLibFile] -> TCM [AgdaLibFile]
forall a b. (a -> b) -> a -> b
$ Maybe String -> LibM [AgdaLibFile]
getInstalledLibraries (CommandLineOptions -> Maybe String
optOverrideLibrariesFile CommandLineOptions
o)
[String]
paths <- LibM [String] -> TCM [String]
forall a. LibM a -> TCM a
libToTCM (LibM [String] -> TCM [String]) -> LibM [String] -> TCM [String]
forall a b. (a -> b) -> a -> b
$ Maybe String -> [AgdaLibFile] -> [String] -> LibM [String]
libraryIncludePaths (CommandLineOptions -> Maybe String
optOverrideLibrariesFile CommandLineOptions
o) [AgdaLibFile]
installed [String]
libs
CommandLineOptions -> TCMT IO CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return CommandLineOptions
o{ optIncludePaths :: [String]
optIncludePaths = [String]
paths [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ CommandLineOptions -> [String]
optIncludePaths CommandLineOptions
o }
addDefaultLibraries
:: AbsolutePath
-> CommandLineOptions
-> TCM CommandLineOptions
addDefaultLibraries :: AbsolutePath -> CommandLineOptions -> TCMT IO CommandLineOptions
addDefaultLibraries AbsolutePath
root CommandLineOptions
o
| SafeMode -> SafeMode
not ([String] -> SafeMode
forall (t :: * -> *) a. Foldable t => t a -> SafeMode
null ([String] -> SafeMode) -> [String] -> SafeMode
forall a b. (a -> b) -> a -> b
$ CommandLineOptions -> [String]
optLibraries CommandLineOptions
o) SafeMode -> SafeMode -> SafeMode
|| SafeMode -> SafeMode
not (CommandLineOptions -> SafeMode
optUseLibs CommandLineOptions
o) = CommandLineOptions -> TCMT IO CommandLineOptions
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandLineOptions
o
| SafeMode
otherwise = do
([String]
libs, [String]
incs) <- LibM ([String], [String]) -> TCM ([String], [String])
forall a. LibM a -> TCM a
libToTCM (LibM ([String], [String]) -> TCM ([String], [String]))
-> LibM ([String], [String]) -> TCM ([String], [String])
forall a b. (a -> b) -> a -> b
$ String -> SafeMode -> LibM ([String], [String])
getDefaultLibraries (AbsolutePath -> String
filePath AbsolutePath
root) (CommandLineOptions -> SafeMode
optDefaultLibs CommandLineOptions
o)
CommandLineOptions -> TCMT IO CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return CommandLineOptions
o{ optIncludePaths :: [String]
optIncludePaths = [String]
incs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ CommandLineOptions -> [String]
optIncludePaths CommandLineOptions
o, optLibraries :: [String]
optLibraries = [String]
libs }
addTrustedExecutables
:: CommandLineOptions
-> TCM CommandLineOptions
addTrustedExecutables :: CommandLineOptions -> TCMT IO CommandLineOptions
addTrustedExecutables CommandLineOptions
o = do
Map ExeName String
trustedExes <- LibM (Map ExeName String) -> TCM (Map ExeName String)
forall a. LibM a -> TCM a
libToTCM (LibM (Map ExeName String) -> TCM (Map ExeName String))
-> LibM (Map ExeName String) -> TCM (Map ExeName String)
forall a b. (a -> b) -> a -> b
$ LibM (Map ExeName String)
getTrustedExecutables
CommandLineOptions -> TCMT IO CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return CommandLineOptions
o{ optTrustedExecutables :: Map ExeName String
optTrustedExecutables = Map ExeName String
trustedExes }
setOptionsFromPragma :: OptionsPragma -> TCM ()
setOptionsFromPragma :: [String] -> TCM ()
setOptionsFromPragma [String]
ps = do
CommandLineOptions
opts <- TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
OptM PragmaOptions -> TCMT IO (Either String PragmaOptions)
forall (m :: * -> *) opts.
Monad m =>
OptM opts -> m (Either String opts)
runOptM ([String] -> CommandLineOptions -> OptM PragmaOptions
parsePragmaOptions [String]
ps CommandLineOptions
opts) TCMT IO (Either String PragmaOptions)
-> (Either String PragmaOptions -> TCM ()) -> TCM ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Left String
err -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError String
err
Right PragmaOptions
opts' -> PragmaOptions -> TCM ()
setPragmaOptions PragmaOptions
opts'
enableDisplayForms :: MonadTCEnv m => m a -> m a
enableDisplayForms :: m a -> m a
enableDisplayForms =
(TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \TCEnv
e -> TCEnv
e { envDisplayFormsEnabled :: SafeMode
envDisplayFormsEnabled = SafeMode
True }
disableDisplayForms :: MonadTCEnv m => m a -> m a
disableDisplayForms :: m a -> m a
disableDisplayForms =
(TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \TCEnv
e -> TCEnv
e { envDisplayFormsEnabled :: SafeMode
envDisplayFormsEnabled = SafeMode
False }
displayFormsEnabled :: MonadTCEnv m => m Bool
displayFormsEnabled :: m SafeMode
displayFormsEnabled = (TCEnv -> SafeMode) -> m SafeMode
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> SafeMode
envDisplayFormsEnabled
getIncludeDirs :: HasOptions m => m [AbsolutePath]
getIncludeDirs :: m [AbsolutePath]
getIncludeDirs = do
[AbsolutePath]
incs <- CommandLineOptions -> [AbsolutePath]
optAbsoluteIncludePaths (CommandLineOptions -> [AbsolutePath])
-> m CommandLineOptions -> m [AbsolutePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
case [AbsolutePath]
incs of
[] -> m [AbsolutePath]
forall a. HasCallStack => a
__IMPOSSIBLE__
[AbsolutePath]
_ -> [AbsolutePath] -> m [AbsolutePath]
forall (m :: * -> *) a. Monad m => a -> m a
return [AbsolutePath]
incs
setIncludeDirs :: [FilePath]
-> AbsolutePath
-> TCM ()
setIncludeDirs :: [String] -> AbsolutePath -> TCM ()
setIncludeDirs [String]
incs AbsolutePath
root = do
[AbsolutePath]
oldIncs <- (TCState -> [AbsolutePath]) -> TCMT IO [AbsolutePath]
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC TCState -> [AbsolutePath]
forall a. LensIncludePaths a => a -> [AbsolutePath]
Lens.getAbsoluteIncludePaths
[String]
incs <- [String] -> TCM [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> TCM [String]) -> [String] -> TCM [String]
forall a b. (a -> b) -> a -> b
$ if [String] -> SafeMode
forall (t :: * -> *) a. Foldable t => t a -> SafeMode
null [String]
incs then [String
"."] else [String]
incs
[AbsolutePath]
incs <- [AbsolutePath] -> TCMT IO [AbsolutePath]
forall (m :: * -> *) a. Monad m => a -> m a
return ([AbsolutePath] -> TCMT IO [AbsolutePath])
-> [AbsolutePath] -> TCMT IO [AbsolutePath]
forall a b. (a -> b) -> a -> b
$ (String -> AbsolutePath) -> [String] -> [AbsolutePath]
forall a b. (a -> b) -> [a] -> [b]
map (String -> AbsolutePath
mkAbsolute (String -> AbsolutePath)
-> (String -> String) -> String -> AbsolutePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbsolutePath -> String
filePath AbsolutePath
root String -> String -> String
</>)) [String]
incs
AbsolutePath
primdir <- IO AbsolutePath -> TCMT IO AbsolutePath
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO AbsolutePath -> TCMT IO AbsolutePath)
-> IO AbsolutePath -> TCMT IO AbsolutePath
forall a b. (a -> b) -> a -> b
$ String -> AbsolutePath
mkAbsolute (String -> AbsolutePath) -> IO String -> IO AbsolutePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO String
getPrimitiveLibDir
[AbsolutePath]
incs <- [AbsolutePath] -> TCMT IO [AbsolutePath]
forall (m :: * -> *) a. Monad m => a -> m a
return ([AbsolutePath] -> TCMT IO [AbsolutePath])
-> [AbsolutePath] -> TCMT IO [AbsolutePath]
forall a b. (a -> b) -> a -> b
$ (AbsolutePath -> AbsolutePath) -> [AbsolutePath] -> [AbsolutePath]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn AbsolutePath -> AbsolutePath
forall a. a -> a
id ([AbsolutePath] -> [AbsolutePath])
-> [AbsolutePath] -> [AbsolutePath]
forall a b. (a -> b) -> a -> b
$ [AbsolutePath]
incs [AbsolutePath] -> [AbsolutePath] -> [AbsolutePath]
forall a. [a] -> [a] -> [a]
++ [AbsolutePath
primdir]
String -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"setIncludeDirs" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
[ Doc
"Old include directories:"
, VerboseLevel -> Doc -> Doc
nest VerboseLevel
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (AbsolutePath -> Doc) -> [AbsolutePath] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map AbsolutePath -> Doc
forall a. Pretty a => a -> Doc
pretty [AbsolutePath]
oldIncs
, Doc
"New include directories:"
, VerboseLevel -> Doc -> Doc
nest VerboseLevel
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (AbsolutePath -> Doc) -> [AbsolutePath] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map AbsolutePath -> Doc
forall a. Pretty a => a -> Doc
pretty [AbsolutePath]
incs
]
SafeMode -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => SafeMode -> f () -> f ()
when ([AbsolutePath] -> [AbsolutePath]
forall a. Ord a => [a] -> [a]
sort [AbsolutePath]
oldIncs [AbsolutePath] -> [AbsolutePath] -> SafeMode
forall a. Eq a => a -> a -> SafeMode
/= [AbsolutePath] -> [AbsolutePath]
forall a. Ord a => [a] -> [a]
sort [AbsolutePath]
incs) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
InteractionOutputCallback
ho <- TCMT IO InteractionOutputCallback
forall (m :: * -> *). ReadTCState m => m InteractionOutputCallback
getInteractionOutputCallback
[TCWarning]
tcWarnings <- Lens' [TCWarning] TCState -> TCMT IO [TCWarning]
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' [TCWarning] TCState
stTCWarnings
Map String ProjectConfig
projectConfs <- Lens' (Map String ProjectConfig) TCState
-> TCMT IO (Map String ProjectConfig)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map String ProjectConfig) TCState
stProjectConfigs
Map String AgdaLibFile
agdaLibFiles <- Lens' (Map String AgdaLibFile) TCState
-> TCMT IO (Map String AgdaLibFile)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map String AgdaLibFile) TCState
stAgdaLibFiles
DecodedModules
decodedModules <- TCM DecodedModules
getDecodedModules
(DecodedModules
keptDecodedModules, ModuleToSource
modFile) <- [AbsolutePath]
-> DecodedModules -> TCM (DecodedModules, ModuleToSource)
modulesToKeep [AbsolutePath]
incs DecodedModules
decodedModules
TCM ()
resetAllState
Lens' [TCWarning] TCState -> [TCWarning] -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
setTCLens Lens' [TCWarning] TCState
stTCWarnings [TCWarning]
tcWarnings
Lens' (Map String ProjectConfig) TCState
-> Map String ProjectConfig -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
setTCLens Lens' (Map String ProjectConfig) TCState
stProjectConfigs Map String ProjectConfig
projectConfs
Lens' (Map String AgdaLibFile) TCState
-> Map String AgdaLibFile -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
setTCLens Lens' (Map String AgdaLibFile) TCState
stAgdaLibFiles Map String AgdaLibFile
agdaLibFiles
InteractionOutputCallback -> TCM ()
setInteractionOutputCallback InteractionOutputCallback
ho
DecodedModules -> TCM ()
setDecodedModules DecodedModules
keptDecodedModules
Lens' ModuleToSource TCState -> ModuleToSource -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
setTCLens Lens' ModuleToSource TCState
stModuleToSource ModuleToSource
modFile
[AbsolutePath] -> TCM ()
forall (m :: * -> *). MonadTCState m => [AbsolutePath] -> m ()
Lens.putAbsoluteIncludePaths [AbsolutePath]
incs
where
modulesToKeep
:: [AbsolutePath]
-> DecodedModules
-> TCM (DecodedModules, ModuleToSource)
modulesToKeep :: [AbsolutePath]
-> DecodedModules -> TCM (DecodedModules, ModuleToSource)
modulesToKeep [AbsolutePath]
incs DecodedModules
old = Map ModuleName ModuleInfo
-> ModuleToSource
-> [ModuleInfo]
-> TCM (DecodedModules, ModuleToSource)
process Map ModuleName ModuleInfo
forall k a. Map k a
Map.empty ModuleToSource
forall k a. Map k a
Map.empty [ModuleInfo]
modules
where
dependencyGraph :: G.Graph A.ModuleName ()
dependencyGraph :: Graph ModuleName ()
dependencyGraph =
[ModuleName] -> Graph ModuleName ()
forall n e. Ord n => [n] -> Graph n e
G.fromNodes
[ Interface -> ModuleName
iModuleName (Interface -> ModuleName) -> Interface -> ModuleName
forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Interface
miInterface ModuleInfo
m
| ModuleInfo
m <- DecodedModules -> [ModuleInfo]
forall k a. Map k a -> [a]
Map.elems DecodedModules
old
]
Graph ModuleName () -> Graph ModuleName () -> Graph ModuleName ()
forall n e. Ord n => Graph n e -> Graph n e -> Graph n e
`G.union`
[Edge ModuleName ()] -> Graph ModuleName ()
forall n e. Ord n => [Edge n e] -> Graph n e
G.fromEdges
[ Edge :: forall n e. n -> n -> e -> Edge n e
G.Edge
{ source :: ModuleName
source = Interface -> ModuleName
iModuleName (Interface -> ModuleName) -> Interface -> ModuleName
forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Interface
miInterface ModuleInfo
m
, target :: ModuleName
target = ModuleName
d
, label :: ()
label = ()
}
| ModuleInfo
m <- DecodedModules -> [ModuleInfo]
forall k a. Map k a -> [a]
Map.elems DecodedModules
old
, (ModuleName
d, Hash
_) <- Interface -> [(ModuleName, Hash)]
iImportedModules (Interface -> [(ModuleName, Hash)])
-> Interface -> [(ModuleName, Hash)]
forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Interface
miInterface ModuleInfo
m
]
modules :: [ModuleInfo]
modules :: [ModuleInfo]
modules =
(SCC ModuleName -> ModuleInfo) -> [SCC ModuleName] -> [ModuleInfo]
forall a b. (a -> b) -> [a] -> [b]
map (\case
Graph.CyclicSCC{} ->
ModuleInfo
forall a. HasCallStack => a
__IMPOSSIBLE__
Graph.AcyclicSCC ModuleName
m ->
case TopLevelModuleName -> DecodedModules -> Maybe ModuleInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (ModuleName -> TopLevelModuleName
A.toTopLevelModuleName ModuleName
m) DecodedModules
old of
Just ModuleInfo
m -> ModuleInfo
m
Maybe ModuleInfo
Nothing -> ModuleInfo
forall a. HasCallStack => a
__IMPOSSIBLE__) ([SCC ModuleName] -> [ModuleInfo])
-> [SCC ModuleName] -> [ModuleInfo]
forall a b. (a -> b) -> a -> b
$
Graph ModuleName () -> [SCC ModuleName]
forall n e. Ord n => Graph n e -> [SCC n]
G.sccs' Graph ModuleName ()
dependencyGraph
process ::
Map A.ModuleName ModuleInfo -> ModuleToSource -> [ModuleInfo] ->
TCM (DecodedModules, ModuleToSource)
process :: Map ModuleName ModuleInfo
-> ModuleToSource
-> [ModuleInfo]
-> TCM (DecodedModules, ModuleToSource)
process !Map ModuleName ModuleInfo
keep !ModuleToSource
modFile [] = (DecodedModules, ModuleToSource)
-> TCM (DecodedModules, ModuleToSource)
forall (m :: * -> *) a. Monad m => a -> m a
return
( [(TopLevelModuleName, ModuleInfo)] -> DecodedModules
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(TopLevelModuleName, ModuleInfo)] -> DecodedModules)
-> [(TopLevelModuleName, ModuleInfo)] -> DecodedModules
forall a b. (a -> b) -> a -> b
$
((ModuleName, ModuleInfo) -> (TopLevelModuleName, ModuleInfo))
-> [(ModuleName, ModuleInfo)] -> [(TopLevelModuleName, ModuleInfo)]
forall a b. (a -> b) -> [a] -> [b]
map ((ModuleName -> TopLevelModuleName)
-> (ModuleName, ModuleInfo) -> (TopLevelModuleName, ModuleInfo)
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst ModuleName -> TopLevelModuleName
A.toTopLevelModuleName) ([(ModuleName, ModuleInfo)] -> [(TopLevelModuleName, ModuleInfo)])
-> [(ModuleName, ModuleInfo)] -> [(TopLevelModuleName, ModuleInfo)]
forall a b. (a -> b) -> a -> b
$
Map ModuleName ModuleInfo -> [(ModuleName, ModuleInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList Map ModuleName ModuleInfo
keep
, ModuleToSource
modFile
)
process Map ModuleName ModuleInfo
keep ModuleToSource
modFile (ModuleInfo
m : [ModuleInfo]
ms) = do
let deps :: [ModuleName]
deps = ((ModuleName, Hash) -> ModuleName)
-> [(ModuleName, Hash)] -> [ModuleName]
forall a b. (a -> b) -> [a] -> [b]
map (ModuleName, Hash) -> ModuleName
forall a b. (a, b) -> a
fst ([(ModuleName, Hash)] -> [ModuleName])
-> [(ModuleName, Hash)] -> [ModuleName]
forall a b. (a -> b) -> a -> b
$ Interface -> [(ModuleName, Hash)]
iImportedModules (Interface -> [(ModuleName, Hash)])
-> Interface -> [(ModuleName, Hash)]
forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Interface
miInterface ModuleInfo
m
depsKept :: SafeMode
depsKept = (ModuleName -> SafeMode) -> [ModuleName] -> SafeMode
forall (t :: * -> *) a.
Foldable t =>
(a -> SafeMode) -> t a -> SafeMode
all (ModuleName -> Map ModuleName ModuleInfo -> SafeMode
forall k a. Ord k => k -> Map k a -> SafeMode
`Map.member` Map ModuleName ModuleInfo
keep) [ModuleName]
deps
(Map ModuleName ModuleInfo
keep, ModuleToSource
modFile) <-
if SafeMode -> SafeMode
not SafeMode
depsKept then (Map ModuleName ModuleInfo, ModuleToSource)
-> TCMT IO (Map ModuleName ModuleInfo, ModuleToSource)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map ModuleName ModuleInfo
keep, ModuleToSource
modFile) else do
let n :: ModuleName
n = Interface -> ModuleName
iModuleName (Interface -> ModuleName) -> Interface -> ModuleName
forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Interface
miInterface ModuleInfo
m
t :: TopLevelModuleName
t = ModuleName -> TopLevelModuleName
A.toTopLevelModuleName ModuleName
n
Either FindError SourceFile
oldF <- TopLevelModuleName -> TCM (Either FindError SourceFile)
findFile' TopLevelModuleName
t
(Either FindError SourceFile
newF, ModuleToSource
modFile) <- IO (Either FindError SourceFile, ModuleToSource)
-> TCMT IO (Either FindError SourceFile, ModuleToSource)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either FindError SourceFile, ModuleToSource)
-> TCMT IO (Either FindError SourceFile, ModuleToSource))
-> IO (Either FindError SourceFile, ModuleToSource)
-> TCMT IO (Either FindError SourceFile, ModuleToSource)
forall a b. (a -> b) -> a -> b
$ [AbsolutePath]
-> TopLevelModuleName
-> ModuleToSource
-> IO (Either FindError SourceFile, ModuleToSource)
findFile'' [AbsolutePath]
incs TopLevelModuleName
t ModuleToSource
modFile
(Map ModuleName ModuleInfo, ModuleToSource)
-> TCMT IO (Map ModuleName ModuleInfo, ModuleToSource)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Map ModuleName ModuleInfo, ModuleToSource)
-> TCMT IO (Map ModuleName ModuleInfo, ModuleToSource))
-> (Map ModuleName ModuleInfo, ModuleToSource)
-> TCMT IO (Map ModuleName ModuleInfo, ModuleToSource)
forall a b. (a -> b) -> a -> b
$ case (Either FindError SourceFile
oldF, Either FindError SourceFile
newF) of
(Right SourceFile
f1, Right SourceFile
f2) | SourceFile
f1 SourceFile -> SourceFile -> SafeMode
forall a. Eq a => a -> a -> SafeMode
== SourceFile
f2 ->
(ModuleName
-> ModuleInfo
-> Map ModuleName ModuleInfo
-> Map ModuleName ModuleInfo
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ModuleName
n ModuleInfo
m Map ModuleName ModuleInfo
keep, ModuleToSource
modFile)
(Either FindError SourceFile, Either FindError SourceFile)
_ -> (Map ModuleName ModuleInfo
keep, ModuleToSource
modFile)
Map ModuleName ModuleInfo
-> ModuleToSource
-> [ModuleInfo]
-> TCM (DecodedModules, ModuleToSource)
process Map ModuleName ModuleInfo
keep ModuleToSource
modFile [ModuleInfo]
ms
isPropEnabled :: HasOptions m => m Bool
isPropEnabled :: m SafeMode
isPropEnabled = PragmaOptions -> SafeMode
optProp (PragmaOptions -> SafeMode) -> m PragmaOptions -> m SafeMode
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
isTwoLevelEnabled :: HasOptions m => m Bool
isTwoLevelEnabled :: m SafeMode
isTwoLevelEnabled = WithDefault 'False -> SafeMode
forall (b :: SafeMode). KnownBool b => WithDefault b -> SafeMode
collapseDefault (WithDefault 'False -> SafeMode)
-> (PragmaOptions -> WithDefault 'False)
-> PragmaOptions
-> SafeMode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optTwoLevel (PragmaOptions -> SafeMode) -> m PragmaOptions -> m SafeMode
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
{-# SPECIALIZE hasUniversePolymorphism :: TCM Bool #-}
hasUniversePolymorphism :: HasOptions m => m Bool
hasUniversePolymorphism :: m SafeMode
hasUniversePolymorphism = PragmaOptions -> SafeMode
optUniversePolymorphism (PragmaOptions -> SafeMode) -> m PragmaOptions -> m SafeMode
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
showImplicitArguments :: HasOptions m => m Bool
showImplicitArguments :: m SafeMode
showImplicitArguments = PragmaOptions -> SafeMode
optShowImplicit (PragmaOptions -> SafeMode) -> m PragmaOptions -> m SafeMode
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
showIrrelevantArguments :: HasOptions m => m Bool
showIrrelevantArguments :: m SafeMode
showIrrelevantArguments = PragmaOptions -> SafeMode
optShowIrrelevant (PragmaOptions -> SafeMode) -> m PragmaOptions -> m SafeMode
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
showIdentitySubstitutions :: HasOptions m => m Bool
showIdentitySubstitutions :: m SafeMode
showIdentitySubstitutions = PragmaOptions -> SafeMode
optShowIdentitySubstitutions (PragmaOptions -> SafeMode) -> m PragmaOptions -> m SafeMode
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
withShowAllArguments :: ReadTCState m => m a -> m a
withShowAllArguments :: m a -> m a
withShowAllArguments = SafeMode -> m a -> m a
forall (m :: * -> *) a. ReadTCState m => SafeMode -> m a -> m a
withShowAllArguments' SafeMode
True
withShowAllArguments' :: ReadTCState m => Bool -> m a -> m a
withShowAllArguments' :: SafeMode -> m a -> m a
withShowAllArguments' SafeMode
yes = (PragmaOptions -> PragmaOptions) -> m a -> m a
forall (m :: * -> *) a.
ReadTCState m =>
(PragmaOptions -> PragmaOptions) -> m a -> m a
withPragmaOptions ((PragmaOptions -> PragmaOptions) -> m a -> m a)
-> (PragmaOptions -> PragmaOptions) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \ PragmaOptions
opts ->
PragmaOptions
opts { optShowImplicit :: SafeMode
optShowImplicit = SafeMode
yes, optShowIrrelevant :: SafeMode
optShowIrrelevant = SafeMode
yes }
withPragmaOptions :: ReadTCState m => (PragmaOptions -> PragmaOptions) -> m a -> m a
withPragmaOptions :: (PragmaOptions -> PragmaOptions) -> m a -> m a
withPragmaOptions = Lens' PragmaOptions TCState
-> (PragmaOptions -> PragmaOptions) -> m a -> m a
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a TCState -> (a -> a) -> m b -> m b
locallyTCState Lens' PragmaOptions TCState
stPragmaOptions
positivityCheckEnabled :: HasOptions m => m Bool
positivityCheckEnabled :: m SafeMode
positivityCheckEnabled = SafeMode -> SafeMode
not (SafeMode -> SafeMode)
-> (PragmaOptions -> SafeMode) -> PragmaOptions -> SafeMode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> SafeMode
optDisablePositivity (PragmaOptions -> SafeMode) -> m PragmaOptions -> m SafeMode
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
{-# SPECIALIZE typeInType :: TCM Bool #-}
typeInType :: HasOptions m => m Bool
typeInType :: m SafeMode
typeInType = SafeMode -> SafeMode
not (SafeMode -> SafeMode)
-> (PragmaOptions -> SafeMode) -> PragmaOptions -> SafeMode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> SafeMode
optUniverseCheck (PragmaOptions -> SafeMode) -> m PragmaOptions -> m SafeMode
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
etaEnabled :: HasOptions m => m Bool
etaEnabled :: m SafeMode
etaEnabled = PragmaOptions -> SafeMode
optEta (PragmaOptions -> SafeMode) -> m PragmaOptions -> m SafeMode
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
maxInstanceSearchDepth :: HasOptions m => m Int
maxInstanceSearchDepth :: m VerboseLevel
maxInstanceSearchDepth = PragmaOptions -> VerboseLevel
optInstanceSearchDepth (PragmaOptions -> VerboseLevel)
-> m PragmaOptions -> m VerboseLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
maxInversionDepth :: HasOptions m => m Int
maxInversionDepth :: m VerboseLevel
maxInversionDepth = PragmaOptions -> VerboseLevel
optInversionMaxDepth (PragmaOptions -> VerboseLevel)
-> m PragmaOptions -> m VerboseLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
getLanguage :: HasOptions m => m Language
getLanguage :: m Language
getLanguage = do
PragmaOptions
opts <- m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
Language -> m Language
forall (m :: * -> *) a. Monad m => a -> m a
return (Language -> m Language) -> Language -> m Language
forall a b. (a -> b) -> a -> b
$
if SafeMode -> SafeMode
not (WithDefault 'False -> SafeMode
forall (b :: SafeMode). KnownBool b => WithDefault b -> SafeMode
collapseDefault (PragmaOptions -> WithDefault 'False
optWithoutK PragmaOptions
opts)) then Language
WithK else
case PragmaOptions -> Maybe Cubical
optCubical PragmaOptions
opts of
Just Cubical
variant -> Cubical -> Language
Cubical Cubical
variant
Maybe Cubical
Nothing -> Language
WithoutK