1 import Base 2 import ./recovery_use.bend as Use 3 import ./world.bend as W 4 import ./column.bend as Col 5 import ./owner_product.bend as Product 6 import ./ordinary_component_binding.bend as B 7 import ./ordinary_declaration.bend as Identity 8 import ./ordinary_recovery_declaration.bend as D 9 import ./ordinary_recoverable_array_resource.bend as F 10 import ./ordinary_recoverable_component_capture.bend as Existing 11 import ./recoverable_component.bend as RC 12 import ./recoverable_component_family.bend as Family 13 import ./recoverable_owner.bend as RO 14 import ./recovery_journal.bend as Journal 15 # Existing schema take/put/view are trusted provisioning, never gameplay inverses. 16 # Nominal recoverable component replacement capability family. P may be 17 # affine Type; the grant is bound to its ordinary component identity, not a 18 # printable access name or a caller-provided inverse. 19 def Ops(~S:Data,~P:Type,~identity:Identity.Declaration,H:Type) -> Type:Existing.ComponentWrite 20 def empty(~S:Data,~P:Type,unit:Unit) -> List>:[] 21 def released(~S:Data,~C:Type,~R:Type,~E:Data,~Capture:Type,~Rest:Type,~P:Type,~V:Data,~Token:Data,~take:C -> Rest & Col.Column,~put:Rest -> Col.Column -> C,~view:P -> P & V,~binding:B.Binding,~All:Type,~ReleasedRest:Type,~path:Product.Lens>,ReleasedRest>,capture:Capture,recovery:All,result:W.World & RC.Record) -> Product.Owner,Capture> & All: 22 match result: 23 case (world,record):(Product.Owner{world,capture},RO.append(~All,~RC.Record,~ReleasedRest,~path,recovery,record)) 24 def inverse(~S:Data,~C:Type,~R:Type,~E:Data,~Capture:Type,~Rest:Type,~P:Type,~V:Data,~Token:Data,~take:C -> Rest & Col.Column,~put:Rest -> Col.Column -> C,~view:P -> P & V,~binding:B.Binding,~All:Type,~ReleasedRest:Type,~path:Product.Lens>,ReleasedRest>,old:RC.Record,success:Bool,state:Product.Owner,Capture>,recovery:All) -> Product.Owner,Capture> & All: 25 match success state: 26 case True{} state:(state,RO.append(~All,~RC.Record,~ReleasedRest,~path,recovery,old)) 27 case False{} Product.Owner{world,capture}:released(~S,~C,~R,~E,~Capture,~Rest,~P,~V,~Token,~take,~put,~view,~binding,~All,~ReleasedRest,~path,capture,recovery,Family.undo(~S,~C,~R,~E,~Rest,~P,~V,~Token,~take,~put,~view,~B.family(~S,~C,~Rest,~P,~V,~Token,~take,~put,~view,binding),old,world)) 28 def replaced(~S:Data,~C:Type,~R:Type,~E:Data,~Capture:Type,~Rest:Type,~P:Type,~V:Data,~Token:Data,~take:C -> Rest & Col.Column,~put:Rest -> Col.Column -> C,~view:P -> P & V,~binding:B.Binding,~All:Type,~ReleasedRest:Type,~path:Product.Lens>,ReleasedRest>,capture:Capture,journal:List,Capture>,~All)>,result:RC.Replacement,S,P>) -> Existing.ComponentAttempt,Capture>,All>,P>: 29 match result: 30 case RC.Applied{world,old}:Existing.ComponentApplied{F.Frame{Product.Owner{world,capture},(success => state => recovery => inverse(~S,~C,~R,~E,~Capture,~Rest,~P,~V,~Token,~take,~put,~view,~binding,~All,~ReleasedRest,~path,old,success,state,recovery)) <> journal}} 31 case RC.Refused{world,incoming,error}:Existing.ComponentRefused{F.Frame{Product.Owner{world,capture},journal},incoming,error} 32 # Replace an optional component owner through the canonical binding. 33 # Immediate refusal returns frame, incoming owner and error without adding 34 # an inverse. Accepted records the displaced component receipt; commit returns 35 # displaced owners, while rollback restores recorded state and recovers 36 # replacements. Other World/capture owners are retained through the frame. 37 def replace(~S:Data,~C:Type,~R:Type,~E:Data,~Capture:Type,~Rest:Type,~P:Type,~V:Data,~Token:Data,~take:C -> Rest & Col.Column,~put:Rest -> Col.Column -> C,~view:P -> P & V,~binding:B.Binding,~All:Type,~ReleasedRest:Type,~path:Product.Lens>,ReleasedRest>,frame:F.Frame,Capture>,All>,handle:W.Handle,incoming:Maybe

) -> Existing.ComponentAttempt,Capture>,All>,P>: 38 match frame: 39 case F.Frame{Product.Owner{world,capture},journal}:replaced(~S,~C,~R,~E,~Capture,~Rest,~P,~V,~Token,~take,~put,~view,~binding,~All,~ReleasedRest,~path,capture,journal,Family.replace(~S,~C,~R,~E,~Rest,~P,~V,~Token,~take,~put,~view,B.family(~S,~C,~Rest,~P,~V,~Token,~take,~put,~view,binding),world,handle,incoming)) 40 # Advanced canonical grant builder specialized at the complete recovery 41 # product/path. Raw erased lenses must match the declaration; gameplay 42 # receives the resulting nominal component operation, not journal callbacks. 43 def grant(~S:Data,~C:Type,~R:Type,~E:Data,~Capture:Type,~Rest:Type,~P:Type,~V:Data,~Token:Data,~take:C -> Rest & Col.Column,~put:Rest -> Col.Column -> C,~view:P -> P & V,~binding:B.Binding,~All:Type,~ReleasedRest:Type,~path:Product.Lens>,ReleasedRest>,unit:Unit) -> Existing.ComponentWrite,Capture>,All>>:Existing.ComponentWrite{replace(~S,~C,~R,~E,~Capture,~Rest,~P,~V,~Token,~take,~put,~view,~binding,~All,~ReleasedRest,~path)} 44 # Build a complete typed component-recovery declaration from its ordinary 45 # binding. Derives access/use metadata and the canonical recovery accumulator 46 # without executing an operation. Compose with other leaves using 47 # ordinary-recovery-declaration.both; semantics: docs/parity/recovery.md. 48 def declaration(~S:Data,~C:Type,~R:Type,~E:Data,~Capture:Type,~Rest:Type,~P:Type,~V:Data,~Token:Data,~take:C -> Rest & Col.Column,~put:Rest -> Col.Column -> C,~view:P -> P & V,~binding:B.Binding) -> D.Declaration,Capture>,List>,Ops(~S,~P,~B.identity(~S,~C,~Rest,~P,~V,~Token,~take,~put,~view,binding)),grant(~S,~C,~R,~E,~Capture,~Rest,~P,~V,~Token,~take,~put,~view,~binding)>: 49 D.Described{empty(~S,~P),[Identity.key(~S,~P,B.identity(~S,~C,~Rest,~P,~V,~Token,~take,~put,~view,binding))],Use.known([Use.Use{Use.Component{Identity.key(~S,~P,B.identity(~S,~C,~Rest,~P,~V,~Token,~take,~put,~view,binding))},Use.Write{}}])}