resources.bend checks
raw source on the hub · import bend-kit-resources@0.1.0.0/resources.bend as Resources
Bounded capacity pools with affine reservations: reserve, release, split, and combine.
1 import
import Base
Types
type Pool source · line 6 · raw
Data
A pool of capacity units, held of them reserved. owner names the pool,
so a reservation cannot return to a different pool.
Pool@owner:Nat -> @capacity:Nat -> @held:Nat -> Pool
type Grant source · line 11 · raw
Type
A reservation of amount units from the pool named owner. It is affine:
it cannot be copied, so it is released at most once.
Grant@owner:Nat -> @amount:Nat -> Grant
type Reserve source · line 14 · raw
Type
Took@pool:Pool -> @grant:Grant -> Reserve
Refused@pool:Pool -> Reserve
type Release source · line 18 · raw
Type
Released@pool:Pool -> Release
Kept@pool:Pool -> @grant:Grant -> Release
type Split source · line 22 · raw
Type
Parts@taken:Grant -> @rest:Grant -> Split
Whole@grant:Grant -> Split
type Combine source · line 26 · raw
Type
Joined@grant:Grant -> Combine
Apart@first:Grant -> @second:Grant -> Combine
Definitions
def new source · line 31 · raw
@owner:Nat -> @capacity:Nat -> Pool
An empty pool of capacity units.
def capacity source · line 34 · raw
@p:Pool -> Nat
def reserved source · line 38 · raw
@p:Pool -> Nat
def available source · line 43 · raw
@p:Pool -> Nat
The units that a reserve can still take.
def reserve.go source · line 47 · raw
@fits:Bool -> @+o:Nat -> @c:Nat -> @h:Nat -> @+n:Nat -> Reserve
def reserve source · line 55 · raw
@p:Pool -> @+n:Nat -> Reserve
Takes n units when they fit. Refused hands back the pool unchanged.
def release.go source · line 59 · raw
@ok:Bool -> @o:Nat -> @c:Nat -> @h:Nat -> @q:Nat -> @+n:Nat -> Release
def release source · line 68 · raw
@p:Pool -> @g:Grant -> Release
Returns g's units to p. Kept hands back both unchanged when g names another pool or holds more than p has reserved.
def split.go source · line 73 · raw
@fits:Bool -> @+o:Nat -> @+a:Nat -> @+n:Nat -> Split
def split source · line 81 · raw
@g:Grant -> @+n:Nat -> Split
Splits n units off g. Whole hands back g when it holds fewer than n.
def combine.go source · line 85 · raw
@same:Bool -> @o:Nat -> @a:Nat -> @q:Nat -> @b:Nat -> Combine
def combine source · line 93 · raw
@x:Grant -> @y:Grant -> Combine
Joins two grants of one pool. Apart hands back both when their pools differ.