From 9ac779c1cfc0748a77563503319592b753cb0613 Mon Sep 17 00:00:00 2001
From: Ellen Arvidsson <ellen@log-e.se>
Date: Sat, 19 Apr 2025 20:35:42 +0300
Subject: [PATCH] prefix notation type parser

---
 .clangd               |   2 +
 .gitignore            |   4 +-
 CMakeLists.txt        |   3 +
 include/msph/common.h |  18 +
 include/msph/err.h    |  24 +-
 include/msph/token.h  |  92 ++---
 include/msph/tree.h   | 239 +++++++++++++
 include/spho/err.h    |  21 +-
 include/spho/tp.h     |   3 +-
 include/spho/util.h   |   7 +
 src/msph/README.md    |  15 +-
 src/msph/msph.c       |  22 +-
 src/msph/token.c      | 157 ++++++---
 src/msph/tree.c       | 761 ++++++++++++++++++++++++++++++++++++++++++
 14 files changed, 1217 insertions(+), 151 deletions(-)
 create mode 100644 .clangd
 create mode 100644 include/msph/common.h
 create mode 100644 include/msph/tree.h
 create mode 100644 src/msph/tree.c

diff --git a/.clangd b/.clangd
new file mode 100644
index 0000000..ba4cbb3
--- /dev/null
+++ b/.clangd
@@ -0,0 +1,2 @@
+Diagnostics:
+  UnusedIncludes: None
diff --git a/.gitignore b/.gitignore
index 58189c6..75a6986 100644
--- a/.gitignore
+++ b/.gitignore
@@ -51,9 +51,11 @@ Module.symvers
 Mkfile.old
 dkms.conf
 
-# CMake build directory
+# CMake build dirs
 build-*/
 
+# CMake compile commands
+compile_commands.json
 
 # vim
 .*.swp
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 3067de7..b9c8a66 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -10,6 +10,8 @@ string(JOIN " " CMAKE_C_FLAGS
        "-Werror=int-conversion")
 set(CMAKE_VERBOSE_MAKEFILE ON)
 
+set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
+
 
 include(CheckSymbolExists)
 
@@ -54,6 +56,7 @@ target_compile_definitions(devcheck PRIVATE
 
 set(MSPH_SRC
 	${SRC_DIR}/msph/token.c
+	${SRC_DIR}/msph/tree.c
 	${SRC_DIR}/msph/msph.c
 )
 
diff --git a/include/msph/common.h b/include/msph/common.h
new file mode 100644
index 0000000..0a0bda2
--- /dev/null
+++ b/include/msph/common.h
@@ -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
diff --git a/include/msph/err.h b/include/msph/err.h
index 8fa7795..41a89d9 100644
--- a/include/msph/err.h
+++ b/include/msph/err.h
@@ -10,11 +10,31 @@
 
 #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_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
index 2177b2c..a8896d3 100644
--- a/include/msph/token.h
+++ b/include/msph/token.h
@@ -1,53 +1,11 @@
 #ifndef _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
@@ -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 {
 	TOK_LBRACE,		// {
@@ -99,6 +47,8 @@ enum msph_tok_type {
 	TOK_RPAREN,		// )
 	TOK_COLON,		// :
 	TOK_EQUALS,		// =
+	TOK_COMMA,		// ,
+	TOK_DOT,		// .
 
 	TOK_AMP,		// &
 	TOK_PIPE,		// |
@@ -109,7 +59,7 @@ enum msph_tok_type {
 	TOK_KW_TYPE,		// type
 	TOK_KW_NOMINAL,		// nominal
 	TOK_KW_MEMBER,		// member
-	TOK_KW_CHECK,		// check
+	TOK_KW_ASSERT,		// assert
 	TOK_KW_BOX,		// box
 	TOK_KW_FORALL,		// forall
 
@@ -117,23 +67,20 @@ enum msph_tok_type {
 	TOK_CONST_FALSE,	// False
 
 	TOK_IDENT,		// identifiers
+	TOK_INVAL,		// special: invalid, use to mark invalid toks
 	TOK_WSPACE,		// special: whitespace
 	TOK_END			// special: denote end of array
 };
 
-#define MSPH_TOKEN_BUF_LEN	128
-
-struct token_s {
-	char	buf[MSPH_TOKEN_BUF_LEN];
-};
-
-union token_data {
-	struct token_s	s;
+union msph_token_data {
+	char	str[MSPH_IDENT_LEN];
 };
 
 struct msph_token {
 	int			type;
-	union token_data	d;
+	union msph_token_data	data;
+
+	SLIST_ENTRY(msph_token)	entries;
 };
 
 #define MSPH_FILE_NAME_LEN	1024
@@ -147,9 +94,6 @@ struct msph_token_src_file {
 	size_t		pos;
 	size_t		end;
 	char		buf[MSPH_FILE_BUF_LEN];
-
-	/* file path */
-	char		name[MSPH_FILE_NAME_LEN];
 };
 
 #define MSPH_TOKEN_SRC_STR	2
@@ -178,17 +122,21 @@ struct msph_token_stream {
 void msph_ctx_init(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 *,
 				    const char *, size_t);
 
 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 *);
+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 *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 */
diff --git a/include/msph/tree.h b/include/msph/tree.h
new file mode 100644
index 0000000..601c35f
--- /dev/null
+++ b/include/msph/tree.h
@@ -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
diff --git a/include/spho/err.h b/include/spho/err.h
index 0dd651d..b03411f 100644
--- a/include/spho/err.h
+++ b/include/spho/err.h
@@ -18,17 +18,23 @@
 
 #define SPHO_ERR_BUF_LEN	2048
 
-
+#define SPHO_ERR(ctx, e)						\
+	do {								\
+		(ctx)->err = (e);					\
+		if ((e) == SPHO_ERR_SYS)				\
+			SPHO_ERR_INFO(ctx, e, errno);			\
+		else							\
+			SPHO_ERR_INFO(ctx, e, 0);			\
+	} while (0)
 
 #ifdef SPHO_DEBUG
 
 #define SPHO_ERR_FILEBUF_LEN	128
 
-#define SPHO_ERR(ctx, e)						\
+#define SPHO_ERR_INFO(ctx, e, info)					\
 	do {								\
 		(ctx)->err = (e);					\
-		if ((e) == SPHO_ERR_SYS)				\
-			(ctx)->err_info = errno;			\
+		(ctx)->err_info = (info);				\
 		snprintf((ctx)->filebuf, sizeof((ctx)->filebuf),	\
 		    __FILE__);						\
 		(ctx)->errline = __LINE__;				\
@@ -85,18 +91,17 @@
 
 #else /* SPHO_DEBUG */
 
-#define SPHO_ERR(ctx, e)						\
+#define SPHO_ERR_INFO(ctx, e, info)					\
 	do {								\
 		(ctx)->err = (e);					\
-		if ((e) == SPHO_ERR_SYS)				\
-			(ctx)->err_info = errno;			\
+		(ctx)->err_info = (info);				\
 	} while (0)
 
 #define SPHO_PRECOND(cond)
 #define SPHO_ASSERT(cond)
 #define SPHO_POSTCOND(cond)
 
-#define SPHO_DBG_PRINT(fmt, ...)
+#define SPHO_DEBUG_PRINT(fmt, ...)
 
 #endif /* SPHO_DEBUG */
 
diff --git a/include/spho/tp.h b/include/spho/tp.h
index 19a7ffb..fdbf8bf 100644
--- a/include/spho/tp.h
+++ b/include/spho/tp.h
@@ -86,7 +86,7 @@ union tp_data {
 	struct tp_bappl_data	bappl;
 	struct tp_konst_data	konst;
 	struct tp_var_data	var;
-	struct tp_nominal_data	nom;
+	struct tp_nominal_data	nom; // XXX
 	struct tp_record_data	rec;
 };
 
@@ -126,6 +126,7 @@ struct spho_tp {
 
 STAILQ_HEAD(spho_tp_l, spho_tp);
 
+
 #define SPHO_TP_ERR(tp, err)	SPHO_ERR((tp)->sc->ctx, (err))
 
 struct spho_var	*spho_var_create(struct spho_scope *, char *, size_t);
diff --git a/include/spho/util.h b/include/spho/util.h
index 2871761..2cb9681 100644
--- a/include/spho/util.h
+++ b/include/spho/util.h
@@ -13,6 +13,13 @@ do {									\
 	}								\
 } 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
index 3c87d87..19b3857 100644
--- a/src/msph/README.md
+++ b/src/msph/README.md
@@ -21,7 +21,7 @@ Body ::= Dirs
 Dir ::= Typedef             (directives, with lack of a better name)
       | Memberdef
       | Nominaldecl
-      | Checkdir
+      | Assert
 
 Typedef ::= 'type' Name '=' TExpr                   (type definition/binding)
           | 'type' Name '[' Names ']' '=' TExpr
@@ -31,13 +31,14 @@ Memberdef ::= 'member' Name ':' TExpr
 
 Nominaldecl ::= 'nominal' Name
 
-Checkdir ::= 'check' TExpr '<:' TExpr
+Assert ::= 'assert' TExpr '<:' TExpr
 
 TExpr ::= 'True'
         | 'False'
         | Var
         | Nominal
         | Trait
+        | Appl
         | TExpr '&' TExpr
         | TExpr '|' TExpr
         | TExpr '=>' TExpr
@@ -50,13 +51,14 @@ 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'
-           | 'check'
+           | 'assert'
            | 'forall'
            | 'box'
            | 'True'
@@ -93,4 +95,11 @@ 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
index b85945c..4d540ab 100644
--- a/src/msph/msph.c
+++ b/src/msph/msph.c
@@ -7,25 +7,16 @@
 
 #define PRINTERR(ctx) \
 	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)
 
-#ifdef SPHO_DEBUG
-#define DEBUGFLAG "d"
-#endif
-
 struct msph_opts {
 	int		tokenize_only;
-#ifdef DEBUGFLAG
-	int		debug;
-#endif
 	const char	*in_path;
 	const char	*out_path;
 } run_opts = {
 	0,
-#ifdef DEBUGFLAG
-	0,
-#endif
 	NULL,
 	NULL
 };
@@ -52,7 +43,7 @@ main(int argc, char *argv[])
 {
 	int opt;
 
-	while ((opt = getopt(argc, argv, DEBUGFLAG "to:")) != -1) {
+	while ((opt = getopt(argc, argv, "to:")) != -1) {
 		switch (opt) {
 		case 't':
 			run_opts.tokenize_only = 1;
@@ -60,11 +51,6 @@ main(int argc, char *argv[])
 		case 'o':
 			run_opts.out_path = optarg;
 			break;
-#ifdef DEBUGFLAG
-		case 'd':
-			run_opts.debug = 1;
-			break;
-#endif
 		case '?':
 		default:
 			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;
 	}
 
diff --git a/src/msph/token.c b/src/msph/token.c
index 299e828..0588b7d 100644
--- a/src/msph/token.c
+++ b/src/msph/token.c
@@ -16,7 +16,7 @@ struct msph_matcher {
 	const int	type;
 };
 
-struct msph_matcher token_matcher[] = {
+struct msph_matcher token_matchers[] = {
 	{ 0, 0, -1 },
 	{ 0, 0, TOK_LBRACE },
 	{ 0, 0, TOK_RBRACE },
@@ -26,6 +26,8 @@ struct msph_matcher token_matcher[] = {
 	{ 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 },
@@ -36,7 +38,7 @@ struct msph_matcher token_matcher[] = {
 	{ 0, 0, TOK_KW_TYPE },
 	{ 0, 0, TOK_KW_NOMINAL },
 	{ 0, 0, TOK_KW_MEMBER },
-	{ 0, 0, TOK_KW_CHECK },
+	{ 0, 0, TOK_KW_ASSERT },
 	{ 0, 0, TOK_KW_BOX },
 	{ 0, 0, TOK_KW_FORALL },
 
@@ -62,6 +64,8 @@ struct msph_token_info {
 	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, "|"),
@@ -72,7 +76,7 @@ struct msph_token_info {
 	TOK_INFO(TOK_KW_TYPE, "type"),
 	TOK_INFO(TOK_KW_NOMINAL, "nominal"),
 	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_FORALL, "forall"),
 
@@ -80,7 +84,6 @@ struct msph_token_info {
 	TOK_INFO(TOK_CONST_FALSE, "False"),
 
 	TOK_INFO(TOK_IDENT, NULL),
-	TOK_INFO(TOK_WSPACE, NULL),
 	{ TOK_END , NULL, NULL }
 #undef TOK_INFO
 };
@@ -113,12 +116,11 @@ void msph_ctx_init(struct msph_ctx *ctx)
 }
 
 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;
 
-	if (ctx == NULL || f == NULL || name == NULL) {
+	if (ctx == NULL || f == NULL) {
 		MSPH_ERR(ctx, MSPH_ERR_INVAL);
 		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.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);
 err:
 	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->src.type = MSPH_TOKEN_SRC_STR;
 	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;
 
 	return (ret);
 }
 
 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;
+	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)
 		return (ret);
@@ -187,7 +188,7 @@ msph_token_str(char *buf, size_t len, struct msph_token *tok)
 
 	switch (tok->type) {
 	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;
 	default:
 		break;
@@ -196,7 +197,7 @@ msph_token_str(char *buf, size_t len, struct msph_token *tok)
 	return (ret);
 }
 
-#define MSPH_TOKEN_PRINT_BUF_LEN	2 * MSPH_TOKEN_BUF_LEN
+#define MSPH_TOKEN_PRINT_BUF_LEN	2 * MSPH_IDENT_LEN
 int
 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;
 	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);
-		if (ret < 0)
-			continue;
+		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);
@@ -240,9 +244,9 @@ msph_token_stream_close(struct msph_token_stream *s)
 	return (ret);
 }
 
-/* -1 or num tokens read */
+/* -1 on error or num tokens read */
 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)
 {
 	size_t ret;
@@ -280,27 +284,88 @@ read_single_tok(struct msph_token *ptr, struct msph_token_stream *s)
 		return (-1);
 
 	max_m = 0;
-	for (m = 1; token_matcher[m].type != TOK_END; m++) {
-		res = tok_match(ctx, src, &token_matcher[m]);
+	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_matcher[m].matchlen > token_matcher[max_m].matchlen) {
+		if (res == 0 && token_matchers[m].matchlen >
+		                token_matchers[max_m].matchlen) {
 			max_m = m;
 		}
 	}
 
-	if (max_m == 0)
-		return (0);
+	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_matcher[max_m], ptr) == -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_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
 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;
 
 		if (maxread == 0) {
-			MSPH_ERR(ctx, MSPH_ERR_TOOLONG);
+			MSPH_ERR(ctx, MSPH_ERR_TOKEN_TOOLONG);
 			return (-1);
 		}
 
@@ -516,8 +581,8 @@ tok_match(struct msph_ctx *ctx, struct msph_token_src *src,
 		MATCH_STR("nominal");
 	case TOK_KW_MEMBER:
 		MATCH_STR("member");
-	case TOK_KW_CHECK:
-		MATCH_STR("check");
+	case TOK_KW_ASSERT:
+		MATCH_STR("assert");
 	case TOK_KW_BOX:
 		MATCH_STR("box");
 	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 %= BUF_LEN(file->buf);
-		SPHO_ASSERT(file->pos < BUF_LEN(file->buf) ||
-		    file->pos < pos_old);
+		SPHO_ASSERT(file->pos <= file->end ||
+		    (file->pos < pos_old && file->pos < BUF_LEN(file->buf)));
 
 		if (ptr == NULL)
 			return (0);
@@ -584,18 +649,18 @@ tok_commit(struct msph_ctx *ctx, struct msph_token_src *src,
 		if (! TOK_HAS_DATA(ptr->type))
 			return (0);
 
-		if (m->matchlen >= sizeof(ptr->d.s.buf)) {
-			MSPH_ERR(ctx, MSPH_ERR_TOOLONG);
+		if (m->matchlen >= sizeof(ptr->data.str)) {
+			MSPH_ERR(ctx, MSPH_ERR_TOKEN_TOOLONG);
 			return (-1);
 		}
 
-		if (fromcbuf_charcpy(ptr->d.s.buf, file->buf, sizeof(file->buf),
-			    pos_old, m->matchlen) == -1) {
-			MSPH_ERR(ctx, MSPH_ERR_TOOLONG);
+		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->d.s.buf[m->matchlen] = '\0';
+		ptr->data.str[m->matchlen] = '\0';
 		return (0);
 
 	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))
 			return (0);
 		
-		if (m->matchlen >= sizeof(ptr->d.s.buf)) {
-			MSPH_ERR(ctx, MSPH_ERR_TOOLONG);
+		if (m->matchlen >= sizeof(ptr->data.str)) {
+			MSPH_ERR(ctx, MSPH_ERR_TOKEN_TOOLONG);
 			return (-1);
 		}
 
-		memcpy(ptr->d.s.buf, str->s, m->matchlen *
+		memcpy(ptr->data.str, str->s, m->matchlen *
 		    sizeof(str->s[0]));
-		ptr->d.s.buf[m->matchlen] = '\0';
+		ptr->data.str[m->matchlen] = '\0';
 
 		return (0);
 	default:
diff --git a/src/msph/tree.c b/src/msph/tree.c
new file mode 100644
index 0000000..ec90d36
--- /dev/null
+++ b/src/msph/tree.c
@@ -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);
+}
+
+