def ASet.side_node

bend-ml-tensor-array@0.1.19.0 · main.bend:2138

import Base

2138def ASet.side_node(-T: Data, -xs: Array<T>, -ys: Array<T>, +n: U32, +k: U32, +w: Bool, sx: ASet.Side(T, xs, U32.shr(n), k, U32.is_lt(k, U32.shr(U32.shr(n)))), sy: ASet.Side(T, ys, U32.shr(n), U32.sub(k, U32.shr(n)), U32.is_lt(U32.sub(k, U32.shr(n)), U32.shr(U32.shr(n))))) -> ASet.Side(T, ANode{xs, ys}, n, k, w):
2139  match w:
2140    case True{}:
2141      match sx:
2142        case Tuple{+s1, r1}:
2143          match r1:
2144            case Tuple{+g1, u1}:
2145              match sy:
2146                case Tuple{+s2, r2}:
2147                  match r2:
2148                    case Tuple{+g2, u2}:
2149                      ({(%s1 : {(ANode{xs, ys}, Pair.snd(Array<T>, U32, Array.size.node(T, ys, _))) == Array.size.node(T, ys, _) : Array<T> & U32}; {==}) : {(ANode{xs, ys}, ASet.sz(T, ANode{xs, ys})) == Array.size(T, ANode{xs, ys}) : Array<T> & U32}}, {(%g1 : {(Pair.fst(Array<T>, T, Array.swap.lo(T, ys, _)), Pair.snd(Array<T>, T, Array.swap.lo(T, ys, _))) == Array.swap.lo(T, ys, _) : Array<T> & T}; {==}) : {(Pair.fst(Array<T>, T, Array.get.go(T, ANode{xs, ys}, n, k, True{})), Pair.snd(Array<T>, T, Array.get.go(T, ANode{xs, ys}, n, k, True{}))) == Array.get.go(T, ANode{xs, ys}, n, k, True{}) : Array<T> & T}}, Unit{})
2150    case False{}:
2151      match sx:
2152        case Tuple{+s1, r1}:
2153          match r1:
2154            case Tuple{+g1, u1}:
2155              match sy:
2156                case Tuple{+s2, r2}:
2157                  match r2:
2158                    case Tuple{+g2, u2}:
2159                      ({(%s1 : {(ANode{xs, ys}, Pair.snd(Array<T>, U32, Array.size.node(T, ys, _))) == Array.size.node(T, ys, _) : Array<T> & U32}; {==}) : {(ANode{xs, ys}, ASet.sz(T, ANode{xs, ys})) == Array.size(T, ANode{xs, ys}) : Array<T> & U32}}, {(%g2 : {(Pair.fst(Array<T>, T, Array.swap.hi(T, xs, _)), Pair.snd(Array<T>, T, Array.swap.hi(T, xs, _))) == Array.swap.hi(T, xs, _) : Array<T> & T}; {==}) : {(Pair.fst(Array<T>, T, Array.get.go(T, ANode{xs, ys}, n, k, False{})), Pair.snd(Array<T>, T, Array.get.go(T, ANode{xs, ys}, n, k, False{}))) == Array.get.go(T, ANode{xs, ys}, n, k, False{}) : Array<T> & T}}, Unit{})