1	import Base
2	import ./relation_commands.bend as Relation
3	import ./owner_product.bend as Product
4	import ./owned_event_log.bend as Log
5	import ./owned_event_key_route.bend as Route
6	import ./event_publication.bend as Publication
7	import ./ordinary_owned_event.bend as Pub
8	
9	# Trusted engine family boundary. Ordinary constructors derive all paths/routes
10	# from child bindings; gameplay never supplies a live lens or key-routing closure.
11	# The raw constructor is trusted provisioning, not a module-privacy guarantee.
12	type Binding<S:Data,R:Type,P:Type,Rest:Type,E:Data,-path:Product.Lens<R,Log.Log<P>,Rest>,-inject:Nat -> E,-select:List<&2,E> -> List<&2,Nat>,-identity:Pub.Domain<S,P>> is Data:
13	  Binding{}
14	def identity_take(~T:Type,owner:T) -> Unit & T:(Unit{},owner)
15	def identity_put(~T:Type,unit:Unit,owner:T) -> T:owner
16	def identity_lens(~T:Type) -> Product.Lens<T,T,Unit>:
17	  Product.Lens{identity_take(~T),identity_put(~T)}
18	def leaf(~S:Data,~P:Type,~identity:Pub.Domain<S,P>) -> Binding<S,Log.Log<P>,P,Unit,Nat,identity_lens(~Log.Log<P>),Route.inject_leaf,Route.select_leaf,identity>:
19	  Binding{}
20	def left_path(~A:Type,~B:Type,~P:Type,~Rest:Type,~path:Product.Lens<A,Log.Log<P>,Rest>) -> Product.Lens<Product.Owner<A,B>,Log.Log<P>,B & Rest>:
21	  Product.compose(~Product.Owner<A,B>,~A,~B,~Log.Log<P>,~Rest,~Product.lens(~A,~B,~Product.Left{}),~path)
22	def right_path(~A:Type,~B:Type,~P:Type,~Rest:Type,~path:Product.Lens<B,Log.Log<P>,Rest>) -> Product.Lens<Product.Owner<A,B>,Log.Log<P>,A & Rest>:
23	  Product.compose(~Product.Owner<A,B>,~B,~A,~Log.Log<P>,~Rest,~Product.lens(~A,~B,~Product.Right{}),~path)
24	def left(~S:Data,~A:Type,~B:Type,~P:Type,~Rest:Type,~EA:Data,~EB:Data,~path:Product.Lens<A,Log.Log<P>,Rest>,~inject:Nat -> EA,~select:List<&2,EA> -> List<&2,Nat>,~identity:Pub.Domain<S,P>,binding:Binding<S,A,P,Rest,EA,path,inject,select,identity>) -> Binding<S,Product.Owner<A,B>,P,B & Rest,Publication.Publication<EA,EB>,left_path(~A,~B,~P,~Rest,~path),Route.inject_left(~EA,~EB,~inject),Route.select_left(~EA,~EB,~select),identity>:
25	  Binding{}
26	def right(~S:Data,~A:Type,~B:Type,~P:Type,~Rest:Type,~EA:Data,~EB:Data,~path:Product.Lens<B,Log.Log<P>,Rest>,~inject:Nat -> EB,~select:List<&2,EB> -> List<&2,Nat>,~identity:Pub.Domain<S,P>,binding:Binding<S,B,P,Rest,EB,path,inject,select,identity>) -> Binding<S,Product.Owner<A,B>,P,A & Rest,Publication.Publication<EA,EB>,right_path(~A,~B,~P,~Rest,~path),Route.inject_right(~EA,~EB,~inject),Route.select_right(~EA,~EB,~select),identity>:
27	  Binding{}
28	def under_resource(~S:Data,~User:Type,~R:Type,~P:Type,~Rest:Type,~E:Data,~path:Product.Lens<R,Log.Log<P>,Rest>,~inject:Nat -> E,~select:List<&2,E> -> List<&2,Nat>,~identity:Pub.Domain<S,P>,binding:Binding<S,R,P,Rest,E,path,inject,select,identity>) -> Binding<S,Product.Owner<User,R>,P,User & Rest,E,right_path(~User,~R,~P,~Rest,~path),inject,select,identity>:
29	  Binding{}
30	
31	# Relation notice transport preserves the canonical log path and payload domain.
32	def notice_inject(~S:Data,~E:Data,~inject:Nat -> E,id:Nat) -> Relation.Notice<S,E>:Relation.Original{inject(id)}
33	def notice_originals(~S:Data,~E:Data,records:List<&2,Relation.Notice<S,E>>) -> List<&2,E>:
34	  match records:
35	    case []:[]
36	    case Relation.Original{event} <> rest:event <> notice_originals(~S,~E,rest)
37	    case _ <> rest:notice_originals(~S,~E,rest)
38	def notice_select(~S:Data,~E:Data,~select:List<&2,E> -> List<&2,Nat>,records:List<&2,Relation.Notice<S,E>>) -> List<&2,Nat>:
39	  select(notice_originals(~S,~E,records))
40	def under_notice(~S:Data,~R:Type,~P:Type,~Rest:Type,~E:Data,~path:Product.Lens<R,Log.Log<P>,Rest>,~inject:Nat -> E,~select:List<&2,E> -> List<&2,Nat>,~identity:Pub.Domain<S,P>,binding:Binding<S,R,P,Rest,E,path,inject,select,identity>) -> Binding<S,R,P,Rest,Relation.Notice<S,E>,path,notice_inject(~S,~E,~inject),notice_select(~S,~E,~select),identity>:
41	  Binding{}