1	import Base
2	import ./change_tick.bend as Tick
3	import ./trace_facts.bend as TraceFacts
4	import entity_key.bend as Key
5	import compose.bend as Q
6	import capabilities.bend as Cap
7	import world.bend as W
8	import transaction.bend as T
9	
10	type Error<U: Data> is Data:
11	  MissingEntity{entityId: Key.Key}
12	  QueryMismatch{entityId: Key.Key}
13	  NoEntities{}
14	  MultipleEntities{count: U32}
15	  BodyError{error: Q.Error<U>}
16	type Scanned<-S: Data,-Store: Type,-R: Type,-E: Data> is Type:
17	  Scanned{world: W.World<S,Store,R,E>,handles: List<&2,W.Handle<S>>}
18	type Executed<-World: Type,U: Data,Out: Data> is Type:
19	  Executed{world: World,result: Result<&2,&2,Error<U>,Out>}
20	
21	def handle_id(~S: Data,handle: W.Handle<S>) -> Key.Key:
22	  match handle:
23	    case W.Handle{_,id}: id
24	def add(~S: Data,selected: Bool,handle: W.Handle<S>,rest: List<&2,W.Handle<S>>) -> List<&2,W.Handle<S>>:
25	  match selected:
26	    case True{}: handle <> rest
27	    case False{}: rest
28	# Selection is a read-only observation even if a trusted plan accidentally mutates.
29	def unselect(~S: Data,~Store: Type,~R: Type,~E: Data,observed: Q.Frame<S,Store,R,E> & Bool) -> W.World<S,Store,R,E> & Bool:
30	  match observed:
31	    case (Q.Frame{T.Tx{world,undo,_,_,_},_,_,_},selected): (T.rollback(~W.World<S,Store,R,E>,undo,world),selected)
32	def prepend(~S: Data,~Store: Type,~R: Type,~E: Data,selected: Bool,handle: W.Handle<S>,observed: Scanned<S,Store,R,E>) -> Scanned<S,Store,R,E>:
33	  match observed:
34	    case Scanned{world,handles}: Scanned{world,add(~S,selected,handle,handles)}
35	def scanned_join(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~plan: Q.Plan<S,Store,R,E,Ops>,+cursor:Maybe<&2,Tick.Tick>,handle: W.Handle<S>,next: W.World<S,Store,R,E> -> Scanned<S,Store,R,E>,observed: W.World<S,Store,R,E> & Bool) -> Scanned<S,Store,R,E>:
36	  (world,selected) = observed
37	  prepend(~S,~Store,~R,~E,selected,handle,next(world))
38	def scan_handles(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~plan: Q.Plan<S,Store,R,E,Ops>,handles: List<&2,W.Handle<S>>,+cursor:Maybe<&2,Tick.Tick>,world: W.World<S,Store,R,E>) -> Scanned<S,Store,R,E>:
39	  match handles:
40	    case []: Scanned{world,[]}
41	    case +handle <> rest: scanned_join(~S,~Store,~R,~E,~Ops,~plan,cursor,handle,(world => scan_handles(~S,~Store,~R,~E,~Ops,~plan,rest,cursor,world)),unselect(~S,~Store,~R,~E,Q.plan_select(~S,~Store,~R,~E,~Ops,plan)(Q.Frame{T.begin(~W.World<S,Store,R,E>,~E,world),handle,None{},cursor})))
42	def scan_reserved(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~plan: Q.Plan<S,Store,R,E,Ops>,cursor:Maybe<&2,Tick.Tick>,observed: W.World<S,Store,R,E> & List<&2,W.Handle<S>>) -> Scanned<S,Store,R,E>:
43	  (world,handles) = observed
44	  scan_handles(~S,~Store,~R,~E,~Ops,~plan,handles,cursor,world)
45	def scan(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~plan: Q.Plan<S,Store,R,E,Ops>,world: W.World<S,Store,R,E>,cursor:Maybe<&2,Tick.Tick>) -> Scanned<S,Store,R,E>:
46	  scan_reserved(~S,~Store,~R,~E,~Ops,~plan,cursor,W.handles(~S,~Store,~R,~E,world))
47	def count_list(~S: Data,handles: List<&2,W.Handle<S>>,n: U32) -> U32:
48	  match handles:
49	    case []: n
50	    case _ <> rest: count_list(~S,rest,(n + 1 : U32))
51	def counted(~S: Data,~Store: Type,~R: Type,~E: Data,observed: Scanned<S,Store,R,E>) -> W.World<S,Store,R,E> & U32:
52	  match observed:
53	    case Scanned{world,handles}: (world,count_list(~S,handles,0))
54	def count(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~plan: Q.Plan<S,Store,R,E,Ops>,world: W.World<S,Store,R,E>,cursor:Maybe<&2,Tick.Tick>) -> W.World<S,Store,R,E> & U32:
55	  counted(~S,~Store,~R,~E,scan(~S,~Store,~R,~E,~Ops,~plan,world,cursor))
56	def executed(~World: Type,~U: Data,~Out: Data,+entityId: Key.Key,observed: Q.Executed<World,Q.Error<U>,Out>) -> Executed<World,U,Out>:
57	  match observed:
58	    case Q.Executed{world,T.Failure{error},_}: Executed{world,Fail{BodyError{error}}}
59	    case Q.Executed{world,T.Success{},value <> []}: Executed{world,Done{value}}
60	    case Q.Executed{world,T.Success{},[]}: Executed{world,Fail{QueryMismatch{entityId}}}
61	    case Q.Executed{world,T.Success{},_}: Executed{world,Fail{QueryMismatch{entityId}}}
62	def complete(~S: Data,~Store: Type,~R: Type,~E: Data,~U: Data,~Out: Data,tx: T.Tx<W.World<S,Store,R,E>,E>) -> T.Tx<W.World<S,Store,R,E>,E> & (T.Outcome<Q.Error<U>> & List<&2,Out>):
63	  (tx,(T.Success{},[]))
64	def scope_finished(~S:Data,~Store:Type,~R:Type,~E:Data,~U:Data,~Out:Data,owned:Bool,result:Executed<W.World<S,Store,R,E>,U,Out>) -> Executed<W.World<S,Store,R,E>,U,Out>:
65	  match result:
66	    case Executed{world,result}:Executed{W.finish_run(~S,~Store,~R,~E,owned,world),result}
67	def invoke_inner(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~plan: Q.Plan<S,Store,R,E,Ops>,~A: Data,~U: Data,~Out: Data,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & (T.Outcome<U> & Out),args: A,world: W.World<S,Store,R,E>,+handle: W.Handle<S>,cursor:Maybe<&2,Tick.Tick>) -> Executed<W.World<S,Store,R,E>,U,Out>:
68	  executed(~W.World<S,Store,R,E>,~U,~Out,handle_id(~S,handle),Q.finished(~S,~Store,~R,~E,~U,~Out,Q.body_returned(~S,~Store,~R,~E,~U,~Out,complete(~S,~Store,~R,~E,~U,~Out),Cap.invoke(~Ops,~A,~(T.Outcome<U> & Out),~body,~Q.Frame<S,Store,R,E>,~Q.plan_caps(~S,~Store,~R,~E,~Ops,plan),args,Q.Frame{T.begin(~W.World<S,Store,R,E>,~E,world),handle,None{},cursor}))))
69	def invoke_scoped(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~plan: Q.Plan<S,Store,R,E,Ops>,~A: Data,~U: Data,~Out: Data,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & (T.Outcome<U> & Out),args: A,admitted:W.World<S,Store,R,E> & Bool,+handle: W.Handle<S>,cursor:Maybe<&2,Tick.Tick>) -> Executed<W.World<S,Store,R,E>,U,Out>:
70	  (world,owned)=admitted
71	  scope_finished(~S,~Store,~R,~E,~U,~Out,owned,invoke_inner(~S,~Store,~R,~E,~Ops,~plan,~A,~U,~Out,~body,args,world,handle,cursor))
72	def invoke(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~plan: Q.Plan<S,Store,R,E,Ops>,~A: Data,~U: Data,~Out: Data,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & (T.Outcome<U> & Out),args: A,world: W.World<S,Store,R,E>,+handle: W.Handle<S>,cursor:Maybe<&2,Tick.Tick>) -> Executed<W.World<S,Store,R,E>,U,Out>:
73	  invoke_scoped(~S,~Store,~R,~E,~Ops,~plan,~A,~U,~Out,~body,args,W.ensure_run(~S,~Store,~R,~E,world),handle,cursor)
74	
75	def single_scanned(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~plan: Q.Plan<S,Store,R,E,Ops>,~A: Data,~U: Data,~Out: Data,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & (T.Outcome<U> & Out),args: A,cursor:Maybe<&2,Tick.Tick>,observed: Scanned<S,Store,R,E>) -> Executed<W.World<S,Store,R,E>,U,Out>:
76	  match observed:
77	    case Scanned{world,[]}: Executed{world,Fail{NoEntities{}}}
78	    case Scanned{world,handle <> []}: invoke(~S,~Store,~R,~E,~Ops,~plan,~A,~U,~Out,~body,args,world,handle,cursor)
79	    case Scanned{world,+handles}: Executed{world,Fail{MultipleEntities{count_list(~S,handles,0)}}}
80	def single(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~plan: Q.Plan<S,Store,R,E,Ops>,~A: Data,~U: Data,~Out: Data,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & (T.Outcome<U> & Out),args: A,world: W.World<S,Store,R,E>,+cursor:Maybe<&2,Tick.Tick>) -> Executed<W.World<S,Store,R,E>,U,Out>:
81	  single_scanned(~S,~Store,~R,~E,~Ops,~plan,~A,~U,~Out,~body,args,cursor,scan(~S,~Store,~R,~E,~Ops,~plan,world,cursor))
82	def lookup_selected(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~plan: Q.Plan<S,Store,R,E,Ops>,~A: Data,~U: Data,~Out: Data,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & (T.Outcome<U> & Out),args: A,handle: W.Handle<S>,cursor:Maybe<&2,Tick.Tick>,observed: W.World<S,Store,R,E> & Bool) -> Executed<W.World<S,Store,R,E>,U,Out>:
83	  match observed:
84	    case (world,False{}): Executed{world,Fail{QueryMismatch{handle_id(~S,handle)}}}
85	    case (world,True{}): invoke(~S,~Store,~R,~E,~Ops,~plan,~A,~U,~Out,~body,args,world,handle,cursor)
86	def lookup_valid(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~plan: Q.Plan<S,Store,R,E,Ops>,~A: Data,~U: Data,~Out: Data,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & (T.Outcome<U> & Out),args: A,+handle: W.Handle<S>,+cursor:Maybe<&2,Tick.Tick>,observed: W.World<S,Store,R,E> & Bool) -> Executed<W.World<S,Store,R,E>,U,Out>:
87	  match observed:
88	    case (world,False{}): Executed{world,Fail{MissingEntity{handle_id(~S,handle)}}}
89	    case (world,True{}): lookup_selected(~S,~Store,~R,~E,~Ops,~plan,~A,~U,~Out,~body,args,handle,cursor,unselect(~S,~Store,~R,~E,Q.plan_select(~S,~Store,~R,~E,~Ops,plan)(Q.Frame{T.begin(~W.World<S,Store,R,E>,~E,world),handle,None{},cursor})))
90	def get(~S: Data,~Store: Type,~R: Type,~E: Data,~Ops: Type -> Type,~plan: Q.Plan<S,Store,R,E,Ops>,~A: Data,~U: Data,~Out: Data,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & (T.Outcome<U> & Out),args: A,world: W.World<S,Store,R,E>,+handle: W.Handle<S>,cursor:Maybe<&2,Tick.Tick>) -> Executed<W.World<S,Store,R,E>,U,Out>:
91	  lookup_valid(~S,~Store,~R,~E,~Ops,~plan,~A,~U,~Out,~body,args,handle,cursor,W.valid(~S,~Store,~R,~E,world,handle))