def aligned_right

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

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

66def aligned_right(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +alignment: Shape.Aligned(left, right, output), +coordinate: Shape.Coordinate(output)) -> {Shape.indices(right, Shape.Aligned.project_right(left, right, output, alignment, coordinate)) == Shape.broadcast_indices(right, Shape.indices(output, coordinate)) : List<&2, Nat>}:
67  match left right output:
68    case Nil{} Nil{} Nil{}:
69      {==}
70    case +lh <> +lt +rh <> +rt +oh <> +ot:
71      Shape.AStep{+axis, +tail} = alignment
72      Shape.CStep{+index, +rest} = coordinate
73      %aligned_right(lt, rt, ot, tail, rest) : {Shape.Fin.value(rh, Shape.Axis.project_right(lh, rh, oh, axis, index)) <> Shape.indices(rt, Shape.Aligned.project_right(lt, rt, ot, tail, rest)) == Shape.broadcast_index(rh, Shape.Fin.value(oh, index)) <> _ : List<&2, Nat>}
74      %axis_right(lh, rh, oh, axis, index) : {Shape.Fin.value(rh, Shape.Axis.project_right(lh, rh, oh, axis, index)) <> Shape.indices(rt, Shape.Aligned.project_right(lt, rt, ot, tail, rest)) == _ <> Shape.indices(rt, Shape.Aligned.project_right(lt, rt, ot, tail, rest)) : List<&2, Nat>}
75      {==}
76    case Nil{} Nil{} oh <> ot:
77      match alignment:
78    case Nil{} rh <> rt Nil{}:
79      match alignment:
80    case lh <> lt Nil{} Nil{}:
81      match alignment:
82    case Nil{} rh <> rt oh <> ot:
83      match alignment:
84    case lh <> lt Nil{} oh <> ot:
85      match alignment:
86    case lh <> lt rh <> rt Nil{}:
87      match alignment: