module Agda.TypeChecking.Monad.Options where

import Prelude hiding (mapM)

import Control.Monad.Reader hiding (mapM)
import Control.Monad.Writer

import Data.Maybe

import System.Directory
import System.FilePath

import Agda.TypeChecking.Monad.Debug (reportSDoc)
import Agda.TypeChecking.Warnings
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Monad.Benchmark
import Agda.Interaction.Options
import qualified Agda.Interaction.Options.Lenses as Lens
import Agda.Interaction.Library
import Agda.Utils.FileName
import Agda.Utils.Maybe
import Agda.Utils.Pretty
import Agda.Utils.Except

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 = PragmaOptions -> [String]
unsafePragmaOptions PragmaOptions
opts
--  when (Lens.getSafeMode clo && not (null unsafe)) $ warning $ SafeFlagPragma unsafe
  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 :: * -> *). MonadWarning m => Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ [String] -> Warning
SafeFlagPragma [String]
unsafe
  Either String CommandLineOptions
ok <- IO (Either String CommandLineOptions)
-> TCMT IO (Either String CommandLineOptions)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either String CommandLineOptions)
 -> TCMT IO (Either String CommandLineOptions))
-> IO (Either String CommandLineOptions)
-> TCMT IO (Either String CommandLineOptions)
forall a b. (a -> b) -> a -> b
$ OptM CommandLineOptions -> IO (Either String CommandLineOptions)
forall a. OptM a -> IO (Either String a)
runOptM (OptM CommandLineOptions -> IO (Either String CommandLineOptions))
-> OptM CommandLineOptions -> IO (Either String CommandLineOptions)
forall a b. (a -> b) -> a -> b
$ Flag CommandLineOptions
checkOpts (CommandLineOptions
clo { optPragmaOptions :: PragmaOptions
optPragmaOptions = PragmaOptions
opts })
  case Either String CommandLineOptions
ok of
    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
  Either String CommandLineOptions
z <- IO (Either String CommandLineOptions)
-> TCMT IO (Either String CommandLineOptions)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either String CommandLineOptions)
 -> TCMT IO (Either String CommandLineOptions))
-> IO (Either String CommandLineOptions)
-> TCMT IO (Either String CommandLineOptions)
forall a b. (a -> b) -> a -> b
$ OptM CommandLineOptions -> IO (Either String CommandLineOptions)
forall a. OptM a -> IO (Either String a)
runOptM (OptM CommandLineOptions -> IO (Either String CommandLineOptions))
-> OptM CommandLineOptions -> IO (Either String CommandLineOptions)
forall a b. (a -> b) -> a -> b
$ Flag CommandLineOptions
checkOpts CommandLineOptions
opts
  case Either String CommandLineOptions
z of
    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
  (Either Doc a
z, [LibWarning]
warns) <- IO (Either Doc a, [LibWarning])
-> TCMT IO (Either Doc a, [LibWarning])
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either Doc a, [LibWarning])
 -> TCMT IO (Either Doc a, [LibWarning]))
-> IO (Either Doc a, [LibWarning])
-> TCMT IO (Either Doc a, [LibWarning])
forall a b. (a -> b) -> a -> b
$ WriterT [LibWarning] IO (Either Doc a)
-> IO (Either Doc a, [LibWarning])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT [LibWarning] IO (Either Doc a)
 -> IO (Either Doc a, [LibWarning]))
-> WriterT [LibWarning] IO (Either Doc a)
-> IO (Either Doc a, [LibWarning])
forall a b. (a -> b) -> a -> b
$ LibM a -> WriterT [LibWarning] IO (Either Doc a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT LibM a
m

  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 :: * -> *). 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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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

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
forall (t :: * -> *). Foldable t => t SafeMode -> SafeMode
or [ SafeMode -> SafeMode
not (SafeMode -> SafeMode) -> SafeMode -> SafeMode
forall a b. (a -> b) -> a -> b
$ CommandLineOptions -> SafeMode
optUseLibs CommandLineOptions
o
       , CommandLineOptions -> SafeMode
optShowVersion 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
forall (t :: * -> *). Foldable t => t SafeMode -> SafeMode
or [ SafeMode -> SafeMode
not (SafeMode -> SafeMode) -> SafeMode -> SafeMode
forall a b. (a -> b) -> a -> b
$ [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
not (SafeMode -> SafeMode) -> SafeMode -> SafeMode
forall a b. (a -> b) -> a -> b
$ CommandLineOptions -> SafeMode
optUseLibs CommandLineOptions
o
       , CommandLineOptions -> SafeMode
optShowVersion 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 }

setOptionsFromPragma :: OptionsPragma -> TCM ()
setOptionsFromPragma :: [String] -> TCM ()
setOptionsFromPragma [String]
ps = do
    CommandLineOptions
opts <- TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
    Either String PragmaOptions
z    <- IO (Either String PragmaOptions)
-> TCMT IO (Either String PragmaOptions)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either String PragmaOptions)
 -> TCMT IO (Either String PragmaOptions))
-> IO (Either String PragmaOptions)
-> TCMT IO (Either String PragmaOptions)
forall a b. (a -> b) -> a -> b
$ OptM PragmaOptions -> IO (Either String PragmaOptions)
forall a. OptM a -> IO (Either String a)
runOptM ([String] -> CommandLineOptions -> OptM PragmaOptions
parsePragmaOptions [String]
ps CommandLineOptions
opts)
    case Either String PragmaOptions
z of
      Left String
err    -> TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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

-- | 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 'stInteractionOutputCallback').
--
-- 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
  String
libdir <- IO String -> TCMT IO String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO String -> TCMT IO String) -> IO String -> TCMT IO String
forall a b. (a -> b) -> a -> b
$ IO String
defaultLibDir
      -- NB: This is an absolute file name, but
      -- Agda.Utils.FilePath wants to check absoluteness anyway.
  let primdir :: AbsolutePath
primdir = String -> AbsolutePath
mkAbsolute (String -> AbsolutePath) -> String -> AbsolutePath
forall a b. (a -> b) -> a -> b
$ String
libdir String -> String -> String
</> String
"prim"
      -- 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]
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
vcat
    [ Doc
"Old include directories:"
    , VerboseLevel -> Doc -> Doc
nest VerboseLevel
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [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
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]
oldIncs [AbsolutePath] -> [AbsolutePath] -> SafeMode
forall a. Eq a => a -> a -> SafeMode
/= [AbsolutePath]
incs) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    InteractionOutputCallback
ho <- TCM 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
    TCM ()
resetAllState
    Lens' [TCWarning] TCState -> [TCWarning] -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
setTCLens Lens' [TCWarning] TCState
stTCWarnings [TCWarning]
tcWarnings
    InteractionOutputCallback -> TCM ()
setInteractionOutputCallback InteractionOutputCallback
ho

  [AbsolutePath] -> TCM ()
Lens.putAbsoluteIncludePaths [AbsolutePath]
incs

setInputFile :: FilePath -> TCM ()
setInputFile :: String -> TCM ()
setInputFile String
file =
    do  CommandLineOptions
opts <- TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
        CommandLineOptions -> TCM ()
setCommandLineOptions (CommandLineOptions -> TCM ()) -> CommandLineOptions -> TCM ()
forall a b. (a -> b) -> a -> b
$
          CommandLineOptions
opts { optInputFile :: Maybe String
optInputFile = String -> Maybe String
forall a. a -> Maybe a
Just String
file }

-- | Should only be run if 'hasInputFile'.
getInputFile :: TCM AbsolutePath
getInputFile :: TCMT IO AbsolutePath
getInputFile = TCMT IO AbsolutePath
-> TCMT IO (Maybe AbsolutePath) -> TCMT IO AbsolutePath
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM TCMT IO AbsolutePath
forall a. HasCallStack => a
__IMPOSSIBLE__ (TCMT IO (Maybe AbsolutePath) -> TCMT IO AbsolutePath)
-> TCMT IO (Maybe AbsolutePath) -> TCMT IO AbsolutePath
forall a b. (a -> b) -> a -> b
$
  TCMT IO (Maybe AbsolutePath)
getInputFile'

-- | Return the 'optInputFile' as 'AbsolutePath', if any.
getInputFile' :: TCM (Maybe AbsolutePath)
getInputFile' :: TCMT IO (Maybe AbsolutePath)
getInputFile' = (String -> TCMT IO AbsolutePath)
-> Maybe String -> TCMT IO (Maybe AbsolutePath)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (IO AbsolutePath -> TCMT IO AbsolutePath
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO AbsolutePath -> TCMT IO AbsolutePath)
-> (String -> IO AbsolutePath) -> String -> TCMT IO AbsolutePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO AbsolutePath
absolute) (Maybe String -> TCMT IO (Maybe AbsolutePath))
-> TCMT IO (Maybe String) -> TCMT IO (Maybe AbsolutePath)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
  CommandLineOptions -> Maybe String
optInputFile (CommandLineOptions -> Maybe String)
-> TCMT IO CommandLineOptions -> TCMT IO (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions

hasInputFile :: HasOptions m => m Bool
hasInputFile :: m SafeMode
hasInputFile = Maybe String -> SafeMode
forall a. Maybe a -> SafeMode
isJust (Maybe String -> SafeMode)
-> (CommandLineOptions -> Maybe String)
-> CommandLineOptions
-> SafeMode
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CommandLineOptions -> Maybe String
optInputFile (CommandLineOptions -> SafeMode)
-> m CommandLineOptions -> m SafeMode
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions

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

{-# 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

-- | 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

ignoreInterfaces :: HasOptions m => m Bool
ignoreInterfaces :: m SafeMode
ignoreInterfaces = CommandLineOptions -> SafeMode
optIgnoreInterfaces (CommandLineOptions -> SafeMode)
-> m CommandLineOptions -> m SafeMode
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions

ignoreAllInterfaces :: HasOptions m => m Bool
ignoreAllInterfaces :: m SafeMode
ignoreAllInterfaces = CommandLineOptions -> SafeMode
optIgnoreAllInterfaces (CommandLineOptions -> SafeMode)
-> m CommandLineOptions -> m SafeMode
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions

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