commit a272042d4ccfb321eafadf888d011186be54e423
parent abcebef5736f7d34d55dd84d41428f9aa87bc7f0
Author: Juan F. Meleiro <juan@juanmeleiro.mat.br>
Date: Sun, 7 Jan 2024 14:37:15 -0300
Add tactics for assumptions and proofs, plus reordering code
Currently, proofs are *not* verified. So that this is implemented, either
a resolution mechanism will need to be added when reaching closed goals,
or some data to refs so that the check is made at tactic application time.
Diffstat:
8 files changed, 262 insertions(+), 57 deletions(-)
diff --git a/coding/build.sh b/coding/build.sh
@@ -1,3 +1,3 @@
#!/bin/sh
-cc -Wall -Wextra -pedantic -g -o vm vm.c formating.c && ./vm
+cc -Wall -Wextra -pedantic -g -o vm *.c && ./vm
diff --git a/coding/formating.c b/coding/formating.c
@@ -16,8 +16,13 @@ print_ref(FILE *f, struct state *st, address ref)
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 {
@@ -82,6 +87,33 @@ print_attitude(FILE *f, struct state *st, struct attitude a)
}
void
+print_assumption(FILE *f, struct state *st, struct assumption a)
+{
+ print_symbol(f, st, resolve(st, symbol, a.name));
+ fputc('[', f);
+ for (size_t i = 0; i < a.nvars; i++) {
+ print_ref(f, st, a.vars + i);
+ }
+ fputs("]: ", f);
+ print_ref(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);
+ fputc('\n', f);
+ }
+}
+
+void
+print_proof(FILE *f, struct state *st, struct proof p)
+{
+ print_ref(f, st, p.argument);
+ fprintf(f, " |- ");
+ print_ref(f, st, p.thesis);
+ fputc('\n', f);
+}
+
+void
print_state(FILE *f, struct state *st)
{
size_t i;
@@ -90,10 +122,12 @@ print_state(FILE *f, struct state *st)
fprintf(f, "SYMBOLS (%ld/%ld)\n", st->nsymbols, st->csymbols);
for (i = 0; i < st->nsymbols; i++) {
- fprintf(f, "%ld: ", i);
+ if (i > 0) fputs(", ", f);
+ fprintf(f, "%ld: '", i);
print_symbol(f, st, resolve(st, symbol, i));
- fputc('\n', f);
+ fputc('\'', f);
}
+ fputc('\n', f);
fprintf(f, "\nTERMS (%ld/%ld)\n", st->nterms, st->cterms);
for (i = 0; i < st->nterms; i++) {
@@ -119,6 +153,16 @@ print_state(FILE *f, struct state *st)
print_attitude(f, st, st->attitudes[i]);
}
+ 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");
for (struct goal *cur = st->focus; cur; cur = cur->next) {
print_goal(f, st, cur);
diff --git a/coding/formating.h b/coding/formating.h
@@ -1,6 +1,6 @@
#include "vm.h"
-#define type_variable(t) ("SJAT"[t])
+#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);
@@ -9,3 +9,5 @@ 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_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
@@ -0,0 +1,76 @@
+#include "tactics.h"
+
+void
+tactic_term(struct state *st, address head, size_t arity)
+{
+ 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);
+
+ if (st->focus) solve(st, sol);
+
+ for (size_t i = 0; i < arity; i++) {
+ add_subgoal(st, t.subterms + i);
+ }
+
+ commit(st);
+}
+
+void
+tactic_attitude(struct state *st, address marker, size_t nvars, size_t npres)
+{
+ assert(!st->focus || resolve(st, ref, st->focus->target).type == ATTITUDE);
+
+ address sol = create_attitude(st, marker, nvars, npres);
+ struct attitude a = resolve(st, attitude, sol);
+
+ if (st->focus) solve(st, sol);
+
+ for (size_t i = 0; i < nvars; i++)
+ add_subgoal(st, a.vars + i);
+
+ for (size_t i = 0; i < npres; i++)
+ add_subgoal(st, a.pressupositions + i);
+
+ commit(st);
+}
+
+void
+tactic_proof(struct state *st, address thesis)
+{
+ 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);
+
+ commit(st);
+}
+
+void
+tactic_assumption(struct state *st, address name, address marker, size_t nvars, size_t nsub)
+{
+ assert(!st->focus || resolve(st, ref, st->focus->target).type == ASSUMPTION);
+
+ address sol = create_assumption(st, name, marker, nvars, nsub);
+ struct assumption a = resolve(st, assumption, sol);
+
+ if (st->focus) solve(st, sol);
+
+ for (size_t i = 0; i < nvars; i++)
+ add_subgoal(st, a.vars + i);
+
+ add_subgoal(st, a.judgment);
+
+ for (size_t i = 0; i < nsub; i++)
+ add_subgoal(st, a.sub + i);
+
+ for (size_t i = 0; i < a.nproofs; i++)
+ add_subgoal(st, a.proofs + i);
+
+ commit(st);
+}
diff --git a/coding/tactics.h b/coding/tactics.h
@@ -0,0 +1,30 @@
+#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);
+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);
+
diff --git a/coding/vm.c b/coding/vm.c
@@ -4,6 +4,7 @@
#include "vm.h"
#include "formating.h"
+#include "tactics.h"
/* OBJECT CREATION */
@@ -15,6 +16,8 @@ state new_state(void)
init(s, symbol);
init(s, term);
init(s, attitude);
+ init(s, assumption);
+ init(s, proof);
s.focus = NULL;
s.cursor = NULL;
return s;
@@ -69,6 +72,37 @@ create_symbol(struct state *st, char *name)
return push(st, symbol, sym);
}
+address
+create_assumption(struct state *st, address name, address 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 = allocate_refs(st, nvars, SYMBOL),
+ .sub = allocate_refs(st, nsub, ASSUMPTION),
+ .judgment = allocate_refs(st, 1, TERM),
+ .nproofs = att->npres,
+ .proofs = allocate_refs(st, att->npres, PROOF)
+ };
+
+ return push(st, assumption, a);
+}
+
+address
+create_proof(struct state *st, address thesis)
+{
+ struct proof p = {
+ .thesis = thesis,
+ .argument = allocate_refs(st, 1, SYMBOL)
+ };
+
+ return push(st, proof, p);
+}
+
/* GOAL MECHANICS */
void
@@ -95,6 +129,7 @@ add_subgoal(struct state *st, address target)
st->cursor = g;
}
g->target = target;
+ g->state = OPEN;
}
void
@@ -102,7 +137,7 @@ commit(struct state *st)
{
if (st->cursor) {
st->cursor = NULL;
- } else {
+ } else if (st->focus) {
st->focus->state = CLOSED;
}
}
@@ -115,42 +150,15 @@ solve(struct state *st, address dest)
assign(st, st->focus->target, dest);
}
-/* TACTICS */
-
-void
-tactic_term(struct state *st, address head, size_t arity)
+struct attitude*
+lookup_attitude(struct state *st, address name)
{
- 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);
-
- if (st->focus) solve(st, sol);
-
- for (size_t i = 0; i < arity; i++) {
- add_subgoal(st, t.subterms + i);
+ for (size_t i = 0; i < st->nattitudes; i++) {
+ if (st->attitudes[i].marker == name) {
+ return &st->attitudes[i];
+ }
}
-
- commit(st);
-}
-
-void
-tactic_attitude(struct state *st, address marker, size_t nvars, size_t npres)
-{
- assert(!st->focus || resolve(st, ref, st->focus->target).type == ATTITUDE);
-
- address sol = create_attitude(st, marker, nvars, npres);
- struct attitude a = resolve(st, attitude, sol);
-
- if (st->focus) solve(st, sol);
-
- for (size_t i = 0; i < nvars; i++)
- add_subgoal(st, a.vars + i);
-
- for (size_t i = 0; i < npres; i++)
- add_subgoal(st, a.pressupositions + i);
-
- commit(st);
+ return NULL;
}
void
@@ -178,30 +186,50 @@ step(struct state *st)
}
}
+void
+run(struct state *st)
+{
+ while (st->focus && st->focus->state == CLOSED)
+ step(st);
+}
+
int
main(void) {
struct state s = new_state();
- address wft = create_symbol(&s, "wft");
+ 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, wft, 1, 0);
- step(&s);
- solve(&s, var_a);
- step(&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_attitude(&s, colon, 2, 1);
- solve(&s, var_a);
- step(&s);
- solve(&s, var_b);
- step(&s);
+ tactic_assumption(&s, type_wft, wft, 0, 0); run(&s);
tactic_term(&s, wft, 1);
- step(&s);
- tactic_term(&s, var_b, 0);
- step(&s);
- step(&s);
+ 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);
print_state(stdout, &s);
return 0;
diff --git a/coding/vm.h b/coding/vm.h
@@ -6,7 +6,8 @@ typedef enum {
SYMBOL,
ATTITUDE,
ASSUMPTION,
- TERM
+ TERM,
+ PROOF,
} ref_t;
typedef enum {
@@ -38,6 +39,24 @@ struct term {
address subterms;
};
+struct assumption {
+ address name;
+ address marker;
+ size_t nvars;
+ size_t nsub;
+ size_t nproofs;
+ address proofs;
+ address judgment;
+ address vars;
+ address sub;
+ address prev;
+};
+
+struct proof {
+ address thesis;
+ address argument;
+};
+
struct goal {
goal_s state;
struct goal *next;
@@ -77,6 +96,8 @@ struct state {
list(symbol);
list(term);
list(attitude);
+ list(assumption);
+ list(proof);
};
struct state new_state(void);
@@ -84,14 +105,15 @@ 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);
void commit(struct state *st);
void solve(struct state *st, address dest);
+struct attitude *lookup_attitude(struct state *st, address name);
-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 step(struct state *st);
diff --git a/coding/vm.txt b/coding/vm.txt
@@ -1,7 +1,10 @@
NEXT STEPS
==========
-- Implement goals for building terms
+- [x] Implement goals for building terms
+- [x] Implement attitudes
+- [ ] Implement assumptions
+- [ ] Implement proofs
NOTES
