1 files changed, 100 insertions, 0 deletions
diff --git a/src/impl/closed.c b/src/impl/closed.c
new file mode 100644
index 0000000..5b607d9
--- /dev/null
+++ b/src/impl/closed.c
@@ -0,0 +1,100 @@
+// Copyright (c) 2024, Marvin Borner <dev@marvinborner.de>
+// SPDX-License-Identifier: MIT
+
+// only works for closed terms!
+
+// technique proposed by Mateusz Naściszewski (afaik)
+// implemented by John Tromp in Haskell
+
+#include <log.h>
+#include <impl.h>
+#include <stdint.h>
+
+static void encode_index(size_t n, size_t i, FILE *fp)
+{
+	if (n == 0)
+		fatal("invalid index (must be closed)\n");
+
+	if (i == 0) {
+		fprintf(fp, "%s", n == 1 ? "1" : "10");
+	} else {
+		fprintf(fp, "1");
+		encode_index(n - 1, i - 1, fp);
+	}
+}
+
+static void encode_level(size_t n, Term *term, FILE *fp)
+{
+	switch (term->type) {
+	case ABS:
+		fprintf(fp, "%s", n == 0 ? "0" : "00");
+		encode_level(n + 1, term->u.abs.body, fp);
+		break;
+	case APP:
+		fprintf(fp, "%s", n == 0 ? "1" : "01");
+		encode_level(n, term->u.app.lhs, fp);
+		encode_level(n, term->u.app.rhs, fp);
+		break;
+	case IDX:
+		encode_index(n, term->u.index, fp);
+		break;
+	default:
+		fatal("invalid type %d\n", term->type);
+	}
+}
+
+static void encode(Term *term, FILE *fp)
+{
+	encode_level(0, term, fp);
+}
+
+static Term *decode_level(size_t n, FILE *fp)
+{
+	Term *res = 0;
+
+	char a = getc(fp);
+
+	if (a == '0' && n == 0) {
+		res = term_new(ABS);
+		res->u.abs.body = decode_level(n + 1, fp);
+	} else if (a == '0') {
+		char b = getc(fp);
+
+		if (b == '0') {
+			res = term_new(ABS);
+			res->u.abs.body = decode_level(n + 1, fp);
+		} else if (b == '1') {
+			res = term_new(APP);
+			res->u.app.lhs = decode_level(n, fp);
+			res->u.app.rhs = decode_level(n, fp);
+		}
+	} else if (a == '1' && n == 0) {
+		res = term_new(APP);
+		res->u.app.lhs = decode_level(n, fp);
+		res->u.app.rhs = decode_level(n, fp);
+	} else if (a == '1') {
+		res = term_new(IDX);
+		res->u.index = 0;
+		while (--n != 0 && getc(fp) == '1')
+			res->u.index++;
+	}
+
+	if (!res)
+		fatal("invalid parsing state!\n");
+
+	return res;
+}
+
+static Term *decode(FILE *fp)
+{
+	return decode_level(0, fp);
+}
+
+Impl impl_closed(void)
+{
+	return (Impl){
+		.name = "closed",
+		.encode = encode,
+		.decode = decode,
+	};
+}