def inner_left

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

1246def inner_left(+left: Shape.Shape, +right: Shape.Shape, +dims: List<&2, U32>,
1247  -same: {dims == Shape.dimensions(left) : List<&2, U32>},
1248  -rows: U32, -inner: U32, -right_inner: U32, -columns: U32,
1249  left_matrix: {dims == [rows, inner] : List<&2, U32>},
1250  right_matrix: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
1251  mismatch: {U32.to_nat(inner) != U32.to_nat(right_inner) : Nat}) ->
1252  {Matrix.plan_left(left, right, dims, same) == Fail{Matrix.InnerDimensionMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>}:
1253  match dims:
1254    case +r <> +i <> Nil{}:
1255      inner_right(left, right, r, i, Equal.sym(List<&2, U32>, [r, i], Shape.dimensions(left), same), Shape.dimensions(right), {==},
1256        inner, right_inner, columns, right_matrix,
1257        Equal.cong(List<&2, U32>, Nat, second_nat, [r, i], [rows, inner], left_matrix), mismatch)
1258    case Nil{}:
1259      Empty.absurd({Matrix.plan_left(left, right, Nil{}, same) == Fail{Matrix.InnerDimensionMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>},
1260        Arith.clash(Equal.cong(List<&2, U32>, Bool, xs => Nat.is_eq(Shape.rank_dimensions(xs), 2n), Nil{}, [rows, inner], left_matrix)))
1261    case +x <> Nil{}:
1262      Empty.absurd({Matrix.plan_left(left, right, [x], same) == Fail{Matrix.InnerDimensionMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>},
1263        Arith.clash(Equal.cong(List<&2, U32>, Bool, xs => Nat.is_eq(Shape.rank_dimensions(xs), 2n), [x], [rows, inner], left_matrix)))
1264    case +x <> +y <> +z <> +t:
1265      Empty.absurd({Matrix.plan_left(left, right, x <> y <> z <> t, same) == Fail{Matrix.InnerDimensionMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>},
1266        Arith.clash(Equal.cong(List<&2, U32>, Bool, xs => Nat.is_eq(Shape.rank_dimensions(xs), 2n), x <> y <> z <> t, [rows, inner], left_matrix)))