def words_valid_of

bendtorch-core@0.1.0.0 · src/tensor/permutation_mapping.bend:318

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as Coordinates

318def words_valid_of(+dimensions: List<&2, U32>, +values: List<&2, U32>,
319  fits: Coordinates.Fits(Shape.naturals(dimensions), Shape.naturals(values))) -> Layout.WordsValid(dimensions, values):
320  match dimensions values:
321    case Nil{} Nil{}:
322      Unit{}
323    case +dimension <> +dt +value <> +vt:
324      Coordinates.FStep{bound, tail} = fits
325      Layout.WStep{
326        %Arith.u32_lt(value, dimension) : {True{} == _ : Bool}
327        bound,
328        words_valid_of(dt, vt, tail)}
329    case Nil{} head <> tail:
330      match fits:
331    case head <> tail Nil{}:
332      match fits: