TensorVjpPROOF.frozen_factors: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF.bend as TensorVjpPROOF
Lines 792-818 of bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF.bend&start_line=792&end_line=818

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/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/sum_to_size_fold_PROOF.bend as SumToSizeFoldProof
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

# The pairs g^T @ x reads on the Second half of g and the Second half of x
# are the pairs on g and x themselves.
def frozen_factors(+row: Nat, +column: Nat, +inner: Nat, +rows: Nat, +columns: Nat,
  +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>,
  +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +count: Nat) ->
  {Contracts.product_factors(row, column, Matrix.Swapped{}, Matrix.Swapped{}, inner, rows, columns,
    shape, fill, Replayed.snoc(ops, StorageLaws.Second{}), left, left_fill, Replayed.snoc(left_ops, StorageLaws.Second{}), count) ==
    Contracts.product_factors(row, column, Matrix.Swapped{}, Matrix.Swapped{}, inner, rows, columns,
      shape, fill, ops, left, left_fill, left_ops, count) : List<&2, DotFold.Factors>}:
  match count:
    case 0n:
      {==}
    case 1n+previous:
      +g_cell = Matrix.read_index(Matrix.Swapped{}, inner, rows, row, previous)
      +x_cell = Matrix.read_index(Matrix.Swapped{}, inner, columns, column, previous)
      factors_snoc(
        Contracts.product_factors(row, column, Matrix.Swapped{}, Matrix.Swapped{}, inner, rows, columns,
          shape, fill, Replayed.snoc(ops, StorageLaws.Second{}), left, left_fill, Replayed.snoc(left_ops, StorageLaws.Second{}), previous),
        Contracts.product_factors(row, column, Matrix.Swapped{}, Matrix.Swapped{}, inner, rows, columns,
          shape, fill, ops, left, left_fill, left_ops, previous),
        Replayed.value(shape, fill, Replayed.snoc(ops, StorageLaws.Second{}), g_cell),
        Replayed.value(left, left_fill, Replayed.snoc(left_ops, StorageLaws.Second{}), x_cell),
        Replayed.value(shape, fill, ops, g_cell),
        Replayed.value(left, left_fill, left_ops, x_cell),
        frozen_factors(row, column, inner, rows, columns, shape, fill, ops, left, left_fill, left_ops, previous),
        SumToSizeFoldProof.half_keeps(shape, fill, ops, StorageLaws.Second{}, g_cell, {==}),
        SumToSizeFoldProof.half_keeps(left, left_fill, left_ops, StorageLaws.Second{}, x_cell, {==}))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/sum_to_size_fold_PROOF.bend&name=half_keeps
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF.bend&name=factors_snoc
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=Op
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend&name=product_factors
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend&name=snoc
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/dot_fold.bend&name=Factors
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=Order
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=read_index