diff options
| -rw-r--r-- | inc/sharing.h | 2 | ||||
| -rw-r--r-- | readme.md | 8 | ||||
| -rw-r--r-- | src/main.c | 2 | ||||
| -rw-r--r-- | src/sharing.c | 43 |
4 files changed, 43 insertions, 12 deletions
diff --git a/inc/sharing.h b/inc/sharing.h index 7be84f4..6689e2d 100644 --- a/inc/sharing.h +++ b/inc/sharing.h @@ -6,6 +6,6 @@ #include <term.h> -void blind_check(void); +void sharing_query(struct term *a, struct term *b); #endif @@ -1,13 +1,13 @@ # Sharing equality of $\lambda$-graphs -A reference implementation of the algorithms presented in \[0\]. +A *reference implementation* of the algorithms presented in \[0\]. I documented my approach of building the shared $\lambda$-graph [in an article](https://text.marvinborner.de/2023-05-30-16.html). -## Instructions - -- `make && ./build/sharing file.blc` +This project does not really have any purpose except for the +implementation itself. Its usage requires some adaption and +modification. ## Libraries @@ -55,7 +55,7 @@ int main(int argc, char *argv[]) parse_blc(&term); free(orig_term); - blind_check(); + // sharing_query(a, b); map_destroy(); return 0; diff --git a/src/sharing.c b/src/sharing.c index eda3fd3..3219860 100644 --- a/src/sharing.c +++ b/src/sharing.c @@ -31,7 +31,7 @@ static void enqueue_and_propagate(struct term *neighbour, struct term *term) term->u.app.rhs->neighbours, neighbour->u.app.rhs); } else if (neighbour->type == VAR && term->type == VAR) { } else { - fatal("huh3?\n"); + fatal("query failed\n"); } neighbour->canonic = term; queue_push(term->queue, neighbour); @@ -54,7 +54,7 @@ static void build_equivalence_class(struct term *term) if (!parent->canonic) { build_equivalence_class(parent); } else if (parent->canonic->building) { - fatal("huh?\n"); + fatal("query failed\n"); } iterator = iterator->next; } @@ -65,7 +65,7 @@ static void build_equivalence_class(struct term *term) if (!neighbour->canonic) { enqueue_and_propagate(neighbour, term); } else if (neighbour->canonic != term) { - fatal("huh2?\n"); + fatal("query failed\n"); } } } @@ -73,7 +73,7 @@ static void build_equivalence_class(struct term *term) term->building = 0; } -static void iter_callback(struct term *term) +static void blind_check_callback(struct term *term) { if (term->canonic) return; @@ -81,7 +81,38 @@ static void iter_callback(struct term *term) } // Procedure BlindCheck() -void blind_check(void) +static void blind_check(void) { - map_foreach(iter_callback); + map_foreach(blind_check_callback); +} + +static void var_check_callback(struct term *term) +{ + if (term->type != VAR) + return; + struct term *canonic = term->canonic; + if (canonic != term) { + // you should compare the binders as stated in the paper. + // due to the implementation I just compare the indices directly + if (canonic->u.var.index != term->u.var.index) { + fatal("query failed\n"); + } + } +} + +// Procedure VarCheck() +static void var_check(void) +{ + map_foreach(var_check_callback); +} + +// this doesn't really make sense for this specific implementation of +// λ-graphs using hashes. It's a reference implementation after all. +void sharing_query(struct term *a, struct term *b) +{ + a->neighbours = list_add(a->neighbours, b); + b->neighbours = list_add(b->neighbours, a); + + blind_check(); + var_check(); } |