def certify

bendtorch-core@0.1.0.0 · src/storage/clone.bend:37

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model

37def certify(-T: Data, +d: Nat, array: Array<T>, valid: Model.Balanced(T, d, array)) -> Cloned<T, d, array>:
38  match d array:
39    case 0n ALeaf{+value}:
40      Cloned{ALeaf{value}, ALeaf{value}, {==}, {==}, {==}, Unit{}, Unit{}}
41    case 0n ANode{xs, ys}:
42      match valid:
43    case 1n+p ALeaf{value}:
44      match valid:
45    case 1n++p ANode{xs, ys}:
46      (ex, ey) = valid
47      join(T, p, xs, ys, certify(T, p, xs, ex), certify(T, p, ys, ey))