def project_right_fits
bendtorch-core@0.1.0.0 · src/shape/boundary_proofs.bend:231
import bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend as BoundaryProofs
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as Coordinates
import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as Laws
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)