prefix notation type parser
This commit is contained in:
parent
9b24c8a496
commit
9ac779c1cf
14 changed files with 1217 additions and 151 deletions
2
.clangd
Normal file
2
.clangd
Normal file
|
|
@ -0,0 +1,2 @@
|
||||||
|
Diagnostics:
|
||||||
|
UnusedIncludes: None
|
||||||
4
.gitignore
vendored
4
.gitignore
vendored
|
|
@ -51,9 +51,11 @@ Module.symvers
|
||||||
Mkfile.old
|
Mkfile.old
|
||||||
dkms.conf
|
dkms.conf
|
||||||
|
|
||||||
# CMake build directory
|
# CMake build dirs
|
||||||
build-*/
|
build-*/
|
||||||
|
|
||||||
|
# CMake compile commands
|
||||||
|
compile_commands.json
|
||||||
|
|
||||||
# vim
|
# vim
|
||||||
.*.swp
|
.*.swp
|
||||||
|
|
|
||||||
|
|
@ -10,6 +10,8 @@ string(JOIN " " CMAKE_C_FLAGS
|
||||||
"-Werror=int-conversion")
|
"-Werror=int-conversion")
|
||||||
set(CMAKE_VERBOSE_MAKEFILE ON)
|
set(CMAKE_VERBOSE_MAKEFILE ON)
|
||||||
|
|
||||||
|
set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
|
||||||
|
|
||||||
|
|
||||||
include(CheckSymbolExists)
|
include(CheckSymbolExists)
|
||||||
|
|
||||||
|
|
@ -54,6 +56,7 @@ target_compile_definitions(devcheck PRIVATE
|
||||||
|
|
||||||
set(MSPH_SRC
|
set(MSPH_SRC
|
||||||
${SRC_DIR}/msph/token.c
|
${SRC_DIR}/msph/token.c
|
||||||
|
${SRC_DIR}/msph/tree.c
|
||||||
${SRC_DIR}/msph/msph.c
|
${SRC_DIR}/msph/msph.c
|
||||||
)
|
)
|
||||||
|
|
||||||
|
|
|
||||||
18
include/msph/common.h
Normal file
18
include/msph/common.h
Normal file
|
|
@ -0,0 +1,18 @@
|
||||||
|
#ifndef _MSPH_COMMON_H
|
||||||
|
#define _MSPH_COMMON_H
|
||||||
|
|
||||||
|
#include "msph/err.h"
|
||||||
|
|
||||||
|
#define MSPH_IDENT_LEN 128
|
||||||
|
|
||||||
|
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
|
||||||
|
};
|
||||||
|
#endif
|
||||||
|
|
@ -10,11 +10,31 @@
|
||||||
|
|
||||||
#define MSPH_ERR_SYS 0x0001
|
#define MSPH_ERR_SYS 0x0001
|
||||||
|
|
||||||
#define MSPH_ERR_INVAL 0x1001
|
#define MSPH_ERR_INVAL 0x0002
|
||||||
|
|
||||||
#define MSPH_ERR_TOOLONG 0x2001
|
#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_ERR(ctx, e) SPHO_ERR(ctx, e)
|
||||||
#define MSPH_TOKS_ERR(toks, e) MSPH_ERR((toks)->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
|
#endif
|
||||||
|
|
|
||||||
|
|
@ -1,53 +1,11 @@
|
||||||
#ifndef _MSPH_EXPR_H
|
#ifndef _MSPH_EXPR_H
|
||||||
#define _MSPH_EXPR_H
|
#define _MSPH_EXPR_H
|
||||||
|
|
||||||
|
#include <sys/queue.h>
|
||||||
|
|
||||||
|
#include "msph/common.h"
|
||||||
|
|
||||||
/*
|
/*
|
||||||
* TYPES:
|
|
||||||
* Conj
|
|
||||||
* Disj
|
|
||||||
* Impl
|
|
||||||
* Arrow
|
|
||||||
* Box
|
|
||||||
* (Sub)
|
|
||||||
* Forall
|
|
||||||
*
|
|
||||||
* True
|
|
||||||
* False
|
|
||||||
* Var
|
|
||||||
* Nominal
|
|
||||||
*
|
|
||||||
* Record
|
|
||||||
*
|
|
||||||
* DEFINITIONS/DIRECTIVES:
|
|
||||||
* Type definition (type A[X..] = T)
|
|
||||||
* Nominal definition (nominal N)
|
|
||||||
* Member definition (member mname : T)
|
|
||||||
*
|
|
||||||
* {
|
|
||||||
* member a: A
|
|
||||||
* member b: B
|
|
||||||
* }
|
|
||||||
*
|
|
||||||
* Subtyping check (check A <: B, checks if A <: B)
|
|
||||||
*
|
|
||||||
* EXTRA DEFINITIONS
|
|
||||||
* Class definition (class C[...] { ... }, shorthand)
|
|
||||||
*
|
|
||||||
* EXPRESSIONS
|
|
||||||
* Conj
|
|
||||||
* Disj
|
|
||||||
* Impl
|
|
||||||
* Arrow
|
|
||||||
* Box
|
|
||||||
* (Sub)
|
|
||||||
* Forall
|
|
||||||
*
|
|
||||||
* True
|
|
||||||
* False
|
|
||||||
* Var
|
|
||||||
* Nominal
|
|
||||||
*
|
|
||||||
* Trait ({ ... }, creates scoping)
|
|
||||||
*
|
*
|
||||||
*
|
*
|
||||||
* TOKENS
|
* TOKENS
|
||||||
|
|
@ -79,16 +37,6 @@
|
||||||
*
|
*
|
||||||
*/
|
*/
|
||||||
|
|
||||||
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
|
|
||||||
};
|
|
||||||
|
|
||||||
enum msph_tok_type {
|
enum msph_tok_type {
|
||||||
TOK_LBRACE, // {
|
TOK_LBRACE, // {
|
||||||
|
|
@ -99,6 +47,8 @@ enum msph_tok_type {
|
||||||
TOK_RPAREN, // )
|
TOK_RPAREN, // )
|
||||||
TOK_COLON, // :
|
TOK_COLON, // :
|
||||||
TOK_EQUALS, // =
|
TOK_EQUALS, // =
|
||||||
|
TOK_COMMA, // ,
|
||||||
|
TOK_DOT, // .
|
||||||
|
|
||||||
TOK_AMP, // &
|
TOK_AMP, // &
|
||||||
TOK_PIPE, // |
|
TOK_PIPE, // |
|
||||||
|
|
@ -109,7 +59,7 @@ enum msph_tok_type {
|
||||||
TOK_KW_TYPE, // type
|
TOK_KW_TYPE, // type
|
||||||
TOK_KW_NOMINAL, // nominal
|
TOK_KW_NOMINAL, // nominal
|
||||||
TOK_KW_MEMBER, // member
|
TOK_KW_MEMBER, // member
|
||||||
TOK_KW_CHECK, // check
|
TOK_KW_ASSERT, // assert
|
||||||
TOK_KW_BOX, // box
|
TOK_KW_BOX, // box
|
||||||
TOK_KW_FORALL, // forall
|
TOK_KW_FORALL, // forall
|
||||||
|
|
||||||
|
|
@ -117,23 +67,20 @@ enum msph_tok_type {
|
||||||
TOK_CONST_FALSE, // False
|
TOK_CONST_FALSE, // False
|
||||||
|
|
||||||
TOK_IDENT, // identifiers
|
TOK_IDENT, // identifiers
|
||||||
|
TOK_INVAL, // special: invalid, use to mark invalid toks
|
||||||
TOK_WSPACE, // special: whitespace
|
TOK_WSPACE, // special: whitespace
|
||||||
TOK_END // special: denote end of array
|
TOK_END // special: denote end of array
|
||||||
};
|
};
|
||||||
|
|
||||||
#define MSPH_TOKEN_BUF_LEN 128
|
union msph_token_data {
|
||||||
|
char str[MSPH_IDENT_LEN];
|
||||||
struct token_s {
|
|
||||||
char buf[MSPH_TOKEN_BUF_LEN];
|
|
||||||
};
|
|
||||||
|
|
||||||
union token_data {
|
|
||||||
struct token_s s;
|
|
||||||
};
|
};
|
||||||
|
|
||||||
struct msph_token {
|
struct msph_token {
|
||||||
int type;
|
int type;
|
||||||
union token_data d;
|
union msph_token_data data;
|
||||||
|
|
||||||
|
SLIST_ENTRY(msph_token) entries;
|
||||||
};
|
};
|
||||||
|
|
||||||
#define MSPH_FILE_NAME_LEN 1024
|
#define MSPH_FILE_NAME_LEN 1024
|
||||||
|
|
@ -147,9 +94,6 @@ struct msph_token_src_file {
|
||||||
size_t pos;
|
size_t pos;
|
||||||
size_t end;
|
size_t end;
|
||||||
char buf[MSPH_FILE_BUF_LEN];
|
char buf[MSPH_FILE_BUF_LEN];
|
||||||
|
|
||||||
/* file path */
|
|
||||||
char name[MSPH_FILE_NAME_LEN];
|
|
||||||
};
|
};
|
||||||
|
|
||||||
#define MSPH_TOKEN_SRC_STR 2
|
#define MSPH_TOKEN_SRC_STR 2
|
||||||
|
|
@ -178,17 +122,21 @@ struct msph_token_stream {
|
||||||
void msph_ctx_init(struct msph_ctx *);
|
void msph_ctx_init(struct msph_ctx *);
|
||||||
|
|
||||||
struct msph_token_stream *msph_token_stream_file(struct msph_ctx *,
|
struct msph_token_stream *msph_token_stream_file(struct msph_ctx *,
|
||||||
FILE *, const char *);
|
FILE *);
|
||||||
struct msph_token_stream *msph_token_stream_frombuf(struct msph_ctx *,
|
struct msph_token_stream *msph_token_stream_frombuf(struct msph_ctx *,
|
||||||
const char *, size_t);
|
const char *, size_t);
|
||||||
|
|
||||||
int msph_token_stream_close(struct msph_token_stream*);
|
int msph_token_stream_close(struct msph_token_stream*);
|
||||||
|
|
||||||
ssize_t msph_token_stream_read_tok(struct msph_token *, size_t,
|
ssize_t msph_token_stream_read(struct msph_token *, size_t,
|
||||||
struct msph_token_stream *);
|
struct msph_token_stream *);
|
||||||
|
int msph_token_stream_eof(struct msph_token_stream *);
|
||||||
int msph_token_stream_print(struct msph_token_stream *, FILE *);
|
int msph_token_stream_print(struct msph_token_stream *, FILE *);
|
||||||
|
|
||||||
ssize_t msph_token_str(char *buf, size_t len, struct msph_token *tok);
|
ssize_t msph_token_str(char *, size_t, struct msph_token *);
|
||||||
|
|
||||||
|
struct msph_token * msph_token_create(struct msph_ctx *, int,
|
||||||
|
union msph_token_data *);
|
||||||
|
|
||||||
|
|
||||||
#endif /* _MSPH_EXPR_H */
|
#endif /* _MSPH_EXPR_H */
|
||||||
|
|
|
||||||
239
include/msph/tree.h
Normal file
239
include/msph/tree.h
Normal file
|
|
@ -0,0 +1,239 @@
|
||||||
|
#ifndef _MSPH_TREE_H
|
||||||
|
#define _MSPH_TREE_H
|
||||||
|
|
||||||
|
#include <sys/queue.h>
|
||||||
|
|
||||||
|
#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 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 {
|
||||||
|
struct msph_tree *parent;
|
||||||
|
int type;
|
||||||
|
};
|
||||||
|
|
||||||
|
struct msph_tree_root;
|
||||||
|
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;
|
||||||
|
struct msph_tree_body *body;
|
||||||
|
};
|
||||||
|
|
||||||
|
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 *);
|
||||||
|
|
||||||
|
#endif
|
||||||
|
|
@ -18,17 +18,23 @@
|
||||||
|
|
||||||
#define SPHO_ERR_BUF_LEN 2048
|
#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
|
#ifdef SPHO_DEBUG
|
||||||
|
|
||||||
#define SPHO_ERR_FILEBUF_LEN 128
|
#define SPHO_ERR_FILEBUF_LEN 128
|
||||||
|
|
||||||
#define SPHO_ERR(ctx, e) \
|
#define SPHO_ERR_INFO(ctx, e, info) \
|
||||||
do { \
|
do { \
|
||||||
(ctx)->err = (e); \
|
(ctx)->err = (e); \
|
||||||
if ((e) == SPHO_ERR_SYS) \
|
(ctx)->err_info = (info); \
|
||||||
(ctx)->err_info = errno; \
|
|
||||||
snprintf((ctx)->filebuf, sizeof((ctx)->filebuf), \
|
snprintf((ctx)->filebuf, sizeof((ctx)->filebuf), \
|
||||||
__FILE__); \
|
__FILE__); \
|
||||||
(ctx)->errline = __LINE__; \
|
(ctx)->errline = __LINE__; \
|
||||||
|
|
@ -85,18 +91,17 @@
|
||||||
|
|
||||||
#else /* SPHO_DEBUG */
|
#else /* SPHO_DEBUG */
|
||||||
|
|
||||||
#define SPHO_ERR(ctx, e) \
|
#define SPHO_ERR_INFO(ctx, e, info) \
|
||||||
do { \
|
do { \
|
||||||
(ctx)->err = (e); \
|
(ctx)->err = (e); \
|
||||||
if ((e) == SPHO_ERR_SYS) \
|
(ctx)->err_info = (info); \
|
||||||
(ctx)->err_info = errno; \
|
|
||||||
} while (0)
|
} while (0)
|
||||||
|
|
||||||
#define SPHO_PRECOND(cond)
|
#define SPHO_PRECOND(cond)
|
||||||
#define SPHO_ASSERT(cond)
|
#define SPHO_ASSERT(cond)
|
||||||
#define SPHO_POSTCOND(cond)
|
#define SPHO_POSTCOND(cond)
|
||||||
|
|
||||||
#define SPHO_DBG_PRINT(fmt, ...)
|
#define SPHO_DEBUG_PRINT(fmt, ...)
|
||||||
|
|
||||||
#endif /* SPHO_DEBUG */
|
#endif /* SPHO_DEBUG */
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -86,7 +86,7 @@ union tp_data {
|
||||||
struct tp_bappl_data bappl;
|
struct tp_bappl_data bappl;
|
||||||
struct tp_konst_data konst;
|
struct tp_konst_data konst;
|
||||||
struct tp_var_data var;
|
struct tp_var_data var;
|
||||||
struct tp_nominal_data nom;
|
struct tp_nominal_data nom; // XXX
|
||||||
struct tp_record_data rec;
|
struct tp_record_data rec;
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
@ -126,6 +126,7 @@ struct spho_tp {
|
||||||
|
|
||||||
STAILQ_HEAD(spho_tp_l, spho_tp);
|
STAILQ_HEAD(spho_tp_l, spho_tp);
|
||||||
|
|
||||||
|
|
||||||
#define SPHO_TP_ERR(tp, err) SPHO_ERR((tp)->sc->ctx, (err))
|
#define SPHO_TP_ERR(tp, err) SPHO_ERR((tp)->sc->ctx, (err))
|
||||||
|
|
||||||
struct spho_var *spho_var_create(struct spho_scope *, char *, size_t);
|
struct spho_var *spho_var_create(struct spho_scope *, char *, size_t);
|
||||||
|
|
|
||||||
|
|
@ -13,6 +13,13 @@ do { \
|
||||||
} \
|
} \
|
||||||
} while (0)
|
} 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
|
#endif
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -21,7 +21,7 @@ Body ::= Dirs
|
||||||
Dir ::= Typedef (directives, with lack of a better name)
|
Dir ::= Typedef (directives, with lack of a better name)
|
||||||
| Memberdef
|
| Memberdef
|
||||||
| Nominaldecl
|
| Nominaldecl
|
||||||
| Checkdir
|
| Assert
|
||||||
|
|
||||||
Typedef ::= 'type' Name '=' TExpr (type definition/binding)
|
Typedef ::= 'type' Name '=' TExpr (type definition/binding)
|
||||||
| 'type' Name '[' Names ']' '=' TExpr
|
| 'type' Name '[' Names ']' '=' TExpr
|
||||||
|
|
@ -31,13 +31,14 @@ Memberdef ::= 'member' Name ':' TExpr
|
||||||
|
|
||||||
Nominaldecl ::= 'nominal' Name
|
Nominaldecl ::= 'nominal' Name
|
||||||
|
|
||||||
Checkdir ::= 'check' TExpr '<:' TExpr
|
Assert ::= 'assert' TExpr '<:' TExpr
|
||||||
|
|
||||||
TExpr ::= 'True'
|
TExpr ::= 'True'
|
||||||
| 'False'
|
| 'False'
|
||||||
| Var
|
| Var
|
||||||
| Nominal
|
| Nominal
|
||||||
| Trait
|
| Trait
|
||||||
|
| Appl
|
||||||
| TExpr '&' TExpr
|
| TExpr '&' TExpr
|
||||||
| TExpr '|' TExpr
|
| TExpr '|' TExpr
|
||||||
| TExpr '=>' TExpr
|
| TExpr '=>' TExpr
|
||||||
|
|
@ -50,13 +51,14 @@ Trait ::= '{' Body '}' (trait, this introduces scoping)
|
||||||
|
|
||||||
Var ::= Name (type variables)
|
Var ::= Name (type variables)
|
||||||
Nominal ::= Name (nominal type)
|
Nominal ::= Name (nominal type)
|
||||||
|
Appl ::= Name '[' TExprs ']'
|
||||||
|
|
||||||
Name ::= '[a-zA-Z0-9_]+' & !Reserved (name/identifier)
|
Name ::= '[a-zA-Z0-9_]+' & !Reserved (name/identifier)
|
||||||
|
|
||||||
Reserved ::= 'type' (reserved/keywords)
|
Reserved ::= 'type' (reserved/keywords)
|
||||||
| 'member'
|
| 'member'
|
||||||
| 'nominal'
|
| 'nominal'
|
||||||
| 'check'
|
| 'assert'
|
||||||
| 'forall'
|
| 'forall'
|
||||||
| 'box'
|
| 'box'
|
||||||
| 'True'
|
| 'True'
|
||||||
|
|
@ -93,4 +95,11 @@ member example_global : Example & ExampleN
|
||||||
|
|
||||||
type TripleConj[X, Y, Z] = X & Y & Z
|
type TripleConj[X, Y, Z] = X & Y & Z
|
||||||
|
|
||||||
|
assert Example <: ExampleN
|
||||||
|
|
||||||
```
|
```
|
||||||
|
|
||||||
|
// A <: B => ...
|
||||||
|
// ==
|
||||||
|
// box (A => B) => ...
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -7,25 +7,16 @@
|
||||||
|
|
||||||
#define PRINTERR(ctx) \
|
#define PRINTERR(ctx) \
|
||||||
do { \
|
do { \
|
||||||
fprintf(stderr, "msph_err: %d (%d)\n", (ctx).err, (ctx).err_info); \
|
fprintf(stderr, "msph_err: %x (%d)\n", (ctx).err, \
|
||||||
|
(ctx).err_info); \
|
||||||
} while (0)
|
} while (0)
|
||||||
|
|
||||||
#ifdef SPHO_DEBUG
|
|
||||||
#define DEBUGFLAG "d"
|
|
||||||
#endif
|
|
||||||
|
|
||||||
struct msph_opts {
|
struct msph_opts {
|
||||||
int tokenize_only;
|
int tokenize_only;
|
||||||
#ifdef DEBUGFLAG
|
|
||||||
int debug;
|
|
||||||
#endif
|
|
||||||
const char *in_path;
|
const char *in_path;
|
||||||
const char *out_path;
|
const char *out_path;
|
||||||
} run_opts = {
|
} run_opts = {
|
||||||
0,
|
0,
|
||||||
#ifdef DEBUGFLAG
|
|
||||||
0,
|
|
||||||
#endif
|
|
||||||
NULL,
|
NULL,
|
||||||
NULL
|
NULL
|
||||||
};
|
};
|
||||||
|
|
@ -52,7 +43,7 @@ main(int argc, char *argv[])
|
||||||
{
|
{
|
||||||
int opt;
|
int opt;
|
||||||
|
|
||||||
while ((opt = getopt(argc, argv, DEBUGFLAG "to:")) != -1) {
|
while ((opt = getopt(argc, argv, "to:")) != -1) {
|
||||||
switch (opt) {
|
switch (opt) {
|
||||||
case 't':
|
case 't':
|
||||||
run_opts.tokenize_only = 1;
|
run_opts.tokenize_only = 1;
|
||||||
|
|
@ -60,11 +51,6 @@ main(int argc, char *argv[])
|
||||||
case 'o':
|
case 'o':
|
||||||
run_opts.out_path = optarg;
|
run_opts.out_path = optarg;
|
||||||
break;
|
break;
|
||||||
#ifdef DEBUGFLAG
|
|
||||||
case 'd':
|
|
||||||
run_opts.debug = 1;
|
|
||||||
break;
|
|
||||||
#endif
|
|
||||||
case '?':
|
case '?':
|
||||||
default:
|
default:
|
||||||
print_usage();
|
print_usage();
|
||||||
|
|
@ -118,7 +104,7 @@ run(struct msph_opts *opts)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
if ((s = msph_token_stream_file(&ctx, in, opts->in_path)) == NULL) {
|
if ((s = msph_token_stream_file(&ctx, in)) == NULL) {
|
||||||
goto err;
|
goto err;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
155
src/msph/token.c
155
src/msph/token.c
|
|
@ -16,7 +16,7 @@ struct msph_matcher {
|
||||||
const int type;
|
const int type;
|
||||||
};
|
};
|
||||||
|
|
||||||
struct msph_matcher token_matcher[] = {
|
struct msph_matcher token_matchers[] = {
|
||||||
{ 0, 0, -1 },
|
{ 0, 0, -1 },
|
||||||
{ 0, 0, TOK_LBRACE },
|
{ 0, 0, TOK_LBRACE },
|
||||||
{ 0, 0, TOK_RBRACE },
|
{ 0, 0, TOK_RBRACE },
|
||||||
|
|
@ -26,6 +26,8 @@ struct msph_matcher token_matcher[] = {
|
||||||
{ 0, 0, TOK_RPAREN },
|
{ 0, 0, TOK_RPAREN },
|
||||||
{ 0, 0, TOK_COLON },
|
{ 0, 0, TOK_COLON },
|
||||||
{ 0, 0, TOK_EQUALS },
|
{ 0, 0, TOK_EQUALS },
|
||||||
|
{ 0, 0, TOK_COMMA },
|
||||||
|
{ 0, 0, TOK_DOT },
|
||||||
|
|
||||||
{ 0, 0, TOK_AMP },
|
{ 0, 0, TOK_AMP },
|
||||||
{ 0, 0, TOK_PIPE },
|
{ 0, 0, TOK_PIPE },
|
||||||
|
|
@ -36,7 +38,7 @@ struct msph_matcher token_matcher[] = {
|
||||||
{ 0, 0, TOK_KW_TYPE },
|
{ 0, 0, TOK_KW_TYPE },
|
||||||
{ 0, 0, TOK_KW_NOMINAL },
|
{ 0, 0, TOK_KW_NOMINAL },
|
||||||
{ 0, 0, TOK_KW_MEMBER },
|
{ 0, 0, TOK_KW_MEMBER },
|
||||||
{ 0, 0, TOK_KW_CHECK },
|
{ 0, 0, TOK_KW_ASSERT },
|
||||||
{ 0, 0, TOK_KW_BOX },
|
{ 0, 0, TOK_KW_BOX },
|
||||||
{ 0, 0, TOK_KW_FORALL },
|
{ 0, 0, TOK_KW_FORALL },
|
||||||
|
|
||||||
|
|
@ -62,6 +64,8 @@ struct msph_token_info {
|
||||||
TOK_INFO(TOK_RPAREN, ")"),
|
TOK_INFO(TOK_RPAREN, ")"),
|
||||||
TOK_INFO(TOK_COLON, ":"),
|
TOK_INFO(TOK_COLON, ":"),
|
||||||
TOK_INFO(TOK_EQUALS, "="),
|
TOK_INFO(TOK_EQUALS, "="),
|
||||||
|
TOK_INFO(TOK_COMMA, ","),
|
||||||
|
TOK_INFO(TOK_DOT, "."),
|
||||||
|
|
||||||
TOK_INFO(TOK_AMP, "&"),
|
TOK_INFO(TOK_AMP, "&"),
|
||||||
TOK_INFO(TOK_PIPE, "|"),
|
TOK_INFO(TOK_PIPE, "|"),
|
||||||
|
|
@ -72,7 +76,7 @@ struct msph_token_info {
|
||||||
TOK_INFO(TOK_KW_TYPE, "type"),
|
TOK_INFO(TOK_KW_TYPE, "type"),
|
||||||
TOK_INFO(TOK_KW_NOMINAL, "nominal"),
|
TOK_INFO(TOK_KW_NOMINAL, "nominal"),
|
||||||
TOK_INFO(TOK_KW_MEMBER, "member"),
|
TOK_INFO(TOK_KW_MEMBER, "member"),
|
||||||
TOK_INFO(TOK_KW_CHECK, "check"),
|
TOK_INFO(TOK_KW_ASSERT, "assert"),
|
||||||
TOK_INFO(TOK_KW_BOX, "box"),
|
TOK_INFO(TOK_KW_BOX, "box"),
|
||||||
TOK_INFO(TOK_KW_FORALL, "forall"),
|
TOK_INFO(TOK_KW_FORALL, "forall"),
|
||||||
|
|
||||||
|
|
@ -80,7 +84,6 @@ struct msph_token_info {
|
||||||
TOK_INFO(TOK_CONST_FALSE, "False"),
|
TOK_INFO(TOK_CONST_FALSE, "False"),
|
||||||
|
|
||||||
TOK_INFO(TOK_IDENT, NULL),
|
TOK_INFO(TOK_IDENT, NULL),
|
||||||
TOK_INFO(TOK_WSPACE, NULL),
|
|
||||||
{ TOK_END , NULL, NULL }
|
{ TOK_END , NULL, NULL }
|
||||||
#undef TOK_INFO
|
#undef TOK_INFO
|
||||||
};
|
};
|
||||||
|
|
@ -113,12 +116,11 @@ void msph_ctx_init(struct msph_ctx *ctx)
|
||||||
}
|
}
|
||||||
|
|
||||||
struct msph_token_stream *
|
struct msph_token_stream *
|
||||||
msph_token_stream_file(struct msph_ctx *ctx, FILE *f, const char *name)
|
msph_token_stream_file(struct msph_ctx *ctx, FILE *f)
|
||||||
{
|
{
|
||||||
size_t res;
|
|
||||||
struct msph_token_stream *ret;
|
struct msph_token_stream *ret;
|
||||||
|
|
||||||
if (ctx == NULL || f == NULL || name == NULL) {
|
if (ctx == NULL || f == NULL) {
|
||||||
MSPH_ERR(ctx, MSPH_ERR_INVAL);
|
MSPH_ERR(ctx, MSPH_ERR_INVAL);
|
||||||
return (NULL);
|
return (NULL);
|
||||||
}
|
}
|
||||||
|
|
@ -135,13 +137,6 @@ msph_token_stream_file(struct msph_ctx *ctx, FILE *f, const char *name)
|
||||||
ret->src.inner.file.pos = 0;
|
ret->src.inner.file.pos = 0;
|
||||||
ret->src.inner.file.end = 0;
|
ret->src.inner.file.end = 0;
|
||||||
|
|
||||||
res = strlcpy(ret->src.inner.file.name, name,
|
|
||||||
sizeof(ret->src.inner.file.name));
|
|
||||||
if (res >= sizeof(ret->src.inner.file.name)) {
|
|
||||||
MSPH_ERR(ctx, MSPH_ERR_TOOLONG);
|
|
||||||
goto err;
|
|
||||||
}
|
|
||||||
|
|
||||||
return (ret);
|
return (ret);
|
||||||
err:
|
err:
|
||||||
if (fclose(f) == EOF)
|
if (fclose(f) == EOF)
|
||||||
|
|
@ -166,18 +161,24 @@ msph_token_stream_frombuf(struct msph_ctx *ctx, const char *buf, size_t len)
|
||||||
ret->ctx = ctx;
|
ret->ctx = ctx;
|
||||||
ret->src.type = MSPH_TOKEN_SRC_STR;
|
ret->src.type = MSPH_TOKEN_SRC_STR;
|
||||||
ret->src.inner.str.s = buf;
|
ret->src.inner.str.s = buf;
|
||||||
ret->src.inner.str.len = len;
|
ret->src.inner.str.len = strnlen(buf, len);
|
||||||
ret->src.inner.str.pos = 0;
|
ret->src.inner.str.pos = 0;
|
||||||
|
|
||||||
return (ret);
|
return (ret);
|
||||||
}
|
}
|
||||||
|
|
||||||
ssize_t
|
ssize_t
|
||||||
msph_token_str(char *buf, size_t len, struct msph_token *tok)
|
msph_token_str(char *buf, size_t len,
|
||||||
|
struct msph_token *tok)
|
||||||
{
|
{
|
||||||
ssize_t ret;
|
ssize_t ret;
|
||||||
|
const char *base;
|
||||||
|
|
||||||
ret = (ssize_t)snprintf(buf, len, "%s", tok_base_str(tok));
|
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)
|
if (ret < 0 || ret >= (ssize_t)len)
|
||||||
return (ret);
|
return (ret);
|
||||||
|
|
@ -187,7 +188,7 @@ msph_token_str(char *buf, size_t len, struct msph_token *tok)
|
||||||
|
|
||||||
switch (tok->type) {
|
switch (tok->type) {
|
||||||
case TOK_IDENT:
|
case TOK_IDENT:
|
||||||
ret += (ssize_t)snprintf(buf, len, "(%s)", tok->d.s.buf);
|
ret += (ssize_t)snprintf(buf, len, "(%s)", tok->data.str);
|
||||||
break;
|
break;
|
||||||
default:
|
default:
|
||||||
break;
|
break;
|
||||||
|
|
@ -196,7 +197,7 @@ msph_token_str(char *buf, size_t len, struct msph_token *tok)
|
||||||
return (ret);
|
return (ret);
|
||||||
}
|
}
|
||||||
|
|
||||||
#define MSPH_TOKEN_PRINT_BUF_LEN 2 * MSPH_TOKEN_BUF_LEN
|
#define MSPH_TOKEN_PRINT_BUF_LEN 2 * MSPH_IDENT_LEN
|
||||||
int
|
int
|
||||||
msph_token_stream_print(struct msph_token_stream *s, FILE *out)
|
msph_token_stream_print(struct msph_token_stream *s, FILE *out)
|
||||||
{
|
{
|
||||||
|
|
@ -204,10 +205,13 @@ msph_token_stream_print(struct msph_token_stream *s, FILE *out)
|
||||||
struct msph_token tok;
|
struct msph_token tok;
|
||||||
char tokstr[MSPH_TOKEN_PRINT_BUF_LEN];
|
char tokstr[MSPH_TOKEN_PRINT_BUF_LEN];
|
||||||
|
|
||||||
while ((ret = msph_token_stream_read_tok( &tok, 1, s)) > 0) {
|
while ((ret = msph_token_stream_read(&tok, 1, s)) > 0) {
|
||||||
|
|
||||||
ret = msph_token_str(tokstr, BUF_LEN(tokstr), &tok);
|
ret = msph_token_str(tokstr, BUF_LEN(tokstr), &tok);
|
||||||
if (ret < 0)
|
if (ret < 0) {
|
||||||
continue;
|
MSPH_ERR_INFO(s->ctx, MSPH_ERR_TOKEN_INVAL, tok.type);
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
|
||||||
if ((size_t)ret < BUF_LEN(tokstr))
|
if ((size_t)ret < BUF_LEN(tokstr))
|
||||||
fprintf(out, "%s\n", tokstr);
|
fprintf(out, "%s\n", tokstr);
|
||||||
|
|
@ -240,9 +244,9 @@ msph_token_stream_close(struct msph_token_stream *s)
|
||||||
return (ret);
|
return (ret);
|
||||||
}
|
}
|
||||||
|
|
||||||
/* -1 or num tokens read */
|
/* -1 on error or num tokens read */
|
||||||
ssize_t
|
ssize_t
|
||||||
msph_token_stream_read_tok(struct msph_token *ptr, size_t n,
|
msph_token_stream_read(struct msph_token *ptr, size_t n,
|
||||||
struct msph_token_stream *s)
|
struct msph_token_stream *s)
|
||||||
{
|
{
|
||||||
size_t ret;
|
size_t ret;
|
||||||
|
|
@ -280,27 +284,88 @@ read_single_tok(struct msph_token *ptr, struct msph_token_stream *s)
|
||||||
return (-1);
|
return (-1);
|
||||||
|
|
||||||
max_m = 0;
|
max_m = 0;
|
||||||
for (m = 1; token_matcher[m].type != TOK_END; m++) {
|
for (m = 1; token_matchers[m].type != TOK_END; m++) {
|
||||||
res = tok_match(ctx, src, &token_matcher[m]);
|
res = tok_match(ctx, src, &token_matchers[m]);
|
||||||
|
|
||||||
if (res == -1)
|
if (res == -1)
|
||||||
return (-1);
|
return (-1);
|
||||||
|
|
||||||
if (res == 0 &&
|
if (res == 0 && token_matchers[m].matchlen >
|
||||||
token_matcher[m].matchlen > token_matcher[max_m].matchlen) {
|
token_matchers[max_m].matchlen) {
|
||||||
max_m = m;
|
max_m = m;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
if (max_m == 0)
|
if (max_m == 0) {
|
||||||
|
if (msph_token_stream_eof(s))
|
||||||
return (0);
|
return (0);
|
||||||
|
MSPH_ERR(s->ctx, MSPH_ERR_TOKEN_NOMATCH);
|
||||||
|
return (-1);
|
||||||
|
}
|
||||||
|
|
||||||
if (tok_commit(ctx, src, &token_matcher[max_m], ptr) == -1)
|
if (tok_commit(ctx, src, &token_matchers[max_m], ptr) == -1)
|
||||||
return (-1);
|
return (-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_create(struct msph_ctx *ctx, int type, union msph_token_data *data)
|
||||||
|
{
|
||||||
|
size_t i;
|
||||||
|
struct msph_token *tok;
|
||||||
|
struct msph_token_info *info;
|
||||||
|
|
||||||
|
info = NULL;
|
||||||
|
|
||||||
|
for (i = 0; token_info[i].type != TOK_END; i++) {
|
||||||
|
if (token_info[i].type == type) {
|
||||||
|
info = &token_info[i];
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
if (info == NULL) {
|
||||||
|
MSPH_ERR_INFO(ctx, MSPH_ERR_TOKEN_INVAL, type);
|
||||||
|
return (NULL);
|
||||||
|
}
|
||||||
|
|
||||||
|
if ((tok = malloc(sizeof(*tok))) == NULL) {
|
||||||
|
MSPH_ERR(ctx, MSPH_ERR_SYS);
|
||||||
|
return (NULL);
|
||||||
|
}
|
||||||
|
|
||||||
|
tok->type = type;
|
||||||
|
|
||||||
|
switch (type) {
|
||||||
|
case TOK_IDENT:
|
||||||
|
memcpy(&tok->data, data, sizeof(*data));
|
||||||
|
break;
|
||||||
|
default:
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
|
||||||
|
return (tok);
|
||||||
|
}
|
||||||
|
|
||||||
static ssize_t
|
static ssize_t
|
||||||
src_file_fill_buf(struct msph_ctx *ctx, struct msph_token_src_file *file)
|
src_file_fill_buf(struct msph_ctx *ctx, struct msph_token_src_file *file)
|
||||||
|
|
@ -316,7 +381,7 @@ src_file_fill_buf(struct msph_ctx *ctx, struct msph_token_src_file *file)
|
||||||
maxread = BUF_LEN(file->buf) - file->end;
|
maxread = BUF_LEN(file->buf) - file->end;
|
||||||
|
|
||||||
if (maxread == 0) {
|
if (maxread == 0) {
|
||||||
MSPH_ERR(ctx, MSPH_ERR_TOOLONG);
|
MSPH_ERR(ctx, MSPH_ERR_TOKEN_TOOLONG);
|
||||||
return (-1);
|
return (-1);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -516,8 +581,8 @@ tok_match(struct msph_ctx *ctx, struct msph_token_src *src,
|
||||||
MATCH_STR("nominal");
|
MATCH_STR("nominal");
|
||||||
case TOK_KW_MEMBER:
|
case TOK_KW_MEMBER:
|
||||||
MATCH_STR("member");
|
MATCH_STR("member");
|
||||||
case TOK_KW_CHECK:
|
case TOK_KW_ASSERT:
|
||||||
MATCH_STR("check");
|
MATCH_STR("assert");
|
||||||
case TOK_KW_BOX:
|
case TOK_KW_BOX:
|
||||||
MATCH_STR("box");
|
MATCH_STR("box");
|
||||||
case TOK_KW_FORALL:
|
case TOK_KW_FORALL:
|
||||||
|
|
@ -574,8 +639,8 @@ tok_commit(struct msph_ctx *ctx, struct msph_token_src *src,
|
||||||
|
|
||||||
file->pos += m->matchlen;
|
file->pos += m->matchlen;
|
||||||
file->pos %= BUF_LEN(file->buf);
|
file->pos %= BUF_LEN(file->buf);
|
||||||
SPHO_ASSERT(file->pos < BUF_LEN(file->buf) ||
|
SPHO_ASSERT(file->pos <= file->end ||
|
||||||
file->pos < pos_old);
|
(file->pos < pos_old && file->pos < BUF_LEN(file->buf)));
|
||||||
|
|
||||||
if (ptr == NULL)
|
if (ptr == NULL)
|
||||||
return (0);
|
return (0);
|
||||||
|
|
@ -584,18 +649,18 @@ tok_commit(struct msph_ctx *ctx, struct msph_token_src *src,
|
||||||
if (! TOK_HAS_DATA(ptr->type))
|
if (! TOK_HAS_DATA(ptr->type))
|
||||||
return (0);
|
return (0);
|
||||||
|
|
||||||
if (m->matchlen >= sizeof(ptr->d.s.buf)) {
|
if (m->matchlen >= sizeof(ptr->data.str)) {
|
||||||
MSPH_ERR(ctx, MSPH_ERR_TOOLONG);
|
MSPH_ERR(ctx, MSPH_ERR_TOKEN_TOOLONG);
|
||||||
return (-1);
|
return (-1);
|
||||||
}
|
}
|
||||||
|
|
||||||
if (fromcbuf_charcpy(ptr->d.s.buf, file->buf, sizeof(file->buf),
|
if (fromcbuf_charcpy(ptr->data.str, file->buf,
|
||||||
pos_old, m->matchlen) == -1) {
|
sizeof(file->buf), pos_old, m->matchlen) == -1) {
|
||||||
MSPH_ERR(ctx, MSPH_ERR_TOOLONG);
|
MSPH_ERR(ctx, MSPH_ERR_TOKEN_TOOLONG);
|
||||||
return (-1);
|
return (-1);
|
||||||
}
|
}
|
||||||
|
|
||||||
ptr->d.s.buf[m->matchlen] = '\0';
|
ptr->data.str[m->matchlen] = '\0';
|
||||||
return (0);
|
return (0);
|
||||||
|
|
||||||
case MSPH_TOKEN_SRC_STR:
|
case MSPH_TOKEN_SRC_STR:
|
||||||
|
|
@ -612,14 +677,14 @@ tok_commit(struct msph_ctx *ctx, struct msph_token_src *src,
|
||||||
if (! TOK_HAS_DATA(ptr->type))
|
if (! TOK_HAS_DATA(ptr->type))
|
||||||
return (0);
|
return (0);
|
||||||
|
|
||||||
if (m->matchlen >= sizeof(ptr->d.s.buf)) {
|
if (m->matchlen >= sizeof(ptr->data.str)) {
|
||||||
MSPH_ERR(ctx, MSPH_ERR_TOOLONG);
|
MSPH_ERR(ctx, MSPH_ERR_TOKEN_TOOLONG);
|
||||||
return (-1);
|
return (-1);
|
||||||
}
|
}
|
||||||
|
|
||||||
memcpy(ptr->d.s.buf, str->s, m->matchlen *
|
memcpy(ptr->data.str, str->s, m->matchlen *
|
||||||
sizeof(str->s[0]));
|
sizeof(str->s[0]));
|
||||||
ptr->d.s.buf[m->matchlen] = '\0';
|
ptr->data.str[m->matchlen] = '\0';
|
||||||
|
|
||||||
return (0);
|
return (0);
|
||||||
default:
|
default:
|
||||||
|
|
|
||||||
761
src/msph/tree.c
Normal file
761
src/msph/tree.c
Normal file
|
|
@ -0,0 +1,761 @@
|
||||||
|
|
||||||
|
#include <sys/queue.h>
|
||||||
|
|
||||||
|
#include <stdlib.h>
|
||||||
|
#include <string.h>
|
||||||
|
|
||||||
|
#define SPHO_ENABLE_DEBUG_PRINT
|
||||||
|
|
||||||
|
#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 void free_the_tree(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)->parent = NULL;
|
||||||
|
T(root)->type = MSPH_TREE_ROOT;
|
||||||
|
|
||||||
|
root->body = NULL;
|
||||||
|
|
||||||
|
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)
|
||||||
|
{
|
||||||
|
int res;
|
||||||
|
struct tree_parse p;
|
||||||
|
struct msph_tree_body *body;
|
||||||
|
|
||||||
|
if (root->body != NULL || T(root)->type != MSPH_TREE_ROOT) {
|
||||||
|
MSPH_ERR(s->ctx, MSPH_ERR_INVAL);
|
||||||
|
return (-1);
|
||||||
|
}
|
||||||
|
|
||||||
|
tree_parse_init(&p, s);
|
||||||
|
EXPECT_READ_NEXT(res, &p, MSPH_TREE_ROOT, return (-1));
|
||||||
|
|
||||||
|
if ((body = tree_parse_body(&p, T(root))) == NULL)
|
||||||
|
return (-1);
|
||||||
|
|
||||||
|
root->body = body;
|
||||||
|
|
||||||
|
return (0);
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
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);
|
||||||
|
}
|
||||||
|
|
||||||
|
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:
|
||||||
|
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;
|
||||||
|
case TOK_RBRACE:
|
||||||
|
if ((tok = msph_token_create(CTX(p), TOK_RBRACE, NULL))
|
||||||
|
== NULL)
|
||||||
|
goto err;
|
||||||
|
tree_parse_push_token(p, tok);
|
||||||
|
goto ret;
|
||||||
|
default:
|
||||||
|
MSPH_ERR_INFO(CTX(p), MSPH_ERR_TREE_NOMATCH,
|
||||||
|
MSPH_TREE_BODY);
|
||||||
|
goto err;
|
||||||
|
}
|
||||||
|
|
||||||
|
if (dir == NULL)
|
||||||
|
goto err;
|
||||||
|
}
|
||||||
|
|
||||||
|
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;
|
||||||
|
|
||||||
|
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:
|
||||||
|
tp = tree_parse_conj(p, parent);
|
||||||
|
break;
|
||||||
|
case TOK_PIPE:
|
||||||
|
tp = tree_parse_disj(p, parent);
|
||||||
|
break;
|
||||||
|
case TOK_IMPL:
|
||||||
|
tp = tree_parse_impl(p, parent);
|
||||||
|
break;
|
||||||
|
case TOK_RARROW:
|
||||||
|
tp = tree_parse_arrow(p, parent);
|
||||||
|
break;
|
||||||
|
case TOK_KW_BOX:
|
||||||
|
tp = tree_parse_box(p, parent);
|
||||||
|
break;
|
||||||
|
case TOK_KW_FORALL:
|
||||||
|
tp = tree_parse_forall(p, parent);
|
||||||
|
break;
|
||||||
|
case TOK_IDENT:
|
||||||
|
tp = tree_parse_name(p, parent);
|
||||||
|
break;
|
||||||
|
case TOK_CONST_TRUE:
|
||||||
|
tp = tree_parse_true(p, parent);
|
||||||
|
break;
|
||||||
|
case TOK_CONST_FALSE:
|
||||||
|
tp = tree_parse_false(p, parent);
|
||||||
|
break;
|
||||||
|
case TOK_LPAREN:
|
||||||
|
tp = tree_parse_paren(p, parent);
|
||||||
|
break;
|
||||||
|
case TOK_LBRACE:
|
||||||
|
tp = tree_parse_trait(p, parent);
|
||||||
|
break;
|
||||||
|
default:
|
||||||
|
MSPH_ERR_INFO(CTX(p), MSPH_ERR_TREE_NOMATCH, MSPH_TREE_TPEXPR);
|
||||||
|
tp = NULL;
|
||||||
|
}
|
||||||
|
|
||||||
|
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, (struct msph_tree *)conj))
|
||||||
|
== NULL)
|
||||||
|
goto err;
|
||||||
|
|
||||||
|
if ((conj->rtp = tree_parse_tpexpr(p, (struct msph_tree *)conj))
|
||||||
|
== NULL)
|
||||||
|
goto err;
|
||||||
|
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;
|
||||||
|
|
||||||
|
if ((disj->rtp = tree_parse_tpexpr(p, (struct msph_tree *)disj))
|
||||||
|
== NULL)
|
||||||
|
goto err;
|
||||||
|
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_PIPE, 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;
|
||||||
|
|
||||||
|
if ((impl->rtp = tree_parse_tpexpr(p, (struct msph_tree *)impl))
|
||||||
|
== NULL)
|
||||||
|
goto err;
|
||||||
|
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 *arrw;
|
||||||
|
|
||||||
|
EXPECT_CURR_TOKEN(p, TOK_PIPE, MSPH_TREE_ARROW, return (NULL));
|
||||||
|
|
||||||
|
if ((arrw = malloc(sizeof(*arrw))) == NULL) {
|
||||||
|
MSPH_ERR(CTX(p), MSPH_ERR_SYS);
|
||||||
|
return (NULL);
|
||||||
|
}
|
||||||
|
T(arrw)->type = MSPH_TREE_ARROW;
|
||||||
|
T(arrw)->parent = parent;
|
||||||
|
arrw->ltp = NULL;
|
||||||
|
arrw->rtp = NULL;
|
||||||
|
|
||||||
|
EXPECT_READ_NEXT(res, p, MSPH_TREE_ARROW, goto err);
|
||||||
|
|
||||||
|
if ((arrw->ltp = tree_parse_tpexpr(p, (struct msph_tree *)arrw))
|
||||||
|
== NULL)
|
||||||
|
goto err;
|
||||||
|
|
||||||
|
if ((arrw->rtp = tree_parse_tpexpr(p, (struct msph_tree *)arrw))
|
||||||
|
== NULL)
|
||||||
|
goto err;
|
||||||
|
err:
|
||||||
|
free_the_tree((struct msph_tree *)arrw);
|
||||||
|
|
||||||
|
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_COLON, 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);
|
||||||
|
}
|
||||||
|
|
||||||
|
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;
|
||||||
|
|
||||||
|
ret = NULL;
|
||||||
|
name = NULL;
|
||||||
|
|
||||||
|
if ((id = tree_parse_ident(p, NULL)) == NULL)
|
||||||
|
return (NULL);
|
||||||
|
|
||||||
|
if ((res = tree_parse_next_token(p)) == 1 &&
|
||||||
|
CURR_TOKEN(p)->type == TOK_LBRAK) {
|
||||||
|
if ((ret = tree_parse_applargs(p, id, parent)) == NULL)
|
||||||
|
goto err;
|
||||||
|
return (ret);
|
||||||
|
} else if (res == -1) {
|
||||||
|
goto err;
|
||||||
|
}
|
||||||
|
|
||||||
|
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;
|
||||||
|
|
||||||
|
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;
|
||||||
|
|
||||||
|
EXPECT_READ_NEXT(res, p, MSPH_TREE_TRAIT, goto err);
|
||||||
|
|
||||||
|
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);
|
||||||
|
}
|
||||||
|
|
||||||
|
static void
|
||||||
|
free_the_tree(struct msph_tree *tree)
|
||||||
|
{
|
||||||
|
/* no one can free the tree :´( */
|
||||||
|
SPHO_POSTCOND((void *)tree == (void *)free);
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue