def Arrays.of_list

bend-osdev-array@0.1.0.1 · array.bend:60

import Base

60# The perfect array of depth d whose slots are xs in order (cut to 2^d
61# slots, or padded with fill): an array built from a Data list, so that a
62# proof can name it as often as it likes (a specification, like leaves)
63def Arrays.of_list(-T: Data, +d: Nat, +xs: List<&2, T>, +fill: T) -> Array<T>:
64  match d:
65    case 0n:
66      ALeaf{Arrays.nth(T, xs, 0n, fill)}
67    case 1n+p:
68      +s = Arrays.slots(p)
69      ANode{Arrays.of_list(T, p, List.take(&2, T, xs, s), fill), Arrays.of_list(T, p, List.drop(&2, T, xs, s), fill)}