1	# The bias reader instantiates the shared grouped source witness: each
2	# reduced output leaves the reader as it was.
3	import Base
4	import ../kernel_parameter_gradient.bend as Kernel
5	import ../traversal_grouped.bend as Grouped
6	import ./storage_witness.bend as ArrayWitness
7	import ./traversal_witness.bend as Witness
8	import ./grouped_source_witness.bend as GroupWitness
9	
10	def bias_evidence(-reader: Array<F32>) -> Data:
11	  ArrayWitness.ArrayWitness<F32,reader>
12	
13	def bias_cell(-reader: Array<F32>,context: Kernel.Context,position: Nat,source: bias_evidence(reader)) ->
14	  Witness.Sample<Array<F32>,F32,reader,Kernel.bias_at(reader,context,position)>:
15	  Witness.array_sample(~F32,reader,Kernel.bias_at(reader,context,position),ArrayWitness.observed(F32,reader,Kernel.bias_address(context,position),source))
16	
17	def image_tail(~Reader: Type,~read: Reader -> Kernel.Context -> Nat -> Reader & F32,-reader: Reader,-result: Reader & F32,
18	  +rest: Nat,+image: Nat,+element: Nat,+work: Kernel.Work,+ranges: List<&2,Grouped.Range>,
19	  head: Witness.Sample<Reader,F32,reader,result>,tail: Witness.Sample<Reader,List<&2,F32>,reader,Kernel.image_values(~Reader,~read,rest,image,element,work,ranges,reader)>) ->
20	  Witness.Sample<Reader,List<&2,F32>,reader,Kernel.image_tail(~Reader,result,reader => Kernel.image_values(~Reader,~read,rest,image,element,work,ranges,reader))>:
21	  Witness.Sample{value,equation} = head
22	  %Equal.sym(Reader & F32,result,(reader,value),equation) : Witness.Sample<Reader,List<&2,F32>,reader,Kernel.image_tail(~Reader,_,reader => Kernel.image_values(~Reader,~read,rest,image,element,work,ranges,reader))>
23	  GroupWitness.prepended(~Reader,reader,value,Kernel.image_values(~Reader,~read,rest,image,element,work,ranges,reader),tail)
24	
25	def images(~Reader: Type,~Evidence: @-reader: Reader -> Data,~read: Reader -> Kernel.Context -> Nat -> Reader & F32,
26	  ~preserves: @-reader: Reader -> @context: Kernel.Context -> @position: Nat -> Evidence(reader) -> Witness.Sample<Reader,F32,reader,read(reader,context,position)>,
27	  remaining: Nat,+image: Nat,+element: Nat,+work: Kernel.Work,+ranges: List<&2,Grouped.Range>,-reader: Reader,+source: Evidence(reader)) ->
28	  Witness.Sample<Reader,List<&2,F32>,reader,Kernel.image_values(~Reader,~read,remaining,image,element,work,ranges,reader)>:
29	  match remaining:
30	    case 0n: Witness.Sample{[],{==}}
31	    case 1n+ +rest:
32	      image_tail(~Reader,~read,reader,Grouped.run(~Reader,~Kernel.Context,~read,ranges,reader,Kernel.Context{work,image,element}),rest,1n+image,element,work,ranges,
33	        GroupWitness.run(~Reader,~Kernel.Context,~Evidence,~read,~preserves,ranges,reader,Kernel.Context{work,image,element},source),
34	        images(~Reader,~Evidence,~read,~preserves,rest,1n+image,element,work,ranges,reader,source))
35	
36	def element(~Reader: Type,~Evidence: @-reader: Reader -> Data,~read: Reader -> Kernel.Context -> Nat -> Reader & F32,
37	  ~preserves: @-reader: Reader -> @context: Kernel.Context -> @position: Nat -> Evidence(reader) -> Witness.Sample<Reader,F32,reader,read(reader,context,position)>,
38	  +work: Kernel.Work,+index: Nat,+ranges: List<&2,Grouped.Range>,-reader: Reader,source: Evidence(reader)) ->
39	  Witness.Sample<Reader,F32,reader,Kernel.element(~Reader,~read,work,index,ranges,reader)>:
40	  Kernel.Work{+count,c,o,h,w,k,s,p,rows,columns,g} = work
41	  GroupWitness.reduced(~Reader,reader,Kernel.image_values(~Reader,~read,count,0n,index,work,ranges,reader),images(~Reader,~Evidence,~read,~preserves,count,0n,index,work,ranges,reader,source))