Dependencies

import mem;
import core;
plugin refly;

Operations

%affine.For

This operation ranges from (including) begin to (excluding) end using step as stride. In addition, this loop manages n loop accumulators whose initial values init must be given. On each iteration, the given body is invoked and receives

the current iteration index,
the current values of the loop accumulators acc, and
a yield continuation to continue with the next iteration, passing the new accumulator values.

After termination of the loop, exit is invoked with the final accumulator values.

axm %affine.For: {m n: Nat, Ts: «n; *»}
               → [Cn [iter: Idx m, acc: «i: n; Ts#i», yield: Cn «i: n; Ts#i»]] // body
               → [Cn «i: n; Ts#i»]                                             // exit
               → Cn [begin _end step: Idx m, init: «i: n; Ts#i»];

Affine Index Operations

%affine.index

The affine index type is an opaque type that can only be manipulated through the following operations.

axm %affine.index: *;

%affine.constant

Constructs an affine index from a constant natural number.

axm %affine.constant: Nat → %affine.index;

%affine.op(add,sub)

Performs addition and subtraction on affine indices.

axm %affine.op(add,sub): [%affine.index, %affine.index] → %affine.index;

%affine.op(neg)

Negates an affine index.

axm %affine.op(neg): %affine.index → %affine.index;

%affine.semiop(mul,ceildiv,floordiv,mod)

Performs semi-linear operations on affine indices. The second argument is a natural number that must be constant with regard to the indices.

axm %affine.semiop(mul,ceildiv,floordiv,mod): [%affine.index, Nat] → %affine.index;

%affine.op.mul

Performs multiplication of an affine index with a constant natural number. The second argument must be a closed constant - a stronger requirement than %affine.semiop imposes - which is enforced via %refly.check.

lam %affine.op.mul (d : %affine.index, c : Nat): %affine.index =

%affine.semiop.mul(d, %refly.check (%core.pe.is_closed(c), c, "The second argument of %affine.op.mul must be a constant."));

%affine.map

Maps a function over a list of affine indices. Any captured variables of the function must be closed over the entire list of indices, i.e. they must not depend on the iteration index. The moduli are per-element: each input index i carries its own modulus sin#i and each output index j its own sout#j.

axm %affine.map: {m n: Nat}
               → {sin: «n; Nat», sout: «m; Nat»}
               → ([«n; %affine.index»] → «m; %affine.index»)
               → «i: n; Idx (sin#i)»
               → (%mem.M 0)
               → [(%mem.M 0), «i: m; Idx (sout#i)»];

%affine.id

The identity map on affine indices.

lam %affine.id {r: Nat} (o: «r; %affine.index»): «r; %affine.index» = o;

%affine.linearize

Row-major flattening of a multi-index: linearize(idxs, s) = Σ_k idxs#k · (∏_{j>k} s#j). s is the (row-major) shape; only its rank n need be a literal.

axm %affine.linearize: {n: Nat} → [idxs: «n; %affine.index», s: «n; Nat»] → %affine.index;

%affine.delinearize

Row-major unflattening: delinearize(lin, s)#d = (lin floordiv (∏_{j>d} s#j)) mod s#d. The inverse of affine.linearize; only the rank m of s need be a literal.

axm %affine.delinearize: {m: Nat} → [lin: %affine.index, s: «m; Nat»] → «m; %affine.index»;

Phases

%affine.lower_for

Lowers the %%affine.For operation to recursive function calls.

axm %affine.lower_for: %compile.Phase;

%affine.lower_index

Lowers the affine index algebra (%%affine.index, %%affine.constant, %%affine.op, %%affine.semiop, %%affine.map) to %core arithmetic.

axm %affine.lower_index: %compile.Phase;

Table of Contents