1	import Base
2	import ../shape/core.bend as Shape
3	import ./axis_spec.bend as Axis
4	import ./layout.bend as Layout
5	import ./transpose_spec.bend as Transpose
6	import ./observation.bend as Values
7	
8	law transpose_axes_requested:
9	  for +shape: Shape.Shape
10	  for +a: U32
11	  for +b: U32
12	  for +inside: {True{} == Transpose.valid(shape, a, b) : Bool}
13	  {Layout.transpose_axes(Shape.dimensions(shape), a, b, 0) ==
14	    Transpose.requested_axes(Shape.rank_dimensions(Shape.dimensions(shape)), U32.to_nat(a), U32.to_nat(b)) : List<&2, U32>}
15	
16	law transpose_axes_valid:
17	  for +shape: Shape.Shape
18	  for +a: U32
19	  for +b: U32
20	  for +inside: {True{} == Transpose.valid(shape, a, b) : Bool}
21	  {True{} == Layout.bijective(shape, Layout.transpose_axes(Shape.dimensions(shape), a, b, 0)) : Bool}
22	
23	law transpose_axes_self_inverse:
24	  for +shape: Shape.Shape
25	  for +a: U32
26	  for +b: U32
27	  for +inside: {True{} == Transpose.valid(shape, a, b) : Bool}
28	  {Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.naturals(Layout.transpose_axes(Shape.dimensions(shape), a, b, 0))) ==
29	    Shape.naturals(Layout.transpose_axes(Shape.dimensions(shape), a, b, 0)) : List<&2, Nat>}
30	
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].
35	law 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>}