def projected_right

bendtorch-core@0.1.0.0 · src/shape/boundary_proofs.bend:220

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as Broadcast
import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as Coordinates

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))