def empty_values

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

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

375# A tensor with no storage holds no word.
376def empty_values(-shape: Shape.Shape, -exact: {0n == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, fuel: Nat, +cursor: Nat,
377  values: List<&2, F32>,
378  logical: Laws.LogicalValues(fuel, shape, Core.TTensor{Storage.Empty{}, exact}, cursor, values)) ->
379  Fact<{0.0 == Reduction.sequential_sum(values, 0.0) : F32}>:
380  match fuel values:
381    case 0n Nil{}:
382      Fact{{==}}
383    case 1n+rest +value <> others:
384      Laws.LogicalStep{index_exact, observed, remaining} = logical
385      Fact{Empty.absurd({0.0 == Reduction.sequential_sum(value <> others, 0.0) : F32}, no_value(value, observed))}
386    case 0n value <> others:
387      Empty.absurd(Fact<{0.0 == Reduction.sequential_sum(value <> others, 0.0) : F32}>, logical)
388    case 1n+rest Nil{}:
389      Empty.absurd(Fact<{0.0 == Reduction.sequential_sum(Nil{}, 0.0) : F32}>, logical)