From 17be15d7b5194467331ebb060a6d1ba4c35a8721 Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Tue, 22 Apr 2025 21:08:03 +0300 Subject: [PATCH] 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); }