commit 067e31f554978b45b84448433b18dc7ba98b6b0e
parent a272042d4ccfb321eafadf888d011186be54e423
Author: Juan F. Meleiro <juan@juanmeleiro.mat.br>
Date: Thu, 18 Jan 2024 16:07:27 -0300
Implement a program tape
Diffstat:
| M | coding/build.sh | | | 4 | +++- |
| M | coding/formating.c | | | 168 | +++++++++++++++++++++++++++++-------------------------------------------------- |
| M | coding/formating.h | | | 11 | +++++------ |
| M | coding/tactics.c | | | 75 | ++++++++++++++++++++++++++++++++++++++++----------------------------------- |
| M | coding/tactics.h | | | 49 | +++++++++++++++++++++++++------------------------ |
| M | coding/vm.c | | | 332 | ++++++++++++++++++++++++++++++++++++++++++++++--------------------------------- |
| M | coding/vm.h | | | 122 | +++++++++++++++++++++++++++++++++++++++++++++++-------------------------------- |
7 files changed, 400 insertions(+), 361 deletions(-)
diff --git a/coding/build.sh b/coding/build.sh
@@ -1,3 +1,5 @@
#!/bin/sh
-cc -Wall -Wextra -pedantic -g -o vm *.c && ./vm
+echo '========================================'
+cc -Wall -Wextra -pedantic -Wfatal-errors -g -o vm *.c 2>&1 &&
+[ "$1" = '-r' ] && ./vm 2>&1
diff --git a/coding/formating.c b/coding/formating.c
@@ -4,102 +4,92 @@
#include "formating.h"
void
-print_ref(FILE *f, struct state *st, address ref)
+print_symbol(FILE *f, struct symbol *s)
{
- 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:
- print_symbol(f, st, resolve(st, symbol, cur.addr));
- break;
- case ATTITUDE:
- print_attitude(f, st, resolve(st, attitude, cur.addr));
- break;
- case ASSUMPTION:
- print_assumption(f, st, resolve(st, assumption, cur.addr));
- break;
- case PROOF:
- print_proof(f, st, resolve(st, proof, cur.addr));
- break;
- }
- } else {
- char v = type_variable(cur.type);
- fprintf(f, "%c%ld", v, ref);
- }
+ if (s == NULL)
+ fputc('_', f);
+ else
+ fprintf(f, "%s", s->name);
}
void
-print_symbol(FILE *f, struct state *st, struct symbol s)
+print_term(FILE *f, struct state *st, struct term *t)
{
- (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));
+ if (t == NULL) {
+ fputc('_', f);
} 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);
+ if (t->nargs == 0) {
+ print_symbol(f, t->head);
+ } else {
+ fputc('(', f);
+ print_symbol(f, t->head);
+ for (size_t i = 0; i < t->nargs; i++) {
+ fputc(' ', f);
+ struct term *s = t->subterms[i];
+ if (s)
+ print_term(f, st, s);
+ else
+ fprintf(f, "%p", (void*)(t->subterms + i));
+ }
+ fputc(')', f);
}
- fputc(')', f);
}
}
void
-print_goal(FILE *f, struct state *st, struct goal *g)
+print_goal(FILE *f, struct goal *g, unsigned int level)
{
if (!g) {
fprintf(f, "Nothing to do.");
} else {
- struct ref r = st->refs[g->target];
- fprintf(f, "Build %c at %ld", type_variable(r.type), g->target);
- if (g->state == CLOSED) {
- fprintf(f, " [CLOSED]");
+ for (size_t i = 0; i < level; i++) fputc(' ', f);
+ fprintf(f, "Build %c at %p", type_variable(g->type), (void*)g->target);
+ struct goal *cur = g->sub;
+ while (cur) {
+ print_goal(f, cur, level + 1);
+ cur = cur->next;
}
}
}
+
void
-print_attitude(FILE *f, struct state *st, struct attitude a)
+print_attitude(FILE *f, struct state *st, struct attitude *a)
{
- fputc('(', f);
- print_symbol(f, st, resolve(st, symbol, a.marker));
- for (size_t i = 0; i < a.nvars; i++) {
- fputc(' ', f);
- print_ref(f, st, a.vars + i);
- }
- fputs(")\n", f);
-
- for (size_t i = 0; i < a.npres; i++) {
- fputs(" ", f);
- print_ref(f, st, a.pressupositions + i);
- fputc('\n', f);
+ if (a == NULL) {
+ fprintf(f, "TBD\n");
+ } else {
+ fputc('(', f);
+ print_symbol(f, a->marker);
+ for (size_t i = 0; i < a->nvars; i++) {
+ fputc(' ', f);
+ print_symbol(f, a->vars[i]);
+ }
+ fputs(")\n", f);
+
+ for (size_t i = 0; i < a->npres; i++) {
+ fputs(" ", f);
+ print_term(f, st, a->pressupositions[i]);
+ fputc('\n', f);
+ }
}
}
+/*
void
print_assumption(FILE *f, struct state *st, struct assumption a)
{
- print_symbol(f, st, resolve(st, symbol, a.name));
+ print_symbol(f, *a.name);
fputc('[', f);
for (size_t i = 0; i < a.nvars; i++) {
- print_ref(f, st, a.vars + i);
+ print_symbol(f, a.vars[i]);
}
fputs("]: ", f);
- print_ref(f, st, a.judgment);
+ print_term(f, st, *a.judgment);
fputc('\n', f);
for (size_t i = 0; i < a.nsub; i++) {
fputs(" ", f);
- print_ref(f, st, a.sub + i);
+ print_assumption(f, st, a.sub[i]);
fputc('\n', f);
}
}
@@ -107,65 +97,29 @@ print_assumption(FILE *f, struct state *st, struct assumption a)
void
print_proof(FILE *f, struct state *st, struct proof p)
{
- print_ref(f, st, p.argument);
+ // print_argument(f, st, *p.argument);
fprintf(f, " |- ");
- print_ref(f, st, p.thesis);
+ print_term(f, st, *p.thesis);
fputc('\n', f);
}
+*/
void
print_state(FILE *f, struct state *st)
{
- size_t i;
+ // size_t i;
fprintf(f, "----------\n");
- fprintf(f, "SYMBOLS (%ld/%ld)\n", st->nsymbols, st->csymbols);
- for (i = 0; i < st->nsymbols; i++) {
- if (i > 0) fputs(", ", f);
- fprintf(f, "%ld: '", i);
- print_symbol(f, st, resolve(st, symbol, i));
- fputc('\'', f);
- }
- fputc('\n', f);
-
- fprintf(f, "\nTERMS (%ld/%ld)\n", st->nterms, st->cterms);
- 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("?", f);
- fputc('\n', f);
- }
-
- fprintf(f, "\nATTITUDES (%ld/%ld)\n", st->nattitudes, st->cattitudes);
- for (i = 0; i < st->nattitudes; i++) {
- fprintf(f, "%ld: ", i);
+ fprintf(f, "ATTITUDES (%ld/%ld)\n", st->nattitudes, st->cattitudes);
+ for (size_t i = 0; i < st->nattitudes; i++) {
print_attitude(f, st, st->attitudes[i]);
}
+ fputc('\n', f);
- fprintf(f, "\nASSUMPTIONS (%ld/%ld)\n", st->nassumptions, st->cassumptions);
- for (i = 0; i < st->nassumptions; i++) {
- print_assumption(f, st, st->assumptions[i]);
- }
-
- fprintf(f, "\nPROOFS (%ld/%ld)\n", st->nproofs, st->cproofs);
- for (i = 0; i < st->nproofs; i++) {
- print_proof(f, st, st->proofs[i]);
- }
-
- fprintf(f, "\nGOALS\n");
+ fprintf(f, "GOALS\n");
for (struct goal *cur = st->focus; cur; cur = cur->next) {
- print_goal(f, st, cur);
+ print_goal(f, cur, 0);
fputc('\n', f);
}
}
diff --git a/coding/formating.h b/coding/formating.h
@@ -2,12 +2,11 @@
#define type_variable(t) ("SJATPR"[t])
-void print_term(FILE *f, struct state *st, struct term t);
-void print_ref(FILE *f, struct state *st, address ref);
-void print_symbol(FILE *f, struct state *st, struct symbol s);
-void print_term(FILE *f, struct state *st, struct term t);
+void print_ref(FILE *f, struct state *st, struct ref *ref);
+void print_symbol(FILE *f, struct symbol *s);
+void print_term(FILE *f, struct state *st, struct term *t);
void print_state(FILE *f, struct state *st);
-void print_goal(FILE *f, struct state *st, struct goal *g);
-void print_attitude(FILE *f, struct state *st, struct attitude a);
+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);
diff --git a/coding/tactics.c b/coding/tactics.c
@@ -1,76 +1,81 @@
#include "tactics.h"
void
-tactic_term(struct state *st, address head, size_t arity)
+tactic_term(struct state *st, struct symbol *head, size_t arity)
{
- assert(!st->focus || resolve(st, ref, st->focus->target).type == TERM);
+ assert(!st->focus || st->focus->type == TERM);
- address sol = create_term(st, head, arity);
- struct term t = resolve(st, term, sol);
+ struct term *t = create_term(head, arity);
- if (st->focus) solve(st, sol);
+ if (st->focus) solve(st, t);
for (size_t i = 0; i < arity; i++) {
- add_subgoal(st, t.subterms + i);
+ add_subgoal(st, TERM, t->subterms + i);
}
commit(st);
}
void
-tactic_attitude(struct state *st, address marker, size_t nvars, size_t npres)
+tactic_attitude(struct state *st, struct symbol *marker, size_t nvars, size_t npres)
{
- assert(!st->focus || resolve(st, ref, st->focus->target).type == ATTITUDE);
+ assert(st->focus && st->focus->type == ATTITUDE);
- address sol = create_attitude(st, marker, nvars, npres);
- struct attitude a = resolve(st, attitude, sol);
-
- if (st->focus) solve(st, sol);
+ struct attitude *a = create_attitude(marker, nvars, npres);
for (size_t i = 0; i < nvars; i++)
- add_subgoal(st, a.vars + i);
+ add_subgoal(st, SYMBOL, a->vars + i);
for (size_t i = 0; i < npres; i++)
- add_subgoal(st, a.pressupositions + i);
+ add_subgoal(st, TERM, a->pressupositions + i);
+ solve(st, a);
commit(st);
}
void
-tactic_proof(struct state *st, address thesis)
+tactic_symbol(struct state *st, struct symbol *s)
{
- assert(!st->focus || resolve(st, ref, st->focus->target).type == PROOF);
-
- address sol = create_proof(st, thesis);
- struct proof p = resolve(st, proof, sol);
-
- if (st->focus) solve(st, sol);
-
- add_subgoal(st, p.argument);
-
+ assert(st->focus && st->focus->type == SYMBOL);
+ solve(st, s);
commit(st);
}
-
+
+// void
+// tactic_proof(struct state *st, struct term *thesis)
+// {
+// assert(!st->focus || st->focus->type == PROOF);
+//
+// struct proof *p = create_proof(st, thesis);
+//
+// if (st->focus) solve(st, p);
+//
+// add_subgoal(st, ASSUMPTION, p->argument);
+//
+// commit(st);
+// }
+
+/*
void
-tactic_assumption(struct state *st, address name, address marker, size_t nvars, size_t nsub)
+tactic_assumption(struct state *st, struct symbol *name, struct symbol *marker, size_t nvars, size_t nsub)
{
- assert(!st->focus || resolve(st, ref, st->focus->target).type == ASSUMPTION);
+ assert(!st->focus || st->focus->type == ASSUMPTION);
- address sol = create_assumption(st, name, marker, nvars, nsub);
- struct assumption a = resolve(st, assumption, sol);
+ struct assumption *a = create_assumption(st, name, marker, nvars, nsub);
- if (st->focus) solve(st, sol);
+ if (st->focus) solve(st, a);
for (size_t i = 0; i < nvars; i++)
- add_subgoal(st, a.vars + i);
+ add_subgoal(st, SYMBOL, a->vars + i);
- add_subgoal(st, a.judgment);
+ add_subgoal(st, TERM, a->judgment);
for (size_t i = 0; i < nsub; i++)
- add_subgoal(st, a.sub + i);
+ add_subgoal(st, ASSUMPTION, a->sub + i);
- for (size_t i = 0; i < a.nproofs; i++)
- add_subgoal(st, a.proofs + i);
+ for (size_t i = 0; i < a->nproofs; i++)
+ add_subgoal(st, PROOF, a->proofs + i);
commit(st);
}
+*/
diff --git a/coding/tactics.h b/coding/tactics.h
@@ -3,28 +3,29 @@
#include "vm.h"
-struct term_args {
- address head;
- size_t arity;
-};
-
-struct attitude_args {
- address marker;
- size_t nvars;
- size_t npres;
-};
-
-struct tactic_args {
- ref_t type;
- union {
- struct term_args term;
- struct attitude_args attitude;
- };
-};
-
-void tactic(struct state *st, struct tactic_args);
-void tactic_term(struct state *st, address head, size_t arity);
-void tactic_attitude(struct state *st, address marker, size_t nvars, size_t npres);
-void tactic_assumption(struct state *st, address name, address marker, size_t nvars, size_t nsub);
-void tactic_proof(struct state *st, address thesis);
+// struct term_args {
+// address head;
+// size_t arity;
+// };
+//
+// struct attitude_args {
+// address marker;
+// size_t nvars;
+// size_t npres;
+// };
+//
+// struct tactic_args {
+// ref_t type;
+// union {
+// struct term_args term;
+// struct attitude_args attitude;
+// };
+// };
+//
+// 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);
diff --git a/coding/vm.c b/coding/vm.c
@@ -12,68 +12,48 @@ struct
state new_state(void)
{
struct state s;
- init(s, ref);
- init(s, symbol);
- init(s, term);
init(s, attitude);
- init(s, assumption);
- init(s, proof);
s.focus = NULL;
s.cursor = NULL;
+ s.head = NULL;
return s;
}
-address
-allocate_refs(struct state *st, size_t n, ref_t type)
+struct term*
+create_term(struct symbol *head, size_t nargs)
{
- 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)
-{
- struct term t = {
- .head = symbol,
- .nargs = nargs,
- .subterms = allocate_refs(st, nargs, TERM)
- };
-
- return push(st, term, t);
+ 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;
}
-address
-create_attitude(struct state *st, address marker, size_t nvars, size_t npres)
+struct attitude*
+create_attitude(struct symbol *marker, size_t nvars, size_t npres)
{
- struct attitude a = {
- .marker = marker,
- .nvars = nvars,
- .npres = npres,
- .vars = allocate_refs(st, nvars, SYMBOL),
- .pressupositions = allocate_refs(st, npres, TERM)
- };
-
- return push(st, attitude, a);
+ 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;
}
-address
-create_symbol(struct state *st, char *name)
+struct symbol*
+create_symbol(char *name)
{
- struct symbol sym = { .name = name };
- return push(st, symbol, sym);
+ struct symbol *sym = malloc(sizeof(struct symbol));
+ sym->name = name;
+ return sym;
}
-address
-create_assumption(struct state *st, address name, address marker, size_t nvars, size_t nsub)
+/*
+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);
@@ -82,155 +62,229 @@ create_assumption(struct state *st, address name, address marker, size_t nvars,
.marker = marker,
.nvars = nvars,
.nsub = nsub,
- .vars = allocate_refs(st, nvars, SYMBOL),
- .sub = allocate_refs(st, nsub, ASSUMPTION),
- .judgment = allocate_refs(st, 1, TERM),
+ .vars = malloc(nvars * sizeof(struct symbol)),
+ .sub = malloc(nsub * sizeof(struct assumption)),
+ .judgment = malloc(1 * sizeof(struct term)),
.nproofs = att->npres,
- .proofs = allocate_refs(st, att->npres, PROOF)
+ .proofs = malloc(att->npres * sizeof(struct proof))
};
return push(st, assumption, a);
}
+*/
-address
-create_proof(struct state *st, address thesis)
+/*
+struct proof*
+create_proof(struct state *st, struct term *thesis)
{
struct proof p = {
.thesis = thesis,
- .argument = allocate_refs(st, 1, SYMBOL)
+ .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
-assign(struct state *st, address ref, address dest)
+add_top_goal(struct state *st, ref_t type)
{
- st->refs[ref].addr = dest;
- st->refs[ref].resolved = 1;
+ 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, address target)
+add_subgoal(struct state *st, ref_t type, void *target)
{
- struct goal *g = malloc(sizeof(struct goal));
+ assert(st->focus);
+ struct goal *new = create_goal(type, target);
- if (!st->cursor) {
- // Creating first subgoal
- g->next = st->focus;
- st->focus = g;
- st->cursor = g;
+ if (st->cursor) {
+ /* There are non-commited already subgoals */
+ st->cursor->next = new;
+ st->cursor = new;
} else {
- // There are already subgoals
- g->next = st->cursor->next;
- st->cursor->next = g;
- st->cursor = g;
+ /* Creating first subgoal */
+ st->cursor = new;
+ if (st->focus) st->focus->sub = new;
+ st->next = new;
}
- g->target = target;
- g->state = OPEN;
}
void
commit(struct state *st)
{
- if (st->cursor) {
- st->cursor = NULL;
- } else if (st->focus) {
- st->focus->state = CLOSED;
+ 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, address dest)
+solve(struct state *st, void *dest)
{
assert(st->focus);
- st->focus->state = CLOSED;
- assign(st, st->focus->target, dest);
+ 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 attitude*
-lookup_attitude(struct state *st, address name)
+struct symbol
+*read_symbol(struct tape *program)
{
- for (size_t i = 0; i < st->nattitudes; i++) {
- if (st->attitudes[i].marker == name) {
- return &st->attitudes[i];
- }
- }
- return NULL;
+ assert(program->code[program->cur].code == SYM);
+ return program->code[program->cur++].sym;
}
-void
-step(struct state *st)
+unsigned int
+read_number(struct tape *program)
{
- struct goal *g;
-
- assert(!st->cursor);
+ assert(program->code[program->cur].code == NUM);
+ return program->code[program->cur++].num;
+}
- if (!st->focus) {
- return; // read in next input
- }
+ref_t
+read_top(struct tape *program)
+{
+ assert(program->code[program->cur].code == TOP);
+ return program->code[program->cur++].type;
+}
- switch (st->focus->state) {
- case OPEN:
- // read in next input
- break;
+void
+step(struct state *st, struct tape *program)
+{
+ unsigned int n, m;
+ struct symbol *sym; // , *mk;
- case CLOSED:
- // verify it, maybe
- g = st->focus;
- st->focus = st->focus->next;
- free(g);
- break;
+ 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)
+run(struct state *st, struct tape *program)
{
- while (st->focus && st->focus->state == CLOSED)
- step(st);
+ while (program->code[program->cur].code != HLT)
+ step(st, program);
}
int
main(void) {
struct state s = new_state();
- address wft = create_symbol(&s, "wft");
- address colon = create_symbol(&s, ":");
- address var_a = create_symbol(&s, "a");
- address var_b = create_symbol(&s, "b");
- address type_wft = create_symbol(&s, "type-wft");
- address type = create_symbol(&s, "type");
- address is_type_wft = create_symbol(&s, "is-type-wft");
- address a_type = create_symbol(&s, "a-type");
-
- tactic_attitude(&s, wft, 1, 0); run(&s);
- solve(&s, var_a); run(&s);
-
- tactic_attitude(&s, colon, 2, 1); run(&s);
- solve(&s, var_a); run(&s);
- solve(&s, var_b); run(&s);
- tactic_term(&s, wft, 1); run(&s);
- tactic_term(&s, var_b, 0); run(&s);
-
- tactic_assumption(&s, type_wft, wft, 0, 0); run(&s);
- tactic_term(&s, wft, 1);
- tactic_term(&s, type, 0); run(&s);
-
- tactic_assumption(&s, is_type_wft, wft, 1, 1); run(&s);
- solve(&s, var_a); run(&s);
- tactic_term(&s, wft, 1); run(&s);
- tactic_term(&s, var_a, 0); run(&s);
- tactic_assumption(&s, a_type, colon, 0, 0); run(&s);
- tactic_term(&s, colon, 2);
- tactic_term(&s, var_a, 0); run(&s);
- tactic_term(&s, type, 0); run(&s);
-
- tactic_proof(&s, 5); run(&s);
- solve(&s, type_wft); run(&s);
+ 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;
}
diff --git a/coding/vm.h b/coding/vm.h
@@ -1,6 +1,5 @@
#ifndef VM_H
#define VM_H
-typedef size_t address;
typedef enum {
SYMBOL,
@@ -10,14 +9,9 @@ typedef enum {
PROOF,
} ref_t;
-typedef enum {
- OPEN,
- CLOSED
-} goal_s;
-
struct ref {
- ref_t type;
- address addr;
+ ref_t type;
+ void *addr;
int resolved;
};
@@ -26,41 +20,43 @@ struct symbol {
};
struct attitude {
- address marker;
+ struct symbol *marker;
size_t nvars;
- address vars;
+ struct symbol **vars;
size_t npres;
- address pressupositions;
+ struct term **pressupositions;
};
struct term {
- address head;
+ struct symbol *head;
size_t nargs;
- address subterms;
+ struct term **subterms;
};
struct assumption {
- address name;
- address marker;
+ struct symbol *name;
+ struct symbol *marker;
size_t nvars;
size_t nsub;
size_t nproofs;
- address proofs;
- address judgment;
- address vars;
- address sub;
- address prev;
+ struct proof *proofs;
+ struct term *judgment;
+ struct symbol *vars;
+ struct assumption *sub;
+ struct assumption *prev;
};
struct proof {
- address thesis;
- address argument;
+ struct term *thesis;
+ struct argument *argument;
};
struct goal {
- goal_s state;
struct goal *next;
- address target;
+ struct goal *parent;
+ struct goal *sub;
+ ref_t type;
+ void **target;
};
#define cap(t) c ## t ## s
@@ -70,51 +66,79 @@ struct goal {
#define init(s, t) do { \
s . cap(t) = 1; \
s . num(t) = 0; \
- s . vec(t) = malloc(sizeof(struct t)); \
+ s . vec(t) = calloc(1, sizeof(struct t)); \
} while(0)
-#define push(s, t, x) ( \
+#define push(s, t, x) do { \
+ if (s -> cap(t) == s -> num(t)) { \
+ s -> vec(t) = realloc(s -> vec(t), s -> cap(t) *= 2 * sizeof(struct t)); \
+ } \
+ (s -> vec(t)[s -> num(t)++] = x); } while(0)
+
+#define reserve(s, t) ( \
( \
(s -> cap(t) == s -> num(t)) ? \
(s -> vec(t) = realloc(s -> vec(t), \
(s -> cap(t) *= 2)*sizeof(struct t))) : \
NULL \
), \
- (s -> vec(t)[s -> num(t)++] = x), \
- (s -> num(t)-1) \
+ (s -> vec(t) + (s -> num(t)++)) \
)
-#define resolve(state, type, addr) state -> type ## s [addr]
+#define list(t) size_t num(t); size_t cap(t); struct t ** vec(t)
+
+/* The program is a series of values. The possible types are:
+ - A TOP instruction + type of top goal
+ - A value, depending on the current focus
+
+ Types of values:
+ - Symbol
+ - Natural number
+*/
+
+enum opcode {
+ TOP,
+ SYM,
+ NUM,
+ HLT
+};
+
+struct op {
+ enum opcode code;
+ union {
+ unsigned int num;
+ struct symbol *sym;
+ ref_t type;
+ };
+};
-#define list(t) size_t num(t); size_t cap(t); struct t * vec(t)
+struct tape {
+ struct op *code;
+ size_t cur;
+};
struct state {
struct goal *focus;
struct goal *cursor;
+ struct goal *next;
+ struct assumption *head;
- list(ref);
- list(symbol);
- list(term);
list(attitude);
- list(assumption);
- list(proof);
};
+
struct state new_state(void);
-address allocate_refs(struct state *st, size_t n, ref_t type);
-address create_term(struct state *st, address symbol, size_t nargs);
-address create_symbol(struct state *st, char *name);
-address create_attitude(struct state *st, address marker, size_t nvars, size_t npres);
-address create_assumption(struct state *st, address name, address marker, size_t nvars, size_t nsub);
-address create_proof(struct state *st, address thesis);
-
-void assign(struct state *st, address ref, address dest);
-void add_subgoal(struct state *st, address target);
+struct ref *allocate_refs(struct state *st, size_t n, ref_t type);
+struct term *create_term(struct symbol *head, size_t nargs);
+struct symbol *create_symbol(char *name);
+struct attitude *create_attitude(struct symbol *marker, size_t nvars, size_t npres);
+struct assumption *create_assumption(struct state *st, struct symbol *name, struct symbol *marker, size_t nvars, size_t nsub);
+struct proof *create_proof(struct state *st, struct term *thesis);
+
+void assign(struct state *st, struct ref *ref, void *dest);
+void add_subgoal(struct state *st, ref_t type, void *target);
void commit(struct state *st);
-void solve(struct state *st, address dest);
-struct attitude *lookup_attitude(struct state *st, address name);
-
-
-void step(struct state *st);
+void solve(struct state *st, void *dest);
+struct attitude *lookup_attitude(struct state *st, struct symbol *name);
#endif
