def tile_step

stelliferous@0.0.2.0 · proofs/kernel_packing_witness.bend:203

import Base
import stelliferous@0.0.2.0/kernel_spatial_packing.bend as Packing
import stelliferous@0.0.2.0/proofs/kernel_packing_read_witness.bend as PackingReadWitness

203def tile_step(+depth: Nat,-input: Array<F32>,-state: Packing.Tiled(),+input_evidence: PackingReadWitness.family(input),evidence: TileEvidence<input,depth,state>) ->
204  TileEvidence<input,depth,Packing.tile_step(state)>:
205  TileEvidence{output,cursor,equation,balanced} = evidence
206  TileCursor{+i,+position,+h,+w,+k,+s,+p,+ow,+channels,+taps,+inner} = cursor
207  %Equal.sym(Packing.Tiled(),state,restore_tiles(input,output,TileCursor{i,position,h,w,k,s,p,ow,channels,taps,inner}),equation) : TileEvidence<input,depth,Packing.tile_step(_)>
208  tile(depth,U32.is_le((position % ow + 8 : U32),ow),U32.is_le((position % ow + 8 : U32),(ow + ow : U32)),input,output,i,position,h,w,k,s,p,ow,channels,taps,inner,input_evidence,balanced)