The tuple Plugin

Table of Contents

• Dependencies
• Operations
  • %tuple.typecat
  • %tuple.cat
  • %tuple.contains
  • %tuple.zip

See also

mim::plug::tuple

Utilitly functions for tuples.

Dependencies

plugin core;

Operations

%tuple.typecat

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

lam %tuple.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))))»;

%tuple.cat

Concatenation of an n-tuple and an m-tuple to an n + m-tuple yielding

axm %tuple.cat: {n m: Nat}
                 → {Ts: «n; *», Us: «m; *»}
                 → [«i: n; Ts#i», «i: m; Us#i»]
                 → %tuple.typecat Ts Us
                 , normalize_cat;
 
lam %tuple.append   {n: Nat}
                    {Ts: «n; *», U: *}
                    (a: «i: n; Ts#i», b: U)
                  : %tuple.typecat Ts U
                  = %tuple.cat (a, b);
 
lam %tuple.prepend  {m: Nat}
                    {T: *, Us: «m; *»}
                    (a: T, b: «i: m; Us#i»)
                  : %tuple.typecat T Us
                  = %tuple.cat (a, b);

%tuple.contains

Does the tuple conain the given element?

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

%tuple.zip

Zips several tensors.

What is more, 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 if inputs
• n_o: number if 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 %tuple.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;