aboutsummaryrefslogtreecommitdiff
path: root/src/reduce.c
diff options
context:
space:
mode:
authorMarvin Borner2023-06-01 23:08:07 +0200
committerMarvin Borner2023-06-01 23:08:07 +0200
commitc9b0537a1f04c8a28e1f9aa9a6112a1e59653eea (patch)
treeec403ce89057acf409ac8ccb21c0538d207f5a47 /src/reduce.c
parentc062eaeea09592cbdf7e5d732e992d0cdd8eedc5 (diff)
Some work on derefs
Diffstat (limited to 'src/reduce.c')
-rw-r--r--src/reduce.c21
1 files changed, 14 insertions, 7 deletions
diff --git a/src/reduce.c b/src/reduce.c
index 9e7520d..38baf06 100644
--- a/src/reduce.c
+++ b/src/reduce.c
@@ -4,6 +4,7 @@
#include <stdio.h>
#include <term.h>
+#include <map.h>
#include <reduce.h>
#include <log.h>
#include <assert.h>
@@ -13,26 +14,28 @@ static struct term *substitute(struct term *term, struct term *substitution,
{
if (term->type == VAR) {
if (term->u.var.index == level) {
- // TODO: deref index
+ term_deref_head(term);
return substitution;
} else {
return term;
}
} else if (term->type == ABS) {
+ hash_t previous = term->u.abs.term->hash;
struct term *new =
substitute(term->u.abs.term, substitution, level + 1);
- if (term->u.abs.term->hash == new->hash)
+ if (previous == new->hash)
return term; // nothing changed
struct term *rehashed = term_rehash_abs(term, new);
term_rehash_parents(rehashed);
return rehashed;
} else if (term->type == APP) {
+ hash_t previous_lhs = term->u.app.lhs->hash;
+ hash_t previous_rhs = term->u.app.rhs->hash;
struct term *lhs =
substitute(term->u.app.lhs, substitution, level);
struct term *rhs =
substitute(term->u.app.rhs, substitution, level);
- if (term->u.app.lhs->hash == lhs->hash &&
- term->u.app.rhs->hash == rhs->hash)
+ if (previous_lhs == lhs->hash && previous_rhs == rhs->hash)
return term; // nothing changed
struct term *rehashed = term_rehash_app(term, lhs, rhs);
term_rehash_parents(rehashed);
@@ -45,8 +48,12 @@ static struct term *substitute(struct term *term, struct term *substitution,
// ([X] Y) -> X/Y
struct term *reduce(struct term *term)
{
- assert(term->type == APP);
- assert(term->u.app.lhs->type == ABS);
+ if (term->type != APP || term->u.app.lhs->type != ABS)
+ fatal("can't reduce non-beta-redex %d\n", term->type);
- return substitute(term->u.app.lhs, term->u.app.rhs, -1);
+ map_delete(term->u.app.lhs->parents, term);
+ map_delete(term->u.app.rhs->parents, term);
+ struct term *reduced = substitute(term->u.app.lhs, term->u.app.rhs, -1);
+ term_deref_head(term);
+ return reduced;
}