def lanes

stelliferous@0.0.2.0 · tensor_operations.bend:127

import Base
import stelliferous@0.0.2.0/storage_buffer.bend as Storage
import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate
import stelliferous@0.0.2.0/traversal_lanes.bend as Lanes
import stelliferous@0.0.2.0/proofs/traversal_lanes_certificate.bend as LanesCertificate

127# The same map with the values of each round of eight computed together: an
128# operation written with FP32 arithmetic alone then compiles to vector code.
129# The certificate's depth decides whether the array holds the positions.
130def lanes(~Context: Data,~operation: Context -> F32 -> F32,+count: Nat,+position: U32,+context: Context,buffer: Storage.Buffer<F32>) -> Storage.Buffer<F32>:
131  Storage.Buffer{storage,length,Certificate.Certificate{+depth,equation}} = buffer
132  Storage.Buffer{Lanes.map_when(~Context,~operation,Lanes.covered(depth,position,count),count,position,context,storage),length,
133    LanesCertificate.map_when(~Context,~operation,Lanes.covered(depth,position,count),count,position,context,storage,Certificate.Certificate{depth,equation})}