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

A state monad for determining unused code.
-}
module Agda.Unused.Monad.State

  ( -- * Definitions

    ModuleState(..)
  , State

    -- * Interface

  , stateEmpty
  , stateItems
  , stateModules

    -- * Get

  , getModule
  , getSources

    -- * Modify

  , modifyInsert
  , modifyDelete
  , modifyBlock
  , modifyCheck
  , modifySources

  ) where

import Agda.Unused.Monad.Reader
  (Environment, askSkip)
import Agda.Unused.Types.Context
  (Context)
import Agda.Unused.Types.Name
  (QName)
import Agda.Unused.Types.Range
  (RangeInfo, rangeContains)

import Agda.Syntax.Position
  (Range, Range'(..))
import Agda.TypeChecking.Monad.Base
  (ModuleToSource)
import Control.Monad
  (unless)
import Control.Monad.Reader
  (MonadReader)
import Control.Monad.State
  (MonadState, gets, modify)
import Data.Map.Strict
  (Map)
import qualified Data.Map.Strict
  as Map
import Data.Set
  (Set)

-- ## Definitions

-- | Cache the results of checking modules. This allows us to:
-- 
-- - Avoid duplicate computations.
-- - Handle cyclic module dependencies without nontermination.
data ModuleState where

  Blocked
    :: ModuleState

  Checked
    :: !Context
    -> ModuleState

  deriving Int -> ModuleState -> ShowS
[ModuleState] -> ShowS
ModuleState -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ModuleState] -> ShowS
$cshowList :: [ModuleState] -> ShowS
show :: ModuleState -> String
$cshow :: ModuleState -> String
showsPrec :: Int -> ModuleState -> ShowS
$cshowsPrec :: Int -> ModuleState -> ShowS
Show

-- | The current computation state.
data State
  = State
  { State -> Map Range RangeInfo
stateItems'
    :: !(Map Range RangeInfo)
    -- ^ Ranges for each unused item.
  , State -> Map QName ModuleState
stateModules'
    :: !(Map QName ModuleState)
    -- ^ States for each module dependency.
  , State -> ModuleToSource
stateSources'
    :: !ModuleToSource
    -- ^ A cache of source paths corresponding to certain module names.
  } deriving Int -> State -> ShowS
[State] -> ShowS
State -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [State] -> ShowS
$cshowList :: [State] -> ShowS
show :: State -> String
$cshow :: State -> String
showsPrec :: Int -> State -> ShowS
$cshowsPrec :: Int -> State -> ShowS
Show

-- ## Interface

-- | Construct an empty state.
stateEmpty
  :: State
stateEmpty :: State
stateEmpty
  = Map Range RangeInfo
-> Map QName ModuleState -> ModuleToSource -> State
State forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty

-- | Get a sorted list of state items.
--
-- If one state item contains another (e.g., an @open@ statement containing
-- @using@ directives), then keep only the containing item.
stateItems
  :: State
  -> [(Range, RangeInfo)]
stateItems :: State -> [(Range, RangeInfo)]
stateItems
  = [(Range, RangeInfo)] -> [(Range, RangeInfo)]
stateItemsFilter
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
Map.toAscList
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. State -> Map Range RangeInfo
stateItems'

-- Remove nested items.
stateItemsFilter
  :: [(Range, RangeInfo)]
  -> [(Range, RangeInfo)]
stateItemsFilter :: [(Range, RangeInfo)] -> [(Range, RangeInfo)]
stateItemsFilter []
  = []
stateItemsFilter ((Range, RangeInfo)
i : (Range, RangeInfo)
i' : [(Range, RangeInfo)]
is) | Range -> Range -> Bool
rangeContains (forall a b. (a, b) -> a
fst (Range, RangeInfo)
i) (forall a b. (a, b) -> a
fst (Range, RangeInfo)
i')
  = [(Range, RangeInfo)] -> [(Range, RangeInfo)]
stateItemsFilter ((Range, RangeInfo)
i forall a. a -> [a] -> [a]
: [(Range, RangeInfo)]
is)
stateItemsFilter ((Range, RangeInfo)
i : (Range, RangeInfo)
i' : [(Range, RangeInfo)]
is) | Range -> Range -> Bool
rangeContains (forall a b. (a, b) -> a
fst (Range, RangeInfo)
i') (forall a b. (a, b) -> a
fst (Range, RangeInfo)
i)
  = [(Range, RangeInfo)] -> [(Range, RangeInfo)]
stateItemsFilter ((Range, RangeInfo)
i' forall a. a -> [a] -> [a]
: [(Range, RangeInfo)]
is)
stateItemsFilter ((Range, RangeInfo)
i : [(Range, RangeInfo)]
is)
  = (Range, RangeInfo)
i forall a. a -> [a] -> [a]
: [(Range, RangeInfo)] -> [(Range, RangeInfo)]
stateItemsFilter [(Range, RangeInfo)]
is

-- | Get a list of visited modules.
stateModules
  :: State
  -> Set QName
stateModules :: State -> Set QName
stateModules
  = forall k a. Map k a -> Set k
Map.keysSet
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. State -> Map QName ModuleState
stateModules'

stateSources
  :: ModuleToSource
  -> State
  -> State
stateSources :: ModuleToSource -> State -> State
stateSources ModuleToSource
ss (State Map Range RangeInfo
rs Map QName ModuleState
ms ModuleToSource
_)
  = Map Range RangeInfo
-> Map QName ModuleState -> ModuleToSource -> State
State Map Range RangeInfo
rs Map QName ModuleState
ms ModuleToSource
ss

stateInsert
  :: Range
  -> RangeInfo
  -> State
  -> State
stateInsert :: Range -> RangeInfo -> State -> State
stateInsert Range
NoRange RangeInfo
_ State
s
  = State
s
stateInsert r :: Range
r@(Range Maybe AbsolutePath
_ Seq IntervalWithoutFile
_) RangeInfo
i (State Map Range RangeInfo
rs Map QName ModuleState
ms ModuleToSource
ss)
  = Map Range RangeInfo
-> Map QName ModuleState -> ModuleToSource -> State
State (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Range
r RangeInfo
i Map Range RangeInfo
rs) Map QName ModuleState
ms ModuleToSource
ss

stateDelete
  :: Set Range
  -> State
  -> State
stateDelete :: Set Range -> State -> State
stateDelete Set Range
rs (State Map Range RangeInfo
rs' Map QName ModuleState
ms ModuleToSource
ss)
  = Map Range RangeInfo
-> Map QName ModuleState -> ModuleToSource -> State
State (forall k a. Ord k => Map k a -> Set k -> Map k a
Map.withoutKeys Map Range RangeInfo
rs' Set Range
rs) Map QName ModuleState
ms ModuleToSource
ss

stateModule
  :: QName
  -> State
  -> Maybe ModuleState
stateModule :: QName -> State -> Maybe ModuleState
stateModule QName
n (State Map Range RangeInfo
_ Map QName ModuleState
ms ModuleToSource
_)
  = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
n Map QName ModuleState
ms

stateBlock
  :: QName
  -> State
  -> State
stateBlock :: QName -> State -> State
stateBlock QName
n (State Map Range RangeInfo
rs Map QName ModuleState
ms ModuleToSource
ss)
  = Map Range RangeInfo
-> Map QName ModuleState -> ModuleToSource -> State
State Map Range RangeInfo
rs (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert QName
n ModuleState
Blocked Map QName ModuleState
ms) ModuleToSource
ss

stateCheck
  :: QName
  -> Context
  -> State
  -> State
stateCheck :: QName -> Context -> State -> State
stateCheck QName
n Context
c (State Map Range RangeInfo
rs Map QName ModuleState
ms ModuleToSource
ss)
  = Map Range RangeInfo
-> Map QName ModuleState -> ModuleToSource -> State
State Map Range RangeInfo
rs (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert QName
n (Context -> ModuleState
Checked Context
c) Map QName ModuleState
ms) ModuleToSource
ss

-- ## Get

-- | Get the state of a module.
getModule
  :: MonadState State m
  => QName
  -> m (Maybe ModuleState)
getModule :: forall (m :: * -> *).
MonadState State m =>
QName -> m (Maybe ModuleState)
getModule QName
n
  = forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (QName -> State -> Maybe ModuleState
stateModule QName
n)

-- | Get the cache of source paths.
getSources
  :: MonadState State m
  => m ModuleToSource
getSources :: forall (m :: * -> *). MonadState State m => m ModuleToSource
getSources
  = forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> ModuleToSource
stateSources'

-- ## Modify

-- | Record a new unused item.
modifyInsert
  :: MonadReader Environment m
  => MonadState State m
  => Range
  -> RangeInfo
  -> m ()
modifyInsert :: forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Range -> RangeInfo -> m ()
modifyInsert Range
r RangeInfo
i
  = forall (m :: * -> *). MonadReader Environment m => m Bool
askSkip forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Range -> RangeInfo -> State -> State
stateInsert Range
r RangeInfo
i))

-- | Mark a list of items as used.
modifyDelete
  :: MonadReader Environment m
  => MonadState State m
  => Set Range
  -> m ()
modifyDelete :: forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Set Range -> m ()
modifyDelete Set Range
rs
  = forall (m :: * -> *). MonadReader Environment m => m Bool
askSkip forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Set Range -> State -> State
stateDelete Set Range
rs))

-- | Mark that we are beginning to check a module.
modifyBlock
  :: MonadState State m
  => QName
  -> m ()
modifyBlock :: forall (m :: * -> *). MonadState State m => QName -> m ()
modifyBlock QName
n
  = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (QName -> State -> State
stateBlock QName
n)

-- | Record the results of checking a module.
modifyCheck
  :: MonadState State m
  => QName
  -> Context
  -> m ()
modifyCheck :: forall (m :: * -> *).
MonadState State m =>
QName -> Context -> m ()
modifyCheck QName
n Context
c
  = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (QName -> Context -> State -> State
stateCheck QName
n Context
c)

-- | Update the cache of sources.
modifySources
  :: MonadState State m
  => ModuleToSource
  -> m ()
modifySources :: forall (m :: * -> *). MonadState State m => ModuleToSource -> m ()
modifySources ModuleToSource
ss
  = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (ModuleToSource -> State -> State
stateSources ModuleToSource
ss)