Dependencies

.import compile;

Types

%mem.M

This type tracks all kind of side-effects.

.ax %mem.M: *;

%mem.Ptr

Pointer type with pointee type T and address space as. At the moment, the address space is not really used and a placeholder for future work.

.ax %mem.Ptr: [*, .Nat] -> *;
 
.lam %mem.Ptr0(T: *): * = %mem.Ptr (T, 0);

Operations w/ Side Effects

The following operations have side effects. For this reason, they consume a %mem.M and yield a new %mem.M.

%mem.load

Loads from a pointer of type %mem.Ptr (T, as) the pointed value of type T.

.ax %mem.load: Π.Tas::[T: *, .Nat][%mem.M, %mem.Ptr Tas] -> [%mem.M, T], normalize_load;

%mem.store

Stores a value of type T to the location pointed to by a pointer of type %mem.Ptr (T, as),

.ax %mem.store: Π.Tas::[T: *, .Nat][%mem.M, %mem.Ptr Tas, T] -> %mem.M, normalize_store;

%mem.remem

Creates a new dummy %mem.M-typed value in order to acknowledge the fact that some unspecified side-effect happened.

.ax %mem.remem: %mem.M -> %mem.M, normalize_remem;

%mem.alloc

Allocates memory of type T in address space as.

.ax %mem.alloc: Π Tas::[*, .Nat][%mem.M] -> [%mem.M, %mem.Ptr Tas];

%mem.slot

Reserves a memory slot for type T in address space as. id has to be provided a unique id.

.ax %mem.slot: Π Tas::[*, .Nat][%mem.M, id: .Nat] -> [%mem.M, %mem.Ptr Tas];

%mem.malloc

Allocates memory of type T in address space as. The difference to %mem.alloc is that the size is automatically inferred.

.ax %mem.malloc: Π Tas::[*, .Nat][%mem.M, .Nat] -> [%mem.M, %mem.Ptr Tas];

%mem.free

Frees memory of type T in address space as.

.ax %mem.free: Π.Tas::[*, .Nat][%mem.M, %mem.Ptr Tas] -> %mem.M;

%mem.mslot

Reserves a memory slot for type T in address space as. The reserved slot will be size bytes large. id has to be provided an unique id.

.ax %mem.mslot: Π Tas::[*, .Nat][%mem.M, size: .Nat, id: .Nat] -> [%mem.M, %mem.Ptr Tas];

Operations w/o Side Effects

%mem.lea

Load effective address. Performs address computation by offsetting the passed pointer with index i.

.ax %mem.lea: Π [n: .Nat, Ts: «n; *», as: .Nat][%mem.Ptr («j: n; Ts#j», as), i: .Idx n] -> %mem.Ptr (Ts#i, as), normalize_lea;

%mem.create/destroy

Create side effect out of thin or pretend that the side effect does not exists.

Warning: Use with caution since you completely remove the %mem.M dependency.

.let %mem.m = ⊤:%mem.M;
.lam %mem.ignore.(O: *)(_: %mem.M, o: O): O = o;
.lam %mem.rm(n: .Nat, Is: «n; *», O: *)
            (f: [%mem.M, «i: n; Is#i»] -> [%mem.M, O])
            (is: «i: n; Is#i»): O
                = %mem.ignore (f (%mem.m, is));

Passes and Phases

Misc

Reshape mode enum.

.ax %mem.reshape_mode: *;
.ax %mem.reshape_flat: %mem.reshape_mode;
.ax %mem.reshape_arg:  %mem.reshape_mode;

Passes

SSA pass expects eta expansion as argument

.ax %mem.ssa_pass: %compile.Pass -> %compile.Pass;

Copy propagation expects beta reduction and eta expansion as argument.

.ax %mem.copy_prop_pass:    [%compile.Pass, %compile.Pass, .Bool] -> %compile.Pass;
.ax %mem.remem_elim_pass:   %compile.Pass;
.ax %mem.alloc2malloc_pass: %compile.Pass;
.ax %mem.reshape_pass:      %mem.reshape_mode -> %compile.Pass;

Phases

.ax %mem.add_mem_phase: %compile.Phase;
 
.let mem_opt_pass_list = {
    .let beta_red = %compile.beta_red_pass;
    .let eta_red  = %compile.eta_red_pass;
    .let eta_exp  = %compile.eta_exp_pass eta_red;
    %compile.pass_list
        beta_red
        eta_red
        eta_exp
        (%mem.ssa_pass eta_exp)
        (%mem.copy_prop_pass (beta_red, eta_exp, .ff))
};
.let mem_opt_phase  = %compile.pass_phase mem_opt_pass_list;
.let mem_prep_phase = %compile.passes_to_phase (⊤:.Nat) (
        %mem.remem_elim_pass,
        %mem.alloc2malloc_pass
    );

Table of Contents