Greenlet — the result type

inductive Control.Concurrent.Green.Greenlet (α : Type) : Type

A computation result that is either immediately available or pending.

• .now a — value available, continuation runs synchronously.
• .later t — value pending; bind uses BaseIO.bindTask to register the continuation without blocking.

• now {α : Type} : α → Greenlet α
• later {α : Type} : Task α → Greenlet α

@[inline]

def Control.Concurrent.Green.Greenlet.toTask {α : Type} : Greenlet α → Task α

Equations

• (Control.Concurrent.Green.Greenlet.now a).toTask = { get := a }
• (Control.Concurrent.Green.Greenlet.later t).toTask = t

@[inline]

def Control.Concurrent.Green.Greenlet.map {α β : Type} (f : α → β) : Greenlet α → Greenlet β

Equations

• Control.Concurrent.Green.Greenlet.map f (Control.Concurrent.Green.Greenlet.now a) = Control.Concurrent.Green.Greenlet.now (f a)
• Control.Concurrent.Green.Greenlet.map f (Control.Concurrent.Green.Greenlet.later t) = Control.Concurrent.Green.Greenlet.later (Task.map f t)

GreenBase — the non-blocking IO monad

structure Control.Concurrent.Green.GreenBase (α : Type) : Type

The core green-thread monad (no error handling, no cancellation).

Wraps BaseIO (Greenlet α) with a custom bind that yields pool threads on .later via BaseIO.bindTask.

• run : BaseIO (Greenlet α)

  Run the green computation, producing a Greenlet.

@[inline]

def Control.Concurrent.Green.GreenBase.pure {α : Type} (a : α) : GreenBase α

Equations

• Control.Concurrent.Green.GreenBase.pure a = { run := pure (Control.Concurrent.Green.Greenlet.now a) }

@[inline]

def Control.Concurrent.Green.GreenBase.bind {α β : Type} (x : GreenBase α) (f : α → GreenBase β) : GreenBase β

Bind that yields the pool thread on .later.

Termination: O(1) beyond its arguments. bindTask registers a callback and returns immediately.

Fairness: The .later branch calls BaseIO.bindTask, not IO.wait. The pool thread is freed.

Equations

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

@[inline]

def Control.Concurrent.Green.GreenBase.map {α β : Type} (f : α → β) (x : GreenBase α) : GreenBase β

Equations

• Control.Concurrent.Green.GreenBase.map f x = { run := (fun (x : Control.Concurrent.Green.Greenlet α) => Control.Concurrent.Green.Greenlet.map f x) <$> x.run }

@[implicit_reducible]

instance Control.Concurrent.Green.GreenBase.instMonad : Monad GreenBase

Equations

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

@[implicit_reducible]

instance Control.Concurrent.Green.GreenBase.instFunctor : Functor GreenBase

Equations

• Control.Concurrent.Green.GreenBase.instFunctor = { map := fun {α β : Type} => Control.Concurrent.Green.GreenBase.map }

@[implicit_reducible]

instance Control.Concurrent.Green.GreenBase.instMonadLiftBaseIO : MonadLift BaseIO GreenBase

Equations

• Control.Concurrent.Green.GreenBase.instMonadLiftBaseIO = { monadLift := fun {α : Type} (x : BaseIO α) => { run := Control.Concurrent.Green.Greenlet.now <$> x } }

@[inline]

def Control.Concurrent.Green.GreenBase.await {α : Type} (t : Task α) : GreenBase α

Await a Task without blocking. The pool thread is freed.

$$\text{await} : \text{Task}\ \alpha \to \text{GreenBase}\ \alpha$$

Equations

• Control.Concurrent.Green.GreenBase.await t = { run := pure (Control.Concurrent.Green.Greenlet.later t) }

@[inline]

def Control.Concurrent.Green.GreenBase.awaitConcurrent {α : Type} (op : Concurrent α) : GreenBase α

Await a Concurrent α operation without blocking.

$$\text{awaitConcurrent} : \text{Concurrent}\ \alpha \to \text{GreenBase}\ \alpha$$

Equations

• Control.Concurrent.Green.GreenBase.awaitConcurrent op = { run := do let task ← op pure (Control.Concurrent.Green.Greenlet.later task) }

@[inline]

def Control.Concurrent.Green.GreenBase.asTask {α : Type} (x : GreenBase α) : BaseIO (Task α)

Convert to a Task for interop with IO.wait.

Equations

• x.asTask = Control.Concurrent.Green.Greenlet.toTask <$> x.run

Green — the full green-thread monad

def Control.Concurrent.Green.Green (α : Type) : Type

A fair green-thread computation with cancellation and error handling.

$$\text{Green}\ \alpha := \text{CancellationToken} \to \text{GreenBase}\ (\text{Except}\ \text{IO.Error}\ \alpha)$$

• Fair: awaiting a Task frees the pool thread (via GreenBase.bind).
• Cancellable: takes a CancellationToken for cooperative cancellation.
• Error-handling: exceptions propagate via Except.

Equations

• Control.Concurrent.Green.Green α = (Std.CancellationToken → Control.Concurrent.Green.GreenBase (Except IO.Error α))

@[inline]

def Control.Concurrent.Green.Green.pure {α : Type} (a : α) : Green α

Equations

• Control.Concurrent.Green.Green.pure a _token = Control.Concurrent.Green.GreenBase.pure (Except.ok a)

@[inline]

def Control.Concurrent.Green.Green.bind {α β : Type} (x : Green α) (f : α → Green β) : Green β

Equations

• x.bind f token = (x token).bind fun (x : Except IO.Error α) => match x with | Except.ok a => f a token | Except.error e => Control.Concurrent.Green.GreenBase.pure (Except.error e)

@[inline]

def Control.Concurrent.Green.Green.map {α β : Type} (f : α → β) (x : Green α) : Green β

Equations

• Control.Concurrent.Green.Green.map f x token = Control.Concurrent.Green.GreenBase.map (fun (x : Except IO.Error α) => Except.map f x) (x token)

@[inline]

def Control.Concurrent.Green.Green.throw {α : Type} (e : IO.Error) : Green α

Equations

• Control.Concurrent.Green.Green.throw e _token = Control.Concurrent.Green.GreenBase.pure (Except.error e)

@[inline]

def Control.Concurrent.Green.Green.tryCatch {α : Type} (x : Green α) (h : IO.Error → Green α) : Green α

Equations

• x.tryCatch h token = (x token).bind fun (x : Except IO.Error α) => match x with | Except.ok a => Control.Concurrent.Green.GreenBase.pure (Except.ok a) | Except.error e => h e token

@[implicit_reducible]

instance Control.Concurrent.Green.Green.instMonad : Monad Green

Equations

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

@[implicit_reducible]

instance Control.Concurrent.Green.Green.instFunctor : Functor Green

Equations

• Control.Concurrent.Green.Green.instFunctor = { map := fun {α β : Type} => Control.Concurrent.Green.Green.map }

@[implicit_reducible]

instance Control.Concurrent.Green.Green.instMonadExceptError : MonadExcept IO.Error Green

Equations

• Control.Concurrent.Green.Green.instMonadExceptError = { throw := fun {α : Type} => Control.Concurrent.Green.Green.throw, tryCatch := fun {α : Type} => Control.Concurrent.Green.Green.tryCatch }

@[implicit_reducible]

instance Control.Concurrent.Green.Green.instMonadFinally : MonadFinally Green

Equations

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

@[implicit_reducible]

instance Control.Concurrent.Green.Green.instMonadLiftIO : MonadLift IO Green

Equations

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

Core operations

@[inline]

def Control.Concurrent.Green.Green.await {α : Type} (t : Task α) : Green α

Await a Task without blocking the pool thread.

Equations

• Control.Concurrent.Green.Green.await t _token = Control.Concurrent.Green.GreenBase.map Except.ok (Control.Concurrent.Green.GreenBase.await t)

@[inline]

def Control.Concurrent.Green.Green.awaitConcurrent {α : Type} (op : Concurrent α) : Green α

Await a Concurrent α operation without blocking the pool thread.

Equations

• Control.Concurrent.Green.Green.awaitConcurrent op _token = Control.Concurrent.Green.GreenBase.map Except.ok (Control.Concurrent.Green.GreenBase.awaitConcurrent op)

@[inline]

def Control.Concurrent.Green.Green.checkCancelled : Green Unit

Check cancellation and throw if cancelled.

Equations

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

MVar integration

@[inline]

def Control.Concurrent.Green.Green.takeMVar {α : Type} [Nonempty α] (mv : MVar α) : Green α

Equations

• Control.Concurrent.Green.Green.takeMVar mv = Control.Concurrent.Green.Green.awaitConcurrent mv.take

@[inline]

def Control.Concurrent.Green.Green.putMVar {α : Type} (mv : MVar α) (a : α) : Green Unit

Equations

• Control.Concurrent.Green.Green.putMVar mv a = Control.Concurrent.Green.Green.awaitConcurrent (mv.put a)

@[inline]

def Control.Concurrent.Green.Green.readMVar {α : Type} [Nonempty α] (mv : MVar α) : Green α

Equations

• Control.Concurrent.Green.Green.readMVar mv = Control.Concurrent.Green.Green.awaitConcurrent mv.read

Chan integration

@[inline]

def Control.Concurrent.Green.Green.readChan {α : Type} [Nonempty α] (ch : Chan α) : Green α

Equations

• Control.Concurrent.Green.Green.readChan ch = Control.Concurrent.Green.Green.awaitConcurrent ch.read

QSem integration

@[inline]

def Control.Concurrent.Green.Green.waitSem (sem : QSem) : Green Unit

Equations

• Control.Concurrent.Green.Green.waitSem sem = Control.Concurrent.Green.Green.awaitConcurrent sem.wait

@[inline]

def Control.Concurrent.Green.Green.waitSemN (sem : QSemN) (n : Nat) : Green Unit

Equations

• Control.Concurrent.Green.Green.waitSemN sem n = Control.Concurrent.Green.Green.awaitConcurrent (sem.wait n)

Running Green computations

def Control.Concurrent.Green.Green.run {α : Type} (action : Green α) (token : Std.CancellationToken) : BaseIO (Task (Except IO.Error α))

Run a Green computation, returning a Task that resolves when the entire continuation chain completes. No pool thread is blocked during any await.

Equations

• action.run token = (action token).asTask

def Control.Concurrent.Green.Green.block {α : Type} (action : Green α) (token : Std.CancellationToken) : IO α

Run a Green computation and block until it completes (top-level only).

Equations

• action.block token = do let task ← liftM (action.run token) let __do_lift ← liftM (IO.wait task) match __do_lift with | Except.ok a => pure a | Except.error e => throw e

Axiom-dependent properties

axiom Control.Concurrent.Green.GreenBase.bind_terminates {α β : Type} (x : GreenBase α) (f : α → GreenBase β) : True

Termination: GreenBase.bind x f terminates if x terminates and f a terminates for all a. Axiom-dependent on lean_io_bind_task returning in O(1).

axiom Control.Concurrent.Green.GreenBase.await_resumes {α β : Type} (t : Task α) (f : α → GreenBase β) : True

Liveness: GreenBase.await t >>= f calls f iff t resolves. Axiom-dependent on lean_io_bind_task invoking the callback exactly once on task completion.

axiom Control.Concurrent.Green.GreenBase.no_pool_starvation {α β : Type} (x : GreenBase α) (f : α → GreenBase β) : True

Fairness: GreenBase.bind never blocks the pool thread. Structural: uses BaseIO.bindTask (non-blocking), not IO.wait (blocking).