def nt_factors

bendtorch-core@0.1.0.0 · src/autograd/tensor_vjp_PROOF.bend:987

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/word_conversion.bend as Conversion
import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Contracts
import bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix
import bendtorch-core@0.1.0.0/src/tensor/dot_fold.bend as DotFold
import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Values

987def nt_factors(+row: Nat, +column: Nat, +rows: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
988  +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +columns: U32, +inner: U32,
989  +matrix: {Shape.dimensions(right) == [columns, inner] : List<&2, U32>},
990  +column_below: {Nat.is_lt(column, U32.to_nat(columns)) == True{} : Bool},
991  +count: Nat, +room: {Nat.is_le(count, U32.to_nat(inner)) == True{} : Bool}) ->
992  {Contracts.product_factors(row, column, Matrix.Kept{}, Matrix.Kept{}, U32.to_nat(inner), rows, U32.to_nat(columns),
993    left, left_fill, left_ops, right, right_fill, right_ops, count) ==
994    Laws.right_transposed_factors(row, column, U32.to_nat(inner), U32.to_nat(columns), left, left_fill, left_ops,
995      right, right_fill, right_ops, Laws.swapped(right), count) : List<&2, DotFold.Factors>}:
996  match count:
997    case 0n:
998      {==}
999    case 1n+previous:
1000      +span = U32.to_nat(inner)
1001      +across = U32.to_nat(columns)
1002      factors_snoc(
1003        Contracts.product_factors(row, column, Matrix.Kept{}, Matrix.Kept{}, span, rows, across,
1004          left, left_fill, left_ops, right, right_fill, right_ops, previous),
1005        Laws.right_transposed_factors(row, column, span, across, left, left_fill, left_ops,
1006          right, right_fill, right_ops, Laws.swapped(right), previous),
1007        Replayed.value(left, left_fill, left_ops, U32.from_nat(Nat.add(Nat.mul(row, span), previous))),
1008        Replayed.value(right, right_fill, right_ops, U32.from_nat(Nat.add(Nat.mul(column, span), previous))),
1009        Replayed.value(left, left_fill, left_ops, U32.from_nat(Nat.add(Nat.mul(row, span), previous))),
1010        Replayed.value(right, right_fill, right_ops,
1011          U32.from_nat(Values.permute_source_index(right, Laws.swapped(right), Nat.add(Nat.mul(previous, across), column)))),
1012        nt_factors(row, column, rows, left, left_fill, left_ops, right, right_fill, right_ops, columns, inner, matrix,
1013          column_below, previous, Conversion.le_predecessor(previous, span, room)),
1014        {==},
1015        nt_word(right, right_fill, right_ops, columns, inner, matrix, column, column_below, previous,
1016          Conversion.le_successor_lt(previous, span, room)))