def band_geometry

stelliferous@0.0.2.0 · tensor_window.bend:99

import Base
import stelliferous@0.0.2.0/tensor_shape.bend as Shapes
import stelliferous@0.0.2.0/tensor_access.bend as Access
import stelliferous@0.0.2.0/tensor_operations.bend as Operations
import stelliferous@0.0.2.0/tensor.bend as Tensors
import stelliferous@0.0.2.0/tensor_band.bend as Bands

99def band_geometry(~Element: Data,~operation: Element -> Element -> Element,name: String,pad: Element,+pool: Access.Pool,+geometry: Bands.Geometry,bands: Bands.Bands(~Element),
100  +shape: List<&2,U32>,fill: Element,workers: U32) -> Tensors.Tensor<Element>:
101  Access.Pool{+height,+width,+kernel,+stride,+padding,+out_height,+out_width} = pool
102  +pool = {Access.Pool{height,width,kernel,stride,padding,out_height,out_width} : Access.Pool}
103  +out_shape = List.append(&2,U32,List.take(&2,U32,shape,Nat.sub(List.length(&2,U32,shape),2n)),[out_height,out_width])
104  band_count(~Element,~operation,name,band_shape(shape,geometry) && Operations.pool_geometry(pool) && U32.is_lt(0,height) && U32.is_lt(0,width) &&
105    Bool.not(Shapes.has_zero(out_shape)),Tensors.count_of(middle_shape(shape,pool)),Tensors.count_of(out_shape),pad,pool,geometry,bands,shape,out_shape,fill,workers)