def indexed_success

bendtorch-core@0.1.0.0 · src/autograd/reduce_PROOF.bend:409

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce
import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend as MatmulProof

409def indexed_success(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan, output: Core.Tensor<target>,
410  +depth: Nat, +length: Nat, -valid: {Storage.bounds(depth, length) == True{} : Bool},
411  -exact: {length == Shape.logical_numel(Shape.dimensions(target)) : Nat},
412  map: Shape.Index<Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))>) ->
413  Laws.Success<Reduce.parallel_indexed(Core.Packed{shape, tensor}, target, plan, output, depth, length, valid, exact, map)>:
414  match map:
415    case Shape.Unindexed{zero}:
416      Laws.Success{{==}}
417    case Shape.Indexed{rows, same}:
418      MatmulProof.take_lift(shape, tensor, pair => Laws.Success<Reduce.parallel_rows(plan, target, depth, length, valid, exact, pair, rows)>,
419        kept => copy => taken => Laws.Success{{==}})