From 5575fbc92dd3076f5ed3f44e6e041c6074a71fd1 Mon Sep 17 00:00:00 2001
From: Marvin Borner
Date: Mon, 29 May 2023 16:51:35 +0200
Subject: Started reducer
has some problems still
---
inc/reduce.h | 11 ++++++
inc/term.h | 7 ++++
src/main.c | 14 +++++---
src/parse.c | 6 ++--
src/reduce.c | 56 ++++++++++++++++++++++++++++++
src/term.c | 109 ++++++++++++++++++++++++++++++++++++++++++++++++-----------
6 files changed, 176 insertions(+), 27 deletions(-)
create mode 100644 inc/reduce.h
create mode 100644 src/reduce.c
diff --git a/inc/reduce.h b/inc/reduce.h
new file mode 100644
index 0000000..9856075
--- /dev/null
+++ b/inc/reduce.h
@@ -0,0 +1,11 @@
+// Copyright (c) 2023, Marvin Borner <dev@marvinborner.de>
+// SPDX-License-Identifier: MIT
+
+#ifndef CALM_REDUCE_H
+#define CALM_REDUCE_H
+
+#include <term.h>
+
+struct term *reduce(struct term *term);
+
+#endif
diff --git a/inc/term.h b/inc/term.h
index eb74c2c..5256b3c 100644
--- a/inc/term.h
+++ b/inc/term.h
@@ -28,7 +28,14 @@ struct term {
};
struct term *term_new(term_type_t type, hash_t hash, size_t depth);
+struct term *term_rehash_abs(struct term *head, struct term *term);
+struct term *term_rehash_app(struct term *head, struct term *lhs,
+ struct term *rhs);
+
+void term_refer_head(struct term *term, size_t depth);
void term_refer(struct term *term, size_t depth);
+void term_deref(struct term *term);
+
void term_print(struct term *term);
#endif
diff --git a/src/main.c b/src/main.c
index 9aaed3c..c60ebd2 100644
--- a/src/main.c
+++ b/src/main.c
@@ -6,6 +6,7 @@
#include <errno.h>
#include <string.h>
+#include <reduce.h>
#include <map.h>
#include <schedule.h>
#include <parse.h>
@@ -54,13 +55,18 @@ int main(int argc, char *argv[])
map_initialize();
char *orig_term = term;
- parse_blc(&term, 1);
+ struct term_handle handle = parse_blc(&term, 1);
free(orig_term);
- schedule_init();
- schedule();
+ term_print(handle.term);
+ struct term *new = reduce(handle.term);
+ fprintf(stderr, "\nafter\n");
+ term_print(new);
+
+ /* schedule_init(); */
+ /* schedule(); */
+ /* schedule_destroy(); */
- schedule_destroy();
map_destroy();
return 0;
}
diff --git a/src/parse.c b/src/parse.c
index b10a698..730ef44 100644
--- a/src/parse.c
+++ b/src/parse.c
@@ -18,7 +18,7 @@ static struct term_handle abs_blc(char **term, size_t depth)
struct term *res_term;
if ((res_term = map_get(res))) {
- term_refer(res_term, depth);
+ term_refer_head(res_term, depth);
} else {
res_term = term_new(res_type, res, depth);
res_term->u.abs.term = inner.term;
@@ -39,7 +39,7 @@ static struct term_handle app_blc(char **term, size_t depth)
struct term *res_term;
if ((res_term = map_get(res))) {
- term_refer(res_term, depth);
+ term_refer_head(res_term, depth);
} else {
res_term = term_new(res_type, res, depth);
res_term->u.app.lhs = lhs.term;
@@ -57,7 +57,7 @@ static struct term_handle var_blc(int index, size_t depth)
struct term *res_term;
if ((res_term = map_get(res))) {
- term_refer(res_term, depth);
+ term_refer_head(res_term, depth);
} else {
res_term = term_new(res_type, res, depth);
res_term->u.var.index = index;
diff --git a/src/reduce.c b/src/reduce.c
new file mode 100644
index 0000000..a927b12
--- /dev/null
+++ b/src/reduce.c
@@ -0,0 +1,56 @@
+// Copyright (c) 2023, Marvin Borner <dev@marvinborner.de>
+// SPDX-License-Identifier: MIT
+
+#include <stdio.h>
+
+#include <term.h>
+#include <reduce.h>
+#include <log.h>
+
+static struct term *substitute(struct term *term, struct term *substitution,
+ size_t level)
+{
+ if (term->type == VAR && term->u.var.index == level) {
+ return substitution;
+ } else if (term->type == ABS) {
+ struct term *new =
+ substitute(term->u.abs.term, substitution, level + 1);
+ return term_rehash_abs(term, new);
+ } else if (term->type == APP) {
+ struct term *lhs =
+ substitute(term->u.app.lhs, substitution, level);
+ struct term *rhs =
+ substitute(term->u.app.rhs, substitution, level);
+ return term_rehash_app(term, lhs, rhs);
+ }
+ fatal("invalid type %d\n", term->type);
+}
+
+static struct term *reduce_app(struct term *term)
+{
+ if (term->u.app.lhs->type == ABS) {
+ return substitute(term->u.app.lhs->u.abs.term, term->u.app.rhs,
+ 0);
+ } else {
+ struct term *lhs = reduce(term->u.app.lhs);
+ struct term *rhs = reduce(term->u.app.rhs);
+ return term_rehash_app(term, lhs, rhs);
+ }
+}
+
+static struct term *reduce_abs(struct term *term)
+{
+ return reduce(term->u.abs.term);
+}
+
+struct term *reduce(struct term *term)
+{
+ if (term->type == APP) {
+ return reduce_app(term);
+ } else if (term->type == ABS) {
+ return reduce_abs(term);
+ } else if (term->type == VAR) {
+ return term;
+ }
+ fatal("invalid type %d\n", term->type);
+}
diff --git a/src/term.c b/src/term.c
index 903ee8a..d52171a 100644
--- a/src/term.c
+++ b/src/term.c
@@ -3,9 +3,11 @@
#include <stdlib.h>
#include <stdio.h>
+#include <assert.h>
#include <log.h>
#include <term.h>
+#include <map.h>
struct term *term_new(term_type_t type, hash_t hash, size_t depth)
{
@@ -19,13 +21,6 @@ struct term *term_new(term_type_t type, hash_t hash, size_t depth)
return term;
}
-void term_refer(struct term *term, size_t depth)
-{
- term->refs++;
- if (depth < term->depth) // lower depths are more important
- term->depth = depth;
-}
-
void term_print(struct term *term)
{
switch (term->type) {
@@ -49,16 +44,90 @@ void term_print(struct term *term)
}
}
-/* void deref_term(struct term *term) */
-/* { */
-/* if (term->type == ABS) { */
-/* deref_term(term->u.abs.term); */
-/* } else if (term->type == APP) { */
-/* deref_term(term->u.app.lhs); */
-/* deref_term(term->u.app.rhs); */
-/* } */
-
-/* // TODO: remove from hashmap? */
-/* if (--term->refs == 0) */
-/* free(term); */
-/* } */
+struct term *term_rehash_abs(struct term *head, struct term *term)
+{
+ if (head->u.abs.term->hash == term->hash)
+ return head;
+
+ hash_t res =
+ hash((uint8_t *)&head->type, sizeof(head->type), term->hash);
+
+ assert(res != head->hash);
+
+ struct term *match = map_get(res);
+ if (match) { // already exists
+ term_refer(match, head->depth);
+ term_deref(head);
+ return match;
+ } else { // create new
+ struct term *new = term_new(ABS, res, head->depth);
+ new->u.abs.term = term;
+ term_refer(term, head->depth + 1);
+ term_deref(head);
+ return new;
+ }
+}
+
+struct term *term_rehash_app(struct term *head, struct term *lhs,
+ struct term *rhs)
+{
+ if (head->u.app.lhs->hash == lhs->hash &&
+ head->u.app.rhs->hash == rhs->hash)
+ return head;
+
+ hash_t res =
+ hash((uint8_t *)&head->type, sizeof(head->type), lhs->hash);
+ res = hash((uint8_t *)&res, sizeof(res), rhs->hash);
+
+ assert(res != head->hash);
+
+ struct term *match = map_get(res);
+ if (match) { // already exists
+ term_refer(match, head->depth);
+ term_deref(head);
+ return match;
+ } else { // create new
+ struct term *new = term_new(APP, res, head->depth);
+ new->u.app.lhs = lhs;
+ new->u.app.rhs = rhs;
+ if (head->u.app.lhs->hash != lhs->hash)
+ term_refer(lhs, head->depth + 1);
+ if (head->u.app.rhs->hash != rhs->hash)
+ term_refer(rhs, head->depth + 1);
+ term_deref(head);
+ return new;
+ }
+}
+
+void term_refer_head(struct term *term, size_t depth)
+{
+ term->refs++;
+ if (depth < term->depth) // lower depths are more important
+ term->depth = depth;
+}
+
+void term_refer(struct term *term, size_t depth)
+{
+ if (term->type == ABS) {
+ term_refer(term->u.abs.term, depth + 1);
+ } else if (term->type == APP) {
+ term_refer(term->u.app.lhs, depth + 1);
+ term_refer(term->u.app.rhs, depth + 1);
+ }
+
+ term_refer_head(term, depth);
+}
+
+void term_deref(struct term *term)
+{
+ if (term->type == ABS) {
+ term_deref(term->u.abs.term);
+ } else if (term->type == APP) {
+ term_deref(term->u.app.lhs);
+ term_deref(term->u.app.rhs);
+ }
+
+ // TODO: remove from hashmap?
+ if (--term->refs == 0)
+ free(term);
+}
--
cgit v1.2.3