The vec Plugin

Table of Contents

• Dependencies
• Iterators
  • %vec.fold
• Scanning
  • %vec.scan
  • %vec.first / %vec.last
  • %vec.len
  • %vec.is_unique
• Modifiers
  • %vec.diff

See also

mim::plug::vec

Utilitly functions for arrays to behave them like vectors in other languages.

Dependencies

plugin core;
plugin refly;

Iterators

%vec.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

axm %vec.fold(l): {A E: *} → {n: Nat} → [f: [A, E] → A] → [A, «n; E»] → A, normalize_fold;
axm %vec.fold(r): {A E: *} → {n: Nat} → [f: [E, A] → A] → [«n; E», A] → A, normalize_fold;

Scanning

%vec.scan

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

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

%vec.first / %vec.last

Is the given element in the vector, and what is the index of its first/last occurence?

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 n 0 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);
lam %vec.first {E: *} {n: Nat} (eq: [E, E] → Bool) (v: «n; E», x: E):                  [Bool, Idx n] = %vec.fold.l (f_first eq x) ((ff, %core.idx n 0 0), v);
lam %vec.last  {E: *} {n: Nat} (eq: [E, E] → Bool) (v: «n; E», x: E):                  [Bool, Idx n] = %vec.fold.r (f_last eq x) (v, (ff, %core.idx n 0 0));

%vec.len

Get length of vector.

lam %vec.len {n: Nat} {T: *} [«n; T»]: Nat = n;

%vec.is_unique

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

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

Modifiers

%vec.diff

Removes elements from vector.

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