def mapped

stelliferous@0.0.2.0 · tensor_operations.bend:120

import Base
import stelliferous@0.0.2.0/storage_buffer.bend as Storage
import stelliferous@0.0.2.0/traversal_array.bend as Traversal
import stelliferous@0.0.2.0/tensor_access.bend as Access
import stelliferous@0.0.2.0/proofs/traversal_certificate.bend as TraversalCertificate

120# A mapper is the ordered map of count values from position on a certified
121# Buffer. mapped applies the operation to one value at a time.
122def mapped(~Element: Data,~operation: Element -> Element,+count: Nat,+position: U32,buffer: Storage.Buffer<Element>) -> Storage.Buffer<Element>:
123  Storage.Buffer{storage,length,certificate} = buffer
124  Storage.Buffer{Traversal.map_in_place(~Element,~Unit,~Access.apply_element(~Element,~operation),count,position,Unit{},storage),length,
125    TraversalCertificate.map_in_place(~Element,~Unit,~Access.apply_element(~Element,~operation),count,position,Unit{},storage,certificate)}