From 80ee17692a50a19359545b9a3f6fc6182829a23c Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Fri, 11 Apr 2025 23:37:06 +0200 Subject: [PATCH 01/10] queueing done --- include/spho/ctx.h | 5 ++++- include/spho/data.h | 6 +++--- include/spho/err.h | 1 + include/spho/spho.h | 22 ---------------------- src/run/devcheck.c | 6 ++++++ src/spho/ctx.c | 29 ++++++++++++++++++----------- 6 files changed, 32 insertions(+), 37 deletions(-) diff --git a/include/spho/ctx.h b/include/spho/ctx.h index 746126c..fbc27e5 100644 --- a/include/spho/ctx.h +++ b/include/spho/ctx.h @@ -3,6 +3,9 @@ #include "spho/data.h" +#define SPHO_ERR_BUF_LEN 2048 +#define SPHO_ERR_FILEBUF_LEN 128 + struct spho_ctx { int err; int err_info; @@ -20,6 +23,6 @@ struct spho_ctx { struct spho_ctx *spho_ctx_create(void); void spho_ctx_destroy(struct spho_ctx *); -char *spho_ctx_strerror(struct spho_ctx *); +const char *spho_ctx_strerror(struct spho_ctx *); #endif diff --git a/include/spho/data.h b/include/spho/data.h index 2050387..837f273 100644 --- a/include/spho/data.h +++ b/include/spho/data.h @@ -24,13 +24,13 @@ struct spho_nom_le { SLIST_ENTRY(spho_nom_le) next; }; -struct spho_const_le { +struct spho_cnst_le { struct spho_cnst cnst; - SLIST_ENTRY(spho_const_le) next; + SLIST_ENTRY(spho_cnst_le) next; }; SLIST_HEAD(spho_nom_l, spho_nom_le); -SLIST_HEAD(spho_const_l, spho_const_le); +SLIST_HEAD(spho_const_l, spho_cnst_le); #endif diff --git a/include/spho/err.h b/include/spho/err.h index f92687a..b11db1b 100644 --- a/include/spho/err.h +++ b/include/spho/err.h @@ -16,6 +16,7 @@ ctx->err_info = errno; \ snprintf(ctx->filebuf, sizeof(ctx->filebuf), "%s", \ __FILE__); \ + ctx->filebuf[sizeof(ctx->filebuf) - 1] = '\0'; \ ctx->errline = __LINE__; \ } while (0) diff --git a/include/spho/spho.h b/include/spho/spho.h index 900444f..780e5d7 100644 --- a/include/spho/spho.h +++ b/include/spho/spho.h @@ -7,26 +7,4 @@ #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/src/run/devcheck.c b/src/run/devcheck.c index e69de29..9a59086 100644 --- a/src/run/devcheck.c +++ b/src/run/devcheck.c @@ -0,0 +1,6 @@ + + +int main(void) +{ + return (0); +} diff --git a/src/spho/ctx.c b/src/spho/ctx.c index 938863f..e1a39c3 100644 --- a/src/spho/ctx.c +++ b/src/spho/ctx.c @@ -1,15 +1,18 @@ +#include #include +#include #include +#include "spho/err.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; + int err; + const char *msg; }; struct spho_err spho_errmsgs[] = { @@ -43,15 +46,15 @@ spho_ctx_destroy(struct spho_ctx *ctx) SPHO_PRECOND(ctx != NULL); - while (! SLIST_EMPTY(&c->noms)) { - nom = SLIST_FIRST(&c->noms); - SLIST_REMOVE_HEAD(&c->noms, next); + while (! SLIST_EMPTY(&ctx->noms)) { + nom = SLIST_FIRST(&ctx->noms); + SLIST_REMOVE_HEAD(&ctx->noms, next); free(nom); } - while (! SLIST_EMPTY(&c->cnsts)) { - cnst = SLIST_FIRST(&c->cnsts); - SLIST_REMOVE_HEAD(&c->cnsts, next); + while (! SLIST_EMPTY(&ctx->cnsts)) { + cnst = SLIST_FIRST(&ctx->cnsts); + SLIST_REMOVE_HEAD(&ctx->cnsts, next); free(cnst); } } @@ -60,8 +63,8 @@ spho_ctx_destroy(struct spho_ctx *ctx) const char * spho_ctx_strerror(struct spho_ctx *ctx) { - char *msg; int res; + const char *msg; SPHO_PRECOND(ctx != NULL); @@ -81,6 +84,10 @@ spho_ctx_strerror(struct spho_ctx *ctx) static const char * spho_ctx_sys_strerror(struct spho_ctx *ctx) { + int res; + + SPHO_POSTCOND(ctx != NULL); + #ifdef SPHO_DEBUG res = snprintf(ctx->errbuf, sizeof(ctx->errbuf), "%s:%d:spho_syserr:%s (%d)", ctx->filebuf, ctx->errline, @@ -89,8 +96,8 @@ spho_ctx_sys_strerror(struct spho_ctx *ctx) 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); + "spho_syserr:%s (%d)", strerror(ctx->err_info), + ctx->err_info); if (res >= sizeof(ctx->errbuf)) ctx->errbuf[sizeof(ctx->errbuf) - 1] = '\0'; #endif From fb95e5d026b74cc7b14d600370e6ee4bda5618a3 Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Fri, 11 Apr 2025 23:43:51 +0200 Subject: [PATCH 02/10] first run of context --- include/spho/spho.h | 5 +---- src/run/devcheck.c | 12 ++++++++++++ 2 files changed, 13 insertions(+), 4 deletions(-) diff --git a/include/spho/spho.h b/include/spho/spho.h index 780e5d7..b33b975 100644 --- a/include/spho/spho.h +++ b/include/spho/spho.h @@ -1,10 +1,7 @@ #ifndef _SPHO_SPHO_H #define _SPHO_SPHO_H -#include - #include "spho/err.h" - -#include "spho/data.h" +#include "spho/ctx.h" #endif diff --git a/src/run/devcheck.c b/src/run/devcheck.c index 9a59086..c975cc0 100644 --- a/src/run/devcheck.c +++ b/src/run/devcheck.c @@ -1,6 +1,18 @@ +#include + +#include "spho/spho.h" int main(void) { + struct spho_ctx *ctx; + + ctx = NULL; + + if ((ctx = spho_ctx_create()) == NULL) + return (-1); + + spho_ctx_destroy(ctx); + return (0); } From 20e3757f44d1af6e3eca508eba2fa9335bad9279 Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Mon, 14 Apr 2025 17:40:22 +0200 Subject: [PATCH 03/10] broken code, but added attempt at writing grammar --- .gitignore | 2 +- CMakeLists.txt | 30 ++++- include/spho/ctx.h | 19 ++-- include/spho/data.h | 32 +----- include/spho/err.h | 90 +++++++++------ include/spho/loc.h | 2 +- include/spho/scope.h | 34 ++++++ include/spho/spho.h | 2 + include/spho/tp.h | 123 +++++++++++++-------- include/spho/util.h | 18 +++ src/msph/README.md | 93 ++++++++++++++++ src/msph/msph.c | 40 +++++++ src/msph/msph_token.c | 247 ++++++++++++++++++++++++++++++++++++++++++ src/msph/msph_token.h | 179 ++++++++++++++++++++++++++++++ src/run/devcheck.c | 2 +- src/spho/ctx.c | 33 +++--- src/spho/scope.c | 156 ++++++++++++++++++++++++++ src/spho/tp.c | 185 ++++++++++++++++++++++++++++++- 18 files changed, 1145 insertions(+), 142 deletions(-) create mode 100644 include/spho/scope.h create mode 100644 include/spho/util.h create mode 100644 src/msph/README.md create mode 100644 src/msph/msph.c create mode 100644 src/msph/msph_token.c create mode 100644 src/msph/msph_token.h create mode 100644 src/spho/scope.c diff --git a/.gitignore b/.gitignore index dd51cb4..58189c6 100644 --- a/.gitignore +++ b/.gitignore @@ -52,7 +52,7 @@ Mkfile.old dkms.conf # CMake build directory -build/ +build-*/ # vim diff --git a/CMakeLists.txt b/CMakeLists.txt index 573a310..f3c8263 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -4,27 +4,55 @@ project(log-e-sappho C) set(CMAKE_C_STANDARD 99) set(CMAKE_C_STANDARD_REQUIRED True) +include(CheckSymbolExists) + set(INCLUDE_DIR include) set(SRC_DIR src) set(SPHO_HEADER_DIR ${INCLUDE_DIR}/spho) set(SPHO_HEADER + ${SPHO_HEADER_DIR}/ctx.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}/scope.h ${SPHO_HEADER_DIR}/tp.h + ${SPHO_HEADER_DIR}/spho.h ) set(SPHO_SRC ${SRC_DIR}/spho/ctx.c + ${SRC_DIR}/spho/scope.c + ${SRC_DIR}/spho/tp.c ) +check_symbol_exists(strlcpy "string.h" HAVE_STRLCPY) + add_library(spho STATIC ${SPHO_HEADER} ${SPHO_SRC}) target_include_directories(spho PRIVATE ${INCLUDE_DIR}) +target_compile_definitions(spho PRIVATE + $<$:SPHO_DEBUG> + $<$:SPHO_USE_STRLCPY> +) add_executable(devcheck ${SRC_DIR}/run/devcheck.c) target_link_libraries(devcheck spho) target_include_directories(devcheck PRIVATE ${INCLUDE_DIR}) +target_compile_definitions(devcheck PRIVATE + $<$:SPHO_DEBUG> +) + + +set(MSPH_SRC + ${SRC_DIR}/msph/msph_token.c + ${SRC_DIR}/msph/msph.c +) + +set(MSPH_HEADER + ${SRC_DIR}/msph/msph_token.h +) + +add_executable(msph ${MSPH_HEADER} ${MSPH_SRC}) +target_include_directories(spho PRIVATE ${INCLUDE_DIR}) diff --git a/include/spho/ctx.h b/include/spho/ctx.h index fbc27e5..9858e85 100644 --- a/include/spho/ctx.h +++ b/include/spho/ctx.h @@ -1,28 +1,31 @@ #ifndef _SPHO_CTX_H #define _SPHO_CTX_H -#include "spho/data.h" +#include "spho/err.h" +#include "spho/scope.h" #define SPHO_ERR_BUF_LEN 2048 #define SPHO_ERR_FILEBUF_LEN 128 struct spho_ctx { + struct spho_scope glob; + int err; int err_info; - - struct spho_nom_l noms; - struct spho_const_l cnsts; + char errbuf[SPHO_ERR_BUF_LEN]; #ifdef SPHO_DEBUG - char filebuf[SPHO_ERR_FILEBUF_LEN]; - int errline; -#else - char errbuf[SPHO_ERR_BUF_LEN]; + char filebuf[SPHO_ERR_FILEBUF_LEN]; + int errline; #endif + }; struct spho_ctx *spho_ctx_create(void); void spho_ctx_destroy(struct spho_ctx *); const char *spho_ctx_strerror(struct spho_ctx *); + +struct spho_nom *spho_nom_add(struct spho_ctx *, char *, size_t); +struct spho_nom *spho_nom_get(struct spho_ctx *, char *, size_t); #endif diff --git a/include/spho/data.h b/include/spho/data.h index 837f273..0cd02c8 100644 --- a/include/spho/data.h +++ b/include/spho/data.h @@ -1,36 +1,12 @@ #ifndef _SPHO_DATA_H #define _SPHO_DATA_H -#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; + char s[128]; + SLIST_ENTRY(spho_nom) next; }; -struct spho_nom_le { - struct spho_nom nom; - SLIST_ENTRY(spho_nom_le) next; -}; - -struct spho_cnst_le { - struct spho_cnst cnst; - SLIST_ENTRY(spho_cnst_le) next; -}; +SLIST_HEAD(spho_nom_l, spho_nom); -SLIST_HEAD(spho_nom_l, spho_nom_le); -SLIST_HEAD(spho_const_l, spho_cnst_le); - -#endif +#endif /* _SPHO_DATA_H */ diff --git a/include/spho/err.h b/include/spho/err.h index b11db1b..b4dcc33 100644 --- a/include/spho/err.h +++ b/include/spho/err.h @@ -1,32 +1,40 @@ #ifndef _SPHO_ERR_H #define _SPHO_ERR_H -#define SPHO_ERR_SYSTEM 0x000001 +#include -#define SPHO_ERR_INTERNAL 0x010001 +#ifdef SPHO_DEBUG +#include +#endif -#define SPHO_ERR_IS_SYSERR(err) (SPHO_ERR_SYSTEM == err) +#define SPHO_ERR_SYS 0x000001 + +#define SPHO_ERR_INTERNAL 0x010001 +#define SPHO_ERR_TOOBIG 0x010002 +#define SPHO_ERR_ARGINVAL 0x010003 +#define SPHO_ERR_NAMEINUSE 0x010004 + +#define SPHO_ERR_IS_SYSERR(err) (SPHO_ERR_SYS == err) #ifdef SPHO_DEBUG -#define SPHO_ERR(ctx, err) \ +#define SPHO_ERR(ctx, e) \ do { \ - ctx->err = err; \ - if (err == SPHO_ERR_SYSTEM) \ - ctx->err_info = errno; \ - snprintf(ctx->filebuf, sizeof(ctx->filebuf), "%s", \ + (ctx)->err = (e); \ + if ((e) == SPHO_ERR_SYS) \ + (ctx)->err_info = errno; \ + snprintf((ctx)->filebuf, sizeof((ctx)->filebuf), \ __FILE__); \ - ctx->filebuf[sizeof(ctx->filebuf) - 1] = '\0'; \ - ctx->errline = __LINE__; \ + (ctx)->errline = __LINE__; \ } while (0) #else /* SPHO_DEBUG */ -#define SPHO_ERR(ctx, err) \ +#define SPHO_ERR(ctx, e) \ do { \ - ctx->err = err; \ - if (err == SPHO_ERR_SYSTEM) \ - ctx->err_info = errno; \ + (ctx)->err = (e); \ + if ((e) == SPHO_ERR_SYS) \ + (ctx)->err_info = errno; \ } while (0) #endif /* SPHO_DEBUG */ @@ -34,30 +42,40 @@ /* 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_STRINGIFY(a) #a +#define SPHO_MACRO_STR(b) SPHO_STRINGIFY(b) -#define SPHO_ASSERT(cond) do { \ - if (! (cond) ) { \ - fprintf(stderr, "SPHO_ASSERT(" #cond ")@" __FILE__ ":" __LINE__ \ - " failed. Aborting."); \ - abort(); \ - } \ -} while (0) +#define __LINE__S SPHO_MACRO_STR(__LINE__) -#define SPHO_POSTCOND(cond) do { \ - if (! (cond) ) { \ - fprintf(stderr, "SPHO_POSTCOND(" #cond ")@" __FILE__ ":" __LINE__ \ - " failed. Aborting."); \ - abort(); \ - } \ -} while (0) +#define SPHO_PRECOND(cond) \ + do { \ + if (! (cond) ) { \ + fprintf(stderr, "SPHO_PRECOND(" #cond ")@" \ + __FILE__ ":" __LINE__S \ + " failed. Aborting.\n"); \ + abort(); \ + } \ + } while (0) + +#define SPHO_ASSERT(cond) \ + do { \ + if (! (cond) ) { \ + fprintf(stderr, "SPHO_ASSERT(" #cond ")@" \ + __FILE__ ":" __LINE__S \ + " failed. Aborting.\n"); \ + abort(); \ + } \ + } while (0) + +#define SPHO_POSTCOND(cond) \ + do { \ + if (! (cond) ) { \ + fprintf(stderr, "SPHO_POSTCOND(" #cond ")@" \ + __FILE__ ":" __LINE__S \ + " failed. Aborting.\n"); \ + abort(); \ + } \ + } while (0) #else #define SPHO_PRECOND(cond) diff --git a/include/spho/loc.h b/include/spho/loc.h index 05f6008..bf6e425 100644 --- a/include/spho/loc.h +++ b/include/spho/loc.h @@ -31,4 +31,4 @@ 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 +#endif diff --git a/include/spho/scope.h b/include/spho/scope.h new file mode 100644 index 0000000..e0d62ff --- /dev/null +++ b/include/spho/scope.h @@ -0,0 +1,34 @@ +#ifndef _SPHO_SCOPE_H +#define _SPHO_SCOPE_H + +#include "spho/data.h" + +SLIST_HEAD(spho_scope_l, spho_scope); + +struct spho_scope { + struct spho_ctx *ctx; + struct spho_scope *parent; + + struct spho_scope_l subs; + struct spho_nom_l noms; + + SLIST_ENTRY(spho_scope) next; +}; + +#define SPHO_SC_ERR(sc, err) SPHO_ERR((sc)->ctx, (err)) + +int spho_scope_init(struct spho_scope *, struct spho_ctx *, + struct spho_scope *); +void spho_scope_term(struct spho_scope *); + +struct spho_scope *spho_scope_global(struct spho_ctx *); +struct spho_scope *spho_scope_create(struct spho_scope *); + +void spho_scope_destroy(struct spho_scope *); + +struct spho_nom *spho_scope_nom_add(struct spho_scope *, const char *, size_t); +int spho_scope_nom_get(struct spho_scope *, const char *, size_t, + struct spho_nom **); +// int spho_scope_nom_del(struct spho_nom *); + +#endif /* _SPHO_SCOPE_H */ diff --git a/include/spho/spho.h b/include/spho/spho.h index b33b975..f8582dc 100644 --- a/include/spho/spho.h +++ b/include/spho/spho.h @@ -1,6 +1,8 @@ #ifndef _SPHO_SPHO_H #define _SPHO_SPHO_H +#include + #include "spho/err.h" #include "spho/ctx.h" diff --git a/include/spho/tp.h b/include/spho/tp.h index 0098237..19a7ffb 100644 --- a/include/spho/tp.h +++ b/include/spho/tp.h @@ -3,13 +3,42 @@ /* base defs */ -struct spho_alias { - struct spho_name name; - struct spho_tp *tp; +#define SPHO_KONST_S_SZ 128 +#define SPHO_KONST_K_TRUE 0x43445 /* don't change!!!!! */ +#define SPHO_KONST_K_FALSE 0x66a57 /* don't change!1! */ + +struct spho_konst { + const char *s; + int k; +}; + +const struct spho_konst SPHO_K_TRUE_V = { "True", SPHO_KONST_K_TRUE }; +const struct spho_konst SPHO_K_FALSE_V = { "False", SPHO_KONST_K_FALSE }; + +#define SPHO_K_TRUE (&SPHO_K_TRUE_V) +#define SPHO_K_FALSE (&SPHO_K_FALSE_V) + + +struct spho_var { + struct spho_nom nom; + + STAILQ_ENTRY(spho_var) next; +}; + +STAILQ_HEAD(spho_var_l, spho_var); + +struct spho_bind { + struct spho_nom nom; + struct spho_tpop *op; +}; + +struct spho_tpop { + struct spho_var_l params; + struct spho_tp *def; }; struct spho_rec { - struct spho_name mname; + struct spho_nom mnom; struct spho_tp *tp; }; @@ -20,21 +49,21 @@ struct tp_bin_data { }; struct tp_box_data { - struct spho_tp *tp; + struct spho_tp *inr; }; struct tp_forall_data { struct spho_var *var; - struct spho_tp *tp; + struct spho_tp *inr; }; -struct tp_alias_data { - struct spho_alias *alias; - struct spho_tp_list *l; +struct tp_bappl_data { + struct spho_bind *bind; + struct spho_tp_l *args; }; -struct tp_const_data { - struct spho_const *c; +struct tp_konst_data { + const struct spho_konst *k; }; struct tp_var_data { @@ -54,8 +83,8 @@ 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_bappl_data bappl; + struct tp_konst_data konst; struct tp_var_data var; struct tp_nominal_data nom; struct tp_record_data rec; @@ -67,8 +96,9 @@ union tp_data { #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_ARROW 0x14 +#define SPHO_TP_FORM_FORALL 0x15 +#define SPHO_TP_FORM_BAPPL 0x16 #define SPHO_TP_FORM_FALSE 0x20 #define SPHO_TP_FORM_TRUE 0x21 @@ -77,43 +107,48 @@ union tp_data { #define SPHO_TP_FORM_REC 0x23 -// TODO explain -#define SPHO_TP_FORM_SUB 0x96 +// #define SPHO_TP_FORM_SUB 0x96 + +#define SPHO_TP_FORM_IS_VALID(f) \ + (f) >= SPHO_TP_FORM_DISJ && (f) <= SPHO_TP_FORM_BAPPL || \ + (f) >= SPHO_TP_FORM_FALSE && (f) <= SPHO_TP_FORM_NOM || \ + (f) == SPHO_TP_FORM_REC /* sappho type */ struct spho_tp { - int form; - union tp_data data; + struct spho_scope *sc; + + int form; + union tp_data data; + + STAILQ_ENTRY(spho_tp) next; }; -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); +STAILQ_HEAD(spho_tp_l, spho_tp); -struct spho_var *spho_var_create(struct spho_ctx *, char *, size_t); -struct spho_var *spho_var_get(struct spho_ctx *, char *, size_t); +#define SPHO_TP_ERR(tp, err) SPHO_ERR((tp)->sc->ctx, (err)) -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_var *spho_var_create(struct spho_scope *, char *, size_t); +struct spho_var *spho_var_get(struct spho_scope *, 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 *spho_tp_create_disj(struct spho_scope *, struct spho_tp *, +// struct spho_tp *, struct spho_tp *); +//struct spho_tp *spho_tp_create_conj(struct spho_scope *, struct spho_tp *, +// struct spho_tp *, struct spho_tp *); +//struct spho_tp *spho_tp_create_impl(struct spho_scope *, struct spho_tp *, +// struct spho_tp *, struct spho_tp *); +//struct spho_tp *spho_tp_create_box(struct spho_scope *, struct spho_tp *, +// struct spho_tp *); +//struct spho_tp *spho_tp_create_arrow(struct spho_scope *, struct spho_tp *, +// struct spho_tp *); +//struct spho_tp *spho_tp_create_forall(struct spho_scope *, struct spho_name *, +// struct spho_tp *); +//struct spho_tp *spho_tp_create_const(struct spho_scope *, struct spho_const *); +//struct spho_tp *spho_tp_create_nominal(struct spho_scope *, +// struct spho_nom *); +//struct spho_tp *spho_tp_create_var(struct spho_scope *, struct spho_var *); +//struct spho_tp *spho_tp_create_record(struct spho_scope *, struct spho_rec *); +//struct spho_tp *spho_tp_create_sub(struct spho_scope *, struct spho_tp *, // struct spho_tp *); void spho_tp_destroy(struct spho_tp*); diff --git a/include/spho/util.h b/include/spho/util.h new file mode 100644 index 0000000..2871761 --- /dev/null +++ b/include/spho/util.h @@ -0,0 +1,18 @@ +#ifndef _SPHO_UTIL_H +#define _SPHO_UTIL_H + + +#define SPHO_UTIL_SLIST_DESTROY(l, elmtype, next, term) \ +do { \ + struct elmtype *elm; \ + while (! SLIST_EMPTY(l)) { \ + elm = SLIST_FIRST(l); \ + SLIST_REMOVE_HEAD(l, next); \ + term(elm); \ + free(elm); \ + } \ +} while (0) + + +#endif + diff --git a/src/msph/README.md b/src/msph/README.md new file mode 100644 index 0000000..00011ea --- /dev/null +++ b/src/msph/README.md @@ -0,0 +1,93 @@ +# msph/micro sappho + +Micro sappho is a minimalistic language for demonstration of the SPHO type +system. It is implemented using a simple parser and lexer that implements the +grammar below. The indended use is to allow experimentation and familiarization +with the SPHO types and subtyping. + +## Grammar + +Grammar in pseudo-bnf + +``` + +MSph ::= Body + +Body ::= Dirs + +Dir ::= Typedef (directives, with lack of a better name) + | Memberdef + | Nominaldecl + | Checkdir + +Typedef ::= 'type' Name '=' TExpr (type definition/binding) + | 'type' Name '[' Names ']' '=' TExpr + | 'type' Name (declaration, donno if useful) + +Memberdef ::= 'member' Name ':' TExpr + +Nominaldecl ::= 'nominal' Name + +Checkdir ::= 'check' TExpr '<:' TExpr + +TExpr ::= 'True' + | 'False' + | Var + | Nominal + | Trait + | TExpr '&' TExpr + | TExpr '|' TExpr + | TExpr '=>' TExpr + | TExpr '->' TExpr + | 'box' TExpr + | 'forall' Name '.' TExpr + | '(' TExpr ')' + +Trait ::= '{' Body '}' (trait, this introduces scoping) + +Var ::= Name (type variables) +Nominal ::= Name (nominal type) + +Name ::= '[a-zA-Z0-9_]+' & !Reserved (name/identifier) + +Reserved ::= 'type' (reserved/keywords) + | 'member' + | 'nominal' + | 'check' + | 'forall' + | 'box' + | 'True' + | 'False' +``` + +Precedence of binary operators: +'&' < +'|' < +'->' < +'=>' + +< means "binds closer" + +## Example + +A simple example msph program + +``` + +nominal ExampleN + +type ExampleDecl +type ExampleDecl2 + +type Example = { + member example_m : C -> C + type FA = forall X. X -> X + + type b = forall X. (box X => ExampleDecl) => ExampleDecl2 +} + +member example_global : Example & ExampleN + +type TripleConj[X, Y, Z] = X & Y & Z + +``` diff --git a/src/msph/msph.c b/src/msph/msph.c new file mode 100644 index 0000000..8643a46 --- /dev/null +++ b/src/msph/msph.c @@ -0,0 +1,40 @@ +#include + + + +#include "msph_token.h" + +#define PRINTERR(ctx) \ + do { \ + fprintf(stderr, "msph_err: %d (%d)\n", (ctx).err, (ctx).err_info); \ + } while (0) + + +int +main(int argc, char **argv) +{ + int ret; + char *path; + struct msph_ctx ctx; + struct msph_token_stream *s; + + + if (argc != 2) + return (-1); + + + path = argv[1]; + + ctx.err = 0; + ctx.err_info = 0; + + if ((s = msph_token_stream_fopen(&ctx, path)) == NULL) { + PRINTERR(ctx); + return (-1); + } + + + ret = msph_token_stream_close(s); + + return (ret); +} diff --git a/src/msph/msph_token.c b/src/msph/msph_token.c new file mode 100644 index 0000000..08c21aa --- /dev/null +++ b/src/msph/msph_token.c @@ -0,0 +1,247 @@ +#include + +#include +#include +#include + +#include "spho/err.h" + + + +#define MSPH_ERR_SYS 0x0001 +#define MSPH_ERR_TOOLONG 0x0002 + +#define MSPH_ERR(ctx, e) SPHO_ERR(ctx, e) +#define MSPH_TOKS_ERR(toks, e) MSPH_ERR((toks)->ctx, e) + +struct msph_token_stream * +msph_token_stream_fopen(struct msph_ctx *ctx, const char *path) +{ + FILE *f; + size_t res; + struct msph_token_stream *ret; + + if ((f = fopen(path, "r")) == NULL) { + MSPH_ERR(ctx, MSPH_ERR_SYS); + return (NULL); + } + + if ((ret = calloc(1, sizeof(struct msph_token_stream))) == NULL) { + MSPH_ERR(ctx, MSPH_ERR_SYS); + goto err; + } + + ret->ctx = ctx; + ret->src.type = MSPH_TOKEN_SRC_FILE; + ret->src.inner.file.f = f; + ret->src.inner.file.eof = 0; + ret->src.inner.file.pos = ret->src.file.buf; + ret->src.inner.file.end = ret->src.file.buf; + ret->src.inner.file.read_ptr = ret->src.file.buf; + + res = strlcpy(ret->src.file.name, path, sizeof(ret->src.file.name)); + if (res >= sizeof(ret->src.file.name)) { + MSPH_ERR(ctx, MSPH_ERR_TOOLONG); + goto err; + } + + return (ret); +err: + if (fclose(f) == EOF) + abort(); + + if (ret != NULL) + free(ret); + + return (NULL); +} + +struct msph_token_stream * +msph_token_stream_frombuf(struct msph_ctx *ctx, const char *buf, size_t len) +{ + struct msph_token_stream *ret; + + if ((ret = calloc(1, sizeof(struct msph_token_stream))) == NULL) { + MSPH_ERR(ctx, MSPH_ERR_SYS); + return (NULL); + } + + ret->ctx = ctx; + ret->type = MSPH_TOKEN_SRC_STR; + ret->src.str.s = buf; + ret->src.str.len = len; + ret->src.str.pos = 0; + + return (ret); +} + + +int +msph_token_stream_close(struct msph_token_stream *s) +{ + int ret; + + ret = -1; + + switch (s->type) { + case MSPH_TOKEN_SRC_FILE: + ret = fclose(s->src.file.f); + break; + case MSPH_TOKEN_SRC_STR: + ret = 0; + break; + default: + break; + } + + return (ret); +} + + +/* -1 or num tokens read */ +ssize_t +msph_token_stream_read_tok(struct msph_token *ptr, size_t n, + struct msph_token_stream *s) +{ + ssize_t ret; + size_t i; + int res; + + ret = 0; + res = -1; + while ((res = read_single_tok(&ptr[i], s)) == 1) { + if (res == -1) { + ret = -1; + break; + } + ret++; + } + + return (ret); +} + +struct msph_token_matcher { + size_t pos_off; + size_t matchlen; + + const int tok_type; +} msph_matcher[] = { + { 0, 0, TOK_START }, + { 0, 0, TOK_IDENT }, + { 0, 0, TOK_END } +}; + +#define BUF_LEN(b) (sizeof(b) / sizeof(b[0])) +static int +file_char_at(struct msph_ctx *ctx, struct msph_token_src *src, size_t i, + char *out) +{ + size_t nread; + size_t maxread; + struct msph_token_src_file *file; + + ret = -1; + file = &src->inner.file; + + if (file->pos + i < file->end) { + *out = file->buf[file->pos + i]; + return (0); + } + if (file->end < file->pos && + ((file->pos + i) % BUF_LEN(file->buf)) < file->end) { + *out = file->buf[(file->pos + i) % BUF_LEN(file->buf)]; + return (0); + } + + if (file->eof) { + return (-1); + } + + if (file->end < file->pos) + maxread = file->pos - file->end; + else + maxread = BUF_LEN(file->buf) - file->end; + + maxread = file->end < file->pos ? file->pos - file->end : + BUF_LEN(file->buf) - file->end; + + if (maxread == 0) { + MSPH_ERR(ctx, MSPH_ERR_TOOLONG); + return (-1); + } + + ret = fread(&file->buf[file->end], sizeof(file->buf[0]), maxread, + file->f); + + if (ret == 0) { + if (ferror(file->f)) { + MSPH_ERR(ctx, MSPH_ERR_SYS); + return (-1); + } + file->eof = 1; + return (-1); + } +} + +static int +char_at(struct msph_token_src *src, size_t i, char *out) +{ + int ret; + + switch (src->type) { + case MSPH_TOKEN_SRC_FILE: + ret = file_char_at(s, i, out); + break; + case MSPH_TOKEN_SRC_STR: + ret = str_char_at(s, i, out); + break; + default: + break; + } + + return (ret); +} + +static int +tok_match(struct msph_token_matcher *m, struct msph_token_stream *s) +{ +} + +static void +tok_commit(struct msph_token *ptr, struct msph_token_stream *s, + struct msph_matcher *m) +{ + SPHO_PRECOND(p != NULL && m != NULL); + SPHO_PRECOND(m->matchlen != 0); + +} + +/* 1: success, 0: failed match, -1: error */ +static int +read_single_tok(struct msph_token *ptr, struct msph_token_stream *s) +{ + int res; + size_t m; + size_t max_m; + + max_m = 0; + for (m = 0; msph_matcher[m].type != TOK_END; m++) { + res = tok_match(&msph_matcher[m], s); + + if (res == -1) + return (-1); + + if (res == 0 && + msph_matcher[m].matchlen > msph_matcher[max_m].matchlen) { + max_m = m; + } + } + + if (max_m == 0) + return (0); + + tok_commit(ptr, &msph_matcher[max_m]); + + return (1); +} + diff --git a/src/msph/msph_token.h b/src/msph/msph_token.h new file mode 100644 index 0000000..1e7a996 --- /dev/null +++ b/src/msph/msph_token.h @@ -0,0 +1,179 @@ +#ifndef _MSPH_EXPR_H +#define _MSPH_EXPR_H + +/* + * TYPES: + * Conj + * Disj + * Impl + * Arrow + * Box + * (Sub) + * Forall + * + * True + * False + * Var + * Nominal + * + * Record + * + * DEFINITIONS/DIRECTIVES: + * Type definition (type A[X..] = T) + * Nominal definition (nominal N) + * Member definition (member mname : T) + * + * { + * member a: A + * member b: B + * } + * + * Subtyping check (check A <: B, checks if A <: B) + * + * EXTRA DEFINITIONS + * Class definition (class C[...] { ... }, shorthand) + * + * EXPRESSIONS + * Conj + * Disj + * Impl + * Arrow + * Box + * (Sub) + * Forall + * + * True + * False + * Var + * Nominal + * + * Trait ({ ... }, creates scoping) + * + * + * TOKENS + * lbrace { + * rbrace } + * lbrak [ + * rbrak ] + * lparen ( + * rparen ) + * colon : + * equals = + * + * op_and & + * op_or | + * op_impl => + * op_sub <: + * + * kw_type type + * kw_nominal nominal + * kw_member member + * kw_check check + * kw_box box + * kw_forall forall + * + * k_true True + * k_false False + * + * ident C, anid, ... + * + */ + +struct msph_ctx { + int err; + int err_info; +}; + +enum msph_tok_type { + TOK_START, + TOK_LBRACE, // { + TOK_RBRACE, // } + TOK_LBRAK, // [ + TOK_RBRAK, // ] + TOK_LPAREN, // ( + TOK_RPAREN, // ) + TOK_OP_COLON, // : + TOK_OP_EQUALS, // = + + TOK_OP_AMP, // & + TOK_OP_PIPE, // | + TOK_OP_RARROW, // => + TOK_OP_SUB, // <: + + TOK_KW_TYPE, // type + TOK_KW_NOMINAL, // nominal + TOK_KW_MEMBER, // member + TOK_KW_CHECK, // check + TOK_KW_BOX, // box + TOK_KW_FORALL, // forall + + TOK_CONST_TRUE, // True + TOK_CONST_FALSE, // False + + TOK_IDENT, // identifiers + TOK_END +}; + +#define MSPH_TOKEN_BUF_SZ 128 + +struct token_s { + char buf[MSPH_TOKEN_BUF_SZ]; +}; + +union token_data { + struct token_s s; +}; + +struct msph_token { + int type; + union token_data d; +}; + +#define MSPH_PATH_LEN 1024 +#define MSPH_FILE_BUF_LEN 4096 +#define MSPH_TOKEN_SRC_FILE 1 + +struct msph_token_src_file { + FILE *f; + int eof; + size_t pos; // TODO rename bufpos + size_t end; // TODO rename bufend + size_t read_pos; + char buf[MSPH_FILE_BUF_LEN]; + + char name[MSPH_PATH_LEN]; +}; + +#define MSPH_TOKEN_SRC_STR 2 +struct msph_token_src_str { + const char *s; + size_t len; + size_t pos; +}; + +union msph_token_src_data { + struct msph_token_src_file file; + struct msph_token_src_str str; +}; + +struct msph_token_src { + int type + union msph_token_src_data inner; +}; + +struct msph_token_stream { + struct msph_ctx *ctx; + + struct msph_token_src src; +}; + +struct msph_token_stream *msph_token_stream_fopen(struct msph_ctx *, + const char *); +struct msph_token_stream *msph_token_stream_frombuf(struct msph_ctx *, + const char *, size_t); + +int msph_token_stream_close(struct msph_token_stream*); + +struct msph_token *msph_token_source_pop(struct msph_token_stream *); + +#endif /* _MSPH_EXPR_H */ diff --git a/src/run/devcheck.c b/src/run/devcheck.c index c975cc0..24c41ff 100644 --- a/src/run/devcheck.c +++ b/src/run/devcheck.c @@ -11,7 +11,7 @@ int main(void) if ((ctx = spho_ctx_create()) == NULL) return (-1); - + spho_ctx_destroy(ctx); return (0); diff --git a/src/spho/ctx.c b/src/spho/ctx.c index e1a39c3..dacc076 100644 --- a/src/spho/ctx.c +++ b/src/spho/ctx.c @@ -4,7 +4,6 @@ #include #include -#include "spho/err.h" #include "spho/ctx.h" static const char *spho_ctx_sys_strerror(struct spho_ctx *); @@ -16,8 +15,11 @@ struct spho_err { }; struct spho_err spho_errmsgs[] = { - { SPHO_ERR_SYSTEM, "spho system error" }, - { SPHO_ERR_INTERNAL, "spho internal error" }, + { SPHO_ERR_SYS, "spho system error" }, + { SPHO_ERR_INTERNAL, "spho internal error" }, + { SPHO_ERR_TOOBIG, "parameter size too big" }, + { SPHO_ERR_ARGINVAL, "invalid argument" }, + { SPHO_ERR_NAMEINUSE, "name in use" }, { -1, NULL } }; @@ -26,14 +28,20 @@ spho_ctx_create(void) { struct spho_ctx *c; + c = NULL; + 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); + if (spho_scope_init(&c->glob, c, NULL) == -1) { + free(c); + return (NULL); + } + + SPHO_POSTCOND(c != NULL); return (c); } @@ -41,22 +49,11 @@ spho_ctx_create(void) 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(&ctx->noms)) { - nom = SLIST_FIRST(&ctx->noms); - SLIST_REMOVE_HEAD(&ctx->noms, next); - free(nom); - } + spho_scope_term(&ctx->glob); - while (! SLIST_EMPTY(&ctx->cnsts)) { - cnst = SLIST_FIRST(&ctx->cnsts); - SLIST_REMOVE_HEAD(&ctx->cnsts, next); - free(cnst); - } + free(ctx); } diff --git a/src/spho/scope.c b/src/spho/scope.c new file mode 100644 index 0000000..988e824 --- /dev/null +++ b/src/spho/scope.c @@ -0,0 +1,156 @@ +#include + +#include +#include + +#include "spho/ctx.h" +#include "spho/scope.h" +#include "spho/util.h" + +static void spho_nom_term(struct spho_nom *); + +int +spho_scope_init(struct spho_scope *sc, struct spho_ctx *ctx, + struct spho_scope *p) +{ + SLIST_INIT(&sc->subs); + SLIST_INIT(&sc->noms); + + sc->parent = p; + + return (0); +} + +void +spho_scope_term(struct spho_scope *sc) +{ + SPHO_UTIL_SLIST_DESTROY(&sc->subs, spho_scope, next, spho_scope_term); + + SPHO_UTIL_SLIST_DESTROY(&sc->noms, spho_nom, next, spho_nom_term); + + sc->parent = NULL; +} + +struct spho_scope * +spho_scope_global(struct spho_ctx *ctx) +{ + SPHO_PRECOND(ctx != NULL); + + return (&ctx->glob); +} + + +struct spho_scope * +spho_scope_create(struct spho_scope *sc) +{ + struct spho_scope *sub; + + if ((sub = malloc(sizeof(struct spho_scope))) == NULL) { + SPHO_ERR(sc->ctx, SPHO_ERR_SYS); + return (NULL); + } + + if (spho_scope_init(sub, sc->ctx, sc) == -1) { + free(sub); + return (NULL); + } + + SLIST_INSERT_HEAD(&sc->subs, sub, next); + + return (sub); +} + + +static void +spho_nom_term(struct spho_nom *nom) +{ + return; +} + +void +spho_scope_destroy(struct spho_scope *sc) +{ + struct spho_scope *sub; + struct spho_scope *p; + + p = sc->parent; + SLIST_REMOVE(&p->subs, sc, spho_scope, next); + spho_scope_term(sc); + free(sc); +} + + +struct spho_nom * +spho_scope_nom_add(struct spho_scope *sc, const char *nomstr, size_t sz) +{ +#ifdef SPHO_USE_STRLCPY + size_t res; +#else + ssize_t res; +#endif + struct spho_nom *nom; + + + if (spho_scope_nom_get(sc, nomstr, sz, &nom) == -1) + return (NULL); + + if (nom != NULL) { + SPHO_SC_ERR(sc, SPHO_ERR_NAMEINUSE); + return (NULL); + } + + if ((nom = malloc(sizeof(struct spho_nom))) == NULL) { + SPHO_SC_ERR(sc, SPHO_ERR_SYS); + return (NULL); + } + +#ifdef SPHO_USE_STRLCPY + res = strlcpy(nom->s, nomstr, sizeof(nom->s)); + if (res >= sizeof(nom->s)) { + SPHO_SC_ERR(sc, SPHO_ERR_TOOBIG); + goto err; + } +#else + res = snprintf(nom->s, sizeof(nom->s), "%s", nomstr); + if (res < 0) { + SPHO_SC_ERR(sc, SPHO_ERR_SYS); + goto err; + } + if (res >= (ssize_t)sizeof(nom->s)) { + SPHO_SC_ERR(sc, SPHO_ERR_TOOBIG); + goto err; + } +#endif + + SLIST_INSERT_HEAD(&sc->noms, nom, next); + + return (nom); +err: + free(nom); + return (NULL); +} + + +int +spho_scope_nom_get(struct spho_scope *sc, const char *nomstr, size_t sz, + struct spho_nom **out) +{ + struct spho_nom *nom; + + nom = NULL; + + if (sz > sizeof(nom->s)) { + SPHO_ERR(sc->ctx, SPHO_ERR_TOOBIG); + return (-1); + } + + out = NULL; + SLIST_FOREACH(nom, &sc->noms, next) { + if (strncmp(nom->s, nomstr, sz) == 0) { + *out = nom; + break; + } + } + + return (0); +} diff --git a/src/spho/tp.c b/src/spho/tp.c index 74195de..e207197 100644 --- a/src/spho/tp.c +++ b/src/spho/tp.c @@ -1,9 +1,11 @@ +#include + +#include + +#include "spho/ctx.h" +#include "spho/scope.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 *, @@ -11,3 +13,178 @@ spho_nom_add(struct spho_ctx *ctx, char *nom, size_t nomlen) //{ // //} + + +struct spho_tp * +spho_tp_alloc(struct spho_scope *sc, int form) +{ + struct spho_tp *tp; + + SPHO_PRECOND(SPHO_TP_FORM_IS_VALID(form)); + + if ((tp = calloc(1, sizeof(struct spho_tp))) == NULL) { + SPHO_SC_ERR(sc, SPHO_ERR_SYS); + return (NULL); + } + + tp->sc = sc; + tp->form = form; + + return (tp); +} + + +int +spho_tp_init_disj(struct spho_tp *tp, struct spho_tp *a, struct spho_tp *b) +{ + if (tp->form != SPHO_TP_FORM_DISJ) { + SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL); + return (-1); + } + + tp->data.binop.left = a; + tp->data.binop.right = b; + + return (0); +} + +int +spho_tp_init_conj(struct spho_tp *tp, struct spho_tp *a, struct spho_tp *b) +{ + if (tp->form != SPHO_TP_FORM_CONJ) { + SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL); + return (-1); + } + + tp->data.binop.left = a; + tp->data.binop.right = b; + + return (0); +} + +int +spho_tp_init_impl(struct spho_tp *tp, struct spho_tp *a, struct spho_tp *b) +{ + if (tp->form != SPHO_TP_FORM_IMPL) { + SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL); + return (-1); + } + + tp->data.binop.left = a; + tp->data.binop.right = b; + + return (0); +} + +int +spho_tp_init_arrow(struct spho_tp *tp, struct spho_tp *a, struct spho_tp *b) +{ + if (tp->form != SPHO_TP_FORM_ARROW) { + SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL); + return (-1); + } + + tp->data.binop.left = a; + tp->data.binop.right = b; + + return (0); +} + +int +spho_tp_init_box(struct spho_tp *tp, struct spho_tp *inr) +{ + if (tp->form != SPHO_TP_FORM_BOX) { + SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL); + return (-1); + } + + tp->data.box.inr = inr; + + return (0); +} + +int +spho_tp_init_forall(struct spho_tp *tp, struct spho_var *var, + struct spho_tp *inr) +{ + if (tp->form != SPHO_TP_FORM_FORALL) { + SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL); + return (-1); + } + + tp->data.fa.var = var; + tp->data.fa.inr = inr; + + return (0); +} + +int +spho_tp_init_bappl(struct spho_tp *tp, struct spho_bind *bind, + struct spho_tp_l *args) +{ + struct spho_tp *arg; + + if (tp->form != SPHO_TP_FORM_BAPPL) { + SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL); + return (-1); + } + + tp->data.bappl.bind = bind; + tp->data.bappl.args = args; + + return (0); +} + +int +spho_tp_init_false(struct spho_tp *tp) +{ + if (tp->form != SPHO_TP_FORM_FALSE) { + SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL); + return (-1); + } + + tp->data.konst.k = SPHO_K_FALSE; + + return (0); +} + +int +spho_tp_init_true(struct spho_tp *tp) +{ + if (tp->form != SPHO_TP_FORM_TRUE) { + SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL); + return (-1); + } + + tp->data.konst.k = SPHO_K_TRUE; + + return (0); +} + +int +spho_tp_init_var(struct spho_tp *tp, struct spho_var *var) +{ + if (tp->form != SPHO_TP_FORM_VAR) { + SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL); + return (-1); + } + + tp->data.var.v = var; + + return (0); +} + +int +spho_tp_init_rec(struct spho_tp *tp, struct spho_rec *rec) +{ + if (tp->form != SPHO_TP_FORM_REC) { + SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL); + return (-1); + } + + tp->data.rec.r = rec; + + return (0); +} + + From dd099f3382ac775ca609c8386c08b63d6e5f536f Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Mon, 14 Apr 2025 17:42:48 +0200 Subject: [PATCH 04/10] added note about ambiguity --- src/msph/README.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/msph/README.md b/src/msph/README.md index 00011ea..3c87d87 100644 --- a/src/msph/README.md +++ b/src/msph/README.md @@ -9,6 +9,9 @@ with the SPHO types and subtyping. Grammar in pseudo-bnf +And yes, it is ambiguous at places. More specification coming when there is +time. + ``` MSph ::= Body From 10e16147ba113485db99fd9a021c6bdeb9e110fb Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Tue, 15 Apr 2025 13:50:23 +0200 Subject: [PATCH 05/10] tokinizing --- CMakeLists.txt | 3 +- src/msph/msph_token.c | 454 +++++++++++++++++++++++++++++++----------- src/msph/msph_token.h | 27 +-- 3 files changed, 360 insertions(+), 124 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index f3c8263..34e7f44 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -55,4 +55,5 @@ set(MSPH_HEADER ) add_executable(msph ${MSPH_HEADER} ${MSPH_SRC}) -target_include_directories(spho PRIVATE ${INCLUDE_DIR}) +target_include_directories(msph PRIVATE ${INCLUDE_DIR}) +target_link_libraries(devcheck spho) diff --git a/src/msph/msph_token.c b/src/msph/msph_token.c index 08c21aa..f69c8b6 100644 --- a/src/msph/msph_token.c +++ b/src/msph/msph_token.c @@ -3,9 +3,11 @@ #include #include #include +#include #include "spho/err.h" +#include "msph_token.h" #define MSPH_ERR_SYS 0x0001 @@ -14,6 +16,31 @@ #define MSPH_ERR(ctx, e) SPHO_ERR(ctx, e) #define MSPH_TOKS_ERR(toks, e) MSPH_ERR((toks)->ctx, e) +struct msph_token_matcher { + size_t off; + size_t matchlen; + + const int type; +} msph_matcher[] = { + { 0, 0, TOK_START }, + { 0, 0, TOK_IDENT }, + { 0, 0, TOK_END } +}; + +static ssize_t src_file_fill_buf(struct msph_ctx *, + struct msph_token_src_file *); +static int tok_match(struct msph_ctx *, struct msph_token_src *, + struct msph_token_matcher *); +static int tok_commit(struct msph_ctx *, struct msph_token_src *, + struct msph_token_matcher *, struct msph_token *); +static int char_at(struct msph_ctx *, struct msph_token_src *, size_t, + char *); +static int fromcbuf_charcpy(char *, const char *, size_t, size_t, size_t); +static int file_char_at(struct msph_ctx *, struct msph_token_src *, size_t, + char *out); +static int read_single_tok(struct msph_token *, struct msph_token_stream *); + + struct msph_token_stream * msph_token_stream_fopen(struct msph_ctx *ctx, const char *path) { @@ -34,13 +61,12 @@ msph_token_stream_fopen(struct msph_ctx *ctx, const char *path) ret->ctx = ctx; ret->src.type = MSPH_TOKEN_SRC_FILE; ret->src.inner.file.f = f; - ret->src.inner.file.eof = 0; - ret->src.inner.file.pos = ret->src.file.buf; - ret->src.inner.file.end = ret->src.file.buf; - ret->src.inner.file.read_ptr = ret->src.file.buf; + ret->src.inner.file.pos = 0; + ret->src.inner.file.end = 0; - res = strlcpy(ret->src.file.name, path, sizeof(ret->src.file.name)); - if (res >= sizeof(ret->src.file.name)) { + res = strlcpy(ret->src.inner.file.name, path, + sizeof(ret->src.inner.file.name)); + if (res >= sizeof(ret->src.inner.file.name)) { MSPH_ERR(ctx, MSPH_ERR_TOOLONG); goto err; } @@ -67,10 +93,10 @@ msph_token_stream_frombuf(struct msph_ctx *ctx, const char *buf, size_t len) } ret->ctx = ctx; - ret->type = MSPH_TOKEN_SRC_STR; - ret->src.str.s = buf; - ret->src.str.len = len; - ret->src.str.pos = 0; + ret->src.type = MSPH_TOKEN_SRC_STR; + ret->src.inner.str.s = buf; + ret->src.inner.str.len = len; + ret->src.inner.str.pos = 0; return (ret); } @@ -83,9 +109,9 @@ msph_token_stream_close(struct msph_token_stream *s) ret = -1; - switch (s->type) { + switch (s->src.type) { case MSPH_TOKEN_SRC_FILE: - ret = fclose(s->src.file.f); + ret = fclose(s->src.inner.file.f); break; case MSPH_TOKEN_SRC_STR: ret = 0; @@ -97,7 +123,6 @@ msph_token_stream_close(struct msph_token_stream *s) return (ret); } - /* -1 or num tokens read */ ssize_t msph_token_stream_read_tok(struct msph_token *ptr, size_t n, @@ -120,102 +145,6 @@ msph_token_stream_read_tok(struct msph_token *ptr, size_t n, return (ret); } -struct msph_token_matcher { - size_t pos_off; - size_t matchlen; - - const int tok_type; -} msph_matcher[] = { - { 0, 0, TOK_START }, - { 0, 0, TOK_IDENT }, - { 0, 0, TOK_END } -}; - -#define BUF_LEN(b) (sizeof(b) / sizeof(b[0])) -static int -file_char_at(struct msph_ctx *ctx, struct msph_token_src *src, size_t i, - char *out) -{ - size_t nread; - size_t maxread; - struct msph_token_src_file *file; - - ret = -1; - file = &src->inner.file; - - if (file->pos + i < file->end) { - *out = file->buf[file->pos + i]; - return (0); - } - if (file->end < file->pos && - ((file->pos + i) % BUF_LEN(file->buf)) < file->end) { - *out = file->buf[(file->pos + i) % BUF_LEN(file->buf)]; - return (0); - } - - if (file->eof) { - return (-1); - } - - if (file->end < file->pos) - maxread = file->pos - file->end; - else - maxread = BUF_LEN(file->buf) - file->end; - - maxread = file->end < file->pos ? file->pos - file->end : - BUF_LEN(file->buf) - file->end; - - if (maxread == 0) { - MSPH_ERR(ctx, MSPH_ERR_TOOLONG); - return (-1); - } - - ret = fread(&file->buf[file->end], sizeof(file->buf[0]), maxread, - file->f); - - if (ret == 0) { - if (ferror(file->f)) { - MSPH_ERR(ctx, MSPH_ERR_SYS); - return (-1); - } - file->eof = 1; - return (-1); - } -} - -static int -char_at(struct msph_token_src *src, size_t i, char *out) -{ - int ret; - - switch (src->type) { - case MSPH_TOKEN_SRC_FILE: - ret = file_char_at(s, i, out); - break; - case MSPH_TOKEN_SRC_STR: - ret = str_char_at(s, i, out); - break; - default: - break; - } - - return (ret); -} - -static int -tok_match(struct msph_token_matcher *m, struct msph_token_stream *s) -{ -} - -static void -tok_commit(struct msph_token *ptr, struct msph_token_stream *s, - struct msph_matcher *m) -{ - SPHO_PRECOND(p != NULL && m != NULL); - SPHO_PRECOND(m->matchlen != 0); - -} - /* 1: success, 0: failed match, -1: error */ static int read_single_tok(struct msph_token *ptr, struct msph_token_stream *s) @@ -223,10 +152,15 @@ read_single_tok(struct msph_token *ptr, struct msph_token_stream *s) int res; size_t m; size_t max_m; + struct msph_ctx *ctx; + struct msph_token_src *src; + + ctx = s->ctx; + src = &s->src; max_m = 0; for (m = 0; msph_matcher[m].type != TOK_END; m++) { - res = tok_match(&msph_matcher[m], s); + res = tok_match(ctx, src, &msph_matcher[m]); if (res == -1) return (-1); @@ -240,8 +174,306 @@ read_single_tok(struct msph_token *ptr, struct msph_token_stream *s) if (max_m == 0) return (0); - tok_commit(ptr, &msph_matcher[max_m]); + if (tok_commit(ctx, src, &msph_matcher[max_m], ptr) == -1) + return (-1); return (1); } + +#define BUF_LEN(b) (sizeof(b) / sizeof((b)[0])) + +static ssize_t +src_file_fill_buf(struct msph_ctx *ctx, struct msph_token_src_file *file) +{ + ssize_t ret; + size_t nread, maxread; + + ret = nread = maxread = 0; + do { + if (file->end < file->pos) + maxread = file->pos - file->end; + else + maxread = BUF_LEN(file->buf) - file->end; + + if (maxread == 0) { + MSPH_ERR(ctx, MSPH_ERR_TOOLONG); + return (-1); + } + + nread = fread(&file->buf[file->end], sizeof(file->buf[0]), + maxread, file->f); + + ret += nread; + file->end = (file->end + nread) % BUF_LEN(file->buf); + + if (nread < maxread) { + if (ferror(file->f)) { + MSPH_ERR(ctx, MSPH_ERR_SYS); + return (-1); + } + break; + } + + } while (file->end != file->pos); + + return (ret); +} + +/* reads a single char from the circular buffer in src */ +static int +file_char_at(struct msph_ctx *ctx, struct msph_token_src *src, size_t i, + char *out) +{ + int ret; + ssize_t fill; + struct msph_token_src_file *file; + + SPHO_PRECOND(s != NULL); + SPHO_PRECOND(s->src.type == MSPH_TOKEN_SRC_FILE); + + ret = 0; + file = &src->inner.file; + + do { + /* simplest case */ + if (file->pos + i < file->end) { + *out = file->buf[file->pos + i]; + return (1); + } + /* wrap around */ + if (file->end < file->pos && + ((file->pos + i) % BUF_LEN(file->buf)) < file->end) { + *out = file->buf[(file->pos + i) % BUF_LEN(file->buf)]; + return (1); + } + + if (feof(file->f)) + return (0); + if (src_file_fill_buf(ctx, file) == -1) + return (-1); + } while (ret++); + + return (-1); +} + +static int +char_at(struct msph_ctx *ctx, struct msph_token_src *src, size_t i, char *out) +{ + int ret; + struct msph_token_src_str *str; + + switch (src->type) { + case MSPH_TOKEN_SRC_FILE: + return (file_char_at(ctx, src, i, out)); + case MSPH_TOKEN_SRC_STR: + str = &src->inner.str; + if (str->pos + i < str->len) { + *out = str->s[str->pos + i]; + return (1); + } + return (0); + default: + break; + } + + return (ret); +} + +static int +fromcbuf_charcpy(char *dst, const char *src, size_t src_len, size_t src_pos, + size_t ncpy) +{ + size_t cpy1, cpy2; + if (src_len < ncpy) { + return (-1); + } + + cpy1 = src_pos + ncpy < src_len ? ncpy : src_len - src_pos; + cpy2 = ncpy - cpy1; + + memcpy(dst, &src[src_pos], cpy1 * sizeof(src[0])); + + if (! cpy2) + return (0); + + memcpy(dst, &src[0], cpy2 * sizeof(src[0])); + + return (0); +} + +static int +tok_match(struct msph_ctx *ctx, struct msph_token_src *src, + struct msph_token_matcher *m) +{ + int res; + int more; + char chr; + const char *match_str; + size_t off, len; + SPHO_PRECOND(m != NULL && s != NULL); + + m->matchlen = 0; + +#define MATCH_CHAR(c) \ + do { \ + if ((res = char_at(ctx, src, 0, &chr)) == -1) \ + return (-1); \ + else if (res == 0) \ + return (0); \ +\ + if (chr == (c)) { \ + m->matchlen = 1; \ + } \ + return (0); \ + } while (0) + +#define MATCH_STR(str) \ + do { \ + match_str = str; \ + len = strlen(match_str); \ + for (off = 0; off < len; off++) { \ + if ((res = char_at(ctx, src, off, &chr)) == -1) \ + return (-1); \ + else if (res == 0) \ + return (0); \ +\ + if (chr != match_str[off]) \ + break; \ + } \ + if (off == len) \ + m->matchlen = len; \ + return (0); \ + } while (0) + + switch (m->type) { + case TOK_LBRACE: + MATCH_CHAR('{'); + case TOK_RBRACE: + MATCH_CHAR('}'); + case TOK_LBRAK: + MATCH_CHAR('['); + case TOK_RBRAK: + MATCH_CHAR(']'); + case TOK_LPAREN: + MATCH_CHAR('('); + case TOK_RPAREN: + MATCH_CHAR(')'); + case TOK_COLON: + MATCH_CHAR(':'); + case TOK_EQUALS: + MATCH_CHAR('='); + case TOK_AMP: + MATCH_CHAR('&'); + case TOK_PIPE: + MATCH_CHAR('|'); + case TOK_RARROW: + MATCH_STR("=>"); + case TOK_SUB: + MATCH_STR("<:"); + case TOK_KW_TYPE: + MATCH_STR("type"); + case TOK_KW_NOMINAL: + MATCH_STR("nominal"); + case TOK_KW_MEMBER: + MATCH_STR("member"); + case TOK_KW_CHECK: + MATCH_STR("check"); + case TOK_KW_BOX: + MATCH_STR("box"); + case TOK_KW_FORALL: + MATCH_STR("forall"); + case TOK_CONST_TRUE: + MATCH_STR("True"); + case TOK_CONST_FALSE: + MATCH_STR("False"); + case TOK_IDENT: + off = 0; + while ((res = char_at(ctx, src, off++, &chr)) == 1) { + if (! isalnum(chr)) + break; + m->matchlen++; + } + if (res == -1) + return (-1); + return (0); + default: + SPHO_ASSERT(0); + return (-1); + break; + } +#undef MATCH_CHAR +#undef MATCH_STR +} + +#define TOK_HAS_DATA(type) (type == TOK_IDENT) +static int +tok_commit(struct msph_ctx *ctx, struct msph_token_src *src, + struct msph_token_matcher *m, struct msph_token *ptr) +{ + size_t pos_old; + struct msph_token_src_str *str; + struct msph_token_src_file *file; + + SPHO_PRECOND(p != NULL && m != NULL); + SPHO_PRECOND(m->matchlen != 0); + + switch (src->type) { + case MSPH_TOKEN_SRC_FILE: + file = &src->inner.file; + pos_old = file->pos; + + file->pos += m->matchlen; + file->pos %= BUF_LEN(file->buf); + SPHO_ASSERT(file->pos < BUF_LEN(file->buf) || + file->pos < pos_old); + + ptr->type = m->type; + if (! TOK_HAS_DATA(ptr->type)) + return (0); + + if (m->matchlen >= sizeof(ptr->d.s.buf)) { + MSPH_ERR(ctx, MSPH_ERR_TOOLONG); + return (-1); + } + + if (fromcbuf_charcpy(ptr->d.s.buf, file->buf, sizeof(file->buf), + pos_old, m->matchlen) == -1) { + MSPH_ERR(ctx, MSPH_ERR_TOOLONG); + return (-1); + } + + ptr->d.s.buf[m->matchlen] = '\0'; + return (0); + + case MSPH_TOKEN_SRC_STR: + str = &src->inner.str; + pos_old = str->pos; + + str->pos += m->matchlen; + SPHO_ASSERT(str->pos <= str->len); + + ptr->type = m->type; + if (! TOK_HAS_DATA(ptr->type)) + return (0); + + if (m->matchlen >= sizeof(ptr->d.s.buf)) { + MSPH_ERR(ctx, MSPH_ERR_TOOLONG); + return (-1); + } + + memcpy(ptr->d.s.buf, str->s, m->matchlen * + sizeof(str->s[0])); + ptr->d.s.buf[m->matchlen] = '\0'; + + return (0); + default: + return (-1); + } +} + + + + + + diff --git a/src/msph/msph_token.h b/src/msph/msph_token.h index 1e7a996..7207052 100644 --- a/src/msph/msph_token.h +++ b/src/msph/msph_token.h @@ -92,13 +92,13 @@ enum msph_tok_type { TOK_RBRAK, // ] TOK_LPAREN, // ( TOK_RPAREN, // ) - TOK_OP_COLON, // : - TOK_OP_EQUALS, // = + TOK_COLON, // : + TOK_EQUALS, // = - TOK_OP_AMP, // & - TOK_OP_PIPE, // | - TOK_OP_RARROW, // => - TOK_OP_SUB, // <: + TOK_AMP, // & + TOK_PIPE, // | + TOK_RARROW, // => + TOK_SUB, // <: TOK_KW_TYPE, // type TOK_KW_NOMINAL, // nominal @@ -135,12 +135,13 @@ struct msph_token { struct msph_token_src_file { FILE *f; - int eof; - size_t pos; // TODO rename bufpos - size_t end; // TODO rename bufend - size_t read_pos; + + /* circular buffer for reading */ + size_t pos; + size_t end; char buf[MSPH_FILE_BUF_LEN]; + /* file path */ char name[MSPH_PATH_LEN]; }; @@ -157,7 +158,7 @@ union msph_token_src_data { }; struct msph_token_src { - int type + int type; union msph_token_src_data inner; }; @@ -174,6 +175,8 @@ struct msph_token_stream *msph_token_stream_frombuf(struct msph_ctx *, int msph_token_stream_close(struct msph_token_stream*); -struct msph_token *msph_token_source_pop(struct msph_token_stream *); +ssize_t msph_token_stream_read_tok(struct msph_token *, size_t, + struct msph_token_stream *); + #endif /* _MSPH_EXPR_H */ From b9266cdf96f410061b08460651669aefc499cab6 Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Tue, 15 Apr 2025 20:02:25 +0200 Subject: [PATCH 06/10] lexing up and running --- CMakeLists.txt | 12 +- include/msph/err.h | 20 ++ src/msph/msph_token.h => include/msph/token.h | 31 +- include/spho/err.h | 51 ++-- src/msph/msph.c | 153 ++++++++-- src/msph/{msph_token.c => token.c} | 269 ++++++++++++++---- 6 files changed, 434 insertions(+), 102 deletions(-) create mode 100644 include/msph/err.h rename src/msph/msph_token.h => include/msph/token.h (80%) rename src/msph/{msph_token.c => token.c} (59%) diff --git a/CMakeLists.txt b/CMakeLists.txt index 34e7f44..a972050 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -46,14 +46,18 @@ target_compile_definitions(devcheck PRIVATE set(MSPH_SRC - ${SRC_DIR}/msph/msph_token.c + ${SRC_DIR}/msph/token.c ${SRC_DIR}/msph/msph.c ) set(MSPH_HEADER - ${SRC_DIR}/msph/msph_token.h + ${INCLUDE_DIR}/msph/token.h ) -add_executable(msph ${MSPH_HEADER} ${MSPH_SRC}) +add_executable(msph ${MSPH_SRC} ${MSPH_HEADER}) target_include_directories(msph PRIVATE ${INCLUDE_DIR}) -target_link_libraries(devcheck spho) +target_link_libraries(msph spho) +target_compile_definitions(msph PRIVATE + $<$:SPHO_DEBUG> + $<$:SPHO_USE_STRLCPY> +) diff --git a/include/msph/err.h b/include/msph/err.h new file mode 100644 index 0000000..8fa7795 --- /dev/null +++ b/include/msph/err.h @@ -0,0 +1,20 @@ +#ifndef _MSPH_ERR_H +#define _MSPH_ERR_H + +#ifdef SPHO_DEBUG +// #define SPHO_ENABLE_DEBUG_PRINT +#endif + +#include "spho/err.h" + + +#define MSPH_ERR_SYS 0x0001 + +#define MSPH_ERR_INVAL 0x1001 + +#define MSPH_ERR_TOOLONG 0x2001 + +#define MSPH_ERR(ctx, e) SPHO_ERR(ctx, e) +#define MSPH_TOKS_ERR(toks, e) MSPH_ERR((toks)->ctx, e) + +#endif diff --git a/src/msph/msph_token.h b/include/msph/token.h similarity index 80% rename from src/msph/msph_token.h rename to include/msph/token.h index 7207052..93dc21a 100644 --- a/src/msph/msph_token.h +++ b/include/msph/token.h @@ -80,12 +80,17 @@ */ struct msph_ctx { - int err; - int err_info; + int err; + int err_info; + char errbuf[SPHO_ERR_BUF_LEN]; + +#ifdef SPHO_DEBUG + char filebuf[SPHO_ERR_FILEBUF_LEN]; + int errline; +#endif }; enum msph_tok_type { - TOK_START, TOK_LBRACE, // { TOK_RBRACE, // } TOK_LBRAK, // [ @@ -111,13 +116,14 @@ enum msph_tok_type { TOK_CONST_FALSE, // False TOK_IDENT, // identifiers - TOK_END + TOK_WSPACE, // special: whitespace + TOK_END // special: denote end of array }; -#define MSPH_TOKEN_BUF_SZ 128 +#define MSPH_TOKEN_BUF_LEN 128 struct token_s { - char buf[MSPH_TOKEN_BUF_SZ]; + char buf[MSPH_TOKEN_BUF_LEN]; }; union token_data { @@ -129,7 +135,7 @@ struct msph_token { union token_data d; }; -#define MSPH_PATH_LEN 1024 +#define MSPH_FILE_NAME_LEN 1024 #define MSPH_FILE_BUF_LEN 4096 #define MSPH_TOKEN_SRC_FILE 1 @@ -142,7 +148,7 @@ struct msph_token_src_file { char buf[MSPH_FILE_BUF_LEN]; /* file path */ - char name[MSPH_PATH_LEN]; + char name[MSPH_FILE_NAME_LEN]; }; #define MSPH_TOKEN_SRC_STR 2 @@ -168,8 +174,10 @@ struct msph_token_stream { struct msph_token_src src; }; -struct msph_token_stream *msph_token_stream_fopen(struct msph_ctx *, - const char *); +void msph_ctx_init(struct msph_ctx *); + +struct msph_token_stream *msph_token_stream_file(struct msph_ctx *, + FILE *, const char *); struct msph_token_stream *msph_token_stream_frombuf(struct msph_ctx *, const char *, size_t); @@ -177,6 +185,9 @@ int msph_token_stream_close(struct msph_token_stream*); ssize_t msph_token_stream_read_tok(struct msph_token *, size_t, struct msph_token_stream *); +int msph_token_stream_print(struct msph_token_stream *, FILE *); + +size_t msph_token_str(char *buf, size_t len, struct msph_token *tok); #endif /* _MSPH_EXPR_H */ diff --git a/include/spho/err.h b/include/spho/err.h index b4dcc33..0dd651d 100644 --- a/include/spho/err.h +++ b/include/spho/err.h @@ -16,8 +16,14 @@ #define SPHO_ERR_IS_SYSERR(err) (SPHO_ERR_SYS == err) +#define SPHO_ERR_BUF_LEN 2048 + + + #ifdef SPHO_DEBUG +#define SPHO_ERR_FILEBUF_LEN 128 + #define SPHO_ERR(ctx, e) \ do { \ (ctx)->err = (e); \ @@ -28,20 +34,6 @@ (ctx)->errline = __LINE__; \ } while (0) -#else /* SPHO_DEBUG */ - -#define SPHO_ERR(ctx, e) \ - do { \ - (ctx)->err = (e); \ - if ((e) == SPHO_ERR_SYS) \ - (ctx)->err_info = errno; \ - } while (0) - -#endif /* SPHO_DEBUG */ - -/* debug stuff */ -#ifdef SPHO_DEBUG - #define SPHO_STRINGIFY(a) #a #define SPHO_MACRO_STR(b) SPHO_STRINGIFY(b) @@ -77,10 +69,35 @@ } \ } while (0) -#else + +#ifdef SPHO_ENABLE_DEBUG_PRINT + +#define SPHO_DEBUG_PRINT(fmt, ...) \ + do { \ + fprintf(stderr, fmt __VA_OPT__(,) __VA_ARGS__); \ + } while (0) + +#else /* SPHO_ENABLE_DEBUG_PRINT */ + +#define SPHO_DEBUG_PRINT(fmt, ...) + +#endif /* SPHO_ENABLE_DEBUG_PRINT */ + +#else /* SPHO_DEBUG */ + +#define SPHO_ERR(ctx, e) \ + do { \ + (ctx)->err = (e); \ + if ((e) == SPHO_ERR_SYS) \ + (ctx)->err_info = errno; \ + } while (0) + #define SPHO_PRECOND(cond) #define SPHO_ASSERT(cond) #define SPHO_POSTCOND(cond) -#endif -#endif +#define SPHO_DBG_PRINT(fmt, ...) + +#endif /* SPHO_DEBUG */ + +#endif /* _SPHO_ERR_H */ diff --git a/src/msph/msph.c b/src/msph/msph.c index 8643a46..b85945c 100644 --- a/src/msph/msph.c +++ b/src/msph/msph.c @@ -1,40 +1,147 @@ +#include #include +#include - - -#include "msph_token.h" +#include "msph/err.h" +#include "msph/token.h" #define PRINTERR(ctx) \ do { \ fprintf(stderr, "msph_err: %d (%d)\n", (ctx).err, (ctx).err_info); \ } while (0) +#ifdef SPHO_DEBUG +#define DEBUGFLAG "d" +#endif + +struct msph_opts { + int tokenize_only; +#ifdef DEBUGFLAG + int debug; +#endif + const char *in_path; + const char *out_path; +} run_opts = { + 0, +#ifdef DEBUGFLAG + 0, +#endif + NULL, + NULL +}; + + +#define USAGE \ + "msph: micro sappho\n" \ + "\tUsage: msph [-t] [-o out_path] [in_path]\n" \ + "\n" \ + "\t-t - print tokenization\n" \ + "\t-o - output path\n" + + +void +print_usage(void) +{ + printf("%s", USAGE); +} + +int run(struct msph_opts *); int -main(int argc, char **argv) +main(int argc, char *argv[]) { - int ret; - char *path; - struct msph_ctx ctx; - struct msph_token_stream *s; + int opt; - - if (argc != 2) - return (-1); - - - path = argv[1]; - - ctx.err = 0; - ctx.err_info = 0; - - if ((s = msph_token_stream_fopen(&ctx, path)) == NULL) { - PRINTERR(ctx); - return (-1); + while ((opt = getopt(argc, argv, DEBUGFLAG "to:")) != -1) { + switch (opt) { + case 't': + run_opts.tokenize_only = 1; + break; + case 'o': + run_opts.out_path = optarg; + break; +#ifdef DEBUGFLAG + case 'd': + run_opts.debug = 1; + break; +#endif + case '?': + default: + print_usage(); + exit(EXIT_FAILURE); + } } + argc -= optind; + argv += optind; - ret = msph_token_stream_close(s); + if (argc > 1) { + print_usage(); + exit(EXIT_FAILURE); + } - return (ret); + if (argc == 1) + run_opts.in_path = argv[0]; + + if (run(&run_opts)) + exit(EXIT_FAILURE); +} + + +int +run(struct msph_opts *opts) +{ + int ret; + struct msph_ctx ctx; + struct msph_token_stream *s; + FILE *in, *out; + + in = out = NULL; + + msph_ctx_init(&ctx); + + if (opts->in_path == NULL) { + in = stdin; opts->in_path = "stdin"; + } else { + if ((in = fopen(opts->in_path, "r")) == NULL) { + MSPH_ERR(&ctx, MSPH_ERR_SYS); + goto err; + } + } + + if (opts->out_path == NULL) { + out = stdout; + } else { + if ((out = fopen(opts->out_path, "w")) == NULL) { + MSPH_ERR(&ctx, MSPH_ERR_SYS); + goto err; + } + } + + if ((s = msph_token_stream_file(&ctx, in, opts->in_path)) == NULL) { + goto err; + } + + printf("msph v0, parsing %s\n", opts->in_path); + + if ((ret = msph_token_stream_print(s, out)) == -1) + goto err; + + if (opts->tokenize_only) + goto exit; + +exit: + if (msph_token_stream_close(s) == -1) + goto err; + + return (0); + +err: + PRINTERR(ctx); + + if (in) + fclose(in); + if (out) + fclose(out); + return (-1); } diff --git a/src/msph/msph_token.c b/src/msph/token.c similarity index 59% rename from src/msph/msph_token.c rename to src/msph/token.c index f69c8b6..959546f 100644 --- a/src/msph/msph_token.c +++ b/src/msph/token.c @@ -5,34 +5,94 @@ #include #include -#include "spho/err.h" - -#include "msph_token.h" +#include "msph/err.h" +#include "msph/token.h" -#define MSPH_ERR_SYS 0x0001 -#define MSPH_ERR_TOOLONG 0x0002 - -#define MSPH_ERR(ctx, e) SPHO_ERR(ctx, e) -#define MSPH_TOKS_ERR(toks, e) MSPH_ERR((toks)->ctx, e) - -struct msph_token_matcher { +struct msph_matcher { size_t off; size_t matchlen; const int type; -} msph_matcher[] = { - { 0, 0, TOK_START }, +}; + +struct msph_matcher token_matcher[] = { + { 0, 0, -1 }, + { 0, 0, TOK_LBRACE }, + { 0, 0, TOK_RBRACE }, + { 0, 0, TOK_LBRAK }, + { 0, 0, TOK_RBRAK }, + { 0, 0, TOK_LPAREN }, + { 0, 0, TOK_RPAREN }, + { 0, 0, TOK_COLON }, + { 0, 0, TOK_EQUALS }, + + { 0, 0, TOK_AMP }, + { 0, 0, TOK_PIPE }, + { 0, 0, TOK_RARROW }, + { 0, 0, TOK_SUB }, + + { 0, 0, TOK_KW_TYPE }, + { 0, 0, TOK_KW_NOMINAL }, + { 0, 0, TOK_KW_MEMBER }, + { 0, 0, TOK_KW_CHECK }, + { 0, 0, TOK_KW_BOX }, + { 0, 0, TOK_KW_FORALL }, + + { 0, 0, TOK_CONST_TRUE }, + { 0, 0, TOK_CONST_FALSE }, + { 0, 0, TOK_IDENT }, { 0, 0, TOK_END } }; +struct msph_matcher wspace = { 0, 0, TOK_WSPACE }; + +struct msph_token_info { + const int type; + const char *dbg_str; + const char *str; +} token_info[] = { +#define TOK_INFO(tok, s) { tok , #tok, s } + TOK_INFO(TOK_LBRACE, "{"), + TOK_INFO(TOK_RBRACE, "}"), + TOK_INFO(TOK_LBRAK, "["), + TOK_INFO(TOK_RBRAK, "]"), + TOK_INFO(TOK_LPAREN, "("), + TOK_INFO(TOK_RPAREN, ")"), + TOK_INFO(TOK_COLON, ":"), + TOK_INFO(TOK_EQUALS, "="), + + TOK_INFO(TOK_AMP, "&"), + TOK_INFO(TOK_PIPE, "|"), + TOK_INFO(TOK_RARROW, "=>"), + TOK_INFO(TOK_SUB, "<:"), + + TOK_INFO(TOK_KW_TYPE, "type"), + TOK_INFO(TOK_KW_NOMINAL, "nominal"), + TOK_INFO(TOK_KW_MEMBER, "member"), + TOK_INFO(TOK_KW_CHECK, "check"), + TOK_INFO(TOK_KW_BOX, "box"), + TOK_INFO(TOK_KW_FORALL, "forall"), + + TOK_INFO(TOK_CONST_TRUE, "True"), + TOK_INFO(TOK_CONST_FALSE, "False"), + + TOK_INFO(TOK_IDENT, NULL), + TOK_INFO(TOK_WSPACE, NULL), + { TOK_END , NULL, NULL } +#undef TOK_INFO +}; + + + +#define BUF_LEN(b) ((sizeof(b) / sizeof((b)[0]))) static ssize_t src_file_fill_buf(struct msph_ctx *, struct msph_token_src_file *); static int tok_match(struct msph_ctx *, struct msph_token_src *, - struct msph_token_matcher *); + struct msph_matcher *); static int tok_commit(struct msph_ctx *, struct msph_token_src *, - struct msph_token_matcher *, struct msph_token *); + struct msph_matcher *, struct msph_token *); static int char_at(struct msph_ctx *, struct msph_token_src *, size_t, char *); static int fromcbuf_charcpy(char *, const char *, size_t, size_t, size_t); @@ -41,18 +101,27 @@ static int file_char_at(struct msph_ctx *, struct msph_token_src *, size_t, static int read_single_tok(struct msph_token *, struct msph_token_stream *); -struct msph_token_stream * -msph_token_stream_fopen(struct msph_ctx *ctx, const char *path) +static const char *tok_base_str(struct msph_token *); + + +void msph_ctx_init(struct msph_ctx *ctx) +{ + ctx->err = 0; + ctx->err_info = 0; +} + +struct msph_token_stream * +msph_token_stream_file(struct msph_ctx *ctx, FILE *f, const char *name) { - FILE *f; size_t res; struct msph_token_stream *ret; - if ((f = fopen(path, "r")) == NULL) { - MSPH_ERR(ctx, MSPH_ERR_SYS); + if (ctx == NULL || f == NULL || name == NULL) { + MSPH_ERR(ctx, MSPH_ERR_INVAL); return (NULL); } + if ((ret = calloc(1, sizeof(struct msph_token_stream))) == NULL) { MSPH_ERR(ctx, MSPH_ERR_SYS); goto err; @@ -64,7 +133,7 @@ msph_token_stream_fopen(struct msph_ctx *ctx, const char *path) ret->src.inner.file.pos = 0; ret->src.inner.file.end = 0; - res = strlcpy(ret->src.inner.file.name, path, + res = strlcpy(ret->src.inner.file.name, name, sizeof(ret->src.inner.file.name)); if (res >= sizeof(ret->src.inner.file.name)) { MSPH_ERR(ctx, MSPH_ERR_TOOLONG); @@ -101,6 +170,53 @@ msph_token_stream_frombuf(struct msph_ctx *ctx, const char *buf, size_t len) return (ret); } +size_t +msph_token_str(char *buf, size_t len, struct msph_token *tok) +{ + size_t ret; + + ret = snprintf(buf, len, "%s", tok_base_str(tok)); + + if (ret > len) + return (ret); + + len -= ret; + buf += ret; + + switch (tok->type) { + case TOK_IDENT: + ret += snprintf(buf, len, "(%s)", tok->d.s.buf); + break; + default: + break; + } + + return (ret); +} + +#define MSPH_TOKEN_PRINT_BUF_LEN 2 * MSPH_TOKEN_BUF_LEN +int +msph_token_stream_print(struct msph_token_stream *s, FILE *out) +{ + ssize_t ret; + ssize_t i; + struct msph_token tok; + char tokstr[MSPH_TOKEN_PRINT_BUF_LEN]; + + while ((ret = msph_token_stream_read_tok( &tok, 1, s)) > 0) { + SPHO_DEBUG_PRINT("msph_token_stream_print: ret=%zd\n", ret); + if (msph_token_str( + tokstr, BUF_LEN(tokstr), &tok) > BUF_LEN(tokstr)) { + tokstr[BUF_LEN(tokstr) - 1] = '\0'; + } + fprintf(out, "%s\n", tokstr); + } + + SPHO_DEBUG_PRINT("msph_token_stream_print: ret=%zd\n", ret); + + return ((int)ret); +} + int msph_token_stream_close(struct msph_token_stream *s) @@ -128,24 +244,21 @@ ssize_t msph_token_stream_read_tok(struct msph_token *ptr, size_t n, struct msph_token_stream *s) { - ssize_t ret; - size_t i; + size_t ret; int res; ret = 0; res = -1; - while ((res = read_single_tok(&ptr[i], s)) == 1) { - if (res == -1) { - ret = -1; - break; - } + while (ret < n && (res = read_single_tok(&ptr[ret], s)) != 0) { + if (res == -1) + return (-1); ret++; } - return (ret); + return ((ssize_t)ret); } -/* 1: success, 0: failed match, -1: error */ +/* 1: matched token, 0: failed to match token, -1: error */ static int read_single_tok(struct msph_token *ptr, struct msph_token_stream *s) { @@ -158,15 +271,23 @@ read_single_tok(struct msph_token *ptr, struct msph_token_stream *s) ctx = s->ctx; src = &s->src; + /* Skipping whitespace */ + if (tok_match(ctx, src, &wspace) == -1) + return (-1); + if (wspace.matchlen > 0 && + tok_commit(ctx, src, &wspace, NULL) == -1) + return (-1); + max_m = 0; - for (m = 0; msph_matcher[m].type != TOK_END; m++) { - res = tok_match(ctx, src, &msph_matcher[m]); + for (m = 1; token_matcher[m].type != TOK_END; m++) { + res = tok_match(ctx, src, &token_matcher[m]); + SPHO_DEBUG_PRINT("read_single_tok: tok_match=%d\n", res); if (res == -1) return (-1); if (res == 0 && - msph_matcher[m].matchlen > msph_matcher[max_m].matchlen) { + token_matcher[m].matchlen > token_matcher[max_m].matchlen) { max_m = m; } } @@ -174,15 +295,15 @@ read_single_tok(struct msph_token *ptr, struct msph_token_stream *s) if (max_m == 0) return (0); - if (tok_commit(ctx, src, &msph_matcher[max_m], ptr) == -1) + SPHO_DEBUG_PRINT("read_single_tok: commit=%zu\n", max_m); + if (tok_commit(ctx, src, &token_matcher[max_m], ptr) == -1) return (-1); + SPHO_DEBUG_PRINT("read_single_tok: committed\n"); return (1); } -#define BUF_LEN(b) (sizeof(b) / sizeof((b)[0])) - static ssize_t src_file_fill_buf(struct msph_ctx *ctx, struct msph_token_src_file *file) { @@ -207,6 +328,9 @@ src_file_fill_buf(struct msph_ctx *ctx, struct msph_token_src_file *file) ret += nread; file->end = (file->end + nread) % BUF_LEN(file->buf); + SPHO_DEBUG_PRINT("src_file_fill_buf: valid range (%zu, %zu)\n", + file->pos, file->end); + if (nread < maxread) { if (ferror(file->f)) { MSPH_ERR(ctx, MSPH_ERR_SYS); @@ -217,6 +341,8 @@ src_file_fill_buf(struct msph_ctx *ctx, struct msph_token_src_file *file) } while (file->end != file->pos); + SPHO_DEBUG_PRINT("src_file_fill_buf: read %zd\n", ret); + return (ret); } @@ -229,13 +355,16 @@ file_char_at(struct msph_ctx *ctx, struct msph_token_src *src, size_t i, ssize_t fill; struct msph_token_src_file *file; - SPHO_PRECOND(s != NULL); - SPHO_PRECOND(s->src.type == MSPH_TOKEN_SRC_FILE); + SPHO_PRECOND(src != NULL); + SPHO_PRECOND(src->type == MSPH_TOKEN_SRC_FILE); ret = 0; file = &src->inner.file; + fill = 0; do { + SPHO_DEBUG_PRINT("want to read %zu, valid range (%zu, %zu)\n", + (file->pos + i) % BUF_LEN(file->buf), file->pos, file->end); /* simplest case */ if (file->pos + i < file->end) { *out = file->buf[file->pos + i]; @@ -250,11 +379,12 @@ file_char_at(struct msph_ctx *ctx, struct msph_token_src *src, size_t i, if (feof(file->f)) return (0); - if (src_file_fill_buf(ctx, file) == -1) + if ((fill = src_file_fill_buf(ctx, file)) == -1) return (-1); - } while (ret++); - return (-1); + } while (fill > 0 && ret++); + + return (ret); } static int @@ -265,18 +395,22 @@ char_at(struct msph_ctx *ctx, struct msph_token_src *src, size_t i, char *out) switch (src->type) { case MSPH_TOKEN_SRC_FILE: - return (file_char_at(ctx, src, i, out)); + ret = file_char_at(ctx, src, i, out); + break; case MSPH_TOKEN_SRC_STR: str = &src->inner.str; if (str->pos + i < str->len) { *out = str->s[str->pos + i]; - return (1); + ret = 1; + } else { + ret = 0; } - return (0); + break; default: break; } + SPHO_DEBUG_PRINT("char_at: ret=%d, *out=%c\n", ret, *out); return (ret); } @@ -289,9 +423,11 @@ fromcbuf_charcpy(char *dst, const char *src, size_t src_len, size_t src_pos, return (-1); } - cpy1 = src_pos + ncpy < src_len ? ncpy : src_len - src_pos; + cpy1 = (src_pos + ncpy < src_len) ? ncpy : src_len - src_pos; cpy2 = ncpy - cpy1; + SPHO_DEBUG_PRINT("fromcbuf_charcpy: cpy1=%zu cpy2=%zu\n", cpy1, cpy2); + memcpy(dst, &src[src_pos], cpy1 * sizeof(src[0])); if (! cpy2) @@ -304,27 +440,30 @@ fromcbuf_charcpy(char *dst, const char *src, size_t src_len, size_t src_pos, static int tok_match(struct msph_ctx *ctx, struct msph_token_src *src, - struct msph_token_matcher *m) + struct msph_matcher *m) { int res; int more; char chr; const char *match_str; size_t off, len; - SPHO_PRECOND(m != NULL && s != NULL); + SPHO_PRECOND(m != NULL && src != NULL); m->matchlen = 0; #define MATCH_CHAR(c) \ do { \ + SPHO_DEBUG_PRINT("tok_match: '%c'\n", c); \ if ((res = char_at(ctx, src, 0, &chr)) == -1) \ return (-1); \ else if (res == 0) \ return (0); \ + SPHO_DEBUG_PRINT("tok_match: char_at(0)='%c'\n", c); \ \ if (chr == (c)) { \ m->matchlen = 1; \ } \ + SPHO_DEBUG_PRINT("tok_match: matchlen=%zu\n", m->matchlen); \ return (0); \ } while (0) @@ -397,6 +536,16 @@ tok_match(struct msph_ctx *ctx, struct msph_token_src *src, if (res == -1) return (-1); return (0); + case TOK_WSPACE: + off = 0; + while((res = char_at(ctx, src, off++, &chr)) == 1) { + if (! isspace(chr)) + break; + m->matchlen++; + } + if (res == -1) + return (-1); + return (0); default: SPHO_ASSERT(0); return (-1); @@ -409,40 +558,50 @@ tok_match(struct msph_ctx *ctx, struct msph_token_src *src, #define TOK_HAS_DATA(type) (type == TOK_IDENT) static int tok_commit(struct msph_ctx *ctx, struct msph_token_src *src, - struct msph_token_matcher *m, struct msph_token *ptr) + struct msph_matcher *m, struct msph_token *ptr) { size_t pos_old; struct msph_token_src_str *str; struct msph_token_src_file *file; - SPHO_PRECOND(p != NULL && m != NULL); + SPHO_PRECOND(ctx != NULL && m != NULL); SPHO_PRECOND(m->matchlen != 0); + SPHO_DEBUG_PRINT("committing\n"); + switch (src->type) { case MSPH_TOKEN_SRC_FILE: file = &src->inner.file; pos_old = file->pos; + SPHO_DEBUG_PRINT("committing\n"); file->pos += m->matchlen; file->pos %= BUF_LEN(file->buf); SPHO_ASSERT(file->pos < BUF_LEN(file->buf) || file->pos < pos_old); + SPHO_DEBUG_PRINT("committing\n"); + if (ptr == NULL) + return (0); + ptr->type = m->type; if (! TOK_HAS_DATA(ptr->type)) return (0); + SPHO_DEBUG_PRINT("committing\n"); if (m->matchlen >= sizeof(ptr->d.s.buf)) { MSPH_ERR(ctx, MSPH_ERR_TOOLONG); return (-1); } + SPHO_DEBUG_PRINT("committing\n"); if (fromcbuf_charcpy(ptr->d.s.buf, file->buf, sizeof(file->buf), pos_old, m->matchlen) == -1) { MSPH_ERR(ctx, MSPH_ERR_TOOLONG); return (-1); } + SPHO_DEBUG_PRINT("committing\n"); ptr->d.s.buf[m->matchlen] = '\0'; return (0); @@ -453,6 +612,9 @@ tok_commit(struct msph_ctx *ctx, struct msph_token_src *src, str->pos += m->matchlen; SPHO_ASSERT(str->pos <= str->len); + if (ptr == NULL) + return (0); + ptr->type = m->type; if (! TOK_HAS_DATA(ptr->type)) return (0); @@ -474,6 +636,17 @@ tok_commit(struct msph_ctx *ctx, struct msph_token_src *src, +static const char * +tok_base_str(struct msph_token *tok) +{ + size_t i; + for (i = 0; token_info[i].type != TOK_END; i++) { + if (token_info[i].type == tok->type) + return (token_info[i].dbg_str); + } + + return (NULL); +} From 9b24c8a496d6354a9cd9571e1ab9778db55d387c Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Tue, 15 Apr 2025 23:50:14 +0200 Subject: [PATCH 07/10] proper c flags --- CMakeLists.txt | 7 +++++++ include/msph/token.h | 7 ++++--- src/msph/token.c | 49 +++++++++++++++++++------------------------- 3 files changed, 32 insertions(+), 31 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index a972050..3067de7 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -3,6 +3,13 @@ project(log-e-sappho C) set(CMAKE_C_STANDARD 99) set(CMAKE_C_STANDARD_REQUIRED True) +string(JOIN " " CMAKE_C_FLAGS + "-Wall -Wextra -Wformat=2" + "-Wconversion -Wsign-conversion -Wimplicit-fallthrough" + "-Werror=implicit -Werror=incompatible-pointer-types" + "-Werror=int-conversion") +set(CMAKE_VERBOSE_MAKEFILE ON) + include(CheckSymbolExists) diff --git a/include/msph/token.h b/include/msph/token.h index 93dc21a..2177b2c 100644 --- a/include/msph/token.h +++ b/include/msph/token.h @@ -102,7 +102,8 @@ enum msph_tok_type { TOK_AMP, // & TOK_PIPE, // | - TOK_RARROW, // => + TOK_IMPL, // => + TOK_RARROW, // -> TOK_SUB, // <: TOK_KW_TYPE, // type @@ -136,7 +137,7 @@ struct msph_token { }; #define MSPH_FILE_NAME_LEN 1024 -#define MSPH_FILE_BUF_LEN 4096 +#define MSPH_FILE_BUF_LEN 2048 #define MSPH_TOKEN_SRC_FILE 1 struct msph_token_src_file { @@ -187,7 +188,7 @@ ssize_t msph_token_stream_read_tok(struct msph_token *, size_t, struct msph_token_stream *); int msph_token_stream_print(struct msph_token_stream *, FILE *); -size_t msph_token_str(char *buf, size_t len, struct msph_token *tok); +ssize_t msph_token_str(char *buf, size_t len, struct msph_token *tok); #endif /* _MSPH_EXPR_H */ diff --git a/src/msph/token.c b/src/msph/token.c index 959546f..299e828 100644 --- a/src/msph/token.c +++ b/src/msph/token.c @@ -29,6 +29,7 @@ struct msph_matcher token_matcher[] = { { 0, 0, TOK_AMP }, { 0, 0, TOK_PIPE }, + { 0, 0, TOK_IMPL }, { 0, 0, TOK_RARROW }, { 0, 0, TOK_SUB }, @@ -64,7 +65,8 @@ struct msph_token_info { TOK_INFO(TOK_AMP, "&"), TOK_INFO(TOK_PIPE, "|"), - TOK_INFO(TOK_RARROW, "=>"), + TOK_INFO(TOK_IMPL, "=>"), + TOK_INFO(TOK_RARROW, "->"), TOK_INFO(TOK_SUB, "<:"), TOK_INFO(TOK_KW_TYPE, "type"), @@ -170,22 +172,22 @@ msph_token_stream_frombuf(struct msph_ctx *ctx, const char *buf, size_t len) return (ret); } -size_t +ssize_t msph_token_str(char *buf, size_t len, struct msph_token *tok) { - size_t ret; + ssize_t ret; - ret = snprintf(buf, len, "%s", tok_base_str(tok)); + ret = (ssize_t)snprintf(buf, len, "%s", tok_base_str(tok)); - if (ret > len) + if (ret < 0 || ret >= (ssize_t)len) return (ret); - len -= ret; + len -= (size_t)ret; buf += ret; switch (tok->type) { case TOK_IDENT: - ret += snprintf(buf, len, "(%s)", tok->d.s.buf); + ret += (ssize_t)snprintf(buf, len, "(%s)", tok->d.s.buf); break; default: break; @@ -199,20 +201,19 @@ int msph_token_stream_print(struct msph_token_stream *s, FILE *out) { ssize_t ret; - ssize_t i; struct msph_token tok; char tokstr[MSPH_TOKEN_PRINT_BUF_LEN]; while ((ret = msph_token_stream_read_tok( &tok, 1, s)) > 0) { - SPHO_DEBUG_PRINT("msph_token_stream_print: ret=%zd\n", ret); - if (msph_token_str( - tokstr, BUF_LEN(tokstr), &tok) > BUF_LEN(tokstr)) { - tokstr[BUF_LEN(tokstr) - 1] = '\0'; - } - fprintf(out, "%s\n", tokstr); - } + ret = msph_token_str(tokstr, BUF_LEN(tokstr), &tok); + if (ret < 0) + continue; - SPHO_DEBUG_PRINT("msph_token_stream_print: ret=%zd\n", ret); + if ((size_t)ret < BUF_LEN(tokstr)) + fprintf(out, "%s\n", tokstr); + else + fprintf(out, "%s...(trunkated)", tokstr); + } return ((int)ret); } @@ -281,7 +282,6 @@ read_single_tok(struct msph_token *ptr, struct msph_token_stream *s) max_m = 0; for (m = 1; token_matcher[m].type != TOK_END; m++) { res = tok_match(ctx, src, &token_matcher[m]); - SPHO_DEBUG_PRINT("read_single_tok: tok_match=%d\n", res); if (res == -1) return (-1); @@ -295,10 +295,8 @@ read_single_tok(struct msph_token *ptr, struct msph_token_stream *s) if (max_m == 0) return (0); - SPHO_DEBUG_PRINT("read_single_tok: commit=%zu\n", max_m); if (tok_commit(ctx, src, &token_matcher[max_m], ptr) == -1) return (-1); - SPHO_DEBUG_PRINT("read_single_tok: committed\n"); return (1); } @@ -393,6 +391,7 @@ char_at(struct msph_ctx *ctx, struct msph_token_src *src, size_t i, char *out) int ret; struct msph_token_src_str *str; + ret = -1; switch (src->type) { case MSPH_TOKEN_SRC_FILE: ret = file_char_at(ctx, src, i, out); @@ -443,7 +442,6 @@ tok_match(struct msph_ctx *ctx, struct msph_token_src *src, struct msph_matcher *m) { int res; - int more; char chr; const char *match_str; size_t off, len; @@ -506,8 +504,10 @@ tok_match(struct msph_ctx *ctx, struct msph_token_src *src, MATCH_CHAR('&'); case TOK_PIPE: MATCH_CHAR('|'); - case TOK_RARROW: + case TOK_IMPL: MATCH_STR("=>"); + case TOK_RARROW: + MATCH_STR("->"); case TOK_SUB: MATCH_STR("<:"); case TOK_KW_TYPE: @@ -567,20 +567,16 @@ tok_commit(struct msph_ctx *ctx, struct msph_token_src *src, SPHO_PRECOND(ctx != NULL && m != NULL); SPHO_PRECOND(m->matchlen != 0); - SPHO_DEBUG_PRINT("committing\n"); - switch (src->type) { case MSPH_TOKEN_SRC_FILE: file = &src->inner.file; pos_old = file->pos; - SPHO_DEBUG_PRINT("committing\n"); file->pos += m->matchlen; file->pos %= BUF_LEN(file->buf); SPHO_ASSERT(file->pos < BUF_LEN(file->buf) || file->pos < pos_old); - SPHO_DEBUG_PRINT("committing\n"); if (ptr == NULL) return (0); @@ -588,20 +584,17 @@ tok_commit(struct msph_ctx *ctx, struct msph_token_src *src, if (! TOK_HAS_DATA(ptr->type)) return (0); - SPHO_DEBUG_PRINT("committing\n"); if (m->matchlen >= sizeof(ptr->d.s.buf)) { MSPH_ERR(ctx, MSPH_ERR_TOOLONG); return (-1); } - SPHO_DEBUG_PRINT("committing\n"); if (fromcbuf_charcpy(ptr->d.s.buf, file->buf, sizeof(file->buf), pos_old, m->matchlen) == -1) { MSPH_ERR(ctx, MSPH_ERR_TOOLONG); return (-1); } - SPHO_DEBUG_PRINT("committing\n"); ptr->d.s.buf[m->matchlen] = '\0'; return (0); From 9ac779c1cfc0748a77563503319592b753cb0613 Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Sat, 19 Apr 2025 20:35:42 +0300 Subject: [PATCH 08/10] prefix notation type parser --- .clangd | 2 + .gitignore | 4 +- CMakeLists.txt | 3 + include/msph/common.h | 18 + include/msph/err.h | 24 +- include/msph/token.h | 92 ++--- include/msph/tree.h | 239 +++++++++++++ include/spho/err.h | 21 +- include/spho/tp.h | 3 +- include/spho/util.h | 7 + src/msph/README.md | 15 +- src/msph/msph.c | 22 +- src/msph/token.c | 157 ++++++--- src/msph/tree.c | 761 ++++++++++++++++++++++++++++++++++++++++++ 14 files changed, 1217 insertions(+), 151 deletions(-) create mode 100644 .clangd create mode 100644 include/msph/common.h create mode 100644 include/msph/tree.h create mode 100644 src/msph/tree.c diff --git a/.clangd b/.clangd new file mode 100644 index 0000000..ba4cbb3 --- /dev/null +++ b/.clangd @@ -0,0 +1,2 @@ +Diagnostics: + UnusedIncludes: None diff --git a/.gitignore b/.gitignore index 58189c6..75a6986 100644 --- a/.gitignore +++ b/.gitignore @@ -51,9 +51,11 @@ Module.symvers Mkfile.old dkms.conf -# CMake build directory +# CMake build dirs build-*/ +# CMake compile commands +compile_commands.json # vim .*.swp diff --git a/CMakeLists.txt b/CMakeLists.txt index 3067de7..b9c8a66 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -10,6 +10,8 @@ string(JOIN " " CMAKE_C_FLAGS "-Werror=int-conversion") set(CMAKE_VERBOSE_MAKEFILE ON) +set(CMAKE_EXPORT_COMPILE_COMMANDS ON) + include(CheckSymbolExists) @@ -54,6 +56,7 @@ target_compile_definitions(devcheck PRIVATE set(MSPH_SRC ${SRC_DIR}/msph/token.c + ${SRC_DIR}/msph/tree.c ${SRC_DIR}/msph/msph.c ) diff --git a/include/msph/common.h b/include/msph/common.h new file mode 100644 index 0000000..0a0bda2 --- /dev/null +++ b/include/msph/common.h @@ -0,0 +1,18 @@ +#ifndef _MSPH_COMMON_H +#define _MSPH_COMMON_H + +#include "msph/err.h" + +#define MSPH_IDENT_LEN 128 + +struct msph_ctx { + int err; + int err_info; + char errbuf[SPHO_ERR_BUF_LEN]; + +#ifdef SPHO_DEBUG + char filebuf[SPHO_ERR_FILEBUF_LEN]; + int errline; +#endif +}; +#endif diff --git a/include/msph/err.h b/include/msph/err.h index 8fa7795..41a89d9 100644 --- a/include/msph/err.h +++ b/include/msph/err.h @@ -10,11 +10,31 @@ #define MSPH_ERR_SYS 0x0001 -#define MSPH_ERR_INVAL 0x1001 +#define MSPH_ERR_INVAL 0x0002 -#define MSPH_ERR_TOOLONG 0x2001 +#define MSPH_ERR_TOKEN_TOOLONG 0x1001 +#define MSPH_ERR_TOKEN_EOF 0x1002 +#define MSPH_ERR_TOKEN_NOMATCH 0x1003 +#define MSPH_ERR_TOKEN_INVAL 0x1004 + +#define MSPH_ERR_TREE_TOOLONG 0x2001 +#define MSPH_ERR_TREE_EOF 0x2002 +#define MSPH_ERR_TREE_NOMATCH 0x2003 + + +// TODO add more diagnostics #define MSPH_ERR(ctx, e) SPHO_ERR(ctx, e) #define MSPH_TOKS_ERR(toks, e) MSPH_ERR((toks)->ctx, e) +#define MSPH_ERR_INFO(ctx, e, info) SPHO_ERR_INFO(ctx, e, info) + + +#define MSPH_ERR_RESET(ctx) \ + do { \ + ctx->err = 0; \ + ctx->err_info = 0; \ + } while (0) + + #endif diff --git a/include/msph/token.h b/include/msph/token.h index 2177b2c..a8896d3 100644 --- a/include/msph/token.h +++ b/include/msph/token.h @@ -1,53 +1,11 @@ #ifndef _MSPH_EXPR_H #define _MSPH_EXPR_H +#include + +#include "msph/common.h" + /* - * TYPES: - * Conj - * Disj - * Impl - * Arrow - * Box - * (Sub) - * Forall - * - * True - * False - * Var - * Nominal - * - * Record - * - * DEFINITIONS/DIRECTIVES: - * Type definition (type A[X..] = T) - * Nominal definition (nominal N) - * Member definition (member mname : T) - * - * { - * member a: A - * member b: B - * } - * - * Subtyping check (check A <: B, checks if A <: B) - * - * EXTRA DEFINITIONS - * Class definition (class C[...] { ... }, shorthand) - * - * EXPRESSIONS - * Conj - * Disj - * Impl - * Arrow - * Box - * (Sub) - * Forall - * - * True - * False - * Var - * Nominal - * - * Trait ({ ... }, creates scoping) * * * TOKENS @@ -79,16 +37,6 @@ * */ -struct msph_ctx { - int err; - int err_info; - char errbuf[SPHO_ERR_BUF_LEN]; - -#ifdef SPHO_DEBUG - char filebuf[SPHO_ERR_FILEBUF_LEN]; - int errline; -#endif -}; enum msph_tok_type { TOK_LBRACE, // { @@ -99,6 +47,8 @@ enum msph_tok_type { TOK_RPAREN, // ) TOK_COLON, // : TOK_EQUALS, // = + TOK_COMMA, // , + TOK_DOT, // . TOK_AMP, // & TOK_PIPE, // | @@ -109,7 +59,7 @@ enum msph_tok_type { TOK_KW_TYPE, // type TOK_KW_NOMINAL, // nominal TOK_KW_MEMBER, // member - TOK_KW_CHECK, // check + TOK_KW_ASSERT, // assert TOK_KW_BOX, // box TOK_KW_FORALL, // forall @@ -117,23 +67,20 @@ enum msph_tok_type { TOK_CONST_FALSE, // False TOK_IDENT, // identifiers + TOK_INVAL, // special: invalid, use to mark invalid toks TOK_WSPACE, // special: whitespace TOK_END // special: denote end of array }; -#define MSPH_TOKEN_BUF_LEN 128 - -struct token_s { - char buf[MSPH_TOKEN_BUF_LEN]; -}; - -union token_data { - struct token_s s; +union msph_token_data { + char str[MSPH_IDENT_LEN]; }; struct msph_token { int type; - union token_data d; + union msph_token_data data; + + SLIST_ENTRY(msph_token) entries; }; #define MSPH_FILE_NAME_LEN 1024 @@ -147,9 +94,6 @@ struct msph_token_src_file { size_t pos; size_t end; char buf[MSPH_FILE_BUF_LEN]; - - /* file path */ - char name[MSPH_FILE_NAME_LEN]; }; #define MSPH_TOKEN_SRC_STR 2 @@ -178,17 +122,21 @@ struct msph_token_stream { void msph_ctx_init(struct msph_ctx *); struct msph_token_stream *msph_token_stream_file(struct msph_ctx *, - FILE *, const char *); + FILE *); struct msph_token_stream *msph_token_stream_frombuf(struct msph_ctx *, const char *, size_t); int msph_token_stream_close(struct msph_token_stream*); -ssize_t msph_token_stream_read_tok(struct msph_token *, size_t, +ssize_t msph_token_stream_read(struct msph_token *, size_t, struct msph_token_stream *); +int msph_token_stream_eof(struct msph_token_stream *); int msph_token_stream_print(struct msph_token_stream *, FILE *); -ssize_t msph_token_str(char *buf, size_t len, struct msph_token *tok); +ssize_t msph_token_str(char *, size_t, struct msph_token *); + +struct msph_token * msph_token_create(struct msph_ctx *, int, + union msph_token_data *); #endif /* _MSPH_EXPR_H */ diff --git a/include/msph/tree.h b/include/msph/tree.h new file mode 100644 index 0000000..601c35f --- /dev/null +++ b/include/msph/tree.h @@ -0,0 +1,239 @@ +#ifndef _MSPH_TREE_H +#define _MSPH_TREE_H + +#include + +#include "msph/common.h" +#include "msph/token.h" + +/* + * TYPES: + * Conj + * Disj + * Impl + * Arrow + * Box + * (Sub) + * Forall + * + * True + * False + * Var + * Nominal + * + * Record + * + * DEFINITIONS/DIRECTIVES: + * Type definition (type A[X..] = T) + * Nominal definition (nominal N) + * Member definition (member mname : T) + * + * { + * member a: A + * member b: B + * } + * + * Subtyping assert (assert A <: B, asserts that A <: B) + * + * EXTRA DEFINITIONS + * Class definition (class C[...] { ... }, shorthand) + * + * EXPRESSIONS + * Conj + * Disj + * Impl + * Arrow + * Box + * (Sub) + * Forall + * + * True + * False + * Var + * Nominal + * + * Trait ({ ... }, creates scoping) + */ + +#define MSPH_TREE_ROOT 0x0001 + +#define MSPH_TREE_BODY 0x0010 + +#define MSPH_TREE_DIR 0x0020 +#define MSPH_TREE_TPDEF 0x0021 +#define MSPH_TREE_NOMINDECL 0x0022 +#define MSPH_TREE_MEMBDECL 0x0023 +#define MSPH_TREE_ASSERT 0x0024 + +#define MSPH_TREE_TPEXPR 0x0040 +#define MSPH_TREE_TRUE 0x0041 +#define MSPH_TREE_FALSE 0x0042 +#define MSPH_TREE_NAME 0x0043 +#define MSPH_TREE_APPL 0x0044 +#define MSPH_TREE_TRAIT 0x0045 +#define MSPH_TREE_CONJ 0x0046 +#define MSPH_TREE_DISJ 0x0047 +#define MSPH_TREE_IMPL 0x0048 +#define MSPH_TREE_ARROW 0x0049 +#define MSPH_TREE_BOX 0x004a +#define MSPH_TREE_FORALL 0x004b +#define MSPH_TREE_PAREN 0x004c + +#define MSPH_TREE_IDENT 0x0100 + + +struct msph_tree { + struct msph_tree *parent; + int type; +}; + +struct msph_tree_root; +struct msph_tree_body; +struct msph_tree_dir; +struct msph_tree_tpdef; +struct msph_tree_nomindecl; +struct msph_tree_assert; +struct msph_tree_ident; +struct msph_tree_tpexpr; + +struct msph_tree_root { + struct msph_tree tr; + + struct msph_ctx *ctx; + struct msph_tree_body *body; +}; + +struct msph_tree_body { + struct msph_tree tr; + + STAILQ_HEAD(msph_tree_dir_l, msph_tree_dir) head; +}; + +struct msph_tree_dir { + struct msph_tree tr; + + STAILQ_ENTRY(msph_tree_dir) entries; +}; + +struct msph_tree_tpdef { + struct msph_tree_dir dir; + + struct msph_tree_ident *id; + struct msph_tree_tpexpr *tp; +}; + +struct msph_tree_nomindecl { + struct msph_tree_dir dir; + + struct msph_tree_ident *id; +}; + +struct msph_tree_membdecl { + struct msph_tree_dir dir; + + struct msph_tree_ident *id; + struct msph_tree_tpexpr *tp; +}; + +struct msph_tree_assert { + struct msph_tree_dir dir; + + struct msph_tree_tpexpr *ltp; + struct msph_tree_tpexpr *rtp; +}; + +struct msph_tree_tpexpr { + struct msph_tree tr; + + STAILQ_ENTRY(msph_tree_tpexpr) entries; +}; + + +struct msph_tree_true { + struct msph_tree_tpexpr tp; +}; + +struct msph_tree_false { + struct msph_tree_tpexpr tp; +}; + +struct msph_tree_name { + struct msph_tree_tpexpr tp; + + struct msph_tree_ident *id; +}; + +struct msph_tree_appl { + struct msph_tree_tpexpr tp; + + struct msph_tree_ident *id; + STAILQ_HEAD(msph_tree_tpexpr_l, msph_tree_tpexpr) head; +}; + +struct msph_tree_trait { + struct msph_tree_tpexpr tp; + + struct msph_tree_body *body; +}; + +struct msph_tree_conj { + struct msph_tree_tpexpr tp; + + struct msph_tree_tpexpr *ltp; + struct msph_tree_tpexpr *rtp; +}; + +struct msph_tree_disj { + struct msph_tree_tpexpr tp; + + struct msph_tree_tpexpr *ltp; + struct msph_tree_tpexpr *rtp; +}; + +struct msph_tree_impl { + struct msph_tree_tpexpr tp; + + struct msph_tree_tpexpr *ltp; + struct msph_tree_tpexpr *rtp; +}; + +struct msph_tree_arrow { + struct msph_tree_tpexpr tp; + + struct msph_tree_tpexpr *ltp; + struct msph_tree_tpexpr *rtp; +}; + +struct msph_tree_box { + struct msph_tree_tpexpr tp; + + struct msph_tree_tpexpr *inner; +}; + +struct msph_tree_forall { + struct msph_tree_tpexpr tp; + + struct msph_tree_ident *ident; + struct msph_tree_tpexpr *inner; +}; + +struct msph_tree_paren { + struct msph_tree_tpexpr tp; + + struct msph_tree_tpexpr *inner; +}; + +struct msph_tree_ident { + struct msph_tree tr; + + char str[MSPH_IDENT_LEN]; + STAILQ_ENTRY(msph_tree_ident) entries; +}; + + + +struct msph_tree_root *msph_tree_makeroot(struct msph_ctx *); + +int msph_tree_parse(struct msph_token_stream *, struct msph_tree_root *); + +#endif diff --git a/include/spho/err.h b/include/spho/err.h index 0dd651d..b03411f 100644 --- a/include/spho/err.h +++ b/include/spho/err.h @@ -18,17 +18,23 @@ #define SPHO_ERR_BUF_LEN 2048 - +#define SPHO_ERR(ctx, e) \ + do { \ + (ctx)->err = (e); \ + if ((e) == SPHO_ERR_SYS) \ + SPHO_ERR_INFO(ctx, e, errno); \ + else \ + SPHO_ERR_INFO(ctx, e, 0); \ + } while (0) #ifdef SPHO_DEBUG #define SPHO_ERR_FILEBUF_LEN 128 -#define SPHO_ERR(ctx, e) \ +#define SPHO_ERR_INFO(ctx, e, info) \ do { \ (ctx)->err = (e); \ - if ((e) == SPHO_ERR_SYS) \ - (ctx)->err_info = errno; \ + (ctx)->err_info = (info); \ snprintf((ctx)->filebuf, sizeof((ctx)->filebuf), \ __FILE__); \ (ctx)->errline = __LINE__; \ @@ -85,18 +91,17 @@ #else /* SPHO_DEBUG */ -#define SPHO_ERR(ctx, e) \ +#define SPHO_ERR_INFO(ctx, e, info) \ do { \ (ctx)->err = (e); \ - if ((e) == SPHO_ERR_SYS) \ - (ctx)->err_info = errno; \ + (ctx)->err_info = (info); \ } while (0) #define SPHO_PRECOND(cond) #define SPHO_ASSERT(cond) #define SPHO_POSTCOND(cond) -#define SPHO_DBG_PRINT(fmt, ...) +#define SPHO_DEBUG_PRINT(fmt, ...) #endif /* SPHO_DEBUG */ diff --git a/include/spho/tp.h b/include/spho/tp.h index 19a7ffb..fdbf8bf 100644 --- a/include/spho/tp.h +++ b/include/spho/tp.h @@ -86,7 +86,7 @@ union tp_data { struct tp_bappl_data bappl; struct tp_konst_data konst; struct tp_var_data var; - struct tp_nominal_data nom; + struct tp_nominal_data nom; // XXX struct tp_record_data rec; }; @@ -126,6 +126,7 @@ struct spho_tp { STAILQ_HEAD(spho_tp_l, spho_tp); + #define SPHO_TP_ERR(tp, err) SPHO_ERR((tp)->sc->ctx, (err)) struct spho_var *spho_var_create(struct spho_scope *, char *, size_t); diff --git a/include/spho/util.h b/include/spho/util.h index 2871761..2cb9681 100644 --- a/include/spho/util.h +++ b/include/spho/util.h @@ -13,6 +13,13 @@ do { \ } \ } while (0) +#ifdef SPHO_USE_STRLCPY +#define SPHO_STRLCPY(dst, src, len) strlcpy(dst, src, len) +#else +#define SPHO_STRLCPY(dst, src, len) \ + (size_t)snprintf(dst, len, "%s", src) +#endif + #endif diff --git a/src/msph/README.md b/src/msph/README.md index 3c87d87..19b3857 100644 --- a/src/msph/README.md +++ b/src/msph/README.md @@ -21,7 +21,7 @@ Body ::= Dirs Dir ::= Typedef (directives, with lack of a better name) | Memberdef | Nominaldecl - | Checkdir + | Assert Typedef ::= 'type' Name '=' TExpr (type definition/binding) | 'type' Name '[' Names ']' '=' TExpr @@ -31,13 +31,14 @@ Memberdef ::= 'member' Name ':' TExpr Nominaldecl ::= 'nominal' Name -Checkdir ::= 'check' TExpr '<:' TExpr +Assert ::= 'assert' TExpr '<:' TExpr TExpr ::= 'True' | 'False' | Var | Nominal | Trait + | Appl | TExpr '&' TExpr | TExpr '|' TExpr | TExpr '=>' TExpr @@ -50,13 +51,14 @@ Trait ::= '{' Body '}' (trait, this introduces scoping) Var ::= Name (type variables) Nominal ::= Name (nominal type) +Appl ::= Name '[' TExprs ']' Name ::= '[a-zA-Z0-9_]+' & !Reserved (name/identifier) Reserved ::= 'type' (reserved/keywords) | 'member' | 'nominal' - | 'check' + | 'assert' | 'forall' | 'box' | 'True' @@ -93,4 +95,11 @@ member example_global : Example & ExampleN type TripleConj[X, Y, Z] = X & Y & Z +assert Example <: ExampleN + ``` + +// A <: B => ... +// == +// box (A => B) => ... + diff --git a/src/msph/msph.c b/src/msph/msph.c index b85945c..4d540ab 100644 --- a/src/msph/msph.c +++ b/src/msph/msph.c @@ -7,25 +7,16 @@ #define PRINTERR(ctx) \ do { \ - fprintf(stderr, "msph_err: %d (%d)\n", (ctx).err, (ctx).err_info); \ + fprintf(stderr, "msph_err: %x (%d)\n", (ctx).err, \ + (ctx).err_info); \ } while (0) -#ifdef SPHO_DEBUG -#define DEBUGFLAG "d" -#endif - struct msph_opts { int tokenize_only; -#ifdef DEBUGFLAG - int debug; -#endif const char *in_path; const char *out_path; } run_opts = { 0, -#ifdef DEBUGFLAG - 0, -#endif NULL, NULL }; @@ -52,7 +43,7 @@ main(int argc, char *argv[]) { int opt; - while ((opt = getopt(argc, argv, DEBUGFLAG "to:")) != -1) { + while ((opt = getopt(argc, argv, "to:")) != -1) { switch (opt) { case 't': run_opts.tokenize_only = 1; @@ -60,11 +51,6 @@ main(int argc, char *argv[]) case 'o': run_opts.out_path = optarg; break; -#ifdef DEBUGFLAG - case 'd': - run_opts.debug = 1; - break; -#endif case '?': default: print_usage(); @@ -118,7 +104,7 @@ run(struct msph_opts *opts) } } - if ((s = msph_token_stream_file(&ctx, in, opts->in_path)) == NULL) { + if ((s = msph_token_stream_file(&ctx, in)) == NULL) { goto err; } diff --git a/src/msph/token.c b/src/msph/token.c index 299e828..0588b7d 100644 --- a/src/msph/token.c +++ b/src/msph/token.c @@ -16,7 +16,7 @@ struct msph_matcher { const int type; }; -struct msph_matcher token_matcher[] = { +struct msph_matcher token_matchers[] = { { 0, 0, -1 }, { 0, 0, TOK_LBRACE }, { 0, 0, TOK_RBRACE }, @@ -26,6 +26,8 @@ struct msph_matcher token_matcher[] = { { 0, 0, TOK_RPAREN }, { 0, 0, TOK_COLON }, { 0, 0, TOK_EQUALS }, + { 0, 0, TOK_COMMA }, + { 0, 0, TOK_DOT }, { 0, 0, TOK_AMP }, { 0, 0, TOK_PIPE }, @@ -36,7 +38,7 @@ struct msph_matcher token_matcher[] = { { 0, 0, TOK_KW_TYPE }, { 0, 0, TOK_KW_NOMINAL }, { 0, 0, TOK_KW_MEMBER }, - { 0, 0, TOK_KW_CHECK }, + { 0, 0, TOK_KW_ASSERT }, { 0, 0, TOK_KW_BOX }, { 0, 0, TOK_KW_FORALL }, @@ -62,6 +64,8 @@ struct msph_token_info { TOK_INFO(TOK_RPAREN, ")"), TOK_INFO(TOK_COLON, ":"), TOK_INFO(TOK_EQUALS, "="), + TOK_INFO(TOK_COMMA, ","), + TOK_INFO(TOK_DOT, "."), TOK_INFO(TOK_AMP, "&"), TOK_INFO(TOK_PIPE, "|"), @@ -72,7 +76,7 @@ struct msph_token_info { TOK_INFO(TOK_KW_TYPE, "type"), TOK_INFO(TOK_KW_NOMINAL, "nominal"), TOK_INFO(TOK_KW_MEMBER, "member"), - TOK_INFO(TOK_KW_CHECK, "check"), + TOK_INFO(TOK_KW_ASSERT, "assert"), TOK_INFO(TOK_KW_BOX, "box"), TOK_INFO(TOK_KW_FORALL, "forall"), @@ -80,7 +84,6 @@ struct msph_token_info { TOK_INFO(TOK_CONST_FALSE, "False"), TOK_INFO(TOK_IDENT, NULL), - TOK_INFO(TOK_WSPACE, NULL), { TOK_END , NULL, NULL } #undef TOK_INFO }; @@ -113,12 +116,11 @@ void msph_ctx_init(struct msph_ctx *ctx) } struct msph_token_stream * -msph_token_stream_file(struct msph_ctx *ctx, FILE *f, const char *name) +msph_token_stream_file(struct msph_ctx *ctx, FILE *f) { - size_t res; struct msph_token_stream *ret; - if (ctx == NULL || f == NULL || name == NULL) { + if (ctx == NULL || f == NULL) { MSPH_ERR(ctx, MSPH_ERR_INVAL); return (NULL); } @@ -135,13 +137,6 @@ msph_token_stream_file(struct msph_ctx *ctx, FILE *f, const char *name) ret->src.inner.file.pos = 0; ret->src.inner.file.end = 0; - res = strlcpy(ret->src.inner.file.name, name, - sizeof(ret->src.inner.file.name)); - if (res >= sizeof(ret->src.inner.file.name)) { - MSPH_ERR(ctx, MSPH_ERR_TOOLONG); - goto err; - } - return (ret); err: if (fclose(f) == EOF) @@ -166,18 +161,24 @@ msph_token_stream_frombuf(struct msph_ctx *ctx, const char *buf, size_t len) ret->ctx = ctx; ret->src.type = MSPH_TOKEN_SRC_STR; ret->src.inner.str.s = buf; - ret->src.inner.str.len = len; + ret->src.inner.str.len = strnlen(buf, len); ret->src.inner.str.pos = 0; return (ret); } ssize_t -msph_token_str(char *buf, size_t len, struct msph_token *tok) +msph_token_str(char *buf, size_t len, + struct msph_token *tok) { ssize_t ret; + const char *base; - ret = (ssize_t)snprintf(buf, len, "%s", tok_base_str(tok)); + base = tok_base_str(tok); + if (base == NULL) { + return (-1); + } + ret = (ssize_t)snprintf(buf, len, "%s", base); if (ret < 0 || ret >= (ssize_t)len) return (ret); @@ -187,7 +188,7 @@ msph_token_str(char *buf, size_t len, struct msph_token *tok) switch (tok->type) { case TOK_IDENT: - ret += (ssize_t)snprintf(buf, len, "(%s)", tok->d.s.buf); + ret += (ssize_t)snprintf(buf, len, "(%s)", tok->data.str); break; default: break; @@ -196,7 +197,7 @@ msph_token_str(char *buf, size_t len, struct msph_token *tok) return (ret); } -#define MSPH_TOKEN_PRINT_BUF_LEN 2 * MSPH_TOKEN_BUF_LEN +#define MSPH_TOKEN_PRINT_BUF_LEN 2 * MSPH_IDENT_LEN int msph_token_stream_print(struct msph_token_stream *s, FILE *out) { @@ -204,10 +205,13 @@ msph_token_stream_print(struct msph_token_stream *s, FILE *out) struct msph_token tok; char tokstr[MSPH_TOKEN_PRINT_BUF_LEN]; - while ((ret = msph_token_stream_read_tok( &tok, 1, s)) > 0) { + while ((ret = msph_token_stream_read(&tok, 1, s)) > 0) { + ret = msph_token_str(tokstr, BUF_LEN(tokstr), &tok); - if (ret < 0) - continue; + if (ret < 0) { + MSPH_ERR_INFO(s->ctx, MSPH_ERR_TOKEN_INVAL, tok.type); + break; + } if ((size_t)ret < BUF_LEN(tokstr)) fprintf(out, "%s\n", tokstr); @@ -240,9 +244,9 @@ msph_token_stream_close(struct msph_token_stream *s) return (ret); } -/* -1 or num tokens read */ +/* -1 on error or num tokens read */ ssize_t -msph_token_stream_read_tok(struct msph_token *ptr, size_t n, +msph_token_stream_read(struct msph_token *ptr, size_t n, struct msph_token_stream *s) { size_t ret; @@ -280,27 +284,88 @@ read_single_tok(struct msph_token *ptr, struct msph_token_stream *s) return (-1); max_m = 0; - for (m = 1; token_matcher[m].type != TOK_END; m++) { - res = tok_match(ctx, src, &token_matcher[m]); + for (m = 1; token_matchers[m].type != TOK_END; m++) { + res = tok_match(ctx, src, &token_matchers[m]); if (res == -1) return (-1); - if (res == 0 && - token_matcher[m].matchlen > token_matcher[max_m].matchlen) { + if (res == 0 && token_matchers[m].matchlen > + token_matchers[max_m].matchlen) { max_m = m; } } - if (max_m == 0) - return (0); + if (max_m == 0) { + if (msph_token_stream_eof(s)) + return (0); + MSPH_ERR(s->ctx, MSPH_ERR_TOKEN_NOMATCH); + return (-1); + } - if (tok_commit(ctx, src, &token_matcher[max_m], ptr) == -1) + if (tok_commit(ctx, src, &token_matchers[max_m], ptr) == -1) return (-1); return (1); } +int +msph_token_stream_eof(struct msph_token_stream *s) +{ + struct msph_token_src_file *file; + struct msph_token_src_str *str; + + switch (s->src.type) { + case MSPH_TOKEN_SRC_FILE: + file = &s->src.inner.file; + return (file->pos == file->end && feof(file->f)); + case MSPH_TOKEN_SRC_STR: + str = &s->src.inner.str; + return (str->pos == str->len); + default: + MSPH_ERR(s->ctx, MSPH_ERR_INVAL); + return (-1); + } +} + +struct msph_token * +msph_token_create(struct msph_ctx *ctx, int type, union msph_token_data *data) +{ + size_t i; + struct msph_token *tok; + struct msph_token_info *info; + + info = NULL; + + for (i = 0; token_info[i].type != TOK_END; i++) { + if (token_info[i].type == type) { + info = &token_info[i]; + break; + } + } + + if (info == NULL) { + MSPH_ERR_INFO(ctx, MSPH_ERR_TOKEN_INVAL, type); + return (NULL); + } + + if ((tok = malloc(sizeof(*tok))) == NULL) { + MSPH_ERR(ctx, MSPH_ERR_SYS); + return (NULL); + } + + tok->type = type; + + switch (type) { + case TOK_IDENT: + memcpy(&tok->data, data, sizeof(*data)); + break; + default: + break; + } + + return (tok); +} static ssize_t src_file_fill_buf(struct msph_ctx *ctx, struct msph_token_src_file *file) @@ -316,7 +381,7 @@ src_file_fill_buf(struct msph_ctx *ctx, struct msph_token_src_file *file) maxread = BUF_LEN(file->buf) - file->end; if (maxread == 0) { - MSPH_ERR(ctx, MSPH_ERR_TOOLONG); + MSPH_ERR(ctx, MSPH_ERR_TOKEN_TOOLONG); return (-1); } @@ -516,8 +581,8 @@ tok_match(struct msph_ctx *ctx, struct msph_token_src *src, MATCH_STR("nominal"); case TOK_KW_MEMBER: MATCH_STR("member"); - case TOK_KW_CHECK: - MATCH_STR("check"); + case TOK_KW_ASSERT: + MATCH_STR("assert"); case TOK_KW_BOX: MATCH_STR("box"); case TOK_KW_FORALL: @@ -574,8 +639,8 @@ tok_commit(struct msph_ctx *ctx, struct msph_token_src *src, file->pos += m->matchlen; file->pos %= BUF_LEN(file->buf); - SPHO_ASSERT(file->pos < BUF_LEN(file->buf) || - file->pos < pos_old); + SPHO_ASSERT(file->pos <= file->end || + (file->pos < pos_old && file->pos < BUF_LEN(file->buf))); if (ptr == NULL) return (0); @@ -584,18 +649,18 @@ tok_commit(struct msph_ctx *ctx, struct msph_token_src *src, if (! TOK_HAS_DATA(ptr->type)) return (0); - if (m->matchlen >= sizeof(ptr->d.s.buf)) { - MSPH_ERR(ctx, MSPH_ERR_TOOLONG); + if (m->matchlen >= sizeof(ptr->data.str)) { + MSPH_ERR(ctx, MSPH_ERR_TOKEN_TOOLONG); return (-1); } - if (fromcbuf_charcpy(ptr->d.s.buf, file->buf, sizeof(file->buf), - pos_old, m->matchlen) == -1) { - MSPH_ERR(ctx, MSPH_ERR_TOOLONG); + if (fromcbuf_charcpy(ptr->data.str, file->buf, + sizeof(file->buf), pos_old, m->matchlen) == -1) { + MSPH_ERR(ctx, MSPH_ERR_TOKEN_TOOLONG); return (-1); } - ptr->d.s.buf[m->matchlen] = '\0'; + ptr->data.str[m->matchlen] = '\0'; return (0); case MSPH_TOKEN_SRC_STR: @@ -612,14 +677,14 @@ tok_commit(struct msph_ctx *ctx, struct msph_token_src *src, if (! TOK_HAS_DATA(ptr->type)) return (0); - if (m->matchlen >= sizeof(ptr->d.s.buf)) { - MSPH_ERR(ctx, MSPH_ERR_TOOLONG); + if (m->matchlen >= sizeof(ptr->data.str)) { + MSPH_ERR(ctx, MSPH_ERR_TOKEN_TOOLONG); return (-1); } - memcpy(ptr->d.s.buf, str->s, m->matchlen * + memcpy(ptr->data.str, str->s, m->matchlen * sizeof(str->s[0])); - ptr->d.s.buf[m->matchlen] = '\0'; + ptr->data.str[m->matchlen] = '\0'; return (0); default: diff --git a/src/msph/tree.c b/src/msph/tree.c new file mode 100644 index 0000000..ec90d36 --- /dev/null +++ b/src/msph/tree.c @@ -0,0 +1,761 @@ + +#include + +#include +#include + +#define SPHO_ENABLE_DEBUG_PRINT + +#include "spho/util.h" + +#include "msph/tree.h" + +struct tree_parse { + struct msph_token_stream *s; + + struct msph_token curr; + + SLIST_HEAD(msph_token_l, msph_token) head; +}; + +#define CURR_TOKEN(parse) (&parse->curr) + +#define T(ptr) ((struct msph_tree *)ptr) +#define CTX(parse) ((parse)->s->ctx) + +static void tree_parse_init(struct tree_parse *, + struct msph_token_stream *); +static int tree_parse_next_token(struct tree_parse *); +static void tree_parse_push_token(struct tree_parse *, struct msph_token *); + + +static void free_the_tree(struct msph_tree *); + +static struct msph_tree_body *tree_parse_body(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_ident *tree_parse_ident(struct tree_parse *, + struct msph_tree *); + +static struct msph_tree_dir *tree_parse_tpdef(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_dir *tree_parse_assert(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_dir *tree_parse_nomindecl( + struct tree_parse *, + struct msph_tree *); +static struct msph_tree_dir *tree_parse_membdecl( + struct tree_parse *, + struct msph_tree *); + +static struct msph_tree_tpexpr *tree_parse_tpexpr(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_true(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_false(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_name(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_applargs(struct tree_parse *, + struct msph_tree_ident*, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_trait(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_conj(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_disj(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_impl(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_arrow(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_box(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_forall(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_paren(struct tree_parse *, + struct msph_tree *); + +struct msph_tree_root * +msph_tree_makeroot(struct msph_ctx *ctx) +{ + struct msph_tree_root *root; + + if ((root = malloc(sizeof(*root))) == NULL) { + MSPH_ERR(ctx, MSPH_ERR_SYS); + return (NULL); + } + + + T(root)->parent = NULL; + T(root)->type = MSPH_TREE_ROOT; + + root->body = NULL; + + return (root); +} + + +/* + * Expect to read next token, otherwise set error and do something + * readres: (int) result of read + * parse: struct tree_parse * to perform read + * err_info: value passed to MSPH_ERR_INFO + * on_err: statement to perform on error + */ +#define EXPECT_READ_NEXT(readres, parse, err_info, on_err) \ + do { \ + if (((readres) = tree_parse_next_token(parse)) == -1) \ + on_err; \ + if ((readres) == 0) { \ + MSPH_ERR_INFO(CTX(parse), MSPH_ERR_TREE_EOF, \ + err_info); \ + on_err; \ + } \ + } while (0) + +/* + * Expect current token type, otherwise set error and do something + * parse: struct tree_parse * to perform read + * toktype: token type expected + * err_info: value passed to MSPH_ERR_INFO + * on_err: statement to perform on error + */ +#define EXPECT_CURR_TOKEN(parse, toktype, err_info, on_err) \ + do { \ + if (CURR_TOKEN(parse)->type != toktype) { \ + MSPH_ERR_INFO(CTX(parse), MSPH_ERR_TREE_NOMATCH, \ + err_info); \ + on_err; \ + } \ + } while (0) + +int +msph_tree_parse(struct msph_token_stream *s, struct msph_tree_root *root) +{ + int res; + struct tree_parse p; + struct msph_tree_body *body; + + if (root->body != NULL || T(root)->type != MSPH_TREE_ROOT) { + MSPH_ERR(s->ctx, MSPH_ERR_INVAL); + return (-1); + } + + tree_parse_init(&p, s); + EXPECT_READ_NEXT(res, &p, MSPH_TREE_ROOT, return (-1)); + + if ((body = tree_parse_body(&p, T(root))) == NULL) + return (-1); + + root->body = body; + + return (0); +} + + +static void +tree_parse_init(struct tree_parse *p, struct msph_token_stream *s) +{ + p->s = s; + + memset(&p->curr, 0, sizeof(p->curr)); + + SLIST_INIT(&p->head); +} + +static int +tree_parse_next_token(struct tree_parse *p) +{ + int ret; + struct msph_token *tok; + if (! SLIST_EMPTY(&p->head)) { + tok = SLIST_FIRST(&p->head); + SLIST_REMOVE_HEAD(&p->head, entries); + memcpy(&p->curr, tok, sizeof(p->curr)); + free(tok); + ret = 1; + } else { + ret = (int)msph_token_stream_read(&p->curr, 1, p->s); + } +#ifdef SPHO_ENABLE_DEBUG_PRINT + if (ret == 1) { + char buf[256]; + msph_token_str(buf, sizeof(buf), CURR_TOKEN(p)); + SPHO_DEBUG_PRINT("tree_parse_read_token: curr=%s\n", + buf); + } +#endif + return (ret); +} + +static struct msph_tree_body * +tree_parse_body(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_dir *dir; + struct msph_tree_body *body; + struct msph_token *tok; + + if ((body = malloc(sizeof(*body))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(body)->type = MSPH_TREE_BODY; + T(body)->parent = parent; + STAILQ_INIT(&body->head); + + while ((res = tree_parse_next_token(p)) > 0) { + dir = NULL; + switch(CURR_TOKEN(p)->type) { + case TOK_KW_TYPE: + dir = tree_parse_tpdef(p, T(body)); + break; + case TOK_KW_NOMINAL: + dir = tree_parse_nomindecl(p, T(body)); + break; + case TOK_KW_MEMBER: + dir = tree_parse_membdecl(p, T(body)); + break; + case TOK_KW_ASSERT: + dir = tree_parse_assert(p, T(body)); + break; + case TOK_RBRACE: + if ((tok = msph_token_create(CTX(p), TOK_RBRACE, NULL)) + == NULL) + goto err; + tree_parse_push_token(p, tok); + goto ret; + default: + MSPH_ERR_INFO(CTX(p), MSPH_ERR_TREE_NOMATCH, + MSPH_TREE_BODY); + goto err; + } + + if (dir == NULL) + goto err; + } + + if (res == -1) + goto err; +ret: + return (body); +err: + free_the_tree(T(body)); + + return (NULL); +} + +void +tree_parse_push_token(struct tree_parse *p, struct msph_token *tok) +{ + SLIST_INSERT_HEAD(&p->head, tok, entries); + CURR_TOKEN(p)->type = TOK_INVAL; +} + + +struct msph_tree_dir * +tree_parse_tpdef(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_tpdef *def; + + EXPECT_CURR_TOKEN(p, TOK_KW_TYPE, MSPH_TREE_TPDEF, return (NULL)); + + if ((def = malloc(sizeof(*def))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(def)->type = MSPH_TREE_TPDEF; + T(def)->parent = parent; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err); + if ((def->id = tree_parse_ident(p, T(def))) == NULL) + goto err; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err); + EXPECT_CURR_TOKEN(p, TOK_EQUALS, MSPH_TREE_TPDEF, goto err); + + EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err); + if ((def->tp = tree_parse_tpexpr(p, T(def))) == NULL) + goto err; + + return ((struct msph_tree_dir *)def); +err: + free_the_tree(T(def)); + return (NULL); +} + +struct msph_tree_ident * +tree_parse_ident(struct tree_parse *p, struct msph_tree *parent) +{ + struct msph_tree_ident *id; + + EXPECT_CURR_TOKEN(p, TOK_IDENT, MSPH_TREE_IDENT, return (NULL)); + + if ((id = malloc(sizeof(*id))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(id)->type = MSPH_TREE_IDENT; + T(id)->parent = parent; + + if (SPHO_STRLCPY(id->str, CURR_TOKEN(p)->data.str, sizeof(id->str)) + >= sizeof(id->str)) { + MSPH_ERR(CTX(p), MSPH_ERR_TREE_TOOLONG); + goto err; + } + + return (id); +err: + free_the_tree(T(id)); + return (NULL); +} + +struct msph_tree_tpexpr * +tree_parse_tpexpr(struct tree_parse *p, struct msph_tree *parent) +{ + struct msph_tree_tpexpr *tp; + + switch (CURR_TOKEN(p)->type) { + case TOK_AMP: + tp = tree_parse_conj(p, parent); + break; + case TOK_PIPE: + tp = tree_parse_disj(p, parent); + break; + case TOK_IMPL: + tp = tree_parse_impl(p, parent); + break; + case TOK_RARROW: + tp = tree_parse_arrow(p, parent); + break; + case TOK_KW_BOX: + tp = tree_parse_box(p, parent); + break; + case TOK_KW_FORALL: + tp = tree_parse_forall(p, parent); + break; + case TOK_IDENT: + tp = tree_parse_name(p, parent); + break; + case TOK_CONST_TRUE: + tp = tree_parse_true(p, parent); + break; + case TOK_CONST_FALSE: + tp = tree_parse_false(p, parent); + break; + case TOK_LPAREN: + tp = tree_parse_paren(p, parent); + break; + case TOK_LBRACE: + tp = tree_parse_trait(p, parent); + break; + default: + MSPH_ERR_INFO(CTX(p), MSPH_ERR_TREE_NOMATCH, MSPH_TREE_TPEXPR); + tp = NULL; + } + + return (tp); +} + +struct msph_tree_tpexpr * +tree_parse_conj(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_conj *conj; + + EXPECT_CURR_TOKEN(p, TOK_AMP, MSPH_TREE_CONJ, return (NULL)); + + if ((conj = malloc(sizeof(*conj))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(conj)->type = MSPH_TREE_CONJ; + T(conj)->parent = parent; + conj->ltp = NULL; + conj->rtp = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_CONJ, goto err); + + if ((conj->ltp = tree_parse_tpexpr(p, (struct msph_tree *)conj)) + == NULL) + goto err; + + if ((conj->rtp = tree_parse_tpexpr(p, (struct msph_tree *)conj)) + == NULL) + goto err; +err: + free_the_tree((struct msph_tree *)conj); + + return (NULL); +} + +struct msph_tree_tpexpr * +tree_parse_disj(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_disj *disj; + + EXPECT_CURR_TOKEN(p, TOK_PIPE, MSPH_TREE_DISJ, return (NULL)); + + if ((disj = malloc(sizeof(*disj))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(disj)->type = MSPH_TREE_DISJ; + T(disj)->parent = parent; + disj->ltp = NULL; + disj->rtp = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_DISJ, goto err); + + if ((disj->ltp = tree_parse_tpexpr(p, (struct msph_tree *)disj)) + == NULL) + goto err; + + if ((disj->rtp = tree_parse_tpexpr(p, (struct msph_tree *)disj)) + == NULL) + goto err; +err: + free_the_tree((struct msph_tree *)disj); + + return (NULL); +} + +struct msph_tree_tpexpr * +tree_parse_impl(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_impl *impl; + + EXPECT_CURR_TOKEN(p, TOK_PIPE, MSPH_TREE_IMPL, return (NULL)); + + if ((impl = malloc(sizeof(*impl))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(impl)->type = MSPH_TREE_IMPL; + T(impl)->parent = parent; + impl->ltp = NULL; + impl->rtp = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_IMPL, goto err); + + if ((impl->ltp = tree_parse_tpexpr(p, (struct msph_tree *)impl)) + == NULL) + goto err; + + if ((impl->rtp = tree_parse_tpexpr(p, (struct msph_tree *)impl)) + == NULL) + goto err; +err: + free_the_tree((struct msph_tree *)impl); + + return (NULL); +} + +struct msph_tree_tpexpr * +tree_parse_arrow(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_arrow *arrw; + + EXPECT_CURR_TOKEN(p, TOK_PIPE, MSPH_TREE_ARROW, return (NULL)); + + if ((arrw = malloc(sizeof(*arrw))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(arrw)->type = MSPH_TREE_ARROW; + T(arrw)->parent = parent; + arrw->ltp = NULL; + arrw->rtp = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_ARROW, goto err); + + if ((arrw->ltp = tree_parse_tpexpr(p, (struct msph_tree *)arrw)) + == NULL) + goto err; + + if ((arrw->rtp = tree_parse_tpexpr(p, (struct msph_tree *)arrw)) + == NULL) + goto err; +err: + free_the_tree((struct msph_tree *)arrw); + + return (NULL); +} + +struct msph_tree_tpexpr * +tree_parse_box(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_box *box; + + EXPECT_CURR_TOKEN(p, TOK_KW_BOX, MSPH_TREE_BOX, return (NULL)); + + if ((box = malloc(sizeof(*box))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(box)->type = MSPH_TREE_BOX; + T(box)->parent = parent; + box->inner = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_BOX, goto err); + if ((box->inner = tree_parse_tpexpr(p, T(box))) == NULL) + goto err; + + return ((struct msph_tree_tpexpr *)box); +err: + free_the_tree(T(box)); + return (NULL); +} + +struct msph_tree_tpexpr * +tree_parse_forall(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_forall *fa; + + EXPECT_CURR_TOKEN(p, TOK_KW_FORALL, MSPH_TREE_FORALL, return (NULL)); + + if ((fa = malloc(sizeof(*fa))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(fa)->type = MSPH_TREE_FORALL; + T(fa)->parent = parent; + fa->ident = NULL; + fa->inner = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_FORALL, goto err); + if ((fa->ident = tree_parse_ident(p, T(fa))) == NULL) + goto err; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_FORALL, goto err); + EXPECT_CURR_TOKEN(p, TOK_COLON, MSPH_TREE_FORALL, goto err); + + EXPECT_READ_NEXT(res, p, MSPH_TREE_FORALL, goto err); + if ((fa->inner = tree_parse_tpexpr(p, T(fa))) == NULL) + goto err; + + return ((struct msph_tree_tpexpr *)fa); +err: + free_the_tree(T(fa)); + return (NULL); +} + +struct msph_tree_tpexpr * +tree_parse_name(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_ident *id; + struct msph_tree_name *name; + struct msph_tree_tpexpr *ret; + + ret = NULL; + name = NULL; + + if ((id = tree_parse_ident(p, NULL)) == NULL) + return (NULL); + + if ((res = tree_parse_next_token(p)) == 1 && + CURR_TOKEN(p)->type == TOK_LBRAK) { + if ((ret = tree_parse_applargs(p, id, parent)) == NULL) + goto err; + return (ret); + } else if (res == -1) { + goto err; + } + + if ((name = malloc(sizeof(*name))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + goto err; + } + T(name)->type = MSPH_TREE_NAME; + T(name)->parent = parent; + + name->id = id; + + return ((struct msph_tree_tpexpr *)name); +err: + free_the_tree(T(id)); + + return (NULL); +} + +/** + * Parse argument list part [...], of type application A[...]. + * + * @param p Parse state + * @param id Parsed ident A (on failure, this is not freed) + * @param parent Parent of resulting appl node + * + * @return tpexpr node representing A[...]. + */ +struct msph_tree_tpexpr * +tree_parse_applargs(struct tree_parse *p, struct msph_tree_ident *id, + struct msph_tree *parent) +{ + int res; + struct msph_tree_appl *appl; + struct msph_tree_tpexpr *tp; + + tp = NULL; + + EXPECT_CURR_TOKEN(p, TOK_LBRAK, MSPH_TREE_APPL, return (NULL)); + + if ((appl = malloc(sizeof(*appl))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(appl)->type = MSPH_TREE_APPL; + T(appl)->parent = parent; + appl->id = NULL; + STAILQ_INIT(&appl->head); + + /* parse the argument list */ + while ((res = tree_parse_next_token(p)) == 1) { + /* if ']' we have reached end of arguments */ + if (CURR_TOKEN(p)->type == TOK_RBRAK) + break; + + /* if not start of argument list, check for comma and step + * tokenizer */ + if (tp != NULL) { + EXPECT_CURR_TOKEN(p, TOK_COMMA, MSPH_TREE_APPL, + goto err); + EXPECT_READ_NEXT(res, p, MSPH_TREE_APPL, goto err); + } + + if ((tp = tree_parse_tpexpr(p, T(appl))) == NULL) + goto err; + + STAILQ_INSERT_TAIL(&appl->head, tp, entries); + } + + /* system error */ + if (res == -1) + goto err; + + /* did not read final ']' because of EOF */ + if (res == 0) { + MSPH_ERR_INFO(CTX(p), MSPH_ERR_TREE_EOF, MSPH_TREE_APPL); + goto err; + } + + /* finally, appl takes ownership of id */ + appl->id = id; + + return ((struct msph_tree_tpexpr *)appl); +err: + free_the_tree(T(appl)); + + return (NULL); +} + +struct msph_tree_tpexpr * +tree_parse_true(struct tree_parse *p, struct msph_tree *parent) +{ + struct msph_tree_true *t; + + EXPECT_CURR_TOKEN(p, TOK_CONST_TRUE, MSPH_TREE_TRUE, return (NULL)); + + if ((t = malloc(sizeof(*t))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(t)->type = MSPH_TREE_TRUE; + T(t)->parent = parent; + + return ((struct msph_tree_tpexpr *)t); +} + +struct msph_tree_tpexpr * +tree_parse_false(struct tree_parse *p, struct msph_tree *parent) +{ + struct msph_tree_true *f; + + EXPECT_CURR_TOKEN(p, TOK_CONST_FALSE, MSPH_TREE_FALSE, return (NULL)); + + if ((f = malloc(sizeof(*f))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(f)->type = MSPH_TREE_FALSE; + T(f)->parent = parent; + + return ((struct msph_tree_tpexpr *)f); +} + +struct msph_tree_tpexpr * +tree_parse_paren(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_paren *par; + + EXPECT_CURR_TOKEN(p, TOK_LPAREN, MSPH_TREE_FALSE, return (NULL)); + + if ((par = malloc(sizeof(*par))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(par)->type = MSPH_TREE_PAREN; + T(par)->parent = parent; + par->inner = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_PAREN, goto err); + + if ((par->inner = tree_parse_tpexpr(p, T(par))) == NULL) + goto err; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_PAREN, goto err); + EXPECT_CURR_TOKEN(p, TOK_RPAREN, MSPH_TREE_PAREN, goto err); + + return ((struct msph_tree_tpexpr *)par); +err: + free_the_tree(T(par)); + + return (NULL); +} + +struct msph_tree_tpexpr * +tree_parse_trait(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_trait *trait; + + EXPECT_CURR_TOKEN(p, TOK_LBRACE, MSPH_TREE_TRAIT, return (NULL)); + + if ((trait = malloc(sizeof(*trait))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(trait)->type = MSPH_TREE_TRAIT; + T(trait)->parent = parent; + trait->body = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_TRAIT, goto err); + + if ((trait->body = tree_parse_body(p, T(trait))) == NULL) + goto err; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_TRAIT, goto err); + EXPECT_CURR_TOKEN(p, TOK_RBRACE, MSPH_TREE_TRAIT, goto err); + + return ((struct msph_tree_tpexpr *)trait); +err: + free_the_tree(T(trait)); + + return (NULL); +} + +static void +free_the_tree(struct msph_tree *tree) +{ + /* no one can free the tree :´( */ + SPHO_POSTCOND((void *)tree == (void *)free); +} + + From 7e5f08028287063bca67aa21cadf39e13d2dc14d Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Sun, 20 Apr 2025 11:24:43 +0300 Subject: [PATCH 09/10] final directives parsing --- src/msph/tree.c | 105 +++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 103 insertions(+), 2 deletions(-) diff --git a/src/msph/tree.c b/src/msph/tree.c index ec90d36..ca9a1de 100644 --- a/src/msph/tree.c +++ b/src/msph/tree.c @@ -534,7 +534,7 @@ tree_parse_forall(struct tree_parse *p, struct msph_tree *parent) goto err; EXPECT_READ_NEXT(res, p, MSPH_TREE_FORALL, goto err); - EXPECT_CURR_TOKEN(p, TOK_COLON, MSPH_TREE_FORALL, goto err); + EXPECT_CURR_TOKEN(p, TOK_DOT, MSPH_TREE_FORALL, goto err); EXPECT_READ_NEXT(res, p, MSPH_TREE_FORALL, goto err); if ((fa->inner = tree_parse_tpexpr(p, T(fa))) == NULL) @@ -751,6 +751,108 @@ err: return (NULL); } +struct msph_tree_dir * +tree_parse_nomindecl(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_nomindecl *nomd; + + EXPECT_CURR_TOKEN(p, TOK_KW_NOMINAL, MSPH_TREE_NOMINDECL, + return (NULL)); + EXPECT_READ_NEXT(res, p, MSPH_TREE_NOMINDECL, return (NULL)); + + if ((nomd = malloc(sizeof(*nomd))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(nomd)->type = MSPH_TREE_NOMINDECL; + T(nomd)->parent = parent; + nomd->id = NULL; + + if ((nomd->id = tree_parse_ident(p, T(nomd))) == NULL) + goto err; + + return ((struct msph_tree_dir *)nomd); +err: + free_the_tree(T(nomd)); + + return (NULL); +} + +struct msph_tree_dir * +tree_parse_membdecl(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_membdecl *membd; + + EXPECT_CURR_TOKEN(p, TOK_KW_MEMBER, MSPH_TREE_MEMBDECL, + return (NULL)); + EXPECT_READ_NEXT(res, p, MSPH_TREE_MEMBDECL, return (NULL)); + + if ((membd = malloc(sizeof(*membd))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(membd)->type = MSPH_TREE_NOMINDECL; + T(membd)->parent = parent; + membd->id = NULL; + membd->tp = NULL; + + if ((membd->id = tree_parse_ident(p, T(membd))) == NULL) + goto err; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_MEMBDECL, goto err); + EXPECT_CURR_TOKEN(p, TOK_COLON, MSPH_TREE_MEMBDECL, + goto err); + EXPECT_READ_NEXT(res, p, MSPH_TREE_MEMBDECL, goto err); + + if ((membd->tp = tree_parse_tpexpr(p, T(membd))) == NULL) + goto err; + + return ((struct msph_tree_dir *)membd); +err: + free_the_tree(T(membd)); + + return (NULL); +} + +struct msph_tree_dir * +tree_parse_assert(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_assert *ass; + + EXPECT_CURR_TOKEN(p, TOK_KW_ASSERT, MSPH_TREE_ASSERT, + return (NULL)); + EXPECT_READ_NEXT(res, p, MSPH_TREE_ASSERT, return (NULL)); + + if ((ass = malloc(sizeof(*ass))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(ass)->type = MSPH_TREE_ASSERT; + T(ass)->parent = parent; + ass->ltp = NULL; + ass->rtp = NULL; + + if ((ass->ltp = tree_parse_tpexpr(p, T(ass))) == NULL) + goto err; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_ASSERT, goto err); + EXPECT_CURR_TOKEN(p, TOK_SUB, MSPH_TREE_ASSERT, + goto err); + EXPECT_READ_NEXT(res, p, MSPH_TREE_ASSERT, goto err); + + if ((ass->ltp = tree_parse_tpexpr(p, T(ass))) == NULL) + goto err; + + return ((struct msph_tree_dir *)ass); +err: + free_the_tree(T(ass)); + + return (NULL); +} + static void free_the_tree(struct msph_tree *tree) { @@ -758,4 +860,3 @@ free_the_tree(struct msph_tree *tree) SPHO_POSTCOND((void *)tree == (void *)free); } - From 17be15d7b5194467331ebb060a6d1ba4c35a8721 Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Tue, 22 Apr 2025 21:08:03 +0300 Subject: [PATCH 10/10] parsing prefix version (binary operators) of msph --- CMakeLists.txt | 3 + example/ex1.msph | 4 + example/ex2.msph | 1 + example/ex3.msph | 13 ++ include/msph/common.h | 7 + include/msph/err.h | 6 +- include/msph/token.h | 14 +- include/msph/tree.h | 22 +- include/spho/err.h | 1 - src/msph/msph.c | 28 ++- src/msph/token.c | 130 +++++++++--- src/msph/tree.c | 480 ++++++++++++++++++++++++++++++++++++++---- 12 files changed, 617 insertions(+), 92 deletions(-) create mode 100644 example/ex1.msph create mode 100644 example/ex2.msph create mode 100644 example/ex3.msph diff --git a/CMakeLists.txt b/CMakeLists.txt index b9c8a66..466a3d9 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -62,6 +62,9 @@ set(MSPH_SRC set(MSPH_HEADER ${INCLUDE_DIR}/msph/token.h + ${INCLUDE_DIR}/msph/tree.h + ${INCLUDE_DIR}/msph/common.h + ${INCLUDE_DIR}/msph/err.h ) add_executable(msph ${MSPH_SRC} ${MSPH_HEADER}) diff --git a/example/ex1.msph b/example/ex1.msph new file mode 100644 index 0000000..0844c3f --- /dev/null +++ b/example/ex1.msph @@ -0,0 +1,4 @@ + +nominal C + + diff --git a/example/ex2.msph b/example/ex2.msph new file mode 100644 index 0000000..5b85fdc --- /dev/null +++ b/example/ex2.msph @@ -0,0 +1 @@ +type A = & C D diff --git a/example/ex3.msph b/example/ex3.msph new file mode 100644 index 0000000..9770336 --- /dev/null +++ b/example/ex3.msph @@ -0,0 +1,13 @@ + +type X = & C (| D E) + +type Y = { + member x : X + type Z = & X { + type T = C + assert C <: D + } + member r : (box forall S. (=> S Y)) + member s : C[X, Y, z] + member f : -> A B +} diff --git a/include/msph/common.h b/include/msph/common.h index 0a0bda2..43a6a6f 100644 --- a/include/msph/common.h +++ b/include/msph/common.h @@ -4,6 +4,7 @@ #include "msph/err.h" #define MSPH_IDENT_LEN 128 +#define MSPH_NAME_LEN 1024 struct msph_ctx { int err; @@ -15,4 +16,10 @@ struct msph_ctx { int errline; #endif }; + +struct msph_text_pos { + unsigned int line; + unsigned int col; +}; + #endif diff --git a/include/msph/err.h b/include/msph/err.h index 41a89d9..bf113d5 100644 --- a/include/msph/err.h +++ b/include/msph/err.h @@ -1,16 +1,12 @@ #ifndef _MSPH_ERR_H #define _MSPH_ERR_H -#ifdef SPHO_DEBUG -// #define SPHO_ENABLE_DEBUG_PRINT -#endif - #include "spho/err.h" #define MSPH_ERR_SYS 0x0001 - #define MSPH_ERR_INVAL 0x0002 +#define MSPH_ERR_TOOLONG 0x0003 #define MSPH_ERR_TOKEN_TOOLONG 0x1001 #define MSPH_ERR_TOKEN_EOF 0x1002 diff --git a/include/msph/token.h b/include/msph/token.h index a8896d3..b984039 100644 --- a/include/msph/token.h +++ b/include/msph/token.h @@ -69,15 +69,18 @@ enum msph_tok_type { TOK_IDENT, // identifiers TOK_INVAL, // special: invalid, use to mark invalid toks TOK_WSPACE, // special: whitespace - TOK_END // special: denote end of array + TOK_END // special: end of array/token stream }; +#define MSPH_TAB_WIDTH 8 + union msph_token_data { char str[MSPH_IDENT_LEN]; }; struct msph_token { int type; + struct msph_text_pos pos; union msph_token_data data; SLIST_ENTRY(msph_token) entries; @@ -110,21 +113,23 @@ union msph_token_src_data { struct msph_token_src { int type; + struct msph_text_pos pos; union msph_token_src_data inner; }; struct msph_token_stream { struct msph_ctx *ctx; + char name[MSPH_NAME_LEN]; struct msph_token_src src; }; void msph_ctx_init(struct msph_ctx *); struct msph_token_stream *msph_token_stream_file(struct msph_ctx *, - FILE *); + const char *, FILE *); struct msph_token_stream *msph_token_stream_frombuf(struct msph_ctx *, - const char *, size_t); + const char *, const char *, size_t); int msph_token_stream_close(struct msph_token_stream*); @@ -135,8 +140,7 @@ int msph_token_stream_print(struct msph_token_stream *, FILE *); ssize_t msph_token_str(char *, size_t, struct msph_token *); -struct msph_token * msph_token_create(struct msph_ctx *, int, - union msph_token_data *); +struct msph_token * msph_token_copy(struct msph_ctx *, struct msph_token *); #endif /* _MSPH_EXPR_H */ diff --git a/include/msph/tree.h b/include/msph/tree.h index 601c35f..22cc883 100644 --- a/include/msph/tree.h +++ b/include/msph/tree.h @@ -55,7 +55,8 @@ * Trait ({ ... }, creates scoping) */ -#define MSPH_TREE_ROOT 0x0001 +#define MSPH_TREE_ROOT 0x0000 +#define MSPH_TREE_UNIT 0x0001 #define MSPH_TREE_BODY 0x0010 @@ -83,11 +84,12 @@ struct msph_tree { - struct msph_tree *parent; int type; + struct msph_tree *parent; }; struct msph_tree_root; +struct msph_tree_text; struct msph_tree_body; struct msph_tree_dir; struct msph_tree_tpdef; @@ -100,7 +102,21 @@ struct msph_tree_root { struct msph_tree tr; struct msph_ctx *ctx; + + STAILQ_HEAD(msph_tree_unit_l, msph_tree_unit) head; +}; + +struct msph_tree_unit { + struct msph_tree tr; + + char name[MSPH_NAME_LEN]; struct msph_tree_body *body; + STAILQ_ENTRY(msph_tree_unit) entries; +}; + +struct msph_tree_text { + struct msph_tree tr; + struct msph_text_pos pos; }; struct msph_tree_body { @@ -236,4 +252,6 @@ struct msph_tree_root *msph_tree_makeroot(struct msph_ctx *); int msph_tree_parse(struct msph_token_stream *, struct msph_tree_root *); +ssize_t msph_tree_fprint(FILE *, struct msph_tree *); + #endif diff --git a/include/spho/err.h b/include/spho/err.h index b03411f..ffde4b0 100644 --- a/include/spho/err.h +++ b/include/spho/err.h @@ -100,7 +100,6 @@ #define SPHO_PRECOND(cond) #define SPHO_ASSERT(cond) #define SPHO_POSTCOND(cond) - #define SPHO_DEBUG_PRINT(fmt, ...) #endif /* SPHO_DEBUG */ diff --git a/src/msph/msph.c b/src/msph/msph.c index 4d540ab..edc2ed7 100644 --- a/src/msph/msph.c +++ b/src/msph/msph.c @@ -4,6 +4,7 @@ #include "msph/err.h" #include "msph/token.h" +#include "msph/tree.h" #define PRINTERR(ctx) \ do { \ @@ -43,7 +44,7 @@ main(int argc, char *argv[]) { int opt; - while ((opt = getopt(argc, argv, "to:")) != -1) { + while ((opt = getopt(argc, argv, "hto:")) != -1) { switch (opt) { case 't': run_opts.tokenize_only = 1; @@ -51,6 +52,9 @@ main(int argc, char *argv[]) case 'o': run_opts.out_path = optarg; break; + case 'h': + print_usage(); + exit(EXIT_SUCCESS); case '?': default: print_usage(); @@ -80,6 +84,7 @@ run(struct msph_opts *opts) int ret; struct msph_ctx ctx; struct msph_token_stream *s; + struct msph_tree_root *root; FILE *in, *out; in = out = NULL; @@ -104,17 +109,30 @@ run(struct msph_opts *opts) } } - if ((s = msph_token_stream_file(&ctx, in)) == NULL) { + if ((s = msph_token_stream_file(&ctx, opts->in_path, in)) == NULL) { goto err; } printf("msph v0, parsing %s\n", opts->in_path); - if ((ret = msph_token_stream_print(s, out)) == -1) + if (opts->tokenize_only) { + if ((ret = msph_token_stream_print(s, out)) == -1) + goto err; + + goto exit; + } + + if ((root = msph_tree_makeroot(&ctx)) == NULL) { + goto err; + } + + if (msph_tree_parse(s, root) == -1) goto err; - if (opts->tokenize_only) - goto exit; + printf("msph tree successfully parsed :)\n"); + + if (msph_tree_fprint(out, (struct msph_tree *)root) < 0) + goto err; exit: if (msph_token_stream_close(s) == -1) diff --git a/src/msph/token.c b/src/msph/token.c index 0588b7d..01b5cd7 100644 --- a/src/msph/token.c +++ b/src/msph/token.c @@ -8,7 +8,6 @@ #include "msph/err.h" #include "msph/token.h" - struct msph_matcher { size_t off; size_t matchlen; @@ -98,6 +97,8 @@ static int tok_match(struct msph_ctx *, struct msph_token_src *, struct msph_matcher *); static int tok_commit(struct msph_ctx *, struct msph_token_src *, struct msph_matcher *, struct msph_token *); +static void tok_update_pos(struct msph_ctx *, struct msph_token_src *, + struct msph_matcher *m); static int char_at(struct msph_ctx *, struct msph_token_src *, size_t, char *); static int fromcbuf_charcpy(char *, const char *, size_t, size_t, size_t); @@ -116,8 +117,9 @@ void msph_ctx_init(struct msph_ctx *ctx) } struct msph_token_stream * -msph_token_stream_file(struct msph_ctx *ctx, FILE *f) +msph_token_stream_file(struct msph_ctx *ctx, const char *name, FILE *f) { + size_t res; struct msph_token_stream *ret; if (ctx == NULL || f == NULL) { @@ -132,7 +134,13 @@ msph_token_stream_file(struct msph_ctx *ctx, FILE *f) } ret->ctx = ctx; + if ((res = strlcpy(ret->name, name, BUF_LEN(ret->name))) + >= BUF_LEN(ret->name)) { + MSPH_ERR(ctx, MSPH_ERR_TOOLONG); + goto err; + } ret->src.type = MSPH_TOKEN_SRC_FILE; + ret->src.pos = (struct msph_text_pos) { .line = 1, .col = 1 }; ret->src.inner.file.f = f; ret->src.inner.file.pos = 0; ret->src.inner.file.end = 0; @@ -149,8 +157,10 @@ err: } struct msph_token_stream * -msph_token_stream_frombuf(struct msph_ctx *ctx, const char *buf, size_t len) +msph_token_stream_frombuf(struct msph_ctx *ctx, const char *name, + const char *buf, size_t len) { + size_t res; struct msph_token_stream *ret; if ((ret = calloc(1, sizeof(struct msph_token_stream))) == NULL) { @@ -159,12 +169,23 @@ msph_token_stream_frombuf(struct msph_ctx *ctx, const char *buf, size_t len) } ret->ctx = ctx; + if ((res = strlcpy(ret->name, name, BUF_LEN(ret->name))) + >= BUF_LEN(ret->name)) { + MSPH_ERR(ctx, MSPH_ERR_TOOLONG); + goto err; + } ret->src.type = MSPH_TOKEN_SRC_STR; + ret->src.pos = (struct msph_text_pos) { .line = 1, .col = 1 }; ret->src.inner.str.s = buf; ret->src.inner.str.len = strnlen(buf, len); ret->src.inner.str.pos = 0; return (ret); + +err: + free(ret); + + return (NULL); } ssize_t @@ -244,7 +265,9 @@ msph_token_stream_close(struct msph_token_stream *s) return (ret); } -/* -1 on error or num tokens read */ +/* read at most n tokens from s into p. + * return -1 on error, or num tokens read + */ ssize_t msph_token_stream_read(struct msph_token *ptr, size_t n, struct msph_token_stream *s) @@ -279,6 +302,7 @@ read_single_tok(struct msph_token *ptr, struct msph_token_stream *s) /* Skipping whitespace */ if (tok_match(ctx, src, &wspace) == -1) return (-1); + SPHO_DEBUG_PRINT("wspace.matchlen=%zu\n", wspace.matchlen); if (wspace.matchlen > 0 && tok_commit(ctx, src, &wspace, NULL) == -1) return (-1); @@ -329,42 +353,34 @@ msph_token_stream_eof(struct msph_token_stream *s) } struct msph_token * -msph_token_create(struct msph_ctx *ctx, int type, union msph_token_data *data) +msph_token_copy(struct msph_ctx *ctx, struct msph_token *token) { size_t i; - struct msph_token *tok; + struct msph_token *copy; struct msph_token_info *info; info = NULL; for (i = 0; token_info[i].type != TOK_END; i++) { - if (token_info[i].type == type) { + if (token_info[i].type == token->type) { info = &token_info[i]; break; } } if (info == NULL) { - MSPH_ERR_INFO(ctx, MSPH_ERR_TOKEN_INVAL, type); + MSPH_ERR_INFO(ctx, MSPH_ERR_TOKEN_INVAL, token->type); return (NULL); } - if ((tok = malloc(sizeof(*tok))) == NULL) { + if ((copy = malloc(sizeof(*copy))) == NULL) { MSPH_ERR(ctx, MSPH_ERR_SYS); return (NULL); } - tok->type = type; + memcpy(copy, token, sizeof(*copy)); - switch (type) { - case TOK_IDENT: - memcpy(&tok->data, data, sizeof(*data)); - break; - default: - break; - } - - return (tok); + return (copy); } static ssize_t @@ -404,8 +420,6 @@ src_file_fill_buf(struct msph_ctx *ctx, struct msph_token_src_file *file) } while (file->end != file->pos); - SPHO_DEBUG_PRINT("src_file_fill_buf: read %zd\n", ret); - return (ret); } @@ -414,20 +428,16 @@ static int file_char_at(struct msph_ctx *ctx, struct msph_token_src *src, size_t i, char *out) { - int ret; ssize_t fill; struct msph_token_src_file *file; SPHO_PRECOND(src != NULL); SPHO_PRECOND(src->type == MSPH_TOKEN_SRC_FILE); - ret = 0; file = &src->inner.file; fill = 0; do { - SPHO_DEBUG_PRINT("want to read %zu, valid range (%zu, %zu)\n", - (file->pos + i) % BUF_LEN(file->buf), file->pos, file->end); /* simplest case */ if (file->pos + i < file->end) { *out = file->buf[file->pos + i]; @@ -445,9 +455,9 @@ file_char_at(struct msph_ctx *ctx, struct msph_token_src *src, size_t i, if ((fill = src_file_fill_buf(ctx, file)) == -1) return (-1); - } while (fill > 0 && ret++); + } while (fill > 0); - return (ret); + return (0); } static int @@ -474,7 +484,34 @@ char_at(struct msph_ctx *ctx, struct msph_token_src *src, size_t i, char *out) break; } - SPHO_DEBUG_PRINT("char_at: ret=%d, *out=%c\n", ret, *out); +#ifdef SPHO_ENABLE_DEBUG_PRINT + if (isspace(*out)) { + const char *charrep; + switch (*out) { + case '\n': + charrep = "\\n"; + break; + case '\t': + charrep = "\\t"; + break; + case '\r': + charrep = "\\r"; + break; + case '\v': + charrep = "\\v"; + break; + case '\f': + charrep = "\\f"; + break; + default: + charrep = "WOOOOOOOOOOPS"; + break; + } + SPHO_DEBUG_PRINT("char_at: ret=%d, *out=%s\n", ret, charrep); + } else { + SPHO_DEBUG_PRINT("char_at: ret=%d, *out=%c\n", ret, *out); + } +#endif return (ret); } @@ -563,6 +600,10 @@ tok_match(struct msph_ctx *ctx, struct msph_token_src *src, MATCH_CHAR(')'); case TOK_COLON: MATCH_CHAR(':'); + case TOK_DOT: + MATCH_CHAR('.'); + case TOK_COMMA: + MATCH_CHAR(','); case TOK_EQUALS: MATCH_CHAR('='); case TOK_AMP: @@ -626,12 +667,16 @@ tok_commit(struct msph_ctx *ctx, struct msph_token_src *src, struct msph_matcher *m, struct msph_token *ptr) { size_t pos_old; + struct msph_text_pos tok_pos; struct msph_token_src_str *str; struct msph_token_src_file *file; SPHO_PRECOND(ctx != NULL && m != NULL); SPHO_PRECOND(m->matchlen != 0); + tok_pos = src->pos; + tok_update_pos(ctx, src, m); + switch (src->type) { case MSPH_TOKEN_SRC_FILE: file = &src->inner.file; @@ -646,6 +691,7 @@ tok_commit(struct msph_ctx *ctx, struct msph_token_src *src, return (0); ptr->type = m->type; + ptr->pos = tok_pos; if (! TOK_HAS_DATA(ptr->type)) return (0); @@ -674,6 +720,7 @@ tok_commit(struct msph_ctx *ctx, struct msph_token_src *src, return (0); ptr->type = m->type; + ptr->pos = tok_pos; if (! TOK_HAS_DATA(ptr->type)) return (0); @@ -692,7 +739,34 @@ tok_commit(struct msph_ctx *ctx, struct msph_token_src *src, } } +static void +tok_update_pos(struct msph_ctx *ctx, struct msph_token_src *src, + struct msph_matcher *m) +{ + int res; + char c; + size_t i; + for (i = 0; i < m->matchlen; i++) { + res = char_at(ctx, src, i, &c); + SPHO_ASSERT(res == 1); + + switch (c) { + case '\t': + src->pos.col += MSPH_TAB_WIDTH; + break; + case '\n': + src->pos.line++; + src->pos.col = 1; + break; + case '\r': + break; + default: + src->pos.col++; + break; + } + } +} static const char * tok_base_str(struct msph_token *tok) diff --git a/src/msph/tree.c b/src/msph/tree.c index ca9a1de..113dbfb 100644 --- a/src/msph/tree.c +++ b/src/msph/tree.c @@ -1,15 +1,16 @@ +#define SPHO_ENABLE_DEBUG_PRINT #include #include #include - -#define SPHO_ENABLE_DEBUG_PRINT +#include #include "spho/util.h" #include "msph/tree.h" + struct tree_parse { struct msph_token_stream *s; @@ -28,9 +29,12 @@ static void tree_parse_init(struct tree_parse *, static int tree_parse_next_token(struct tree_parse *); static void tree_parse_push_token(struct tree_parse *, struct msph_token *); +static ssize_t tree_ind_fprint(FILE *, int, struct msph_tree *); static void free_the_tree(struct msph_tree *); +static struct msph_tree_unit *tree_parse_unit(struct tree_parse *, + struct msph_tree *); static struct msph_tree_body *tree_parse_body(struct tree_parse *, struct msph_tree *); static struct msph_tree_ident *tree_parse_ident(struct tree_parse *, @@ -84,12 +88,12 @@ msph_tree_makeroot(struct msph_ctx *ctx) MSPH_ERR(ctx, MSPH_ERR_SYS); return (NULL); } - - - T(root)->parent = NULL; T(root)->type = MSPH_TREE_ROOT; + T(root)->parent = NULL; - root->body = NULL; + root->ctx = ctx; + + STAILQ_INIT(&root->head); return (root); } @@ -132,26 +136,348 @@ msph_tree_makeroot(struct msph_ctx *ctx) int msph_tree_parse(struct msph_token_stream *s, struct msph_tree_root *root) { - int res; struct tree_parse p; - struct msph_tree_body *body; + struct msph_tree_unit *unit; - if (root->body != NULL || T(root)->type != MSPH_TREE_ROOT) { + if (T(root)->type != MSPH_TREE_ROOT) { MSPH_ERR(s->ctx, MSPH_ERR_INVAL); return (-1); } tree_parse_init(&p, s); - EXPECT_READ_NEXT(res, &p, MSPH_TREE_ROOT, return (-1)); - if ((body = tree_parse_body(&p, T(root))) == NULL) + if ((unit = tree_parse_unit(&p, T(root))) == NULL) return (-1); - root->body = body; + STAILQ_INSERT_TAIL(&root->head, unit, entries); return (0); } +ssize_t +msph_tree_fprint(FILE *f, struct msph_tree *tree) { + return (tree_ind_fprint(f, 0, tree)); +} + +#define MSPH_TREE_INDENT " " + +__attribute__((format(printf, 3, 4))) +static ssize_t +ind_fprintf(FILE *f, int indent, const char *fmt, ...) +{ + int res; + ssize_t ret; + int i; + va_list ap; + + ret = 0; + va_start(ap, fmt); + + for (i = 0; i < indent; i++) { + res = fprintf(f, "%s", MSPH_TREE_INDENT); + if (res < 0) { + return ((ssize_t)res); + } + ret += (ssize_t)res; + } + + res = vfprintf(f, fmt, ap); + if (res < 0) { + return ((ssize_t)res); + } + ret += (ssize_t)res; + va_end(ap); + + return (ret); +} + +static ssize_t +tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) +{ + ssize_t ret, res; + struct msph_tree_root *root; + struct msph_tree_unit *unit; + struct msph_tree_body *body; + struct msph_tree_dir *dir; + struct msph_tree_nomindecl *nomd; + struct msph_tree_assert *ass; + struct msph_tree_tpdef *tpdef; + struct msph_tree_membdecl *membdecl; + struct msph_tree_conj *conj; + struct msph_tree_disj *disj; + struct msph_tree_impl *impl; + struct msph_tree_arrow *arrow; + struct msph_tree_box *box; + struct msph_tree_forall *forall; + struct msph_tree_appl *appl; + struct msph_tree_trait *trait; + struct msph_tree_name *name; + struct msph_tree_paren *paren; + struct msph_tree_ident *ident; + struct msph_tree_tpexpr *tp; + + ret = 0; + switch (tree->type) { + case MSPH_TREE_ROOT: + root = (struct msph_tree_root *)tree; + if ((res = ind_fprintf(f, indent, "(root\n")) < 0) + return (res); + STAILQ_FOREACH(unit, &root->head, entries) { + if ((res = tree_ind_fprint(f, indent+1, T(unit))) + < 0) + return (res); + ret += res; + } + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + break; + case MSPH_TREE_UNIT: + unit = (struct msph_tree_unit *)tree; + if ((res = ind_fprintf(f, indent, "(unit:%s\n", unit->name)) + < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(unit->body))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_BODY: + body = (struct msph_tree_body *)tree; + if ((res = ind_fprintf(f, indent, "(body\n")) < 0) + return (res); + ret += res; + STAILQ_FOREACH(dir, &body->head, entries) { + if ((res = tree_ind_fprint(f, indent+1, T(dir))) + < 0) + return (res); + ret += res; + } + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_NOMINDECL: + nomd = (struct msph_tree_nomindecl *)tree; + if ((res = ind_fprintf(f, indent, "(nomindecl\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(nomd->id))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_ASSERT: + ass = (struct msph_tree_assert *)tree; + if ((res = ind_fprintf(f, indent, "(assert\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(ass->ltp))) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(ass->rtp))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_TPDEF: + tpdef = (struct msph_tree_tpdef *)tree; + if ((res = ind_fprintf(f, indent, "(tpdef\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(tpdef->id))) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(tpdef->tp))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_MEMBDECL: + membdecl = (struct msph_tree_membdecl *)tree; + if ((res = ind_fprintf(f, indent, "(membdecl:%s\n", + membdecl->id->str)) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(membdecl->tp))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_CONJ: + conj = (struct msph_tree_conj *)tree; + if ((res = ind_fprintf(f, indent, "(conj\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(conj->ltp))) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(conj->rtp))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_DISJ: + disj = (struct msph_tree_disj *)tree; + if ((res = ind_fprintf(f, indent, "(disj\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(disj->ltp))) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(disj->rtp))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_IMPL: + impl = (struct msph_tree_impl *)tree; + if ((res = ind_fprintf(f, indent, "(impl\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(impl->ltp))) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(impl->rtp))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_ARROW: + arrow = (struct msph_tree_arrow *)tree; + if ((res = ind_fprintf(f, indent, "(arrow\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(arrow->ltp))) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(arrow->rtp))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_BOX: + box = (struct msph_tree_box *)tree; + if ((res = ind_fprintf(f, indent, "(box\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(box->inner))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_FORALL: + forall = (struct msph_tree_forall *)tree; + if ((res = ind_fprintf(f, indent, "(forall:\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(forall->ident))) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(forall->inner))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_PAREN: + paren = (struct msph_tree_paren *)tree; + if ((res = ind_fprintf(f, indent, "(paren\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(paren->inner))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_APPL: + appl = (struct msph_tree_appl *)tree; + if ((res = ind_fprintf(f, indent, "(appl\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(appl->id))) < 0) + return (res); + ret += res; + STAILQ_FOREACH(tp, &appl->head, entries) { + if ((res = tree_ind_fprint(f, indent+1, T(tp))) < 0) + return (res); + ret += res; + } + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_NAME: + name = (struct msph_tree_name *)tree; + if ((res = ind_fprintf(f, indent, "(name\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(name->id))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_TRAIT: + trait = (struct msph_tree_trait *)tree; + if ((res = ind_fprintf(f, indent, "(trait\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(trait->body))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_IDENT: + ident = (struct msph_tree_ident *)tree; + if ((res = ind_fprintf(f, indent, "(ident:%s)\n", ident->str)) + < 0) + return (res); + ret += res; + break; + case MSPH_TREE_TRUE: + if ((res = ind_fprintf(f, indent, "(true)\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_FALSE: + if ((res = ind_fprintf(f, indent, "(false)\n")) < 0) + return (res); + ret += res; + break; + default: + SPHO_ASSERT(0); + break; + } + + return (ret); +} static void tree_parse_init(struct tree_parse *p, struct msph_token_stream *s) @@ -188,6 +514,37 @@ tree_parse_next_token(struct tree_parse *p) return (ret); } +struct msph_tree_unit * +tree_parse_unit(struct tree_parse *p, struct msph_tree *parent) +{ + size_t namelen; + struct msph_tree_unit *unit; + + if ((unit = malloc(sizeof(*unit))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(unit)->type = MSPH_TREE_UNIT; + T(unit)->parent = parent; + unit->body = NULL; + + if ((namelen = strlcpy(unit->name, p->s->name, sizeof(unit->name))) + >= sizeof(unit->name)) { + MSPH_ERR(CTX(p), MSPH_ERR_TOOLONG); + goto err; + } + + if ((unit->body = tree_parse_body(p, T(unit))) == NULL) + goto err; + + return (unit); + +err: + free_the_tree(T(unit)); + + return (NULL); +} + static struct msph_tree_body * tree_parse_body(struct tree_parse *p, struct msph_tree *parent) { @@ -208,6 +565,7 @@ tree_parse_body(struct tree_parse *p, struct msph_tree *parent) dir = NULL; switch(CURR_TOKEN(p)->type) { case TOK_KW_TYPE: + SPHO_DEBUG_PRINT("parsing tpdef\n"); dir = tree_parse_tpdef(p, T(body)); break; case TOK_KW_NOMINAL: @@ -219,20 +577,18 @@ tree_parse_body(struct tree_parse *p, struct msph_tree *parent) case TOK_KW_ASSERT: dir = tree_parse_assert(p, T(body)); break; - case TOK_RBRACE: - if ((tok = msph_token_create(CTX(p), TOK_RBRACE, NULL)) + default: + if ((tok = msph_token_copy(CTX(p), CURR_TOKEN(p))) == NULL) goto err; tree_parse_push_token(p, tok); goto ret; - default: - MSPH_ERR_INFO(CTX(p), MSPH_ERR_TREE_NOMATCH, - MSPH_TREE_BODY); - goto err; } if (dir == NULL) goto err; + + STAILQ_INSERT_TAIL(&body->head, dir, entries); } if (res == -1) @@ -290,6 +646,7 @@ tree_parse_ident(struct tree_parse *p, struct msph_tree *parent) { struct msph_tree_ident *id; + SPHO_DEBUG_PRINT("parsing ident\n"); EXPECT_CURR_TOKEN(p, TOK_IDENT, MSPH_TREE_IDENT, return (NULL)); if ((id = malloc(sizeof(*id))) == NULL) { @@ -318,36 +675,47 @@ tree_parse_tpexpr(struct tree_parse *p, struct msph_tree *parent) switch (CURR_TOKEN(p)->type) { case TOK_AMP: + SPHO_DEBUG_PRINT("parsing conj\n"); tp = tree_parse_conj(p, parent); break; case TOK_PIPE: + SPHO_DEBUG_PRINT("parsing disj\n"); tp = tree_parse_disj(p, parent); break; case TOK_IMPL: + SPHO_DEBUG_PRINT("parsing impl\n"); tp = tree_parse_impl(p, parent); break; case TOK_RARROW: + SPHO_DEBUG_PRINT("parsing arrow\n"); tp = tree_parse_arrow(p, parent); break; case TOK_KW_BOX: + SPHO_DEBUG_PRINT("parsing box\n"); tp = tree_parse_box(p, parent); break; case TOK_KW_FORALL: + SPHO_DEBUG_PRINT("parsing forall\n"); tp = tree_parse_forall(p, parent); break; case TOK_IDENT: + SPHO_DEBUG_PRINT("parsing name\n"); tp = tree_parse_name(p, parent); break; case TOK_CONST_TRUE: + SPHO_DEBUG_PRINT("parsing true\n"); tp = tree_parse_true(p, parent); break; case TOK_CONST_FALSE: + SPHO_DEBUG_PRINT("parsing false\n"); tp = tree_parse_false(p, parent); break; case TOK_LPAREN: + SPHO_DEBUG_PRINT("parsing paren\n"); tp = tree_parse_paren(p, parent); break; case TOK_LBRACE: + SPHO_DEBUG_PRINT("parsing trait\n"); tp = tree_parse_trait(p, parent); break; default: @@ -355,6 +723,7 @@ tree_parse_tpexpr(struct tree_parse *p, struct msph_tree *parent) tp = NULL; } + SPHO_DEBUG_PRINT("returning tp type=%x\n", T(tp)->type); return (tp); } @@ -376,14 +745,16 @@ tree_parse_conj(struct tree_parse *p, struct msph_tree *parent) conj->rtp = NULL; EXPECT_READ_NEXT(res, p, MSPH_TREE_CONJ, goto err); - - if ((conj->ltp = tree_parse_tpexpr(p, (struct msph_tree *)conj)) + if ((conj->ltp = tree_parse_tpexpr(p, T(conj))) == NULL) goto err; - if ((conj->rtp = tree_parse_tpexpr(p, (struct msph_tree *)conj)) + EXPECT_READ_NEXT(res, p, MSPH_TREE_CONJ, goto err); + if ((conj->rtp = tree_parse_tpexpr(p, T(conj))) == NULL) goto err; + + return ((struct msph_tree_tpexpr *)conj); err: free_the_tree((struct msph_tree *)conj); @@ -408,14 +779,16 @@ tree_parse_disj(struct tree_parse *p, struct msph_tree *parent) disj->rtp = NULL; EXPECT_READ_NEXT(res, p, MSPH_TREE_DISJ, goto err); - if ((disj->ltp = tree_parse_tpexpr(p, (struct msph_tree *)disj)) == NULL) goto err; + EXPECT_READ_NEXT(res, p, MSPH_TREE_DISJ, goto err); if ((disj->rtp = tree_parse_tpexpr(p, (struct msph_tree *)disj)) == NULL) goto err; + + return ((struct msph_tree_tpexpr *)disj); err: free_the_tree((struct msph_tree *)disj); @@ -428,7 +801,7 @@ tree_parse_impl(struct tree_parse *p, struct msph_tree *parent) int res; struct msph_tree_impl *impl; - EXPECT_CURR_TOKEN(p, TOK_PIPE, MSPH_TREE_IMPL, return (NULL)); + EXPECT_CURR_TOKEN(p, TOK_IMPL, MSPH_TREE_IMPL, return (NULL)); if ((impl = malloc(sizeof(*impl))) == NULL) { MSPH_ERR(CTX(p), MSPH_ERR_SYS); @@ -440,14 +813,16 @@ tree_parse_impl(struct tree_parse *p, struct msph_tree *parent) impl->rtp = NULL; EXPECT_READ_NEXT(res, p, MSPH_TREE_IMPL, goto err); - if ((impl->ltp = tree_parse_tpexpr(p, (struct msph_tree *)impl)) == NULL) goto err; + EXPECT_READ_NEXT(res, p, MSPH_TREE_IMPL, goto err); if ((impl->rtp = tree_parse_tpexpr(p, (struct msph_tree *)impl)) == NULL) goto err; + + return ((struct msph_tree_tpexpr *)impl); err: free_the_tree((struct msph_tree *)impl); @@ -458,30 +833,32 @@ struct msph_tree_tpexpr * tree_parse_arrow(struct tree_parse *p, struct msph_tree *parent) { int res; - struct msph_tree_arrow *arrw; + struct msph_tree_arrow *arrow; - EXPECT_CURR_TOKEN(p, TOK_PIPE, MSPH_TREE_ARROW, return (NULL)); + EXPECT_CURR_TOKEN(p, TOK_RARROW, MSPH_TREE_ARROW, return (NULL)); - if ((arrw = malloc(sizeof(*arrw))) == NULL) { + if ((arrow = malloc(sizeof(*arrow))) == NULL) { MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - T(arrw)->type = MSPH_TREE_ARROW; - T(arrw)->parent = parent; - arrw->ltp = NULL; - arrw->rtp = NULL; + T(arrow)->type = MSPH_TREE_ARROW; + T(arrow)->parent = parent; + arrow->ltp = NULL; + arrow->rtp = NULL; EXPECT_READ_NEXT(res, p, MSPH_TREE_ARROW, goto err); - - if ((arrw->ltp = tree_parse_tpexpr(p, (struct msph_tree *)arrw)) + if ((arrow->ltp = tree_parse_tpexpr(p, (struct msph_tree *)arrow)) == NULL) goto err; - if ((arrw->rtp = tree_parse_tpexpr(p, (struct msph_tree *)arrw)) + EXPECT_READ_NEXT(res, p, MSPH_TREE_ARROW, goto err); + if ((arrow->rtp = tree_parse_tpexpr(p, (struct msph_tree *)arrow)) == NULL) goto err; + + return ((struct msph_tree_tpexpr *)arrow); err: - free_the_tree((struct msph_tree *)arrw); + free_the_tree((struct msph_tree *)arrow); return (NULL); } @@ -546,6 +923,7 @@ err: return (NULL); } +/* parse name or appl */ struct msph_tree_tpexpr * tree_parse_name(struct tree_parse *p, struct msph_tree *parent) { @@ -553,22 +931,32 @@ tree_parse_name(struct tree_parse *p, struct msph_tree *parent) struct msph_tree_ident *id; struct msph_tree_name *name; struct msph_tree_tpexpr *ret; + struct msph_token *tok; ret = NULL; name = NULL; if ((id = tree_parse_ident(p, NULL)) == NULL) return (NULL); + SPHO_DEBUG_PRINT("parsed ident=%s\n", id->str); - if ((res = tree_parse_next_token(p)) == 1 && - CURR_TOKEN(p)->type == TOK_LBRAK) { - if ((ret = tree_parse_applargs(p, id, parent)) == NULL) + if ((res = tree_parse_next_token(p)) == 1) { + if (CURR_TOKEN(p)->type == TOK_LBRAK) { + if ((ret = tree_parse_applargs(p, id, parent)) == NULL) + goto err; + return (ret); + } + + if ((tok = msph_token_copy(CTX(p), CURR_TOKEN(p))) + == NULL) { goto err; - return (ret); + } + tree_parse_push_token(p, tok); } else if (res == -1) { goto err; } + SPHO_DEBUG_PRINT("ident is name\n"); if ((name = malloc(sizeof(*name))) == NULL) { MSPH_ERR(CTX(p), MSPH_ERR_SYS); goto err; @@ -576,6 +964,7 @@ tree_parse_name(struct tree_parse *p, struct msph_tree *parent) T(name)->type = MSPH_TREE_NAME; T(name)->parent = parent; + T(id)->parent = T(name); name->id = id; return ((struct msph_tree_tpexpr *)name); @@ -736,8 +1125,6 @@ tree_parse_trait(struct tree_parse *p, struct msph_tree *parent) T(trait)->parent = parent; trait->body = NULL; - EXPECT_READ_NEXT(res, p, MSPH_TREE_TRAIT, goto err); - if ((trait->body = tree_parse_body(p, T(trait))) == NULL) goto err; @@ -759,7 +1146,6 @@ tree_parse_nomindecl(struct tree_parse *p, struct msph_tree *parent) EXPECT_CURR_TOKEN(p, TOK_KW_NOMINAL, MSPH_TREE_NOMINDECL, return (NULL)); - EXPECT_READ_NEXT(res, p, MSPH_TREE_NOMINDECL, return (NULL)); if ((nomd = malloc(sizeof(*nomd))) == NULL) { MSPH_ERR(CTX(p), MSPH_ERR_SYS); @@ -769,6 +1155,7 @@ tree_parse_nomindecl(struct tree_parse *p, struct msph_tree *parent) T(nomd)->parent = parent; nomd->id = NULL; + EXPECT_READ_NEXT(res, p, MSPH_TREE_NOMINDECL, return (NULL)); if ((nomd->id = tree_parse_ident(p, T(nomd))) == NULL) goto err; @@ -793,7 +1180,7 @@ tree_parse_membdecl(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - T(membd)->type = MSPH_TREE_NOMINDECL; + T(membd)->type = MSPH_TREE_MEMBDECL; T(membd)->parent = parent; membd->id = NULL; membd->tp = NULL; @@ -843,7 +1230,7 @@ tree_parse_assert(struct tree_parse *p, struct msph_tree *parent) goto err); EXPECT_READ_NEXT(res, p, MSPH_TREE_ASSERT, goto err); - if ((ass->ltp = tree_parse_tpexpr(p, T(ass))) == NULL) + if ((ass->rtp = tree_parse_tpexpr(p, T(ass))) == NULL) goto err; return ((struct msph_tree_dir *)ass); @@ -856,7 +1243,8 @@ err: static void free_the_tree(struct msph_tree *tree) { - /* no one can free the tree :´( */ - SPHO_POSTCOND((void *)tree == (void *)free); + /* no one will free the tree :´( */ + SPHO_POSTCOND((void *)tree != (void *)free); + SPHO_POSTCOND(0); }