src/tensor/axis_LAWS.bend
bendtorch-core@0.1.0.0 · 157 lines · 20 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
4import bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend as Axis
5import bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend as Algebra
6
7def axis_plan_succeeded(-shape: Shape.Shape, -axes: List<&2, U32>, result: Result<&2, &2, Layout.Error, Layout.Plan<shape, axes>>) -> Bool:
8 match result:
9 case Fail{error}:
10 False{}
11 case Done{plan}:
12 True{}
13
14law axis_lookup_refines:
15 for +items: List<&2, U32>
16 for +index: Nat
17 {Layout.lookup(items, index) == Axis.lookup(U32, items, index) : Maybe<&2, U32>}
18
19law axis_gather_refines:
20 for +axes: List<&2, U32>
21 for +items: List<&2, U32>
22 {Layout.reorder(items, axes) == Axis.gather(U32, items, Shape.naturals(axes)) : Maybe<&2, List<&2, U32>>}
23
24law axis_scatter_refines:
25 for +shape: Shape.Shape
26 for +axes: List<&2, U32>
27 for +coordinates: List<&2, U32>
28 {Layout.inverse_coordinates(Shape.dimensions(shape), axes, coordinates, 0) ==
29 Axis.scatter(U32, Shape.rank_dimensions(Shape.dimensions(shape)), Shape.naturals(axes), coordinates, 0n) : Maybe<&2, List<&2, U32>>}
30
31law axis_validity_refines:
32 for +shape: Shape.Shape
33 for +axes: List<&2, U32>
34 for accepted: {True{} == Layout.bijective(shape, axes) : Bool}
35 {True{} == Axis.valid(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.naturals(axes)) : Bool}
36
37law axis_lookup_complete:
38 for -A: Data
39 for +items: List<&2, A>
40 for +index: Nat
41 for bound: Shape.LT(index, List.length(&2, A, items))
42 Algebra.Selected<A, items, index>
43
44law axis_permutation_complete:
45 for +shape: Shape.Shape
46 for +axes: List<&2, U32>
47 for accepted: {True{} == Layout.bijective(shape, axes) : Bool}
48 {Layout.reorder(Shape.dimensions(shape), axes) == Some{Axis.order(U32, Shape.dimensions(shape), Shape.naturals(axes))} : Maybe<&2, List<&2, U32>>}
49
50law axis_permutation_rejects:
51 for +shape: Shape.Shape
52 for +axes: List<&2, U32>
53 for rejected: {False{} == Layout.bijective(shape, axes) : Bool}
54 {axis_plan_succeeded(shape, axes, Layout.permutation(shape, axes)) == False{} : Bool}
55
56law axis_dimension_rank:
57 for +shape: Shape.Shape
58 for +axes: List<&2, U32>
59 for accepted: {True{} == Layout.bijective(shape, axes) : Bool}
60 {Shape.rank_dimensions(Axis.order(U32, Shape.dimensions(shape), Shape.naturals(axes))) == Shape.rank_dimensions(Shape.dimensions(shape)) : Nat}
61
62law axis_dimension_product:
63 for +shape: Shape.Shape
64 for +axes: List<&2, U32>
65 for accepted: {True{} == Layout.bijective(shape, axes) : Bool}
66 {Shape.logical_numel(Axis.order(U32, Shape.dimensions(shape), Shape.naturals(axes))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}
67
68law axis_scatter_complete:
69 for +shape: Shape.Shape
70 for +axes: List<&2, U32>
71 for +coordinates: List<&2, U32>
72 for accepted: {True{} == Layout.bijective(shape, axes) : Bool}
73 for length: {Shape.rank_dimensions(coordinates) == Shape.rank_dimensions(Shape.dimensions(shape)) : Nat}
74 {Layout.inverse_coordinates(Shape.dimensions(shape), axes, coordinates, 0) ==
75 Some{Axis.order(U32, coordinates, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.naturals(axes)))} : Maybe<&2, List<&2, U32>>}
76
77law axis_scatter_gather:
78 for +shape: Shape.Shape
79 for +axes: List<&2, U32>
80 for +coordinates: List<&2, U32>
81 for accepted: {True{} == Layout.bijective(shape, axes) : Bool}
82 for length: {Shape.rank_dimensions(coordinates) == Shape.rank_dimensions(Shape.dimensions(shape)) : Nat}
83 {Layout.inverse_coordinates(Shape.dimensions(shape), axes, Axis.order(U32, coordinates, Shape.naturals(axes)), 0) == Some{coordinates} : Maybe<&2, List<&2, U32>>}
84
85law axis_inverse_valid:
86 for +rank: Nat
87 for +axes: List<&2, Nat>
88 for bound: Shape.LE(rank, 4n)
89 for accepted: {True{} == Axis.valid(rank, axes) : Bool}
90 {True{} == Axis.valid(rank, Axis.inverse_axes(rank, axes)) : Bool}
91
92law axis_inverse_selected:
93 for +rank: Nat
94 for +axes: List<&2, Nat>
95 for bound: Shape.LE(rank, 4n)
96 for accepted: {True{} == Axis.valid(rank, axes) : Bool}
97 {Axis.inverse(rank, axes) == Some{Axis.inverse_axes(rank, axes)} : Maybe<&2, List<&2, Nat>>}
98
99law axis_inverse_involution:
100 for +rank: Nat
101 for +axes: List<&2, Nat>
102 for bound: Shape.LE(rank, 4n)
103 for accepted: {True{} == Axis.valid(rank, axes) : Bool}
104 {Axis.inverse_axes(rank, Axis.inverse_axes(rank, axes)) == axes : List<&2, Nat>}
105
106law axis_inverse_list_composition:
107 for -A: Data
108 for +rank: Nat
109 for +axes: List<&2, Nat>
110 for +items: List<&2, A>
111 for bound: Shape.LE(rank, 4n)
112 for accepted: {True{} == Axis.valid(rank, axes) : Bool}
113 for length: {List.length(&2, A, items) == rank : Nat}
114 {Axis.order(A, Axis.order(A, items, axes), Axis.inverse_axes(rank, axes)) == items : List<&2, A>}
115
116law axis_inverse_reverse_composition:
117 for -A: Data
118 for +rank: Nat
119 for +axes: List<&2, Nat>
120 for +items: List<&2, A>
121 for bound: Shape.LE(rank, 4n)
122 for accepted: {True{} == Axis.valid(rank, axes) : Bool}
123 for length: {List.length(&2, A, items) == rank : Nat}
124 {Axis.order(A, Axis.order(A, items, Axis.inverse_axes(rank, axes)), axes) == items : List<&2, A>}
125
126law axis_inverse_scatter_composition:
127 for -A: Data
128 for +rank: Nat
129 for +axes: List<&2, Nat>
130 for +items: List<&2, A>
131 for +bound: Shape.LE(rank, 4n)
132 for +accepted: {True{} == Axis.valid(rank, axes) : Bool}
133 for length: {List.length(&2, A, items) == rank : Nat}
134 {Axis.scatter(A, rank, Axis.inverse_axes(rank, axes), Axis.order(A, items, Axis.inverse_axes(rank, axes)), 0n) == Some{items} : Maybe<&2, List<&2, A>>}
135
136law axis_coordinate_fit:
137 for +rank: Nat
138 for +axes: List<&2, Nat>
139 for +dimensions: List<&2, Nat>
140 for +coordinates: List<&2, Nat>
141 for bound: Shape.LE(rank, 4n)
142 for accepted: {True{} == Axis.valid(rank, axes) : Bool}
143 for dimensions_length: {List.length(&2, Nat, dimensions) == rank : Nat}
144 for coordinates_length: {List.length(&2, Nat, coordinates) == rank : Nat}
145 {Shape.fit(Axis.order(Nat, dimensions, axes), Axis.order(Nat, coordinates, axes)) == Shape.fit(dimensions, coordinates) : Bool}
146
147law axis_scatter_fit:
148 for +rank: Nat
149 for +axes: List<&2, Nat>
150 for +dimensions: List<&2, Nat>
151 for +coordinates: List<&2, Nat>
152 for +bound: Shape.LE(rank, 4n)
153 for +accepted: {True{} == Axis.valid(rank, axes) : Bool}
154 for +dimensions_length: {List.length(&2, Nat, dimensions) == rank : Nat}
155 for coordinates_length: {List.length(&2, Nat, coordinates) == rank : Nat}
156 for fits: {True{} == Shape.fit(Axis.order(Nat, dimensions, axes), coordinates) : Bool}
157 {True{} == Shape.fit(dimensions, Axis.order(Nat, coordinates, Axis.inverse_axes(rank, axes))) : Bool}