Dependencies

import compile;

Types

Code

The reified internal representation of a Mim expression of type T.

axm Code: * → *;

Reify / Reflect

reify

Yields the internal MimIR representation of a Mim expression as refly.Code.

axm reify: {T: *} → T → [Code T], normalize_reify;

reflect

Converts a refly.Code back to a Mim expression.

axm reflect: {T: *} → [Code T] → T, normalize_reflect;

Inspect

type

Returns the type of an expression.

axm type: {T: *} → T → *, normalize_type;

gid

Returns the internal mim::Def::gid of the argument.

axm gid: {T: *} → T → Nat, normalize_gid;

dbg

Debugs a given expression.

tmp: Prints debug information of a given expression at construction time and vanishes afterwards.
perm: Permanently debugs at every construction. Gets removed at codegen preparation in mim::plug::refly::RemoveDbgPerm.

anx let error   = 0;
anx let warn    = 1;
anx let info    = 2;
anx let verbose = 3;
anx let debug   = 4;
 
axm dbg.(tmp, perm): {T: *} → [Nat, T] → T, normalize_dbg;

Testing

equiv

Checks for structural / alpha-equivalence. Two bits select the check:

Alpha: check α-equivalence instead of structural identity
Equal: assert equivalence instead of inequivalence

Subtag	Alias	A	E	Meaning
ae	struc_ne	o	o	assert not structurally equivalent
aE	struc_eq	o	x	assert structurally equivalent
Ae	alpha_ne	x	o	assert not alpha-equivalent
AE	alpha_eq	x	x	assert alpha-equivalent

axm equiv.(ae = struc_ne, aE = struc_eq,
           Ae = alpha_ne, AE = alpha_eq):
    {T: *} → [T, T] → T, normalize_equiv;

check_bot

Checks whether the argument is ⊥.

axm check_bot: {T: *} → T → T, normalize_check_bot;

check

Checks the given condition and emits the error message if it is ff.

axm check: {T: *} → {n: Nat} → [Bool, T, «n; I8»] → T, normalize_check;

Phases

remove_dbg_repl

Removes the permanent refly.dbg markers for code generation.

axm remove_dbg_repl: compile.Phase;