lnsol/log-e-sappho
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

sphophi decorating with types

Browse source
This commit is contained in:
Ellen Arvidsson 2025-05-01 18:16:10 +02:00
parent 17be15d7b5
commit a22c9726cd
19 changed files with 1762 additions and 380 deletions
Download patch file Download diff file Expand all files Collapse all files

3
include/msph/common.h
View file

@ -2,6 +2,7 @@
#define _MSPH_COMMON_H
#include "msph/err.h"
#include "spho/ctx.h"
#define MSPH_IDENT_LEN 128
#define MSPH_NAME_LEN 1024
@ -11,6 +12,8 @@ struct msph_ctx {
int err_info;
char errbuf[SPHO_ERR_BUF_LEN];
struct spho_ctx *spho;
#ifdef SPHO_DEBUG
char filebuf[SPHO_ERR_FILEBUF_LEN];
int errline;

33
include/msph/decor.h Normal file
View file

@ -0,0 +1,33 @@
#ifndef _MSPH_DECOR_H
#define _MSPH_DECOR_H
struct msph_tp_decor {
struct spho_tp *tp;
};
#define TP_DECOR_INIT(ptr) \
do { \
(ptr)->tp = NULL; \
} while (0)
struct msph_scope_decor {
struct spho_scope *sc;
};
#define SCOPE_DECOR_INIT(ptr) \
do { \
(ptr)->sc = NULL; \
} while (0)
struct msph_nom_decor {
struct spho_nom *nom;
};
#define NOM_DECOR_INIT(ptr) \
do { \
(ptr)->nom = NULL; \
} while (0)
#define GET_SCOPE(ptr) ((ptr)->dec.sc)
#endif /* _MSPH_DECOR_H */

4
include/msph/err.h
View file

@ -17,6 +17,10 @@
#define MSPH_ERR_TREE_EOF 0x2002
#define MSPH_ERR_TREE_NOMATCH 0x2003
#define MSPH_ERR_TYPE_INVAL 0x3001
#define MSPH_ERR_SPHOPHI 0x10001
// TODO add more diagnostics

15
include/msph/sphophi.h Normal file
View file

@ -0,0 +1,15 @@
#ifndef _MSPH_TYPE_H
#define _MSPH_TYPE_H
#include "msph/tree.h"
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(struct msph_tree_root *);
int msph_sphoxex(struct msph_tree_root *);
#endif

63
include/msph/tree.h
View file

@ -5,6 +5,7 @@
#include "msph/common.h"
#include "msph/token.h"
#include "msph/decor.h"
/*
* TYPES:
@ -99,7 +100,7 @@ struct msph_tree_ident;
struct msph_tree_tpexpr;
struct msph_tree_root {
struct msph_tree tr;
struct msph_tree htr;
struct msph_ctx *ctx;
@ -107,145 +108,154 @@ struct msph_tree_root {
};
struct msph_tree_unit {
struct msph_tree tr;
struct msph_tree htr;
char name[MSPH_NAME_LEN];
struct msph_tree_body *body;
struct msph_scope_decor dec;
STAILQ_ENTRY(msph_tree_unit) entries;
};
struct msph_tree_text {
struct msph_tree tr;
struct msph_tree htr;
struct msph_text_pos pos;
};
struct msph_tree_body {
struct msph_tree tr;
struct msph_tree htr;
STAILQ_HEAD(msph_tree_dir_l, msph_tree_dir) head;
};
struct msph_tree_dir {
struct msph_tree tr;
struct msph_tree_text htxt;
STAILQ_ENTRY(msph_tree_dir) entries;
};
struct msph_tree_tpdef {
struct msph_tree_dir dir;
struct msph_tree_dir hdir;
struct msph_tree_ident *id;
struct msph_tree_tpexpr *tp;
};
struct msph_tree_nomindecl {
struct msph_tree_dir dir;
struct msph_tree_dir hdir;
struct msph_tree_ident *id;
};
struct msph_tree_membdecl {
struct msph_tree_dir dir;
struct msph_tree_dir hdir;
struct msph_tree_ident *id;
struct msph_tree_tpexpr *tp;
};
struct msph_tree_assert {
struct msph_tree_dir dir;
struct msph_tree_dir hdir;
struct msph_tree_tpexpr *ltp;
struct msph_tree_tpexpr *rtp;
};
struct msph_tree_tpexpr {
struct msph_tree tr;
struct msph_tree_text htxt;
STAILQ_ENTRY(msph_tree_tpexpr) entries;
struct msph_tp_decor dec;
};
struct msph_tree_true {
struct msph_tree_tpexpr tp;
struct msph_tree_tpexpr htpe;
};
struct msph_tree_false {
struct msph_tree_tpexpr tp;
struct msph_tree_tpexpr htpe;
};
struct msph_tree_name {
struct msph_tree_tpexpr tp;
struct msph_tree_tpexpr htpe;
struct msph_tree_ident *id;
};
struct msph_tree_appl {
struct msph_tree_tpexpr tp;
struct msph_tree_tpexpr htpe;
struct msph_tree_ident *id;
STAILQ_HEAD(msph_tree_tpexpr_l, msph_tree_tpexpr) head;
};
struct msph_tree_trait {
struct msph_tree_tpexpr tp;
struct msph_tree_tpexpr htpe;
struct msph_tree_body *body;
struct msph_scope_decor dec;
};
struct msph_tree_conj {
struct msph_tree_tpexpr tp;
struct msph_tree_tpexpr htpe;
struct msph_tree_tpexpr *ltp;
struct msph_tree_tpexpr *rtp;
};
struct msph_tree_disj {
struct msph_tree_tpexpr tp;
struct msph_tree_tpexpr htpe;
struct msph_tree_tpexpr *ltp;
struct msph_tree_tpexpr *rtp;
};
struct msph_tree_impl {
struct msph_tree_tpexpr tp;
struct msph_tree_tpexpr htpe;
struct msph_tree_tpexpr *ltp;
struct msph_tree_tpexpr *rtp;
};
struct msph_tree_arrow {
struct msph_tree_tpexpr tp;
struct msph_tree_tpexpr htpe;
struct msph_tree_tpexpr *ltp;
struct msph_tree_tpexpr *rtp;
};
struct msph_tree_box {
struct msph_tree_tpexpr tp;
struct msph_tree_tpexpr htpe;
struct msph_tree_tpexpr *inner;
};
struct msph_tree_forall {
struct msph_tree_tpexpr tp;
struct msph_tree_tpexpr htpe;
struct msph_tree_ident *ident;
struct msph_tree_ident *id;
struct msph_tree_tpexpr *inner;
struct msph_scope_decor dec;
};
struct msph_tree_paren {
struct msph_tree_tpexpr tp;
struct msph_tree_tpexpr htpe;
struct msph_tree_tpexpr *inner;
};
struct msph_tree_ident {
struct msph_tree tr;
struct msph_tree_text htxt;
char str[MSPH_IDENT_LEN];
STAILQ_ENTRY(msph_tree_ident) entries;
};
struct msph_nom_decor dec;
};
struct msph_tree_root *msph_tree_makeroot(struct msph_ctx *);
@ -254,4 +264,7 @@ int msph_tree_parse(struct msph_token_stream *, struct msph_tree_root *);
ssize_t msph_tree_fprint(FILE *, struct msph_tree *);
#define T(ptr) ((struct msph_tree *)ptr)
#define TXT(ptr) ((struct msph_tree_text *)ptr)
#endif

12
include/spho/data.h
View file

@ -1,12 +0,0 @@
#ifndef _SPHO_DATA_H
#define _SPHO_DATA_H
struct spho_nom {
char s[128];
SLIST_ENTRY(spho_nom) next;
};
SLIST_HEAD(spho_nom_l, spho_nom);
#endif /* _SPHO_DATA_H */

3
include/spho/err.h
View file

@ -12,7 +12,8 @@
#define SPHO_ERR_INTERNAL 0x010001
#define SPHO_ERR_TOOBIG 0x010002
#define SPHO_ERR_ARGINVAL 0x010003
#define SPHO_ERR_NAMEINUSE 0x010004
#define SPHO_ERR_NOM_INUSE 0x020001
#define SPHO_ERR_NOM_NOTINSCOPE 0x020002
#define SPHO_ERR_IS_SYSERR(err) (SPHO_ERR_SYS == err)

7
include/spho/parse.h
View file

@ -1,7 +0,0 @@
#ifndef _SPHO_PARSE_H
#define _SPHO_PARSE_H
#endif

118
include/spho/scope.h
View file

@ -1,7 +1,118 @@
#ifndef _SPHO_SCOPE_H
#define _SPHO_SCOPE_H
#include "spho/data.h"
#include <sys/queue.h>
#include <stdlib.h>
#define SPHO_NOM_LEN 128
struct spho_nom {
char s[SPHO_NOM_LEN];
SLIST_ENTRY(spho_nom) next;
};
SLIST_HEAD(spho_nom_l, spho_nom);
#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;
struct spho_tp *right;
};
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;
};
struct tp_appl_data {
struct spho_nom *nom;
struct spho_tp_l *args;
};
struct tp_konst_data {
int key;
const char *str;
};
extern const struct tp_konst_data tp_konst_true;
extern const struct tp_konst_data tp_konst_false;
#define SPHO_K_TRUE (&tp_konst_true)
#define SPHO_K_FALSE (&tp_konst_false)
/* type data union */
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;
};
/* sappho type */
struct spho_tp {
struct spho_scope *sc;
int form;
union tp_data d;
STAILQ_ENTRY(spho_tp) entries;
};
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 {
struct spho_tp tp;
TAILQ_ENTRY(spho_tp_alloc) allocs;
};
TAILQ_HEAD(spho_tp_alloc_l, spho_tp_alloc);
SLIST_HEAD(spho_scope_l, spho_scope);
@ -11,6 +122,7 @@ struct spho_scope {
struct spho_scope_l subs;
struct spho_nom_l noms;
struct spho_tp_alloc_l tps;
SLIST_ENTRY(spho_scope) next;
};
@ -24,11 +136,13 @@ void spho_scope_term(struct spho_scope *);
struct spho_scope *spho_scope_global(struct spho_ctx *);
struct spho_scope *spho_scope_create(struct spho_scope *);
void spho_scope_destroy(struct spho_scope *);
struct spho_nom *spho_scope_nom_add(struct spho_scope *, const char *, size_t);
int spho_scope_nom_get(struct spho_scope *, const char *, size_t,
struct spho_nom **);
// int spho_scope_nom_del(struct spho_nom *);
int spho_scope_nom_lookup(struct spho_scope *, const char *, size_t,
struct spho_nom **);
#endif /* _SPHO_SCOPE_H */

171
include/spho/tp.h
View file

@ -1,160 +1,55 @@
#ifndef _SPHO_TP_H
#define _SPHO_TP_H
/* base defs */
#define SPHO_KONST_S_SZ 128
#define SPHO_KONST_K_TRUE 0x43445 /* don't change!!!!! */
#define SPHO_KONST_K_FALSE 0x66a57 /* don't change!1! */
struct spho_konst {
const char *s;
int k;
};
const struct spho_konst SPHO_K_TRUE_V = { "True", SPHO_KONST_K_TRUE };
const struct spho_konst SPHO_K_FALSE_V = { "False", SPHO_KONST_K_FALSE };
#define SPHO_K_TRUE (&SPHO_K_TRUE_V)
#define SPHO_K_FALSE (&SPHO_K_FALSE_V)
struct spho_var {
struct spho_nom nom;
STAILQ_ENTRY(spho_var) next;
};
STAILQ_HEAD(spho_var_l, spho_var);
struct spho_bind {
struct spho_nom nom;
struct spho_tpop *op;
};
struct spho_tpop {
struct spho_var_l params;
struct spho_tp *def;
};
struct spho_rec {
struct spho_nom mnom;
struct spho_tp *tp;
};
/* type data */
struct tp_bin_data {
struct spho_tp *left;
struct spho_tp *right;
};
struct tp_box_data {
struct spho_tp *inr;
};
struct tp_forall_data {
struct spho_var *var;
struct spho_tp *inr;
};
struct tp_bappl_data {
struct spho_bind *bind;
struct spho_tp_l *args;
};
struct tp_konst_data {
const struct spho_konst *k;
};
struct tp_var_data {
struct spho_var *v;
};
struct tp_nominal_data {
struct spho_nom *n;
};
struct tp_record_data {
struct spho_rec *r;
};
/* type data union */
union tp_data {
struct tp_bin_data binop;
struct tp_box_data box;
struct tp_forall_data fa;
struct tp_bappl_data bappl;
struct tp_konst_data konst;
struct tp_var_data var;
struct tp_nominal_data nom; // XXX
struct tp_record_data rec;
};
#include "spho/scope.h"
#define SPHO_TP_FORM_UNKNOWN 0x00
#define SPHO_TP_FORM_DISJ 0x10
#define SPHO_TP_FORM_CONJ 0x11
#define SPHO_TP_FORM_CONJ 0x10
#define SPHO_TP_FORM_DISJ 0x11
#define SPHO_TP_FORM_IMPL 0x12
#define SPHO_TP_FORM_BOX 0x13
#define SPHO_TP_FORM_ARROW 0x14
#define SPHO_TP_FORM_ARROW 0x13
#define SPHO_TP_FORM_BOX 0x14
#define SPHO_TP_FORM_FORALL 0x15
#define SPHO_TP_FORM_BAPPL 0x16
#define SPHO_TP_FORM_APPL 0x16
#define SPHO_TP_FORM_FALSE 0x20
#define SPHO_TP_FORM_TRUE 0x21
#define SPHO_TP_FORM_VAR 0x22
#define SPHO_TP_FORM_TRUE 0x20
#define SPHO_TP_FORM_FALSE 0x21
#define SPHO_TP_FORM_NOM 0x23
#define SPHO_TP_FORM_REC 0x23
#define SPHO_TP_FORM_MEMBER 0x24
// #define SPHO_TP_FORM_SUB 0x96
#define SPHO_TP_FORM_IS_VALID(f) \
(f) >= SPHO_TP_FORM_DISJ && (f) <= SPHO_TP_FORM_BAPPL || \
(f) >= SPHO_TP_FORM_FALSE && (f) <= SPHO_TP_FORM_NOM || \
(f) == SPHO_TP_FORM_REC
/* sappho type */
struct spho_tp {
struct spho_scope *sc;
int form;
union tp_data data;
STAILQ_ENTRY(spho_tp) next;
};
STAILQ_HEAD(spho_tp_l, spho_tp);
#define SPHO_TP_ERR(tp, err) SPHO_ERR((tp)->sc->ctx, (err))
struct spho_var *spho_var_create(struct spho_scope *, char *, size_t);
struct spho_var *spho_var_get(struct spho_scope *, char *, size_t);
//struct spho_var *spho_var_create(struct spho_scope *, char *, size_t);
//struct spho_var *spho_var_get(struct spho_scope *, char *, size_t);
//struct spho_tp *spho_tp_create_disj(struct spho_scope *, struct spho_tp *,
// struct spho_tp *, struct spho_tp *);
//struct spho_tp *spho_tp_create_conj(struct spho_scope *, struct spho_tp *,
// struct spho_tp *, struct spho_tp *);
//struct spho_tp *spho_tp_create_impl(struct spho_scope *, struct spho_tp *,
// struct spho_tp *, struct spho_tp *);
//struct spho_tp *spho_tp_create_box(struct spho_scope *, struct spho_tp *,
// struct spho_tp *);
//struct spho_tp *spho_tp_create_arrow(struct spho_scope *, struct spho_tp *,
// struct spho_tp *);
//struct spho_tp *spho_tp_create_forall(struct spho_scope *, struct spho_name *,
// struct spho_tp *);
struct spho_tp *spho_tp_create_conj(struct spho_scope *, struct spho_tp *,
struct spho_tp *);
struct spho_tp *spho_tp_create_disj(struct spho_scope *, struct spho_tp *,
struct spho_tp *);
struct spho_tp *spho_tp_create_impl(struct spho_scope *, struct spho_tp *,
struct spho_tp *);
struct spho_tp *spho_tp_create_arrow(struct spho_scope *, struct spho_tp *,
struct spho_tp *);
struct spho_tp *spho_tp_create_box(struct spho_scope *, struct spho_tp *);
struct spho_tp *spho_tp_create_forall(struct spho_scope *, struct spho_nom *,
struct spho_tp *);
struct spho_tp *spho_tp_create_true(struct spho_scope *);
struct spho_tp *spho_tp_create_false(struct spho_scope *);
struct spho_tp *spho_tp_create_name(struct spho_scope *,
struct spho_nom *);
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_nominal(struct spho_scope *,
// struct spho_nom *);
//struct spho_tp *spho_tp_create_var(struct spho_scope *, struct spho_var *);
//struct spho_tp *spho_tp_create_record(struct spho_scope *, struct spho_rec *);
//struct spho_tp *spho_tp_create_sub(struct spho_scope *, struct spho_tp *,
// struct spho_tp *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 *);
void spho_tp_destroy(struct spho_tp*);
void spho_tp_free(struct spho_tp *);
void spho_tp_destroy(struct spho_tp *);
#endif