Agda.Unused.Monad.State

A state monad for determining unused code.

Definitions

data ModuleState where

Cache the results of checking modules. This allows us to:

• Avoid duplicate computations.
• Handle cyclic module dependencies without nontermination.

Constructors

Blocked :: ModuleState

Checked :: !Context -> ModuleState

Instances

Show ModuleState

Defined in Agda.Unused.Monad.State

Methods

showsPrec :: Int -> ModuleState -> ShowS

show :: ModuleState -> String

showList :: [ModuleState] -> ShowS

data State

The current computation state.

Instances

Show State

Defined in Agda.Unused.Monad.State

Methods

showsPrec :: Int -> State -> ShowS

show :: State -> String

showList :: [State] -> ShowS

Interface

stateEmpty :: State

Construct an empty state.

stateItems :: State -> [(Range, RangeInfo)]

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.

stateModules :: State -> Set QName

Get a list of visited modules.

Get

getModule :: MonadState State m => QName -> m (Maybe ModuleState)

Get the state of a module.

getSources :: MonadState State m => m ModuleToSource

Get the cache of source paths.

Modify

modifyInsert :: MonadReader Environment m => MonadState State m => Range -> RangeInfo -> m ()

Record a new unused item.

modifyDelete :: MonadReader Environment m => MonadState State m => Set Range -> m ()

Mark a list of items as used.

modifyBlock :: MonadState State m => QName -> m ()

Mark that we are beginning to check a module.

modifyCheck :: MonadState State m => QName -> Context -> m ()

Record the results of checking a module.

modifySources :: MonadState State m => ModuleToSource -> m ()

Update the cache of sources.