commit 73b5c1b66e955db70e1c34db37636ab534c94fb6
parent 4427db8f18e506b5b1ab4c23964b3f0518850a98
Author: Juan F. Meleiro <juan@juanmeleiro.mat.br>
Date: Sat, 6 Jan 2024 18:16:43 -0300
Add goals and tactics for building terms
Diffstat:
| A | coding/build.sh | | | 3 | +++ |
| A | coding/formating.c | | | 105 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
| A | coding/formating.h | | | 10 | ++++++++++ |
| M | coding/vm.c | | | 208 | +++++++++++++++++++++++++++++++------------------------------------------------ |
| A | coding/vm.h | | | 85 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
| A | coding/vm.txt | | | 70 | ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
6 files changed, 355 insertions(+), 126 deletions(-)
diff --git a/coding/build.sh b/coding/build.sh
@@ -0,0 +1,3 @@
+#!/bin/sh
+
+cc -o vm vm.c formating.c && ./vm
diff --git a/coding/formating.c b/coding/formating.c
@@ -0,0 +1,105 @@
+#include <stdio.h>
+#include <stdlib.h>
+
+#include "formating.h"
+
+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_goal(FILE *f, struct state *st, struct goal *g)
+{
+ 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]");
+ }
+ }
+}
+
+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("?", f);
+ fputc('\n', f);
+ }
+
+ fprintf(f, "\nGOALS\n");
+ for (struct goal *cur = st->focus; cur; cur = cur->next) {
+ print_goal(f, st, cur);
+ fputc('\n', f);
+ }
+}
+
diff --git a/coding/formating.h b/coding/formating.h
@@ -0,0 +1,10 @@
+#include "vm.h"
+
+#define type_variable(t) ("SJAT"[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_state(FILE *f, struct state *st);
+void print_goal(FILE *f, struct state *st, struct goal *g);
diff --git a/coding/vm.c b/coding/vm.c
@@ -2,76 +2,21 @@
#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;
-
-};
+#include "vm.h"
+#include "formating.h"
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))
- };
+ struct state s;
+ init(s, ref);
+ init(s, symbol);
+ init(s, term);
+ s.focus = NULL;
+ s.cursor = NULL;
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)
{
@@ -111,8 +56,6 @@ create_symbol(struct state *st, char *name)
return push(st, symbol, sym);
}
-#define resolve(state, type, addr) state -> type ## s [addr]
-
void
assign(struct state *st, address ref, address dest)
{
@@ -120,95 +63,108 @@ assign(struct state *st, address ref, address 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)
+add_subgoal(struct state *st, address target)
{
- 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;
- }
+ struct goal *g = malloc(sizeof(struct goal));
+
+ if (!st->cursor) {
+ // Creating first subgoal
+ g->next = st->focus;
+ st->focus = g;
+ st->cursor = g;
} else {
- char v = type_variable(cur.type);
- fprintf(f, "%c%ld", v, ref);
+ // There are already subgoals
+ g->next = st->cursor->next;
+ st->cursor->next = g;
+ st->cursor = g;
}
+ g->target = target;
}
void
-print_symbol(FILE *f, struct state *st, struct symbol s)
+commit(struct state *st)
{
- (void)st;
- fprintf(f, "%s", s.name);
+ if (st->cursor) {
+ st->cursor = NULL;
+ } else {
+ st->focus->state = CLOSED;
+ }
}
void
-print_term(FILE *f, struct state *st, struct term t)
+solve(struct state *st, address dest)
{
- 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);
- }
+ assert(st->focus);
+ st->focus->state = CLOSED;
+ assign(st, st->focus->target, dest);
}
void
-print_state(FILE *f, struct state *st)
+tactic_term(struct state *st, address head, size_t arity)
{
- size_t i;
+ assert(!st->focus || resolve(st, ref, st->focus->target).type == TERM);
+
+ address sol = create_term(st, head, arity);
+ struct term t = resolve(st, term, sol);
- fprintf(f, "----------\n");
+ if (st->focus) solve(st, sol);
- 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);
+ for (size_t i = 0; i < arity; i++) {
+ add_subgoal(st, t.subterms + i);
}
- 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);
+ commit(st);
+}
+
+void
+step(struct state *st)
+{
+ struct goal *g;
+
+ assert(!st->cursor);
+
+ if (!st->focus) {
+ return; // read in next input
}
- 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);
+ switch (st->focus->state) {
+ case OPEN:
+ // read in next input
+ break;
+
+ case CLOSED:
+ // verify it, maybe
+ g = st->focus;
+ st->focus = st->focus->next;
+ free(g);
+ break;
}
}
-int main(void) {
+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);
+ cur = create_symbol(&state, "x");
+
+ tactic_term(&state, cur, 2);
+ step(&state);
+
+ tactic_term(&state, cur, 2);
+ step(&state);
+
+ tactic_term(&state, cur, 0);
+ step(&state);
+
+ tactic_term(&state, cur, 0);
+ step(&state);
+ step(&state);
+
+ tactic_term(&state, cur, 0);
+ step(&state);
+
print_state(stdout, &state);
return 0;
}
diff --git a/coding/vm.h b/coding/vm.h
@@ -0,0 +1,85 @@
+#ifndef VM_H
+#define VM_H
+typedef size_t address;
+
+typedef enum {
+ SYMBOL,
+ JUDGMENT_FORM,
+ ASSUMPTION,
+ TERM
+} ref_t;
+
+typedef enum {
+ OPEN,
+ CLOSED
+} goal_s;
+
+struct ref {
+ ref_t type;
+ address addr;
+ int resolved;
+};
+
+struct symbol {
+ char *name;
+};
+
+struct term {
+ address head;
+ size_t nargs;
+ address subterms;
+};
+
+struct goal {
+ goal_s state;
+ struct goal *next;
+ address 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) = malloc(sizeof(struct t)); \
+ } while(0)
+
+#define push(s, t, x) ( \
+ ( \
+ (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) \
+)
+
+#define list(t) size_t num(t); size_t cap(t); struct t * vec(t)
+
+struct state {
+ struct goal *focus;
+ struct goal *cursor;
+
+ list(ref);
+ list(symbol);
+ list(term);
+};
+
+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);
+
+#define resolve(state, type, addr) state -> type ## s [addr]
+
+void add_subgoal(struct state *st, address target);
+
+void assign(struct state *st, address ref, address dest);
+
+#endif
diff --git a/coding/vm.txt b/coding/vm.txt
@@ -0,0 +1,70 @@
+NEXT STEPS
+==========
+
+- Implement goals for building terms
+
+
+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.
