def total_words

bendtorch-core@0.1.0.0 · src/tensor/contracts/sum_proof.bend:25

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
import bendtorch-core@0.1.0.0/src/tensor/reduction.bend as Reduction
import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
import bendtorch-core@0.1.0.0/src/tensor/contracts/fold.bend as Fold
import bendtorch-core@0.1.0.0/src/tensor/contracts/sum.bend as Sum
import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Laws

25def total_words(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +count: Nat) ->
26  {Fold.total(~Unit, ~Sum.add, ~Unit, ~Sum.position, ~Sum.every, Unit{}, Unit{}, shape, fill, ops, count) ==
27    Reduction.sequential_sum(Laws.words(shape, fill, ops, count), 0.0) : F32}:
28  match count:
29    case 0n:
30      {==}
31    case 1n+previous:
32      +word = Replayed.value(shape, fill, ops, U32.from_nat(previous))
33      %Equal.sym(F32, Reduction.sequential_sum(List.append(&2, F32, Laws.words(shape, fill, ops, previous), [word]), 0.0),
34        F32.add(Reduction.sequential_sum(Laws.words(shape, fill, ops, previous), 0.0), word),
35        sequential_snoc(Laws.words(shape, fill, ops, previous), word, 0.0)) :
36        {F32.add(Fold.total(~Unit, ~Sum.add, ~Unit, ~Sum.position, ~Sum.every, Unit{}, Unit{}, shape, fill, ops, previous), word) == _ : F32}
37      Equal.cong(F32, F32, total => F32.add(total, word),
38        Fold.total(~Unit, ~Sum.add, ~Unit, ~Sum.position, ~Sum.every, Unit{}, Unit{}, shape, fill, ops, previous),
39        Reduction.sequential_sum(Laws.words(shape, fill, ops, previous), 0.0),
40        total_words(shape, fill, ops, previous))