~/jendhub

def decoded_offset

bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:1297

import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformPROOF
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/index_proofs.bend as ShapeIndex
import bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend as Mapping

1297def decoded_offset(+shape: Shape.Shape, +index: U32,
1298  +inside: {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(shape)) : Bool}) ->
1299  {Shape.offset(Shape.extents(shape), Shape.digits(Shape.extents(shape), U32.to_nat(index))) == U32.to_nat(index) : Nat}:
1300  %Mapping.decoded_indices(shape, index, inside) : {Shape.offset(Shape.extents(shape), _) == U32.to_nat(index) : Nat}
1301  Equal.trans(Nat, Shape.offset(Shape.extents(shape), Shape.indices(Shape.extents(shape), Mapping.decoded_coordinate(shape, index, inside))),
1302    Shape.row_major(Shape.extents(shape), Mapping.decoded_coordinate(shape, index, inside)), U32.to_nat(index),
1303    Coordinates.offset_indices(Shape.extents(shape), Mapping.decoded_coordinate(shape, index, inside)),
1304    Equal.trans(Nat, Shape.row_major(Shape.extents(shape), Mapping.decoded_coordinate(shape, index, inside)),
1305      Shape.Fin.value(Shape.numel(Shape.extents(shape)),
1306        Coordinates.fin_from(Shape.numel(Shape.extents(shape)), U32.to_nat(index), Coordinates.size_fits(shape, U32.to_nat(index), inside))),
1307      U32.to_nat(index),
1308      Equal.trans(Nat, Shape.row_major(Shape.extents(shape), Mapping.decoded_coordinate(shape, index, inside)),
1309        Shape.Fin.value(Shape.numel(Shape.extents(shape)), Shape.flatten(Shape.extents(shape), Mapping.decoded_coordinate(shape, index, inside))),
1310        Shape.Fin.value(Shape.numel(Shape.extents(shape)),
1311          Coordinates.fin_from(Shape.numel(Shape.extents(shape)), U32.to_nat(index), Coordinates.size_fits(shape, U32.to_nat(index), inside))),
1312        Equal.sym(Nat, Shape.Fin.value(Shape.numel(Shape.extents(shape)), Shape.flatten(Shape.extents(shape), Mapping.decoded_coordinate(shape, index, inside))),
1313          Shape.row_major(Shape.extents(shape), Mapping.decoded_coordinate(shape, index, inside)),
1314          ShapeIndex.flatten_row_major(Shape.extents(shape), Mapping.decoded_coordinate(shape, index, inside))),
1315        Equal.cong(Shape.Fin(Shape.numel(Shape.extents(shape))), Nat, value => Shape.Fin.value(Shape.numel(Shape.extents(shape)), value),
1316          Shape.flatten(Shape.extents(shape), Mapping.decoded_coordinate(shape, index, inside)),
1317          Coordinates.fin_from(Shape.numel(Shape.extents(shape)), U32.to_nat(index), Coordinates.size_fits(shape, U32.to_nat(index), inside)),
1318          ShapeIndex.flatten_unflatten(Shape.extents(shape),
1319            Coordinates.fin_from(Shape.numel(Shape.extents(shape)), U32.to_nat(index), Coordinates.size_fits(shape, U32.to_nat(index), inside))))),
1320      Coordinates.fin_from_value(Shape.numel(Shape.extents(shape)), U32.to_nat(index), Coordinates.size_fits(shape, U32.to_nat(index), inside))))

Uses (27)

Used by (1)