def aligned_left

bendtorch-core@0.1.0.0 · src/shape/broadcast_proofs.bend:43

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

43def aligned_left(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +alignment: Shape.Aligned(left, right, output), +coordinate: Shape.Coordinate(output)) -> {Shape.indices(left, Shape.Aligned.project_left(left, right, output, alignment, coordinate)) == Shape.broadcast_indices(left, Shape.indices(output, coordinate)) : List<&2, Nat>}:
44  match left right output:
45    case Nil{} Nil{} Nil{}:
46      {==}
47    case +lh <> +lt +rh <> +rt +oh <> +ot:
48      Shape.AStep{+axis, +tail} = alignment
49      Shape.CStep{+index, +rest} = coordinate
50      %aligned_left(lt, rt, ot, tail, rest) : {Shape.Fin.value(lh, Shape.Axis.project_left(lh, rh, oh, axis, index)) <> Shape.indices(lt, Shape.Aligned.project_left(lt, rt, ot, tail, rest)) == Shape.broadcast_index(lh, Shape.Fin.value(oh, index)) <> _ : List<&2, Nat>}
51      %axis_left(lh, rh, oh, axis, index) : {Shape.Fin.value(lh, Shape.Axis.project_left(lh, rh, oh, axis, index)) <> Shape.indices(lt, Shape.Aligned.project_left(lt, rt, ot, tail, rest)) == _ <> Shape.indices(lt, Shape.Aligned.project_left(lt, rt, ot, tail, rest)) : List<&2, Nat>}
52      {==}
53    case Nil{} Nil{} oh <> ot:
54      match alignment:
55    case Nil{} rh <> rt Nil{}:
56      match alignment:
57    case lh <> lt Nil{} Nil{}:
58      match alignment:
59    case Nil{} rh <> rt oh <> ot:
60      match alignment:
61    case lh <> lt Nil{} oh <> ot:
62      match alignment:
63    case lh <> lt rh <> rt Nil{}:
64      match alignment: