src/shape/boundary_proofs.bend
bendtorch-core@0.1.0.0 · 296 lines · 31 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
4import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as Broadcast
5import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as Coordinates
6import bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend as Projection
7import bendtorch-core@0.1.0.0/src/shape/flat.bend as Flat
8import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as Laws
9
10def fin_of_from(+bound: Nat, +value: Nat, fits: {True{} == Nat.is_lt(value, bound) : Bool}) -> {Laws.fin_of(bound, value) == Some{Coordinates.fin_from(bound, value, fits)} : Maybe<&2, Shape.Fin(bound)>}:
11 match bound value:
12 case 0n 0n:
13 Empty.absurd({Laws.fin_of(0n, 0n) == Some{Coordinates.fin_from(0n, 0n, fits)} : Maybe<&2, Shape.Fin(0n)>}, Shape.clash(fits))
14 case 0n 1n+q:
15 Empty.absurd({Laws.fin_of(0n, 1n+q) == Some{Coordinates.fin_from(0n, 1n+q, fits)} : Maybe<&2, Shape.Fin(0n)>}, Shape.clash(fits))
16 case 1n+p 0n:
17 {==}
18 case 1n+p 1n+q:
19 Equal.cong(Maybe<&2, Shape.Fin(p)>, Maybe<&2, Shape.Fin(1n+p)>, index => Laws.fin_of.next(p, index), Laws.fin_of(p, q), Some{Coordinates.fin_from(p, q, fits)}, fin_of_from(p, q, fits))
20
21def fin_of_none(+bound: Nat, +value: Nat, misses: {False{} == Nat.is_lt(value, bound) : Bool}) -> {None{} == Laws.fin_of(bound, value) : Maybe<&2, Shape.Fin(bound)>}:
22 match bound value:
23 case 0n value:
24 {==}
25 case 1n+p 0n:
26 Empty.absurd({None{} == Laws.fin_of(1n+p, 0n) : Maybe<&2, Shape.Fin(1n+p)>}, Nats.contradiction(Nat.is_lt(0n, 1n+p), {==}, misses))
27 case 1n+p 1n+q:
28 Equal.cong(Maybe<&2, Shape.Fin(p)>, Maybe<&2, Shape.Fin(1n+p)>, index => Laws.fin_of.next(p, index), None{}, Laws.fin_of(p, q), fin_of_none(p, q, misses))
29
30def fin_of_value(+bound: Nat, +index: Shape.Fin(bound)) -> {Some{index} == Laws.fin_of(bound, Shape.Fin.value(bound, index)) : Maybe<&2, Shape.Fin(bound)>}:
31 match bound:
32 case 0n:
33 match index:
34 case 1n+p:
35 match index:
36 case Shape.FZero{}:
37 {==}
38 case Shape.FNext{+previous}:
39 Equal.cong(Maybe<&2, Shape.Fin(p)>, Maybe<&2, Shape.Fin(1n+p)>, index => Laws.fin_of.next(p, index), Some{previous}, Laws.fin_of(p, Shape.Fin.value(p, previous)), fin_of_value(p, previous))
40
41def decode_none(-dh: Nat, -dt: List<&2, Nat>, +tail: Maybe<&2, Shape.Coordinate(dt)>) -> {None{} == Laws.decode.step(dh, dt, tail, None{}) : Maybe<&2, Shape.Coordinate(dh <> dt)>}:
42 match tail:
43 case None{}:
44 {==}
45 case Some{rest}:
46 {==}
47
48def decode_fit(+dims: List<&2, Nat>, +values: List<&2, Nat>, +fits: Coordinates.Fits(dims, values)) -> {Laws.decode(dims, values) == Some{Coordinates.coordinate_of(dims, values, fits)} : Maybe<&2, Shape.Coordinate(dims)>}:
49 match dims values:
50 case Nil{} Nil{}:
51 {==}
52 case +dh <> +dt +vh <> +vt:
53 Coordinates.FStep{+bound, +tail} = fits
54 %Equal.sym(Maybe<&2, Shape.Coordinate(dt)>, Laws.decode(dt, vt), Some{Coordinates.coordinate_of(dt, vt, tail)}, decode_fit(dt, vt, tail)) : {Laws.decode.step(dh, dt, _, Laws.fin_of(dh, vh)) == Some{Shape.CStep{Coordinates.fin_from(dh, vh, bound), Coordinates.coordinate_of(dt, vt, tail)}} : Maybe<&2, Shape.Coordinate(dh <> dt)>}
55 %Equal.sym(Maybe<&2, Shape.Fin(dh)>, Laws.fin_of(dh, vh), Some{Coordinates.fin_from(dh, vh, bound)}, fin_of_from(dh, vh, bound)) : {Laws.decode.step(dh, dt, Some{Coordinates.coordinate_of(dt, vt, tail)}, _) == Some{Shape.CStep{Coordinates.fin_from(dh, vh, bound), Coordinates.coordinate_of(dt, vt, tail)}} : Maybe<&2, Shape.Coordinate(dh <> dt)>}
56 {==}
57 case Nil{} vh <> vt:
58 match fits:
59 case dh <> dt Nil{}:
60 match fits:
61
62def decode_unfit.step(+dh: Nat, +dt: List<&2, Nat>, +vh: Nat, +vt: List<&2, Nat>, +verdict: Shape.BoolCase<Nat.is_lt(vh, dh)>, misses: {False{} == Bool.and(Nat.is_lt(vh, dh), Shape.fit(dt, vt)) : Bool}, rec: {False{} == Shape.fit(dt, vt) : Bool} -> {None{} == Laws.decode(dt, vt) : Maybe<&2, Shape.Coordinate(dt)>}) -> {None{} == Laws.decode.step(dh, dt, Laws.decode(dt, vt), Laws.fin_of(dh, vh)) : Maybe<&2, Shape.Coordinate(dh <> dt)>}:
63 match verdict:
64 case Shape.BFalse{equal}:
65 %fin_of_none(dh, vh, equal) : {None{} == Laws.decode.step(dh, dt, Laws.decode(dt, vt), _) : Maybe<&2, Shape.Coordinate(dh <> dt)>}
66 decode_none(dh, dt, Laws.decode(dt, vt))
67 case Shape.BTrue{equal}:
68 %rec(Equal.trans(Bool, False{}, Bool.and(Nat.is_lt(vh, dh), Shape.fit(dt, vt)), Shape.fit(dt, vt), misses, Equal.cong(Bool, Bool, head => Bool.and(head, Shape.fit(dt, vt)), Nat.is_lt(vh, dh), True{}, Equal.sym(Bool, True{}, Nat.is_lt(vh, dh), equal)))) : {None{} == Laws.decode.step(dh, dt, _, Laws.fin_of(dh, vh)) : Maybe<&2, Shape.Coordinate(dh <> dt)>}
69 {==}
70
71def decode_unfit(+dims: List<&2, Nat>, +values: List<&2, Nat>, misses: {False{} == Shape.fit(dims, values) : Bool}) -> {None{} == Laws.decode(dims, values) : Maybe<&2, Shape.Coordinate(dims)>}:
72 match dims values:
73 case Nil{} Nil{}:
74 Empty.absurd({None{} == Laws.decode(Nil{}, Nil{}) : Maybe<&2, Shape.Coordinate(Nil{})>}, Shape.clash(Equal.sym(Bool, False{}, True{}, misses)))
75 case +dh <> +dt +vh <> +vt:
76 decode_unfit.step(dh, dt, vh, vt, Shape.bool_case(Nat.is_lt(vh, dh)), misses, rest => decode_unfit(dt, vt, rest))
77 case Nil{} vh <> vt:
78 {==}
79 case dh <> dt Nil{}:
80 {==}
81
82def fit_words_true(+dims: List<&2, U32>, +values: List<&2, U32>, equal: {True{} == Shape.fit_words(dims, values) : Bool}) -> {True{} == Shape.fit(Shape.naturals(dims), Shape.naturals(values)) : Bool}:
83 %Coordinates.fit_words_spec(dims, values) : {True{} == _ : Bool}
84 equal
85
86def fit_words_false(+dims: List<&2, U32>, +values: List<&2, U32>, equal: {False{} == Shape.fit_words(dims, values) : Bool}) -> {False{} == Shape.fit(Shape.naturals(dims), Shape.naturals(values)) : Bool}:
87 %Coordinates.fit_words_spec(dims, values) : {False{} == _ : Bool}
88 equal
89
90def decode_rank(+dims: List<&2, U32>, +values: List<&2, U32>, mismatch: {False{} == Nat.is_eq(Shape.rank_dimensions(dims), Shape.rank_dimensions(values)) : Bool}) -> {None{} == Laws.decode(Shape.naturals(dims), Shape.naturals(values)) : Maybe<&2, Shape.Coordinate(Shape.naturals(dims))>}:
91 match dims values:
92 case Nil{} Nil{}:
93 Empty.absurd({None{} == Laws.decode(Nil{}, Nil{}) : Maybe<&2, Shape.Coordinate(Nil{})>}, Nats.contradiction(Nat.is_eq(0n, 0n), {==}, mismatch))
94 case +dh <> +dt +vh <> +vt:
95 %decode_rank(dt, vt, mismatch) : {None{} == Laws.decode.step(U32.to_nat(dh), Shape.naturals(dt), _, Laws.fin_of(U32.to_nat(dh), U32.to_nat(vh))) : Maybe<&2, Shape.Coordinate(Shape.naturals(dh <> dt))>}
96 {==}
97 case Nil{} vh <> vt:
98 {==}
99 case dh <> dt Nil{}:
100 {==}
101
102def decode_indices(+dims: List<&2, Nat>, +coordinate: Shape.Coordinate(dims)) -> {Some{coordinate} == Laws.decode(dims, Shape.indices(dims, coordinate)) : Maybe<&2, Shape.Coordinate(dims)>}:
103 match dims:
104 case Nil{}:
105 match coordinate:
106 case Unit{}:
107 {==}
108 case +head <> +tail:
109 Shape.CStep{+index, +rest} = coordinate
110 %decode_indices(tail, rest) : {Some{Shape.CStep{index, rest}} == Laws.decode.step(head, tail, _, Laws.fin_of(head, Shape.Fin.value(head, index))) : Maybe<&2, Shape.Coordinate(head <> tail)>}
111 %fin_of_value(head, index) : {Some{Shape.CStep{index, rest}} == Laws.decode.step(head, tail, Some{rest}, _) : Maybe<&2, Shape.Coordinate(head <> tail)>}
112 {==}
113
114def checked_fit(+shape: Shape.Shape, +values: List<&2, Nat>, +verdict: Shape.BoolCase<Shape.fit_values(Shape.dimensions(shape), values)>, ok: {True{} == Shape.fit(Shape.extents(shape), values) : Bool}) -> {Laws.coordinate_result(shape, Shape.coordinate_checked.finish(shape, values, verdict)) == Some{Shape.words(values)} : Maybe<&2, List<&2, U32>>}:
115 match verdict:
116 case Shape.BFalse{equal}:
117 Empty.absurd({None{} == Some{Shape.words(values)} : Maybe<&2, List<&2, U32>>}, Nats.contradiction(Shape.fit(Shape.extents(shape), values), ok, Equal.trans(Bool, False{}, Shape.fit_values(Shape.dimensions(shape), values), Shape.fit(Shape.extents(shape), values), equal, Shape.fit_values_spec(Shape.dimensions(shape), values))))
118 case Shape.BTrue{equal}:
119 {==}
120
121def checked_indices(+shape: Shape.Shape, +coordinate: Shape.Coordinate(Shape.extents(shape))) -> {Laws.coordinate_result(shape, Shape.coordinate_checked.nat(shape, Shape.indices(Shape.extents(shape), coordinate))) == Some{Shape.words(Shape.indices(Shape.extents(shape), coordinate))} : Maybe<&2, List<&2, U32>>}:
122 +values = Shape.indices(Shape.extents(shape), coordinate)
123 checked_fit(shape, values, Shape.bool_case(Shape.fit_values(Shape.dimensions(shape), values)), Coordinates.fit_indices(Shape.extents(shape), coordinate))
124
125def flat_view(-shape: Shape.Shape, +index: Nat, +verdict: Shape.BoolCase<Nat.is_lt(index, Shape.elements(shape))>, fits: {True{} == Nat.is_lt(index, Shape.elements(shape)) : Bool}) -> {Laws.index_result(shape, Shape.flat_checked.finish(shape, index, verdict)) == Some{U32.from_nat(index)} : Maybe<&2, U32>}:
126 match verdict:
127 case Shape.BFalse{equal}:
128 Empty.absurd({Laws.index_result(shape, Shape.flat_checked.finish(shape, index, Shape.BFalse{equal})) == Some{U32.from_nat(index)} : Maybe<&2, U32>}, Nats.contradiction(Nat.is_lt(index, Shape.elements(shape)), fits, equal))
129 case Shape.BTrue{equal}:
130 {==}
131
132def horner_fits(+shape: Shape.Shape, +values: List<&2, U32>, +fits: Coordinates.Fits(Shape.extents(shape), Shape.naturals(values))) -> {Shape.horner(Shape.dimensions(shape), values, 0n) == Shape.row_major(Shape.extents(shape), Coordinates.coordinate_of(Shape.extents(shape), Shape.naturals(values), fits)) : Nat}:
133 Equal.trans(Nat, Shape.horner(Shape.dimensions(shape), values, 0n), Shape.offset(Shape.extents(shape), Shape.naturals(values)), Shape.row_major(Shape.extents(shape), Coordinates.coordinate_of(Shape.extents(shape), Shape.naturals(values), fits)), Coordinates.horner_spec(Shape.dimensions(shape), values, 0n, fits), Equal.sym(Nat, Shape.row_major(Shape.extents(shape), Coordinates.coordinate_of(Shape.extents(shape), Shape.naturals(values), fits)), Shape.offset(Shape.extents(shape), Shape.naturals(values)), Coordinates.offset_of(Shape.extents(shape), Shape.naturals(values), fits)))
134
135def horner_below(+shape: Shape.Shape, +values: List<&2, U32>, +fits: Coordinates.Fits(Shape.extents(shape), Shape.naturals(values))) -> {True{} == Nat.is_lt(Shape.horner(Shape.dimensions(shape), values, 0n), Shape.elements(shape)) : Bool}:
136 +coordinate = Coordinates.coordinate_of(Shape.extents(shape), Shape.naturals(values), fits)
137 %Equal.sym(Nat, Shape.elements(shape), Shape.numel(Shape.extents(shape)), Shape.elements_exact(shape)) : {True{} == Nat.is_lt(Shape.horner(Shape.dimensions(shape), values, 0n), _) : Bool}
138 %Equal.sym(Nat, Shape.horner(Shape.dimensions(shape), values, 0n), Shape.row_major(Shape.extents(shape), coordinate), horner_fits(shape, values, fits)) : {True{} == Nat.is_lt(_, Shape.numel(Shape.extents(shape))) : Bool}
139 Nats.lt_true(Shape.row_major(Shape.extents(shape), coordinate), Shape.numel(Shape.extents(shape)), Coordinates.row_major_lt(Shape.extents(shape), coordinate))
140
141def flatten_fits(+shape: Shape.Shape, +values: List<&2, U32>, +verdict: Shape.BoolCase<Shape.fit_words(Shape.dimensions(shape), values)>) -> {Laws.index_result(shape, Shape.flatten_checked.fits(shape, values, verdict)) == Laws.flatten_spec(Shape.extents(shape), Laws.decode(Shape.extents(shape), Shape.naturals(values))) : Maybe<&2, U32>}:
142 match verdict:
143 case Shape.BFalse{equal}:
144 %decode_unfit(Shape.extents(shape), Shape.naturals(values), fit_words_false(Shape.dimensions(shape), values, equal)) : {None{} == Laws.flatten_spec(Shape.extents(shape), _) : Maybe<&2, U32>}
145 {==}
146 case Shape.BTrue{equal}:
147 +fits = Coordinates.fits_of(Shape.extents(shape), Shape.naturals(values), fit_words_true(Shape.dimensions(shape), values, equal))
148 +coordinate = Coordinates.coordinate_of(Shape.extents(shape), Shape.naturals(values), fits)
149 +flat = Shape.horner(Shape.dimensions(shape), values, 0n)
150 %Equal.sym(Maybe<&2, Shape.Coordinate(Shape.extents(shape))>, Laws.decode(Shape.extents(shape), Shape.naturals(values)), Some{coordinate}, decode_fit(Shape.extents(shape), Shape.naturals(values), fits)) : {Laws.index_result(shape, Shape.flat_checked(shape, flat)) == Laws.flatten_spec(Shape.extents(shape), _) : Maybe<&2, U32>}
151 %horner_fits(shape, values, fits) : {Laws.index_result(shape, Shape.flat_checked(shape, flat)) == Some{U32.from_nat(_)} : Maybe<&2, U32>}
152 flat_view(shape, flat, Shape.bool_case(Nat.is_lt(flat, Shape.elements(shape))), horner_below(shape, values, fits))
153
154def flatten_ranked(+shape: Shape.Shape, +values: List<&2, U32>, +same: Shape.BoolCase<Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.rank_dimensions(values))>) -> {Laws.index_result(shape, Shape.flatten_checked.ranked(shape, values, same)) == Laws.flatten_spec(Shape.extents(shape), Laws.decode(Shape.extents(shape), Shape.naturals(values))) : Maybe<&2, U32>}:
155 match same:
156 case Shape.BFalse{equal}:
157 %decode_rank(Shape.dimensions(shape), values, equal) : {None{} == Laws.flatten_spec(Shape.extents(shape), _) : Maybe<&2, U32>}
158 {==}
159 case Shape.BTrue{equal}:
160 flatten_fits(shape, values, Shape.bool_case(Shape.fit_words(Shape.dimensions(shape), values)))
161
162def flatten_checked(+shape: Shape.Shape, +values: List<&2, U32>) -> {Laws.index_result(shape, Shape.flatten_checked(shape, values)) == Laws.flatten_spec(Shape.extents(shape), Laws.decode(Shape.extents(shape), Shape.naturals(values))) : Maybe<&2, U32>}:
163 flatten_ranked(shape, values, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.rank_dimensions(values))))
164
165def unflatten_verdict(+shape: Shape.Shape, +index: Nat, +verdict: Shape.BoolCase<Nat.is_lt(index, Shape.elements(shape))>) -> {Laws.coordinate_result(shape, Shape.unflatten_checked.finish(shape, index, verdict)) == Laws.unflatten_spec(Shape.extents(shape), Laws.fin_of(Shape.numel(Shape.extents(shape)), index)) : Maybe<&2, List<&2, U32>>}:
166 match verdict:
167 case Shape.BFalse{equal}:
168 %fin_of_none(Shape.numel(Shape.extents(shape)), index, Coordinates.size_misses(shape, index, equal)) : {None{} == Laws.unflatten_spec(Shape.extents(shape), _) : Maybe<&2, List<&2, U32>>}
169 {==}
170 case Shape.BTrue{equal}:
171 +fits = Coordinates.size_fits(shape, index, equal)
172 +flat = Coordinates.fin_from(Shape.numel(Shape.extents(shape)), index, fits)
173 %Equal.sym(Maybe<&2, Shape.Fin(Shape.numel(Shape.extents(shape)))>, Laws.fin_of(Shape.numel(Shape.extents(shape)), index), Some{flat}, fin_of_from(Shape.numel(Shape.extents(shape)), index, fits)) : {Laws.coordinate_result(shape, Shape.coordinate_checked.nat(shape, Shape.digits_words(Shape.dimensions(shape), index))) == Laws.unflatten_spec(Shape.extents(shape), _) : Maybe<&2, List<&2, U32>>}
174 %Equal.sym(List<&2, Nat>, Shape.digits_words(Shape.dimensions(shape), index), Shape.digits(Shape.extents(shape), index), Coordinates.digits_words_spec(Shape.dimensions(shape), index)) : {Laws.coordinate_result(shape, Shape.coordinate_checked.nat(shape, _)) == Some{Shape.words(Shape.indices(Shape.extents(shape), Shape.unflatten(Shape.extents(shape), flat)))} : Maybe<&2, List<&2, U32>>}
175 %Coordinates.fin_from_value(Shape.numel(Shape.extents(shape)), index, fits) : {Laws.coordinate_result(shape, Shape.coordinate_checked.nat(shape, Shape.digits(Shape.extents(shape), _))) == Some{Shape.words(Shape.indices(Shape.extents(shape), Shape.unflatten(Shape.extents(shape), flat)))} : Maybe<&2, List<&2, U32>>}
176 %Coordinates.digits_unflatten(Shape.extents(shape), flat) : {Laws.coordinate_result(shape, Shape.coordinate_checked.nat(shape, _)) == Some{Shape.words(Shape.indices(Shape.extents(shape), Shape.unflatten(Shape.extents(shape), flat)))} : Maybe<&2, List<&2, U32>>}
177 checked_indices(shape, Shape.unflatten(Shape.extents(shape), flat))
178
179def unflatten_checked(+shape: Shape.Shape, +index: U32) -> {Laws.coordinate_result(shape, Shape.unflatten_checked(shape, index)) == Laws.unflatten_spec(Shape.extents(shape), Laws.fin_of(Shape.numel(Shape.extents(shape)), U32.to_nat(index))) : Maybe<&2, List<&2, U32>>}:
180 unflatten_verdict(shape, U32.to_nat(index), Shape.bool_case(Nat.is_lt(U32.to_nat(index), Shape.elements(shape))))
181
182def projected_left(+left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +alignment: Shape.Broadcast<Shape.extents(left), Shape.extents(right), Shape.extents(output)>, +values: List<&2, U32>, +fits: Coordinates.Fits(Shape.extents(output), Shape.naturals(values))) -> {Shape.projected_words(Shape.dimensions(left), List.drop(&2, U32, values, Nat.sub(Shape.rank_dimensions(values), Shape.rank_dimensions(Shape.dimensions(left))))) == Shape.indices(Shape.extents(left), Shape.project_left(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, Coordinates.coordinate_of(Shape.extents(output), Shape.naturals(values), fits))) : List<&2, Nat>}:
183 +coordinate = Coordinates.coordinate_of(Shape.extents(output), Shape.naturals(values), fits)
184 +expected = Shape.indices(Shape.extents(left), Shape.project_left(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, coordinate))
185 +count = Nat.sub(Shape.rank_dimensions(values), Shape.rank_dimensions(Shape.dimensions(left)))
186 %Equal.sym(List<&2, Nat>, Shape.projected_words(Shape.dimensions(left), List.drop(&2, U32, values, count)), Shape.broadcast_indices(Shape.extents(left), Shape.naturals(List.drop(&2, U32, values, count))), Coordinates.projected_words_spec(Shape.dimensions(left), List.drop(&2, U32, values, count))) : {_ == expected : List<&2, Nat>}
187 %Equal.sym(List<&2, Nat>, Shape.naturals(List.drop(&2, U32, values, count)), List.drop(&2, Nat, Shape.naturals(values), count), Coordinates.naturals_drop(values, count)) : {Shape.broadcast_indices(Shape.extents(left), _) == expected : List<&2, Nat>}
188 %Equal.sym(Nat, Shape.rank_dimensions(values), List.length(&2, Nat, Shape.naturals(values)), Shape.rank_naturals(values)) : {Shape.broadcast_indices(Shape.extents(left), List.drop(&2, Nat, Shape.naturals(values), Nat.sub(_, Shape.rank_dimensions(Shape.dimensions(left))))) == expected : List<&2, Nat>}
189 %Equal.sym(Nat, Shape.rank_dimensions(Shape.dimensions(left)), List.length(&2, Nat, Shape.extents(left)), Shape.rank_naturals(Shape.dimensions(left))) : {Shape.broadcast_indices(Shape.extents(left), List.drop(&2, Nat, Shape.naturals(values), Nat.sub(List.length(&2, Nat, Shape.naturals(values)), _))) == expected : List<&2, Nat>}
190 %Coordinates.indices_of(Shape.extents(output), Shape.naturals(values), fits) : {Shape.project_indices(Shape.extents(left), _) == expected : List<&2, Nat>}
191 Equal.sym(List<&2, Nat>, expected, Shape.project_indices(Shape.extents(left), Shape.indices(Shape.extents(output), coordinate)), Broadcast.project_left(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, coordinate))
192
193def project_left_fits(+left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +alignment: Shape.Broadcast<Shape.extents(left), Shape.extents(right), Shape.extents(output)>, +values: List<&2, U32>, +verdict: Shape.BoolCase<Shape.fit_words(Shape.dimensions(output), values)>) -> {Laws.coordinate_result(left, Shape.projection_checked.fits(left, output, values, verdict)) == Laws.project_left_spec(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, Laws.decode(Shape.extents(output), Shape.naturals(values))) : Maybe<&2, List<&2, U32>>}:
194 match verdict:
195 case Shape.BFalse{equal}:
196 %decode_unfit(Shape.extents(output), Shape.naturals(values), fit_words_false(Shape.dimensions(output), values, equal)) : {None{} == Laws.project_left_spec(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, _) : Maybe<&2, List<&2, U32>>}
197 {==}
198 case Shape.BTrue{equal}:
199 +fits = Coordinates.fits_of(Shape.extents(output), Shape.naturals(values), fit_words_true(Shape.dimensions(output), values, equal))
200 +coordinate = Coordinates.coordinate_of(Shape.extents(output), Shape.naturals(values), fits)
201 +projected = Shape.project_left(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, coordinate)
202 +count = Nat.sub(Shape.rank_dimensions(values), Shape.rank_dimensions(Shape.dimensions(left)))
203 %Equal.sym(Maybe<&2, Shape.Coordinate(Shape.extents(output))>, Laws.decode(Shape.extents(output), Shape.naturals(values)), Some{coordinate}, decode_fit(Shape.extents(output), Shape.naturals(values), fits)) : {Laws.coordinate_result(left, Shape.coordinate_checked.nat(left, Shape.projected_words(Shape.dimensions(left), List.drop(&2, U32, values, count)))) == Laws.project_left_spec(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, _) : Maybe<&2, List<&2, U32>>}
204 %Equal.sym(List<&2, Nat>, Shape.projected_words(Shape.dimensions(left), List.drop(&2, U32, values, count)), Shape.indices(Shape.extents(left), projected), projected_left(left, right, output, alignment, values, fits)) : {Laws.coordinate_result(left, Shape.coordinate_checked.nat(left, _)) == Some{Shape.words(Shape.indices(Shape.extents(left), projected))} : Maybe<&2, List<&2, U32>>}
205 checked_indices(left, projected)
206
207def project_left_ranked(+left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +alignment: Shape.Broadcast<Shape.extents(left), Shape.extents(right), Shape.extents(output)>, +values: List<&2, U32>, +same: Shape.BoolCase<Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(output)), Shape.rank_dimensions(values))>) -> {Laws.coordinate_result(left, Shape.projection_checked.ranked(left, output, values, same)) == Laws.project_left_spec(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, Laws.decode(Shape.extents(output), Shape.naturals(values))) : Maybe<&2, List<&2, U32>>}:
208 match same:
209 case Shape.BFalse{equal}:
210 %decode_rank(Shape.dimensions(output), values, equal) : {None{} == Laws.project_left_spec(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, _) : Maybe<&2, List<&2, U32>>}
211 {==}
212 case Shape.BTrue{equal}:
213 project_left_fits(left, right, output, alignment, values, Shape.bool_case(Shape.fit_words(Shape.dimensions(output), values)))
214
215def project_left_checked(+plan: Shape.BroadcastPlan, +values: List<&2, U32>) -> {Laws.coordinate_result(Shape.left_shape(plan), Shape.project_left_checked(plan, values)) == Laws.project_left_spec(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.alignment(plan), Laws.decode(Shape.extents(Shape.output_shape(plan)), Shape.naturals(values))) : Maybe<&2, List<&2, U32>>}:
216 match plan:
217 case Shape.BPlan{+left, +right, +output, +alignment}:
218 project_left_ranked(left, right, output, alignment, values, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(output)), Shape.rank_dimensions(values))))
219
220def projected_right(+left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +alignment: Shape.Broadcast<Shape.extents(left), Shape.extents(right), Shape.extents(output)>, +values: List<&2, U32>, +fits: Coordinates.Fits(Shape.extents(output), Shape.naturals(values))) -> {Shape.projected_words(Shape.dimensions(right), List.drop(&2, U32, values, Nat.sub(Shape.rank_dimensions(values), Shape.rank_dimensions(Shape.dimensions(right))))) == Shape.indices(Shape.extents(right), Shape.project_right(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, Coordinates.coordinate_of(Shape.extents(output), Shape.naturals(values), fits))) : List<&2, Nat>}:
221 +coordinate = Coordinates.coordinate_of(Shape.extents(output), Shape.naturals(values), fits)
222 +expected = Shape.indices(Shape.extents(right), Shape.project_right(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, coordinate))
223 +count = Nat.sub(Shape.rank_dimensions(values), Shape.rank_dimensions(Shape.dimensions(right)))
224 %Equal.sym(List<&2, Nat>, Shape.projected_words(Shape.dimensions(right), List.drop(&2, U32, values, count)), Shape.broadcast_indices(Shape.extents(right), Shape.naturals(List.drop(&2, U32, values, count))), Coordinates.projected_words_spec(Shape.dimensions(right), List.drop(&2, U32, values, count))) : {_ == expected : List<&2, Nat>}
225 %Equal.sym(List<&2, Nat>, Shape.naturals(List.drop(&2, U32, values, count)), List.drop(&2, Nat, Shape.naturals(values), count), Coordinates.naturals_drop(values, count)) : {Shape.broadcast_indices(Shape.extents(right), _) == expected : List<&2, Nat>}
226 %Equal.sym(Nat, Shape.rank_dimensions(values), List.length(&2, Nat, Shape.naturals(values)), Shape.rank_naturals(values)) : {Shape.broadcast_indices(Shape.extents(right), List.drop(&2, Nat, Shape.naturals(values), Nat.sub(_, Shape.rank_dimensions(Shape.dimensions(right))))) == expected : List<&2, Nat>}
227 %Equal.sym(Nat, Shape.rank_dimensions(Shape.dimensions(right)), List.length(&2, Nat, Shape.extents(right)), Shape.rank_naturals(Shape.dimensions(right))) : {Shape.broadcast_indices(Shape.extents(right), List.drop(&2, Nat, Shape.naturals(values), Nat.sub(List.length(&2, Nat, Shape.naturals(values)), _))) == expected : List<&2, Nat>}
228 %Coordinates.indices_of(Shape.extents(output), Shape.naturals(values), fits) : {Shape.project_indices(Shape.extents(right), _) == expected : List<&2, Nat>}
229 Equal.sym(List<&2, Nat>, expected, Shape.project_indices(Shape.extents(right), Shape.indices(Shape.extents(output), coordinate)), Broadcast.project_right(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, coordinate))
230
231def project_right_fits(+left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +alignment: Shape.Broadcast<Shape.extents(left), Shape.extents(right), Shape.extents(output)>, +values: List<&2, U32>, +verdict: Shape.BoolCase<Shape.fit_words(Shape.dimensions(output), values)>) -> {Laws.coordinate_result(right, Shape.projection_checked.fits(right, output, values, verdict)) == Laws.project_right_spec(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, Laws.decode(Shape.extents(output), Shape.naturals(values))) : Maybe<&2, List<&2, U32>>}:
232 match verdict:
233 case Shape.BFalse{equal}:
234 %decode_unfit(Shape.extents(output), Shape.naturals(values), fit_words_false(Shape.dimensions(output), values, equal)) : {None{} == Laws.project_right_spec(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, _) : Maybe<&2, List<&2, U32>>}
235 {==}
236 case Shape.BTrue{equal}:
237 +fits = Coordinates.fits_of(Shape.extents(output), Shape.naturals(values), fit_words_true(Shape.dimensions(output), values, equal))
238 +coordinate = Coordinates.coordinate_of(Shape.extents(output), Shape.naturals(values), fits)
239 +projected = Shape.project_right(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, coordinate)
240 +count = Nat.sub(Shape.rank_dimensions(values), Shape.rank_dimensions(Shape.dimensions(right)))
241 %Equal.sym(Maybe<&2, Shape.Coordinate(Shape.extents(output))>, Laws.decode(Shape.extents(output), Shape.naturals(values)), Some{coordinate}, decode_fit(Shape.extents(output), Shape.naturals(values), fits)) : {Laws.coordinate_result(right, Shape.coordinate_checked.nat(right, Shape.projected_words(Shape.dimensions(right), List.drop(&2, U32, values, count)))) == Laws.project_right_spec(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, _) : Maybe<&2, List<&2, U32>>}
242 %Equal.sym(List<&2, Nat>, Shape.projected_words(Shape.dimensions(right), List.drop(&2, U32, values, count)), Shape.indices(Shape.extents(right), projected), projected_right(left, right, output, alignment, values, fits)) : {Laws.coordinate_result(right, Shape.coordinate_checked.nat(right, _)) == Some{Shape.words(Shape.indices(Shape.extents(right), projected))} : Maybe<&2, List<&2, U32>>}
243 checked_indices(right, projected)
244
245def project_right_ranked(+left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +alignment: Shape.Broadcast<Shape.extents(left), Shape.extents(right), Shape.extents(output)>, +values: List<&2, U32>, +same: Shape.BoolCase<Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(output)), Shape.rank_dimensions(values))>) -> {Laws.coordinate_result(right, Shape.projection_checked.ranked(right, output, values, same)) == Laws.project_right_spec(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, Laws.decode(Shape.extents(output), Shape.naturals(values))) : Maybe<&2, List<&2, U32>>}:
246 match same:
247 case Shape.BFalse{equal}:
248 %decode_rank(Shape.dimensions(output), values, equal) : {None{} == Laws.project_right_spec(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, _) : Maybe<&2, List<&2, U32>>}
249 {==}
250 case Shape.BTrue{equal}:
251 project_right_fits(left, right, output, alignment, values, Shape.bool_case(Shape.fit_words(Shape.dimensions(output), values)))
252
253def project_right_checked(+plan: Shape.BroadcastPlan, +values: List<&2, U32>) -> {Laws.coordinate_result(Shape.right_shape(plan), Shape.project_right_checked(plan, values)) == Laws.project_right_spec(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.alignment(plan), Laws.decode(Shape.extents(Shape.output_shape(plan)), Shape.naturals(values))) : Maybe<&2, List<&2, U32>>}:
254 match plan:
255 case Shape.BPlan{+left, +right, +output, +alignment}:
256 project_right_ranked(left, right, output, alignment, values, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(output)), Shape.rank_dimensions(values))))
257
258def project_left_index(+plan: Shape.BroadcastPlan, +map: Shape.Index<Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))>, +index: Shape.FlatIndex<Shape.output_shape(plan)>) -> {Some{Shape.index_value(Shape.left_shape(plan), Flat.project_left_index(plan, map, index))} == Laws.flatten_spec(Shape.extents(Shape.left_shape(plan)), Laws.project_left_coordinate(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.alignment(plan), Laws.fin_of(Shape.numel(Shape.extents(Shape.output_shape(plan))), Laws.position(Shape.output_shape(plan), index)))) : Maybe<&2, U32>}:
259 match map index:
260 case Shape.Indexed{+rows, +exact} Shape.FIndex{+value, +bound}:
261 +left = Shape.extents(Shape.left_shape(plan))
262 +right = Shape.extents(Shape.right_shape(plan))
263 +output = Shape.extents(Shape.output_shape(plan))
264 +fits = Coordinates.size_fits(Shape.output_shape(plan), value, bound)
265 +flat = Coordinates.fin_from(Shape.numel(output), value, fits)
266 +table = Shape.index_table(left, right, output)
267 +projected = Shape.row_major(Shape.extents(Shape.left_shape(plan)), Shape.project_left(left, right, output, Shape.alignment(plan), Shape.unflatten(output, flat)))
268 %Equal.sym(Maybe<&2, Shape.Fin(Shape.numel(output))>, Laws.fin_of(Shape.numel(output), value), Some{flat}, fin_of_from(Shape.numel(output), value, fits)) : {Some{U32.from_nat(Shape.walk_left(rows, value))} == Laws.flatten_spec(Shape.extents(Shape.left_shape(plan)), Laws.project_left_coordinate(left, right, output, Shape.alignment(plan), _)) : Maybe<&2, U32>}
269 %Equal.sym(List<&2, Shape.Row>, rows, table, exact) : {Some{U32.from_nat(Shape.walk_left(_, value))} == Some{U32.from_nat(projected)} : Maybe<&2, U32>}
270 %Coordinates.fin_from_value(Shape.numel(output), value, fits) : {Some{U32.from_nat(Shape.walk_left(table, _))} == Some{U32.from_nat(projected)} : Maybe<&2, U32>}
271 Equal.cong(Nat, Maybe<&2, U32>, flat => Some{U32.from_nat(flat)}, Shape.walk_left(table, Shape.Fin.value(Shape.numel(output), flat)), projected, Projection.walk_left_value(left, right, output, Shape.alignment(plan), flat))
272 case Shape.Unindexed{zero} Shape.FIndex{+value, bound}:
273 +left = Shape.extents(Shape.left_shape(plan))
274 +right = Shape.extents(Shape.right_shape(plan))
275 +output = Shape.extents(Shape.output_shape(plan))
276 Empty.absurd({Some{Shape.index_value(Shape.left_shape(plan), Flat.project_left_index(plan, Shape.Unindexed{zero}, Shape.FIndex{value, bound}))} == Laws.flatten_spec(Shape.extents(Shape.left_shape(plan)), Laws.project_left_coordinate(left, right, output, Shape.alignment(plan), Laws.fin_of(Shape.numel(output), value))) : Maybe<&2, U32>}, Flat.hollow(Shape.output_shape(plan), value, zero, bound))
277
278def project_right_index(+plan: Shape.BroadcastPlan, +map: Shape.Index<Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))>, +index: Shape.FlatIndex<Shape.output_shape(plan)>) -> {Some{Shape.index_value(Shape.right_shape(plan), Flat.project_right_index(plan, map, index))} == Laws.flatten_spec(Shape.extents(Shape.right_shape(plan)), Laws.project_right_coordinate(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.alignment(plan), Laws.fin_of(Shape.numel(Shape.extents(Shape.output_shape(plan))), Laws.position(Shape.output_shape(plan), index)))) : Maybe<&2, U32>}:
279 match map index:
280 case Shape.Indexed{+rows, +exact} Shape.FIndex{+value, +bound}:
281 +left = Shape.extents(Shape.left_shape(plan))
282 +right = Shape.extents(Shape.right_shape(plan))
283 +output = Shape.extents(Shape.output_shape(plan))
284 +fits = Coordinates.size_fits(Shape.output_shape(plan), value, bound)
285 +flat = Coordinates.fin_from(Shape.numel(output), value, fits)
286 +table = Shape.index_table(left, right, output)
287 +projected = Shape.row_major(Shape.extents(Shape.right_shape(plan)), Shape.project_right(left, right, output, Shape.alignment(plan), Shape.unflatten(output, flat)))
288 %Equal.sym(Maybe<&2, Shape.Fin(Shape.numel(output))>, Laws.fin_of(Shape.numel(output), value), Some{flat}, fin_of_from(Shape.numel(output), value, fits)) : {Some{U32.from_nat(Shape.walk_right(rows, value))} == Laws.flatten_spec(Shape.extents(Shape.right_shape(plan)), Laws.project_right_coordinate(left, right, output, Shape.alignment(plan), _)) : Maybe<&2, U32>}
289 %Equal.sym(List<&2, Shape.Row>, rows, table, exact) : {Some{U32.from_nat(Shape.walk_right(_, value))} == Some{U32.from_nat(projected)} : Maybe<&2, U32>}
290 %Coordinates.fin_from_value(Shape.numel(output), value, fits) : {Some{U32.from_nat(Shape.walk_right(table, _))} == Some{U32.from_nat(projected)} : Maybe<&2, U32>}
291 Equal.cong(Nat, Maybe<&2, U32>, flat => Some{U32.from_nat(flat)}, Shape.walk_right(table, Shape.Fin.value(Shape.numel(output), flat)), projected, Projection.walk_right_value(left, right, output, Shape.alignment(plan), flat))
292 case Shape.Unindexed{zero} Shape.FIndex{+value, bound}:
293 +left = Shape.extents(Shape.left_shape(plan))
294 +right = Shape.extents(Shape.right_shape(plan))
295 +output = Shape.extents(Shape.output_shape(plan))
296 Empty.absurd({Some{Shape.index_value(Shape.right_shape(plan), Flat.project_right_index(plan, Shape.Unindexed{zero}, Shape.FIndex{value, bound}))} == Laws.flatten_spec(Shape.extents(Shape.right_shape(plan)), Laws.project_right_coordinate(left, right, output, Shape.alignment(plan), Laws.fin_of(Shape.numel(output), value))) : Maybe<&2, U32>}, Flat.hollow(Shape.output_shape(plan), value, zero, bound))