def indexed_retains

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

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/tensor/elementwise_totality.bend as Totality
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/elementwise_parallel_proof.bend as Parallel
import bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend as MatmulProof

174def indexed_retains(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan, output: Core.Tensor<target>,
175  +depth: Nat, +length: Nat, -valid: {Storage.bounds(depth, length) == True{} : Bool},
176  -exact: {length == Shape.logical_numel(Shape.dimensions(target)) : Nat},
177  map: Shape.Index<Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))>) ->
178  Laws.Retained<Core.Packed{shape, tensor}, Reduce.parallel_indexed(Core.Packed{shape, tensor}, target, plan, output, depth, length, valid, exact, map)>:
179  match map:
180    case Shape.Unindexed{zero}:
181      Laws.Retained{property => {==}}
182    case Shape.Indexed{rows, same}:
183      MatmulProof.take_lift(shape, tensor,
184        pair => Laws.Retained<Core.Packed{shape, tensor}, Reduce.parallel_rows(plan, target, depth, length, valid, exact, pair, rows)>,
185        kept => copy => taken => Laws.Retained{{\{Parallel.Taken: depth => balanced => reads => retained => retained} :
186          Parallel.Taken<Core.Packed{shape, tensor}, (Core.Packed{shape, kept}, copy)> -> Totality.SameSource(Core.Packed{shape, tensor}, Core.Packed{shape, kept})}(taken)})