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

-- | Sets the pragma options.

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

-- | Sets the command line options (both persistent and pragma options
-- are updated).
--
-- Relative include directories are made absolute with respect to the
-- current working directory. If the include directories have changed
-- (thus, they are 'Left' now, and were previously @'Right' something@),
-- then the state is reset (completely, see setIncludeDirs) .
--
-- An empty list of relative include directories (@'Left' []@) is
-- interpreted as @["."]@.
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
     -- ^ The base directory of relative paths.
  -> 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
     -- ^ The base directory of relative paths.
  -> 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
     -- ^ The base directory of relative paths.
  -> 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 }

-- This function is only called when an interactor exists
-- (i.e. when Agda actually does something).
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
  -- Wen, 2020-06-03
  -- Replace the map wholesale instead of computing the union because this function
  -- should never be called more than once, and doing so either has the same result
  -- or is a security risk.
  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'

-- | Disable display forms.
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 }

-- | Disable display forms.
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 }

-- | Check if display forms are enabled.
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

-- | Gets the include directories.
--
-- Precondition: 'optAbsoluteIncludePaths' must be nonempty (i.e.
-- 'setCommandLineOptions' must have run).

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

-- | Makes the given directories absolute and stores them as include
-- directories.
--
-- If the include directories change, then the state is reset
-- (completely, except for the include directories and some other
-- things).
--
-- An empty list is interpreted as @["."]@.

setIncludeDirs :: [FilePath]    -- ^ New include directories.
               -> AbsolutePath  -- ^ The base directory of relative paths.
               -> TCM ()
setIncludeDirs :: [String] -> AbsolutePath -> TCM ()
setIncludeDirs [String]
incs AbsolutePath
root = do
  -- save the previous include dirs
  [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

  -- Add the current dir if no include path is given
  [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
  -- Make paths absolute
  [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

  -- Andreas, 2013-10-30  Add default include dir
      -- NB: This is an absolute file name, but
      -- Agda.Utils.FilePath wants to check absoluteness anyway.
  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
      -- We add the default dir at the end, since it is then
      -- printed last in error messages.
      -- Might also be useful to overwrite default imports...
  [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
    ]

  -- Check whether the include dirs have changed.  If yes, reset state.
  -- Andreas, 2013-10-30 comments:
  -- The logic, namely using the include-dirs variable as a driver
  -- for the interaction, qualifies for a code-obfuscation contest.
  -- I guess one Boolean more in the state cost 10.000 EUR at the time
  -- of this implementation...
  --
  -- Andreas, perhaps you have misunderstood something: If the include
  -- directories have changed and we do not reset the decoded modules,
  -- then we might (depending on how the rest of the code works) end
  -- up in a situation in which we use the contents of the file
  -- "old-path/M.agda", when the user actually meant
  -- "new-path/M.agda".
  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 -- restore already generated warnings
    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  -- restore cached project configs & .agda-lib
    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    -- files, since they use absolute paths
    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
  -- A decoded module is kept if its top-level module name is resolved
  -- to the same absolute path using the old and the new include
  -- directories, and the same applies to all dependencies.
  --
  -- File system accesses are cached using the ModuleToSource data
  -- structure: For the old include directories this should mean that
  -- the file system is not accessed, but the file system is accessed
  -- for the new include directories, and certain changes to the file
  -- system could lead to interfaces being discarded. A new
  -- ModuleToSource structure, constructed using the new include
  -- directories, is returned.
  modulesToKeep
    :: [AbsolutePath]  -- New include directories.
    -> DecodedModules  -- Old decoded modules.
    -> 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
    -- A graph with one node per module in old, and an edge from m to
    -- n if the module corresponding to m imports the module
    -- corresponding to n.
    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
        ]

    -- All the modules from old, sorted so that all of a module's
    -- dependencies precede it in the list.
    modules :: [ModuleInfo]
    modules :: [ModuleInfo]
modules =
      (SCC ModuleName -> ModuleInfo) -> [SCC ModuleName] -> [ModuleInfo]
forall a b. (a -> b) -> [a] -> [b]
map (\case
              Graph.CyclicSCC{} ->
                -- Agda does not allow cycles in the dependency graph.
                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

-- | Switch on printing of implicit and irrelevant arguments.
--   E.g. for reification in with-function generation.
--
--   Restores all 'PragmaOptions' after completion.
--   Thus, do not attempt to make persistent 'PragmaOptions'
--   changes in a `withShowAllArguments` bracket.

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 }

-- | Change 'PragmaOptions' for a computation and restore afterwards.
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

-- | Returns the 'Language' currently in effect.

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