From 05f3cde3e7924c9ffcc1937661b3cc290d89c11a Mon Sep 17 00:00:00 2001 From: Marvin Borner Date: Sat, 7 Sep 2024 17:53:27 +0200 Subject: Initial bootstrap --- src/term.c | 65 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 65 insertions(+) create mode 100644 src/term.c (limited to 'src/term.c') diff --git a/src/term.c b/src/term.c new file mode 100644 index 0000000..e68611e --- /dev/null +++ b/src/term.c @@ -0,0 +1,65 @@ +// Copyright (c) 2024, Marvin Borner +// SPDX-License-Identifier: MIT + +#include +#include + +#include +#include +#include + +Term *term_new(TermType type) +{ + struct term *term = malloc(sizeof(*term)); + if (!term) + fatal("out of memory!\n"); + term->type = type; + return term; +} + +void term_free(Term *term) +{ + switch (term->type) { + case ABS: + term_free(term->u.abs.body); + free(term); + break; + case APP: + term_free(term->u.app.lhs); + term_free(term->u.app.rhs); + free(term); + break; + case IDX: + free(term); + break; + default: + fatal("invalid type %d\n", term->type); + } +} + +void term_diff(Term *a, Term *b) +{ + if (a->type != b->type) { + fprintf(stderr, "Term a: "); + print_bruijn(a); + fprintf(stderr, "\nTerm b: "); + print_bruijn(b); + fatal("\ntype mismatch %d %d\n", a->type, b->type); + } + + switch (a->type) { + case ABS: + term_diff(a->u.abs.body, b->u.abs.body); + break; + case APP: + term_diff(a->u.app.lhs, b->u.app.lhs); + term_diff(a->u.app.rhs, b->u.app.rhs); + break; + case IDX: + if (a->u.index != b->u.index) + fatal("var mismatch %d=%d\n", a->u.index, b->u.index); + break; + default: + fatal("invalid type %d\n", a->type); + } +} -- cgit v1.2.3