1	import Base
2	import entity_key.bend as K
3	
4	type Phase is Data:
5	  Consumed{}
6	  Pending{}
7	  Live{}
8	  DeadRetained{}
9	  Free{}
10	type Slot is Data:
11	  Slot{generation:U32,phase:Phase}
12	type Allocator is Type:
13	  Allocator{next:U32,high:U32,slots:Array<Slot>,capacity:U32,depth:Nat,free:List<&2,U32>,order:List<&2,K.Key>}
14	type Reservation is Data:
15	  Reserved{key:K.Key}
16	  Exhausted{}
17	
18	def empty() -> Allocator:
19	  Allocator{1,0,Array.new(Slot,0n,Slot{0,Consumed{}}),1,0n,[],[]}
20	
21	def live(phase:Phase) -> Bool:
22	  match phase:
23	    case Live{}:True{}
24	    case _:False{}
25	def pending(phase:Phase) -> Bool:
26	  match phase:
27	    case Pending{}:True{}
28	    case _:False{}
29	def metadata(phase:Phase) -> Bool:
30	  match phase:
31	    case Free{}:False{}
32	    case _:True{}
33	def phase_valid(mode:U32,phase:Phase) -> Bool:
34	  match mode:
35	    case 0:metadata(phase)
36	    case 1:live(phase)
37	    case _:pending(phase)
38	def slot_valid(+key:K.Key,mode:U32,slot:Slot) -> Bool:
39	  match slot:
40	    case Slot{generation,phase}:Bool.and(U32.is_eq(K.generation(key),generation),phase_valid(mode,phase))
41	def checked_slot(+key:K.Key,mode:U32,+next:U32,+high:U32,+capacity:U32,+depth:Nat,+free:List<&2,U32>,+order:List<&2,K.Key>,observed:Array<Slot> & Slot) -> Allocator & Bool:
42	  match observed:
43	    case (slots,slot):(Allocator{next,high,slots,capacity,depth,free,order},slot_valid(key,mode,slot))
44	def checked_bounds(allowed:Bool,allocator:Allocator,+key:K.Key,mode:U32) -> Allocator & Bool:
45	  match allowed allocator:
46	    case False{} allocator:(allocator,False{})
47	    case True{} Allocator{+next,+high,slots,+capacity,+depth,+free,+order}:checked_slot(key,mode,next,high,capacity,depth,free,order,Array.get(Slot,slots,K.index(key)))
48	def checked(allocator:Allocator,+key:K.Key,mode:U32) -> Allocator & Bool:
49	  match allocator:
50	    case Allocator{+next,high,slots,+capacity,depth,free,order}:checked_bounds(Bool.and(U32.is_lt(0,K.index(key)),Bool.and(U32.is_lt(K.index(key),next),U32.is_lt(K.index(key),capacity))),Allocator{next,high,slots,capacity,depth,free,order},key,mode)
51	
52	def keep(same:Bool,head:K.Key,rest:List<&2,K.Key>) -> List<&2,K.Key>:
53	  match same:
54	    case True{}:rest
55	    case False{}:head <> rest
56	
57	def without(keys:List<&2,K.Key>,+key:K.Key) -> List<&2,K.Key>:
58	  match keys:
59	    case []:[]
60	    case +head <> rest:keep(K.equal(head,key),head,without(rest,key))
61	
62	def phase_slot(key:K.Key,phase:Phase) -> Slot:
63	  Slot{K.generation(key),phase}
64	def write_phase(allocator:Allocator,+key:K.Key,phase:Phase) -> Allocator:
65	  match allocator:
66	    case Allocator{next,high,slots,capacity,depth,free,order}:Allocator{next,high,Array.set(Slot,slots,K.index(key),phase_slot(key,phase)),capacity,depth,free,order}
67	def set_checked(phase:Phase,+key:K.Key,observed:Allocator & Bool) -> Allocator & Bool:
68	  match observed:
69	    case (allocator,False{}):(allocator,False{})
70	    case (allocator,True{}):(write_phase(allocator,key,phase),True{})
71	def set(allocator:Allocator,+key:K.Key,phase:Phase) -> Allocator & Bool:
72	  set_checked(phase,key,checked(allocator,key,0))
73	def abandon_checked(+key:K.Key,observed:Allocator & Bool) -> Allocator:
74	  match observed:
75	    case (allocator,False{}):allocator
76	    case (Allocator{next,high,slots,capacity,depth,free,order},True{}):Allocator{next,high,Array.set(Slot,slots,K.index(key),phase_slot(key,Consumed{})),capacity,depth,free,without(order,key)}
77	def abandon(allocator:Allocator,+key:K.Key) -> Allocator:
78	  abandon_checked(key,checked(allocator,key,2))
79	
80	def release_checked(+key:K.Key,observed:Allocator & Bool) -> Allocator:
81	  match observed:
82	    case (allocator,False{}):allocator
83	    case (Allocator{next,high,slots,capacity,depth,free,order},True{}):Allocator{next,high,Array.set(Slot,slots,K.index(key),Slot{(K.generation(key) + 1 : U32),Free{}}),capacity,depth,K.index(key) <> free,without(order,key)}
84	def release(allocator:Allocator,+key:K.Key) -> Allocator:
85	  release_checked(key,checked(allocator,key,0))
86	
87	def reserve_recycled(+index:U32,+next:U32,+high:U32,+capacity:U32,+depth:Nat,+free:List<&2,U32>,+order:List<&2,K.Key>,observed:Array<Slot> & Slot) -> Allocator & Reservation:
88	  match observed:
89	    case (slots,Slot{+generation,_}):(Allocator{next,high,Array.set(Slot,slots,index,Slot{generation,Consumed{}}),capacity,depth,free,List.append(&2,K.Key,order,[K.EntityKey{index,generation}])},Reserved{K.EntityKey{index,generation}})
90	def reserve_fresh(available:Bool,grow:Bool,allocator:Allocator) -> Allocator & Reservation:
91	  match available grow allocator:
92	    case False{} _ allocator:(allocator,Exhausted{})
93	    case True{} False{} Allocator{+next,_,slots,+capacity,+depth,free,order}:(Allocator{(next + 1 : U32),next,Array.set(Slot,slots,next,Slot{0,Consumed{}}),capacity,depth,free,List.append(&2,K.Key,order,[K.EntityKey{next,0}])},Reserved{K.EntityKey{next,0}})
94	    case True{} True{} Allocator{+next,_,slots,+capacity,+depth,free,order}:(Allocator{(next + 1 : U32),next,Array.set(Slot,ANode{slots,Array.new(Slot,depth,Slot{0,Consumed{}})},next,Slot{0,Consumed{}}),(capacity * 2 : U32),1n+depth,free,List.append(&2,K.Key,order,[K.EntityKey{next,0}])},Reserved{K.EntityKey{next,0}})
95	def reserve(allocator:Allocator) -> Allocator & Reservation:
96	  match allocator:
97	    case Allocator{+next,high,slots,+capacity,depth,[],order}:reserve_fresh(U32.is_lt(next,131073),Bool.not(U32.is_lt(next,capacity)),Allocator{next,high,slots,capacity,depth,[],order})
98	    case Allocator{+next,+high,slots,+capacity,+depth,+index <> free,+order}:reserve_recycled(index,next,high,capacity,depth,free,order,Array.get(Slot,slots,index))
99	
100	def visible_join(+key:K.Key,next:Allocator -> List<&2,K.Key> -> Allocator & List<&2,K.Key>,reversed:List<&2,K.Key>,observed:Allocator & Bool) -> Allocator & List<&2,K.Key>:
101	  match observed:
102	    case (allocator,present):next(allocator,keep(Bool.not(present),key,reversed))
103	def visible_state_join(+key:K.Key,reversed:List<&2,K.Key>,observed:Allocator & Bool) -> Allocator & List<&2,K.Key>:
104	  match observed:
105	    case (allocator,present):(allocator,keep(Bool.not(present),key,reversed))
106	def visible_state_loop(keys:List<&2,K.Key>,state:Allocator & List<&2,K.Key>) -> Allocator & List<&2,K.Key>:
107	  match keys state:
108	    case [], (allocator,reversed):(allocator,List.reverse(&2,K.Key,reversed))
109	    case +key <> rest, (allocator,reversed):visible_state_loop(rest,visible_state_join(key,reversed,checked(allocator,key,1)))
110	def visible_loop(keys:List<&2,K.Key>,allocator:Allocator,reversed:List<&2,K.Key>) -> Allocator & List<&2,K.Key>:
111	  visible_state_loop(keys,(allocator,reversed))
112	def visible(allocator:Allocator) -> Allocator & List<&2,K.Key>:
113	  match allocator:
114	    case Allocator{next,high,slots,capacity,depth,free,+order}:visible_loop(order,Allocator{next,high,slots,capacity,depth,free,order},[])
115	
116	# Restore cancellation consumes queued reservations without freeing their IDs.
117	def abandon_pending_kept(+key:K.Key,observed:Allocator & List<&2,K.Key>) -> Allocator & List<&2,K.Key>:
118	  match observed:
119	    case (allocator,keys):(allocator,key <> keys)
120	def abandon_pending_checked(+key:K.Key,next:Allocator -> Allocator & List<&2,K.Key>,observed:Allocator & Bool) -> Allocator & List<&2,K.Key>:
121	  match observed:
122	    case (allocator,True{}):next(write_phase(allocator,key,Consumed{}))
123	    case (allocator,False{}):abandon_pending_kept(key,next(allocator))
124	def abandon_pending_loop(keys:List<&2,K.Key>,allocator:Allocator) -> Allocator & List<&2,K.Key>:
125	  match keys:
126	    case []:(allocator,[])
127	    case +key <> rest:abandon_pending_checked(key,next => abandon_pending_loop(rest,next),checked(allocator,key,2))
128	def abandon_pending_join(observed:Allocator & List<&2,K.Key>) -> Allocator:
129	  match observed:
130	    case (Allocator{next,high,slots,capacity,depth,free,_},order):Allocator{next,high,slots,capacity,depth,free,order}
131	def abandon_pending(allocator:Allocator) -> Allocator:
132	  match allocator:
133	    case Allocator{+next,+high,slots,+capacity,+depth,+free,+order}:abandon_pending_join(abandon_pending_loop(order,Allocator{next,high,slots,capacity,depth,free,order}))
134	
135	# A file may advance fresh-index progress, never replace generations or owners.
136	def floor_finish(+floor:U32,allocator:Allocator) -> Allocator:
137	  match allocator:
138	    case Allocator{next,high,slots,capacity,depth,free,order}:Allocator{U32.max(next,floor),U32.max(high,U32.sub(floor,1)),slots,capacity,depth,free,order}
139	def floor_step(grow:Bool,+floor:U32,next:Allocator -> Allocator,allocator:Allocator) -> Allocator:
140	  match grow allocator:
141	    case False{} allocator:floor_finish(floor,allocator)
142	    case True{} Allocator{n,high,slots,+capacity,+depth,free,order}:next(Allocator{n,high,ANode{slots,Array.new(Slot,depth,Slot{0,Consumed{}})},(capacity * 2 : U32),1n+depth,free,order})
143	def floor_grow(fuel:Nat,+floor:U32,allocator:Allocator) -> Allocator:
144	  match fuel allocator:
145	    case 0n allocator:floor_finish(floor,allocator)
146	    case 1n+rest Allocator{+next,+high,slots,+capacity,+depth,+free,+order}:floor_step(U32.is_lt(capacity,floor),floor,owner => floor_grow(rest,floor,owner),Allocator{next,high,slots,capacity,depth,free,order})
147	def floor_checked(allowed:Bool,+floor:U32,allocator:Allocator) -> Allocator & Bool:
148	  match allowed:
149	    case False{}:(allocator,False{})
150	    case True{}:(floor_grow(18n,floor,allocator),True{})
151	def advance_floor(allocator:Allocator,+floor:U32) -> Allocator & Bool:
152	  floor_checked(Bool.and(U32.is_lt(0,floor),U32.is_le(floor,131073)),floor,allocator)
153	
154	def count_keys(keys:List<&2,K.Key>) -> Nat:
155	  match keys:
156	    case []:0n
157	    case _ <> rest:1n+count_keys(rest)
158	def count_free(keys:List<&2,U32>) -> Nat:
159	  match keys:
160	    case []:0n
161	    case _ <> rest:1n+count_free(rest)
162	def restore_room_join(+floor:U32,needed:Nat,observed:Allocator & List<&2,K.Key>) -> Allocator & Bool:
163	  match observed:
164	    case (Allocator{+next,+high,slots,+capacity,+depth,+free,+order},live):
165	      (Allocator{next,high,slots,capacity,depth,free,order},Bool.and(Bool.and(U32.is_lt(0,floor),U32.is_le(floor,131073)),Nat.is_le(needed,Nat.add(Nat.add(count_keys(live),count_free(free)),U32.to_nat(U32.sub(131073,U32.max(next,floor)))))))
166	def restore_room(allocator:Allocator,floor:U32,needed:Nat) -> Allocator & Bool:
167	  restore_room_join(floor,needed,visible(allocator))