def right_bound

bendtorch-core@0.1.0.0 · src/shape/flat.bend:35

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as Coordinates
import bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend as Projection

35def right_bound(+plan: Shape.BroadcastPlan, -rows: List<&2, Shape.Row>, exact: {rows == Shape.index_table(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))) : List<&2, Shape.Row>}, +value: Nat, bound: {True{} == Nat.is_lt(value, Shape.elements(Shape.output_shape(plan))) : Bool}) -> {True{} == Nat.is_lt(Shape.walk_right(rows, value), Shape.elements(Shape.right_shape(plan))) : Bool}:
36  +left = Shape.extents(Shape.left_shape(plan))
37  +right = Shape.extents(Shape.right_shape(plan))
38  +output = Shape.extents(Shape.output_shape(plan))
39  +input = Shape.right_shape(plan)
40  +fits = Coordinates.size_fits(Shape.output_shape(plan), value, bound)
41  +index = Coordinates.fin_from(Shape.numel(output), value, fits)
42  +projected = Shape.project_right(left, right, output, Shape.alignment(plan), Shape.unflatten(output, index))
43  +table = Shape.index_table(left, right, output)
44  %Equal.sym(List<&2, Shape.Row>, rows, table, exact) : {True{} == Nat.is_lt(Shape.walk_right(_, value), Shape.elements(input)) : Bool}
45  %Coordinates.fin_from_value(Shape.numel(output), value, fits) : {True{} == Nat.is_lt(Shape.walk_right(table, _), Shape.elements(input)) : Bool}
46  %Equal.sym(Nat, Shape.walk_right(table, Shape.Fin.value(Shape.numel(output), index)), Shape.row_major(Shape.extents(input), projected), Projection.walk_right_value(left, right, output, Shape.alignment(plan), index)) : {True{} == Nat.is_lt(_, Shape.elements(input)) : Bool}
47  %Equal.sym(Nat, Shape.elements(input), Shape.numel(Shape.extents(input)), Shape.elements_exact(input)) : {True{} == Nat.is_lt(Shape.row_major(Shape.extents(input), projected), _) : Bool}
48  %Nats.lt_true(Shape.row_major(Shape.extents(input), projected), Shape.numel(Shape.extents(input)), Coordinates.row_major_lt(Shape.extents(input), projected)) : {True{} == _ : Bool}
49  {==}