1	import Base
2	import ./execution_access.bend as Access
3	import ./world.bend as W
4	import ./state.bend as State
5	import ./component.bend as Component
6	import ./capabilities.bend as Cap
7	
8	# Existing State.observed compares declared endpoints against the immediate
9	# canonical checked read before deciding whether to invoke a canonical modifier.
10	# No payload owner or raw replacement operation is returned to an ordinary body.
11	type Operations<-S:Data,-K:Data,-V:Data,-Move:Data,-H:Type> is Type:
12	  Operations{move:H -> W.Handle<S> -> Move -> H & State.Outcome<V,Unit>}
13	def Ops(~S:Data,~K:Data,~V:Data,~Move:Data,Permit:Data,H:Type) -> Type:Operations<S,K,V,Move,H>
14	def Modifier(~S:Data,~H:Type,~P:Type,~V:Data) -> Type:
15	  (P -> P & V) -> H -> W.Handle<S> -> H & Maybe<&2,V>
16	type MoveOwner<-S:Data,-H:Type,-P:Type,-V:Data> is Type:
17	  MoveOwner{scope:H,handle:W.Handle<S>,modifier:Maybe<&1,Modifier(~S,~H,~P,~V)>}
18	def write_result(~S:Data,~H:Type,~P:Type,~V:Data,handle:W.Handle<S>,result:H & Maybe<&2,V>) -> MoveOwner<S,H,P,V> & State.WriteStatus<Unit>:
19	  match result:
20	    case (scope,None{}):(MoveOwner{scope,handle,None{}},State.WriteRejected{Unit{}})
21	    case (scope,Some{_}):(MoveOwner{scope,handle,None{}},State.WriteAccepted{})
22	def write_owner(~S:Data,~H:Type,~P:Type,~V:Data,~update:V -> P -> P & V,owner:MoveOwner<S,H,P,V>,value:V) -> MoveOwner<S,H,P,V> & State.WriteStatus<Unit>:
23	  match owner:
24	    case MoveOwner{scope,handle,None{}}:(MoveOwner{scope,handle,None{}},State.WriteRejected{Unit{}})
25	    case MoveOwner{scope,+handle,Some{modify}}:write_result(~S,~H,~P,~V,handle,modify(update(value),scope,handle))
26	def completed(~S:Data,~H:Type,~P:Type,~V:Data,result:MoveOwner<S,H,P,V> & State.Outcome<V,Unit>) -> H & State.Outcome<V,Unit>:
27	  match result:
28	    case (MoveOwner{scope,_,_},outcome):(scope,outcome)
29	def endpoints_observed(~S:Data,~H:Type,~P:Type,~V:Data,~equal:V -> V -> Bool,~update:V -> P -> P & V,owner:MoveOwner<S,H,P,V>,actual:Component.Access<V>,endpoints:V & V) -> H & State.Outcome<V,Unit>:
30	  match endpoints:
31	    case (expected,target):completed(~S,~H,~P,~V,State.observed(~MoveOwner<S,H,P,V>,~V,~Unit,~equal,~Cap.Request{write_owner(~S,~H,~P,~V,~update)},expected,target,(owner,actual)))
32	def read_result(~S:Data,~H:Type,~P:Type,~V:Data,~Move:Data,~equal:V -> V -> Bool,~endpoints:Move -> V & V,~update:V -> P -> P & V,modify:Modifier(~S,~H,~P,~V),handle:W.Handle<S>,request:Move,result:H & Component.Access<V>) -> H & State.Outcome<V,Unit>:
33	  match result:
34	    case (scope,actual):endpoints_observed(~S,~H,~P,~V,~equal,~update,MoveOwner{scope,handle,Some{modify}},actual,endpoints(request))
35	def move(~S:Data,~H:Type,~P:Type,~V:Data,~Move:Data,~equal:V -> V -> Bool,~endpoints:Move -> V & V,~update:V -> P -> P & V,get:H -> W.Handle<S> -> H & Component.Access<V>,modify:Modifier(~S,~H,~P,~V),scope:H,handle:W.Handle<S>,request:Move) -> H & State.Outcome<V,Unit>:
36	  match handle:
37	    case +handle:read_result(~S,~H,~P,~V,~Move,~equal,~endpoints,~update,modify,handle,request,get(scope,handle))
38	def narrow(~S:Data,~K:Data,~H:Type,~P:Type,~V:Data,~Move:Data,~equal:V -> V -> Bool,~endpoints:Move -> V & V,~update:V -> P -> P & V,cap:Access.ComponentWrite<S,H,P,V>) -> Operations<S,K,V,Move,H>:
39	  match cap:
40	    case Access.ComponentWrite{_,modify,get}:Operations{move(~S,~H,~P,~V,~Move,~equal,~endpoints,~update,get,modify)}
41	def move_field(~S:Data,~K:Data,~H:Type,~V:Data,~Move:Data,cap:Operations<S,K,V,Move,H>) -> H -> W.Handle<S> -> Move -> H & State.Outcome<V,Unit>:
42	  match cap:
43	    case Operations{move}:move