1	import Base
2	import ./ordinary_owned_event_binding.bend as Binding
3	import ./ordinary_owned_event.bend as Pub
4	import ./owned_event_log.bend as Log
5	import ./owner_product.bend as Product
6	import ./owned_event_key_route.bend as Route
7	import ./ordinary_event_declaration.bend as Event
8	import ./ordinary_event_family.bend as Family
9	import ./event_stream.bend as Stream
10	import ./event_publication.bend as Publication
11	
12	# Trusted setup constructor; ordinary constructors derive matching log and stream paths.
13	type Setup<S:Data,R:Type,P:Type,Rest:Type,E:Data,D:Data,F:Type,-path:Product.Lens<R,Log.Log<P>,Rest>,-inject:Nat -> E,-select:List<&2,E> -> List<&2,Nat>,-identity:Pub.Domain<S,P>,-make:D -> Nat -> F,-sync:F -> Nat -> List<&2,E> -> F,-frame:F -> Nat -> F,-retain:F -> Nat -> List<&2,E> -> F & List<&2,E>,-inventory:F -> F & List<&2,String>,-take:F -> F & Stream.Stream<S,Nat>,-put:F -> Stream.Stream<S,Nat> -> F> is Data:
14	  Setup{owned:Binding.Binding<S,R,P,Rest,E,path,inject,select,identity>,provision:Family.Provision<S,E,D,F,make,sync,frame,retain,inventory>,selection:Family.Selection<S,Nat,F,take,put>}
15	def domain(~S:Data,~P:Type,identity:Pub.Domain<S,P>) -> Event.Domain<S,Nat>:
16	  match identity:
17	    case Pub.Domain{key}:Event.Domain{key}
18	def leaf(~S:Data,~P:Type,~identity:Pub.Domain<S,P>) -> Setup<S,Log.Log<P>,P,Unit,Nat,Event.Domain<S,Nat>,Stream.Stream<S,Nat>,Binding.identity_lens(~Log.Log<P>),Route.inject_leaf,Route.select_leaf,identity,Family.leaf_make(~S,~Nat),Family.leaf_sync(~S,~Nat),Family.leaf_frame(~S,~Nat),Family.leaf_retain(~S,~Nat),Family.leaf_inventory(~S,~Nat),Family.selected_leaf(~S,~Nat),Family.replaced_leaf(~S,~Nat)>:
19	  Setup{Binding.leaf(~S,~P,~identity),Family.leaf(~S,~Nat,domain(~S,~P,identity)),Family.select_leaf(~S,~Nat)}
20	def left(~S:Data,~RA:Type,~PA:Type,~RestA:Type,~EA:Data,~DA:Data,~FA:Type,~pathA:Product.Lens<RA,Log.Log<PA>,RestA>,~injectA:Nat -> EA,~selectA:List<&2,EA> -> List<&2,Nat>,~identityA:Pub.Domain<S,PA>,~makeA:DA -> Nat -> FA,~syncA:FA -> Nat -> List<&2,EA> -> FA,~frameA:FA -> Nat -> FA,~retainA:FA -> Nat -> List<&2,EA> -> FA & List<&2,EA>,~inventoryA:FA -> FA & List<&2,String>,~takeA:FA -> FA & Stream.Stream<S,Nat>,~putA:FA -> Stream.Stream<S,Nat> -> FA,~RB:Type,~PB:Type,~RestB:Type,~EB:Data,~DB:Data,~FB:Type,~pathB:Product.Lens<RB,Log.Log<PB>,RestB>,~injectB:Nat -> EB,~selectB:List<&2,EB> -> List<&2,Nat>,~identityB:Pub.Domain<S,PB>,~makeB:DB -> Nat -> FB,~syncB:FB -> Nat -> List<&2,EB> -> FB,~frameB:FB -> Nat -> FB,~retainB:FB -> Nat -> List<&2,EB> -> FB & List<&2,EB>,~inventoryB:FB -> FB & List<&2,String>,~takeB:FB -> FB & Stream.Stream<S,Nat>,~putB:FB -> Stream.Stream<S,Nat> -> FB,first:Setup<S,RA,PA,RestA,EA,DA,FA,pathA,injectA,selectA,identityA,makeA,syncA,frameA,retainA,inventoryA,takeA,putA>,second:Setup<S,RB,PB,RestB,EB,DB,FB,pathB,injectB,selectB,identityB,makeB,syncB,frameB,retainB,inventoryB,takeB,putB>) -> Setup<S,Product.Owner<RA,RB>,PA,RB & RestA,Publication.Publication<EA,EB>,Family.Domains<DA,DB>,Product.Owner<FA,FB>,Binding.left_path(~RA,~RB,~PA,~RestA,~pathA),Route.inject_left(~EA,~EB,~injectA),Route.select_left(~EA,~EB,~selectA),identityA,Family.node_make(~DA,~DB,~FA,~FB,~makeA,~makeB),Family.node_sync(~EA,~EB,~FA,~FB,~syncA,~syncB),Family.node_frame(~FA,~FB,~frameA,~frameB),Family.pair_retain(~EA,~EB,~FA,~FB,~retainA,~retainB),Family.pair_inventory(~FA,~FB,~inventoryA,~inventoryB),Family.left_take(~S,~Nat,~FA,~FB,~takeA),Family.left_put(~S,~Nat,~FA,~FB,~putA)>:
21	  match first second:
22	    case Setup{ownedA,provisionA,selectionA} Setup{ownedB,provisionB,selectionB}:Setup{Binding.left(~S,~RA,~RB,~PA,~RestA,~EA,~EB,~pathA,~injectA,~selectA,~identityA,ownedA),Family.branch(~S,~EA,~EB,~DA,~DB,~FA,~FB,~makeA,~makeB,~syncA,~syncB,~frameA,~frameB,~retainA,~retainB,~inventoryA,~inventoryB,provisionA,provisionB),Family.select_left(~S,~Nat,~FA,~FB,~takeA,~putA,selectionA)}
23	def right(~S:Data,~RA:Type,~PA:Type,~RestA:Type,~EA:Data,~DA:Data,~FA:Type,~pathA:Product.Lens<RA,Log.Log<PA>,RestA>,~injectA:Nat -> EA,~selectA:List<&2,EA> -> List<&2,Nat>,~identityA:Pub.Domain<S,PA>,~makeA:DA -> Nat -> FA,~syncA:FA -> Nat -> List<&2,EA> -> FA,~frameA:FA -> Nat -> FA,~retainA:FA -> Nat -> List<&2,EA> -> FA & List<&2,EA>,~inventoryA:FA -> FA & List<&2,String>,~takeA:FA -> FA & Stream.Stream<S,Nat>,~putA:FA -> Stream.Stream<S,Nat> -> FA,~RB:Type,~PB:Type,~RestB:Type,~EB:Data,~DB:Data,~FB:Type,~pathB:Product.Lens<RB,Log.Log<PB>,RestB>,~injectB:Nat -> EB,~selectB:List<&2,EB> -> List<&2,Nat>,~identityB:Pub.Domain<S,PB>,~makeB:DB -> Nat -> FB,~syncB:FB -> Nat -> List<&2,EB> -> FB,~frameB:FB -> Nat -> FB,~retainB:FB -> Nat -> List<&2,EB> -> FB & List<&2,EB>,~inventoryB:FB -> FB & List<&2,String>,~takeB:FB -> FB & Stream.Stream<S,Nat>,~putB:FB -> Stream.Stream<S,Nat> -> FB,first:Setup<S,RA,PA,RestA,EA,DA,FA,pathA,injectA,selectA,identityA,makeA,syncA,frameA,retainA,inventoryA,takeA,putA>,second:Setup<S,RB,PB,RestB,EB,DB,FB,pathB,injectB,selectB,identityB,makeB,syncB,frameB,retainB,inventoryB,takeB,putB>) -> Setup<S,Product.Owner<RA,RB>,PB,RA & RestB,Publication.Publication<EA,EB>,Family.Domains<DA,DB>,Product.Owner<FA,FB>,Binding.right_path(~RA,~RB,~PB,~RestB,~pathB),Route.inject_right(~EA,~EB,~injectB),Route.select_right(~EA,~EB,~selectB),identityB,Family.node_make(~DA,~DB,~FA,~FB,~makeA,~makeB),Family.node_sync(~EA,~EB,~FA,~FB,~syncA,~syncB),Family.node_frame(~FA,~FB,~frameA,~frameB),Family.pair_retain(~EA,~EB,~FA,~FB,~retainA,~retainB),Family.pair_inventory(~FA,~FB,~inventoryA,~inventoryB),Family.right_take(~S,~Nat,~FA,~FB,~takeB),Family.right_put(~S,~Nat,~FA,~FB,~putB)>:
24	  match first second:
25	    case Setup{ownedA,provisionA,selectionA} Setup{ownedB,provisionB,selectionB}:Setup{Binding.right(~S,~RA,~RB,~PB,~RestB,~EA,~EB,~pathB,~injectB,~selectB,~identityB,ownedB),Family.branch(~S,~EA,~EB,~DA,~DB,~FA,~FB,~makeA,~makeB,~syncA,~syncB,~frameA,~frameB,~retainA,~retainB,~inventoryA,~inventoryB,provisionA,provisionB),Family.select_right(~S,~Nat,~FA,~FB,~takeB,~putB,selectionB)}
26	def under_resource(~S:Data,~User:Type,~R:Type,~P:Type,~Rest:Type,~E:Data,~D:Data,~F:Type,~path:Product.Lens<R,Log.Log<P>,Rest>,~inject:Nat -> E,~select:List<&2,E> -> List<&2,Nat>,~identity:Pub.Domain<S,P>,~make:D -> Nat -> F,~sync:F -> Nat -> List<&2,E> -> F,~frame:F -> Nat -> F,~retain:F -> Nat -> List<&2,E> -> F & List<&2,E>,~inventory:F -> F & List<&2,String>,~take:F -> F & Stream.Stream<S,Nat>,~put:F -> Stream.Stream<S,Nat> -> F,setup:Setup<S,R,P,Rest,E,D,F,path,inject,select,identity,make,sync,frame,retain,inventory,take,put>) -> Setup<S,Product.Owner<User,R>,P,User & Rest,E,D,F,Binding.right_path(~User,~R,~P,~Rest,~path),inject,select,identity,make,sync,frame,retain,inventory,take,put>:
27	  match setup:
28	    case Setup{owned,provision,selection}:Setup{Binding.under_resource(~S,~User,~R,~P,~Rest,~E,~path,~inject,~select,~identity,owned),provision,selection}