commit abcebef5736f7d34d55dd84d41428f9aa87bc7f0
parent 73b5c1b66e955db70e1c34db37636ab534c94fb6
Author: Juan F. Meleiro <juan@juanmeleiro.mat.br>
Date: Sat, 6 Jan 2024 19:16:34 -0300
Add logic relating to attitudes
Diffstat:
5 files changed, 114 insertions(+), 39 deletions(-)
diff --git a/coding/build.sh b/coding/build.sh
@@ -1,3 +1,3 @@
#!/bin/sh
-cc -o vm vm.c formating.c && ./vm
+cc -Wall -Wextra -pedantic -g -o vm vm.c formating.c && ./vm
diff --git a/coding/formating.c b/coding/formating.c
@@ -3,8 +3,6 @@
#include "formating.h"
-void print_term(FILE *f, struct state *st, struct term t);
-
void
print_ref(FILE *f, struct state *st, address ref)
{
@@ -15,8 +13,9 @@ print_ref(FILE *f, struct state *st, address ref)
print_term(f, st, resolve(st, term, cur.addr));
break;
case SYMBOL:
+ print_symbol(f, st, resolve(st, symbol, cur.addr));
break;
- case JUDGMENT_FORM:
+ case ATTITUDE:
break;
case ASSUMPTION:
break;
@@ -65,20 +64,38 @@ print_goal(FILE *f, struct state *st, struct goal *g)
}
void
+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);
+ }
+}
+
+void
print_state(FILE *f, struct state *st)
{
size_t i;
fprintf(f, "----------\n");
- fprintf(f, "SYMBOLS\n");
+ fprintf(f, "SYMBOLS (%ld/%ld)\n", st->nsymbols, st->csymbols);
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");
+ 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]);
@@ -96,6 +113,12 @@ print_state(FILE *f, struct state *st)
fputc('\n', f);
}
+ fprintf(f, "\nATTITUDES (%ld/%ld)\n", st->nattitudes, st->cattitudes);
+ for (i = 0; i < st->nattitudes; i++) {
+ fprintf(f, "%ld: ", i);
+ print_attitude(f, st, st->attitudes[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
@@ -8,3 +8,4 @@ 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);
+void print_attitude(FILE *f, struct state *st, struct attitude a);
diff --git a/coding/vm.c b/coding/vm.c
@@ -5,6 +5,8 @@
#include "vm.h"
#include "formating.h"
+/* OBJECT CREATION */
+
struct
state new_state(void)
{
@@ -12,6 +14,7 @@ state new_state(void)
init(s, ref);
init(s, symbol);
init(s, term);
+ init(s, attitude);
s.focus = NULL;
s.cursor = NULL;
return s;
@@ -36,17 +39,27 @@ allocate_refs(struct state *st, size_t n, ref_t type)
address
create_term(struct state *st, address symbol, size_t nargs)
{
- address cur;
-
struct term t = {
.head = symbol,
.nargs = nargs,
.subterms = allocate_refs(st, nargs, TERM)
};
- cur = push(st, term, t);
+ return push(st, term, t);
+}
+
+address
+create_attitude(struct state *st, address 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 cur;
+ return push(st, attitude, a);
}
address
@@ -56,6 +69,8 @@ create_symbol(struct state *st, char *name)
return push(st, symbol, sym);
}
+/* GOAL MECHANICS */
+
void
assign(struct state *st, address ref, address dest)
{
@@ -100,6 +115,8 @@ solve(struct state *st, address dest)
assign(st, st->focus->target, dest);
}
+/* TACTICS */
+
void
tactic_term(struct state *st, address head, size_t arity)
{
@@ -118,6 +135,25 @@ tactic_term(struct state *st, address head, size_t arity)
}
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
step(struct state *st)
{
struct goal *g;
@@ -144,27 +180,29 @@ step(struct state *st)
int
main(void) {
- struct state state = new_state();
- address cur, cur2;
-
- 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);
+ 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");
+
+ tactic_attitude(&s, wft, 1, 0);
+ step(&s);
+ solve(&s, var_a);
+ step(&s);
+
+ tactic_attitude(&s, colon, 2, 1);
+ solve(&s, var_a);
+ step(&s);
+ solve(&s, var_b);
+ step(&s);
+ tactic_term(&s, wft, 1);
+ step(&s);
+ tactic_term(&s, var_b, 0);
+ step(&s);
+ step(&s);
+
+ print_state(stdout, &s);
return 0;
}
diff --git a/coding/vm.h b/coding/vm.h
@@ -4,7 +4,7 @@ typedef size_t address;
typedef enum {
SYMBOL,
- JUDGMENT_FORM,
+ ATTITUDE,
ASSUMPTION,
TERM
} ref_t;
@@ -24,6 +24,14 @@ struct symbol {
char *name;
};
+struct attitude {
+ address marker;
+ size_t nvars;
+ address vars;
+ size_t npres;
+ address pressupositions;
+};
+
struct term {
address head;
size_t nargs;
@@ -57,6 +65,8 @@ struct goal {
(s -> num(t)-1) \
)
+#define resolve(state, type, addr) state -> type ## s [addr]
+
#define list(t) size_t num(t); size_t cap(t); struct t * vec(t)
struct state {
@@ -66,20 +76,23 @@ struct state {
list(ref);
list(symbol);
list(term);
+ list(attitude);
};
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);
-#define resolve(state, type, addr) state -> type ## s [addr]
-
+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);
-void assign(struct state *st, address ref, address dest);
+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);
#endif
