1	import Base
2	import ./change_tick.bend as Tick
3	import ./machine.bend as M
4	import ./machine_stream.bend as St
5	import ./ordinary_machine_declaration.bend as OD
6	import ./world.bend as W
7	
8	# Runtime constructor inputs remain runtime values, never erased closure captures.
9	def with_resource(~S:Data,~C:Type,~R:Type,~E:Data,~Out:Type,effect:R -> R & Out,world:W.World<S,C,R,E>) -> W.World<S,C,R,E> & Out:
10	  match world:
11	    case W.World{+namespace,allocator,store,resource,+events,pending,+registrations,+nextSystemId,+clock}:W.observe_resource_finish(~S,~C,~R,~E,~Out,effect(resource),namespace,allocator,store,events,pending,registrations,nextSystemId,clock)
12	
13	# The operational slot, stream and change revision share one schema-owned cell.
14	# Revisions are not Registry cursors; each registered condition owns its observation.
15	type State<S:Data,K:Data,V:Data> is Data:
16	  State{slot:M.Slot<S,K,V>,stream:St.Stream<V>,revision:Nat}
17	def empty(~S:Data,~K:Data,~V:Data) -> State<S,K,V>:
18	  State{M.Missing{},St.empty(~V),0n}
19	def slot(~S:Data,~K:Data,~V:Data,+state:State<S,K,V>) -> State<S,K,V> & M.Slot<S,K,V>:
20	  match state:
21	    case State{+value,stream,revision}:(State{value,stream,revision},value)
22	def revision(~S:Data,~K:Data,~V:Data,+state:State<S,K,V>) -> State<S,K,V> & Nat:
23	  match state:
24	    case State{value,stream,+revision}:(State{value,stream,revision},revision)
25	def same_current(~S:Data,~K:Data,~V:Data,~same:V -> V -> Bool,before:M.Slot<S,K,V>,after:M.Slot<S,K,V>) -> Bool:
26	  match before after:
27	    case M.Missing{} M.Missing{}:True{}
28	    case M.Present{a,_,_,_} M.Present{b,_,_,_}:same(a,b)
29	    case _ _:False{}
30	def next_revision(same:Bool,revision:Nat) -> Nat:
31	  match same:
32	    case True{}:revision
33	    case False{}:(revision + 1n : Nat)
34	# Queue-only writes preserve revision. Actual unequal commits increment it.
35	def replaced(~S:Data,~K:Data,~V:Data,~same:V -> V -> Bool,state:State<S,K,V>,+value:M.Slot<S,K,V>) -> State<S,K,V>:
36	  match state:
37	    case State{old,stream,revision}:State{value,stream,next_revision(same_current(~S,~K,~V,~same,old,value),revision)}
38	def insertion_slot(~S:Data,~K:Data,~V:Data,value:V,old:M.Slot<S,K,V>) -> M.Slot<S,K,V>:
39	  match old:
40	    case M.Missing{}:M.Present{value,M.NoPending{},None{},True{}}
41	    case M.Present{_,pending,previous,_}:M.Present{value,pending,previous,True{}}
42	# Recreating an absent State appends; only occupied insert_state clears messages.
43	def insertion_stream(~S:Data,~K:Data,~V:Data,old:M.Slot<S,K,V>,stream:St.Stream<V>,tick:Nat,value:V) -> St.Stream<V>:
44	  match old:
45	    case M.Missing{}:St.publish(~V,stream,tick,M.Initial{value})
46	    case _:St.initial(~V,stream,tick,value)
47	def inserted(~S:Data,~K:Data,~V:Data,state:State<S,K,V>,+value:V,tick:Nat) -> State<S,K,V>:
48	  match state:
49	    case State{+old,stream,revision}:State{insertion_slot(~S,~K,~V,value,old),insertion_stream(~S,~K,~V,old,stream,tick,value),(revision + 1n : Nat)}
50	def slot_returned(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & State<S,K,V>,~put:R -> State<S,K,V> -> R,resource:R,pair:State<S,K,V> & M.Slot<S,K,V>) -> R & M.Slot<S,K,V>:
51	  match pair:
52	    case (state,value):(put(resource,state),value)
53	def taken_slot(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & State<S,K,V>,~put:R -> State<S,K,V> -> R,pair:R & State<S,K,V>) -> R & M.Slot<S,K,V>:
54	  match pair:
55	    case (resource,state):slot_returned(~S,~K,~V,~R,~take,~put,resource,slot(~S,~K,~V,state))
56	def take_slot(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & State<S,K,V>,~put:R -> State<S,K,V> -> R,resource:R) -> R & M.Slot<S,K,V>:
57	  taken_slot(~S,~K,~V,~R,~take,~put,take(resource))
58	def put_taken(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & State<S,K,V>,~put:R -> State<S,K,V> -> R,~same:V -> V -> Bool,value:M.Slot<S,K,V>,pair:R & State<S,K,V>) -> R:
59	  match pair:
60	    case (resource,state):put(resource,replaced(~S,~K,~V,~same,state,value))
61	def put_slot(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & State<S,K,V>,~put:R -> State<S,K,V> -> R,~same:V -> V -> Bool,resource:R,value:M.Slot<S,K,V>) -> R:
62	  put_taken(~S,~K,~V,~R,~take,~put,~same,value,take(resource))
63	def declared(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & State<S,K,V>,~put:R -> State<S,K,V> -> R,name:String,values:List<&2,V>) -> OD.Declaration<S,K,V,R,take_slot(~S,~K,~V,~R,~take,~put)>:
64	  OD.declared(~S,~K,~V,~R,~take_slot(~S,~K,~V,~R,~take,~put),name,values)
65	def insert_taken(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & State<S,K,V>,~put:R -> State<S,K,V> -> R,value:V,tick:Nat,pair:R & State<S,K,V>) -> R & Unit:
66	  match pair:
67	    case (resource,state):(put(resource,inserted(~S,~K,~V,state,value,tick)),Unit{})
68	def inserted_world(~S:Data,~C:Type,~R:Type,~E:Data,pair:W.World<S,C,R,E> & Unit) -> W.World<S,C,R,E>:
69	  match pair:
70	    case (world,_):world
71	def insert_clocked(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & State<S,K,V>,~put:R -> State<S,K,V> -> R,~C:Type,~E:Data,value:V,pair:W.World<S,C,R,E> & Tick.Tick) -> W.World<S,C,R,E>:
72	  match pair:
73	    case (world,tick):inserted_world(~S,~C,~R,~E,with_resource(~S,~C,~R,~E,~Unit,(resource => insert_taken(~S,~K,~V,~R,~take,~put,value,Tick.total(tick),take(resource))),world))
74	# Stream publication advances administrative time independently of component run ticks.
75	def insert_state(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & State<S,K,V>,~put:R -> State<S,K,V> -> R,~C:Type,~E:Data,~declaration:OD.Declaration<S,K,V,R,take_slot(~S,~K,~V,~R,~take,~put)>,world:W.World<S,C,R,E>,value:V) -> W.World<S,C,R,E>:
76	  insert_clocked(~S,~K,~V,~R,~take,~put,~C,~E,value,W.advance_clock(~S,~C,~R,~E,world))
77	def defaulted(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & State<S,K,V>,~put:R -> State<S,K,V> -> R,~C:Type,~E:Data,~declaration:OD.Declaration<S,K,V,R,take_slot(~S,~K,~V,~R,~take,~put)>,pair:W.World<S,C,R,E> & V) -> W.World<S,C,R,E>:
78	  match pair:
79	    case (world,value):insert_state(~S,~K,~V,~R,~take,~put,~C,~E,~declaration,world,value)
80	def init_checked(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & State<S,K,V>,~put:R -> State<S,K,V> -> R,~C:Type,~E:Data,~declaration:OD.Declaration<S,K,V,R,take_slot(~S,~K,~V,~R,~take,~put)>,~make:W.World<S,C,R,E> -> W.World<S,C,R,E> & V,pair:W.World<S,C,R,E> & M.Slot<S,K,V>) -> W.World<S,C,R,E>:
81	  match pair:
82	    case (world,M.Missing{}):defaulted(~S,~K,~V,~R,~take,~put,~C,~E,~declaration,make(world))
83	    case (world,_):world
84	def init_state(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & State<S,K,V>,~put:R -> State<S,K,V> -> R,~C:Type,~E:Data,~declaration:OD.Declaration<S,K,V,R,take_slot(~S,~K,~V,~R,~take,~put)>,~make:W.World<S,C,R,E> -> W.World<S,C,R,E> & V,world:W.World<S,C,R,E>) -> W.World<S,C,R,E>:
85	  init_checked(~S,~K,~V,~R,~take,~put,~C,~E,~declaration,~make,W.observe_resource(~S,~C,~R,~E,~M.Slot<S,K,V>,~take_slot(~S,~K,~V,~R,~take,~put),world))