law permute_source_transposed

bendtorch-core@0.1.0.0 · src/tensor/transpose_LAWS.bend:31

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Values

31# The index map of a rank-2 transpose reads the transposed cell. For an input
32# of dimensions [rows, columns], output cell [j, l] of the [columns, rows]
33# transpose sits at j * rows + l, and `permute_source` with axes [1, 0] sends
34# it to input index l * columns + j, the input cell [l, j].
35law permute_source_transposed:
36  for +input: Shape.Shape
37  for +rows: U32
38  for +columns: U32
39  for matrix: {Shape.dimensions(input) == [rows, columns] : List<&2, U32>}
40  for +j: Nat
41  for j_below: {Nat.is_lt(j, U32.to_nat(columns)) == True{} : Bool}
42  for +l: Nat
43  for l_below: {Nat.is_lt(l, U32.to_nat(rows)) == True{} : Bool}
44  {Values.permute_source(input, [1, 0], U32.from_nat(Nat.add(Nat.mul(j, U32.to_nat(rows)), l))) ==
45    Some{U32.from_nat(Nat.add(Nat.mul(l, U32.to_nat(columns)), j))} : Maybe<&2, U32>}