def dot_decision

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

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/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix
import bendtorch-core@0.1.0.0/src/tensor/matmul_LAWS.bend as Laws

236def dot_decision(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, a: Core.Tensor<left>, -b: Core.Tensor<right>,
237  +row: U32, +column: U32, +cursor: Nat, +accumulator: F32,
238  -rec: @a: Core.Tensor<left> -> @b: Core.Tensor<right> -> @+value: F32 ->
239    Laws.SourceDot<fuel, left, right, a, b, row, column, 1n+cursor, value, Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value)>,
240  decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)>) ->
241  Laws.SourceDot<1n+fuel, left, right, a, b, row, column, cursor, accumulator, Matrix.dot_decided(left, right,
242    a => b => value => Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value), a, b, row, column, cursor, U32.from_nat(cursor), accumulator, decision)>:
243  match decision:
244    case Shape.BFalse{equal}:
245      Laws.SourceDot{unit => Unit{}}
246    case Shape.BTrue{equal}:
247      left_certificate(fuel, left, right, a, b, row, column, cursor, accumulator, rec,
248        Lifecycle.natural_equal(U32.to_nat(U32.from_nat(cursor)), cursor, equal), coordinate_certificate(left, a, [row, U32.from_nat(cursor)]))