def left_bound

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

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

12def left_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_left(rows, value), Shape.elements(Shape.left_shape(plan))) : Bool}:
13  +left = Shape.extents(Shape.left_shape(plan))
14  +right = Shape.extents(Shape.right_shape(plan))
15  +output = Shape.extents(Shape.output_shape(plan))
16  +input = Shape.left_shape(plan)
17  +fits = Coordinates.size_fits(Shape.output_shape(plan), value, bound)
18  +index = Coordinates.fin_from(Shape.numel(output), value, fits)
19  +projected = Shape.project_left(left, right, output, Shape.alignment(plan), Shape.unflatten(output, index))
20  +table = Shape.index_table(left, right, output)
21  %Equal.sym(List<&2, Shape.Row>, rows, table, exact) : {True{} == Nat.is_lt(Shape.walk_left(_, value), Shape.elements(input)) : Bool}
22  %Coordinates.fin_from_value(Shape.numel(output), value, fits) : {True{} == Nat.is_lt(Shape.walk_left(table, _), Shape.elements(input)) : Bool}
23  %Equal.sym(Nat, Shape.walk_left(table, Shape.Fin.value(Shape.numel(output), index)), Shape.row_major(Shape.extents(input), projected), Projection.walk_left_value(left, right, output, Shape.alignment(plan), index)) : {True{} == Nat.is_lt(_, Shape.elements(input)) : Bool}
24  %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}
25  %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}
26  {==}