1	import Base
2	import ./recovery_use.bend as Use
3	import ./resource_field_binding.bend as Binding
4	import ./world.bend as W
5	import ./owner_product.bend as Product
6	import ./ordinary_recovery_declaration.bend as D
7	import ./ordinary_recoverable_array_resource.bend as F
8	import ./recoverable_array.bend as A
9	import ./recoverable_array_owner.bend as AO
10	import ./recovery_journal.bend as Journal
11	import ./world_resource_owner.bend as WR
12	import ./ordinary_schema.bend as Schema
13	# Canonical selected resource field with generated recovery path; no caller inverse.
14	# Binding supplies the same identity/path pair as ordinary resource-field grants.
15	# Advanced capability-shape projection for identity-indexed recoverable Array<P>
16	# replacement and checked element swap, with opaque execution owner H.
17	def Ops(~S:Data,~P:Type,~identity:Schema.Resource<S,Array<P>>,H:Type) -> Type:F.Write<S,P,identity,H>
18	# Trusted recovery lens into World resources while threading actual capture and
19	# all other World fields. This is setup plumbing, not a gameplay World accessor.
20	def resource_target(~S:Data,~C:Type,~R:Type,~E:Data,~Capture:Type) -> Product.Lens<Product.Owner<W.World<S,C,R,E>,Capture>,R,Capture & WR.Rest<S,C,R,E>>:
21	  Product.compose(~Product.Owner<W.World<S,C,R,E>,Capture>,~W.World<S,C,R,E>,~Capture,~R,~WR.Rest<S,C,R,E>,~Product.lens(~W.World<S,C,R,E>,~Capture,~Product.Left{}),~WR.lens(~S,~C,~R,~E))
22	# Trusted composition of World-resource and selected Array-field lenses.
23	# Canonical binding supplies the identity/path pair; siblings/capture stay owned.
24	def target(~S:Data,~C:Type,~E:Data,~Capture:Type,~R:Type,~P:Type,~FieldRest:Type,~fieldLens:Product.Lens<R,Array<P>,FieldRest>) -> Product.Lens<Product.Owner<W.World<S,C,R,E>,Capture>,Array<P>,(Capture & WR.Rest<S,C,R,E>) & FieldRest>:
25	  Product.compose(~Product.Owner<W.World<S,C,R,E>,Capture>,~R,~(Capture & WR.Rest<S,C,R,E>),~Array<P>,~FieldRest,~resource_target(~S,~C,~R,~E,~Capture),~fieldLens)
26	def empty(~Capture:Type,~R:Type,~P:Type,~FieldRest:Type,~fieldLens:Product.Lens<R,Array<P>,FieldRest>,unit:Unit) -> List<A.Record<P>>:[]
27	def replaced(~S:Data,~C:Type,~E:Data,~Capture:Type,~R:Type,~P:Type,~FieldRest:Type,~fieldLens:Product.Lens<R,Array<P>,FieldRest>,~All:Type,~Rest:Type,~path:Product.Lens<All,List<A.Record<P>>,Rest>,result:Product.Owner<W.World<S,C,R,E>,Capture> & List<Journal.Action(~Product.Owner<W.World<S,C,R,E>,Capture>,~All)>) -> F.Frame<Product.Owner<W.World<S,C,R,E>,Capture>,All>:
28	  match result:
29	    case (state,journal):F.Frame{state,journal}
30	# Advanced recoverable replacement: consume incoming Array<P>, install it in
31	# the selected field and journal the displaced array in the shared recovery path.
32	# Commit returns displaced owners; rollback restores originals and returns displaced
33	# replacements through the declaration recovery result, not a duplicate live owner.
34	def replace(~S:Data,~C:Type,~E:Data,~Capture:Type,~R:Type,~P:Type,~FieldRest:Type,~fieldLens:Product.Lens<R,Array<P>,FieldRest>,~All:Type,~Rest:Type,~path:Product.Lens<All,List<A.Record<P>>,Rest>,frame:F.Frame<Product.Owner<W.World<S,C,R,E>,Capture>,All>,incoming:Array<P>) -> F.Frame<Product.Owner<W.World<S,C,R,E>,Capture>,All>:
35	  match frame:
36	    case F.Frame{state,journal}:replaced(~S,~C,~E,~Capture,~R,~P,~FieldRest,~fieldLens,~All,~Rest,~path,AO.replace(~Product.Owner<W.World<S,C,R,E>,Capture>,~P,~((Capture & WR.Rest<S,C,R,E>) & FieldRest),~target(~S,~C,~E,~Capture,~R,~P,~FieldRest,~fieldLens),~All,~Rest,~path,state,journal,incoming))
37	def swapped(~S:Data,~C:Type,~E:Data,~Capture:Type,~R:Type,~P:Type,~FieldRest:Type,~fieldLens:Product.Lens<R,Array<P>,FieldRest>,~All:Type,~Rest:Type,~path:Product.Lens<All,List<A.Record<P>>,Rest>,result:AO.Attempt<Product.Owner<W.World<S,C,R,E>,Capture>,All,P>) -> F.Attempt<F.Frame<Product.Owner<W.World<S,C,R,E>,Capture>,All>,P>:
38	  match result:
39	    case AO.Applied{state,journal}:F.Applied{F.Frame{state,journal}}
40	    case AO.Refused{state,journal,incoming}:F.Refused{F.Frame{state,journal},incoming}
41	# Advanced bounds-checked element replacement consuming P. Applied journals old P;
42	# Refused returns actual incoming P with state/journal preserved when index is out
43	# of bounds. Recovery follows shared journal order; unlike raw Array access this
44	# does not wrap an invalid index into another slot.
45	def swap(~S:Data,~C:Type,~E:Data,~Capture:Type,~R:Type,~P:Type,~FieldRest:Type,~fieldLens:Product.Lens<R,Array<P>,FieldRest>,~All:Type,~Rest:Type,~path:Product.Lens<All,List<A.Record<P>>,Rest>,frame:F.Frame<Product.Owner<W.World<S,C,R,E>,Capture>,All>,index:U32,incoming:P) -> F.Attempt<F.Frame<Product.Owner<W.World<S,C,R,E>,Capture>,All>,P>:
46	  match frame:
47	    case F.Frame{state,journal}:swapped(~S,~C,~E,~Capture,~R,~P,~FieldRest,~fieldLens,~All,~Rest,~path,AO.swap(~Product.Owner<W.World<S,C,R,E>,Capture>,~P,~((Capture & WR.Rest<S,C,R,E>) & FieldRest),~target(~S,~C,~E,~Capture,~R,~P,~FieldRest,~fieldLens),~All,~Rest,~path,state,journal,index,incoming))
48	# Advanced canonical grant builder hiding resource lens and journal plumbing
49	# behind the identity-indexed recoverable write operations. Does not execute them.
50	def grant(~S:Data,~C:Type,~E:Data,~Capture:Type,~R:Type,~P:Type,~FieldRest:Type,~fieldLens:Product.Lens<R,Array<P>,FieldRest>,~identity:Schema.Resource<S,Array<P>>,~All:Type,~Rest:Type,~path:Product.Lens<All,List<A.Record<P>>,Rest>,unit:Unit) -> F.Write<S,P,identity,F.Frame<Product.Owner<W.World<S,C,R,E>,Capture>,All>>:
51	  F.Write{replace(~S,~C,~E,~Capture,~R,~P,~FieldRest,~fieldLens,~All,~Rest,~path),swap(~S,~C,~E,~Capture,~R,~P,~FieldRest,~fieldLens,~All,~Rest,~path)}
52	# Derive the recoverable selected Array resource declaration from its canonical
53	# Binding. Initializes empty recovery records and publishes known Write-use metadata
54	# for this resource key. Shared recovery composition controls finish/undo order;
55	# there is no caller-authored inverse or automatic external-effect rollback.
56	# See docs/parity/recovery.md for explicit owned recovery boundaries.
57	def declaration(~S:Data,~C:Type,~E:Data,~Capture:Type,~R:Type,~P:Type,~FieldRest:Type,~fieldLens:Product.Lens<R,Array<P>,FieldRest>,~identity:Schema.Resource<S,Array<P>>,~binding:Binding.Binding<S,R,Array<P>,FieldRest,fieldLens,identity>) -> D.Declaration<S,Product.Owner<W.World<S,C,R,E>,Capture>,List<A.Record<P>>,Ops(~S,~P,~identity),grant(~S,~C,~E,~Capture,~R,~P,~FieldRest,~fieldLens,~identity)>:
58	  D.Described{empty(~Capture,~R,~P,~FieldRest,~fieldLens),[Schema.resource_key(~S,~Array<P>,identity)],Use.known([Use.Use{Use.Resource{Schema.resource_key(~S,~Array<P>,identity)},Use.Write{}}])}