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 -> [QName]

Get a list of visited modules.

stateBlock :: QName -> State -> State

Mark that we are beginning to check a module.

stateCheck :: QName -> Context -> State -> State

Record the results of checking a module.

stateLookup :: QName -> State -> Maybe ModuleState

Lookup the state of a module.

Modify

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

Mark a list of items as used.

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

Record a new unused item.