\print {
	/* Output results of read-back. */
	this.nf = M;
	++this.total;
} \atom_{M};

\read_{C}[a] {
	/* Unshare variable. */
	++this.total;
} \share[\copy(b, \read_{C}(a)), b];

\read_{C}[a] {
	/* Initiate application. */
	++this.total;
} \apply[\lambda(b, \read_{C}(a)), b];

\read_{C}[a] {
	/* Read back abstraction. */
	++this.total;
} \lambda[\atom_{this.mkid()}, \read_{this.abst(C)}(a)];

\lambda[\read_{this.appl(M)}(a), a] {
	/* Read back application. */
	++this.total;
} \atom_{M};

\read_{C}[\atom_{this.atom(C, M)}] {
	/* Read back an atom. */
	++this.total;
} \atom_{M};

\copy[\atom_{M}, \atom_{this.clone(M)}] {
	/* Copy an atom. */
	++this.total;
} \atom_{M};

\dup[\atom_{M}, \atom_{this.clone(M)}] {
	/* Duplicate an atom. */
	++this.total;
} \atom_{M};

\lambda[a, b] {
	/* Unshare variable. */
	++this.total;
} \share[\copy(c, \lambda(a, b)), c];

\lambda[a, b] {
	/* Initiate application. */
	++this.total;
} \apply[\lambda(c, \lambda(a, b)), c];

\lambda[a, b] {
	/* Apply a closed term. */
	++this.beta;
	++this.total;
} \lambda[a, b];

\copy[a, b] {
	/* Unshare variable. */
	++this.total;
} \share[\copy(c, \copy(a, b)), c];

\copy[a, b] {
	/* Initiate application. */
	++this.total;
} \apply[\lambda(c, \copy(a, b)), c];

\copy[\lambda(a, b), \lambda(c, d)] {
	/* Initiate copy of a closed term. */
	++this.total;
} \lambda[\dup(a, c), \dup(b, d)];

\dup[a, b] {
	/* Unshare variable. */
	++this.total;
} \share[\copy(c, \dup(a, b)), c];

\dup[a, b] {
	/* Duplicate sharing. */
	++this.total;
} \copy[\dup(\amb(c, \share(a, d), d), \amb(e, \share(b, f), f)), \dup(c, e)];

\dup[\apply(a, b), \apply(c, d)] {
	/* Duplicate application. */
	++this.total;
} \apply[\dup(a, c), \dup(b, d)];

\dup[\lambda(a, b), \lambda(c, d)] {
	/* Duplicate abstraction. */
	++this.total;
} \lambda[\dup(a, c), \dup(b, d)];

\dup[a, b] {
	/* Finish duplication. */
	++this.total;
} \dup[a, b];

\erase {
	/* Erase an atom. */
	++this.total;
} \atom_{M};

\erase {
	/* Erase sharing. */
	++this.total;
} \share[a, a];

\erase {
	/* Erase application. */
	++this.total;
} \apply[\erase, \erase];

\erase {
	/* Erase abstraction. */
	++this.total;
} \lambda[\erase, \erase];

\erase {
	/* Erase copy initiator. */
	++this.total;
} \copy[\erase, \erase];

\erase {
	/* Erase duplicator. */
	++this.total;
} \dup[\erase, \erase];

\erase {
	/* Finish erasing. */
	++this.total;
} \erase;

$$

\read_{this.mkhole()}(!print) = root;
root = \lambda(w1, w3);
w3 = \apply(w4, w5);
w4 = \apply(w6, w7);
w6 = \lambda(w2, w8);
w8 = w2;
w7 = \atom_{this.mkid("v1")};
w5 = w1;

$$

const gfv = [];
let id = 0;

function mkvar(fresh)
{
	if (fresh)
		++id;

	return "v" + id.toFixed(0);
}

function mkid(name)
{
	const fv = {};
	const obj = {
		node: "atom",
		name: name,
		fv: fv
	};

	if (name) {
		gfv[name] = true;
		return obj;
	}

	do {
		name = mkvar(true);
	} while (gfv[name]);

	obj.name = name;
	fv[name] = true;
	return obj;
}

function mkhole()
{
	const obj = {};

	obj.fv = {};
	obj.bv = {};
	obj.hole = obj;
	return obj;
}

function subst(hole, obj)
{
	const parent = hole.parent;
	const body = obj.body;
	const left = obj.left;
	const right = obj.right;

	if (parent)
		obj.parent = hole.parent;
	else
		delete obj.parent;

	Object.assign(hole, obj);

	if (body)
		body.parent = hole;
	if (left)
		left.parent = hole;
	if (right)
		right.parent = hole;
}

function eta(obj)
{
	let parent, left, right, name;

	if ("appl" != obj.node)
		return;

	parent = obj.parent;
	if (!parent)
		return;
	if ("abst" != parent.node)
		return;

	right = obj.right;
	if ("atom" != right.node)
		return;

	name = parent.var;
	if (name != right.name)
		return;

	left = obj.left;
	if (left.fv[name])
		return;

	subst(parent, left);

	eta(parent);
}

function atom(context, obj, name)
{
	const ofv = obj.fv;
	const cfv = context.fv;
	const bv = context.bv;
	const chole = context.hole;
	const ohole = obj.hole;

	if (name)
		bv[name] = true;

	for (const key in ofv)
		if (!(key in bv))
			cfv[key] = true;

	subst(chole, obj);

	if (ohole) {
		delete chole.hole;
		context.hole = ohole;
	} else {
		delete context.hole;
		eta(chole);
	}

	return context;
}

function abst(context)
{
	const hole = mkhole();
	const name = mkvar();
	const obj = {
		node: "abst",
		var: name,
		body: hole,
		fv: {},
		hole: hole
	};

	hole.parent = obj;
	return atom(context, obj, name);
}

function appl(left)
{
	const context = mkhole();
	const hole = mkhole();
	const obj = {
		node: "appl",
		left: left,
		right: hole,
		fv: Object.assign({}, left.fv),
		hole: hole
	};

	left.parent = obj;
	hole.parent = obj;
	return atom(context, obj);
}

function clone(obj, root, hole, parent)
{
	const copy = {};

	if (!obj)
		return;

	if (!root) {
		root = copy;
		hole = obj.hole;
	}

	copy.node = obj.node;
	copy.var = obj.var;
	copy.name = obj.name;
	copy.parent = parent;
	copy.body = clone(obj.body, root, hole, copy);
	copy.left = clone(obj.left, root, hole, copy);
	copy.right = clone(obj.right, root, hole, copy);

	copy.fv = Object.assign({}, obj.fv);
	copy.bv = Object.assign({}, obj.bv);

	if (obj === hole)
		root.hole = copy;

	return copy;
}

this.clone = clone;
this.mkid = mkid;
this.mkvar = mkvar;
this.mkhole = mkhole;
this.abst = abst;
this.appl = appl;
this.atom = atom;

this.beta = 0;
this.total = 0;