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

broken code, but added attempt at writing grammar

Browse source
This commit is contained in:
Ellen Arvidsson 2025-04-14 17:40:22 +02:00
parent fb95e5d026
commit 20e3757f44
18 changed files with 1145 additions and 142 deletions
Download patch file Download diff file Expand all files Collapse all files

2
.gitignore vendored
View file

@ -52,7 +52,7 @@ Mkfile.old
dkms.conf
# CMake build directory
build/
build-*/
# vim

30
CMakeLists.txt
View file

@ -4,27 +4,55 @@ project(log-e-sappho C)
set(CMAKE_C_STANDARD 99)
set(CMAKE_C_STANDARD_REQUIRED True)
include(CheckSymbolExists)
set(INCLUDE_DIR include)
set(SRC_DIR src)
set(SPHO_HEADER_DIR ${INCLUDE_DIR}/spho)
set(SPHO_HEADER
${SPHO_HEADER_DIR}/ctx.h
${SPHO_HEADER_DIR}/data.h
${SPHO_HEADER_DIR}/err.h
${SPHO_HEADER_DIR}/loc.h
${SPHO_HEADER_DIR}/parse.h
${SPHO_HEADER_DIR}/spho.h
${SPHO_HEADER_DIR}/scope.h
${SPHO_HEADER_DIR}/tp.h
${SPHO_HEADER_DIR}/spho.h
)
set(SPHO_SRC
${SRC_DIR}/spho/ctx.c
${SRC_DIR}/spho/scope.c
${SRC_DIR}/spho/tp.c
)
check_symbol_exists(strlcpy "string.h" HAVE_STRLCPY)
add_library(spho STATIC ${SPHO_HEADER} ${SPHO_SRC})
target_include_directories(spho PRIVATE ${INCLUDE_DIR})
target_compile_definitions(spho PRIVATE
$<$<CONFIG:Debug>:SPHO_DEBUG>
$<$<BOOL:${HAVE_STRLCPY}>:SPHO_USE_STRLCPY>
)
add_executable(devcheck ${SRC_DIR}/run/devcheck.c)
target_link_libraries(devcheck spho)
target_include_directories(devcheck PRIVATE ${INCLUDE_DIR})
target_compile_definitions(devcheck PRIVATE
$<$<CONFIG:Debug>:SPHO_DEBUG>
)
set(MSPH_SRC
${SRC_DIR}/msph/msph_token.c
${SRC_DIR}/msph/msph.c
)
set(MSPH_HEADER
${SRC_DIR}/msph/msph_token.h
)
add_executable(msph ${MSPH_HEADER} ${MSPH_SRC})
target_include_directories(spho PRIVATE ${INCLUDE_DIR})

19
include/spho/ctx.h
View file

@ -1,28 +1,31 @@
#ifndef _SPHO_CTX_H
#define _SPHO_CTX_H
#include "spho/data.h"
#include "spho/err.h"
#include "spho/scope.h"
#define SPHO_ERR_BUF_LEN 2048
#define SPHO_ERR_FILEBUF_LEN 128
struct spho_ctx {
struct spho_scope glob;
int err;
int err_info;
struct spho_nom_l noms;
struct spho_const_l cnsts;
char errbuf[SPHO_ERR_BUF_LEN];
#ifdef SPHO_DEBUG
char filebuf[SPHO_ERR_FILEBUF_LEN];
int errline;
#else
char errbuf[SPHO_ERR_BUF_LEN];
char filebuf[SPHO_ERR_FILEBUF_LEN];
int errline;
#endif
};
struct spho_ctx *spho_ctx_create(void);
void spho_ctx_destroy(struct spho_ctx *);
const char *spho_ctx_strerror(struct spho_ctx *);
struct spho_nom *spho_nom_add(struct spho_ctx *, char *, size_t);
struct spho_nom *spho_nom_get(struct spho_ctx *, char *, size_t);
#endif

32
include/spho/data.h
View file

@ -1,36 +1,12 @@
#ifndef _SPHO_DATA_H
#define _SPHO_DATA_H
#include <sys/queue.h>
struct spho_name {
char str[128];
};
struct spho_var {
struct spho_name name;
};
struct spho_cnst {
struct spho_name name;
};
struct spho_nom {
struct spho_name name;
char s[128];
SLIST_ENTRY(spho_nom) next;
};
struct spho_nom_le {
struct spho_nom nom;
SLIST_ENTRY(spho_nom_le) next;
};
struct spho_cnst_le {
struct spho_cnst cnst;
SLIST_ENTRY(spho_cnst_le) next;
};
SLIST_HEAD(spho_nom_l, spho_nom);
SLIST_HEAD(spho_nom_l, spho_nom_le);
SLIST_HEAD(spho_const_l, spho_cnst_le);
#endif
#endif /* _SPHO_DATA_H */

90
include/spho/err.h
View file

@ -1,32 +1,40 @@
#ifndef _SPHO_ERR_H
#define _SPHO_ERR_H
#define SPHO_ERR_SYSTEM 0x000001
#include <errno.h>
#define SPHO_ERR_INTERNAL 0x010001
#ifdef SPHO_DEBUG
#include <stdio.h>
#endif
#define SPHO_ERR_IS_SYSERR(err) (SPHO_ERR_SYSTEM == err)
#define SPHO_ERR_SYS 0x000001
#define SPHO_ERR_INTERNAL 0x010001
#define SPHO_ERR_TOOBIG 0x010002
#define SPHO_ERR_ARGINVAL 0x010003
#define SPHO_ERR_NAMEINUSE 0x010004
#define SPHO_ERR_IS_SYSERR(err) (SPHO_ERR_SYS == err)
#ifdef SPHO_DEBUG
#define SPHO_ERR(ctx, err) \
#define SPHO_ERR(ctx, e) \
do { \
ctx->err = err; \
if (err == SPHO_ERR_SYSTEM) \
ctx->err_info = errno; \
snprintf(ctx->filebuf, sizeof(ctx->filebuf), "%s", \
(ctx)->err = (e); \
if ((e) == SPHO_ERR_SYS) \
(ctx)->err_info = errno; \
snprintf((ctx)->filebuf, sizeof((ctx)->filebuf), \
__FILE__); \
ctx->filebuf[sizeof(ctx->filebuf) - 1] = '\0'; \
ctx->errline = __LINE__; \
(ctx)->errline = __LINE__; \
} while (0)
#else /* SPHO_DEBUG */
#define SPHO_ERR(ctx, err) \
#define SPHO_ERR(ctx, e) \
do { \
ctx->err = err; \
if (err == SPHO_ERR_SYSTEM) \
ctx->err_info = errno; \
(ctx)->err = (e); \
if ((e) == SPHO_ERR_SYS) \
(ctx)->err_info = errno; \
} while (0)
#endif /* SPHO_DEBUG */
@ -34,30 +42,40 @@
/* debug stuff */
#ifdef SPHO_DEBUG
/* PRECOND/ASSERT/POSTCOND */
#define SPHO_PRECOND(cond) do { \
if (! (cond) ) { \
fprintf(stderr, "SPHO_PRECOND(" #cond ")@" __FILE__ ":" __LINE__ \
" failed. Aborting."); \
abort(); \
} \
} while (0)
#define SPHO_STRINGIFY(a) #a
#define SPHO_MACRO_STR(b) SPHO_STRINGIFY(b)
#define SPHO_ASSERT(cond) do { \
if (! (cond) ) { \
fprintf(stderr, "SPHO_ASSERT(" #cond ")@" __FILE__ ":" __LINE__ \
" failed. Aborting."); \
abort(); \
} \
} while (0)
#define __LINE__S SPHO_MACRO_STR(__LINE__)
#define SPHO_POSTCOND(cond) do { \
if (! (cond) ) { \
fprintf(stderr, "SPHO_POSTCOND(" #cond ")@" __FILE__ ":" __LINE__ \
" failed. Aborting."); \
abort(); \
} \
} while (0)
#define SPHO_PRECOND(cond) \
do { \
if (! (cond) ) { \
fprintf(stderr, "SPHO_PRECOND(" #cond ")@" \
__FILE__ ":" __LINE__S \
" failed. Aborting.\n"); \
abort(); \
} \
} while (0)
#define SPHO_ASSERT(cond) \
do { \
if (! (cond) ) { \
fprintf(stderr, "SPHO_ASSERT(" #cond ")@" \
__FILE__ ":" __LINE__S \
" failed. Aborting.\n"); \
abort(); \
} \
} while (0)
#define SPHO_POSTCOND(cond) \
do { \
if (! (cond) ) { \
fprintf(stderr, "SPHO_POSTCOND(" #cond ")@" \
__FILE__ ":" __LINE__S \
" failed. Aborting.\n"); \
abort(); \
} \
} while (0)
#else
#define SPHO_PRECOND(cond)

2
include/spho/loc.h
View file

@ -31,4 +31,4 @@ struct spho_loc *spho_loc_create_line(struct spho_ctx *, char *, int);
struct spho_loc *spho_loc_create_linecol(struct spho_ctx *, char *, int, int);
void spho_loc_destroy(struct spho_loc *);
#endif
#endif

34
include/spho/scope.h Normal file
View file

@ -0,0 +1,34 @@
#ifndef _SPHO_SCOPE_H
#define _SPHO_SCOPE_H
#include "spho/data.h"
SLIST_HEAD(spho_scope_l, spho_scope);
struct spho_scope {
struct spho_ctx *ctx;
struct spho_scope *parent;
struct spho_scope_l subs;
struct spho_nom_l noms;
SLIST_ENTRY(spho_scope) next;
};
#define SPHO_SC_ERR(sc, err) SPHO_ERR((sc)->ctx, (err))
int spho_scope_init(struct spho_scope *, struct spho_ctx *,
struct spho_scope *);
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 *);
#endif /* _SPHO_SCOPE_H */

2
include/spho/spho.h
View file

@ -1,6 +1,8 @@
#ifndef _SPHO_SPHO_H
#define _SPHO_SPHO_H
#include <sys/queue.h>
#include "spho/err.h"
#include "spho/ctx.h"

123
include/spho/tp.h
View file

@ -3,13 +3,42 @@
/* base defs */
struct spho_alias {
struct spho_name name;
struct spho_tp *tp;
#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_name mname;
struct spho_nom mnom;
struct spho_tp *tp;
};
@ -20,21 +49,21 @@ struct tp_bin_data {
};
struct tp_box_data {
struct spho_tp *tp;
struct spho_tp *inr;
};
struct tp_forall_data {
struct spho_var *var;
struct spho_tp *tp;
struct spho_tp *inr;
};
struct tp_alias_data {
struct spho_alias *alias;
struct spho_tp_list *l;
struct tp_bappl_data {
struct spho_bind *bind;
struct spho_tp_l *args;
};
struct tp_const_data {
struct spho_const *c;
struct tp_konst_data {
const struct spho_konst *k;
};
struct tp_var_data {
@ -54,8 +83,8 @@ union tp_data {
struct tp_bin_data binop;
struct tp_box_data box;
struct tp_forall_data fa;
struct tp_alias_data alias;
struct tp_const_data cnst;
struct tp_bappl_data bappl;
struct tp_konst_data konst;
struct tp_var_data var;
struct tp_nominal_data nom;
struct tp_record_data rec;
@ -67,8 +96,9 @@ union tp_data {
#define SPHO_TP_FORM_CONJ 0x11
#define SPHO_TP_FORM_IMPL 0x12
#define SPHO_TP_FORM_BOX 0x13
#define SPHO_TP_FORM_FORALL 0x14
#define SPHO_TP_FORM_ALIAS 0x15
#define SPHO_TP_FORM_ARROW 0x14
#define SPHO_TP_FORM_FORALL 0x15
#define SPHO_TP_FORM_BAPPL 0x16
#define SPHO_TP_FORM_FALSE 0x20
#define SPHO_TP_FORM_TRUE 0x21
@ -77,43 +107,48 @@ union tp_data {
#define SPHO_TP_FORM_REC 0x23
// TODO explain
#define SPHO_TP_FORM_SUB 0x96
// #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 {
int form;
union tp_data data;
struct spho_scope *sc;
int form;
union tp_data data;
STAILQ_ENTRY(spho_tp) next;
};
struct spho_nom *spho_nom_add(struct spho_ctx *, char *, size_t);
struct spho_nom *spho_nom_get_or_add(struct spho_ctx *, char *, size_t);
// struct spho_nom *spho_tp_nom_get(char *, size_t);
STAILQ_HEAD(spho_tp_l, spho_tp);
struct spho_var *spho_var_create(struct spho_ctx *, char *, size_t);
struct spho_var *spho_var_get(struct spho_ctx *, char *, size_t);
#define SPHO_TP_ERR(tp, err) SPHO_ERR((tp)->sc->ctx, (err))
struct spho_alias *spho_alias_add(struct spho_ctx *, char *, size_t);
struct spho_alias *spho_alias_get(struct spho_ctx *, 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_ctx *, struct spho_tp *,
struct spho_tp *, struct spho_tp *);
struct spho_tp *spho_tp_create_conj(struct spho_ctx *, struct spho_tp *,
struct spho_tp *, struct spho_tp *);
struct spho_tp *spho_tp_create_impl(struct spho_ctx *, struct spho_tp *,
struct spho_tp *, struct spho_tp *);
struct spho_tp *spho_tp_create_box(struct spho_ctx *, struct spho_tp *,
struct spho_tp *);
struct spho_tp *spho_tp_create_forall(struct spho_ctx *, struct spho_name *,
struct spho_tp *);
struct spho_tp *spho_tp_create_alias(struct spho_ctx *, struct spho_alias *,
struct spho_tp *);
struct spho_tp *spho_tp_create_const(struct spho_ctx *, struct spho_const *);
struct spho_tp *spho_tp_create_nominal(struct spho_ctx *,
struct spho_nom *);
struct spho_tp *spho_tp_create_var(struct spho_ctx *, struct spho_var *);
struct spho_tp *spho_tp_create_record(struct spho_ctx *, struct spho_rec *);
//struct spho_tp *spho_tp_create_sub(struct spho_ctx *, struct spho_tp *,
//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_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 *);
void spho_tp_destroy(struct spho_tp*);

18
include/spho/util.h Normal file
View file

@ -0,0 +1,18 @@
#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)
#endif

93
src/msph/README.md Normal file
View file

@ -0,0 +1,93 @@
# msph/micro sappho
Micro sappho is a minimalistic language for demonstration of the SPHO type
system. It is implemented using a simple parser and lexer that implements the
grammar below. The indended use is to allow experimentation and familiarization
with the SPHO types and subtyping.
## Grammar
Grammar in pseudo-bnf
```
MSph ::= Body
Body ::= Dirs
Dir ::= Typedef (directives, with lack of a better name)
| Memberdef
| Nominaldecl
| Checkdir
Typedef ::= 'type' Name '=' TExpr (type definition/binding)
| 'type' Name '[' Names ']' '=' TExpr
| 'type' Name (declaration, donno if useful)
Memberdef ::= 'member' Name ':' TExpr
Nominaldecl ::= 'nominal' Name
Checkdir ::= 'check' TExpr '<:' TExpr
TExpr ::= 'True'
| 'False'
| Var
| Nominal
| Trait
| TExpr '&' TExpr
| TExpr '|' TExpr
| TExpr '=>' TExpr
| TExpr '->' TExpr
| 'box' TExpr
| 'forall' Name '.' TExpr
| '(' TExpr ')'
Trait ::= '{' Body '}' (trait, this introduces scoping)
Var ::= Name (type variables)
Nominal ::= Name (nominal type)
Name ::= '[a-zA-Z0-9_]+' & !Reserved (name/identifier)
Reserved ::= 'type' (reserved/keywords)
| 'member'
| 'nominal'
| 'check'
| 'forall'
| 'box'
| 'True'
| 'False'
```
Precedence of binary operators:
'&' <
'|' <
'->' <
'=>'
< means "binds closer"
## Example
A simple example msph program
```
nominal ExampleN
type ExampleDecl
type ExampleDecl2
type Example = {
member example_m : C -> C
type FA = forall X. X -> X
type b = forall X. (box X => ExampleDecl) => ExampleDecl2
}
member example_global : Example & ExampleN
type TripleConj[X, Y, Z] = X & Y & Z
```

40
src/msph/msph.c Normal file
View file

@ -0,0 +1,40 @@
#include <stdio.h>
#include "msph_token.h"
#define PRINTERR(ctx) \
do { \
fprintf(stderr, "msph_err: %d (%d)\n", (ctx).err, (ctx).err_info); \
} while (0)
int
main(int argc, char **argv)
{
int ret;
char *path;
struct msph_ctx ctx;
struct msph_token_stream *s;
if (argc != 2)
return (-1);
path = argv[1];
ctx.err = 0;
ctx.err_info = 0;
if ((s = msph_token_stream_fopen(&ctx, path)) == NULL) {
PRINTERR(ctx);
return (-1);
}
ret = msph_token_stream_close(s);
return (ret);
}

247
src/msph/msph_token.c Normal file
View file

@ -0,0 +1,247 @@
#include <sys/errno.h>
#include <stdlib.h>
#include <stdio.h>
#include <string.h>
#include "spho/err.h"
#define MSPH_ERR_SYS 0x0001
#define MSPH_ERR_TOOLONG 0x0002
#define MSPH_ERR(ctx, e) SPHO_ERR(ctx, e)
#define MSPH_TOKS_ERR(toks, e) MSPH_ERR((toks)->ctx, e)
struct msph_token_stream *
msph_token_stream_fopen(struct msph_ctx *ctx, const char *path)
{
FILE *f;
size_t res;
struct msph_token_stream *ret;
if ((f = fopen(path, "r")) == NULL) {
MSPH_ERR(ctx, MSPH_ERR_SYS);
return (NULL);
}
if ((ret = calloc(1, sizeof(struct msph_token_stream))) == NULL) {
MSPH_ERR(ctx, MSPH_ERR_SYS);
goto err;
}
ret->ctx = ctx;
ret->src.type = MSPH_TOKEN_SRC_FILE;
ret->src.inner.file.f = f;
ret->src.inner.file.eof = 0;
ret->src.inner.file.pos = ret->src.file.buf;
ret->src.inner.file.end = ret->src.file.buf;
ret->src.inner.file.read_ptr = ret->src.file.buf;
res = strlcpy(ret->src.file.name, path, sizeof(ret->src.file.name));
if (res >= sizeof(ret->src.file.name)) {
MSPH_ERR(ctx, MSPH_ERR_TOOLONG);
goto err;
}
return (ret);
err:
if (fclose(f) == EOF)
abort();
if (ret != NULL)
free(ret);
return (NULL);
}
struct msph_token_stream *
msph_token_stream_frombuf(struct msph_ctx *ctx, const char *buf, size_t len)
{
struct msph_token_stream *ret;
if ((ret = calloc(1, sizeof(struct msph_token_stream))) == NULL) {
MSPH_ERR(ctx, MSPH_ERR_SYS);
return (NULL);
}
ret->ctx = ctx;
ret->type = MSPH_TOKEN_SRC_STR;
ret->src.str.s = buf;
ret->src.str.len = len;
ret->src.str.pos = 0;
return (ret);
}
int
msph_token_stream_close(struct msph_token_stream *s)
{
int ret;
ret = -1;
switch (s->type) {
case MSPH_TOKEN_SRC_FILE:
ret = fclose(s->src.file.f);
break;
case MSPH_TOKEN_SRC_STR:
ret = 0;
break;
default:
break;
}
return (ret);
}
/* -1 or num tokens read */
ssize_t
msph_token_stream_read_tok(struct msph_token *ptr, size_t n,
struct msph_token_stream *s)
{
ssize_t ret;
size_t i;
int res;
ret = 0;
res = -1;
while ((res = read_single_tok(&ptr[i], s)) == 1) {
if (res == -1) {
ret = -1;
break;
}
ret++;
}
return (ret);
}
struct msph_token_matcher {
size_t pos_off;
size_t matchlen;
const int tok_type;
} msph_matcher[] = {
{ 0, 0, TOK_START },
{ 0, 0, TOK_IDENT },
{ 0, 0, TOK_END }
};
#define BUF_LEN(b) (sizeof(b) / sizeof(b[0]))
static int
file_char_at(struct msph_ctx *ctx, struct msph_token_src *src, size_t i,
char *out)
{
size_t nread;
size_t maxread;
struct msph_token_src_file *file;
ret = -1;
file = &src->inner.file;
if (file->pos + i < file->end) {
*out = file->buf[file->pos + i];
return (0);
}
if (file->end < file->pos &&
((file->pos + i) % BUF_LEN(file->buf)) < file->end) {
*out = file->buf[(file->pos + i) % BUF_LEN(file->buf)];
return (0);
}
if (file->eof) {
return (-1);
}
if (file->end < file->pos)
maxread = file->pos - file->end;
else
maxread = BUF_LEN(file->buf) - file->end;
maxread = file->end < file->pos ? file->pos - file->end :
BUF_LEN(file->buf) - file->end;
if (maxread == 0) {
MSPH_ERR(ctx, MSPH_ERR_TOOLONG);
return (-1);
}
ret = fread(&file->buf[file->end], sizeof(file->buf[0]), maxread,
file->f);
if (ret == 0) {
if (ferror(file->f)) {
MSPH_ERR(ctx, MSPH_ERR_SYS);
return (-1);
}
file->eof = 1;
return (-1);
}
}
static int
char_at(struct msph_token_src *src, size_t i, char *out)
{
int ret;
switch (src->type) {
case MSPH_TOKEN_SRC_FILE:
ret = file_char_at(s, i, out);
break;
case MSPH_TOKEN_SRC_STR:
ret = str_char_at(s, i, out);
break;
default:
break;
}
return (ret);
}
static int
tok_match(struct msph_token_matcher *m, struct msph_token_stream *s)
{
}
static void
tok_commit(struct msph_token *ptr, struct msph_token_stream *s,
struct msph_matcher *m)
{
SPHO_PRECOND(p != NULL && m != NULL);
SPHO_PRECOND(m->matchlen != 0);
}
/* 1: success, 0: failed match, -1: error */
static int
read_single_tok(struct msph_token *ptr, struct msph_token_stream *s)
{
int res;
size_t m;
size_t max_m;
max_m = 0;
for (m = 0; msph_matcher[m].type != TOK_END; m++) {
res = tok_match(&msph_matcher[m], s);
if (res == -1)
return (-1);
if (res == 0 &&
msph_matcher[m].matchlen > msph_matcher[max_m].matchlen) {
max_m = m;
}
}
if (max_m == 0)
return (0);
tok_commit(ptr, &msph_matcher[max_m]);
return (1);
}

179
src/msph/msph_token.h Normal file
View file

@ -0,0 +1,179 @@
#ifndef _MSPH_EXPR_H
#define _MSPH_EXPR_H
/*
* TYPES:
* Conj
* Disj
* Impl
* Arrow
* Box
* (Sub)
* Forall
*
* True
* False
* Var
* Nominal
*
* Record
*
* DEFINITIONS/DIRECTIVES:
* Type definition (type A[X..] = T)
* Nominal definition (nominal N)
* Member definition (member mname : T)
*
* {
* member a: A
* member b: B
* }
*
* Subtyping check (check A <: B, checks if A <: B)
*
* EXTRA DEFINITIONS
* Class definition (class C[...] { ... }, shorthand)
*
* EXPRESSIONS
* Conj
* Disj
* Impl
* Arrow
* Box
* (Sub)
* Forall
*
* True
* False
* Var
* Nominal
*
* Trait ({ ... }, creates scoping)
*
*
* TOKENS
* lbrace {
* rbrace }
* lbrak [
* rbrak ]
* lparen (
* rparen )
* colon :
* equals =
*
* op_and &
* op_or |
* op_impl =>
* op_sub <:
*
* kw_type type
* kw_nominal nominal
* kw_member member
* kw_check check
* kw_box box
* kw_forall forall
*
* k_true True
* k_false False
*
* ident C, anid, ...
*
*/
struct msph_ctx {
int err;
int err_info;
};
enum msph_tok_type {
TOK_START,
TOK_LBRACE, // {
TOK_RBRACE, // }
TOK_LBRAK, // [
TOK_RBRAK, // ]
TOK_LPAREN, // (
TOK_RPAREN, // )
TOK_OP_COLON, // :
TOK_OP_EQUALS, // =
TOK_OP_AMP, // &
TOK_OP_PIPE, // |
TOK_OP_RARROW, // =>
TOK_OP_SUB, // <:
TOK_KW_TYPE, // type
TOK_KW_NOMINAL, // nominal
TOK_KW_MEMBER, // member
TOK_KW_CHECK, // check
TOK_KW_BOX, // box
TOK_KW_FORALL, // forall
TOK_CONST_TRUE, // True
TOK_CONST_FALSE, // False
TOK_IDENT, // identifiers
TOK_END
};
#define MSPH_TOKEN_BUF_SZ 128
struct token_s {
char buf[MSPH_TOKEN_BUF_SZ];
};
union token_data {
struct token_s s;
};
struct msph_token {
int type;
union token_data d;
};
#define MSPH_PATH_LEN 1024
#define MSPH_FILE_BUF_LEN 4096
#define MSPH_TOKEN_SRC_FILE 1
struct msph_token_src_file {
FILE *f;
int eof;
size_t pos; // TODO rename bufpos
size_t end; // TODO rename bufend
size_t read_pos;
char buf[MSPH_FILE_BUF_LEN];
char name[MSPH_PATH_LEN];
};
#define MSPH_TOKEN_SRC_STR 2
struct msph_token_src_str {
const char *s;
size_t len;
size_t pos;
};
union msph_token_src_data {
struct msph_token_src_file file;
struct msph_token_src_str str;
};
struct msph_token_src {
int type
union msph_token_src_data inner;
};
struct msph_token_stream {
struct msph_ctx *ctx;
struct msph_token_src src;
};
struct msph_token_stream *msph_token_stream_fopen(struct msph_ctx *,
const char *);
struct msph_token_stream *msph_token_stream_frombuf(struct msph_ctx *,
const char *, size_t);
int msph_token_stream_close(struct msph_token_stream*);
struct msph_token *msph_token_source_pop(struct msph_token_stream *);
#endif /* _MSPH_EXPR_H */

2
src/run/devcheck.c
View file

@ -11,7 +11,7 @@ int main(void)
if ((ctx = spho_ctx_create()) == NULL)
return (-1);
spho_ctx_destroy(ctx);
return (0);

33
src/spho/ctx.c
View file

@ -4,7 +4,6 @@
#include <stdlib.h>
#include <string.h>
#include "spho/err.h"
#include "spho/ctx.h"
static const char *spho_ctx_sys_strerror(struct spho_ctx *);
@ -16,8 +15,11 @@ struct spho_err {
};
struct spho_err spho_errmsgs[] = {
{ SPHO_ERR_SYSTEM, "spho system error" },
{ SPHO_ERR_INTERNAL, "spho internal error" },
{ SPHO_ERR_SYS, "spho system error" },
{ SPHO_ERR_INTERNAL, "spho internal error" },
{ SPHO_ERR_TOOBIG, "parameter size too big" },
{ SPHO_ERR_ARGINVAL, "invalid argument" },
{ SPHO_ERR_NAMEINUSE, "name in use" },
{ -1, NULL }
};
@ -26,14 +28,20 @@ spho_ctx_create(void)
{
struct spho_ctx *c;
c = NULL;
if ((c = malloc(sizeof(struct spho_ctx))) == NULL)
return (NULL);
c->err = 0;
c->err_info = 0;
SLIST_INIT(&c->noms);
SLIST_INIT(&c->cnsts);
if (spho_scope_init(&c->glob, c, NULL) == -1) {
free(c);
return (NULL);
}
SPHO_POSTCOND(c != NULL);
return (c);
}
@ -41,22 +49,11 @@ spho_ctx_create(void)
void
spho_ctx_destroy(struct spho_ctx *ctx)
{
struct spho_nom_le *nom;
struct spho_cnst_le *cnst;
SPHO_PRECOND(ctx != NULL);
while (! SLIST_EMPTY(&ctx->noms)) {
nom = SLIST_FIRST(&ctx->noms);
SLIST_REMOVE_HEAD(&ctx->noms, next);
free(nom);
}
spho_scope_term(&ctx->glob);
while (! SLIST_EMPTY(&ctx->cnsts)) {
cnst = SLIST_FIRST(&ctx->cnsts);
SLIST_REMOVE_HEAD(&ctx->cnsts, next);
free(cnst);
}
free(ctx);
}

156
src/spho/scope.c Normal file
View file

@ -0,0 +1,156 @@
#include <sys/queue.h>
#include <stdlib.h>
#include <string.h>
#include "spho/ctx.h"
#include "spho/scope.h"
#include "spho/util.h"
static void spho_nom_term(struct spho_nom *);
int
spho_scope_init(struct spho_scope *sc, struct spho_ctx *ctx,
struct spho_scope *p)
{
SLIST_INIT(&sc->subs);
SLIST_INIT(&sc->noms);
sc->parent = p;
return (0);
}
void
spho_scope_term(struct spho_scope *sc)
{
SPHO_UTIL_SLIST_DESTROY(&sc->subs, spho_scope, next, spho_scope_term);
SPHO_UTIL_SLIST_DESTROY(&sc->noms, spho_nom, next, spho_nom_term);
sc->parent = NULL;
}
struct spho_scope *
spho_scope_global(struct spho_ctx *ctx)
{
SPHO_PRECOND(ctx != NULL);
return (&ctx->glob);
}
struct spho_scope *
spho_scope_create(struct spho_scope *sc)
{
struct spho_scope *sub;
if ((sub = malloc(sizeof(struct spho_scope))) == NULL) {
SPHO_ERR(sc->ctx, SPHO_ERR_SYS);
return (NULL);
}
if (spho_scope_init(sub, sc->ctx, sc) == -1) {
free(sub);
return (NULL);
}
SLIST_INSERT_HEAD(&sc->subs, sub, next);
return (sub);
}
static void
spho_nom_term(struct spho_nom *nom)
{
return;
}
void
spho_scope_destroy(struct spho_scope *sc)
{
struct spho_scope *sub;
struct spho_scope *p;
p = sc->parent;
SLIST_REMOVE(&p->subs, sc, spho_scope, next);
spho_scope_term(sc);
free(sc);
}
struct spho_nom *
spho_scope_nom_add(struct spho_scope *sc, const char *nomstr, size_t sz)
{
#ifdef SPHO_USE_STRLCPY
size_t res;
#else
ssize_t res;
#endif
struct spho_nom *nom;
if (spho_scope_nom_get(sc, nomstr, sz, &nom) == -1)
return (NULL);
if (nom != NULL) {
SPHO_SC_ERR(sc, SPHO_ERR_NAMEINUSE);
return (NULL);
}
if ((nom = malloc(sizeof(struct spho_nom))) == NULL) {
SPHO_SC_ERR(sc, SPHO_ERR_SYS);
return (NULL);
}
#ifdef SPHO_USE_STRLCPY
res = strlcpy(nom->s, nomstr, sizeof(nom->s));
if (res >= sizeof(nom->s)) {
SPHO_SC_ERR(sc, SPHO_ERR_TOOBIG);
goto err;
}
#else
res = snprintf(nom->s, sizeof(nom->s), "%s", nomstr);
if (res < 0) {
SPHO_SC_ERR(sc, SPHO_ERR_SYS);
goto err;
}
if (res >= (ssize_t)sizeof(nom->s)) {
SPHO_SC_ERR(sc, SPHO_ERR_TOOBIG);
goto err;
}
#endif
SLIST_INSERT_HEAD(&sc->noms, nom, next);
return (nom);
err:
free(nom);
return (NULL);
}
int
spho_scope_nom_get(struct spho_scope *sc, const char *nomstr, size_t sz,
struct spho_nom **out)
{
struct spho_nom *nom;
nom = NULL;
if (sz > sizeof(nom->s)) {
SPHO_ERR(sc->ctx, SPHO_ERR_TOOBIG);
return (-1);
}
out = NULL;
SLIST_FOREACH(nom, &sc->noms, next) {
if (strncmp(nom->s, nomstr, sz) == 0) {
*out = nom;
break;
}
}
return (0);
}

185
src/spho/tp.c
View file

@ -1,9 +1,11 @@
#include <sys/queue.h>
#include <stdlib.h>
#include "spho/ctx.h"
#include "spho/scope.h"
#include "spho/tp.h"
struct spho_nom *
spho_nom_add(struct spho_ctx *ctx, char *nom, size_t nomlen)
{
}
//struct spho_tp *
//spho_tp_create_disj(struct spho_ctx *, struct spho_tp *, struct spho_tp *,
@ -11,3 +13,178 @@ spho_nom_add(struct spho_ctx *ctx, char *nom, size_t nomlen)
//{
//
//}
struct spho_tp *
spho_tp_alloc(struct spho_scope *sc, int form)
{
struct spho_tp *tp;
SPHO_PRECOND(SPHO_TP_FORM_IS_VALID(form));
if ((tp = calloc(1, sizeof(struct spho_tp))) == NULL) {
SPHO_SC_ERR(sc, SPHO_ERR_SYS);
return (NULL);
}
tp->sc = sc;
tp->form = form;
return (tp);
}
int
spho_tp_init_disj(struct spho_tp *tp, struct spho_tp *a, struct spho_tp *b)
{
if (tp->form != SPHO_TP_FORM_DISJ) {
SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
return (-1);
}
tp->data.binop.left = a;
tp->data.binop.right = b;
return (0);
}
int
spho_tp_init_conj(struct spho_tp *tp, struct spho_tp *a, struct spho_tp *b)
{
if (tp->form != SPHO_TP_FORM_CONJ) {
SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
return (-1);
}
tp->data.binop.left = a;
tp->data.binop.right = b;
return (0);
}
int
spho_tp_init_impl(struct spho_tp *tp, struct spho_tp *a, struct spho_tp *b)
{
if (tp->form != SPHO_TP_FORM_IMPL) {
SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
return (-1);
}
tp->data.binop.left = a;
tp->data.binop.right = b;
return (0);
}
int
spho_tp_init_arrow(struct spho_tp *tp, struct spho_tp *a, struct spho_tp *b)
{
if (tp->form != SPHO_TP_FORM_ARROW) {
SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
return (-1);
}
tp->data.binop.left = a;
tp->data.binop.right = b;
return (0);
}
int
spho_tp_init_box(struct spho_tp *tp, struct spho_tp *inr)
{
if (tp->form != SPHO_TP_FORM_BOX) {
SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
return (-1);
}
tp->data.box.inr = inr;
return (0);
}
int
spho_tp_init_forall(struct spho_tp *tp, struct spho_var *var,
struct spho_tp *inr)
{
if (tp->form != SPHO_TP_FORM_FORALL) {
SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
return (-1);
}
tp->data.fa.var = var;
tp->data.fa.inr = inr;
return (0);
}
int
spho_tp_init_bappl(struct spho_tp *tp, struct spho_bind *bind,
struct spho_tp_l *args)
{
struct spho_tp *arg;
if (tp->form != SPHO_TP_FORM_BAPPL) {
SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
return (-1);
}
tp->data.bappl.bind = bind;
tp->data.bappl.args = args;
return (0);
}
int
spho_tp_init_false(struct spho_tp *tp)
{
if (tp->form != SPHO_TP_FORM_FALSE) {
SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
return (-1);
}
tp->data.konst.k = SPHO_K_FALSE;
return (0);
}
int
spho_tp_init_true(struct spho_tp *tp)
{
if (tp->form != SPHO_TP_FORM_TRUE) {
SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
return (-1);
}
tp->data.konst.k = SPHO_K_TRUE;
return (0);
}
int
spho_tp_init_var(struct spho_tp *tp, struct spho_var *var)
{
if (tp->form != SPHO_TP_FORM_VAR) {
SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
return (-1);
}
tp->data.var.v = var;
return (0);
}
int
spho_tp_init_rec(struct spho_tp *tp, struct spho_rec *rec)
{
if (tp->form != SPHO_TP_FORM_REC) {
SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
return (-1);
}
tp->data.rec.r = rec;
return (0);
}