@[inline, reducible]

abbrev Lake.Job (α : Type u_1) : Type u_1

A Lake job.

Equations

• Lake.Job α = Lake.OptionIOTask α

@[inline, reducible]

abbrev Lake.JobM (α : Type) : Type

The monad of Lake jobs.

Equations

• Lake.JobM = Lake.BuildM

@[inline, reducible]

abbrev Lake.ResultM : Type → Type

The monad of a finished Lake job.

Equations

• Lake.ResultM = Lake.OptionIO

@[inline]

def Lake.Job.nil : Lake.Job Unit

Equations

• Lake.Job.nil = pure ()

@[inline]

def Lake.Job.async {α : Type} (act : Lake.JobM α) : Lake.SchedulerM (Lake.Job α)

Equations

• Lake.Job.async act = Lake.async act

@[inline]

def Lake.Job.await {α : Type} (self : Lake.Job α) : Lake.ResultM α

Equations

• Lake.Job.await self = Lake.await self

@[inline]

def Lake.Job.bindSync {α : Type} {β : Type} (self : Lake.Job α) (f : α → Lake.JobM β) (prio : optParam Task.Priority Task.Priority.default) : Lake.SchedulerM (Lake.Job β)

Equations

• Lake.Job.bindSync self f prio = Lake.bindSync prio self f

@[inline]

def Lake.Job.bindAsync {α : Type} {β : Type} (self : Lake.Job α) (f : α → Lake.SchedulerM (Lake.Job β)) : Lake.SchedulerM (Lake.Job β)

Equations

• Lake.Job.bindAsync self f = Lake.bindAsync self f

@[inline, reducible]

abbrev Lake.BuildJob (α : Type u_1) : Type u_1

A Lake build job.

Equations

• Lake.BuildJob α = Lake.Job (α × Lake.BuildTrace)

@[inline]

def Lake.BuildJob.mk {α : Type u_1} (job : Lake.Job (α × Lake.BuildTrace)) : Lake.BuildJob α

Equations

• Lake.BuildJob.mk job = job

@[inline]

def Lake.BuildJob.ofJob (self : Lake.Job Lake.BuildTrace) : Lake.BuildJob Unit

Equations

• Lake.BuildJob.ofJob self = Lake.BuildJob.mk ((fun x => ((), x)) <$> self)

@[inline]

def Lake.BuildJob.toJob {α : Type u_1} (self : Lake.BuildJob α) : Lake.Job (α × Lake.BuildTrace)

Equations

• Lake.BuildJob.toJob self = self

@[inline]

def Lake.BuildJob.nil : Lake.BuildJob Unit

Equations

• Lake.BuildJob.nil = Lake.BuildJob.mk (pure ((), Lake.nilTrace))

@[inline]

def Lake.BuildJob.pure {α : Type u_1} (a : α) : Lake.BuildJob α

Equations

• Lake.BuildJob.pure a = Lake.BuildJob.mk (pure (a, Lake.nilTrace))

instance Lake.BuildJob.instPureBuildJob : Pure Lake.BuildJob

Equations

• Lake.BuildJob.instPureBuildJob = { pure := fun {α} => Lake.BuildJob.pure }

@[inline]

def Lake.BuildJob.map {α : Type u_1} {β : Type u_1} (f : α → β) (self : Lake.BuildJob α) : Lake.BuildJob β

Equations

• Lake.BuildJob.map f self = Lake.BuildJob.mk ((fun x => match x with | (a, t) => (f a, t)) <$> Lake.BuildJob.toJob self)

instance Lake.BuildJob.instFunctorBuildJob : Functor Lake.BuildJob

Equations

• Lake.BuildJob.instFunctorBuildJob = { map := fun {α β} => Lake.BuildJob.map, mapConst := fun {α β} => Lake.BuildJob.map ∘ Function.const β }

@[inline]

def Lake.BuildJob.mapWithTrace {α : Type u_1} {β : Type u_1} (f : α → Lake.BuildTrace → β × Lake.BuildTrace) (self : Lake.BuildJob α) : Lake.BuildJob β

Equations

• Lake.BuildJob.mapWithTrace f self = Lake.BuildJob.mk ((fun x => match x with | (a, t) => f a t) <$> Lake.BuildJob.toJob self)

@[inline]

def Lake.BuildJob.bindSync {α : Type} {β : Type} (self : Lake.BuildJob α) (f : α → Lake.BuildTrace → Lake.JobM β) (prio : optParam Task.Priority Task.Priority.default) : Lake.SchedulerM (Lake.Job β)

Equations

• Lake.BuildJob.bindSync self f prio = Lake.Job.bindSync (Lake.BuildJob.toJob self) (fun x => match x with | (a, t) => f a t) prio

@[inline]

def Lake.BuildJob.bindAsync {α : Type} {β : Type} (self : Lake.BuildJob α) (f : α → Lake.BuildTrace → Lake.SchedulerM (Lake.Job β)) : Lake.SchedulerM (Lake.Job β)

Equations

• Lake.BuildJob.bindAsync self f = Lake.Job.bindAsync (Lake.BuildJob.toJob self) fun x => match x with | (a, t) => f a t

@[inline]

def Lake.BuildJob.await {α : Type} (self : Lake.BuildJob α) : Lake.ResultM α

Equations

• Lake.BuildJob.await self = (fun x => x.fst) <$> Lake.await (Lake.BuildJob.toJob self)

instance Lake.BuildJob.instAwaitBuildJobResultM : Lake.Await Lake.BuildJob Lake.ResultM

Equations

• Lake.BuildJob.instAwaitBuildJobResultM = { await := fun {α} => Lake.BuildJob.await }

@[inline]

def Lake.BuildJob.materialize {α : Type} (self : Lake.BuildJob α) : Lake.ResultM Unit

Equations

• Lake.BuildJob.materialize self = discard (Lake.await (Lake.BuildJob.toJob self))

def Lake.BuildJob.mix {α : Type} {β : Type} (t1 : Lake.BuildJob α) (t2 : Lake.BuildJob β) : BaseIO (Lake.BuildJob Unit)

Equations

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

def Lake.BuildJob.mixList {α : Type} (jobs : List (Lake.BuildJob α)) : BaseIO (Lake.BuildJob Unit)

Equations

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

def Lake.BuildJob.mixArray {α : Type} (jobs : Array (Lake.BuildJob α)) : BaseIO (Lake.BuildJob Unit)

Equations

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

def Lake.BuildJob.seqWithAsync {α : Type} {β : Type} {γ : Type} (f : α → β → γ) (t1 : Lake.BuildJob α) (t2 : Lake.BuildJob β) : BaseIO (Lake.BuildJob γ)

Equations

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

instance Lake.BuildJob.instSeqWithAsyncBaseIOBuildJob : Lake.SeqWithAsync BaseIO Lake.BuildJob

Equations

• Lake.BuildJob.instSeqWithAsyncBaseIOBuildJob = { seqWithAsync := fun {γ α β} => Lake.BuildJob.seqWithAsync }

def Lake.BuildJob.collectList {α : Type} (jobs : List (Lake.BuildJob α)) : BaseIO (Lake.BuildJob (List α))

Equations

• Lake.BuildJob.collectList jobs = List.foldrM (Lake.seqWithAsync List.cons) (pure []) jobs

def Lake.BuildJob.collectArray {α : Type} (jobs : Array (Lake.BuildJob α)) : BaseIO (Lake.BuildJob (Array α))

Equations

• Lake.BuildJob.collectArray jobs = Array.foldlM (Lake.seqWithAsync Array.push) (pure #[]) jobs 0 (Array.size jobs)