module Agda.Unused.Monad.Reader
(
Mode(..)
, Environment(..)
, askSkip
, askLocal
, askGlobalMain
, askRoot
, askIncludes
, localSkip
, localGlobal
) where
import Agda.Utils.FileName
(AbsolutePath)
import Control.Monad.Reader
(MonadReader, ask, local)
data Mode where
Skip
:: Mode
Local
:: Mode
Global
:: Mode
GlobalMain
:: Mode
deriving (Mode -> Mode -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Mode -> Mode -> Bool
$c/= :: Mode -> Mode -> Bool
== :: Mode -> Mode -> Bool
$c== :: Mode -> Mode -> Bool
Eq, Int -> Mode -> ShowS
[Mode] -> ShowS
Mode -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Mode] -> ShowS
$cshowList :: [Mode] -> ShowS
show :: Mode -> String
$cshow :: Mode -> String
showsPrec :: Int -> Mode -> ShowS
$cshowsPrec :: Int -> Mode -> ShowS
Show)
data Environment
= Environment
{ Environment -> Mode
environmentMode
:: !Mode
, Environment -> String
environmentRoot
:: !FilePath
, Environment -> [AbsolutePath]
environmentIncludes
:: ![AbsolutePath]
} deriving Int -> Environment -> ShowS
[Environment] -> ShowS
Environment -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Environment] -> ShowS
$cshowList :: [Environment] -> ShowS
show :: Environment -> String
$cshow :: Environment -> String
showsPrec :: Int -> Environment -> ShowS
$cshowsPrec :: Int -> Environment -> ShowS
Show
askMode
:: MonadReader Environment m
=> m Mode
askMode :: forall (m :: * -> *). MonadReader Environment m => m Mode
askMode
= Environment -> Mode
environmentMode forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *). MonadReader r m => m r
ask
askSkip
:: MonadReader Environment m
=> m Bool
askSkip :: forall (m :: * -> *). MonadReader Environment m => m Bool
askSkip
= (forall a. Eq a => a -> a -> Bool
== Mode
Skip) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadReader Environment m => m Mode
askMode
askLocal
:: MonadReader Environment m
=> m Bool
askLocal :: forall (m :: * -> *). MonadReader Environment m => m Bool
askLocal
= (forall a. Eq a => a -> a -> Bool
== Mode
Local) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadReader Environment m => m Mode
askMode
askGlobalMain
:: MonadReader Environment m
=> m Bool
askGlobalMain :: forall (m :: * -> *). MonadReader Environment m => m Bool
askGlobalMain
= (forall a. Eq a => a -> a -> Bool
== Mode
GlobalMain) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadReader Environment m => m Mode
askMode
askRoot
:: MonadReader Environment m
=> m FilePath
askRoot :: forall (m :: * -> *). MonadReader Environment m => m String
askRoot
= Environment -> String
environmentRoot forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *). MonadReader r m => m r
ask
askIncludes
:: MonadReader Environment m
=> m [AbsolutePath]
askIncludes :: forall (m :: * -> *). MonadReader Environment m => m [AbsolutePath]
askIncludes
= Environment -> [AbsolutePath]
environmentIncludes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *). MonadReader r m => m r
ask
localMode
:: MonadReader Environment m
=> Mode
-> m a
-> m a
localMode :: forall (m :: * -> *) a.
MonadReader Environment m =>
Mode -> m a -> m a
localMode Mode
m
= forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Environment
e -> Environment
e {environmentMode :: Mode
environmentMode = Mode
m})
localSkip
:: MonadReader Environment m
=> m a
-> m a
localSkip :: forall (m :: * -> *) a. MonadReader Environment m => m a -> m a
localSkip
= forall (m :: * -> *) a.
MonadReader Environment m =>
Mode -> m a -> m a
localMode Mode
Skip
localGlobal
:: MonadReader Environment m
=> m a
-> m a
localGlobal :: forall (m :: * -> *) a. MonadReader Environment m => m a -> m a
localGlobal
= forall (m :: * -> *) a.
MonadReader Environment m =>
Mode -> m a -> m a
localMode Mode
Global