The refly Plugin

Table of Contents

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

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

Retuns type of an expression.

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

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

Testing

%refly.equiv

Checks for structurual / alpha-equivalence. We are using two disjoint relations:

• Alpha
• Equal

Subtag	Alias	A	E	Meaning
ae	f	o	o	assert strucutrual equivalent
aE	e	o	x	assert not structurual equivalent
Ae	l	x	o	assert alpha equivalent
AE	le	x	x	assert not 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

Checks the given condition and emits the error message, if false.

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;

Stages

Repls

axm %refly.remove_dbg_repl: %compile.Repl;