def decoded_of

bendtorch-core@0.1.0.0 · src/tensor/matmul_PROOF.bend:1440

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as ShapeLaws
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as Parallel
import bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend as MatrixIndex

1440def decoded_of(+output: Shape.Shape, +index: U32, +row: U32, +column: U32,
1441  result: Result<&2, &2, Shape.Error, Shape.CheckedCoordinate<output>>,
1442  -same: {result == Shape.unflatten_checked(output, index) : Result<&2, &2, Shape.Error, Shape.CheckedCoordinate<output>>},
1443  -found: {ShapeLaws.coordinate_result(output, result) == Some{[row, column]} : Maybe<&2, List<&2, U32>>}) ->
1444  Parallel.Fact<Decoded<output, index, row, column>>:
1445  match result:
1446    case Fail{error}:
1447      Parallel.Fact{Empty.absurd(Decoded<output, index, row, column>,
1448        Arith.clash(Equal.cong(Maybe<&2, List<&2, U32>>, Bool, value => Maybe.is_some(&2, List<&2, U32>, value), None{}, Some{[row, column]}, found)))}
1449    case Done{coordinate}:
1450      Parallel.Fact{Decoded{coordinate,
1451        Equal.sym(Result<&2, &2, Shape.Error, Shape.CheckedCoordinate<output>>, Done{coordinate}, Shape.unflatten_checked(output, index), same),
1452        MatrixIndex.some_equal(List<&2, U32>, Shape.coordinate_values(output, coordinate), [row, column], found)}}