{- |
Module: Agda.Unused.Monad.Reader

A reader monad for determining unused code.
-}
module Agda.Unused.Monad.Reader

  ( -- * Definition
    
    Mode(..)
  , Environment(..)

    -- * Ask

  , askSkip
  , askLocal
  , askGlobalMain
  , askRoot
  , askIncludes

    -- * Local

  , localSkip
  , localGlobal

  ) where

import Agda.Utils.FileName
  (AbsolutePath)
import Control.Monad.Reader
  (MonadReader, ask, local)

-- ## Definition

-- | A type indicating how checking should be done.
data Mode where

  -- | Check nothing.
  Skip
    :: Mode

  -- | Check private items only.
  Local
    :: Mode

  -- | Check all items.
  Global
    :: Mode

  -- | Check imports & reject all other declarations.
  GlobalMain
    :: Mode

  deriving (Mode -> Mode -> Bool
(Mode -> Mode -> Bool) -> (Mode -> Mode -> Bool) -> Eq Mode
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
(Int -> Mode -> ShowS)
-> (Mode -> String) -> ([Mode] -> ShowS) -> Show Mode
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)

-- | An environment type for use in a reader monad.
data Environment
  = Environment
  { Environment -> Mode
environmentMode
    :: !Mode
    -- ^ The current check mode.
  , Environment -> String
environmentRoot
    :: !FilePath
    -- ^ The project root path.
  , Environment -> [AbsolutePath]
environmentIncludes
    :: ![AbsolutePath]
    -- ^ The include paths.
  } deriving Int -> Environment -> ShowS
[Environment] -> ShowS
Environment -> String
(Int -> Environment -> ShowS)
-> (Environment -> String)
-> ([Environment] -> ShowS)
-> Show Environment
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

-- ## Ask

askMode
  :: MonadReader Environment m
  => m Mode
askMode :: m Mode
askMode
  = Environment -> Mode
environmentMode (Environment -> Mode) -> m Environment -> m Mode
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Environment
forall r (m :: * -> *). MonadReader r m => m r
ask

-- | Ask whether to skip checking names.
askSkip
  :: MonadReader Environment m
  => m Bool
askSkip :: m Bool
askSkip
  = (Mode -> Mode -> Bool
forall a. Eq a => a -> a -> Bool
== Mode
Skip) (Mode -> Bool) -> m Mode -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Mode
forall (m :: * -> *). MonadReader Environment m => m Mode
askMode

-- | Ask whether we are in local mode.
askLocal
  :: MonadReader Environment m
  => m Bool
askLocal :: m Bool
askLocal
  = (Mode -> Mode -> Bool
forall a. Eq a => a -> a -> Bool
== Mode
Local) (Mode -> Bool) -> m Mode -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Mode
forall (m :: * -> *). MonadReader Environment m => m Mode
askMode

-- | Ask whether we are in global main mode.
askGlobalMain
  :: MonadReader Environment m
  => m Bool
askGlobalMain :: m Bool
askGlobalMain
  = (Mode -> Mode -> Bool
forall a. Eq a => a -> a -> Bool
== Mode
GlobalMain) (Mode -> Bool) -> m Mode -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Mode
forall (m :: * -> *). MonadReader Environment m => m Mode
askMode

-- | Ask for the project root path.
askRoot
  :: MonadReader Environment m
  => m FilePath
askRoot :: m String
askRoot
  = Environment -> String
environmentRoot (Environment -> String) -> m Environment -> m String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Environment
forall r (m :: * -> *). MonadReader r m => m r
ask

-- | Ask for the include paths.
askIncludes
  :: MonadReader Environment m
  => m [AbsolutePath]
askIncludes :: m [AbsolutePath]
askIncludes
  = Environment -> [AbsolutePath]
environmentIncludes (Environment -> [AbsolutePath])
-> m Environment -> m [AbsolutePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Environment
forall r (m :: * -> *). MonadReader r m => m r
ask

-- ## Local

localMode
  :: MonadReader Environment m
  => Mode
  -> m a
  -> m a
localMode :: Mode -> m a -> m a
localMode Mode
m
  = (Environment -> Environment) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Environment
e -> Environment
e {environmentMode :: Mode
environmentMode = Mode
m})

-- | Perform a local computation, but skip checking names.
localSkip
  :: MonadReader Environment m
  => m a
  -> m a
localSkip :: m a -> m a
localSkip
  = Mode -> m a -> m a
forall (m :: * -> *) a.
MonadReader Environment m =>
Mode -> m a -> m a
localMode Mode
Skip

-- | Perform a local computation in global mode.
localGlobal
  :: MonadReader Environment m
  => m a
  -> m a
localGlobal :: m a -> m a
localGlobal
  = Mode -> m a -> m a
forall (m :: * -> *) a.
MonadReader Environment m =>
Mode -> m a -> m a
localMode Mode
Global