def output_status

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix
import bendtorch-core@0.1.0.0/src/tensor/math_totality.bend as Totality
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise

1625# The parallel product succeeds on valid inputs: after the plan and the
1626# allocation, nothing it does can fail.
1627def output_status(+output: Shape.Shape, +inner: Nat, +columns: Nat, +depth: Nat, +length: Nat, -valid: {Storage.bounds(depth, length) == True{} : Bool},
1628  -exact: {length == Shape.logical_numel(Shape.dimensions(output)) : Nat},
1629  +left: Shape.Shape, a: Core.Tensor<left>, +right: Shape.Shape, b: Core.Tensor<right>) ->
1630  Totality.Status<Matrix.Error, Core.Dynamic & Core.Dynamic & Core.Dynamic,
1631    Matrix.parallel_output(output, inner, columns, depth, length, valid, exact, Elementwise.take(Core.pack(left, a)), Elementwise.take(Core.pack(right, b)))>:
1632  take_lift(left, a, taken => Totality.Status<Matrix.Error, Core.Dynamic & Core.Dynamic & Core.Dynamic,
1633      Matrix.parallel_output(output, inner, columns, depth, length, valid, exact, taken, Elementwise.take(Core.pack(right, b)))>,
1634    kept_left => copy_left => taken_left =>
1635      take_lift(right, b, taken => Totality.Status<Matrix.Error, Core.Dynamic & Core.Dynamic & Core.Dynamic,
1636          Matrix.parallel_output(output, inner, columns, depth, length, valid, exact, (Core.Packed{left, kept_left}, copy_left), taken)>,
1637        kept_right => copy_right => taken_right => Totality.Status{{==}}))