loa

commit ccde1ec5e431ac13cb0028fa8a9510a41cff333e
Author: Juan F. Meleiro <juan@juanmeleiro.mat.br>
Date:   Sat,  6 Jan 2024 13:32:28 -0300

Add first working mockup of a LoA VM

Diffstat:
A
vm.c
 | 
214
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

1 file changed, 214 insertions(+), 0 deletions(-)
diff --git a/vm.c b/vm.c
@@ -0,0 +1,214 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <assert.h>
+
+typedef size_t address;
+
+typedef enum {
+	SYMBOL,
+	JUDGMENT_FORM,
+	ASSUMPTION,
+	TERM
+} ref_t;
+
+char
+type_variable(ref_t t)
+{
+	char *cs = "SJAT";
+	return cs[t];
+}
+
+struct ref {
+	ref_t type;
+	address addr;
+	int resolved;
+};
+
+struct symbol {
+	char *name;
+};
+
+struct term {
+	address head;
+	size_t nargs;
+	address subterms;
+};
+
+struct state {
+
+	size_t nrefs;
+	size_t crefs;
+	struct ref *refs;
+
+	size_t nsymbols;
+	size_t csymbols;
+	struct symbol *symbols;
+
+	size_t nterms;
+	size_t cterms;
+	struct term *terms;
+
+};
+
+struct
+state new_state(void)
+{
+	struct state s = {
+		.nrefs = 0,
+		.crefs = 1,
+		.refs = malloc(sizeof(struct ref)),
+		.nsymbols = 0,
+		.csymbols = 1,
+		.symbols = malloc(sizeof(struct symbol)),
+		.nterms = 0,
+		.cterms = 1,
+		.terms = malloc(sizeof(struct term))
+	};
+	return s;
+}
+
+#define cap(st, t) st -> c ## t ## s
+#define num(st, t) st -> n ## t ## s
+#define vec(st, t) st -> t ## s
+#define push(s, t, x) (((cap(s,t) == num(s,t)) ? (vec(s,t) = realloc(vec(s,t), (cap(s,t) *= 2)*sizeof(struct t))) : NULL), (vec(s,t)[num(s,t)++] = x), (num(s,t)-1))
+
+address
+allocate_refs(struct state *st, size_t n, ref_t type)
+{
+	address start = st->nrefs;
+
+	struct ref cur = {
+		.type = type,
+		.resolved = 0
+	};
+
+	for (size_t i = 0; i < n; i++)
+		(void) push(st, ref, cur);
+
+	return start;
+}
+
+address
+create_term(struct state *st, address symbol, size_t nargs)
+{
+	address cur;
+
+	struct term t = {
+		.head = symbol,
+		.nargs = nargs,
+		.subterms = allocate_refs(st, nargs, TERM)
+	};
+
+	cur = push(st, term, t);
+
+	return cur;
+}
+
+address
+create_symbol(struct state *st, char *name)
+{
+	struct symbol sym = { .name = name };
+	return push(st, symbol, sym);
+}
+
+#define resolve(state, type, addr) state -> type ## s [addr]
+
+void
+assign(struct state *st, address ref, address dest)
+{
+	st->refs[ref].addr = dest;
+	st->refs[ref].resolved = 1;
+}
+
+void print_term(FILE *f, struct state *st, struct term t);
+
+void
+print_ref(FILE *f, struct state *st, address ref)
+{
+	struct ref cur = st->refs[ref];
+	if (cur.resolved) {
+		switch (cur.type) {
+			case TERM:
+				print_term(f, st, resolve(st, term, cur.addr));
+			break;
+			case SYMBOL:
+			break;
+			case JUDGMENT_FORM:
+			break;
+			case ASSUMPTION:
+			break;
+		}
+	} else {
+		char v = type_variable(cur.type);
+		fprintf(f, "%c%ld", v, ref);
+	}
+}
+
+void
+print_symbol(FILE *f, struct state *st, struct symbol s)
+{
+	(void)st;
+	fprintf(f, "%s", s.name);
+}
+
+void
+print_term(FILE *f, struct state *st, struct term t)
+{
+	if (t.nargs == 0) {
+		print_symbol(f, st, resolve(st, symbol, t.head));
+	} else {
+		fputc('(', f);
+		print_symbol(f, st, resolve(st, symbol, t.head));
+		for (size_t i = 0; i < t.nargs; i++) {
+			fputc(' ', f);
+			print_ref(f, st, t.subterms + i);
+		}
+		fputc(')', f);
+	}
+}
+
+void
+print_state(FILE *f, struct state *st)
+{
+	size_t i;
+
+	fprintf(f, "----------\n");
+
+	fprintf(f, "SYMBOLS\n");
+	for (i = 0; i < st->nsymbols; i++) {
+		fprintf(f, "%ld: ", i);
+		print_symbol(f, st, resolve(st, symbol, i));
+		fputc('\n', f);
+	}
+
+	fprintf(f, "\nTERMS\n");
+	for (i = 0; i < st->nterms; i++) {
+		fprintf(f, "%ld: ", i);
+		print_term(f, st, st->terms[i]);
+		fputc('\n', f);
+	}
+
+	fprintf(f, "\nREFS (%ld/%ld)\n", st->nrefs, st->crefs);
+	for (i = 0; i < st->nrefs; i++) {
+		fprintf(f, "%ld: ", i);
+		fprintf(f, "%c -> ", type_variable(st->refs[i].type));
+		if (st->refs[i].resolved)
+			fprintf(f, "%ld", st->refs[i].addr);
+		else
+			fputs("?\n", f);
+		fputc('\n', f);
+	}
+}
+
+int main(void) {
+	struct state state = new_state();
+	address cur, cur2;
+
+	cur = create_symbol(&state, "first");
+	cur2 = create_symbol(&state, "second");
+	cur = create_term(&state, cur, 1);
+	cur2 = create_term(&state, cur2, 0);
+	assign(&state, 0, 1);
+	print_state(stdout, &state);
+	return 0;
+}