src/tensor/permutation_mapping.bend
bendtorch-core@0.1.0.0 · 750 lines · 65 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/lifecycle.bend as Lifecycle
5import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
6import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as Coordinates
7import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
8import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as WordConversion
9import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as ShapeLaws
10import bendtorch-core@0.1.0.0/src/shape/PROOF.bend as ShapeProof
11import bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend as Axis
12import bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend as AxisAlgebra
13
14def permutation_checked(+input: Shape.Shape, +axes: List<&2, U32>, plan: Layout.Plan<input, axes>) ->
15 {True{} == Layout.bijective(input, axes) : Bool}:
16 Layout.Permutation{out, valid, ordered, count} = plan
17 valid
18
19def and_left(a: Bool, -b: Bool, equal: {True{} == Bool.and(a, b) : Bool}) -> {True{} == a : Bool}:
20 match a:
21 case False{}:
22 equal
23 case True{}:
24 {==}
25
26def and_right(a: Bool, -b: Bool, equal: {True{} == Bool.and(a, b) : Bool}) -> {True{} == b : Bool}:
27 match a:
28 case False{}:
29 Empty.absurd({True{} == b : Bool}, Lifecycle.false_true(equal))
30 case True{}:
31 equal
32
33def reverse_go_cancel(+values: List<&2, U32>, +accumulator: List<&2, U32>) ->
34 {Layout.reverse_words_go(Layout.reverse_words_go(values, accumulator), Nil{}) ==
35 Layout.reverse_words_go(accumulator, values) : List<&2, U32>}:
36 match values:
37 case Nil{}:
38 {==}
39 case +head <> +tail:
40 reverse_go_cancel(tail, head <> accumulator)
41
42def reverse_involution(+values: List<&2, U32>) -> {Layout.reverse_words(Layout.reverse_words(values)) == values : List<&2, U32>}:
43 reverse_go_cancel(values, Nil{})
44
45def codec_decoded(+dimensions: List<&2, U32>, +index: U32) ->
46 {Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(dimensions), index)) ==
47 Shape.words(Shape.digits(Shape.naturals(dimensions), U32.to_nat(index))) : List<&2, U32>}:
48 Equal.trans(List<&2, U32>, Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(dimensions), index)),
49 Shape.words(Shape.digits_words(dimensions, U32.to_nat(index))),
50 Shape.words(Shape.digits(Shape.naturals(dimensions), U32.to_nat(index))),
51 Equal.trans(List<&2, U32>, Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(dimensions), index)),
52 Layout.reverse_words(Layout.reverse_words(Shape.words(Shape.digits_words(dimensions, U32.to_nat(index))))),
53 Shape.words(Shape.digits_words(dimensions, U32.to_nat(index))),
54 Equal.cong(List<&2, U32>, List<&2, U32>, dims =>
55 Layout.reverse_words(Layout.reverse_words(Shape.words(Shape.digits_words(dims, U32.to_nat(index))))),
56 Layout.reverse_words(Layout.reverse_words(dimensions)), dimensions, reverse_involution(dimensions)),
57 reverse_involution(Shape.words(Shape.digits_words(dimensions, U32.to_nat(index))))),
58 Equal.cong(List<&2, Nat>, List<&2, U32>, Shape.words, Shape.digits_words(dimensions, U32.to_nat(index)),
59 Shape.digits(Shape.naturals(dimensions), U32.to_nat(index)), Coordinates.digits_words_spec(dimensions, U32.to_nat(index))))
60
61def coordinate_fits(+dimensions: List<&2, U32>, +values: List<&2, U32>, valid: Layout.WordsValid(dimensions, values)) ->
62 Coordinates.Fits(Shape.naturals(dimensions), Shape.naturals(values)):
63 match dimensions values:
64 case Nil{} Nil{}:
65 Unit{}
66 case +dimension <> +dt +value <> +vt:
67 Layout.WStep{bound, tail} = valid
68 Coordinates.FStep{
69 %Equal.sym(Bool, Nat.is_lt(U32.to_nat(value), U32.to_nat(dimension)), U32.is_lt(value, dimension), Arith.u32_lt(value, dimension)) :
70 {True{} == _ : Bool}
71 bound,
72 coordinate_fits(dt, vt, tail)}
73 case Nil{} head <> tail:
74 match valid:
75 case head <> tail Nil{}:
76 match valid:
77
78def codec_flattened(+dimensions: List<&2, U32>, +values: List<&2, U32>, +valid: Layout.WordsValid(dimensions, values)) ->
79 {Layout.flatten_words(dimensions, values, 0) == U32.from_nat(Shape.offset(Shape.naturals(dimensions), Shape.naturals(values))) : U32}:
80 Equal.cong(Nat, U32, U32.from_nat, Shape.horner(dimensions, values, 0n), Shape.offset(Shape.naturals(dimensions), Shape.naturals(values)),
81 Coordinates.horner_spec(dimensions, values, 0n, coordinate_fits(dimensions, values, valid)))
82
83def mapping_reference(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
84 mapping: Layout.Mapping<input, axes, plan, index>) ->
85 {Some{Layout.source_index(input, axes, plan, index, mapping)} == Layout.reference_source(input, axes, plan, index) : Maybe<&2, U32>}:
86 Layout.Mapped{oi, oc, ic, source, requested, decoded, inverse, flattened, roundtrip} = mapping
87 Layout.CWord{+values, +valid} = ic
88 %AxisAlgebra.inverse_coordinates(input, axes,
89 Shape.words(Shape.digits(Shape.extents(Layout.output(input, axes, plan)), U32.to_nat(index)))) :
90 {Some{Layout.index_value(input, source)} == Layout.reference_source_coordinates(Shape.dimensions(input), _) : Maybe<&2, U32>}
91 %Equal.trans(List<&2, U32>, Layout.coordinate_values(Layout.output(input, axes, plan), oc),
92 Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index)),
93 Shape.words(Shape.digits(Shape.extents(Layout.output(input, axes, plan)), U32.to_nat(index))), decoded,
94 codec_decoded(Shape.dimensions(Layout.output(input, axes, plan)), index)) :
95 {Some{Layout.index_value(input, source)} == Layout.reference_source_coordinates(Shape.dimensions(input),
96 Layout.inverse_coordinates(Shape.dimensions(input), axes, _, 0)) : Maybe<&2, U32>}
97 %inverse : {Some{Layout.index_value(input, source)} == Layout.reference_source_coordinates(Shape.dimensions(input), _) : Maybe<&2, U32>}
98 Equal.cong(U32, Maybe<&2, U32>, value => Some{value}, Layout.index_value(input, source),
99 U32.from_nat(Shape.offset(Shape.extents(input), Shape.naturals(values))),
100 Equal.trans(U32, Layout.index_value(input, source), Layout.flatten_words(Shape.dimensions(input), values, 0),
101 U32.from_nat(Shape.offset(Shape.extents(input), Shape.naturals(values))), flattened,
102 codec_flattened(Shape.dimensions(input), values, valid)))
103
104def flat_mathematical_bounded(+shape: Shape.Shape, index: Layout.FlatIndex<shape>) ->
105 {Nat.is_lt(U32.to_nat(Layout.index_value(shape, index)), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}:
106 Layout.FIndex{+value, bound} = index
107 %Shape.elements_exact(shape) : {Nat.is_lt(U32.to_nat(value), _) == True{} : Bool}
108 Arith.lt_le_trans(U32.to_nat(value), U32.to_nat(Shape.count(shape)), Shape.elements(shape),
109 Equal.trans(Bool, Nat.is_lt(U32.to_nat(value), U32.to_nat(Shape.count(shape))), U32.is_lt(value, Shape.count(shape)), True{},
110 Arith.u32_lt(value, Shape.count(shape)), Equal.sym(Bool, True{}, U32.is_lt(value, Shape.count(shape)), bound)),
111 WordConversion.natural_word_le(Shape.elements(shape)))
112
113def decoded_coordinate(+shape: Shape.Shape, +index: U32,
114 +inside: {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(shape)) : Bool}) -> Shape.Coordinate(Shape.extents(shape)):
115 Shape.unflatten(Shape.extents(shape), Coordinates.fin_from(Shape.numel(Shape.extents(shape)), U32.to_nat(index),
116 Coordinates.size_fits(shape, U32.to_nat(index), inside)))
117
118def decoded_indices(+shape: Shape.Shape, +index: U32,
119 +inside: {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(shape)) : Bool}) ->
120 {Shape.indices(Shape.extents(shape), decoded_coordinate(shape, index, inside)) ==
121 Shape.digits(Shape.extents(shape), U32.to_nat(index)) : List<&2, Nat>}:
122 Equal.trans(List<&2, Nat>, Shape.indices(Shape.extents(shape), decoded_coordinate(shape, index, inside)),
123 Shape.digits(Shape.extents(shape), Shape.Fin.value(Shape.numel(Shape.extents(shape)),
124 Coordinates.fin_from(Shape.numel(Shape.extents(shape)), U32.to_nat(index), Coordinates.size_fits(shape, U32.to_nat(index), inside)))),
125 Shape.digits(Shape.extents(shape), U32.to_nat(index)),
126 Coordinates.digits_unflatten(Shape.extents(shape),
127 Coordinates.fin_from(Shape.numel(Shape.extents(shape)), U32.to_nat(index), Coordinates.size_fits(shape, U32.to_nat(index), inside))),
128 Equal.cong(Nat, List<&2, Nat>, value => Shape.digits(Shape.extents(shape), value),
129 Shape.Fin.value(Shape.numel(Shape.extents(shape)),
130 Coordinates.fin_from(Shape.numel(Shape.extents(shape)), U32.to_nat(index), Coordinates.size_fits(shape, U32.to_nat(index), inside))),
131 U32.to_nat(index), Coordinates.fin_from_value(Shape.numel(Shape.extents(shape)), U32.to_nat(index),
132 Coordinates.size_fits(shape, U32.to_nat(index), inside))))
133
134def decoded_fit(+shape: Shape.Shape, +index: U32,
135 +inside: {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(shape)) : Bool}) ->
136 {True{} == Shape.fit(Shape.extents(shape), Shape.digits(Shape.extents(shape), U32.to_nat(index))) : Bool}:
137 %decoded_indices(shape, index, inside) : {True{} == Shape.fit(Shape.extents(shape), _) : Bool}
138 Coordinates.fit_indices(Shape.extents(shape), decoded_coordinate(shape, index, inside))
139
140def decoded_word_fits(+shape: Shape.Shape, +index: U32,
141 +inside: {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(shape)) : Bool}) ->
142 Coordinates.Fits(Shape.extents(shape), Shape.naturals(Shape.words(Shape.digits(Shape.extents(shape), U32.to_nat(index))))):
143 %Equal.sym(List<&2, Nat>, Shape.naturals(Shape.words(Shape.digits(Shape.extents(shape), U32.to_nat(index)))),
144 Shape.digits(Shape.extents(shape), U32.to_nat(index)),
145 WordConversion.naturals_words_fitting(Shape.dimensions(shape), Shape.digits(Shape.extents(shape), U32.to_nat(index)), decoded_fit(shape, index, inside))) :
146 Coordinates.Fits(Shape.extents(shape), _)
147 Coordinates.fits_of(Shape.extents(shape), Shape.digits(Shape.extents(shape), U32.to_nat(index)), decoded_fit(shape, index, inside))
148
149def element_counts_same(+input: Shape.Shape, +target: Shape.Shape,
150 same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}) ->
151 {Shape.elements(input) == Shape.elements(target) : Nat}:
152 Equal.trans(Nat, Shape.elements(input), Shape.logical_numel(Shape.dimensions(input)), Shape.elements(target), Shape.elements_exact(input),
153 Equal.trans(Nat, Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target)), Shape.elements(target), same,
154 Equal.sym(Nat, Shape.elements(target), Shape.logical_numel(Shape.dimensions(target)), Shape.elements_exact(target))))
155
156def natural_equal_true(+left: Nat, +right: Nat, same: {left == right : Nat}) -> {Nat.is_eq(left, right) == True{} : Bool}:
157 %same : {Nat.is_eq(left, _) == True{} : Bool}
158 Arith.eq_refl(left)
159
160def metadata_present(value: Maybe<&2, List<&2, U32>>) -> Bool:
161 match value:
162 case None{}:
163 False{}
164 case Some{values}:
165 True{}
166
167def reordered_rank_bound(+input: Shape.Shape, +axes: List<&2, U32>, +valid: {True{} == Layout.bijective(input, axes) : Bool}) ->
168 Shape.LE(Shape.rank_dimensions(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))), 4n):
169 match input:
170 case Shape.SShape{+dimensions, +size, +exact, +rank_bound, +capacity_bound}:
171 %Equal.sym(Nat, Shape.rank_dimensions(Axis.order(U32, dimensions, Shape.naturals(axes))), Shape.rank_dimensions(dimensions),
172 AxisAlgebra.permutation_rank(Shape.SShape{dimensions, size, exact, rank_bound, capacity_bound}, axes, valid)) : Shape.LE(_, 4n)
173 rank_bound
174
175def reordered_capacity_bound(+input: Shape.Shape, +axes: List<&2, U32>, +valid: {True{} == Layout.bijective(input, axes) : Bool}) ->
176 Shape.LE(Shape.logical_numel(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))), 1048576n):
177 match input:
178 case Shape.SShape{+dimensions, +size, +exact, +rank_bound, +capacity_bound}:
179 %Equal.sym(Nat, Shape.logical_numel(Axis.order(U32, dimensions, Shape.naturals(axes))), Shape.logical_numel(dimensions),
180 AxisAlgebra.permutation_product(Shape.SShape{dimensions, size, exact, rank_bound, capacity_bound}, axes, valid)) : Shape.LE(_, 1048576n)
181 capacity_bound
182
183def reordered_construct_complete(+input: Shape.Shape, +axes: List<&2, U32>, +valid: {True{} == Layout.bijective(input, axes) : Bool}) ->
184 {ShapeLaws.built(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)),
185 Shape.construct(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)))) ==
186 Some{Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))} : Maybe<&2, List<&2, U32>>}:
187 ShapeLaws.construction_complete(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)),
188 reordered_rank_bound(input, axes, valid), reordered_capacity_bound(input, axes, valid))
189
190def selected_construct_complete(+input: Shape.Shape, +axes: List<&2, U32>, +dimensions: List<&2, U32>,
191 +valid: {True{} == Layout.bijective(input, axes) : Bool},
192 same: {dimensions == Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)) : List<&2, U32>}) ->
193 {ShapeLaws.built(dimensions, Shape.construct(dimensions)) == Some{dimensions} : Maybe<&2, List<&2, U32>>}:
194 %Equal.sym(List<&2, U32>, dimensions, Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)), same) :
195 {ShapeLaws.built(_, Shape.construct(_)) == Some{_} : Maybe<&2, List<&2, U32>>}
196 reordered_construct_complete(input, axes, valid)
197
198def reordered_elements_same(+input: Shape.Shape, +axes: List<&2, U32>, +output: Shape.Shape,
199 +valid: {True{} == Layout.bijective(input, axes) : Bool},
200 preserved: {Shape.dimensions(output) == Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)) : List<&2, U32>}) ->
201 {Shape.elements(input) == Shape.elements(output) : Nat}:
202 element_counts_same(input, output,
203 Equal.trans(Nat, Shape.logical_numel(Shape.dimensions(input)),
204 Shape.logical_numel(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))), Shape.logical_numel(Shape.dimensions(output)),
205 Equal.sym(Nat, Shape.logical_numel(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))), Shape.logical_numel(Shape.dimensions(input)),
206 AxisAlgebra.permutation_product(input, axes, valid)),
207 Equal.cong(List<&2, U32>, Nat, Shape.logical_numel, Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)), Shape.dimensions(output),
208 Equal.sym(List<&2, U32>, Shape.dimensions(output), Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)), preserved))))
209
210def plan_counted_success(+input: Shape.Shape, +axes: List<&2, U32>, +output: Shape.Shape,
211 +valid: {True{} == Layout.bijective(input, axes) : Bool},
212 +ordered: {Some{Shape.dimensions(output)} == Layout.reorder(Shape.dimensions(input), axes) : Maybe<&2, List<&2, U32>>},
213 decision: Shape.BoolCase<Nat.is_eq(Shape.elements(input), Shape.elements(output))>,
214 same: {Shape.elements(input) == Shape.elements(output) : Nat}) ->
215 {Result.is_done(&2, &2, Layout.Error, Layout.Plan<input, axes>, Layout.plan_counted(input, axes, output, valid, ordered, decision)) == True{} : Bool}:
216 match decision:
217 case Shape.BFalse{equal}:
218 Empty.absurd({False{} == True{} : Bool},
219 Arith.clash(Equal.trans(Bool, False{}, Nat.is_eq(Shape.elements(input), Shape.elements(output)), True{}, equal,
220 natural_equal_true(Shape.elements(input), Shape.elements(output), same))))
221 case Shape.BTrue{equal}:
222 {==}
223
224def plan_built_success(+input: Shape.Shape, +axes: List<&2, U32>, +dimensions: List<&2, U32>,
225 +valid: {True{} == Layout.bijective(input, axes) : Bool},
226 +selected: {Some{dimensions} == Layout.reorder(Shape.dimensions(input), axes) : Maybe<&2, List<&2, U32>>},
227 built: Shape.ConstructResult<dimensions>,
228 complete: {ShapeLaws.built(dimensions, built) == Some{dimensions} : Maybe<&2, List<&2, U32>>},
229 +same: {dimensions == Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)) : List<&2, U32>}) ->
230 {Result.is_done(&2, &2, Layout.Error, Layout.Plan<input, axes>, Layout.plan_built(input, axes, dimensions, valid, selected, built)) == True{} : Bool}:
231 match built:
232 case Shape.SError{error}:
233 Empty.absurd({False{} == True{} : Bool},
234 Arith.clash(Equal.cong(Maybe<&2, List<&2, U32>>, Bool, metadata_present, None{}, Some{dimensions}, complete)))
235 case Shape.SBuilt{+output, +preserved}:
236 plan_counted_success(input, axes, output, valid,
237 Equal.trans(Maybe<&2, List<&2, U32>>, Some{Shape.dimensions(output)}, Some{dimensions}, Layout.reorder(Shape.dimensions(input), axes),
238 Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, values => Some{values}, Shape.dimensions(output), dimensions, preserved), selected),
239 Shape.bool_case(Nat.is_eq(Shape.elements(input), Shape.elements(output))),
240 reordered_elements_same(input, axes, output, valid,
241 Equal.trans(List<&2, U32>, Shape.dimensions(output), dimensions, Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)), preserved, same)))
242
243def plan_selected_success(+input: Shape.Shape, +axes: List<&2, U32>, +valid: {True{} == Layout.bijective(input, axes) : Bool},
244 selected: Maybe<&2, List<&2, U32>>, +same: {selected == Layout.reorder(Shape.dimensions(input), axes) : Maybe<&2, List<&2, U32>>}) ->
245 {Result.is_done(&2, &2, Layout.Error, Layout.Plan<input, axes>, Layout.plan_selected(input, axes, valid, selected, same)) == True{} : Bool}:
246 match selected:
247 case None{}:
248 Empty.absurd({False{} == True{} : Bool},
249 Arith.clash(Equal.cong(Maybe<&2, List<&2, U32>>, Bool, metadata_present, None{},
250 Some{Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))},
251 Equal.trans(Maybe<&2, List<&2, U32>>, None{}, Layout.reorder(Shape.dimensions(input), axes),
252 Some{Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))}, same, AxisAlgebra.permutation_complete(input, axes, valid)))))
253 case Some{+dimensions}:
254 plan_built_success(input, axes, dimensions, valid, same, Shape.construct(dimensions),
255 selected_construct_complete(input, axes, dimensions, valid,
256 Equal.cong(Maybe<&2, List<&2, U32>>, List<&2, U32>, Axis.values(U32), Some{dimensions},
257 Some{Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))},
258 Equal.trans(Maybe<&2, List<&2, U32>>, Some{dimensions}, Layout.reorder(Shape.dimensions(input), axes),
259 Some{Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))}, same, AxisAlgebra.permutation_complete(input, axes, valid)))),
260 Equal.cong(Maybe<&2, List<&2, U32>>, List<&2, U32>, Axis.values(U32), Some{dimensions},
261 Some{Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))},
262 Equal.trans(Maybe<&2, List<&2, U32>>, Some{dimensions}, Layout.reorder(Shape.dimensions(input), axes),
263 Some{Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))}, same, AxisAlgebra.permutation_complete(input, axes, valid))))
264
265def plan_decided_success(+input: Shape.Shape, +axes: List<&2, U32>, decision: Shape.BoolCase<Layout.bijective(input, axes)>,
266 +valid: {True{} == Layout.bijective(input, axes) : Bool}) ->
267 {Result.is_done(&2, &2, Layout.Error, Layout.Plan<input, axes>, Layout.plan_decided(input, axes, decision)) == True{} : Bool}:
268 match decision:
269 case Shape.BFalse{equal}:
270 Empty.absurd({False{} == True{} : Bool},
271 Arith.clash(Equal.trans(Bool, False{}, Layout.bijective(input, axes), True{}, equal,
272 Equal.sym(Bool, True{}, Layout.bijective(input, axes), valid))))
273 case Shape.BTrue{equal}:
274 plan_selected_success(input, axes, equal, Layout.reorder(Shape.dimensions(input), axes), {==})
275
276def plan_unique_success(+input: Shape.Shape, +axes: List<&2, U32>, decision: Shape.BoolCase<Layout.unique(axes)>,
277 +valid: {True{} == Layout.bijective(input, axes) : Bool}) ->
278 {Result.is_done(&2, &2, Layout.Error, Layout.Plan<input, axes>, Layout.plan_unique(input, axes, decision)) == True{} : Bool}:
279 match decision:
280 case Shape.BFalse{equal}:
281 Empty.absurd({False{} == True{} : Bool},
282 Arith.clash(Equal.trans(Bool, False{}, Layout.unique(axes), True{}, equal,
283 Equal.sym(Bool, True{}, Layout.unique(axes),
284 and_right(Layout.bounded(axes, Shape.rank(input)), Layout.unique(axes),
285 and_right(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))),
286 Bool.and(Layout.bounded(axes, Shape.rank(input)), Layout.unique(axes)), valid))))))
287 case Shape.BTrue{equal}:
288 plan_decided_success(input, axes, Shape.bool_case(Layout.bijective(input, axes)), valid)
289
290def plan_bounded_success(+input: Shape.Shape, +axes: List<&2, U32>, decision: Shape.BoolCase<Layout.bounded(axes, Shape.rank(input))>,
291 +valid: {True{} == Layout.bijective(input, axes) : Bool}) ->
292 {Result.is_done(&2, &2, Layout.Error, Layout.Plan<input, axes>, Layout.plan_bounded(input, axes, decision)) == True{} : Bool}:
293 match decision:
294 case Shape.BFalse{equal}:
295 Empty.absurd({False{} == True{} : Bool},
296 Arith.clash(Equal.trans(Bool, False{}, Layout.bounded(axes, Shape.rank(input)), True{}, equal,
297 Equal.sym(Bool, True{}, Layout.bounded(axes, Shape.rank(input)),
298 and_left(Layout.bounded(axes, Shape.rank(input)), Layout.unique(axes),
299 and_right(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))),
300 Bool.and(Layout.bounded(axes, Shape.rank(input)), Layout.unique(axes)), valid))))))
301 case Shape.BTrue{equal}:
302 plan_unique_success(input, axes, Shape.bool_case(Layout.unique(axes)), valid)
303
304def plan_ranked_success(+input: Shape.Shape, +axes: List<&2, U32>,
305 decision: Shape.BoolCase<Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))>,
306 +valid: {True{} == Layout.bijective(input, axes) : Bool}) ->
307 {Result.is_done(&2, &2, Layout.Error, Layout.Plan<input, axes>, Layout.plan_ranked(input, axes, decision)) == True{} : Bool}:
308 match decision:
309 case Shape.BFalse{equal}:
310 Empty.absurd({False{} == True{} : Bool},
311 Arith.clash(Equal.trans(Bool, False{}, Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))), True{}, equal,
312 Equal.sym(Bool, True{}, Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))),
313 and_left(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))),
314 Bool.and(Layout.bounded(axes, Shape.rank(input)), Layout.unique(axes)), valid)))))
315 case Shape.BTrue{equal}:
316 plan_bounded_success(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), valid)
317
318def words_valid_of(+dimensions: List<&2, U32>, +values: List<&2, U32>,
319 fits: Coordinates.Fits(Shape.naturals(dimensions), Shape.naturals(values))) -> Layout.WordsValid(dimensions, values):
320 match dimensions values:
321 case Nil{} Nil{}:
322 Unit{}
323 case +dimension <> +dt +value <> +vt:
324 Coordinates.FStep{bound, tail} = fits
325 Layout.WStep{
326 %Arith.u32_lt(value, dimension) : {True{} == _ : Bool}
327 bound,
328 words_valid_of(dt, vt, tail)}
329 case Nil{} head <> tail:
330 match fits:
331 case head <> tail Nil{}:
332 match fits:
333
334def words_finish_success(-dimension: U32, -dt: List<&2, U32>, -value: U32, -vt: List<&2, U32>,
335 bound: {True{} == U32.is_lt(value, dimension) : Bool}, result: Result<&2, &2, Shape.Error, Layout.WordsValid(dt, vt)>,
336 successful: {Result.is_done(&2, &2, Shape.Error, Layout.WordsValid(dt, vt), result) == True{} : Bool}) ->
337 {Result.is_done(&2, &2, Shape.Error, Layout.WordsValid(dimension <> dt, value <> vt),
338 Layout.words_finish(dimension, dt, value, vt, bound, result)) == True{} : Bool}:
339 match result:
340 case Fail{error}:
341 Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))
342 case Done{tail}:
343 {==}
344
345def words_decided_success(+dimension: U32, +dt: List<&2, U32>, +value: U32, +vt: List<&2, U32>,
346 decision: Shape.BoolCase<U32.is_lt(value, dimension)>, bound: {True{} == U32.is_lt(value, dimension) : Bool},
347 successful: {Result.is_done(&2, &2, Shape.Error, Layout.WordsValid(dt, vt), Layout.words_check(dt, vt)) == True{} : Bool}) ->
348 {Result.is_done(&2, &2, Shape.Error, Layout.WordsValid(dimension <> dt, value <> vt),
349 Layout.words_decided(dimension, dt, value, vt, unit => Layout.words_check(dt, vt), decision)) == True{} : Bool}:
350 match decision:
351 case Shape.BFalse{equal}:
352 Empty.absurd({False{} == True{} : Bool}, Lifecycle.false_true(Equal.trans(Bool, True{}, U32.is_lt(value, dimension), False{}, bound,
353 Equal.sym(Bool, False{}, U32.is_lt(value, dimension), equal))))
354 case Shape.BTrue{equal}:
355 words_finish_success(dimension, dt, value, vt, equal, Layout.words_check(dt, vt), successful)
356
357def words_check_success(+dimensions: List<&2, U32>, +values: List<&2, U32>, valid: Layout.WordsValid(dimensions, values)) ->
358 {Result.is_done(&2, &2, Shape.Error, Layout.WordsValid(dimensions, values), Layout.words_check(dimensions, values)) == True{} : Bool}:
359 match dimensions values:
360 case Nil{} Nil{}:
361 {==}
362 case +dimension <> +dt +value <> +vt:
363 Layout.WStep{bound, tail} = valid
364 words_decided_success(dimension, dt, value, vt, Shape.bool_case(U32.is_lt(value, dimension)), bound, words_check_success(dt, vt, tail))
365 case Nil{} head <> tail:
366 match valid:
367 case head <> tail Nil{}:
368 match valid:
369
370def decoded_words_valid(+shape: Shape.Shape, +index: U32,
371 +inside: {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(shape)) : Bool}) ->
372 Layout.WordsValid(Shape.dimensions(shape), Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(shape)), index))):
373 %Equal.sym(List<&2, U32>, Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(shape)), index)),
374 Shape.words(Shape.digits(Shape.extents(shape), U32.to_nat(index))), codec_decoded(Shape.dimensions(shape), index)) :
375 Layout.WordsValid(Shape.dimensions(shape), _)
376 words_valid_of(Shape.dimensions(shape), Shape.words(Shape.digits(Shape.extents(shape), U32.to_nat(index))), decoded_word_fits(shape, index, inside))
377
378def coordinate_offset_bound(+shape: Shape.Shape, +values: List<&2, U32>, +valid: Layout.WordsValid(Shape.dimensions(shape), values)) ->
379 Shape.LT(Shape.offset(Shape.extents(shape), Shape.naturals(values)), Shape.elements(shape)):
380 %Equal.sym(Nat, Shape.elements(shape), Shape.numel(Shape.extents(shape)), Shape.elements_exact(shape)) :
381 Shape.LT(Shape.offset(Shape.extents(shape), Shape.naturals(values)), _)
382 %Coordinates.offset_of(Shape.extents(shape), Shape.naturals(values), coordinate_fits(Shape.dimensions(shape), values, valid)) :
383 Shape.LT(_, Shape.numel(Shape.extents(shape)))
384 Coordinates.row_major_lt(Shape.extents(shape), Coordinates.coordinate_of(Shape.extents(shape), Shape.naturals(values),
385 coordinate_fits(Shape.dimensions(shape), values, valid)))
386
387def coordinate_offset_exact(+shape: Shape.Shape, +values: List<&2, U32>, +valid: Layout.WordsValid(Shape.dimensions(shape), values)) ->
388 {U32.to_nat(U32.from_nat(Shape.offset(Shape.extents(shape), Shape.naturals(values)))) == Shape.offset(Shape.extents(shape), Shape.naturals(values)) : Nat}:
389 WordConversion.natural_word_exact(Shape.offset(Shape.extents(shape), Shape.naturals(values)), Shape.count(shape),
390 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.elements(shape), WordConversion.shape_count_exact(shape)) :
391 {Nat.is_le(Shape.offset(Shape.extents(shape), Shape.naturals(values)), _) == True{} : Bool}
392 WordConversion.lt_le(Shape.offset(Shape.extents(shape), Shape.naturals(values)), Shape.elements(shape),
393 Equal.sym(Bool, True{}, Nat.is_lt(Shape.offset(Shape.extents(shape), Shape.naturals(values)), Shape.elements(shape)),
394 Nats.lt_true(Shape.offset(Shape.extents(shape), Shape.naturals(values)), Shape.elements(shape), coordinate_offset_bound(shape, values, valid)))))
395
396def coordinate_flatten_exact(+shape: Shape.Shape, +values: List<&2, U32>, +valid: Layout.WordsValid(Shape.dimensions(shape), values)) ->
397 {U32.to_nat(Layout.flatten_words(Shape.dimensions(shape), values, 0)) == Shape.offset(Shape.extents(shape), Shape.naturals(values)) : Nat}:
398 Equal.trans(Nat, U32.to_nat(Layout.flatten_words(Shape.dimensions(shape), values, 0)),
399 U32.to_nat(U32.from_nat(Shape.offset(Shape.extents(shape), Shape.naturals(values)))), Shape.offset(Shape.extents(shape), Shape.naturals(values)),
400 Equal.cong(U32, Nat, U32.to_nat, Layout.flatten_words(Shape.dimensions(shape), values, 0),
401 U32.from_nat(Shape.offset(Shape.extents(shape), Shape.naturals(values))), codec_flattened(Shape.dimensions(shape), values, valid)),
402 coordinate_offset_exact(shape, values, valid))
403
404def words_valid_rank(+dimensions: List<&2, U32>, +values: List<&2, U32>, valid: Layout.WordsValid(dimensions, values)) ->
405 {Shape.rank_dimensions(values) == Shape.rank_dimensions(dimensions) : Nat}:
406 match dimensions values:
407 case Nil{} Nil{}:
408 {==}
409 case +dimension <> +dt +value <> +vt:
410 Layout.WStep{bound, tail} = valid
411 Equal.cong(Nat, Nat, n => 1n+n, Shape.rank_dimensions(vt), Shape.rank_dimensions(dt), words_valid_rank(dt, vt, tail))
412 case Nil{} head <> tail:
413 match valid:
414 case head <> tail Nil{}:
415 match valid:
416
417def words_fit_true(+dimensions: List<&2, U32>, +values: List<&2, U32>, +valid: Layout.WordsValid(dimensions, values)) ->
418 {True{} == Shape.fit(Shape.naturals(dimensions), Shape.naturals(values)) : Bool}:
419 %Coordinates.indices_of(Shape.naturals(dimensions), Shape.naturals(values), coordinate_fits(dimensions, values, valid)) :
420 {True{} == Shape.fit(Shape.naturals(dimensions), _) : Bool}
421 Coordinates.fit_indices(Shape.naturals(dimensions), Coordinates.coordinate_of(Shape.naturals(dimensions), Shape.naturals(values),
422 coordinate_fits(dimensions, values, valid)))
423
424def permutation_dimensions_order(+input: Shape.Shape, +axes: List<&2, U32>, plan: Layout.Plan<input, axes>) ->
425 {Shape.dimensions(Layout.output(input, axes, plan)) == Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)) : List<&2, U32>}:
426 Layout.Permutation{+output, valid, ordered, count} = plan
427 Equal.cong(Maybe<&2, List<&2, U32>>, List<&2, U32>, Axis.values(U32), Some{Shape.dimensions(output)},
428 Some{Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))},
429 Equal.trans(Maybe<&2, List<&2, U32>>, Some{Shape.dimensions(output)}, Layout.reorder(Shape.dimensions(input), axes),
430 Some{Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))}, ordered, AxisAlgebra.permutation_complete(input, axes, valid)))
431
432def shape_rank_bound(+shape: Shape.Shape) -> Shape.LE(Shape.rank_dimensions(Shape.dimensions(shape)), 4n):
433 match shape:
434 case Shape.SShape{dimensions, size, exact, ranked, capacity}:
435 ranked
436
437def reverse_restored(-A: Data, -rank: Nat, -axes: List<&2, Nat>, -items: List<&2, A>, certificate: AxisAlgebra.ListFacts<A, rank, axes, items>) ->
438 {Axis.order(A, Axis.order(A, items, Axis.inverse_axes(rank, axes)), axes) == items : List<&2, A>}:
439 AxisAlgebra.Lists{selected, ranked, scattered, restored, reverse, scatter_restored} = certificate
440 reverse
441
442def natural_coordinate_length(+input: Shape.Shape, +coordinates: List<&2, U32>,
443 length: {Shape.rank_dimensions(coordinates) == Shape.rank_dimensions(Shape.dimensions(input)) : Nat}) ->
444 {List.length(&2, Nat, Shape.naturals(coordinates)) == Shape.rank_dimensions(Shape.dimensions(input)) : Nat}:
445 Equal.trans(Nat, List.length(&2, Nat, Shape.naturals(coordinates)), Shape.rank_dimensions(coordinates), Shape.rank_dimensions(Shape.dimensions(input)),
446 Equal.sym(Nat, Shape.rank_dimensions(coordinates), List.length(&2, Nat, Shape.naturals(coordinates)), Shape.rank_naturals(coordinates)), length)
447
448def inverse_coordinate_length(+input: Shape.Shape, +axes: List<&2, U32>, +coordinates: List<&2, U32>,
449 accepted: {True{} == Layout.bijective(input, axes) : Bool},
450 length: {Shape.rank_dimensions(coordinates) == Shape.rank_dimensions(Shape.dimensions(input)) : Nat}) ->
451 {List.length(&2, Nat, Axis.order(Nat, Shape.naturals(coordinates), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))) ==
452 Shape.rank_dimensions(Shape.dimensions(input)) : Nat}:
453 AxisAlgebra.ranked(Nat, Shape.rank_dimensions(Shape.dimensions(input)), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)),
454 Shape.naturals(coordinates),
455 AxisAlgebra.facts_lists(Nat, Shape.rank_dimensions(Shape.dimensions(input)), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)),
456 Shape.naturals(coordinates), natural_coordinate_length(input, coordinates, length),
457 AxisAlgebra.facts(Shape.rank_dimensions(Shape.dimensions(input)), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)),
458 shape_rank_bound(input), AxisAlgebra.facts_inverse_valid(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes), AxisAlgebra.shape_facts(input, axes, accepted)))))
459
460def inverse_coordinate_fit_certified(+input: Shape.Shape, +axes: List<&2, U32>, +coordinates: List<&2, U32>,
461 +accepted: {True{} == Layout.bijective(input, axes) : Bool},
462 +length: {Shape.rank_dimensions(coordinates) == Shape.rank_dimensions(Shape.dimensions(input)) : Nat},
463 fitted: {True{} == Shape.fit(Shape.naturals(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))), Shape.naturals(coordinates)) : Bool},
464 certificate: AxisAlgebra.Facts<Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)>) ->
465 {True{} == Shape.fit(Shape.extents(input),
466 Shape.naturals(Axis.order(U32, coordinates, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))))) : Bool}:
467 AxisAlgebra.Certified{iv, selected, restored, lists, product, fit} = certificate
468 %Equal.sym(List<&2, Nat>,
469 Shape.naturals(Axis.order(U32, coordinates, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))),
470 Axis.order(Nat, Shape.naturals(coordinates), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))),
471 AxisAlgebra.order_naturals(Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)), coordinates)) :
472 {True{} == Shape.fit(Shape.extents(input), _) : Bool}
473 Equal.trans(Bool, True{},
474 Shape.fit(Axis.order(Nat, Shape.extents(input), Shape.naturals(axes)),
475 Axis.order(Nat, Axis.order(Nat, Shape.naturals(coordinates), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))), Shape.naturals(axes))),
476 Shape.fit(Shape.extents(input), Axis.order(Nat, Shape.naturals(coordinates), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))),
477 %AxisAlgebra.order_naturals(Shape.naturals(axes), Shape.dimensions(input)) :
478 {True{} == Shape.fit(_, Axis.order(Nat, Axis.order(Nat, Shape.naturals(coordinates), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))), Shape.naturals(axes))) : Bool}
479 %Equal.sym(List<&2, Nat>,
480 Axis.order(Nat, Axis.order(Nat, Shape.naturals(coordinates), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))), Shape.naturals(axes)),
481 Shape.naturals(coordinates), reverse_restored(Nat, Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes), Shape.naturals(coordinates),
482 AxisAlgebra.facts_lists(Nat, Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes), Shape.naturals(coordinates),
483 natural_coordinate_length(input, coordinates, length), AxisAlgebra.shape_facts(input, axes, accepted)))) :
484 {True{} == Shape.fit(Shape.naturals(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))), _) : Bool}
485 fitted,
486 fit(Shape.extents(input), Axis.order(Nat, Shape.naturals(coordinates), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))),
487 Equal.sym(Nat, Shape.rank_dimensions(Shape.dimensions(input)), List.length(&2, Nat, Shape.extents(input)), Shape.rank_naturals(Shape.dimensions(input))),
488 inverse_coordinate_length(input, axes, coordinates, accepted, length)))
489
490def inverse_coordinate_fit(+input: Shape.Shape, +axes: List<&2, U32>, +coordinates: List<&2, U32>,
491 +accepted: {True{} == Layout.bijective(input, axes) : Bool},
492 length: {Shape.rank_dimensions(coordinates) == Shape.rank_dimensions(Shape.dimensions(input)) : Nat},
493 fitted: {True{} == Shape.fit(Shape.naturals(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))), Shape.naturals(coordinates)) : Bool}) ->
494 {True{} == Shape.fit(Shape.extents(input),
495 Shape.naturals(Axis.order(U32, coordinates, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))))) : Bool}:
496 inverse_coordinate_fit_certified(input, axes, coordinates, accepted, length, fitted, AxisAlgebra.shape_facts(input, axes, accepted))
497
498def output_coordinate_rank(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +coordinate: Layout.CheckedCoordinate<Layout.output(input, axes, plan)>) ->
499 {Shape.rank_dimensions(Layout.coordinate_values(Layout.output(input, axes, plan), coordinate)) == Shape.rank_dimensions(Shape.dimensions(input)) : Nat}:
500 Layout.Permutation{+output, +accepted, +ordered, +count} = plan
501 Layout.CWord{+values, valid} = coordinate
502 Equal.trans(Nat, Shape.rank_dimensions(values), Shape.rank_dimensions(Shape.dimensions(output)), Shape.rank_dimensions(Shape.dimensions(input)),
503 words_valid_rank(Shape.dimensions(output), values, valid),
504 Equal.trans(Nat, Shape.rank_dimensions(Shape.dimensions(output)), Shape.rank_dimensions(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))),
505 Shape.rank_dimensions(Shape.dimensions(input)),
506 Equal.cong(List<&2, U32>, Nat, Shape.rank_dimensions, Shape.dimensions(output), Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)),
507 permutation_dimensions_order(input, axes, Layout.Permutation{output, accepted, ordered, count})), AxisAlgebra.permutation_rank(input, axes, accepted)))
508
509def inverse_words_valid(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +coordinate: Layout.CheckedCoordinate<Layout.output(input, axes, plan)>,
510 +values: List<&2, U32>, inverse: {Some{values} == Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), coordinate), 0) : Maybe<&2, List<&2, U32>>}) ->
511 Layout.WordsValid(Shape.dimensions(input), values):
512 Layout.Permutation{+output, +accepted, +ordered, +count} = plan
513 Layout.CWord{+coordinates, +valid} = coordinate
514 %Equal.sym(List<&2, U32>, values, Axis.order(U32, coordinates, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))),
515 Equal.cong(Maybe<&2, List<&2, U32>>, List<&2, U32>, Axis.values(U32), Some{values},
516 Some{Axis.order(U32, coordinates, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))},
517 Equal.trans(Maybe<&2, List<&2, U32>>, Some{values}, Layout.inverse_coordinates(Shape.dimensions(input), axes, coordinates, 0),
518 Some{Axis.order(U32, coordinates, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))}, inverse,
519 AxisAlgebra.scatter_complete(input, axes, coordinates, accepted,
520 output_coordinate_rank(input, axes, Layout.Permutation{output, accepted, ordered, count}, Layout.CWord{coordinates, valid}))))) :
521 Layout.WordsValid(Shape.dimensions(input), _)
522 words_valid_of(Shape.dimensions(input), Axis.order(U32, coordinates, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))),
523 Coordinates.fits_of(Shape.extents(input),
524 Shape.naturals(Axis.order(U32, coordinates, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))),
525 inverse_coordinate_fit(input, axes, coordinates, accepted,
526 output_coordinate_rank(input, axes, Layout.Permutation{output, accepted, ordered, count}, Layout.CWord{coordinates, valid}),
527 %permutation_dimensions_order(input, axes, Layout.Permutation{output, accepted, ordered, count}) :
528 {True{} == Shape.fit(Shape.naturals(_), Shape.naturals(coordinates)) : Bool}
529 words_fit_true(Shape.dimensions(output), coordinates, valid))))
530
531def coordinate_flatten_bounded(+shape: Shape.Shape, +values: List<&2, U32>, +valid: Layout.WordsValid(Shape.dimensions(shape), values)) ->
532 {True{} == U32.is_lt(Layout.flatten_words(Shape.dimensions(shape), values, 0), Shape.count(shape)) : Bool}:
533 %Arith.u32_lt(Layout.flatten_words(Shape.dimensions(shape), values, 0), Shape.count(shape)) : {True{} == _ : Bool}
534 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.elements(shape), WordConversion.shape_count_exact(shape)) :
535 {True{} == Nat.is_lt(U32.to_nat(Layout.flatten_words(Shape.dimensions(shape), values, 0)), _) : Bool}
536 %Equal.sym(Nat, U32.to_nat(Layout.flatten_words(Shape.dimensions(shape), values, 0)), Shape.offset(Shape.extents(shape), Shape.naturals(values)),
537 coordinate_flatten_exact(shape, values, valid)) : {True{} == Nat.is_lt(_, Shape.elements(shape)) : Bool}
538 Nats.lt_true(Shape.offset(Shape.extents(shape), Shape.naturals(values)), Shape.elements(shape), coordinate_offset_bound(shape, values, valid))
539
540def checked_coordinate_flatten_bounded(+shape: Shape.Shape, coordinate: Layout.CheckedCoordinate<shape>) ->
541 {True{} == U32.is_lt(Layout.flatten_words(Shape.dimensions(shape), Layout.coordinate_values(shape, coordinate), 0), Shape.count(shape)) : Bool}:
542 Layout.CWord{values, valid} = coordinate
543 coordinate_flatten_bounded(shape, values, valid)
544
545def word_same_refl(+width: Nat, +word: Word(width)) -> {Layout.word_same(width, word, word) == True{} : Bool}:
546 match width:
547 case 0n:
548 {==}
549 case 1n+p:
550 match word:
551 case WCon{False{}, +tail}:
552 word_same_refl(p, tail)
553 case WCon{True{}, +tail}:
554 word_same_refl(p, tail)
555
556def word_value_same_refl(+value: U32) -> {Layout.word_value_same(value, value) == True{} : Bool}:
557 match value:
558 case U32{+word}:
559 word_same_refl(32n, word)
560
561def words_same_refl(+values: List<&2, U32>) -> {Layout.words_same(values, values) == True{} : Bool}:
562 match values:
563 case Nil{}:
564 {==}
565 case +head <> +tail:
566 %Equal.sym(Bool, Layout.word_value_same(head, head), True{}, word_value_same_refl(head)) :
567 {Bool.and(_, Layout.words_same(tail, tail)) == True{} : Bool}
568 words_same_refl(tail)
569
570def inverse_words_order(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +coordinate: Layout.CheckedCoordinate<Layout.output(input, axes, plan)>,
571 +values: List<&2, U32>, inverse: {Some{values} == Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), coordinate), 0) : Maybe<&2, List<&2, U32>>}) ->
572 {values == Axis.order(U32, Layout.coordinate_values(Layout.output(input, axes, plan), coordinate),
573 Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))) : List<&2, U32>}:
574 Layout.Permutation{output, accepted, ordered, count} = plan
575 Equal.cong(Maybe<&2, List<&2, U32>>, List<&2, U32>, Axis.values(U32), Some{values},
576 Some{Axis.order(U32, Layout.coordinate_values(output, coordinate), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))},
577 Equal.trans(Maybe<&2, List<&2, U32>>, Some{values}, Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(output, coordinate), 0),
578 Some{Axis.order(U32, Layout.coordinate_values(output, coordinate), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))}, inverse,
579 AxisAlgebra.scatter_complete(input, axes, Layout.coordinate_values(output, coordinate), accepted,
580 output_coordinate_rank(input, axes, Layout.Permutation{output, accepted, ordered, count}, coordinate))))
581
582def inverse_words_reordered(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +coordinate: Layout.CheckedCoordinate<Layout.output(input, axes, plan)>,
583 +values: List<&2, U32>, +inverse: {Some{values} == Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), coordinate), 0) : Maybe<&2, List<&2, U32>>}) ->
584 {Layout.reorder(values, axes) == Some{Layout.coordinate_values(Layout.output(input, axes, plan), coordinate)} : Maybe<&2, List<&2, U32>>}:
585 Layout.Permutation{+output, +accepted, +ordered, +count} = plan
586 Equal.trans(Maybe<&2, List<&2, U32>>, Layout.reorder(values, axes), Axis.gather(U32, values, Shape.naturals(axes)),
587 Some{Layout.coordinate_values(output, coordinate)}, AxisAlgebra.reorder(axes, values),
588 Equal.trans(Maybe<&2, List<&2, U32>>, Axis.gather(U32, values, Shape.naturals(axes)), Some{Axis.order(U32, values, Shape.naturals(axes))},
589 Some{Layout.coordinate_values(output, coordinate)},
590 AxisAlgebra.selected(U32, Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes), values,
591 AxisAlgebra.facts_lists(U32, Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes), values,
592 Equal.trans(Nat, List.length(&2, U32, values), Shape.rank_dimensions(values), Shape.rank_dimensions(Shape.dimensions(input)),
593 AxisAlgebra.word_length(values), words_valid_rank(Shape.dimensions(input), values,
594 inverse_words_valid(input, axes, Layout.Permutation{output, accepted, ordered, count}, coordinate, values, inverse))),
595 AxisAlgebra.shape_facts(input, axes, accepted))),
596 Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, items => Some{items}, Axis.order(U32, values, Shape.naturals(axes)),
597 Layout.coordinate_values(output, coordinate),
598 Equal.trans(List<&2, U32>, Axis.order(U32, values, Shape.naturals(axes)),
599 Axis.order(U32, Axis.order(U32, Layout.coordinate_values(output, coordinate), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))), Shape.naturals(axes)),
600 Layout.coordinate_values(output, coordinate),
601 Equal.cong(List<&2, U32>, List<&2, U32>, items => Axis.order(U32, items, Shape.naturals(axes)), values,
602 Axis.order(U32, Layout.coordinate_values(output, coordinate), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))),
603 inverse_words_order(input, axes, Layout.Permutation{output, accepted, ordered, count}, coordinate, values, inverse)),
604 reverse_restored(U32, Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes), Layout.coordinate_values(output, coordinate),
605 AxisAlgebra.facts_lists(U32, Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes), Layout.coordinate_values(output, coordinate),
606 Equal.trans(Nat, List.length(&2, U32, Layout.coordinate_values(output, coordinate)), Shape.rank_dimensions(Layout.coordinate_values(output, coordinate)),
607 Shape.rank_dimensions(Shape.dimensions(input)), AxisAlgebra.word_length(Layout.coordinate_values(output, coordinate)),
608 output_coordinate_rank(input, axes, Layout.Permutation{output, accepted, ordered, count}, coordinate)), AxisAlgebra.shape_facts(input, axes, accepted)))))))
609
610def inverse_words_roundtrip(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +coordinate: Layout.CheckedCoordinate<Layout.output(input, axes, plan)>,
611 +values: List<&2, U32>, inverse: {Some{values} == Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), coordinate), 0) : Maybe<&2, List<&2, U32>>}) ->
612 {True{} == Layout.maybe_same(Layout.reorder(values, axes), Some{Layout.coordinate_values(Layout.output(input, axes, plan), coordinate)}) : Bool}:
613 %Equal.sym(Maybe<&2, List<&2, U32>>, Layout.reorder(values, axes), Some{Layout.coordinate_values(Layout.output(input, axes, plan), coordinate)},
614 inverse_words_reordered(input, axes, plan, coordinate, values, inverse)) :
615 {True{} == Layout.maybe_same(_, Some{Layout.coordinate_values(Layout.output(input, axes, plan), coordinate)}) : Bool}
616 Equal.sym(Bool, Layout.words_same(Layout.coordinate_values(Layout.output(input, axes, plan), coordinate), Layout.coordinate_values(Layout.output(input, axes, plan), coordinate)), True{},
617 words_same_refl(Layout.coordinate_values(Layout.output(input, axes, plan), coordinate)))
618
619def mapping_flat_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
620 oi: Layout.FlatIndex<Layout.output(input, axes, plan)>, oc: Layout.CheckedCoordinate<Layout.output(input, axes, plan)>, +ic: Layout.CheckedCoordinate<input>,
621 requested: {Layout.index_value(Layout.output(input, axes, plan), oi) == index : U32},
622 decoded: {Layout.coordinate_values(Layout.output(input, axes, plan), oc) == Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index)) : List<&2, U32>},
623 inverse: {Some{Layout.coordinate_values(input, ic)} == Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), oc), 0) : Maybe<&2, List<&2, U32>>},
624 roundtrip: {True{} == Layout.maybe_same(Layout.reorder(Layout.coordinate_values(input, ic), axes), Some{Layout.coordinate_values(Layout.output(input, axes, plan), oc)}) : Bool},
625 +source_index: U32, flat: {source_index == Layout.flatten_words(Shape.dimensions(input), Layout.coordinate_values(input, ic), 0) : U32},
626 decision: Shape.BoolCase<U32.is_lt(source_index, Shape.count(input))>, bounded: {True{} == U32.is_lt(source_index, Shape.count(input)) : Bool}) ->
627 {Result.is_done(&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>,
628 Layout.map_flat(input, axes, plan, index, oi, oc, ic, requested, decoded, inverse, roundtrip, source_index, flat, decision)) == True{} : Bool}:
629 match decision:
630 case Shape.BFalse{equal}:
631 Empty.absurd({False{} == True{} : Bool}, Arith.clash(Equal.trans(Bool, False{}, U32.is_lt(source_index, Shape.count(input)), True{}, equal,
632 Equal.sym(Bool, True{}, U32.is_lt(source_index, Shape.count(input)), bounded))))
633 case Shape.BTrue{equal}:
634 {==}
635
636def mapping_roundtrip_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
637 +oi: Layout.FlatIndex<Layout.output(input, axes, plan)>, +oc: Layout.CheckedCoordinate<Layout.output(input, axes, plan)>, +ic: Layout.CheckedCoordinate<input>,
638 +requested: {Layout.index_value(Layout.output(input, axes, plan), oi) == index : U32},
639 +decoded: {Layout.coordinate_values(Layout.output(input, axes, plan), oc) == Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index)) : List<&2, U32>},
640 +inverse: {Some{Layout.coordinate_values(input, ic)} == Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), oc), 0) : Maybe<&2, List<&2, U32>>},
641 decision: Shape.BoolCase<Layout.maybe_same(Layout.reorder(Layout.coordinate_values(input, ic), axes), Some{Layout.coordinate_values(Layout.output(input, axes, plan), oc)})>,
642 roundtrip: {True{} == Layout.maybe_same(Layout.reorder(Layout.coordinate_values(input, ic), axes), Some{Layout.coordinate_values(Layout.output(input, axes, plan), oc)}) : Bool}) ->
643 {Result.is_done(&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>,
644 Layout.map_roundtrip(input, axes, plan, index, oi, oc, ic, requested, decoded, inverse, decision)) == True{} : Bool}:
645 match decision:
646 case Shape.BFalse{equal}:
647 Empty.absurd({False{} == True{} : Bool}, Arith.clash(Equal.trans(Bool, False{},
648 Layout.maybe_same(Layout.reorder(Layout.coordinate_values(input, ic), axes), Some{Layout.coordinate_values(Layout.output(input, axes, plan), oc)}), True{}, equal,
649 Equal.sym(Bool, True{}, Layout.maybe_same(Layout.reorder(Layout.coordinate_values(input, ic), axes), Some{Layout.coordinate_values(Layout.output(input, axes, plan), oc)}), roundtrip))))
650 case Shape.BTrue{equal}:
651 mapping_flat_success(input, axes, plan, index, oi, oc, ic, requested, decoded, inverse, equal,
652 Layout.flatten_words(Shape.dimensions(input), Layout.coordinate_values(input, ic), 0), {==},
653 Shape.bool_case(U32.is_lt(Layout.flatten_words(Shape.dimensions(input), Layout.coordinate_values(input, ic), 0), Shape.count(input))),
654 checked_coordinate_flatten_bounded(input, ic))
655
656def mapping_input_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
657 +oi: Layout.FlatIndex<Layout.output(input, axes, plan)>, +oc: Layout.CheckedCoordinate<Layout.output(input, axes, plan)>,
658 +requested: {Layout.index_value(Layout.output(input, axes, plan), oi) == index : U32},
659 +decoded: {Layout.coordinate_values(Layout.output(input, axes, plan), oc) == Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index)) : List<&2, U32>},
660 +values: List<&2, U32>, +inverse: {Some{values} == Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), oc), 0) : Maybe<&2, List<&2, U32>>},
661 checked: Result<&2, &2, Shape.Error, Layout.WordsValid(Shape.dimensions(input), values)>,
662 successful: {Result.is_done(&2, &2, Shape.Error, Layout.WordsValid(Shape.dimensions(input), values), checked) == True{} : Bool}) ->
663 {Result.is_done(&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>,
664 Layout.map_input(input, axes, plan, index, oi, oc, requested, decoded, values, inverse, checked)) == True{} : Bool}:
665 match checked:
666 case Fail{error}:
667 Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))
668 case Done{+valid}:
669 mapping_roundtrip_success(input, axes, plan, index, oi, oc, Layout.CWord{values, valid}, requested, decoded, inverse,
670 Shape.bool_case(Layout.maybe_same(Layout.reorder(values, axes), Some{Layout.coordinate_values(Layout.output(input, axes, plan), oc)})),
671 inverse_words_roundtrip(input, axes, plan, oc, values, inverse))
672
673def mapping_inverse_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
674 +oi: Layout.FlatIndex<Layout.output(input, axes, plan)>, +oc: Layout.CheckedCoordinate<Layout.output(input, axes, plan)>,
675 +requested: {Layout.index_value(Layout.output(input, axes, plan), oi) == index : U32},
676 +decoded: {Layout.coordinate_values(Layout.output(input, axes, plan), oc) == Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index)) : List<&2, U32>},
677 result: Maybe<&2, List<&2, U32>>,
678 +same: {result == Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), oc), 0) : Maybe<&2, List<&2, U32>>}) ->
679 {Result.is_done(&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>,
680 Layout.map_inverse(input, axes, plan, index, oi, oc, requested, decoded, result, same)) == True{} : Bool}:
681 match result:
682 case None{}:
683 Empty.absurd({False{} == True{} : Bool},
684 Arith.clash(Equal.cong(Maybe<&2, List<&2, U32>>, Bool, metadata_present, None{},
685 Some{Axis.order(U32, Layout.coordinate_values(Layout.output(input, axes, plan), oc), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))},
686 Equal.trans(Maybe<&2, List<&2, U32>>, None{}, Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), oc), 0),
687 Some{Axis.order(U32, Layout.coordinate_values(Layout.output(input, axes, plan), oc), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))}, same,
688 AxisAlgebra.scatter_complete(input, axes, Layout.coordinate_values(Layout.output(input, axes, plan), oc), permutation_checked(input, axes, plan),
689 output_coordinate_rank(input, axes, plan, oc))))))
690 case Some{+values}:
691 mapping_input_success(input, axes, plan, index, oi, oc, requested, decoded, values, same, Layout.words_check(Shape.dimensions(input), values),
692 words_check_success(Shape.dimensions(input), values, inverse_words_valid(input, axes, plan, oc, values, same)))
693
694def mapping_output_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
695 +oi: Layout.FlatIndex<Layout.output(input, axes, plan)>, +requested: {Layout.index_value(Layout.output(input, axes, plan), oi) == index : U32},
696 +values: List<&2, U32>, +decoded: {values == Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index)) : List<&2, U32>},
697 checked: Result<&2, &2, Shape.Error, Layout.WordsValid(Shape.dimensions(Layout.output(input, axes, plan)), values)>,
698 successful: {Result.is_done(&2, &2, Shape.Error, Layout.WordsValid(Shape.dimensions(Layout.output(input, axes, plan)), values), checked) == True{} : Bool}) ->
699 {Result.is_done(&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>,
700 Layout.map_output(input, axes, plan, index, oi, requested, values, decoded, checked)) == True{} : Bool}:
701 match checked:
702 case Fail{error}:
703 Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))
704 case Done{+valid}:
705 mapping_inverse_success(input, axes, plan, index, oi, Layout.CWord{values, valid}, requested, decoded,
706 Layout.inverse_coordinates(Shape.dimensions(input), axes, values, 0), {==})
707
708def mapping_decided_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
709 decision: Shape.BoolCase<U32.is_lt(index, Shape.count(Layout.output(input, axes, plan)))>,
710 inside: {True{} == U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))) : Bool}) ->
711 {Result.is_done(&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>, Layout.map_decided(input, axes, plan, index, decision)) == True{} : Bool}:
712 match decision:
713 case Shape.BFalse{equal}:
714 Empty.absurd({False{} == True{} : Bool}, Arith.clash(Equal.trans(Bool, False{}, U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))), True{}, equal,
715 Equal.sym(Bool, True{}, U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))), inside))))
716 case Shape.BTrue{+equal}:
717 mapping_output_success(input, axes, plan, index, Layout.FIndex{index, equal}, {==},
718 Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index)), {==},
719 Layout.words_check(Shape.dimensions(Layout.output(input, axes, plan)), Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index))),
720 words_check_success(Shape.dimensions(Layout.output(input, axes, plan)),
721 Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index)),
722 decoded_words_valid(Layout.output(input, axes, plan), index,
723 %Equal.sym(Nat, Shape.elements(Layout.output(input, axes, plan)), Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), Shape.elements_exact(Layout.output(input, axes, plan))) :
724 {True{} == Nat.is_lt(U32.to_nat(index), _) : Bool}
725 Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))), True{},
726 flat_mathematical_bounded(Layout.output(input, axes, plan), Layout.FIndex{index, equal})))))
727
728def cursor_word_exact(+shape: Shape.Shape, +cursor: Nat, within: {Nat.is_le(cursor, Shape.elements(shape)) == True{} : Bool}) ->
729 {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat}:
730 WordConversion.natural_word_exact(cursor, Shape.count(shape),
731 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.elements(shape), WordConversion.shape_count_exact(shape)) :
732 {Nat.is_le(cursor, _) == True{} : Bool}
733 within)
734
735def cursor_index_bounded(+shape: Shape.Shape, +cursor: Nat, +inside: {True{} == Nat.is_lt(cursor, Shape.elements(shape)) : Bool}) ->
736 {True{} == U32.is_lt(U32.from_nat(cursor), Shape.count(shape)) : Bool}:
737 %Arith.u32_lt(U32.from_nat(cursor), Shape.count(shape)) : {True{} == _ : Bool}
738 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.elements(shape), WordConversion.shape_count_exact(shape)) :
739 {True{} == Nat.is_lt(U32.to_nat(U32.from_nat(cursor)), _) : Bool}
740 %Equal.sym(Nat, U32.to_nat(U32.from_nat(cursor)), cursor, cursor_word_exact(shape, cursor,
741 WordConversion.lt_le(cursor, Shape.elements(shape), Equal.sym(Bool, True{}, Nat.is_lt(cursor, Shape.elements(shape)), inside)))) :
742 {True{} == Nat.is_lt(_, Shape.elements(shape)) : Bool}
743 inside
744
745def permutation_output_rank(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>) ->
746 {Shape.rank_dimensions(Shape.dimensions(Layout.output(input, axes, plan))) == Shape.rank_dimensions(Shape.dimensions(input)) : Nat}:
747 Equal.trans(Nat, Shape.rank_dimensions(Shape.dimensions(Layout.output(input, axes, plan))),
748 Shape.rank_dimensions(Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))), Shape.rank_dimensions(Shape.dimensions(input)),
749 Equal.cong(List<&2, U32>, Nat, Shape.rank_dimensions, Shape.dimensions(Layout.output(input, axes, plan)), Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)),
750 permutation_dimensions_order(input, axes, plan)), AxisAlgebra.permutation_rank(input, axes, permutation_checked(input, axes, plan)))