captured_column.bend
bendvy-ecs-core@0.1.0.0 · 109 lines · 0 definitions
1import Base
2import column.bend as Col
3import owner_handoff.bend as H
4import lifecycle.bend as L
5import indexed_lifecycle.bend as M
6
7# Provisioning captures a restoration closure only after accepted extraction.
8# Gameplay never receives its captured column/index or a replacement restore target.
9type Slot<-C:Type> is Type:
10 Slot{owner:Maybe<&1,C>,stamp:L.Stamp,dirty:Bool}
11type Capture<-S:Data,-C:Type> is Type:
12 Captured{id:U32,owner:Maybe<&1,C>,stamp:L.Stamp,restore:Slot<C> -> Col.Column<S,C>}
13 Unavailable{column:Col.Column<S,C>}
14
15def stamped(~S:Data,~C:Type,+id:U32,column:Col.Column<S,C>,stamp:L.Stamp,dirty:Bool) -> Col.Column<S,C>:
16 match dirty:
17 case False{}: column
18 case True{}: Col.restore_stamp(~S,~C,column,id,stamp)
19def restore_plain(~S:Data,~C:Type,+id:U32,values:Array<Maybe<&1,C>>,stamps:List<&2,L.Entry>,slot:Slot<C>) -> Col.Column<S,C>:
20 match slot:
21 case Slot{owner,stamp,dirty}: stamped(~S,~C,id,Col.Column{Array.set(Maybe<&1,C>,values,U32.sub(id,1),owner),stamps},stamp,dirty)
22def indexed_restore_plain(~S:Data,~C:Type,+id:U32,values:Array<Maybe<&1,C>>,metadata:M.Metadata,slot:Slot<C>) -> Col.Column<S,C>:
23 match slot:
24 case Slot{owner,stamp,dirty}: stamped(~S,~C,id,Col.indexed_wrap(~S,~C,Array.set(Maybe<&1,C>,values,U32.sub(id,1),owner),metadata),stamp,dirty)
25def indexed_plain_got(~S:Data,~C:Type,+id:U32,values:Array<Maybe<&1,C>>,owner:Maybe<&1,C>,result:M.Metadata & L.Stamp) -> Capture<S,C>:
26 match result:
27 case (metadata,stamp): Captured{id,owner,stamp,slot => indexed_restore_plain(~S,~C,id,values,metadata,slot)}
28def indexed_plain_taken(~S:Data,~C:Type,+id:U32,metadata:M.Metadata,result:Array<Maybe<&1,C>> & Maybe<&1,C>) -> Capture<S,C>:
29 match result:
30 case (values,owner): indexed_plain_got(~S,~C,id,values,owner,M.get(metadata,id))
31def indexed_plain_checked(~S:Data,~C:Type,+id:U32,metadata:M.Metadata,values:Array<Maybe<&1,C>>,valid:Bool) -> Capture<S,C>:
32 match valid:
33 case False{}: Unavailable{Col.indexed_wrap(~S,~C,values,metadata)}
34 case True{}: indexed_plain_taken(~S,~C,id,metadata,Array.swap(Maybe<&1,C>,values,U32.sub(id,1),None{}))
35def indexed_plain_sized(~S:Data,~C:Type,+id:U32,metadata:M.Metadata,sized:Array<Maybe<&1,C>> & U32) -> Capture<S,C>:
36 match sized:
37 case (values,size): indexed_plain_checked(~S,~C,id,metadata,values,U32.is_gt(id,0) && U32.is_le(id,size) && U32.is_le(id,131072))
38def indexed_plain_state(~S:Data,~C:Type,+id:U32,state:Col.IndexedOrdinaryState<S,C>) -> Capture<S,C>:
39 match state:
40 case Col.IndexedOrdinaryState{values,metadata}: indexed_plain_sized(~S,~C,id,metadata,Array.size(Maybe<&1,C>,values))
41def restore_prepared(~S:Data,~C:Type,+id:U32,values:Array<Maybe<&1,C>>,stamps:List<&2,L.Entry>,capacity:U32,remaining:H.PrototypeHandoffRows<S,C>,past:Col.History<S,C>,slot:Slot<C>) -> Col.Column<S,C>:
42 match slot:
43 case Slot{owner,stamp,dirty}: stamped(~S,~C,id,Col.Prepared{Col.Owned{Col.State{values,stamps,capacity,id,owner,remaining,past}}},stamp,dirty)
44def indexed_restore_prepared(~S:Data,~C:Type,+id:U32,values:Array<Maybe<&1,C>>,metadata:M.Metadata,capacity:U32,remaining:H.PrototypeHandoffRows<S,C>,past:Col.History<S,C>,slot:Slot<C>) -> Col.Column<S,C>:
45 match slot:
46 case Slot{owner,stamp,dirty}: stamped(~S,~C,id,Col.PreparedIndexed{Col.IndexedPreparedOwned{Col.IndexedPreparedState{values,metadata,capacity,id,owner,remaining,past}}},stamp,dirty)
47def captured_prepared(~S:Data,~C:Type,+id:U32,values:Array<Maybe<&1,C>>,+stamps:List<&2,L.Entry>,capacity:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:Col.History<S,C>) -> Capture<S,C>:
48 Captured{id,owner,L.get(stamps,id),slot => restore_prepared(~S,~C,id,values,stamps,capacity,remaining,past,slot)}
49# Exact constant-None specialization of Col.seek: phase and fuel remain observable.
50def indexed_captured_got(~S:Data,~C:Type,+id:U32,values:Array<Maybe<&1,C>>,capacity:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:Col.History<S,C>,result:M.Metadata & L.Stamp) -> Capture<S,C>:
51 match result:
52 case (metadata,stamp): Captured{id,owner,stamp,slot => indexed_restore_prepared(~S,~C,id,values,metadata,capacity,remaining,past,slot)}
53def indexed_captured_prepared(~S:Data,~C:Type,+id:U32,values:Array<Maybe<&1,C>>,metadata:M.Metadata,capacity:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:Col.History<S,C>) -> Capture<S,C>:
54 indexed_captured_got(~S,~C,id,values,capacity,owner,remaining,past,M.get(metadata,id))
55def capture_seek(~S:Data,~C:Type,fuel:Nat,values:Array<Maybe<&1,C>>,stamps:List<&2,L.Entry>,capacity:U32,+target:U32,remaining:H.PrototypeHandoffRows<S,C>,past:Col.History<S,C>,phase:Col.SeekPhase) -> Capture<S,C>:
56 match fuel remaining phase:
57 case _ H.HandoffNil{} _: captured_prepared(~S,~C,target,values,stamps,capacity,None{},H.HandoffNil{},past)
58 case 0n H.HandoffCon{id,owner,rest} _: Unavailable{Col.Prepared{Col.Owned{Col.State{values,stamps,capacity,0,None{},H.HandoffCon{id,owner,rest},past}}}}
59 case 1n+more H.HandoffCon{+id,owner,rest} Col.Inspect{}: capture_seek(~S,~C,more,values,stamps,capacity,target,H.HandoffCon{id,owner,rest},past,Col.Choice{U32.is_eq(target,id),U32.is_lt(target,id)})
60 case 1n+more H.HandoffCon{id,owner,rest} Col.Choice{True{},_}: captured_prepared(~S,~C,target,values,stamps,capacity,Some{owner},rest,past)
61 case 1n+more H.HandoffCon{id,owner,rest} Col.Choice{False{},True{}}: captured_prepared(~S,~C,target,values,stamps,capacity,None{},H.HandoffCon{id,owner,rest},past)
62 case 1n+more H.HandoffCon{id,owner,rest} Col.Choice{False{},False{}}: capture_seek(~S,~C,more,values,stamps,capacity,target,rest,Col.HistoryCon{id,Some{owner},past},Col.Inspect{})
63def indexed_capture_seek(~S:Data,~C:Type,fuel:Nat,values:Array<Maybe<&1,C>>,metadata:M.Metadata,capacity:U32,+target:U32,remaining:H.PrototypeHandoffRows<S,C>,past:Col.History<S,C>,phase:Col.SeekPhase) -> Capture<S,C>:
64 match fuel remaining phase:
65 case _ H.HandoffNil{} _: indexed_captured_prepared(~S,~C,target,values,metadata,capacity,None{},H.HandoffNil{},past)
66 case 0n H.HandoffCon{id,owner,rest} _: Unavailable{Col.PreparedIndexed{Col.IndexedPreparedOwned{Col.IndexedPreparedState{values,metadata,capacity,0,None{},H.HandoffCon{id,owner,rest},past}}}}
67 case 1n+more H.HandoffCon{+id,owner,rest} Col.Inspect{}: indexed_capture_seek(~S,~C,more,values,metadata,capacity,target,H.HandoffCon{id,owner,rest},past,Col.Choice{U32.is_eq(target,id),U32.is_lt(target,id)})
68 case 1n+more H.HandoffCon{id,owner,rest} Col.Choice{True{},_}: indexed_captured_prepared(~S,~C,target,values,metadata,capacity,Some{owner},rest,past)
69 case 1n+more H.HandoffCon{id,owner,rest} Col.Choice{False{},True{}}: indexed_captured_prepared(~S,~C,target,values,metadata,capacity,None{},H.HandoffCon{id,owner,rest},past)
70 case 1n+more H.HandoffCon{id,owner,rest} Col.Choice{False{},False{}}: indexed_capture_seek(~S,~C,more,values,metadata,capacity,target,rest,Col.HistoryCon{id,Some{owner},past},Col.Inspect{})
71def plain_taken(~S:Data,~C:Type,+id:U32,+stamps:List<&2,L.Entry>,result:Array<Maybe<&1,C>> & Maybe<&1,C>) -> Capture<S,C>:
72 match result:
73 case (values,owner): Captured{id,owner,L.get(stamps,id),slot => restore_plain(~S,~C,id,values,stamps,slot)}
74def plain_checked(~S:Data,~C:Type,+id:U32,stamps:List<&2,L.Entry>,values:Array<Maybe<&1,C>>,valid:Bool) -> Capture<S,C>:
75 match valid:
76 case False{}: Unavailable{Col.Column{values,stamps}}
77 case True{}: plain_taken(~S,~C,id,stamps,Array.swap(Maybe<&1,C>,values,U32.sub(id,1),None{}))
78def plain_sized(~S:Data,~C:Type,+id:U32,stamps:List<&2,L.Entry>,sized:Array<Maybe<&1,C>> & U32) -> Capture<S,C>:
79 match sized:
80 case (values,size): plain_checked(~S,~C,id,stamps,values,U32.is_gt(id,0) && U32.is_le(id,size) && U32.is_le(id,131072))
81def recovered_capture(~S:Data,~C:Type,+id:U32,column:Col.Column<S,C>) -> Capture<S,C>:
82 match column:
83 case Col.Column{values,stamps}: plain_sized(~S,~C,id,stamps,Array.size(Maybe<&1,C>,values))
84 case Col.Indexed{carrier}: indexed_plain_state(~S,~C,id,Col.indexed_unseal(~S,~C,carrier))
85 case other: Unavailable{other}
86def prepared_checked(~S:Data,~C:Type,+id:U32,values:Array<Maybe<&1,C>>,stamps:List<&2,L.Entry>,+capacity:U32,+current:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:Col.History<S,C>,valid:Bool,same:Bool,backwards:Bool) -> Capture<S,C>:
87 match valid same backwards:
88 case False{} _ _: Unavailable{Col.Prepared{Col.Owned{Col.State{values,stamps,capacity,current,owner,remaining,past}}}}
89 case True{} True{} _: captured_prepared(~S,~C,id,values,stamps,capacity,owner,remaining,past)
90 case True{} False{} True{}: recovered_capture(~S,~C,id,Col.recover(~S,~C,Col.Prepared{Col.Owned{Col.State{values,stamps,capacity,current,owner,remaining,past}}}))
91 case True{} False{} False{}: capture_seek(~S,~C,U32.to_nat(U32.add(U32.add(capacity,capacity),1)),values,stamps,capacity,id,remaining,Col.past_current(~S,~C,current,owner,past,U32.is_gt(current,0)),Col.Inspect{})
92def indexed_prepared_checked(~S:Data,~C:Type,+id:U32,values:Array<Maybe<&1,C>>,metadata:M.Metadata,+capacity:U32,+current:U32,owner:Maybe<&1,C>,remaining:H.PrototypeHandoffRows<S,C>,past:Col.History<S,C>,valid:Bool,same:Bool,backwards:Bool) -> Capture<S,C>:
93 match valid same backwards:
94 case False{} _ _: Unavailable{Col.PreparedIndexed{Col.IndexedPreparedOwned{Col.IndexedPreparedState{values,metadata,capacity,current,owner,remaining,past}}}}
95 case True{} True{} _: indexed_captured_prepared(~S,~C,id,values,metadata,capacity,owner,remaining,past)
96 case True{} False{} True{}: recovered_capture(~S,~C,id,Col.recover(~S,~C,Col.PreparedIndexed{Col.IndexedPreparedOwned{Col.IndexedPreparedState{values,metadata,capacity,current,owner,remaining,past}}}))
97 case True{} False{} False{}: indexed_capture_seek(~S,~C,U32.to_nat(U32.add(U32.add(capacity,capacity),1)),values,metadata,capacity,id,remaining,Col.past_current(~S,~C,current,owner,past,U32.is_gt(current,0)),Col.Inspect{})
98def prepared_state(~S:Data,~C:Type,+id:U32,state:Col.State<S,C>) -> Capture<S,C>:
99 match state:
100 case Col.State{values,stamps,+capacity,+current,owner,remaining,past}: prepared_checked(~S,~C,id,values,stamps,capacity,current,owner,remaining,past,U32.is_gt(id,0) && U32.is_le(id,capacity),U32.is_eq(id,current),U32.is_lt(id,current))
101def indexed_prepared_state(~S:Data,~C:Type,+id:U32,state:Col.IndexedPreparedState<S,C>) -> Capture<S,C>:
102 match state:
103 case Col.IndexedPreparedState{values,metadata,+capacity,+current,owner,remaining,past}: indexed_prepared_checked(~S,~C,id,values,metadata,capacity,current,owner,remaining,past,U32.is_gt(id,0) && U32.is_le(id,capacity),U32.is_eq(id,current),U32.is_lt(id,current))
104def capture(~S:Data,~C:Type,column:Col.Column<S,C>,+id:U32) -> Capture<S,C>:
105 match column:
106 case Col.Column{values,stamps}: plain_sized(~S,~C,id,stamps,Array.size(Maybe<&1,C>,values))
107 case Col.Prepared{carrier}: prepared_state(~S,~C,id,Col.unseal(~S,~C,carrier))
108 case Col.Indexed{carrier}: indexed_plain_state(~S,~C,id,Col.indexed_unseal(~S,~C,carrier))
109 case Col.PreparedIndexed{carrier}: indexed_prepared_state(~S,~C,id,Col.indexed_prepared_unseal(~S,~C,carrier))