loa

Virtual machine for the Logic of Assumptions
git clone git://juanmeleiro.mat.br/loa
Log | Files | Refs

commit 9d7c856c2d0f4190cf577369e93da9f5c9444f18
parent 85c2cf9d24765de0a96d19da6bd02c54e9fae58f
Author: Juan F. Meleiro <juan@juanmeleiro.mat.br>
Date:   Fri, 26 Apr 2024 17:24:10 -0300

Implement shape of model without checker functions

Diffstat:
Mcoding/assoc.c | 31+++++++++++++++++--------------
Mcoding/assoc.test.c | 13+++++++++++++
Acoding/model.c | 60++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Mcoding/model.h | 16+++++++++-------
Acoding/model.test.c | 114+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Mcoding/schema.c | 7++++---
Mcoding/schema.h | 1+
Mcoding/symbol.c | 4+++-
Mcoding/symbol.test.c | 27+++++++++++++++++++++++++++
Mcoding/test.sh | 2+-
10 files changed, 249 insertions(+), 26 deletions(-)

diff --git a/coding/assoc.c b/coding/assoc.c @@ -22,27 +22,30 @@ new_cell(symbol s, void *v) struct cell *c = malloc(sizeof(struct cell)); c->key = s; c->value = v; + c->next = NULL; return c; } void -set(struct cell *c, symbol s, void* v) -{ - if (c->key == s) - c->value = v; - else if (c->next == NULL) - c->next = new_cell(s, v); - else - set(c->next, s, v); -} - -void assoc_set(assoc* a, symbol s, void* v) { - if (a->cells == NULL) + if (a->cells == NULL) { a->cells = new_cell(s, v); - else - set(a->cells, s, v); + } else { + struct cell *c = a->cells; + while (1) { + if (c->key == s) { + c->value = v; + break; + } else if (c->next == NULL) { + c->next = new_cell(s, v); + break; + } else { + c = c->next; + continue; + } + } + } } void* diff --git a/coding/assoc.test.c b/coding/assoc.test.c @@ -67,11 +67,24 @@ test_keys() return res; } +void +test_many_keys() +{ + assoc *a = new_assoc(); + char k[2] = "a"; + for (char c = 'a'; c <= 'z'; c++) { + k[0] = c; + assoc_set(a, intern(k), (void*)1); + } + assert(get_amount_of_keys(a) == 26); +} + int main() { assert(test_get_after_set_is_id()); assert(test_amount_of_keys()); assert(test_keys()); + test_many_keys(); return 0; } diff --git a/coding/model.c b/coding/model.c @@ -0,0 +1,60 @@ +#include "model.h" + +#include "schema.h" + +#define I intern + +#define start_schema(NAME) \ + schema * _ ## NAME ## _schema = NULL; \ + schema* \ + NAME ## _schema() { \ + if (_ ## NAME ## _schema != NULL) return _ ## NAME ## _schema; \ + schema *it = new_schema(); \ + _ ## NAME ## _schema = it; \ + +#define end_schema(NAME) \ + return it; \ + } + +#define schema(NAME) NAME ## _schema() + +start_schema(context) + add_constructor (it, I("attitude") ); + mark_as_leaf (it, I("attitude"), I("name") ); + assign_subschema (it, I("attitude"), I("vars"), schema(vars) ); + assign_subschema (it, I("attitude"), I("pressupositions"), schema(term_list) ); + + add_constructor (it, I("assumption") ); + mark_as_leaf (it, I("assumption"), I("name") ); + assign_subschema (it, I("assumption"), I("judgment"), schema(term) ); + assign_subschema (it, I("assumption"), I("proof"), schema(proof) ); +end_schema(context); + +start_schema(term) + add_constructor (it, I("term") ); + mark_as_leaf (it, I("term"), I("head") ); + assign_subschema (it, I("term"), I("tail"), schema(term_list) ); +end_schema(term) + +start_schema(term_list) + add_constructor (it, I("cons") ); + add_constructor (it, I("nil") ); + assign_subschema (it, I("cons"), I("car"), schema(term) ); + assign_subschema (it, I("cons"), I("cdr"), schema(term_list) ); +end_schema(term_list) + +start_schema(vars) + add_constructor (it, I("var") ); + add_constructor (it, I("nil") ); + assign_subschema (it, I("var"), I("rest"), schema(vars) ); + mark_as_leaf (it, I("var"), I("name") ); +end_schema(vars) + +start_schema(proof) + add_constructor (it, I("done") ); + add_constructor (it, I("step") ); + mark_as_leaf (it, I("step"), I("tactic") ); + assign_subschema (it, I("step"), I("args"), schema(term_list) ); + assign_subschema (it, I("step"), I("rest"), schema(proof) ); +end_schema(proof) + diff --git a/coding/model.h b/coding/model.h @@ -1,9 +1,11 @@ #include "schema.h" -schema *context_schema(void); -schema *attitude_schema(void); -schema *assumption_schema(void); -schema *term_schema(void); -schema *vars_schema(void); -schema *term_list_schema(void); -schema *proof_schema(void); +#define schema(NAME) NAME ## _schema() + +schema *schema(context); +schema *schema(attitude); +schema *schema(assumption); +schema *schema(term); +schema *schema(vars); +schema *schema(term_list); +schema *schema(proof); diff --git a/coding/model.test.c b/coding/model.test.c @@ -0,0 +1,114 @@ +#include <stdbool.h> +#include <assert.h> + +#include "symbol.h" +#include "schema.h" +#include "model.h" +#include "gardener.h" + +#define I intern + +bool +test_existence(void) +{ + assert(schema(context)); + assert(schema(term)); + assert(schema(term_list)); + // if ( schema(vars) == NULL) return false; + // if ( schema(term_list) == NULL) return false; + // if ( schema(proof) == NULL) return false; + return true; +} + +void +test_context(void) +{ + schema *ctx = schema(context); + bool res = true; + + assert (has_key (ctx, I("attitude"), I("name") )); + assert (has_key (ctx, I("attitude"), I("vars") )); + assert (has_key (ctx, I("attitude"), I("pressupositions") )); + assert (has_key (ctx, I("assumption"), I("name") )); + assert (has_key (ctx, I("assumption"), I("judgment") )); + assert (has_key (ctx, I("assumption"), I("proof") )); + + assert (takes_leaf (ctx, I("attitude"), I("name") ) ); + assert (get_subschema (ctx, I("attitude"), I("vars") ) == schema(vars) ); + assert (get_subschema (ctx, I("attitude"), I("pressupositions") ) == schema(term_list) ); + + assert (takes_leaf (ctx, I("assumption"), I("name") ) ); + assert (get_subschema (ctx, I("assumption"), I("judgment") ) == schema(term) ); + assert (get_subschema (ctx, I("assumption"), I("proof") ) == schema(proof) ); +} + +void +test_term(void) +{ + schema *term = schema(term); + assert (is_constructor (term, I("term") ) ); + assert (has_key (term, I("term"), I("head") ) ); + assert (has_key (term, I("term"), I("tail") ) ); + assert (takes_leaf (term, I("term"), I("head") ) ); + assert (get_subschema (term, I("term"), I("tail") ) == schema(term_list) ); +} + +void +test_term_list(void) +{ + schema *tl = schema(term_list); + + assert (is_constructor (tl, I("cons") ) ); + assert (is_constructor (tl, I("nil") ) ); + assert (has_key (tl, I("cons"), I("car") ) ); + assert (has_key (tl, I("cons"), I("cdr") ) ); + assert (get_subschema (tl, I("cons"), I("car") ) == schema(term) ); + assert (get_subschema (tl, I("cons"), I("cdr") ) == schema(term_list) ); +} + +void +test_vars(void) +{ + schema *it = schema(vars); + assert (is_constructor (it, I("var") ) ); + assert (is_constructor (it, I("nil") ) ); + assert (has_key (it, I("var"), I("name") ) ); + assert (has_key (it, I("var"), I("rest") ) ); + assert (takes_leaf (it, I("var"), I("name") ) ); + assert (get_subschema (it, I("var"), I("rest") ) == schema(vars) ); +} + +void +test_proof(void) +{ + schema *it = schema(proof); + assert (is_constructor (it, I("step") ) ); + assert (is_constructor (it, I("done") ) ); + assert (has_key (it, I("step"), I("tactic") ) ); + assert (has_key (it, I("step"), I("args") ) ); + assert (takes_leaf (it, I("step"), I("tactic") ) ); + assert (get_subschema (it, I("step"), I("args") ) == schema(term_list) ); + assert (get_subschema (it, I("step"), I("rest") ) == schema(proof) ); +} + +void +test_use(void) +{ + gardener *g = new_gardener(schema(context)); + + start(g, I("attitude")); + assert(!get_error(g)); +} + +int +main() +{ + test_existence(); + test_context(); + test_term(); + test_term_list(); + test_vars(); + test_proof(); + test_use(); + return 0; +} diff --git a/coding/schema.c b/coding/schema.c @@ -10,6 +10,9 @@ struct schema { bool (*checker)(tree*); }; +struct schema _LEAF = { NULL }; +struct schema *LEAF = &_LEAF; + struct constructor { assoc *subschemas; }; @@ -27,9 +30,6 @@ new_schema(void) return s; } -struct schema _LEAF = { NULL }; -struct schema *LEAF = &_LEAF; - constructor* new_constructor() { @@ -91,6 +91,7 @@ bool (*get_check_function(schema* s))(tree*) void add_constructor(schema* s, symbol c) { + assert(s); assert(!is_constructor(s, c)); constructor *sub = new_constructor(); assoc_set(s->constructors, c, sub); diff --git a/coding/schema.h b/coding/schema.h @@ -14,6 +14,7 @@ void set_check_function(schema*, bool (*)(tree*)); /* USING */ schema* get_subschema(schema*, symbol, symbol); +bool is_constructor(schema*, symbol); bool has_key(schema*, symbol, symbol); bool takes_leaf(schema*, symbol, symbol); bool check(schema*, tree*); diff --git a/coding/symbol.c b/coding/symbol.c @@ -23,7 +23,9 @@ append(char *name) if (len == cap) db = realloc(db, (cap *= 2)*sizeof(char*)); assert(db); - db[len] = name; + db[len] = malloc(sizeof(char)*strlen(name)); + assert(db[len]); + strcpy(db[len], name); return len++; } diff --git a/coding/symbol.test.c b/coding/symbol.test.c @@ -1,4 +1,5 @@ #include "symbol.h" +#include <stdlib.h> #include <stdbool.h> #include <assert.h> #include <string.h> @@ -18,8 +19,34 @@ test_intern_of_repr_is_id() return intern(repr(s)) == s; } +void +test_intern_a_lot_of_strings() +{ + char str[5]; + for (size_t i = 0; i < 1000; i++) { + for (size_t c = 0; c < 5; c++) { + str[c] = 'a' + ((i + c) % 26); + } + (void)intern(str); + } +} + +void +test_intern_many_frames(size_t depth) +{ + if (depth == 0) return; + char str[5]; + for (size_t i = 0; i < 5; i++) str[i] = random(); + symbol s = intern(str); + test_intern_many_frames(depth - 1); + assert(intern(str) == s); + assert(strcmp(repr(s), str) == 0); +} + int main() { assert(test_repr_of_intern_is_iso()); assert(test_intern_of_repr_is_id()); + test_intern_a_lot_of_strings(); + test_intern_many_frames(1000); } diff --git a/coding/test.sh b/coding/test.sh @@ -2,7 +2,7 @@ src=$(ls *.c | grep -v '\.test\.c') -for m in symbol assoc stack tree schema gardener +for m in symbol assoc stack tree schema gardener model do f=$m.test.c out=$(basename $f .c)