{- |
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
  (Range, Range'(..), RangeInfo, rangeContains)

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
(Int -> ModuleState -> ShowS)
-> (ModuleState -> String)
-> ([ModuleState] -> ShowS)
-> Show ModuleState
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
(Int -> State -> ShowS)
-> (State -> String) -> ([State] -> ShowS) -> Show State
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 Map Range RangeInfo
forall a. Monoid a => a
mempty Map QName ModuleState
forall a. Monoid a => a
mempty ModuleToSource
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
  ([(Range, RangeInfo)] -> [(Range, RangeInfo)])
-> (State -> [(Range, RangeInfo)]) -> State -> [(Range, RangeInfo)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Range RangeInfo -> [(Range, RangeInfo)]
forall k a. Map k a -> [(k, a)]
Map.toAscList
  (Map Range RangeInfo -> [(Range, RangeInfo)])
-> (State -> Map Range RangeInfo) -> State -> [(Range, RangeInfo)]
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 ((Range, RangeInfo) -> Range
forall a b. (a, b) -> a
fst (Range, RangeInfo)
i) ((Range, RangeInfo) -> Range
forall a b. (a, b) -> a
fst (Range, RangeInfo)
i')
  = [(Range, RangeInfo)] -> [(Range, RangeInfo)]
stateItemsFilter ((Range, RangeInfo)
i (Range, RangeInfo) -> [(Range, RangeInfo)] -> [(Range, RangeInfo)]
forall a. a -> [a] -> [a]
: [(Range, RangeInfo)]
is)
stateItemsFilter ((Range, RangeInfo)
i : (Range, RangeInfo)
i' : [(Range, RangeInfo)]
is) | Range -> Range -> Bool
rangeContains ((Range, RangeInfo) -> Range
forall a b. (a, b) -> a
fst (Range, RangeInfo)
i') ((Range, RangeInfo) -> Range
forall a b. (a, b) -> a
fst (Range, RangeInfo)
i)
  = [(Range, RangeInfo)] -> [(Range, RangeInfo)]
stateItemsFilter ((Range, RangeInfo)
i' (Range, RangeInfo) -> [(Range, RangeInfo)] -> [(Range, RangeInfo)]
forall a. a -> [a] -> [a]
: [(Range, RangeInfo)]
is)
stateItemsFilter ((Range, RangeInfo)
i : [(Range, RangeInfo)]
is)
  = (Range, RangeInfo)
i (Range, RangeInfo) -> [(Range, RangeInfo)] -> [(Range, RangeInfo)]
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
  = Map QName ModuleState -> Set QName
forall k a. Map k a -> Set k
Map.keysSet
  (Map QName ModuleState -> Set QName)
-> (State -> Map QName ModuleState) -> State -> Set QName
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 SrcFile
_ Seq IntervalWithoutFile
_) RangeInfo
i (State Map Range RangeInfo
rs Map QName ModuleState
ms ModuleToSource
ss)
  = Map Range RangeInfo
-> Map QName ModuleState -> ModuleToSource -> State
State (Range -> RangeInfo -> Map Range RangeInfo -> Map Range RangeInfo
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 (Map Range RangeInfo -> Set Range -> Map Range RangeInfo
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
_)
  = QName -> Map QName ModuleState -> Maybe ModuleState
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 (QName
-> ModuleState -> Map QName ModuleState -> Map QName ModuleState
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 (QName
-> ModuleState -> Map QName ModuleState -> Map QName ModuleState
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 :: QName -> m (Maybe ModuleState)
getModule QName
n
  = (State -> Maybe ModuleState) -> m (Maybe ModuleState)
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 :: m ModuleToSource
getSources
  = (State -> ModuleToSource) -> m ModuleToSource
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 :: Range -> RangeInfo -> m ()
modifyInsert Range
r RangeInfo
i
  = m Bool
forall (m :: * -> *). MonadReader Environment m => m Bool
askSkip m Bool -> (Bool -> m ()) -> m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Bool -> m () -> m ()) -> m () -> Bool -> m ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((State -> State) -> m ()
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 :: Set Range -> m ()
modifyDelete Set Range
rs
  = m Bool
forall (m :: * -> *). MonadReader Environment m => m Bool
askSkip m Bool -> (Bool -> m ()) -> m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Bool -> m () -> m ()) -> m () -> Bool -> m ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((State -> State) -> m ()
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 :: QName -> m ()
modifyBlock QName
n
  = (State -> State) -> m ()
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 :: QName -> Context -> m ()
modifyCheck QName
n Context
c
  = (State -> State) -> m ()
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 :: ModuleToSource -> m ()
modifySources ModuleToSource
ss
  = (State -> State) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (ModuleToSource -> State -> State
stateSources ModuleToSource
ss)