def reduced

stelliferous@0.0.2.0 · proofs/tensor_access_certificate.bend:253

import Base
import stelliferous@0.0.2.0/tensor_view.bend as Views
import stelliferous@0.0.2.0/traversal_array.bend as Traversal
import stelliferous@0.0.2.0/tensor_cursor.bend as Cursor
import stelliferous@0.0.2.0/proofs/tensor_cursor_witness.bend as CursorWitness
import stelliferous@0.0.2.0/proofs/traversal_visit_witness.bend as VisitWitness
import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness

253def reduced(~Element: Data,~Accumulator: Data,~operation: Accumulator -> Element -> Accumulator,
254  call: ReduceCall,-storage: Array<Element>,-initial: Accumulator,certificate: Certificate.Certificate<Element,storage>) ->
255  {TraversalWitness.first(~Array<Element>,~Accumulator,reduce_operation(~Element,~Accumulator,~operation,call,storage,initial)) == storage : Array<Element>}:
256  match call:
257    case ReduceCall{True{},count,Views.View{axes,offset}}:
258      TraversalWitness.fold(~Array<Element>,~Element,~Accumulator,~Traversal.Offsets,~TraversalWitness.array_evidence(~Element),~Traversal.source_offset(~Element),~operation,~TraversalWitness.offset_read(~Element),
259        count,storage,0,Traversal.Offsets{offset,0},initial,Certificate.witness(Element,storage,certificate))
260    case ReduceCall{False{},count,view}:
261      TraversalWitness.fold_finished(~Array<Element>,~Accumulator,~Cursor.Cursor,storage,
262        Traversal.visit_fold(~Array<Element>,~Element,~Accumulator,~Cursor.Cursor,~Cursor.read(~Element),~operation,count,Traversal.State{storage,initial,0,Cursor.prepare(view)}),
263        VisitWitness.fold_run(~Array<Element>,~Element,~Accumulator,~Cursor.Cursor,~TraversalWitness.array_evidence(~Element),~Cursor.read(~Element),~operation,~CursorWitness.read(~Element),
264          count,storage,Traversal.State{storage,initial,0,Cursor.prepare(view)},Certificate.witness(Element,storage,certificate),
265          TraversalWitness.FoldEvidence{initial,0,Cursor.prepare(view),{==}}))