1	# Bounded capacity pools with affine reservations: reserve, release, split, and combine.
2	import 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.
6	type 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.
11	type Grant is Type:
12	  Grant{owner: Nat, amount: Nat}
13	
14	type Reserve is Type:
15	  Took{pool: Pool, grant: Grant}
16	  Refused{pool: Pool}
17	
18	type Release is Type:
19	  Released{pool: Pool}
20	  Kept{pool: Pool, grant: Grant}
21	
22	type Split is Type:
23	  Parts{taken: Grant, rest: Grant}
24	  Whole{grant: Grant}
25	
26	type Combine is Type:
27	  Joined{grant: Grant}
28	  Apart{first: Grant, second: Grant}
29	
30	# An empty pool of `capacity` units.
31	def new(owner: Nat, capacity: Nat) -> Pool:
32	  Pool{owner, capacity, 0n}
33	
34	def capacity(p: Pool) -> Nat:
35	  Pool{o, c, h} = p
36	  c
37	
38	def reserved(p: Pool) -> Nat:
39	  Pool{o, c, h} = p
40	  h
41	
42	# The units that a reserve can still take.
43	def available(p: Pool) -> Nat:
44	  Pool{o, c, h} = p
45	  Nat.sub(c, h)
46	
47	def 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.
55	def 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	
59	def 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.
68	def 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	
73	def 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.
81	def split(g: Grant, +n: Nat) -> Split:
82	  Grant{+o, +a} = g
83	  split.go(Nat.is_le(n, a), o, a, n)
84	
85	def 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.
93	def 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)