ordinary_owned_event_binding.bend
bendvy-ecs-core@0.1.0.0 · 41 lines · 0 definitions
1import Base
2import bendvy-ecs-core@0.1.0.0/relation_commands.bend as Relation
3import bendvy-ecs-core@0.1.0.0/owner_product.bend as Product
4import bendvy-ecs-core@0.1.0.0/owned_event_log.bend as Log
5import bendvy-ecs-core@0.1.0.0/owned_event_key_route.bend as Route
6import bendvy-ecs-core@0.1.0.0/event_publication.bend as Publication
7import bendvy-ecs-core@0.1.0.0/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.
12type 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{}
14def identity_take(~T:Type,owner:T) -> Unit & T:(Unit{},owner)
15def identity_put(~T:Type,unit:Unit,owner:T) -> T:owner
16def identity_lens(~T:Type) -> Product.Lens<T,T,Unit>:
17 Product.Lens{identity_take(~T),identity_put(~T)}
18def 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{}
20def 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)
22def 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)
24def 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{}
26def 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{}
28def 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.
32def notice_inject(~S:Data,~E:Data,~inject:Nat -> E,id:Nat) -> Relation.Notice<S,E>:Relation.Original{inject(id)}
33def 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)
38def 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))
40def 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{}