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	# Canonical capture target and generated recovery path; no caller inverse.
12	# Recoverable retained Array<Q> capture capability family: whole-array
13	# replace and bounded element swap. Q may be affine Type; arbitrary capture
14	# mutation outside these declared operations is not automatically reversible.
15	def Ops(~Q:Type,H:Type) -> Type:Existing.CaptureWrite<Q,H>
16	def empty(~Q:Type,unit:Unit) -> List<A.Record<Q>>:[]
17	def replaced(~S:Data,~C:Type,~R:Type,~E:Data,~Q:Type,~All:Type,~Rest:Type,~path:Product.Lens<All,List<A.Record<Q>>,Rest>,result:Product.Owner<W.World<S,C,R,E>,Array<Q>> & List<Journal.Action(~Product.Owner<W.World<S,C,R,E>,Array<Q>>,~All)>) -> F.Frame<Product.Owner<W.World<S,C,R,E>,Array<Q>>,All>:
18	  match result:
19	    case (state,journal):F.Frame{state,journal}
20	# Replace retained Array<Q> capture, recording its displaced owner in the
21	# shared recovery journal. Commit returns the displaced array; rollback
22	# restores it and returns the replacement through the recovery accumulator.
23	# World remains the retained sibling of capture.
24	def replace(~S:Data,~C:Type,~R:Type,~E:Data,~Q:Type,~All:Type,~Rest:Type,~path:Product.Lens<All,List<A.Record<Q>>,Rest>,frame:F.Frame<Product.Owner<W.World<S,C,R,E>,Array<Q>>,All>,incoming:Array<Q>) -> F.Frame<Product.Owner<W.World<S,C,R,E>,Array<Q>>,All>:
25	  match frame:
26	    case F.Frame{state,journal}:replaced(~S,~C,~R,~E,~Q,~All,~Rest,~path,AO.replace(~Product.Owner<W.World<S,C,R,E>,Array<Q>>,~Q,~W.World<S,C,R,E>,~Product.lens(~W.World<S,C,R,E>,~Array<Q>,~Product.Right{}),~All,~Rest,~path,state,journal,incoming))
27	def swapped(~S:Data,~C:Type,~R:Type,~E:Data,~Q:Type,~All:Type,~Rest:Type,~path:Product.Lens<All,List<A.Record<Q>>,Rest>,result:AO.Attempt<Product.Owner<W.World<S,C,R,E>,Array<Q>>,All,Q>) -> F.Attempt<F.Frame<Product.Owner<W.World<S,C,R,E>,Array<Q>>,All>,Q>:
28	  match result:
29	    case AO.Applied{state,journal}:F.Applied{F.Frame{state,journal}}
30	    case AO.Refused{state,journal,incoming}:F.Refused{F.Frame{state,journal},incoming}
31	# Attempt a bounded capture element replacement. Refused retains frame and
32	# incoming Q without extending the journal; accepted records the old element
33	# for commit/rollback recovery. Does not copy either affine element.
34	def swap(~S:Data,~C:Type,~R:Type,~E:Data,~Q:Type,~All:Type,~Rest:Type,~path:Product.Lens<All,List<A.Record<Q>>,Rest>,frame:F.Frame<Product.Owner<W.World<S,C,R,E>,Array<Q>>,All>,index:U32,incoming:Q) -> F.Attempt<F.Frame<Product.Owner<W.World<S,C,R,E>,Array<Q>>,All>,Q>:
35	  match frame:
36	    case F.Frame{state,journal}:swapped(~S,~C,~R,~E,~Q,~All,~Rest,~path,AO.swap(~Product.Owner<W.World<S,C,R,E>,Array<Q>>,~Q,~W.World<S,C,R,E>,~Product.lens(~W.World<S,C,R,E>,~Array<Q>,~Product.Right{}),~All,~Rest,~path,state,journal,index,incoming))
37	# Advanced canonical builder selecting the capture and generated recovery
38	# path inside the complete product. Raw indices are trusted setup; the body
39	# sees only its closed replace/swap operations.
40	def grant(~S:Data,~C:Type,~R:Type,~E:Data,~Q:Type,~All:Type,~Rest:Type,~path:Product.Lens<All,List<A.Record<Q>>,Rest>,unit:Unit) -> Existing.CaptureWrite<Q,F.Frame<Product.Owner<W.World<S,C,R,E>,Array<Q>>,All>>:Existing.CaptureWrite{replace(~S,~C,~R,~E,~Q,~All,~Rest,~path),swap(~S,~C,~R,~E,~Q,~All,~Rest,~path)}
41	# Declare canonical Array<Q> capture recovery with complete typed Capture
42	# use metadata and no fabricated World access key. Compose with component/
43	# resource declarations through ordinary-recovery-declaration.both. Does not
44	# execute a body or make host IO reversible; see docs/parity/recovery.md.
45	def declaration(~S:Data,~C:Type,~R:Type,~E:Data,~Q:Type) -> D.Declaration<S,Product.Owner<W.World<S,C,R,E>,Array<Q>>,List<A.Record<Q>>,Ops(~Q),grant(~S,~C,~R,~E,~Q)>:D.Described{empty(~Q),[],Use.known([Use.Use{Use.Capture{},Use.Write{}}])}