The refly Plugin

Table of Contents

• Dependencies
• Types
• Reify/Reflect
  • %refly.reify
  • %refly.reflect
• Inspect
  • %refly.gid
  • %refly.dbg
• Manipulate
  • %refly.refine
• Passes and Phases
  • Passes

See also

mim::plug::refly

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

Dependencies

import compile;

Types

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.gid

Retuns 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;

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;

Passes and Phases

Passes

axm %refly.remove_dbg_perm_pass: %compile.Pass;