Mikan

Safe Haskell	None
Language	Haskell2010

Mikan.Utils.Update

Contents

The ChangeT monad transformer
- Updaters

Description

Computations that track a dirty bit.

Synopsis

class Monad m => MonadChange (m :: Type -> Type) where
- tellDirty :: m ()
- listenDirty :: m a -> m (a, Bool)
data ChangeT (m :: Type -> Type) a
type Change a = ChangeT Identity a
runChangeT :: Functor m => ChangeT m a -> m (a, Bool)
runChange :: Change a -> (a, Bool)
mapChangeT :: (m (a, Any) -> n (b, Any)) -> ChangeT m a -> ChangeT n b
type UpdaterT (m :: Type -> Type) a = a -> ChangeT m a
type Updater a = UpdaterT Identity a
runUpdaterT :: Functor m => UpdaterT m a -> a -> m (a, Bool)
evalUpdater :: Updater a -> a -> a
dirty :: forall (m :: Type -> Type) a. Monad m => UpdaterT m a
sharing :: forall (m :: Type -> Type) a. Monad m => UpdaterT m a -> UpdaterT m a

Documentation

class Monad m => MonadChange (m :: Type -> Type) where Source #

The class of change monads.

Methods

tellDirty :: m () Source #

Mark a computation as having changed something.

listenDirty :: m a -> m (a, Bool) Source #

Check to see if a computation changed anything.

Instances

Instances details

MonadChange Identity Source #	Always assume change has happened.
Instance details Defined in Mikan.Utils.Update Methods tellDirty :: Identity () Source # listenDirty :: Identity a -> Identity (a, Bool) Source #
Monad m => MonadChange (ChangeT m) Source #
Instance details Defined in Mikan.Utils.Update Methods tellDirty :: ChangeT m () Source # listenDirty :: ChangeT m a -> ChangeT m (a, Bool) Source #
Monad m => MonadChange (IdentityT m) Source #	Always assume change has happened.
Instance details Defined in Mikan.Utils.Update Methods tellDirty :: IdentityT m () Source # listenDirty :: IdentityT m a -> IdentityT m (a, Bool) Source #

The ChangeT monad transformer

data ChangeT (m :: Type -> Type) a Source #

The ChangeT monad transformer, which tracks a single dirty bit.

Instances

Instances details

MonadTransControl ChangeT Source #

Instance details

Defined in Mikan.Utils.Update

Associated Types

type StT ChangeT a
Instance details Defined in Mikan.Utils.Update type StT ChangeT a = (a, Any)

Methods

liftWith :: Monad m => (Run ChangeT -> m a) -> ChangeT m a #

restoreT :: Monad m => m (StT ChangeT a) -> ChangeT m a #

MonadTrans ChangeT Source #

Instance details

Defined in Mikan.Utils.Update

Methods

lift :: Monad m => m a -> ChangeT m a #

HasOptions m => HasOptions (ChangeT m) Source #

Instance details

Defined in Mikan.Interaction.Options.HasOptions

Methods

pragmaOptions :: ChangeT m PragmaOptions Source #

commandLineOptions :: ChangeT m CommandLineOptions Source #

MonadReduce m => MonadReduce (ChangeT m) Source #

Instance details

Defined in Mikan.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> ChangeT m a Source #

MonadTCEnv m => MonadTCEnv (ChangeT m) Source #

Instance details

Defined in Mikan.TypeChecking.Monad.Base

Methods

askTC :: ChangeT m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> ChangeT m a -> ChangeT m a Source #

MonadTCM tcm => MonadTCM (ChangeT tcm) Source #

Instance details

Defined in Mikan.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> ChangeT tcm a Source #

MonadTCState m => MonadTCState (ChangeT m) Source #

Instance details

Defined in Mikan.TypeChecking.Monad.Base

Methods

getTC :: ChangeT m TCState Source #

putTC :: TCState -> ChangeT m () Source #

modifyTC :: (TCState -> TCState) -> ChangeT m () Source #

ReadTCState m => ReadTCState (ChangeT m) Source #

Instance details

Defined in Mikan.TypeChecking.Monad.Base

Methods

getTCState :: ChangeT m TCState Source #

locallyTCState :: Lens' TCState a -> (a -> a) -> ChangeT m b -> ChangeT m b Source #

getSessionState :: ChangeT m SessionState Source #

withTCState :: (TCState -> TCState) -> ChangeT m a -> ChangeT m a Source #

HasBuiltins m => HasBuiltins (ChangeT m) Source #

Instance details

Defined in Mikan.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: SomeBuiltin -> ChangeT m (Maybe (Builtin PrimFun)) Source #

MonadAddContext m => MonadAddContext (ChangeT m) Source #

Instance details

Defined in Mikan.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> ChangeT m a -> ChangeT m a Source #

addLetBinding' :: IsAxiom -> Origin -> Name -> Term -> Dom Type -> ChangeT m a -> ChangeT m a Source #

updateContext :: Substitution -> (Context -> Context) -> ChangeT m a -> ChangeT m a Source #

withFreshName :: Range -> ArgName -> (Name -> ChangeT m a) -> ChangeT m a Source #

MonadDebug m => MonadDebug (ChangeT m) Source #

Instance details

Defined in Mikan.TypeChecking.Monad.Debug

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> ChangeT m Doc Source #

traceDebugMessage :: VerboseKey -> VerboseLevel -> Doc -> ChangeT m a -> ChangeT m a Source #

verboseBracket :: VerboseKey -> VerboseLevel -> String -> ChangeT m a -> ChangeT m a Source #

getVerbosity :: ChangeT m Verbosity Source #

getProfileOptions :: ChangeT m ProfileOptions Source #

isDebugPrinting :: ChangeT m Bool Source #

nowDebugPrinting :: ChangeT m a -> ChangeT m a Source #

PureTCM m => PureTCM (ChangeT m) Source #

Instance details

Defined in Mikan.TypeChecking.Monad.Pure

HasConstInfo m => HasConstInfo (ChangeT m) Source #

Instance details

Defined in Mikan.TypeChecking.Monad.Signature

Methods

getConstInfo :: QName -> ChangeT m Definition Source #

getConstInfo' :: QName -> ChangeT m (Either SigError Definition) Source #

MonadFileId m => MonadFileId (ChangeT m) Source #

Instance details

Defined in Mikan.Utils.FileId

Methods

fileFromId :: FileId -> ChangeT m File Source #

idFromFile :: File -> ChangeT m FileId Source #

Monad m => MonadChange (ChangeT m) Source #

Instance details

Defined in Mikan.Utils.Update

Methods

tellDirty :: ChangeT m () Source #

listenDirty :: ChangeT m a -> ChangeT m (a, Bool) Source #

Applicative m => Applicative (ChangeT m) Source #

Instance details

Defined in Mikan.Utils.Update

Methods

pure :: a -> ChangeT m a #

(<*>) :: ChangeT m (a -> b) -> ChangeT m a -> ChangeT m b #

liftA2 :: (a -> b -> c) -> ChangeT m a -> ChangeT m b -> ChangeT m c #

(*>) :: ChangeT m a -> ChangeT m b -> ChangeT m b #

(<*) :: ChangeT m a -> ChangeT m b -> ChangeT m a #

Functor m => Functor (ChangeT m) Source #

Instance details

Defined in Mikan.Utils.Update

Methods

fmap :: (a -> b) -> ChangeT m a -> ChangeT m b #

(<$) :: a -> ChangeT m b -> ChangeT m a #

Monad m => Monad (ChangeT m) Source #

Instance details

Defined in Mikan.Utils.Update

Methods

(>>=) :: ChangeT m a -> (a -> ChangeT m b) -> ChangeT m b #

(>>) :: ChangeT m a -> ChangeT m b -> ChangeT m b #

return :: a -> ChangeT m a #

MonadFail m => MonadFail (ChangeT m) Source #

Instance details

Defined in Mikan.Utils.Update

Methods

fail :: String -> ChangeT m a #

MonadIO m => MonadIO (ChangeT m) Source #

Instance details

Defined in Mikan.Utils.Update

Methods

liftIO :: IO a -> ChangeT m a #

type StT ChangeT a Source #

Instance details

Defined in Mikan.Utils.Update

type StT ChangeT a = (a, Any)

type Change a = ChangeT Identity a Source #

runChangeT :: Functor m => ChangeT m a -> m (a, Bool) Source #

Run a ChangeT computation, returning result plus change flag.

runChange :: Change a -> (a, Bool) Source #

Run a Change computation, returning result plus change flag.

mapChangeT :: (m (a, Any) -> n (b, Any)) -> ChangeT m a -> ChangeT n b Source #

Map a ChangeT computation (monad transformer action).

Updaters

type UpdaterT (m :: Type -> Type) a = a -> ChangeT m a Source #

type Updater a = UpdaterT Identity a Source #

runUpdaterT :: Functor m => UpdaterT m a -> a -> m (a, Bool) Source #

Blindly run an updater.

evalUpdater :: Updater a -> a -> a Source #

Evaluate an updater using sharing.

dirty :: forall (m :: Type -> Type) a. Monad m => UpdaterT m a Source #

Mark a computation as dirty.

sharing :: forall (m :: Type -> Type) a. Monad m => UpdaterT m a -> UpdaterT m a Source #

Replace result of updating with original input if nothing has changed.