commit 13a9ecc93ef4334db0fca4aa33e38b2fa759ebfc
parent 067e31f554978b45b84448433b18dc7ba98b6b0e
Author: Juan F. Meleiro <juan@juanmeleiro.mat.br>
Date: Thu, 18 Jan 2024 18:05:34 -0300
Add somewhat proper error handling to VM
Diffstat:
6 files changed, 219 insertions(+), 47 deletions(-)
diff --git a/coding/formating.c b/coding/formating.c
@@ -1,5 +1,6 @@
#include <stdio.h>
#include <stdlib.h>
+#include <assert.h>
#include "formating.h"
@@ -124,3 +125,114 @@ print_state(FILE *f, struct state *st)
}
}
+void
+print_tape(FILE *f, struct tape *t)
+{
+ size_t c = 0;
+ struct op op;
+ fputs("TAPE\n", f);
+ do {
+ if (t->cur == c)
+ fputs("> ", f);
+ else
+ fputs(" ", f);
+
+ op = t->code[c];
+ switch (op.code) {
+ case TOP:
+ fputs("TOP ", f);
+ fputc(type_variable(op.type), f);
+ fputc('\n', f);
+ break;
+ case SYM:
+ fprintf(f, "SYM %s\n", op.sym->name);
+ break;
+ case NUM:
+ fprintf(f, "NUM %d\n", op.num);
+ break;
+ case HLT:
+ fputs("HLT\n", f);
+ break;
+ }
+
+ c++;
+ } while(op.code != HLT);
+}
+
+void
+print_opcode(FILE *f, enum opcode code)
+{
+ switch(code) {
+ case TOP:
+ fputs("TOP", f);
+ break;
+ case SYM:
+ fputs("SYM", f);
+ break;
+ case NUM:
+ fputs("NUM", f);
+ break;
+ case HLT:
+ fputs("HLT", f);
+ break;
+ }
+}
+
+void
+print_error(FILE *f, struct vm *m)
+{
+ struct tape *t = m->tape;
+
+ switch (m->err) {
+ case OK:
+ return;
+ break;
+ case NONEXISTENT_ATTITUDE:
+ fputs("No attitude with name '", f);
+ print_symbol(f, t->code[t->cur].sym);
+ fputs("'\n", f);
+ break;
+ case INVALID_TOP_GOAL_TYPE:
+ fputs("Invalid top goal type '", f);
+ print_symbol(f, t->code[t->cur].sym);
+ fputs("'\n", f);
+ break;
+ case ADDING_TOP_GOAL_WHEN_FOCUS:
+ fputs("Tried creating a top goal while focused\n", f);
+ break;
+ case ADDING_SUBGOAL_WITHOUT_FOCUS:
+ fputs("Tried adding a subgoal while unfocused\n", f);
+ break;
+ case COMMITING_WITHOUT_FOCUS:
+ fputs("Tried commiting while unfocused\n", f);
+ break;
+ case SOLVING_WITHOUT_FOCUS:
+ fputs("Tried solving while unfocused\n", f);
+ break;
+ case EXPECTED_SYMBOL:
+ fputs("Expected a symbol, but found ", f);
+ print_opcode(f, t->code[t->cur].code);
+ fputc('\n', f);
+ break;
+ case EXPECTED_NUMBER:
+ fputs("Expected a number, but found ", f);
+ print_opcode(f, t->code[t->cur].code);
+ fputc('\n', f);
+ break;
+ case EXPECTED_TOP:
+ fputs("Expected a goal creation, but found ", f);
+ print_opcode(f, t->code[t->cur].code);
+ fputc('\n', f);
+ break;
+ }
+}
+
+void
+print_machine(FILE *f, struct vm *m)
+{
+ fputs("VM\n", f);
+ print_error(f, m);
+ print_state(f, m->state);
+ fputc('\n', f);
+ print_tape(f, m->tape);
+}
diff --git a/coding/formating.h b/coding/formating.h
@@ -10,3 +10,4 @@ void print_goal(FILE *f, struct goal *g, unsigned int level);
void print_attitude(FILE *f, struct state *st, struct attitude *a);
void print_assumption(FILE *f, struct state *st, struct assumption a);
void print_proof(FILE *f, struct state *st, struct proof p);
+void print_machine(FILE *f, struct vm *m);
diff --git a/coding/tactics.c b/coding/tactics.c
@@ -1,6 +1,6 @@
#include "tactics.h"
-void
+res_t
tactic_term(struct state *st, struct symbol *head, size_t arity)
{
assert(!st->focus || st->focus->type == TERM);
@@ -14,9 +14,11 @@ tactic_term(struct state *st, struct symbol *head, size_t arity)
}
commit(st);
+
+ return OK;
}
-void
+res_t
tactic_attitude(struct state *st, struct symbol *marker, size_t nvars, size_t npres)
{
assert(st->focus && st->focus->type == ATTITUDE);
@@ -31,14 +33,17 @@ tactic_attitude(struct state *st, struct symbol *marker, size_t nvars, size_t np
solve(st, a);
commit(st);
+
+ return OK;
}
-void
+res_t
tactic_symbol(struct state *st, struct symbol *s)
{
assert(st->focus && st->focus->type == SYMBOL);
solve(st, s);
commit(st);
+ return OK;
}
// void
diff --git a/coding/tactics.h b/coding/tactics.h
@@ -23,9 +23,9 @@
// };
//
// void tactic(struct state *st, struct tactic_args);
-void tactic_term(struct state *st, struct symbol *head, size_t arity);
-void tactic_symbol(struct state *st, struct symbol *s);
-void tactic_attitude(struct state *st, struct symbol *marker, size_t nvars, size_t npres);
-void tactic_assumption(struct state *st, struct symbol *name, struct symbol *marker, size_t nvars, size_t nsub);
-void tactic_proof(struct state *st, struct term *thesis);
+res_t tactic_term(struct state *st, struct symbol *head, size_t arity);
+res_t tactic_symbol(struct state *st, struct symbol *s);
+res_t tactic_attitude(struct state *st, struct symbol *marker, size_t nvars, size_t npres);
+res_t tactic_assumption(struct state *st, struct symbol *name, struct symbol *marker, size_t nvars, size_t nsub);
+res_t tactic_proof(struct state *st, struct term *thesis);
diff --git a/coding/vm.c b/coding/vm.c
@@ -16,6 +16,7 @@ state new_state(void)
s.focus = NULL;
s.cursor = NULL;
s.head = NULL;
+ s.err = OK;
return s;
}
@@ -104,8 +105,11 @@ void
add_top_goal(struct state *st, ref_t type)
{
void *addr;
- assert(type == ATTITUDE);
- assert(!st->focus);
+
+ check_ok(st);
+ check(st, type == ATTITUDE, INVALID_TOP_GOAL_TYPE);
+ check(st, !st->focus, ADDING_TOP_GOAL_WHEN_FOCUS);
+
if (type == ATTITUDE) {
addr = reserve(st, attitude);
}
@@ -115,7 +119,8 @@ add_top_goal(struct state *st, ref_t type)
void
add_subgoal(struct state *st, ref_t type, void *target)
{
- assert(st->focus);
+ check_ok(st);
+ check(st, st->focus, ADDING_SUBGOAL_WITHOUT_FOCUS);
struct goal *new = create_goal(type, target);
if (st->cursor) {
@@ -133,7 +138,9 @@ add_subgoal(struct state *st, ref_t type, void *target)
void
commit(struct state *st)
{
- assert(st->focus);
+ check_ok(st);
+ check(st, st->focus, COMMITING_WITHOUT_FOCUS);
+
if (st->focus->sub) {
st->focus = st->focus->sub;
} else if (st->focus->next) {
@@ -150,7 +157,8 @@ commit(struct state *st)
void
solve(struct state *st, void *dest)
{
- assert(st->focus);
+ check_ok(st);
+ check(st, st->focus, SOLVING_WITHOUT_FOCUS);
switch (st->focus->type) {
case TERM:
*st->focus->target = (struct term*)dest;
@@ -170,60 +178,74 @@ solve(struct state *st, void *dest)
}
}
-struct symbol
-*read_symbol(struct tape *program)
+struct symbol*
+read_symbol(struct vm *m)
{
- assert(program->code[program->cur].code == SYM);
- return program->code[program->cur++].sym;
+ if (m->tape->code[m->tape->cur].code == SYM) {
+ return m->tape->code[m->tape->cur++].sym;
+ } else {
+ m->err = EXPECTED_SYMBOL;
+ return NULL;
+ }
}
unsigned int
-read_number(struct tape *program)
+read_number(struct vm *m)
{
- assert(program->code[program->cur].code == NUM);
- return program->code[program->cur++].num;
+ if (m->tape->code[m->tape->cur].code == NUM) {
+ return m->tape->code[m->tape->cur++].num;
+ } else {
+ m->err = EXPECTED_NUMBER;
+ return 0;
+ }
}
ref_t
-read_top(struct tape *program)
+read_top(struct vm *m)
{
- assert(program->code[program->cur].code == TOP);
- return program->code[program->cur++].type;
+ if (m->tape->code[m->tape->cur].code == TOP) {
+ return m->tape->code[m->tape->cur++].type;
+ } else {
+ m->err = EXPECTED_TOP;
+ return 0;
+ }
}
void
-step(struct state *st, struct tape *program)
+step(struct vm *m)
{
- unsigned int n, m;
+ unsigned int n, k;
struct symbol *sym; // , *mk;
- if (!st->focus) {
+ check_ok(m);
+
+ if (!m->state->focus) {
/* No active goal. Expect goal creation */
- ref_t ty = read_top(program);
- add_top_goal(st, ty);
+ ref_t ty = read_top(m);
+ add_top_goal(m->state, ty);
} else {
- switch (st->focus->type) {
+ switch (m->state->focus->type) {
case SYMBOL:
- sym = read_symbol(program);
- tactic_symbol(st, sym);
+ sym = read_symbol(m);
+ tactic_symbol(m->state, sym);
break;
case ATTITUDE:
- sym = read_symbol(program);
- n = read_number(program);
- m = read_number(program);
- tactic_attitude(st, sym, n, m);
+ sym = read_symbol(m);
+ n = read_number(m);
+ k = read_number(m);
+ tactic_attitude(m->state, sym, n, k);
break;
case ASSUMPTION:
- // sym = read_symbol(program);
- // mk = read_symbol(program);
- // n = read_number(program);
- // m = read_number(program);
+ // sym = read_symbol(m);
+ // mk = read_symbol(m);
+ // n = read_number(m);
+ // m = read_number(m);
// tactic_assumption(st, sym, mk, n, m);
break;
case TERM:
- sym = read_symbol(program);
- n = read_number(program);
- tactic_term(st, sym, n);
+ sym = read_symbol(m);
+ n = read_number(m);
+ tactic_term(m->state, sym, n);
break;
case PROOF:
exit(1);
@@ -233,10 +255,13 @@ step(struct state *st, struct tape *program)
}
void
-run(struct state *st, struct tape *program)
+run(struct vm *m)
{
- while (program->code[program->cur].code != HLT)
- step(st, program);
+ while (
+ m->tape->code[m->tape->cur].code != HLT &&
+ m->err == OK
+ )
+ step(m);
}
int
@@ -283,8 +308,14 @@ main(void) {
.cur = 0
};
- run(&s, &t);
- print_state(stdout, &s);
+ struct vm machine = {
+ .state = &s,
+ .tape = &t
+ };
+
+ run(&machine);
+ print_machine(stdout, &machine);
+ // run(&machine);
return 0;
}
diff --git a/coding/vm.h b/coding/vm.h
@@ -9,6 +9,22 @@ typedef enum {
PROOF,
} ref_t;
+typedef enum {
+ OK,
+ NONEXISTENT_ATTITUDE,
+ INVALID_TOP_GOAL_TYPE,
+ ADDING_TOP_GOAL_WHEN_FOCUS,
+ ADDING_SUBGOAL_WITHOUT_FOCUS,
+ COMMITING_WITHOUT_FOCUS,
+ SOLVING_WITHOUT_FOCUS,
+ EXPECTED_SYMBOL,
+ EXPECTED_NUMBER,
+ EXPECTED_TOP
+} res_t;
+
+#define check_ok(st) if (st->err != OK) return;
+#define check(st, expr, e) if (!(expr)) {st->err = e; return;}
+
struct ref {
ref_t type;
void *addr;
@@ -122,10 +138,17 @@ struct state {
struct goal *cursor;
struct goal *next;
struct assumption *head;
+ res_t err;
list(attitude);
};
+struct vm {
+ struct state *state;
+ struct tape *tape;
+ res_t err;
+};
+
struct state new_state(void);
struct ref *allocate_refs(struct state *st, size_t n, ref_t type);
