@[reducible, inline]

abbrev Concurrency.Semaphore.Count : Type

Equations

• Concurrency.Semaphore.Count = Nat

structure Concurrency.Semaphore : Type

• condition : Std.Condvar
• count : Std.Mutex Nat

def Concurrency.Semaphore.new (n : Nat := 0) : BaseIO Semaphore

Equations

• Concurrency.Semaphore.new n = Concurrency.Semaphore.mk✝ <$> Std.Condvar.new <*> Std.Mutex.new n

def Concurrency.Semaphore.isAvailable {m : Type → Type u_1} [Monad m] [MonadState Nat m] : m Bool

Equations

• Concurrency.Semaphore.isAvailable = do let count ← get pure (decide (count > 0))

def Concurrency.Semaphore.isUnavailable {m : Type → Type u_1} [Monad m] [MonadState Nat m] : m Bool

Equations

• Concurrency.Semaphore.isUnavailable = not <$> Concurrency.Semaphore.isAvailable

def Concurrency.Semaphore.wait (self : Semaphore) : BaseIO Unit

Equations

• self.wait = self.count.atomicallyOnce self.condition Concurrency.Semaphore.isAvailable (modify Nat.pred)

def Concurrency.Semaphore.signal (self : Semaphore) : BaseIO Unit

Equations

• self.signal = self.count.atomically do modify Nat.succ liftM self.condition.notifyOne

def Concurrency.Semaphore.bracket {m : Type → Type u_1} {a : Type} [Monad m] [MonadFinally m] [MonadLift BaseIO m] (self : Semaphore) (action : m a) : m a

Equations

• self.bracket action = tryFinally (do liftM self.wait action) (liftM self.signal)