diff --git a/.gitignore b/.gitignore
index 4929d75..4935877 100644
--- a/.gitignore
+++ b/.gitignore
@@ -52,6 +52,8 @@ Mkfile.old
 dkms.conf
 
 # vim
+.swp
+.swo
 .*.swp
 .*.swo
 
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 99b7405..ea221d1 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
new file mode 100644
index 0000000..f9f5e51
--- /dev/null
+++ b/CMakePresets.json
@@ -0,0 +1,82 @@
+{
+  "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 8d01411..4259565 100644
--- a/README.md
+++ b/README.md
@@ -4,14 +4,73 @@ 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 . -B build
-cd build
+cmake . --preset=debug
+cd build-debug
 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 b2b01f1..246c2e2 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. modular logic)
+       | box t              (box, c.f. modal 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,17 +114,19 @@ 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 40c97dc..9b71035 100644
--- a/docs/about/progress.md
+++ b/docs/about/progress.md
@@ -1,11 +1,9 @@
-# draft of presentation
-
-## sappho short
+# 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
 
@@ -15,7 +13,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. modular logic)
+       | box t              (box, c.f. modal logic)
        | a [t..]            (type operator application)
        | x                  (variable)
        | n                  (nominal)
@@ -30,7 +28,7 @@ n ∈ nominal
 a ∈ opname
 ```
 
-The type `t <: s` would be expressive sugar for `box (t => s)`
+The type `t <: s` would be syntactic sugar for `box (t => s)`
 
 ### msph and spho
 
@@ -60,7 +58,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
@@ -75,7 +73,8 @@ 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
@@ -85,3 +84,4 @@ 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
new file mode 100644
index 0000000..2f73457
--- /dev/null
+++ b/example/comparable.msph
@@ -0,0 +1,16 @@
+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
deleted file mode 100644
index 0844c3f..0000000
--- a/example/ex1.msph
+++ /dev/null
@@ -1,4 +0,0 @@
-
-nominal C
-
-
diff --git a/example/ex2.msph b/example/ex2.msph
deleted file mode 100644
index 5b85fdc..0000000
--- a/example/ex2.msph
+++ /dev/null
@@ -1 +0,0 @@
-type A = & C D
diff --git a/example/ex3.msph b/example/ex3.msph
deleted file mode 100644
index 9770336..0000000
--- a/example/ex3.msph
+++ /dev/null
@@ -1,13 +0,0 @@
-
-type X = & C (| D E)
-
-type Y = {
-	member x : X
-	type Z = & X {
- 		type T = C
-		assert C <: D
-	}
-	member r : (box forall S. (=> S Y))
-	member s : C[X, Y, z]
-	member f : -> A B
-}
diff --git a/example/ex4.msph b/example/ex4.msph
deleted file mode 100644
index ffc0174..0000000
--- a/example/ex4.msph
+++ /dev/null
@@ -1,20 +0,0 @@
-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
deleted file mode 100644
index 5774e54..0000000
--- a/example/ex5.msph
+++ /dev/null
@@ -1,21 +0,0 @@
-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
new file mode 100644
index 0000000..b636f3b
--- /dev/null
+++ b/example/graph.msph
@@ -0,0 +1,10 @@
+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
deleted file mode 100644
index afdeccb..0000000
--- a/example/non-parse/ex6.msph
+++ /dev/null
@@ -1,21 +0,0 @@
-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/subt/rec-lockstep.msph b/example/rec-lockstep.msph
similarity index 100%
rename from example/subt/rec-lockstep.msph
rename to example/rec-lockstep.msph
diff --git a/example/self.msph b/example/self.msph
new file mode 100644
index 0000000..d482e1c
--- /dev/null
+++ b/example/self.msph
@@ -0,0 +1,19 @@
+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/include/msph/common.h b/include/msph/msph.h
similarity index 85%
rename from include/msph/common.h
rename to include/msph/msph.h
index eb49da4..f34980b 100644
--- a/include/msph/common.h
+++ b/include/msph/msph.h
@@ -1,5 +1,5 @@
-#ifndef _MSPH_COMMON_H
-#define _MSPH_COMMON_H
+#ifndef _MSPH_H
+#define _MSPH_H
 
 #include "msph/err.h"
 #include "spho/ctx.h"
@@ -25,4 +25,4 @@ struct msph_text_pos {
 	unsigned int	col;
 };
 
-#endif
+#endif /* ifndef _MSPH_H */
diff --git a/include/msph/token.h b/include/msph/token.h
index b984039..18fb7ae 100644
--- a/include/msph/token.h
+++ b/include/msph/token.h
@@ -3,7 +3,7 @@
 
 #include <sys/queue.h>
 
-#include "msph/common.h"
+#include "msph/msph.h"
 
 /*
  *
@@ -39,6 +39,8 @@
 
 
 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,		// [
@@ -67,9 +69,10 @@ enum msph_tok_type {
 	TOK_CONST_FALSE,	// False
 
 	TOK_IDENT,		// identifiers
-	TOK_INVAL,		// special: invalid, use to mark invalid toks
-	TOK_WSPACE,		// special: whitespace
-	TOK_END			// special: end of array/token stream
+	TOK_WSPACE,		// whitespace
+
+	TOK_NOPE		// special indicator: end of info array,
+				//		      start of parsing
 };
 
 #define MSPH_TAB_WIDTH		8
diff --git a/include/msph/tree.h b/include/msph/tree.h
index 028f329..3fffcfc 100644
--- a/include/msph/tree.h
+++ b/include/msph/tree.h
@@ -3,7 +3,7 @@
 
 #include <sys/queue.h>
 
-#include "msph/common.h"
+#include "msph/msph.h"
 #include "msph/token.h"
 
 /* tree decorations */
@@ -37,6 +37,8 @@ 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
@@ -162,8 +164,7 @@ struct msph_tree_membdecl {
 struct msph_tree_assert {
 	struct msph_tree_dir	hd_dir;
 
-	struct msph_tree_tpexpr	*ltp;
-	struct msph_tree_tpexpr	*rtp;
+	struct msph_tree_tpexpr	*tp;
 };
 
 struct msph_tree_namedecl {
@@ -209,6 +210,7 @@ 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;
 
@@ -230,6 +232,13 @@ 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;
 
@@ -259,7 +268,11 @@ struct msph_tree_paren {
 
 struct msph_tree_root	*msph_tree_makeroot(struct msph_ctx *);
 
-int	msph_tree_parse(struct msph_token_stream *, struct msph_tree_root *);
+#define MSPH_PARSE_PREFIX	1
+#define MSPH_PARSE_INFIX	2
+
+int	msph_tree_parse(struct msph_token_stream *, struct msph_tree_root *,
+	    int);
 
 ssize_t	msph_tree_fprint(FILE *, struct msph_tree *);
 
diff --git a/include/spho/ctx.h b/include/spho/ctx.h
index 9858e85..00bb1f4 100644
--- a/include/spho/ctx.h
+++ b/include/spho/ctx.h
@@ -14,6 +14,8 @@ 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;
@@ -22,6 +24,7 @@ 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 2f56532..6e34929 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__);						\
+		    __FILE__ ":%s", __func__);				\
 		(ctx)->errline = __LINE__;				\
 	} while (0)
 
diff --git a/include/spho/scope.h b/include/spho/scope.h
index ff682c4..52362e8 100644
--- a/include/spho/scope.h
+++ b/include/spho/scope.h
@@ -7,13 +7,22 @@
 
 #define SPHO_NOM_LEN	128
 
-/* name */
-struct spho_nom {
-	char			s[SPHO_NOM_LEN];
-	SLIST_ENTRY(spho_nom)	next; // TODO change to allocs
+
+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_HEAD(spho_nom_l, spho_nom);
 
 
 #define TP_KONST_KEY_TRUE	0x43445 /* don't change!!!!! */
@@ -76,6 +85,7 @@ struct spho_tp {
 
 	int			kind;
 	union tp_data		d;
+	union spho_ext_data	ext_data;
 
 	STAILQ_ENTRY(spho_tp)	entries;
 };
@@ -85,30 +95,20 @@ 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;
 
-	TAILQ_ENTRY(spho_tp_alloc)	allocs;
+	STAILQ_ENTRY(spho_tp_alloc)	entries;
 };
 
-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,33 +116,38 @@ struct spho_scope {
 	struct spho_ctx		*ctx;
 	struct spho_scope	*parent;
 
-	struct spho_scope_l	subs;
-
-	size_t			n_noms;
-	struct spho_nom_l	noms;
-	struct spho_tp_alloc_l	tps;
-
+	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;
 
-	SLIST_ENTRY(spho_scope)	next;
+	STAILQ_ENTRY(spho_scope)	entries;
 };
 
 #define SPHO_SC_ERR(sc, err)	SPHO_ERR((sc)->ctx, (err))
 
-int	spho_scope_init(struct spho_scope *, struct spho_ctx *,
+void	spho_scope_init(struct spho_scope *, struct spho_ctx *,
 	    struct spho_scope *);
-void	spho_scope_term(struct spho_scope *);
+void	spho_scope_cleanup(struct spho_scope *);
 
 struct spho_scope	*spho_scope_global(struct spho_ctx *);
-struct spho_scope	*spho_scope_create(struct spho_scope *);
+struct spho_scope	*spho_scope_create_subscope(struct spho_scope *);
 
 
-void spho_scope_destroy(struct spho_scope *);
+void spho_scope_free(struct spho_scope *);
 
 struct spho_nom	*spho_scope_nom_add(struct spho_scope *, const char *, size_t);
-int	spho_scope_nom_lookup_str(struct spho_scope *, const char *, size_t,
+int	spho_scope_nom_lookup(struct spho_scope *, const char *, size_t,
 	    struct spho_nom **);
-int	spho_scope_nom_lookup_str_strict(struct spho_scope *, const char *,
+int	spho_scope_nom_lookup_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 041bdff..c9d3afe 100644
--- a/src/msph/msph.c
+++ b/src/msph/msph.c
@@ -2,28 +2,20 @@
 #include <stdio.h>
 #include <unistd.h>
 
-#include "msph/err.h"
+#include "msph/msph.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" \
-	"\tUsage: msph [-t] [-o out_path] [in_path]\n" \
-	"\n" \
-	"\t-t	- print tokenization\n" \
-	"\t-o	- output path\n"
+"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"
 
 void
 print_usage(void)
@@ -31,6 +23,64 @@ 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
@@ -38,7 +88,7 @@ main(int argc, char *argv[])
 {
 	int opt;
 
-	while ((opt = getopt(argc, argv, "hto:")) != -1) {
+	while ((opt = getopt(argc, argv, "hto:p:")) != -1) {
 		switch (opt) {
 		case 't':
 			run_opts.tokenize_only = 1;
@@ -46,6 +96,19 @@ 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);
@@ -81,6 +144,7 @@ run(struct msph_opts *opts)
 	struct msph_tree_root *root;
 	FILE *in, *out;
 
+
 	in = out = NULL;
 	s = NULL;
 	root = NULL;
@@ -122,7 +186,7 @@ run(struct msph_opts *opts)
 		goto err;
 	}
 
-	if (msph_tree_parse(s, root) == -1)
+	if (msph_tree_parse(s, root, opts->parser) == -1)
 		goto err;
 
 	printf("msph tree successfully parsed :)\n");
@@ -140,13 +204,7 @@ exit:
 	return (0);
 
 err:
-	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);
-	}
+	print_error(&ctx);
 
 	if (in)
 		fclose(in);
@@ -156,6 +214,7 @@ err:
 }
 
 
+
 void
 msph_ctx_init(struct msph_ctx *ctx)
 {
diff --git a/src/msph/sphophi.c b/src/msph/sphophi.c
index a9dec26..0a629b5 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_tp_prebind(struct spho_scope *,
+static int	msph_tree_sphophi_prebind(struct spho_scope *,
 		    struct msph_tree *);
 
 /* is the tree a name binding? */
@@ -65,6 +65,8 @@ 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,
@@ -109,6 +111,8 @@ 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,
@@ -154,7 +158,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_tp_prebind,
+	return (msph_sphophi_foreach_pre(msph_tree_sphophi_prebind,
 		    root));
 }
 
@@ -191,25 +195,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(sc)) == NULL)
-			ret = -1;
+		if ((SCOPE(tree) = spho_scope_create_subscope(sc)) == NULL)
+			return (-1);
 		ADD_FLAG(tree, MSPH_TREE_FLAG_SCOPE);
 		break;
 	case MSPH_TREE_TPDEF:
 		tpdef = (struct msph_tree_tpdef *)tree;
-		if (! STAILQ_EMPTY(&tpdef->params) &&
-		    ((SCOPE(tpdef) = spho_scope_create(sc)) == NULL)) {
-			ret = -1;
-		}
+		if (STAILQ_EMPTY(&tpdef->params))
+			break;
+		if (((SCOPE(tpdef) = spho_scope_create_subscope(sc)) == NULL))
+			return (-1);
 		ADD_FLAG(tree, MSPH_TREE_FLAG_SCOPE);
 		break;
-	case MSPH_TREE_IDENT:
-		if (! IS_BINDING(tree->parent))
-			break;
+	case MSPH_TREE_NAMEDECL:
+		SPHO_ASSERT(IS_BINDING(tree->parent));
 		ident = (struct msph_tree_ident *)tree;
 		if ((NOM(ident) = spho_scope_nom_add(sc, ident->str,
-			    sizeof(ident->str))) == NULL)
-			ret = -1;
+			    sizeof(ident->str))) == NULL) {
+			return (-1);
+		}
 		ADD_FLAG(tree, MSPH_TREE_FLAG_NOM);
 		break;
 	default:
@@ -230,12 +234,14 @@ msph_tree_sphophi_decor_tpexpr_nom(struct spho_scope *sc,
 
 	switch (TREE_ID(tree)) {
 	case MSPH_TREE_IDENT:
-		if (! IS_TPEXPR(tree->parent))
-			break;
-		ident = (struct msph_tree_ident *)tree;
-		ret = spho_scope_nom_lookup_str_strict(sc, ident->str,
-			    sizeof(ident->str), &NOM(ident));
+		SPHO_ASSERT(IS_TPEXPR(tree->parent));
 
+		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);
 		break;
 	default:
 		break;
@@ -261,6 +267,7 @@ 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;
@@ -271,43 +278,59 @@ msph_tree_sphophi_decor_tp(struct spho_scope *sc, struct msph_tree *tree)
 	dir = NULL;
 	membd = NULL;
 
-	if (! (tree->type & MSPH_TREE_TPEXPR))
+	if (! IS_TPEXPR(tree))
 		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:
@@ -383,7 +406,7 @@ msph_tree_sphophi_decor_tp(struct spho_scope *sc, struct msph_tree *tree)
 		ADD_FLAG(trait, MSPH_TREE_FLAG_TP);
 		break;
 	default:
-		SPHO_ASSERT(0);
+		SPHO_RIP("impossible-default-reached");
 		break;
 	}
 
@@ -397,7 +420,7 @@ cleanup:
 }
 
 static int
-msph_tree_sphophi_tp_prebind(struct spho_scope *sc,
+msph_tree_sphophi_prebind(struct spho_scope *sc,
     struct msph_tree *tree)
 {
 	int ret;
@@ -433,8 +456,8 @@ msph_tree_sphophi_tp_prebind(struct spho_scope *sc,
 				return (-1);
 			}
 
-			if ((ret = spho_scope_prebind_tp_op(sc, NOM(name), op))
-			    == -1) {
+			if ((ret = spho_scope_prebind_tp_op(sc,
+				    NOM(tpdef->name), op)) == -1) {
 				return (-1);
 			}
 		} else {
@@ -444,6 +467,8 @@ msph_tree_sphophi_tp_prebind(struct spho_scope *sc,
 			}
 		}
 		break;
+	case MSPH_TREE_NOMINDECL:
+		break;
 	default:
 		break;
 	}
@@ -628,9 +653,7 @@ 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->ltp)) != 0)
-		return (ret);
-	if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, ass->rtp)) != 0)
+	if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, ass->tp)) != 0)
 		return (ret);
 
 	return (ret);
@@ -680,6 +703,10 @@ 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);
@@ -717,7 +744,7 @@ msph_sphophi_foreach_pre_tpexpr(msph_tree_sphophi_f f, struct spho_scope *sc,
 		    (struct msph_tree_false *)tpexpr);
 		break;
 	default:
-		SPHO_RIP("default-reach");
+		SPHO_RIP("impossible-default-reached");
 		break;
 	}
 
@@ -775,6 +802,23 @@ 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)
@@ -1092,9 +1136,7 @@ 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->ltp)) != 0)
-		return (ret);
-	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, ass->rtp)) != 0)
+	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, ass->tp)) != 0)
 		return (ret);
 
 	return (f(sc, TREE(ass)));
@@ -1144,6 +1186,10 @@ 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);
@@ -1240,6 +1286,22 @@ 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 e83a11d..81f61c7 100644
--- a/src/msph/token.c
+++ b/src/msph/token.c
@@ -7,7 +7,7 @@
 
 #include "spho/spho.h"
 
-#include "msph/err.h"
+#include "msph/msph.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_END }
+	{ 0, 0, TOK_NOPE }
 };
 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_END , NULL, NULL }
+	{ TOK_NOPE , 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_END; m++) {
+	for (m = 1; token_matchers[m].type != TOK_NOPE; 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_END; i++) {
+	for (i = 0; token_info[i].type != TOK_NOPE; 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_END; i++) {
+	for (i = 0; token_info[i].type != TOK_NOPE; 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 199628c..2444da6 100644
--- a/src/msph/tree.c
+++ b/src/msph/tree.c
@@ -1,5 +1,6 @@
 #define SPHO_ENABLE_DEBUG_PRINT
 
+
 #include <sys/queue.h>
 
 #include <stdlib.h>
@@ -8,14 +9,16 @@
 
 #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;
+
 	SLIST_HEAD(msph_token_l, msph_token)	head;
 };
 
@@ -24,12 +27,10 @@ struct tree_parse {
 #define CTX(parse)		((parse)->s->ctx)
 
 static void	tree_parse_init(struct tree_parse *,
-		    struct msph_token_stream *);
+		    struct msph_token_stream *, int);
 static int	tree_parse_next_token(struct tree_parse *);
-static void	tree_parse_push_token(struct tree_parse *,
-		    struct msph_token *);
 
-static ssize_t	tree_ind_fprint(FILE *, int, struct msph_tree *);
+static int	tree_ind_fprint(FILE *, int, struct msph_tree *);
 
 static void	free_the_tree(struct msph_tree *);
 
@@ -59,6 +60,37 @@ 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 *,
@@ -71,14 +103,6 @@ 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 *,
@@ -91,12 +115,13 @@ msph_tree_makeroot(struct msph_ctx *ctx)
 {
 	struct msph_tree_root	*root;
 
-	if ((root = malloc(sizeof(*root))) == NULL) {
+	if ((root = calloc(1, 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;
 
@@ -105,6 +130,8 @@ 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
@@ -118,6 +145,8 @@ 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; \
@@ -134,6 +163,8 @@ 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; \
@@ -141,7 +172,8 @@ msph_tree_makeroot(struct msph_ctx *ctx)
 	} while (0)
 
 int
-msph_tree_parse(struct msph_token_stream *s, struct msph_tree_root *root)
+msph_tree_parse(struct msph_token_stream *s, struct msph_tree_root *root,
+    int parser)
 {
 	struct tree_parse p;
 	struct msph_tree_unit *unit;
@@ -151,7 +183,15 @@ msph_tree_parse(struct msph_token_stream *s, struct msph_tree_root *root)
 		return (-1);
 	}
 
-	tree_parse_init(&p, s);
+	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);
+	}
 
 	if ((unit = tree_parse_unit(&p, TREE(root))) == NULL)
 		return (-1);
@@ -166,383 +206,25 @@ 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)
+tree_parse_init(struct tree_parse *p, struct msph_token_stream *s, int parser)
 {
 	p->s = s;
-
 	memset(&p->curr, 0, sizeof(p->curr));
-
-	SLIST_INIT(&p->head);
+	p->curr.type = TOK_NOPE;
+	p->parser = parser;
 }
 
 static int
 tree_parse_next_token(struct tree_parse *p)
 {
 	int ret;
-	struct msph_token *tok;
-	if (! SLIST_EMPTY(&p->head)) {
-		tok = SLIST_FIRST(&p->head);
-		SLIST_REMOVE_HEAD(&p->head, entries);
-		memcpy(&p->curr, tok, sizeof(p->curr));
-		free(tok);
-		ret = 1;
-	} else {
-		ret = (int)msph_token_stream_read(&p->curr, 1, p->s);
-	}
+
+	SPHO_PRECOND(p->curr.type > TOK_EOF);
+
+	ret = (int)msph_token_stream_read(&p->curr, 1, p->s);
+
 #ifdef SPHO_ENABLE_DEBUG_PRINT
 	if (ret == 1) {
 		char buf[256];
@@ -551,6 +233,12 @@ 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);
 }
 
@@ -560,7 +248,7 @@ tree_parse_unit(struct tree_parse *p, struct msph_tree *parent)
 	size_t namelen;
 	struct msph_tree_unit *unit;
 
-	if ((unit = malloc(sizeof(*unit))) == NULL) {
+	if ((unit = calloc(1, sizeof(*unit))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -575,6 +263,8 @@ 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;
 
@@ -589,24 +279,23 @@ 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 = malloc(sizeof(*body))) == NULL) {
+	if ((body = calloc(1, 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 ((res = tree_parse_next_token(p)) > 0) {
+	while (1) {
 		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:
@@ -619,10 +308,6 @@ 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;
 		}
 
@@ -632,8 +317,6 @@ 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:
@@ -642,12 +325,6 @@ 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 *
@@ -659,7 +336,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 = malloc(sizeof(*def))) == NULL) {
+	if ((def = calloc(1, sizeof(*def))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -673,22 +350,17 @@ 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);
 
@@ -715,7 +387,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);
 }
@@ -733,7 +405,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);
 }
@@ -747,7 +419,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 = malloc(sizeof(size))) == NULL) {
+	if ((id = calloc(1, size)) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -756,12 +428,14 @@ tree_parse_ident_extsize(struct tree_parse *p, struct msph_tree *parent,
 	TEXT(id)->pos = CURR_TOKEN(p)->pos;
 	DECOR_INIT(id);
 
-	if (SPHO_STRLCPY(id->str, CURR_TOKEN(p)->data.str, sizeof(id->str))
+	if (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));
@@ -770,21 +444,39 @@ 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(p, parent);
+		tp = tree_parse_conj_prefix(p, parent);
 		break;
 	case TOK_PIPE:
-		tp = tree_parse_disj(p, parent);
+		tp = tree_parse_disj_prefix(p, parent);
 		break;
 	case TOK_IMPL:
-		tp = tree_parse_impl(p, parent);
+		tp = tree_parse_impl_prefix(p, parent);
+		break;
+	case TOK_SUB:
+		tp = tree_parse_subt_prefix(p, parent);
 		break;
 	case TOK_RARROW:
-		tp = tree_parse_arrow(p, parent);
+		tp = tree_parse_arrow_prefix(p, parent);
 		break;
 	case TOK_KW_BOX:
 		tp = tree_parse_box(p, parent);
@@ -817,14 +509,14 @@ tree_parse_tpexpr(struct tree_parse *p, struct msph_tree *parent)
 }
 
 struct msph_tree_tpexpr *
-tree_parse_conj(struct tree_parse *p, struct msph_tree *parent)
+tree_parse_conj_prefix(struct tree_parse *p, struct msph_tree *parent)
 {
 	int res;
 	struct msph_tree_conj *conj;
 
 	EXPECT_CURR_TOKEN(p, TOK_AMP, MSPH_TREE_CONJ, return (NULL));
 
-	if ((conj = malloc(sizeof(*conj))) == NULL) {
+	if ((conj = calloc(1, sizeof(*conj))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -836,12 +528,12 @@ tree_parse_conj(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(p, TREE(conj))) 
+	if ((conj->ltp = tree_parse_tpexpr_prefix(p, TREE(conj))) 
 	    == NULL)
 		goto err;
 
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_CONJ, goto err);
-	if ((conj->rtp = tree_parse_tpexpr(p, TREE(conj)))
+	if ((conj->rtp = tree_parse_tpexpr_prefix(p, TREE(conj)))
 	    == NULL)
 		goto err;
 
@@ -853,14 +545,14 @@ err:
 }
 
 struct msph_tree_tpexpr *
-tree_parse_disj(struct tree_parse *p, struct msph_tree *parent)
+tree_parse_disj_prefix(struct tree_parse *p, struct msph_tree *parent)
 {
 	int res;
 	struct msph_tree_disj *disj;
 
 	EXPECT_CURR_TOKEN(p, TOK_PIPE, MSPH_TREE_DISJ, return (NULL));
 
-	if ((disj = malloc(sizeof(*disj))) == NULL) {
+	if ((disj = calloc(1, sizeof(*disj))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -872,12 +564,12 @@ tree_parse_disj(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(p, (struct msph_tree *)disj)) 
+	if ((disj->ltp = tree_parse_tpexpr_prefix(p, (struct msph_tree *)disj)) 
 	    == NULL)
 		goto err;
 
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_DISJ, goto err);
-	if ((disj->rtp = tree_parse_tpexpr(p, (struct msph_tree *)disj))
+	if ((disj->rtp = tree_parse_tpexpr_prefix(p, (struct msph_tree *)disj))
 	    == NULL)
 		goto err;
 
@@ -889,14 +581,14 @@ err:
 }
 
 struct msph_tree_tpexpr *
-tree_parse_impl(struct tree_parse *p, struct msph_tree *parent)
+tree_parse_impl_prefix(struct tree_parse *p, struct msph_tree *parent)
 {
 	int res;
 	struct msph_tree_impl *impl;
 
 	EXPECT_CURR_TOKEN(p, TOK_IMPL, MSPH_TREE_IMPL, return (NULL));
 
-	if ((impl = malloc(sizeof(*impl))) == NULL) {
+	if ((impl = calloc(1, sizeof(*impl))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -908,12 +600,12 @@ tree_parse_impl(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(p, (struct msph_tree *)impl)) 
+	if ((impl->ltp = tree_parse_tpexpr_prefix(p, (struct msph_tree *)impl)) 
 	    == NULL)
 		goto err;
 
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_IMPL, goto err);
-	if ((impl->rtp = tree_parse_tpexpr(p, (struct msph_tree *)impl))
+	if ((impl->rtp = tree_parse_tpexpr_prefix(p, (struct msph_tree *)impl))
 	    == NULL)
 		goto err;
 
@@ -925,14 +617,50 @@ err:
 }
 
 struct msph_tree_tpexpr *
-tree_parse_arrow(struct tree_parse *p, struct msph_tree *parent)
+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)
 {
 	int res;
 	struct msph_tree_arrow *arrow;
 
 	EXPECT_CURR_TOKEN(p, TOK_RARROW, MSPH_TREE_ARROW, return (NULL));
 
-	if ((arrow = malloc(sizeof(*arrow))) == NULL) {
+	if ((arrow = calloc(1, sizeof(*arrow))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -944,12 +672,12 @@ tree_parse_arrow(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(p, (struct msph_tree *)arrow)) 
+	if ((arrow->ltp = tree_parse_tpexpr_prefix(p, (struct msph_tree *)arrow)) 
 	    == NULL)
 		goto err;
 
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_ARROW, goto err);
-	if ((arrow->rtp = tree_parse_tpexpr(p, (struct msph_tree *)arrow))
+	if ((arrow->rtp = tree_parse_tpexpr_prefix(p, (struct msph_tree *)arrow))
 	    == NULL)
 		goto err;
 
@@ -960,6 +688,318 @@ 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)
 {
@@ -968,7 +1008,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 = malloc(sizeof(*box))) == NULL) {
+	if ((box = calloc(1, sizeof(*box))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -996,7 +1036,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 = malloc(sizeof(*fa))) == NULL) {
+	if ((fa = calloc(1, sizeof(*fa))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -1028,11 +1068,9 @@ 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;
@@ -1040,24 +1078,13 @@ tree_parse_tpname_or_tpappl(struct tree_parse *p, struct msph_tree *parent)
 	if ((nameref = tree_parse_nameref(p, NULL)) == NULL)
 		return (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) {
+	if (CURR_TOKEN(p)->type == TOK_LBRAK) {
+		if ((ret = tree_parse_tpapplargs(p, nameref, parent)) == NULL) 
 			goto err;
-		}
-		tree_parse_push_token(p, tok);
-	} else if (res == -1) {
-		goto err;
+		return (ret);
 	}
 
-	if ((tpname = malloc(sizeof(*tpname))) == NULL) {
+	if ((tpname = calloc(1, sizeof(*tpname))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		goto err;
 	}
@@ -1097,7 +1124,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 = malloc(sizeof(*tpappl))) == NULL) {
+	if ((tpappl = calloc(1, sizeof(*tpappl))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -1107,41 +1134,30 @@ tree_parse_tpapplargs(struct tree_parse *p, struct msph_tree_nameref *name,
 	tpappl->name = NULL;
 	STAILQ_INIT(&tpappl->args);
 
-	/* 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;
+	EXPECT_READ_NEXT(res, p, MSPH_TREE_TPAPPL, 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);
-		}
+	if ((tp = tree_parse_tpexpr(p, TREE(tpappl))) == NULL)
+		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);
 	}
 
-	/* 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;
-	}
+	EXPECT_CURR_TOKEN(p, TOK_RBRAK, 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));
@@ -1156,7 +1172,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 = malloc(sizeof(*t))) == NULL) {
+	if ((t = calloc(1, sizeof(*t))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -1165,6 +1181,8 @@ 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);
 }
 
@@ -1175,7 +1193,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 = malloc(sizeof(*f))) == NULL) {
+	if ((f = calloc(1, sizeof(*f))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -1184,6 +1202,8 @@ 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);
 }
 
@@ -1195,7 +1215,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 = malloc(sizeof(*par))) == NULL) {
+	if ((par = calloc(1, sizeof(*par))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -1210,9 +1230,10 @@ 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));
@@ -1228,7 +1249,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 = malloc(sizeof(*trait))) == NULL) {
+	if ((trait = calloc(1, sizeof(*trait))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
 		return (NULL);
 	}
@@ -1238,12 +1259,15 @@ 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));
@@ -1261,13 +1285,14 @@ 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 = malloc(sizeof(*nomind))) == NULL) {
+	if ((nomind = calloc(1, 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);
@@ -1292,13 +1317,14 @@ 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 = malloc(sizeof(*membd))) == NULL) {
+	if ((membd = calloc(1, 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;
 
@@ -1306,7 +1332,6 @@ 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);
@@ -1327,29 +1352,20 @@ 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 = malloc(sizeof(*ass))) == NULL) {
+	if ((ass = calloc(1, 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;
-	ass->ltp = NULL;
-	ass->rtp = NULL;
+	DECOR_INIT(ass);
+	ass->tp = NULL;
 
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_ASSERT, goto err);
-	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)
+	if ((ass->tp = tree_parse_tpexpr(p, TREE(ass))) == NULL)
 		goto err;
 
 	return ((struct msph_tree_dir *)ass);
@@ -1367,3 +1383,411 @@ 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 fc2258b..7bc0d6b 100644
--- a/src/spho/bind.c
+++ b/src/spho/bind.c
@@ -19,20 +19,21 @@ spho_prebind_create(struct spho_scope *sc)
 		return (NULL);
 	}
 
-	if ((bind->binds = calloc(sc->n_noms, sizeof(*bind->binds))) == NULL) {
+	if ((bind->binds = calloc(sc->nom_cnt, sizeof(*bind->binds))) == NULL) {
 		SPHO_ERR(sc->ctx, SPHO_ERR_SYS);
 		free(bind);
 		return (NULL);
 	}
 
 	bind->sc = sc;
-	bind->sz = sc->n_noms;
+	bind->sz = sc->nom_cnt;
 
 
 	i = 0;
-	SLIST_FOREACH(nom, &sc->noms, next) {
+	SLIST_FOREACH(nom, &sc->noms, entries) {
 		SPHO_ASSERT(i < bind->sz);
-		bind->binds[i++] = (struct spho_prebind_pair) { NULL, 0, NULL };
+		bind->binds[i++] =
+		       	(struct spho_prebind_pair) { nom, 0, { NULL } };
 	}
 
 	return (bind);
diff --git a/src/spho/ctx.c b/src/spho/ctx.c
index cd43288..2b82bd9 100644
--- a/src/spho/ctx.c
+++ b/src/spho/ctx.c
@@ -37,28 +37,31 @@ spho_ctx_create(void)
 
 	c = NULL;
 
-	if ((c = malloc(sizeof(struct spho_ctx))) == NULL)
+	if ((c = calloc(1, sizeof(struct spho_ctx))) == NULL)
 		return (NULL);
 
-	c->err = 0;
-	c->err_info = 0;
-
-	if (spho_scope_init(&c->glob, c, NULL) == -1) {
-		free(c);
-		return (NULL);
-	}
-
-	SPHO_POSTCOND(c != NULL);
+	spho_ctx_init(c);
 
 	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_term(&ctx->glob);
+	spho_scope_cleanup(&ctx->glob);
 
 	free(ctx);
 }
diff --git a/src/spho/scope.c b/src/spho/scope.c
index da5c679..9f1b15c 100644
--- a/src/spho/scope.c
+++ b/src/spho/scope.c
@@ -8,41 +8,59 @@
 #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 *);
 
-int
+void
 spho_scope_init(struct spho_scope *sc, struct spho_ctx *ctx,
     struct spho_scope *p)
 {
 	sc->ctx = ctx;
 	sc->parent = p;
 
-	SLIST_INIT(&sc->subs);
+	STAILQ_INIT(&sc->subs);
 
 	SLIST_INIT(&sc->noms);
-	sc->n_noms = 0;
+	sc->nom_cnt = 0;
 
-	TAILQ_INIT(&sc->tps);
+	STAILQ_INIT(&sc->tps);
 
 	sc->bind_loc = NULL;
-
-	return (0);
 }
 
 void
-spho_scope_term(struct spho_scope *sc)
+spho_scope_cleanup(struct spho_scope *sc)
 {
-	SPHO_UTIL_SLIST_DESTROY(&sc->subs, spho_scope, next, spho_scope_term);
+	struct spho_scope *sub;
+	struct spho_nom *nom;
+	struct spho_tp_alloc *tp_alloc;
 
-	SPHO_UTIL_SLIST_DESTROY(&sc->noms, spho_nom, next, spho_nom_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);
+	}
 
 	sc->parent = NULL;
 
-	if (sc->bind_loc == NULL)
+	if (sc->bind_loc != NULL)
 		spho_prebind_free(sc->bind_loc);
 	sc->bind_loc = NULL;
 }
@@ -57,7 +75,7 @@ spho_scope_global(struct spho_ctx *ctx)
 
 
 struct spho_scope *
-spho_scope_create(struct spho_scope *sc)
+spho_scope_create_subscope(struct spho_scope *sc)
 {
 	struct spho_scope *sub;
 
@@ -66,35 +84,24 @@ spho_scope_create(struct spho_scope *sc)
 		return (NULL);
 	}
 
-	if (spho_scope_init(sub, sc->ctx, sc) == -1) {
-		free(sub);
-		return (NULL);
-	}
+	spho_scope_init(sub, sc->ctx, sc);
 
-	SLIST_INSERT_HEAD(&sc->subs, sub, next);
+	STAILQ_INSERT_TAIL(&sc->subs, sub, entries);
 
 	return (sub);
 }
 
-
-static void
-spho_nom_term(__attribute__((unused)) struct spho_nom *nom)
-{
-	return;
-}
-
 void
-spho_scope_destroy(struct spho_scope *sc)
+spho_scope_free(struct spho_scope *sc)
 {
 	struct spho_scope *p;
 
 	p = sc->parent;
-	SLIST_REMOVE(&p->subs, sc, spho_scope, next);
-	spho_scope_term(sc);
+	STAILQ_REMOVE(&p->subs, sc, spho_scope, entries);
+	spho_scope_cleanup(sc);
 	free(sc);
 }
 
-
 struct spho_nom *
 spho_scope_nom_add(struct spho_scope *sc, const char *nomstr, size_t sz)
 {
@@ -121,9 +128,10 @@ 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, next);
-	sc->n_noms++;
+	SLIST_INSERT_HEAD(&sc->noms, nom, entries);
+	sc->nom_cnt++;
 
 	return (nom);
 err:
@@ -133,7 +141,7 @@ err:
 
 
 int
-spho_scope_nom_lookup_str(struct spho_scope *sc, const char *nomstr, size_t sz,
+spho_scope_nom_lookup(struct spho_scope *sc, const char *nomstr, size_t sz,
     struct spho_nom **out)
 {
 	struct spho_nom *nom;
@@ -147,7 +155,7 @@ spho_scope_nom_lookup_str(struct spho_scope *sc, const char *nomstr, size_t sz,
 
 	*out = NULL;
 	while (*out == NULL && sc != NULL) {
-		SLIST_FOREACH(nom, &sc->noms, next) {
+		SLIST_FOREACH(nom, &sc->noms, entries) {
 			if (strncmp(nom->s, nomstr, sz) == 0) {
 				*out = nom;
 				break;
@@ -160,10 +168,10 @@ spho_scope_nom_lookup_str(struct spho_scope *sc, const char *nomstr, size_t sz,
 }
 
 int
-spho_scope_nom_lookup_str_strict(struct spho_scope *sc, const char *nomstr,
+spho_scope_nom_lookup_strict(struct spho_scope *sc, const char *nomstr,
     size_t sz, struct spho_nom **out)
 {
-	if (spho_scope_nom_lookup_str(sc, nomstr, sz, out) == -1)
+	if (spho_scope_nom_lookup(sc, nomstr, sz, out) == -1)
 		return (-1);
 
 	if (*out == NULL) {
@@ -177,10 +185,8 @@ spho_scope_nom_lookup_str_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);
 }
@@ -234,7 +240,7 @@ scope_nom_lookup_str_local(struct spho_scope *sc, const char *nomstr,
 	}
 
 	*out = NULL;
-	SLIST_FOREACH(nom, &sc->noms, next) {
+	SLIST_FOREACH(nom, &sc->noms, entries) {
 		if (strncmp(nom->s, nomstr, sz) == 0) {
 			*out = nom;
 			break;
@@ -249,7 +255,7 @@ scope_nom_in_local(struct spho_scope *sc, struct spho_nom *nom)
 {
 	struct spho_nom *sc_nom;
 
-	SLIST_FOREACH(sc_nom, &sc->noms, next) {
+	SLIST_FOREACH(sc_nom, &sc->noms, entries) {
 		if (sc_nom == nom)
 			return (1);
 	}
diff --git a/src/spho/tp.c b/src/spho/tp.c
index 4140633..2fe6140 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;
-	TAILQ_INSERT_TAIL(&sc->tps, tp_alloc, allocs);
+	STAILQ_INSERT_TAIL(&sc->tps, tp_alloc, entries);
 
 	return ((struct spho_tp *)tp_alloc);
 }
@@ -36,25 +36,11 @@ spho_tp_op_alloc(struct spho_scope *sc)
 	}
 
 	((struct spho_tp_op *)tp_alloc)->sc = sc;
-	TAILQ_INSERT_TAIL(&sc->tps, tp_alloc, allocs);
+	STAILQ_INSERT_TAIL(&sc->tps, tp_alloc, entries);
 
 	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)
@@ -270,45 +256,3 @@ 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);
-}