Skip to content

Instantly share code, notes, and snippets.

@codedot
Last active Aug 29, 2015
Embed
What would you like to do?
Implementation of closed reduction with read-back mechanism using Interaction Nets Compiler
${
#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;
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment