diff --git a/.clangd b/.clangd new file mode 100644 index 0000000..ba4cbb3 --- /dev/null +++ b/.clangd @@ -0,0 +1,2 @@ +Diagnostics: + UnusedIncludes: None diff --git a/.gitignore b/.gitignore index dd51cb4..75a6986 100644 --- a/.gitignore +++ b/.gitignore @@ -51,9 +51,11 @@ Module.symvers Mkfile.old dkms.conf -# CMake build directory -build/ +# CMake build dirs +build-*/ +# CMake compile commands +compile_commands.json # vim .*.swp diff --git a/CMakeLists.txt b/CMakeLists.txt index 573a310..466a3d9 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -3,6 +3,17 @@ project(log-e-sappho C) 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") +set(CMAKE_VERBOSE_MAKEFILE ON) + +set(CMAKE_EXPORT_COMPILE_COMMANDS ON) + + +include(CheckSymbolExists) set(INCLUDE_DIR include) set(SRC_DIR src) @@ -10,21 +21,56 @@ 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 + $<$:SPHO_DEBUG> + $<$: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 + $<$:SPHO_DEBUG> +) + + +set(MSPH_SRC + ${SRC_DIR}/msph/token.c + ${SRC_DIR}/msph/tree.c + ${SRC_DIR}/msph/msph.c +) + +set(MSPH_HEADER + ${INCLUDE_DIR}/msph/token.h + ${INCLUDE_DIR}/msph/tree.h + ${INCLUDE_DIR}/msph/common.h + ${INCLUDE_DIR}/msph/err.h +) + +add_executable(msph ${MSPH_SRC} ${MSPH_HEADER}) +target_include_directories(msph PRIVATE ${INCLUDE_DIR}) +target_link_libraries(msph spho) +target_compile_definitions(msph PRIVATE + $<$:SPHO_DEBUG> + $<$:SPHO_USE_STRLCPY> +) diff --git a/example/ex1.msph b/example/ex1.msph new file mode 100644 index 0000000..0844c3f --- /dev/null +++ b/example/ex1.msph @@ -0,0 +1,4 @@ + +nominal C + + diff --git a/example/ex2.msph b/example/ex2.msph new file mode 100644 index 0000000..5b85fdc --- /dev/null +++ b/example/ex2.msph @@ -0,0 +1 @@ +type A = & C D diff --git a/example/ex3.msph b/example/ex3.msph new file mode 100644 index 0000000..9770336 --- /dev/null +++ b/example/ex3.msph @@ -0,0 +1,13 @@ + +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/include/msph/common.h b/include/msph/common.h new file mode 100644 index 0000000..43a6a6f --- /dev/null +++ b/include/msph/common.h @@ -0,0 +1,25 @@ +#ifndef _MSPH_COMMON_H +#define _MSPH_COMMON_H + +#include "msph/err.h" + +#define MSPH_IDENT_LEN 128 +#define MSPH_NAME_LEN 1024 + +struct msph_ctx { + int err; + int err_info; + char errbuf[SPHO_ERR_BUF_LEN]; + +#ifdef SPHO_DEBUG + char filebuf[SPHO_ERR_FILEBUF_LEN]; + int errline; +#endif +}; + +struct msph_text_pos { + unsigned int line; + unsigned int col; +}; + +#endif diff --git a/include/msph/err.h b/include/msph/err.h new file mode 100644 index 0000000..bf113d5 --- /dev/null +++ b/include/msph/err.h @@ -0,0 +1,36 @@ +#ifndef _MSPH_ERR_H +#define _MSPH_ERR_H + +#include "spho/err.h" + + +#define MSPH_ERR_SYS 0x0001 +#define MSPH_ERR_INVAL 0x0002 +#define MSPH_ERR_TOOLONG 0x0003 + +#define MSPH_ERR_TOKEN_TOOLONG 0x1001 +#define MSPH_ERR_TOKEN_EOF 0x1002 +#define MSPH_ERR_TOKEN_NOMATCH 0x1003 +#define MSPH_ERR_TOKEN_INVAL 0x1004 + +#define MSPH_ERR_TREE_TOOLONG 0x2001 +#define MSPH_ERR_TREE_EOF 0x2002 +#define MSPH_ERR_TREE_NOMATCH 0x2003 + + +// TODO add more diagnostics + +#define MSPH_ERR(ctx, e) SPHO_ERR(ctx, e) +#define MSPH_TOKS_ERR(toks, e) MSPH_ERR((toks)->ctx, e) + +#define MSPH_ERR_INFO(ctx, e, info) SPHO_ERR_INFO(ctx, e, info) + + +#define MSPH_ERR_RESET(ctx) \ + do { \ + ctx->err = 0; \ + ctx->err_info = 0; \ + } while (0) + + +#endif diff --git a/include/msph/token.h b/include/msph/token.h new file mode 100644 index 0000000..b984039 --- /dev/null +++ b/include/msph/token.h @@ -0,0 +1,146 @@ +#ifndef _MSPH_EXPR_H +#define _MSPH_EXPR_H + +#include + +#include "msph/common.h" + +/* + * + * + * 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, ... + * + */ + + +enum msph_tok_type { + TOK_LBRACE, // { + TOK_RBRACE, // } + TOK_LBRAK, // [ + TOK_RBRAK, // ] + TOK_LPAREN, // ( + TOK_RPAREN, // ) + TOK_COLON, // : + TOK_EQUALS, // = + TOK_COMMA, // , + TOK_DOT, // . + + TOK_AMP, // & + TOK_PIPE, // | + TOK_IMPL, // => + TOK_RARROW, // -> + TOK_SUB, // <: + + TOK_KW_TYPE, // type + TOK_KW_NOMINAL, // nominal + TOK_KW_MEMBER, // member + TOK_KW_ASSERT, // assert + TOK_KW_BOX, // box + TOK_KW_FORALL, // forall + + TOK_CONST_TRUE, // True + 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 +}; + +#define MSPH_TAB_WIDTH 8 + +union msph_token_data { + char str[MSPH_IDENT_LEN]; +}; + +struct msph_token { + int type; + struct msph_text_pos pos; + union msph_token_data data; + + SLIST_ENTRY(msph_token) entries; +}; + +#define MSPH_FILE_NAME_LEN 1024 +#define MSPH_FILE_BUF_LEN 2048 +#define MSPH_TOKEN_SRC_FILE 1 + +struct msph_token_src_file { + FILE *f; + + /* circular buffer for reading */ + size_t pos; + size_t end; + char buf[MSPH_FILE_BUF_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; + struct msph_text_pos pos; + union msph_token_src_data inner; +}; + +struct msph_token_stream { + struct msph_ctx *ctx; + + char name[MSPH_NAME_LEN]; + struct msph_token_src src; +}; + +void msph_ctx_init(struct msph_ctx *); + +struct msph_token_stream *msph_token_stream_file(struct msph_ctx *, + const char *, FILE *); +struct msph_token_stream *msph_token_stream_frombuf(struct msph_ctx *, + const char *, const char *, size_t); + +int msph_token_stream_close(struct msph_token_stream*); + +ssize_t msph_token_stream_read(struct msph_token *, size_t, + struct msph_token_stream *); +int msph_token_stream_eof(struct msph_token_stream *); +int msph_token_stream_print(struct msph_token_stream *, FILE *); + +ssize_t msph_token_str(char *, size_t, struct msph_token *); + +struct msph_token * msph_token_copy(struct msph_ctx *, struct msph_token *); + + +#endif /* _MSPH_EXPR_H */ diff --git a/include/msph/tree.h b/include/msph/tree.h new file mode 100644 index 0000000..22cc883 --- /dev/null +++ b/include/msph/tree.h @@ -0,0 +1,257 @@ +#ifndef _MSPH_TREE_H +#define _MSPH_TREE_H + +#include + +#include "msph/common.h" +#include "msph/token.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 assert (assert A <: B, asserts that A <: B) + * + * EXTRA DEFINITIONS + * Class definition (class C[...] { ... }, shorthand) + * + * EXPRESSIONS + * Conj + * Disj + * Impl + * Arrow + * Box + * (Sub) + * Forall + * + * True + * False + * Var + * Nominal + * + * Trait ({ ... }, creates scoping) + */ + +#define MSPH_TREE_ROOT 0x0000 +#define MSPH_TREE_UNIT 0x0001 + +#define MSPH_TREE_BODY 0x0010 + +#define MSPH_TREE_DIR 0x0020 +#define MSPH_TREE_TPDEF 0x0021 +#define MSPH_TREE_NOMINDECL 0x0022 +#define MSPH_TREE_MEMBDECL 0x0023 +#define MSPH_TREE_ASSERT 0x0024 + +#define MSPH_TREE_TPEXPR 0x0040 +#define MSPH_TREE_TRUE 0x0041 +#define MSPH_TREE_FALSE 0x0042 +#define MSPH_TREE_NAME 0x0043 +#define MSPH_TREE_APPL 0x0044 +#define MSPH_TREE_TRAIT 0x0045 +#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_PAREN 0x004c + +#define MSPH_TREE_IDENT 0x0100 + + +struct msph_tree { + int type; + struct msph_tree *parent; +}; + +struct msph_tree_root; +struct msph_tree_text; +struct msph_tree_body; +struct msph_tree_dir; +struct msph_tree_tpdef; +struct msph_tree_nomindecl; +struct msph_tree_assert; +struct msph_tree_ident; +struct msph_tree_tpexpr; + +struct msph_tree_root { + struct msph_tree tr; + + struct msph_ctx *ctx; + + STAILQ_HEAD(msph_tree_unit_l, msph_tree_unit) head; +}; + +struct msph_tree_unit { + struct msph_tree tr; + + char name[MSPH_NAME_LEN]; + struct msph_tree_body *body; + STAILQ_ENTRY(msph_tree_unit) entries; +}; + +struct msph_tree_text { + struct msph_tree tr; + struct msph_text_pos pos; +}; + +struct msph_tree_body { + struct msph_tree tr; + + STAILQ_HEAD(msph_tree_dir_l, msph_tree_dir) head; +}; + +struct msph_tree_dir { + struct msph_tree tr; + + STAILQ_ENTRY(msph_tree_dir) entries; +}; + +struct msph_tree_tpdef { + struct msph_tree_dir dir; + + struct msph_tree_ident *id; + struct msph_tree_tpexpr *tp; +}; + +struct msph_tree_nomindecl { + struct msph_tree_dir dir; + + struct msph_tree_ident *id; +}; + +struct msph_tree_membdecl { + struct msph_tree_dir dir; + + struct msph_tree_ident *id; + struct msph_tree_tpexpr *tp; +}; + +struct msph_tree_assert { + struct msph_tree_dir dir; + + struct msph_tree_tpexpr *ltp; + struct msph_tree_tpexpr *rtp; +}; + +struct msph_tree_tpexpr { + struct msph_tree tr; + + STAILQ_ENTRY(msph_tree_tpexpr) entries; +}; + + +struct msph_tree_true { + struct msph_tree_tpexpr tp; +}; + +struct msph_tree_false { + struct msph_tree_tpexpr tp; +}; + +struct msph_tree_name { + struct msph_tree_tpexpr tp; + + struct msph_tree_ident *id; +}; + +struct msph_tree_appl { + struct msph_tree_tpexpr tp; + + 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_body *body; +}; + +struct msph_tree_conj { + struct msph_tree_tpexpr tp; + + struct msph_tree_tpexpr *ltp; + struct msph_tree_tpexpr *rtp; +}; + +struct msph_tree_disj { + struct msph_tree_tpexpr tp; + + struct msph_tree_tpexpr *ltp; + struct msph_tree_tpexpr *rtp; +}; + +struct msph_tree_impl { + struct msph_tree_tpexpr tp; + + struct msph_tree_tpexpr *ltp; + struct msph_tree_tpexpr *rtp; +}; + +struct msph_tree_arrow { + struct msph_tree_tpexpr tp; + + struct msph_tree_tpexpr *ltp; + struct msph_tree_tpexpr *rtp; +}; + +struct msph_tree_box { + struct msph_tree_tpexpr tp; + + struct msph_tree_tpexpr *inner; +}; + +struct msph_tree_forall { + struct msph_tree_tpexpr tp; + + struct msph_tree_ident *ident; + struct msph_tree_tpexpr *inner; +}; + +struct msph_tree_paren { + struct msph_tree_tpexpr tp; + + struct msph_tree_tpexpr *inner; +}; + +struct msph_tree_ident { + struct msph_tree tr; + + char str[MSPH_IDENT_LEN]; + STAILQ_ENTRY(msph_tree_ident) entries; +}; + + + +struct msph_tree_root *msph_tree_makeroot(struct msph_ctx *); + +int msph_tree_parse(struct msph_token_stream *, struct msph_tree_root *); + +ssize_t msph_tree_fprint(FILE *, struct msph_tree *); + +#endif diff --git a/include/spho/ctx.h b/include/spho/ctx.h index 746126c..9858e85 100644 --- a/include/spho/ctx.h +++ b/include/spho/ctx.h @@ -1,25 +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 *); -char *spho_ctx_strerror(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 diff --git a/include/spho/data.h b/include/spho/data.h index 2050387..0cd02c8 100644 --- a/include/spho/data.h +++ b/include/spho/data.h @@ -1,36 +1,12 @@ #ifndef _SPHO_DATA_H #define _SPHO_DATA_H -#include - -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_const_le { - struct spho_cnst cnst; - SLIST_ENTRY(spho_const_le) next; -}; +SLIST_HEAD(spho_nom_l, spho_nom); -SLIST_HEAD(spho_nom_l, spho_nom_le); -SLIST_HEAD(spho_const_l, spho_const_le); - -#endif +#endif /* _SPHO_DATA_H */ diff --git a/include/spho/err.h b/include/spho/err.h index f92687a..ffde4b0 100644 --- a/include/spho/err.h +++ b/include/spho/err.h @@ -1,67 +1,107 @@ #ifndef _SPHO_ERR_H #define _SPHO_ERR_H -#define SPHO_ERR_SYSTEM 0x000001 +#include -#define SPHO_ERR_INTERNAL 0x010001 +#ifdef SPHO_DEBUG +#include +#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) + +#define SPHO_ERR_BUF_LEN 2048 + +#define SPHO_ERR(ctx, e) \ + do { \ + (ctx)->err = (e); \ + if ((e) == SPHO_ERR_SYS) \ + SPHO_ERR_INFO(ctx, e, errno); \ + else \ + SPHO_ERR_INFO(ctx, e, 0); \ + } while (0) #ifdef SPHO_DEBUG -#define SPHO_ERR(ctx, err) \ +#define SPHO_ERR_FILEBUF_LEN 128 + +#define SPHO_ERR_INFO(ctx, e, info) \ do { \ - ctx->err = err; \ - if (err == SPHO_ERR_SYSTEM) \ - ctx->err_info = errno; \ - snprintf(ctx->filebuf, sizeof(ctx->filebuf), "%s", \ + (ctx)->err = (e); \ + (ctx)->err_info = (info); \ + snprintf((ctx)->filebuf, sizeof((ctx)->filebuf), \ __FILE__); \ - ctx->errline = __LINE__; \ + (ctx)->errline = __LINE__; \ } while (0) +#define SPHO_STRINGIFY(a) #a +#define SPHO_MACRO_STR(b) SPHO_STRINGIFY(b) + +#define __LINE__S SPHO_MACRO_STR(__LINE__) + +#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) + + +#ifdef SPHO_ENABLE_DEBUG_PRINT + +#define SPHO_DEBUG_PRINT(fmt, ...) \ + do { \ + fprintf(stderr, fmt __VA_OPT__(,) __VA_ARGS__); \ + } while (0) + +#else /* SPHO_ENABLE_DEBUG_PRINT */ + +#define SPHO_DEBUG_PRINT(fmt, ...) + +#endif /* SPHO_ENABLE_DEBUG_PRINT */ + #else /* SPHO_DEBUG */ -#define SPHO_ERR(ctx, err) \ +#define SPHO_ERR_INFO(ctx, e, info) \ do { \ - ctx->err = err; \ - if (err == SPHO_ERR_SYSTEM) \ - ctx->err_info = errno; \ + (ctx)->err = (e); \ + (ctx)->err_info = (info); \ } while (0) -#endif /* SPHO_DEBUG */ - -/* 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_ASSERT(cond) do { \ - if (! (cond) ) { \ - fprintf(stderr, "SPHO_ASSERT(" #cond ")@" __FILE__ ":" __LINE__ \ - " failed. Aborting."); \ - abort(); \ - } \ -} while (0) - -#define SPHO_POSTCOND(cond) do { \ - if (! (cond) ) { \ - fprintf(stderr, "SPHO_POSTCOND(" #cond ")@" __FILE__ ":" __LINE__ \ - " failed. Aborting."); \ - abort(); \ - } \ -} while (0) - -#else #define SPHO_PRECOND(cond) #define SPHO_ASSERT(cond) #define SPHO_POSTCOND(cond) -#endif +#define SPHO_DEBUG_PRINT(fmt, ...) -#endif +#endif /* SPHO_DEBUG */ + +#endif /* _SPHO_ERR_H */ diff --git a/include/spho/loc.h b/include/spho/loc.h index 05f6008..bf6e425 100644 --- a/include/spho/loc.h +++ b/include/spho/loc.h @@ -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 \ No newline at end of file +#endif diff --git a/include/spho/scope.h b/include/spho/scope.h new file mode 100644 index 0000000..e0d62ff --- /dev/null +++ b/include/spho/scope.h @@ -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 */ diff --git a/include/spho/spho.h b/include/spho/spho.h index 900444f..f8582dc 100644 --- a/include/spho/spho.h +++ b/include/spho/spho.h @@ -4,29 +4,6 @@ #include #include "spho/err.h" - -#include "spho/data.h" - -#define SPHO_ERR_BUF_LEN 2048 -#define SPHO_ERR_FILEBUF_LEN 128 - -struct spho_ctx { - int err; - int err_info; - - struct spho_nom_l noms; - struct spho_const_l cnsts; - -#ifdef SPHO_DEBUG - char filebuf[SPHO_ERR_FILEBUF_LEN]; - int errline; -#else - char errbuf[SPHO_ERR_BUF_LEN]; -#endif -}; - -struct spho_ctx *spho_ctx_create(void); -void spho_ctx_destroy(struct spho_ctx *); -char *spho_ctx_strerror(struct spho_ctx *); +#include "spho/ctx.h" #endif diff --git a/include/spho/tp.h b/include/spho/tp.h index 0098237..fdbf8bf 100644 --- a/include/spho/tp.h +++ b/include/spho/tp.h @@ -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,10 +83,10 @@ 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_nominal_data nom; // XXX 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,49 @@ 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); -struct spho_alias *spho_alias_add(struct spho_ctx *, char *, size_t); -struct spho_alias *spho_alias_get(struct spho_ctx *, char *, size_t); +#define SPHO_TP_ERR(tp, err) SPHO_ERR((tp)->sc->ctx, (err)) -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_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_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*); diff --git a/include/spho/util.h b/include/spho/util.h new file mode 100644 index 0000000..2cb9681 --- /dev/null +++ b/include/spho/util.h @@ -0,0 +1,25 @@ +#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/README.md b/src/msph/README.md new file mode 100644 index 0000000..19b3857 --- /dev/null +++ b/src/msph/README.md @@ -0,0 +1,105 @@ +# 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 + +And yes, it is ambiguous at places. More specification coming when there is +time. + +``` + +MSph ::= Body + +Body ::= Dirs + +Dir ::= Typedef (directives, with lack of a better name) + | Memberdef + | Nominaldecl + | Assert + +Typedef ::= 'type' Name '=' TExpr (type definition/binding) + | 'type' Name '[' Names ']' '=' TExpr + | 'type' Name (declaration, donno if useful) + +Memberdef ::= 'member' Name ':' TExpr + +Nominaldecl ::= 'nominal' Name + +Assert ::= 'assert' TExpr '<:' TExpr + +TExpr ::= 'True' + | 'False' + | Var + | Nominal + | Trait + | Appl + | 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) +Appl ::= Name '[' TExprs ']' + +Name ::= '[a-zA-Z0-9_]+' & !Reserved (name/identifier) + +Reserved ::= 'type' (reserved/keywords) + | 'member' + | 'nominal' + | 'assert' + | '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 + +assert Example <: ExampleN + +``` + +// A <: B => ... +// == +// box (A => B) => ... + diff --git a/src/msph/msph.c b/src/msph/msph.c new file mode 100644 index 0000000..edc2ed7 --- /dev/null +++ b/src/msph/msph.c @@ -0,0 +1,151 @@ +#include +#include +#include + +#include "msph/err.h" +#include "msph/token.h" +#include "msph/tree.h" + +#define PRINTERR(ctx) \ + do { \ + fprintf(stderr, "msph_err: %x (%d)\n", (ctx).err, \ + (ctx).err_info); \ + } while (0) + +struct msph_opts { + int tokenize_only; + const char *in_path; + const char *out_path; +} run_opts = { + 0, + 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" + + +void +print_usage(void) +{ + printf("%s", USAGE); +} + +int run(struct msph_opts *); + +int +main(int argc, char *argv[]) +{ + int opt; + + while ((opt = getopt(argc, argv, "hto:")) != -1) { + switch (opt) { + case 't': + run_opts.tokenize_only = 1; + break; + case 'o': + run_opts.out_path = optarg; + break; + case 'h': + print_usage(); + exit(EXIT_SUCCESS); + case '?': + default: + print_usage(); + exit(EXIT_FAILURE); + } + } + + argc -= optind; + argv += optind; + + if (argc > 1) { + print_usage(); + exit(EXIT_FAILURE); + } + + if (argc == 1) + run_opts.in_path = argv[0]; + + if (run(&run_opts)) + exit(EXIT_FAILURE); +} + + +int +run(struct msph_opts *opts) +{ + int ret; + struct msph_ctx ctx; + struct msph_token_stream *s; + struct msph_tree_root *root; + FILE *in, *out; + + in = out = NULL; + + msph_ctx_init(&ctx); + + if (opts->in_path == NULL) { + in = stdin; opts->in_path = "stdin"; + } else { + if ((in = fopen(opts->in_path, "r")) == NULL) { + MSPH_ERR(&ctx, MSPH_ERR_SYS); + goto err; + } + } + + if (opts->out_path == NULL) { + out = stdout; + } else { + if ((out = fopen(opts->out_path, "w")) == NULL) { + MSPH_ERR(&ctx, MSPH_ERR_SYS); + goto err; + } + } + + if ((s = msph_token_stream_file(&ctx, opts->in_path, in)) == NULL) { + goto err; + } + + printf("msph v0, parsing %s\n", opts->in_path); + + if (opts->tokenize_only) { + if ((ret = msph_token_stream_print(s, out)) == -1) + goto err; + + goto exit; + } + + if ((root = msph_tree_makeroot(&ctx)) == NULL) { + goto err; + } + + if (msph_tree_parse(s, root) == -1) + goto err; + + printf("msph tree successfully parsed :)\n"); + + if (msph_tree_fprint(out, (struct msph_tree *)root) < 0) + goto err; + +exit: + if (msph_token_stream_close(s) == -1) + goto err; + + return (0); + +err: + PRINTERR(ctx); + + if (in) + fclose(in); + if (out) + fclose(out); + return (-1); +} diff --git a/src/msph/token.c b/src/msph/token.c new file mode 100644 index 0000000..01b5cd7 --- /dev/null +++ b/src/msph/token.c @@ -0,0 +1,784 @@ +#include + +#include +#include +#include +#include + +#include "msph/err.h" +#include "msph/token.h" + +struct msph_matcher { + size_t off; + size_t matchlen; + + const int type; +}; + +struct msph_matcher token_matchers[] = { + { 0, 0, -1 }, + { 0, 0, TOK_LBRACE }, + { 0, 0, TOK_RBRACE }, + { 0, 0, TOK_LBRAK }, + { 0, 0, TOK_RBRAK }, + { 0, 0, TOK_LPAREN }, + { 0, 0, TOK_RPAREN }, + { 0, 0, TOK_COLON }, + { 0, 0, TOK_EQUALS }, + { 0, 0, TOK_COMMA }, + { 0, 0, TOK_DOT }, + + { 0, 0, TOK_AMP }, + { 0, 0, TOK_PIPE }, + { 0, 0, TOK_IMPL }, + { 0, 0, TOK_RARROW }, + { 0, 0, TOK_SUB }, + + { 0, 0, TOK_KW_TYPE }, + { 0, 0, TOK_KW_NOMINAL }, + { 0, 0, TOK_KW_MEMBER }, + { 0, 0, TOK_KW_ASSERT }, + { 0, 0, TOK_KW_BOX }, + { 0, 0, TOK_KW_FORALL }, + + { 0, 0, TOK_CONST_TRUE }, + { 0, 0, TOK_CONST_FALSE }, + + { 0, 0, TOK_IDENT }, + { 0, 0, TOK_END } +}; +struct msph_matcher wspace = { 0, 0, TOK_WSPACE }; + +struct msph_token_info { + const int type; + const char *dbg_str; + const char *str; +} token_info[] = { +#define TOK_INFO(tok, s) { tok , #tok, s } + TOK_INFO(TOK_LBRACE, "{"), + TOK_INFO(TOK_RBRACE, "}"), + TOK_INFO(TOK_LBRAK, "["), + TOK_INFO(TOK_RBRAK, "]"), + TOK_INFO(TOK_LPAREN, "("), + TOK_INFO(TOK_RPAREN, ")"), + TOK_INFO(TOK_COLON, ":"), + TOK_INFO(TOK_EQUALS, "="), + TOK_INFO(TOK_COMMA, ","), + TOK_INFO(TOK_DOT, "."), + + TOK_INFO(TOK_AMP, "&"), + TOK_INFO(TOK_PIPE, "|"), + TOK_INFO(TOK_IMPL, "=>"), + TOK_INFO(TOK_RARROW, "->"), + TOK_INFO(TOK_SUB, "<:"), + + TOK_INFO(TOK_KW_TYPE, "type"), + TOK_INFO(TOK_KW_NOMINAL, "nominal"), + TOK_INFO(TOK_KW_MEMBER, "member"), + TOK_INFO(TOK_KW_ASSERT, "assert"), + TOK_INFO(TOK_KW_BOX, "box"), + TOK_INFO(TOK_KW_FORALL, "forall"), + + TOK_INFO(TOK_CONST_TRUE, "True"), + TOK_INFO(TOK_CONST_FALSE, "False"), + + TOK_INFO(TOK_IDENT, NULL), + { TOK_END , NULL, NULL } +#undef TOK_INFO +}; + + + +#define BUF_LEN(b) ((sizeof(b) / sizeof((b)[0]))) + +static ssize_t src_file_fill_buf(struct msph_ctx *, + struct msph_token_src_file *); +static int tok_match(struct msph_ctx *, struct msph_token_src *, + struct msph_matcher *); +static int tok_commit(struct msph_ctx *, struct msph_token_src *, + struct msph_matcher *, struct msph_token *); +static void tok_update_pos(struct msph_ctx *, struct msph_token_src *, + struct msph_matcher *m); +static int char_at(struct msph_ctx *, struct msph_token_src *, size_t, + char *); +static int fromcbuf_charcpy(char *, const char *, size_t, size_t, size_t); +static int file_char_at(struct msph_ctx *, struct msph_token_src *, size_t, + char *out); +static int read_single_tok(struct msph_token *, struct msph_token_stream *); + + +static const char *tok_base_str(struct msph_token *); + + +void msph_ctx_init(struct msph_ctx *ctx) +{ + ctx->err = 0; + ctx->err_info = 0; +} + +struct msph_token_stream * +msph_token_stream_file(struct msph_ctx *ctx, const char *name, FILE *f) +{ + size_t res; + struct msph_token_stream *ret; + + if (ctx == NULL || f == NULL) { + MSPH_ERR(ctx, MSPH_ERR_INVAL); + return (NULL); + } + + + if ((ret = calloc(1, sizeof(struct msph_token_stream))) == NULL) { + MSPH_ERR(ctx, MSPH_ERR_SYS); + goto err; + } + + ret->ctx = ctx; + if ((res = strlcpy(ret->name, name, BUF_LEN(ret->name))) + >= BUF_LEN(ret->name)) { + MSPH_ERR(ctx, MSPH_ERR_TOOLONG); + goto err; + } + ret->src.type = MSPH_TOKEN_SRC_FILE; + ret->src.pos = (struct msph_text_pos) { .line = 1, .col = 1 }; + ret->src.inner.file.f = f; + ret->src.inner.file.pos = 0; + ret->src.inner.file.end = 0; + + 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 *name, + const char *buf, size_t len) +{ + size_t res; + 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; + if ((res = strlcpy(ret->name, name, BUF_LEN(ret->name))) + >= BUF_LEN(ret->name)) { + MSPH_ERR(ctx, MSPH_ERR_TOOLONG); + goto err; + } + ret->src.type = MSPH_TOKEN_SRC_STR; + ret->src.pos = (struct msph_text_pos) { .line = 1, .col = 1 }; + ret->src.inner.str.s = buf; + ret->src.inner.str.len = strnlen(buf, len); + ret->src.inner.str.pos = 0; + + return (ret); + +err: + free(ret); + + return (NULL); +} + +ssize_t +msph_token_str(char *buf, size_t len, + struct msph_token *tok) +{ + ssize_t ret; + const char *base; + + base = tok_base_str(tok); + if (base == NULL) { + return (-1); + } + ret = (ssize_t)snprintf(buf, len, "%s", base); + + if (ret < 0 || ret >= (ssize_t)len) + return (ret); + + len -= (size_t)ret; + buf += ret; + + switch (tok->type) { + case TOK_IDENT: + ret += (ssize_t)snprintf(buf, len, "(%s)", tok->data.str); + break; + default: + break; + } + + return (ret); +} + +#define MSPH_TOKEN_PRINT_BUF_LEN 2 * MSPH_IDENT_LEN +int +msph_token_stream_print(struct msph_token_stream *s, FILE *out) +{ + ssize_t ret; + struct msph_token tok; + char tokstr[MSPH_TOKEN_PRINT_BUF_LEN]; + + while ((ret = msph_token_stream_read(&tok, 1, s)) > 0) { + + ret = msph_token_str(tokstr, BUF_LEN(tokstr), &tok); + if (ret < 0) { + MSPH_ERR_INFO(s->ctx, MSPH_ERR_TOKEN_INVAL, tok.type); + break; + } + + if ((size_t)ret < BUF_LEN(tokstr)) + fprintf(out, "%s\n", tokstr); + else + fprintf(out, "%s...(trunkated)", tokstr); + } + + return ((int)ret); +} + + +int +msph_token_stream_close(struct msph_token_stream *s) +{ + int ret; + + ret = -1; + + switch (s->src.type) { + case MSPH_TOKEN_SRC_FILE: + ret = fclose(s->src.inner.file.f); + break; + case MSPH_TOKEN_SRC_STR: + ret = 0; + break; + default: + break; + } + + return (ret); +} + +/* read at most n tokens from s into p. + * return -1 on error, or num tokens read + */ +ssize_t +msph_token_stream_read(struct msph_token *ptr, size_t n, + struct msph_token_stream *s) +{ + size_t ret; + int res; + + ret = 0; + res = -1; + while (ret < n && (res = read_single_tok(&ptr[ret], s)) != 0) { + if (res == -1) + return (-1); + ret++; + } + + return ((ssize_t)ret); +} + +/* 1: matched token, 0: failed to match token, -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; + struct msph_ctx *ctx; + struct msph_token_src *src; + + ctx = s->ctx; + src = &s->src; + + /* Skipping whitespace */ + if (tok_match(ctx, src, &wspace) == -1) + return (-1); + SPHO_DEBUG_PRINT("wspace.matchlen=%zu\n", wspace.matchlen); + if (wspace.matchlen > 0 && + tok_commit(ctx, src, &wspace, NULL) == -1) + return (-1); + + max_m = 0; + for (m = 1; token_matchers[m].type != TOK_END; m++) { + res = tok_match(ctx, src, &token_matchers[m]); + + if (res == -1) + return (-1); + + if (res == 0 && token_matchers[m].matchlen > + token_matchers[max_m].matchlen) { + max_m = m; + } + } + + if (max_m == 0) { + if (msph_token_stream_eof(s)) + return (0); + MSPH_ERR(s->ctx, MSPH_ERR_TOKEN_NOMATCH); + return (-1); + } + + if (tok_commit(ctx, src, &token_matchers[max_m], ptr) == -1) + return (-1); + + return (1); +} + +int +msph_token_stream_eof(struct msph_token_stream *s) +{ + struct msph_token_src_file *file; + struct msph_token_src_str *str; + + switch (s->src.type) { + case MSPH_TOKEN_SRC_FILE: + file = &s->src.inner.file; + return (file->pos == file->end && feof(file->f)); + case MSPH_TOKEN_SRC_STR: + str = &s->src.inner.str; + return (str->pos == str->len); + default: + MSPH_ERR(s->ctx, MSPH_ERR_INVAL); + return (-1); + } +} + +struct msph_token * +msph_token_copy(struct msph_ctx *ctx, struct msph_token *token) +{ + size_t i; + struct msph_token *copy; + struct msph_token_info *info; + + info = NULL; + + for (i = 0; token_info[i].type != TOK_END; i++) { + if (token_info[i].type == token->type) { + info = &token_info[i]; + break; + } + } + + if (info == NULL) { + MSPH_ERR_INFO(ctx, MSPH_ERR_TOKEN_INVAL, token->type); + return (NULL); + } + + if ((copy = malloc(sizeof(*copy))) == NULL) { + MSPH_ERR(ctx, MSPH_ERR_SYS); + return (NULL); + } + + memcpy(copy, token, sizeof(*copy)); + + return (copy); +} + +static ssize_t +src_file_fill_buf(struct msph_ctx *ctx, struct msph_token_src_file *file) +{ + ssize_t ret; + size_t nread, maxread; + + ret = nread = maxread = 0; + do { + if (file->end < file->pos) + maxread = file->pos - file->end; + else + maxread = BUF_LEN(file->buf) - file->end; + + if (maxread == 0) { + MSPH_ERR(ctx, MSPH_ERR_TOKEN_TOOLONG); + return (-1); + } + + nread = fread(&file->buf[file->end], sizeof(file->buf[0]), + maxread, file->f); + + ret += nread; + file->end = (file->end + nread) % BUF_LEN(file->buf); + + SPHO_DEBUG_PRINT("src_file_fill_buf: valid range (%zu, %zu)\n", + file->pos, file->end); + + if (nread < maxread) { + if (ferror(file->f)) { + MSPH_ERR(ctx, MSPH_ERR_SYS); + return (-1); + } + break; + } + + } while (file->end != file->pos); + + return (ret); +} + +/* reads a single char from the circular buffer in src */ +static int +file_char_at(struct msph_ctx *ctx, struct msph_token_src *src, size_t i, + char *out) +{ + ssize_t fill; + struct msph_token_src_file *file; + + SPHO_PRECOND(src != NULL); + SPHO_PRECOND(src->type == MSPH_TOKEN_SRC_FILE); + + file = &src->inner.file; + fill = 0; + + do { + /* simplest case */ + if (file->pos + i < file->end) { + *out = file->buf[file->pos + i]; + return (1); + } + /* wrap around */ + 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 (1); + } + + if (feof(file->f)) + return (0); + if ((fill = src_file_fill_buf(ctx, file)) == -1) + return (-1); + + } while (fill > 0); + + return (0); +} + +static int +char_at(struct msph_ctx *ctx, struct msph_token_src *src, size_t i, char *out) +{ + int ret; + struct msph_token_src_str *str; + + ret = -1; + switch (src->type) { + case MSPH_TOKEN_SRC_FILE: + ret = file_char_at(ctx, src, i, out); + break; + case MSPH_TOKEN_SRC_STR: + str = &src->inner.str; + if (str->pos + i < str->len) { + *out = str->s[str->pos + i]; + ret = 1; + } else { + ret = 0; + } + break; + default: + break; + } + +#ifdef SPHO_ENABLE_DEBUG_PRINT + if (isspace(*out)) { + const char *charrep; + switch (*out) { + case '\n': + charrep = "\\n"; + break; + case '\t': + charrep = "\\t"; + break; + case '\r': + charrep = "\\r"; + break; + case '\v': + charrep = "\\v"; + break; + case '\f': + charrep = "\\f"; + break; + default: + charrep = "WOOOOOOOOOOPS"; + break; + } + SPHO_DEBUG_PRINT("char_at: ret=%d, *out=%s\n", ret, charrep); + } else { + SPHO_DEBUG_PRINT("char_at: ret=%d, *out=%c\n", ret, *out); + } +#endif + return (ret); +} + +static int +fromcbuf_charcpy(char *dst, const char *src, size_t src_len, size_t src_pos, + size_t ncpy) +{ + size_t cpy1, cpy2; + if (src_len < ncpy) { + return (-1); + } + + cpy1 = (src_pos + ncpy < src_len) ? ncpy : src_len - src_pos; + cpy2 = ncpy - cpy1; + + SPHO_DEBUG_PRINT("fromcbuf_charcpy: cpy1=%zu cpy2=%zu\n", cpy1, cpy2); + + memcpy(dst, &src[src_pos], cpy1 * sizeof(src[0])); + + if (! cpy2) + return (0); + + memcpy(dst, &src[0], cpy2 * sizeof(src[0])); + + return (0); +} + +static int +tok_match(struct msph_ctx *ctx, struct msph_token_src *src, + struct msph_matcher *m) +{ + int res; + char chr; + const char *match_str; + size_t off, len; + SPHO_PRECOND(m != NULL && src != NULL); + + m->matchlen = 0; + +#define MATCH_CHAR(c) \ + do { \ + SPHO_DEBUG_PRINT("tok_match: '%c'\n", c); \ + if ((res = char_at(ctx, src, 0, &chr)) == -1) \ + return (-1); \ + else if (res == 0) \ + return (0); \ + SPHO_DEBUG_PRINT("tok_match: char_at(0)='%c'\n", c); \ +\ + if (chr == (c)) { \ + m->matchlen = 1; \ + } \ + SPHO_DEBUG_PRINT("tok_match: matchlen=%zu\n", m->matchlen); \ + return (0); \ + } while (0) + +#define MATCH_STR(str) \ + do { \ + match_str = str; \ + len = strlen(match_str); \ + for (off = 0; off < len; off++) { \ + if ((res = char_at(ctx, src, off, &chr)) == -1) \ + return (-1); \ + else if (res == 0) \ + return (0); \ +\ + if (chr != match_str[off]) \ + break; \ + } \ + if (off == len) \ + m->matchlen = len; \ + return (0); \ + } while (0) + + switch (m->type) { + case TOK_LBRACE: + MATCH_CHAR('{'); + case TOK_RBRACE: + MATCH_CHAR('}'); + case TOK_LBRAK: + MATCH_CHAR('['); + case TOK_RBRAK: + MATCH_CHAR(']'); + case TOK_LPAREN: + MATCH_CHAR('('); + case TOK_RPAREN: + MATCH_CHAR(')'); + case TOK_COLON: + MATCH_CHAR(':'); + case TOK_DOT: + MATCH_CHAR('.'); + case TOK_COMMA: + MATCH_CHAR(','); + case TOK_EQUALS: + MATCH_CHAR('='); + case TOK_AMP: + MATCH_CHAR('&'); + case TOK_PIPE: + MATCH_CHAR('|'); + case TOK_IMPL: + MATCH_STR("=>"); + case TOK_RARROW: + MATCH_STR("->"); + case TOK_SUB: + MATCH_STR("<:"); + case TOK_KW_TYPE: + MATCH_STR("type"); + case TOK_KW_NOMINAL: + MATCH_STR("nominal"); + case TOK_KW_MEMBER: + MATCH_STR("member"); + case TOK_KW_ASSERT: + MATCH_STR("assert"); + case TOK_KW_BOX: + MATCH_STR("box"); + case TOK_KW_FORALL: + MATCH_STR("forall"); + case TOK_CONST_TRUE: + MATCH_STR("True"); + case TOK_CONST_FALSE: + MATCH_STR("False"); + case TOK_IDENT: + off = 0; + while ((res = char_at(ctx, src, off++, &chr)) == 1) { + if (! isalnum(chr)) + break; + m->matchlen++; + } + if (res == -1) + return (-1); + return (0); + case TOK_WSPACE: + off = 0; + while((res = char_at(ctx, src, off++, &chr)) == 1) { + if (! isspace(chr)) + break; + m->matchlen++; + } + if (res == -1) + return (-1); + return (0); + default: + SPHO_ASSERT(0); + return (-1); + break; + } +#undef MATCH_CHAR +#undef MATCH_STR +} + +#define TOK_HAS_DATA(type) (type == TOK_IDENT) +static int +tok_commit(struct msph_ctx *ctx, struct msph_token_src *src, + struct msph_matcher *m, struct msph_token *ptr) +{ + size_t pos_old; + struct msph_text_pos tok_pos; + struct msph_token_src_str *str; + struct msph_token_src_file *file; + + SPHO_PRECOND(ctx != NULL && m != NULL); + SPHO_PRECOND(m->matchlen != 0); + + tok_pos = src->pos; + tok_update_pos(ctx, src, m); + + switch (src->type) { + case MSPH_TOKEN_SRC_FILE: + file = &src->inner.file; + pos_old = file->pos; + + file->pos += m->matchlen; + file->pos %= BUF_LEN(file->buf); + SPHO_ASSERT(file->pos <= file->end || + (file->pos < pos_old && file->pos < BUF_LEN(file->buf))); + + if (ptr == NULL) + return (0); + + ptr->type = m->type; + ptr->pos = tok_pos; + if (! TOK_HAS_DATA(ptr->type)) + return (0); + + if (m->matchlen >= sizeof(ptr->data.str)) { + MSPH_ERR(ctx, MSPH_ERR_TOKEN_TOOLONG); + return (-1); + } + + if (fromcbuf_charcpy(ptr->data.str, file->buf, + sizeof(file->buf), pos_old, m->matchlen) == -1) { + MSPH_ERR(ctx, MSPH_ERR_TOKEN_TOOLONG); + return (-1); + } + + ptr->data.str[m->matchlen] = '\0'; + return (0); + + case MSPH_TOKEN_SRC_STR: + str = &src->inner.str; + pos_old = str->pos; + + str->pos += m->matchlen; + SPHO_ASSERT(str->pos <= str->len); + + if (ptr == NULL) + return (0); + + ptr->type = m->type; + ptr->pos = tok_pos; + if (! TOK_HAS_DATA(ptr->type)) + return (0); + + if (m->matchlen >= sizeof(ptr->data.str)) { + MSPH_ERR(ctx, MSPH_ERR_TOKEN_TOOLONG); + return (-1); + } + + memcpy(ptr->data.str, str->s, m->matchlen * + sizeof(str->s[0])); + ptr->data.str[m->matchlen] = '\0'; + + return (0); + default: + return (-1); + } +} + +static void +tok_update_pos(struct msph_ctx *ctx, struct msph_token_src *src, + struct msph_matcher *m) +{ + int res; + char c; + size_t i; + + for (i = 0; i < m->matchlen; i++) { + res = char_at(ctx, src, i, &c); + SPHO_ASSERT(res == 1); + + switch (c) { + case '\t': + src->pos.col += MSPH_TAB_WIDTH; + break; + case '\n': + src->pos.line++; + src->pos.col = 1; + break; + case '\r': + break; + default: + src->pos.col++; + break; + } + } +} + +static const char * +tok_base_str(struct msph_token *tok) +{ + size_t i; + for (i = 0; token_info[i].type != TOK_END; i++) { + if (token_info[i].type == tok->type) + return (token_info[i].dbg_str); + } + + return (NULL); +} + + + diff --git a/src/msph/tree.c b/src/msph/tree.c new file mode 100644 index 0000000..113dbfb --- /dev/null +++ b/src/msph/tree.c @@ -0,0 +1,1250 @@ +#define SPHO_ENABLE_DEBUG_PRINT + +#include + +#include +#include +#include + +#include "spho/util.h" + +#include "msph/tree.h" + + +struct tree_parse { + struct msph_token_stream *s; + + struct msph_token curr; + + SLIST_HEAD(msph_token_l, msph_token) head; +}; + +#define CURR_TOKEN(parse) (&parse->curr) + +#define T(ptr) ((struct msph_tree *)ptr) +#define CTX(parse) ((parse)->s->ctx) + +static void tree_parse_init(struct tree_parse *, + struct msph_token_stream *); +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 *); + +static void free_the_tree(struct msph_tree *); + +static struct msph_tree_unit *tree_parse_unit(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_body *tree_parse_body(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_ident *tree_parse_ident(struct tree_parse *, + struct msph_tree *); + +static struct msph_tree_dir *tree_parse_tpdef(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_dir *tree_parse_assert(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_dir *tree_parse_nomindecl( + struct tree_parse *, + struct msph_tree *); +static struct msph_tree_dir *tree_parse_membdecl( + struct tree_parse *, + struct msph_tree *); + +static struct msph_tree_tpexpr *tree_parse_tpexpr(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 *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_name(struct tree_parse *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_applargs(struct tree_parse *, + struct msph_tree_ident*, + 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 *, + struct msph_tree *); +static struct msph_tree_tpexpr *tree_parse_paren(struct tree_parse *, + struct msph_tree *); + +struct msph_tree_root * +msph_tree_makeroot(struct msph_ctx *ctx) +{ + struct msph_tree_root *root; + + if ((root = malloc(sizeof(*root))) == NULL) { + MSPH_ERR(ctx, MSPH_ERR_SYS); + return (NULL); + } + T(root)->type = MSPH_TREE_ROOT; + T(root)->parent = NULL; + + root->ctx = ctx; + + STAILQ_INIT(&root->head); + + return (root); +} + + +/* + * Expect to read next token, otherwise set error and do something + * readres: (int) result of read + * parse: struct tree_parse * to perform read + * err_info: value passed to MSPH_ERR_INFO + * on_err: statement to perform on error + */ +#define EXPECT_READ_NEXT(readres, parse, err_info, on_err) \ + do { \ + if (((readres) = tree_parse_next_token(parse)) == -1) \ + on_err; \ + if ((readres) == 0) { \ + MSPH_ERR_INFO(CTX(parse), MSPH_ERR_TREE_EOF, \ + err_info); \ + on_err; \ + } \ + } while (0) + +/* + * Expect current token type, otherwise set error and do something + * parse: struct tree_parse * to perform read + * toktype: token type expected + * err_info: value passed to MSPH_ERR_INFO + * on_err: statement to perform on error + */ +#define EXPECT_CURR_TOKEN(parse, toktype, err_info, on_err) \ + do { \ + if (CURR_TOKEN(parse)->type != toktype) { \ + MSPH_ERR_INFO(CTX(parse), MSPH_ERR_TREE_NOMATCH, \ + err_info); \ + on_err; \ + } \ + } while (0) + +int +msph_tree_parse(struct msph_token_stream *s, struct msph_tree_root *root) +{ + struct tree_parse p; + struct msph_tree_unit *unit; + + if (T(root)->type != MSPH_TREE_ROOT) { + MSPH_ERR(s->ctx, MSPH_ERR_INVAL); + return (-1); + } + + tree_parse_init(&p, s); + + if ((unit = tree_parse_unit(&p, T(root))) == NULL) + return (-1); + + STAILQ_INSERT_TAIL(&root->head, unit, entries); + + return (0); +} + +ssize_t +msph_tree_fprint(FILE *f, struct msph_tree *tree) { + return (tree_ind_fprint(f, 0, tree)); +} + +#define MSPH_TREE_INDENT " " + +__attribute__((format(printf, 3, 4))) +static ssize_t +ind_fprintf(FILE *f, int indent, const char *fmt, ...) +{ + int res; + ssize_t ret; + int i; + va_list ap; + + ret = 0; + va_start(ap, fmt); + + for (i = 0; i < indent; i++) { + res = fprintf(f, "%s", MSPH_TREE_INDENT); + if (res < 0) { + return ((ssize_t)res); + } + ret += (ssize_t)res; + } + + res = vfprintf(f, fmt, ap); + if (res < 0) { + return ((ssize_t)res); + } + ret += (ssize_t)res; + va_end(ap); + + return (ret); +} + +static ssize_t +tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) +{ + ssize_t ret, res; + struct msph_tree_root *root; + struct msph_tree_unit *unit; + struct msph_tree_body *body; + struct msph_tree_dir *dir; + struct msph_tree_nomindecl *nomd; + struct msph_tree_assert *ass; + struct msph_tree_tpdef *tpdef; + struct msph_tree_membdecl *membdecl; + struct msph_tree_conj *conj; + struct msph_tree_disj *disj; + struct msph_tree_impl *impl; + struct msph_tree_arrow *arrow; + struct msph_tree_box *box; + struct msph_tree_forall *forall; + struct msph_tree_appl *appl; + struct msph_tree_trait *trait; + struct msph_tree_name *name; + struct msph_tree_paren *paren; + struct msph_tree_ident *ident; + struct msph_tree_tpexpr *tp; + + ret = 0; + switch (tree->type) { + case MSPH_TREE_ROOT: + root = (struct msph_tree_root *)tree; + if ((res = ind_fprintf(f, indent, "(root\n")) < 0) + return (res); + STAILQ_FOREACH(unit, &root->head, entries) { + if ((res = tree_ind_fprint(f, indent+1, T(unit))) + < 0) + return (res); + ret += res; + } + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + break; + case MSPH_TREE_UNIT: + unit = (struct msph_tree_unit *)tree; + if ((res = ind_fprintf(f, indent, "(unit:%s\n", unit->name)) + < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(unit->body))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_BODY: + body = (struct msph_tree_body *)tree; + if ((res = ind_fprintf(f, indent, "(body\n")) < 0) + return (res); + ret += res; + STAILQ_FOREACH(dir, &body->head, entries) { + if ((res = tree_ind_fprint(f, indent+1, T(dir))) + < 0) + return (res); + ret += res; + } + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_NOMINDECL: + nomd = (struct msph_tree_nomindecl *)tree; + if ((res = ind_fprintf(f, indent, "(nomindecl\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(nomd->id))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_ASSERT: + ass = (struct msph_tree_assert *)tree; + if ((res = ind_fprintf(f, indent, "(assert\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(ass->ltp))) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(ass->rtp))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_TPDEF: + tpdef = (struct msph_tree_tpdef *)tree; + if ((res = ind_fprintf(f, indent, "(tpdef\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(tpdef->id))) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(tpdef->tp))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_MEMBDECL: + membdecl = (struct msph_tree_membdecl *)tree; + if ((res = ind_fprintf(f, indent, "(membdecl:%s\n", + membdecl->id->str)) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(membdecl->tp))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_CONJ: + conj = (struct msph_tree_conj *)tree; + if ((res = ind_fprintf(f, indent, "(conj\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(conj->ltp))) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(conj->rtp))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_DISJ: + disj = (struct msph_tree_disj *)tree; + if ((res = ind_fprintf(f, indent, "(disj\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(disj->ltp))) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(disj->rtp))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_IMPL: + impl = (struct msph_tree_impl *)tree; + if ((res = ind_fprintf(f, indent, "(impl\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(impl->ltp))) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(impl->rtp))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_ARROW: + arrow = (struct msph_tree_arrow *)tree; + if ((res = ind_fprintf(f, indent, "(arrow\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(arrow->ltp))) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(arrow->rtp))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_BOX: + box = (struct msph_tree_box *)tree; + if ((res = ind_fprintf(f, indent, "(box\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(box->inner))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_FORALL: + forall = (struct msph_tree_forall *)tree; + if ((res = ind_fprintf(f, indent, "(forall:\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(forall->ident))) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(forall->inner))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_PAREN: + paren = (struct msph_tree_paren *)tree; + if ((res = ind_fprintf(f, indent, "(paren\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(paren->inner))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_APPL: + appl = (struct msph_tree_appl *)tree; + if ((res = ind_fprintf(f, indent, "(appl\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(appl->id))) < 0) + return (res); + ret += res; + STAILQ_FOREACH(tp, &appl->head, entries) { + if ((res = tree_ind_fprint(f, indent+1, T(tp))) < 0) + return (res); + ret += res; + } + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_NAME: + name = (struct msph_tree_name *)tree; + if ((res = ind_fprintf(f, indent, "(name\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(name->id))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_TRAIT: + trait = (struct msph_tree_trait *)tree; + if ((res = ind_fprintf(f, indent, "(trait\n")) < 0) + return (res); + ret += res; + if ((res = tree_ind_fprint(f, indent+1, T(trait->body))) < 0) + return (res); + ret += res; + if ((res = ind_fprintf(f, indent, ")\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_IDENT: + ident = (struct msph_tree_ident *)tree; + if ((res = ind_fprintf(f, indent, "(ident:%s)\n", ident->str)) + < 0) + return (res); + ret += res; + break; + case MSPH_TREE_TRUE: + if ((res = ind_fprintf(f, indent, "(true)\n")) < 0) + return (res); + ret += res; + break; + case MSPH_TREE_FALSE: + if ((res = ind_fprintf(f, indent, "(false)\n")) < 0) + return (res); + ret += res; + break; + default: + SPHO_ASSERT(0); + break; + } + + 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); + } + T(unit)->type = MSPH_TREE_UNIT; + T(unit)->parent = parent; + 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, T(unit))) == NULL) + goto err; + + return (unit); + +err: + free_the_tree(T(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); + } + T(body)->type = MSPH_TREE_BODY; + T(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, T(body)); + break; + case TOK_KW_NOMINAL: + dir = tree_parse_nomindecl(p, T(body)); + break; + case TOK_KW_MEMBER: + dir = tree_parse_membdecl(p, T(body)); + break; + case TOK_KW_ASSERT: + dir = tree_parse_assert(p, T(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(T(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; + + 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); + } + T(def)->type = MSPH_TREE_TPDEF; + T(def)->parent = parent; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err); + if ((def->id = tree_parse_ident(p, T(def))) == NULL) + goto err; + + EXPECT_READ_NEXT(res, p, 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, T(def))) == NULL) + goto err; + + return ((struct msph_tree_dir *)def); +err: + free_the_tree(T(def)); + return (NULL); +} + +struct msph_tree_ident * +tree_parse_ident(struct tree_parse *p, struct msph_tree *parent) +{ + struct msph_tree_ident *id; + + SPHO_DEBUG_PRINT("parsing ident\n"); + EXPECT_CURR_TOKEN(p, TOK_IDENT, MSPH_TREE_IDENT, return (NULL)); + + if ((id = malloc(sizeof(*id))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(id)->type = MSPH_TREE_IDENT; + T(id)->parent = parent; + + 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(T(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: + SPHO_DEBUG_PRINT("parsing conj\n"); + tp = tree_parse_conj(p, parent); + break; + case TOK_PIPE: + SPHO_DEBUG_PRINT("parsing disj\n"); + tp = tree_parse_disj(p, parent); + break; + case TOK_IMPL: + SPHO_DEBUG_PRINT("parsing impl\n"); + tp = tree_parse_impl(p, parent); + break; + case TOK_RARROW: + SPHO_DEBUG_PRINT("parsing arrow\n"); + tp = tree_parse_arrow(p, parent); + break; + case TOK_KW_BOX: + SPHO_DEBUG_PRINT("parsing box\n"); + tp = tree_parse_box(p, parent); + break; + case TOK_KW_FORALL: + SPHO_DEBUG_PRINT("parsing forall\n"); + tp = tree_parse_forall(p, parent); + break; + case TOK_IDENT: + SPHO_DEBUG_PRINT("parsing name\n"); + tp = tree_parse_name(p, parent); + break; + case TOK_CONST_TRUE: + SPHO_DEBUG_PRINT("parsing true\n"); + tp = tree_parse_true(p, parent); + break; + case TOK_CONST_FALSE: + SPHO_DEBUG_PRINT("parsing false\n"); + tp = tree_parse_false(p, parent); + break; + case TOK_LPAREN: + SPHO_DEBUG_PRINT("parsing paren\n"); + tp = tree_parse_paren(p, parent); + break; + case TOK_LBRACE: + SPHO_DEBUG_PRINT("parsing trait\n"); + 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", T(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); + } + T(conj)->type = MSPH_TREE_CONJ; + T(conj)->parent = parent; + conj->ltp = NULL; + conj->rtp = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_CONJ, goto err); + if ((conj->ltp = tree_parse_tpexpr(p, T(conj))) + == NULL) + goto err; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_CONJ, goto err); + if ((conj->rtp = tree_parse_tpexpr(p, T(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); + } + T(disj)->type = MSPH_TREE_DISJ; + T(disj)->parent = parent; + 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); + } + T(impl)->type = MSPH_TREE_IMPL; + T(impl)->parent = parent; + 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); + } + T(arrow)->type = MSPH_TREE_ARROW; + T(arrow)->parent = parent; + 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); + } + T(box)->type = MSPH_TREE_BOX; + T(box)->parent = parent; + box->inner = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_BOX, goto err); + if ((box->inner = tree_parse_tpexpr(p, T(box))) == NULL) + goto err; + + return ((struct msph_tree_tpexpr *)box); +err: + free_the_tree(T(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); + } + T(fa)->type = MSPH_TREE_FORALL; + T(fa)->parent = parent; + fa->ident = NULL; + fa->inner = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_FORALL, goto err); + if ((fa->ident = tree_parse_ident(p, T(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, T(fa))) == NULL) + goto err; + + return ((struct msph_tree_tpexpr *)fa); +err: + free_the_tree(T(fa)); + return (NULL); +} + +/* parse name or appl */ +struct msph_tree_tpexpr * +tree_parse_name(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_ident *id; + struct msph_tree_name *name; + struct msph_tree_tpexpr *ret; + struct msph_token *tok; + + ret = NULL; + name = NULL; + + if ((id = tree_parse_ident(p, NULL)) == NULL) + return (NULL); + SPHO_DEBUG_PRINT("parsed ident=%s\n", id->str); + + if ((res = tree_parse_next_token(p)) == 1) { + if (CURR_TOKEN(p)->type == TOK_LBRAK) { + if ((ret = tree_parse_applargs(p, id, 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; + } + + SPHO_DEBUG_PRINT("ident is name\n"); + if ((name = malloc(sizeof(*name))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + goto err; + } + T(name)->type = MSPH_TREE_NAME; + T(name)->parent = parent; + + T(id)->parent = T(name); + name->id = id; + + return ((struct msph_tree_tpexpr *)name); +err: + free_the_tree(T(id)); + + 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_applargs(struct tree_parse *p, struct msph_tree_ident *id, + struct msph_tree *parent) +{ + int res; + struct msph_tree_appl *appl; + struct msph_tree_tpexpr *tp; + + tp = NULL; + + EXPECT_CURR_TOKEN(p, TOK_LBRAK, MSPH_TREE_APPL, return (NULL)); + + if ((appl = malloc(sizeof(*appl))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(appl)->type = MSPH_TREE_APPL; + T(appl)->parent = parent; + appl->id = NULL; + STAILQ_INIT(&appl->head); + + /* 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 start of argument list, check for comma and step + * tokenizer */ + if (tp != NULL) { + EXPECT_CURR_TOKEN(p, TOK_COMMA, MSPH_TREE_APPL, + goto err); + EXPECT_READ_NEXT(res, p, MSPH_TREE_APPL, goto err); + } + + if ((tp = tree_parse_tpexpr(p, T(appl))) == NULL) + goto err; + + STAILQ_INSERT_TAIL(&appl->head, tp, entries); + } + + /* system error */ + 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_APPL); + goto err; + } + + /* finally, appl takes ownership of id */ + appl->id = id; + + return ((struct msph_tree_tpexpr *)appl); +err: + free_the_tree(T(appl)); + + 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); + } + T(t)->type = MSPH_TREE_TRUE; + T(t)->parent = parent; + + 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); + } + T(f)->type = MSPH_TREE_FALSE; + T(f)->parent = parent; + + 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); + } + T(par)->type = MSPH_TREE_PAREN; + T(par)->parent = parent; + par->inner = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_PAREN, goto err); + + if ((par->inner = tree_parse_tpexpr(p, T(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(T(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); + } + T(trait)->type = MSPH_TREE_TRAIT; + T(trait)->parent = parent; + trait->body = NULL; + + if ((trait->body = tree_parse_body(p, T(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(T(trait)); + + return (NULL); +} + +struct msph_tree_dir * +tree_parse_nomindecl(struct tree_parse *p, struct msph_tree *parent) +{ + int res; + struct msph_tree_nomindecl *nomd; + + EXPECT_CURR_TOKEN(p, TOK_KW_NOMINAL, MSPH_TREE_NOMINDECL, + return (NULL)); + + if ((nomd = malloc(sizeof(*nomd))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(nomd)->type = MSPH_TREE_NOMINDECL; + T(nomd)->parent = parent; + nomd->id = NULL; + + EXPECT_READ_NEXT(res, p, MSPH_TREE_NOMINDECL, return (NULL)); + if ((nomd->id = tree_parse_ident(p, T(nomd))) == NULL) + goto err; + + return ((struct msph_tree_dir *)nomd); +err: + free_the_tree(T(nomd)); + + 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)); + EXPECT_READ_NEXT(res, p, MSPH_TREE_MEMBDECL, return (NULL)); + + if ((membd = malloc(sizeof(*membd))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(membd)->type = MSPH_TREE_MEMBDECL; + T(membd)->parent = parent; + membd->id = NULL; + membd->tp = NULL; + + if ((membd->id = tree_parse_ident(p, T(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, T(membd))) == NULL) + goto err; + + return ((struct msph_tree_dir *)membd); +err: + free_the_tree(T(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)); + EXPECT_READ_NEXT(res, p, MSPH_TREE_ASSERT, return (NULL)); + + if ((ass = malloc(sizeof(*ass))) == NULL) { + MSPH_ERR(CTX(p), MSPH_ERR_SYS); + return (NULL); + } + T(ass)->type = MSPH_TREE_ASSERT; + T(ass)->parent = parent; + ass->ltp = NULL; + ass->rtp = NULL; + + if ((ass->ltp = tree_parse_tpexpr(p, T(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, T(ass))) == NULL) + goto err; + + return ((struct msph_tree_dir *)ass); +err: + free_the_tree(T(ass)); + + return (NULL); +} + +static void +free_the_tree(struct msph_tree *tree) +{ + /* no one will free the tree :ยด( */ + SPHO_POSTCOND((void *)tree != (void *)free); + SPHO_POSTCOND(0); +} + diff --git a/src/run/devcheck.c b/src/run/devcheck.c index e69de29..24c41ff 100644 --- a/src/run/devcheck.c +++ b/src/run/devcheck.c @@ -0,0 +1,18 @@ + +#include + +#include "spho/spho.h" + +int main(void) +{ + struct spho_ctx *ctx; + + ctx = NULL; + + if ((ctx = spho_ctx_create()) == NULL) + return (-1); + + spho_ctx_destroy(ctx); + + return (0); +} diff --git a/src/spho/ctx.c b/src/spho/ctx.c index 938863f..dacc076 100644 --- a/src/spho/ctx.c +++ b/src/spho/ctx.c @@ -1,5 +1,7 @@ +#include #include +#include #include #include "spho/ctx.h" @@ -8,13 +10,16 @@ static const char *spho_ctx_sys_strerror(struct spho_ctx *); static const char *spho_ctx_intern_strerror(struct spho_ctx *); struct spho_err { - int num; - char *msg; + int err; + const char *msg; }; 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 } }; @@ -23,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); } @@ -38,30 +49,19 @@ 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(&c->noms)) { - nom = SLIST_FIRST(&c->noms); - SLIST_REMOVE_HEAD(&c->noms, next); - free(nom); - } + spho_scope_term(&ctx->glob); - while (! SLIST_EMPTY(&c->cnsts)) { - cnst = SLIST_FIRST(&c->cnsts); - SLIST_REMOVE_HEAD(&c->cnsts, next); - free(cnst); - } + free(ctx); } const char * spho_ctx_strerror(struct spho_ctx *ctx) { - char *msg; int res; + const char *msg; SPHO_PRECOND(ctx != NULL); @@ -81,6 +81,10 @@ spho_ctx_strerror(struct spho_ctx *ctx) static const char * spho_ctx_sys_strerror(struct spho_ctx *ctx) { + int res; + + SPHO_POSTCOND(ctx != NULL); + #ifdef SPHO_DEBUG res = snprintf(ctx->errbuf, sizeof(ctx->errbuf), "%s:%d:spho_syserr:%s (%d)", ctx->filebuf, ctx->errline, @@ -89,8 +93,8 @@ spho_ctx_sys_strerror(struct spho_ctx *ctx) ctx->errbuf[sizeof(ctx->errbuf) - 1] = '\0'; #else res = snprintf(ctx->errbuf, sizeof(ctx->errbuf), - "spho_syserr:%s (%d)", ctx->filebuf, ctx->errline, - strerror(ctx->err_info), ctx->err_info); + "spho_syserr:%s (%d)", strerror(ctx->err_info), + ctx->err_info); if (res >= sizeof(ctx->errbuf)) ctx->errbuf[sizeof(ctx->errbuf) - 1] = '\0'; #endif diff --git a/src/spho/scope.c b/src/spho/scope.c new file mode 100644 index 0000000..988e824 --- /dev/null +++ b/src/spho/scope.c @@ -0,0 +1,156 @@ +#include + +#include +#include + +#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); +} diff --git a/src/spho/tp.c b/src/spho/tp.c index 74195de..e207197 100644 --- a/src/spho/tp.c +++ b/src/spho/tp.c @@ -1,9 +1,11 @@ +#include + +#include + +#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); +} + +