def join

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

import Base

19def join(-T: Data, -d: Nat, -xs: Array<T>, -ys: Array<T>,
20  left: Cloned<T, d, xs>, right: Cloned<T, d, ys>) -> Cloned<T, 1n+d, ANode{xs, ys}>:
21  match left:
22    case Cloned{xa, xb, exact_x, same_xa, same_xb, valid_xa, valid_xb}:
23      match right:
24        case Cloned{ya, yb, exact_y, same_ya, same_yb, valid_ya, valid_yb}:
25          Cloned{ANode{xa, ya}, ANode{xb, yb},
26            Equal.trans(Array<T> & Array<T>, (ANode{xa, ya}, ANode{xb, yb}),
27              Array.clone.node(T, Array.clone(T, xs), (ya, yb)),
28              Array.clone.node(T, Array.clone(T, xs), Array.clone(T, ys)),
29              Equal.cong(Array<T> & Array<T>, Array<T> & Array<T>,
30                r => Array.clone.node(T, r, (ya, yb)), (xa, xb), Array.clone(T, xs), exact_x),
31              Equal.cong(Array<T> & Array<T>, Array<T> & Array<T>,
32                r => Array.clone.node(T, Array.clone(T, xs), r), (ya, yb), Array.clone(T, ys), exact_y)),
33            node_equal(T, xa, ya, xs, ys, same_xa, same_ya),
34            node_equal(T, xb, yb, xs, ys, same_xb, same_yb),
35            (valid_xa, valid_ya), (valid_xb, valid_yb)}