The tuple Plugin

See also

mim::plug::tuple

Utility functions for tuples.

Dependencies

plugin core;

Operations

typecat

Computes the type of a tuple.cat with an n- and an m-tuple.

anx lam typecat {n m: Nat} (Ts: «n; *») (Us: «m; *») : * = // «i: n + m; select(i < n , Ts#i, Us#(i - n))»
    «i: core.nat.add (n, m);
        let nat_i = core.bitcast Nat i;
        core.Select (
            core.ncmp.l (nat_i, n),
            Ts#(core.bitcast (Idx n) i),
            Us#(core.bitcast (Idx m) (core.nat.sub (nat_i, n))))»;

cat

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

axm cat: {n m: Nat}
          → {Ts: «n; *», Us: «m; *»}
          → [«i: n; Ts#i», «i: m; Us#i»]
          → typecat Ts Us
          , normalize_cat;

append / prepend

Appends / prepends a single element to a tuple.

anx lam append   {n: Nat}
                 {Ts: «n; *», U: *}
                 (a: «i: n; Ts#i», b: U)
               : typecat Ts U
               = cat (a, b);
 
anx lam prepend  {m: Nat}
                 {T: *, Us: «m; *»}
                 (a: T, b: «i: m; Us#i»)
               : typecat T Us
               = cat (a, b);

head / tail

The first element of a tuple / all elements but the first.

anx lam head {n: Nat}
    {Ts: «n; *»}
    (values: «i: n; Ts#i»)
  : [Ts#(core.idx core.mode.US n 0)]
  = values#(core.idx core.mode.US n 0);
 
anx lam tail {n: Nat}
    {Ts: «n; *»}
    (values: «i: n; Ts#i»)
  : «i: core.nat.sub (n, 1); Ts#(core.bitcast (Idx n) (core.nat.add (core.bitcast Nat i, 1)))»
  = ‹i: core.nat.sub (n, 1); values#(core.bitcast (Idx n) (core.nat.add (core.bitcast Nat i, 1)))›;

contains

Does the tuple contain the given element?

axm contains: {n: Nat} → {Ts: «n; *», U: *} → [«i: n; Ts#i», U] → Bool, normalize_contains;

zip

Zips several tensors. The signature will likely change in the future:

• r: rank of the tensors to zip
• s: shape of the tensors to zip
• n_i: number of inputs
• n_o: number of outputs
• Is: tuple with n_i many elements that describe the element types of the inputs
• Os: tuple with n_o many elements that describe the element types of the outputs
• f: zipping function that expects an n_i-tuple whose elements correspond to Is and yields an n_o-tuple whose element types correspond to Os
• is: the actual input tensors

axm zip: [r: Nat, s: «r; Nat»]
       → [n_i: Nat, Is: «n_i; *», n_o: Nat, Os: «n_o; *», f: «i: n_i; Is#i» → «o: n_o; Os#o»]
       → «i: n_i; «s; Is#i»»
       → «o: n_o; «s; Os#o»», normalize_zip;