commit 00916fc909459a4af75768f0d62dbac6a8c2495c
parent e26850e8f35c3b20b02edfa9ffa5c9ed81f8a58a
Author: Juan F. Meleiro <juan@juanmeleiro.mat.br>
Date: Sat, 30 Mar 2024 12:54:02 -0300
Start new iteration, with new concepts
Diffstat:
23 files changed, 270 insertions(+), 1017 deletions(-)
diff --git a/coding/assoc.h b/coding/assoc.h
@@ -1,4 +1,4 @@
-#include "interning.h"
+#include "symbol.h"
typedef struct assoc assoc;
diff --git a/coding/assoc.test.c b/coding/assoc.test.c
@@ -2,7 +2,7 @@
#include <assert.h>
#include <stdio.h>
-#include "interning.h"
+#include "symbol.h"
#include "assoc.h"
bool
@@ -20,7 +20,6 @@ test_get_after_set_is_id()
int
main()
{
- initialize();
assert(test_get_after_set_is_id());
return 0;
}
diff --git a/coding/build.sh b/coding/build.sh
@@ -1,5 +1,8 @@
#!/bin/sh
+run=$1
+set -- symbol.c assoc.c tree.c schema.c gardener.c
+
echo '========================================'
-cc -Wall -Wextra -pedantic -Wfatal-errors -g -o vm *.c 2>&1 &&
-[ "$1" = '-r' ] && ./vm 2>&1
+cc -Wall -Wextra -pedantic -Wfatal-errors -g -o vm "$@" 2>&1 &&
+[ "$run" = '-r' ] && ./vm 2>&1
diff --git a/coding/formating.c b/coding/formating.c
@@ -1,238 +0,0 @@
-#include <stdio.h>
-#include <stdlib.h>
-#include <assert.h>
-
-#include "formating.h"
-
-void
-print_symbol(FILE *f, struct symbol *s)
-{
- if (s == NULL)
- fputc('_', f);
- else
- fprintf(f, "%s", s->name);
-}
-
-void
-print_term(FILE *f, struct state *st, struct term *t)
-{
- if (t == NULL) {
- fputc('_', f);
- } else {
- 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);
- }
- }
-}
-
-void
-print_goal(FILE *f, struct goal *g, unsigned int level)
-{
- if (!g) {
- fprintf(f, "Nothing to do.");
- } else {
- 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)
-{
- 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, *a.name);
- fputc('[', f);
- for (size_t i = 0; i < a.nvars; i++) {
- print_symbol(f, a.vars[i]);
- }
- fputs("]: ", f);
- print_term(f, st, *a.judgment);
- fputc('\n', f);
- for (size_t i = 0; i < a.nsub; i++) {
- fputs(" ", f);
- print_assumption(f, st, a.sub[i]);
- fputc('\n', f);
- }
-}
-
-void
-print_proof(FILE *f, struct state *st, struct proof p)
-{
- // print_argument(f, st, *p.argument);
- fprintf(f, " |- ");
- print_term(f, st, *p.thesis);
- fputc('\n', f);
-}
-*/
-
-void
-print_state(FILE *f, struct state *st)
-{
- // size_t i;
-
- fprintf(f, "----------\n");
-
- 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, "GOALS\n");
- for (struct goal *cur = st->focus; cur; cur = cur->next) {
- print_goal(f, cur, 0);
- fputc('\n', f);
- }
-}
-
-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
@@ -1,13 +0,0 @@
-#include "vm.h"
-
-#define type_variable(t) ("SJATPR"[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 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/gardener.c.wip b/coding/gardener.c.wip
@@ -0,0 +1,64 @@
+#include "gardener.h"
+
+#include "tree.h"
+#include "schema.h"
+
+struct gardener {
+};
+
+schema* get_schema (gardener *g);
+void set_schema (gardener *g, schema *s);
+schema* push_schema (gardener *g);
+schema* pop_schema (gardener *g);
+tree* get_tree (gardener *g);
+void set_tree (gardener *g, tree *t);
+tree* pop_tree (gardener *g);
+void push_tree (gardener *g);
+void set_error (gardener *g);
+bool at_ground (gardener *g);
+
+/* PUBLIC */
+
+gardener* new_gardener(schema*);
+
+void
+fill(gardener* g, symbol key, symbol value)
+{
+ tree *new = new_leaf(value);
+ set(get_cur_tree(g), key, new);
+}
+
+void
+sub(gardener* g, symbol key, symbol constructor)
+{
+ tree *new = new_node(constructor);
+ set(get_cur_tree(g), key, new);
+ push_cur_tree(g);
+ push_schema(g, get_subschema(peek_schema(g), key));
+ set_cur_tree(g, new);
+}
+
+bool
+done(gardener* g)
+{
+ schema *s = pop_schema(g);
+ if (check(s, get_cur_tree(g))) {
+ set_error(g);
+ return false;
+ } else {
+ set_cur_tree(g, pop_tree(g));
+ }
+}
+
+void
+sup(gardener* g, symbol key, symbol constructor)
+{
+ if (at_ground(g)) {
+ tree *sup = new_node(constructor);
+ set(sup, key, get_cur_tree(g));
+ set_cur_tree(g, sup);
+ } else {
+ set_error(g);
+ }
+}
+
diff --git a/coding/gardener.h b/coding/gardener.h
@@ -0,0 +1,11 @@
+#include <stdbool.h>
+#include "schema.h"
+
+typedef struct gardener gardener;
+
+gardener* new_gardener(schema*);
+
+void fill(gardener*, symbol key, symbol value);
+void sub(gardener*, symbol key, symbol constructor);
+bool done(gardener*);
+void sup(gardener*, symbol key, symbol constructor);
diff --git a/coding/interning.c b/coding/interning.c
@@ -1,45 +0,0 @@
-#include "interning.h"
-#include <stdbool.h>
-#include <assert.h>
-#include <string.h>
-
-static char **db = NULL;
-static size_t cap = 0;
-static size_t len = 0;
-static bool initialized = false;
-
-void
-initialize(void)
-{
- cap = 1;
- db = malloc(cap * sizeof(char*));
- initialized = true;
-}
-
-symbol
-append(char *name)
-{
- assert(initialized);
- if (len == cap)
- db = realloc(db, (cap *= 2)*sizeof(char*));
- assert(db);
- db[len] = name;
- return len++;
-}
-
-symbol
-intern(char *name)
-{
- assert(initialized);
- for (size_t i = 0; i < len; i++)
- if (strcmp(name, db[i]) == 0)
- return i;
- return append(name);
-}
-
-char*
-repr(symbol s)
-{
- assert(initialized);
- return db[s];
-}
diff --git a/coding/interning.h b/coding/interning.h
@@ -1,12 +0,0 @@
-#include <stdlib.h>
-
-typedef size_t symbol;
-
-/* Guarantees:
- - strcmp(repr(intern(s)), s) == 0
- - intern(repr(s)) == s
- */
-
-void initialize();
-symbol intern(char*);
-char* repr(symbol);
diff --git a/coding/interning.test.c b/coding/interning.test.c
@@ -1,26 +0,0 @@
-#include "interning.h"
-#include <stdbool.h>
-#include <assert.h>
-#include <string.h>
-
-bool
-test_repr_of_intern_is_iso()
-{
- char *test = "abc";
- return strcmp(repr(intern(test)), test) == 0;
-}
-
-bool
-test_intern_of_repr_is_id()
-{
- char *test = "abc";
- symbol s = intern(test);
- return intern(repr(s)) == s;
-}
-
-int
-main() {
- initialize();
- assert(test_repr_of_intern_is_iso());
- assert(test_intern_of_repr_is_id());
-}
diff --git a/coding/schema.h b/coding/schema.h
@@ -0,0 +1,10 @@
+#include <stdbool.h>
+
+#include "symbol.h"
+#include "tree.h"
+
+typedef struct schema schema;
+
+schema* new_schema(void);
+schema* get_subschema(schema*, symbol);
+bool check(schema*, tree*);
diff --git a/coding/symbol.c b/coding/symbol.c
@@ -0,0 +1,45 @@
+#include "symbol.h"
+#include <stdbool.h>
+#include <assert.h>
+#include <string.h>
+
+static char **db = NULL;
+static size_t cap = 0;
+static size_t len = 0;
+static bool initialized = false;
+
+void
+initialize(void)
+{
+ cap = 1;
+ db = malloc(cap * sizeof(char*));
+ initialized = true;
+}
+
+symbol
+append(char *name)
+{
+ assert(initialized);
+ if (len == cap)
+ db = realloc(db, (cap *= 2)*sizeof(char*));
+ assert(db);
+ db[len] = name;
+ return len++;
+}
+
+symbol
+intern(char *name)
+{
+ if (!initialized) initialize();
+ for (size_t i = 0; i < len; i++)
+ if (strcmp(name, db[i]) == 0)
+ return i;
+ return append(name);
+}
+
+char*
+repr(symbol s)
+{
+ if (!initialized) initialize();
+ return db[s];
+}
diff --git a/coding/symbol.h b/coding/symbol.h
@@ -0,0 +1,11 @@
+#include <stdlib.h>
+
+typedef size_t symbol;
+
+/* Guarantees:
+ - strcmp(repr(intern(s)), s) == 0
+ - intern(repr(s)) == s
+ */
+
+symbol intern(char*);
+char* repr(symbol);
diff --git a/coding/symbol.test.c b/coding/symbol.test.c
@@ -0,0 +1,25 @@
+#include "symbol.h"
+#include <stdbool.h>
+#include <assert.h>
+#include <string.h>
+
+bool
+test_repr_of_intern_is_iso()
+{
+ char *test = "abc";
+ return strcmp(repr(intern(test)), test) == 0;
+}
+
+bool
+test_intern_of_repr_is_id()
+{
+ char *test = "abc";
+ symbol s = intern(test);
+ return intern(repr(s)) == s;
+}
+
+int
+main() {
+ assert(test_repr_of_intern_is_iso());
+ assert(test_intern_of_repr_is_id());
+}
diff --git a/coding/tactics.c b/coding/tactics.c
@@ -1,86 +0,0 @@
-#include "tactics.h"
-
-res_t
-tactic_term(struct state *st, struct symbol *head, size_t arity)
-{
- assert(!st->focus || st->focus->type == TERM);
-
- struct term *t = create_term(head, arity);
-
- if (st->focus) solve(st, t);
-
- for (size_t i = 0; i < arity; i++) {
- add_subgoal(st, TERM, t->subterms + i);
- }
-
- commit(st);
-
- return OK;
-}
-
-res_t
-tactic_attitude(struct state *st, struct symbol *marker, size_t nvars, size_t npres)
-{
- assert(st->focus && st->focus->type == ATTITUDE);
-
- struct attitude *a = create_attitude(marker, nvars, npres);
-
- for (size_t i = 0; i < nvars; i++)
- add_subgoal(st, SYMBOL, a->vars + i);
-
- for (size_t i = 0; i < npres; i++)
- add_subgoal(st, TERM, a->pressupositions + i);
-
- solve(st, a);
- commit(st);
-
- return OK;
-}
-
-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
-// 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, struct symbol *name, struct symbol *marker, size_t nvars, size_t nsub)
-{
- assert(!st->focus || st->focus->type == ASSUMPTION);
-
- struct assumption *a = create_assumption(st, name, marker, nvars, nsub);
-
- if (st->focus) solve(st, a);
-
- for (size_t i = 0; i < nvars; i++)
- add_subgoal(st, SYMBOL, a->vars + i);
-
- add_subgoal(st, TERM, a->judgment);
-
- for (size_t i = 0; i < nsub; i++)
- add_subgoal(st, ASSUMPTION, a->sub + 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
@@ -1,31 +0,0 @@
-#include <stdlib.h>
-#include <assert.h>
-
-#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);
-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/test.sh b/coding/test.sh
@@ -0,0 +1,12 @@
+#!/bin/sh
+
+src=$(ls *.c | grep -v '\.test\.c')
+
+for f in *.test.c
+do
+ out=$(basename $f .c)
+ cc -fmax-errors=1 $f $src -o $out || exit 1
+ ./$out
+done
+
+rm *.test
diff --git a/coding/tree.c b/coding/tree.c
@@ -0,0 +1,48 @@
+#include <stdbool.h>
+#include "assoc.h"
+#include "tree.h"
+
+struct tree {
+ symbol head;
+ assoc *children;
+};
+
+bool
+is_leaf(tree* t)
+{
+ return (t->children == NULL);
+}
+
+tree*
+new_leaf(symbol s)
+{
+ tree *t = malloc(sizeof(tree));
+ t->head = s;
+ t->children = NULL;
+ return t;
+}
+
+tree*
+new_node(symbol h)
+{
+ tree *t = malloc(sizeof(tree));
+ t->head = h;
+ t->children = new_assoc();
+ return t;
+}
+
+void
+set_subtree(tree* t, symbol k, tree* v)
+{
+ if (t->children)
+ assoc_set(t->children, k, (void*) v);
+}
+
+tree*
+get_subtree(tree* t, symbol k)
+{
+ if (t->children)
+ return (tree*) assoc_get(t->children, k);
+ else
+ return NULL;
+}
diff --git a/coding/tree.h b/coding/tree.h
@@ -0,0 +1,13 @@
+#include "symbol.h"
+
+typedef struct tree tree;
+
+tree* new_leaf (symbol);
+tree* new_node (symbol);
+void set_subtree (tree*, symbol, tree*);
+tree* get_subtree (tree*, symbol);
+bool is_leaf (tree*);
+
+/* Guarantees:
+ * - set(t, k, v), is_leaf(t) || get(t, k) == v;
+ */
diff --git a/coding/tree.test.c b/coding/tree.test.c
@@ -0,0 +1,24 @@
+#include <stdio.h>
+#include <stdbool.h>
+#include <assert.h>
+
+#include "symbol.h"
+#include "tree.h"
+
+bool
+test_get_after_set_is_id_on_node()
+{
+ symbol k = intern("key");
+ symbol h = intern("head");
+ tree *t = new_node(h);
+ set_subtree(t, k, (tree*) 0xabababab);
+ return get_subtree(t, k) == (tree*) 0xabababab;
+}
+
+
+int
+main()
+{
+ assert(test_get_after_set_is_id_on_node());
+ return 0;
+}
diff --git a/coding/vm.c b/coding/vm.c
@@ -1,321 +0,0 @@
-#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;
- s.err = OK;
- 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;
-
- 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);
- }
- st->focus = create_goal(type, addr);
-}
-
-void
-add_subgoal(struct state *st, ref_t type, void *target)
-{
- check_ok(st);
- check(st, st->focus, ADDING_SUBGOAL_WITHOUT_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)
-{
- check_ok(st);
- check(st, st->focus, COMMITING_WITHOUT_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)
-{
- check_ok(st);
- check(st, st->focus, SOLVING_WITHOUT_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 vm *m)
-{
- 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 vm *m)
-{
- 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 vm *m)
-{
- 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 vm *m)
-{
- unsigned int n, k;
- struct symbol *sym; // , *mk;
-
- check_ok(m);
-
- if (!m->state->focus) {
- /* No active goal. Expect goal creation */
- ref_t ty = read_top(m);
- add_top_goal(m->state, ty);
- } else {
- switch (m->state->focus->type) {
- case SYMBOL:
- sym = read_symbol(m);
- tactic_symbol(m->state, sym);
- break;
- case ATTITUDE:
- 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(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(m);
- n = read_number(m);
- tactic_term(m->state, sym, n);
- break;
- case PROOF:
- exit(1);
- break;
- }
- }
-}
-
-void
-run(struct vm *m)
-{
- while (
- m->tape->code[m->tape->cur].code != HLT &&
- m->err == OK
- )
- step(m);
-}
-
-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
- };
-
- 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
@@ -1,167 +0,0 @@
-#ifndef VM_H
-#define VM_H
-
-typedef enum {
- SYMBOL,
- ATTITUDE,
- ASSUMPTION,
- TERM,
- 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;
- int resolved;
-};
-
-struct symbol {
- char *name;
-};
-
-struct attitude {
- struct symbol *marker;
- size_t nvars;
- struct symbol **vars;
- size_t npres;
- struct term **pressupositions;
-};
-
-struct term {
- struct symbol *head;
- size_t nargs;
- struct term **subterms;
-};
-
-struct assumption {
- struct symbol *name;
- struct symbol *marker;
- size_t nvars;
- size_t nsub;
- size_t nproofs;
- struct proof *proofs;
- struct term *judgment;
- struct symbol *vars;
- struct assumption *sub;
- struct assumption *prev;
-};
-
-struct proof {
- struct term *thesis;
- struct argument *argument;
-};
-
-struct goal {
- struct goal *next;
- struct goal *parent;
- struct goal *sub;
- ref_t type;
- void **target;
-};
-
-#define cap(t) c ## t ## s
-#define num(t) n ## t ## s
-#define vec(t) t ## s
-
-#define init(s, t) do { \
- s . cap(t) = 1; \
- s . num(t) = 0; \
- s . vec(t) = calloc(1, sizeof(struct t)); \
- } while(0)
-
-#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)++)) \
-)
-
-#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;
- };
-};
-
-struct tape {
- struct op *code;
- size_t cur;
-};
-
-struct state {
- struct goal *focus;
- 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);
-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, void *dest);
-struct attitude *lookup_attitude(struct state *st, struct symbol *name);
-
-#endif
diff --git a/coding/vm.txt b/coding/vm.txt
@@ -1,73 +0,0 @@
-NEXT STEPS
-==========
-
-- [x] Implement goals for building terms
-- [x] Implement attitudes
-- [ ] Implement assumptions
-- [ ] Implement proofs
-
-
-NOTES
-=====
-
-GOALS
------
-Goals specify a thing to build and a destination.
-
-- NONE None (JUDGMENT, ASSUMPTION)
-- JUDG-VAR Give judgment parameter name (SYMBOL)
-- JUDG-PRE Construct pressuposition term (TERM)
-- ASMP-VAR Give assumption parameter name (SYMBOL)
-- ASMP-SUB Construct assumption (ASSUMPTION)
-- ASMP-JUG Construct judgment term (TERM)
-- ASMP-PRF Prove judgment (PROOF)
-- ASMP-ARG Construct proof argument (TERM)
-
-TACTICS
--------
-Tactics take arguments and build things for solving goals.
-
-- JUG (symbol, arity, subsize) Start a judgment form [construct JUDGMENT]
-- ASM (symbol, arity, subsize) Start an assumption [construct ASSUMPTION]
-- NAM (symbol) Name a symbol [construct SYMBOL]
-- ATM (symbol) Construct an atomic term [construct TERM]
-- APP (symbol, arity) Start a complex term [TERM]
-- REF (symbol) Reference an assumption [PROOF]
-
-EFFECTS
--------
-Each tactic changes the state of the system and possibly creates more
-goals, but also discharges the current one.
-
-- JUG (symbol name, int arity, int subsize):
- - allocate new judgment and set target to point to it
- - create `arity` symbol goals pointing to its variables
- - create `subsize` term goals pointing to its pressupositions
-
-- ASM (symbol name, int arity, int subsize):
- - allocate new assumption and set target to point to it
- - create `arity` symbol goals pointing to its variables
- - create `subsize` assumption goals pointing to its subassumptions
- - create a term goal pointing to its judgment
- - create a proof goal pointing to its judgment
-
-- NAM (symbol): set target's value to givem symbol
-
-- ATM (symbol):
- - allocate new term with arity 0
- - set term's head to given symbol
- - set target to point to term
-
-- APP (symbol head, int arity):
- - allocate new term with arity `arity`
- - set term's head to `head`
- - create `arity` symbol goals pointing to the term's subterms
-
-- REF (symbol):
- - set target proposition's candidate to given symbol
- - create one term goal for each variable in assumption refered to by symbol
- - create one proof goal for each subassumption of the assumption refered to by symbol
-
-RESOLUTION
-----------
-When all subgoals of a goal are resolved, extra logic might be needed to verify the resolution of the current goal.
