149 lines
2.7 KiB
C
149 lines
2.7 KiB
C
#ifndef _MSPH_EXPR_H
|
|
#define _MSPH_EXPR_H
|
|
|
|
#include <sys/queue.h>
|
|
|
|
#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_INVAL = -1, // special: invalid, use to mark invalid toks
|
|
TOK_EOF = 0, // special: end-of-file
|
|
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_WSPACE, // whitespace
|
|
|
|
TOK_NOPE // special indicator: end of info array,
|
|
// start of parsing
|
|
};
|
|
|
|
#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 */
|