diff --git a/.gitignore b/.gitignore
index 4935877..4929d75 100644
--- a/.gitignore
+++ b/.gitignore
@@ -52,8 +52,6 @@ Mkfile.old
 dkms.conf
 
 # vim
-.swp
-.swo
 .*.swp
 .*.swo
 
diff --git a/CMakeLists.txt b/CMakeLists.txt
index ea221d1..99b7405 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -5,10 +5,10 @@ set(CMAKE_C_STANDARD 99)
 set(CMAKE_C_STANDARD_REQUIRED True)
 string(JOIN " " CMAKE_C_FLAGS
 	"-Wall -Wextra -Wformat=2"
-	"-Wconversion -Wsign-conversion -Wimplicit-fallthrough"
-	"-Werror=implicit"
-	"-Werror=incompatible-pointer-types"
-	"-Werror=int-conversion")
+       "-Wconversion -Wsign-conversion -Wimplicit-fallthrough"
+       "-Werror=implicit"
+       "-Werror=incompatible-pointer-types"
+       "-Werror=int-conversion")
 set(CMAKE_VERBOSE_MAKEFILE ON)
 
 set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
diff --git a/CMakePresets.json b/CMakePresets.json
deleted file mode 100644
index f9f5e51..0000000
--- a/CMakePresets.json
+++ /dev/null
@@ -1,82 +0,0 @@
-{
-  "version": 10,
-  "cmakeMinimumRequired": {
-    "major": 3,
-    "minor": 31,
-    "patch": 0
-  },
-  "configurePresets": [
-    {
-      "name": "debug",
-      "displayName": "Debug",
-      "description": "Debug config",
-      "generator": "Unix Makefiles",
-      "binaryDir": "${sourceDir}/build-${presetName}/",
-      "cacheVariables": {
-        "CMAKE_BUILD_TYPE": "Debug"
-      }
-    },
-    {
-      "name": "release",
-      "displayName": "Release",
-      "description": "Release config",
-      "generator": "Unix Makefiles",
-      "binaryDir": "${sourceDir}/build-${presetName}/",
-      "cacheVariables": {
-        "CMAKE_BUILD_TYPE": "Release"
-      }
-    }
-  ],
-  "buildPresets": [
-    {
-      "name": "debug",
-      "configurePreset": "debug"
-    },
-    {
-      "name": "release",
-      "configurePreset": "release"
-    }
-  ],
-  "$comment": [{
-    "testPresets": [
-      {
-        "name": "default",
-        "configurePreset": "default",
-        "output": {"outputOnFailure": true},
-        "execution": {"noTestsAction": "error", "stopOnFailure": true}
-      }
-    ],
-    "packagePresets": [
-      {
-        "name": "default",
-        "configurePreset": "default",
-        "generators": [
-          "TGZ"
-        ]
-      }
-    ],
-    "workflowPresets": [
-      {
-        "name": "default",
-        "steps": [
-          {
-            "type": "configure",
-            "name": "default"
-          },
-          {
-            "type": "build",
-            "name": "default"
-          },
-          {
-            "type": "test",
-            "name": "default"
-          },
-          {
-            "type": "package",
-            "name": "default"
-          }
-        ]
-      }
-    ]
-  }]
-}
diff --git a/README.md b/README.md
index 4259565..8d01411 100644
--- a/README.md
+++ b/README.md
@@ -4,73 +4,14 @@ experimental type system implementation
 
 ## getting and building
 
-This will get you a basic build configured for development and debugging in the
-subdirectory `build-debug/` of repository base:
 ```sh
 git clone https://gitta.log-e.se/lnsol/log-e-sappho.git
 cd ./log-e-sappho
-cmake . --preset=debug
-cd build-debug
+cmake . -B build
+cd build
 make
 ```
 
-To get sane error messages from editors using `clangd` for diagnostics, i.e.
-using the same compilation flags configured for the build by cmake, in the repo
-base directory link `compile_commands.json`:
-```sh
-ln -s build-debug/compile_commands.json
-```
-
-## "Code style"
-
-I learned C from a guy that used to hack on OpenBSD, and just got used to
-writing it this way. If you wanna hack on this yourself, use your judgement.
-Look at the rest of the code and make yours look similar. Like, who cares about
-rules really? Here are some guidelines tho.
-
-**80 columns text width.**
-
-Use **8 spaces wide TABS** (yes, actual TABS, not just 8 spaces) for
-indentation and when inside `while`-/`if`-/etc. **conditions that span multiple
-lines, indent 4 spaces + 0 or more TABS**, as to separate condition from body
-of the conditional statement.
-
-(Look at the following examples using a tab width of 8, otherwise they won't
-make much sense.)
-
-I.e. do
-```c
-if (1 /* this is a very long condition */
-    == 2 /* spanning multiple lines */
-	    || 2 < 3 /* and we indent like this */) {
-	this = the_way;
-	/* as to increase distinguishability of condition from body */
-}
-```
-not
-```c
-if ( /* ... */
-	2 < 3) {
-	eyes = bleeding;
-}
-```
-
-Conditional statements without `{ .. }` is okay (preferred) if the condition
-fits on one line.
-
-I.e. do
-```c
-if (1 /* short condition that fits on one line */)
-	u = the_best;
-```
-and
-```c
-if (the_variable_that_has_that_long_name = function_with_a_long_name_too(
-	    arg_is_shorter_tho)) {
-	gesture = clapping;
-}
-```
-
 ## repository content
 
 This repository contains:
diff --git a/docs/about/formalities.md b/docs/about/formalities.md
index 246c2e2..b2b01f1 100644
--- a/docs/about/formalities.md
+++ b/docs/about/formalities.md
@@ -8,7 +8,7 @@ s, t ::= s | t              (disjunction, a.k.a. union)
        | s => t             (implication)
        | s -> t             (arrow, a.k.a. function)
        | forall x . t       (forall, polymorphic)
-       | box t              (box, c.f. modal logic)
+       | box t              (box, c.f. modular logic)
        | a [t..]            (type operator application)
        | x                  (variable)
        | n                  (nominal)
@@ -37,23 +37,23 @@ s, γ ⊢ s, δ
 ---- [false-left]
 false, γ ⊢ δ
 
-// trace pairs: none?
+// trace pairs: none
 s, t, γ ⊢ δ
 ---- [conj-left]
 s & t, γ ⊢ δ
 
-// trace pairs: none?
+// trace pairs: none
 γ ⊢ s, t, δ
 ---- [disj-right]
 γ ⊢ s | t, δ
 
-// trace pairs: none?
+// trace pairs: none
 s, γ ⊢ δ
 t, γ ⊢ δ
 ---- [disj-left]
 s | t, γ ⊢ δ
 
-// trace pairs: none?
+// trace pairs: none
 γ ⊢ s, δ
 γ ⊢ t, δ
 ---- [conj-right]
@@ -61,12 +61,12 @@ s | t, γ ⊢ δ
 
 // XXX
 // remove s => t? always make progress
-// trace pairs: none?
+// trace pairs: none
 s => t, s, t, γ ⊢ δ
 ---- [impl-left]
 s => t, s, γ ⊢ δ
 
-// trace pairs: none?
+// trace pairs: none
 s, γ ⊢ t, δ
 ---- [impl-right]
 γ ⊢ s => t, δ
@@ -89,7 +89,7 @@ box t, γ ⊢ δ
 // to exclude typedefs like
 // type A = A
 // Or that our cycle detection excludes paths between "identical" states.
-// trace pairs: none?
+// trace pairs: none
 γ ⊢ expand(a[t..]), δ
 ----
 γ ⊢ a[t..], δ
@@ -114,19 +114,17 @@ n fresh
 ---- [forall]
 γ ⊢ δ
 
-// TODO can we choose a simpler rule instead?
 // 1 + n! premises
 // trace pairs: i ∈ [1..(n! + 1)], premise[i] -- conclusion
-c, γ*  ⊢ a_1, ..., a_n, δ*
+c, γ*  ⊢ a_1, ..., a_n
 ∀ I ⊆ {1, ..., n}.
 	c, γ* ⊢ { a_i | i ∈ I }, δ*
 	OR
 	{ b_i | i ∈ ¬I }, γ* ⊢ d, δ*
 ---- [loads-of-fun]
-a_1 -> b_1, ..., a_n -> b_n, γ    ⊢    c -> d, δ
+a_1 -> b_1, ..., a_n -> b_n, γ ⊢ c -> d, δ
 ```
 
-
 ### context operators
 
 * box filtering
diff --git a/docs/about/progress.md b/docs/about/progress.md
index 9b71035..40c97dc 100644
--- a/docs/about/progress.md
+++ b/docs/about/progress.md
@@ -1,9 +1,11 @@
-# sappho short
+# draft of presentation
+
+## sappho short
 	- sappho types intro
 	- a quick look at msph and spho
 
 
-## The types
+### The types
 
 We take a look at the grammar for sappho types
 
@@ -13,7 +15,7 @@ s, t ::= s | t              (disjunction, a.k.a. union)
        | s => t             (implication)
        | s -> t             (arrow, a.k.a. function)
        | forall x . t       (forall, polymorphic)
-       | box t              (box, c.f. modal logic)
+       | box t              (box, c.f. modular logic)
        | a [t..]            (type operator application)
        | x                  (variable)
        | n                  (nominal)
@@ -28,7 +30,7 @@ n ∈ nominal
 a ∈ opname
 ```
 
-The type `t <: s` would be syntactic sugar for `box (t => s)`
+The type `t <: s` would be expressive sugar for `box (t => s)`
 
 ### msph and spho
 
@@ -58,7 +60,7 @@ Thoughts
 * maybe eventually add a basic term language and interpreter
 * can we use external software/libraries for proof search?
 
-# interpretation of types
+## interpretation of types
 	- example programs in `msph`
 		- unified syntax for types and bounded polymorphism
 		- example: self typing
@@ -73,8 +75,7 @@ Check formalities.md.
 	- simple rules
 	- type constructor rules
 	- recursion and cyclic proofs
-
-# next steps?
+* next steps?
 	- formals:
 		- formulate theorems
 			- if we use semantic subtyping, isn't it enough to
@@ -84,4 +85,3 @@ Check formalities.md.
 		- simple rules, should be fairly simple
 		- type constructors, straightforward hopefully
 		- recursion and cyclic proofs... `¯\_(ツ)_/¯`
-	- describe use of language with type system (interpretation of types)
diff --git a/example/comparable.msph b/example/comparable.msph
deleted file mode 100644
index 2f73457..0000000
--- a/example/comparable.msph
+++ /dev/null
@@ -1,16 +0,0 @@
-nominal lt
-nominal eq
-nominal gt
-
-type ord = lt | eq | gt
-
-type comparable[t] = {
-	member cmp : t -> ord
-}
-
-
-type integer = {
-	member cmp : integer -> ord
-}
-
-assert integer <: comparable[integer]
diff --git a/example/ex1.msph b/example/ex1.msph
new file mode 100644
index 0000000..0844c3f
--- /dev/null
+++ b/example/ex1.msph
@@ -0,0 +1,4 @@
+
+nominal C
+
+
diff --git a/example/ex2.msph b/example/ex2.msph
new file mode 100644
index 0000000..5b85fdc
--- /dev/null
+++ b/example/ex2.msph
@@ -0,0 +1 @@
+type A = & C D
diff --git a/example/ex3.msph b/example/ex3.msph
new file mode 100644
index 0000000..9770336
--- /dev/null
+++ b/example/ex3.msph
@@ -0,0 +1,13 @@
+
+type X = & C (| D E)
+
+type Y = {
+	member x : X
+	type Z = & X {
+ 		type T = C
+		assert C <: D
+	}
+	member r : (box forall S. (=> S Y))
+	member s : C[X, Y, z]
+	member f : -> A B
+}
diff --git a/example/ex4.msph b/example/ex4.msph
new file mode 100644
index 0000000..ffc0174
--- /dev/null
+++ b/example/ex4.msph
@@ -0,0 +1,20 @@
+nominal M
+nominal N
+nominal O
+nominal P
+
+type A = {
+	member member1: & N M
+	member member2: | M N
+}
+
+type B = forall X. {
+	member member1 : & X A
+}
+
+member outer1 : box {
+	member member1: & B True
+	type T = & B A
+	member member2 : | (& T O) P
+	type S = & B False
+}
diff --git a/example/ex5.msph b/example/ex5.msph
new file mode 100644
index 0000000..5774e54
--- /dev/null
+++ b/example/ex5.msph
@@ -0,0 +1,21 @@
+nominal N
+nominal M
+
+
+type T[X, Y] = {
+	// body
+}
+
+type A = T[N, M] // binding X -> N, Y -> M
+type B = T[M, N] // binding X -> M, Y -> N
+
+// converted to
+
+type A = ⟨ X -> N, Y -> M ⟩ {
+	// body
+}
+type B = ⟨ X -> M, Y -> N ⟩ {
+	// body
+}
+
+
diff --git a/example/graph.msph b/example/graph.msph
deleted file mode 100644
index b636f3b..0000000
--- a/example/graph.msph
+++ /dev/null
@@ -1,10 +0,0 @@
-type gnode[e] = {
-	member edges : iterable[e]
-}
-
-type gedge[n] = {
-	member src : n
-	member dst : n
-}
-
-type graph[n, e] = (n <: gnode[e]) & (e <: gedge[n])
diff --git a/example/non-parse/ex6.msph b/example/non-parse/ex6.msph
new file mode 100644
index 0000000..afdeccb
--- /dev/null
+++ b/example/non-parse/ex6.msph
@@ -0,0 +1,21 @@
+type A[X, Y] = {
+	type B[Z] = {
+		mb : X & Z
+	}
+
+	ma : B[Y]
+}
+
+
+m : A[M, N]
+
+
+m : ⟨X -> M, Y -> N⟩ {
+	ma : B[Y]
+}
+
+m : ⟨X -> M, Y -> N⟩ {
+	ma : ⟨Z -> Y⟩  {
+		mb : X & Z
+	}
+}
diff --git a/example/self.msph b/example/self.msph
deleted file mode 100644
index d482e1c..0000000
--- a/example/self.msph
+++ /dev/null
@@ -1,19 +0,0 @@
-type Accumulator[Self] = (Self <: Accumulator[Self]) & {
-	member add : Int -> Self
-}
-
-type MyAccum = {
-	member add : Int -> MyAccum
-}
-
-assert MyAccum <: Accumulator[MyAccum]
-
-
-
-
-
-type Acchmmmmulator[Self] = (Self <: Acchmmmmulator[Self]) => {
-	member add : Int -> Self
-}
-
-
diff --git a/example/rec-lockstep.msph b/example/subt/rec-lockstep.msph
similarity index 100%
rename from example/rec-lockstep.msph
rename to example/subt/rec-lockstep.msph
diff --git a/include/msph/msph.h b/include/msph/common.h
similarity index 85%
rename from include/msph/msph.h
rename to include/msph/common.h
index f34980b..eb49da4 100644
--- a/include/msph/msph.h
+++ b/include/msph/common.h
@@ -1,5 +1,5 @@
-#ifndef _MSPH_H
-#define _MSPH_H
+#ifndef _MSPH_COMMON_H
+#define _MSPH_COMMON_H
 
 #include "msph/err.h"
 #include "spho/ctx.h"
@@ -25,4 +25,4 @@ struct msph_text_pos {
 	unsigned int	col;
 };
 
-#endif /* ifndef _MSPH_H */
+#endif
diff --git a/include/msph/token.h b/include/msph/token.h
index 18fb7ae..b984039 100644
--- a/include/msph/token.h
+++ b/include/msph/token.h
@@ -3,7 +3,7 @@
 
 #include <sys/queue.h>
 
-#include "msph/msph.h"
+#include "msph/common.h"
 
 /*
  *
@@ -39,8 +39,6 @@
 
 
 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,		// [
@@ -69,10 +67,9 @@ enum msph_tok_type {
 	TOK_CONST_FALSE,	// False
 
 	TOK_IDENT,		// identifiers
-	TOK_WSPACE,		// whitespace
-
-	TOK_NOPE		// special indicator: end of info array,
-				//		      start of parsing
+	TOK_INVAL,		// special: invalid, use to mark invalid toks
+	TOK_WSPACE,		// special: whitespace
+	TOK_END			// special: end of array/token stream
 };
 
 #define MSPH_TAB_WIDTH		8
diff --git a/include/msph/tree.h b/include/msph/tree.h
index 3fffcfc..028f329 100644
--- a/include/msph/tree.h
+++ b/include/msph/tree.h
@@ -3,7 +3,7 @@
 
 #include <sys/queue.h>
 
-#include "msph/msph.h"
+#include "msph/common.h"
 #include "msph/token.h"
 
 /* tree decorations */
@@ -37,8 +37,6 @@ struct msph_decor {
 #define MSPH_TREE_BOX		0x004a
 #define MSPH_TREE_FORALL	0x004b
 #define MSPH_TREE_PAREN		0x004c
-#define MSPH_TREE_SUBT		0x004d
-
 
 #define MSPH_TREE_IDENT		0x0100
 #define MSPH_TREE_NAMEDECL	0x0101
@@ -164,7 +162,8 @@ struct msph_tree_membdecl {
 struct msph_tree_assert {
 	struct msph_tree_dir	hd_dir;
 
-	struct msph_tree_tpexpr	*tp;
+	struct msph_tree_tpexpr	*ltp;
+	struct msph_tree_tpexpr	*rtp;
 };
 
 struct msph_tree_namedecl {
@@ -210,7 +209,6 @@ struct msph_tree_trait {
 	struct msph_tree_body	*body;
 };
 
-/* XXX should probably merge all binary type ops into one */
 struct msph_tree_conj {
 	struct msph_tree_tpexpr	hd_tpe;
 
@@ -232,13 +230,6 @@ struct msph_tree_impl {
 	struct msph_tree_tpexpr	*rtp;
 };
 
-struct msph_tree_subt {
-	struct msph_tree_tpexpr	hd_tpe;
-
-	struct msph_tree_tpexpr	*ltp;
-	struct msph_tree_tpexpr	*rtp;
-};
-
 struct msph_tree_arrow {
 	struct msph_tree_tpexpr	hd_tpe;
 
@@ -268,11 +259,7 @@ struct msph_tree_paren {
 
 struct msph_tree_root	*msph_tree_makeroot(struct msph_ctx *);
 
-#define MSPH_PARSE_PREFIX	1
-#define MSPH_PARSE_INFIX	2
-
-int	msph_tree_parse(struct msph_token_stream *, struct msph_tree_root *,
-	    int);
+int	msph_tree_parse(struct msph_token_stream *, struct msph_tree_root *);
 
 ssize_t	msph_tree_fprint(FILE *, struct msph_tree *);
 
diff --git a/include/spho/ctx.h b/include/spho/ctx.h
index 00bb1f4..9858e85 100644
--- a/include/spho/ctx.h
+++ b/include/spho/ctx.h
@@ -14,8 +14,6 @@ struct spho_ctx {
 	int	err_info;
 	char	errbuf[SPHO_ERR_BUF_LEN];
 
-	unsigned int	nom_cnt;
-
 #ifdef SPHO_DEBUG
 	char	filebuf[SPHO_ERR_FILEBUF_LEN];
 	int	errline;
@@ -24,7 +22,6 @@ struct spho_ctx {
 };
 
 struct spho_ctx		*spho_ctx_create(void);
-void			spho_ctx_init(struct spho_ctx *);
 void			spho_ctx_destroy(struct spho_ctx *);
 const char		*spho_ctx_strerror(struct spho_ctx *);
 
diff --git a/include/spho/err.h b/include/spho/err.h
index 6e34929..2f56532 100644
--- a/include/spho/err.h
+++ b/include/spho/err.h
@@ -39,7 +39,7 @@
 		(ctx)->err = (e);					\
 		(ctx)->err_info = (info);				\
 		snprintf((ctx)->filebuf, sizeof((ctx)->filebuf),	\
-		    __FILE__ ":%s", __func__);				\
+		    __FILE__);						\
 		(ctx)->errline = __LINE__;				\
 	} while (0)
 
diff --git a/include/spho/scope.h b/include/spho/scope.h
index 52362e8..ff682c4 100644
--- a/include/spho/scope.h
+++ b/include/spho/scope.h
@@ -7,22 +7,13 @@
 
 #define SPHO_NOM_LEN	128
 
-
-union spho_ext_data {
-	void		*ptr;
-	uint64_t	n;
-};
-
 /* name */
 struct spho_nom {
-	unsigned int		id;
 	char			s[SPHO_NOM_LEN];
-
-	union spho_ext_data	ext_data;
-
-	SLIST_ENTRY(spho_nom)	entries; 
+	SLIST_ENTRY(spho_nom)	next; // TODO change to allocs
 };
 
+SLIST_HEAD(spho_nom_l, spho_nom);
 
 
 #define TP_KONST_KEY_TRUE	0x43445 /* don't change!!!!! */
@@ -85,7 +76,6 @@ struct spho_tp {
 
 	int			kind;
 	union tp_data		d;
-	union spho_ext_data	ext_data;
 
 	STAILQ_ENTRY(spho_tp)	entries;
 };
@@ -95,20 +85,30 @@ struct spho_tp_op {
 
 	struct spho_scope	*op_sc;
 	struct spho_tp		*op_tp;
-	union spho_ext_data	ext_data;
 };
 
 STAILQ_HEAD(spho_tp_l, spho_tp);
 
+struct spho_tp_ptr {
+	struct spho_tp *p;
+	STAILQ_ENTRY(spho_tp_ptr)	entries;
+};
+
+STAILQ_HEAD(spho_tp_ptr_l, spho_tp_ptr);
+
 struct spho_tp_alloc {
 	union {
 		struct spho_tp		tp;
 		struct spho_tp_op	tp_op;
 	}		alloc;
 
-	STAILQ_ENTRY(spho_tp_alloc)	entries;
+	TAILQ_ENTRY(spho_tp_alloc)	allocs;
 };
 
+TAILQ_HEAD(spho_tp_alloc_l, spho_tp_alloc);
+
+SLIST_HEAD(spho_scope_l, spho_scope);
+
 /* defined in spho/bind.h */
 struct spho_bind;
 
@@ -116,38 +116,33 @@ struct spho_scope {
 	struct spho_ctx		*ctx;
 	struct spho_scope	*parent;
 
-	STAILQ_HEAD(
-	    spho_scope_l,
-	    spho_scope)		subs;
-	STAILQ_HEAD(
-	    spho_tp_alloc_l,
-	    spho_tp_alloc)	tps;
-	SLIST_HEAD(
-	    spho_nom_l,
-	    spho_nom)		noms;
-	size_t			nom_cnt;
-	struct spho_prebind	*bind_loc;
-	union spho_ext_data	ext_data;
+	struct spho_scope_l	subs;
 
-	STAILQ_ENTRY(spho_scope)	entries;
+	size_t			n_noms;
+	struct spho_nom_l	noms;
+	struct spho_tp_alloc_l	tps;
+
+	struct spho_prebind	*bind_loc;
+
+	SLIST_ENTRY(spho_scope)	next;
 };
 
 #define SPHO_SC_ERR(sc, err)	SPHO_ERR((sc)->ctx, (err))
 
-void	spho_scope_init(struct spho_scope *, struct spho_ctx *,
+int	spho_scope_init(struct spho_scope *, struct spho_ctx *,
 	    struct spho_scope *);
-void	spho_scope_cleanup(struct spho_scope *);
+void	spho_scope_term(struct spho_scope *);
 
 struct spho_scope	*spho_scope_global(struct spho_ctx *);
-struct spho_scope	*spho_scope_create_subscope(struct spho_scope *);
+struct spho_scope	*spho_scope_create(struct spho_scope *);
 
 
-void spho_scope_free(struct spho_scope *);
+void spho_scope_destroy(struct spho_scope *);
 
 struct spho_nom	*spho_scope_nom_add(struct spho_scope *, const char *, size_t);
-int	spho_scope_nom_lookup(struct spho_scope *, const char *, size_t,
+int	spho_scope_nom_lookup_str(struct spho_scope *, const char *, size_t,
 	    struct spho_nom **);
-int	spho_scope_nom_lookup_strict(struct spho_scope *, const char *,
+int	spho_scope_nom_lookup_str_strict(struct spho_scope *, const char *,
 	    size_t, struct spho_nom **);
 
 int	spho_scope_prebind_init(struct spho_scope *);
diff --git a/src/msph/msph.c b/src/msph/msph.c
index c9d3afe..041bdff 100644
--- a/src/msph/msph.c
+++ b/src/msph/msph.c
@@ -2,20 +2,28 @@
 #include <stdio.h>
 #include <unistd.h>
 
-#include "msph/msph.h"
+#include "msph/err.h"
 #include "msph/token.h"
 #include "msph/tree.h"
 #include "msph/sphophi.h"
 
+struct msph_opts {
+	int		tokenize_only;
+	const char	*in_path;
+	const char	*out_path;
+} run_opts = {
+	0,
+	NULL,
+	NULL
+};
+
 
 #define USAGE \
-"msph: micro sappho\n" \
-"	Usage: msph [-t] [-o out_path] [-p i|p] [in_path]\n" \
-"\n" \
-"	-t			- print tokenization\n" \
-"	-o			- output path\n" \
-"	-p i[nfix]|p[refix]	- infix or prefix &, |, =>, -> parsing\n" \
-"				  (default infix)\n"
+	"msph: micro sappho\n" \
+	"\tUsage: msph [-t] [-o out_path] [in_path]\n" \
+	"\n" \
+	"\t-t	- print tokenization\n" \
+	"\t-o	- output path\n"
 
 void
 print_usage(void)
@@ -23,64 +31,6 @@ print_usage(void)
 	printf("%s", USAGE);
 }
 
-struct err_info {
-	int		err;
-	const char	*msg;
-} errinfo[] = {
-	{ MSPH_ERR_SYS, "system error" },
-	{ MSPH_ERR_INVAL, "invalid argument" },
-	{ MSPH_ERR_TOOLONG, "input too long" },
-
-	{ MSPH_ERR_TOKEN_TOOLONG, "token too long" },
-	{ MSPH_ERR_TOKEN_EOF, "tokenizer reached end of file" },
-	{ MSPH_ERR_TOKEN_NOMATCH, "no matching token" },
-	{ MSPH_ERR_TOKEN_INVAL, "token invalid" },
-
-	{ MSPH_ERR_TREE_TOOLONG, "parsed data too long" },
-	{ MSPH_ERR_TREE_EOF, "parsing reached unexpected end of file" },
-	{ MSPH_ERR_TREE_NOMATCH, "parser matching failed" },
-
-	{ MSPH_ERR_TYPE_INVAL, "invalid type" },
-
-	{ MSPH_ERR_SPHOPHI, "spho error" },
-	{ -1, NULL }
-};
-
-void
-print_error(struct msph_ctx *ctx)
-{
-	size_t i;
-	const char *err_msg;
-
-	err_msg = NULL;
-	for (i = 0; errinfo[i].err != -1; i++) {
-		if (ctx->err == errinfo[i].err) {
-			err_msg = errinfo[i].msg;
-			break;
-		}
-	}
-	if (err_msg == NULL) {
-		err_msg = "unknown error";
-	}
-
-	fprintf(stderr, "ERROR(%x, %d):%s\n", ctx->err, ctx->err_info, err_msg);
-
-	if (ctx->err == MSPH_ERR_SPHOPHI)
-		fprintf(stderr, "\t%s\n", spho_ctx_strerror(ctx->spho));
-}
-
-struct msph_opts {
-	int		tokenize_only;
-	int		parser;
-	const char	*in_path;
-	const char	*out_path;
-} run_opts = {
-	0,
-	MSPH_PARSE_INFIX,
-	NULL,
-	NULL
-};
-
 int run(struct msph_opts *);
 
 int
@@ -88,7 +38,7 @@ main(int argc, char *argv[])
 {
 	int opt;
 
-	while ((opt = getopt(argc, argv, "hto:p:")) != -1) {
+	while ((opt = getopt(argc, argv, "hto:")) != -1) {
 		switch (opt) {
 		case 't':
 			run_opts.tokenize_only = 1;
@@ -96,19 +46,6 @@ main(int argc, char *argv[])
 		case 'o':
 			run_opts.out_path = optarg;
 			break;
-		case 'p':
-			switch (optarg[0]) {
-			case 'p':
-				run_opts.parser = MSPH_PARSE_PREFIX;
-				break;
-			case 'i':
-				run_opts.parser = MSPH_PARSE_INFIX;
-				break;
-			default:
-				print_usage();
-				exit(EXIT_FAILURE);
-			}
-			break;
 		case 'h':
 			print_usage();
 			exit(EXIT_SUCCESS);
@@ -144,7 +81,6 @@ run(struct msph_opts *opts)
 	struct msph_tree_root *root;
 	FILE *in, *out;
 
-
 	in = out = NULL;
 	s = NULL;
 	root = NULL;
@@ -186,7 +122,7 @@ run(struct msph_opts *opts)
 		goto err;
 	}
 
-	if (msph_tree_parse(s, root, opts->parser) == -1)
+	if (msph_tree_parse(s, root) == -1)
 		goto err;
 
 	printf("msph tree successfully parsed :)\n");
@@ -204,7 +140,13 @@ exit:
 	return (0);
 
 err:
-	print_error(&ctx);
+	if (root != NULL && ctx.err == MSPH_ERR_SPHOPHI) {
+		fprintf(stderr, "ERROR:%s\n",
+		    spho_ctx_strerror(ctx.spho));
+	} else {
+		fprintf(stderr, "ERROR:msph_err: %x (%d)\n", (ctx).err,
+		    (ctx).err_info);
+	}
 
 	if (in)
 		fclose(in);
@@ -214,7 +156,6 @@ err:
 }
 
 
-
 void
 msph_ctx_init(struct msph_ctx *ctx)
 {
diff --git a/src/msph/sphophi.c b/src/msph/sphophi.c
index 0a629b5..a9dec26 100644
--- a/src/msph/sphophi.c
+++ b/src/msph/sphophi.c
@@ -15,7 +15,7 @@ static int	msph_tree_sphophi_decor_tpexpr_nom(struct spho_scope *,
 		    struct msph_tree *);
 static int	msph_tree_sphophi_decor_tp(struct spho_scope *,
 		    struct msph_tree *);
-static int	msph_tree_sphophi_prebind(struct spho_scope *,
+static int	msph_tree_sphophi_tp_prebind(struct spho_scope *,
 		    struct msph_tree *);
 
 /* is the tree a name binding? */
@@ -65,8 +65,6 @@ static int	msph_sphophi_foreach_pre_disj(msph_tree_sphophi_f,
 		    struct spho_scope *, struct msph_tree_disj *);
 static int	msph_sphophi_foreach_pre_impl(msph_tree_sphophi_f,
 		    struct spho_scope *, struct msph_tree_impl *);
-static int	msph_sphophi_foreach_pre_subt(msph_tree_sphophi_f,
-		    struct spho_scope *, struct msph_tree_subt *);
 static int	msph_sphophi_foreach_pre_arrow(msph_tree_sphophi_f,
 		    struct spho_scope *, struct msph_tree_arrow *);
 static int	msph_sphophi_foreach_pre_box(msph_tree_sphophi_f,
@@ -111,8 +109,6 @@ static int	msph_sphophi_foreach_post_disj(msph_tree_sphophi_f,
 		    struct spho_scope *, struct msph_tree_disj *);
 static int	msph_sphophi_foreach_post_impl(msph_tree_sphophi_f,
 		    struct spho_scope *, struct msph_tree_impl *);
-static int	msph_sphophi_foreach_post_subt(msph_tree_sphophi_f,
-		    struct spho_scope *, struct msph_tree_subt *);
 static int	msph_sphophi_foreach_post_arrow(msph_tree_sphophi_f,
 		    struct spho_scope *, struct msph_tree_arrow *);
 static int	msph_sphophi_foreach_post_box(msph_tree_sphophi_f,
@@ -158,7 +154,7 @@ msph_sphophi_tp(struct msph_tree_root *root)
 int
 msph_sphophi_tp_prebind(struct msph_tree_root *root)
 {
-	return (msph_sphophi_foreach_pre(msph_tree_sphophi_prebind,
+	return (msph_sphophi_foreach_pre(msph_tree_sphophi_tp_prebind,
 		    root));
 }
 
@@ -195,25 +191,25 @@ msph_tree_sphophi_decor_scope(struct spho_scope *sc, struct msph_tree *tree)
 	case MSPH_TREE_UNIT:
 	case MSPH_TREE_TRAIT:
 	case MSPH_TREE_FORALL:
-		if ((SCOPE(tree) = spho_scope_create_subscope(sc)) == NULL)
-			return (-1);
+		if ((SCOPE(tree) = spho_scope_create(sc)) == NULL)
+			ret = -1;
 		ADD_FLAG(tree, MSPH_TREE_FLAG_SCOPE);
 		break;
 	case MSPH_TREE_TPDEF:
 		tpdef = (struct msph_tree_tpdef *)tree;
-		if (STAILQ_EMPTY(&tpdef->params))
-			break;
-		if (((SCOPE(tpdef) = spho_scope_create_subscope(sc)) == NULL))
-			return (-1);
+		if (! STAILQ_EMPTY(&tpdef->params) &&
+		    ((SCOPE(tpdef) = spho_scope_create(sc)) == NULL)) {
+			ret = -1;
+		}
 		ADD_FLAG(tree, MSPH_TREE_FLAG_SCOPE);
 		break;
-	case MSPH_TREE_NAMEDECL:
-		SPHO_ASSERT(IS_BINDING(tree->parent));
+	case MSPH_TREE_IDENT:
+		if (! IS_BINDING(tree->parent))
+			break;
 		ident = (struct msph_tree_ident *)tree;
 		if ((NOM(ident) = spho_scope_nom_add(sc, ident->str,
-			    sizeof(ident->str))) == NULL) {
-			return (-1);
-		}
+			    sizeof(ident->str))) == NULL)
+			ret = -1;
 		ADD_FLAG(tree, MSPH_TREE_FLAG_NOM);
 		break;
 	default:
@@ -234,14 +230,12 @@ msph_tree_sphophi_decor_tpexpr_nom(struct spho_scope *sc,
 
 	switch (TREE_ID(tree)) {
 	case MSPH_TREE_IDENT:
-		SPHO_ASSERT(IS_TPEXPR(tree->parent));
-
+		if (! IS_TPEXPR(tree->parent))
+			break;
 		ident = (struct msph_tree_ident *)tree;
-		if (spho_scope_nom_lookup_strict(sc, ident->str,
-		    sizeof(ident->str), &NOM(ident)) == -1) {
-			return (-1);
-		}
-		ADD_FLAG(ident, MSPH_TREE_FLAG_NOM);
+		ret = spho_scope_nom_lookup_str_strict(sc, ident->str,
+			    sizeof(ident->str), &NOM(ident));
+
 		break;
 	default:
 		break;
@@ -267,7 +261,6 @@ msph_tree_sphophi_decor_tp(struct spho_scope *sc, struct msph_tree *tree)
 	struct msph_tree_trait *trait;
 	struct msph_tree_dir *dir;
 	struct msph_tree_membdecl *membd;
-	struct msph_tree_subt *subt;
 
 	struct spho_tp_l *tps;
 	struct spho_tp *tp, *tp_memb;
@@ -278,59 +271,43 @@ msph_tree_sphophi_decor_tp(struct spho_scope *sc, struct msph_tree *tree)
 	dir = NULL;
 	membd = NULL;
 
-	if (! IS_TPEXPR(tree))
+	if (! (tree->type & MSPH_TREE_TPEXPR))
 		return (0);
 
 	switch (TREE_ID(tree)) {
 	case MSPH_TREE_CONJ:
 		conj = (struct msph_tree_conj *)tree;
 		if ((TP(conj) = spho_tp_create_conj(sc, TP(conj->ltp),
-			    TP(conj->rtp))) == NULL) {
+		    TP(conj->rtp))) == NULL)
 			goto cleanup;
-		}
 		ADD_FLAG(conj, MSPH_TREE_FLAG_TP);
 		break;
 	case MSPH_TREE_DISJ:
 		disj = (struct msph_tree_disj *)tree;
 		if ((TP(disj) = spho_tp_create_conj(sc, TP(disj->ltp),
-			    TP(disj->rtp))) == NULL) {
+		    TP(disj->rtp))) == NULL)
 			goto cleanup;
-		}
 		ADD_FLAG(disj, MSPH_TREE_FLAG_TP);
 		break;
 	case MSPH_TREE_IMPL:
 		impl = (struct msph_tree_impl *)tree;
 		if ((TP(impl) = spho_tp_create_conj(sc, TP(impl->ltp),
-			    TP(impl->rtp))) == NULL) {
+		    TP(impl->rtp))) == NULL)
 			goto cleanup;
-		}
 		ADD_FLAG(impl, MSPH_TREE_FLAG_TP);
 		break;
-	case MSPH_TREE_SUBT:
-		/* a <: b == box(a => b) */
-		subt = (struct msph_tree_subt *)tree;
-		if ((tp = spho_tp_create_impl(sc, TP(subt->ltp),
-			    TP(subt->rtp))) == NULL) {
-			goto cleanup;
-		}
-		if ((TP(subt) = spho_tp_create_box(sc, tp)) == NULL)
-			goto cleanup;
-		ADD_FLAG(subt, MSPH_TREE_FLAG_TP);
-		break;
 	case MSPH_TREE_ARROW:
 		arrow = (struct msph_tree_arrow *)tree;
 		if ((TP(arrow) = spho_tp_create_conj(sc, TP(arrow->ltp),
-		    TP(arrow->rtp))) == NULL) {
+		    TP(arrow->rtp))) == NULL)
 			goto cleanup;
-		}
 		ADD_FLAG(arrow, MSPH_TREE_FLAG_TP);
 		break;
 	case MSPH_TREE_TPNAME:
 		tpname = (struct msph_tree_tpname *)tree;
 		if ((TP(tpname) = spho_tp_create_name(sc, NOM(tpname->name)))
-		    == NULL) {
+		    == NULL)
 			goto cleanup;
-		}
 		ADD_FLAG(tpname, MSPH_TREE_FLAG_TP);
 		break;
 	case MSPH_TREE_TPAPPL:
@@ -406,7 +383,7 @@ msph_tree_sphophi_decor_tp(struct spho_scope *sc, struct msph_tree *tree)
 		ADD_FLAG(trait, MSPH_TREE_FLAG_TP);
 		break;
 	default:
-		SPHO_RIP("impossible-default-reached");
+		SPHO_ASSERT(0);
 		break;
 	}
 
@@ -420,7 +397,7 @@ cleanup:
 }
 
 static int
-msph_tree_sphophi_prebind(struct spho_scope *sc,
+msph_tree_sphophi_tp_prebind(struct spho_scope *sc,
     struct msph_tree *tree)
 {
 	int ret;
@@ -456,8 +433,8 @@ msph_tree_sphophi_prebind(struct spho_scope *sc,
 				return (-1);
 			}
 
-			if ((ret = spho_scope_prebind_tp_op(sc,
-				    NOM(tpdef->name), op)) == -1) {
+			if ((ret = spho_scope_prebind_tp_op(sc, NOM(name), op))
+			    == -1) {
 				return (-1);
 			}
 		} else {
@@ -467,8 +444,6 @@ msph_tree_sphophi_prebind(struct spho_scope *sc,
 			}
 		}
 		break;
-	case MSPH_TREE_NOMINDECL:
-		break;
 	default:
 		break;
 	}
@@ -653,7 +628,9 @@ msph_sphophi_foreach_pre_assert(msph_tree_sphophi_f f, struct spho_scope *sc,
 	if ((ret = f(sc, TREE(ass))) != 0)
 		return (ret);
 
-	if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, ass->tp)) != 0)
+	if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, ass->ltp)) != 0)
+		return (ret);
+	if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, ass->rtp)) != 0)
 		return (ret);
 
 	return (ret);
@@ -703,10 +680,6 @@ msph_sphophi_foreach_pre_tpexpr(msph_tree_sphophi_f f, struct spho_scope *sc,
 		ret = msph_sphophi_foreach_pre_impl(f, sc,
 		    (struct msph_tree_impl *)tpexpr);
 		break;
-	case MSPH_TREE_SUBT:
-		ret = msph_sphophi_foreach_pre_subt(f, sc,
-		    (struct msph_tree_subt *)tpexpr);
-		break;
 	case MSPH_TREE_ARROW:
 		ret = msph_sphophi_foreach_pre_arrow(f, sc,
 		    (struct msph_tree_arrow *)tpexpr);
@@ -744,7 +717,7 @@ msph_sphophi_foreach_pre_tpexpr(msph_tree_sphophi_f f, struct spho_scope *sc,
 		    (struct msph_tree_false *)tpexpr);
 		break;
 	default:
-		SPHO_RIP("impossible-default-reached");
+		SPHO_RIP("default-reach");
 		break;
 	}
 
@@ -802,23 +775,6 @@ msph_sphophi_foreach_pre_impl(msph_tree_sphophi_f f, struct spho_scope *sc,
 	return (msph_sphophi_foreach_pre_tpexpr(f, sc, impl->rtp));
 }
 
-static int
-msph_sphophi_foreach_pre_subt(msph_tree_sphophi_f f, struct spho_scope *sc,
-    struct msph_tree_subt *subt)
-{
-	int ret;
-
-	SPHO_PRECOND(sc != NULL);
-	SPHO_PRECOND(subt != NULL);
-
-	if ((ret = f(sc, TREE(subt))) != 0)
-		return (ret);
-
-	if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, subt->ltp)) != 0)
-		return (ret);
-	return (msph_sphophi_foreach_pre_tpexpr(f, sc, subt->rtp));
-}
-
 static int
 msph_sphophi_foreach_pre_arrow(msph_tree_sphophi_f f, struct spho_scope *sc,
     struct msph_tree_arrow *arrow)
@@ -1136,7 +1092,9 @@ msph_sphophi_foreach_post_assert(msph_tree_sphophi_f f, struct spho_scope *sc,
 	SPHO_PRECOND(sc != NULL);
 	SPHO_PRECOND(ass != NULL);
 
-	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, ass->tp)) != 0)
+	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, ass->ltp)) != 0)
+		return (ret);
+	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, ass->rtp)) != 0)
 		return (ret);
 
 	return (f(sc, TREE(ass)));
@@ -1186,10 +1144,6 @@ msph_sphophi_foreach_post_tpexpr(msph_tree_sphophi_f f, struct spho_scope *sc,
 		ret = msph_sphophi_foreach_post_impl(f, sc,
 		    (struct msph_tree_impl *)tpexpr);
 		break;
-	case MSPH_TREE_SUBT:
-		ret = msph_sphophi_foreach_post_subt(f, sc,
-		    (struct msph_tree_subt *)tpexpr);
-		break;
 	case MSPH_TREE_ARROW:
 		ret = msph_sphophi_foreach_post_arrow(f, sc,
 		    (struct msph_tree_arrow *)tpexpr);
@@ -1286,22 +1240,6 @@ msph_sphophi_foreach_post_impl(msph_tree_sphophi_f f, struct spho_scope *sc,
 	return (f(sc, TREE(impl)));
 }
 
-static int
-msph_sphophi_foreach_post_subt(msph_tree_sphophi_f f, struct spho_scope *sc,
-    struct msph_tree_subt *subt)
-{
-	int ret;
-
-	SPHO_PRECOND(sc != NULL);
-	SPHO_PRECOND(subt != NULL);
-
-	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, subt->ltp)) != 0)
-		return (ret);
-	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, subt->rtp)) != 0)
-		return (ret);
-
-	return (f(sc, TREE(subt)));
-}
 static int
 msph_sphophi_foreach_post_arrow(msph_tree_sphophi_f f, struct spho_scope *sc,
     struct msph_tree_arrow *arrow)
diff --git a/src/msph/token.c b/src/msph/token.c
index 81f61c7..e83a11d 100644
--- a/src/msph/token.c
+++ b/src/msph/token.c
@@ -7,7 +7,7 @@
 
 #include "spho/spho.h"
 
-#include "msph/msph.h"
+#include "msph/err.h"
 #include "msph/token.h"
 
 
@@ -48,7 +48,7 @@ struct msph_matcher token_matchers[] = {
 	{ 0, 0, TOK_CONST_FALSE },
 
 	{ 0, 0, TOK_IDENT },
-	{ 0, 0, TOK_NOPE }
+	{ 0, 0, TOK_END }
 };
 struct msph_matcher wspace = { 0, 0, TOK_WSPACE };
 
@@ -86,7 +86,7 @@ struct msph_token_info {
 	TOK_INFO(TOK_CONST_FALSE, "False"),
 
 	TOK_INFO(TOK_IDENT, NULL),
-	{ TOK_NOPE , NULL, NULL }
+	{ TOK_END , NULL, NULL }
 #undef TOK_INFO
 };
 
@@ -305,7 +305,7 @@ read_single_tok(struct msph_token *ptr, struct msph_token_stream *s)
 		return (-1);
 
 	max_m = 0;
-	for (m = 1; token_matchers[m].type != TOK_NOPE; m++) {
+	for (m = 1; token_matchers[m].type != TOK_END; m++) {
 		res = tok_match(ctx, src, &token_matchers[m]);
 
 		if (res == -1)
@@ -358,7 +358,7 @@ msph_token_copy(struct msph_ctx *ctx, struct msph_token *token)
 
 	info = NULL;
 
-	for (i = 0; token_info[i].type != TOK_NOPE; i++) {
+	for (i = 0; token_info[i].type != TOK_END; i++) {
 		if (token_info[i].type == token->type) {
 			info = &token_info[i];
 			break;
@@ -769,7 +769,7 @@ static const char *
 tok_base_str(struct msph_token *tok)
 {
 	size_t i;
-	for (i = 0; token_info[i].type != TOK_NOPE; i++) {
+	for (i = 0; token_info[i].type != TOK_END; i++) {
 		if (token_info[i].type == tok->type)
 			return (token_info[i].dbg_str);
 	}
diff --git a/src/msph/tree.c b/src/msph/tree.c
index 2444da6..199628c 100644
--- a/src/msph/tree.c
+++ b/src/msph/tree.c
@@ -1,6 +1,5 @@
 #define SPHO_ENABLE_DEBUG_PRINT
 
-
 #include <sys/queue.h>
 
 #include <stdlib.h>
@@ -9,15 +8,13 @@
 
 #include "spho/spho.h"
 
-#include "msph/msph.h"
 #include "msph/tree.h"
 
 
 struct tree_parse {
 	struct msph_token_stream	*s;
-	struct msph_token		curr;
 
-	int	parser;
+	struct msph_token		curr;
 
 	SLIST_HEAD(msph_token_l, msph_token)	head;
 };
@@ -27,10 +24,12 @@ struct tree_parse {
 #define CTX(parse)		((parse)->s->ctx)
 
 static void	tree_parse_init(struct tree_parse *,
-		    struct msph_token_stream *, int);
+		    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 int	tree_ind_fprint(FILE *, int, struct msph_tree *);
+static ssize_t	tree_ind_fprint(FILE *, int, struct msph_tree *);
 
 static void	free_the_tree(struct msph_tree *);
 
@@ -60,37 +59,6 @@ static struct msph_tree_dir *tree_parse_membdecl(
 
 static struct msph_tree_tpexpr	*tree_parse_tpexpr(struct tree_parse *,
 				    struct msph_tree *);
-
-/* prefix &, |, =>, -> */
-static struct msph_tree_tpexpr	*tree_parse_tpexpr_prefix(struct tree_parse *,
-				    struct msph_tree *);
-static struct msph_tree_tpexpr	*tree_parse_conj_prefix(struct tree_parse *,
-				    struct msph_tree *);
-static struct msph_tree_tpexpr	*tree_parse_disj_prefix(struct tree_parse *,
-				    struct msph_tree *);
-static struct msph_tree_tpexpr	*tree_parse_impl_prefix(struct tree_parse *,
-				    struct msph_tree *);
-static struct msph_tree_tpexpr	*tree_parse_arrow_prefix(struct tree_parse *,
-				    struct msph_tree *);
-static struct msph_tree_tpexpr	*tree_parse_subt_prefix(struct tree_parse *,
-				    struct msph_tree *);
-
-/* infix &, |, =>, -> */
-static struct msph_tree_tpexpr	*tree_parse_tpexpr_infix(struct tree_parse *,
-				    struct msph_tree *);
-static struct msph_tree_tpexpr	*tree_parse_conj_infix(struct tree_parse *,
-				    struct msph_tree *);
-static struct msph_tree_tpexpr	*tree_parse_disj_infix(struct tree_parse *,
-				    struct msph_tree *);
-static struct msph_tree_tpexpr	*tree_parse_impl_infix(struct tree_parse *,
-				    struct msph_tree *);
-static struct msph_tree_tpexpr	*tree_parse_arrow_infix(struct tree_parse *,
-				    struct msph_tree *);
-static struct msph_tree_tpexpr	*tree_parse_subt_infix(struct tree_parse *,
-				    struct msph_tree *);
-
-static struct msph_tree_tpexpr	*tree_parse_tpexpr_atom(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 *,
@@ -103,6 +71,14 @@ static struct msph_tree_tpexpr	*tree_parse_tpapplargs(struct tree_parse *,
 				    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 *,
@@ -115,13 +91,12 @@ msph_tree_makeroot(struct msph_ctx *ctx)
 {
 	struct msph_tree_root	*root;
 
-	if ((root = calloc(1, sizeof(*root))) == NULL) {
+	if ((root = malloc(sizeof(*root))) == NULL) {
 		MSPH_ERR(ctx, MSPH_ERR_SYS);
 		return (NULL);
 	}
 	TREE(root)->type = MSPH_TREE_ROOT;
 	TREE(root)->parent = NULL;
-	DECOR_INIT(root);
 
 	root->ctx = ctx;
 
@@ -130,8 +105,6 @@ msph_tree_makeroot(struct msph_ctx *ctx)
 	return (root);
 }
 
-#define __POS_FMT		"line: %u, col: %u"
-#define __POS_ARGS(pos)		(pos).line, (pos).col
 
 /*
  * Expect to read next token, otherwise set error and do something
@@ -145,8 +118,6 @@ msph_tree_makeroot(struct msph_ctx *ctx)
 		if (((readres) = tree_parse_next_token(parse)) == -1) \
 			on_err; \
 		if ((readres) == 0) { \
-			fprintf(stderr, "unexpected end-of-file after " \
-			    __POS_FMT "\n", __POS_ARGS((parse)->s->src.pos)); \
 			MSPH_ERR_INFO(CTX(parse), MSPH_ERR_TREE_EOF, \
 			    err_info); \
 			on_err; \
@@ -163,8 +134,6 @@ msph_tree_makeroot(struct msph_ctx *ctx)
 #define EXPECT_CURR_TOKEN(parse, toktype, err_info, on_err) \
 	do { \
 		if (CURR_TOKEN(parse)->type != toktype) { \
-			fprintf(stderr, "parser expected token " #toktype \
-			    "\n"); \
 			MSPH_ERR_INFO(CTX(parse), MSPH_ERR_TREE_NOMATCH, \
 			    err_info); \
 			on_err; \
@@ -172,8 +141,7 @@ msph_tree_makeroot(struct msph_ctx *ctx)
 	} while (0)
 
 int
-msph_tree_parse(struct msph_token_stream *s, struct msph_tree_root *root,
-    int parser)
+msph_tree_parse(struct msph_token_stream *s, struct msph_tree_root *root)
 {
 	struct tree_parse p;
 	struct msph_tree_unit *unit;
@@ -183,15 +151,7 @@ msph_tree_parse(struct msph_token_stream *s, struct msph_tree_root *root,
 		return (-1);
 	}
 
-	switch (parser) {
-	case MSPH_PARSE_INFIX:
-	case MSPH_PARSE_PREFIX:
-		tree_parse_init(&p, s, parser);
-		break;
-	default:
-		MSPH_ERR(s->ctx, MSPH_ERR_INVAL);
-		return (-1);
-	}
+	tree_parse_init(&p, s);
 
 	if ((unit = tree_parse_unit(&p, TREE(root))) == NULL)
 		return (-1);
@@ -206,25 +166,383 @@ msph_tree_fprint(FILE *f, struct msph_tree *tree) {
 	return (tree_ind_fprint(f, 0, tree));
 }
 
+#define MSPH_TREE_INDENT	"    "
+
+__attribute__((format(printf, 3, 4)))
+static ssize_t
+indent_fprintf(FILE *f, int indent, const char *fmt, ...)
+{
+	int res;
+	ssize_t ret;
+	int i;
+	va_list ap;
+
+	ret = 0;
+	va_start(ap, fmt);
+
+	for (i = 0; i < indent; i++) {
+		res = fprintf(f, "%s", MSPH_TREE_INDENT);
+		if (res < 0) {
+			return ((ssize_t)res);
+		}
+		ret += (ssize_t)res;
+	}
+
+	res = vfprintf(f, fmt, ap);
+	if (res < 0) {
+		return ((ssize_t)res);
+	}
+	ret += (ssize_t)res;
+	va_end(ap);
+
+	return (ret);
+}
+
+static ssize_t
+tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree)
+{
+	ssize_t ret, res;
+	struct msph_tree_root *root;
+	struct msph_tree_unit *unit;
+	struct msph_tree_body *body;
+	struct msph_tree_dir *dir;
+	struct msph_tree_nomindecl *nomd;
+	struct msph_tree_assert *ass;
+	struct msph_tree_tpdef *tpdef;
+	struct msph_tree_membdecl *membdecl;
+	struct msph_tree_conj *conj;
+	struct msph_tree_disj *disj;
+	struct msph_tree_impl *impl;
+	struct msph_tree_arrow *arrow;
+	struct msph_tree_box *box;
+	struct msph_tree_forall *forall;
+	struct msph_tree_tpappl *tpappl;
+	struct msph_tree_trait *trait;
+	struct msph_tree_tpname *name;
+	struct msph_tree_paren *paren;
+	struct msph_tree_ident *ident;
+	struct msph_tree_tpexpr *tp;
+
+	ret = 0;
+	switch (TREE_ID(tree)) {
+	case MSPH_TREE_ROOT:
+		root = (struct msph_tree_root *)tree;
+		if ((res = indent_fprintf(f, indent, "(root\n")) < 0)
+			return (res);
+		STAILQ_FOREACH(unit, &root->head, entries) {
+			if ((res = tree_ind_fprint(f, indent+1, TREE(unit)))
+			    < 0)
+				return (res);
+			ret += res;
+		}
+		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
+			return (res);
+		break;
+	case MSPH_TREE_UNIT:
+		unit = (struct msph_tree_unit *)tree;
+		if ((res = indent_fprintf(f, indent, "(unit:%s\n", unit->name))
+		    < 0)
+			return (res);
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(unit->body))) < 0)
+			return (res);
+		ret += res;
+		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
+			return (res);
+		ret += res;
+		break;
+	case MSPH_TREE_BODY:
+		body = (struct msph_tree_body *)tree;
+		if ((res = indent_fprintf(f, indent, "(body\n")) < 0)
+			return (res);
+		ret += res;
+		STAILQ_FOREACH(dir, &body->head, entries) {
+			if ((res = tree_ind_fprint(f, indent+1, TREE(dir)))
+			    < 0)
+				return (res);
+			ret += res;
+		}
+		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
+			return (res);
+		ret += res;
+		break;
+	case MSPH_TREE_NOMINDECL:
+		nomd = (struct msph_tree_nomindecl *)tree;
+		if ((res = indent_fprintf(f, indent, "(nomindecl:%u,%u\n",
+		    TEXT(nomd)->pos.line, TEXT(nomd)->pos.col)) < 0)
+			return (res);
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(nomd->name))) < 0)
+			return (res);
+		ret += res;
+		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
+			return (res);
+		ret += res;
+		break;
+	case MSPH_TREE_ASSERT:
+		ass = (struct msph_tree_assert *)tree;
+		if ((res = indent_fprintf(f, indent, "(assert:%u,%u\n",
+		    TEXT(ass)->pos.line, TEXT(ass)->pos.col)) < 0)
+			return (res);
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(ass->ltp))) < 0)
+			return (res);
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(ass->rtp))) < 0)
+			return (res);
+		ret += res;
+		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
+			return (res);
+		ret += res;
+		break;
+	case MSPH_TREE_TPDEF:
+		tpdef = (struct msph_tree_tpdef *)tree;
+		if ((res = indent_fprintf(f, indent, "(tpdef:%u,%u\n",
+		    TEXT(tpdef)->pos.line, TEXT(tpdef)->pos.col)) < 0)
+			return (res);
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(tpdef->name))) < 0)
+			return (res);
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(tpdef->tp))) < 0)
+			return (res);
+		ret += res;
+		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
+			return (res);
+		ret += res;
+		break;
+	case MSPH_TREE_MEMBDECL:
+		membdecl = (struct msph_tree_membdecl *)tree;
+		if ((res = indent_fprintf(f, indent, "(membdecl:%u,%u\n",
+		    TEXT(membdecl)->pos.line, TEXT(membdecl)->pos.col)) < 0) {
+			return (res);
+		}
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(membdecl->name)))
+		    < 0) {
+			return (res);
+		}
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(membdecl->tp)))
+		    < 0) {
+			return (res);
+		}
+		ret += res;
+		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
+			return (res);
+		ret += res;
+		break;
+	case MSPH_TREE_CONJ:
+		conj = (struct msph_tree_conj *)tree;
+		if ((res = indent_fprintf(f, indent, "(conj:%u,%u\n",
+		    TEXT(conj)->pos.line, TEXT(conj)->pos.col)) < 0)
+			return (res);
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(conj->ltp))) < 0)
+			return (res);
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(conj->rtp))) < 0)
+			return (res);
+		ret += res;
+		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
+			return (res);
+		ret += res;
+		break;
+	case MSPH_TREE_DISJ:
+		disj = (struct msph_tree_disj *)tree;
+		if ((res = indent_fprintf(f, indent, "(disj:%u,%u\n",
+		    TEXT(disj)->pos.line, TEXT(disj)->pos.col)) < 0)
+			return (res);
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(disj->ltp))) < 0)
+			return (res);
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(disj->rtp))) < 0)
+			return (res);
+		ret += res;
+		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
+			return (res);
+		ret += res;
+		break;
+	case MSPH_TREE_IMPL:
+		impl = (struct msph_tree_impl *)tree;
+		if ((res = indent_fprintf(f, indent, "(impl:%u,%u\n",
+		    TEXT(impl)->pos.line, TEXT(impl)->pos.col)) < 0)
+			return (res);
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(impl->ltp))) < 0)
+			return (res);
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(impl->rtp))) < 0)
+			return (res);
+		ret += res;
+		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
+			return (res);
+		ret += res;
+		break;
+	case MSPH_TREE_ARROW:
+		arrow = (struct msph_tree_arrow *)tree;
+		if ((res = indent_fprintf(f, indent, "(arrow:%u,%u\n",
+		    TEXT(arrow)->pos.line, TEXT(arrow)->pos.col)) < 0)
+			return (res);
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(arrow->ltp))) < 0)
+			return (res);
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(arrow->rtp))) < 0)
+			return (res);
+		ret += res;
+		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
+			return (res);
+		ret += res;
+		break;
+	case MSPH_TREE_BOX:
+		box = (struct msph_tree_box *)tree;
+		if ((res = indent_fprintf(f, indent, "(box:%u,%u\n",
+		    TEXT(box)->pos.line, TEXT(box)->pos.col)) < 0)
+			return (res);
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(box->inner))) < 0)
+			return (res);
+		ret += res;
+		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
+			return (res);
+		ret += res;
+		break;
+	case MSPH_TREE_FORALL:
+		forall = (struct msph_tree_forall *)tree;
+		if ((res = indent_fprintf(f, indent, "(forall:%u,%u\n",
+		    TEXT(forall)->pos.line, TEXT(forall)->pos.col)) < 0)
+			return (res);
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(forall->name)))
+		    < 0)
+			return (res);
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(forall->inner)))
+		    < 0) {
+			return (res);
+		}
+		ret += res;
+		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
+			return (res);
+		ret += res;
+		break;
+	case MSPH_TREE_PAREN:
+		paren = (struct msph_tree_paren *)tree;
+		if ((res = indent_fprintf(f, indent, "(paren:%u,%u\n",
+		    TEXT(paren)->pos.line, TEXT(paren)->pos.col)) < 0)
+			return (res);
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(paren->inner)))
+		    < 0) {
+			return (res);
+		}
+		ret += res;
+		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
+			return (res);
+		ret += res;
+		break;
+	case MSPH_TREE_TPAPPL:
+		tpappl = (struct msph_tree_tpappl *)tree;
+		if ((res = indent_fprintf(f, indent, "(tpappl:%u,%u\n",
+		    TEXT(tpappl)->pos.line, TEXT(tpappl)->pos.col)) < 0)
+			return (res);
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(tpappl->name))) < 0)
+			return (res);
+		ret += res;
+		STAILQ_FOREACH(tp, &tpappl->args, entries) {
+			if ((res = tree_ind_fprint(f, indent+1, TREE(tp))) < 0)
+				return (res);
+			ret += res;
+		}
+		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
+			return (res);
+		ret += res;
+		break;
+	case MSPH_TREE_TPNAME:
+		name = (struct msph_tree_tpname *)tree;
+		if ((res = indent_fprintf(f, indent, "(name:%u,%u\n",
+		    TEXT(name)->pos.line, TEXT(name)->pos.col)) < 0)
+			return (res);
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(name->name))) < 0)
+			return (res);
+		ret += res;
+		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
+			return (res);
+		ret += res;
+		break;
+	case MSPH_TREE_TRAIT:
+		trait = (struct msph_tree_trait *)tree;
+		if ((res = indent_fprintf(f, indent, "(trait:%u,%u\n",
+		    TEXT(trait)->pos.line, TEXT(trait)->pos.col)) < 0)
+			return (res);
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, TREE(trait->body)))
+		    < 0) {
+			return (res);
+		}
+		ret += res;
+		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
+			return (res);
+		ret += res;
+		break;
+	case MSPH_TREE_NAMEDECL:
+	case MSPH_TREE_NAMEREF:
+	case MSPH_TREE_IDENT:
+		ident = IDENT(tree);
+		if ((res = indent_fprintf(f, indent, "(ident:%u,%u:%s)\n",
+		    TEXT(ident)->pos.line, TEXT(ident)->pos.col, ident->str))
+		    < 0)
+			return (res);
+		ret += res;
+		break;
+	case MSPH_TREE_TRUE:
+		if ((res = indent_fprintf(f, indent, "(true:%u,%u)\n",
+		    TEXT(tree)->pos.line, TEXT(tree)->pos.col)) < 0)
+			return (res);
+		ret += res;
+		break;
+	case MSPH_TREE_FALSE:
+		if ((res = indent_fprintf(f, indent, "(false:%u,%u)\n",
+		    TEXT(tree)->pos.line, TEXT(tree)->pos.col)) < 0)
+			return (res);
+		ret += res;
+		break;
+	default:
+		SPHO_ASSERT(0);
+		break;
+	}
+
+	return (ret);
+}
 
 static void
-tree_parse_init(struct tree_parse *p, struct msph_token_stream *s, int parser)
+tree_parse_init(struct tree_parse *p, struct msph_token_stream *s)
 {
 	p->s = s;
+
 	memset(&p->curr, 0, sizeof(p->curr));
-	p->curr.type = TOK_NOPE;
-	p->parser = parser;
+
+	SLIST_INIT(&p->head);
 }
 
 static int
 tree_parse_next_token(struct tree_parse *p)
 {
 	int ret;
-
-	SPHO_PRECOND(p->curr.type > TOK_EOF);
-
-	ret = (int)msph_token_stream_read(&p->curr, 1, p->s);
-
+	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];
@@ -233,12 +551,6 @@ tree_parse_next_token(struct tree_parse *p)
 		    buf);
 	}
 #endif
-
-	if (ret <= 0)
-		memset(&p->curr, 0, sizeof(p->curr));
-	if (ret < 0)
-		p->curr.type = TOK_INVAL;
-
 	return (ret);
 }
 
@@ -248,7 +560,7 @@ tree_parse_unit(struct tree_parse *p, struct msph_tree *parent)
 	size_t namelen;
 	struct msph_tree_unit *unit;
 
-	if ((unit = calloc(1, sizeof(*unit))) == NULL) {
+	if ((unit = malloc(sizeof(*unit))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -263,8 +575,6 @@ tree_parse_unit(struct tree_parse *p, struct msph_tree *parent)
 		goto err;
 	}
 
-	tree_parse_next_token(p);
-
 	if ((unit->body = tree_parse_body(p, TREE(unit))) == NULL)
 		goto err;
 
@@ -279,23 +589,24 @@ err:
 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 = calloc(1, sizeof(*body))) == NULL) {
+	if ((body = malloc(sizeof(*body))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
 	TREE(body)->type = MSPH_TREE_BODY;
 	TREE(body)->parent = parent;
 	STAILQ_INIT(&body->head);
-	DECOR_INIT(body);
 
-	while (1) {
+	while ((res = tree_parse_next_token(p)) > 0) {
 		dir = NULL;
-
 		switch(CURR_TOKEN(p)->type) {
 		case TOK_KW_TYPE:
+			SPHO_DEBUG_PRINT("parsing tpdef\n");
 			dir = tree_parse_tpdef(p, TREE(body));
 			break;
 		case TOK_KW_NOMINAL:
@@ -308,6 +619,10 @@ tree_parse_body(struct tree_parse *p, struct msph_tree *parent)
 			dir = tree_parse_assert(p, TREE(body));
 			break;
 		default:
+			if ((tok = msph_token_copy(CTX(p), CURR_TOKEN(p)))
+			    == NULL)
+				goto err;
+			tree_parse_push_token(p, tok);
 			goto ret;
 		}
 
@@ -317,6 +632,8 @@ tree_parse_body(struct tree_parse *p, struct msph_tree *parent)
 		STAILQ_INSERT_TAIL(&body->head, dir, entries);
 	}
 
+	if (res == -1)
+		goto err;
 ret:
 	return (body);
 err:
@@ -325,6 +642,12 @@ err:
 	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 *
@@ -336,7 +659,7 @@ tree_parse_tpdef(struct tree_parse *p, struct msph_tree *parent)
 
 	EXPECT_CURR_TOKEN(p, TOK_KW_TYPE, MSPH_TREE_TPDEF, return (NULL));
 
-	if ((def = calloc(1, sizeof(*def))) == NULL) {
+	if ((def = malloc(sizeof(*def))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -350,17 +673,22 @@ tree_parse_tpdef(struct tree_parse *p, struct msph_tree *parent)
 	if ((def->name = tree_parse_namedecl(p, TREE(def))) == NULL)
 		goto err;
 
+	EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err);
+
 	if (CURR_TOKEN(p)->type == TOK_LBRAK) {
+		ADD_FLAG(TREE(def), MSPH_TREE_FLAG_SCOPE);
+
 		do {
 			EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err);
 			name = tree_parse_namedecl(p, TREE(def));
 			if (name == NULL)
 				goto err;
 			STAILQ_INSERT_TAIL(&def->params, name, entries);
+
+			EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err);
 		} while (CURR_TOKEN(p)->type == TOK_COMMA);
 
 		EXPECT_CURR_TOKEN(p, TOK_RBRAK, MSPH_TREE_TPDEF, goto err);
-		EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err);
 	}
 	EXPECT_CURR_TOKEN(p, TOK_EQUALS, MSPH_TREE_TPDEF, goto err);
 
@@ -387,7 +715,7 @@ tree_parse_namedecl(struct tree_parse *p, struct msph_tree *parent)
 		return (NULL);
 
 	SPHO_ASSERT(TREE(name)->type == MSPH_TREE_IDENT);
-	TREE(name)->type = MSPH_TREE_NAMEDECL;
+	TREE(name)->type |= MSPH_TREE_NAMEDECL;
 
 	return (name);
 }
@@ -405,7 +733,7 @@ tree_parse_nameref(struct tree_parse *p, struct msph_tree *parent)
 		return (NULL);
 
 	SPHO_ASSERT(TREE(name)->type == MSPH_TREE_IDENT);
-	TREE(name)->type = MSPH_TREE_NAMEREF;
+	TREE(name)->type |= MSPH_TREE_NAMEREF;
 
 	return (name);
 }
@@ -419,7 +747,7 @@ tree_parse_ident_extsize(struct tree_parse *p, struct msph_tree *parent,
 
 	EXPECT_CURR_TOKEN(p, TOK_IDENT, MSPH_TREE_IDENT, return (NULL));
 
-	if ((id = calloc(1, size)) == NULL) {
+	if ((id = malloc(sizeof(size))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -428,14 +756,12 @@ tree_parse_ident_extsize(struct tree_parse *p, struct msph_tree *parent,
 	TEXT(id)->pos = CURR_TOKEN(p)->pos;
 	DECOR_INIT(id);
 
-	if (strlcpy(id->str, CURR_TOKEN(p)->data.str, sizeof(id->str))
+	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;
 	}
 
-	tree_parse_next_token(p);
-
 	return (id);
 err:
 	free_the_tree(TREE(id));
@@ -444,39 +770,21 @@ err:
 
 struct msph_tree_tpexpr *
 tree_parse_tpexpr(struct tree_parse *p, struct msph_tree *parent)
-{
-	switch (p->parser) {
-	case MSPH_PARSE_INFIX:
-		return (tree_parse_tpexpr_infix(p, parent));
-	case MSPH_PARSE_PREFIX:
-		return (tree_parse_tpexpr_prefix(p, parent));
-	default:
-		SPHO_RIP("impossible-invalid-parser");
-		return (NULL);
-	}
-
-}
-
-struct msph_tree_tpexpr *
-tree_parse_tpexpr_prefix(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_prefix(p, parent);
+		tp = tree_parse_conj(p, parent);
 		break;
 	case TOK_PIPE:
-		tp = tree_parse_disj_prefix(p, parent);
+		tp = tree_parse_disj(p, parent);
 		break;
 	case TOK_IMPL:
-		tp = tree_parse_impl_prefix(p, parent);
-		break;
-	case TOK_SUB:
-		tp = tree_parse_subt_prefix(p, parent);
+		tp = tree_parse_impl(p, parent);
 		break;
 	case TOK_RARROW:
-		tp = tree_parse_arrow_prefix(p, parent);
+		tp = tree_parse_arrow(p, parent);
 		break;
 	case TOK_KW_BOX:
 		tp = tree_parse_box(p, parent);
@@ -509,14 +817,14 @@ tree_parse_tpexpr_prefix(struct tree_parse *p, struct msph_tree *parent)
 }
 
 struct msph_tree_tpexpr *
-tree_parse_conj_prefix(struct tree_parse *p, struct msph_tree *parent)
+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 = calloc(1, sizeof(*conj))) == NULL) {
+	if ((conj = malloc(sizeof(*conj))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -528,12 +836,12 @@ tree_parse_conj_prefix(struct tree_parse *p, struct msph_tree *parent)
 	conj->rtp = NULL;
 
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_CONJ, goto err);
-	if ((conj->ltp = tree_parse_tpexpr_prefix(p, TREE(conj))) 
+	if ((conj->ltp = tree_parse_tpexpr(p, TREE(conj))) 
 	    == NULL)
 		goto err;
 
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_CONJ, goto err);
-	if ((conj->rtp = tree_parse_tpexpr_prefix(p, TREE(conj)))
+	if ((conj->rtp = tree_parse_tpexpr(p, TREE(conj)))
 	    == NULL)
 		goto err;
 
@@ -545,14 +853,14 @@ err:
 }
 
 struct msph_tree_tpexpr *
-tree_parse_disj_prefix(struct tree_parse *p, struct msph_tree *parent)
+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 = calloc(1, sizeof(*disj))) == NULL) {
+	if ((disj = malloc(sizeof(*disj))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -564,12 +872,12 @@ tree_parse_disj_prefix(struct tree_parse *p, struct msph_tree *parent)
 	disj->rtp = NULL;
 
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_DISJ, goto err);
-	if ((disj->ltp = tree_parse_tpexpr_prefix(p, (struct msph_tree *)disj)) 
+	if ((disj->ltp = tree_parse_tpexpr(p, (struct msph_tree *)disj)) 
 	    == NULL)
 		goto err;
 
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_DISJ, goto err);
-	if ((disj->rtp = tree_parse_tpexpr_prefix(p, (struct msph_tree *)disj))
+	if ((disj->rtp = tree_parse_tpexpr(p, (struct msph_tree *)disj))
 	    == NULL)
 		goto err;
 
@@ -581,14 +889,14 @@ err:
 }
 
 struct msph_tree_tpexpr *
-tree_parse_impl_prefix(struct tree_parse *p, struct msph_tree *parent)
+tree_parse_impl(struct tree_parse *p, struct msph_tree *parent)
 {
 	int res;
 	struct msph_tree_impl *impl;
 
 	EXPECT_CURR_TOKEN(p, TOK_IMPL, MSPH_TREE_IMPL, return (NULL));
 
-	if ((impl = calloc(1, sizeof(*impl))) == NULL) {
+	if ((impl = malloc(sizeof(*impl))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -600,12 +908,12 @@ tree_parse_impl_prefix(struct tree_parse *p, struct msph_tree *parent)
 	impl->rtp = NULL;
 
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_IMPL, goto err);
-	if ((impl->ltp = tree_parse_tpexpr_prefix(p, (struct msph_tree *)impl)) 
+	if ((impl->ltp = tree_parse_tpexpr(p, (struct msph_tree *)impl)) 
 	    == NULL)
 		goto err;
 
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_IMPL, goto err);
-	if ((impl->rtp = tree_parse_tpexpr_prefix(p, (struct msph_tree *)impl))
+	if ((impl->rtp = tree_parse_tpexpr(p, (struct msph_tree *)impl))
 	    == NULL)
 		goto err;
 
@@ -617,50 +925,14 @@ err:
 }
 
 struct msph_tree_tpexpr *
-tree_parse_subt_prefix(struct tree_parse *p, struct msph_tree *parent)
-{
-	int res;
-	struct msph_tree_subt *subt;
-
-	EXPECT_CURR_TOKEN(p, TOK_SUB, MSPH_TREE_SUBT, return (NULL));
-
-	if ((subt = calloc(1, sizeof(*subt))) == NULL) {
-		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
-		return (NULL);
-	}
-	TREE(subt)->type = MSPH_TREE_SUBT;
-	TREE(subt)->parent = parent;
-	TEXT(subt)->pos = CURR_TOKEN(p)->pos;
-	DECOR_INIT(subt);
-	subt->ltp = NULL;
-	subt->rtp = NULL;
-
-	EXPECT_READ_NEXT(res, p, MSPH_TREE_SUBT, goto err);
-	if ((subt->ltp = tree_parse_tpexpr_prefix(p, (struct msph_tree *)subt)) 
-	    == NULL)
-		goto err;
-
-	EXPECT_READ_NEXT(res, p, MSPH_TREE_SUBT, goto err);
-	if ((subt->rtp = tree_parse_tpexpr_prefix(p, (struct msph_tree *)subt))
-	    == NULL)
-		goto err;
-
-	return ((struct msph_tree_tpexpr *)subt);
-err:
-	free_the_tree((struct msph_tree *)subt);
-
-	return (NULL);
-}
-
-struct msph_tree_tpexpr *
-tree_parse_arrow_prefix(struct tree_parse *p, struct msph_tree *parent)
+tree_parse_arrow(struct tree_parse *p, struct msph_tree *parent)
 {
 	int res;
 	struct msph_tree_arrow *arrow;
 
 	EXPECT_CURR_TOKEN(p, TOK_RARROW, MSPH_TREE_ARROW, return (NULL));
 
-	if ((arrow = calloc(1, sizeof(*arrow))) == NULL) {
+	if ((arrow = malloc(sizeof(*arrow))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -672,12 +944,12 @@ tree_parse_arrow_prefix(struct tree_parse *p, struct msph_tree *parent)
 	arrow->rtp = NULL;
 
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_ARROW, goto err);
-	if ((arrow->ltp = tree_parse_tpexpr_prefix(p, (struct msph_tree *)arrow)) 
+	if ((arrow->ltp = tree_parse_tpexpr(p, (struct msph_tree *)arrow)) 
 	    == NULL)
 		goto err;
 
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_ARROW, goto err);
-	if ((arrow->rtp = tree_parse_tpexpr_prefix(p, (struct msph_tree *)arrow))
+	if ((arrow->rtp = tree_parse_tpexpr(p, (struct msph_tree *)arrow))
 	    == NULL)
 		goto err;
 
@@ -688,318 +960,6 @@ err:
 	return (NULL);
 }
 
-static struct msph_tree_tpexpr *
-tree_parse_tpexpr_infix(struct tree_parse *p, struct msph_tree *parent)
-{
-	return (tree_parse_impl_infix(p, parent));
-}
-
-/*
- * infix type algebraics parsing.
- *
- * In reverse order of precedence (later means higher precedence):
- *  [op    _ associativity]
- * - impl  _ right
- * - subt  - right
- * - disj  _ left (both)
- * - conj  _ left (both)
- * - arrow _ right
- *
- * 
- */
-static struct msph_tree_tpexpr *
-tree_parse_impl_infix(struct tree_parse *p, struct msph_tree *parent)
-{
-	int res;
-	struct msph_tree_tpexpr *left, *right;
-	struct msph_tree_impl *impl;
-	struct msph_text_pos infix_pos;
-
-	impl = NULL;
-	left = right = NULL;
-
-	if ((left = tree_parse_subt_infix(p, NULL)) == NULL) {
-		return (NULL);
-	}
-
-	if (CURR_TOKEN(p)->type != TOK_IMPL) {
-		TREE(left)->parent = parent;
-		return (left);
-	}
-	infix_pos = CURR_TOKEN(p)->pos;
-
-	EXPECT_READ_NEXT(res, p, MSPH_TREE_IMPL, goto err);
-
-	if ((right = tree_parse_impl_infix(p, NULL)) == NULL)
-		goto err;
-
-	if ((impl = calloc(1, sizeof(*impl))) ==  NULL) {
-		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
-		goto err;
-	}
-
-	TREE(impl)->type = MSPH_TREE_IMPL;
-	TREE(impl)->parent = parent;
-	TEXT(impl)->pos = infix_pos;
-	DECOR_INIT(impl);
-
-	impl->ltp = left;
-	TREE(left)->parent = TREE(impl);
-
-	impl->rtp = right;
-	TREE(right)->parent = TREE(impl);
-
-	return ((struct msph_tree_tpexpr *)impl);
-err:
-	if (left != NULL)
-		free_the_tree(TREE(left));
-	if (right != NULL)
-		free_the_tree(TREE(right));
-	return (NULL);
-}
-
-static struct msph_tree_tpexpr *
-tree_parse_subt_infix(struct tree_parse *p, struct msph_tree *parent)
-{
-	int res;
-	struct msph_tree_tpexpr *left, *right;
-	struct msph_tree_subt *subt;
-	struct msph_text_pos infix_pos;
-
-	subt = NULL;
-	left = right = NULL;
-
-	if ((left = tree_parse_disj_infix(p, NULL)) == NULL) {
-		return (NULL);
-	}
-
-	if (CURR_TOKEN(p)->type != TOK_SUB) {
-		TREE(left)->parent = parent;
-		return (left);
-	}
-	infix_pos = CURR_TOKEN(p)->pos;
-
-	EXPECT_READ_NEXT(res, p, MSPH_TREE_SUBT, goto err);
-
-	if ((right = tree_parse_subt_infix(p, NULL)) == NULL)
-		goto err;
-
-	if ((subt = calloc(1, sizeof(*subt))) ==  NULL) {
-		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
-		goto err;
-	}
-
-	TREE(subt)->type = MSPH_TREE_SUBT;
-	TREE(subt)->parent = parent;
-	TEXT(subt)->pos = infix_pos;
-	DECOR_INIT(subt);
-
-	subt->ltp = left;
-	TREE(left)->parent = TREE(subt);
-
-	subt->rtp = right;
-	TREE(right)->parent = TREE(subt);
-
-	return ((struct msph_tree_tpexpr *)subt);
-err:
-	if (left != NULL)
-		free_the_tree(TREE(left));
-	if (right != NULL)
-		free_the_tree(TREE(right));
-	return (NULL);
-}
-
-static struct msph_tree_tpexpr *
-tree_parse_disj_infix(struct tree_parse *p, struct msph_tree *parent)
-{
-	int res;
-	struct msph_tree_tpexpr *left, *right;
-	struct msph_tree_disj *disj;
-	struct msph_text_pos infix_pos;
-
-	left = right = NULL;
-	disj = NULL;
-
-	if ((left = tree_parse_conj_infix(p, NULL)) == NULL)
-		return (NULL);
-
-	TREE(left)->parent = parent;
-
-	while (CURR_TOKEN(p)->type == TOK_PIPE) {
-		infix_pos = CURR_TOKEN(p)->pos;
-		EXPECT_READ_NEXT(res, p, MSPH_TREE_DISJ, goto err);
-
-		if ((right = tree_parse_conj_infix(p, NULL)) == NULL)
-			goto err;
-
-		if ((disj = calloc(1, sizeof(*disj))) == NULL) {
-			MSPH_ERR(CTX(p), MSPH_ERR_SYS);
-			goto err;
-		}
-
-		TREE(disj)->type = MSPH_TREE_DISJ;
-		TREE(disj)->parent = parent;
-		TEXT(disj)->pos = infix_pos;
-		DECOR_INIT(disj);
-
-		disj->ltp = left;
-		TREE(left)->parent = TREE(disj);
-		disj->rtp = right;
-		TREE(right)->parent = TREE(disj);
-
-		left = (struct msph_tree_tpexpr *)disj;
-		right = NULL;
-	}
-
-	SPHO_POSTCOND(TREE(left)->parent == parent);
-
-	return (left);
-err:
-	if (right != NULL)
-		free_the_tree(TREE(right));
-
-	free_the_tree(TREE(left));
-	return (NULL);
-}
-
-static struct msph_tree_tpexpr *
-tree_parse_conj_infix(struct tree_parse *p, struct msph_tree *parent)
-{
-	int res;
-	struct msph_tree_tpexpr *left, *right;
-	struct msph_tree_conj *conj;
-	struct msph_text_pos infix_pos;
-
-	left = right = NULL;
-	conj = NULL;
-
-	if ((left = tree_parse_arrow_infix(p, NULL)) == NULL)
-		return (NULL);
-
-	TREE(left)->parent = parent;
-
-	while (CURR_TOKEN(p)->type == TOK_AMP) {
-		infix_pos = CURR_TOKEN(p)->pos;
-		EXPECT_READ_NEXT(res, p, MSPH_TREE_CONJ, goto err);
-
-		if ((right = tree_parse_arrow_infix(p, NULL)) == NULL)
-			goto err;
-
-		if ((conj = calloc(1, sizeof(*conj))) == NULL) {
-			MSPH_ERR(CTX(p), MSPH_ERR_SYS);
-			goto err;
-		}
-
-		TREE(conj)->type = MSPH_TREE_CONJ;
-		TREE(conj)->parent = parent;
-		TEXT(conj)->pos = infix_pos;
-		DECOR_INIT(conj);
-
-		conj->ltp = left;
-		TREE(left)->parent = TREE(conj);
-		conj->rtp = right;
-		TREE(right)->parent = TREE(conj);
-
-		left = (struct msph_tree_tpexpr *)conj;
-		right = NULL;
-	}
-
-	SPHO_POSTCOND(TREE(left)->parent == parent);
-
-	return (left);
-err:
-	if (right != NULL)
-		free_the_tree(TREE(right));
-
-	free_the_tree(TREE(left));
-	return (NULL);
-}
-static struct msph_tree_tpexpr *
-tree_parse_arrow_infix(struct tree_parse *p, struct msph_tree *parent)
-{
-	int res;
-	struct msph_tree_tpexpr *left, *right;
-	struct msph_tree_arrow *arrow;
-	struct msph_text_pos infix_pos;
-
-	arrow = NULL;
-	left = right = NULL;
-
-	if ((left = tree_parse_tpexpr_atom(p, NULL)) == NULL) {
-		return (NULL);
-	}
-
-	if (CURR_TOKEN(p)->type != TOK_RARROW) {
-		TREE(left)->parent = parent;
-		return (left);
-	}
-	infix_pos = CURR_TOKEN(p)->pos;
-
-	EXPECT_READ_NEXT(res, p, MSPH_TREE_ARROW, goto err);
-
-	if ((right = tree_parse_arrow_infix(p, NULL)) == NULL)
-		goto err;
-
-	if ((arrow = calloc(1, sizeof(*arrow))) ==  NULL) {
-		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
-		goto err;
-	}
-
-	TREE(arrow)->type = MSPH_TREE_ARROW;
-	TREE(arrow)->parent = parent;
-	TEXT(arrow)->pos = infix_pos;
-	DECOR_INIT(arrow);
-
-	arrow->ltp = left;
-	TREE(left)->parent = TREE(arrow);
-
-	arrow->rtp = right;
-	TREE(right)->parent = TREE(arrow);
-
-	return ((struct msph_tree_tpexpr *)arrow);
-err:
-	if (left != NULL)
-		free_the_tree(TREE(left));
-	if (right != NULL)
-		free_the_tree(TREE(right));
-	return (NULL);
-}
-
-
-struct msph_tree_tpexpr *
-tree_parse_tpexpr_atom(struct tree_parse *p, struct msph_tree *parent)
-{
-	struct msph_tree_tpexpr *tp;
-
-	switch (CURR_TOKEN(p)->type) {
-	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_tpname_or_tpappl(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_box(struct tree_parse *p, struct msph_tree *parent)
 {
@@ -1008,7 +968,7 @@ tree_parse_box(struct tree_parse *p, struct msph_tree *parent)
 
 	EXPECT_CURR_TOKEN(p, TOK_KW_BOX, MSPH_TREE_BOX, return (NULL));
 
-	if ((box = calloc(1, sizeof(*box))) == NULL) {
+	if ((box = malloc(sizeof(*box))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -1036,7 +996,7 @@ tree_parse_forall(struct tree_parse *p, struct msph_tree *parent)
 
 	EXPECT_CURR_TOKEN(p, TOK_KW_FORALL, MSPH_TREE_FORALL, return (NULL));
 
-	if ((fa = calloc(1, sizeof(*fa))) == NULL) {
+	if ((fa = malloc(sizeof(*fa))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -1068,9 +1028,11 @@ err:
 struct msph_tree_tpexpr *
 tree_parse_tpname_or_tpappl(struct tree_parse *p, struct msph_tree *parent)
 {
+	int res;
 	struct msph_tree_tpname *tpname;
 	struct msph_tree_tpexpr *ret;
 	struct msph_tree_nameref *nameref;
+	struct msph_token *tok;
 
 	ret = NULL;
 	nameref = NULL;
@@ -1078,13 +1040,24 @@ tree_parse_tpname_or_tpappl(struct tree_parse *p, struct msph_tree *parent)
 	if ((nameref = tree_parse_nameref(p, NULL)) == NULL)
 		return (NULL);
 
-	if (CURR_TOKEN(p)->type == TOK_LBRAK) {
-		if ((ret = tree_parse_tpapplargs(p, nameref, parent)) == NULL) 
+	if ((res = tree_parse_next_token(p)) == 1) {
+		if (CURR_TOKEN(p)->type == TOK_LBRAK) {
+			if ((ret = tree_parse_tpapplargs(p, nameref, parent))
+			    == NULL)
+				goto err;
+			return (ret);
+		}
+
+		if ((tok = msph_token_copy(CTX(p), CURR_TOKEN(p)))
+		    == NULL) {
 			goto err;
-		return (ret);
+		}
+		tree_parse_push_token(p, tok);
+	} else if (res == -1) {
+		goto err;
 	}
 
-	if ((tpname = calloc(1, sizeof(*tpname))) == NULL) {
+	if ((tpname = malloc(sizeof(*tpname))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		goto err;
 	}
@@ -1124,7 +1097,7 @@ tree_parse_tpapplargs(struct tree_parse *p, struct msph_tree_nameref *name,
 
 	EXPECT_CURR_TOKEN(p, TOK_LBRAK, MSPH_TREE_TPAPPL, return (NULL));
 
-	if ((tpappl = calloc(1, sizeof(*tpappl))) == NULL) {
+	if ((tpappl = malloc(sizeof(*tpappl))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -1134,30 +1107,41 @@ tree_parse_tpapplargs(struct tree_parse *p, struct msph_tree_nameref *name,
 	tpappl->name = NULL;
 	STAILQ_INIT(&tpappl->args);
 
-	EXPECT_READ_NEXT(res, p, MSPH_TREE_TPAPPL, goto err);
+	/* 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 ((tp = tree_parse_tpexpr(p, TREE(tpappl))) == NULL)
-		goto err;
+		/* if not at start of argument list, check for comma to know if
+		 * we should parse another argument */
+		if (tp != NULL) {
+			EXPECT_CURR_TOKEN(p, TOK_COMMA, MSPH_TREE_TPAPPL,
+			    goto err);
+			EXPECT_READ_NEXT(res, p, MSPH_TREE_TPAPPL, goto err);
+		}
 
-	/* more arguments */
-	while (CURR_TOKEN(p)->type == TOK_COMMA) {
-
-		EXPECT_READ_NEXT(res, p, MSPH_TREE_TPAPPL, goto err);
 		if ((tp = tree_parse_tpexpr(p, TREE(tpappl))) == NULL)
 			goto err;
 
 		STAILQ_INSERT_TAIL(&tpappl->args, tp, entries);
 	}
 
-	EXPECT_CURR_TOKEN(p, TOK_RBRAK, MSPH_TREE_TPAPPL, goto err);
+	/* SYS_ERROR set in tree_parse_next_token */
+	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_TPAPPL);
+		goto err;
+	}
 
 	/* finally, appl takes ownership of id */
 	TREE(name)->parent = TREE(tpappl);
 	tpappl->name = name;
 	TEXT(tpappl)->pos = TEXT(name)->pos;
 
-	tree_parse_next_token(p);
-
 	return ((struct msph_tree_tpexpr *)tpappl);
 err:
 	free_the_tree(TREE(tpappl));
@@ -1172,7 +1156,7 @@ tree_parse_true(struct tree_parse *p, struct msph_tree *parent)
 
 	EXPECT_CURR_TOKEN(p, TOK_CONST_TRUE, MSPH_TREE_TRUE, return (NULL));
 
-	if ((t = calloc(1, sizeof(*t))) == NULL) {
+	if ((t = malloc(sizeof(*t))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -1181,8 +1165,6 @@ tree_parse_true(struct tree_parse *p, struct msph_tree *parent)
 	TEXT(t)->pos = CURR_TOKEN(p)->pos;
 	DECOR_INIT(t);
 
-	tree_parse_next_token(p);
-
 	return ((struct msph_tree_tpexpr *)t);
 }
 
@@ -1193,7 +1175,7 @@ tree_parse_false(struct tree_parse *p, struct msph_tree *parent)
 
 	EXPECT_CURR_TOKEN(p, TOK_CONST_FALSE, MSPH_TREE_FALSE, return (NULL));
 
-	if ((f = calloc(1, sizeof(*f))) == NULL) {
+	if ((f = malloc(sizeof(*f))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -1202,8 +1184,6 @@ tree_parse_false(struct tree_parse *p, struct msph_tree *parent)
 	TEXT(f)->pos = CURR_TOKEN(p)->pos;
 	DECOR_INIT(f);
 
-	tree_parse_next_token(p);
-
 	return ((struct msph_tree_tpexpr *)f);
 }
 
@@ -1215,7 +1195,7 @@ tree_parse_paren(struct tree_parse *p, struct msph_tree *parent)
 
 	EXPECT_CURR_TOKEN(p, TOK_LPAREN, MSPH_TREE_FALSE, return (NULL));
 
-	if ((par = calloc(1, sizeof(*par))) == NULL) {
+	if ((par = malloc(sizeof(*par))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -1230,10 +1210,9 @@ tree_parse_paren(struct tree_parse *p, struct msph_tree *parent)
 	if ((par->inner = tree_parse_tpexpr(p, TREE(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);
 
-	tree_parse_next_token(p);
-
 	return ((struct msph_tree_tpexpr *)par);
 err:
 	free_the_tree(TREE(par));
@@ -1249,7 +1228,7 @@ tree_parse_trait(struct tree_parse *p, struct msph_tree *parent)
 
 	EXPECT_CURR_TOKEN(p, TOK_LBRACE, MSPH_TREE_TRAIT, return (NULL));
 
-	if ((trait = calloc(1, sizeof(*trait))) == NULL) {
+	if ((trait = malloc(sizeof(*trait))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -1259,15 +1238,12 @@ tree_parse_trait(struct tree_parse *p, struct msph_tree *parent)
 	DECOR_INIT(trait);
 	trait->body = NULL;
 
-	EXPECT_READ_NEXT(res, p, MSPH_TREE_TRAIT, goto err);
-
 	if ((trait->body = tree_parse_body(p, TREE(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);
 
-	tree_parse_next_token(p);
-
 	return ((struct msph_tree_tpexpr *)trait);
 err:
 	free_the_tree(TREE(trait));
@@ -1285,14 +1261,13 @@ tree_parse_nomindecl(struct tree_parse *p, struct msph_tree *parent)
 	EXPECT_CURR_TOKEN(p, TOK_KW_NOMINAL, MSPH_TREE_NOMINDECL,
 	    return (NULL));
 
-	if ((nomind = calloc(1, sizeof(*nomind))) == NULL) {
+	if ((nomind = malloc(sizeof(*nomind))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
 	TREE(nomind)->type = MSPH_TREE_NOMINDECL;
 	TREE(nomind)->parent = parent;
 	TEXT(nomind)->pos = CURR_TOKEN(p)->pos;
-	DECOR_INIT(nomind);
 	nomind->name = NULL;
 
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_NOMINDECL, goto err);
@@ -1317,14 +1292,13 @@ tree_parse_membdecl(struct tree_parse *p, struct msph_tree *parent)
 	EXPECT_CURR_TOKEN(p, TOK_KW_MEMBER, MSPH_TREE_MEMBDECL,
 	    return (NULL));
 
-	if ((membd = calloc(1, sizeof(*membd))) == NULL) {
+	if ((membd = malloc(sizeof(*membd))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
 	TREE(membd)->type = MSPH_TREE_MEMBDECL;
 	TREE(membd)->parent = parent;
 	TEXT(membd)->pos = CURR_TOKEN(p)->pos;
-	DECOR_INIT(membd);
 	membd->name = NULL;
 	membd->tp = NULL;
 
@@ -1332,6 +1306,7 @@ tree_parse_membdecl(struct tree_parse *p, struct msph_tree *parent)
 	if ((membd->name = tree_parse_namedecl(p, TREE(membd))) == NULL)
 		goto err;
 
+	EXPECT_READ_NEXT(res, p, MSPH_TREE_MEMBDECL, goto err);
 	EXPECT_CURR_TOKEN(p, TOK_COLON, MSPH_TREE_MEMBDECL,
 	    goto err);
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_MEMBDECL, goto err);
@@ -1352,20 +1327,29 @@ tree_parse_assert(struct tree_parse *p, struct msph_tree *parent)
 	int res;
 	struct msph_tree_assert *ass;
 
-	EXPECT_CURR_TOKEN(p, TOK_KW_ASSERT, MSPH_TREE_ASSERT, return (NULL));
+	EXPECT_CURR_TOKEN(p, TOK_KW_ASSERT, MSPH_TREE_ASSERT,
+	    return (NULL));
 
-	if ((ass = calloc(1, sizeof(*ass))) == NULL) {
+	if ((ass = malloc(sizeof(*ass))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
 	TREE(ass)->type = MSPH_TREE_ASSERT;
 	TREE(ass)->parent = parent;
 	TEXT(ass)->pos = CURR_TOKEN(p)->pos;
-	DECOR_INIT(ass);
-	ass->tp = NULL;
+	ass->ltp = NULL;
+	ass->rtp = NULL;
 
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_ASSERT, goto err);
-	if ((ass->tp = tree_parse_tpexpr(p, TREE(ass))) == NULL)
+	if ((ass->ltp = tree_parse_tpexpr(p, TREE(ass))) == NULL)
+		goto err;
+
+	EXPECT_READ_NEXT(res, p, MSPH_TREE_ASSERT, goto err);
+	EXPECT_CURR_TOKEN(p, TOK_SUB, MSPH_TREE_ASSERT,
+	    goto err);
+	EXPECT_READ_NEXT(res, p, MSPH_TREE_ASSERT, goto err);
+
+	if ((ass->rtp = tree_parse_tpexpr(p, TREE(ass))) == NULL)
 		goto err;
 
 	return ((struct msph_tree_dir *)ass);
@@ -1383,411 +1367,3 @@ free_the_tree(struct msph_tree *tree)
 	// SPHO_POSTCOND(0);
 }
 
-#define MSPH_TREE_INDENT	"    "
-
-__attribute__((format(printf, 3, 4)))
-static int
-indent_fprintf(FILE *f, int indent, const char *fmt, ...)
-{
-	int res, ret;
-	int i;
-	va_list ap;
-
-	ret = 0;
-	va_start(ap, fmt);
-
-	for (i = 0; i < indent; i++) {
-		res = fprintf(f, "%s", MSPH_TREE_INDENT);
-		if (res < 0) {
-			return (res);
-		}
-		ret += res;
-	}
-
-	res = vfprintf(f, fmt, ap);
-	if (res < 0) {
-		return (res);
-	}
-	ret += res;
-	va_end(ap);
-
-	return (ret);
-}
-
-static int
-tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree)
-{
-	int ret, res;
-	struct msph_tree_root *root;
-	struct msph_tree_unit *unit;
-	struct msph_tree_body *body;
-	struct msph_tree_dir *dir;
-	struct msph_tree_nomindecl *nomd;
-	struct msph_tree_assert *ass;
-	struct msph_tree_tpdef *tpdef;
-	struct msph_tree_membdecl *membdecl;
-	struct msph_tree_conj *conj;
-	struct msph_tree_disj *disj;
-	struct msph_tree_impl *impl;
-	struct msph_tree_subt *subt;
-	struct msph_tree_arrow *arrow;
-	struct msph_tree_box *box;
-	struct msph_tree_forall *forall;
-	struct msph_tree_tpappl *tpappl;
-	struct msph_tree_trait *trait;
-	struct msph_tree_tpname *name;
-	struct msph_tree_paren *paren;
-	struct msph_tree_ident *ident;
-	struct msph_tree_tpexpr *tp;
-	struct msph_tree_namedecl *named;
-	const char *ident_kind;
-
-	ret = 0;
-	switch (TREE_ID(tree)) {
-	case MSPH_TREE_ROOT:
-		root = (struct msph_tree_root *)tree;
-		if ((res = indent_fprintf(f, indent, "(root\n")) < 0)
-			return (res);
-		STAILQ_FOREACH(unit, &root->head, entries) {
-			if ((res = tree_ind_fprint(f, indent+1, TREE(unit)))
-			    < 0) {
-				return (res);
-			}
-			ret += res;
-		}
-		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
-			return (res);
-		break;
-	case MSPH_TREE_UNIT:
-		unit = (struct msph_tree_unit *)tree;
-		if ((res = indent_fprintf(f, indent, "(unit:%s\n", unit->name))
-		    < 0) {
-			return (res);
-		}
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(unit->body))) < 0)
-			return (res);
-		ret += res;
-		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
-			return (res);
-		ret += res;
-		break;
-	case MSPH_TREE_BODY:
-		body = (struct msph_tree_body *)tree;
-		if ((res = indent_fprintf(f, indent, "(body\n")) < 0)
-			return (res);
-		ret += res;
-		STAILQ_FOREACH(dir, &body->head, entries) {
-			if ((res = tree_ind_fprint(f, indent+1, TREE(dir)))
-			    < 0) {
-				return (res);
-			}
-			ret += res;
-		}
-		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
-			return (res);
-		ret += res;
-		break;
-	case MSPH_TREE_NOMINDECL:
-		nomd = (struct msph_tree_nomindecl *)tree;
-		if ((res = indent_fprintf(f, indent, "(nomindecl:%u,%u\n",
-		    TEXT(nomd)->pos.line, TEXT(nomd)->pos.col)) < 0) {
-			return (res);
-		}
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(nomd->name))) < 0)
-			return (res);
-		ret += res;
-		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
-			return (res);
-		ret += res;
-		break;
-	case MSPH_TREE_ASSERT:
-		ass = (struct msph_tree_assert *)tree;
-		if ((res = indent_fprintf(f, indent, "(assert:%u,%u\n",
-		    TEXT(ass)->pos.line, TEXT(ass)->pos.col)) < 0) {
-			return (res);
-		}
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(ass->tp))) < 0)
-			return (res);
-		ret += res;
-		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
-			return (res);
-		ret += res;
-		break;
-	case MSPH_TREE_TPDEF:
-		tpdef = (struct msph_tree_tpdef *)tree;
-		if ((res = indent_fprintf(f, indent, "(tpdef:%u,%u\n",
-		    TEXT(tpdef)->pos.line, TEXT(tpdef)->pos.col)) < 0) {
-			return (res);
-		}
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(tpdef->name)))
-		    < 0) {
-			return (res);
-		}
-		ret += res;
-		STAILQ_FOREACH(named, &tpdef->params, entries) {
-			if ((res = tree_ind_fprint(f, indent+1, TREE(named)))
-			    < 0) {
-				return (res);
-			}
-			ret += res;
-		}
-		if ((res = tree_ind_fprint(f, indent+1, TREE(tpdef->tp))) < 0)
-			return (res);
-		ret += res;
-		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
-			return (res);
-		ret += res;
-		break;
-	case MSPH_TREE_MEMBDECL:
-		membdecl = (struct msph_tree_membdecl *)tree;
-		if ((res = indent_fprintf(f, indent, "(membdecl:%u,%u\n",
-		    TEXT(membdecl)->pos.line, TEXT(membdecl)->pos.col)) < 0) {
-			return (res);
-		}
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(membdecl->name)))
-		    < 0) {
-			return (res);
-		}
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(membdecl->tp)))
-		    < 0) {
-			return (res);
-		}
-		ret += res;
-		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
-			return (res);
-		ret += res;
-		break;
-	case MSPH_TREE_CONJ:
-		conj = (struct msph_tree_conj *)tree;
-		if ((res = indent_fprintf(f, indent, "(&conj:%u,%u\n",
-		    TEXT(conj)->pos.line, TEXT(conj)->pos.col)) < 0) {
-			return (res);
-		}
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(conj->ltp))) < 0)
-			return (res);
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(conj->rtp))) < 0)
-			return (res);
-		ret += res;
-		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
-			return (res);
-		ret += res;
-		break;
-	case MSPH_TREE_DISJ:
-		disj = (struct msph_tree_disj *)tree;
-		if ((res = indent_fprintf(f, indent, "(|disj:%u,%u\n",
-		    TEXT(disj)->pos.line, TEXT(disj)->pos.col)) < 0) {
-			return (res);
-		}
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(disj->ltp))) < 0)
-			return (res);
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(disj->rtp))) < 0)
-			return (res);
-		ret += res;
-		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
-			return (res);
-		ret += res;
-		break;
-	case MSPH_TREE_IMPL:
-		impl = (struct msph_tree_impl *)tree;
-		if ((res = indent_fprintf(f, indent, "(=>impl:%u,%u\n",
-		    TEXT(impl)->pos.line, TEXT(impl)->pos.col)) < 0) {
-			return (res);
-		}
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(impl->ltp))) < 0)
-			return (res);
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(impl->rtp))) < 0)
-			return (res);
-		ret += res;
-		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
-			return (res);
-		ret += res;
-		break;
-	case MSPH_TREE_SUBT:
-		subt = (struct msph_tree_subt *)tree;
-		if ((res = indent_fprintf(f, indent, "(<:subt:%u,%u\n",
-		    TEXT(subt)->pos.line, TEXT(subt)->pos.col)) < 0) {
-			return (res);
-		}
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(subt->ltp))) < 0)
-			return (res);
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(subt->rtp))) < 0)
-			return (res);
-		ret += res;
-		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
-			return (res);
-		ret += res;
-		break;
-	case MSPH_TREE_ARROW:
-		arrow = (struct msph_tree_arrow *)tree;
-		if ((res = indent_fprintf(f, indent, "(->arrow:%u,%u\n",
-		    TEXT(arrow)->pos.line, TEXT(arrow)->pos.col)) < 0) {
-			return (res);
-		}
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(arrow->ltp))) < 0)
-			return (res);
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(arrow->rtp))) < 0)
-			return (res);
-		ret += res;
-		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
-			return (res);
-		ret += res;
-		break;
-	case MSPH_TREE_BOX:
-		box = (struct msph_tree_box *)tree;
-		if ((res = indent_fprintf(f, indent, "(box:%u,%u\n",
-		    TEXT(box)->pos.line, TEXT(box)->pos.col)) < 0) {
-			return (res);
-		}
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(box->inner))) < 0)
-			return (res);
-		ret += res;
-		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
-			return (res);
-		ret += res;
-		break;
-	case MSPH_TREE_FORALL:
-		forall = (struct msph_tree_forall *)tree;
-		if ((res = indent_fprintf(f, indent, "(forall:%u,%u\n",
-		    TEXT(forall)->pos.line, TEXT(forall)->pos.col)) < 0) {
-			return (res);
-		}
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(forall->name)))
-		    < 0)
-			return (res);
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(forall->inner)))
-		    < 0) {
-			return (res);
-		}
-		ret += res;
-		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
-			return (res);
-		ret += res;
-		break;
-	case MSPH_TREE_PAREN:
-		paren = (struct msph_tree_paren *)tree;
-		if ((res = indent_fprintf(f, indent, "(paren:%u,%u\n",
-		    TEXT(paren)->pos.line, TEXT(paren)->pos.col)) < 0) {
-			return (res);
-		}
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(paren->inner)))
-		    < 0) {
-			return (res);
-		}
-		ret += res;
-		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
-			return (res);
-		ret += res;
-		break;
-	case MSPH_TREE_TPAPPL:
-		tpappl = (struct msph_tree_tpappl *)tree;
-		if ((res = indent_fprintf(f, indent, "(tpappl:%u,%u\n",
-		    TEXT(tpappl)->pos.line, TEXT(tpappl)->pos.col)) < 0)
-			return (res);
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(tpappl->name)))
-		    < 0) {
-			return (res);
-		}
-		ret += res;
-		STAILQ_FOREACH(tp, &tpappl->args, entries) {
-			if ((res = tree_ind_fprint(f, indent+1, TREE(tp)))
-			    < 0) {
-				return (res);
-			}
-			ret += res;
-		}
-		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
-			return (res);
-		ret += res;
-		break;
-	case MSPH_TREE_TPNAME:
-		name = (struct msph_tree_tpname *)tree;
-		if ((res = indent_fprintf(f, indent, "(name:%u,%u\n",
-		    TEXT(name)->pos.line, TEXT(name)->pos.col)) < 0) {
-			return (res);
-		}
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(name->name))) < 0)
-			return (res);
-		ret += res;
-		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
-			return (res);
-		ret += res;
-		break;
-	case MSPH_TREE_TRAIT:
-		trait = (struct msph_tree_trait *)tree;
-		if ((res = indent_fprintf(f, indent, "(trait:%u,%u\n",
-		    TEXT(trait)->pos.line, TEXT(trait)->pos.col)) < 0)
-			return (res);
-		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, TREE(trait->body)))
-		    < 0) {
-			return (res);
-		}
-		ret += res;
-		if ((res = indent_fprintf(f, indent, ")\n")) < 0)
-			return (res);
-		ret += res;
-		break;
-	case MSPH_TREE_NAMEDECL:
-	case MSPH_TREE_NAMEREF:
-	case MSPH_TREE_IDENT:
-		switch (TREE_ID(tree)) {
-		case MSPH_TREE_NAMEDECL:
-			ident_kind = "/namedecl";
-			break;
-		case MSPH_TREE_NAMEREF:
-			ident_kind = "/nameref";
-			break;
-		default:
-			ident_kind = "";
-		}
-		ident = IDENT(tree);
-		if ((res = indent_fprintf(f, indent, "(ident%s:%u,%u:%s)\n",
-		    ident_kind, TEXT(ident)->pos.line, TEXT(ident)->pos.col,
-		    ident->str)) < 0) {
-			return (res);
-		}
-		ret += res;
-		break;
-	case MSPH_TREE_TRUE:
-		if ((res = indent_fprintf(f, indent, "(true:%u,%u)\n",
-		    TEXT(tree)->pos.line, TEXT(tree)->pos.col)) < 0) {
-			return (res);
-		}
-		ret += res;
-		break;
-	case MSPH_TREE_FALSE:
-		if ((res = indent_fprintf(f, indent, "(false:%u,%u)\n",
-		    TEXT(tree)->pos.line, TEXT(tree)->pos.col)) < 0) {
-			return (res);
-		}
-		ret += res;
-		break;
-	default:
-		SPHO_ASSERT(0);
-		break;
-	}
-
-	return (ret);
-}
diff --git a/src/spho/bind.c b/src/spho/bind.c
index 7bc0d6b..fc2258b 100644
--- a/src/spho/bind.c
+++ b/src/spho/bind.c
@@ -19,21 +19,20 @@ spho_prebind_create(struct spho_scope *sc)
 		return (NULL);
 	}
 
-	if ((bind->binds = calloc(sc->nom_cnt, sizeof(*bind->binds))) == NULL) {
+	if ((bind->binds = calloc(sc->n_noms, sizeof(*bind->binds))) == NULL) {
 		SPHO_ERR(sc->ctx, SPHO_ERR_SYS);
 		free(bind);
 		return (NULL);
 	}
 
 	bind->sc = sc;
-	bind->sz = sc->nom_cnt;
+	bind->sz = sc->n_noms;
 
 
 	i = 0;
-	SLIST_FOREACH(nom, &sc->noms, entries) {
+	SLIST_FOREACH(nom, &sc->noms, next) {
 		SPHO_ASSERT(i < bind->sz);
-		bind->binds[i++] =
-		       	(struct spho_prebind_pair) { nom, 0, { NULL } };
+		bind->binds[i++] = (struct spho_prebind_pair) { NULL, 0, NULL };
 	}
 
 	return (bind);
diff --git a/src/spho/ctx.c b/src/spho/ctx.c
index 2b82bd9..cd43288 100644
--- a/src/spho/ctx.c
+++ b/src/spho/ctx.c
@@ -37,31 +37,28 @@ spho_ctx_create(void)
 
 	c = NULL;
 
-	if ((c = calloc(1, sizeof(struct spho_ctx))) == NULL)
+	if ((c = malloc(sizeof(struct spho_ctx))) == NULL)
 		return (NULL);
 
-	spho_ctx_init(c);
+	c->err = 0;
+	c->err_info = 0;
+
+	if (spho_scope_init(&c->glob, c, NULL) == -1) {
+		free(c);
+		return (NULL);
+	}
+
+	SPHO_POSTCOND(c != NULL);
 
 	return (c);
 }
 
-void
-spho_ctx_init(struct spho_ctx *ctx)
-{
-	ctx->err = 0;
-	ctx->err_info = 0;
-
-	ctx->nom_cnt = 0;
-
-	spho_scope_init(&ctx->glob, ctx, NULL);
-}
-
 void
 spho_ctx_destroy(struct spho_ctx *ctx)
 {
 	SPHO_PRECOND(ctx != NULL);
 
-	spho_scope_cleanup(&ctx->glob);
+	spho_scope_term(&ctx->glob);
 
 	free(ctx);
 }
diff --git a/src/spho/scope.c b/src/spho/scope.c
index 9f1b15c..da5c679 100644
--- a/src/spho/scope.c
+++ b/src/spho/scope.c
@@ -8,59 +8,41 @@
 #include "spho/scope.h"
 #include "spho/bind.h"
 
+static void spho_nom_term(struct spho_nom *);
+
 static int scope_nom_lookup_str_local(struct spho_scope *, const char *,
     size_t, struct spho_nom **);
 static int scope_nom_in_local(struct spho_scope *, struct spho_nom *);
 
-void
+int
 spho_scope_init(struct spho_scope *sc, struct spho_ctx *ctx,
     struct spho_scope *p)
 {
 	sc->ctx = ctx;
 	sc->parent = p;
 
-	STAILQ_INIT(&sc->subs);
+	SLIST_INIT(&sc->subs);
 
 	SLIST_INIT(&sc->noms);
-	sc->nom_cnt = 0;
+	sc->n_noms = 0;
 
-	STAILQ_INIT(&sc->tps);
+	TAILQ_INIT(&sc->tps);
 
 	sc->bind_loc = NULL;
+
+	return (0);
 }
 
 void
-spho_scope_cleanup(struct spho_scope *sc)
+spho_scope_term(struct spho_scope *sc)
 {
-	struct spho_scope *sub;
-	struct spho_nom *nom;
-	struct spho_tp_alloc *tp_alloc;
+	SPHO_UTIL_SLIST_DESTROY(&sc->subs, spho_scope, next, spho_scope_term);
 
-	/* XXX is doable without recursive call, but cba */
-	while (! STAILQ_EMPTY(&sc->subs)) {
-		sub = STAILQ_FIRST(&sc->subs);
-		STAILQ_REMOVE_HEAD(&sc->subs, entries);
-		spho_scope_cleanup(sub);
-		free(sub);
-	}
-
-	/* all type structs are allocated from scope */
-	while (! STAILQ_EMPTY(&sc->tps)) {
-		tp_alloc = STAILQ_FIRST(&sc->tps);
-		STAILQ_REMOVE_HEAD(&sc->tps, entries);
-		free(tp_alloc);
-	}
-
-	/* names are allocated in scope too */
-	while (! SLIST_EMPTY(&sc->noms)) {
-		nom = SLIST_FIRST(&sc->noms);
-		SLIST_REMOVE_HEAD(&sc->noms, entries);
-		free(nom);
-	}
+	SPHO_UTIL_SLIST_DESTROY(&sc->noms, spho_nom, next, spho_nom_term);
 
 	sc->parent = NULL;
 
-	if (sc->bind_loc != NULL)
+	if (sc->bind_loc == NULL)
 		spho_prebind_free(sc->bind_loc);
 	sc->bind_loc = NULL;
 }
@@ -75,7 +57,7 @@ spho_scope_global(struct spho_ctx *ctx)
 
 
 struct spho_scope *
-spho_scope_create_subscope(struct spho_scope *sc)
+spho_scope_create(struct spho_scope *sc)
 {
 	struct spho_scope *sub;
 
@@ -84,24 +66,35 @@ spho_scope_create_subscope(struct spho_scope *sc)
 		return (NULL);
 	}
 
-	spho_scope_init(sub, sc->ctx, sc);
+	if (spho_scope_init(sub, sc->ctx, sc) == -1) {
+		free(sub);
+		return (NULL);
+	}
 
-	STAILQ_INSERT_TAIL(&sc->subs, sub, entries);
+	SLIST_INSERT_HEAD(&sc->subs, sub, next);
 
 	return (sub);
 }
 
+
+static void
+spho_nom_term(__attribute__((unused)) struct spho_nom *nom)
+{
+	return;
+}
+
 void
-spho_scope_free(struct spho_scope *sc)
+spho_scope_destroy(struct spho_scope *sc)
 {
 	struct spho_scope *p;
 
 	p = sc->parent;
-	STAILQ_REMOVE(&p->subs, sc, spho_scope, entries);
-	spho_scope_cleanup(sc);
+	SLIST_REMOVE(&p->subs, sc, spho_scope, next);
+	spho_scope_term(sc);
 	free(sc);
 }
 
+
 struct spho_nom *
 spho_scope_nom_add(struct spho_scope *sc, const char *nomstr, size_t sz)
 {
@@ -128,10 +121,9 @@ spho_scope_nom_add(struct spho_scope *sc, const char *nomstr, size_t sz)
 		SPHO_SC_ERR(sc, SPHO_ERR_TOOBIG);
 		goto err;
 	}
-	nom->id = sc->ctx->nom_cnt++;
 
-	SLIST_INSERT_HEAD(&sc->noms, nom, entries);
-	sc->nom_cnt++;
+	SLIST_INSERT_HEAD(&sc->noms, nom, next);
+	sc->n_noms++;
 
 	return (nom);
 err:
@@ -141,7 +133,7 @@ err:
 
 
 int
-spho_scope_nom_lookup(struct spho_scope *sc, const char *nomstr, size_t sz,
+spho_scope_nom_lookup_str(struct spho_scope *sc, const char *nomstr, size_t sz,
     struct spho_nom **out)
 {
 	struct spho_nom *nom;
@@ -155,7 +147,7 @@ spho_scope_nom_lookup(struct spho_scope *sc, const char *nomstr, size_t sz,
 
 	*out = NULL;
 	while (*out == NULL && sc != NULL) {
-		SLIST_FOREACH(nom, &sc->noms, entries) {
+		SLIST_FOREACH(nom, &sc->noms, next) {
 			if (strncmp(nom->s, nomstr, sz) == 0) {
 				*out = nom;
 				break;
@@ -168,10 +160,10 @@ spho_scope_nom_lookup(struct spho_scope *sc, const char *nomstr, size_t sz,
 }
 
 int
-spho_scope_nom_lookup_strict(struct spho_scope *sc, const char *nomstr,
+spho_scope_nom_lookup_str_strict(struct spho_scope *sc, const char *nomstr,
     size_t sz, struct spho_nom **out)
 {
-	if (spho_scope_nom_lookup(sc, nomstr, sz, out) == -1)
+	if (spho_scope_nom_lookup_str(sc, nomstr, sz, out) == -1)
 		return (-1);
 
 	if (*out == NULL) {
@@ -185,8 +177,10 @@ spho_scope_nom_lookup_strict(struct spho_scope *sc, const char *nomstr,
 int
 spho_scope_prebind_init(struct spho_scope *sc)
 {
-	if ((sc->bind_loc = spho_prebind_create(sc)) == NULL)
+	if ((sc->bind_loc = spho_prebind_create(sc)) 
+	    == NULL) {
 		return (-1);
+	}
 
 	return (0);
 }
@@ -240,7 +234,7 @@ scope_nom_lookup_str_local(struct spho_scope *sc, const char *nomstr,
 	}
 
 	*out = NULL;
-	SLIST_FOREACH(nom, &sc->noms, entries) {
+	SLIST_FOREACH(nom, &sc->noms, next) {
 		if (strncmp(nom->s, nomstr, sz) == 0) {
 			*out = nom;
 			break;
@@ -255,7 +249,7 @@ scope_nom_in_local(struct spho_scope *sc, struct spho_nom *nom)
 {
 	struct spho_nom *sc_nom;
 
-	SLIST_FOREACH(sc_nom, &sc->noms, entries) {
+	SLIST_FOREACH(sc_nom, &sc->noms, next) {
 		if (sc_nom == nom)
 			return (1);
 	}
diff --git a/src/spho/tp.c b/src/spho/tp.c
index 2fe6140..4140633 100644
--- a/src/spho/tp.c
+++ b/src/spho/tp.c
@@ -20,7 +20,7 @@ spho_tp_alloc(struct spho_scope *sc)
 	}
 
 	((struct spho_tp *)tp_alloc)->sc = sc;
-	STAILQ_INSERT_TAIL(&sc->tps, tp_alloc, entries);
+	TAILQ_INSERT_TAIL(&sc->tps, tp_alloc, allocs);
 
 	return ((struct spho_tp *)tp_alloc);
 }
@@ -36,11 +36,25 @@ spho_tp_op_alloc(struct spho_scope *sc)
 	}
 
 	((struct spho_tp_op *)tp_alloc)->sc = sc;
-	STAILQ_INSERT_TAIL(&sc->tps, tp_alloc, entries);
+	TAILQ_INSERT_TAIL(&sc->tps, tp_alloc, allocs);
 
 	return ((struct spho_tp_op *)tp_alloc);
 }
 
+static void
+spho_tp_free(struct spho_tp *tp)
+{
+	struct spho_scope *sc;
+	struct spho_tp_alloc *tp_alloc;
+
+	sc = tp->sc;
+	tp_alloc = (struct spho_tp_alloc *)tp;
+
+	TAILQ_REMOVE(&sc->tps, tp_alloc, allocs);
+
+	free(tp_alloc);
+}
+
 struct spho_tp *
 spho_tp_create_conj(struct spho_scope *sc, struct spho_tp *ltp,
     struct spho_tp *rtp)
@@ -256,3 +270,45 @@ spho_tp_op_create(struct spho_scope *sc, struct spho_scope *op_sc, struct spho_t
 
 	return (op);
 }
+
+/* Free type structure. External data (like nom) are freed elsewhere. */
+void
+spho_tp_destroy(struct spho_tp *tp)
+{
+	struct spho_tp *arg;
+
+	switch (tp->kind & SPHO_TP_FORM_MASK) {
+	case SPHO_TP_FORM_TRUE:
+	case SPHO_TP_FORM_FALSE:
+	case SPHO_TP_FORM_NAME: 
+	case SPHO_TP_FORM_VAR:
+		break;
+	case SPHO_TP_FORM_CONJ:
+	case SPHO_TP_FORM_DISJ:
+	case SPHO_TP_FORM_IMPL:
+	case SPHO_TP_FORM_ARROW:
+		spho_tp_destroy(tp->d.binop.left);
+		spho_tp_destroy(tp->d.binop.right);
+		break;
+	case SPHO_TP_FORM_BOX:
+		spho_tp_destroy(tp->d.unop.operand);
+		break;
+	case SPHO_TP_FORM_FORALL:
+		spho_tp_destroy(tp->d.fa.tp);
+		break;
+	case SPHO_TP_FORM_MEMBER: 
+		spho_tp_destroy(tp->d.memb.tp);
+		break;
+	case SPHO_TP_FORM_APPL:
+		STAILQ_FOREACH(arg, tp->d.appl.args, entries) {
+			spho_tp_destroy(arg);
+		}
+		free(tp->d.appl.args);
+		break;
+	default:
+		SPHO_ASSERT(0);
+		break;
+	}
+
+	spho_tp_free(tp);
+}