Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Utils.Update

Synopsis

- data ChangeT (m :: Type -> Type) a
- runChangeT :: Functor m => ChangeT m a -> m (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
- runUpdaterT :: Functor m => UpdaterT m a -> a -> m (a, Bool)
- type Change a = ChangeT Identity a
- class Monad m => MonadChange (m :: Type -> Type) where
  - tellDirty :: m ()
  - listenDirty :: m a -> m (a, Bool)
- runChange :: Change a -> (a, Bool)
- type Updater a = UpdaterT Identity a
- sharing :: forall (m :: Type -> Type) a. Monad m => UpdaterT m a -> UpdaterT m a
- runUpdater :: Updater a -> a -> (a, Bool)
- dirty :: forall (m :: Type -> Type) a. Monad m => UpdaterT m a
- ifDirty :: (Monad m, MonadChange m) => m a -> (a -> m b) -> (a -> m b) -> m b
- class Traversable f => Updater1 (f :: Type -> Type) where
  - updater1 :: Updater a -> Updater (f a)
  - updates1 :: Updater a -> Updater (f a)
  - update1 :: Updater a -> EndoFun (f a)
- class Updater2 (f :: Type -> Type -> Type) where
  - 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)

# Documentation

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

The `ChangeT` monad transformer.

#### Instances

Instances details

MonadTransControl ChangeT Source # |

Instance details

Defined in Agda.Utils.Update

Associated Types

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

Methods

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

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

MonadTrans ChangeT Source # |
Instance details Defined in Agda.Utils.Update Methods lift :: Monad m => m a -> ChangeT m a Source #
HasOptions m => HasOptions (ChangeT m) Source # |
Instance details Defined in Agda.Interaction.Options.HasOptions Methods pragmaOptions :: ChangeT m PragmaOptions Source # commandLineOptions :: ChangeT m CommandLineOptions Source #
MonadReduce m => MonadReduce (ChangeT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftReduce :: ReduceM a -> ChangeT m a Source #
MonadTCEnv m => MonadTCEnv (ChangeT m) Source # |
Instance details Defined in Agda.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 Agda.TypeChecking.Monad.Base Methods liftTCM :: TCM a -> ChangeT tcm a Source #
MonadTCState m => MonadTCState (ChangeT m) Source # |
Instance details Defined in Agda.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 Agda.TypeChecking.Monad.Base Methods getTCState :: ChangeT m TCState Source # locallyTCState :: Lens' TCState a -> (a -> a) -> ChangeT m b -> ChangeT m b Source # withTCState :: (TCState -> TCState) -> ChangeT m a -> ChangeT m a Source #
HasBuiltins m => HasBuiltins (ChangeT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Builtin Methods getBuiltinThing :: SomeBuiltin -> ChangeT m (Maybe (Builtin PrimFun)) Source #
MonadAddContext m => MonadAddContext (ChangeT m) Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

addLetBinding' :: 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 Agda.TypeChecking.Monad.Debug

Methods

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

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> 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 Agda.TypeChecking.Monad.Pure
HasConstInfo m => HasConstInfo (ChangeT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Signature Methods getConstInfo :: QName -> ChangeT m Definition Source # getConstInfo' :: QName -> ChangeT m (Either SigError Definition) Source # getRewriteRulesFor :: QName -> ChangeT m RewriteRules Source #
Monad m => MonadChange (ChangeT m) Source # |
Instance details Defined in Agda.Utils.Update Methods tellDirty :: ChangeT m () Source # listenDirty :: ChangeT m a -> ChangeT m (a, Bool) Source #
MonadIO m => MonadIO (ChangeT m) Source # |
Instance details Defined in Agda.Utils.Update Methods liftIO :: IO a -> ChangeT m a Source #
Applicative m => Applicative (ChangeT m) Source # |
Instance details Defined in Agda.Utils.Update Methods pure :: a -> ChangeT m a Source # (<*>) :: ChangeT m (a -> b) -> ChangeT m a -> ChangeT m b Source # liftA2 :: (a -> b -> c) -> ChangeT m a -> ChangeT m b -> ChangeT m c Source # (*>) :: ChangeT m a -> ChangeT m b -> ChangeT m b Source # (<*) :: ChangeT m a -> ChangeT m b -> ChangeT m a Source #
Functor m => Functor (ChangeT m) Source # |
Instance details Defined in Agda.Utils.Update Methods fmap :: (a -> b) -> ChangeT m a -> ChangeT m b Source # (<$) :: a -> ChangeT m b -> ChangeT m a Source #
Monad m => Monad (ChangeT m) Source # |
Instance details Defined in Agda.Utils.Update Methods (>>=) :: ChangeT m a -> (a -> ChangeT m b) -> ChangeT m b Source # (>>) :: ChangeT m a -> ChangeT m b -> ChangeT m b Source # return :: a -> ChangeT m a Source #
MonadFail m => MonadFail (ChangeT m) Source # |
Instance details Defined in Agda.Utils.Update Methods fail :: String -> ChangeT m a Source #
type StT ChangeT a Source # |
Instance details Defined in Agda.Utils.Update type StT ChangeT a = (a, Any)

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

Run a `ChangeT` 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).

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

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

Blindly run an updater.

type Change a = ChangeT Identity a Source #

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

The class of change monads.

Methods

tellDirty Source #

Arguments

:: m () | Mark computation as having changed something.

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

#### Instances

Instances details

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

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

Run a `Change` computation, returning result plus change flag.

type Updater a = UpdaterT Identity a Source #

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.

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

Blindly run an updater.

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

Mark a computation as dirty.

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

class Traversable f => Updater1 (f :: Type -> Type) where Source #

Like `Functor`, but preserving sharing.

Minimal complete definition

Nothing

Methods

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

updates1 Source #

Arguments

:: Updater a |

-> Updater (f a)

    = sharing . updater1

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

#### Instances

Instances details

Updater1 Maybe Source # |
Instance details Defined in Agda.Utils.Update Methods updater1 :: Updater a -> Updater (Maybe a) Source # updates1 :: Updater a -> Updater (Maybe a) Source # update1 :: Updater a -> EndoFun (Maybe a) Source #
Updater1 [] Source # |
Instance details Defined in Agda.Utils.Update Methods updater1 :: Updater a -> Updater [a] Source # updates1 :: Updater a -> Updater [a] Source # update1 :: Updater a -> EndoFun [a] Source #

class Updater2 (f :: Type -> Type -> Type) where Source #

Like `Bifunctor`, but preserving sharing.

Minimal complete definition

updater2

Methods

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

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

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

#### Instances

Instances details

Updater2 Either Source # |
Instance details Defined in Agda.Utils.Update Methods updater2 :: Updater a -> Updater b -> Updater (Either a b) Source # updates2 :: Updater a -> Updater b -> Updater (Either a b) Source # update2 :: Updater a -> Updater b -> EndoFun (Either a b) Source #
Updater2 (,) Source # |
Instance details Defined in Agda.Utils.Update Methods updater2 :: Updater a -> Updater b -> Updater (a, b) Source # updates2 :: Updater a -> Updater b -> Updater (a, b) Source # update2 :: Updater a -> Updater b -> EndoFun (a, b) Source #