1	import Base
2	import ../tensor_cursor.bend as Cursor
3	import ../traversal_array.bend as Traversal
4	import ./storage_witness.bend as Witness
5	import ./traversal_witness.bend as TraversalWitness
6	import ./traversal_visit_witness.bend as VisitWitness
7	
8	def read_value(~Element: Data,axes: Cursor.Levels(),address: U32,-storage: Array<Element>,-result: Array<Element> & Element,
9	  observed: Witness.Read<Element,storage,result>) ->
10	  VisitWitness.Sample<Array<Element>,Element,Cursor.Cursor,storage,Cursor.read_value(~Element,axes,address,result)>:
11	  match observed:
12	    case Witness.Read{value,equation}:
13	      %Equal.sym(Array<Element> & Element,result,(storage,value),equation) :
14	        VisitWitness.Sample<Array<Element>,Element,Cursor.Cursor,storage,Cursor.read_value(~Element,axes,address,_)>
15	      VisitWitness.Sample{Cursor.advance(axes,address),value,{==}}
16	
17	def read(~Element: Data,-storage: Array<Element>,cursor: Cursor.Cursor,evidence: Witness.ArrayWitness<Element,storage>) ->
18	  VisitWitness.Sample<Array<Element>,Element,Cursor.Cursor,storage,Cursor.read(~Element,storage,cursor)>:
19	  Cursor.Cursor{axes,+address} = cursor
20	  read_value(~Element,axes,address,storage,Array.get(Element,storage,address),Witness.observed(Element,storage,address,evidence))
21	
22	def stride_value(~Element: Data,address: U32,+stride: U32,-storage: Array<Element>,-result: Array<Element> & Element,
23	  observed: Witness.Read<Element,storage,result>) ->
24	  VisitWitness.Sample<Array<Element>,Element,Cursor.Stride,storage,Cursor.stride_value(~Element,address,stride,result)>:
25	  match observed:
26	    case Witness.Read{value,equation}:
27	      %Equal.sym(Array<Element> & Element,result,(storage,value),equation) :
28	        VisitWitness.Sample<Array<Element>,Element,Cursor.Stride,storage,Cursor.stride_value(~Element,address,stride,_)>
29	      VisitWitness.Sample{Cursor.Stride{(address + stride : U32),stride},value,{==}}
30	
31	def read_stride(~Element: Data,-storage: Array<Element>,cursor: Cursor.Stride,evidence: Witness.ArrayWitness<Element,storage>) ->
32	  VisitWitness.Sample<Array<Element>,Element,Cursor.Stride,storage,Cursor.read_stride(~Element,storage,cursor)>:
33	  Cursor.Stride{+address,+stride} = cursor
34	  stride_value(~Element,address,stride,storage,Array.get(Element,storage,address),Witness.observed(Element,storage,address,evidence))