aboutsummaryrefslogtreecommitdiff
path: root/src/impl
diff options
context:
space:
mode:
Diffstat (limited to 'src/impl')
-rw-r--r--src/impl/blc.c65
-rw-r--r--src/impl/blc2.c93
-rw-r--r--src/impl/closed.c100
-rw-r--r--src/impl/mateusz.c0
4 files changed, 258 insertions, 0 deletions
diff --git a/src/impl/blc.c b/src/impl/blc.c
index e69de29..893b856 100644
--- a/src/impl/blc.c
+++ b/src/impl/blc.c
@@ -0,0 +1,65 @@
+// Copyright (c) 2024, Marvin Borner <dev@marvinborner.de>
+// SPDX-License-Identifier: MIT
+
+#include <log.h>
+#include <impl.h>
+
+static void encode(Term *term, FILE *fp)
+{
+ switch (term->type) {
+ case ABS:
+ fprintf(fp, "00");
+ encode(term->u.abs.body, fp);
+ break;
+ case APP:
+ fprintf(fp, "01");
+ encode(term->u.app.lhs, fp);
+ encode(term->u.app.rhs, fp);
+ break;
+ case IDX:
+ for (size_t i = 0; i <= term->u.index; i++)
+ fprintf(fp, "1");
+ fprintf(fp, "0");
+ break;
+ default:
+ fatal("invalid type %d\n", term->type);
+ }
+}
+
+static Term *decode(FILE *fp)
+{
+ Term *res = 0;
+
+ char a = getc(fp);
+
+ if (a == '0') {
+ char b = getc(fp);
+ if (b == '0') {
+ res = term_new(ABS);
+ res->u.abs.body = decode(fp);
+ } else if (b == '1') {
+ res = term_new(APP);
+ res->u.app.lhs = decode(fp);
+ res->u.app.rhs = decode(fp);
+ }
+ } else if (a == '1') {
+ res = term_new(IDX);
+ res->u.index = 0;
+ while (getc(fp) == '1')
+ res->u.index++;
+ }
+
+ if (!res)
+ fatal("invalid parsing state!\n");
+
+ return res;
+}
+
+Impl impl_blc(void)
+{
+ return (Impl){
+ .name = "blc",
+ .encode = encode,
+ .decode = decode,
+ };
+}
diff --git a/src/impl/blc2.c b/src/impl/blc2.c
index e69de29..3cf7ff8 100644
--- a/src/impl/blc2.c
+++ b/src/impl/blc2.c
@@ -0,0 +1,93 @@
+// Copyright (c) 2024, Marvin Borner <dev@marvinborner.de>
+// SPDX-License-Identifier: MIT
+
+#include <log.h>
+#include <impl.h>
+#include <stdint.h>
+
+// haskell by John Tromp
+static void levenshtein_encode(size_t n, FILE *fp)
+{
+ if (n == 0) {
+ fprintf(fp, "10");
+ return;
+ }
+
+ fprintf(fp, "1");
+
+ size_t length = (8 * sizeof(n)) - __builtin_clzll(n);
+ levenshtein_encode(length - 1, fp);
+
+ if (length == 1)
+ return;
+
+ for (size_t i = 1 << (length - 2); i != 0; i >>= 1)
+ fprintf(fp, "%d", (i & n) != 0);
+}
+
+static void encode(Term *term, FILE *fp)
+{
+ switch (term->type) {
+ case ABS:
+ fprintf(fp, "00");
+ encode(term->u.abs.body, fp);
+ break;
+ case APP:
+ fprintf(fp, "01");
+ encode(term->u.app.lhs, fp);
+ encode(term->u.app.rhs, fp);
+ break;
+ case IDX:
+ levenshtein_encode(term->u.index, fp);
+ break;
+ default:
+ fatal("invalid type %d\n", term->type);
+ }
+}
+
+// by John Tromp
+static size_t levenshtein_decode(FILE *fp)
+{
+ if (getc(fp) == '0')
+ return 0;
+ size_t x, l = levenshtein_decode(fp);
+ for (x = 1; l--;)
+ x = 2 * x + (getc(fp) != '0');
+ return x;
+}
+
+static Term *decode(FILE *fp)
+{
+ Term *res = 0;
+
+ char a = getc(fp);
+
+ if (a == '0') {
+ char b = getc(fp);
+ if (b == '0') {
+ res = term_new(ABS);
+ res->u.abs.body = decode(fp);
+ } else if (b == '1') {
+ res = term_new(APP);
+ res->u.app.lhs = decode(fp);
+ res->u.app.rhs = decode(fp);
+ }
+ } else if (a == '1') {
+ res = term_new(IDX);
+ res->u.index = levenshtein_decode(fp);
+ }
+
+ if (!res)
+ fatal("invalid parsing state!\n");
+
+ return res;
+}
+
+Impl impl_blc2(void)
+{
+ return (Impl){
+ .name = "blc2",
+ .encode = encode,
+ .decode = decode,
+ };
+}
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,
+ };
+}
diff --git a/src/impl/mateusz.c b/src/impl/mateusz.c
deleted file mode 100644
index e69de29..0000000
--- a/src/impl/mateusz.c
+++ /dev/null