aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--inc/term.h1
-rw-r--r--makefile2
-rw-r--r--src/main.c4
-rw-r--r--src/parse.c2
-rw-r--r--src/reduce.c68
-rw-r--r--src/schedule.c1
-rw-r--r--src/term.c1
-rw-r--r--test/idx_inc.blc (renamed from test/inc.blc)0
-rw-r--r--test/idx_inc.blc.dump55
-rw-r--r--test/idx_open.blc (renamed from test/open.blc)0
-rw-r--r--test/idx_open.blc.dump45
-rw-r--r--test/idx_simple.blc (renamed from test/simple.blc)0
-rw-r--r--test/idx_simple.blc.dump45
-rw-r--r--test/idx_unbound.blc1
-rw-r--r--test/parenting.blc1
-rwxr-xr-xtest/run16
16 files changed, 184 insertions, 58 deletions
diff --git a/inc/term.h b/inc/term.h
index cea5278..35ed80d 100644
--- a/inc/term.h
+++ b/inc/term.h
@@ -24,7 +24,6 @@ struct term {
union {
struct {
struct term *term;
- char bound;
} abs;
struct {
struct term *lhs;
diff --git a/makefile b/makefile
index 98f26dd..90dd071 100644
--- a/makefile
+++ b/makefile
@@ -10,7 +10,7 @@ INC = ${CURDIR}/inc
SRCS = $(wildcard $(SRC)/*.c) $(wildcard $(SRC)/*/*.c)
OBJS = $(patsubst $(SRC)/%.c, $(BUILD)/%.o, $(SRCS))
-CFLAGS_DEBUG = -Wno-error -g -O0 -Wno-unused -fsanitize=address,undefined,leak
+CFLAGS_DEBUG = -DDEBUG=1 -Wno-error -g -O0 -Wno-unused -fsanitize=address,undefined,leak
CFLAGS_WARNINGS = -Wall -Wextra -Wshadow -Wpointer-arith -Wwrite-strings -Wredundant-decls -Wnested-externs -Wmissing-declarations -Wstrict-prototypes -Wmissing-prototypes -Wcast-qual -Wswitch-default -Wswitch-enum -Wunreachable-code -Wundef -Wold-style-definition -pedantic -Wno-switch-enum -Wframe-larger-than=512 -Wstack-usage=1024
CFLAGS = $(CFLAGS_WARNINGS) -std=c99 -Ofast -I$(INC) -lm
diff --git a/src/main.c b/src/main.c
index 10c9572..33d9d19 100644
--- a/src/main.c
+++ b/src/main.c
@@ -47,7 +47,7 @@ static char *read_path(const char *path)
int main(int argc, char *argv[])
{
-#if DEBUG
+#ifdef DEBUG
debug_enable(1);
#endif
@@ -64,9 +64,7 @@ int main(int argc, char *argv[])
schedule_sync_priorities();
- /* map_dump(map_all_terms()); */
debug("reducing...\n");
-
schedule();
map_dump(map_all_terms(), 0);
diff --git a/src/parse.c b/src/parse.c
index b3840d3..e2d2498 100644
--- a/src/parse.c
+++ b/src/parse.c
@@ -22,7 +22,7 @@ static struct term_handle abs_blc(char **term, size_t depth)
} else {
res_term = term_new(res_type, res, depth);
res_term->u.abs.term = inner.term;
- // TODO: remove hash from map_set (already in term anyway)?
+ // TODO: remove hash from map_set (already in term anyway)
map_set(map_all_terms(), res_term);
}
diff --git a/src/reduce.c b/src/reduce.c
index f693645..7cbc944 100644
--- a/src/reduce.c
+++ b/src/reduce.c
@@ -16,15 +16,15 @@ static struct term *shift(struct term *term, size_t level, size_t amount)
if (term->type == VAR) {
if (level > term->u.var.index)
return term;
- /* term->refs += 1; // TODO: Kinda hacky */
- return term_rehash_var(term, term->u.var.index + amount);
+ term->refs += 1; // TODO: Kinda hacky
+ return term_rehash_var(term, term->u.var.index + amount, 0);
} else if (term->type == ABS) {
struct term *previous = term->u.abs.term;
struct term *new = shift(term->u.abs.term, level + 1, amount);
if (previous->hash == new->hash)
return term; // nothing changed
- /* term->refs += 1; */
- return term_rehash_abs(term, new);
+ term->refs += 1;
+ return term_rehash_abs(term, new, 0);
} else if (term->type == APP) {
hash_t previous_lhs = term->u.app.lhs->hash;
hash_t previous_rhs = term->u.app.rhs->hash;
@@ -32,84 +32,50 @@ static struct term *shift(struct term *term, size_t level, size_t amount)
struct term *rhs = shift(term->u.app.rhs, level, amount);
if (previous_lhs == lhs->hash && previous_rhs == rhs->hash)
return term; // nothing changed
- /* term->refs += 1; */
- return term_rehash_app(term, lhs, rhs);
+ term->refs += 1;
+ return term_rehash_app(term, lhs, rhs, 0);
}
fatal("invalid type %d\n", term->type);
}
-// TODO: remove or to enum
-struct substitution_state {
- int a;
-};
-
// only substitutes (and therefore increments indices and rehashes)
-// TODO: formalize (write all rules)
-// TODO: fix inc.bruijn
-// TODO: fix unbound.bruijn
-// TODO: try [([[1 1]] [[1]])]
-// TODO: fix reparenting
static struct term *substitute(struct term *term, struct term *substitution,
- size_t level, struct substitution_state *state)
+ size_t level)
{
debug("substituting %lx with %lx\n", term->hash & HASH_MASK,
substitution->hash & HASH_MASK);
if (term->type == VAR) {
if (level == term->u.var.index) { // replace by shifted term
- state->a = 1;
struct term *shifted = shift(substitution, 0, level);
- if (shifted->hash != substitution->hash) {
- state->a = 4;
- }
return shifted;
} else if (level > term->u.var.index) { // crush unbound
- state->a = 2;
- term_deref(substitution, 1);
return term;
} else { // shift idx by -1
- state->a = 3;
struct term *shifted = shift(term, 0, -1);
- term_deref(substitution, 1);
return shifted;
}
} else if (term->type == ABS) {
- /* struct term *previous = term->u.abs.term; */
+ struct term *previous = term->u.abs.term;
hash_t previous_hash = term->u.abs.term->hash;
/* term->refs += 1; */
/* previous->refs += 1; */
- struct term *new = substitute(term->u.abs.term, substitution,
- level + 1, state);
+ struct term *new =
+ substitute(term->u.abs.term, substitution, level + 1);
if (previous_hash == new->hash)
- return term; // nothing changed
- struct term *rehashed = term_rehash_abs(term, new);
+ return new; // nothing changed
+ struct term *rehashed = term_rehash_abs(term, new, 1);
term_rehash_parents(rehashed);
- if (state->a == 3) {
- /* term_deref_head(previous, 1); */
- /* term_deref_head(previous, 1); */
- /* term->refs -= 1; */
- state->a = 0;
- }
- if (state->a == 1) {
- /* term_deref_head(previous, 1); */
- /* term_deref_head(previous, 1); */
- state->a = 0;
- }
- if (state->a == 4) {
- /* term_deref_head(term, 0); */
- /* term_deref_head(previous, 0); */
- state->a = 0;
- }
return rehashed;
} else if (term->type == APP) { // no beta reduction; just substitution
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, state);
+ substitute(term->u.app.lhs, substitution, level);
struct term *rhs =
- substitute(term->u.app.rhs, substitution, level, state);
+ substitute(term->u.app.rhs, substitution, level);
if (previous_lhs == lhs->hash && previous_rhs == rhs->hash)
return term; // nothing changed
- struct term *rehashed = term_rehash_app(term, lhs, rhs);
+ struct term *rehashed = term_rehash_app(term, lhs, rhs, 1);
term_rehash_parents(rehashed);
return rehashed;
}
@@ -124,7 +90,5 @@ struct term *reduce(struct term *term)
fatal("can't reduce non-beta-redex %d\n", term->type);
debug("reducing %lx\n", term->hash & HASH_MASK);
-
- struct substitution_state state = { 0 };
- return substitute(term->u.app.lhs, term->u.app.rhs, -1, &state);
+ return substitute(term->u.app.lhs, term->u.app.rhs, -1);
}
diff --git a/src/schedule.c b/src/schedule.c
index 458d8a2..081acfe 100644
--- a/src/schedule.c
+++ b/src/schedule.c
@@ -55,6 +55,7 @@ static size_t choose_position(void)
static pqueue_pri_t calculate_priority(struct term *term)
{
+ // TODO: Try different formulas (hyperfine)
return (parse_get_max_depth() - term->depth + 1) * term->refs;
}
diff --git a/src/term.c b/src/term.c
index 8329b85..bc347f2 100644
--- a/src/term.c
+++ b/src/term.c
@@ -111,6 +111,7 @@ struct term *term_rehash_abs(struct term *head, struct term *term,
}
// TODO: main problem is reparenting substitution tickle-up
+// TODO: investigate reparenting using gen.blc? ?!!?!
struct term *term_rehash_app(struct term *head, struct term *lhs,
struct term *rhs, int including_parents)
{
diff --git a/test/inc.blc b/test/idx_inc.blc
index 9cd3419..9cd3419 100644
--- a/test/inc.blc
+++ b/test/idx_inc.blc
diff --git a/test/idx_inc.blc.dump b/test/idx_inc.blc.dump
new file mode 100644
index 0000000..bede771
--- /dev/null
+++ b/test/idx_inc.blc.dump
@@ -0,0 +1,55 @@
+[DEBUG] reading from inc.blc
+[DEBUG] referring head of 71eb
+[DEBUG] referring head of 76e3
+[DEBUG] reducing...
+[DEBUG] queue size: 1
+
+---
+Map dump:
+type refs hash term parents
+1 1 bc00 [[1]] {([[1]] [1]), }
+1 1 d5b2 [([[1]] [1])] {}
+1 2 76e3 [1] {[[1]], ([[1]] [1]), }
+2 1 49e4 ([[1]] [1]) {[([[1]] [1])], }
+3 2 71eb 1 {[1], }
+---
+
+[DEBUG] reducing 49e4
+[DEBUG] substituting bc00 with 76e3
+[DEBUG] substituting 76e3 with 76e3
+[DEBUG] substituting 71eb with 76e3
+[DEBUG] shifting 76e3
+[DEBUG] shifting 71eb
+[DEBUG] rehashing var 71eb (2)
+[DEBUG] dereferring head of 71eb
+[DEBUG] dereferring head of 71eb
+[DEBUG] rehashing abs 76e3 (ccd5)
+[DEBUG] dereferring head of 76e3
+[DEBUG] rehashing abs 76e3 (e935)
+[DEBUG] dereferring head of 76e3
+[DEBUG] rehashing parents of 276f
+[DEBUG] rehashing abs bc00 (276f)
+[DEBUG] dereferring head of bc00
+[DEBUG] destroying head of bc00
+[DEBUG] destroying head of 49e4
+[DEBUG] destroying head of d5b2
+[DEBUG] rehashing parents of ae76
+[DEBUG] no more redexes!
+
+---
+Map dump:
+type refs hash term parents
+1 1 76e3 [1] {}
+3 1 ccd5 2 {[2], }
+1 1 e935 [2] {[[2]], }
+1 1 ae76 [[[2]]] {}
+3 1 71eb 1 {[1], }
+1 1 276f [[2]] {[[[2]]], }
+---
+
+[DEBUG] destroying head of 76e3
+[DEBUG] destroying head of ccd5
+[DEBUG] destroying head of e935
+[DEBUG] destroying head of 276f
+[DEBUG] destroying head of ae76
+[DEBUG] destroying head of 71eb
diff --git a/test/open.blc b/test/idx_open.blc
index 1540526..1540526 100644
--- a/test/open.blc
+++ b/test/idx_open.blc
diff --git a/test/idx_open.blc.dump b/test/idx_open.blc.dump
new file mode 100644
index 0000000..94a265b
--- /dev/null
+++ b/test/idx_open.blc.dump
@@ -0,0 +1,45 @@
+[DEBUG] reading from open.blc
+[DEBUG] reducing...
+[DEBUG] queue size: 1
+
+---
+Map dump:
+type refs hash term parents
+1 1 bc00 [[1]] {([4] [[1]]), }
+1 1 7573 [4] {([4] [[1]]), }
+1 1 76e3 [1] {[[1]], }
+1 1 3418 [([4] [[1]])] {}
+3 1 71eb 1 {[1], }
+3 1 c8dd 4 {[4], }
+2 1 8cde ([4] [[1]]) {[([4] [[1]])], }
+---
+
+[DEBUG] reducing 8cde
+[DEBUG] substituting 7573 with bc00
+[DEBUG] substituting c8dd with bc00
+[DEBUG] shifting c8dd
+[DEBUG] rehashing var c8dd (3)
+[DEBUG] dereferring head of c8dd
+[DEBUG] dereferring head of 71eb
+[DEBUG] destroying head of 71eb
+[DEBUG] destroying head of 76e3
+[DEBUG] destroying head of bc00
+[DEBUG] destroying head of 8cde
+[DEBUG] destroying head of 3418
+[DEBUG] rehashing abs 7573 (5f3e)
+[DEBUG] dereferring head of 7573
+[DEBUG] destroying head of 7573
+[DEBUG] rehashing parents of f80c
+[DEBUG] dereferring head of c8dd
+[DEBUG] destroying head of c8dd
+[DEBUG] no more redexes!
+
+---
+Map dump:
+type refs hash term parents
+1 1 f80c [3] {}
+3 1 5f3e 3 {[3], }
+---
+
+[DEBUG] destroying head of f80c
+[DEBUG] destroying head of 5f3e
diff --git a/test/simple.blc b/test/idx_simple.blc
index 05c2b00..05c2b00 100644
--- a/test/simple.blc
+++ b/test/idx_simple.blc
diff --git a/test/idx_simple.blc.dump b/test/idx_simple.blc.dump
new file mode 100644
index 0000000..2adc459
--- /dev/null
+++ b/test/idx_simple.blc.dump
@@ -0,0 +1,45 @@
+[DEBUG] reading from simple.blc
+[DEBUG] reducing...
+[DEBUG] queue size: 1
+
+---
+Map dump:
+type refs hash term parents
+1 1 bc00 [[1]] {([0] [[1]]), }
+1 1 76e3 [1] {[[1]], }
+2 1 4db9 ([0] [[1]]) {[([0] [[1]])], }
+1 1 180b [0] {([0] [[1]]), }
+3 1 71eb 1 {[1], }
+1 1 4e2b [([0] [[1]])] {}
+3 1 b2bf 0 {[0], }
+---
+
+[DEBUG] reducing 4db9
+[DEBUG] substituting 180b with bc00
+[DEBUG] substituting b2bf with bc00
+[DEBUG] shifting bc00
+[DEBUG] shifting 76e3
+[DEBUG] shifting 71eb
+[DEBUG] rehashing abs 180b (bc00)
+[DEBUG] dereferring head of 180b
+[DEBUG] destroying head of 180b
+[DEBUG] destroying head of 4db9
+[DEBUG] destroying head of 4e2b
+[DEBUG] rehashing parents of 7deb
+[DEBUG] dereferring head of b2bf
+[DEBUG] destroying head of b2bf
+[DEBUG] no more redexes!
+
+---
+Map dump:
+type refs hash term parents
+1 1 bc00 [[1]] {[[[1]]], }
+1 1 76e3 [1] {[[1]], }
+3 1 71eb 1 {[1], }
+1 1 7deb [[[1]]] {}
+---
+
+[DEBUG] destroying head of bc00
+[DEBUG] destroying head of 7deb
+[DEBUG] destroying head of 76e3
+[DEBUG] destroying head of 71eb
diff --git a/test/idx_unbound.blc b/test/idx_unbound.blc
new file mode 100644
index 0000000..835abbb
--- /dev/null
+++ b/test/idx_unbound.blc
@@ -0,0 +1 @@
+01000000100010
diff --git a/test/parenting.blc b/test/parenting.blc
new file mode 100644
index 0000000..bc2a397
--- /dev/null
+++ b/test/parenting.blc
@@ -0,0 +1 @@
+01010010000000000111011110010010000000000111100111011110
diff --git a/test/run b/test/run
new file mode 100755
index 0000000..8822eb9
--- /dev/null
+++ b/test/run
@@ -0,0 +1,16 @@
+#!/bin/sh
+
+set -e
+
+FAIL="\033[0;31m[FAIL]\033[0m "
+SUCC="\033[0;32m[SUCC]\033[0m "
+
+# for file in *.blc; do
+for file in idx_open.blc idx_simple.blc; do
+ ../build/calm "$file" &>../build/"$file".dump
+ cmp "$file".dump ../build/"$file".dump && printf "$SUCC" || printf "$FAIL"
+ echo "reduction of $file"
+ rm ../build/"$file".dump
+ valgrind --leak-check=full -s --error-exitcode=1 ../build/calm "$file" &>/dev/null && printf "$SUCC" || printf "$FAIL"
+ echo "memory failures of $file"
+done