type MatmulSoleContract

bendtorch-core@0.1.0.0 · src/autograd/tensor_vjp_LAWS.bend:389

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend as Backward
import bendtorch-core@0.1.0.0/src/autograd/tensor_backward_LAWS.bend as TensorBackward

389# What a VJP that sends one contribution of a matrix promises: it goes to node
390# b with target's dimensions and holds cell(row, column) at row * columns +
391# column for every row < rows and column < columns.
392type MatmulSoleContract<-b: Nat, -target: Shape.Shape, -rows: Nat, -columns: Nat, -cell: Nat -> Nat -> F32,
393  -pass: Backward.Pass> is Type:
394  MatmulSoleContract{
395    target_id: {TensorBackward.sole_target(TensorBackward.sole(pass)) == Some{b} : Maybe<&2, Nat>},
396    dimensions: {TensorBackward.sole_dimensions(TensorBackward.sole(pass)) == Some{Shape.dimensions(target)} : Maybe<&2, List<&2, U32>>},
397    value: @+row: Nat -> @row_below: {Nat.is_lt(row, rows) == True{} : Bool} ->
398      @+column: Nat -> @column_below: {Nat.is_lt(column, columns) == True{} : Bool} ->
399      {TensorBackward.sole_point(TensorBackward.sole(pass), U32.from_nat(Nat.add(Nat.mul(row, columns), column))) ==
400        Some{cell(row, column)} : Maybe<&2, F32>}}