1	import Base
2	import ./world.bend as W
3	import ./entity_key.bend as K
4	import ./execution_state.bend as State
5	import ./execution_query_domain.bend as D
6	import ./indexed_lifecycle.bend as Indexed
7	import ./chunk_column.bend as Column
8	
9	# Captured handles must originate from admitted actual World/Prepared state.
10	# Comparing all namespace/key/generation fields precedes physical conversion.
11	type Offset<-S:Data> is Data:
12	  MissingEntity{handle:W.Handle<S>}
13	  OutsideStorage{handle:W.Handle<S>,capacity:U32}
14	  Physical{handle:W.Handle<S>,offset:U32}
15	def checked_range(~S:Data,+handle:W.Handle<S>,+capacity:U32,+logical:U32,live:Bool,inRange:Bool) -> Offset<S>:
16	  match live inRange:
17	    case False{} _:MissingEntity{handle}
18	    case True{} False{}:OutsideStorage{handle,capacity}
19	    case True{} True{}:Physical{handle,U32.sub(logical,1)}
20	def checked_logical(~S:Data,+namespace:U32,+handles:List<&2,W.Handle<S>>,+capacity:U32,+handle:W.Handle<S>,+handleNamespace:U32,+key:K.Key) -> Offset<S>:
21	  checked_range(~S,handle,capacity,K.index(key),Bool.and(U32.is_eq(namespace,handleNamespace),State.member(~S,handle,handles)),Bool.and(Indexed.normal(K.index(key)),U32.is_le(K.index(key),capacity)))
22	def checked_offset(~S:Data,namespace:U32,handles:List<&2,W.Handle<S>>,capacity:U32,handle:W.Handle<S>) -> Offset<S>:
23	  match handle:
24	    case W.Handle{+hn,+key}:checked_logical(~S,namespace,handles,capacity,W.Handle{hn,key},hn,key)
25	type TargetCheck<-S:Data> is Data:
26	  Targets{handles:List<&2,W.Handle<S>>,offsets:D.Domain}
27	  Refused{handles:List<&2,W.Handle<S>>}
28	def unique(~S:Data,handles:List<&2,W.Handle<S>>) -> Bool:
29	  match handles:
30	    case []:True{}
31	    case +head <> +tail:Bool.and(Bool.not(State.member(~S,head,tail)),unique(~S,tail))
32	
33	def offset_handles(~S:Data,~C:Type,~R:Type,~E:Data,namespace:U32,capacity:U32,handle:W.Handle<S>,result:W.World<S,C,R,E> & List<&2,W.Handle<S>>) -> W.World<S,C,R,E> & Offset<S>:
34	  match result:
35	    case (world,handles):(world,checked_offset(~S,namespace,handles,capacity,handle))
36	def offset_namespace(~S:Data,~C:Type,~R:Type,~E:Data,capacity:U32,handle:W.Handle<S>,result:W.World<S,C,R,E> & U32) -> W.World<S,C,R,E> & Offset<S>:
37	  match result:
38	    case (world,namespace):offset_handles(~S,~C,~R,~E,namespace,capacity,handle,W.handles(~S,~C,~R,~E,world))
39	def offset_valid(~S:Data,~C:Type,~R:Type,~E:Data,capacity:U32,handle:W.Handle<S>,result:W.World<S,C,R,E> & Bool) -> W.World<S,C,R,E> & Offset<S>:
40	  match result:
41	    case (world,False{}):(world,MissingEntity{handle})
42	    case (world,True{}):offset_namespace(~S,~C,~R,~E,capacity,handle,W.namespace(~S,~C,~R,~E,world))
43	def world_offset(~S:Data,~C:Type,~R:Type,~E:Data,world:W.World<S,C,R,E>,capacity:U32,+handle:W.Handle<S>) -> W.World<S,C,R,E> & Offset<S>:
44	  offset_valid(~S,~C,~R,~E,capacity,handle,W.valid(~S,~C,~R,~E,world,handle))
45	
46	def index_checked(+logical:U32,normal:Bool) -> Maybe<&2,U32>:
47	  match normal:
48	    case False{}:None{}
49	    case True{}:Some{U32.sub(logical,1)}
50	def physical_index(+logical:U32) -> Maybe<&2,U32>:
51	  index_checked(logical,Indexed.normal(logical))
52	def captured_offset(~S:Data,+handles:List<&2,W.Handle<S>>,handle:W.Handle<S>) -> Offset<S>:
53	  match handles:
54	    case []:MissingEntity{handle}
55	    case W.Handle{+namespace,+key} <> +rest:checked_offset(~S,namespace,W.Handle{namespace,key} <> rest,Column.maximum_capacity(),handle)
56	def physical_live(~S:Data,checked:Offset<S>) -> Bool:
57	  match checked:
58	    case Physical{_,_}:True{}
59	    case _:False{}
60	def captured_live(~S:Data,handles:List<&2,W.Handle<S>>,handle:W.Handle<S>) -> Bool:
61	  physical_live(~S,captured_offset(~S,handles,handle))
62	def prepend_offset(~S:Data,tail:Maybe<&2,List<&2,U32>>,checked:Offset<S>) -> Maybe<&2,List<&2,U32>>:
63	  match tail checked:
64	    case Some{tail} Physical{_,offset}:Some{offset <> tail}
65	    case _ _:None{}
66	def target_offsets(~S:Data,+namespace:U32,+all:List<&2,W.Handle<S>>,remaining:List<&2,W.Handle<S>>) -> Maybe<&2,List<&2,U32>>:
67	  match remaining:
68	    case []:Some{[]}
69	    case +head <> tail:prepend_offset(~S,target_offsets(~S,namespace,all,tail),checked_offset(~S,namespace,all,Column.maximum_capacity(),head))
70	def targets_valid(~S:Data,handles:List<&2,W.Handle<S>>,domain:D.Domain,valid:Bool) -> TargetCheck<S>:
71	  match valid:
72	    case False{}:Refused{handles}
73	    case True{}:Targets{handles,domain}
74	def targets_validation(~S:Data,+handles:List<&2,W.Handle<S>>,+domain:D.Domain,validation:D.Validation) -> TargetCheck<S>:
75	  match validation:
76	    case D.Valid{}:targets_valid(~S,handles,domain,unique(~S,handles))
77	    case _:Refused{handles}
78	def targets_offsets(~S:Data,handles:List<&2,W.Handle<S>>,offsets:Maybe<&2,List<&2,U32>>) -> TargetCheck<S>:
79	  match offsets:
80	    case None{}:Refused{handles}
81	    case Some{+offsets}:targets_validation(~S,handles,D.Domain{offsets},D.validate(Column.maximum_capacity(),D.Domain{offsets}))
82	def targets(~S:Data,namespace:U32,+handles:List<&2,W.Handle<S>>) -> TargetCheck<S>:
83	  targets_offsets(~S,handles,target_offsets(~S,namespace,handles,handles))