module Agda.Unused.Monad.State
(
ModuleState(..)
, State
, stateEmpty
, stateItems
, stateModules
, getModule
, getSources
, 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)
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
data State
= State
{ State -> Map Range RangeInfo
stateItems'
:: !(Map Range RangeInfo)
, State -> Map QName ModuleState
stateModules'
:: !(Map QName ModuleState)
, State -> ModuleToSource
stateSources'
:: !ModuleToSource
} 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
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
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'
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
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
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)
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'
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))
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))
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)
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)
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)