Normalization

1 files changed, 34 insertions, 2 deletions

diff --git a/src/parse.c b/src/parse.c
index 495f55f..306bf4f 100644
--- a/src/parse.c
+++ b/src/parse.c
@@ -6,6 +6,12 @@
 #include <parse.h>
 #include <term.h>
 
+static int name_generator(void)
+{
+	static int current = 0x424242; // TODO: idk?
+	return current++;
+}
+
 static struct term *rec(const char **term)
 {
 	struct term *res = 0;
@@ -22,7 +28,8 @@ static struct term *rec(const char **term)
 		res->u.app.rhs = rec(term);
 	} else if (**term >= '0' && **term <= '9') {
 		res = new_term(VAR);
-		res->u.var = **term - '0';
+		res->u.var.name = **term - '0';
+		res->u.var.type = BRUIJN_INDEX;
 		(*term)++;
 	} else {
 		(*term)++;
@@ -31,7 +38,32 @@ static struct term *rec(const char **term)
 	return res;
 }
 
+// TODO: WARNING: This might not be 100% correct! Verify!
+static void to_barendregt(struct term *term, int level, int replacement)
+{
+	switch (term->type) {
+	case ABS:
+		term->u.abs.name = name_generator();
+		to_barendregt(term->u.abs.term, level + 1, term->u.abs.name);
+		break;
+	case APP:
+		to_barendregt(term->u.app.lhs, level, replacement);
+		to_barendregt(term->u.app.rhs, level, replacement);
+		break;
+	case VAR:
+		if (term->u.var.type == BRUIJN_INDEX) {
+			term->u.var.name = replacement - term->u.var.name;
+			term->u.var.type = BARENDREGT_VARIABLE;
+		}
+		break;
+	default:
+		fprintf(stderr, "Invalid type %d\n", term->type);
+	}
+}
+
 struct term *parse(const char *term)
 {
-	return rec(&term);
+	struct term *parsed = rec(&term);
+	to_barendregt(parsed, -1, -1);
+	return parsed;
 }