lnsol/log-e-sappho
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

decisions decisions decisions...

Browse source
This commit is contained in:
Ellen Arvidsson 2025-06-25 17:10:11 +02:00
parent 0344ec69b0
commit d4106c7004
3 changed files with 90 additions and 53 deletions
Download patch file Download diff file Expand all files Collapse all files

12
include/spho/spho.h
View file

@ -27,20 +27,20 @@ do { \
#define SPHO_STRINGIFY(a) #a
#define SPHO_MACRO_STR(b) SPHO_STRINGIFY(b)
#define __LINE__S SPHO_MACRO_STR(__LINE__)
#define SPHO_RIP(msg) \
#define SPHO_RIP(msg, ...) \
do { \
fprintf(stderr, "SPHO_RIP(" msg ")@" \
__FILE__ ":" __LINE__S \
" failed. Aborting.\n"); \
fprintf(stderr, "SPHO_RIP(" msg ")@" \
__FILE__ ":" __LINE__S \
" failed. Aborting.\n" __VA_OPT__(,) __VA_ARGS__); \
abort(); \
} while (0)
#ifdef SPHO_DEBUG
#define __LINE__S SPHO_MACRO_STR(__LINE__)
#define SPHO_PRECOND(cond) \
do { \
if (! (cond) ) { \

5
include/spho/subt.h
View file

@ -1,6 +1,9 @@
#ifndef _SPHO_SUBT_H
#define _SPHO_SUBT_H
#include "spho/bind.h"
#include "spho/scope.h"
int spho_is_subt(struct spho_ctx *, const struct spho_tp *,
const struct spho_tp *);
#endif /* ifndef _SPHO_SUBT_H */

126
src/spho/subt.c
View file

@ -9,36 +9,39 @@
#include "spho/subt.h"
struct bound_tp {
/* bound type */
struct bound {
struct spho_bind *bind;
const struct spho_tp *tp;
};
struct seqnt {
/* sequent */
struct sqnt {
struct spho_ctx *ctx;
size_t sz;
size_t filled;
struct bound_tp *elms;
struct bound *elms;
};
struct seqnt_tstl {
struct seqnt left;
struct seqnt right;
/* sequent turnstile */
struct tstl {
struct sqnt left;
struct sqnt right;
};
static struct bound_tp *spho_bound_tp(const struct spho_tp *);
static struct bound *bound_tp(const struct spho_tp *);
/* read scopes and create bound type */
struct bound_tp *
spho_bound_tp(const struct spho_tp *tp)
struct bound *
bound_tp(const struct spho_tp *tp)
{
struct spho_scope *sc;
struct spho_bind *bind, *more_bind;
struct bound_tp *ret;
struct bound *ret;
SPHO_PRECOND(tp != NULL);
SPHO_PRECOND(tp->sc != NULL);
@ -95,17 +98,12 @@ err:
return (NULL);
}
static struct seqnt *
seqnt_alloc(struct spho_ctx *ctx, size_t initsz)
static int
sqnt_init(struct spho_ctx *ctx, size_t initsz, struct sqnt *seq)
{
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) {
@ -116,22 +114,20 @@ seqnt_alloc(struct spho_ctx *ctx, size_t initsz)
seq->sz = initsz;
seq->filled = 0;
return (seq);
return (0);
err:
if (seq != NULL) {
if (seq->elms != NULL)
free(seq->elms);
free(seq);
}
if (seq->elms != NULL)
free(seq->elms);
seq->elms = NULL;
return (NULL);
return (-1);
}
static int
seqnt_makebig(struct seqnt *seq)
sqnt_makebig(struct sqnt *seq)
{
size_t new_sz;
struct bound_tp *new_elms;
struct bound *new_elms;
SPHO_PRECOND(seq != NULL);
SPHO_PRECOND(seq->sz > 0);
@ -152,11 +148,11 @@ seqnt_makebig(struct seqnt *seq)
}
static int
seqnt_insert_from_ptr(struct seqnt *seq, struct bound_tp *elm)
sqnt_add_bound(struct sqnt *seq, struct bound *elm)
{
SPHO_PRECOND(seq->filled <= seq->sz);
if (seq->filled >= seq->sz && (seqnt_makebig(seq) == -1))
if (seq->filled >= seq->sz && (sqnt_makebig(seq) == -1))
return (-1);
seq->elms[seq->filled++] = *elm;
@ -167,38 +163,76 @@ seqnt_insert_from_ptr(struct seqnt *seq, struct bound_tp *elm)
}
static int
seqnt_insert_bind_tp(struct seqnt *seq, struct spho_bind *elm_bind,
struct spho_tp *elm_tp)
tstl_init(struct spho_ctx *ctx, size_t lsz, size_t rsz,
struct tstl *ts)
{
SPHO_PRECOND(seq->filled <= seq->sz);
if (seq->filled >= seq->sz && (seqnt_makebig(seq) == -1))
if (sqnt_init(ctx, lsz, &ts->left) == -1)
return (-1);
if (sqnt_init(ctx, rsz, &ts->right) == -1)
return (-1);
seq->elms[seq->filled++] = (struct bound_tp){ elm_bind, elm_tp };
SPHO_POSTCOND(seq->filled <= seq->sz);
return (0);
}
static struct tstl *
tstl_alloc(struct spho_ctx *ctx)
{
struct tstl *ts;
if ((ts = calloc(1, sizeof(*ts))) == NULL) {
SPHO_ERR(ctx, SPHO_ERR_SYS);
return (NULL);
}
if (tstl_init(ctx, 0, 0, ts) == -1) {
free(ts);
return (NULL);
}
return (ts);
}
static int
tstl_add_left(struct tstl *ts, struct bound *tp)
{
return (sqnt_add_bound(&ts->left, tp));
}
static int
tstl_add_right(struct tstl *ts, struct bound *tp)
{
return (sqnt_add_bound(&ts->right, tp));
}
static int
tstl_decide(struct tstl *ts)
{
SPHO_RIP("implement");
}
int
spho_is_subt(struct spho_tp *tp_left, struct spho_tp *tp_right)
spho_is_subt(struct spho_ctx *ctx, const struct spho_tp *tp_left,
const struct spho_tp *tp_right)
{
struct bound_tp *left, *right;
struct tstl ts;
struct bound *left, *right;
if ((left = spho_bound_tp(tp_left)) == NULL)
if ((left = bound_tp(tp_left)) == NULL)
return (-1);
if ((right = spho_bound_tp(tp_right)) == NULL)
if ((right = bound_tp(tp_right)) == NULL)
return (-1);
// TODO check well-definedness (e.g. no undefs)
// TODO check well-definedness of types (e.g. no undefs)
// XXX skip boxing step
// TODO create seqnt and seqnt_tstl
// TODO run decider
if ((tstl_init(ctx, 0, 0, &ts)) == -1)
return (-1);
if (tstl_add_left(&ts, left) == -1)
return (-1);
if (tstl_add_right(&ts, right) == -1)
return (-1);
if (tstl_decide(&ts) == -1)
return (-1);
return (-1);
}