def tensor_status

bendtorch-core@0.1.0.0 · src/tensor/reduction_PROOF.bend:488

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/reduction.bend as Reduction
import bendtorch-core@0.1.0.0/src/tensor/math_totality.bend as Totality
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage

488# The fold never fails.
489def tensor_status(-shape: Shape.Shape, +fuel: Nat, tensor: Core.Tensor<shape>) ->
490  Totality.Status<Core.Error, Core.Tensor<shape> & F32, Reduction.tensor_sum(shape, fuel, tensor)>:
491  Core.TTensor{storage, exact} = tensor
492  match storage:
493    case Storage.Empty{}:
494      Totality.Status{{==}}
495    case Storage.Owned{+depth, +length, array, balanced, valid}:
496      owned_status(shape, depth, length, array, balanced, valid, exact, Reduction.array_sum(fuel, 0n, 0.0, array),
497        Reduction.array_sum_keeps(depth, array, balanced, fuel, 0n, 0.0, array, {==}))