def flatten_ranked_bounds

bendtorch-core@0.1.0.0 · src/shape/PROOF.bend:82

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend as Plan

82def flatten_ranked_bounds(+shape: Shape.Shape, +values: List<&2, U32>,
83  same_rank: Shape.BoolCase<Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.rank_dimensions(values))>,
84  same: {Shape.rank_dimensions(Shape.dimensions(shape)) == Shape.rank_dimensions(values) : Nat},
85  outside: {Shape.fit_words(Shape.dimensions(shape), values) == False{} : Bool}) ->
86  {Shape.flatten_checked.ranked(shape, values, same_rank) == Fail{Shape.CoordinateOutOfBounds{}} : Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>}:
87  match same_rank:
88    case Shape.BFalse{equal}:
89      Empty.absurd({Shape.flatten_checked.ranked(shape, values, Shape.BFalse{equal}) == Fail{Shape.CoordinateOutOfBounds{}} : Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>},
90        Shape.clash(Equal.trans(Bool, True{}, Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.rank_dimensions(values)), False{},
91          Plan.eq_true(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.rank_dimensions(values), same),
92          Equal.sym(Bool, False{}, Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.rank_dimensions(values)), equal))))
93    case Shape.BTrue{equal}:
94      flatten_fits_bounds(shape, values, Shape.bool_case(Shape.fit_words(Shape.dimensions(shape), values)), outside)