def ASet.reads_f

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

import Base

2226# the write goes into the high half ys
2227def ASet.reads_f(-T: Data, -xs: Array<T>, -ys: Array<T>, +n: U32, +j: U32, +v: T, +k: U32, +w: Bool, +g: {(Pair.fst(Array<T>, T, ASet.RL(T, xs, n, k)), Pair.snd(Array<T>, T, ASet.RL(T, xs, n, k))) == ASet.RL(T, xs, n, k) : Array<T> & T}, r: ASet.Reads(T, ys, U32.shr(n), U32.sub(j, U32.shr(n)), v, U32.is_lt(U32.sub(j, U32.shr(n)), U32.shr(U32.shr(n))), U32.sub(k, U32.shr(n)), U32.is_lt(U32.sub(k, U32.shr(n)), U32.shr(U32.shr(n))))) -> ASet.Reads(T, ANode{xs, ys}, n, j, v, False{}, k, w):
2228  match w:
2229    case True{}:
2230      match r:
2231        case Tuple{+d, r1}:
2232          match r1:
2233            case Tuple{+e1, r2}:
2234              match r2:
2235                case Tuple{+e2, r3}:
2236                  match r3:
2237                    case Tuple{e3, u}:
2238                      ({(%d : {(Array.set.fin(T, Array.swap.hi(T, xs, _)), Pair.snd(Array<T>, T, Array.swap.hi(T, xs, _))) == Array.swap.hi(T, xs, _) : Array<T> & T}; {==}) : {(ASet.NA(T, ANode{xs, ys}, n, j, v, False{}), Pair.snd(Array<T>, T, ASet.G(T, ANode{xs, ys}, n, j, v, False{}))) == ASet.G(T, ANode{xs, ys}, n, j, v, False{}) : Array<T> & T}},
2239                        {(%g : {(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}},
2240                        {(%d : {(Pair.fst(Array<T>, T, Array.get.go(T, Array.set.fin(T, Array.swap.hi(T, xs, _)), n, k, True{})), Pair.snd(Array<T>, T, Array.get.go(T, Array.set.fin(T, Array.swap.hi(T, xs, _)), n, k, True{}))) == Array.get.go(T, Array.set.fin(T, Array.swap.hi(T, xs, _)), n, k, True{}) : Array<T> & T}; %g : {(Pair.fst(Array<T>, T, Array.swap.lo(T, ASet.WH(T, ys, n, j, v), _)), Pair.snd(Array<T>, T, Array.swap.lo(T, ASet.WH(T, ys, n, j, v), _))) == Array.swap.lo(T, ASet.WH(T, ys, n, j, v), _) : Array<T> & T}; {==}) : {(Pair.fst(Array<T>, T, Array.get.go(T, ASet.NA(T, ANode{xs, ys}, n, j, v, False{}), n, k, True{})), Pair.snd(Array<T>, T, Array.get.go(T, ASet.NA(T, ANode{xs, ys}, n, j, v, False{}), n, k, True{}))) == Array.get.go(T, ASet.NA(T, ANode{xs, ys}, n, j, v, False{}), n, k, True{}) : Array<T> & T}},
2241                        (h => (%d : {Pair.snd(Array<T>, T, Array.get.go(T, Array.set.fin(T, Array.swap.hi(T, xs, _)), n, k, True{})) == Pair.snd(Array<T>, T, Array.get.go(T, ANode{xs, ys}, n, k, True{})) : T}; %g : {Pair.snd(Array<T>, T, Array.swap.lo(T, ASet.WH(T, ys, n, j, v), _)) == Pair.snd(Array<T>, T, Array.swap.lo(T, ys, _)) : T}; {==})),
2242                        Unit{})
2243    case False{}:
2244      match r:
2245        case Tuple{+d, r1}:
2246          match r1:
2247            case Tuple{+e1, r2}:
2248              match r2:
2249                case Tuple{+e2, r3}:
2250                  match r3:
2251                    case Tuple{e3, u}:
2252                      ({(%d : {(Array.set.fin(T, Array.swap.hi(T, xs, _)), Pair.snd(Array<T>, T, Array.swap.hi(T, xs, _))) == Array.swap.hi(T, xs, _) : Array<T> & T}; {==}) : {(ASet.NA(T, ANode{xs, ys}, n, j, v, False{}), Pair.snd(Array<T>, T, ASet.G(T, ANode{xs, ys}, n, j, v, False{}))) == ASet.G(T, ANode{xs, ys}, n, j, v, False{}) : Array<T> & T}},
2253                        {(%e1 : {(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}},
2254                        {(%d : {(Pair.fst(Array<T>, T, Array.get.go(T, Array.set.fin(T, Array.swap.hi(T, xs, _)), n, k, False{})), Pair.snd(Array<T>, T, Array.get.go(T, Array.set.fin(T, Array.swap.hi(T, xs, _)), n, k, False{}))) == Array.get.go(T, Array.set.fin(T, Array.swap.hi(T, xs, _)), n, k, False{}) : Array<T> & T}; %e2 : {(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, ASet.NA(T, ANode{xs, ys}, n, j, v, False{}), n, k, False{})), Pair.snd(Array<T>, T, Array.get.go(T, ASet.NA(T, ANode{xs, ys}, n, j, v, False{}), n, k, False{}))) == Array.get.go(T, ASet.NA(T, ANode{xs, ys}, n, j, v, False{}), n, k, False{}) : Array<T> & T}},
2255                        (h => (%d : {Pair.snd(Array<T>, T, Array.get.go(T, Array.set.fin(T, Array.swap.hi(T, xs, _)), n, k, False{})) == Pair.snd(Array<T>, T, Array.get.go(T, ANode{xs, ys}, n, k, False{})) : T}; %e2 : {Pair.snd(Array<T>, T, Array.swap.hi(T, xs, _)) == Pair.snd(Array<T>, T, Array.swap.hi(T, xs, ASet.RH(T, ys, n, k))) : T}; %e1 : {Pair.snd(Array<T>, T, ASet.RH(T, ASet.WH(T, ys, n, j, v), n, k)) == Pair.snd(Array<T>, T, Array.swap.hi(T, xs, _)) : T}; e3(h))),
2256                        Unit{})