1	import Base
2	import ./trace_facts.bend as Facts
3	import ./world.bend as W
4	import ./owner_product.bend as Product
5	import ./owned_event_log.bend as Log
6	import ./owned_event_family_storage.bend as Storage
7	import ./recovery_journal.bend as Journal
8	# Trusted transport. Ordinary declaration builders derive both paths together;
9	# authored gameplay receives only the abstract emission capability.
10	type Stage<State:Type,Recovery:Type> is Type:
11	  Stage{newest:List<Journal.Action(~State,~Recovery)>,trace:Facts.State}
12	def empty(~State:Type,~Recovery:Type) -> Stage<State,Recovery>:Stage{[],Facts.Off{}}
13	def recovered(~P:Type,~All:Type,~Rest:Type,~path:Product.Lens<All,List<P>,Rest>,payload:P,parts:Rest & List<P>) -> All:
14	  match parts:
15	    case (rest,values):Product.put_field(~All,~List<P>,~Rest,path)(rest,List.append(&1,P,values,[payload]))
16	def recover(~P:Type,~All:Type,~Rest:Type,~path:Product.Lens<All,List<P>,Rest>,payload:P,all:All) -> All:
17	  recovered(~P,~All,~Rest,~path,payload,Product.get_field(~All,~List<P>,~Rest,path)(all))
18	def action(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~E:Data,~path:Product.Lens<R,Log.Log<P>,Rest>,~inject:Nat -> E,~All:Type,~RecoveryRest:Type,~recovery:Product.Lens<All,List<P>,RecoveryRest>,payload:P,success:Bool,world:W.World<S,C,R,E>,all:All) -> W.World<S,C,R,E> & All:
19	  match success:
20	    case True{}:(Storage.commit_owned(~S,~C,~R,~P,~Rest,~E,~path,~inject,world,[payload]),all)
21	    case False{}:(world,recover(~P,~All,~RecoveryRest,~recovery,payload,all))
22	def emit(~S:Data,~C:Type,~R:Type,~P:Type,~Rest:Type,~E:Data,~path:Product.Lens<R,Log.Log<P>,Rest>,~inject:Nat -> E,~All:Type,~RecoveryRest:Type,~recovery:Product.Lens<All,List<P>,RecoveryRest>,stage:Stage<W.World<S,C,R,E>,All>,payload:P) -> Stage<W.World<S,C,R,E>,All>:
23	  match stage:
24	    case Stage{newest,trace}:Stage{(success => world => all => action(~S,~C,~R,~P,~Rest,~E,~path,~inject,~All,~RecoveryRest,~recovery,payload,success,world,all)) <> newest,trace}
25	# Reverse the action spine once: commits retain the global inter-family order,
26	# and abort receipts retain each family's order. Every closure executes once.
27	def finish(~State:Type,~Recovery:Type,stage:Stage<State,Recovery>,success:Bool,state:State,recovery:Recovery) -> State & Recovery:
28	  match stage:
29	    case Stage{newest,_}:Journal.finish(~State,~Recovery,List.reverse(&1,Journal.Action(~State,~Recovery),newest),success,state,recovery)
30	
31	def with_trace(~State:Type,~Recovery:Type,trace:Facts.State) -> Stage<State,Recovery>:Stage{[],trace}
32	def record_named(~State:Type,~Recovery:Type,name:String,stage:Stage<State,Recovery>) -> Stage<State,Recovery>:
33	  match stage:
34	    case Stage{newest,Facts.Off{}}:Stage{newest,Facts.Off{}}
35	    case Stage{newest,Facts.On{facts}}:Stage{newest,Facts.On{Facts.Fact{Facts.EventValue{},name,Facts.SendOperation{},None{},Facts.UnavailableValue{},Facts.OpaqueValue{},Facts.Attempted{}} <> facts}}
36	def finish_observed(~State:Type,~Recovery:Type,stage:Stage<State,Recovery>,+success:Bool,state:State,recovery:Recovery) -> (State & Recovery) & Facts.State:
37	  match stage:
38	    case Stage{newest,trace}:(Journal.finish(~State,~Recovery,List.reverse(&1,Journal.Action(~State,~Recovery),newest),success,state,recovery),Facts.settle(trace,success))