Documentation

Init.System.ST

def EST (ε σ : Type) :

A restricted version of IO in which mutable state and exceptions are the only side effects.

It is possible to run EST computations in a non-monadic context using runEST.

Equations
    Instances For
      @[reducible, inline]
      abbrev ST (σ : Type) :

      A restricted version of IO in which mutable state is the only side effect.

      It is possible to run ST computations in a non-monadic context using runST.

      Equations
        Instances For
          instance instMonadEST (ε σ : Type) :
          Monad (EST ε σ)
          Equations
            instance instMonadExceptOfEST (ε σ : Type) :
            MonadExceptOf ε (EST ε σ)
            Equations
              instance instInhabitedEST {ε σ α : Type} [Inhabited ε] :
              Inhabited (EST ε σ α)
              Equations
                instance instMonadST (σ : Type) :
                Monad (ST σ)
                Equations
                  class STWorld (σ : outParam Type) (m : TypeType) :

                  An auxiliary class used to infer the “state” of EST and ST monads.

                    Instances
                      instance instSTWorldOfMonadLift {σ : Type} {m n : TypeType} [MonadLift m n] [STWorld σ m] :
                      STWorld σ n
                      Equations
                        instance instSTWorldEST {ε σ : Type} :
                        STWorld σ (EST ε σ)
                        Equations
                          @[noinline]
                          def runEST {ε α : Type} (x : (σ : Type) → EST ε σ α) :
                          Except ε α

                          Runs an EST computation, in which mutable state and exceptions are the only side effects.

                          Equations
                            Instances For
                              @[noinline]
                              def runST {α : Type} (x : (σ : Type) → ST σ α) :
                              α

                              Runs an ST computation, in which mutable state via ST.Ref is the only side effect.

                              Equations
                                Instances For
                                  @[always_inline]
                                  instance instMonadLiftSTEST {ε σ : Type} :
                                  MonadLift (ST σ) (EST ε σ)
                                  Equations
                                    structure ST.Ref (σ α : Type) :

                                    Mutable reference cells that contain values of type α. These cells can read from and mutated in the ST σ monad.

                                    Instances For
                                      instance ST.instNonemptyRef {σ α : Type} [s : Nonempty α] :
                                      Nonempty (Ref σ α)
                                      @[extern lean_st_mk_ref]
                                      opaque ST.Prim.mkRef {σ α : Type} (a : α) :
                                      ST σ (Ref σ α)
                                      @[extern lean_st_ref_get]
                                      opaque ST.Prim.Ref.get {σ α : Type} (r : Ref σ α) :
                                      ST σ α
                                      @[extern lean_st_ref_set]
                                      opaque ST.Prim.Ref.set {σ α : Type} (r : Ref σ α) (a : α) :
                                      ST σ Unit
                                      @[extern lean_st_ref_swap]
                                      opaque ST.Prim.Ref.swap {σ α : Type} (r : Ref σ α) (a : α) :
                                      ST σ α
                                      @[extern lean_st_ref_take]
                                      unsafe opaque ST.Prim.Ref.take {σ α : Type} (r : Ref σ α) :
                                      ST σ α
                                      @[extern lean_st_ref_ptr_eq]
                                      opaque ST.Prim.Ref.ptrEq {σ α : Type} (r1 r2 : Ref σ α) :
                                      ST σ Bool
                                      @[inline]
                                      unsafe def ST.Prim.Ref.modifyUnsafe {σ α : Type} (r : Ref σ α) (f : αα) :
                                      ST σ Unit
                                      Equations
                                        Instances For
                                          @[inline]
                                          unsafe def ST.Prim.Ref.modifyGetUnsafe {σ α β : Type} (r : Ref σ α) (f : αβ × α) :
                                          ST σ β
                                          Equations
                                            Instances For
                                              @[implemented_by ST.Prim.Ref.modifyUnsafe]
                                              def ST.Prim.Ref.modify {σ α : Type} (r : Ref σ α) (f : αα) :
                                              ST σ Unit
                                              Equations
                                                Instances For
                                                  @[implemented_by ST.Prim.Ref.modifyGetUnsafe]
                                                  def ST.Prim.Ref.modifyGet {σ α β : Type} (r : Ref σ α) (f : αβ × α) :
                                                  ST σ β
                                                  Equations
                                                    Instances For
                                                      @[inline]
                                                      def ST.mkRef {σ : Type} {m : TypeType} [MonadLiftT (ST σ) m] {α : Type} (a : α) :
                                                      m (Ref σ α)

                                                      Creates a new mutable reference that contains the provided value a.

                                                      Equations
                                                        Instances For
                                                          @[inline]
                                                          def ST.Ref.get {σ : Type} {m : TypeType} [MonadLiftT (ST σ) m] {α : Type} (r : Ref σ α) :
                                                          m α

                                                          Reads the value of a mutable reference.

                                                          Equations
                                                            Instances For
                                                              @[inline]
                                                              def ST.Ref.set {σ : Type} {m : TypeType} [MonadLiftT (ST σ) m] {α : Type} (r : Ref σ α) (a : α) :

                                                              Replaces the value of a mutable reference.

                                                              Equations
                                                                Instances For
                                                                  @[inline]
                                                                  def ST.Ref.swap {σ : Type} {m : TypeType} [MonadLiftT (ST σ) m] {α : Type} (r : Ref σ α) (a : α) :
                                                                  m α

                                                                  Atomically swaps the value of a mutable reference cell with another value. The reference cell's original value is returned.

                                                                  Equations
                                                                    Instances For
                                                                      @[inline]
                                                                      unsafe def ST.Ref.take {σ : Type} {m : TypeType} [MonadLiftT (ST σ) m] {α : Type} (r : Ref σ α) :
                                                                      m α

                                                                      Reads the value of a mutable reference cell, removing it.

                                                                      This causes subsequent attempts to read from or take the reference cell to block until a new value is written using ST.Ref.set.

                                                                      Equations
                                                                        Instances For
                                                                          @[inline]
                                                                          def ST.Ref.ptrEq {σ : Type} {m : TypeType} [MonadLiftT (ST σ) m] {α : Type} (r1 r2 : Ref σ α) :

                                                                          Checks whether two reference cells are in fact aliases for the same cell.

                                                                          Even if they contain the same value, two references allocated by different executions of IO.mkRef or ST.mkRef are distinct. Modifying one has no effect on the other. Likewise, a single reference cell may be aliased, and modifications to one alias also modify the other.

                                                                          Equations
                                                                            Instances For
                                                                              @[inline]
                                                                              def ST.Ref.modify {σ : Type} {m : TypeType} [MonadLiftT (ST σ) m] {α : Type} (r : Ref σ α) (f : αα) :

                                                                              Atomically modifies a mutable reference cell by replacing its contents with the result of a function call.

                                                                              Equations
                                                                                Instances For
                                                                                  @[inline]
                                                                                  def ST.Ref.modifyGet {σ : Type} {m : TypeType} [MonadLiftT (ST σ) m] {α β : Type} (r : Ref σ α) (f : αβ × α) :
                                                                                  m β

                                                                                  Atomically modifies a mutable reference cell by replacing its contents with the result of a function call that simultaneously computes a value to return.

                                                                                  Equations
                                                                                    Instances For
                                                                                      def ST.Ref.toMonadStateOf {σ : Type} {m : TypeType} [MonadLiftT (ST σ) m] {α : Type} (r : Ref σ α) :

                                                                                      Creates a MonadStateOf instance from a reference cell.

                                                                                      This allows programs written against the state monad API to be executed using a mutable reference cell to track the state.

                                                                                      Equations
                                                                                        Instances For