def broadcast_unique

bendtorch-core@0.1.0.0 · src/shape/unique_proofs.bend:130

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape

130def broadcast_unique(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +other: List<&2, Nat>, +first: Shape.Broadcast<left, right, output>, +second: Shape.Broadcast<left, right, other>) -> {output == other : List<&2, Nat>}:
131  match first:
132    case Shape.BAlign{+lp1, +rp1, +m1, +a1}:
133      match second:
134        case Shape.BAlign{+lp2, +rp2, +m2, +a2}:
135          +left_rank = List.length(&2, Nat, left)
136          +right_rank = List.length(&2, Nat, right)
137          +e1 = balance(lp1, rp1, left, right, output, a1)
138          +e2 = balance(lp2, rp2, left, right, other, a2)
139          +same_left = left_padding_equal(lp1, rp1, lp2, rp2, left_rank, right_rank, m1, m2, e1, e2)
140          +same_right = cancel_right(rp1, rp2, right_rank, Equal.trans(Nat, Nat.add(rp1, right_rank), Nat.add(lp1, left_rank), Nat.add(rp2, right_rank), Equal.sym(Nat, Nat.add(lp1, left_rank), Nat.add(rp1, right_rank), e1), Equal.trans(Nat, Nat.add(lp1, left_rank), Nat.add(lp2, left_rank), Nat.add(rp2, right_rank), Equal.cong(Nat, Nat, value => Nat.add(value, left_rank), lp1, lp2, same_left), e2)))
141          aligned_unique(Shape.pad(lp1, left), Shape.pad(rp1, right), output, other, a1, retype(lp1, lp2, rp1, rp2, left, right, other, same_left, same_right, a2))