loa

vm.c (5640B)

---

 #include <stdio.h>
 #include <stdlib.h>
 #include <assert.h>
 
 #include "vm.h"
 #include "formating.h"
 #include "tactics.h"
 
 /* OBJECT CREATION */
 
 struct
 state new_state(void)
 {
 	struct state s;
 	init(s, attitude);
 	s.focus = NULL;
 	s.cursor = NULL;
 	s.head = NULL;
 	return s;
 }
 
 struct term*
 create_term(struct symbol *head, size_t nargs)
 {
 	struct term *t = malloc(sizeof(struct term));
 	t->head = head;
 	t->nargs = nargs;
 	t->subterms = malloc(sizeof(struct term*) * nargs);
 	for (size_t i = 0; i < nargs; i++)
 		t->subterms[i] = NULL;
 	return t;
 }
 
 struct attitude*
 create_attitude(struct symbol *marker, size_t nvars, size_t npres)
 {
 	struct attitude *a = malloc(sizeof(struct attitude));
 	a->marker = marker;
 	a->nvars = nvars;
 	a->vars = calloc(nvars, sizeof(struct symbol*));
 	a->npres = npres;
 	a->pressupositions = calloc(npres, sizeof(struct term*));
 	return a;
 }
 
 struct symbol*
 create_symbol(char *name)
 {
 	struct symbol *sym = malloc(sizeof(struct symbol));
 	sym->name = name;
 	return sym;
 }
 
 /*
 struct assumption*
 create_assumption(struct state *st, struct symbol *name, struct symbol *marker, size_t nvars, size_t nsub)
 {
 	struct attitude *att = lookup_attitude(st, marker);
 	assert(att != NULL);
 	struct assumption a = {
 		.name = name,
 		.marker = marker,
 		.nvars = nvars,
 		.nsub = nsub,
 		.vars = malloc(nvars * sizeof(struct symbol)),
 		.sub = malloc(nsub * sizeof(struct assumption)),
 		.judgment = malloc(1 * sizeof(struct term)),
 		.nproofs = att->npres,
 		.proofs = malloc(att->npres * sizeof(struct proof))
 	};
 
 	return push(st, assumption, a);
 }
 */
 
 /*
 struct proof*
 create_proof(struct state *st, struct term *thesis)
 {
 	struct proof p = {
 		.thesis = thesis,
 		.argument = malloc(1 * sizeof(struct symbol))
 	};
 
 	return push(st, proof, p);
 }
 */
 
 /* GOAL MECHANICS */
 
 struct goal*
 create_goal(ref_t type, void *target)
 {
 	struct goal *new = malloc(sizeof(struct goal));
 	new->next = NULL;
 	new->parent = NULL;
 	new->sub = NULL;
 	new->type = type;
 	new->target = target;
 	return new;
 }
 
 void
 add_top_goal(struct state *st, ref_t type)
 {
 	void *addr;
 	assert(type == ATTITUDE);
 	assert(!st->focus);
 	if (type == ATTITUDE) {
 		addr = reserve(st, attitude);
 	}
 	st->focus = create_goal(type, addr);
 }
 
 void
 add_subgoal(struct state *st, ref_t type, void *target)
 {
 	assert(st->focus);
 	struct goal *new = create_goal(type, target);
 
 	if (st->cursor) {
 		/* There are non-commited already subgoals */
 		st->cursor->next = new;
 		st->cursor = new;
 	} else {
 		/* Creating first subgoal */
 		st->cursor = new;
 		if (st->focus) st->focus->sub = new;
 		st->next = new;
 	}
 }
 
 void
 commit(struct state *st)
 {
 	assert(st->focus);
 	if (st->focus->sub) {
 		st->focus = st->focus->sub;
 	} else if (st->focus->next) {
 		st->focus = st->focus->next;
 	} else if (st->focus->parent) {
 		/* Do resolution */
 		st->focus = st->focus->parent;
 	} else {
 		st->focus = NULL;
 	}
 	st->cursor = NULL;
 }
 
 void
 solve(struct state *st, void *dest)
 {
 	assert(st->focus);
 	switch (st->focus->type) {
 		case TERM:
 			*st->focus->target = (struct term*)dest;
 		break;
 		case SYMBOL:
 			*st->focus->target = (struct symbol*)dest;
 		break;
 		case ATTITUDE:
 			*st->focus->target = (struct attitude*)dest;
 		break;
 		case PROOF:
 			*st->focus->target = (struct proof*)dest;
 		break;
 		case ASSUMPTION:
 			*st->focus->target = (struct assumption*)dest;
 		break;
 	}
 }
 
 struct symbol
 *read_symbol(struct tape *program)
 {
 	assert(program->code[program->cur].code == SYM);
 	return program->code[program->cur++].sym;
 }
 
 unsigned int
 read_number(struct tape *program)
 {
 	assert(program->code[program->cur].code == NUM);
 	return program->code[program->cur++].num;
 }
 
 ref_t
 read_top(struct tape *program)
 {
 	assert(program->code[program->cur].code == TOP);
 	return program->code[program->cur++].type;
 }
 
 void
 step(struct state *st, struct tape *program)
 {
 	unsigned int n, m;
 	struct symbol *sym; // , *mk;
 
 	if (!st->focus) {
 		/* No active goal. Expect goal creation */
 		ref_t ty = read_top(program);
 		add_top_goal(st, ty);
 	} else {
 		switch (st->focus->type) {
 			case SYMBOL:
 				sym = read_symbol(program);
 				tactic_symbol(st, sym);
 			break;
 			case ATTITUDE:
 				sym = read_symbol(program);
 				n = read_number(program);
 				m = read_number(program);
 				tactic_attitude(st, sym, n, m);
 			break;
 			case ASSUMPTION:
 				// sym = read_symbol(program);
 				// mk = read_symbol(program);
 				// n = read_number(program);
 				// m = read_number(program);
 				// tactic_assumption(st, sym, mk, n, m);
 			break;
 			case TERM:
 				sym = read_symbol(program);
 				n = read_number(program);
 				tactic_term(st, sym, n);
 			break;
 			case PROOF:
 				exit(1);
 			break;
 		}
 	}
 }
 
 void
 run(struct state *st, struct tape *program)
 {
 	while (program->code[program->cur].code != HLT)
 		step(st, program);
 }
 
 int
 main(void) {
 	struct state s = new_state();
 
 	struct symbol *wft   = create_symbol("wft");
 	struct symbol *colon = create_symbol(":");
 	struct symbol *var_a = create_symbol("a");
 	struct symbol *var_b = create_symbol("b");
 	// struct symbol *type  = create_symbol("type");
 
 	struct op code[] = {
 		{ TOP, { .type = ATTITUDE } },
 
 		{ SYM, { .sym = wft } },
 		{ NUM, { .num = 1 } },
 		{ NUM, { .num = 0 } },
 
 		{ SYM, { .sym = var_a } },
 
 
 		{ TOP, { .type = ATTITUDE } },
 
 		{ SYM, { .sym = colon } },
 		{ NUM, { .num = 2 } },
 		{ NUM, { .num = 1 } },
 
 		{ SYM, { .sym = var_a } },
 
 		{ SYM, { .sym = var_b } },
 
 		{ SYM, { .sym = wft } },
 		{ NUM, { .num = 1 } },
 
 		{ SYM, { .sym = var_b } },
 		{ NUM, { .num = 0 } },
 
 		{ HLT , { 0 } }
 	};
 
 	struct tape t = {
 		.code = code,
 		.cur = 0
 	};
 
 	run(&s, &t);
 	print_state(stdout, &s);
 
 	return 0;
 }