1	import Base
2	import ./change_tick.bend as Tick
3	
4	# Administrative time and captured execution ticks. Payloads never live here.
5	# Nested execution restores its enclosing tick without rewinding World time.
6	type State is Data:
7	  State{now:Tick.Tick,scopes:List<&2,Tick.Tick>}
8	
9	def empty() -> State:
10	  State{Tick.zero(),[]}
11	
12	def now(state:State) -> Tick.Tick:
13	  match state:
14	    case State{tick,_}:tick
15	
16	def floor_tick(ordered:Bool,current:Tick.Tick,minimum:Tick.Tick) -> Tick.Tick:
17	  match ordered:
18	    case True{}:minimum
19	    case False{}:current
20	
21	# Trusted restore publication raises administrative time without rebasing any
22	# retained reader cursor or captured scope. Admission requires quiescent scopes.
23	# Elapsed receiver time is preserved; saved events are not replayed.
24	def floor(state:State,+minimum:Tick.Tick) -> State:
25	  match state:
26	    case State{+current,scopes}:State{floor_tick(Tick.not_future(current,minimum),current,minimum),scopes}
27	
28	def entered(+tick:Tick.Tick,scopes:List<&2,Tick.Tick>) -> State & Tick.Tick:
29	  (State{tick,tick <> scopes},tick)
30	
31	# Every admitted system execution captures exactly one new change tick.
32	def enter(state:State) -> State & Tick.Tick:
33	  match state:
34	    case State{tick,scopes}:entered(Tick.next(tick),scopes)
35	
36	def left(tick:Tick.Tick,scopes:List<&2,Tick.Tick>) -> State:
37	  match scopes:
38	    case []:State{tick,[]}
39	    case _ <> rest:State{tick,rest}
40	
41	# Complete an execution scope; administrative time is retained on failure too.
42	def leave(state:State) -> State:
43	  match state:
44	    case State{tick,scopes}:left(tick,scopes)
45	
46	def advanced(+tick:Tick.Tick,scopes:List<&2,Tick.Tick>) -> State & Tick.Tick:
47	  (State{tick,scopes},tick)
48	
49	# Advance an explicit direct/deferred boundary without opening a system scope.
50	def advance(state:State) -> State & Tick.Tick:
51	  match state:
52	    case State{tick,scopes}:advanced(Tick.next(tick),scopes)
53	
54	def write_scoped(tick:Tick.Tick,scopes:List<&2,Tick.Tick>) -> State & Tick.Tick:
55	  match scopes:
56	    case []:advanced(Tick.next(tick),[])
57	    case +active <> rest:(State{tick,active <> rest},active)
58	
59	# Writes in a system reuse its captured tick; standalone writes get a new tick.
60	def write(state:State) -> State & Tick.Tick:
61	  match state:
62	    case State{tick,scopes}:write_scoped(tick,scopes)
63	
64	# Captured tick of the enclosing execution, or administrative time outside a run.
65	def current_scoped(tick:Tick.Tick,scopes:List<&2,Tick.Tick>) -> Tick.Tick:
66	  match scopes:
67	    case []:tick
68	    case active <> _:active
69	def current(state:State) -> Tick.Tick:
70	  match state:
71	    case State{tick,scopes}:current_scoped(tick,scopes)
72	
73	# Lower query execution reuses an admitted scope, opening one only when direct.
74	def ensured(+tick:Tick.Tick,scopes:List<&2,Tick.Tick>) -> State & Bool:
75	  match scopes:
76	    case []:(State{Tick.next(tick),[Tick.next(tick)]},True{})
77	    case active <> rest:(State{tick,active <> rest},False{})
78	def ensure(state:State) -> State & Bool:
79	  match state:
80	    case State{tick,scopes}:ensured(tick,scopes)
81	def finish(owned:Bool,state:State) -> State:
82	  match owned:
83	    case False{}:state
84	    case True{}:leave(state)