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

queue problems

Browse source
This commit is contained in:
Ellen Arvidsson 2025-04-11 23:16:29 +02:00
parent 2ac5491b44
commit 8dd2fe0e34
10 changed files with 427 additions and 59 deletions
Download patch file Download diff file Expand all files Collapse all files

8
.gitignore vendored
View file

@ -54,3 +54,11 @@ dkms.conf
# CMake build directory # CMake build directory
build/ build/
# vim
.*.swp
.*.swo
# vscode
.vscode
.cache

5
CMakeLists.txt
View file

@ -11,12 +11,15 @@ set(SPHO_HEADER_DIR ${INCLUDE_DIR}/spho)
set(SPHO_HEADER set(SPHO_HEADER
${SPHO_HEADER_DIR}/data.h ${SPHO_HEADER_DIR}/data.h
${SPHO_HEADER_DIR}/err.h
${SPHO_HEADER_DIR}/loc.h
${SPHO_HEADER_DIR}/parse.h ${SPHO_HEADER_DIR}/parse.h
${SPHO_HEADER_DIR}/spho.h
${SPHO_HEADER_DIR}/tp.h ${SPHO_HEADER_DIR}/tp.h
) )
set(SPHO_SRC set(SPHO_SRC
${SRC_DIR}/spho/tp.c ${SRC_DIR}/spho/ctx.c
) )
add_library(spho STATIC ${SPHO_HEADER} ${SPHO_SRC}) add_library(spho STATIC ${SPHO_HEADER} ${SPHO_SRC})

25
include/spho/ctx.h Normal file
View file

@ -0,0 +1,25 @@
#ifndef _SPHO_CTX_H
#define _SPHO_CTX_H
#include "spho/data.h"
struct spho_ctx {
int err;
int err_info;
struct spho_nom_l noms;
struct spho_const_l cnsts;
#ifdef SPHO_DEBUG
char filebuf[SPHO_ERR_FILEBUF_LEN];
int errline;
#else
char errbuf[SPHO_ERR_BUF_LEN];
#endif
};
struct spho_ctx *spho_ctx_create(void);
void spho_ctx_destroy(struct spho_ctx *);
char *spho_ctx_strerror(struct spho_ctx *);
#endif

32
include/spho/data.h
View file

@ -1,4 +1,36 @@
#ifndef _SPHO_DATA_H #ifndef _SPHO_DATA_H
#define _SPHO_DATA_H #define _SPHO_DATA_H
#include <sys/queue.h>
struct spho_name {
char str[128];
};
struct spho_var {
struct spho_name name;
};
struct spho_cnst {
struct spho_name name;
};
struct spho_nom {
struct spho_name name;
};
struct spho_nom_le {
struct spho_nom nom;
SLIST_ENTRY(spho_nom_le) next;
};
struct spho_const_le {
struct spho_cnst cnst;
SLIST_ENTRY(spho_const_le) next;
};
SLIST_HEAD(spho_nom_l, struct spho_nom_le);
SLIST_HEAD(spho_const_l, struct spho_const_le);
#endif #endif

67
include/spho/err.h Normal file
View file

@ -0,0 +1,67 @@
#ifndef _SPHO_ERR_H
#define _SPHO_ERR_H
#define SPHO_ERR_SYSTEM 0x000001
#define SPHO_ERR_INTERNAL 0x010001
#define SPHO_ERR_IS_SYSERR(err) (SPHO_ERR_SYSTEM == err)
#ifdef SPHO_DEBUG
#define SPHO_ERR(ctx, err) \
do { \
ctx->err = err; \
if (err == SPHO_ERR_SYSTEM) \
ctx->err_info = errno; \
snprintf(ctx->filebuf, sizeof(ctx->filebuf), "%s", \
__FILE__); \
ctx->errline = __LINE__; \
} while (0)
#else /* SPHO_DEBUG */
#define SPHO_ERR(ctx, err) \
do { \
ctx->err = err; \
if (err == SPHO_ERR_SYSTEM) \
ctx->err_info = errno; \
} while (0)
#endif /* SPHO_DEBUG */
/* debug stuff */
#ifdef SPHO_DEBUG
/* PRECOND/ASSERT/POSTCOND */
#define SPHO_PRECOND(cond) do { \
if (! (cond) ) { \
fprintf(stderr, "SPHO_PRECOND(" #cond ")@" __FILE__ ":" __LINE__ \
" failed. Aborting."); \
abort(); \
} \
} while (0)
#define SPHO_ASSERT(cond) do { \
if (! (cond) ) { \
fprintf(stderr, "SPHO_ASSERT(" #cond ")@" __FILE__ ":" __LINE__ \
" failed. Aborting."); \
abort(); \
} \
} while (0)
#define SPHO_POSTCOND(cond) do { \
if (! (cond) ) { \
fprintf(stderr, "SPHO_POSTCOND(" #cond ")@" __FILE__ ":" __LINE__ \
" failed. Aborting."); \
abort(); \
} \
} while (0)
#else
#define SPHO_PRECOND(cond)
#define SPHO_ASSERT(cond)
#define SPHO_POSTCOND(cond)
#endif
#endif

34
include/spho/loc.h Normal file
View file

@ -0,0 +1,34 @@
#ifndef _SPHO_LOC_H
#define _SPHO_LOC_H
#define SPHO_LOCTYPE_LINE 1
#define SPHO_LOCTYPE_LINE_COL 2
struct spho_loc_line {
char *fpath;
unsigned int lineno;
};
struct spho_loc_line {
char *fpath;
unsigned int lineno;
unsigned int colno;
};
union spho_loc_info {
struct spho_loc_line line;
};
struct spho_loc {
struct spho_ctx *ctx;
int loctype;
union spho_loc_info locinfo;
};
char *spho_loc_str(struct spho_loc *);
struct spho_loc *spho_loc_create_line(struct spho_ctx *, char *, int);
struct spho_loc *spho_loc_create_linecol(struct spho_ctx *, char *, int, int);
void spho_loc_destroy(struct spho_loc *);
#endif

32
include/spho/spho.h Normal file
View file

@ -0,0 +1,32 @@
#ifndef _SPHO_SPHO_H
#define _SPHO_SPHO_H
#include <sys/queue.h>
#include "spho/err.h"
#include "spho/data.h"
#define SPHO_ERR_BUF_LEN 2048
#define SPHO_ERR_FILEBUF_LEN 128
struct spho_ctx {
int err;
int err_info;
struct spho_nom_l noms;
struct spho_const_l cnsts;
#ifdef SPHO_DEBUG
char filebuf[SPHO_ERR_FILEBUF_LEN];
int errline;
#else
char errbuf[SPHO_ERR_BUF_LEN];
#endif
};
struct spho_ctx *spho_ctx_create(void);
void spho_ctx_destroy(struct spho_ctx *);
char *spho_ctx_strerror(struct spho_ctx *);
#endif

96
include/spho/tp.h
View file

@ -1,43 +1,14 @@
#ifndef _SPHO_TP_H #ifndef _SPHO_TP_H
#define _SPHO_TP_H #define _SPHO_TP_H
#define SPHO_TP_FORM_UNKNOWN 0x00
#define SPHO_TP_FORM_DISJ 0x10
#define SPHO_TP_FORM_CONJ 0x11
#define SPHO_TP_FORM_IMPL 0x12
#define SPHO_TP_FORM_BOX 0x13
#define SPHO_TP_FORM_FORALL 0x14
#define SPHO_TP_FORM_ALIAS 0x15
#define SPHO_TP_FORM_FALSE 0x20
#define SPHO_TP_FORM_TRUE 0x21
#define SPHO_TP_FORM_VAR 0x22
#define SPHO_TP_FORM_NOM 0x23
#define SPHO_TP_FORM_REC 0x23
// TODO explain
#define SPHO_TP_FORM_SUB 0x96
/* base defs */ /* base defs */
struct spho_name {
char str[128];
};
struct spho_var {
struct spho_name name;
};
struct spho_alias { struct spho_alias {
struct spho_name name; struct spho_name name;
struct spho_tp *tp;
}; };
struct spho_nominal { struct spho_rec {
struct spho_name name;
};
struct spho_record {
struct spho_name mname; struct spho_name mname;
struct spho_tp *tp; struct spho_tp *tp;
}; };
@ -66,12 +37,16 @@ struct tp_const_data {
struct spho_const *c; struct spho_const *c;
}; };
struct tp_var_data {
struct spho_var *v;
};
struct tp_nominal_data { struct tp_nominal_data {
struct spho_nominal *name; struct spho_nom *n;
}; };
struct tp_record_data { struct tp_record_data {
struct spho_record *r; struct spho_rec *r;
}; };
/* type data union */ /* type data union */
@ -81,14 +56,69 @@ union tp_data {
struct tp_forall_data fa; struct tp_forall_data fa;
struct tp_alias_data alias; struct tp_alias_data alias;
struct tp_const_data cnst; struct tp_const_data cnst;
struct tp_var_data var;
struct tp_nominal_data nom; struct tp_nominal_data nom;
struct tp_record_data rec; struct tp_record_data rec;
}; };
#define SPHO_TP_FORM_UNKNOWN 0x00
#define SPHO_TP_FORM_DISJ 0x10
#define SPHO_TP_FORM_CONJ 0x11
#define SPHO_TP_FORM_IMPL 0x12
#define SPHO_TP_FORM_BOX 0x13
#define SPHO_TP_FORM_FORALL 0x14
#define SPHO_TP_FORM_ALIAS 0x15
#define SPHO_TP_FORM_FALSE 0x20
#define SPHO_TP_FORM_TRUE 0x21
#define SPHO_TP_FORM_VAR 0x22
#define SPHO_TP_FORM_NOM 0x23
#define SPHO_TP_FORM_REC 0x23
// TODO explain
#define SPHO_TP_FORM_SUB 0x96
/* sappho type */ /* sappho type */
struct spho_tp { struct spho_tp {
int form; int form;
union tp_data data; union tp_data data;
}; };
struct spho_nom *spho_nom_add(struct spho_ctx *, char *, size_t);
struct spho_nom *spho_nom_get_or_add(struct spho_ctx *, char *, size_t);
// struct spho_nom *spho_tp_nom_get(char *, size_t);
struct spho_var *spho_var_create(struct spho_ctx *, char *, size_t);
struct spho_var *spho_var_get(struct spho_ctx *, char *, size_t);
struct spho_alias *spho_alias_add(struct spho_ctx *, char *, size_t);
struct spho_alias *spho_alias_get(struct spho_ctx *, char *, size_t);
struct spho_tp *spho_tp_create_disj(struct spho_ctx *, struct spho_tp *,
struct spho_tp *, struct spho_tp *);
struct spho_tp *spho_tp_create_conj(struct spho_ctx *, struct spho_tp *,
struct spho_tp *, struct spho_tp *);
struct spho_tp *spho_tp_create_impl(struct spho_ctx *, struct spho_tp *,
struct spho_tp *, struct spho_tp *);
struct spho_tp *spho_tp_create_box(struct spho_ctx *, struct spho_tp *,
struct spho_tp *);
struct spho_tp *spho_tp_create_forall(struct spho_ctx *, struct spho_name *,
struct spho_tp *);
struct spho_tp *spho_tp_create_alias(struct spho_ctx *, struct spho_alias *,
struct spho_tp *);
struct spho_tp *spho_tp_create_const(struct spho_ctx *, struct spho_const *);
struct spho_tp *spho_tp_create_nominal(struct spho_ctx *,
struct spho_nom *);
struct spho_tp *spho_tp_create_var(struct spho_ctx *, struct spho_var *);
struct spho_tp *spho_tp_create_record(struct spho_ctx *, struct spho_rec *);
//struct spho_tp *spho_tp_create_sub(struct spho_ctx *, struct spho_tp *,
// struct spho_tp *);
void spho_tp_destroy(struct spho_tp*);
void spho_tp_free(struct spho_tp *);
#endif #endif

126
src/spho/ctx.c Normal file
View file

@ -0,0 +1,126 @@
#include <stdio.h>
#include <string.h>
#include "spho/ctx.h"
static const char *spho_ctx_sys_strerror(struct spho_ctx *);
static const char *spho_ctx_intern_strerror(struct spho_ctx *);
struct spho_err {
int num;
char *msg;
};
struct spho_err spho_errmsgs[] = {
{ SPHO_ERR_SYSTEM, "spho system error" },
{ SPHO_ERR_INTERNAL, "spho internal error" },
{ -1, NULL }
};
struct spho_ctx *
spho_ctx_create(void)
{
struct spho_ctx *c;
if ((c = malloc(sizeof(struct spho_ctx))) == NULL)
return (NULL);
c->err = 0;
c->err_info = 0;
SLIST_INIT(&c->noms);
SLIST_INIT(&c->cnsts);
return (c);
}
void
spho_ctx_destroy(struct spho_ctx *ctx)
{
struct spho_nom_le *nom;
struct spho_cnst_le *cnst;
SPHO_PRECOND(ctx != NULL);
while (! SLIST_EMPTY(&c->noms)) {
nom = SLIST_FIRST(&c->noms);
SLIST_REMOVE_HEAD(&c->noms, next);
free(nom);
}
while (! SLIST_EMPTY(&c->cnsts)) {
cnst = SLIST_FIRST(&c->cnsts);
SLIST_REMOVE_HEAD(&c->cnsts, next);
free(cnst);
}
}
const char *
spho_ctx_strerror(struct spho_ctx *ctx)
{
char *msg;
int res;
SPHO_PRECOND(ctx != NULL);
msg = NULL;
if (SPHO_ERR_IS_SYSERR(ctx->err))
msg = spho_ctx_sys_strerror(ctx);
else
msg = spho_ctx_intern_strerror(ctx);
SPHO_POSTCOND(msg != NULL);
return (msg);
}
static const char *
spho_ctx_sys_strerror(struct spho_ctx *ctx)
{
#ifdef SPHO_DEBUG
res = snprintf(ctx->errbuf, sizeof(ctx->errbuf),
"%s:%d:spho_syserr:%s (%d)", ctx->filebuf, ctx->errline,
strerror(ctx->err_info), ctx->err_info);
if (res >= sizeof(ctx->errbuf))
ctx->errbuf[sizeof(ctx->errbuf) - 1] = '\0';
#else
res = snprintf(ctx->errbuf, sizeof(ctx->errbuf),
"spho_syserr:%s (%d)", ctx->filebuf, ctx->errline,
strerror(ctx->err_info), ctx->err_info);
if (res >= sizeof(ctx->errbuf))
ctx->errbuf[sizeof(ctx->errbuf) - 1] = '\0';
#endif
return (ctx->errbuf);
}
static const char *
spho_ctx_intern_strerror(struct spho_ctx *ctx)
{
int i;
int res;
SPHO_PRECOND(ctx != NULL);
for (i = 0; spho_errmsgs[i].msg != NULL; i++) {
if (spho_errmsgs[i].err == ctx->err) {
#ifdef SPHO_DEBUG
res = snprintf(ctx->errbuf, sizeof(ctx->errbuf),
"%s:%d:spho_intern_err:%s", ctx->filebuf,
ctx->errline, spho_errmsgs[i].msg);
#else
res = snprintf(ctx->errbuf, sizeof(ctx->errbuf),
"spho_intern_err:%s", ctx->errbuf);
#endif
}
}
SPHO_POSTCOND(res != -1);
return (ctx->errbuf);
}

11
src/spho/tp.c
View file

@ -1,2 +1,13 @@
#include "spho/tp.h" #include "spho/tp.h"
struct spho_nom *
spho_nom_add(struct spho_ctx *ctx, char *nom, size_t nomlen)
{
}
//struct spho_tp *
//spho_tp_create_disj(struct spho_ctx *, struct spho_tp *, struct spho_tp *,
// struct spho_tp *)
//{
//
//}