Init.System.ST

source

def EST (ε : Type) (σ : Type) :

Type → Type

Equations

EST ε σ = EStateM ε σ

Instances For

source

@[inline, reducible]

abbrev ST (σ : Type) :

Type → Type

Equations

ST σ = EST Empty σ

Instances For

source

instance instMonadEST (ε : Type) (σ : Type) :

Monad (EST ε σ)

Equations

instMonadEST ε σ = inferInstanceAs (Monad (EStateM ε σ))

source

instance instMonadExceptOfEST (ε : Type) (σ : Type) :

MonadExceptOf ε (EST ε σ)

Equations

instMonadExceptOfEST ε σ = inferInstanceAs (MonadExceptOf ε (EStateM ε σ))

source

instance instInhabitedEST {ε : Type} {σ : Type} {α : Type} [Inhabited ε] :

Inhabited (EST ε σ α)

Equations

instInhabitedEST = inferInstanceAs (Inhabited (EStateM ε σ α))

source

instance instMonadST (σ : Type) :

Monad (ST σ)

Equations

instMonadST σ = inferInstanceAs (Monad (EST Empty σ))

source

class STWorld (σ : outParam Type) (m : Type → Type) :

Type

Instances

source

instance instSTWorld {σ : Type} {m : Type → Type} {n : Type → Type} [MonadLift m n] [STWorld σ m] :

STWorld σ n

Equations

instSTWorld = { }

source

instance instSTWorldEST {ε : Type} {σ : Type} :

STWorld σ (EST ε σ)

Equations

instSTWorldEST = { }

source

@[noinline]

def runEST {ε : Type} {α : Type} (x : (σ : Type) → EST ε σ α) :

Except ε α

Equations

runEST x = match x Unit () with | EStateM.Result.ok a a_1 => Except.ok a | EStateM.Result.error ex a => Except.error ex

Instances For

source

@[noinline]

def runST {α : Type} (x : (σ : Type) → ST σ α) :

Equations

runST x = match x Unit () with | EStateM.Result.ok a a_1 => a | EStateM.Result.error ex a => nomatch ex

Instances For

source

@[always_inline]

instance instMonadLiftSTEST {ε : Type} {σ : Type} :

MonadLift (ST σ) (EST ε σ)

Equations

One or more equations did not get rendered due to their size.

source

opaque ST.RefPointed :

NonemptyType

References

source

structure ST.Ref (σ : Type) (α : Type) :

Type

ref : NonemptyType.type ST.RefPointed
h : Nonempty α

Instances For

source

instance ST.instNonemptyRef {σ : Type} {α : Type} [s : Nonempty α] :

Nonempty (ST.Ref σ α)

Equations

(_ : Nonempty (ST.Ref σ α)) = (_ : Nonempty (ST.Ref σ α))

source

@[extern lean_st_mk_ref]

opaque ST.Prim.mkRef {σ : Type} {α : Type} (a : α) :

ST σ (ST.Ref σ α)

source

@[extern lean_st_ref_get]

opaque ST.Prim.Ref.get {σ : Type} {α : Type} (r : ST.Ref σ α) :

ST σ α

source

@[extern lean_st_ref_set]

opaque ST.Prim.Ref.set {σ : Type} {α : Type} (r : ST.Ref σ α) (a : α) :

ST σ Unit

source

@[extern lean_st_ref_swap]

opaque ST.Prim.Ref.swap {σ : Type} {α : Type} (r : ST.Ref σ α) (a : α) :

ST σ α

source

@[extern lean_st_ref_take]

unsafe opaque ST.Prim.Ref.take {σ : Type} {α : Type} (r : ST.Ref σ α) :

ST σ α

source

@[extern lean_st_ref_ptr_eq]

opaque ST.Prim.Ref.ptrEq {σ : Type} {α : Type} (r1 : ST.Ref σ α) (r2 : ST.Ref σ α) :

ST σ Bool

source

@[inline]

unsafe def ST.Prim.Ref.modifyUnsafe {σ : Type} {α : Type} (r : ST.Ref σ α) (f : α → α) :

ST σ Unit

Equations

ST.Prim.Ref.modifyUnsafe r f = do let v ← ST.Prim.Ref.take r ST.Prim.Ref.set r (f v)

Instances For

source

@[inline]

unsafe def ST.Prim.Ref.modifyGetUnsafe {σ : Type} {α : Type} {β : Type} (r : ST.Ref σ α) (f : α → β × α) :

ST σ β

Equations

ST.Prim.Ref.modifyGetUnsafe r f = do let v ← ST.Prim.Ref.take r match f v with | (b, a) => do ST.Prim.Ref.set r a pure b

Instances For

source

@[implemented_by ST.Prim.Ref.modifyUnsafe]

def ST.Prim.Ref.modify {σ : Type} {α : Type} (r : ST.Ref σ α) (f : α → α) :

ST σ Unit

Equations

ST.Prim.Ref.modify r f = do let v ← ST.Prim.Ref.get r ST.Prim.Ref.set r (f v)

Instances For

source

@[implemented_by ST.Prim.Ref.modifyGetUnsafe]

def ST.Prim.Ref.modifyGet {σ : Type} {α : Type} {β : Type} (r : ST.Ref σ α) (f : α → β × α) :

ST σ β

Equations

ST.Prim.Ref.modifyGet r f = do let v ← ST.Prim.Ref.get r match f v with | (b, a) => do ST.Prim.Ref.set r a pure b

Instances For

source

@[inline]

def ST.mkRef {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (a : α) :

m (ST.Ref σ α)

Equations

ST.mkRef a = liftM (ST.Prim.mkRef a)

Instances For

source

@[inline]

def ST.Ref.get {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) :

m α

Equations

ST.Ref.get r = liftM (ST.Prim.Ref.get r)

Instances For

source

@[inline]

def ST.Ref.set {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) (a : α) :

m Unit

Equations

ST.Ref.set r a = liftM (ST.Prim.Ref.set r a)

Instances For

source

@[inline]

def ST.Ref.swap {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) (a : α) :

m α

Equations

ST.Ref.swap r a = liftM (ST.Prim.Ref.swap r a)

Instances For

source

@[inline]

unsafe def ST.Ref.take {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) :

m α

Equations

ST.Ref.take r = liftM (ST.Prim.Ref.take r)

Instances For

source

@[inline]

def ST.Ref.ptrEq {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r1 : ST.Ref σ α) (r2 : ST.Ref σ α) :

m Bool

Equations

ST.Ref.ptrEq r1 r2 = liftM (ST.Prim.Ref.ptrEq r1 r2)

Instances For

source

@[inline]

def ST.Ref.modify {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) (f : α → α) :

m Unit

Equations

ST.Ref.modify r f = liftM (ST.Prim.Ref.modify r f)

Instances For

source

@[inline]

def ST.Ref.modifyGet {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} {β : Type} (r : ST.Ref σ α) (f : α → β × α) :

m β

Equations

ST.Ref.modifyGet r f = liftM (ST.Prim.Ref.modifyGet r f)

Instances For

source

def ST.Ref.toMonadStateOf {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) :

MonadStateOf α m

Equations

ST.Ref.toMonadStateOf r = { get := ST.Ref.get r, set := ST.Ref.set r, modifyGet := fun {α_1 : Type} => ST.Ref.modifyGet r }

Instances For