Agda.Utils.Update

Documentation

data ChangeT m a

The ChangeT monad transformer.

Instances

MonadTransControl ChangeT

Defined in Agda.Utils.Update

Associated Types

type StT ChangeT a

Methods

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

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

MonadTrans ChangeT

Defined in Agda.Utils.Update

Methods

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

HasOptions m => HasOptions (ChangeT m)

Defined in Agda.Interaction.Options.HasOptions

Methods

pragmaOptions :: ChangeT m PragmaOptions

commandLineOptions :: ChangeT m CommandLineOptions

MonadReduce m => MonadReduce (ChangeT m)

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> ChangeT m a

MonadTCEnv m => MonadTCEnv (ChangeT m)

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: ChangeT m TCEnv

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

MonadTCM tcm => MonadTCM (ChangeT tcm)

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> ChangeT tcm a

MonadTCState m => MonadTCState (ChangeT m)

Defined in Agda.TypeChecking.Monad.Base

Methods

getTC :: ChangeT m TCState

putTC :: TCState -> ChangeT m ()

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

ReadTCState m => ReadTCState (ChangeT m)

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: ChangeT m TCState

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

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

HasBuiltins m => HasBuiltins (ChangeT m)

Defined in Agda.TypeChecking.Monad.Builtin

Methods

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

MonadAddContext m => MonadAddContext (ChangeT m)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

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

MonadDebug m => MonadDebug (ChangeT m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> ChangeT m String

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> ChangeT m a -> ChangeT m a

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

getVerbosity :: ChangeT m Verbosity

getProfileOptions :: ChangeT m ProfileOptions

isDebugPrinting :: ChangeT m Bool

nowDebugPrinting :: ChangeT m a -> ChangeT m a

PureTCM m => PureTCM (ChangeT m)

Defined in Agda.TypeChecking.Monad.Pure

HasConstInfo m => HasConstInfo (ChangeT m)

Defined in Agda.TypeChecking.Monad.Signature

Methods

getConstInfo :: QName -> ChangeT m Definition

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

getRewriteRulesFor :: QName -> ChangeT m RewriteRules

Monad m => MonadChange (ChangeT m)

Defined in Agda.Utils.Update

Methods

tellDirty :: ChangeT m ()

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

MonadFail m => MonadFail (ChangeT m)

Defined in Agda.Utils.Update

Methods

fail :: String -> ChangeT m a

MonadIO m => MonadIO (ChangeT m)

Defined in Agda.Utils.Update

Methods

liftIO :: IO a -> ChangeT m a

Applicative m => Applicative (ChangeT m)

Defined in Agda.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)

Defined in Agda.Utils.Update

Methods

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

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

Monad m => Monad (ChangeT m)

Defined in Agda.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

type StT ChangeT a

Defined in Agda.Utils.Update

type StT ChangeT a = (a, Any)

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

Run a ChangeT computation, returning result plus change flag.

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

Map a ChangeT computation (monad transformer action).

type UpdaterT m a = a -> ChangeT m a

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

Blindly run an updater.

type Change a = ChangeT Identity a

class Monad m => MonadChange m where

The class of change monads.

Methods

tellDirty

Arguments

:: m ()

Mark computation as having changed something.

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

Instances

MonadChange Identity

A mock change monad. Always assume change has happened.

Defined in Agda.Utils.Update

Methods

tellDirty :: Identity ()

listenDirty :: Identity a -> Identity (a, Bool)

Monad m => MonadChange (ChangeT m)

Defined in Agda.Utils.Update

Methods

tellDirty :: ChangeT m ()

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

Monad m => MonadChange (IdentityT m)

Defined in Agda.Utils.Update

Methods

tellDirty :: IdentityT m ()

listenDirty :: IdentityT m a -> IdentityT m (a, Bool)

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

Run a Change computation, returning result plus change flag.

type Updater a = UpdaterT Identity a

sharing :: Monad m => UpdaterT m a -> UpdaterT m a

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

runUpdater :: Updater a -> a -> (a, Bool)

Blindly run an updater.

dirty :: Monad m => UpdaterT m a

Mark a computation as dirty.

ifDirty :: (Monad m, MonadChange m) => m a -> (a -> m b) -> (a -> m b) -> m b

class Traversable f => Updater1 f where

Like Functor, but preserving sharing.

Minimal complete definition

Nothing

Methods

updater1 :: Updater a -> Updater (f a)

updates1

Arguments

:: Updater a

-> Updater (f a)

= sharing . updater1

update1 :: Updater a -> EndoFun (f a)

Instances

Updater1 Maybe

Defined in Agda.Utils.Update

Methods

updater1 :: Updater a -> Updater (Maybe a)

updates1 :: Updater a -> Updater (Maybe a)

update1 :: Updater a -> EndoFun (Maybe a)

Updater1 List

Defined in Agda.Utils.Update

Methods

updater1 :: Updater a -> Updater [a]

updates1 :: Updater a -> Updater [a]

update1 :: Updater a -> EndoFun [a]

class Updater2 f where

Like Bifunctor, but preserving sharing.

Minimal complete definition

updater2

Methods

updater2 :: Updater a -> Updater b -> Updater (f a b)

updates2 :: Updater a -> Updater b -> Updater (f a b)

update2 :: Updater a -> Updater b -> EndoFun (f a b)

Instances

Updater2 Either

Defined in Agda.Utils.Update

Methods

updater2 :: Updater a -> Updater b -> Updater (Either a b)

updates2 :: Updater a -> Updater b -> Updater (Either a b)

update2 :: Updater a -> Updater b -> EndoFun (Either a b)

Updater2 (,)

Defined in Agda.Utils.Update

Methods

updater2 :: Updater a -> Updater b -> Updater (a, b)

updates2 :: Updater a -> Updater b -> Updater (a, b)

update2 :: Updater a -> Updater b -> EndoFun (a, b)