1	import Base
2	import ../kernel_block.bend as Block
3	
4	def read_at_refines(
5	  ~Native: Type,~Context: Data,~Element: Data,~Index: Data,
6	  ~read: Native -> Context -> Index -> Native & Element,
7	  -source: Native,+context: Context,+first: Index,+second: Index,+left: Element,+right: Element,
8	  first_read: {read(source,context,first) == (source,left) : Native & Element},
9	  second_read: {read(source,context,second) == (source,right) : Native & Element}
10	) -> {Block.read_at(~Native,~Context,~Element,~Index,~read,source,context,first,second) ==
11	  (source,Block.Twin{left,right}) : Native & Block.Twin<Element>}:
12	  %Equal.sym(Native & Element,read(source,context,first),(source,left),first_read) :
13	    {Block.read_second(~Native,~Context,~Element,~Index,~read,_,context,second) ==
14	      (source,Block.Twin{left,right}) : Native & Block.Twin<Element>}
15	  %Equal.sym(Native & Element,read(source,context,second),(source,right),second_read) :
16	    {Block.finish_pair(~Native,~Element,left,_) == (source,Block.Twin{left,right}) : Native & Block.Twin<Element>}
17	  {==}
18	
19	# Pair composition is independent of element shape and block width.
20	def pair_sample(
21	  ~Model: Data,~Context: Data,~Element: Data,
22	  ~sample: Model -> Context -> Nat -> Element,~stride: Nat,
23	  model: Model,context: Context,index: Nat
24	) -> Block.Twin<Element>:
25	  +model = model
26	  +context = context
27	  +index = index
28	  Block.Twin{sample(model,context,index),sample(model,context,Nat.add(index,stride))}
29	
30	def read_pair_refines(
31	  ~Native: Type,~Model: Data,~Context: Data,~Element: Data,
32	  ~pack: Model -> Native,
33	  ~read: Native -> Context -> Nat -> Native & Element,
34	  ~sample: Model -> Context -> Nat -> Element,
35	  ~stride: Nat,+model: Model,+context: Context,+index: Nat,
36	  first_read: {read(pack(model),context,index) == (pack(model),sample(model,context,index)) : Native & Element},
37	  second_read: {read(pack(model),context,Nat.add(index,stride)) == (pack(model),sample(model,context,Nat.add(index,stride))) : Native & Element}
38	) -> {Block.read_pair(~Native,~Context,~Element,~read,~stride,pack(model),context,index) == (pack(model),pair_sample(~Model,~Context,
39	    ~Element,~sample,~stride,model,context,index)) : Native & Block.Twin<Element>}:
40	  read_at_refines(~Native,~Context,~Element,~Nat,~read,pack(model),context,index,Nat.add(index,stride),
41	    sample(model,context,index),sample(model,context,Nat.add(index,stride)),first_read,second_read)