starting subt implementation
This commit is contained in:
parent
7d23372846
commit
0344ec69b0
8 changed files with 231 additions and 17 deletions
|
|
@ -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
|
||||
)
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
};
|
||||
|
|
|
|||
6
include/spho/subt.h
Normal file
6
include/spho/subt.h
Normal file
|
|
@ -0,0 +1,6 @@
|
|||
#ifndef _SPHO_SUBT_H
|
||||
#define _SPHO_SUBT_H
|
||||
|
||||
#include "spho/bind.h"
|
||||
|
||||
#endif /* ifndef _SPHO_SUBT_H */
|
||||
|
|
@ -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),
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
205
src/spho/subt.c
Normal file
205
src/spho/subt.c
Normal file
|
|
@ -0,0 +1,205 @@
|
|||
/*
|
||||
* Subtyping
|
||||
*/
|
||||
#include <stdlib.h>
|
||||
|
||||
#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);
|
||||
}
|
||||
|
||||
Loading…
Add table
Add a link
Reference in a new issue