def AP.get_leaves

bend-osdev-array@0.1.0.1 · PROOF.bend:1070

import Base
import bend-osdev-array@0.1.0.1/array.bend as A

1070def AP.get_leaves(-T: Data, +d: Nat, +t: AP.Tree<T>, +i: U32, b: Bool, +eb: {U32.is_lt(i, U32.shr(U32.shln(1, d))) == b : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hp: {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), A.Arrays.slots(d)) == True{} : Bool}) -> {List.get(&2, T, A.Arrays.leaves(T, AP.build(T, t)), U32.to_nat(i)) == Some{AP.get_v(T, t, U32.shln(1, d), i, b)} : Maybe<&2, T>}:
1071  match d t b:
1072    case 0n APLeaf{+x} _:
1073      %Equal.sym(Nat, U32.to_nat(i), 0n, AP.lt_one(U32.to_nat(i), hi)) : {List.get(&2, T, Con{x, Nil{}}, _) == Some{x} : Maybe<&2, T>}
1074      {==}
1075    case 0n APNode{xs, ys} _:
1076      Empty.absurd({List.get(&2, T, A.Arrays.leaves(T, AP.build(T, APNode{xs, ys})), U32.to_nat(i)) == Some{AP.get_v(T, APNode{xs, ys}, U32.shln(1, 0n), i, b)} : Maybe<&2, T>}, AP.ft(hp))
1077    case 1n+p APLeaf{x} _:
1078      Empty.absurd({List.get(&2, T, A.Arrays.leaves(T, AP.build(T, APLeaf{x})), U32.to_nat(i)) == Some{AP.get_v(T, APLeaf{x}, U32.shln(1, 1n+p), i, b)} : Maybe<&2, T>}, AP.ft(hp))
1079    case 1n+ +p APNode{xs, ys} True{}:
1080      +hd1 = AP.lt_succ_l(p, 32n, hd)
1081      +s = A.Arrays.slots(p)
1082      +sh = U32.shln(1, p)
1083      +lx = A.Arrays.leaves(T, AP.build(T, xs))
1084      +ly = A.Arrays.leaves(T, AP.build(T, ys))
1085      +v = U32.to_nat(i)
1086      +hpx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1087      +hi1 = AP.lt_true(i, p, hd1, AP.eb_fix(i, p, True{}, hd, eb))
1088      +hl = AP.lt_rw_r(v, List.length(&2, T, lx), s, AP.len_perf(T, p, xs, hpx), hi1)
1089      %Equal.sym(U32, U32.shr(U32.shln(1, 1n+p)), sh, AP.shr_shln(p, hd)) : {List.get(&2, T, List.append(&2, T, lx, ly), v) == Some{AP.get_v(T, xs, _, i, U32.is_lt(i, U32.shr(_)))} : Maybe<&2, T>}
1090      Equal.trans(Maybe<&2, T>, List.get(&2, T, List.append(&2, T, lx, ly), v), List.get(&2, T, lx, v), Some{AP.get_v(T, xs, sh, i, U32.is_lt(i, U32.shr(sh)))}, AP.get_app_l(T, lx, ly, v, hl), AP.get_leaves(T, p, xs, i, U32.is_lt(i, U32.shr(sh)), {==}, hd1, hpx, hi1))
1091    case 1n+ +p APNode{xs, ys} False{}:
1092      +hd1 = AP.lt_succ_l(p, 32n, hd)
1093      +s = A.Arrays.slots(p)
1094      +sh = U32.shln(1, p)
1095      +lx = A.Arrays.leaves(T, AP.build(T, xs))
1096      +ly = A.Arrays.leaves(T, AP.build(T, ys))
1097      +j = U32.sub(i, sh)
1098      +w = U32.to_nat(j)
1099      +hpx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1100      +hpy = AP.and_r(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1101      +hs = AP.split(i, p, hd1, AP.eb_fix(i, p, False{}, hd, eb))
1102      +hj = AP.lt_split2(w, s, AP.lt_rw_l(Nat.add(s, w), U32.to_nat(i), Nat.double(s), hs, hi))
1103      %Equal.sym(U32, U32.shr(U32.shln(1, 1n+p)), sh, AP.shr_shln(p, hd)) : {List.get(&2, T, List.append(&2, T, lx, ly), U32.to_nat(i)) == Some{AP.get_v(T, ys, _, U32.sub(i, _), U32.is_lt(U32.sub(i, _), U32.shr(_)))} : Maybe<&2, T>}
1104      %hs : {List.get(&2, T, List.append(&2, T, lx, ly), _) == Some{AP.get_v(T, ys, sh, j, U32.is_lt(j, U32.shr(sh)))} : Maybe<&2, T>}
1105      %AP.len_perf(T, p, xs, hpx) : {List.get(&2, T, List.append(&2, T, lx, ly), Nat.add(_, w)) == Some{AP.get_v(T, ys, sh, j, U32.is_lt(j, U32.shr(sh)))} : Maybe<&2, T>}
1106      Equal.trans(Maybe<&2, T>, List.get(&2, T, List.append(&2, T, lx, ly), Nat.add(List.length(&2, T, lx), w)), List.get(&2, T, ly, w), Some{AP.get_v(T, ys, sh, j, U32.is_lt(j, U32.shr(sh)))}, AP.get_app_r(T, lx, ly, w), AP.get_leaves(T, p, ys, j, U32.is_lt(j, U32.shr(sh)), {==}, hd1, hpy, hj))