def flat_pair
bendtorch-core@0.1.0.0 · src/tensor/matrix_index_proof.bend:188
import bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend as MatrixIndexProof
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as ShapeLaws
import bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend as Boundary
import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as Coordinates
188def flat_pair(+shape: Shape.Shape, +first: U32, +second: U32, +x: U32, +y: U32,
189 +dimensions: {Shape.dimensions(shape) == [first, second] : List<&2, U32>},
190 x_inside: {Nat.is_lt(U32.to_nat(x), U32.to_nat(first)) == True{} : Bool},
191 y_inside: {Nat.is_lt(U32.to_nat(y), U32.to_nat(second)) == True{} : Bool}) ->
192 {ShapeLaws.index_result(shape, Shape.flatten_checked(shape, [x, y])) ==
193 Some{U32.from_nat(Nat.add(Nat.mul(U32.to_nat(x), U32.to_nat(second)), U32.to_nat(y)))} : Maybe<&2, U32>}:
194 +values : List<&2, Nat> = [U32.to_nat(x), U32.to_nat(y)]
195 +fits = Coordinates.pair_fits(shape, first, second, x, y, dimensions, x_inside, y_inside)
196 +coordinate = Coordinates.coordinate_of(Shape.extents(shape), values, fits)
197 +target : Maybe<&2, U32> = Some{U32.from_nat(Nat.add(Nat.mul(U32.to_nat(x), U32.to_nat(second)), U32.to_nat(y)))}
198 Equal.trans(Maybe<&2, U32>, ShapeLaws.index_result(shape, Shape.flatten_checked(shape, [x, y])),
199 ShapeLaws.flatten_spec(Shape.extents(shape), ShapeLaws.decode(Shape.extents(shape), values)), target,
200 Boundary.flatten_checked(shape, [x, y]),
201 Equal.trans(Maybe<&2, U32>, ShapeLaws.flatten_spec(Shape.extents(shape), ShapeLaws.decode(Shape.extents(shape), values)),
202 Some{U32.from_nat(Shape.row_major(Shape.extents(shape), coordinate))}, target,
203 Equal.cong(Maybe<&2, Shape.Coordinate(Shape.extents(shape))>, Maybe<&2, U32>, found => ShapeLaws.flatten_spec(Shape.extents(shape), found),
204 ShapeLaws.decode(Shape.extents(shape), values), Some{coordinate}, Boundary.decode_fit(Shape.extents(shape), values, fits)),
205 Equal.trans(Maybe<&2, U32>, Some{U32.from_nat(Shape.row_major(Shape.extents(shape), coordinate))},
206 Some{U32.from_nat(Shape.offset(Shape.extents(shape), values))}, target,
207 Equal.cong(Nat, Maybe<&2, U32>, offset => Some{U32.from_nat(offset)}, Shape.row_major(Shape.extents(shape), coordinate),
208 Shape.offset(Shape.extents(shape), values), Coordinates.offset_of(Shape.extents(shape), values, fits)),
209 Equal.trans(Maybe<&2, U32>, Some{U32.from_nat(Shape.offset(Shape.extents(shape), values))},
210 Some{U32.from_nat(Shape.offset([U32.to_nat(first), U32.to_nat(second)], values))}, target,
211 Equal.cong(List<&2, U32>, Maybe<&2, U32>, dims => Some{U32.from_nat(Shape.offset(Shape.naturals(dims), values))},
212 Shape.dimensions(shape), [first, second], dimensions),
213 Equal.cong(Nat, Maybe<&2, U32>, offset => Some{U32.from_nat(offset)},
214 Shape.offset([U32.to_nat(first), U32.to_nat(second)], values),
215 Nat.add(Nat.mul(U32.to_nat(x), U32.to_nat(second)), U32.to_nat(y)),
216 offset_pair(U32.to_nat(x), U32.to_nat(y), U32.to_nat(first), U32.to_nat(second)))))))