aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/impl/blc.c0
-rw-r--r--src/impl/blc2.c0
-rw-r--r--src/impl/mateusz.c0
-rw-r--r--src/impl/merged_abs.c0
-rw-r--r--src/impl/merged_app.c0
-rw-r--r--src/impl/merged_both.c0
-rw-r--r--src/log.c40
-rw-r--r--src/main.c15
-rw-r--r--src/parse.c66
-rw-r--r--src/print.c52
-rw-r--r--src/term.c65
11 files changed, 238 insertions, 0 deletions
diff --git a/src/impl/blc.c b/src/impl/blc.c
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/src/impl/blc.c
diff --git a/src/impl/blc2.c b/src/impl/blc2.c
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/src/impl/blc2.c
diff --git a/src/impl/mateusz.c b/src/impl/mateusz.c
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/src/impl/mateusz.c
diff --git a/src/impl/merged_abs.c b/src/impl/merged_abs.c
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/src/impl/merged_abs.c
diff --git a/src/impl/merged_app.c b/src/impl/merged_app.c
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/src/impl/merged_app.c
diff --git a/src/impl/merged_both.c b/src/impl/merged_both.c
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/src/impl/merged_both.c
diff --git a/src/log.c b/src/log.c
new file mode 100644
index 0000000..5b4c82e
--- /dev/null
+++ b/src/log.c
@@ -0,0 +1,40 @@
+// Copyright (c) 2024, Marvin Borner <dev@marvinborner.de>
+// SPDX-License-Identifier: MIT
+
+#include <stdio.h>
+#include <stdarg.h>
+#include <stdlib.h>
+
+#include <log.h>
+
+static int debug_enabled = 0;
+
+void debug(const char *format, ...)
+{
+ if (!debug_enabled)
+ return;
+
+ fprintf(stderr, "[DEBUG]: ");
+
+ va_list ap;
+ va_start(ap, format);
+ vfprintf(stderr, format, ap);
+ va_end(ap);
+}
+
+void debug_enable(int enable)
+{
+ debug_enabled = enable;
+}
+
+void fatal(const char *format, ...)
+{
+ fprintf(stderr, "[FATAL]: ");
+
+ va_list ap;
+ va_start(ap, format);
+ vfprintf(stderr, format, ap);
+ va_end(ap);
+
+ abort();
+}
diff --git a/src/main.c b/src/main.c
new file mode 100644
index 0000000..802bfca
--- /dev/null
+++ b/src/main.c
@@ -0,0 +1,15 @@
+// Copyright (c) 2024, Marvin Borner <dev@marvinborner.de>
+// SPDX-License-Identifier: MIT
+
+#include <stdio.h>
+
+#include <term.h>
+#include <parse.h>
+#include <print.h>
+
+int main(void)
+{
+ Term *term = parse_blc_fp(stdin);
+ print_bruijn(term);
+ printf("\n");
+}
diff --git a/src/parse.c b/src/parse.c
new file mode 100644
index 0000000..f2f89cd
--- /dev/null
+++ b/src/parse.c
@@ -0,0 +1,66 @@
+// Copyright (c) 2024, Marvin Borner <dev@marvinborner.de>
+// SPDX-License-Identifier: MIT
+
+#include <parse.h>
+#include <log.h>
+#include <term.h>
+
+Term *parse_blc_fp(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 = parse_blc_fp(fp);
+ }
+ if (b == '1') {
+ res = term_new(APP);
+ res->u.app.lhs = parse_blc_fp(fp);
+ res->u.app.rhs = parse_blc_fp(fp);
+ }
+ }
+
+ 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;
+}
+
+Term *parse_blc(const char **term)
+{
+ Term *res = 0;
+ if (!**term) {
+ fatal("invalid parsing state!\n");
+ } else if (**term == '0' && *(*term + 1) == '0') {
+ (*term) += 2;
+ res = term_new(ABS);
+ res->u.abs.body = parse_blc(term);
+ } else if (**term == '0' && *(*term + 1) == '1') {
+ (*term) += 2;
+ res = term_new(APP);
+ res->u.app.lhs = parse_blc(term);
+ res->u.app.rhs = parse_blc(term);
+ } else if (**term == '1') {
+ const char *cur = *term;
+ while (**term == '1')
+ (*term)++;
+ res = term_new(IDX);
+ res->u.index = *term - cur - 1;
+ (*term)++;
+ } else {
+ (*term)++;
+ res = parse_blc(term);
+ }
+ return res;
+}
diff --git a/src/print.c b/src/print.c
new file mode 100644
index 0000000..b6493e1
--- /dev/null
+++ b/src/print.c
@@ -0,0 +1,52 @@
+// Copyright (c) 2024, Marvin Borner <dev@marvinborner.de>
+// SPDX-License-Identifier: MIT
+
+#include <stdio.h>
+
+#include <print.h>
+#include <log.h>
+
+void print_bruijn(Term *term)
+{
+ switch (term->type) {
+ case ABS:
+ fprintf(stderr, "[");
+ print_bruijn(term->u.abs.body);
+ fprintf(stderr, "]");
+ break;
+ case APP:
+ fprintf(stderr, "(");
+ print_bruijn(term->u.app.lhs);
+ fprintf(stderr, " ");
+ print_bruijn(term->u.app.rhs);
+ fprintf(stderr, ")");
+ break;
+ case IDX:
+ fprintf(stderr, "%lu", term->u.index);
+ break;
+ default:
+ fatal("invalid type %d\n", term->type);
+ }
+}
+
+void print_blc(Term *term)
+{
+ switch (term->type) {
+ case ABS:
+ printf("00");
+ print_blc(term->u.abs.body);
+ break;
+ case APP:
+ printf("01");
+ print_blc(term->u.app.lhs);
+ print_blc(term->u.app.rhs);
+ break;
+ case IDX:
+ for (size_t i = 0; i <= term->u.index; i++)
+ printf("1");
+ printf("0");
+ break;
+ default:
+ fatal("invalid type %d\n", term->type);
+ }
+}
diff --git a/src/term.c b/src/term.c
new file mode 100644
index 0000000..e68611e
--- /dev/null
+++ b/src/term.c
@@ -0,0 +1,65 @@
+// Copyright (c) 2024, Marvin Borner <dev@marvinborner.de>
+// SPDX-License-Identifier: MIT
+
+#include <stdlib.h>
+#include <stdio.h>
+
+#include <term.h>
+#include <log.h>
+#include <print.h>
+
+Term *term_new(TermType type)
+{
+ struct term *term = malloc(sizeof(*term));
+ if (!term)
+ fatal("out of memory!\n");
+ term->type = type;
+ return term;
+}
+
+void term_free(Term *term)
+{
+ switch (term->type) {
+ case ABS:
+ term_free(term->u.abs.body);
+ free(term);
+ break;
+ case APP:
+ term_free(term->u.app.lhs);
+ term_free(term->u.app.rhs);
+ free(term);
+ break;
+ case IDX:
+ free(term);
+ break;
+ default:
+ fatal("invalid type %d\n", term->type);
+ }
+}
+
+void term_diff(Term *a, Term *b)
+{
+ if (a->type != b->type) {
+ fprintf(stderr, "Term a: ");
+ print_bruijn(a);
+ fprintf(stderr, "\nTerm b: ");
+ print_bruijn(b);
+ fatal("\ntype mismatch %d %d\n", a->type, b->type);
+ }
+
+ switch (a->type) {
+ case ABS:
+ term_diff(a->u.abs.body, b->u.abs.body);
+ break;
+ case APP:
+ term_diff(a->u.app.lhs, b->u.app.lhs);
+ term_diff(a->u.app.rhs, b->u.app.rhs);
+ break;
+ case IDX:
+ if (a->u.index != b->u.index)
+ fatal("var mismatch %d=%d\n", a->u.index, b->u.index);
+ break;
+ default:
+ fatal("invalid type %d\n", a->type);
+ }
+}