From bc9d13896015031601d4defebbbc9611d67d9f71 Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Thu, 26 Jun 2025 01:28:04 +0200 Subject: [PATCH 01/10] added cmake presets --- CMakeLists.txt | 8 ++--- CMakePresets.json | 82 +++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 86 insertions(+), 4 deletions(-) create mode 100644 CMakePresets.json diff --git a/CMakeLists.txt b/CMakeLists.txt index 99b7405..ea221d1 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -5,10 +5,10 @@ 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") + "-Wconversion -Wsign-conversion -Wimplicit-fallthrough" + "-Werror=implicit" + "-Werror=incompatible-pointer-types" + "-Werror=int-conversion") set(CMAKE_VERBOSE_MAKEFILE ON) set(CMAKE_EXPORT_COMPILE_COMMANDS ON) diff --git a/CMakePresets.json b/CMakePresets.json new file mode 100644 index 0000000..f9f5e51 --- /dev/null +++ b/CMakePresets.json @@ -0,0 +1,82 @@ +{ + "version": 10, + "cmakeMinimumRequired": { + "major": 3, + "minor": 31, + "patch": 0 + }, + "configurePresets": [ + { + "name": "debug", + "displayName": "Debug", + "description": "Debug config", + "generator": "Unix Makefiles", + "binaryDir": "${sourceDir}/build-${presetName}/", + "cacheVariables": { + "CMAKE_BUILD_TYPE": "Debug" + } + }, + { + "name": "release", + "displayName": "Release", + "description": "Release config", + "generator": "Unix Makefiles", + "binaryDir": "${sourceDir}/build-${presetName}/", + "cacheVariables": { + "CMAKE_BUILD_TYPE": "Release" + } + } + ], + "buildPresets": [ + { + "name": "debug", + "configurePreset": "debug" + }, + { + "name": "release", + "configurePreset": "release" + } + ], + "$comment": [{ + "testPresets": [ + { + "name": "default", + "configurePreset": "default", + "output": {"outputOnFailure": true}, + "execution": {"noTestsAction": "error", "stopOnFailure": true} + } + ], + "packagePresets": [ + { + "name": "default", + "configurePreset": "default", + "generators": [ + "TGZ" + ] + } + ], + "workflowPresets": [ + { + "name": "default", + "steps": [ + { + "type": "configure", + "name": "default" + }, + { + "type": "build", + "name": "default" + }, + { + "type": "test", + "name": "default" + }, + { + "type": "package", + "name": "default" + } + ] + } + ] + }] +} From 65066c493e6bc4b2d7876e6144c59ecdab8d7774 Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Fri, 27 Jun 2025 02:45:56 +0200 Subject: [PATCH 02/10] typo --- docs/about/formalities.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/about/formalities.md b/docs/about/formalities.md index b2b01f1..57871b4 100644 --- a/docs/about/formalities.md +++ b/docs/about/formalities.md @@ -116,7 +116,7 @@ n fresh // 1 + n! premises // trace pairs: i ∈ [1..(n! + 1)], premise[i] -- conclusion -c, γ* ⊢ a_1, ..., a_n +c, γ* ⊢ a_1, ..., a_n, δ* ∀ I ⊆ {1, ..., n}. c, γ* ⊢ { a_i | i ∈ I }, δ* OR From 33f38c03d6db65a5ee4030ca4057c07496361a27 Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Fri, 27 Jun 2025 02:48:48 +0200 Subject: [PATCH 03/10] infix parsing and prebind fixes --- .gitignore | 2 + include/msph/token.h | 9 +- include/msph/tree.h | 19 +- include/spho/ctx.h | 3 + include/spho/err.h | 2 +- include/spho/scope.h | 65 +- src/msph/msph.c | 31 +- src/msph/sphophi.c | 128 ++- src/msph/token.c | 10 +- src/msph/tree.c | 2196 +++++++++++++++++++++++++----------------- src/spho/bind.c | 9 +- src/spho/ctx.c | 25 +- src/spho/scope.c | 85 +- src/spho/tp.c | 60 +- 14 files changed, 1555 insertions(+), 1089 deletions(-) diff --git a/.gitignore b/.gitignore index 4929d75..4935877 100644 --- a/.gitignore +++ b/.gitignore @@ -52,6 +52,8 @@ Mkfile.old dkms.conf # vim +.swp +.swo .*.swp .*.swo diff --git a/include/msph/token.h b/include/msph/token.h index b984039..21617eb 100644 --- a/include/msph/token.h +++ b/include/msph/token.h @@ -39,6 +39,8 @@ enum msph_tok_type { + TOK_INVAL = -1, // special: invalid, use to mark invalid toks + TOK_EOF = 0, // special: end-of-file TOK_LBRACE, // { TOK_RBRACE, // } TOK_LBRAK, // [ @@ -67,9 +69,10 @@ 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: end of array/token stream + TOK_WSPACE, // whitespace + + TOK_NOPE // special indicator: end of info array, + // start of parsing }; #define MSPH_TAB_WIDTH 8 diff --git a/include/msph/tree.h b/include/msph/tree.h index 028f329..a7567ab 100644 --- a/include/msph/tree.h +++ b/include/msph/tree.h @@ -37,6 +37,8 @@ struct msph_decor { #define MSPH_TREE_BOX 0x004a #define MSPH_TREE_FORALL 0x004b #define MSPH_TREE_PAREN 0x004c +#define MSPH_TREE_SUBT 0x004d + #define MSPH_TREE_IDENT 0x0100 #define MSPH_TREE_NAMEDECL 0x0101 @@ -162,8 +164,7 @@ struct msph_tree_membdecl { struct msph_tree_assert { struct msph_tree_dir hd_dir; - struct msph_tree_tpexpr *ltp; - struct msph_tree_tpexpr *rtp; + struct msph_tree_tpexpr *tp; }; struct msph_tree_namedecl { @@ -209,6 +210,7 @@ struct msph_tree_trait { struct msph_tree_body *body; }; +/* XXX should probably merge all binary type ops into one */ struct msph_tree_conj { struct msph_tree_tpexpr hd_tpe; @@ -230,6 +232,13 @@ struct msph_tree_impl { struct msph_tree_tpexpr *rtp; }; +struct msph_tree_subt { + struct msph_tree_tpexpr hd_tpe; + + struct msph_tree_tpexpr *ltp; + struct msph_tree_tpexpr *rtp; +}; + struct msph_tree_arrow { struct msph_tree_tpexpr hd_tpe; @@ -259,7 +268,11 @@ struct msph_tree_paren { struct msph_tree_root *msph_tree_makeroot(struct msph_ctx *); -int msph_tree_parse(struct msph_token_stream *, struct msph_tree_root *); +#define MSPH_PARSE_PREFIX 1 +#define MSPH_PARSE_INFIX 2 + +int msph_tree_parse(struct msph_token_stream *, struct msph_tree_root *, + int); ssize_t msph_tree_fprint(FILE *, struct msph_tree *); diff --git a/include/spho/ctx.h b/include/spho/ctx.h index 9858e85..00bb1f4 100644 --- a/include/spho/ctx.h +++ b/include/spho/ctx.h @@ -14,6 +14,8 @@ struct spho_ctx { int err_info; char errbuf[SPHO_ERR_BUF_LEN]; + unsigned int nom_cnt; + #ifdef SPHO_DEBUG char filebuf[SPHO_ERR_FILEBUF_LEN]; int errline; @@ -22,6 +24,7 @@ struct spho_ctx { }; struct spho_ctx *spho_ctx_create(void); +void spho_ctx_init(struct spho_ctx *); void spho_ctx_destroy(struct spho_ctx *); const char *spho_ctx_strerror(struct spho_ctx *); diff --git a/include/spho/err.h b/include/spho/err.h index 2f56532..6e34929 100644 --- a/include/spho/err.h +++ b/include/spho/err.h @@ -39,7 +39,7 @@ (ctx)->err = (e); \ (ctx)->err_info = (info); \ snprintf((ctx)->filebuf, sizeof((ctx)->filebuf), \ - __FILE__); \ + __FILE__ ":%s", __func__); \ (ctx)->errline = __LINE__; \ } while (0) diff --git a/include/spho/scope.h b/include/spho/scope.h index ff682c4..52362e8 100644 --- a/include/spho/scope.h +++ b/include/spho/scope.h @@ -7,13 +7,22 @@ #define SPHO_NOM_LEN 128 -/* name */ -struct spho_nom { - char s[SPHO_NOM_LEN]; - SLIST_ENTRY(spho_nom) next; // TODO change to allocs + +union spho_ext_data { + void *ptr; + uint64_t n; +}; + +/* name */ +struct spho_nom { + unsigned int id; + char s[SPHO_NOM_LEN]; + + union spho_ext_data ext_data; + + SLIST_ENTRY(spho_nom) entries; }; -SLIST_HEAD(spho_nom_l, spho_nom); #define TP_KONST_KEY_TRUE 0x43445 /* don't change!!!!! */ @@ -76,6 +85,7 @@ struct spho_tp { int kind; union tp_data d; + union spho_ext_data ext_data; STAILQ_ENTRY(spho_tp) entries; }; @@ -85,30 +95,20 @@ struct spho_tp_op { struct spho_scope *op_sc; struct spho_tp *op_tp; + union spho_ext_data ext_data; }; STAILQ_HEAD(spho_tp_l, spho_tp); -struct spho_tp_ptr { - struct spho_tp *p; - STAILQ_ENTRY(spho_tp_ptr) entries; -}; - -STAILQ_HEAD(spho_tp_ptr_l, spho_tp_ptr); - struct spho_tp_alloc { union { struct spho_tp tp; struct spho_tp_op tp_op; } alloc; - TAILQ_ENTRY(spho_tp_alloc) allocs; + STAILQ_ENTRY(spho_tp_alloc) entries; }; -TAILQ_HEAD(spho_tp_alloc_l, spho_tp_alloc); - -SLIST_HEAD(spho_scope_l, spho_scope); - /* defined in spho/bind.h */ struct spho_bind; @@ -116,33 +116,38 @@ struct spho_scope { struct spho_ctx *ctx; struct spho_scope *parent; - struct spho_scope_l subs; - - size_t n_noms; - struct spho_nom_l noms; - struct spho_tp_alloc_l tps; - + STAILQ_HEAD( + spho_scope_l, + spho_scope) subs; + STAILQ_HEAD( + spho_tp_alloc_l, + spho_tp_alloc) tps; + SLIST_HEAD( + spho_nom_l, + spho_nom) noms; + size_t nom_cnt; struct spho_prebind *bind_loc; + union spho_ext_data ext_data; - SLIST_ENTRY(spho_scope) next; + STAILQ_ENTRY(spho_scope) entries; }; #define SPHO_SC_ERR(sc, err) SPHO_ERR((sc)->ctx, (err)) -int spho_scope_init(struct spho_scope *, struct spho_ctx *, +void spho_scope_init(struct spho_scope *, struct spho_ctx *, struct spho_scope *); -void spho_scope_term(struct spho_scope *); +void spho_scope_cleanup(struct spho_scope *); struct spho_scope *spho_scope_global(struct spho_ctx *); -struct spho_scope *spho_scope_create(struct spho_scope *); +struct spho_scope *spho_scope_create_subscope(struct spho_scope *); -void spho_scope_destroy(struct spho_scope *); +void spho_scope_free(struct spho_scope *); struct spho_nom *spho_scope_nom_add(struct spho_scope *, const char *, size_t); -int spho_scope_nom_lookup_str(struct spho_scope *, const char *, size_t, +int spho_scope_nom_lookup(struct spho_scope *, const char *, size_t, struct spho_nom **); -int spho_scope_nom_lookup_str_strict(struct spho_scope *, const char *, +int spho_scope_nom_lookup_strict(struct spho_scope *, const char *, size_t, struct spho_nom **); int spho_scope_prebind_init(struct spho_scope *); diff --git a/src/msph/msph.c b/src/msph/msph.c index 041bdff..1554e61 100644 --- a/src/msph/msph.c +++ b/src/msph/msph.c @@ -9,21 +9,25 @@ struct msph_opts { int tokenize_only; + int parser; const char *in_path; const char *out_path; } run_opts = { 0, + MSPH_PARSE_INFIX, 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" +"msph: micro sappho\n" \ +" Usage: msph [-t] [-o out_path] [-p i|p] [in_path]\n" \ +"\n" \ +" -t - print tokenization\n" \ +" -o - output path\n" \ +" -p i[nfix]|p[refix] - infix or prefix &, |, =>, -> parsing\n" \ +" (default infix)\n" void print_usage(void) @@ -38,7 +42,7 @@ main(int argc, char *argv[]) { int opt; - while ((opt = getopt(argc, argv, "hto:")) != -1) { + while ((opt = getopt(argc, argv, "hto:p:")) != -1) { switch (opt) { case 't': run_opts.tokenize_only = 1; @@ -46,6 +50,19 @@ main(int argc, char *argv[]) case 'o': run_opts.out_path = optarg; break; + case 'p': + switch (optarg[0]) { + case 'p': + run_opts.parser = MSPH_PARSE_PREFIX; + break; + case 'i': + run_opts.parser = MSPH_PARSE_INFIX; + break; + default: + print_usage(); + exit(EXIT_FAILURE); + } + break; case 'h': print_usage(); exit(EXIT_SUCCESS); @@ -122,7 +139,7 @@ run(struct msph_opts *opts) goto err; } - if (msph_tree_parse(s, root) == -1) + if (msph_tree_parse(s, root, opts->parser) == -1) goto err; printf("msph tree successfully parsed :)\n"); diff --git a/src/msph/sphophi.c b/src/msph/sphophi.c index a9dec26..59eacdb 100644 --- a/src/msph/sphophi.c +++ b/src/msph/sphophi.c @@ -15,7 +15,7 @@ static int msph_tree_sphophi_decor_tpexpr_nom(struct spho_scope *, struct msph_tree *); static int msph_tree_sphophi_decor_tp(struct spho_scope *, struct msph_tree *); -static int msph_tree_sphophi_tp_prebind(struct spho_scope *, +static int msph_tree_sphophi_prebind(struct spho_scope *, struct msph_tree *); /* is the tree a name binding? */ @@ -65,6 +65,8 @@ static int msph_sphophi_foreach_pre_disj(msph_tree_sphophi_f, struct spho_scope *, struct msph_tree_disj *); static int msph_sphophi_foreach_pre_impl(msph_tree_sphophi_f, struct spho_scope *, struct msph_tree_impl *); +static int msph_sphophi_foreach_pre_subt(msph_tree_sphophi_f, + struct spho_scope *, struct msph_tree_subt *); static int msph_sphophi_foreach_pre_arrow(msph_tree_sphophi_f, struct spho_scope *, struct msph_tree_arrow *); static int msph_sphophi_foreach_pre_box(msph_tree_sphophi_f, @@ -109,6 +111,8 @@ static int msph_sphophi_foreach_post_disj(msph_tree_sphophi_f, struct spho_scope *, struct msph_tree_disj *); static int msph_sphophi_foreach_post_impl(msph_tree_sphophi_f, struct spho_scope *, struct msph_tree_impl *); +static int msph_sphophi_foreach_post_subt(msph_tree_sphophi_f, + struct spho_scope *, struct msph_tree_subt *); static int msph_sphophi_foreach_post_arrow(msph_tree_sphophi_f, struct spho_scope *, struct msph_tree_arrow *); static int msph_sphophi_foreach_post_box(msph_tree_sphophi_f, @@ -154,7 +158,7 @@ msph_sphophi_tp(struct msph_tree_root *root) int msph_sphophi_tp_prebind(struct msph_tree_root *root) { - return (msph_sphophi_foreach_pre(msph_tree_sphophi_tp_prebind, + return (msph_sphophi_foreach_pre(msph_tree_sphophi_prebind, root)); } @@ -191,25 +195,25 @@ msph_tree_sphophi_decor_scope(struct spho_scope *sc, struct msph_tree *tree) case MSPH_TREE_UNIT: case MSPH_TREE_TRAIT: case MSPH_TREE_FORALL: - if ((SCOPE(tree) = spho_scope_create(sc)) == NULL) - ret = -1; + if ((SCOPE(tree) = spho_scope_create_subscope(sc)) == NULL) + return (-1); ADD_FLAG(tree, MSPH_TREE_FLAG_SCOPE); break; case MSPH_TREE_TPDEF: tpdef = (struct msph_tree_tpdef *)tree; - if (! STAILQ_EMPTY(&tpdef->params) && - ((SCOPE(tpdef) = spho_scope_create(sc)) == NULL)) { - ret = -1; - } + if (STAILQ_EMPTY(&tpdef->params)) + break; + if (((SCOPE(tpdef) = spho_scope_create_subscope(sc)) == NULL)) + return (-1); ADD_FLAG(tree, MSPH_TREE_FLAG_SCOPE); break; - case MSPH_TREE_IDENT: - if (! IS_BINDING(tree->parent)) - break; + case MSPH_TREE_NAMEDECL: + SPHO_ASSERT(IS_BINDING(tree->parent)); ident = (struct msph_tree_ident *)tree; if ((NOM(ident) = spho_scope_nom_add(sc, ident->str, - sizeof(ident->str))) == NULL) - ret = -1; + sizeof(ident->str))) == NULL) { + return (-1); + } ADD_FLAG(tree, MSPH_TREE_FLAG_NOM); break; default: @@ -230,12 +234,14 @@ msph_tree_sphophi_decor_tpexpr_nom(struct spho_scope *sc, switch (TREE_ID(tree)) { case MSPH_TREE_IDENT: - if (! IS_TPEXPR(tree->parent)) - break; - ident = (struct msph_tree_ident *)tree; - ret = spho_scope_nom_lookup_str_strict(sc, ident->str, - sizeof(ident->str), &NOM(ident)); + SPHO_ASSERT(IS_TPEXPR(tree->parent)); + ident = (struct msph_tree_ident *)tree; + if (spho_scope_nom_lookup_strict(sc, ident->str, + sizeof(ident->str), &NOM(ident)) == -1) { + return (-1); + } + ADD_FLAG(ident, MSPH_TREE_FLAG_NOM); break; default: break; @@ -261,6 +267,7 @@ msph_tree_sphophi_decor_tp(struct spho_scope *sc, struct msph_tree *tree) struct msph_tree_trait *trait; struct msph_tree_dir *dir; struct msph_tree_membdecl *membd; + struct msph_tree_subt *subt; struct spho_tp_l *tps; struct spho_tp *tp, *tp_memb; @@ -271,43 +278,59 @@ msph_tree_sphophi_decor_tp(struct spho_scope *sc, struct msph_tree *tree) dir = NULL; membd = NULL; - if (! (tree->type & MSPH_TREE_TPEXPR)) + if (! IS_TPEXPR(tree)) return (0); switch (TREE_ID(tree)) { case MSPH_TREE_CONJ: conj = (struct msph_tree_conj *)tree; if ((TP(conj) = spho_tp_create_conj(sc, TP(conj->ltp), - TP(conj->rtp))) == NULL) + TP(conj->rtp))) == NULL) { goto cleanup; + } ADD_FLAG(conj, MSPH_TREE_FLAG_TP); break; case MSPH_TREE_DISJ: disj = (struct msph_tree_disj *)tree; if ((TP(disj) = spho_tp_create_conj(sc, TP(disj->ltp), - TP(disj->rtp))) == NULL) + TP(disj->rtp))) == NULL) { goto cleanup; + } ADD_FLAG(disj, MSPH_TREE_FLAG_TP); break; case MSPH_TREE_IMPL: impl = (struct msph_tree_impl *)tree; if ((TP(impl) = spho_tp_create_conj(sc, TP(impl->ltp), - TP(impl->rtp))) == NULL) + TP(impl->rtp))) == NULL) { goto cleanup; + } ADD_FLAG(impl, MSPH_TREE_FLAG_TP); break; + case MSPH_TREE_SUBT: + /* a <: b == box(a => b) */ + subt = (struct msph_tree_subt *)tree; + if ((tp = spho_tp_create_impl(sc, TP(subt->ltp), + TP(subt->rtp))) == NULL) { + goto cleanup; + } + if ((TP(subt) = spho_tp_create_box(sc, tp)) == NULL) + goto cleanup; + ADD_FLAG(subt, MSPH_TREE_FLAG_TP); + break; case MSPH_TREE_ARROW: arrow = (struct msph_tree_arrow *)tree; if ((TP(arrow) = spho_tp_create_conj(sc, TP(arrow->ltp), - TP(arrow->rtp))) == NULL) + TP(arrow->rtp))) == NULL) { goto cleanup; + } ADD_FLAG(arrow, MSPH_TREE_FLAG_TP); break; case MSPH_TREE_TPNAME: tpname = (struct msph_tree_tpname *)tree; if ((TP(tpname) = spho_tp_create_name(sc, NOM(tpname->name))) - == NULL) + == NULL) { goto cleanup; + } ADD_FLAG(tpname, MSPH_TREE_FLAG_TP); break; case MSPH_TREE_TPAPPL: @@ -383,7 +406,7 @@ msph_tree_sphophi_decor_tp(struct spho_scope *sc, struct msph_tree *tree) ADD_FLAG(trait, MSPH_TREE_FLAG_TP); break; default: - SPHO_ASSERT(0); + SPHO_RIP("impossible-default-reached"); break; } @@ -397,7 +420,7 @@ cleanup: } static int -msph_tree_sphophi_tp_prebind(struct spho_scope *sc, +msph_tree_sphophi_prebind(struct spho_scope *sc, struct msph_tree *tree) { int ret; @@ -444,6 +467,8 @@ msph_tree_sphophi_tp_prebind(struct spho_scope *sc, } } break; + case MSPH_TREE_NOMINDECL: + break; default: break; } @@ -628,9 +653,7 @@ msph_sphophi_foreach_pre_assert(msph_tree_sphophi_f f, struct spho_scope *sc, if ((ret = f(sc, TREE(ass))) != 0) return (ret); - if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, ass->ltp)) != 0) - return (ret); - if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, ass->rtp)) != 0) + if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, ass->tp)) != 0) return (ret); return (ret); @@ -680,6 +703,10 @@ msph_sphophi_foreach_pre_tpexpr(msph_tree_sphophi_f f, struct spho_scope *sc, ret = msph_sphophi_foreach_pre_impl(f, sc, (struct msph_tree_impl *)tpexpr); break; + case MSPH_TREE_SUBT: + ret = msph_sphophi_foreach_pre_subt(f, sc, + (struct msph_tree_subt *)tpexpr); + break; case MSPH_TREE_ARROW: ret = msph_sphophi_foreach_pre_arrow(f, sc, (struct msph_tree_arrow *)tpexpr); @@ -717,7 +744,7 @@ msph_sphophi_foreach_pre_tpexpr(msph_tree_sphophi_f f, struct spho_scope *sc, (struct msph_tree_false *)tpexpr); break; default: - SPHO_RIP("default-reach"); + SPHO_RIP("impossible-default-reached"); break; } @@ -775,6 +802,23 @@ msph_sphophi_foreach_pre_impl(msph_tree_sphophi_f f, struct spho_scope *sc, return (msph_sphophi_foreach_pre_tpexpr(f, sc, impl->rtp)); } +static int +msph_sphophi_foreach_pre_subt(msph_tree_sphophi_f f, struct spho_scope *sc, + struct msph_tree_subt *subt) +{ + int ret; + + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(subt != NULL); + + if ((ret = f(sc, TREE(subt))) != 0) + return (ret); + + if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, subt->ltp)) != 0) + return (ret); + return (msph_sphophi_foreach_pre_tpexpr(f, sc, subt->rtp)); +} + static int msph_sphophi_foreach_pre_arrow(msph_tree_sphophi_f f, struct spho_scope *sc, struct msph_tree_arrow *arrow) @@ -1092,9 +1136,7 @@ msph_sphophi_foreach_post_assert(msph_tree_sphophi_f f, struct spho_scope *sc, SPHO_PRECOND(sc != NULL); SPHO_PRECOND(ass != NULL); - if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, ass->ltp)) != 0) - return (ret); - if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, ass->rtp)) != 0) + if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, ass->tp)) != 0) return (ret); return (f(sc, TREE(ass))); @@ -1144,6 +1186,10 @@ msph_sphophi_foreach_post_tpexpr(msph_tree_sphophi_f f, struct spho_scope *sc, ret = msph_sphophi_foreach_post_impl(f, sc, (struct msph_tree_impl *)tpexpr); break; + case MSPH_TREE_SUBT: + ret = msph_sphophi_foreach_post_subt(f, sc, + (struct msph_tree_subt *)tpexpr); + break; case MSPH_TREE_ARROW: ret = msph_sphophi_foreach_post_arrow(f, sc, (struct msph_tree_arrow *)tpexpr); @@ -1240,6 +1286,22 @@ msph_sphophi_foreach_post_impl(msph_tree_sphophi_f f, struct spho_scope *sc, return (f(sc, TREE(impl))); } +static int +msph_sphophi_foreach_post_subt(msph_tree_sphophi_f f, struct spho_scope *sc, + struct msph_tree_subt *subt) +{ + int ret; + + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(subt != NULL); + + if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, subt->ltp)) != 0) + return (ret); + if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, subt->rtp)) != 0) + return (ret); + + return (f(sc, TREE(subt))); +} static int msph_sphophi_foreach_post_arrow(msph_tree_sphophi_f f, struct spho_scope *sc, struct msph_tree_arrow *arrow) diff --git a/src/msph/token.c b/src/msph/token.c index e83a11d..abe2677 100644 --- a/src/msph/token.c +++ b/src/msph/token.c @@ -48,7 +48,7 @@ struct msph_matcher token_matchers[] = { { 0, 0, TOK_CONST_FALSE }, { 0, 0, TOK_IDENT }, - { 0, 0, TOK_END } + { 0, 0, TOK_NOPE } }; struct msph_matcher wspace = { 0, 0, TOK_WSPACE }; @@ -86,7 +86,7 @@ struct msph_token_info { TOK_INFO(TOK_CONST_FALSE, "False"), TOK_INFO(TOK_IDENT, NULL), - { TOK_END , NULL, NULL } + { TOK_NOPE , NULL, NULL } #undef TOK_INFO }; @@ -305,7 +305,7 @@ read_single_tok(struct msph_token *ptr, struct msph_token_stream *s) return (-1); max_m = 0; - for (m = 1; token_matchers[m].type != TOK_END; m++) { + for (m = 1; token_matchers[m].type != TOK_NOPE; m++) { res = tok_match(ctx, src, &token_matchers[m]); if (res == -1) @@ -358,7 +358,7 @@ msph_token_copy(struct msph_ctx *ctx, struct msph_token *token) info = NULL; - for (i = 0; token_info[i].type != TOK_END; i++) { + for (i = 0; token_info[i].type != TOK_NOPE; i++) { if (token_info[i].type == token->type) { info = &token_info[i]; break; @@ -769,7 +769,7 @@ static const char * tok_base_str(struct msph_token *tok) { size_t i; - for (i = 0; token_info[i].type != TOK_END; i++) { + for (i = 0; token_info[i].type != TOK_NOPE; i++) { if (token_info[i].type == tok->type) return (token_info[i].dbg_str); } diff --git a/src/msph/tree.c b/src/msph/tree.c index 199628c..b50f0f7 100644 --- a/src/msph/tree.c +++ b/src/msph/tree.c @@ -1,4 +1,6 @@ #define SPHO_ENABLE_DEBUG_PRINT +#include "msph/common.h" +#include "msph/common.h" #include @@ -13,9 +15,10 @@ struct tree_parse { struct msph_token_stream *s; - struct msph_token curr; + int parser; + SLIST_HEAD(msph_token_l, msph_token) head; }; @@ -24,10 +27,8 @@ struct tree_parse { #define CTX(parse) ((parse)->s->ctx) static void tree_parse_init(struct tree_parse *, - struct msph_token_stream *); + struct msph_token_stream *, int); 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 *); @@ -59,6 +60,37 @@ static struct msph_tree_dir *tree_parse_membdecl( static struct msph_tree_tpexpr *tree_parse_tpexpr(struct tree_parse *, struct msph_tree *); + +/* prefix &, |, =>, -> */ +static struct msph_tree_tpexpr *tree_parse_tpexpr_prefix(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_conj_prefix(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_disj_prefix(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_impl_prefix(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_arrow_prefix(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_subt_prefix(struct tree_parse *, + struct msph_tree *); + +/* infix &, |, =>, -> */ +static struct msph_tree_tpexpr *tree_parse_tpexpr_infix(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_conj_infix(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_disj_infix(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_impl_infix(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_arrow_infix(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_subt_infix(struct tree_parse *, + struct msph_tree *); + +static struct msph_tree_tpexpr *tree_parse_tpexpr_atom(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 *, @@ -71,14 +103,6 @@ static struct msph_tree_tpexpr *tree_parse_tpapplargs(struct tree_parse *, 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 *, @@ -91,12 +115,13 @@ msph_tree_makeroot(struct msph_ctx *ctx) { struct msph_tree_root *root; - if ((root = malloc(sizeof(*root))) == NULL) { + if ((root = calloc(1, sizeof(*root))) == NULL) { MSPH_ERR(ctx, MSPH_ERR_SYS); return (NULL); } TREE(root)->type = MSPH_TREE_ROOT; TREE(root)->parent = NULL; + DECOR_INIT(root); root->ctx = ctx; @@ -141,7 +166,8 @@ msph_tree_makeroot(struct msph_ctx *ctx) } while (0) int -msph_tree_parse(struct msph_token_stream *s, struct msph_tree_root *root) +msph_tree_parse(struct msph_token_stream *s, struct msph_tree_root *root, + int parser) { struct tree_parse p; struct msph_tree_unit *unit; @@ -151,7 +177,15 @@ msph_tree_parse(struct msph_token_stream *s, struct msph_tree_root *root) return (-1); } - tree_parse_init(&p, s); + switch (parser) { + case MSPH_PARSE_INFIX: + case MSPH_PARSE_PREFIX: + tree_parse_init(&p, s, parser); + break; + default: + MSPH_ERR(s->ctx, MSPH_ERR_INVAL); + return (-1); + } if ((unit = tree_parse_unit(&p, TREE(root))) == NULL) return (-1); @@ -166,6 +200,1180 @@ msph_tree_fprint(FILE *f, struct msph_tree *tree) { return (tree_ind_fprint(f, 0, tree)); } + +static void +tree_parse_init(struct tree_parse *p, struct msph_token_stream *s, int parser) +{ + p->s = s; + memset(&p->curr, 0, sizeof(p->curr)); + p->curr.type = TOK_NOPE; + p->parser = parser; +} + +static int +tree_parse_next_token(struct tree_parse *p) +{ + int ret; + + SPHO_PRECOND(p->curr.type > TOK_EOF); + + 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 + + if (ret <= 0) + memset(&p->curr, 0, sizeof(p->curr)); + if (ret < 0) + p->curr.type = TOK_INVAL; + + 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 = calloc(1, sizeof(*unit))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + TREE(unit)->type = MSPH_TREE_UNIT; + TREE(unit)->parent = parent; + DECOR_INIT(unit); + 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; + } + + tree_parse_next_token(p); + + if ((unit->body = tree_parse_body(p, TREE(unit))) == NULL) + goto err; + + return (unit); + +err: + free_the_tree(TREE(unit)); + + return (NULL); +} + +static struct msph_tree_body * +tree_parse_body(struct tree_parse *p, struct msph_tree *parent) +{ + struct msph_tree_dir *dir; + struct msph_tree_body *body; + + if ((body = calloc(1, sizeof(*body))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + TREE(body)->type = MSPH_TREE_BODY; + TREE(body)->parent = parent; + STAILQ_INIT(&body->head); + DECOR_INIT(body); + + while (1) { + dir = NULL; + + switch(CURR_TOKEN(p)->type) { + case TOK_KW_TYPE: + dir = tree_parse_tpdef(p, TREE(body)); + break; + case TOK_KW_NOMINAL: + dir = tree_parse_nomindecl(p, TREE(body)); + break; + case TOK_KW_MEMBER: + dir = tree_parse_membdecl(p, TREE(body)); + break; + case TOK_KW_ASSERT: + dir = tree_parse_assert(p, TREE(body)); + break; + default: + break; + } + + if (dir == NULL) + break; + + STAILQ_INSERT_TAIL(&body->head, dir, entries); + } + + return (body); +} + + + +struct msph_tree_dir * +tree_parse_tpdef(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_tpdef *def; + struct msph_tree_namedecl *name; + + EXPECT_CURR_TOKEN(p, TOK_KW_TYPE, MSPH_TREE_TPDEF, return (NULL)); + + if ((def = calloc(1, sizeof(*def))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + TREE(def)->type = MSPH_TREE_TPDEF; + TREE(def)->parent = parent; + TEXT(def)->pos = CURR_TOKEN(p)->pos; + STAILQ_INIT(&def->params); + DECOR_INIT(def); + + EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err); + if ((def->name = tree_parse_namedecl(p, TREE(def))) == NULL) + goto err; + + if (CURR_TOKEN(p)->type == TOK_LBRAK) { + do { + EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err); + name = tree_parse_namedecl(p, TREE(def)); + if (name == NULL) + goto err; + STAILQ_INSERT_TAIL(&def->params, name, entries); + + EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err); + } while (CURR_TOKEN(p)->type == TOK_COMMA); + + EXPECT_CURR_TOKEN(p, TOK_RBRAK, 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, TREE(def))) == NULL) + goto err; + + return ((struct msph_tree_dir *)def); +err: + free_the_tree(TREE(def)); + return (NULL); +} + +struct msph_tree_namedecl * +tree_parse_namedecl(struct tree_parse *p, struct msph_tree *parent) +{ + struct msph_tree_namedecl *name; + + EXPECT_CURR_TOKEN(p, TOK_IDENT, MSPH_TREE_NAMEDECL, return (NULL)); + + name = (struct msph_tree_namedecl *)tree_parse_ident_extsize(p, parent, + sizeof(*name)); + if (name == NULL) + return (NULL); + + SPHO_ASSERT(TREE(name)->type == MSPH_TREE_IDENT); + TREE(name)->type = MSPH_TREE_NAMEDECL; + + return (name); +} + +struct msph_tree_nameref * +tree_parse_nameref(struct tree_parse *p, struct msph_tree *parent) +{ + struct msph_tree_nameref *name; + + EXPECT_CURR_TOKEN(p, TOK_IDENT, MSPH_TREE_NAMEREF, return (NULL)); + + name = (struct msph_tree_nameref *)tree_parse_ident_extsize(p, parent, + sizeof(*name)); + if (name == NULL) + return (NULL); + + SPHO_ASSERT(TREE(name)->type == MSPH_TREE_IDENT); + TREE(name)->type = MSPH_TREE_NAMEREF; + + return (name); +} + +struct msph_tree_ident * +tree_parse_ident_extsize(struct tree_parse *p, struct msph_tree *parent, + size_t size) +{ + struct msph_tree_ident *id; + SPHO_PRECOND(size >= sizeof(struct msph_tree_ident)); + + EXPECT_CURR_TOKEN(p, TOK_IDENT, MSPH_TREE_IDENT, return (NULL)); + + if ((id = calloc(1, size)) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + TREE(id)->type = MSPH_TREE_IDENT; + TREE(id)->parent = parent; + TEXT(id)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(id); + + 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; + } + + tree_parse_next_token(p); + + return (id); +err: + free_the_tree(TREE(id)); + return (NULL); +} + +struct msph_tree_tpexpr * +tree_parse_tpexpr(struct tree_parse *p, struct msph_tree *parent) +{ + switch (p->parser) { + case MSPH_PARSE_INFIX: + return (tree_parse_tpexpr_infix(p, parent)); + case MSPH_PARSE_PREFIX: + return (tree_parse_tpexpr_prefix(p, parent)); + default: + SPHO_RIP("impossible-invalid-parser"); + return (NULL); + } + +} + +struct msph_tree_tpexpr * +tree_parse_tpexpr_prefix(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_prefix(p, parent); + break; + case TOK_PIPE: + tp = tree_parse_disj_prefix(p, parent); + break; + case TOK_IMPL: + tp = tree_parse_impl_prefix(p, parent); + break; + case TOK_SUB: + tp = tree_parse_subt_prefix(p, parent); + break; + case TOK_RARROW: + tp = tree_parse_arrow_prefix(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_tpname_or_tpappl(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; + } + + SPHO_DEBUG_PRINT("returning tp type=%x\n", TREE(tp)->type); + return (tp); +} + +struct msph_tree_tpexpr * +tree_parse_conj_prefix(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 = calloc(1, sizeof(*conj))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + TREE(conj)->type = MSPH_TREE_CONJ; + TREE(conj)->parent = parent; + TEXT(conj)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(conj); + conj->ltp = NULL; + conj->rtp = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_CONJ, goto err); + if ((conj->ltp = tree_parse_tpexpr_prefix(p, TREE(conj))) + == NULL) + goto err; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_CONJ, goto err); + if ((conj->rtp = tree_parse_tpexpr_prefix(p, TREE(conj))) + == NULL) + goto err; + + return ((struct msph_tree_tpexpr *)conj); +err: + free_the_tree((struct msph_tree *)conj); + + return (NULL); +} + +struct msph_tree_tpexpr * +tree_parse_disj_prefix(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 = calloc(1, sizeof(*disj))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + TREE(disj)->type = MSPH_TREE_DISJ; + TREE(disj)->parent = parent; + TEXT(disj)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(disj); + disj->ltp = NULL; + disj->rtp = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_DISJ, goto err); + if ((disj->ltp = tree_parse_tpexpr_prefix(p, (struct msph_tree *)disj)) + == NULL) + goto err; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_DISJ, goto err); + if ((disj->rtp = tree_parse_tpexpr_prefix(p, (struct msph_tree *)disj)) + == NULL) + goto err; + + return ((struct msph_tree_tpexpr *)disj); +err: + free_the_tree((struct msph_tree *)disj); + + return (NULL); +} + +struct msph_tree_tpexpr * +tree_parse_impl_prefix(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_impl *impl; + + EXPECT_CURR_TOKEN(p, TOK_IMPL, MSPH_TREE_IMPL, return (NULL)); + + if ((impl = calloc(1, sizeof(*impl))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + TREE(impl)->type = MSPH_TREE_IMPL; + TREE(impl)->parent = parent; + TEXT(impl)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(impl); + impl->ltp = NULL; + impl->rtp = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_IMPL, goto err); + if ((impl->ltp = tree_parse_tpexpr_prefix(p, (struct msph_tree *)impl)) + == NULL) + goto err; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_IMPL, goto err); + if ((impl->rtp = tree_parse_tpexpr_prefix(p, (struct msph_tree *)impl)) + == NULL) + goto err; + + return ((struct msph_tree_tpexpr *)impl); +err: + free_the_tree((struct msph_tree *)impl); + + return (NULL); +} + +struct msph_tree_tpexpr * +tree_parse_subt_prefix(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_subt *subt; + + EXPECT_CURR_TOKEN(p, TOK_SUB, MSPH_TREE_SUBT, return (NULL)); + + if ((subt = calloc(1, sizeof(*subt))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + TREE(subt)->type = MSPH_TREE_SUBT; + TREE(subt)->parent = parent; + TEXT(subt)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(subt); + subt->ltp = NULL; + subt->rtp = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_SUBT, goto err); + if ((subt->ltp = tree_parse_tpexpr_prefix(p, (struct msph_tree *)subt)) + == NULL) + goto err; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_SUBT, goto err); + if ((subt->rtp = tree_parse_tpexpr_prefix(p, (struct msph_tree *)subt)) + == NULL) + goto err; + + return ((struct msph_tree_tpexpr *)subt); +err: + free_the_tree((struct msph_tree *)subt); + + return (NULL); +} + +struct msph_tree_tpexpr * +tree_parse_arrow_prefix(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_arrow *arrow; + + EXPECT_CURR_TOKEN(p, TOK_RARROW, MSPH_TREE_ARROW, return (NULL)); + + if ((arrow = calloc(1, sizeof(*arrow))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + TREE(arrow)->type = MSPH_TREE_ARROW; + TREE(arrow)->parent = parent; + TEXT(arrow)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(arrow); + arrow->ltp = NULL; + arrow->rtp = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_ARROW, goto err); + if ((arrow->ltp = tree_parse_tpexpr_prefix(p, (struct msph_tree *)arrow)) + == NULL) + goto err; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_ARROW, goto err); + if ((arrow->rtp = tree_parse_tpexpr_prefix(p, (struct msph_tree *)arrow)) + == NULL) + goto err; + + return ((struct msph_tree_tpexpr *)arrow); +err: + free_the_tree((struct msph_tree *)arrow); + + return (NULL); +} + +static struct msph_tree_tpexpr * +tree_parse_tpexpr_infix(struct tree_parse *p, struct msph_tree *parent) +{ + return (tree_parse_impl_infix(p, parent)); +} + +/* + * infix type algebraics parsing. + * + * In reverse order of precedence (later means higher precedence): + * [op _ associativity] + * - impl _ right + * - subt - right + * - disj _ left (both) + * - conj _ left (both) + * - arrow _ right + * + * + */ +static struct msph_tree_tpexpr * +tree_parse_impl_infix(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_tpexpr *left, *right; + struct msph_tree_impl *impl; + struct msph_text_pos infix_pos; + + impl = NULL; + left = right = NULL; + + if ((left = tree_parse_subt_infix(p, NULL)) == NULL) { + return (NULL); + } + + if (CURR_TOKEN(p)->type != TOK_IMPL) { + TREE(left)->parent = parent; + return (left); + } + infix_pos = CURR_TOKEN(p)->pos; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_IMPL, goto err); + + if ((right = tree_parse_impl_infix(p, NULL)) == NULL) + goto err; + + if ((impl = calloc(1, sizeof(*impl))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + goto err; + } + + TREE(impl)->type = MSPH_TREE_IMPL; + TREE(impl)->parent = parent; + TEXT(impl)->pos = infix_pos; + DECOR_INIT(impl); + + impl->ltp = left; + TREE(left)->parent = TREE(impl); + + impl->rtp = right; + TREE(right)->parent = TREE(impl); + + return ((struct msph_tree_tpexpr *)impl); +err: + if (left != NULL) + free_the_tree(TREE(left)); + if (right != NULL) + free_the_tree(TREE(right)); + return (NULL); +} + +static struct msph_tree_tpexpr * +tree_parse_subt_infix(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_tpexpr *left, *right; + struct msph_tree_subt *subt; + struct msph_text_pos infix_pos; + + subt = NULL; + left = right = NULL; + + if ((left = tree_parse_disj_infix(p, NULL)) == NULL) { + return (NULL); + } + + if (CURR_TOKEN(p)->type != TOK_SUB) { + TREE(left)->parent = parent; + return (left); + } + infix_pos = CURR_TOKEN(p)->pos; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_SUBT, goto err); + + if ((right = tree_parse_subt_infix(p, NULL)) == NULL) + goto err; + + if ((subt = calloc(1, sizeof(*subt))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + goto err; + } + + TREE(subt)->type = MSPH_TREE_SUBT; + TREE(subt)->parent = parent; + TEXT(subt)->pos = infix_pos; + DECOR_INIT(subt); + + subt->ltp = left; + TREE(left)->parent = TREE(subt); + + subt->rtp = right; + TREE(right)->parent = TREE(subt); + + return ((struct msph_tree_tpexpr *)subt); +err: + if (left != NULL) + free_the_tree(TREE(left)); + if (right != NULL) + free_the_tree(TREE(right)); + return (NULL); +} + +static struct msph_tree_tpexpr * +tree_parse_disj_infix(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_tpexpr *left, *right; + struct msph_tree_disj *disj; + struct msph_text_pos infix_pos; + + left = right = NULL; + disj = NULL; + + if ((left = tree_parse_conj_infix(p, NULL)) == NULL) + return (NULL); + + TREE(left)->parent = parent; + + while (CURR_TOKEN(p)->type == TOK_PIPE) { + infix_pos = CURR_TOKEN(p)->pos; + EXPECT_READ_NEXT(res, p, MSPH_TREE_DISJ, goto err); + + if ((right = tree_parse_conj_infix(p, NULL)) == NULL) + goto err; + + if ((disj = calloc(1, sizeof(*disj))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + goto err; + } + + TREE(disj)->type = MSPH_TREE_DISJ; + TREE(disj)->parent = parent; + TEXT(disj)->pos = infix_pos; + DECOR_INIT(disj); + + disj->ltp = left; + TREE(left)->parent = TREE(disj); + disj->rtp = right; + TREE(right)->parent = TREE(disj); + + left = (struct msph_tree_tpexpr *)disj; + right = NULL; + } + + SPHO_POSTCOND(TREE(left)->parent == parent); + + return (left); +err: + if (right != NULL) + free_the_tree(TREE(right)); + + free_the_tree(TREE(left)); + return (NULL); +} + +static struct msph_tree_tpexpr * +tree_parse_conj_infix(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_tpexpr *left, *right; + struct msph_tree_conj *conj; + struct msph_text_pos infix_pos; + + left = right = NULL; + conj = NULL; + + if ((left = tree_parse_arrow_infix(p, NULL)) == NULL) + return (NULL); + + TREE(left)->parent = parent; + + while (CURR_TOKEN(p)->type == TOK_AMP) { + infix_pos = CURR_TOKEN(p)->pos; + EXPECT_READ_NEXT(res, p, MSPH_TREE_CONJ, goto err); + + if ((right = tree_parse_arrow_infix(p, NULL)) == NULL) + goto err; + + if ((conj = calloc(1, sizeof(*conj))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + goto err; + } + + TREE(conj)->type = MSPH_TREE_CONJ; + TREE(conj)->parent = parent; + TEXT(conj)->pos = infix_pos; + DECOR_INIT(conj); + + conj->ltp = left; + TREE(left)->parent = TREE(conj); + conj->rtp = right; + TREE(right)->parent = TREE(conj); + + left = (struct msph_tree_tpexpr *)conj; + right = NULL; + } + + SPHO_POSTCOND(TREE(left)->parent == parent); + + return (left); +err: + if (right != NULL) + free_the_tree(TREE(right)); + + free_the_tree(TREE(left)); + return (NULL); +} +static struct msph_tree_tpexpr * +tree_parse_arrow_infix(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_tpexpr *left, *right; + struct msph_tree_arrow *arrow; + struct msph_text_pos infix_pos; + + arrow = NULL; + left = right = NULL; + + if ((left = tree_parse_tpexpr_atom(p, NULL)) == NULL) { + return (NULL); + } + + if (CURR_TOKEN(p)->type != TOK_RARROW) { + TREE(left)->parent = parent; + return (left); + } + infix_pos = CURR_TOKEN(p)->pos; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_ARROW, goto err); + + if ((right = tree_parse_arrow_infix(p, NULL)) == NULL) + goto err; + + if ((arrow = calloc(1, sizeof(*arrow))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + goto err; + } + + TREE(arrow)->type = MSPH_TREE_ARROW; + TREE(arrow)->parent = parent; + TEXT(arrow)->pos = infix_pos; + DECOR_INIT(arrow); + + arrow->ltp = left; + TREE(left)->parent = TREE(arrow); + + arrow->rtp = right; + TREE(right)->parent = TREE(arrow); + + return ((struct msph_tree_tpexpr *)arrow); +err: + if (left != NULL) + free_the_tree(TREE(left)); + if (right != NULL) + free_the_tree(TREE(right)); + return (NULL); +} + + +struct msph_tree_tpexpr * +tree_parse_tpexpr_atom(struct tree_parse *p, struct msph_tree *parent) +{ + struct msph_tree_tpexpr *tp; + + switch (CURR_TOKEN(p)->type) { + 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_tpname_or_tpappl(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; + } + + SPHO_DEBUG_PRINT("returning tp type=%x\n", TREE(tp)->type); + return (tp); +} +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 = calloc(1, sizeof(*box))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + TREE(box)->type = MSPH_TREE_BOX; + TREE(box)->parent = parent; + TEXT(box)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(box); + box->inner = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_BOX, goto err); + if ((box->inner = tree_parse_tpexpr(p, TREE(box))) == NULL) + goto err; + + return ((struct msph_tree_tpexpr *)box); +err: + free_the_tree(TREE(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 = calloc(1, sizeof(*fa))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + TREE(fa)->type = MSPH_TREE_FORALL; + TREE(fa)->parent = parent; + TEXT(fa)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(fa); + fa->name = NULL; + fa->inner = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_FORALL, goto err); + if ((fa->name = tree_parse_namedecl(p, TREE(fa))) == NULL) + goto err; + + EXPECT_READ_NEXT(res, p, 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, TREE(fa))) == NULL) + goto err; + + return ((struct msph_tree_tpexpr *)fa); +err: + free_the_tree(TREE(fa)); + return (NULL); +} + +/* parse name or appl */ +struct msph_tree_tpexpr * +tree_parse_tpname_or_tpappl(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_tpname *tpname; + struct msph_tree_tpexpr *ret; + struct msph_tree_nameref *nameref; + + ret = NULL; + nameref = NULL; + + if ((nameref = tree_parse_nameref(p, NULL)) == NULL) + return (NULL); + + if (CURR_TOKEN(p)->type == TOK_LBRAK) { + EXPECT_READ_NEXT(res, p, MSPH_TREE_TPAPPL, goto err); + if ((ret = tree_parse_tpapplargs(p, nameref, parent)) == NULL) + goto err; + return (ret); + } + + if ((tpname = calloc(1, sizeof(*tpname))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + goto err; + } + TREE(tpname)->type = MSPH_TREE_TPNAME; + TREE(tpname)->parent = parent; + + TEXT(tpname)->pos = TEXT(nameref)->pos; + DECOR_INIT(tpname); + TREE(nameref)->parent = TREE(tpname); + tpname->name = nameref; + + return ((struct msph_tree_tpexpr *)tpname); +err: + free_the_tree(TREE(nameref)); + + 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_tpapplargs(struct tree_parse *p, struct msph_tree_nameref *name, + struct msph_tree *parent) +{ + int res; + struct msph_tree_tpappl *tpappl; + struct msph_tree_tpexpr *tp; + + tp = NULL; + + EXPECT_CURR_TOKEN(p, TOK_LBRAK, MSPH_TREE_TPAPPL, return (NULL)); + + if ((tpappl = calloc(1, sizeof(*tpappl))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + TREE(tpappl)->type = MSPH_TREE_TPAPPL; + TREE(tpappl)->parent = parent; + DECOR_INIT(tpappl); + tpappl->name = NULL; + STAILQ_INIT(&tpappl->args); + + EXPECT_READ_NEXT(res, p, MSPH_TREE_TPAPPL, goto err); + + if ((tp = tree_parse_tpexpr(p, TREE(tpappl))) == NULL) + goto err; + + /* more arguments */ + while (CURR_TOKEN(p)->type == TOK_COMMA) { + + EXPECT_READ_NEXT(res, p, MSPH_TREE_TPAPPL, goto err); + if ((tp = tree_parse_tpexpr(p, TREE(tpappl))) == NULL) + goto err; + + STAILQ_INSERT_TAIL(&tpappl->args, tp, entries); + } + + EXPECT_CURR_TOKEN(p, TOK_RBRAK, MSPH_TREE_TPAPPL, goto err); + + /* finally, appl takes ownership of id */ + TREE(name)->parent = TREE(tpappl); + tpappl->name = name; + TEXT(tpappl)->pos = TEXT(name)->pos; + + tree_parse_next_token(p); + + return ((struct msph_tree_tpexpr *)tpappl); +err: + free_the_tree(TREE(tpappl)); + + 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 = calloc(1, sizeof(*t))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + TREE(t)->type = MSPH_TREE_TRUE; + TREE(t)->parent = parent; + TEXT(t)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(t); + + tree_parse_next_token(p); + + 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 = calloc(1, sizeof(*f))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + TREE(f)->type = MSPH_TREE_FALSE; + TREE(f)->parent = parent; + TEXT(f)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(f); + + tree_parse_next_token(p); + + 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 = calloc(1, sizeof(*par))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + TREE(par)->type = MSPH_TREE_PAREN; + TREE(par)->parent = parent; + TEXT(par)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(par); + par->inner = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_PAREN, goto err); + + if ((par->inner = tree_parse_tpexpr(p, TREE(par))) == NULL) + goto err; + + EXPECT_CURR_TOKEN(p, TOK_RPAREN, MSPH_TREE_PAREN, goto err); + + tree_parse_next_token(p); + + return ((struct msph_tree_tpexpr *)par); +err: + free_the_tree(TREE(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 = calloc(1, sizeof(*trait))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + TREE(trait)->type = MSPH_TREE_TRAIT; + TREE(trait)->parent = parent; + TEXT(trait)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(trait); + trait->body = NULL; + + if ((trait->body = tree_parse_body(p, TREE(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(TREE(trait)); + + return (NULL); +} + +struct msph_tree_dir * +tree_parse_nomindecl(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_namedecl *name; + struct msph_tree_nomindecl *nomind; + + EXPECT_CURR_TOKEN(p, TOK_KW_NOMINAL, MSPH_TREE_NOMINDECL, + return (NULL)); + + if ((nomind = calloc(1, sizeof(*nomind))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + TREE(nomind)->type = MSPH_TREE_NOMINDECL; + TREE(nomind)->parent = parent; + TEXT(nomind)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(nomind); + nomind->name = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_NOMINDECL, goto err); + if ((name = tree_parse_namedecl(p, TREE(nomind))) == NULL) + goto err; + + nomind->name = name; + + return ((struct msph_tree_dir *)nomind); +err: + free_the_tree(TREE(nomind)); + + 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)); + + if ((membd = calloc(1, sizeof(*membd))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + TREE(membd)->type = MSPH_TREE_MEMBDECL; + TREE(membd)->parent = parent; + TEXT(membd)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(membd); + membd->name = NULL; + membd->tp = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_MEMBDECL, goto err); + if ((membd->name = tree_parse_namedecl(p, TREE(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, TREE(membd))) == NULL) + goto err; + + return ((struct msph_tree_dir *)membd); +err: + free_the_tree(TREE(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)); + + if ((ass = calloc(1, sizeof(*ass))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + TREE(ass)->type = MSPH_TREE_ASSERT; + TREE(ass)->parent = parent; + TEXT(ass)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(ass); + ass->tp = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_ASSERT, goto err); + if ((ass->tp = tree_parse_tpexpr(p, TREE(ass))) == NULL) + goto err; + + return ((struct msph_tree_dir *)ass); +err: + free_the_tree(TREE(ass)); + + return (NULL); +} + +static void +free_the_tree(struct msph_tree *tree) +{ + /* will anyone ever free the tree? :´( */ + SPHO_POSTCOND((void *)tree != (void *)free); + // SPHO_POSTCOND(0); +} + #define MSPH_TREE_INDENT " " __attribute__((format(printf, 3, 4))) @@ -213,6 +1421,7 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) struct msph_tree_conj *conj; struct msph_tree_disj *disj; struct msph_tree_impl *impl; + struct msph_tree_subt *subt; struct msph_tree_arrow *arrow; struct msph_tree_box *box; struct msph_tree_forall *forall; @@ -222,6 +1431,7 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) struct msph_tree_paren *paren; struct msph_tree_ident *ident; struct msph_tree_tpexpr *tp; + const char *ident_kind; ret = 0; switch (TREE_ID(tree)) { @@ -231,8 +1441,9 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) return (res); STAILQ_FOREACH(unit, &root->head, entries) { if ((res = tree_ind_fprint(f, indent+1, TREE(unit))) - < 0) + < 0) { return (res); + } ret += res; } if ((res = indent_fprintf(f, indent, ")\n")) < 0) @@ -241,8 +1452,9 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) case MSPH_TREE_UNIT: unit = (struct msph_tree_unit *)tree; if ((res = indent_fprintf(f, indent, "(unit:%s\n", unit->name)) - < 0) + < 0) { return (res); + } ret += res; if ((res = tree_ind_fprint(f, indent+1, TREE(unit->body))) < 0) return (res); @@ -258,8 +1470,9 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) ret += res; STAILQ_FOREACH(dir, &body->head, entries) { if ((res = tree_ind_fprint(f, indent+1, TREE(dir))) - < 0) + < 0) { return (res); + } ret += res; } if ((res = indent_fprintf(f, indent, ")\n")) < 0) @@ -269,8 +1482,9 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) case MSPH_TREE_NOMINDECL: nomd = (struct msph_tree_nomindecl *)tree; if ((res = indent_fprintf(f, indent, "(nomindecl:%u,%u\n", - TEXT(nomd)->pos.line, TEXT(nomd)->pos.col)) < 0) + TEXT(nomd)->pos.line, TEXT(nomd)->pos.col)) < 0) { return (res); + } ret += res; if ((res = tree_ind_fprint(f, indent+1, TREE(nomd->name))) < 0) return (res); @@ -282,13 +1496,11 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) case MSPH_TREE_ASSERT: ass = (struct msph_tree_assert *)tree; if ((res = indent_fprintf(f, indent, "(assert:%u,%u\n", - TEXT(ass)->pos.line, TEXT(ass)->pos.col)) < 0) + TEXT(ass)->pos.line, TEXT(ass)->pos.col)) < 0) { return (res); + } ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(ass->ltp))) < 0) - return (res); - ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(ass->rtp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(ass->tp))) < 0) return (res); ret += res; if ((res = indent_fprintf(f, indent, ")\n")) < 0) @@ -298,11 +1510,14 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) case MSPH_TREE_TPDEF: tpdef = (struct msph_tree_tpdef *)tree; if ((res = indent_fprintf(f, indent, "(tpdef:%u,%u\n", - TEXT(tpdef)->pos.line, TEXT(tpdef)->pos.col)) < 0) + TEXT(tpdef)->pos.line, TEXT(tpdef)->pos.col)) < 0) { return (res); + } ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(tpdef->name))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(tpdef->name))) + < 0) { return (res); + } ret += res; if ((res = tree_ind_fprint(f, indent+1, TREE(tpdef->tp))) < 0) return (res); @@ -334,9 +1549,10 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) break; case MSPH_TREE_CONJ: conj = (struct msph_tree_conj *)tree; - if ((res = indent_fprintf(f, indent, "(conj:%u,%u\n", - TEXT(conj)->pos.line, TEXT(conj)->pos.col)) < 0) + if ((res = indent_fprintf(f, indent, "(&conj:%u,%u\n", + TEXT(conj)->pos.line, TEXT(conj)->pos.col)) < 0) { return (res); + } ret += res; if ((res = tree_ind_fprint(f, indent+1, TREE(conj->ltp))) < 0) return (res); @@ -350,9 +1566,10 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) break; case MSPH_TREE_DISJ: disj = (struct msph_tree_disj *)tree; - if ((res = indent_fprintf(f, indent, "(disj:%u,%u\n", - TEXT(disj)->pos.line, TEXT(disj)->pos.col)) < 0) + if ((res = indent_fprintf(f, indent, "(|disj:%u,%u\n", + TEXT(disj)->pos.line, TEXT(disj)->pos.col)) < 0) { return (res); + } ret += res; if ((res = tree_ind_fprint(f, indent+1, TREE(disj->ltp))) < 0) return (res); @@ -366,9 +1583,10 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) break; case MSPH_TREE_IMPL: impl = (struct msph_tree_impl *)tree; - if ((res = indent_fprintf(f, indent, "(impl:%u,%u\n", - TEXT(impl)->pos.line, TEXT(impl)->pos.col)) < 0) + if ((res = indent_fprintf(f, indent, "(=>impl:%u,%u\n", + TEXT(impl)->pos.line, TEXT(impl)->pos.col)) < 0) { return (res); + } ret += res; if ((res = tree_ind_fprint(f, indent+1, TREE(impl->ltp))) < 0) return (res); @@ -380,11 +1598,29 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) return (res); ret += res; break; + case MSPH_TREE_SUBT: + subt = (struct msph_tree_subt *)tree; + if ((res = indent_fprintf(f, indent, "(<:subt:%u,%u\n", + TEXT(subt)->pos.line, TEXT(subt)->pos.col)) < 0) { + return (res); + } + ret += res; + if ((res = tree_ind_fprint(f, indent+1, TREE(subt->ltp))) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, TREE(subt->rtp))) < 0) + return (res); + ret += res; + if ((res = indent_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; case MSPH_TREE_ARROW: arrow = (struct msph_tree_arrow *)tree; - if ((res = indent_fprintf(f, indent, "(arrow:%u,%u\n", - TEXT(arrow)->pos.line, TEXT(arrow)->pos.col)) < 0) + if ((res = indent_fprintf(f, indent, "(->arrow:%u,%u\n", + TEXT(arrow)->pos.line, TEXT(arrow)->pos.col)) < 0) { return (res); + } ret += res; if ((res = tree_ind_fprint(f, indent+1, TREE(arrow->ltp))) < 0) return (res); @@ -399,8 +1635,9 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) case MSPH_TREE_BOX: box = (struct msph_tree_box *)tree; if ((res = indent_fprintf(f, indent, "(box:%u,%u\n", - TEXT(box)->pos.line, TEXT(box)->pos.col)) < 0) + TEXT(box)->pos.line, TEXT(box)->pos.col)) < 0) { return (res); + } ret += res; if ((res = tree_ind_fprint(f, indent+1, TREE(box->inner))) < 0) return (res); @@ -412,8 +1649,9 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) case MSPH_TREE_FORALL: forall = (struct msph_tree_forall *)tree; if ((res = indent_fprintf(f, indent, "(forall:%u,%u\n", - TEXT(forall)->pos.line, TEXT(forall)->pos.col)) < 0) + TEXT(forall)->pos.line, TEXT(forall)->pos.col)) < 0) { return (res); + } ret += res; if ((res = tree_ind_fprint(f, indent+1, TREE(forall->name))) < 0) @@ -431,8 +1669,9 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) case MSPH_TREE_PAREN: paren = (struct msph_tree_paren *)tree; if ((res = indent_fprintf(f, indent, "(paren:%u,%u\n", - TEXT(paren)->pos.line, TEXT(paren)->pos.col)) < 0) + TEXT(paren)->pos.line, TEXT(paren)->pos.col)) < 0) { return (res); + } ret += res; if ((res = tree_ind_fprint(f, indent+1, TREE(paren->inner))) < 0) { @@ -449,12 +1688,16 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) TEXT(tpappl)->pos.line, TEXT(tpappl)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(tpappl->name))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(tpappl->name))) + < 0) { return (res); + } ret += res; STAILQ_FOREACH(tp, &tpappl->args, entries) { - if ((res = tree_ind_fprint(f, indent+1, TREE(tp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(tp))) + < 0) { return (res); + } ret += res; } if ((res = indent_fprintf(f, indent, ")\n")) < 0) @@ -464,8 +1707,9 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) case MSPH_TREE_TPNAME: name = (struct msph_tree_tpname *)tree; if ((res = indent_fprintf(f, indent, "(name:%u,%u\n", - TEXT(name)->pos.line, TEXT(name)->pos.col)) < 0) + TEXT(name)->pos.line, TEXT(name)->pos.col)) < 0) { return (res); + } ret += res; if ((res = tree_ind_fprint(f, indent+1, TREE(name->name))) < 0) return (res); @@ -492,23 +1736,36 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) case MSPH_TREE_NAMEDECL: case MSPH_TREE_NAMEREF: case MSPH_TREE_IDENT: + switch (TREE_ID(tree)) { + case MSPH_TREE_NAMEDECL: + ident_kind = "/namedecl"; + break; + case MSPH_TREE_NAMEREF: + ident_kind = "/nameref"; + break; + default: + ident_kind = ""; + } ident = IDENT(tree); - if ((res = indent_fprintf(f, indent, "(ident:%u,%u:%s)\n", - TEXT(ident)->pos.line, TEXT(ident)->pos.col, ident->str)) - < 0) + if ((res = indent_fprintf(f, indent, "(ident%s:%u,%u:%s)\n", + ident_kind, TEXT(ident)->pos.line, TEXT(ident)->pos.col, + ident->str)) < 0) { return (res); + } ret += res; break; case MSPH_TREE_TRUE: if ((res = indent_fprintf(f, indent, "(true:%u,%u)\n", - TEXT(tree)->pos.line, TEXT(tree)->pos.col)) < 0) + TEXT(tree)->pos.line, TEXT(tree)->pos.col)) < 0) { return (res); + } ret += res; break; case MSPH_TREE_FALSE: if ((res = indent_fprintf(f, indent, "(false:%u,%u)\n", - TEXT(tree)->pos.line, TEXT(tree)->pos.col)) < 0) + TEXT(tree)->pos.line, TEXT(tree)->pos.col)) < 0) { return (res); + } ret += res; break; default: @@ -518,852 +1775,3 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) return (ret); } - -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); -} - -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); - } - TREE(unit)->type = MSPH_TREE_UNIT; - TREE(unit)->parent = parent; - DECOR_INIT(unit); - 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, TREE(unit))) == NULL) - goto err; - - return (unit); - -err: - free_the_tree(TREE(unit)); - - return (NULL); -} - -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); - } - TREE(body)->type = MSPH_TREE_BODY; - TREE(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: - SPHO_DEBUG_PRINT("parsing tpdef\n"); - dir = tree_parse_tpdef(p, TREE(body)); - break; - case TOK_KW_NOMINAL: - dir = tree_parse_nomindecl(p, TREE(body)); - break; - case TOK_KW_MEMBER: - dir = tree_parse_membdecl(p, TREE(body)); - break; - case TOK_KW_ASSERT: - dir = tree_parse_assert(p, TREE(body)); - break; - default: - if ((tok = msph_token_copy(CTX(p), CURR_TOKEN(p))) - == NULL) - goto err; - tree_parse_push_token(p, tok); - goto ret; - } - - if (dir == NULL) - goto err; - - STAILQ_INSERT_TAIL(&body->head, dir, entries); - } - - if (res == -1) - goto err; -ret: - return (body); -err: - free_the_tree(TREE(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; - struct msph_tree_namedecl *name; - - 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); - } - TREE(def)->type = MSPH_TREE_TPDEF; - TREE(def)->parent = parent; - TEXT(def)->pos = CURR_TOKEN(p)->pos; - STAILQ_INIT(&def->params); - DECOR_INIT(def); - - EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err); - if ((def->name = tree_parse_namedecl(p, TREE(def))) == NULL) - goto err; - - EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err); - - if (CURR_TOKEN(p)->type == TOK_LBRAK) { - ADD_FLAG(TREE(def), MSPH_TREE_FLAG_SCOPE); - - do { - EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err); - name = tree_parse_namedecl(p, TREE(def)); - if (name == NULL) - goto err; - STAILQ_INSERT_TAIL(&def->params, name, entries); - - EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err); - } while (CURR_TOKEN(p)->type == TOK_COMMA); - - EXPECT_CURR_TOKEN(p, TOK_RBRAK, 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, TREE(def))) == NULL) - goto err; - - return ((struct msph_tree_dir *)def); -err: - free_the_tree(TREE(def)); - return (NULL); -} - -struct msph_tree_namedecl * -tree_parse_namedecl(struct tree_parse *p, struct msph_tree *parent) -{ - struct msph_tree_namedecl *name; - - EXPECT_CURR_TOKEN(p, TOK_IDENT, MSPH_TREE_NAMEDECL, return (NULL)); - - name = (struct msph_tree_namedecl *)tree_parse_ident_extsize(p, parent, - sizeof(*name)); - if (name == NULL) - return (NULL); - - SPHO_ASSERT(TREE(name)->type == MSPH_TREE_IDENT); - TREE(name)->type |= MSPH_TREE_NAMEDECL; - - return (name); -} - -struct msph_tree_nameref * -tree_parse_nameref(struct tree_parse *p, struct msph_tree *parent) -{ - struct msph_tree_nameref *name; - - EXPECT_CURR_TOKEN(p, TOK_IDENT, MSPH_TREE_NAMEREF, return (NULL)); - - name = (struct msph_tree_nameref *)tree_parse_ident_extsize(p, parent, - sizeof(*name)); - if (name == NULL) - return (NULL); - - SPHO_ASSERT(TREE(name)->type == MSPH_TREE_IDENT); - TREE(name)->type |= MSPH_TREE_NAMEREF; - - return (name); -} - -struct msph_tree_ident * -tree_parse_ident_extsize(struct tree_parse *p, struct msph_tree *parent, - size_t size) -{ - struct msph_tree_ident *id; - SPHO_PRECOND(size >= sizeof(struct msph_tree_ident)); - - EXPECT_CURR_TOKEN(p, TOK_IDENT, MSPH_TREE_IDENT, return (NULL)); - - if ((id = malloc(sizeof(size))) == NULL) { - MSPH_ERR(CTX(p), MSPH_ERR_SYS); - return (NULL); - } - TREE(id)->type = MSPH_TREE_IDENT; - TREE(id)->parent = parent; - TEXT(id)->pos = CURR_TOKEN(p)->pos; - DECOR_INIT(id); - - 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(TREE(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_tpname_or_tpappl(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; - } - - SPHO_DEBUG_PRINT("returning tp type=%x\n", TREE(tp)->type); - 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); - } - TREE(conj)->type = MSPH_TREE_CONJ; - TREE(conj)->parent = parent; - TEXT(conj)->pos = CURR_TOKEN(p)->pos; - DECOR_INIT(conj); - conj->ltp = NULL; - conj->rtp = NULL; - - EXPECT_READ_NEXT(res, p, MSPH_TREE_CONJ, goto err); - if ((conj->ltp = tree_parse_tpexpr(p, TREE(conj))) - == NULL) - goto err; - - EXPECT_READ_NEXT(res, p, MSPH_TREE_CONJ, goto err); - if ((conj->rtp = tree_parse_tpexpr(p, TREE(conj))) - == NULL) - goto err; - - return ((struct msph_tree_tpexpr *)conj); -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); - } - TREE(disj)->type = MSPH_TREE_DISJ; - TREE(disj)->parent = parent; - TEXT(disj)->pos = CURR_TOKEN(p)->pos; - DECOR_INIT(disj); - 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; - - 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); - - 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_IMPL, MSPH_TREE_IMPL, return (NULL)); - - if ((impl = malloc(sizeof(*impl))) == NULL) { - MSPH_ERR(CTX(p), MSPH_ERR_SYS); - return (NULL); - } - TREE(impl)->type = MSPH_TREE_IMPL; - TREE(impl)->parent = parent; - TEXT(impl)->pos = CURR_TOKEN(p)->pos; - DECOR_INIT(impl); - 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; - - 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); - - return (NULL); -} - -struct msph_tree_tpexpr * -tree_parse_arrow(struct tree_parse *p, struct msph_tree *parent) -{ - int res; - struct msph_tree_arrow *arrow; - - EXPECT_CURR_TOKEN(p, TOK_RARROW, MSPH_TREE_ARROW, return (NULL)); - - if ((arrow = malloc(sizeof(*arrow))) == NULL) { - MSPH_ERR(CTX(p), MSPH_ERR_SYS); - return (NULL); - } - TREE(arrow)->type = MSPH_TREE_ARROW; - TREE(arrow)->parent = parent; - TEXT(arrow)->pos = CURR_TOKEN(p)->pos; - DECOR_INIT(arrow); - arrow->ltp = NULL; - arrow->rtp = NULL; - - EXPECT_READ_NEXT(res, p, MSPH_TREE_ARROW, goto err); - if ((arrow->ltp = tree_parse_tpexpr(p, (struct msph_tree *)arrow)) - == NULL) - goto err; - - 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 *)arrow); - - 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); - } - TREE(box)->type = MSPH_TREE_BOX; - TREE(box)->parent = parent; - TEXT(box)->pos = CURR_TOKEN(p)->pos; - DECOR_INIT(box); - box->inner = NULL; - - EXPECT_READ_NEXT(res, p, MSPH_TREE_BOX, goto err); - if ((box->inner = tree_parse_tpexpr(p, TREE(box))) == NULL) - goto err; - - return ((struct msph_tree_tpexpr *)box); -err: - free_the_tree(TREE(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); - } - TREE(fa)->type = MSPH_TREE_FORALL; - TREE(fa)->parent = parent; - TEXT(fa)->pos = CURR_TOKEN(p)->pos; - DECOR_INIT(fa); - fa->name = NULL; - fa->inner = NULL; - - EXPECT_READ_NEXT(res, p, MSPH_TREE_FORALL, goto err); - if ((fa->name = tree_parse_namedecl(p, TREE(fa))) == NULL) - goto err; - - EXPECT_READ_NEXT(res, p, 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, TREE(fa))) == NULL) - goto err; - - return ((struct msph_tree_tpexpr *)fa); -err: - free_the_tree(TREE(fa)); - return (NULL); -} - -/* parse name or appl */ -struct msph_tree_tpexpr * -tree_parse_tpname_or_tpappl(struct tree_parse *p, struct msph_tree *parent) -{ - int res; - struct msph_tree_tpname *tpname; - struct msph_tree_tpexpr *ret; - struct msph_tree_nameref *nameref; - struct msph_token *tok; - - ret = NULL; - nameref = NULL; - - if ((nameref = tree_parse_nameref(p, NULL)) == NULL) - return (NULL); - - if ((res = tree_parse_next_token(p)) == 1) { - if (CURR_TOKEN(p)->type == TOK_LBRAK) { - if ((ret = tree_parse_tpapplargs(p, nameref, parent)) - == NULL) - goto err; - return (ret); - } - - if ((tok = msph_token_copy(CTX(p), CURR_TOKEN(p))) - == NULL) { - goto err; - } - tree_parse_push_token(p, tok); - } else if (res == -1) { - goto err; - } - - if ((tpname = malloc(sizeof(*tpname))) == NULL) { - MSPH_ERR(CTX(p), MSPH_ERR_SYS); - goto err; - } - TREE(tpname)->type = MSPH_TREE_TPNAME; - TREE(tpname)->parent = parent; - - TEXT(tpname)->pos = TEXT(nameref)->pos; - DECOR_INIT(tpname); - TREE(nameref)->parent = TREE(tpname); - tpname->name = nameref; - - return ((struct msph_tree_tpexpr *)tpname); -err: - free_the_tree(TREE(nameref)); - - 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_tpapplargs(struct tree_parse *p, struct msph_tree_nameref *name, - struct msph_tree *parent) -{ - int res; - struct msph_tree_tpappl *tpappl; - struct msph_tree_tpexpr *tp; - - tp = NULL; - - EXPECT_CURR_TOKEN(p, TOK_LBRAK, MSPH_TREE_TPAPPL, return (NULL)); - - if ((tpappl = malloc(sizeof(*tpappl))) == NULL) { - MSPH_ERR(CTX(p), MSPH_ERR_SYS); - return (NULL); - } - TREE(tpappl)->type = MSPH_TREE_TPAPPL; - TREE(tpappl)->parent = parent; - DECOR_INIT(tpappl); - tpappl->name = NULL; - STAILQ_INIT(&tpappl->args); - - /* 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 at start of argument list, check for comma to know if - * we should parse another argument */ - if (tp != NULL) { - EXPECT_CURR_TOKEN(p, TOK_COMMA, MSPH_TREE_TPAPPL, - goto err); - EXPECT_READ_NEXT(res, p, MSPH_TREE_TPAPPL, goto err); - } - - if ((tp = tree_parse_tpexpr(p, TREE(tpappl))) == NULL) - goto err; - - STAILQ_INSERT_TAIL(&tpappl->args, tp, entries); - } - - /* SYS_ERROR set in tree_parse_next_token */ - 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_TPAPPL); - goto err; - } - - /* finally, appl takes ownership of id */ - TREE(name)->parent = TREE(tpappl); - tpappl->name = name; - TEXT(tpappl)->pos = TEXT(name)->pos; - - return ((struct msph_tree_tpexpr *)tpappl); -err: - free_the_tree(TREE(tpappl)); - - 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); - } - TREE(t)->type = MSPH_TREE_TRUE; - TREE(t)->parent = parent; - TEXT(t)->pos = CURR_TOKEN(p)->pos; - DECOR_INIT(t); - - 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); - } - TREE(f)->type = MSPH_TREE_FALSE; - TREE(f)->parent = parent; - TEXT(f)->pos = CURR_TOKEN(p)->pos; - DECOR_INIT(f); - - 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); - } - TREE(par)->type = MSPH_TREE_PAREN; - TREE(par)->parent = parent; - TEXT(par)->pos = CURR_TOKEN(p)->pos; - DECOR_INIT(par); - par->inner = NULL; - - EXPECT_READ_NEXT(res, p, MSPH_TREE_PAREN, goto err); - - if ((par->inner = tree_parse_tpexpr(p, TREE(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(TREE(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); - } - TREE(trait)->type = MSPH_TREE_TRAIT; - TREE(trait)->parent = parent; - TEXT(trait)->pos = CURR_TOKEN(p)->pos; - DECOR_INIT(trait); - trait->body = NULL; - - if ((trait->body = tree_parse_body(p, TREE(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(TREE(trait)); - - return (NULL); -} - -struct msph_tree_dir * -tree_parse_nomindecl(struct tree_parse *p, struct msph_tree *parent) -{ - int res; - struct msph_tree_namedecl *name; - struct msph_tree_nomindecl *nomind; - - EXPECT_CURR_TOKEN(p, TOK_KW_NOMINAL, MSPH_TREE_NOMINDECL, - return (NULL)); - - if ((nomind = malloc(sizeof(*nomind))) == NULL) { - MSPH_ERR(CTX(p), MSPH_ERR_SYS); - return (NULL); - } - TREE(nomind)->type = MSPH_TREE_NOMINDECL; - TREE(nomind)->parent = parent; - TEXT(nomind)->pos = CURR_TOKEN(p)->pos; - nomind->name = NULL; - - EXPECT_READ_NEXT(res, p, MSPH_TREE_NOMINDECL, goto err); - if ((name = tree_parse_namedecl(p, TREE(nomind))) == NULL) - goto err; - - nomind->name = name; - - return ((struct msph_tree_dir *)nomind); -err: - free_the_tree(TREE(nomind)); - - 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)); - - if ((membd = malloc(sizeof(*membd))) == NULL) { - MSPH_ERR(CTX(p), MSPH_ERR_SYS); - return (NULL); - } - TREE(membd)->type = MSPH_TREE_MEMBDECL; - TREE(membd)->parent = parent; - TEXT(membd)->pos = CURR_TOKEN(p)->pos; - membd->name = NULL; - membd->tp = NULL; - - EXPECT_READ_NEXT(res, p, MSPH_TREE_MEMBDECL, goto err); - if ((membd->name = tree_parse_namedecl(p, TREE(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, TREE(membd))) == NULL) - goto err; - - return ((struct msph_tree_dir *)membd); -err: - free_the_tree(TREE(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)); - - if ((ass = malloc(sizeof(*ass))) == NULL) { - MSPH_ERR(CTX(p), MSPH_ERR_SYS); - return (NULL); - } - TREE(ass)->type = MSPH_TREE_ASSERT; - TREE(ass)->parent = parent; - TEXT(ass)->pos = CURR_TOKEN(p)->pos; - ass->ltp = NULL; - ass->rtp = NULL; - - EXPECT_READ_NEXT(res, p, MSPH_TREE_ASSERT, goto err); - if ((ass->ltp = tree_parse_tpexpr(p, TREE(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->rtp = tree_parse_tpexpr(p, TREE(ass))) == NULL) - goto err; - - return ((struct msph_tree_dir *)ass); -err: - free_the_tree(TREE(ass)); - - return (NULL); -} - -static void -free_the_tree(struct msph_tree *tree) -{ - /* will anyone ever free the tree? :´( */ - SPHO_POSTCOND((void *)tree != (void *)free); - // SPHO_POSTCOND(0); -} - diff --git a/src/spho/bind.c b/src/spho/bind.c index fc2258b..7bc0d6b 100644 --- a/src/spho/bind.c +++ b/src/spho/bind.c @@ -19,20 +19,21 @@ spho_prebind_create(struct spho_scope *sc) return (NULL); } - if ((bind->binds = calloc(sc->n_noms, sizeof(*bind->binds))) == NULL) { + if ((bind->binds = calloc(sc->nom_cnt, sizeof(*bind->binds))) == NULL) { SPHO_ERR(sc->ctx, SPHO_ERR_SYS); free(bind); return (NULL); } bind->sc = sc; - bind->sz = sc->n_noms; + bind->sz = sc->nom_cnt; i = 0; - SLIST_FOREACH(nom, &sc->noms, next) { + SLIST_FOREACH(nom, &sc->noms, entries) { SPHO_ASSERT(i < bind->sz); - bind->binds[i++] = (struct spho_prebind_pair) { NULL, 0, NULL }; + bind->binds[i++] = + (struct spho_prebind_pair) { nom, 0, { NULL } }; } return (bind); diff --git a/src/spho/ctx.c b/src/spho/ctx.c index cd43288..2b82bd9 100644 --- a/src/spho/ctx.c +++ b/src/spho/ctx.c @@ -37,28 +37,31 @@ spho_ctx_create(void) c = NULL; - if ((c = malloc(sizeof(struct spho_ctx))) == NULL) + if ((c = calloc(1, sizeof(struct spho_ctx))) == NULL) return (NULL); - c->err = 0; - c->err_info = 0; - - if (spho_scope_init(&c->glob, c, NULL) == -1) { - free(c); - return (NULL); - } - - SPHO_POSTCOND(c != NULL); + spho_ctx_init(c); return (c); } +void +spho_ctx_init(struct spho_ctx *ctx) +{ + ctx->err = 0; + ctx->err_info = 0; + + ctx->nom_cnt = 0; + + spho_scope_init(&ctx->glob, ctx, NULL); +} + void spho_ctx_destroy(struct spho_ctx *ctx) { SPHO_PRECOND(ctx != NULL); - spho_scope_term(&ctx->glob); + spho_scope_cleanup(&ctx->glob); free(ctx); } diff --git a/src/spho/scope.c b/src/spho/scope.c index da5c679..40a41a5 100644 --- a/src/spho/scope.c +++ b/src/spho/scope.c @@ -8,41 +8,59 @@ #include "spho/scope.h" #include "spho/bind.h" -static void spho_nom_term(struct spho_nom *); - static int scope_nom_lookup_str_local(struct spho_scope *, const char *, size_t, struct spho_nom **); static int scope_nom_in_local(struct spho_scope *, struct spho_nom *); -int +void spho_scope_init(struct spho_scope *sc, struct spho_ctx *ctx, struct spho_scope *p) { sc->ctx = ctx; sc->parent = p; - SLIST_INIT(&sc->subs); + STAILQ_INIT(&sc->subs); SLIST_INIT(&sc->noms); - sc->n_noms = 0; + sc->nom_cnt = 0; - TAILQ_INIT(&sc->tps); + STAILQ_INIT(&sc->tps); sc->bind_loc = NULL; - - return (0); } void -spho_scope_term(struct spho_scope *sc) +spho_scope_cleanup(struct spho_scope *sc) { - SPHO_UTIL_SLIST_DESTROY(&sc->subs, spho_scope, next, spho_scope_term); + struct spho_scope *sub; + struct spho_nom *nom; + struct spho_tp_alloc *tp_alloc; - SPHO_UTIL_SLIST_DESTROY(&sc->noms, spho_nom, next, spho_nom_term); + /* XXX is doable without recursive call, but cba */ + while (! STAILQ_EMPTY(&sc->subs)) { + sub = STAILQ_FIRST(&sc->subs); + STAILQ_REMOVE_HEAD(&sc->subs, entries); + spho_scope_cleanup(sub); + free(sub); + } + + /* all type structs are allocated from scope */ + while (! STAILQ_EMPTY(&sc->tps)) { + tp_alloc = STAILQ_FIRST(&sc->tps); + STAILQ_REMOVE_HEAD(&sc->tps, entries); + free(tp_alloc); + } + + /* names are allocated in scope too */ + while (! SLIST_EMPTY(&sc->noms)) { + nom = SLIST_FIRST(&sc->noms); + SLIST_REMOVE_HEAD(&sc->noms, entries); + free(nom); + } sc->parent = NULL; - if (sc->bind_loc == NULL) + if (sc->bind_loc != NULL) spho_prebind_free(sc->bind_loc); sc->bind_loc = NULL; } @@ -57,7 +75,7 @@ spho_scope_global(struct spho_ctx *ctx) struct spho_scope * -spho_scope_create(struct spho_scope *sc) +spho_scope_create_subscope(struct spho_scope *sc) { struct spho_scope *sub; @@ -66,35 +84,24 @@ spho_scope_create(struct spho_scope *sc) return (NULL); } - if (spho_scope_init(sub, sc->ctx, sc) == -1) { - free(sub); - return (NULL); - } + spho_scope_init(sub, sc->ctx, sc); - SLIST_INSERT_HEAD(&sc->subs, sub, next); + STAILQ_INSERT_TAIL(&sc->subs, sub, entries); return (sub); } - -static void -spho_nom_term(__attribute__((unused)) struct spho_nom *nom) -{ - return; -} - void -spho_scope_destroy(struct spho_scope *sc) +spho_scope_free(struct spho_scope *sc) { struct spho_scope *p; p = sc->parent; - SLIST_REMOVE(&p->subs, sc, spho_scope, next); - spho_scope_term(sc); + STAILQ_REMOVE(&p->subs, sc, spho_scope, entries); + spho_scope_cleanup(sc); free(sc); } - struct spho_nom * spho_scope_nom_add(struct spho_scope *sc, const char *nomstr, size_t sz) { @@ -122,8 +129,8 @@ spho_scope_nom_add(struct spho_scope *sc, const char *nomstr, size_t sz) goto err; } - SLIST_INSERT_HEAD(&sc->noms, nom, next); - sc->n_noms++; + SLIST_INSERT_HEAD(&sc->noms, nom, entries); + sc->nom_cnt++; return (nom); err: @@ -133,7 +140,7 @@ err: int -spho_scope_nom_lookup_str(struct spho_scope *sc, const char *nomstr, size_t sz, +spho_scope_nom_lookup(struct spho_scope *sc, const char *nomstr, size_t sz, struct spho_nom **out) { struct spho_nom *nom; @@ -147,7 +154,7 @@ spho_scope_nom_lookup_str(struct spho_scope *sc, const char *nomstr, size_t sz, *out = NULL; while (*out == NULL && sc != NULL) { - SLIST_FOREACH(nom, &sc->noms, next) { + SLIST_FOREACH(nom, &sc->noms, entries) { if (strncmp(nom->s, nomstr, sz) == 0) { *out = nom; break; @@ -160,10 +167,10 @@ spho_scope_nom_lookup_str(struct spho_scope *sc, const char *nomstr, size_t sz, } int -spho_scope_nom_lookup_str_strict(struct spho_scope *sc, const char *nomstr, +spho_scope_nom_lookup_strict(struct spho_scope *sc, const char *nomstr, size_t sz, struct spho_nom **out) { - if (spho_scope_nom_lookup_str(sc, nomstr, sz, out) == -1) + if (spho_scope_nom_lookup(sc, nomstr, sz, out) == -1) return (-1); if (*out == NULL) { @@ -177,10 +184,8 @@ spho_scope_nom_lookup_str_strict(struct spho_scope *sc, const char *nomstr, int spho_scope_prebind_init(struct spho_scope *sc) { - if ((sc->bind_loc = spho_prebind_create(sc)) - == NULL) { + if ((sc->bind_loc = spho_prebind_create(sc)) == NULL) return (-1); - } return (0); } @@ -234,7 +239,7 @@ scope_nom_lookup_str_local(struct spho_scope *sc, const char *nomstr, } *out = NULL; - SLIST_FOREACH(nom, &sc->noms, next) { + SLIST_FOREACH(nom, &sc->noms, entries) { if (strncmp(nom->s, nomstr, sz) == 0) { *out = nom; break; @@ -249,7 +254,7 @@ scope_nom_in_local(struct spho_scope *sc, struct spho_nom *nom) { struct spho_nom *sc_nom; - SLIST_FOREACH(sc_nom, &sc->noms, next) { + SLIST_FOREACH(sc_nom, &sc->noms, entries) { if (sc_nom == nom) return (1); } diff --git a/src/spho/tp.c b/src/spho/tp.c index 4140633..2fe6140 100644 --- a/src/spho/tp.c +++ b/src/spho/tp.c @@ -20,7 +20,7 @@ spho_tp_alloc(struct spho_scope *sc) } ((struct spho_tp *)tp_alloc)->sc = sc; - TAILQ_INSERT_TAIL(&sc->tps, tp_alloc, allocs); + STAILQ_INSERT_TAIL(&sc->tps, tp_alloc, entries); return ((struct spho_tp *)tp_alloc); } @@ -36,25 +36,11 @@ spho_tp_op_alloc(struct spho_scope *sc) } ((struct spho_tp_op *)tp_alloc)->sc = sc; - TAILQ_INSERT_TAIL(&sc->tps, tp_alloc, allocs); + STAILQ_INSERT_TAIL(&sc->tps, tp_alloc, entries); return ((struct spho_tp_op *)tp_alloc); } -static void -spho_tp_free(struct spho_tp *tp) -{ - struct spho_scope *sc; - struct spho_tp_alloc *tp_alloc; - - sc = tp->sc; - tp_alloc = (struct spho_tp_alloc *)tp; - - TAILQ_REMOVE(&sc->tps, tp_alloc, allocs); - - free(tp_alloc); -} - struct spho_tp * spho_tp_create_conj(struct spho_scope *sc, struct spho_tp *ltp, struct spho_tp *rtp) @@ -270,45 +256,3 @@ spho_tp_op_create(struct spho_scope *sc, struct spho_scope *op_sc, struct spho_t return (op); } - -/* Free type structure. External data (like nom) are freed elsewhere. */ -void -spho_tp_destroy(struct spho_tp *tp) -{ - struct spho_tp *arg; - - switch (tp->kind & SPHO_TP_FORM_MASK) { - case SPHO_TP_FORM_TRUE: - case SPHO_TP_FORM_FALSE: - case SPHO_TP_FORM_NAME: - case SPHO_TP_FORM_VAR: - break; - case SPHO_TP_FORM_CONJ: - case SPHO_TP_FORM_DISJ: - case SPHO_TP_FORM_IMPL: - case SPHO_TP_FORM_ARROW: - spho_tp_destroy(tp->d.binop.left); - spho_tp_destroy(tp->d.binop.right); - break; - case SPHO_TP_FORM_BOX: - spho_tp_destroy(tp->d.unop.operand); - break; - case SPHO_TP_FORM_FORALL: - spho_tp_destroy(tp->d.fa.tp); - break; - case SPHO_TP_FORM_MEMBER: - spho_tp_destroy(tp->d.memb.tp); - break; - case SPHO_TP_FORM_APPL: - STAILQ_FOREACH(arg, tp->d.appl.args, entries) { - spho_tp_destroy(arg); - } - free(tp->d.appl.args); - break; - default: - SPHO_ASSERT(0); - break; - } - - spho_tp_free(tp); -} From ad1d5776f8e14635c43259282f8220a95c6597fa Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Fri, 27 Jun 2025 04:23:50 +0200 Subject: [PATCH 04/10] fix typdef param shit --- src/msph/sphophi.c | 4 ++-- src/msph/tree.c | 48 +++++++++++++++++++++++++++++----------------- src/spho/scope.c | 1 + 3 files changed, 33 insertions(+), 20 deletions(-) diff --git a/src/msph/sphophi.c b/src/msph/sphophi.c index 59eacdb..0a629b5 100644 --- a/src/msph/sphophi.c +++ b/src/msph/sphophi.c @@ -456,8 +456,8 @@ msph_tree_sphophi_prebind(struct spho_scope *sc, return (-1); } - if ((ret = spho_scope_prebind_tp_op(sc, NOM(name), op)) - == -1) { + if ((ret = spho_scope_prebind_tp_op(sc, + NOM(tpdef->name), op)) == -1) { return (-1); } } else { diff --git a/src/msph/tree.c b/src/msph/tree.c index b50f0f7..87d99d7 100644 --- a/src/msph/tree.c +++ b/src/msph/tree.c @@ -30,7 +30,7 @@ static void tree_parse_init(struct tree_parse *, struct msph_token_stream *, int); static int tree_parse_next_token(struct tree_parse *); -static ssize_t tree_ind_fprint(FILE *, int, struct msph_tree *); +static int tree_ind_fprint(FILE *, int, struct msph_tree *); static void free_the_tree(struct msph_tree *); @@ -302,16 +302,21 @@ tree_parse_body(struct tree_parse *p, struct msph_tree *parent) dir = tree_parse_assert(p, TREE(body)); break; default: - break; + goto ret; } if (dir == NULL) - break; + goto err; STAILQ_INSERT_TAIL(&body->head, dir, entries); } +ret: return (body); +err: + free_the_tree(TREE(body)); + + return (NULL); } @@ -346,11 +351,10 @@ tree_parse_tpdef(struct tree_parse *p, struct msph_tree *parent) if (name == NULL) goto err; STAILQ_INSERT_TAIL(&def->params, name, entries); - - EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err); } while (CURR_TOKEN(p)->type == TOK_COMMA); EXPECT_CURR_TOKEN(p, TOK_RBRAK, MSPH_TREE_TPDEF, goto err); + EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err); } EXPECT_CURR_TOKEN(p, TOK_EQUALS, MSPH_TREE_TPDEF, goto err); @@ -418,7 +422,7 @@ tree_parse_ident_extsize(struct tree_parse *p, struct msph_tree *parent, TEXT(id)->pos = CURR_TOKEN(p)->pos; DECOR_INIT(id); - if (SPHO_STRLCPY(id->str, CURR_TOKEN(p)->data.str, sizeof(id->str)) + if (strlcpy(id->str, CURR_TOKEN(p)->data.str, sizeof(id->str)) >= sizeof(id->str)) { MSPH_ERR(CTX(p), MSPH_ERR_TREE_TOOLONG); goto err; @@ -988,7 +992,6 @@ tree_parse_tpexpr_atom(struct tree_parse *p, struct msph_tree *parent) tp = NULL; } - SPHO_DEBUG_PRINT("returning tp type=%x\n", TREE(tp)->type); return (tp); } struct msph_tree_tpexpr * @@ -1252,12 +1255,15 @@ tree_parse_trait(struct tree_parse *p, struct msph_tree *parent) DECOR_INIT(trait); trait->body = NULL; + EXPECT_READ_NEXT(res, p, MSPH_TREE_TRAIT, goto err); + if ((trait->body = tree_parse_body(p, TREE(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); + tree_parse_next_token(p); + return ((struct msph_tree_tpexpr *)trait); err: free_the_tree(TREE(trait)); @@ -1322,7 +1328,6 @@ tree_parse_membdecl(struct tree_parse *p, struct msph_tree *parent) if ((membd->name = tree_parse_namedecl(p, TREE(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); @@ -1377,11 +1382,10 @@ free_the_tree(struct msph_tree *tree) #define MSPH_TREE_INDENT " " __attribute__((format(printf, 3, 4))) -static ssize_t +static int indent_fprintf(FILE *f, int indent, const char *fmt, ...) { - int res; - ssize_t ret; + int res, ret; int i; va_list ap; @@ -1391,25 +1395,25 @@ indent_fprintf(FILE *f, int indent, const char *fmt, ...) for (i = 0; i < indent; i++) { res = fprintf(f, "%s", MSPH_TREE_INDENT); if (res < 0) { - return ((ssize_t)res); + return (res); } - ret += (ssize_t)res; + ret += res; } res = vfprintf(f, fmt, ap); if (res < 0) { - return ((ssize_t)res); + return (res); } - ret += (ssize_t)res; + ret += res; va_end(ap); return (ret); } -static ssize_t +static int tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) { - ssize_t ret, res; + int ret, res; struct msph_tree_root *root; struct msph_tree_unit *unit; struct msph_tree_body *body; @@ -1431,6 +1435,7 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) struct msph_tree_paren *paren; struct msph_tree_ident *ident; struct msph_tree_tpexpr *tp; + struct msph_tree_namedecl *named; const char *ident_kind; ret = 0; @@ -1519,6 +1524,13 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) return (res); } ret += res; + STAILQ_FOREACH(named, &tpdef->params, entries) { + if ((res = tree_ind_fprint(f, indent+1, TREE(named))) + < 0) { + return (res); + } + ret += res; + } if ((res = tree_ind_fprint(f, indent+1, TREE(tpdef->tp))) < 0) return (res); ret += res; diff --git a/src/spho/scope.c b/src/spho/scope.c index 40a41a5..9f1b15c 100644 --- a/src/spho/scope.c +++ b/src/spho/scope.c @@ -128,6 +128,7 @@ spho_scope_nom_add(struct spho_scope *sc, const char *nomstr, size_t sz) SPHO_SC_ERR(sc, SPHO_ERR_TOOBIG); goto err; } + nom->id = sc->ctx->nom_cnt++; SLIST_INSERT_HEAD(&sc->noms, nom, entries); sc->nom_cnt++; From 0aa49cfe9b41bb2ca3c67e8a5909936800e26577 Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Wed, 25 Jun 2025 22:02:54 +0200 Subject: [PATCH 05/10] progress 2025-06-27 --- docs/about/progress.md | 87 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 87 insertions(+) create mode 100644 docs/about/progress.md diff --git a/docs/about/progress.md b/docs/about/progress.md new file mode 100644 index 0000000..40c97dc --- /dev/null +++ b/docs/about/progress.md @@ -0,0 +1,87 @@ +# draft of presentation + +## sappho short + - sappho types intro + - a quick look at msph and spho + + +### The types + +We take a look at the grammar for sappho types + +```cmath +s, t ::= s | t (disjunction, a.k.a. union) + | s & t (conjunction, a.k.a. intersection) + | s => t (implication) + | s -> t (arrow, a.k.a. function) + | forall x . t (forall, polymorphic) + | box t (box, c.f. modular logic) + | a [t..] (type operator application) + | x (variable) + | n (nominal) + | true (true, a.k.a. top) + | false (false, a.k.a. bottom) + | { m : t } (member, a.k.a. atomic record) + | ( t ) + + +x ∈ var +n ∈ nominal +a ∈ opname +``` + +The type `t <: s` would be expressive sugar for `box (t => s)` + +### msph and spho + +**`msph`** is a minimal language for describing types in sappho and a partial +implementation (as of 2025-06-25). The goal being to have a prototype for +deciding subtyping by the end of the summer. Right now it includes + +* parser (prefix notation `&`, `|`, `=>`, `->`) +* iterative decorators adding scope, type, and binding data. +* interface with these decorations is implemented as a separate library, + **spho**. + +**`spho`** is the WIP type system implementation, as of now having bindings to + +* handle type representation data structures +* handle scoping of names and bindings +* initial progress on subtyping implementation + +Left to do to get a prototype subtype checker working: + +* handling of subtyping sequent judgement rules +* search heuristic for basic proof search +* cyclic proof search + +Thoughts + +* maybe eventually add a basic term language and interpreter +* can we use external software/libraries for proof search? + +## interpretation of types + - example programs in `msph` + - unified syntax for types and bounded polymorphism + - example: self typing + - example: conditional method existence + - example: capabilities? + - the meaning of `true` and existence of methods. + - undefined behaviour and `true`? + - how does this relate to the denotation stuff from before? + +# formal rules and the sequent calculus +Check formalities.md. + - simple rules + - type constructor rules + - recursion and cyclic proofs +* next steps? + - formals: + - formulate theorems + - if we use semantic subtyping, isn't it enough to + prove subtyping sound with regards to set denotation? + - specify term language? + - implementation: sequent calculus based subtyping decider + - simple rules, should be fairly simple + - type constructors, straightforward hopefully + - recursion and cyclic proofs... `¯\_(ツ)_/¯` From 333534a8d1185245aca6ad5d6fa00937126ef5aa Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Sat, 28 Jun 2025 00:20:00 +0200 Subject: [PATCH 06/10] fixing parsing --- docs/about/formalities.md | 20 ++++---- docs/about/progress.md | 16 +++--- include/msph/{common.h => msph.h} | 6 +-- include/msph/token.h | 2 +- include/msph/tree.h | 2 +- src/msph/msph.c | 82 +++++++++++++++++++++++-------- src/msph/token.c | 2 +- src/msph/tree.c | 12 +++-- 8 files changed, 95 insertions(+), 47 deletions(-) rename include/msph/{common.h => msph.h} (85%) diff --git a/docs/about/formalities.md b/docs/about/formalities.md index 57871b4..246c2e2 100644 --- a/docs/about/formalities.md +++ b/docs/about/formalities.md @@ -8,7 +8,7 @@ s, t ::= s | t (disjunction, a.k.a. union) | s => t (implication) | s -> t (arrow, a.k.a. function) | forall x . t (forall, polymorphic) - | box t (box, c.f. modular logic) + | box t (box, c.f. modal logic) | a [t..] (type operator application) | x (variable) | n (nominal) @@ -37,23 +37,23 @@ s, γ ⊢ s, δ ---- [false-left] false, γ ⊢ δ -// trace pairs: none +// trace pairs: none? s, t, γ ⊢ δ ---- [conj-left] s & t, γ ⊢ δ -// trace pairs: none +// trace pairs: none? γ ⊢ s, t, δ ---- [disj-right] γ ⊢ s | t, δ -// trace pairs: none +// trace pairs: none? s, γ ⊢ δ t, γ ⊢ δ ---- [disj-left] s | t, γ ⊢ δ -// trace pairs: none +// trace pairs: none? γ ⊢ s, δ γ ⊢ t, δ ---- [conj-right] @@ -61,12 +61,12 @@ s | t, γ ⊢ δ // XXX // remove s => t? always make progress -// trace pairs: none +// trace pairs: none? s => t, s, t, γ ⊢ δ ---- [impl-left] s => t, s, γ ⊢ δ -// trace pairs: none +// trace pairs: none? s, γ ⊢ t, δ ---- [impl-right] γ ⊢ s => t, δ @@ -89,7 +89,7 @@ box t, γ ⊢ δ // to exclude typedefs like // type A = A // Or that our cycle detection excludes paths between "identical" states. -// trace pairs: none +// trace pairs: none? γ ⊢ expand(a[t..]), δ ---- γ ⊢ a[t..], δ @@ -114,6 +114,7 @@ n fresh ---- [forall] γ ⊢ δ +// TODO can we choose a simpler rule instead? // 1 + n! premises // trace pairs: i ∈ [1..(n! + 1)], premise[i] -- conclusion c, γ* ⊢ a_1, ..., a_n, δ* @@ -122,9 +123,10 @@ c, γ* ⊢ a_1, ..., a_n, δ* OR { b_i | i ∈ ¬I }, γ* ⊢ d, δ* ---- [loads-of-fun] -a_1 -> b_1, ..., a_n -> b_n, γ ⊢ c -> d, δ +a_1 -> b_1, ..., a_n -> b_n, γ ⊢ c -> d, δ ``` + ### context operators * box filtering diff --git a/docs/about/progress.md b/docs/about/progress.md index 40c97dc..9b71035 100644 --- a/docs/about/progress.md +++ b/docs/about/progress.md @@ -1,11 +1,9 @@ -# draft of presentation - -## sappho short +# sappho short - sappho types intro - a quick look at msph and spho -### The types +## The types We take a look at the grammar for sappho types @@ -15,7 +13,7 @@ s, t ::= s | t (disjunction, a.k.a. union) | s => t (implication) | s -> t (arrow, a.k.a. function) | forall x . t (forall, polymorphic) - | box t (box, c.f. modular logic) + | box t (box, c.f. modal logic) | a [t..] (type operator application) | x (variable) | n (nominal) @@ -30,7 +28,7 @@ n ∈ nominal a ∈ opname ``` -The type `t <: s` would be expressive sugar for `box (t => s)` +The type `t <: s` would be syntactic sugar for `box (t => s)` ### msph and spho @@ -60,7 +58,7 @@ Thoughts * maybe eventually add a basic term language and interpreter * can we use external software/libraries for proof search? -## interpretation of types +# interpretation of types - example programs in `msph` - unified syntax for types and bounded polymorphism - example: self typing @@ -75,7 +73,8 @@ Check formalities.md. - simple rules - type constructor rules - recursion and cyclic proofs -* next steps? + +# next steps? - formals: - formulate theorems - if we use semantic subtyping, isn't it enough to @@ -85,3 +84,4 @@ Check formalities.md. - simple rules, should be fairly simple - type constructors, straightforward hopefully - recursion and cyclic proofs... `¯\_(ツ)_/¯` + - describe use of language with type system (interpretation of types) diff --git a/include/msph/common.h b/include/msph/msph.h similarity index 85% rename from include/msph/common.h rename to include/msph/msph.h index eb49da4..f34980b 100644 --- a/include/msph/common.h +++ b/include/msph/msph.h @@ -1,5 +1,5 @@ -#ifndef _MSPH_COMMON_H -#define _MSPH_COMMON_H +#ifndef _MSPH_H +#define _MSPH_H #include "msph/err.h" #include "spho/ctx.h" @@ -25,4 +25,4 @@ struct msph_text_pos { unsigned int col; }; -#endif +#endif /* ifndef _MSPH_H */ diff --git a/include/msph/token.h b/include/msph/token.h index 21617eb..18fb7ae 100644 --- a/include/msph/token.h +++ b/include/msph/token.h @@ -3,7 +3,7 @@ #include -#include "msph/common.h" +#include "msph/msph.h" /* * diff --git a/include/msph/tree.h b/include/msph/tree.h index a7567ab..3fffcfc 100644 --- a/include/msph/tree.h +++ b/include/msph/tree.h @@ -3,7 +3,7 @@ #include -#include "msph/common.h" +#include "msph/msph.h" #include "msph/token.h" /* tree decorations */ diff --git a/src/msph/msph.c b/src/msph/msph.c index 1554e61..c9d3afe 100644 --- a/src/msph/msph.c +++ b/src/msph/msph.c @@ -2,23 +2,11 @@ #include #include -#include "msph/err.h" +#include "msph/msph.h" #include "msph/token.h" #include "msph/tree.h" #include "msph/sphophi.h" -struct msph_opts { - int tokenize_only; - int parser; - const char *in_path; - const char *out_path; -} run_opts = { - 0, - MSPH_PARSE_INFIX, - NULL, - NULL -}; - #define USAGE \ "msph: micro sappho\n" \ @@ -35,6 +23,64 @@ print_usage(void) printf("%s", USAGE); } +struct err_info { + int err; + const char *msg; +} errinfo[] = { + { MSPH_ERR_SYS, "system error" }, + { MSPH_ERR_INVAL, "invalid argument" }, + { MSPH_ERR_TOOLONG, "input too long" }, + + { MSPH_ERR_TOKEN_TOOLONG, "token too long" }, + { MSPH_ERR_TOKEN_EOF, "tokenizer reached end of file" }, + { MSPH_ERR_TOKEN_NOMATCH, "no matching token" }, + { MSPH_ERR_TOKEN_INVAL, "token invalid" }, + + { MSPH_ERR_TREE_TOOLONG, "parsed data too long" }, + { MSPH_ERR_TREE_EOF, "parsing reached unexpected end of file" }, + { MSPH_ERR_TREE_NOMATCH, "parser matching failed" }, + + { MSPH_ERR_TYPE_INVAL, "invalid type" }, + + { MSPH_ERR_SPHOPHI, "spho error" }, + { -1, NULL } +}; + +void +print_error(struct msph_ctx *ctx) +{ + size_t i; + const char *err_msg; + + err_msg = NULL; + for (i = 0; errinfo[i].err != -1; i++) { + if (ctx->err == errinfo[i].err) { + err_msg = errinfo[i].msg; + break; + } + } + if (err_msg == NULL) { + err_msg = "unknown error"; + } + + fprintf(stderr, "ERROR(%x, %d):%s\n", ctx->err, ctx->err_info, err_msg); + + if (ctx->err == MSPH_ERR_SPHOPHI) + fprintf(stderr, "\t%s\n", spho_ctx_strerror(ctx->spho)); +} + +struct msph_opts { + int tokenize_only; + int parser; + const char *in_path; + const char *out_path; +} run_opts = { + 0, + MSPH_PARSE_INFIX, + NULL, + NULL +}; + int run(struct msph_opts *); int @@ -98,6 +144,7 @@ run(struct msph_opts *opts) struct msph_tree_root *root; FILE *in, *out; + in = out = NULL; s = NULL; root = NULL; @@ -157,13 +204,7 @@ exit: return (0); err: - if (root != NULL && ctx.err == MSPH_ERR_SPHOPHI) { - fprintf(stderr, "ERROR:%s\n", - spho_ctx_strerror(ctx.spho)); - } else { - fprintf(stderr, "ERROR:msph_err: %x (%d)\n", (ctx).err, - (ctx).err_info); - } + print_error(&ctx); if (in) fclose(in); @@ -173,6 +214,7 @@ err: } + void msph_ctx_init(struct msph_ctx *ctx) { diff --git a/src/msph/token.c b/src/msph/token.c index abe2677..81f61c7 100644 --- a/src/msph/token.c +++ b/src/msph/token.c @@ -7,7 +7,7 @@ #include "spho/spho.h" -#include "msph/err.h" +#include "msph/msph.h" #include "msph/token.h" diff --git a/src/msph/tree.c b/src/msph/tree.c index 87d99d7..2444da6 100644 --- a/src/msph/tree.c +++ b/src/msph/tree.c @@ -1,6 +1,5 @@ #define SPHO_ENABLE_DEBUG_PRINT -#include "msph/common.h" -#include "msph/common.h" + #include @@ -10,6 +9,7 @@ #include "spho/spho.h" +#include "msph/msph.h" #include "msph/tree.h" @@ -130,6 +130,8 @@ msph_tree_makeroot(struct msph_ctx *ctx) return (root); } +#define __POS_FMT "line: %u, col: %u" +#define __POS_ARGS(pos) (pos).line, (pos).col /* * Expect to read next token, otherwise set error and do something @@ -143,6 +145,8 @@ msph_tree_makeroot(struct msph_ctx *ctx) if (((readres) = tree_parse_next_token(parse)) == -1) \ on_err; \ if ((readres) == 0) { \ + fprintf(stderr, "unexpected end-of-file after " \ + __POS_FMT "\n", __POS_ARGS((parse)->s->src.pos)); \ MSPH_ERR_INFO(CTX(parse), MSPH_ERR_TREE_EOF, \ err_info); \ on_err; \ @@ -159,6 +163,8 @@ msph_tree_makeroot(struct msph_ctx *ctx) #define EXPECT_CURR_TOKEN(parse, toktype, err_info, on_err) \ do { \ if (CURR_TOKEN(parse)->type != toktype) { \ + fprintf(stderr, "parser expected token " #toktype \ + "\n"); \ MSPH_ERR_INFO(CTX(parse), MSPH_ERR_TREE_NOMATCH, \ err_info); \ on_err; \ @@ -1062,7 +1068,6 @@ err: struct msph_tree_tpexpr * tree_parse_tpname_or_tpappl(struct tree_parse *p, struct msph_tree *parent) { - int res; struct msph_tree_tpname *tpname; struct msph_tree_tpexpr *ret; struct msph_tree_nameref *nameref; @@ -1074,7 +1079,6 @@ tree_parse_tpname_or_tpappl(struct tree_parse *p, struct msph_tree *parent) return (NULL); if (CURR_TOKEN(p)->type == TOK_LBRAK) { - EXPECT_READ_NEXT(res, p, MSPH_TREE_TPAPPL, goto err); if ((ret = tree_parse_tpapplargs(p, nameref, parent)) == NULL) goto err; return (ret); From 9db2cb800d0994fa0ca116f1f92ed25d4bd36780 Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Sat, 28 Jun 2025 00:25:37 +0200 Subject: [PATCH 07/10] cleaning up examples --- example/comparable.msph | 16 ++++++++++++++++ example/ex1.msph | 4 ---- example/ex2.msph | 1 - example/ex3.msph | 13 ------------- example/ex4.msph | 20 -------------------- example/ex5.msph | 21 --------------------- example/graph.msph | 10 ++++++++++ example/non-parse/ex6.msph | 21 --------------------- example/{subt => }/rec-lockstep.msph | 0 example/self.msph | 19 +++++++++++++++++++ 10 files changed, 45 insertions(+), 80 deletions(-) create mode 100644 example/comparable.msph delete mode 100644 example/ex1.msph delete mode 100644 example/ex2.msph delete mode 100644 example/ex3.msph delete mode 100644 example/ex4.msph delete mode 100644 example/ex5.msph create mode 100644 example/graph.msph delete mode 100644 example/non-parse/ex6.msph rename example/{subt => }/rec-lockstep.msph (100%) create mode 100644 example/self.msph diff --git a/example/comparable.msph b/example/comparable.msph new file mode 100644 index 0000000..2f73457 --- /dev/null +++ b/example/comparable.msph @@ -0,0 +1,16 @@ +nominal lt +nominal eq +nominal gt + +type ord = lt | eq | gt + +type comparable[t] = { + member cmp : t -> ord +} + + +type integer = { + member cmp : integer -> ord +} + +assert integer <: comparable[integer] diff --git a/example/ex1.msph b/example/ex1.msph deleted file mode 100644 index 0844c3f..0000000 --- a/example/ex1.msph +++ /dev/null @@ -1,4 +0,0 @@ - -nominal C - - diff --git a/example/ex2.msph b/example/ex2.msph deleted file mode 100644 index 5b85fdc..0000000 --- a/example/ex2.msph +++ /dev/null @@ -1 +0,0 @@ -type A = & C D diff --git a/example/ex3.msph b/example/ex3.msph deleted file mode 100644 index 9770336..0000000 --- a/example/ex3.msph +++ /dev/null @@ -1,13 +0,0 @@ - -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/example/ex4.msph b/example/ex4.msph deleted file mode 100644 index ffc0174..0000000 --- a/example/ex4.msph +++ /dev/null @@ -1,20 +0,0 @@ -nominal M -nominal N -nominal O -nominal P - -type A = { - member member1: & N M - member member2: | M N -} - -type B = forall X. { - member member1 : & X A -} - -member outer1 : box { - member member1: & B True - type T = & B A - member member2 : | (& T O) P - type S = & B False -} diff --git a/example/ex5.msph b/example/ex5.msph deleted file mode 100644 index 5774e54..0000000 --- a/example/ex5.msph +++ /dev/null @@ -1,21 +0,0 @@ -nominal N -nominal M - - -type T[X, Y] = { - // body -} - -type A = T[N, M] // binding X -> N, Y -> M -type B = T[M, N] // binding X -> M, Y -> N - -// converted to - -type A = ⟨ X -> N, Y -> M ⟩ { - // body -} -type B = ⟨ X -> M, Y -> N ⟩ { - // body -} - - diff --git a/example/graph.msph b/example/graph.msph new file mode 100644 index 0000000..b636f3b --- /dev/null +++ b/example/graph.msph @@ -0,0 +1,10 @@ +type gnode[e] = { + member edges : iterable[e] +} + +type gedge[n] = { + member src : n + member dst : n +} + +type graph[n, e] = (n <: gnode[e]) & (e <: gedge[n]) diff --git a/example/non-parse/ex6.msph b/example/non-parse/ex6.msph deleted file mode 100644 index afdeccb..0000000 --- a/example/non-parse/ex6.msph +++ /dev/null @@ -1,21 +0,0 @@ -type A[X, Y] = { - type B[Z] = { - mb : X & Z - } - - ma : B[Y] -} - - -m : A[M, N] - - -m : ⟨X -> M, Y -> N⟩ { - ma : B[Y] -} - -m : ⟨X -> M, Y -> N⟩ { - ma : ⟨Z -> Y⟩ { - mb : X & Z - } -} diff --git a/example/subt/rec-lockstep.msph b/example/rec-lockstep.msph similarity index 100% rename from example/subt/rec-lockstep.msph rename to example/rec-lockstep.msph diff --git a/example/self.msph b/example/self.msph new file mode 100644 index 0000000..d482e1c --- /dev/null +++ b/example/self.msph @@ -0,0 +1,19 @@ +type Accumulator[Self] = (Self <: Accumulator[Self]) & { + member add : Int -> Self +} + +type MyAccum = { + member add : Int -> MyAccum +} + +assert MyAccum <: Accumulator[MyAccum] + + + + + +type Acchmmmmulator[Self] = (Self <: Acchmmmmulator[Self]) => { + member add : Int -> Self +} + + From 37c1f93902e944e6c61d45a4b226833328e53a98 Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Sat, 28 Jun 2025 01:08:29 +0200 Subject: [PATCH 08/10] updated with some code style and build instructions --- README.md | 60 +++++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 58 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 8d01411..0aa5d85 100644 --- a/README.md +++ b/README.md @@ -4,14 +4,70 @@ experimental type system implementation ## getting and building +This will get you a basic build configured for development and debugging in the +subdirectory `build-debug/` of repository base: ```sh git clone https://gitta.log-e.se/lnsol/log-e-sappho.git cd ./log-e-sappho -cmake . -B build -cd build +cmake . --preset=debug +cd build-debug make ``` +To get sane error messages from editors using `clangd` for diagnostics, i.e. +using the same compilation flags configured for the build by cmake, in the repo +base directory link `compile_commands.json`: +```sh +ln -s build-debug/compile_commands.json +``` + +## "Code style" + +I learned C from a guy that used to hack on OpenBSD, and just got used to +writing it this way. If you wanna hack on this yourself, use your judgement. +Look at the rest of the code and make yours look similar. Like, who cares about +rules really? Here are some guidelines tho. + +**80 columns text width.** + +Use **8 spaces wide TABS** (yes, actual TABS, not just 8 spaces) for +indentation and when inside `while`-/`if`-/etc. **conditions that span multiple +lines, indent 4 spaces + 0 or more TABS**, as to separate condition from body +of + +I.e. do +```c +if (1 /* this is a very long condition */ + == 2 /* spanning multiple lines */ + || 2 < 3 /* and we indent like this) { + this = the_way; + /* as to increase distinguishability of condition from body */ +} +``` +not +```c +if ( /* ... */ + 2 < 3) { + eyes = bleeding; +} +``` + +Conditional statements without `{ .. }` is okay (preferred) if the condition +fits on one line. + +I.e. do +```c +if (1 /* short condition that fits on one line */) + u = the_best; +``` +and +```c +if (the_variable_that_has_that_long_name = function_with_a_long_name_too( + arg_is_shorter_tho)) { + gesture = clapping; +} +``` + ## repository content This repository contains: From f62108106433b58767a01b08dd7e85d428c448c4 Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Sat, 28 Jun 2025 01:22:32 +0200 Subject: [PATCH 09/10] comment about tab width --- README.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 0aa5d85..8b39d9d 100644 --- a/README.md +++ b/README.md @@ -33,7 +33,10 @@ rules really? Here are some guidelines tho. Use **8 spaces wide TABS** (yes, actual TABS, not just 8 spaces) for indentation and when inside `while`-/`if`-/etc. **conditions that span multiple lines, indent 4 spaces + 0 or more TABS**, as to separate condition from body -of +of the conditional statement. + +(Look at the following examples using a tab width of 8, otherwise they won't +make much sense.) I.e. do ```c From 82241b237c5b7eb9a6c7ae729adeb2e20c4894a5 Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Sat, 28 Jun 2025 01:40:36 +0200 Subject: [PATCH 10/10] oops --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 8b39d9d..4259565 100644 --- a/README.md +++ b/README.md @@ -42,7 +42,7 @@ I.e. do ```c if (1 /* this is a very long condition */ == 2 /* spanning multiple lines */ - || 2 < 3 /* and we indent like this) { + || 2 < 3 /* and we indent like this */) { this = the_way; /* as to increase distinguishability of condition from body */ }