-- | Lenses for 'CommandLineOptions' and 'PragmaOptions'.
--
--   Add as needed.
--
--   Nothing smart happening here.

module Agda.Interaction.Options.Lenses where

import Control.Monad.IO.Class   ( MonadIO(..) )

import Data.Set (Set)
import qualified Data.Set as Set

import System.FilePath ((</>))

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.State
import Agda.Interaction.Library (getPrimitiveLibDir)
import Agda.Interaction.Options

import Agda.Utils.Lens
import Agda.Utils.FileName

---------------------------------------------------------------------------
-- * Pragma options
---------------------------------------------------------------------------

class LensPragmaOptions a where
  getPragmaOptions  :: a -> PragmaOptions
  setPragmaOptions  :: PragmaOptions -> a -> a
  mapPragmaOptions  :: (PragmaOptions -> PragmaOptions) -> a -> a
  lensPragmaOptions :: Lens' PragmaOptions a
  -- lensPragmaOptions :: forall f. Functor f => (PragmaOptions -> f PragmaOptions) -> a -> f a

  -- default implementations
  setPragmaOptions     = forall a.
LensPragmaOptions a =>
(PragmaOptions -> PragmaOptions) -> a -> a
mapPragmaOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const
  mapPragmaOptions PragmaOptions -> PragmaOptions
f a
a = forall a. LensPragmaOptions a => PragmaOptions -> a -> a
setPragmaOptions (PragmaOptions -> PragmaOptions
f forall a b. (a -> b) -> a -> b
$ forall a. LensPragmaOptions a => a -> PragmaOptions
getPragmaOptions a
a) a
a

instance LensPragmaOptions CommandLineOptions where
  getPragmaOptions :: CommandLineOptions -> PragmaOptions
getPragmaOptions = CommandLineOptions -> PragmaOptions
optPragmaOptions
  setPragmaOptions :: PragmaOptions -> CommandLineOptions -> CommandLineOptions
setPragmaOptions PragmaOptions
opts CommandLineOptions
st = CommandLineOptions
st { optPragmaOptions :: PragmaOptions
optPragmaOptions = PragmaOptions
opts }
  lensPragmaOptions :: Lens' PragmaOptions CommandLineOptions
lensPragmaOptions PragmaOptions -> f PragmaOptions
f CommandLineOptions
st = PragmaOptions -> f PragmaOptions
f (CommandLineOptions -> PragmaOptions
optPragmaOptions CommandLineOptions
st) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ PragmaOptions
opts -> CommandLineOptions
st { optPragmaOptions :: PragmaOptions
optPragmaOptions = PragmaOptions
opts }

instance LensPragmaOptions TCState where
  getPragmaOptions :: TCState -> PragmaOptions
getPragmaOptions = (forall o i. o -> Lens' i o -> i
^.Lens' PragmaOptions TCState
stPragmaOptions)
  setPragmaOptions :: PragmaOptions -> TCState -> TCState
setPragmaOptions = forall i o. Lens' i o -> LensSet i o
set Lens' PragmaOptions TCState
stPragmaOptions
  lensPragmaOptions :: Lens' PragmaOptions TCState
lensPragmaOptions = Lens' PragmaOptions TCState
stPragmaOptions

modifyPragmaOptions :: MonadTCState m => (PragmaOptions -> PragmaOptions) -> m ()
modifyPragmaOptions :: forall (m :: * -> *).
MonadTCState m =>
(PragmaOptions -> PragmaOptions) -> m ()
modifyPragmaOptions = forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
LensPragmaOptions a =>
(PragmaOptions -> PragmaOptions) -> a -> a
mapPragmaOptions

---------------------------------------------------------------------------
-- ** Verbosity in the local pragma options
---------------------------------------------------------------------------

class LensVerbosity a where
  getVerbosity :: a -> Verbosity
  setVerbosity :: Verbosity -> a -> a
  mapVerbosity :: (Verbosity -> Verbosity) -> a -> a

  -- default implementations
  setVerbosity     = forall a. LensVerbosity a => (Verbosity -> Verbosity) -> a -> a
mapVerbosity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const
  mapVerbosity Verbosity -> Verbosity
f a
a = forall a. LensVerbosity a => Verbosity -> a -> a
setVerbosity (Verbosity -> Verbosity
f forall a b. (a -> b) -> a -> b
$ forall a. LensVerbosity a => a -> Verbosity
getVerbosity a
a) a
a

instance LensVerbosity PragmaOptions where
  getVerbosity :: PragmaOptions -> Verbosity
getVerbosity = PragmaOptions -> Verbosity
optVerbose
  setVerbosity :: Verbosity -> PragmaOptions -> PragmaOptions
setVerbosity Verbosity
is PragmaOptions
opts = PragmaOptions
opts { optVerbose :: Verbosity
optVerbose = Verbosity
is }

instance LensVerbosity TCState where
  getVerbosity :: TCState -> Verbosity
getVerbosity = forall a. LensVerbosity a => a -> Verbosity
getVerbosity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensPragmaOptions a => a -> PragmaOptions
getPragmaOptions
  mapVerbosity :: (Verbosity -> Verbosity) -> TCState -> TCState
mapVerbosity = forall a.
LensPragmaOptions a =>
(PragmaOptions -> PragmaOptions) -> a -> a
mapPragmaOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensVerbosity a => (Verbosity -> Verbosity) -> a -> a
mapVerbosity

modifyVerbosity :: MonadTCState m => (Verbosity -> Verbosity) -> m ()
modifyVerbosity :: forall (m :: * -> *).
MonadTCState m =>
(Verbosity -> Verbosity) -> m ()
modifyVerbosity = forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensVerbosity a => (Verbosity -> Verbosity) -> a -> a
mapVerbosity

putVerbosity :: MonadTCState m => Verbosity -> m ()
putVerbosity :: forall (m :: * -> *). MonadTCState m => Verbosity -> m ()
putVerbosity = forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensVerbosity a => Verbosity -> a -> a
setVerbosity

---------------------------------------------------------------------------
-- * Command line options
---------------------------------------------------------------------------

class LensCommandLineOptions a where
  getCommandLineOptions :: a -> CommandLineOptions
  setCommandLineOptions :: CommandLineOptions -> a -> a
  mapCommandLineOptions :: (CommandLineOptions -> CommandLineOptions) -> a -> a

  -- default implementations
  setCommandLineOptions     = forall a.
LensCommandLineOptions a =>
(CommandLineOptions -> CommandLineOptions) -> a -> a
mapCommandLineOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const
  mapCommandLineOptions CommandLineOptions -> CommandLineOptions
f a
a = forall a. LensCommandLineOptions a => CommandLineOptions -> a -> a
setCommandLineOptions (CommandLineOptions -> CommandLineOptions
f forall a b. (a -> b) -> a -> b
$ forall a. LensCommandLineOptions a => a -> CommandLineOptions
getCommandLineOptions a
a) a
a

instance LensCommandLineOptions PersistentTCState where
  getCommandLineOptions :: PersistentTCState -> CommandLineOptions
getCommandLineOptions = PersistentTCState -> CommandLineOptions
stPersistentOptions
  setCommandLineOptions :: CommandLineOptions -> PersistentTCState -> PersistentTCState
setCommandLineOptions CommandLineOptions
opts PersistentTCState
st = PersistentTCState
st { stPersistentOptions :: CommandLineOptions
stPersistentOptions = CommandLineOptions
opts }

instance LensCommandLineOptions TCState where
  getCommandLineOptions :: TCState -> CommandLineOptions
getCommandLineOptions = forall a. LensCommandLineOptions a => a -> CommandLineOptions
getCommandLineOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState
  mapCommandLineOptions :: (CommandLineOptions -> CommandLineOptions) -> TCState -> TCState
mapCommandLineOptions = (PersistentTCState -> PersistentTCState) -> TCState -> TCState
updatePersistentState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
LensCommandLineOptions a =>
(CommandLineOptions -> CommandLineOptions) -> a -> a
mapCommandLineOptions

modifyCommandLineOptions :: MonadTCState m => (CommandLineOptions -> CommandLineOptions) -> m ()
modifyCommandLineOptions :: forall (m :: * -> *).
MonadTCState m =>
(CommandLineOptions -> CommandLineOptions) -> m ()
modifyCommandLineOptions = forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
LensCommandLineOptions a =>
(CommandLineOptions -> CommandLineOptions) -> a -> a
mapCommandLineOptions

---------------------------------------------------------------------------
-- ** Safe mode
---------------------------------------------------------------------------

type SafeMode = Bool

class LensSafeMode a where
  getSafeMode :: a -> SafeMode
  setSafeMode :: SafeMode -> a -> a
  mapSafeMode :: (SafeMode -> SafeMode) -> a -> a

  -- default implementations
  setSafeMode     = forall a. LensSafeMode a => (SafeMode -> SafeMode) -> a -> a
mapSafeMode forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const
  mapSafeMode SafeMode -> SafeMode
f a
a = forall a. LensSafeMode a => SafeMode -> a -> a
setSafeMode (SafeMode -> SafeMode
f forall a b. (a -> b) -> a -> b
$ forall a. LensSafeMode a => a -> SafeMode
getSafeMode a
a) a
a

instance LensSafeMode PragmaOptions where
  getSafeMode :: PragmaOptions -> SafeMode
getSafeMode = PragmaOptions -> SafeMode
optSafe
  setSafeMode :: SafeMode -> PragmaOptions -> PragmaOptions
setSafeMode SafeMode
is PragmaOptions
opts = PragmaOptions
opts { optSafe :: SafeMode
optSafe = SafeMode
is } -- setSafeOption

instance LensSafeMode CommandLineOptions where
  getSafeMode :: CommandLineOptions -> SafeMode
getSafeMode = forall a. LensSafeMode a => a -> SafeMode
getSafeMode forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensPragmaOptions a => a -> PragmaOptions
getPragmaOptions
  mapSafeMode :: (SafeMode -> SafeMode) -> CommandLineOptions -> CommandLineOptions
mapSafeMode = forall a.
LensPragmaOptions a =>
(PragmaOptions -> PragmaOptions) -> a -> a
mapPragmaOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensSafeMode a => (SafeMode -> SafeMode) -> a -> a
mapSafeMode

instance LensSafeMode PersistentTCState where
  getSafeMode :: PersistentTCState -> SafeMode
getSafeMode = forall a. LensSafeMode a => a -> SafeMode
getSafeMode forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensCommandLineOptions a => a -> CommandLineOptions
getCommandLineOptions
  mapSafeMode :: (SafeMode -> SafeMode) -> PersistentTCState -> PersistentTCState
mapSafeMode = forall a.
LensCommandLineOptions a =>
(CommandLineOptions -> CommandLineOptions) -> a -> a
mapCommandLineOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensSafeMode a => (SafeMode -> SafeMode) -> a -> a
mapSafeMode

instance LensSafeMode TCState where
  getSafeMode :: TCState -> SafeMode
getSafeMode = forall a. LensSafeMode a => a -> SafeMode
getSafeMode forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensCommandLineOptions a => a -> CommandLineOptions
getCommandLineOptions
  mapSafeMode :: (SafeMode -> SafeMode) -> TCState -> TCState
mapSafeMode = forall a.
LensCommandLineOptions a =>
(CommandLineOptions -> CommandLineOptions) -> a -> a
mapCommandLineOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensSafeMode a => (SafeMode -> SafeMode) -> a -> a
mapSafeMode

modifySafeMode :: MonadTCState m => (SafeMode -> SafeMode) -> m ()
modifySafeMode :: forall (m :: * -> *).
MonadTCState m =>
(SafeMode -> SafeMode) -> m ()
modifySafeMode = forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensSafeMode a => (SafeMode -> SafeMode) -> a -> a
mapSafeMode

putSafeMode :: MonadTCState m => SafeMode -> m ()
putSafeMode :: forall (m :: * -> *). MonadTCState m => SafeMode -> m ()
putSafeMode = forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensSafeMode a => SafeMode -> a -> a
setSafeMode

-- | These builtins may use postulates, and are still considered --safe

builtinModulesWithSafePostulates :: Set FilePath
builtinModulesWithSafePostulates :: Set FilePath
builtinModulesWithSafePostulates =
  Set FilePath
primitiveModules forall a. Ord a => Set a -> Set a -> Set a
`Set.union` (forall a. Ord a => [a] -> Set a
Set.fromList
  [ FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Bool.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Char.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Char" FilePath -> FilePath -> FilePath
</> FilePath
"Properties.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Coinduction.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Cubical" FilePath -> FilePath -> FilePath
</> FilePath
"Glue.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Cubical" FilePath -> FilePath -> FilePath
</> FilePath
"HCompU.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Cubical" FilePath -> FilePath -> FilePath
</> FilePath
"Id.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Cubical" FilePath -> FilePath -> FilePath
</> FilePath
"Path.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Cubical" FilePath -> FilePath -> FilePath
</> FilePath
"Sub.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Equality" FilePath -> FilePath -> FilePath
</> FilePath
"Erase.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Equality.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Float.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Float" FilePath -> FilePath -> FilePath
</> FilePath
"Properties.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"FromNat.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"FromNeg.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"FromString.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Int.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"IO.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"List.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Maybe.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Nat.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Reflection.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Reflection" FilePath -> FilePath -> FilePath
</> FilePath
"Properties.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Reflection" FilePath -> FilePath -> FilePath
</> FilePath
"External.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Sigma.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Size.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Strict.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"String.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"String" FilePath -> FilePath -> FilePath
</> FilePath
"Properties.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Unit.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Word.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Word" FilePath -> FilePath -> FilePath
</> FilePath
"Properties.agda"
  ])

-- | These builtins may not use postulates under --safe. They are not
--   automatically unsafe, but will be if they use an unsafe feature.

builtinModulesWithUnsafePostulates :: Set FilePath
builtinModulesWithUnsafePostulates :: Set FilePath
builtinModulesWithUnsafePostulates = forall a. Ord a => [a] -> Set a
Set.fromList
  [ FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"TrustMe.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Builtin" FilePath -> FilePath -> FilePath
</> FilePath
"Equality" FilePath -> FilePath -> FilePath
</> FilePath
"Rewrite.agda"
  ]

primitiveModules :: Set FilePath
primitiveModules :: Set FilePath
primitiveModules = forall a. Ord a => [a] -> Set a
Set.fromList
  [ FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Primitive.agda"
  , FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Primitive" FilePath -> FilePath -> FilePath
</> FilePath
"Cubical.agda"
  ]

builtinModules :: Set FilePath
builtinModules :: Set FilePath
builtinModules = Set FilePath
builtinModulesWithSafePostulates forall a. Ord a => Set a -> Set a -> Set a
`Set.union`
                 Set FilePath
builtinModulesWithUnsafePostulates

isPrimitiveModule :: MonadIO m => FilePath -> m Bool
isPrimitiveModule :: forall (m :: * -> *). MonadIO m => FilePath -> m SafeMode
isPrimitiveModule FilePath
file = do
  FilePath
libdirPrim <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO FilePath
getPrimitiveLibDir
  forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath
file forall a. Ord a => a -> Set a -> SafeMode
`Set.member` forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (FilePath
libdirPrim FilePath -> FilePath -> FilePath
</>) Set FilePath
primitiveModules)

isBuiltinModule :: MonadIO m => FilePath -> m Bool
isBuiltinModule :: forall (m :: * -> *). MonadIO m => FilePath -> m SafeMode
isBuiltinModule FilePath
file = do
  FilePath
libdirPrim <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO FilePath
getPrimitiveLibDir
  forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath
file forall a. Ord a => a -> Set a -> SafeMode
`Set.member` forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (FilePath
libdirPrim FilePath -> FilePath -> FilePath
</>) Set FilePath
builtinModules)

isBuiltinModuleWithSafePostulates :: MonadIO m => FilePath -> m Bool
isBuiltinModuleWithSafePostulates :: forall (m :: * -> *). MonadIO m => FilePath -> m SafeMode
isBuiltinModuleWithSafePostulates FilePath
file = do
  FilePath
libdirPrim <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO FilePath
getPrimitiveLibDir
  let safeBuiltins :: Set FilePath
safeBuiltins   = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (FilePath
libdirPrim FilePath -> FilePath -> FilePath
</>) Set FilePath
builtinModulesWithSafePostulates
  forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath
file forall a. Ord a => a -> Set a -> SafeMode
`Set.member` Set FilePath
safeBuiltins)

---------------------------------------------------------------------------
-- ** Include directories
---------------------------------------------------------------------------

class LensIncludePaths a where
  getIncludePaths :: a -> [FilePath]
  setIncludePaths :: [FilePath] -> a -> a
  mapIncludePaths :: ([FilePath] -> [FilePath]) -> a -> a

  getAbsoluteIncludePaths :: a -> [AbsolutePath]
  setAbsoluteIncludePaths :: [AbsolutePath] -> a -> a
  mapAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath]) -> a -> a

  -- default implementations
  setIncludePaths     = forall a.
LensIncludePaths a =>
([FilePath] -> [FilePath]) -> a -> a
mapIncludePaths forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const
  mapIncludePaths [FilePath] -> [FilePath]
f a
a = forall a. LensIncludePaths a => [FilePath] -> a -> a
setIncludePaths ([FilePath] -> [FilePath]
f forall a b. (a -> b) -> a -> b
$ forall a. LensIncludePaths a => a -> [FilePath]
getIncludePaths a
a) a
a
  setAbsoluteIncludePaths     = forall a.
LensIncludePaths a =>
([AbsolutePath] -> [AbsolutePath]) -> a -> a
mapAbsoluteIncludePaths forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const
  mapAbsoluteIncludePaths [AbsolutePath] -> [AbsolutePath]
f a
a = forall a. LensIncludePaths a => [AbsolutePath] -> a -> a
setAbsoluteIncludePaths ([AbsolutePath] -> [AbsolutePath]
f forall a b. (a -> b) -> a -> b
$ forall a. LensIncludePaths a => a -> [AbsolutePath]
getAbsoluteIncludePaths a
a) a
a

instance LensIncludePaths CommandLineOptions where
  getIncludePaths :: CommandLineOptions -> [FilePath]
getIncludePaths = CommandLineOptions -> [FilePath]
optIncludePaths
  setIncludePaths :: [FilePath] -> CommandLineOptions -> CommandLineOptions
setIncludePaths [FilePath]
is CommandLineOptions
opts = CommandLineOptions
opts { optIncludePaths :: [FilePath]
optIncludePaths = [FilePath]
is }
  getAbsoluteIncludePaths :: CommandLineOptions -> [AbsolutePath]
getAbsoluteIncludePaths = CommandLineOptions -> [AbsolutePath]
optAbsoluteIncludePaths
  setAbsoluteIncludePaths :: [AbsolutePath] -> CommandLineOptions -> CommandLineOptions
setAbsoluteIncludePaths [AbsolutePath]
is CommandLineOptions
opts = CommandLineOptions
opts { optAbsoluteIncludePaths :: [AbsolutePath]
optAbsoluteIncludePaths = [AbsolutePath]
is }

instance LensIncludePaths PersistentTCState where
  getIncludePaths :: PersistentTCState -> [FilePath]
getIncludePaths = forall a. LensIncludePaths a => a -> [FilePath]
getIncludePaths forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensCommandLineOptions a => a -> CommandLineOptions
getCommandLineOptions
  mapIncludePaths :: ([FilePath] -> [FilePath])
-> PersistentTCState -> PersistentTCState
mapIncludePaths = forall a.
LensCommandLineOptions a =>
(CommandLineOptions -> CommandLineOptions) -> a -> a
mapCommandLineOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
LensIncludePaths a =>
([FilePath] -> [FilePath]) -> a -> a
mapIncludePaths
  getAbsoluteIncludePaths :: PersistentTCState -> [AbsolutePath]
getAbsoluteIncludePaths = forall a. LensIncludePaths a => a -> [AbsolutePath]
getAbsoluteIncludePaths forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensCommandLineOptions a => a -> CommandLineOptions
getCommandLineOptions
  mapAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath])
-> PersistentTCState -> PersistentTCState
mapAbsoluteIncludePaths = forall a.
LensCommandLineOptions a =>
(CommandLineOptions -> CommandLineOptions) -> a -> a
mapCommandLineOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
LensIncludePaths a =>
([AbsolutePath] -> [AbsolutePath]) -> a -> a
mapAbsoluteIncludePaths

instance LensIncludePaths TCState where
  getIncludePaths :: TCState -> [FilePath]
getIncludePaths = forall a. LensIncludePaths a => a -> [FilePath]
getIncludePaths forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensCommandLineOptions a => a -> CommandLineOptions
getCommandLineOptions
  mapIncludePaths :: ([FilePath] -> [FilePath]) -> TCState -> TCState
mapIncludePaths = forall a.
LensCommandLineOptions a =>
(CommandLineOptions -> CommandLineOptions) -> a -> a
mapCommandLineOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
LensIncludePaths a =>
([FilePath] -> [FilePath]) -> a -> a
mapIncludePaths
  getAbsoluteIncludePaths :: TCState -> [AbsolutePath]
getAbsoluteIncludePaths = forall a. LensIncludePaths a => a -> [AbsolutePath]
getAbsoluteIncludePaths forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensCommandLineOptions a => a -> CommandLineOptions
getCommandLineOptions
  mapAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath]) -> TCState -> TCState
mapAbsoluteIncludePaths = forall a.
LensCommandLineOptions a =>
(CommandLineOptions -> CommandLineOptions) -> a -> a
mapCommandLineOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
LensIncludePaths a =>
([AbsolutePath] -> [AbsolutePath]) -> a -> a
mapAbsoluteIncludePaths

modifyIncludePaths :: MonadTCState m => ([FilePath] -> [FilePath]) -> m ()
modifyIncludePaths :: forall (m :: * -> *).
MonadTCState m =>
([FilePath] -> [FilePath]) -> m ()
modifyIncludePaths = forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
LensIncludePaths a =>
([FilePath] -> [FilePath]) -> a -> a
mapIncludePaths

putIncludePaths :: MonadTCState m => [FilePath] -> m ()
putIncludePaths :: forall (m :: * -> *). MonadTCState m => [FilePath] -> m ()
putIncludePaths = forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensIncludePaths a => [FilePath] -> a -> a
setIncludePaths

modifyAbsoluteIncludePaths :: MonadTCState m => ([AbsolutePath] -> [AbsolutePath]) -> m ()
modifyAbsoluteIncludePaths :: forall (m :: * -> *).
MonadTCState m =>
([AbsolutePath] -> [AbsolutePath]) -> m ()
modifyAbsoluteIncludePaths = forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
LensIncludePaths a =>
([AbsolutePath] -> [AbsolutePath]) -> a -> a
mapAbsoluteIncludePaths

putAbsoluteIncludePaths :: MonadTCState m => [AbsolutePath] -> m ()
putAbsoluteIncludePaths :: forall (m :: * -> *). MonadTCState m => [AbsolutePath] -> m ()
putAbsoluteIncludePaths = forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensIncludePaths a => [AbsolutePath] -> a -> a
setAbsoluteIncludePaths

---------------------------------------------------------------------------
-- ** Include directories
---------------------------------------------------------------------------

type PersistentVerbosity = Verbosity
class LensPersistentVerbosity a where
  getPersistentVerbosity :: a -> PersistentVerbosity
  setPersistentVerbosity :: PersistentVerbosity -> a -> a
  mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> a -> a

  -- default implementations
  setPersistentVerbosity     = forall a.
LensPersistentVerbosity a =>
(Verbosity -> Verbosity) -> a -> a
mapPersistentVerbosity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const
  mapPersistentVerbosity Verbosity -> Verbosity
f a
a = forall a. LensPersistentVerbosity a => Verbosity -> a -> a
setPersistentVerbosity (Verbosity -> Verbosity
f forall a b. (a -> b) -> a -> b
$ forall a. LensPersistentVerbosity a => a -> Verbosity
getPersistentVerbosity a
a) a
a

instance LensPersistentVerbosity PragmaOptions where
  getPersistentVerbosity :: PragmaOptions -> Verbosity
getPersistentVerbosity = forall a. LensVerbosity a => a -> Verbosity
getVerbosity
  setPersistentVerbosity :: Verbosity -> PragmaOptions -> PragmaOptions
setPersistentVerbosity = forall a. LensVerbosity a => Verbosity -> a -> a
setVerbosity

instance LensPersistentVerbosity CommandLineOptions where
  getPersistentVerbosity :: CommandLineOptions -> Verbosity
getPersistentVerbosity = forall a. LensPersistentVerbosity a => a -> Verbosity
getPersistentVerbosity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensPragmaOptions a => a -> PragmaOptions
getPragmaOptions
  mapPersistentVerbosity :: (Verbosity -> Verbosity)
-> CommandLineOptions -> CommandLineOptions
mapPersistentVerbosity = forall a.
LensPragmaOptions a =>
(PragmaOptions -> PragmaOptions) -> a -> a
mapPragmaOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
LensPersistentVerbosity a =>
(Verbosity -> Verbosity) -> a -> a
mapPersistentVerbosity

instance LensPersistentVerbosity PersistentTCState where
  getPersistentVerbosity :: PersistentTCState -> Verbosity
getPersistentVerbosity = forall a. LensPersistentVerbosity a => a -> Verbosity
getPersistentVerbosity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensCommandLineOptions a => a -> CommandLineOptions
getCommandLineOptions
  mapPersistentVerbosity :: (Verbosity -> Verbosity) -> PersistentTCState -> PersistentTCState
mapPersistentVerbosity = forall a.
LensCommandLineOptions a =>
(CommandLineOptions -> CommandLineOptions) -> a -> a
mapCommandLineOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
LensPersistentVerbosity a =>
(Verbosity -> Verbosity) -> a -> a
mapPersistentVerbosity

instance LensPersistentVerbosity TCState where
  getPersistentVerbosity :: TCState -> Verbosity
getPersistentVerbosity = forall a. LensPersistentVerbosity a => a -> Verbosity
getPersistentVerbosity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensCommandLineOptions a => a -> CommandLineOptions
getCommandLineOptions
  mapPersistentVerbosity :: (Verbosity -> Verbosity) -> TCState -> TCState
mapPersistentVerbosity = forall a.
LensCommandLineOptions a =>
(CommandLineOptions -> CommandLineOptions) -> a -> a
mapCommandLineOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
LensPersistentVerbosity a =>
(Verbosity -> Verbosity) -> a -> a
mapPersistentVerbosity

modifyPersistentVerbosity :: MonadTCState m => (PersistentVerbosity -> PersistentVerbosity) -> m ()
modifyPersistentVerbosity :: forall (m :: * -> *).
MonadTCState m =>
(Verbosity -> Verbosity) -> m ()
modifyPersistentVerbosity = forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
LensPersistentVerbosity a =>
(Verbosity -> Verbosity) -> a -> a
mapPersistentVerbosity

putPersistentVerbosity :: MonadTCState m => PersistentVerbosity -> m ()
putPersistentVerbosity :: forall (m :: * -> *). MonadTCState m => Verbosity -> m ()
putPersistentVerbosity = forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensPersistentVerbosity a => Verbosity -> a -> a
setPersistentVerbosity