resources.bend

bend-kit-resources@0.1.0.0 · 96 lines · 18 definitions

1# Bounded capacity pools with affine reservations: reserve, release, split, and combine.
2import Base
3
4# A pool of `capacity` units, `held` of them reserved. `owner` names the pool,
5# so a reservation cannot return to a different pool.
6type Pool is Data:
7  Pool{owner: Nat, capacity: Nat, held: Nat}
8
9# A reservation of `amount` units from the pool named `owner`. It is affine:
10# it cannot be copied, so it is released at most once.
11type Grant is Type:
12  Grant{owner: Nat, amount: Nat}
13
14type Reserve is Type:
15  Took{pool: Pool, grant: Grant}
16  Refused{pool: Pool}
17
18type Release is Type:
19  Released{pool: Pool}
20  Kept{pool: Pool, grant: Grant}
21
22type Split is Type:
23  Parts{taken: Grant, rest: Grant}
24  Whole{grant: Grant}
25
26type Combine is Type:
27  Joined{grant: Grant}
28  Apart{first: Grant, second: Grant}
29
30# An empty pool of `capacity` units.
31def new(owner: Nat, capacity: Nat) -> Pool:
32  Pool{owner, capacity, 0n}
33
34def capacity(p: Pool) -> Nat:
35  Pool{o, c, h} = p
36  c
37
38def reserved(p: Pool) -> Nat:
39  Pool{o, c, h} = p
40  h
41
42# The units that a reserve can still take.
43def available(p: Pool) -> Nat:
44  Pool{o, c, h} = p
45  Nat.sub(c, h)
46
47def reserve.go(fits: Bool, +o: Nat, c: Nat, h: Nat, +n: Nat) -> Reserve:
48  match fits:
49    case True{}:
50      Took{Pool{o, c, Nat.add(h, n)}, Grant{o, n}}
51    case False{}:
52      Refused{Pool{o, c, h}}
53
54# Takes n units when they fit. Refused hands back the pool unchanged.
55def reserve(p: Pool, +n: Nat) -> Reserve:
56  Pool{o, +c, +h} = p
57  reserve.go(Nat.is_le(Nat.add(h, n), c), o, c, h, n)
58
59def release.go(ok: Bool, o: Nat, c: Nat, h: Nat, q: Nat, +n: Nat) -> Release:
60  match ok:
61    case True{}:
62      Released{Pool{o, c, Nat.sub(h, n)}}
63    case False{}:
64      Kept{Pool{o, c, h}, Grant{q, n}}
65
66# Returns g's units to p. Kept hands back both unchanged when g names another
67# pool or holds more than p has reserved.
68def release(p: Pool, g: Grant) -> Release:
69  Pool{+o, c, +h} = p
70  Grant{+q, +n} = g
71  release.go(Nat.is_eq(o, q) && Nat.is_le(n, h), o, c, h, q, n)
72
73def split.go(fits: Bool, +o: Nat, +a: Nat, +n: Nat) -> Split:
74  match fits:
75    case True{}:
76      Parts{Grant{o, n}, Grant{o, Nat.sub(a, n)}}
77    case False{}:
78      Whole{Grant{o, a}}
79
80# Splits n units off g. Whole hands back g when it holds fewer than n.
81def split(g: Grant, +n: Nat) -> Split:
82  Grant{+o, +a} = g
83  split.go(Nat.is_le(n, a), o, a, n)
84
85def combine.go(same: Bool, o: Nat, a: Nat, q: Nat, b: Nat) -> Combine:
86  match same:
87    case True{}:
88      Joined{Grant{o, Nat.add(a, b)}}
89    case False{}:
90      Apart{Grant{o, a}, Grant{q, b}}
91
92# Joins two grants of one pool. Apart hands back both when their pools differ.
93def combine(x: Grant, y: Grant) -> Combine:
94  Grant{+o, a} = x
95  Grant{+q, b} = y
96  combine.go(Nat.is_eq(o, q), o, a, q, b)