kernel_block.bend

stelliferous@0.0.3.0 · 33 lines · 0 definitions

1import Base
2
3# A statically shaped product. Pairing readers preserves one buffer owner.
4type Twin<-Element: Data> is Data:
5  Twin{first: Element,second: Element}
6
7def finish_pair(~State: Type,~Element: Data,first: Element,result: State & Element) -> State & Twin<Element>:
8  (state,second) = result
9  (state,Twin{first,second})
10
11def read_second(
12  ~State: Type,~Context: Data,~Element: Data,~Index: Data,
13  ~read: State -> Context -> Index -> State & Element,
14  result: State & Element,context: Context,index: Index
15) -> State & Twin<Element>:
16  (state,first) = result
17  finish_pair(~State,~Element,first,read(state,context,index))
18
19def read_at(
20  ~State: Type,~Context: Data,~Element: Data,~Index: Data,
21  ~read: State -> Context -> Index -> State & Element,
22  state: State,+context: Context,first: Index,second: Index
23) -> State & Twin<Element>:
24  read_second(~State,~Context,~Element,~Index,~read,read(state,context,first),context,second)
25
26def read_pair(
27  ~State: Type,~Context: Data,~Element: Data,
28  ~read: State -> Context -> Nat -> State & Element,~stride: Nat,
29  state: State,context: Context,index: Nat
30) -> State & Twin<Element>:
31  +context = context
32  +index = index
33  read_at(~State,~Context,~Element,~Nat,~read,state,context,index,Nat.add(index,stride))