def plan_left_status

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

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/tensor/math_totality.bend as Totality

1119def plan_left_status(dimensions: List<&2, U32>, +left: Shape.Shape, +right: Shape.Shape,
1120  -same: {dimensions == Shape.dimensions(left) : List<&2, U32>}, -valid: Totality.MatrixInputs<left, right>) ->
1121  PlanStatus<left, right, Matrix.plan_left(left, right, dimensions, same)>:
1122  match dimensions:
1123    case +rows <> +inner <> Nil{}:
1124      plan_right_status(Shape.dimensions(right), left, right, rows, inner, Equal.sym(List<&2, U32>, [rows, inner], Shape.dimensions(left), same), {==}, valid)
1125    case Nil{}:
1126      PlanStatus{Empty.absurd({False{} == True{} : Bool}, {\{Totality.Impossible: empty => empty} : Totality.Impossible -> Empty}(rank_clash(left, right, Nil{}, same, {==}, valid)))}
1127    case head <> Nil{}:
1128      PlanStatus{Empty.absurd({False{} == True{} : Bool}, {\{Totality.Impossible: empty => empty} : Totality.Impossible -> Empty}(rank_clash(left, right, [head], same, {==}, valid)))}
1129    case first <> second <> third <> rest:
1130      PlanStatus{Empty.absurd({False{} == True{} : Bool}, {\{Totality.Impossible: empty => empty} : Totality.Impossible -> Empty}(rank_clash(left, right, first <> second <> third <> rest, same, {==}, valid)))}