def tensor_value

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

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/reduction_LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage

407# The array fold of `Reduction.sum` adds the tensor's words in index order
408# from +0.0.
409def tensor_value(-shape: Shape.Shape, +fuel: Nat, tensor: Core.Tensor<shape>, +values: List<&2, F32>,
410  logical: Laws.LogicalValues(fuel, shape, tensor, 0n, values)) ->
411  Fact<{Laws.loop_value(shape, Reduction.tensor_sum(shape, fuel, tensor)) == Some{Reduction.sequential_sum(values, 0.0)} : Maybe<&2, F32>}>:
412  Core.TTensor{storage, exact} = tensor
413  match storage:
414    case Storage.Empty{}:
415      Fact{Equal.cong(F32, Maybe<&2, F32>, x => Some{x}, 0.0, Reduction.sequential_sum(values, 0.0),
416        {\{Fact: p => p} : Fact<({0.0 == Reduction.sequential_sum(values, 0.0) : F32})> -> {0.0 == Reduction.sequential_sum(values, 0.0) : F32}}(
417          empty_values(shape, exact, fuel, 0n, values, logical)))}
418    case Storage.Owned{+depth, +length, array, balanced, valid}:
419      owned_value(shape, depth, length, array, balanced, valid, exact, fuel, values, logical, Reduction.array_sum(fuel, 0n, 0.0, array),
420        Reduction.array_sum_keeps(depth, array, balanced, fuel, 0n, 0.0, array, {==}), {==})