def gather

stelliferous@0.0.2.0 · proofs/traversal_lanes_certificate.bend:71

import Base
import stelliferous@0.0.2.0/kernel_tile.bend as Tile
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness
import stelliferous@0.0.2.0/traversal_lanes.bend as Lanes
import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate
import stelliferous@0.0.2.0/proofs/traversal_lanes_witness.bend as LanesWitness

71def gather(~Context: Data,~map: Context -> F32 -> F32,-values: Array<F32>,+position: U32,+context: Context,
72  certificate: Certificate.Certificate<F32,values>) ->
73  Certificate.Certificate<F32,TraversalWitness.first(~Array<F32>,~Tile.Tile8,Lanes.gather(~Context,~map,values,position,context))>:
74  Certificate.Certificate{+depth,+equation} = certificate
75  %Equal.sym(Array<F32>,TraversalWitness.first(~Array<F32>,~Tile.Tile8,Lanes.gather(~Context,~map,values,position,context)),values,
76    gathered_owner(~Context,~map,values,position,context,
77      LanesWitness.gather(~Context,~map,depth,values,position,context,Certificate.witness_at(F32,depth,values,equation)))) :
78    Certificate.Certificate<F32,_>
79  Certificate.Certificate{depth,equation}