Dependencies

plugin core;
plugin option;
plugin refly;

Iterators

fold

Fold aka Reduction of the vector with f:

vec.fold.l f (init, (e1, ..., en)) is f (... (f (f (init, e1), e2)) ..., en).
vec.fold.r f ((e1, ..., en), init) is f (e1, f (e2, ... (f (en, init) ...))).

vec.fold.l	vec.fold.r

pub mod fold {
    axm l: {A E: *} → {n: Nat} → [f: [A, E] → A] → [A, «n; E»] → A, normalize_fold;
    axm r: {A E: *} → {n: Nat} → [f: [E, A] → A] → [«n; E», A] → A, normalize_fold;
}

zip

Combines multiple vectors element-wise using the provided function. Given ni vectors of length n, and a function f that takes one element from each vector, vec.zip produces a new vector of length n where each element is the result of applying f.

axm zip: {ni n: Nat} → {Is: «ni; *», R: *} → [f: «i: ni; Is#i» → R] → [«i: ni; «n; Is#i»»] → «n; R», normalize_zip;

Scanning

scan

Does the given predicate hold for all elements/at least one element?

axm scan.(for_all, exists): {E: *} → {n: Nat} → [p: E → Bool] → «n; E» → Bool, normalize_scan;

first / last

Yields the index of the first/last occurrence of the given element, or option.none if it does not occur.

lam f_first    {E: *} {n: Nat} (eq: [E, E] → Bool) (x: E) ((b: Bool, i: Idx n), y: E): [Bool, Idx n] = (((ff, core.wrap.add 0 (i, core.idx 0 n 1)), (tt, i))#(eq (x, y)), (b, i))#b;
lam f_last     {E: *} {n: Nat} (eq: [E, E] → Bool) (x: E) (y: E, (b: Bool, i: Idx n)): [Bool, Idx n] = f_first eq x ((b, i), y);
anx lam first {E: *} {n: Nat} (eq: [E, E] → Bool) (v: «n; E», x: E): option.Opt (Idx n) = option.some_if (fold.l (f_first eq x) ((ff, core.idx 0 n 0), v));
anx lam last  {E: *} {n: Nat} (eq: [E, E] → Bool) (v: «n; E», x: E): option.Opt (Idx n) = option.some_if (fold.r (f_last  eq x) (v, (ff, core.idx 0 n 0)));

len

Yields the length of the vector.

anx lam len {n: Nat} {T: *} (_: «n; T»): Nat = n;

is_unique

Checks whether all elements in the given vector are distinct from each other (using structural equivalence).

axm is_unique: {T: *} → {n: Nat} → «n; T» → Bool, normalize_is_unique;

Modifiers

cat

Concatenates an n-vector and an m-vector to an n + m-vector.

axm cat: {n m: Nat}
       → {T: *}
       → [«n; T», «m; T»]
       → «core.nat.add (n, m); T», normalize_cat;

diff

Removes the elements at the given indices from the vector; the indices must be distinct (checked via vec.is_unique).

axm diff: {T: *}
        → {n m: Nat}
        → [«n; T», is: «m; Idx n»]
        → «refly.check (is_unique is, core.nat.sub (n, m), "given indices are not distinct"); T», normalize_diff;