Implementation of closed reduction with read-back mechanism using Interaction Nets Compiler

lambda.in

${
#include <stdio.h>
#include <stdlib.h>
#include <string.h>

char *var(int fresh);
char *append(char *format, char *buf, char *str);

#define ABST(BUF, STR) append("%s%s: ", (BUF), (STR))
#define APPL(BUF, STR) append("%s%s ", (BUF), (STR))
#define ATOM(BUF, STR) append("%s(%s)", (BUF), (STR))
}$

\print {
	/* Output results of read-back. */
	puts(RVAL);
	free(RVAL);
} \atom;

\read[a] {
	/* Unshare variable. */
} \share[\copy(b, \read_{LVAL}(a)), b];

\read[a] {
	/* Initiate application. */
} \apply[\lambda(b, \read_{LVAL}(a)), b];

\read[a] {
	/* Read back abstraction. */
} \lambda[\atom_{var(1)}, \read_{ABST(LVAL, var(0))}(a)];

\lambda[\read_{APPL(strdup(""), RVAL)}(a), a] {
	/* Read back application. */
} \atom;

\read[\atom_{ATOM(LVAL, RVAL)}] {
	/* Read back an atom. */
} \atom;

\copy[\atom_{RVAL}, \atom_{strdup(RVAL)}] {
	/* Copy an atom. */
} \atom;

\dup[\atom_{RVAL}, \atom_{strdup(RVAL)}] {
	/* Duplicate an atom. */
} \atom;

\erase {
	/* Erase an atom. */
	free(RVAL);
} \atom;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\erase {
	/* Finish erasing. */
} \erase;

$$

{"Application"} = \apply(function, argument);
first1 = \amb(second1, \share(shared1, back1), back1);
first2 = \amb(second2, \share(shared2, back2), back2);
first3 = \amb(second3, \share(shared3, back3), back3);

{"Abstraction"} = \lambda(variable, body);

term = \read_{strdup("")}(\print);
term = {"Encoding"};

$$

char *var(int fresh)
{
	static int id;

	char buf[BUFSIZ];

	if (fresh)
		++id;

	sprintf(buf, "v%d", id);
	return strdup(buf);
}

char *append(char *format, char *buf, char *str)
{
	size_t size = strlen(format) + strlen(str);
	char *result = malloc(strlen(buf) + size);

	sprintf(result, format, buf, str);

	free(buf);
	free(str);
	return result;
}