The refly Plugin

Table of Contents

• Dependencies
• Types
  • %refly.Code
• Reify / Reflect
  • %refly.reify
  • %refly.reflect
• Inspect
  • %refly.type
  • %refly.gid
  • %refly.dbg
• Testing
  • %refly.equiv
  • %refly.check_bot
  • %refly.check
• Manipulate
  • %refly.refine
• Phases

See also

mim::plug::refly

The refly plugin allows you to reify and reflect MimIR's own representation.

Dependencies

import compile;

Types

%refly.Code

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

axm %refly.Code: * → *;

Reify / Reflect

%refly.reify

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

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

%refly.reflect

Converts a %refly.Code back to a Mim expression.

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

Inspect

%refly.type

Returns the type of an expression.

axm %refly.type: {T: *} → T → *, normalize_type;

%refly.gid

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

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

%refly.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.

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

Testing

%refly.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 %refly.equiv(ae = struc_ne, aE = struc_eq,
                 Ae = alpha_ne, AE = alpha_eq):
    {T: *} → [T, T] → T, normalize_equiv;

%refly.check_bot

Checks whether the argument is ⊥.

axm %refly.check_bot: {T: *} → T → T, normalize_check_bot;

%refly.check

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

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

Manipulate

%refly.refine

Sets the ith operand of the reified code e to x.

axm %refly.refine: {E X: *} → [e: %refly.Code E, i: Nat, x: %refly.Code X] → %refly.Code E, normalize_refine;

Phases

Removes the permanent %refly.dbg markers for code generation.

axm %refly.remove_dbg_repl: %compile.Phase;