1	import Base
2	import ./deferred_command.bend as Deferred
3	import ./trace_facts.bend as TraceFacts
4	import ./owner_product.bend as Product
5	import ./world.bend as W
6	import ./transaction.bend as T
7	import ./resource.bend as Resource
8	import ./capabilities.bend as Cap
9	# Canonical product lenses preserve affine siblings during selected-field operations.
10	def viewed(~R:Type,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<R,P,Rest>,rest:Rest,result:P & V) -> R & V:
11	  match result:
12	    case (part,value):(Product.put_field(~R,~P,~Rest,lens)(rest,part),value)
13	def taken(~R:Type,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<R,P,Rest>,~view:P -> P & V,result:Rest & P) -> R & V:
14	  match result:
15	    case (rest,part):viewed(~R,~P,~Rest,~V,~lens,rest,view(part))
16	def project(~R:Type,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<R,P,Rest>,~view:P -> P & V,resource:R) -> R & V:
17	  taken(~R,~P,~Rest,~V,~lens,~view,Product.get_field(~R,~P,~Rest,lens)(resource))
18	def replacing(~R:Type,~P:Type,~Rest:Type,~lens:Product.Lens<R,P,Rest>,replacement:P,result:Rest & P) -> R & P:
19	  match result:
20	    case (rest,old):(Product.put_field(~R,~P,~Rest,lens)(rest,replacement),old)
21	def replace(~R:Type,~P:Type,~Rest:Type,~lens:Product.Lens<R,P,Rest>,replacement:P,resource:R) -> R & P:
22	  replacing(~R,~P,~Rest,~lens,replacement,Product.get_field(~R,~P,~Rest,lens)(resource))
23	# Runtime replacement owners cannot be captured in an erased projector template.
24	# Trusted engine boundary threads the same World fields through the core join.
25	def replace_world(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Rest:Type,~lens:Product.Lens<R,P,Rest>,replacement:P,world:W.World<S,C,R,E>) -> W.World<S,C,R,E> & P:
26	  match world:
27	    case W.World{+namespace,allocator,store,resource,+events,pending,+registrations,+nextSystemId,+clock}:W.observe_resource_finish(~S,~C,~R,~E,~P,replace(~R,~P,~Rest,~lens,replacement,resource),namespace,allocator,store,events,pending,registrations,nextSystemId,clock)
28	def restored(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,result:W.World<S,C,R,E> & P) -> W.World<S,C,R,E>:
29	  match result:
30	    case (world,_):world
31	def restore(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Rest:Type,~lens:Product.Lens<R,P,Rest>,old:P,world:W.World<S,C,R,E>) -> W.World<S,C,R,E>:
32	  restored(~S,~C,~R,~E,~P,replace_world(~S,~C,~R,~E,~P,~Rest,~lens,old,world))
33	def journaled(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Rest:Type,~lens:Product.Lens<R,P,Rest>,undo:List<(W.World<S,C,R,E> -> W.World<S,C,R,E>)>,commands:List<Deferred.Command<W.World<S,C,R,E>>>,events:List<&2,E>,trace:TraceFacts.State,result:W.World<S,C,R,E> & P) -> T.Tx<W.World<S,C,R,E>,E>:
34	  match result:
35	    case (world,old):T.Tx{world,(w=>restore(~S,~C,~R,~E,~P,~Rest,~lens,old,w)) <> undo,commands,events,trace}
36	def tx_set(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Rest:Type,~lens:Product.Lens<R,P,Rest>,tx:T.Tx<W.World<S,C,R,E>,E>,replacement:P) -> T.Tx<W.World<S,C,R,E>,E>:
37	  match tx:
38	    case T.Tx{world,undo,commands,events,trace}:journaled(~S,~C,~R,~E,~P,~Rest,~lens,undo,commands,events,trace,replace_world(~S,~C,~R,~E,~P,~Rest,~lens,replacement,world))
39	def read(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<R,P,Rest>,~view:P -> P & V) -> Cap.ValueRead<T.Tx<W.World<S,C,R,E>,E>,V>:
40	  Cap.ValueRead{Resource.tx_get(~S,~C,~R,~E,~V,~project(~R,~P,~Rest,~V,~lens,~view))}
41	def write(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<R,P,Rest>,~view:P -> P & V) -> Cap.ValueWrite<T.Tx<W.World<S,C,R,E>,E>,P,V>:
42	  Cap.ValueWrite{Resource.tx_get(~S,~C,~R,~E,~V,~project(~R,~P,~Rest,~V,~lens,~view)),tx_set(~S,~C,~R,~E,~P,~Rest,~lens)}
43	
44	# The disabled arm reaches the original setter before any view or rendering.
45	def observed_set_ready(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<R,P,Rest>,~view:P -> P & V,~render:V -> String,key:String,result:T.Tx<W.World<S,C,R,E>,E> & V,incoming:P & V) -> T.Tx<W.World<S,C,R,E>,E>:
46	  match result incoming:
47	    case (tx,before), (replacement,after):T.record(~W.World<S,C,R,E>,~E,tx_set(~S,~C,~R,~E,~P,~Rest,~lens,tx,replacement),TraceFacts.Fact{TraceFacts.ResourceValue{},key,TraceFacts.WriteOperation{},None{},TraceFacts.DisplayedValue{render(before)},TraceFacts.DisplayedValue{render(after)},TraceFacts.Attempted{}})
48	def observed_set_enabled(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<R,P,Rest>,~view:P -> P & V,~render:V -> String,key:String,replacement:P,result:T.Tx<W.World<S,C,R,E>,E> & Bool) -> T.Tx<W.World<S,C,R,E>,E>:
49	  match result:
50	    case (tx,False{}):tx_set(~S,~C,~R,~E,~P,~Rest,~lens,tx,replacement)
51	    case (tx,True{}):observed_set_ready(~S,~C,~R,~E,~P,~Rest,~V,~lens,~view,~render,key,Resource.tx_get(~S,~C,~R,~E,~V,~project(~R,~P,~Rest,~V,~lens,~view),tx),view(replacement))
52	def observed_set(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<R,P,Rest>,~view:P -> P & V,~render:V -> String,~key:String,tx:T.Tx<W.World<S,C,R,E>,E>,replacement:P) -> T.Tx<W.World<S,C,R,E>,E>:
53	  observed_set_enabled(~S,~C,~R,~E,~P,~Rest,~V,~lens,~view,~render,key,replacement,T.trace_enabled(~W.World<S,C,R,E>,~E,tx))
54	def write_observed(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Rest:Type,~V:Data,~lens:Product.Lens<R,P,Rest>,~view:P -> P & V,~render:V -> String,~key:String) -> Cap.ValueWrite<T.Tx<W.World<S,C,R,E>,E>,P,V>:
55	  Cap.ValueWrite{Resource.tx_get(~S,~C,~R,~E,~V,~project(~R,~P,~Rest,~V,~lens,~view)),observed_set(~S,~C,~R,~E,~P,~Rest,~V,~lens,~view,~render,~key)}