def geometry_decided

bendtorch-core@0.1.0.0 · src/tensor/batched_matmul_PROOF.bend:770

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend as Batched

770def geometry_decided(+lr: Nat, +l1: U32, +l2: U32, +rows: U32, +inner: U32, +lv: Bool, +rr: Nat, +r1: U32, +r2: U32, +columns: U32,
771  +rinner: U32, +rv: Bool, decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(inner), U32.to_nat(rinner))>) ->
772  ExpectedOf(lr, l1, l2, rows, inner, lv, rr, r1, r2, columns, rinner, rv,
773    Batched.compatible(Batched.Operand{Batched.Batch{lr, l1, l2}, rows, inner, lv}, Batched.Operand{Batched.Batch{rr, r1, r2}, columns, rinner, rv},
774      Nat.is_eq(U32.to_nat(inner), U32.to_nat(rinner)))):
775  match decision:
776    case Shape.BFalse{equal}:
777      %equal : ExpectedOf(lr, l1, l2, rows, inner, lv, rr, r1, r2, columns, rinner, rv,
778        Batched.compatible(Batched.Operand{Batched.Batch{lr, l1, l2}, rows, inner, lv}, Batched.Operand{Batched.Batch{rr, r1, r2}, columns, rinner, rv}, _))
779      Unit{}
780    case Shape.BTrue{+equal}:
781      %equal : ExpectedOf(lr, l1, l2, rows, inner, lv, rr, r1, r2, columns, rinner, rv,
782        Batched.compatible(Batched.Operand{Batched.Batch{lr, l1, l2}, rows, inner, lv}, Batched.Operand{Batched.Batch{rr, r1, r2}, columns, rinner, rv}, _))
783      geometry_batched(lr, l1, l2, rows, inner, lv, rr, r1, r2, columns, rinner, rv,
784        Lifecycle.natural_equal(U32.to_nat(inner), U32.to_nat(rinner), equal),
785        Batched.axis(l1, r1), Batched.axis(l2, r2), axis_meaning(l1, r1), axis_meaning(l2, r2))