def wrap_pixel

stelliferous@0.0.2.0 · proofs/kernel_packing_read_witness.bend:39

import Base
import stelliferous@0.0.2.0/kernel_spatial_packing.bend as Packing
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness

39def wrap_pixel(same: Bool,-input: Array<F32>,+row: U32,+column: U32,+channel: U32,+height: U32,+width: U32,+stride: U32,+next_row: U32,+offset: U32,+output_width: U32,+kernel_column: U32,+padding: U32,+lane: U32,evidence: family(input)) ->
40  TraversalWitness.Sample<Array<F32>,F32,input,Packing.wrap_pixel(same,input,row,column,channel,height,width,stride,next_row,offset,output_width,kernel_column,padding,lane)>:
41  match same:
42    case True{}: pixel(input,row,(column + lane * stride : U32),channel,height,width,evidence)
43    case False{}: pixel(input,next_row,((offset + lane - output_width) * stride + kernel_column - padding : U32),channel,height,width,evidence)