Init.Control.State

source

noncomputable def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) :

Type (max u v)

Equations

StateT σ m α = (σ → m (α × σ))

source

@[inline]

def StateT.run {σ : Type u} {m : Type u → Type v} {α : Type u} (x : StateT σ m α) (s : σ) :

m (α × σ)

Equations

StateT.run x s = x s

source

@[inline]

def StateT.run' {σ : Type u} {m : Type u → Type v} [inst : Functor m] {α : Type u} (x : StateT σ m α) (s : σ) :

m α

Equations

StateT.run' x s = (fun a => a.fst) <$> x s

source

noncomputable def StateM (σ : Type u) (α : Type u) :

Type u

Equations

StateM σ α = StateT σ Id α

source

noncomputable instance instSubsingletonStateM {σ : Type u_1} {α : Type u_1} [inst : Subsingleton σ] [inst : Subsingleton α] :

Subsingleton (StateM σ α)

Equations

@instSubsingletonStateM = @instSubsingletonStateM.proof_1

source

@[inline]

def StateT.pure {σ : Type u} {m : Type u → Type v} [inst : Monad m] {α : Type u} (a : α) :

StateT σ m α

Equations

StateT.pure a s = pure (a, s)

source

@[inline]

def StateT.bind {σ : Type u} {m : Type u → Type v} [inst : Monad m] {α : Type u} {β : Type u} (x : StateT σ m α) (f : α → StateT σ m β) :

StateT σ m β

Equations

StateT.bind x f s = do let discr ← x s match discr with | (a, s) => f a s

source

@[inline]

def StateT.map {σ : Type u} {m : Type u → Type v} [inst : Monad m] {α : Type u} {β : Type u} (f : α → β) (x : StateT σ m α) :

StateT σ m β

Equations

StateT.map f x s = do let discr ← x s match discr with | (a, s) => pure (f a, s)

source

instance StateT.instMonadStateT {σ : Type u} {m : Type u → Type v} [inst : Monad m] :

Monad (StateT σ m)

Equations

StateT.instMonadStateT = Monad.mk

source

@[inline]

def StateT.orElse {σ : Type u} {m : Type u → Type v} [inst : Alternative m] {α : Type u} (x₁ : StateT σ m α) (x₂ : Unit → StateT σ m α) :

StateT σ m α

Equations

StateT.orElse x₁ x₂ s = HOrElse.hOrElse (x₁ s) fun x => x₂ () s

source

@[inline]

def StateT.failure {σ : Type u} {m : Type u → Type v} [inst : Alternative m] {α : Type u} :

StateT σ m α

Equations

StateT.failure x = failure

source

instance StateT.instAlternativeStateT {σ : Type u} {m : Type u → Type v} [inst : Monad m] [inst : Alternative m] :

Alternative (StateT σ m)

Equations

StateT.instAlternativeStateT = Alternative.mk (fun {α} => StateT.failure) fun {α} => StateT.orElse

source

@[inline]

def StateT.get {σ : Type u} {m : Type u → Type v} [inst : Monad m] :

StateT σ m σ

Equations

StateT.get s = pure (s, s)

source

@[inline]

def StateT.set {σ : Type u} {m : Type u → Type v} [inst : Monad m] :

σ → StateT σ m PUnit

Equations

StateT.set s' x = pure (PUnit.unit, s')

source

@[inline]

def StateT.modifyGet {σ : Type u} {m : Type u → Type v} [inst : Monad m] {α : Type u} (f : σ → α × σ) :

StateT σ m α

Equations

StateT.modifyGet f s = pure (f s)

source

@[inline]

def StateT.lift {σ : Type u} {m : Type u → Type v} [inst : Monad m] {α : Type u} (t : m α) :

StateT σ m α

Equations

StateT.lift t s = do let a ← t pure (a, s)

source

instance StateT.instMonadLiftStateT {σ : Type u} {m : Type u → Type v} [inst : Monad m] :

MonadLift m (StateT σ m)

Equations

StateT.instMonadLiftStateT = { monadLift := fun {α} => StateT.lift }

source

instance StateT.instMonadFunctorStateT (σ : Type u_1) (m : Type u_1 → Type u_2) [inst : Monad m] :

MonadFunctor m (StateT σ m)

Equations

StateT.instMonadFunctorStateT σ m = { monadMap := fun {α} f x s => f (α × σ) (x s) }

source

instance StateT.instMonadExceptOfStateT {σ : Type u} {m : Type u → Type v} [inst : Monad m] (ε : Type u_1) [inst : MonadExceptOf ε m] :

MonadExceptOf ε (StateT σ m)

Equations

StateT.instMonadExceptOfStateT ε = { throw := fun {α} => StateT.lift ∘ throwThe ε, tryCatch := fun {α} x c s => tryCatchThe ε (x s) fun e => c e s }

source

instance instMonadStateOfStateT {σ : Type u} {m : Type u → Type v} [inst : Monad m] :

MonadStateOf σ (StateT σ m)

Equations

instMonadStateOfStateT = { get := StateT.get, set := StateT.set, modifyGet := fun {α} => StateT.modifyGet }

source

instance StateT.monadControl (σ : Type u) (m : Type u → Type v) [inst : Monad m] :

MonadControl m (StateT σ m)

Equations

StateT.monadControl σ m = { stM := fun α => α × σ, liftWith := fun {α} f => do let s ← get liftM (f fun {β} x => StateT.run x s), restoreM := fun {α} x => do let discr ← liftM x match discr with | (a, s) => do set s pure a }

source

instance StateT.tryFinally {m : Type u → Type v} {σ : Type u} [inst : MonadFinally m] [inst : Monad m] :

MonadFinally (StateT σ m)

Equations

StateT.tryFinally = { tryFinally' := fun {α β} x h s => do let discr ← tryFinally' (x s) fun _fun_discr => match _fun_discr with | some (a, s') => h (some a) s' | none => h none s match discr with | ((a, snd), b, s'') => pure ((a, b), s'') }