def align_complete

bendtorch-core@0.1.0.0 · src/shape/plan_proofs.bend:136

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

136def align_complete(+left: List<&2, U32>, +right: List<&2, U32>, +output: List<&2, Nat>, +aligned: Shape.Aligned(Shape.naturals(left), Shape.naturals(right), output)) -> {Some{output} == aligned_output(left, right, Shape.align(left, right)) : Maybe<&2, List<&2, Nat>>}:
137  match left right output:
138    case Nil{} Nil{} Nil{}:
139      {==}
140    case +lh <> +lt +rh <> +rt +oh <> +ot:
141      Shape.AStep{+axis, +tail} = aligned
142      align_step_complete(lh, lt, rh, rt, oh, ot, Shape.align(lt, rt), Shape.axis_choice(lh, rh), align_complete(lt, rt, ot, tail), axis_complete(lh, rh, oh, axis))
143    case Nil{} Nil{} oh <> ot:
144      match aligned:
145    case Nil{} rh <> rt Nil{}:
146      match aligned:
147    case lh <> lt Nil{} Nil{}:
148      match aligned:
149    case Nil{} rh <> rt oh <> ot:
150      match aligned:
151    case lh <> lt Nil{} oh <> ot:
152      match aligned:
153    case lh <> lt rh <> rt Nil{}:
154      match aligned: