1	import Base
2	import ./change_tick.bend as Tick
3	import world.bend as W
4	import transaction.bend as T
5	import commands.bend as Cmd
6	import compose.bend as Q
7	import capabilities.bend as Cap
8	
9	# Trusted declaration; gameplay can only thread universally quantified H.
10	type Plan<-S:Data,-Store:Type,-R:Type,-E:Data,-Ops:Type -> Type,-H:Type> is Type:
11	  Plan{caps:Ops(H),select:Q.Frame<S,Store,R,E> -> Q.Frame<S,Store,R,E> & Bool,enter:Q.Frame<S,Store,R,E> -> H,leave:H -> Q.Frame<S,Store,R,E>}
12	
13	def plan_caps(~S:Data,~Store:Type,~R:Type,~E:Data,~Ops:Type -> Type,~H:Type,plan:Plan<S,Store,R,E,Ops,H>) -> Ops(H):
14	  match plan:
15	    case Plan{caps,_,_,_}: caps
16	
17	def plan_select(~S:Data,~Store:Type,~R:Type,~E:Data,~Ops:Type -> Type,~H:Type,plan:Plan<S,Store,R,E,Ops,H>) -> Q.Frame<S,Store,R,E> -> Q.Frame<S,Store,R,E> & Bool:
18	  match plan:
19	    case Plan{_,select,_,_}: select
20	
21	def plan_enter(~S:Data,~Store:Type,~R:Type,~E:Data,~Ops:Type -> Type,~H:Type,plan:Plan<S,Store,R,E,Ops,H>) -> Q.Frame<S,Store,R,E> -> H:
22	  match plan:
23	    case Plan{_,_,enter,_}: enter
24	
25	def plan_leave(~S:Data,~Store:Type,~R:Type,~E:Data,~Ops:Type -> Type,~H:Type,plan:Plan<S,Store,R,E,Ops,H>) -> H -> Q.Frame<S,Store,R,E>:
26	  match plan:
27	    case Plan{_,_,_,leave}: leave
28	
29	def left(~S:Data,~Store:Type,~R:Type,~E:Data,~H:Type,~U:Data,~Out:Data,~leave:H -> Q.Frame<S,Store,R,E>,observed:H & (T.Outcome<U> & Out)) -> Q.Frame<S,Store,R,E> & (T.Outcome<U> & Out):
30	  match observed:
31	    case (owner,result): (leave(owner),result)
32	
33	def prepend(~S: Data,~Store: Type,~R: Type,~E: Data,~U: Data,~Out: Data,value: Out,observed: T.Tx<W.World<S,Store,R,E>,E> & (T.Outcome<Q.Error<U>> & List<&2,Out>)) -> T.Tx<W.World<S,Store,R,E>,E> & (T.Outcome<Q.Error<U>> & List<&2,Out>):
34	  (tx,result) = observed
35	  (outcome,values) = result
36	  (tx,(outcome,value <> values))
37	def completed(~S: Data,~Store: Type,~R: Type,~E: Data,~U: Data,~Out: Data,next: T.Tx<W.World<S,Store,R,E>,E> -> T.Tx<W.World<S,Store,R,E>,E> & (T.Outcome<Q.Error<U>> & List<&2,Out>),tx: T.Tx<W.World<S,Store,R,E>,E>,value: Out,result: T.Outcome<Q.Error<U>>) -> T.Tx<W.World<S,Store,R,E>,E> & (T.Outcome<Q.Error<U>> & List<&2,Out>):
38	  match result:
39	    case T.Success{}: prepend(~S,~Store,~R,~E,~U,~Out,value,next(tx))
40	    case T.Failure{error}: (tx,(T.Failure{error},[]))
41	def body_returned(~S: Data,~Store: Type,~R: Type,~E: Data,~U: Data,~Out: Data,next: T.Tx<W.World<S,Store,R,E>,E> -> T.Tx<W.World<S,Store,R,E>,E> & (T.Outcome<Q.Error<U>> & List<&2,Out>),observed: Q.Frame<S,Store,R,E> & (T.Outcome<U> & Out)) -> T.Tx<W.World<S,Store,R,E>,E> & (T.Outcome<Q.Error<U>> & List<&2,Out>):
42	  match observed:
43	    case (Q.Frame{tx,_,internal,_},(user,value)): completed(~S,~Store,~R,~E,~U,~Out,next,tx,value,Q.outcome(~U,internal,user))
44	def selected(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~H: Type,~A: Data,~U: Data,~Out: Data,~plan: Plan<S,Store,R,E,Ops,H>,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & (T.Outcome<U> & Out),args: A,next: T.Tx<W.World<S,Store,R,E>,E> -> T.Tx<W.World<S,Store,R,E>,E> & (T.Outcome<Q.Error<U>> & List<&2,Out>),observed: Q.Frame<S,Store,R,E> & Bool) -> T.Tx<W.World<S,Store,R,E>,E> & (T.Outcome<Q.Error<U>> & List<&2,Out>):
45	  match observed:
46	    case (Q.Frame{tx,_,_,_},False{}): next(tx)
47	    case (frame,True{}): body_returned(~S,~Store,~R,~E,~U,~Out,next,left(~S,~Store,~R,~E,~H,~U,~Out,~plan_leave(~S,~Store,~R,~E,~Ops,~H,plan),Cap.invoke(~Ops,~A,~(T.Outcome<U> & Out),~body,~H,~plan_caps(~S,~Store,~R,~E,~Ops,~H,plan),args,plan_enter(~S,~Store,~R,~E,~Ops,~H,plan)(frame))))
48	def run_handles(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~H: Type,~A: Data,~U: Data,~Out: Data,~plan: Plan<S,Store,R,E,Ops,H>,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & (T.Outcome<U> & Out),handles: List<&2,W.Handle<S>>,+args: A,+cursor:Maybe<&2,Tick.Tick>,tx: T.Tx<W.World<S,Store,R,E>,E>) -> T.Tx<W.World<S,Store,R,E>,E> & (T.Outcome<Q.Error<U>> & List<&2,Out>):
49	  match handles:
50	    case []: (tx,(T.Success{},[]))
51	    case handle <> rest: selected(~S,~Store,~R,~E,~Ops,~H,~A,~U,~Out,~plan,~body,args,(tx => run_handles(~S,~Store,~R,~E,~Ops,~H,~A,~U,~Out,~plan,~body,rest,args,cursor,tx)),plan_select(~S,~Store,~R,~E,~Ops,~H,plan)(Q.Frame{tx,handle,None{},cursor}))
52	def finish_returned(~S: Data,~Store: Type,~R: Type,~E: Data,~U: Data,~Out: Data,values: List<&2,Out>,returned: T.Returned<W.World<S,Store,R,E>,Q.Error<U>>) -> Q.Executed<W.World<S,Store,R,E>,Q.Error<U>,Out>:
53	  match returned:
54	    case T.Returned{world,T.Success{}}: Q.Executed{world,T.Success{},values}
55	    case T.Returned{world,T.Failure{error}}: Q.Executed{world,T.Failure{error},[]}
56	def finished(~S: Data,~Store: Type,~R: Type,~E: Data,~U: Data,~Out: Data,observed: T.Tx<W.World<S,Store,R,E>,E> & (T.Outcome<Q.Error<U>> & List<&2,Out>)) -> Q.Executed<W.World<S,Store,R,E>,Q.Error<U>,Out>:
57	  match observed:
58	    case (tx,(result,values)): finish_returned(~S,~Store,~R,~E,~U,~Out,values,Cmd.tx_finish(~S,~Store,~R,~E,~Q.Error<U>,tx,result))
59	def scope_finished(~S:Data,~Store:Type,~R:Type,~E:Data,~U:Data,~Out:Data,owned:Bool,result:Q.Executed<W.World<S,Store,R,E>,Q.Error<U>,Out>) -> Q.Executed<W.World<S,Store,R,E>,Q.Error<U>,Out>:
60	  match result:
61	    case Q.Executed{world,outcome,values}:Q.Executed{W.finish_run(~S,~Store,~R,~E,owned,world),outcome,values}
62	def reserved_inner(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~H: Type,~A: Data,~U: Data,~Out: Data,~plan: Plan<S,Store,R,E,Ops,H>,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & (T.Outcome<U> & Out),args: A,cursor:Maybe<&2,Tick.Tick>,observed: W.World<S,Store,R,E> & List<&2,W.Handle<S>>) -> Q.Executed<W.World<S,Store,R,E>,Q.Error<U>,Out>:
63	  (world,handles) = observed
64	  finished(~S,~Store,~R,~E,~U,~Out,run_handles(~S,~Store,~R,~E,~Ops,~H,~A,~U,~Out,~plan,~body,handles,args,cursor,T.begin(~W.World<S,Store,R,E>,~E,world)))
65	# Snapshot live handles in ascending order; deferred commands stay invisible.
66	def reserved_scoped(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~H: Type,~A: Data,~U: Data,~Out: Data,~plan: Plan<S,Store,R,E,Ops,H>,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & (T.Outcome<U> & Out),args: A,cursor:Maybe<&2,Tick.Tick>,handles:List<&2,W.Handle<S>>,admitted:W.World<S,Store,R,E> & Bool) -> Q.Executed<W.World<S,Store,R,E>,Q.Error<U>,Out>:
67	  (world,owned)=admitted
68	  scope_finished(~S,~Store,~R,~E,~U,~Out,owned,reserved_inner(~S,~Store,~R,~E,~Ops,~H,~A,~U,~Out,~plan,~body,args,cursor,(world,handles)))
69	def reserved(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~H: Type,~A: Data,~U: Data,~Out: Data,~plan: Plan<S,Store,R,E,Ops,H>,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & (T.Outcome<U> & Out),args: A,cursor:Maybe<&2,Tick.Tick>,observed: W.World<S,Store,R,E> & List<&2,W.Handle<S>>) -> Q.Executed<W.World<S,Store,R,E>,Q.Error<U>,Out>:
70	  (world,handles)=observed
71	  reserved_scoped(~S,~Store,~R,~E,~Ops,~H,~A,~U,~Out,~plan,~body,args,cursor,handles,W.ensure_run(~S,~Store,~R,~E,world))
72	
73	def each(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~H: Type,~A: Data,~U: Data,~Out: Data,~plan: Plan<S,Store,R,E,Ops,H>,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & (T.Outcome<U> & Out),args: A,world: W.World<S,Store,R,E>) -> Q.Executed<W.World<S,Store,R,E>,Q.Error<U>,Out>:
74	  reserved(~S,~Store,~R,~E,~Ops,~H,~A,~U,~Out,~plan,~body,args,None{},W.handles(~S,~Store,~R,~E,world))
75	
76	
77	# Preserve explicit reader cursor in the accepted row frame.
78	def each_since(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~H: Type,~A: Data,~U: Data,~Out: Data,~plan: Plan<S,Store,R,E,Ops,H>,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & (T.Outcome<U> & Out),args: A,world: W.World<S,Store,R,E>,cursor:Maybe<&2,Tick.Tick>) -> Q.Executed<W.World<S,Store,R,E>,Q.Error<U>,Out>:
79	  reserved(~S,~Store,~R,~E,~Ops,~H,~A,~U,~Out,~plan,~body,args,cursor,W.handles(~S,~Store,~R,~E,world))
80	
81	# Separate closed template fields avoid constructing runtime Plan for projections.
82	def selected_fields(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~H: Type,~A: Data,~U: Data,~Out: Data,~caps:Ops(H),~select:Q.Frame<S,Store,R,E> -> Q.Frame<S,Store,R,E> & Bool,~enter:Q.Frame<S,Store,R,E> -> H,~leave:H -> Q.Frame<S,Store,R,E>,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & (T.Outcome<U> & Out),args: A,next: T.Tx<W.World<S,Store,R,E>,E> -> T.Tx<W.World<S,Store,R,E>,E> & (T.Outcome<Q.Error<U>> & List<&2,Out>),observed: Q.Frame<S,Store,R,E> & Bool) -> T.Tx<W.World<S,Store,R,E>,E> & (T.Outcome<Q.Error<U>> & List<&2,Out>):
83	  match observed:
84	    case (Q.Frame{tx,_,_,_},False{}): next(tx)
85	    case (frame,True{}): body_returned(~S,~Store,~R,~E,~U,~Out,next,left(~S,~Store,~R,~E,~H,~U,~Out,~leave,Cap.invoke(~Ops,~A,~(T.Outcome<U> & Out),~body,~H,~caps,args,enter(frame))))
86	def run_handles_fields(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~H: Type,~A: Data,~U: Data,~Out: Data,~caps:Ops(H),~select:Q.Frame<S,Store,R,E> -> Q.Frame<S,Store,R,E> & Bool,~enter:Q.Frame<S,Store,R,E> -> H,~leave:H -> Q.Frame<S,Store,R,E>,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & (T.Outcome<U> & Out),handles: List<&2,W.Handle<S>>,+args: A,+cursor:Maybe<&2,Tick.Tick>,tx: T.Tx<W.World<S,Store,R,E>,E>) -> T.Tx<W.World<S,Store,R,E>,E> & (T.Outcome<Q.Error<U>> & List<&2,Out>):
87	  match handles:
88	    case []: (tx,(T.Success{},[]))
89	    case handle <> rest: selected_fields(~S,~Store,~R,~E,~Ops,~H,~A,~U,~Out,~caps,~select,~enter,~leave,~body,args,(tx => run_handles_fields(~S,~Store,~R,~E,~Ops,~H,~A,~U,~Out,~caps,~select,~enter,~leave,~body,rest,args,cursor,tx)),select(Q.Frame{tx,handle,None{},cursor}))
90	def reserved_fields_inner(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~H: Type,~A: Data,~U: Data,~Out: Data,~caps:Ops(H),~select:Q.Frame<S,Store,R,E> -> Q.Frame<S,Store,R,E> & Bool,~enter:Q.Frame<S,Store,R,E> -> H,~leave:H -> Q.Frame<S,Store,R,E>,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & (T.Outcome<U> & Out),args: A,cursor:Maybe<&2,Tick.Tick>,observed: W.World<S,Store,R,E> & List<&2,W.Handle<S>>) -> Q.Executed<W.World<S,Store,R,E>,Q.Error<U>,Out>:
91	  (world,handles) = observed
92	  finished(~S,~Store,~R,~E,~U,~Out,run_handles_fields(~S,~Store,~R,~E,~Ops,~H,~A,~U,~Out,~caps,~select,~enter,~leave,~body,handles,args,cursor,T.begin(~W.World<S,Store,R,E>,~E,world)))
93	# Snapshot live handles in ascending order; deferred commands stay invisible.
94	def reserved_fields_scoped(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~H: Type,~A: Data,~U: Data,~Out: Data,~caps:Ops(H),~select:Q.Frame<S,Store,R,E> -> Q.Frame<S,Store,R,E> & Bool,~enter:Q.Frame<S,Store,R,E> -> H,~leave:H -> Q.Frame<S,Store,R,E>,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & (T.Outcome<U> & Out),args: A,cursor:Maybe<&2,Tick.Tick>,handles:List<&2,W.Handle<S>>,admitted:W.World<S,Store,R,E> & Bool) -> Q.Executed<W.World<S,Store,R,E>,Q.Error<U>,Out>:
95	  (world,owned)=admitted
96	  scope_finished(~S,~Store,~R,~E,~U,~Out,owned,reserved_fields_inner(~S,~Store,~R,~E,~Ops,~H,~A,~U,~Out,~caps,~select,~enter,~leave,~body,args,cursor,(world,handles)))
97	def reserved_fields(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~H: Type,~A: Data,~U: Data,~Out: Data,~caps:Ops(H),~select:Q.Frame<S,Store,R,E> -> Q.Frame<S,Store,R,E> & Bool,~enter:Q.Frame<S,Store,R,E> -> H,~leave:H -> Q.Frame<S,Store,R,E>,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & (T.Outcome<U> & Out),args: A,cursor:Maybe<&2,Tick.Tick>,observed: W.World<S,Store,R,E> & List<&2,W.Handle<S>>) -> Q.Executed<W.World<S,Store,R,E>,Q.Error<U>,Out>:
98	  (world,handles)=observed
99	  reserved_fields_scoped(~S,~Store,~R,~E,~Ops,~H,~A,~U,~Out,~caps,~select,~enter,~leave,~body,args,cursor,handles,W.ensure_run(~S,~Store,~R,~E,world))
100	
101	def each_fields(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~H: Type,~A: Data,~U: Data,~Out: Data,~caps:Ops(H),~select:Q.Frame<S,Store,R,E> -> Q.Frame<S,Store,R,E> & Bool,~enter:Q.Frame<S,Store,R,E> -> H,~leave:H -> Q.Frame<S,Store,R,E>,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & (T.Outcome<U> & Out),args: A,world: W.World<S,Store,R,E>) -> Q.Executed<W.World<S,Store,R,E>,Q.Error<U>,Out>:
102	  reserved_fields(~S,~Store,~R,~E,~Ops,~H,~A,~U,~Out,~caps,~select,~enter,~leave,~body,args,None{},W.handles(~S,~Store,~R,~E,world))
103	
104	
105	# Preserve explicit reader cursor in the accepted row frame.
106	def each_fields_since(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~H: Type,~A: Data,~U: Data,~Out: Data,~caps:Ops(H),~select:Q.Frame<S,Store,R,E> -> Q.Frame<S,Store,R,E> & Bool,~enter:Q.Frame<S,Store,R,E> -> H,~leave:H -> Q.Frame<S,Store,R,E>,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & (T.Outcome<U> & Out),args: A,world: W.World<S,Store,R,E>,cursor:Maybe<&2,Tick.Tick>) -> Q.Executed<W.World<S,Store,R,E>,Q.Error<U>,Out>:
107	  reserved_fields(~S,~Store,~R,~E,~Ops,~H,~A,~U,~Out,~caps,~select,~enter,~leave,~body,args,cursor,W.handles(~S,~Store,~R,~E,world))