From 55970b1bafaab8c0bbe17c9b0b4a348f580f34d1 Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Fri, 23 May 2025 14:02:51 +0200 Subject: [PATCH] starting to add code for name bindings --- CMakeLists.txt | 3 ++- example/non-parse/ex6.msph | 21 ++++++++++++++++++++ include/spho/bind.h | 29 +++++++++++++++++++++++++++ include/spho/scope.h | 39 +++++++++++++------------------------ include/spho/tp.h | 19 +++++++++--------- src/spho/bind.c | 40 ++++++++++++++++++++++++++++++++++++++ src/spho/scope.c | 6 ++++-- src/spho/tp.c | 33 +++++++++++++------------------ 8 files changed, 131 insertions(+), 59 deletions(-) create mode 100644 example/non-parse/ex6.msph create mode 100644 include/spho/bind.h create mode 100644 src/spho/bind.c diff --git a/CMakeLists.txt b/CMakeLists.txt index 8f3758c..cd65d36 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -23,9 +23,9 @@ set(SPHO_HEADER_DIR ${INCLUDE_DIR}/spho) set(SPHO_HEADER ${SPHO_HEADER_DIR}/ctx.h ${SPHO_HEADER_DIR}/err.h - ${SPHO_HEADER_DIR}/loc.h ${SPHO_HEADER_DIR}/scope.h ${SPHO_HEADER_DIR}/tp.h + ${SPHO_HEADER_DIR}/bind.h ${SPHO_HEADER_DIR}/spho.h ) @@ -33,6 +33,7 @@ set(SPHO_SRC ${SRC_DIR}/spho/ctx.c ${SRC_DIR}/spho/scope.c ${SRC_DIR}/spho/tp.c + ${SRC_DIR}/spho/bind.c ) check_symbol_exists(strlcpy "string.h" HAVE_STRLCPY) diff --git a/example/non-parse/ex6.msph b/example/non-parse/ex6.msph new file mode 100644 index 0000000..afdeccb --- /dev/null +++ b/example/non-parse/ex6.msph @@ -0,0 +1,21 @@ +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/include/spho/bind.h b/include/spho/bind.h new file mode 100644 index 0000000..7d2ae06 --- /dev/null +++ b/include/spho/bind.h @@ -0,0 +1,29 @@ +#ifndef _SPHO_BIND_H +#define _SPHO_BIND_H + +#include + +#include "spho/scope.h" + +struct spho_binding { + struct spho_nom *nom; + struct spho_tp *tp; + + STAILQ_ENTRY(spho_binding) entries; +}; + +struct spho_bind { + STAILQ_HEAD(spho_binding_l, spho_binding) head; + + struct spho_ctx *ctx; + struct spho_bind *parent; +}; + + +struct spho_bind *spho_bind_create(struct spho_ctx *, struct spho_bind *); + +int spho_bind_add(struct spho_bind *, struct spho_nom *, struct spho_tp *); + +void spho_bind_destroy(struct spho_bind *); + +#endif diff --git a/include/spho/scope.h b/include/spho/scope.h index 843b554..3d6b02a 100644 --- a/include/spho/scope.h +++ b/include/spho/scope.h @@ -7,40 +7,22 @@ #define SPHO_NOM_LEN 128 +/* name */ struct spho_nom { char s[SPHO_NOM_LEN]; - SLIST_ENTRY(spho_nom) next; + SLIST_ENTRY(spho_nom) next; // TODO change to allocs }; 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! */ - -struct spho_var { - struct spho_nom nom; - - STAILQ_ENTRY(spho_var) next; -}; - -STAILQ_HEAD(spho_var_l, spho_var); - -struct spho_bind { - struct spho_nom nom; - struct spho_tpop *op; -}; - -struct spho_tpop { - struct spho_var_l params; - struct spho_tp *def; -}; - -struct spho_rec { - struct spho_nom mnom; - struct spho_tp *tp; -}; - /* type data */ struct tp_binop_data { struct spho_tp *left; @@ -90,7 +72,7 @@ union tp_data { struct spho_tp { struct spho_scope *sc; - int form; + int kind; union tp_data d; STAILQ_ENTRY(spho_tp) entries; @@ -116,6 +98,9 @@ TAILQ_HEAD(spho_tp_alloc_l, spho_tp_alloc); SLIST_HEAD(spho_scope_l, spho_scope); +/* defined in spho/bind.h */ +struct spho_bind; + struct spho_scope { struct spho_ctx *ctx; struct spho_scope *parent; @@ -124,6 +109,8 @@ struct spho_scope { struct spho_nom_l noms; struct spho_tp_alloc_l tps; + struct spho_bind *bind; + SLIST_ENTRY(spho_scope) next; }; diff --git a/include/spho/tp.h b/include/spho/tp.h index 5395d76..ab2e945 100644 --- a/include/spho/tp.h +++ b/include/spho/tp.h @@ -12,20 +12,21 @@ #define SPHO_TP_FORM_BOX 0x14 #define SPHO_TP_FORM_FORALL 0x15 #define SPHO_TP_FORM_APPL 0x16 +#define SPHO_TP_FORM_MEMBER 0x17 #define SPHO_TP_FORM_TRUE 0x20 #define SPHO_TP_FORM_FALSE 0x21 -#define SPHO_TP_FORM_NOM 0x23 +#define SPHO_TP_FORM_NAME 0x23 -#define SPHO_TP_FORM_MEMBER 0x24 +#define SPHO_TP_FORM_MASK 0xff -// #define SPHO_TP_FORM_SUB 0x96 +#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_ERR(tp, err) SPHO_ERR((tp)->sc->ctx, (err)) -//struct spho_var *spho_var_create(struct spho_scope *, char *, size_t); -//struct spho_var *spho_var_get(struct spho_scope *, char *, size_t); - struct spho_tp *spho_tp_create_conj(struct spho_scope *, struct spho_tp *, struct spho_tp *); struct spho_tp *spho_tp_create_disj(struct spho_scope *, struct spho_tp *, @@ -45,10 +46,8 @@ struct spho_tp *spho_tp_create_appl(struct spho_scope *, struct spho_nom *, struct spho_tp_l *); struct spho_tp *spho_tp_create_member(struct spho_scope *, struct spho_nom *, struct spho_tp *); -//struct spho_tp *spho_tp_create_const(struct spho_scope *, struct spho_const *); -// struct spho_tp *spho_tp_create_var(struct spho_scope *, struct spho_var *); -// struct spho_tp *spho_tp_create_sub(struct spho_scope *, struct spho_tp *, -// struct spho_tp *); +struct spho_tp *spho_tp_create_var(struct spho_scope *, struct spho_nom *); +struct spho_tp *spho_tp_create_nominal(struct spho_scope *, struct spho_nom *); void spho_tp_destroy(struct spho_tp *); diff --git a/src/spho/bind.c b/src/spho/bind.c new file mode 100644 index 0000000..6578aa6 --- /dev/null +++ b/src/spho/bind.c @@ -0,0 +1,40 @@ +#include + +#include "spho/ctx.h" +#include "spho/bind.h" + +struct spho_bind * +spho_bind_create(struct spho_ctx *ctx, struct spho_bind *parent) +{ + struct spho_bind *bind; + + if ((bind = malloc(sizeof(*bind))) == NULL) { + SPHO_ERR(ctx, SPHO_ERR_SYS); + return (NULL); + } + + STAILQ_INIT(&bind->head); + bind->ctx = ctx; + bind->parent = parent; + + return (bind); +} + +int +spho_bind_add(struct spho_bind *bind, struct spho_nom *nom, struct spho_tp *tp) +{ + 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); +} + diff --git a/src/spho/scope.c b/src/spho/scope.c index 442834c..2d91d5f 100644 --- a/src/spho/scope.c +++ b/src/spho/scope.c @@ -16,12 +16,14 @@ int 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); SLIST_INIT(&sc->noms); TAILQ_INIT(&sc->tps); - sc->ctx = ctx; - sc->parent = p; + sc->bind = NULL; return (0); } diff --git a/src/spho/tp.c b/src/spho/tp.c index 6f73d47..d6e5f2e 100644 --- a/src/spho/tp.c +++ b/src/spho/tp.c @@ -10,13 +10,6 @@ const struct tp_konst_data tp_konst_true = { TP_KONST_KEY_TRUE, "True" }; const struct tp_konst_data tp_konst_false = { TP_KONST_KEY_FALSE, "False" }; -//struct spho_tp * -//spho_tp_create_disj(struct spho_ctx *, struct spho_tp *, struct spho_tp *, -// struct spho_tp *) -//{ -// -//} - static struct spho_tp * spho_tp_alloc(struct spho_scope *sc) { @@ -56,7 +49,7 @@ spho_tp_create_conj(struct spho_scope *sc, struct spho_tp *ltp, if ((tp = spho_tp_alloc(sc)) == NULL) return (NULL); - tp->form = SPHO_TP_FORM_CONJ; + tp->kind = SPHO_TP_FORM_CONJ; tp->d.binop.left = ltp; tp->d.binop.right = rtp; @@ -72,7 +65,7 @@ spho_tp_create_disj(struct spho_scope *sc, struct spho_tp *ltp, if ((tp = spho_tp_alloc(sc)) == NULL) return (NULL); - tp->form = SPHO_TP_FORM_DISJ; + tp->kind = SPHO_TP_FORM_DISJ; tp->d.binop.left = ltp; tp->d.binop.right = rtp; @@ -88,7 +81,7 @@ spho_tp_create_impl(struct spho_scope *sc, struct spho_tp *ltp, if ((tp = spho_tp_alloc(sc)) == NULL) return (NULL); - tp->form = SPHO_TP_FORM_IMPL; + tp->kind = SPHO_TP_FORM_IMPL; tp->d.binop.left = ltp; tp->d.binop.right = rtp; @@ -104,7 +97,7 @@ spho_tp_create_arrow(struct spho_scope *sc, struct spho_tp *ltp, if ((tp = spho_tp_alloc(sc)) == NULL) return (NULL); - tp->form = SPHO_TP_FORM_ARROW; + tp->kind = SPHO_TP_FORM_ARROW; tp->d.binop.left = ltp; tp->d.binop.right = rtp; @@ -119,7 +112,7 @@ spho_tp_create_box(struct spho_scope *sc, struct spho_tp *inner) if ((tp = spho_tp_alloc(sc)) == NULL) return (NULL); - tp->form = SPHO_TP_FORM_BOX; + tp->kind = SPHO_TP_FORM_BOX; tp->d.unop.operand = inner; return (tp); @@ -134,7 +127,7 @@ spho_tp_create_forall(struct spho_scope *sc, struct spho_nom *nom, if ((ret = spho_tp_alloc(sc)) == NULL) return (NULL); - ret->form = SPHO_TP_FORM_FORALL; + ret->kind = SPHO_TP_FORM_FORALL; ret->d.bind.nom = nom; ret->d.bind.bound = tp; @@ -149,7 +142,7 @@ spho_tp_create_true(struct spho_scope *sc) if ((ret = spho_tp_alloc(sc)) == NULL) return (NULL); - ret->form = SPHO_TP_FORM_TRUE; + ret->kind = SPHO_TP_FORM_TRUE; ret->d.konst = tp_konst_true; return (ret); @@ -163,7 +156,7 @@ spho_tp_create_false(struct spho_scope *sc) if ((ret = spho_tp_alloc(sc)) == NULL) return (NULL); - ret->form = SPHO_TP_FORM_FALSE; + ret->kind = SPHO_TP_FORM_FALSE; ret->d.konst = tp_konst_false; return (ret); @@ -177,7 +170,7 @@ spho_tp_create_name(struct spho_scope *sc, struct spho_nom *nom) if ((ret = spho_tp_alloc(sc)) == NULL) return (NULL); - ret->form = SPHO_TP_FORM_NOM; + ret->kind = SPHO_TP_FORM_NAME; ret->d.nom.nom = nom; return (ret); @@ -192,7 +185,7 @@ spho_tp_create_appl(struct spho_scope *sc, struct spho_nom *nom, if ((ret = spho_tp_alloc(sc)) == NULL) return (NULL); - ret->form = SPHO_TP_FORM_APPL; + ret->kind = SPHO_TP_FORM_APPL; ret->d.appl.nom = nom; ret->d.appl.args = args; @@ -208,7 +201,7 @@ spho_tp_create_member(struct spho_scope *sc, struct spho_nom *nom, if ((ret = spho_tp_alloc(sc)) == NULL) return (NULL); - ret->form = SPHO_TP_FORM_MEMBER; + ret->kind = SPHO_TP_FORM_MEMBER; ret->d.bind.nom = nom; ret->d.bind.bound = tp; @@ -221,10 +214,10 @@ spho_tp_destroy(struct spho_tp *tp) { struct spho_tp *arg; - switch (tp->form) { + switch (tp->kind & SPHO_TP_FORM_MASK) { case SPHO_TP_FORM_TRUE: case SPHO_TP_FORM_FALSE: - case SPHO_TP_FORM_NOM: + case SPHO_TP_FORM_NAME: break; case SPHO_TP_FORM_CONJ: case SPHO_TP_FORM_DISJ: