owned_compose.bend
bendvy-ecs-core@0.1.0.1 · 107 lines · 0 definitions
1import Base
2import bendvy-ecs-core@0.1.0.1/change_tick.bend as Tick
3import world.bend as W
4import transaction.bend as T
5import commands.bend as Cmd
6import compose.bend as Q
7import capabilities.bend as Cap
8
9# Trusted declaration; gameplay can only thread universally quantified H.
10type 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
13def 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
17def 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
21def 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
25def 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
29def 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
33def 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))
37def 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},[]))
41def 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))
44def 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))))
48def 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}))
52def 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},[]}
56def 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))
59def 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}
62def 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.
66def 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)))
69def 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
73def 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.
78def 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.
82def 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))))
86def 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}))
90def 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.
94def 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)))
97def 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
101def 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.
106def 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))