1	import Base
2	import ./relation_types.bend as G
3	import ./entity_key.bend as Key
4	
5	type Progress<-S:Data,-State:Type> is Type:
6	  Complete{world:State}
7	  Incomplete{world:State,frames:List<&2,G.CleanupFrame<S>>}
8	def Step(~S:Data,~State:Type) -> Type:
9	  G.CleanupFrame<S> -> State -> @+namespace:U32 -> List<&2,G.Descriptor<S>> -> List<&2,G.CleanupFrame<S>> -> State & List<&2,G.CleanupFrame<S>>
10	
11	def resumed_generic(-S:Data,-State:Type,observed:State & List<&2,G.CleanupFrame<S>>,next:State -> List<&2,G.CleanupFrame<S>> -> Progress<S,State>) -> Progress<S,State>:
12	  (world,frames) = observed
13	  next(world,frames)
14	def drive(~S:Data,~State:Type,~step:Step(~S,~State),fuel: Nat,frames: List<&2,G.CleanupFrame<S>>,world: State,+namespace: U32,+descriptors: List<&2,G.Descriptor<S>>) -> Progress<S,State>:
15	  match fuel frames:
16	    case _ Nil{}: Complete{world}
17	    case 0n frames: Incomplete{world,frames}
18	    case 1n+rest Con{frame,frames}: resumed_generic(S,State,step(frame,world,namespace,descriptors,frames),world => frames => drive(~S,~State,~step,rest,frames,world,namespace,descriptors))
19	
20	
21	# This is the existing structural inventory bound expressed as arbitrary Nat.
22	# Counting is eager; very large inventories can spend work in arithmetic before
23	# the same driver discovers completion. No narrower integer or cap is used.
24	def inventory_units(remaining:Nat,nodes:Nat,+edges:Nat,descriptors:Nat) -> Nat:
25	  Nat.mul(remaining,Nat.mul(Nat.add(edges,1n+nodes),Nat.add(3n,Nat.add(Nat.mul(2n,descriptors),Nat.mul(2n,edges)))))
26	def total_units(-S:Data,remaining:Nat,nodes:Nat,edges:List<&2,G.Edge<S>>,descriptors:List<&2,G.Descriptor<S>>) -> Nat:
27	  inventory_units(remaining,nodes,List.length(&2,G.Edge<S>,edges),List.length(&2,G.Descriptor<S>,descriptors))
28	def owner_blocks(~S:Data,~State:Type,~step:Step(~S,~State),remaining:Nat,result:Progress<S,State>,+nodes:Nat,+edges:List<&2,G.Edge<S>>,+namespace:U32,+descriptors:List<&2,G.Descriptor<S>>) -> Progress<S,State>:
29	  match remaining result:
30	    case 0n result:result
31	    case _ Complete{world}:Complete{world}
32	    case remaining Incomplete{world,frames}:drive(~S,~State,~step,total_units(S,remaining,nodes,edges,descriptors),frames,world,namespace,descriptors)
33	
34	def automatic(~S:Data,~State:Type,~step:Step(~S,~State),state:State,+nodes:Nat,+edges:List<&2,G.Edge<S>>,+namespace:U32,key:Key.Key,+descriptors:List<&2,G.Descriptor<S>>) -> Progress<S,State>:
35	  owner_blocks(~S,~State,~step,nodes,drive(~S,~State,~step,1n,[G.CleanupEnter{key}],state,namespace,descriptors),nodes,edges,namespace,descriptors)
36	
37	def resumed(~S:Data,~State:Type,observed:State & List<&2,G.CleanupFrame<S>>,next:State -> List<&2,G.CleanupFrame<S>> -> Progress<S,State>) -> Progress<S,State>:
38	  resumed_generic(S,State,observed,next)