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 by refly.remove_dbg_repl.

The first argument of dbg is a log level; these lets name them.

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

struc

Asserts structural identity (e) or non-identity (ne) of both arguments.

axm struc.(ne, e): {T: *} → [T, T] → T, normalize_struc;

alpha

Asserts α-equivalence (e) or α-inequivalence (ne) of both arguments.

axm alpha.(ne, e): {T: *} → [T, T] → T, normalize_alpha;

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;