From cbd21e1da0d763225e7ea3594d4e6d8e96863790 Mon Sep 17 00:00:00 2001 From: Marvin Borner Date: Tue, 30 May 2023 23:05:30 +0200 Subject: Added hash-based approach --- inc/lib/hash.h | 14 +++ inc/lib/hashmap.h | 31 ++++++ inc/lib/list.h | 15 +++ inc/lib/queue.h | 23 ++++ inc/map.h | 16 +++ inc/parse.h | 2 +- inc/queue.h | 24 ---- inc/sharing.h | 11 ++ inc/term.h | 13 ++- readme.md | 22 +++- src/lib/hash.c | 135 ++++++++++++++++++++++ src/lib/hashmap.c | 327 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ src/lib/list.c | 32 ++++++ src/lib/queue.c | 61 ++++++++++ src/main.c | 10 +- src/map.c | 59 ++++++++++ src/parse.c | 74 ++++++++++-- src/queue.c | 56 ---------- src/sharing.c | 87 +++++++++++++++ src/term.c | 5 +- 20 files changed, 914 insertions(+), 103 deletions(-) create mode 100644 inc/lib/hash.h create mode 100644 inc/lib/hashmap.h create mode 100644 inc/lib/list.h create mode 100644 inc/lib/queue.h create mode 100644 inc/map.h delete mode 100644 inc/queue.h create mode 100644 inc/sharing.h create mode 100644 src/lib/hash.c create mode 100644 src/lib/hashmap.c create mode 100644 src/lib/list.c create mode 100644 src/lib/queue.c create mode 100644 src/map.c delete mode 100644 src/queue.c create mode 100644 src/sharing.c diff --git a/inc/lib/hash.h b/inc/lib/hash.h new file mode 100644 index 0000000..7cfad83 --- /dev/null +++ b/inc/lib/hash.h @@ -0,0 +1,14 @@ +// Copyright (c) 2023, Marvin Borner +// SPDX-License-Identifier: MIT + +#ifndef SHARING_HASH_H +#define SHARING_HASH_H + +#include +#include + +typedef uint64_t hash_t; + +hash_t hash(void *data, size_t len, uint64_t seed); + +#endif diff --git a/inc/lib/hashmap.h b/inc/lib/hashmap.h new file mode 100644 index 0000000..db70bdd --- /dev/null +++ b/inc/lib/hashmap.h @@ -0,0 +1,31 @@ +// Copyright 2020 Joshua J Baker. All rights reserved. +// Copyright 2023 Marvin Borner +// Use of this source code is governed by an MIT-style +// license that can be found in the LICENSE file. + +#ifndef SHARING_HASHMAP_H +#define SHARING_HASHMAP_H + +#include +#include +#include + +struct hashmap; + +struct hashmap *hashmap_new(size_t elsize, size_t cap, + void (*elfree)(void *item)); + +void hashmap_free(struct hashmap *map); +void hashmap_clear(struct hashmap *map, bool update_cap); +size_t hashmap_count(struct hashmap *map); +bool hashmap_oom(struct hashmap *map); +void *hashmap_probe(struct hashmap *map, uint64_t position); +bool hashmap_scan(struct hashmap *map, bool (*iter)(void *item)); +bool hashmap_iter(struct hashmap *map, size_t *i, void **item); + +void *hashmap_get(struct hashmap *map, uint64_t hash); +void *hashmap_delete(struct hashmap *map, uint64_t hash); +void *hashmap_set(struct hashmap *map, void *item, uint64_t hash); +void hashmap_set_grow_by_power(struct hashmap *map, size_t power); + +#endif diff --git a/inc/lib/list.h b/inc/lib/list.h new file mode 100644 index 0000000..b57d85b --- /dev/null +++ b/inc/lib/list.h @@ -0,0 +1,15 @@ +// Copyright (c) 2023, Marvin Borner +// SPDX-License-Identifier: MIT + +#ifndef SHARING_LIST_H +#define SHARING_LIST_H + +struct list { + void *data; + struct list *next; +}; + +struct list *list_add(struct list *list, void *data); +void list_free(struct list *list); + +#endif diff --git a/inc/lib/queue.h b/inc/lib/queue.h new file mode 100644 index 0000000..b0d22ef --- /dev/null +++ b/inc/lib/queue.h @@ -0,0 +1,23 @@ +// Copyright (c) 2023, Marvin Borner +// SPDX-License-Identifier: MIT + +#ifndef SHARING_QUEUE_H +#define SHARING_QUEUE_H + +struct queue_node { + void *data; + struct queue_node *next; +}; + +struct queue { + struct queue_node *head; + struct queue_node *tail; +}; + +struct queue *queue_new(void); +void queue_free(struct queue *queue); +void queue_push(struct queue *queue, void *data); +void *queue_pop(struct queue *queue); +int queue_empty(struct queue *queue); + +#endif diff --git a/inc/map.h b/inc/map.h new file mode 100644 index 0000000..84d1ae5 --- /dev/null +++ b/inc/map.h @@ -0,0 +1,16 @@ +// Copyright (c) 2023, Marvin Borner +// SPDX-License-Identifier: MIT + +#ifndef SHARING_MAP_H +#define SHARING_MAP_H + +#include + +struct term *map_get(hash_t hash); +void map_set(struct term *term, hash_t hash); +void map_delete(struct term *term); +void map_initialize(void); +void map_destroy(void); +void map_foreach(void (*func)(struct term *)); + +#endif diff --git a/inc/parse.h b/inc/parse.h index 451647f..2b881e6 100644 --- a/inc/parse.h +++ b/inc/parse.h @@ -6,6 +6,6 @@ #include -struct term *parse_blc(char **term); +struct term_handle parse_blc(char **term); #endif diff --git a/inc/queue.h b/inc/queue.h deleted file mode 100644 index 5a704b4..0000000 --- a/inc/queue.h +++ /dev/null @@ -1,24 +0,0 @@ -// Copyright (c) 2023, Marvin Borner -// SPDX-License-Identifier: MIT - -#ifndef SHARING_QUEUE_H -#define SHARING_QUEUE_H - -#include - -struct queue_node { - void *data; - struct queue_node *next; -}; - -struct queue { - struct queue_node *head; - struct queue_node *tail; -}; - -struct queue *queue_new(void); -void queue_free(struct queue *queue); -void queue_push(struct queue *queue, void *data); -void *queue_pop(struct queue *queue); - -#endif diff --git a/inc/sharing.h b/inc/sharing.h new file mode 100644 index 0000000..7be84f4 --- /dev/null +++ b/inc/sharing.h @@ -0,0 +1,11 @@ +// Copyright (c) 2023, Marvin Borner +// SPDX-License-Identifier: MIT + +#ifndef SHARING_SHARING_H +#define SHARING_SHARING_H + +#include + +void blind_check(void); + +#endif diff --git a/inc/term.h b/inc/term.h index 3bc94eb..fe4b6b8 100644 --- a/inc/term.h +++ b/inc/term.h @@ -6,15 +6,24 @@ #include -#include +#include +#include typedef enum { INV, ABS, APP, VAR } term_type_t; +struct term_handle { + struct term *term; + hash_t hash; +}; + struct term { term_type_t type; + hash_t hash; struct term *canonic; char building; struct queue *queue; + struct list *parents; + struct list *neighbours; union { struct { struct term *term; @@ -29,7 +38,7 @@ struct term { } u; }; -struct term *term_new(term_type_t type); +struct term *term_new(term_type_t type, hash_t hash); void term_free(struct term *term); void term_print(struct term *term); diff --git a/readme.md b/readme.md index d48ae96..e6d9692 100644 --- a/readme.md +++ b/readme.md @@ -1,8 +1,24 @@ -# Sharing equality +# Sharing equality of $\lambda$-graphs -An 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` + +## Libraries + +- [hashmap.c](https://github.com/tidwall/hashmap.c) \[MIT\]: Simple but + efficient hashmap +- [xxHash](https://github.com/Cyan4973/xxHash/) \[BSD 2-Clause\]: + Extremely fast hash algorithm + +## References \[0\]: Condoluci, Andrea, Beniamino Accattoli, and Claudio Sacerdoti -Coen. "Sharing equality is linear." Proceedings of the 21st +Coen. “Sharing equality is linear.” Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming. 2019. diff --git a/src/lib/hash.c b/src/lib/hash.c new file mode 100644 index 0000000..392f79d --- /dev/null +++ b/src/lib/hash.c @@ -0,0 +1,135 @@ +//----------------------------------------------------------------------------- +// xxHash Library +// Copyright (c) 2012-2021 Yann Collet +// Copyright (c) 2023 Marvin Borner +// All rights reserved. +// +// BSD 2-Clause License (https://www.opensource.org/licenses/bsd-license.php) +// +// xxHash3 +//----------------------------------------------------------------------------- + +#include + +#include + +#define XXH_PRIME_1 11400714785074694791ULL +#define XXH_PRIME_2 14029467366897019727ULL +#define XXH_PRIME_3 1609587929392839161ULL +#define XXH_PRIME_4 9650029242287828579ULL +#define XXH_PRIME_5 2870177450012600261ULL + +static uint64_t XXH_read64(void *memptr) +{ + uint64_t val; + memcpy(&val, memptr, sizeof(val)); + return val; +} + +static uint32_t XXH_read32(void *memptr) +{ + uint32_t val; + memcpy(&val, memptr, sizeof(val)); + return val; +} + +static uint64_t XXH_rotl64(uint64_t x, int r) +{ + return (x << r) | (x >> (64 - r)); +} + +hash_t hash(void *data, size_t len, uint64_t seed) +{ + uint8_t *p = (uint8_t *)data; + uint8_t *end = p + len; + uint64_t h64; + + if (len >= 32) { + uint8_t *limit = end - 32; + uint64_t v1 = seed + XXH_PRIME_1 + XXH_PRIME_2; + uint64_t v2 = seed + XXH_PRIME_2; + uint64_t v3 = seed + 0; + uint64_t v4 = seed - XXH_PRIME_1; + + do { + v1 += XXH_read64(p) * XXH_PRIME_2; + v1 = XXH_rotl64(v1, 31); + v1 *= XXH_PRIME_1; + + v2 += XXH_read64(p + 8) * XXH_PRIME_2; + v2 = XXH_rotl64(v2, 31); + v2 *= XXH_PRIME_1; + + v3 += XXH_read64(p + 16) * XXH_PRIME_2; + v3 = XXH_rotl64(v3, 31); + v3 *= XXH_PRIME_1; + + v4 += XXH_read64(p + 24) * XXH_PRIME_2; + v4 = XXH_rotl64(v4, 31); + v4 *= XXH_PRIME_1; + + p += 32; + } while (p <= limit); + + h64 = XXH_rotl64(v1, 1) + XXH_rotl64(v2, 7) + + XXH_rotl64(v3, 12) + XXH_rotl64(v4, 18); + + v1 *= XXH_PRIME_2; + v1 = XXH_rotl64(v1, 31); + v1 *= XXH_PRIME_1; + h64 ^= v1; + h64 = h64 * XXH_PRIME_1 + XXH_PRIME_4; + + v2 *= XXH_PRIME_2; + v2 = XXH_rotl64(v2, 31); + v2 *= XXH_PRIME_1; + h64 ^= v2; + h64 = h64 * XXH_PRIME_1 + XXH_PRIME_4; + + v3 *= XXH_PRIME_2; + v3 = XXH_rotl64(v3, 31); + v3 *= XXH_PRIME_1; + h64 ^= v3; + h64 = h64 * XXH_PRIME_1 + XXH_PRIME_4; + + v4 *= XXH_PRIME_2; + v4 = XXH_rotl64(v4, 31); + v4 *= XXH_PRIME_1; + h64 ^= v4; + h64 = h64 * XXH_PRIME_1 + XXH_PRIME_4; + } else { + h64 = seed + XXH_PRIME_5; + } + + h64 += (uint64_t)len; + + while (p + 8 <= end) { + uint64_t k1 = XXH_read64(p); + k1 *= XXH_PRIME_2; + k1 = XXH_rotl64(k1, 31); + k1 *= XXH_PRIME_1; + h64 ^= k1; + h64 = XXH_rotl64(h64, 27) * XXH_PRIME_1 + XXH_PRIME_4; + p += 8; + } + + if (p + 4 <= end) { + h64 ^= (uint64_t)(XXH_read32(p)) * XXH_PRIME_1; + h64 = XXH_rotl64(h64, 23) * XXH_PRIME_2 + XXH_PRIME_3; + p += 4; + } + + while (p < end) { + h64 ^= (*p) * XXH_PRIME_5; + h64 = XXH_rotl64(h64, 11) * XXH_PRIME_1; + p++; + } + + h64 ^= h64 >> 33; + h64 *= XXH_PRIME_2; + h64 ^= h64 >> 29; + h64 *= XXH_PRIME_3; + h64 ^= h64 >> 32; + + return h64; +} diff --git a/src/lib/hashmap.c b/src/lib/hashmap.c new file mode 100644 index 0000000..7de7245 --- /dev/null +++ b/src/lib/hashmap.c @@ -0,0 +1,327 @@ +// Copyright 2020 Joshua J Baker. All rights reserved. +// Copyright 2023 Marvin Borner +// Use of this source code is governed by an MIT-style +// license that can be found in the LICENSE file. + +// This is a fork of tidwall's hashmap. It's heavily reduced and adapted. + +#include +#include +#include +#include +#include + +#include +#include + +#define GROW_AT 0.60 +#define SHRINK_AT 0.10 + +struct bucket { + uint64_t hash : 48; + uint64_t dib : 16; +}; + +struct hashmap { + size_t elsize; + size_t cap; + void (*elfree)(void *item); + size_t bucketsz; + size_t nbuckets; + size_t count; + size_t mask; + size_t growat; + size_t shrinkat; + uint8_t growpower; + bool oom; + void *buckets; + void *spare; + void *edata; +}; + +void hashmap_set_grow_by_power(struct hashmap *map, size_t power) +{ + map->growpower = power < 1 ? 1 : power > 16 ? 16 : power; +} + +static struct bucket *bucket_at0(void *buckets, size_t bucketsz, size_t i) +{ + return (struct bucket *)(((char *)buckets) + (bucketsz * i)); +} + +static struct bucket *bucket_at(struct hashmap *map, size_t index) +{ + return bucket_at0(map->buckets, map->bucketsz, index); +} + +static void *bucket_item(struct bucket *entry) +{ + return ((char *)entry) + sizeof(struct bucket); +} + +static uint64_t clip_hash(uint64_t hash) +{ + return hash & 0xFFFFFFFFFFFF; +} + +struct hashmap *hashmap_new(size_t elsize, size_t cap, + void (*elfree)(void *item)) +{ + size_t ncap = 16; + if (cap < ncap) { + cap = ncap; + } else { + while (ncap < cap) { + ncap *= 2; + } + cap = ncap; + } + size_t bucketsz = sizeof(struct bucket) + elsize; + while (bucketsz & (sizeof(uintptr_t) - 1)) { + bucketsz++; + } + // hashmap + spare + edata + size_t size = sizeof(struct hashmap) + bucketsz * 2; + struct hashmap *map = malloc(size); + if (!map) { + return NULL; + } + memset(map, 0, sizeof(struct hashmap)); + map->elsize = elsize; + map->bucketsz = bucketsz; + map->elfree = elfree; + map->spare = ((char *)map) + sizeof(struct hashmap); + map->edata = (char *)map->spare + bucketsz; + map->cap = cap; + map->nbuckets = cap; + map->mask = map->nbuckets - 1; + map->buckets = malloc(map->bucketsz * map->nbuckets); + if (!map->buckets) { + free(map); + return NULL; + } + memset(map->buckets, 0, map->bucketsz * map->nbuckets); + map->growpower = 1; + map->growat = map->nbuckets * GROW_AT; + map->shrinkat = map->nbuckets * SHRINK_AT; + return map; +} + +static void free_elements(struct hashmap *map) +{ + if (!map->elfree) + return; + + for (size_t i = 0; i < map->nbuckets; i++) { + struct bucket *bucket = bucket_at(map, i); + if (bucket->dib) + map->elfree(bucket_item(bucket)); + } +} + +void hashmap_clear(struct hashmap *map, bool update_cap) +{ + map->count = 0; + free_elements(map); + if (update_cap) { + map->cap = map->nbuckets; + } else if (map->nbuckets != map->cap) { + void *new_buckets = malloc(map->bucketsz * map->cap); + if (new_buckets) { + free(map->buckets); + map->buckets = new_buckets; + } + map->nbuckets = map->cap; + } + memset(map->buckets, 0, map->bucketsz * map->nbuckets); + map->mask = map->nbuckets - 1; + map->growat = map->nbuckets * 0.75; + map->shrinkat = map->nbuckets * 0.10; +} + +static bool resize0(struct hashmap *map, size_t new_cap) +{ + struct hashmap *map2 = hashmap_new(map->elsize, new_cap, map->elfree); + if (!map2) + return false; + for (size_t i = 0; i < map->nbuckets; i++) { + struct bucket *entry = bucket_at(map, i); + if (!entry->dib) { + continue; + } + entry->dib = 1; + size_t j = entry->hash & map2->mask; + while (1) { + struct bucket *bucket = bucket_at(map2, j); + if (bucket->dib == 0) { + memcpy(bucket, entry, map->bucketsz); + break; + } + if (bucket->dib < entry->dib) { + memcpy(map2->spare, bucket, map->bucketsz); + memcpy(bucket, entry, map->bucketsz); + memcpy(entry, map2->spare, map->bucketsz); + } + j = (j + 1) & map2->mask; + entry->dib += 1; + } + } + free(map->buckets); + map->buckets = map2->buckets; + map->nbuckets = map2->nbuckets; + map->mask = map2->mask; + map->growat = map2->growat; + map->shrinkat = map2->shrinkat; + free(map2); + return true; +} + +static bool resize(struct hashmap *map, size_t new_cap) +{ + return resize0(map, new_cap); +} + +void *hashmap_set(struct hashmap *map, void *item, uint64_t hash) +{ + hash = clip_hash(hash); + map->oom = false; + if (map->count == map->growat) { + if (!resize(map, map->nbuckets * (1 << map->growpower))) { + map->oom = true; + return NULL; + } + } + + struct bucket *entry = map->edata; + entry->hash = hash; + entry->dib = 1; + void *eitem = bucket_item(entry); + memcpy(eitem, item, map->elsize); + + void *bitem; + size_t i = entry->hash & map->mask; + while (1) { + struct bucket *bucket = bucket_at(map, i); + if (bucket->dib == 0) { + memcpy(bucket, entry, map->bucketsz); + map->count++; + return NULL; + } + bitem = bucket_item(bucket); + if (entry->hash == bucket->hash) { + memcpy(map->spare, bitem, map->elsize); + memcpy(bitem, eitem, map->elsize); + return map->spare; + } + if (bucket->dib < entry->dib) { + memcpy(map->spare, bucket, map->bucketsz); + memcpy(bucket, entry, map->bucketsz); + memcpy(entry, map->spare, map->bucketsz); + eitem = bucket_item(entry); + } + i = (i + 1) & map->mask; + entry->dib += 1; + } +} + +void *hashmap_get(struct hashmap *map, uint64_t hash) +{ + hash = clip_hash(hash); + size_t i = hash & map->mask; + while (1) { + struct bucket *bucket = bucket_at(map, i); + if (!bucket->dib) + return NULL; + if (bucket->hash == hash) + return bucket_item(bucket); + i = (i + 1) & map->mask; + } +} + +void *hashmap_probe(struct hashmap *map, uint64_t position) +{ + size_t i = position & map->mask; + struct bucket *bucket = bucket_at(map, i); + if (!bucket->dib) { + return NULL; + } + return bucket_item(bucket); +} + +void *hashmap_delete(struct hashmap *map, uint64_t hash) +{ + hash = clip_hash(hash); + map->oom = false; + size_t i = hash & map->mask; + while (1) { + struct bucket *bucket = bucket_at(map, i); + if (!bucket->dib) + return NULL; + void *bitem = bucket_item(bucket); + if (bucket->hash == hash) { + memcpy(map->spare, bitem, map->elsize); + bucket->dib = 0; + while (1) { + struct bucket *prev = bucket; + i = (i + 1) & map->mask; + bucket = bucket_at(map, i); + if (bucket->dib <= 1) { + prev->dib = 0; + break; + } + memcpy(prev, bucket, map->bucketsz); + prev->dib--; + } + map->count--; + if (map->nbuckets > map->cap && + map->count <= map->shrinkat) { + resize(map, map->nbuckets / 2); + } + return map->spare; + } + i = (i + 1) & map->mask; + } +} + +size_t hashmap_count(struct hashmap *map) +{ + return map->count; +} + +void hashmap_free(struct hashmap *map) +{ + if (!map) + return; + free_elements(map); + free(map->buckets); + free(map); +} + +bool hashmap_oom(struct hashmap *map) +{ + return map->oom; +} + +bool hashmap_scan(struct hashmap *map, bool (*iter)(void *item)) +{ + for (size_t i = 0; i < map->nbuckets; i++) { + struct bucket *bucket = bucket_at(map, i); + if (bucket->dib && !iter(bucket_item(bucket))) { + return false; + } + } + return true; +} + +bool hashmap_iter(struct hashmap *map, size_t *i, void **item) +{ + struct bucket *bucket; + do { + if (*i >= map->nbuckets) + return false; + bucket = bucket_at(map, *i); + (*i)++; + } while (!bucket->dib); + *item = bucket_item(bucket); + return true; +} diff --git a/src/lib/list.c b/src/lib/list.c new file mode 100644 index 0000000..db7c5a6 --- /dev/null +++ b/src/lib/list.c @@ -0,0 +1,32 @@ +// Copyright (c) 2023, Marvin Borner +// SPDX-License-Identifier: MIT + +#include + +#include +#include + +static struct list *list_new(void) +{ + struct list *list = malloc(sizeof(*list)); + if (!list) + fatal("out of memory!\n"); + return list; +} + +struct list *list_add(struct list *list, void *data) +{ + struct list *new = list_new(); + new->data = data; + new->next = list; + return new; +} + +void list_free(struct list *list) +{ + while (list) { + struct list *next = list->next; + free(list); + list = next; + } +} diff --git a/src/lib/queue.c b/src/lib/queue.c new file mode 100644 index 0000000..f039257 --- /dev/null +++ b/src/lib/queue.c @@ -0,0 +1,61 @@ +// Copyright (c) 2023, Marvin Borner +// SPDX-License-Identifier: MIT + +#include + +#include +#include + +struct queue *queue_new(void) +{ + struct queue *queue = malloc(sizeof(*queue)); + if (!queue) + fatal("out of memory!\n"); + queue->head = 0; + queue->tail = 0; + return queue; +} + +void queue_free(struct queue *queue) +{ + while (queue->head) { + struct queue_node *node = queue->head; + queue->head = node->next; + free(node); + } + free(queue); +} + +void queue_push(struct queue *queue, void *data) +{ + struct queue_node *node = malloc(sizeof(*node)); + if (!node) + fatal("out of memory!\n"); + node->data = data; + node->next = 0; + if (queue->tail) { + queue->tail->next = node; + queue->tail = node; + } else { + queue->head = node; + queue->tail = node; + } +} + +void *queue_pop(struct queue *queue) +{ + if (!queue->head) + return 0; + struct queue_node *node = queue->head; + queue->head = node->next; + if (!queue->head) + queue->tail = 0; + void *data = node->data; + free(node); + return data; +} + +int queue_empty(struct queue *queue) +{ + return !queue->head; +} diff --git a/src/main.c b/src/main.c index de74288..2403e47 100644 --- a/src/main.c +++ b/src/main.c @@ -6,6 +6,8 @@ #include #include +#include +#include #include #include @@ -47,14 +49,14 @@ int main(int argc, char *argv[]) fatal("usage: %s \n", argc ? argv[0] : "sharing"); char *term = read_path(argv[1]); + map_initialize(); char *orig_term = term; - struct term *parsed = parse_blc(&term); + parse_blc(&term); free(orig_term); - term_print(parsed); - fprintf(stderr, "\n"); + blind_check(); - term_free(parsed); + map_destroy(); return 0; } diff --git a/src/map.c b/src/map.c new file mode 100644 index 0000000..f71b794 --- /dev/null +++ b/src/map.c @@ -0,0 +1,59 @@ +// Copyright (c) 2023, Marvin Borner +// SPDX-License-Identifier: MIT + +#include +#include + +#include +#include +#include +#include + +static struct hashmap *all_terms; + +static void hashmap_free_term(void *item) +{ + struct term *term = *(struct term **)item; + list_free(term->parents); + list_free(term->neighbours); + queue_free(term->queue); + free(term); +} + +struct term *map_get(hash_t hash) +{ + struct term **handle = hashmap_get(all_terms, hash); + if (!handle) + return 0; + return *handle; +} + +void map_set(struct term *term, hash_t hash) +{ + hashmap_set(all_terms, &term, hash); +} + +void map_initialize(void) +{ + all_terms = hashmap_new(sizeof(struct term *), 0, hashmap_free_term); +} + +void map_delete(struct term *term) +{ + hashmap_delete(all_terms, term->hash); +} + +void map_destroy(void) +{ + hashmap_free(all_terms); +} + +void map_foreach(void (*func)(struct term *)) +{ + size_t iter = 0; + void *iter_val; + while (hashmap_iter(all_terms, &iter, &iter_val)) { + struct term *term = *(struct term **)iter_val; + func(term); + } +} diff --git a/src/parse.c b/src/parse.c index 18dfffe..2ef3817 100644 --- a/src/parse.c +++ b/src/parse.c @@ -3,33 +3,85 @@ #include +#include #include #include +#include -struct term *parse_blc(char **term) +static struct term_handle abs_blc(char **term) +{ + term_type_t res_type = ABS; + struct term_handle inner = parse_blc(term); + hash_t res = hash((uint8_t *)&res_type, sizeof(res_type), inner.hash); + + struct term *res_term; + if (!(res_term = map_get(res))) { + res_term = term_new(res_type, res); + res_term->u.abs.term = inner.term; + map_set(res_term, res); + } + + res_term->u.abs.term->parents = + list_add(res_term->u.abs.term->parents, res_term); + return (struct term_handle){ .term = res_term, .hash = res }; +} + +static struct term_handle app_blc(char **term) +{ + term_type_t res_type = APP; + struct term_handle lhs = parse_blc(term); + struct term_handle rhs = parse_blc(term); + + hash_t res = hash((uint8_t *)&res_type, sizeof(res_type), lhs.hash); + res = hash((uint8_t *)&res, sizeof(res), rhs.hash); + + struct term *res_term; + if (!(res_term = map_get(res))) { + res_term = term_new(res_type, res); + res_term->u.app.lhs = lhs.term; + res_term->u.app.rhs = rhs.term; + map_set(res_term, res); + } + + res_term->u.app.lhs->parents = + list_add(res_term->u.app.lhs->parents, res_term); + res_term->u.app.rhs->parents = + list_add(res_term->u.app.rhs->parents, res_term); + return (struct term_handle){ .term = res_term, .hash = res }; +} + +static struct term_handle var_blc(int index) +{ + term_type_t res_type = VAR; + hash_t res = hash((uint8_t *)&res_type, sizeof(res_type), index); + + struct term *res_term; + if (!(res_term = map_get(res))) { + res_term = term_new(res_type, res); + res_term->u.var.index = index; + map_set(res_term, res); + } + + return (struct term_handle){ .term = res_term, .hash = res }; +} + +struct term_handle parse_blc(char **term) { if (!**term) { fatal("invalid parsing state!\n"); } else if (**term == '0' && *(*term + 1) == '0') { (*term) += 2; - struct term *new = term_new(ABS); - new->u.abs.term = parse_blc(term); - return new; + return abs_blc(term); } else if (**term == '0' && *(*term + 1) == '1') { (*term) += 2; - struct term *new = term_new(APP); - new->u.app.lhs = parse_blc(term); - new->u.app.rhs = parse_blc(term); - return new; + return app_blc(term); } else if (**term == '1') { const char *cur = *term; while (**term == '1') (*term)++; int index = *term - cur - 1; (*term)++; - struct term *new = term_new(VAR); - new->u.var.index = index; - return new; + return var_blc(index); } else { (*term)++; return parse_blc(term); diff --git a/src/queue.c b/src/queue.c deleted file mode 100644 index 5f30717..0000000 --- a/src/queue.c +++ /dev/null @@ -1,56 +0,0 @@ -// Copyright (c) 2023, Marvin Borner -// SPDX-License-Identifier: MIT - -#include - -#include -#include - -struct queue *queue_new(void) -{ - struct queue *queue = malloc(sizeof(*queue)); - if (!queue) - fatal("out of memory!\n"); - queue->head = 0; - queue->tail = 0; - return queue; -} - -void queue_free(struct queue *queue) -{ - while (queue->head) { - struct queue_node *node = queue->head; - queue->head = node->next; - free(node); - } - free(queue); -} - -void queue_push(struct queue *queue, void *data) -{ - struct queue_node *node = malloc(sizeof(*node)); - if (!node) - fatal("out of memory!\n"); - node->data = data; - node->next = 0; - if (queue->tail) { - queue->tail->next = node; - queue->tail = node; - } else { - queue->head = node; - queue->tail = node; - } -} - -void *queue_pop(struct queue *queue) -{ - if (!queue->head) - return 0; - struct queue_node *node = queue->head; - queue->head = node->next; - if (!queue->head) - queue->tail = 0; - void *data = node->data; - free(node); - return data; -} diff --git a/src/sharing.c b/src/sharing.c new file mode 100644 index 0000000..eda3fd3 --- /dev/null +++ b/src/sharing.c @@ -0,0 +1,87 @@ +// Copyright (c) 2023, Marvin Borner +// SPDX-License-Identifier: MIT + +#include + +#include +#include +#include +#include + +// Procedure EnqueueAndPropagate() +static void enqueue_and_propagate(struct term *neighbour, struct term *term) +{ + if (neighbour->type == ABS && term->type == ABS) { + // m' ~ c' + neighbour->u.abs.term->neighbours = list_add( + neighbour->u.abs.term->neighbours, term->u.abs.term); + term->u.abs.term->neighbours = list_add( + term->u.abs.term->neighbours, neighbour->u.abs.term); + } else if (neighbour->type == APP && term->type == APP) { + // m1 ~ c1 + neighbour->u.app.lhs->neighbours = list_add( + neighbour->u.app.lhs->neighbours, term->u.app.lhs); + term->u.app.lhs->neighbours = list_add( + term->u.app.lhs->neighbours, neighbour->u.app.lhs); + + // m2 ~ c2 + neighbour->u.app.rhs->neighbours = list_add( + neighbour->u.app.rhs->neighbours, term->u.app.rhs); + term->u.app.rhs->neighbours = list_add( + term->u.app.rhs->neighbours, neighbour->u.app.rhs); + } else if (neighbour->type == VAR && term->type == VAR) { + } else { + fatal("huh3?\n"); + } + neighbour->canonic = term; + queue_push(term->queue, neighbour); +} + +// Procedure BuildEquivalenceClass() +static void build_equivalence_class(struct term *term) +{ + term->canonic = term; + term->building = 1; + term->queue = queue_new(); + queue_push(term->queue, term); + + while (!queue_empty(term->queue)) { + struct term *cur = queue_pop(term->queue); + + struct list *iterator = cur->parents; + while (iterator) { + struct term *parent = iterator->data; + if (!parent->canonic) { + build_equivalence_class(parent); + } else if (parent->canonic->building) { + fatal("huh?\n"); + } + iterator = iterator->next; + } + + iterator = cur->neighbours; + while (iterator) { + struct term *neighbour = iterator->data; + if (!neighbour->canonic) { + enqueue_and_propagate(neighbour, term); + } else if (neighbour->canonic != term) { + fatal("huh2?\n"); + } + } + } + + term->building = 0; +} + +static void iter_callback(struct term *term) +{ + if (term->canonic) + return; + build_equivalence_class(term); +} + +// Procedure BlindCheck() +void blind_check(void) +{ + map_foreach(iter_callback); +} diff --git a/src/term.c b/src/term.c index aa7c17b..a301aa3 100644 --- a/src/term.c +++ b/src/term.c @@ -8,12 +8,13 @@ #include #include -struct term *term_new(term_type_t type) +struct term *term_new(term_type_t type, hash_t hash) { - struct term *term = malloc(sizeof(*term)); + struct term *term = calloc(sizeof(*term), 1); if (!term) fatal("out of memory!\n"); term->type = type; + term->hash = hash; return term; } -- cgit v1.2.3