The tuple Plugin

Table of Contents

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

See also

mim::plug::tuple

Utilitly functions for tuples.

Dependencies

plugin core;

Operations

%tuple.cat

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

axm %tuple.cat: {n m: Nat}
                 → {Ts: «n; *», Us: «m; *»}
                 → [«i: n; Ts#i», «i: m; Us#i»]
                 → «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))))
                   » // «i: n + m; select(i < n , Ts#i, Us#(i - n))»
                 , normalize_cat;
 
lam %tuple.append   {n: Nat}
                    {Ts: «n; *», U: *}
                    (a: «i: n; Ts#i», b: U)
                  : «i: %core.nat.add (n, 1);
                        %core.select (%core.ncmp.l (%core.bitcast Nat i, n), Ts#(%core.bitcast (Idx n) i), U)
                    » // «i: n + 1; select(i < n , Ts#i, U)»
                  = %tuple.cat (a, b);
 
lam %tuple.prepend  {m: Nat}
                    {T: *, Us: «m; *»}
                    (a: T, b: «i: m; Us#i»)
                  : «i: %core.nat.add (1, m);
                        let nat_i = %core.bitcast Nat i;
                        %core.select (%core.ncmp.l (nat_i, 1), T, Us#(%core.bitcast (Idx m) (%core.nat.sub (nat_i, 1))))
                    » // «i: 1 + m; select(i < 1 , T, Us#(i - 1))»
                  = %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;