max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: priority for bindSync

Browse source
This commit is contained in:
Gabriel Ebner 2023-04-06 00:20:05 +00:00 • committed by Mac
parent 98a55105ff
commit 312960820c
2 changed files with 13 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
Lake/Build/Job.lean
View file

@ -31,8 +31,8 @@ namespace Job
await self
@[inline] protected def bindSync
(self : Job α) (f : α → JobM β) : SchedulerM (Job β) :=
bindSync self f
(self : Job α) (f : α → JobM β) (prio := Task.Priority.default) : SchedulerM (Job β) :=
bindSync prio self f
@[inline] protected def bindAsync
(self : Job α) (f : α → SchedulerM (Job β)) : SchedulerM (Job β) :=
@ -69,8 +69,9 @@ instance : Functor BuildJob where
map := BuildJob.map
@[inline] protected def bindSync
(self : BuildJob α) (f : α → BuildTrace → JobM β) : SchedulerM (Job β) :=
self.toJob.bindSync fun (a, t) => f a t
(self : BuildJob α) (f : α → BuildTrace → JobM β)
(prio : Task.Priority := .default) : SchedulerM (Job β) :=
self.toJob.bindSync (prio := prio) fun (a, t) => f a t
@[inline] protected def bindAsync
(self : BuildJob α) (f : α → BuildTrace → SchedulerM (Job β)) : SchedulerM (Job β) :=

16
Lake/Util/Async.lean
View file

@ -101,7 +101,7 @@ instance [Await k m] : Await (OptionT k) (OptionT m) where
class BindSync (m : Type u → Type v) (n : outParam $ Type u' → Type w) (k : outParam $ Type u → Type u') where
/-- Perform a synchronous action after another (a)synchronous task completes successfully. -/
bindSync {α β : Type u} : k α → (α → m β) → n (k β)
bindSync {α β : Type u} : Task.Priority → k α → (α → m β) → n (k β)
export BindSync (bindSync)
@ -143,29 +143,29 @@ extends SeqAsync n k, SeqLeftAsync n k, SeqRightAsync n k, SeqWithAsync n k wher
/-! ## Standard Instances -/
instance : BindSync Id Id Task := ⟨flip Task.map⟩
instance : BindSync BaseIO BaseIO BaseIOTask := ⟨flip BaseIO.mapTask⟩
instance : BindSync Id Id Task := ⟨fun _ => flip Task.map⟩
instance : BindSync BaseIO BaseIO BaseIOTask := ⟨fun _ => flip BaseIO.mapTask⟩
instance : BindSync (EIO ε) BaseIO (ETask ε) where
bindSync ka f := ka.run |> BaseIO.mapTask fun
bindSync prio ka f := ka.run |> BaseIO.mapTask (prio := prio) fun
| Except.ok a => f a |>.toBaseIO
| Except.error e => pure <| Except.error e
instance : BindSync OptionIO BaseIO OptionIOTask where
bindSync ka f := ka.run |> BaseIO.mapTask fun
bindSync prio ka f := ka.run |> BaseIO.mapTask (prio := prio) fun
| some a => f a |>.toBaseIO
| none => pure none
instance [BindSync m n k] : BindSync (ReaderT ρ m) (ReaderT ρ n) k where
bindSync ka f := fun r => bindSync ka fun a => f a r
bindSync prio ka f := fun r => bindSync prio ka fun a => f a r
instance [BindSync m n k] [Pure m] : BindSync (ExceptT ε m) n (ExceptT ε k) where
bindSync ka f := cast (by delta ExceptT; rfl) <| bindSync (n := n) ka.run fun
bindSync prio ka f := cast (by delta ExceptT; rfl) <| bindSync prio (n := n) ka.run fun
| Except.ok a => f a |>.run
| Except.error e => pure <| Except.error e
instance [BindSync m n k] [Pure m] : BindSync (OptionT m) n (OptionT k) where
bindSync ka f := cast (by delta OptionT; rfl) <| bindSync ka.run fun
bindSync prio ka f := cast (by delta OptionT; rfl) <| bindSync prio ka.run fun
| some a => f a |>.run
| none => pure none