1	import Base
2	import ./deferred_command.bend as Deferred
3	import ./trace_facts.bend as TraceFacts
4	import ./decode_owned_journal.bend as Journal
5	import ./decode_requests.bend as Request
6	import ./world.bend as W
7	import ./transaction.bend as T
8	import ./bundle_install.bend as Install
9	import ./bundle_batch.bend as Batch
10	
11	# Trusted immediate structural kernel. Reversible receipts and refused owners
12	# leave the world journal; the provisioning frame retains them for Local.
13	def deactivated(~S:Data,~C:Type,~R:Type,~E:Data,result:W.World<S,C,R,E> & W.Status) -> W.World<S,C,R,E>:
14	  match result:
15	    case (world,_):world
16	
17	def restored(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Q:Type,target:W.Handle<S>,result:Install.Restore<W.World<S,C,R,E>,Request.Packet<P>,Q>) -> Install.Restore<W.World<S,C,R,E>,Request.Packet<P>,Q>:
18	  match result:
19	    case Install.Restored{world,payload}:Install.Restored{deactivated(~S,~C,~R,~E,W.deactivate(~S,~C,~R,~E,world,target)),payload}
20	    case Install.Pending{world,recovery,error}:Install.Pending{world,recovery,error}
21	
22	def receipt(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Q:Type,+target:W.Handle<S>,world:W.World<S,C,R,E>,inverse:W.World<S,C,R,E> -> Install.Restore<W.World<S,C,R,E>,Request.Packet<P>,Q>,commands:List<Deferred.Command<W.World<S,C,R,E>>>,events:List<&2,E>,trace:TraceFacts.State,result:List<(W.World<S,C,R,E> -> W.World<S,C,R,E>)> & Nat) -> T.Tx<W.World<S,C,R,E>,E> & (Result<&2,&2,W.WorldError,W.Handle<S>> & (Maybe<&1,Request.Packet<P>> & (Maybe<&1,Journal.Receipt<W.World<S,C,R,E>,Request.Packet<P>,Q>> & Maybe<&1,Journal.Pending<Q>>))):
23	  match result:
24	    case (undo,position):(T.Tx{world,undo,commands,events,trace},(Done{target},(None{},(Some{Journal.Receipt{position,(world => restored(~S,~C,~R,~E,~P,~Q,target,inverse(world)))}},None{}))))
25	
26	def installed(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Q:Type,+target:W.Handle<S>,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:Install.Attempt<W.World<S,C,R,E>,Request.Packet<P>,Q>) -> T.Tx<W.World<S,C,R,E>,E> & (Result<&2,&2,W.WorldError,W.Handle<S>> & (Maybe<&1,Request.Packet<P>> & (Maybe<&1,Journal.Receipt<W.World<S,C,R,E>,Request.Packet<P>,Q>> & Maybe<&1,Journal.Pending<Q>>))):
27	  match result:
28	    case Install.Installed{world,inverse}:receipt(~S,~C,~R,~E,~P,~Q,target,world,inverse,commands,events,trace,Journal.count_inverses(~W.World<S,C,R,E>,undo))
29	    case Install.Refused{world,payload,error}:(T.Tx{deactivated(~S,~C,~R,~E,W.deactivate(~S,~C,~R,~E,world,target)),undo,commands,events,trace},(Fail{error},(Some{payload},(None{},None{}))))
30	    case Install.Quarantined{world,recovery,+error}:(T.Tx{world,undo,commands,events,trace},(Fail{error},(None{},(None{},Some{Journal.Pending{recovery,error}}))))
31	
32	def activated(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Q:Type,~install:W.World<S,C,R,E> -> W.Handle<S> -> Request.Packet<P> -> Install.Attempt<W.World<S,C,R,E>,Request.Packet<P>,Q>,+target:W.Handle<S>,payload:Request.Packet<P>,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> & W.Status) -> T.Tx<W.World<S,C,R,E>,E> & (Result<&2,&2,W.WorldError,W.Handle<S>> & (Maybe<&1,Request.Packet<P>> & (Maybe<&1,Journal.Receipt<W.World<S,C,R,E>,Request.Packet<P>,Q>> & Maybe<&1,Journal.Pending<Q>>))):
33	  match result:
34	    case (world,W.Accepted{}):installed(~S,~C,~R,~E,~P,~Q,target,undo,commands,events,trace,install(world,target,payload))
35	    case (world,W.Rejected{error}):(T.Tx{world,undo,commands,events,trace},(Fail{error},(Some{payload},(None{},None{}))))
36	
37	def reserved(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Q:Type,~install:W.World<S,C,R,E> -> W.Handle<S> -> Request.Packet<P> -> Install.Attempt<W.World<S,C,R,E>,Request.Packet<P>,Q>,payload:Request.Packet<P>,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> & W.Reservation<S>) -> T.Tx<W.World<S,C,R,E>,E> & (Result<&2,&2,W.WorldError,W.Handle<S>> & (Maybe<&1,Request.Packet<P>> & (Maybe<&1,Journal.Receipt<W.World<S,C,R,E>,Request.Packet<P>,Q>> & Maybe<&1,Journal.Pending<Q>>))):
38	  match result:
39	    case (world,W.Reserved{+target}):activated(~S,~C,~R,~E,~P,~Q,~install,target,payload,undo,commands,events,trace,W.activate(~S,~C,~R,~E,world,target))
40	    case (world,W.ReservationRejected{error}):(T.Tx{world,undo,commands,events,trace},(Fail{error},(Some{payload},(None{},None{}))))
41	
42	def spawn(~S:Data,~C:Type,~R:Type,~E:Data,~P:Type,~Q:Type,~install:W.World<S,C,R,E> -> W.Handle<S> -> Request.Packet<P> -> Install.Attempt<W.World<S,C,R,E>,Request.Packet<P>,Q>,tx:T.Tx<W.World<S,C,R,E>,E>,payload:Request.Packet<P>) -> T.Tx<W.World<S,C,R,E>,E> & (Result<&2,&2,W.WorldError,W.Handle<S>> & (Maybe<&1,Request.Packet<P>> & (Maybe<&1,Journal.Receipt<W.World<S,C,R,E>,Request.Packet<P>,Q>> & Maybe<&1,Journal.Pending<Q>>))):
43	  match tx:
44	    case T.Tx{world,undo,commands,events,trace}:reserved(~S,~C,~R,~E,~P,~Q,~install,payload,undo,commands,events,trace,W.reserve_id(~S,~C,~R,~E,world))