diff --git a/CMakeLists.txt b/CMakeLists.txt index f22b1e6..81de430 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -27,6 +27,7 @@ set(SPHO_HEADER ${SPHO_HEADER_DIR}/err.h ${SPHO_HEADER_DIR}/scope.h ${SPHO_HEADER_DIR}/spho.h + ${SPHO_HEADER_DIR}/subt.h ${SPHO_HEADER_DIR}/tp.h ) @@ -34,6 +35,7 @@ set(SPHO_SRC ${SRC_DIR}/spho/bind.c ${SRC_DIR}/spho/ctx.c ${SRC_DIR}/spho/scope.c + ${SRC_DIR}/spho/subt.c ${SRC_DIR}/spho/tp.c ) diff --git a/include/spho/bind.h b/include/spho/bind.h index 3cdd75d..4e175c3 100644 --- a/include/spho/bind.h +++ b/include/spho/bind.h @@ -31,11 +31,6 @@ struct spho_prebind { struct spho_prebind_pair *binds; }; -struct spho_bind { - struct spho_prebind *local; - struct spho_bind *parent; -}; - struct spho_prebind *spho_prebind_create(struct spho_scope *); int spho_prebind_undef(struct spho_prebind *, const struct spho_nom *); @@ -48,6 +43,12 @@ int spho_prebind_member_tp(struct spho_prebind *, const struct spho_nom *, struct spho_prebind *spho_prebind_dupl(const struct spho_prebind *); -void spho_prebind_destroy(struct spho_prebind *); +void spho_prebind_free(struct spho_prebind *); + + +struct spho_bind { + struct spho_prebind *loc; + struct spho_bind *parent; +}; #endif diff --git a/include/spho/scope.h b/include/spho/scope.h index a9f7526..ff682c4 100644 --- a/include/spho/scope.h +++ b/include/spho/scope.h @@ -122,7 +122,7 @@ struct spho_scope { struct spho_nom_l noms; struct spho_tp_alloc_l tps; - struct spho_prebind *bind; + struct spho_prebind *bind_loc; SLIST_ENTRY(spho_scope) next; }; diff --git a/include/spho/subt.h b/include/spho/subt.h new file mode 100644 index 0000000..c185107 --- /dev/null +++ b/include/spho/subt.h @@ -0,0 +1,6 @@ +#ifndef _SPHO_SUBT_H +#define _SPHO_SUBT_H + +#include "spho/bind.h" + +#endif /* ifndef _SPHO_SUBT_H */ diff --git a/src/msph/sphophi.c b/src/msph/sphophi.c index 0e3c662..a9dec26 100644 --- a/src/msph/sphophi.c +++ b/src/msph/sphophi.c @@ -419,7 +419,7 @@ msph_tree_sphophi_tp_prebind(struct spho_scope *sc, if (HAS_PARAMS(tpdef)) { SPHO_ASSERT(HAS_SCOPE(tpdef)); SPHO_ASSERT(SCOPE(tpdef) != NULL); - SPHO_ASSERT(SCOPE(tpdef)->bind != NULL); + SPHO_ASSERT(SCOPE(tpdef)->bind_loc != NULL); STAILQ_FOREACH(name, &tpdef->params, entries) { if (spho_scope_prebind_undef(SCOPE(tpdef), diff --git a/src/spho/bind.c b/src/spho/bind.c index 714b323..fc2258b 100644 --- a/src/spho/bind.c +++ b/src/spho/bind.c @@ -158,7 +158,7 @@ spho_prebind_dupl(const struct spho_prebind *bind) } void -spho_prebind_destroy(struct spho_prebind *bind) +spho_prebind_free(struct spho_prebind *bind) { free(bind->binds); free(bind); diff --git a/src/spho/scope.c b/src/spho/scope.c index 589b8d7..da5c679 100644 --- a/src/spho/scope.c +++ b/src/spho/scope.c @@ -28,7 +28,7 @@ spho_scope_init(struct spho_scope *sc, struct spho_ctx *ctx, TAILQ_INIT(&sc->tps); - sc->bind = NULL; + sc->bind_loc = NULL; return (0); } @@ -42,9 +42,9 @@ spho_scope_term(struct spho_scope *sc) sc->parent = NULL; - if (sc->bind == NULL) - spho_prebind_destroy(sc->bind); - sc->bind = NULL; + if (sc->bind_loc == NULL) + spho_prebind_free(sc->bind_loc); + sc->bind_loc = NULL; } struct spho_scope * @@ -177,7 +177,7 @@ spho_scope_nom_lookup_str_strict(struct spho_scope *sc, const char *nomstr, int spho_scope_prebind_init(struct spho_scope *sc) { - if ((sc->bind = spho_prebind_create(sc)) + if ((sc->bind_loc = spho_prebind_create(sc)) == NULL) { return (-1); } @@ -194,7 +194,7 @@ spho_scope_prebind_tp(struct spho_scope *sc, struct spho_nom *nom, return (-1); } - return (spho_prebind_tp(sc->bind, nom, tp)); + return (spho_prebind_tp(sc->bind_loc, nom, tp)); } int @@ -206,7 +206,7 @@ spho_scope_prebind_tp_op(struct spho_scope *sc, struct spho_nom *nom, return (-1); } - return (spho_prebind_tp_op(sc->bind, nom, tp_op)); + return (spho_prebind_tp_op(sc->bind_loc, nom, tp_op)); } int @@ -217,7 +217,7 @@ spho_scope_prebind_undef(struct spho_scope *sc, struct spho_nom *nom) return (-1); } - return (spho_prebind_undef(sc->bind, nom)); + return (spho_prebind_undef(sc->bind_loc, nom)); } static int diff --git a/src/spho/subt.c b/src/spho/subt.c new file mode 100644 index 0000000..062e021 --- /dev/null +++ b/src/spho/subt.c @@ -0,0 +1,205 @@ +/* + * Subtyping + */ +#include + +#include "spho/bind.h" +#include "spho/bind.h" +#include "spho/spho.h" + +#include "spho/subt.h" + +struct bound_tp { + struct spho_bind *bind; + const struct spho_tp *tp; +}; + +struct seqnt { + struct spho_ctx *ctx; + + size_t sz; + size_t filled; + struct bound_tp *elms; +}; + +struct seqnt_tstl { + struct seqnt left; + struct seqnt right; +}; + + +static struct bound_tp *spho_bound_tp(const struct spho_tp *); + + +/* read scopes and create bound type */ +struct bound_tp * +spho_bound_tp(const struct spho_tp *tp) +{ + struct spho_scope *sc; + struct spho_bind *bind, *more_bind; + + struct bound_tp *ret; + + SPHO_PRECOND(tp != NULL); + SPHO_PRECOND(tp->sc != NULL); + SPHO_PRECOND(tp->sc->bind_loc != NULL); + + sc = tp->sc; + bind = NULL; + + if ((ret = calloc(1, sizeof(*ret))) == NULL) { + SPHO_ERR(sc->ctx, SPHO_ERR_SYS); + return (NULL); + } + ret->tp = tp; + + + if ((ret->bind = calloc(1, sizeof(*ret->bind))) == NULL) { + SPHO_ERR(sc->ctx, SPHO_ERR_SYS); + goto err; + } + + /* initialize parent and duplicate scope-local bindings */ + ret->bind->parent = NULL; + if ((ret->bind->loc = spho_prebind_dupl(sc->bind_loc)) == NULL) { + goto err; + } + + /* iterate up through parent scopes and gather their local bindings */ + bind = ret->bind; + while ((sc = sc->parent) != NULL) { + if ((more_bind = calloc(1, sizeof(*more_bind))) == NULL) { + SPHO_ERR(sc->ctx, SPHO_ERR_SYS); + goto err; + } + more_bind->parent = NULL; + if ((more_bind->loc = spho_prebind_dupl(sc->bind_loc)) + == NULL) { + goto err; + } + bind->parent = more_bind; + bind = bind->parent; + } + + return (ret); + +err: + while (ret->bind != NULL) { + bind = ret->bind; + ret->bind = ret->bind->parent; + + spho_prebind_free(bind->loc); + free(bind); + } + + return (NULL); +} + +static struct seqnt * +seqnt_alloc(struct spho_ctx *ctx, size_t initsz) +{ + struct seqnt *seq; + if (initsz == 0) + initsz = 32; /* just feels good */ + + if ((seq = calloc(1, sizeof(*seq))) == NULL) { + SPHO_ERR(ctx, SPHO_ERR_SYS); + return (NULL); + } + seq->ctx = ctx; + + if ((seq->elms = calloc(initsz, sizeof(*seq->elms))) == NULL) { + SPHO_ERR(seq->ctx, SPHO_ERR_SYS); + goto err; + } + + seq->sz = initsz; + seq->filled = 0; + + return (seq); +err: + if (seq != NULL) { + if (seq->elms != NULL) + free(seq->elms); + free(seq); + } + + return (NULL); +} + +static int +seqnt_makebig(struct seqnt *seq) +{ + size_t new_sz; + struct bound_tp *new_elms; + + SPHO_PRECOND(seq != NULL); + SPHO_PRECOND(seq->sz > 0); + SPHO_PRECOND(seq->sz <= (SIZE_MAX >> 1)); + SPHO_PRECOND(seq->elms != NULL); + + new_sz = seq->sz << 1; + + if ((new_elms = realloc(seq->elms, new_sz)) == NULL) { + SPHO_ERR(seq->ctx, SPHO_ERR_SYS); + return (-1); + } + + seq->sz = new_sz; + seq->elms = new_elms; + + return (0); +} + +static int +seqnt_insert_from_ptr(struct seqnt *seq, struct bound_tp *elm) +{ + SPHO_PRECOND(seq->filled <= seq->sz); + + if (seq->filled >= seq->sz && (seqnt_makebig(seq) == -1)) + return (-1); + + seq->elms[seq->filled++] = *elm; + + SPHO_POSTCOND(seq->filled <= seq->sz); + + return (0); +} + +static int +seqnt_insert_bind_tp(struct seqnt *seq, struct spho_bind *elm_bind, + struct spho_tp *elm_tp) +{ + SPHO_PRECOND(seq->filled <= seq->sz); + + if (seq->filled >= seq->sz && (seqnt_makebig(seq) == -1)) + return (-1); + + seq->elms[seq->filled++] = (struct bound_tp){ elm_bind, elm_tp }; + + SPHO_POSTCOND(seq->filled <= seq->sz); + + return (0); +} + + +int +spho_is_subt(struct spho_tp *tp_left, struct spho_tp *tp_right) +{ + struct bound_tp *left, *right; + + if ((left = spho_bound_tp(tp_left)) == NULL) + return (-1); + if ((right = spho_bound_tp(tp_right)) == NULL) + return (-1); + + // TODO check well-definedness (e.g. no undefs) + + // XXX skip boxing step + + // TODO create seqnt and seqnt_tstl + // TODO run decider + + return (-1); +} +