1	import Base
2	import ./recovery_use.bend as Use
3	import ./world.bend as W
4	import ./owner_product.bend as Product
5	import ./ordinary_recovery_declaration.bend as D
6	import ./ordinary_recoverable_array_resource.bend as F
7	import ./ordinary_recoverable_component_capture.bend as Existing
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 World resource target and generated recovery path; no caller inverse.
14	# Nominal recoverable Array<P> resource capability family with whole-array
15	# replace and bounded element swap. P may be arbitrary affine Type; this does
16	# not provide automatic inverses for unrelated resource mutations.
17	def Ops(~S:Data,~P:Type,~identity:Schema.Resource<S,Array<P>>,H:Type) -> Type:F.Write<S,P,identity,H>
18	# Advanced trusted lens selecting the Array<P> World resource while
19	# retaining capture and the rest of World. No live owner is copied or exposed.
20	def target(~S:Data,~C:Type,~E:Data,~Capture:Type,~P:Type) -> Product.Lens<Product.Owner<W.World<S,C,Array<P>,E>,Capture>,Array<P>,Capture & WR.Rest<S,C,Array<P>,E>>:
21	  Product.compose(~Product.Owner<W.World<S,C,Array<P>,E>,Capture>,~W.World<S,C,Array<P>,E>,~Capture,~Array<P>,~WR.Rest<S,C,Array<P>,E>,~Product.lens(~W.World<S,C,Array<P>,E>,~Capture,~Product.Left{}),~WR.lens(~S,~C,~Array<P>,~E))
22	def empty(~Capture:Type,~P:Type,unit:Unit) -> List<A.Record<P>>:[]
23	def replaced(~S:Data,~C:Type,~E:Data,~Capture:Type,~P:Type,~All:Type,~Rest:Type,~path:Product.Lens<All,List<A.Record<P>>,Rest>,result:Product.Owner<W.World<S,C,Array<P>,E>,Capture> & List<Journal.Action(~Product.Owner<W.World<S,C,Array<P>,E>,Capture>,~All)>) -> F.Frame<Product.Owner<W.World<S,C,Array<P>,E>,Capture>,All>:
24	  match result:
25	    case (state,journal):F.Frame{state,journal}
26	# Replace the whole Array<P> resource in the shared recovery journal.
27	# Consumes incoming array and returns frame; commit recovers the displaced
28	# array, rollback restores it and recovers the replacement. Capture and other
29	# World owners remain siblings, not independent copies.
30	def replace(~S:Data,~C:Type,~E:Data,~Capture:Type,~P:Type,~All:Type,~Rest:Type,~path:Product.Lens<All,List<A.Record<P>>,Rest>,frame:F.Frame<Product.Owner<W.World<S,C,Array<P>,E>,Capture>,All>,incoming:Array<P>) -> F.Frame<Product.Owner<W.World<S,C,Array<P>,E>,Capture>,All>:
31	  match frame:
32	    case F.Frame{state,journal}:replaced(~S,~C,~E,~Capture,~P,~All,~Rest,~path,AO.replace(~Product.Owner<W.World<S,C,Array<P>,E>,Capture>,~P,~(Capture & WR.Rest<S,C,Array<P>,E>),~target(~S,~C,~E,~Capture,~P),~All,~Rest,~path,state,journal,incoming))
33	def swapped(~S:Data,~C:Type,~E:Data,~Capture:Type,~P:Type,~All:Type,~Rest:Type,~path:Product.Lens<All,List<A.Record<P>>,Rest>,result:AO.Attempt<Product.Owner<W.World<S,C,Array<P>,E>,Capture>,All,P>) -> F.Attempt<F.Frame<Product.Owner<W.World<S,C,Array<P>,E>,Capture>,All>,P>:
34	  match result:
35	    case AO.Applied{state,journal}:F.Applied{F.Frame{state,journal}}
36	    case AO.Refused{state,journal,incoming}:F.Refused{F.Frame{state,journal},incoming}
37	# Attempt one Array<P> resource element swap. Out-of-bounds returns Refused
38	# with incoming P and unchanged journal; success records the displaced owner.
39	# Receipt recovery follows the enclosing commit/rollback, not immediate copying.
40	def swap(~S:Data,~C:Type,~E:Data,~Capture:Type,~P:Type,~All:Type,~Rest:Type,~path:Product.Lens<All,List<A.Record<P>>,Rest>,frame:F.Frame<Product.Owner<W.World<S,C,Array<P>,E>,Capture>,All>,index:U32,incoming:P) -> F.Attempt<F.Frame<Product.Owner<W.World<S,C,Array<P>,E>,Capture>,All>,P>:
41	  match frame:
42	    case F.Frame{state,journal}:swapped(~S,~C,~E,~Capture,~P,~All,~Rest,~path,AO.swap(~Product.Owner<W.World<S,C,Array<P>,E>,Capture>,~P,~(Capture & WR.Rest<S,C,Array<P>,E>),~target(~S,~C,~E,~Capture,~P),~All,~Rest,~path,state,journal,index,incoming))
43	# Advanced closed grant builder for canonical resource and recovery paths.
44	# Gameplay receives typed replace/swap; it does not author inverses or journals.
45	def grant(~S:Data,~C:Type,~E:Data,~Capture:Type,~P:Type,~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,Array<P>,E>,Capture>,All>>:
46	  F.Write{replace(~S,~C,~E,~Capture,~P,~All,~Rest,~path),swap(~S,~C,~E,~Capture,~P,~All,~Rest,~path)}
47	# Declare recoverable Array<P> resource operations using its ordinary
48	# resource identity. Supplies complete access/use metadata and generated
49	# recovery path; performs no resource mutation or allocation of payload values.
50	# Supported domain and receipts: docs/parity/recovery.md.
51	def declaration(~S:Data,~C:Type,~E:Data,~Capture:Type,~P:Type,~identity:Schema.Resource<S,Array<P>>) -> D.Declaration<S,Product.Owner<W.World<S,C,Array<P>,E>,Capture>,List<A.Record<P>>,Ops(~S,~P,~identity),grant(~S,~C,~E,~Capture,~P,~identity)>:
52	  D.Described{empty(~Capture,~P),[Schema.resource_key(~S,~Array<P>,identity)],Use.known([Use.Use{Use.Resource{Schema.resource_key(~S,~Array<P>,identity)},Use.Write{}}])}