diff --git a/.gitignore b/.gitignore index 047d12e..dd51cb4 100644 --- a/.gitignore +++ b/.gitignore @@ -54,3 +54,11 @@ dkms.conf # CMake build directory build/ + +# vim +.*.swp +.*.swo + +# vscode +.vscode +.cache diff --git a/CMakeLists.txt b/CMakeLists.txt index b72bfd6..573a310 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -10,13 +10,16 @@ set(SRC_DIR src) set(SPHO_HEADER_DIR ${INCLUDE_DIR}/spho) set(SPHO_HEADER - ${SPHO_HEADER_DIR}/data.h - ${SPHO_HEADER_DIR}/parse.h - ${SPHO_HEADER_DIR}/tp.h + ${SPHO_HEADER_DIR}/data.h + ${SPHO_HEADER_DIR}/err.h + ${SPHO_HEADER_DIR}/loc.h + ${SPHO_HEADER_DIR}/parse.h + ${SPHO_HEADER_DIR}/spho.h + ${SPHO_HEADER_DIR}/tp.h ) set(SPHO_SRC - ${SRC_DIR}/spho/tp.c + ${SRC_DIR}/spho/ctx.c ) add_library(spho STATIC ${SPHO_HEADER} ${SPHO_SRC}) diff --git a/include/spho/ctx.h b/include/spho/ctx.h new file mode 100644 index 0000000..746126c --- /dev/null +++ b/include/spho/ctx.h @@ -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 diff --git a/include/spho/data.h b/include/spho/data.h index 7440a4d..17f1541 100644 --- a/include/spho/data.h +++ b/include/spho/data.h @@ -1,4 +1,36 @@ #ifndef _SPHO_DATA_H #define _SPHO_DATA_H -#endif \ No newline at end of file +#include + +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 diff --git a/include/spho/err.h b/include/spho/err.h new file mode 100644 index 0000000..f92687a --- /dev/null +++ b/include/spho/err.h @@ -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 diff --git a/include/spho/loc.h b/include/spho/loc.h new file mode 100644 index 0000000..05f6008 --- /dev/null +++ b/include/spho/loc.h @@ -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 \ No newline at end of file diff --git a/include/spho/spho.h b/include/spho/spho.h new file mode 100644 index 0000000..900444f --- /dev/null +++ b/include/spho/spho.h @@ -0,0 +1,32 @@ +#ifndef _SPHO_SPHO_H +#define _SPHO_SPHO_H + +#include + +#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 diff --git a/include/spho/tp.h b/include/spho/tp.h index 09a0d18..0098237 100644 --- a/include/spho/tp.h +++ b/include/spho/tp.h @@ -1,94 +1,124 @@ #ifndef _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 */ -struct spho_name { - char str[128]; -}; - -struct spho_var { - struct spho_name name; -}; struct spho_alias { - struct spho_name name; + struct spho_name name; + struct spho_tp *tp; }; -struct spho_nominal { - struct spho_name name; -}; - -struct spho_record { - struct spho_name mname; - struct spho_tp *tp; +struct spho_rec { + struct spho_name mname; + struct spho_tp *tp; }; /* type data */ struct tp_bin_data { - struct spho_tp *left; - struct spho_tp *right; + struct spho_tp *left; + struct spho_tp *right; }; struct tp_box_data { - struct spho_tp *tp; + struct spho_tp *tp; }; struct tp_forall_data { - struct spho_var *var; - struct spho_tp *tp; + struct spho_var *var; + struct spho_tp *tp; }; struct tp_alias_data { - struct spho_alias *alias; - struct spho_tp_list *l; + struct spho_alias *alias; + struct spho_tp_list *l; }; 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 spho_nominal *name; + struct spho_nom *n; }; struct tp_record_data { - struct spho_record *r; + struct spho_rec *r; }; /* type data union */ union tp_data { - struct tp_bin_data binop; - struct tp_box_data box; - struct tp_forall_data fa; - struct tp_alias_data alias; - struct tp_const_data cnst; - struct tp_nominal_data nom; - struct tp_record_data rec; + struct tp_bin_data binop; + struct tp_box_data box; + struct tp_forall_data fa; + struct tp_alias_data alias; + struct tp_const_data cnst; + struct tp_var_data var; + struct tp_nominal_data nom; + 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 */ struct spho_tp { - int form; - union tp_data data; + int form; + union tp_data data; }; -#endif \ No newline at end of file +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 diff --git a/src/spho/ctx.c b/src/spho/ctx.c new file mode 100644 index 0000000..938863f --- /dev/null +++ b/src/spho/ctx.c @@ -0,0 +1,126 @@ + +#include +#include + +#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); +} + diff --git a/src/spho/tp.c b/src/spho/tp.c index dac68f0..74195de 100644 --- a/src/spho/tp.c +++ b/src/spho/tp.c @@ -1,2 +1,13 @@ #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 *) +//{ +// +//}