diff --git a/.clangd b/.clangd deleted file mode 100644 index ba4cbb3..0000000 --- a/.clangd +++ /dev/null @@ -1,2 +0,0 @@ -Diagnostics: - UnusedIncludes: None diff --git a/.gitignore b/.gitignore index 75a6986..dd51cb4 100644 --- a/.gitignore +++ b/.gitignore @@ -51,11 +51,9 @@ Module.symvers Mkfile.old dkms.conf -# CMake build dirs -build-*/ +# CMake build directory +build/ -# CMake compile commands -compile_commands.json # vim .*.swp diff --git a/CMakeLists.txt b/CMakeLists.txt index 466a3d9..573a310 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -3,17 +3,6 @@ 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) @@ -21,56 +10,21 @@ 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}/scope.h - ${SPHO_HEADER_DIR}/tp.h ${SPHO_HEADER_DIR}/spho.h + ${SPHO_HEADER_DIR}/tp.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 deleted file mode 100644 index 0844c3f..0000000 --- a/example/ex1.msph +++ /dev/null @@ -1,4 +0,0 @@ - -nominal C - - diff --git a/example/ex2.msph b/example/ex2.msph deleted file mode 100644 index 5b85fdc..0000000 --- a/example/ex2.msph +++ /dev/null @@ -1 +0,0 @@ -type A = & C D diff --git a/example/ex3.msph b/example/ex3.msph deleted file mode 100644 index 9770336..0000000 --- a/example/ex3.msph +++ /dev/null @@ -1,13 +0,0 @@ - -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 deleted file mode 100644 index 43a6a6f..0000000 --- a/include/msph/common.h +++ /dev/null @@ -1,25 +0,0 @@ -#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 deleted file mode 100644 index bf113d5..0000000 --- a/include/msph/err.h +++ /dev/null @@ -1,36 +0,0 @@ -#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 deleted file mode 100644 index b984039..0000000 --- a/include/msph/token.h +++ /dev/null @@ -1,146 +0,0 @@ -#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 deleted file mode 100644 index 22cc883..0000000 --- a/include/msph/tree.h +++ /dev/null @@ -1,257 +0,0 @@ -#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 9858e85..746126c 100644 --- a/include/spho/ctx.h +++ b/include/spho/ctx.h @@ -1,31 +1,25 @@ #ifndef _SPHO_CTX_H #define _SPHO_CTX_H -#include "spho/err.h" -#include "spho/scope.h" - -#define SPHO_ERR_BUF_LEN 2048 -#define SPHO_ERR_FILEBUF_LEN 128 +#include "spho/data.h" struct spho_ctx { - struct spho_scope glob; - int err; int err_info; - char errbuf[SPHO_ERR_BUF_LEN]; + + struct spho_nom_l noms; + struct spho_const_l cnsts; #ifdef SPHO_DEBUG - char filebuf[SPHO_ERR_FILEBUF_LEN]; - int errline; + 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 *); -const char *spho_ctx_strerror(struct spho_ctx *); +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 0cd02c8..2050387 100644 --- a/include/spho/data.h +++ b/include/spho/data.h @@ -1,12 +1,36 @@ #ifndef _SPHO_DATA_H #define _SPHO_DATA_H -struct spho_nom { - char s[128]; - SLIST_ENTRY(spho_nom) next; +#include + +struct spho_name { + char str[128]; }; -SLIST_HEAD(spho_nom_l, spho_nom); +struct spho_var { + struct spho_name name; +}; + +struct spho_cnst { + struct spho_name name; +}; + +struct spho_nom { + struct spho_name name; +}; + +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; +}; -#endif /* _SPHO_DATA_H */ +SLIST_HEAD(spho_nom_l, spho_nom_le); +SLIST_HEAD(spho_const_l, spho_const_le); + +#endif diff --git a/include/spho/err.h b/include/spho/err.h index ffde4b0..f92687a 100644 --- a/include/spho/err.h +++ b/include/spho/err.h @@ -1,107 +1,67 @@ #ifndef _SPHO_ERR_H #define _SPHO_ERR_H -#include +#define SPHO_ERR_SYSTEM 0x000001 -#ifdef SPHO_DEBUG -#include -#endif +#define SPHO_ERR_INTERNAL 0x010001 -#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) +#define SPHO_ERR_IS_SYSERR(err) (SPHO_ERR_SYSTEM == err) #ifdef SPHO_DEBUG -#define SPHO_ERR_FILEBUF_LEN 128 - -#define SPHO_ERR_INFO(ctx, e, info) \ +#define SPHO_ERR(ctx, err) \ do { \ - (ctx)->err = (e); \ - (ctx)->err_info = (info); \ - snprintf((ctx)->filebuf, sizeof((ctx)->filebuf), \ + ctx->err = err; \ + if (err == SPHO_ERR_SYSTEM) \ + ctx->err_info = errno; \ + snprintf(ctx->filebuf, sizeof(ctx->filebuf), "%s", \ __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_INFO(ctx, e, info) \ +#define SPHO_ERR(ctx, err) \ do { \ - (ctx)->err = (e); \ - (ctx)->err_info = (info); \ + ctx->err = err; \ + if (err == SPHO_ERR_SYSTEM) \ + ctx->err_info = errno; \ } while (0) -#define SPHO_PRECOND(cond) -#define SPHO_ASSERT(cond) -#define SPHO_POSTCOND(cond) -#define SPHO_DEBUG_PRINT(fmt, ...) - #endif /* SPHO_DEBUG */ -#endif /* _SPHO_ERR_H */ +/* 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 + +#endif diff --git a/include/spho/loc.h b/include/spho/loc.h index bf6e425..05f6008 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 +#endif \ No newline at end of file diff --git a/include/spho/scope.h b/include/spho/scope.h deleted file mode 100644 index e0d62ff..0000000 --- a/include/spho/scope.h +++ /dev/null @@ -1,34 +0,0 @@ -#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 f8582dc..900444f 100644 --- a/include/spho/spho.h +++ b/include/spho/spho.h @@ -4,6 +4,29 @@ #include #include "spho/err.h" -#include "spho/ctx.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 *); #endif diff --git a/include/spho/tp.h b/include/spho/tp.h index fdbf8bf..0098237 100644 --- a/include/spho/tp.h +++ b/include/spho/tp.h @@ -3,42 +3,13 @@ /* base defs */ -#define SPHO_KONST_S_SZ 128 -#define SPHO_KONST_K_TRUE 0x43445 /* don't change!!!!! */ -#define SPHO_KONST_K_FALSE 0x66a57 /* don't change!1! */ - -struct spho_konst { - const char *s; - int k; -}; - -const struct spho_konst SPHO_K_TRUE_V = { "True", SPHO_KONST_K_TRUE }; -const struct spho_konst SPHO_K_FALSE_V = { "False", SPHO_KONST_K_FALSE }; - -#define SPHO_K_TRUE (&SPHO_K_TRUE_V) -#define SPHO_K_FALSE (&SPHO_K_FALSE_V) - - -struct spho_var { - struct spho_nom nom; - - STAILQ_ENTRY(spho_var) next; -}; - -STAILQ_HEAD(spho_var_l, spho_var); - -struct spho_bind { - struct spho_nom nom; - struct spho_tpop *op; -}; - -struct spho_tpop { - struct spho_var_l params; - struct spho_tp *def; +struct spho_alias { + struct spho_name name; + struct spho_tp *tp; }; struct spho_rec { - struct spho_nom mnom; + struct spho_name mname; struct spho_tp *tp; }; @@ -49,21 +20,21 @@ struct tp_bin_data { }; struct tp_box_data { - struct spho_tp *inr; + struct spho_tp *tp; }; struct tp_forall_data { struct spho_var *var; - struct spho_tp *inr; + struct spho_tp *tp; }; -struct tp_bappl_data { - struct spho_bind *bind; - struct spho_tp_l *args; +struct tp_alias_data { + struct spho_alias *alias; + struct spho_tp_list *l; }; -struct tp_konst_data { - const struct spho_konst *k; +struct tp_const_data { + struct spho_const *c; }; struct tp_var_data { @@ -83,10 +54,10 @@ union tp_data { struct tp_bin_data binop; struct tp_box_data box; struct tp_forall_data fa; - struct tp_bappl_data bappl; - struct tp_konst_data konst; + struct tp_alias_data alias; + struct tp_const_data cnst; struct tp_var_data var; - struct tp_nominal_data nom; // XXX + struct tp_nominal_data nom; struct tp_record_data rec; }; @@ -96,9 +67,8 @@ 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_ARROW 0x14 -#define SPHO_TP_FORM_FORALL 0x15 -#define SPHO_TP_FORM_BAPPL 0x16 +#define SPHO_TP_FORM_FORALL 0x14 +#define SPHO_TP_FORM_ALIAS 0x15 #define SPHO_TP_FORM_FALSE 0x20 #define SPHO_TP_FORM_TRUE 0x21 @@ -107,49 +77,43 @@ union tp_data { #define SPHO_TP_FORM_REC 0x23 -// #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 +// TODO explain +#define SPHO_TP_FORM_SUB 0x96 /* sappho type */ struct spho_tp { - struct spho_scope *sc; - - int form; - union tp_data data; - - STAILQ_ENTRY(spho_tp) next; + int form; + union tp_data data; }; -STAILQ_HEAD(spho_tp_l, spho_tp); +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); +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_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 *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 *); void spho_tp_destroy(struct spho_tp*); diff --git a/include/spho/util.h b/include/spho/util.h deleted file mode 100644 index 2cb9681..0000000 --- a/include/spho/util.h +++ /dev/null @@ -1,25 +0,0 @@ -#ifndef _SPHO_UTIL_H -#define _SPHO_UTIL_H - - -#define SPHO_UTIL_SLIST_DESTROY(l, elmtype, next, term) \ -do { \ - struct elmtype *elm; \ - while (! SLIST_EMPTY(l)) { \ - elm = SLIST_FIRST(l); \ - SLIST_REMOVE_HEAD(l, next); \ - term(elm); \ - free(elm); \ - } \ -} while (0) - -#ifdef SPHO_USE_STRLCPY -#define SPHO_STRLCPY(dst, src, len) strlcpy(dst, src, len) -#else -#define SPHO_STRLCPY(dst, src, len) \ - (size_t)snprintf(dst, len, "%s", src) -#endif - - -#endif - diff --git a/src/msph/README.md b/src/msph/README.md deleted file mode 100644 index 19b3857..0000000 --- a/src/msph/README.md +++ /dev/null @@ -1,105 +0,0 @@ -# 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 deleted file mode 100644 index edc2ed7..0000000 --- a/src/msph/msph.c +++ /dev/null @@ -1,151 +0,0 @@ -#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 deleted file mode 100644 index 01b5cd7..0000000 --- a/src/msph/token.c +++ /dev/null @@ -1,784 +0,0 @@ -#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 deleted file mode 100644 index 113dbfb..0000000 --- a/src/msph/tree.c +++ /dev/null @@ -1,1250 +0,0 @@ -#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 24c41ff..e69de29 100644 --- a/src/run/devcheck.c +++ b/src/run/devcheck.c @@ -1,18 +0,0 @@ - -#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 dacc076..938863f 100644 --- a/src/spho/ctx.c +++ b/src/spho/ctx.c @@ -1,7 +1,5 @@ -#include #include -#include #include #include "spho/ctx.h" @@ -10,16 +8,13 @@ static const char *spho_ctx_sys_strerror(struct spho_ctx *); static const char *spho_ctx_intern_strerror(struct spho_ctx *); struct spho_err { - int err; - const char *msg; + int num; + char *msg; }; struct spho_err spho_errmsgs[] = { - { 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" }, + { SPHO_ERR_SYSTEM, "spho system error" }, + { SPHO_ERR_INTERNAL, "spho internal error" }, { -1, NULL } }; @@ -28,20 +23,14 @@ 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; - if (spho_scope_init(&c->glob, c, NULL) == -1) { - free(c); - return (NULL); - } - - SPHO_POSTCOND(c != NULL); + SLIST_INIT(&c->noms); + SLIST_INIT(&c->cnsts); return (c); } @@ -49,19 +38,30 @@ 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); - spho_scope_term(&ctx->glob); + while (! SLIST_EMPTY(&c->noms)) { + nom = SLIST_FIRST(&c->noms); + SLIST_REMOVE_HEAD(&c->noms, next); + free(nom); + } - free(ctx); + while (! SLIST_EMPTY(&c->cnsts)) { + cnst = SLIST_FIRST(&c->cnsts); + SLIST_REMOVE_HEAD(&c->cnsts, next); + free(cnst); + } } const char * spho_ctx_strerror(struct spho_ctx *ctx) { + char *msg; int res; - const char *msg; SPHO_PRECOND(ctx != NULL); @@ -81,10 +81,6 @@ 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, @@ -93,8 +89,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)", strerror(ctx->err_info), - ctx->err_info); + "spho_syserr:%s (%d)", ctx->filebuf, ctx->errline, + 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 deleted file mode 100644 index 988e824..0000000 --- a/src/spho/scope.c +++ /dev/null @@ -1,156 +0,0 @@ -#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 e207197..74195de 100644 --- a/src/spho/tp.c +++ b/src/spho/tp.c @@ -1,11 +1,9 @@ -#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 *, @@ -13,178 +11,3 @@ //{ // //} - - -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); -} - -