From e036fa16f8551a2831d3dcb9810aa3d8f4672257 Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Fri, 13 Jun 2025 17:36:36 +0200 Subject: [PATCH] recursive lockstep example --- README.md | 203 +++++++++++++++++++++++++++++---- example/subt/rec-lockstep.msph | 9 ++ include/msph/sphophi.h | 1 + include/msph/tree.h | 20 +++- include/spho/bind.h | 37 +++++- include/spho/err.h | 1 + include/spho/scope.h | 40 ++++--- include/spho/spho.h | 19 +++ include/spho/tp.h | 5 +- include/spho/util.h | 25 ---- src/msph/sphophi.c | 120 +++++++++++++++---- src/msph/tree.c | 21 +++- src/spho/bind.c | 71 +++++++++--- src/spho/scope.c | 69 ++++++++--- src/spho/tp.c | 28 ++++- 15 files changed, 536 insertions(+), 133 deletions(-) create mode 100644 example/subt/rec-lockstep.msph delete mode 100644 include/spho/util.h diff --git a/README.md b/README.md index 8a29000..78b0f90 100644 --- a/README.md +++ b/README.md @@ -79,19 +79,18 @@ box t, γ ⊢ δ ρ; γ ⊢ box t, δ -// recursion through operators are handled using the recursion context ρ -// XXX compare with iso-recursive subtyping (double expansion) ----- [op-discharge] -a [t..], ρ; γ ⊢ a [t..], δ - -a [t..]*, ρ; γ ⊢ expand(a [t..]), δ ----- [op-expand1] -ρ; γ ⊢ a [t..], δ - -a [t..], ρ; γ ⊢ expand(a [t..]), δ ----- [op-expand2] -a [t..]*, ρ; γ ⊢ a [t..], δ +// using cyclic proof strategy, rule for dealing with aliases/type operators +// becomes really simple. However, this requires well-formedness rules on types +// to exclude typedefs like +// type A = A +// Or that our cycle detection excludes paths between "identical" states. +γ ⊢ expand(a[t..]), δ +---- +γ ⊢ a[t..], δ +expand(a[t..]), γ ⊢ δ +---- +a[t..], γ ⊢ δ // member types are filtered according to member name @@ -108,10 +107,12 @@ n fresh ρ; γ ⊢ δ - - +ρ; t[n/x], s[n/y] ⊢ u[n/z] +---- +ρ; forall x. t, forall y. s ⊢ forall z. u ``` + ### context operators * box filtering @@ -123,22 +124,50 @@ n fresh * member unwrapping ``` (t, γ) >> m =def= s, (γ >> m) if t == { m : s }, for some s + t, (γ >> m) if t == box s, for some s γ >> m otherwise ``` * forall-unwrapping and substitution ``` (t, γ) [n] =def= s [n/x], (γ [n]) if t == forall x . s, for some x, s + t, (γ [n]) if t == box s, for some s γ [n] otherwise ``` -What happens when box is buried under type operators, like box s & box t? It -could be that the above definition filters out too much of the contexts. +### Recursive subtyping + +Type aliases creates the possibility of recursive types, and thus we need to +handle recursive subtyping + +Handling subtyping co-inductively would enable us to handle the relation +``` +type A = { x : { y : A } } +type B = { y : { x : B } } + +A <: { x : B } +{ x : B } <: A +``` + + +We have made progress if we "switch context" + +If we make progress and end up at the same sequent, co-induction gives us the +conclusion. + +Some actions/rules lead to equivalent contexts, i.e. does not switch +context/make progress. + +### Other + +True ~ { x : True } on the left +False ~ { x : False } on the right + +or rather + +True ~ { x : True } in positive position +False ~ { x : False } in negative position -My gut feeling™ makes me think it is just a matter of reordering sequent rules -to get keep the things wanted in context, which for an algorithm sucks, but from -a declarative standpoint would be okay. This needs some further validation, and -of course a reformulation for the actual algorithm. @@ -154,6 +183,139 @@ if ¬s, then s => t holds ``` +altho +``` +γ ⊢ s => t, s, δ +``` + +Given the msph program +``` +nominal n + +type Woops[e] = { + member f : (e <: false => n) | (e <: false) +} + +type Noooes = { + member f : true +} +``` +we can prove that, for any type `t` +``` +Noooes <: Woops[t] +``` + +The derivation looks like this: +``` +---- [identity] +true, t <: false ⊢ n, (t <: false) +---- [impl-right] +true ⊢ (t <: false => n), (t <: false) +---- [disj-right] +true ⊢ (t <: false => n) | (t <: false) +---- [member] +{ f : true } ⊢ { f : (t <: false => n) | (t <: false) } +---- [expand-right] +{ f : true } ⊢ Woops[t] +---- [expand-left] +Nooes ⊢ Woops[t] +---- [impl-right] +⊢ Nooes => Woops[t] +---- [box-right] +⊢ Nooes <: Woops[t] +``` + +This looks a bit dangerous at first. However, if we translate the implication to +using disjunction and negation, we get +``` +(t <: false => N) | (t <: false) == (¬(t <: false) | n) | (t <: false) +``` + +Considering the two cases +``` +(1) t == false +(2) t != false +``` +we see that in (1) +``` +(¬(t <: false) | n) | (t <: false) == +(¬(true) | n) | (true) == +true +``` +and in (2) +``` +(¬(t <: false) | n) | (t <: false) == +(¬(false) | n) | false == +(true | n) | false == +true +``` + +## What is true? + +Our "set interpretation" of types says `true` represents the full universe of +"things". + +What are these things? + +For all intents and purposes, a programmer can look at them as the values of +our language. + +What does this mean in practical terms? + +Well, it means something of type `true` is "a value". + +What is "a value" then? + +That's a good question. It can be anything really. + +An integer? + +Yep! + +A function? + +Yes, m'am! + +A solution to the halting problem? + +Well, yeah! But good luck constructing that. + +A... + +I think you get my point. A value can be anything from a simple integer to +nuclear apocalypse. The thing is, from the point of view of our program, it +means "we cannot really say anything here". + +But couldn't that be dangerous? + +Depends on what you mean by dangerous. + +I mean, to be able to give everything a type? + +Well, let me ask you this: do you like rat poison? + +What? To eat? + +Yeah! + +Nooo, that'd be dangerous! + +Yeah, exactly my point. + +What? + +You know what rat poison is obviously, despite it being dangerous? + +Well, yeah... + +Maybe you got it already, but my point is: rat poison is dangerous, but you +still know about it, and its existance. So, something being dangerous does not +mean you have this blank spot of knowledge that you just keep ignoring because +of this perceived danger. + + + + ### interpretation of ⊢ what is the interpretation of @@ -171,3 +333,4 @@ disjunction of δ hold for k + diff --git a/example/subt/rec-lockstep.msph b/example/subt/rec-lockstep.msph new file mode 100644 index 0000000..2b74462 --- /dev/null +++ b/example/subt/rec-lockstep.msph @@ -0,0 +1,9 @@ + +type A = { x : { y : A } } + +type B = { y : { x : B } } + + +assert { x : B } <: A + +assert A <: { x : B } diff --git a/include/msph/sphophi.h b/include/msph/sphophi.h index 052b9bf..fa723be 100644 --- a/include/msph/sphophi.h +++ b/include/msph/sphophi.h @@ -7,6 +7,7 @@ int msph_sphophi_init(struct msph_tree_root *); int msph_sphophi_scope(struct msph_tree_root *); int msph_sphophi_nom_lookup(struct msph_tree_root *); int msph_sphophi_tp(struct msph_tree_root *); +int msph_sphophi_bind_static_tp_names(struct msph_tree_root *); int msph_sphophi(struct msph_tree_root *); diff --git a/include/msph/tree.h b/include/msph/tree.h index b2e793d..a41a939 100644 --- a/include/msph/tree.h +++ b/include/msph/tree.h @@ -56,8 +56,8 @@ * Trait ({ ... }, creates scoping) */ -#define MSPH_TREE_ROOT 0x0000 -#define MSPH_TREE_UNIT 0x0001 +#define MSPH_TREE_ROOT (0x0000 | MSPH_TREE_FLAG_SCOPE) +#define MSPH_TREE_UNIT (0x0001 | MSPH_TREE_FLAG_SCOPE) #define MSPH_TREE_BODY 0x0010 @@ -72,17 +72,25 @@ #define MSPH_TREE_FALSE 0x0042 #define MSPH_TREE_NAME 0x0043 #define MSPH_TREE_APPL 0x0044 -#define MSPH_TREE_TRAIT 0x0045 +#define MSPH_TREE_TRAIT (0x0045 | MSPH_TREE_FLAG_SCOPE) #define MSPH_TREE_CONJ 0x0046 #define MSPH_TREE_DISJ 0x0047 #define MSPH_TREE_IMPL 0x0048 #define MSPH_TREE_ARROW 0x0049 #define MSPH_TREE_BOX 0x004a -#define MSPH_TREE_FORALL 0x004b +#define MSPH_TREE_FORALL (0x004b | MSPH_TREE_FLAG_SCOPE) #define MSPH_TREE_PAREN 0x004c -#define MSPH_TREE_IDENT 0x0100 +#define MSPH_TREE_IDENT 0x0080 +#define MSPH_TREE_MASK_ID 0x0fff +#define MSPH_TREE_MASK_FLAGS 0xf000 + +#define MSPH_TREE_FLAG_SCOPE 0x1000 +#define MSPH_TREE_FLAG_STATIC_BIND 0x2000 + +#define MSPH_TREE_SCOPE(type) (type & MSPH_TREE_FLAG_SCOPE) +#define MSPH_TREE_STATIC_BIND(type) (type & MSPH_TREE_FLAG_STATIC_BIND) struct msph_tree { int type; @@ -145,6 +153,7 @@ struct msph_tree_nomindecl { struct msph_tree_dir hdir; struct msph_tree_ident *id; + struct msph_tree_tpexpr *tp; }; struct msph_tree_membdecl { @@ -257,7 +266,6 @@ struct msph_tree_ident { struct msph_nom_decor dec; }; - struct msph_tree_root *msph_tree_makeroot(struct msph_ctx *); int msph_tree_parse(struct msph_token_stream *, struct msph_tree_root *); diff --git a/include/spho/bind.h b/include/spho/bind.h index 7d2ae06..9a19b38 100644 --- a/include/spho/bind.h +++ b/include/spho/bind.h @@ -5,24 +5,49 @@ #include "spho/scope.h" +#define SPHO_BIND_KIND_TP 1 +#define SPHO_BIND_KIND_TPOP 2 + +union spho_bound { + struct spho_tp *tp; + struct spho_tpop *op; +}; + struct spho_binding { struct spho_nom *nom; - struct spho_tp *tp; - STAILQ_ENTRY(spho_binding) entries; + int kind; + union spho_bound bound; +}; + +struct spho_bind_scope { + struct spho_scope *sc; + + size_t cap_bds; + size_t n_bds; + struct spho_binding *bds; }; struct spho_bind { - STAILQ_HEAD(spho_binding_l, spho_binding) head; - struct spho_ctx *ctx; + struct spho_bind_scope *binder; struct spho_bind *parent; }; +struct spho_bind_scope *spho_bind_scope_create(struct spho_scope *); -struct spho_bind *spho_bind_create(struct spho_ctx *, struct spho_bind *); +int spho_bind_scope_add_tp(struct spho_bind_scope *, struct spho_nom *, + struct spho_tp *); +int spho_bind_scope_add_tpop(struct spho_bind_scope *, struct spho_nom *, + struct spho_tpop *); -int spho_bind_add(struct spho_bind *, struct spho_nom *, struct spho_tp *); +void spho_bind_scope_destroy(struct spho_bind_scope *); + +struct spho_bind *spho_bind_create(struct spho_ctx *, struct spho_bind_scope *, + struct spho_bind *); + +int spho_bind_lkp(int, struct spho_bind *, struct spho_nom *, + union spho_bound **); void spho_bind_destroy(struct spho_bind *); diff --git a/include/spho/err.h b/include/spho/err.h index e9bad83..29ce9d1 100644 --- a/include/spho/err.h +++ b/include/spho/err.h @@ -14,6 +14,7 @@ #define SPHO_ERR_ARGINVAL 0x010003 #define SPHO_ERR_NOM_INUSE 0x020001 #define SPHO_ERR_NOM_NOTINSCOPE 0x020002 +#define SPHO_ERR_BIND_EXISTS 0x030001 #define SPHO_ERR_IS_SYSERR(err) (SPHO_ERR_SYS == err) diff --git a/include/spho/scope.h b/include/spho/scope.h index 3d6b02a..5042c8f 100644 --- a/include/spho/scope.h +++ b/include/spho/scope.h @@ -15,10 +15,6 @@ struct spho_nom { SLIST_HEAD(spho_nom_l, spho_nom); -/* binding - * - * bindings needs to be able to change, so we do not store it in names directly. - */ #define TP_KONST_KEY_TRUE 0x43445 /* don't change!!!!! */ #define TP_KONST_KEY_FALSE 0x66a57 /* don't change!1! */ @@ -33,11 +29,6 @@ struct tp_unop_data { struct spho_tp *operand; }; -struct tp_binding_data { - struct spho_nom *nom; - struct spho_tp *bound; -}; - struct tp_nom_data { struct spho_nom *nom; }; @@ -52,6 +43,16 @@ struct tp_konst_data { const char *str; }; +struct tp_forall_data { + struct spho_nom *nom; + struct spho_tp *tp; +}; + +struct tp_member_data { + struct spho_nom *nom; + struct spho_tp *tp; +}; + extern const struct tp_konst_data tp_konst_true; extern const struct tp_konst_data tp_konst_false; @@ -62,10 +63,11 @@ extern const struct tp_konst_data tp_konst_false; union tp_data { struct tp_binop_data binop; struct tp_unop_data unop; - struct tp_binding_data bind; struct tp_appl_data appl; struct tp_nom_data nom; struct tp_konst_data konst; + struct tp_forall_data fa; + struct tp_member_data memb; }; /* sappho type */ @@ -95,6 +97,10 @@ struct spho_tp_alloc { TAILQ_HEAD(spho_tp_alloc_l, spho_tp_alloc); +struct spho_tpop { + struct spho_scope *sc; + struct spho_tp *tp; +}; SLIST_HEAD(spho_scope_l, spho_scope); @@ -109,7 +115,7 @@ struct spho_scope { struct spho_nom_l noms; struct spho_tp_alloc_l tps; - struct spho_bind *bind; + struct spho_bind_scope *stat_bind; SLIST_ENTRY(spho_scope) next; }; @@ -127,9 +133,13 @@ struct spho_scope *spho_scope_create(struct spho_scope *); void spho_scope_destroy(struct spho_scope *); struct spho_nom *spho_scope_nom_add(struct spho_scope *, const char *, size_t); -int spho_scope_nom_get(struct spho_scope *, const char *, size_t, - struct spho_nom **); -int spho_scope_nom_lookup(struct spho_scope *, const char *, size_t, - struct spho_nom **); +int spho_scope_nom_lookup_str(struct spho_scope *, const char *, size_t, + struct spho_nom **); +int spho_scope_nom_lookup_str_strict(struct spho_scope *, const char *, + size_t, struct spho_nom **); + +int spho_scope_tp_bind_init(struct spho_scope *); +int spho_scope_tp_bind_nom(struct spho_scope *, struct spho_nom *, + struct spho_tp *); #endif /* _SPHO_SCOPE_H */ diff --git a/include/spho/spho.h b/include/spho/spho.h index f8582dc..7674bf1 100644 --- a/include/spho/spho.h +++ b/include/spho/spho.h @@ -6,4 +6,23 @@ #include "spho/err.h" #include "spho/ctx.h" + +#define SPHO_UTIL_SLIST_DESTROY(l, elmtype, next, term) \ +do { \ + struct elmtype *elm; \ + while (! SLIST_EMPTY(l)) { \ + elm = SLIST_FIRST(l); \ + SLIST_REMOVE_HEAD(l, next); \ + term(elm); \ + free(elm); \ + } \ +} while (0) + +#ifdef SPHO_USE_STRLCPY +#define SPHO_STRLCPY(dst, src, len) strlcpy(dst, src, len) +#else +#define SPHO_STRLCPY(dst, src, len) \ + (size_t)snprintf(dst, len, "%s", src) +#endif + #endif diff --git a/include/spho/tp.h b/include/spho/tp.h index ab2e945..1279eb6 100644 --- a/include/spho/tp.h +++ b/include/spho/tp.h @@ -13,6 +13,7 @@ #define SPHO_TP_FORM_FORALL 0x15 #define SPHO_TP_FORM_APPL 0x16 #define SPHO_TP_FORM_MEMBER 0x17 +#define SPHO_TP_FORM_NOMINAL 0x18 #define SPHO_TP_FORM_TRUE 0x20 #define SPHO_TP_FORM_FALSE 0x21 @@ -22,8 +23,8 @@ #define SPHO_TP_MOD_FIRST (SPHO_TP_FORM_MASK + 1) -#define SPHO_TP_MOD_VAR (SPHO_TP_FLAG_FIRST) -#define SPHO_TP_MOD_NOMINAL (SPHO_TP_FLAG_FIRST << 1) +// #define SPHO_TP_MOD_VAR (SPHO_TP_FLAG_FIRST) +// #define SPHO_TP_MOD_NOMINAL (SPHO_TP_FLAG_FIRST << 1) #define SPHO_TP_ERR(tp, err) SPHO_ERR((tp)->sc->ctx, (err)) diff --git a/include/spho/util.h b/include/spho/util.h deleted file mode 100644 index 2cb9681..0000000 --- a/include/spho/util.h +++ /dev/null @@ -1,25 +0,0 @@ -#ifndef _SPHO_UTIL_H -#define _SPHO_UTIL_H - - -#define SPHO_UTIL_SLIST_DESTROY(l, elmtype, next, term) \ -do { \ - struct elmtype *elm; \ - while (! SLIST_EMPTY(l)) { \ - elm = SLIST_FIRST(l); \ - SLIST_REMOVE_HEAD(l, next); \ - term(elm); \ - free(elm); \ - } \ -} while (0) - -#ifdef SPHO_USE_STRLCPY -#define SPHO_STRLCPY(dst, src, len) strlcpy(dst, src, len) -#else -#define SPHO_STRLCPY(dst, src, len) \ - (size_t)snprintf(dst, len, "%s", src) -#endif - - -#endif - diff --git a/src/msph/sphophi.c b/src/msph/sphophi.c index 8e39263..74414a4 100644 --- a/src/msph/sphophi.c +++ b/src/msph/sphophi.c @@ -13,6 +13,11 @@ static int msph_tree_sphophi_decor_nom_lookup(struct spho_scope *, struct msph_tree *); static int msph_tree_sphophi_decor_tp(struct spho_scope *, struct msph_tree *); +static int msph_tree_sphophi_bind_static_tp_name(struct spho_scope *, + struct msph_tree *); + +static int msph_tree_sphophi_get_scope(struct msph_tree *, struct + spho_scope **); /* foreach_pre: top down foreach */ static int msph_sphophi_foreach_pre(msph_tree_sphophi_f, @@ -135,6 +140,13 @@ msph_sphophi_tp(struct msph_tree_root *root) return (msph_sphophi_foreach_post(msph_tree_sphophi_decor_tp, root)); } +int +msph_sphophi_bind_static_tp_names(struct msph_tree_root *root) +{ + return (msph_sphophi_foreach_pre(msph_tree_sphophi_bind_static_tp_name, + root)); +} + int msph_sphophi(struct msph_tree_root *root) { int ret; @@ -147,16 +159,18 @@ int msph_sphophi(struct msph_tree_root *root) return (ret); if ((ret = msph_sphophi_tp(root)) != 0) return (ret); + if ((ret = msph_sphophi_bind_static_tp_names(root)) != 0) + return (ret); return (ret); } -#define IS_BINDING(tree) (((tree)->type == MSPH_TREE_TPDEF) || \ - ((tree)->type == MSPH_TREE_NOMINDECL) || \ - ((tree)->type == MSPH_TREE_MEMBDECL) || \ - ((tree)->type == MSPH_TREE_FORALL)) -#define IS_TPEXPR(tree) (((tree)->type & MSPH_TREE_TPEXPR)) +#define IS_BINDING(tree) ((tree)->type == MSPH_TREE_TPDEF || \ + (tree)->type == MSPH_TREE_NOMINDECL || \ + (tree)->type == MSPH_TREE_MEMBDECL || \ + (tree)->type == MSPH_TREE_FORALL) +#define IS_TPEXPR(tree) ((tree)->type & MSPH_TREE_TPEXPR) static int msph_tree_sphophi_decor_scope(struct spho_scope *sc, struct msph_tree *tree) @@ -214,11 +228,8 @@ msph_tree_sphophi_decor_nom_lookup(struct spho_scope *sc, if (tree->parent->type != MSPH_TREE_NAME) break; ident = (struct msph_tree_ident *)tree; - if ((ret = spho_scope_nom_lookup(sc, ident->str, - sizeof(ident->str), &ident->dec.nom)) != 0) - break; - if (ident->dec.nom == NULL) - ret = -1; + ret = spho_scope_nom_lookup_str_strict(sc, ident->str, + sizeof(ident->str), &ident->dec.nom); break; default: break; @@ -265,31 +276,31 @@ msph_tree_sphophi_decor_tp(struct spho_scope *sc, struct msph_tree *tree) switch (tree->type) { case MSPH_TREE_CONJ: conj = (struct msph_tree_conj *)tree; - if ((TP(&conj->htpe) = spho_tp_create_conj(sc, TP(conj->ltp), + if ((tpexpr->dec.tp = spho_tp_create_conj(sc, TP(conj->ltp), TP(conj->rtp))) == NULL) goto cleanup; break; case MSPH_TREE_DISJ: disj = (struct msph_tree_disj *)tree; - if ((TP(&disj->htpe) = spho_tp_create_conj(sc, TP(disj->ltp), + if ((tpexpr->dec.tp = spho_tp_create_conj(sc, TP(disj->ltp), TP(disj->rtp))) == NULL) goto cleanup; break; case MSPH_TREE_IMPL: impl = (struct msph_tree_impl *)tree; - if ((TP(&impl->htpe) = spho_tp_create_conj(sc, TP(impl->ltp), + if ((tpexpr->dec.tp = spho_tp_create_conj(sc, TP(impl->ltp), TP(impl->rtp))) == NULL) goto cleanup; break; case MSPH_TREE_ARROW: arrow = (struct msph_tree_arrow *)tree; - if ((TP(&arrow->htpe) = spho_tp_create_conj(sc, TP(arrow->ltp), + if ((tpexpr->dec.tp = spho_tp_create_conj(sc, TP(arrow->ltp), TP(arrow->rtp))) == NULL) goto cleanup; break; case MSPH_TREE_NAME: name = (struct msph_tree_name *)tree; - if ((TP(&name->htpe) = spho_tp_create_name(sc, NOM(name->id))) + if ((tpexpr->dec.tp = spho_tp_create_name(sc, NOM(name->id))) == NULL) goto cleanup; break; @@ -303,34 +314,34 @@ msph_tree_sphophi_decor_tp(struct spho_scope *sc, struct msph_tree *tree) STAILQ_FOREACH(tpexpr_i, &appl->head, entries) { STAILQ_INSERT_TAIL(tps, tpexpr_i->dec.tp, entries); } - if ((TP(&appl->htpe) = spho_tp_create_appl(sc, NOM(appl->id), + if ((tpexpr->dec.tp = spho_tp_create_appl(sc, NOM(appl->id), tps)) == NULL) goto cleanup; tps = NULL; break; case MSPH_TREE_TRUE: - if ((TP(tpexpr) = spho_tp_create_true(sc)) == NULL) + if ((tpexpr->dec.tp = spho_tp_create_true(sc)) == NULL) goto cleanup; break; case MSPH_TREE_FALSE: - if ((TP(tpexpr) = spho_tp_create_false(sc)) == NULL) + if ((tpexpr->dec.tp = spho_tp_create_false(sc)) == NULL) goto cleanup; break; case MSPH_TREE_FORALL: forall = (struct msph_tree_forall *)tree; - if ((TP(&forall->htpe) = spho_tp_create_forall(sc, + if ((tpexpr->dec.tp = spho_tp_create_forall(sc, NOM(forall->id), TP(forall->inner))) == NULL) goto cleanup; break; case MSPH_TREE_BOX: box = (struct msph_tree_box *)tree; - if ((TP(&box->htpe) = spho_tp_create_box(sc, TP(box->inner))) + if ((tpexpr->dec.tp = spho_tp_create_box(sc, TP(box->inner))) == NULL) goto cleanup; break; case MSPH_TREE_PAREN: paren = (struct msph_tree_paren *)tree; - if ((TP(&paren->htpe) = TP(paren->inner)) == NULL) + if ((tpexpr->dec.tp = TP(paren->inner)) == NULL) goto cleanup; break; case MSPH_TREE_TRAIT: @@ -352,7 +363,7 @@ msph_tree_sphophi_decor_tp(struct spho_scope *sc, struct msph_tree *tree) == NULL) goto cleanup; } - trait->htpe.dec.tp = tp; + tpexpr->dec.tp = tp; } break; default: @@ -369,6 +380,71 @@ cleanup: return (ret); } +static int +msph_tree_sphophi_bind_static_tp_name(struct spho_scope *sc, + struct msph_tree *tree) +{ + int ret; + struct spho_scope *sub_sc; + struct msph_tree_tpdef *tpdef; + struct msph_tree_nomindecl *nomdecl; + + ret = 0; + + if (MSPH_TREE_SCOPE(tree->type) && + MSPH_TREE_STATIC_BIND(tree->type)) { + if ((ret = msph_tree_sphophi_get_scope(tree, &sub_sc)) == -1) + goto ret; + if ((ret = spho_scope_tp_bind_init(sub_sc)) == -1) + goto ret; + } + + switch (tree->type) { + case MSPH_TREE_TPDEF: + tpdef = (struct msph_tree_tpdef *)tree; + + ret = spho_scope_tp_bind_nom(sc, tpdef->id->dec.nom, + tpdef->tp->dec.tp); + break; + case MSPH_TREE_NOMINDECL: + nomdecl = (struct msph_tree_nomindecl *)tree; + + ret = spho_scope_tp_bind_nom(sc, nomdecl->id->dec.nom, + nomdecl->tp->dec.tp); + break; + default: + break; + } +ret: + return (ret); +} + +static int +msph_tree_sphophi_get_scope(struct msph_tree *tree, struct spho_scope **out) +{ + SPHO_PRECOND(MSPH_TREE_SCOPE(tree->type)); + + *out = NULL; + switch (tree->type) { + case MSPH_TREE_ROOT: + *out = spho_scope_global( + ((struct msph_tree_root *)tree)->ctx->spho); + break; + case MSPH_TREE_UNIT: + *out = ((struct msph_tree_unit *)tree)->dec.sc; + break; + case MSPH_TREE_TRAIT: + *out = ((struct msph_tree_trait *)tree)->dec.sc; + break; + default: + break; + } + + SPHO_POSTCOND(*out != NULL); + + return (0); +} + /* foreach pre: top down foreach node */ static int msph_sphophi_foreach_pre(msph_tree_sphophi_f f, struct msph_tree_root *root) diff --git a/src/msph/tree.c b/src/msph/tree.c index 440fc53..89d7221 100644 --- a/src/msph/tree.c +++ b/src/msph/tree.c @@ -1180,6 +1180,8 @@ struct msph_tree_dir * tree_parse_nomindecl(struct tree_parse *p, struct msph_tree *parent) { int res; + struct msph_tree_ident *id; + struct msph_tree_name *name; struct msph_tree_nomindecl *nomd; EXPECT_CURR_TOKEN(p, TOK_KW_NOMINAL, MSPH_TREE_NOMINDECL, @@ -1193,11 +1195,28 @@ tree_parse_nomindecl(struct tree_parse *p, struct msph_tree *parent) T(nomd)->parent = parent; TXT(nomd)->pos = CURR_TOKEN(p)->pos; nomd->id = NULL; + nomd->tp = NULL; EXPECT_READ_NEXT(res, p, MSPH_TREE_NOMINDECL, goto err); - if ((nomd->id = tree_parse_ident(p, T(nomd))) == NULL) + if ((id = tree_parse_ident(p, T(nomd))) == NULL) goto err; + /* name tpexpr to match tree shape of tpdef. This is not represented in + * msph language grammar. */ + if ((name = malloc(sizeof(*name))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + goto err; + } + T(name)->type = MSPH_TREE_NAME; + T(name)->parent = T(nomd); + + TXT(name)->pos = TXT(nomd->id)->pos; + TP_DECOR_INIT(&name->htpe.dec); + name->id = id; + + nomd->id = id; + nomd->tp = (struct msph_tree_tpexpr *)name; + return ((struct msph_tree_dir *)nomd); err: free_the_tree(T(nomd)); diff --git a/src/spho/bind.c b/src/spho/bind.c index 6578aa6..dd55a51 100644 --- a/src/spho/bind.c +++ b/src/spho/bind.c @@ -4,37 +4,74 @@ #include "spho/bind.h" struct spho_bind * -spho_bind_create(struct spho_ctx *ctx, struct spho_bind *parent) +spho_bind_create(struct spho_ctx *ctx, struct spho_bind_scope *binder, + struct spho_bind *parent) { struct spho_bind *bind; + SPHO_PRECOND(ctx != NULL); + SPHO_PRECOND(binder != NULL); + if ((bind = malloc(sizeof(*bind))) == NULL) { - SPHO_ERR(ctx, SPHO_ERR_SYS); + SPHO_ERR(binder->sc->ctx, SPHO_ERR_SYS); return (NULL); } - STAILQ_INIT(&bind->head); bind->ctx = ctx; + bind->binder = binder; bind->parent = parent; return (bind); } int -spho_bind_add(struct spho_bind *bind, struct spho_nom *nom, struct spho_tp *tp) +spho_bind_lkp(int, struct spho_bind *bind, struct spho_nom *nom, + union spho_bound **out) { - struct spho_binding *b; - - if ((b = malloc(sizeof(*b))) == NULL) { - SPHO_ERR(bind->ctx, SPHO_ERR_SYS); - return (-1); - } - - b->nom = nom; - b->tp = tp; - - STAILQ_INSERT_TAIL(&bind->head, b, entries); - - return (0); + // TODO + return (-1); } +void +spho_bind_destroy(struct spho_bind *bind) +{ + free(bind); +} + + +struct spho_bind_scope * +spho_bind_scope_create(struct spho_scope *sc) +{ + size_t sz; + struct spho_binding *bds; + struct spho_bind_scope *ret; + + SPHO_PRECOND(sc != NULL); + + if ((ret = malloc(sizeof(*ret))) == NULL) { + SPHO_ERR(sc->ctx, SPHO_ERR_SYS); + return (NULL); + } + + if ((bds = calloc(sz, sizeof(*bds))) == NULL) { + SPHO_ERR(sc->ctx, SPHO_ERR_SYS); + goto err; + } + + ret->sc = sc; + ret->cap_bds = sz; + ret->n_bds = 0; + ret->bds = bds; + +err: + free(ret); + + return (NULL); +} + +int +spho_binder_add_tp(struct spho_bind_scope *bdr, struct spho_nom *nom, + struct spho_tp *tp) +{ + +} diff --git a/src/spho/scope.c b/src/spho/scope.c index 2d91d5f..c5347a0 100644 --- a/src/spho/scope.c +++ b/src/spho/scope.c @@ -3,14 +3,16 @@ #include #include +#include "spho/spho.h" #include "spho/ctx.h" #include "spho/scope.h" -#include "spho/util.h" +#include "spho/bind.h" static void spho_nom_term(struct spho_nom *); -static int spho_scope_nom_get_norec(struct spho_scope *, const char *, size_t , - struct spho_nom **); +static int scope_nom_lookup_str_loc(struct spho_scope *, const char *, + size_t, struct spho_nom **); +static int scope_nom_in_loc(struct spho_scope *, struct spho_nom *); int spho_scope_init(struct spho_scope *sc, struct spho_ctx *ctx, @@ -23,7 +25,7 @@ spho_scope_init(struct spho_scope *sc, struct spho_ctx *ctx, SLIST_INIT(&sc->noms); TAILQ_INIT(&sc->tps); - sc->bind = NULL; + sc->stat_bind = NULL; return (0); } @@ -36,6 +38,10 @@ spho_scope_term(struct spho_scope *sc) SPHO_UTIL_SLIST_DESTROY(&sc->noms, spho_nom, next, spho_nom_term); sc->parent = NULL; + + if (sc->stat_bind == NULL) + spho_bind_scope_destroy(sc->stat_bind); + sc->stat_bind = NULL; } struct spho_scope * @@ -69,7 +75,7 @@ spho_scope_create(struct spho_scope *sc) static void -spho_nom_term(struct spho_nom *nom) +spho_nom_term(__attribute__((unused)) struct spho_nom *nom) { return; } @@ -98,7 +104,7 @@ spho_scope_nom_add(struct spho_scope *sc, const char *nomstr, size_t sz) nom = NULL; - if (spho_scope_nom_get_norec(sc, nomstr, sz, &nom) == -1) + if (scope_nom_lookup_str_loc(sc, nomstr, sz, &nom) == -1) return (NULL); if (nom != NULL) { @@ -139,7 +145,7 @@ err: int -spho_scope_nom_get(struct spho_scope *sc, const char *nomstr, size_t sz, +spho_scope_nom_lookup_str(struct spho_scope *sc, const char *nomstr, size_t sz, struct spho_nom **out) { struct spho_nom *nom; @@ -166,12 +172,10 @@ spho_scope_nom_get(struct spho_scope *sc, const char *nomstr, size_t sz, } int -spho_scope_nom_lookup(struct spho_scope *sc, const char *nomstr, size_t sz, - struct spho_nom **out) +spho_scope_nom_lookup_str_strict(struct spho_scope *sc, const char *nomstr, + size_t sz, struct spho_nom **out) { - int ret; - - if (spho_scope_nom_get(sc, nomstr, sz, out) == -1) + if (spho_scope_nom_lookup_str(sc, nomstr, sz, out) == -1) return (-1); if (*out == NULL) { @@ -181,9 +185,33 @@ spho_scope_nom_lookup(struct spho_scope *sc, const char *nomstr, size_t sz, return (0); } + +int +spho_scope_static_bind_init(struct spho_scope *sc) +{ + if ((sc->stat_bind = spho_bind_scope_create(sc)) + == NULL) { + return (-1); + } + + return (0); +} + +int +spho_scope_static_bind_add_tp(struct spho_scope *sc, struct spho_nom *nom, + struct spho_tp *tp) +{ + if (! scope_nom_in_loc(sc, nom)) { + SPHO_ERR(sc->ctx, SPHO_ERR_NOM_NOTINSCOPE); + return (-1); + } + + return (spho_bind_scope_add_tp(sc->stat_bind, nom, tp)); +} + static int -spho_scope_nom_get_norec(struct spho_scope *sc, const char *nomstr, size_t sz, - struct spho_nom **out) +scope_nom_lookup_str_loc(struct spho_scope *sc, const char *nomstr, + size_t sz, struct spho_nom **out) { struct spho_nom *nom; @@ -204,3 +232,16 @@ spho_scope_nom_get_norec(struct spho_scope *sc, const char *nomstr, size_t sz, return (0); } + +static int +scope_nom_in_loc(struct spho_scope *sc, struct spho_nom *nom) +{ + struct spho_nom *sc_nom; + + SLIST_FOREACH(sc_nom, &sc->noms, next) { + if (sc_nom == nom) + return (1); + } + + return (0); +} diff --git a/src/spho/tp.c b/src/spho/tp.c index d6e5f2e..3f6e4aa 100644 --- a/src/spho/tp.c +++ b/src/spho/tp.c @@ -128,8 +128,8 @@ spho_tp_create_forall(struct spho_scope *sc, struct spho_nom *nom, return (NULL); ret->kind = SPHO_TP_FORM_FORALL; - ret->d.bind.nom = nom; - ret->d.bind.bound = tp; + ret->d.fa.nom = nom; + ret->d.fa.tp = tp; return (ret); } @@ -202,12 +202,28 @@ spho_tp_create_member(struct spho_scope *sc, struct spho_nom *nom, return (NULL); ret->kind = SPHO_TP_FORM_MEMBER; - ret->d.bind.nom = nom; - ret->d.bind.bound = tp; + ret->d.memb.nom = nom; + ret->d.memb.tp = tp; return (ret); } +struct spho_tp * +spho_tp_create_nominal(struct spho_scope *sc, struct spho_nom *nom) +{ + struct spho_tp *ret; + + if ((ret = spho_tp_alloc(sc)) == NULL) + return (NULL); + + ret->kind = SPHO_TP_FORM_NOMINAL; + ret->d.nom.nom = nom; + + return (ret); +} + + + /* Free type structure. External data (like nom) are freed elsewhere. */ void spho_tp_destroy(struct spho_tp *tp) @@ -230,8 +246,10 @@ spho_tp_destroy(struct spho_tp *tp) 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.bind.bound); + spho_tp_destroy(tp->d.memb.tp); break; case SPHO_TP_FORM_APPL: STAILQ_FOREACH(arg, tp->d.appl.args, entries) {