def align_step_complete

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

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

123def align_step_complete(-lh: U32, -lt: List<&2, U32>, -rh: U32, -rt: List<&2, U32>, -oh: Nat, -ot: List<&2, Nat>, +rest: Shape.Alignment<lt, rt>, +choice: Shape.AxisChoice<lh, rh>, rest_seen: {Some{ot} == aligned_output(lt, rt, rest) : Maybe<&2, List<&2, Nat>>}, choice_seen: {Some{oh} == choice_output(lh, rh, choice) : Maybe<&2, Nat>}) -> {Some{oh <> ot} == aligned_output(lh <> lt, rh <> rt, Shape.align.step(lh, lt, rh, rt, rest, choice)) : Maybe<&2, List<&2, Nat>>}:
124  match rest:
125    case Shape.Misaligned{}:
126      Empty.absurd({Some{oh <> ot} == aligned_output(lh <> lt, rh <> rt, Shape.align.step(lh, lt, rh, rt, Shape.Misaligned{}, choice)) : Maybe<&2, List<&2, Nat>>}, some_none(List<&2, Nat>, ot, rest_seen))
127    case Shape.Aligns{tail, aligned}:
128      match choice:
129        case Shape.Clashes{}:
130          Empty.absurd({Some{oh <> ot} == None{} : Maybe<&2, List<&2, Nat>>}, some_none(Nat, oh, choice_seen))
131        case Shape.Picks{output, axis}:
132          %some_injective(Nat, oh, U32.to_nat(output), choice_seen) : {Some{oh <> ot} == Some{_ <> Shape.naturals(tail)} : Maybe<&2, List<&2, Nat>>}
133          %some_injective(List<&2, Nat>, ot, Shape.naturals(tail), rest_seen) : {Some{oh <> ot} == Some{oh <> _} : Maybe<&2, List<&2, Nat>>}
134          {==}