diff --git a/CMakeLists.txt b/CMakeLists.txt
index 466a3d9..8f3758c 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -22,10 +22,8 @@ set(SPHO_HEADER_DIR ${INCLUDE_DIR}/spho)
 
 set(SPHO_HEADER
 	${SPHO_HEADER_DIR}/ctx.h
-	${SPHO_HEADER_DIR}/data.h
 	${SPHO_HEADER_DIR}/err.h
 	${SPHO_HEADER_DIR}/loc.h
-	${SPHO_HEADER_DIR}/parse.h
 	${SPHO_HEADER_DIR}/scope.h
 	${SPHO_HEADER_DIR}/tp.h
 	${SPHO_HEADER_DIR}/spho.h
@@ -57,6 +55,7 @@ target_compile_definitions(devcheck PRIVATE
 set(MSPH_SRC
 	${SRC_DIR}/msph/token.c
 	${SRC_DIR}/msph/tree.c
+	${SRC_DIR}/msph/sphophi.c
 	${SRC_DIR}/msph/msph.c
 )
 
@@ -65,6 +64,8 @@ set(MSPH_HEADER
 	${INCLUDE_DIR}/msph/tree.h
 	${INCLUDE_DIR}/msph/common.h
 	${INCLUDE_DIR}/msph/err.h
+	${INCLUDE_DIR}/msph/decor.h
+	${INCLUDE_DIR}/msph/sphophi.h
 )
 
 add_executable(msph ${MSPH_SRC} ${MSPH_HEADER})
diff --git a/example/ex4.msph b/example/ex4.msph
new file mode 100644
index 0000000..ffc0174
--- /dev/null
+++ b/example/ex4.msph
@@ -0,0 +1,20 @@
+nominal M
+nominal N
+nominal O
+nominal P
+
+type A = {
+	member member1: & N M
+	member member2: | M N
+}
+
+type B = forall X. {
+	member member1 : & X A
+}
+
+member outer1 : box {
+	member member1: & B True
+	type T = & B A
+	member member2 : | (& T O) P
+	type S = & B False
+}
diff --git a/include/msph/common.h b/include/msph/common.h
index 43a6a6f..eb49da4 100644
--- a/include/msph/common.h
+++ b/include/msph/common.h
@@ -2,6 +2,7 @@
 #define _MSPH_COMMON_H
 
 #include "msph/err.h"
+#include "spho/ctx.h"
 
 #define MSPH_IDENT_LEN	128
 #define MSPH_NAME_LEN	1024
@@ -11,6 +12,8 @@ struct msph_ctx {
 	int	err_info;
 	char	errbuf[SPHO_ERR_BUF_LEN];
 
+	struct spho_ctx *spho;
+
 #ifdef SPHO_DEBUG
 	char	filebuf[SPHO_ERR_FILEBUF_LEN];
 	int	errline;
diff --git a/include/msph/decor.h b/include/msph/decor.h
new file mode 100644
index 0000000..db302d3
--- /dev/null
+++ b/include/msph/decor.h
@@ -0,0 +1,33 @@
+#ifndef _MSPH_DECOR_H
+#define _MSPH_DECOR_H
+
+struct msph_tp_decor {
+	struct spho_tp		*tp;
+};
+
+#define TP_DECOR_INIT(ptr) \
+	do { \
+		(ptr)->tp = NULL; \
+	} while (0)
+
+struct msph_scope_decor {
+	struct spho_scope	*sc;
+};
+
+#define SCOPE_DECOR_INIT(ptr) \
+	do { \
+		(ptr)->sc = NULL; \
+	} while (0)
+
+struct msph_nom_decor {
+	struct spho_nom		*nom;
+};
+
+#define NOM_DECOR_INIT(ptr) \
+	do { \
+		(ptr)->nom = NULL; \
+	} while (0)
+
+#define GET_SCOPE(ptr)	((ptr)->dec.sc)
+
+#endif /* _MSPH_DECOR_H */
diff --git a/include/msph/err.h b/include/msph/err.h
index bf113d5..1ef4dc7 100644
--- a/include/msph/err.h
+++ b/include/msph/err.h
@@ -17,6 +17,10 @@
 #define MSPH_ERR_TREE_EOF	0x2002
 #define MSPH_ERR_TREE_NOMATCH	0x2003
 
+#define MSPH_ERR_TYPE_INVAL	0x3001
+
+#define MSPH_ERR_SPHOPHI	0x10001
+
 
 // TODO add more diagnostics
 
diff --git a/include/msph/sphophi.h b/include/msph/sphophi.h
new file mode 100644
index 0000000..052b9bf
--- /dev/null
+++ b/include/msph/sphophi.h
@@ -0,0 +1,15 @@
+#ifndef _MSPH_TYPE_H
+#define _MSPH_TYPE_H
+
+#include "msph/tree.h"
+
+int	msph_sphophi_init(struct msph_tree_root *);
+int	msph_sphophi_scope(struct msph_tree_root *);
+int	msph_sphophi_nom_lookup(struct msph_tree_root *);
+int	msph_sphophi_tp(struct msph_tree_root *);
+
+int	msph_sphophi(struct msph_tree_root *);
+
+int	msph_sphoxex(struct msph_tree_root *);
+
+#endif
diff --git a/include/msph/tree.h b/include/msph/tree.h
index 22cc883..b2e793d 100644
--- a/include/msph/tree.h
+++ b/include/msph/tree.h
@@ -5,6 +5,7 @@
 
 #include "msph/common.h"
 #include "msph/token.h"
+#include "msph/decor.h"
 
 /*
  * TYPES:
@@ -99,7 +100,7 @@ struct msph_tree_ident;
 struct msph_tree_tpexpr;
 
 struct msph_tree_root {
-	struct msph_tree	tr;
+	struct msph_tree	htr;
 
 	struct msph_ctx		*ctx;
 
@@ -107,145 +108,154 @@ struct msph_tree_root {
 };
 
 struct msph_tree_unit {
-	struct msph_tree	tr;
+	struct msph_tree	htr;
 
 	char			name[MSPH_NAME_LEN];
 	struct msph_tree_body	*body;
+	struct msph_scope_decor	dec;
+
 	STAILQ_ENTRY(msph_tree_unit)	entries;
 };
 
 struct msph_tree_text {
-	struct msph_tree	tr;
+	struct msph_tree	htr;
 	struct msph_text_pos	pos;
 };
 
 struct msph_tree_body {
-	struct msph_tree		tr;
+	struct msph_tree		htr;
 
 	STAILQ_HEAD(msph_tree_dir_l, msph_tree_dir)	head;
 };
 
 struct msph_tree_dir {
-	struct msph_tree		tr;
+	struct msph_tree_text		htxt;
 
 	STAILQ_ENTRY(msph_tree_dir)	entries;
 };
 
 struct msph_tree_tpdef {
-	struct msph_tree_dir		dir;
+	struct msph_tree_dir		hdir;
 
 	struct msph_tree_ident		*id;
 	struct msph_tree_tpexpr		*tp;
 };
 
 struct msph_tree_nomindecl {
-	struct msph_tree_dir	dir;
+	struct msph_tree_dir	hdir;
 
 	struct msph_tree_ident	*id;
 };
 
 struct msph_tree_membdecl {
-	struct msph_tree_dir	dir;
+	struct msph_tree_dir	hdir;
 
 	struct msph_tree_ident	*id;
 	struct msph_tree_tpexpr	*tp;
 };
 
 struct msph_tree_assert {
-	struct msph_tree_dir	dir;
+	struct msph_tree_dir	hdir;
 
 	struct msph_tree_tpexpr	*ltp;
 	struct msph_tree_tpexpr	*rtp;
 };
 
 struct msph_tree_tpexpr {
-	struct msph_tree		tr;
+	struct msph_tree_text		htxt;
 
 	STAILQ_ENTRY(msph_tree_tpexpr)	entries;
+
+	struct msph_tp_decor		dec;
 };
 
 
 struct msph_tree_true {
-	struct msph_tree_tpexpr	tp;
+	struct msph_tree_tpexpr	htpe;
 };
 
 struct msph_tree_false {
-	struct msph_tree_tpexpr	tp;
+	struct msph_tree_tpexpr	htpe;
 };
 
 struct msph_tree_name {
-	struct msph_tree_tpexpr	tp;
+	struct msph_tree_tpexpr	htpe;
 
 	struct msph_tree_ident	*id;
 };
 
 struct msph_tree_appl {
-	struct msph_tree_tpexpr	tp;
+	struct msph_tree_tpexpr	htpe;
 
 	struct msph_tree_ident	*id;
 	STAILQ_HEAD(msph_tree_tpexpr_l, msph_tree_tpexpr) head;
 };
 
 struct msph_tree_trait {
-	struct msph_tree_tpexpr	tp;
+	struct msph_tree_tpexpr	htpe;
 
 	struct msph_tree_body	*body;
+
+	struct msph_scope_decor	dec;
 };
 
 struct msph_tree_conj {
-	struct msph_tree_tpexpr	tp;
+	struct msph_tree_tpexpr	htpe;
 
 	struct msph_tree_tpexpr	*ltp;
 	struct msph_tree_tpexpr	*rtp;
 };
 
 struct msph_tree_disj {
-	struct msph_tree_tpexpr	tp;
+	struct msph_tree_tpexpr	htpe;
 
 	struct msph_tree_tpexpr	*ltp;
 	struct msph_tree_tpexpr	*rtp;
 };
 
 struct msph_tree_impl {
-	struct msph_tree_tpexpr	tp;
+	struct msph_tree_tpexpr	htpe;
 
 	struct msph_tree_tpexpr	*ltp;
 	struct msph_tree_tpexpr	*rtp;
 };
 
 struct msph_tree_arrow {
-	struct msph_tree_tpexpr	tp;
+	struct msph_tree_tpexpr	htpe;
 
 	struct msph_tree_tpexpr	*ltp;
 	struct msph_tree_tpexpr	*rtp;
 };
 
 struct msph_tree_box {
-	struct msph_tree_tpexpr	tp;
+	struct msph_tree_tpexpr	htpe;
 
 	struct msph_tree_tpexpr	*inner;
 };
 
 struct msph_tree_forall {
-	struct msph_tree_tpexpr	tp;
+	struct msph_tree_tpexpr	htpe;
 
-	struct msph_tree_ident	*ident;
+	struct msph_tree_ident	*id;
 	struct msph_tree_tpexpr	*inner;
+
+	struct msph_scope_decor	dec;
 };
 
 struct msph_tree_paren {
-	struct msph_tree_tpexpr	tp;
+	struct msph_tree_tpexpr	htpe;
 
 	struct msph_tree_tpexpr	*inner;
 };
 
 struct msph_tree_ident {
-	struct msph_tree tr;
+	struct msph_tree_text	htxt;
 
 	char str[MSPH_IDENT_LEN];
 	STAILQ_ENTRY(msph_tree_ident) entries;
-};
 
+	struct msph_nom_decor	dec;
+};
 
 
 struct msph_tree_root	*msph_tree_makeroot(struct msph_ctx *);
@@ -254,4 +264,7 @@ int	msph_tree_parse(struct msph_token_stream *, struct msph_tree_root *);
 
 ssize_t	msph_tree_fprint(FILE *, struct msph_tree *);
 
+#define T(ptr)			((struct msph_tree *)ptr)
+#define TXT(ptr)		((struct msph_tree_text *)ptr)
+
 #endif
diff --git a/include/spho/data.h b/include/spho/data.h
deleted file mode 100644
index 0cd02c8..0000000
--- a/include/spho/data.h
+++ /dev/null
@@ -1,12 +0,0 @@
-#ifndef _SPHO_DATA_H
-#define _SPHO_DATA_H
-
-struct spho_nom {
-	char			s[128];
-	SLIST_ENTRY(spho_nom)	next;
-};
-
-SLIST_HEAD(spho_nom_l, spho_nom);
-
-
-#endif /* _SPHO_DATA_H */
diff --git a/include/spho/err.h b/include/spho/err.h
index ffde4b0..e9bad83 100644
--- a/include/spho/err.h
+++ b/include/spho/err.h
@@ -12,7 +12,8 @@
 #define SPHO_ERR_INTERNAL	0x010001
 #define SPHO_ERR_TOOBIG		0x010002
 #define SPHO_ERR_ARGINVAL	0x010003
-#define SPHO_ERR_NAMEINUSE	0x010004
+#define SPHO_ERR_NOM_INUSE	0x020001
+#define SPHO_ERR_NOM_NOTINSCOPE	0x020002
 
 #define SPHO_ERR_IS_SYSERR(err)		(SPHO_ERR_SYS == err)
 
diff --git a/include/spho/parse.h b/include/spho/parse.h
deleted file mode 100644
index f534f68..0000000
--- a/include/spho/parse.h
+++ /dev/null
@@ -1,7 +0,0 @@
-#ifndef _SPHO_PARSE_H
-#define _SPHO_PARSE_H
-
-
-
-
-#endif
\ No newline at end of file
diff --git a/include/spho/scope.h b/include/spho/scope.h
index e0d62ff..843b554 100644
--- a/include/spho/scope.h
+++ b/include/spho/scope.h
@@ -1,7 +1,118 @@
 #ifndef _SPHO_SCOPE_H
 #define _SPHO_SCOPE_H
 
-#include "spho/data.h"
+#include <sys/queue.h>
+
+#include <stdlib.h>
+
+#define SPHO_NOM_LEN	128
+
+struct spho_nom {
+	char			s[SPHO_NOM_LEN];
+	SLIST_ENTRY(spho_nom)	next;
+};
+
+SLIST_HEAD(spho_nom_l, spho_nom);
+
+#define TP_KONST_KEY_TRUE	0x43445 /* don't change!!!!! */
+#define TP_KONST_KEY_FALSE	0x66a57 /* don't change!1! */
+
+
+struct spho_var {
+	struct spho_nom		nom;
+
+	STAILQ_ENTRY(spho_var)	next;
+};
+
+STAILQ_HEAD(spho_var_l, spho_var);
+
+struct spho_bind {
+	struct spho_nom		nom;
+	struct spho_tpop	*op;
+};
+
+struct spho_tpop {
+	struct spho_var_l	params;
+	struct spho_tp		*def;
+};
+
+struct spho_rec {
+	struct spho_nom		mnom;
+	struct spho_tp		*tp;
+};
+
+/* type data */
+struct tp_binop_data {
+	struct spho_tp		*left;
+	struct spho_tp		*right;
+};
+
+struct tp_unop_data {
+	struct spho_tp		*operand;
+};
+
+struct tp_binding_data {
+	struct spho_nom		*nom;
+	struct spho_tp		*bound;
+};
+
+struct tp_nom_data {
+	struct spho_nom		*nom;
+};
+
+struct tp_appl_data {
+	struct spho_nom		*nom;
+	struct spho_tp_l	*args;
+};
+
+struct tp_konst_data {
+	int		key;
+	const char	*str;
+};
+
+extern const struct tp_konst_data tp_konst_true;
+extern const struct tp_konst_data tp_konst_false;
+
+#define SPHO_K_TRUE	(&tp_konst_true)
+#define SPHO_K_FALSE	(&tp_konst_false)
+
+/* type data union */
+union tp_data {
+	struct tp_binop_data	binop;
+	struct tp_unop_data	unop;
+	struct tp_binding_data	bind;
+	struct tp_appl_data	appl;
+	struct tp_nom_data	nom;
+	struct tp_konst_data	konst;
+};
+
+/* sappho type */
+struct spho_tp {
+	struct spho_scope	*sc;
+
+	int			form;
+	union tp_data		d;
+
+	STAILQ_ENTRY(spho_tp)	entries;
+};
+
+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 {
+	struct spho_tp	tp;
+
+	TAILQ_ENTRY(spho_tp_alloc)	allocs;
+};
+
+TAILQ_HEAD(spho_tp_alloc_l, spho_tp_alloc);
+
 
 SLIST_HEAD(spho_scope_l, spho_scope);
 
@@ -11,6 +122,7 @@ struct spho_scope {
 
 	struct spho_scope_l	subs;
 	struct spho_nom_l	noms;
+	struct spho_tp_alloc_l	tps;
 
 	SLIST_ENTRY(spho_scope)	next;
 };
@@ -24,11 +136,13 @@ void	spho_scope_term(struct spho_scope *);
 struct spho_scope	*spho_scope_global(struct spho_ctx *);
 struct spho_scope	*spho_scope_create(struct spho_scope *);
 
+
 void spho_scope_destroy(struct spho_scope *);
 
 struct spho_nom	*spho_scope_nom_add(struct spho_scope *, const char *, size_t);
 int		spho_scope_nom_get(struct spho_scope *, const char *, size_t,
 		    struct spho_nom **);
-// int		spho_scope_nom_del(struct spho_nom *);
+int		spho_scope_nom_lookup(struct spho_scope *, const char *, size_t,
+		    struct spho_nom **);
 
 #endif /* _SPHO_SCOPE_H */
diff --git a/include/spho/tp.h b/include/spho/tp.h
index fdbf8bf..5395d76 100644
--- a/include/spho/tp.h
+++ b/include/spho/tp.h
@@ -1,160 +1,55 @@
 #ifndef _SPHO_TP_H
 #define _SPHO_TP_H
 
-/* base defs */
-
-#define SPHO_KONST_S_SZ		128
-#define SPHO_KONST_K_TRUE	0x43445 /* don't change!!!!! */
-#define SPHO_KONST_K_FALSE	0x66a57 /* don't change!1! */
-
-struct spho_konst {
-	const char	*s;
-	int		k;
-};
-
-const struct spho_konst SPHO_K_TRUE_V = { "True", SPHO_KONST_K_TRUE };
-const struct spho_konst SPHO_K_FALSE_V = { "False", SPHO_KONST_K_FALSE };
-
-#define SPHO_K_TRUE	(&SPHO_K_TRUE_V)
-#define SPHO_K_FALSE	(&SPHO_K_FALSE_V)
-
-
-struct spho_var {
-	struct spho_nom		nom;
-
-	STAILQ_ENTRY(spho_var)	next;
-};
-
-STAILQ_HEAD(spho_var_l, spho_var);
-
-struct spho_bind {
-	struct spho_nom		nom;
-	struct spho_tpop	*op;
-};
-
-struct spho_tpop {
-	struct spho_var_l	params;
-	struct spho_tp		*def;
-};
-
-struct spho_rec {
-	struct spho_nom		mnom;
-	struct spho_tp		*tp;
-};
-
-/* type data */
-struct tp_bin_data {
-	struct spho_tp		*left;
-	struct spho_tp		*right;
-};
-
-struct tp_box_data {
-	struct spho_tp *inr;
-};
-
-struct tp_forall_data {
-	struct spho_var		*var;
-	struct spho_tp		*inr;
-};
-
-struct tp_bappl_data {
-	struct spho_bind	*bind;
-	struct spho_tp_l	*args;
-};
-
-struct tp_konst_data {
-	const struct spho_konst	*k;
-};
-
-struct tp_var_data {
-	struct spho_var		*v;
-};
-
-struct tp_nominal_data {
-	struct spho_nom		*n;
-};
-
-struct tp_record_data {
-	struct spho_rec		*r;
-};
-
-/* type data union */
-union tp_data {
-	struct tp_bin_data	binop;
-	struct tp_box_data	box;
-	struct tp_forall_data	fa;
-	struct tp_bappl_data	bappl;
-	struct tp_konst_data	konst;
-	struct tp_var_data	var;
-	struct tp_nominal_data	nom; // XXX
-	struct tp_record_data	rec;
-};
+#include "spho/scope.h"
 
 #define SPHO_TP_FORM_UNKNOWN	0x00
 
-#define SPHO_TP_FORM_DISJ	0x10
-#define SPHO_TP_FORM_CONJ	0x11
+#define SPHO_TP_FORM_CONJ	0x10
+#define SPHO_TP_FORM_DISJ	0x11
 #define SPHO_TP_FORM_IMPL	0x12
-#define SPHO_TP_FORM_BOX	0x13
-#define SPHO_TP_FORM_ARROW	0x14
+#define SPHO_TP_FORM_ARROW	0x13
+#define SPHO_TP_FORM_BOX	0x14
 #define SPHO_TP_FORM_FORALL	0x15
-#define SPHO_TP_FORM_BAPPL	0x16
+#define SPHO_TP_FORM_APPL	0x16
 
-#define SPHO_TP_FORM_FALSE	0x20
-#define SPHO_TP_FORM_TRUE	0x21
-#define SPHO_TP_FORM_VAR	0x22
+#define SPHO_TP_FORM_TRUE	0x20
+#define SPHO_TP_FORM_FALSE	0x21
 #define SPHO_TP_FORM_NOM	0x23
 
-#define SPHO_TP_FORM_REC	0x23
+#define SPHO_TP_FORM_MEMBER	0x24
 
 // #define SPHO_TP_FORM_SUB	0x96
 
-#define SPHO_TP_FORM_IS_VALID(f) \
-	(f) >= SPHO_TP_FORM_DISJ && (f) <= SPHO_TP_FORM_BAPPL || \
-	(f) >= SPHO_TP_FORM_FALSE && (f) <= SPHO_TP_FORM_NOM  || \
-	(f) == SPHO_TP_FORM_REC
-
-/* sappho type */
-struct spho_tp {
-	struct spho_scope	*sc;
-
-	int			form;
-	union tp_data		data;
-
-	STAILQ_ENTRY(spho_tp)	next;
-};
-
-STAILQ_HEAD(spho_tp_l, spho_tp);
-
-
 #define SPHO_TP_ERR(tp, err)	SPHO_ERR((tp)->sc->ctx, (err))
 
-struct spho_var	*spho_var_create(struct spho_scope *, char *, size_t);
-struct spho_var	*spho_var_get(struct spho_scope *, char *, size_t);
+//struct spho_var	*spho_var_create(struct spho_scope *, char *, size_t);
+//struct spho_var	*spho_var_get(struct spho_scope *, char *, size_t);
 
-//struct spho_tp	*spho_tp_create_disj(struct spho_scope *, struct spho_tp *,
-//		    struct spho_tp *, struct spho_tp *);
-//struct spho_tp	*spho_tp_create_conj(struct spho_scope *, struct spho_tp *,
-//		    struct spho_tp *, struct spho_tp *);
-//struct spho_tp	*spho_tp_create_impl(struct spho_scope *, struct spho_tp *,
-//		    struct spho_tp *, struct spho_tp *);
-//struct spho_tp	*spho_tp_create_box(struct spho_scope *, struct spho_tp *,
-//		    struct spho_tp *);
-//struct spho_tp	*spho_tp_create_arrow(struct spho_scope *, struct spho_tp *,
-//		    struct spho_tp *);
-//struct spho_tp	*spho_tp_create_forall(struct spho_scope *, struct spho_name *,
-//		    struct spho_tp *);
+struct spho_tp	*spho_tp_create_conj(struct spho_scope *, struct spho_tp *,
+		    struct spho_tp *);
+struct spho_tp	*spho_tp_create_disj(struct spho_scope *, struct spho_tp *,
+		    struct spho_tp *);
+struct spho_tp	*spho_tp_create_impl(struct spho_scope *, struct spho_tp *,
+		    struct spho_tp *);
+struct spho_tp	*spho_tp_create_arrow(struct spho_scope *, struct spho_tp *,
+		    struct spho_tp *);
+struct spho_tp	*spho_tp_create_box(struct spho_scope *, struct spho_tp *);
+struct spho_tp	*spho_tp_create_forall(struct spho_scope *, struct spho_nom *,
+		    struct spho_tp *);
+struct spho_tp	*spho_tp_create_true(struct spho_scope *);
+struct spho_tp	*spho_tp_create_false(struct spho_scope *);
+struct spho_tp	*spho_tp_create_name(struct spho_scope *,
+		    struct spho_nom *);
+struct spho_tp	*spho_tp_create_appl(struct spho_scope *, struct spho_nom *,
+		    struct spho_tp_l *);
+struct spho_tp	*spho_tp_create_member(struct spho_scope *, struct spho_nom *,
+		    struct spho_tp *);
 //struct spho_tp	*spho_tp_create_const(struct spho_scope *, struct spho_const *);
-//struct spho_tp	*spho_tp_create_nominal(struct spho_scope *,
-//		    struct spho_nom *);
-//struct spho_tp	*spho_tp_create_var(struct spho_scope *, struct spho_var *);
-//struct spho_tp	*spho_tp_create_record(struct spho_scope *, struct spho_rec *);
-//struct spho_tp	*spho_tp_create_sub(struct spho_scope *, struct spho_tp *,
+// struct spho_tp	*spho_tp_create_var(struct spho_scope *, struct spho_var *);
+// struct spho_tp	*spho_tp_create_sub(struct spho_scope *, struct spho_tp *,
 //		    struct spho_tp *);
 
-void	spho_tp_destroy(struct spho_tp*);
-
-void	spho_tp_free(struct spho_tp *);
-
+void	spho_tp_destroy(struct spho_tp *);
 
 #endif
diff --git a/src/msph/msph.c b/src/msph/msph.c
index edc2ed7..041bdff 100644
--- a/src/msph/msph.c
+++ b/src/msph/msph.c
@@ -5,12 +5,7 @@
 #include "msph/err.h"
 #include "msph/token.h"
 #include "msph/tree.h"
-
-#define PRINTERR(ctx) \
-	do { \
-		fprintf(stderr, "msph_err: %x (%d)\n", (ctx).err, \
-		    (ctx).err_info); \
-	} while (0)
+#include "msph/sphophi.h"
 
 struct msph_opts {
 	int		tokenize_only;
@@ -30,7 +25,6 @@ struct msph_opts {
 	"\t-t	- print tokenization\n" \
 	"\t-o	- output path\n"
 
-
 void
 print_usage(void)
 {
@@ -88,6 +82,8 @@ run(struct msph_opts *opts)
 	FILE *in, *out;
 
 	in = out = NULL;
+	s = NULL;
+	root = NULL;
 
 	msph_ctx_init(&ctx);
 
@@ -134,6 +130,9 @@ run(struct msph_opts *opts)
 	if (msph_tree_fprint(out, (struct msph_tree *)root) < 0)
 		goto err;
 
+	if (msph_sphophi(root) != 0)
+		goto err;
+
 exit:
 	if (msph_token_stream_close(s) == -1)
 		goto err;
@@ -141,7 +140,13 @@ exit:
 	return (0);
 
 err:
-	PRINTERR(ctx);
+	if (root != NULL && ctx.err == MSPH_ERR_SPHOPHI) {
+		fprintf(stderr, "ERROR:%s\n",
+		    spho_ctx_strerror(ctx.spho));
+	} else {
+		fprintf(stderr, "ERROR:msph_err: %x (%d)\n", (ctx).err,
+		    (ctx).err_info);
+	}
 
 	if (in)
 		fclose(in);
@@ -149,3 +154,14 @@ err:
 		fclose(out);
 	return (-1);
 }
+
+
+void
+msph_ctx_init(struct msph_ctx *ctx)
+{
+	ctx->err = 0;
+	ctx->err_info = 0;
+
+	ctx->spho = NULL;
+}
+
diff --git a/src/msph/sphophi.c b/src/msph/sphophi.c
new file mode 100644
index 0000000..8e39263
--- /dev/null
+++ b/src/msph/sphophi.c
@@ -0,0 +1,1136 @@
+#include <sys/queue.h>
+
+#include "spho/spho.h"
+#include "spho/tp.h"
+
+#include "msph/sphophi.h"
+
+typedef int (*msph_tree_sphophi_f)(struct spho_scope *, struct msph_tree *);
+
+static int	msph_tree_sphophi_decor_scope(struct spho_scope *,
+		    struct msph_tree *);
+static int	msph_tree_sphophi_decor_nom_lookup(struct spho_scope *,
+		    struct msph_tree *);
+static int	msph_tree_sphophi_decor_tp(struct spho_scope *,
+		    struct msph_tree *);
+
+/* foreach_pre: top down foreach */
+static int	msph_sphophi_foreach_pre(msph_tree_sphophi_f,
+		    struct msph_tree_root *);
+static int	msph_sphophi_foreach_pre_unit(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_unit *);
+static int	msph_sphophi_foreach_pre_body(msph_tree_sphophi_f, 
+		    struct spho_scope *, struct msph_tree_body *);
+static int	msph_sphophi_foreach_pre_dir(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_dir *);
+static int	msph_sphophi_foreach_pre_assert(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_assert *);
+static int	msph_sphophi_foreach_pre_membdecl(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_membdecl *);
+static int	msph_sphophi_foreach_pre_tpdef(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_tpdef *);
+static int	msph_sphophi_foreach_pre_nomindecl(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_nomindecl *);
+static int	msph_sphophi_foreach_pre_tpexpr(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_tpexpr *);
+static int	msph_sphophi_foreach_pre_true(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_true *);
+static int	msph_sphophi_foreach_pre_false(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_false *);
+static int	msph_sphophi_foreach_pre_name(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_name *);
+static int	msph_sphophi_foreach_pre_appl(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_appl *);
+static int	msph_sphophi_foreach_pre_trait(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_trait *);
+static int	msph_sphophi_foreach_pre_conj(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_conj *);
+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_arrow(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_arrow *);
+static int	msph_sphophi_foreach_pre_box(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_box *);
+static int	msph_sphophi_foreach_pre_forall(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_forall *);
+static int	msph_sphophi_foreach_pre_paren(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_paren *);
+static int	msph_sphophi_foreach_pre_ident(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_ident *);
+
+/* foreach_post: bottom up foreach */
+static int	msph_sphophi_foreach_post(msph_tree_sphophi_f,
+		    struct msph_tree_root *);
+static int	msph_sphophi_foreach_post_unit(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_unit *);
+static int	msph_sphophi_foreach_post_body(msph_tree_sphophi_f, 
+		    struct spho_scope *, struct msph_tree_body *);
+static int	msph_sphophi_foreach_post_dir(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_dir *);
+static int	msph_sphophi_foreach_post_assert(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_assert *);
+static int	msph_sphophi_foreach_post_membdecl(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_membdecl *);
+static int	msph_sphophi_foreach_post_tpdef(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_tpdef *);
+static int	msph_sphophi_foreach_post_nomindecl(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_nomindecl *);
+static int	msph_sphophi_foreach_post_tpexpr(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_tpexpr *);
+static int	msph_sphophi_foreach_post_true(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_true *);
+static int	msph_sphophi_foreach_post_false(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_false *);
+static int	msph_sphophi_foreach_post_name(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_name *);
+static int	msph_sphophi_foreach_post_appl(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_appl *);
+static int	msph_sphophi_foreach_post_trait(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_trait *);
+static int	msph_sphophi_foreach_post_conj(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_conj *);
+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_arrow(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_arrow *);
+static int	msph_sphophi_foreach_post_box(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_box *);
+static int	msph_sphophi_foreach_post_forall(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_forall *);
+static int	msph_sphophi_foreach_post_paren(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_paren *);
+static int	msph_sphophi_foreach_post_ident(msph_tree_sphophi_f,
+		    struct spho_scope *, struct msph_tree_ident *);
+
+int msph_sphophi_init(struct msph_tree_root *root)
+{
+	if ((root->ctx->spho = spho_ctx_create()) == NULL) {
+		MSPH_ERR(root->ctx, MSPH_ERR_SYS);
+		return (-1);
+	}
+
+	return (0);
+}
+
+int
+msph_sphophi_scope(struct msph_tree_root *root)
+{
+	return (msph_sphophi_foreach_pre(msph_tree_sphophi_decor_scope, root));
+}
+
+int
+msph_sphophi_nom_lookup(struct msph_tree_root *root)
+{
+	return (msph_sphophi_foreach_pre(msph_tree_sphophi_decor_nom_lookup,
+		    root));
+}
+
+int
+msph_sphophi_tp(struct msph_tree_root *root)
+{
+	return (msph_sphophi_foreach_post(msph_tree_sphophi_decor_tp, root));
+}
+
+int msph_sphophi(struct msph_tree_root *root)
+{
+	int ret;
+
+	if ((ret = msph_sphophi_init(root)) != 0)
+		return (ret);
+	if ((ret = msph_sphophi_scope(root)) != 0)
+		return (ret);
+	if ((ret = msph_sphophi_nom_lookup(root)) != 0)
+		return (ret);
+	if ((ret = msph_sphophi_tp(root)) != 0)
+		return (ret);
+
+	return (ret);
+}
+
+
+#define IS_BINDING(tree)	(((tree)->type == MSPH_TREE_TPDEF)	|| \
+				 ((tree)->type == MSPH_TREE_NOMINDECL)	|| \
+				 ((tree)->type == MSPH_TREE_MEMBDECL)	|| \
+				 ((tree)->type == MSPH_TREE_FORALL))
+#define IS_TPEXPR(tree)		(((tree)->type & MSPH_TREE_TPEXPR))
+
+static int
+msph_tree_sphophi_decor_scope(struct spho_scope *sc, struct msph_tree *tree)
+{
+	int ret;
+	struct msph_tree_unit *unit;
+	struct msph_tree_trait *trait;
+	struct msph_tree_forall *forall;
+	struct msph_tree_ident *ident;
+
+	ret = 0;
+
+	switch (tree->type) {
+	case MSPH_TREE_UNIT:
+		unit = (struct msph_tree_unit *)tree;
+		if ((unit->dec.sc = spho_scope_create(sc)) == NULL)
+			ret = -1;
+		break;
+	case MSPH_TREE_TRAIT:
+		trait = (struct msph_tree_trait *)tree;
+		if ((trait->dec.sc = spho_scope_create(sc)) == NULL)
+			ret = -1;
+		break;
+	case MSPH_TREE_FORALL:
+		forall = (struct msph_tree_forall *)tree;
+		if ((forall->dec.sc = spho_scope_create(sc)) == NULL)
+			ret = -1;
+		break;
+	case MSPH_TREE_IDENT:
+		if (! IS_BINDING(tree->parent))
+			break;
+		ident = (struct msph_tree_ident *)tree;
+		if ((ident->dec.nom = spho_scope_nom_add(sc, ident->str,
+			    sizeof(ident->str))) == NULL)
+			ret = -1;
+		break;
+	default:
+		break;
+	}
+
+	return (ret);
+}
+
+static int
+msph_tree_sphophi_decor_nom_lookup(struct spho_scope *sc,
+    struct msph_tree *tree)
+{
+	int ret;
+	struct msph_tree_ident *ident;
+
+	ret = 0;
+
+	switch (tree->type) {
+	case MSPH_TREE_IDENT:
+		if (tree->parent->type != MSPH_TREE_NAME)
+			break;
+		ident = (struct msph_tree_ident *)tree;
+		if ((ret = spho_scope_nom_lookup(sc, ident->str,
+			    sizeof(ident->str), &ident->dec.nom)) != 0)
+			break;
+		if (ident->dec.nom == NULL)
+			ret = -1;
+		break;
+	default:
+		break;
+	}
+
+	return (ret);
+}
+
+#define TP(ptr)		((ptr)->dec.tp)
+#define NOM(ptr)	((ptr)->dec.nom)
+
+static int
+msph_tree_sphophi_decor_tp(struct spho_scope *sc, struct msph_tree *tree)
+{
+	int ret;
+	struct msph_tree_tpexpr *tpexpr, *tpexpr_i;
+	struct msph_tree_conj *conj;
+	struct msph_tree_disj *disj;
+	struct msph_tree_impl *impl;
+	struct msph_tree_arrow *arrow;
+	struct msph_tree_name *name;
+	struct msph_tree_appl *appl;
+	struct msph_tree_box *box;
+	struct msph_tree_forall *forall;
+	struct msph_tree_paren *paren;
+	struct msph_tree_trait *trait;
+	struct msph_tree_dir *dir;
+	struct msph_tree_membdecl *membd;
+
+	struct spho_tp_l *tps;
+	struct spho_tp *tp, *tp_memb;
+
+	ret = -1;
+	tps = NULL;
+	tp = tp_memb = NULL;
+	dir = NULL;
+	membd = NULL;
+
+	if (! (tree->type & MSPH_TREE_TPEXPR))
+		return (0);
+
+	tpexpr = (struct msph_tree_tpexpr *)tree;
+
+	switch (tree->type) {
+	case MSPH_TREE_CONJ:
+		conj = (struct msph_tree_conj *)tree;
+		if ((TP(&conj->htpe) = spho_tp_create_conj(sc, TP(conj->ltp),
+		    TP(conj->rtp))) == NULL)
+			goto cleanup;
+		break;
+	case MSPH_TREE_DISJ:
+		disj = (struct msph_tree_disj *)tree;
+		if ((TP(&disj->htpe) = spho_tp_create_conj(sc, TP(disj->ltp),
+		    TP(disj->rtp))) == NULL)
+			goto cleanup;
+		break;
+	case MSPH_TREE_IMPL:
+		impl = (struct msph_tree_impl *)tree;
+		if ((TP(&impl->htpe) = spho_tp_create_conj(sc, TP(impl->ltp),
+		    TP(impl->rtp))) == NULL)
+			goto cleanup;
+		break;
+	case MSPH_TREE_ARROW:
+		arrow = (struct msph_tree_arrow *)tree;
+		if ((TP(&arrow->htpe) = spho_tp_create_conj(sc, TP(arrow->ltp),
+		    TP(arrow->rtp))) == NULL)
+			goto cleanup;
+		break;
+	case MSPH_TREE_NAME:
+		name = (struct msph_tree_name *)tree;
+		if ((TP(&name->htpe) = spho_tp_create_name(sc, NOM(name->id)))
+		    == NULL)
+			goto cleanup;
+		break;
+	case MSPH_TREE_APPL:
+		appl = (struct msph_tree_appl *)tree;
+		if ((tps = malloc(sizeof(*tps))) == NULL) {
+			SPHO_SC_ERR(sc, SPHO_ERR_SYS);
+			goto cleanup;
+		}
+		STAILQ_INIT(tps);
+		STAILQ_FOREACH(tpexpr_i, &appl->head, entries) {
+			STAILQ_INSERT_TAIL(tps, tpexpr_i->dec.tp, entries);
+		}
+		if ((TP(&appl->htpe) = spho_tp_create_appl(sc, NOM(appl->id),
+			    tps)) == NULL)
+			goto cleanup;
+		tps = NULL;
+		break;
+	case MSPH_TREE_TRUE:
+		if ((TP(tpexpr) = spho_tp_create_true(sc)) == NULL)
+			goto cleanup;
+		break;
+	case MSPH_TREE_FALSE:
+		if ((TP(tpexpr) = spho_tp_create_false(sc)) == NULL)
+			goto cleanup;
+		break;
+	case MSPH_TREE_FORALL:
+		forall = (struct msph_tree_forall *)tree;
+		if ((TP(&forall->htpe) = spho_tp_create_forall(sc,
+			    NOM(forall->id), TP(forall->inner))) == NULL)
+			goto cleanup;
+		break;
+	case MSPH_TREE_BOX:
+		box = (struct msph_tree_box *)tree;
+		if ((TP(&box->htpe) = spho_tp_create_box(sc, TP(box->inner)))
+		    == NULL)
+			goto cleanup;
+		break;
+	case MSPH_TREE_PAREN:
+		paren = (struct msph_tree_paren *)tree;
+		if ((TP(&paren->htpe) = TP(paren->inner)) == NULL)
+			goto cleanup;
+		break;
+	case MSPH_TREE_TRAIT:
+		trait = (struct msph_tree_trait *)tree;
+
+		STAILQ_FOREACH(dir, &trait->body->head, entries) {
+			if (T(dir)->type != MSPH_TREE_MEMBDECL)
+				continue;
+			membd = (struct msph_tree_membdecl *)dir;
+			// TODO check that we make sure to dealloc when
+			// spho has stabilized a bit
+			if ((tp_memb = spho_tp_create_member(sc, membd->id->dec.nom,
+			    membd->tp->dec.tp)) == NULL)
+				goto cleanup;
+			if (tp == NULL) {
+				tp = tp_memb;
+			} else {
+				if ((tp = spho_tp_create_conj(sc, tp, tp_memb))
+				    == NULL)
+					goto cleanup;
+			}
+			trait->htpe.dec.tp = tp;
+		}
+		break;
+	default:
+		SPHO_ASSERT(0);
+		break;
+	}
+
+	ret = 0;
+
+cleanup:
+	if (tps != NULL)
+		free(tps);
+
+	return (ret);
+}
+
+/* foreach pre: top down foreach node */
+static int
+msph_sphophi_foreach_pre(msph_tree_sphophi_f f, struct msph_tree_root *root)
+{
+	int ret;
+	struct spho_scope *sc;
+	struct msph_tree_unit *unit;
+
+	if (root == NULL || root->ctx == NULL)
+		return (-1);
+
+	if (root->ctx->spho == NULL) {
+		MSPH_ERR(root->ctx, MSPH_ERR_TYPE_INVAL);
+		return (-1);
+	}
+
+	sc = spho_scope_global(root->ctx->spho);
+
+	if ((ret = f(sc, T(root))) != 0) {
+		goto err;
+	}
+
+	ret = 0;
+	STAILQ_FOREACH(unit, &root->head, entries) {
+		if ((ret = msph_sphophi_foreach_pre_unit(f, sc, unit)) != 0)
+			goto err;
+	}
+
+	return (ret);
+err:
+	MSPH_ERR(root->ctx, MSPH_ERR_SPHOPHI);
+	return (ret);
+}
+
+static int
+msph_sphophi_foreach_pre_unit(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_unit *unit)
+{
+	int ret;
+
+	if ((ret = f(sc, T(unit))) != 0)
+		return (ret);
+
+	sc = GET_SCOPE(unit);
+
+	return (msph_sphophi_foreach_pre_body(f, sc, unit->body));
+}
+
+static int
+msph_sphophi_foreach_pre_body(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_body *body)
+{
+	int ret;
+	struct msph_tree_dir *dir;
+
+	if ((ret = f(sc, T(body))) != 0)
+		return (ret);
+
+	ret = 0;
+	STAILQ_FOREACH(dir, &body->head, entries) {
+		if ((ret = msph_sphophi_foreach_pre_dir(f, sc, dir)) != 0)
+			return (ret);
+	}
+
+	return (ret);
+}
+
+static int
+msph_sphophi_foreach_pre_dir(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_dir *dir)
+{
+	int ret;
+
+	ret = -1;
+	switch (dir->htxt.htr.type) {
+	case MSPH_TREE_TPDEF:
+		ret = msph_sphophi_foreach_pre_tpdef(f, sc,
+		    (struct msph_tree_tpdef *)dir);
+		break;
+	case MSPH_TREE_MEMBDECL:
+		ret = msph_sphophi_foreach_pre_membdecl(f, sc,
+		    (struct msph_tree_membdecl *)dir);
+		break;
+	case MSPH_TREE_NOMINDECL:
+		ret = msph_sphophi_foreach_pre_nomindecl(f, sc,
+		    (struct msph_tree_nomindecl *)dir);
+		break;
+	case MSPH_TREE_ASSERT:
+		ret = msph_sphophi_foreach_pre_assert(f, sc,
+		    (struct msph_tree_assert *)dir);
+		break;
+	default:
+		SPHO_ASSERT(0);
+		break;
+	}
+
+	return (ret);
+}
+
+static int
+msph_sphophi_foreach_pre_tpdef(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_tpdef *tpdef)
+{
+	int ret;
+
+	if ((ret = f(sc, T(tpdef))) != 0)
+		return (ret);
+
+	if ((ret = msph_sphophi_foreach_pre_ident(f, sc, tpdef->id)) != 0)
+		return (ret);
+
+	return (msph_sphophi_foreach_pre_tpexpr(f, sc, tpdef->tp));
+}
+
+static int
+msph_sphophi_foreach_pre_nomindecl(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_nomindecl *nomd)
+{
+	int ret;
+
+	if ((ret = f(sc, T(nomd))) != 0)
+		return (ret);
+
+	return (msph_sphophi_foreach_pre_ident(f, sc, nomd->id));
+}
+
+static int
+msph_sphophi_foreach_pre_membdecl(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_membdecl *membd)
+{
+	int ret;
+
+	if ((ret = f(sc, T(membd))) != 0)
+		return (ret);
+
+	if (msph_sphophi_foreach_pre_ident(f, sc, membd->id) != 0)
+		return (ret);
+	if (msph_sphophi_foreach_pre_tpexpr(f, sc, membd->tp) != 0)
+		return (ret);
+
+	return (0);
+}
+
+static int
+msph_sphophi_foreach_pre_assert(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_assert *ass)
+{
+	int ret;
+
+	if ((ret = f(sc, T(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)
+		return (ret);
+
+	return (ret);
+}
+
+static int
+msph_sphophi_foreach_pre_ident(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_ident *ident)
+{
+	return (f(sc, T(ident)));
+}
+
+static int
+msph_sphophi_foreach_pre_tpexpr(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_tpexpr *tpexpr)
+{
+	int ret;
+
+	ret = -1;
+
+	switch (tpexpr->htxt.htr.type) {
+	case MSPH_TREE_CONJ:
+		ret = msph_sphophi_foreach_pre_conj(f, sc,
+		    (struct msph_tree_conj *)tpexpr);
+		break;
+	case MSPH_TREE_DISJ:
+		ret = msph_sphophi_foreach_pre_disj(f, sc,
+		    (struct msph_tree_disj *)tpexpr);
+		break;
+	case MSPH_TREE_IMPL:
+		ret = msph_sphophi_foreach_pre_impl(f, sc,
+		    (struct msph_tree_impl *)tpexpr);
+		break;
+	case MSPH_TREE_ARROW:
+		ret = msph_sphophi_foreach_pre_arrow(f, sc,
+		    (struct msph_tree_arrow *)tpexpr);
+		break;
+	case MSPH_TREE_NAME:
+		ret = msph_sphophi_foreach_pre_name(f, sc,
+		    (struct msph_tree_name *)tpexpr);
+		break;
+	case MSPH_TREE_APPL:
+		ret = msph_sphophi_foreach_pre_appl(f, sc,
+		    (struct msph_tree_appl *)tpexpr);
+		break;
+	case MSPH_TREE_TRAIT:
+		ret = msph_sphophi_foreach_pre_trait(f, sc,
+		    (struct msph_tree_trait *)tpexpr);
+		break;
+	case MSPH_TREE_BOX:
+		ret = msph_sphophi_foreach_pre_box(f, sc,
+		    (struct msph_tree_box *)tpexpr);
+		break;
+	case MSPH_TREE_FORALL:
+		ret = msph_sphophi_foreach_pre_forall(f, sc,
+		    (struct msph_tree_forall *)tpexpr);
+		break;
+	case MSPH_TREE_PAREN:
+		ret = msph_sphophi_foreach_pre_paren(f, sc,
+		    (struct msph_tree_paren *)tpexpr);
+		break;
+	case MSPH_TREE_TRUE:
+		ret = msph_sphophi_foreach_pre_true(f, sc,
+		    (struct msph_tree_true *)tpexpr);
+		break;
+	case MSPH_TREE_FALSE:
+		ret = msph_sphophi_foreach_pre_false(f, sc,
+		    (struct msph_tree_false *)tpexpr);
+		break;
+	default:
+		SPHO_ASSERT(0);
+		break;
+	}
+
+	return (ret);
+}
+
+static int
+msph_sphophi_foreach_pre_conj(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_conj *conj)
+{
+	int ret;
+
+	if ((ret = f(sc, T(conj))) != 0)
+		return (ret);
+
+	if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, conj->ltp)) != 0)
+		return (ret);
+
+	return (msph_sphophi_foreach_pre_tpexpr(f, sc, conj->rtp));
+}
+
+static int
+msph_sphophi_foreach_pre_disj(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_disj *disj)
+{
+	int ret;
+
+	if ((ret = f(sc, T(disj))) != 0)
+		return (ret);
+	if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, disj->ltp)) != 0)
+		return (ret);
+	return (msph_sphophi_foreach_pre_tpexpr(f, sc, disj->rtp));
+}
+
+static int
+msph_sphophi_foreach_pre_impl(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_impl *impl)
+{
+	int ret;
+
+	if ((ret = f(sc, T(impl))) != 0)
+		return (ret);
+
+	if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, impl->ltp)) != 0)
+		return (ret);
+	return (msph_sphophi_foreach_pre_tpexpr(f, sc, impl->rtp));
+}
+
+static int
+msph_sphophi_foreach_pre_arrow(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_arrow *arrow)
+{
+	int ret;
+
+	if ((ret = f(sc, T(arrow))) != 0)
+		return (ret);
+
+	if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, arrow->ltp)) != 0)
+		return (ret);
+	return (msph_sphophi_foreach_pre_tpexpr(f, sc, arrow->rtp));
+}
+
+static int
+msph_sphophi_foreach_pre_name(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_name *name)
+{
+	int ret;
+
+	if ((ret = f(sc, T(name))) != 0)
+		return (ret);
+
+	return (msph_sphophi_foreach_pre_ident(f, sc, name->id));
+}
+
+static int
+msph_sphophi_foreach_pre_appl(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_appl *appl)
+{
+	int ret;
+	struct msph_tree_tpexpr *tp;
+
+	if ((ret = f(sc, T(appl))) != 0)
+		return (ret);
+
+	ret = 0;
+	STAILQ_FOREACH(tp, &appl->head, entries) {
+		if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, tp)) != 0)
+			return (ret);
+	}
+
+	return (ret);
+}
+
+static int
+msph_sphophi_foreach_pre_trait(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_trait *trait)
+{
+	int ret;
+	if ((ret = f(sc, T(trait))) != 0)
+		return (ret);
+
+	sc = GET_SCOPE(trait);
+
+	return (msph_sphophi_foreach_pre_body(f, sc, trait->body));
+}
+
+static int
+msph_sphophi_foreach_pre_box(msph_tree_sphophi_f f,struct spho_scope *sc,
+    struct msph_tree_box *box)
+{
+	int ret;
+
+	if ((ret = f(sc, T(box))) != 0)
+		return (ret);
+
+	return (msph_sphophi_foreach_pre_tpexpr(f, sc, box->inner));
+}
+
+static int
+msph_sphophi_foreach_pre_forall(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_forall *forall)
+{
+	int ret;
+	
+	if ((ret = f(sc, T(forall))) != 0)
+		return (ret);
+
+	sc = GET_SCOPE(forall);
+
+	return (msph_sphophi_foreach_pre_tpexpr(f, sc, forall->inner));
+}
+
+static int
+msph_sphophi_foreach_pre_paren(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_paren *paren)
+{
+	int ret;
+
+	if ((ret = f(sc, T(paren))) != 0)
+		return (ret);
+
+	return (msph_sphophi_foreach_pre_tpexpr(f, sc, paren->inner));
+}
+
+static int
+msph_sphophi_foreach_pre_true(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_true *tru)
+{
+	return (f(sc, T(tru)));
+}
+
+static int
+msph_sphophi_foreach_pre_false(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_false *fls)
+{
+	return (f(sc, T(fls)));
+}
+
+
+/* foreach post: bottom up foreach */
+static int
+msph_sphophi_foreach_post(msph_tree_sphophi_f f, struct msph_tree_root *root)
+{
+	int ret;
+	struct spho_scope *sc;
+	struct msph_tree_unit *unit;
+
+	if (root == NULL || root->ctx == NULL)
+		return (-1);
+
+	if (root->ctx->spho == NULL) {
+		MSPH_ERR(root->ctx, MSPH_ERR_TYPE_INVAL);
+		return (-1);
+	}
+
+	sc = spho_scope_global(root->ctx->spho);
+
+	ret = 0;
+	STAILQ_FOREACH(unit, &root->head, entries) {
+		if ((ret = msph_sphophi_foreach_post_unit(f, sc, unit)) != 0)
+			goto err;
+	}
+
+	if ((ret = f(sc, T(root))) != 0)
+		goto err;
+
+	return (ret);
+err:
+	MSPH_ERR(root->ctx, MSPH_ERR_SPHOPHI);
+	return (ret);
+}
+
+static int
+msph_sphophi_foreach_post_unit(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_unit *unit)
+{
+	int ret;
+	struct spho_scope *inner_sc;
+
+	inner_sc = GET_SCOPE(unit);
+
+	if ((ret = msph_sphophi_foreach_post_body(f, inner_sc, unit->body))
+	    != 0)
+		return (ret);
+
+	return (f(sc, T(unit)));
+}
+
+static int
+msph_sphophi_foreach_post_body(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_body *body)
+{
+	int ret;
+	struct msph_tree_dir *dir;
+
+	ret = 0;
+	STAILQ_FOREACH(dir, &body->head, entries) {
+		if ((ret = msph_sphophi_foreach_post_dir(f, sc, dir)) != 0)
+			return (ret);
+	}
+
+	return (f(sc, T(body)));
+}
+
+static int
+msph_sphophi_foreach_post_dir(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_dir *dir)
+{
+	int ret;
+
+	ret = -1;
+	switch (dir->htxt.htr.type) {
+	case MSPH_TREE_TPDEF:
+		ret = msph_sphophi_foreach_post_tpdef(f, sc,
+		    (struct msph_tree_tpdef *)dir);
+		break;
+	case MSPH_TREE_MEMBDECL:
+		ret = msph_sphophi_foreach_post_membdecl(f, sc,
+		    (struct msph_tree_membdecl *)dir);
+		break;
+	case MSPH_TREE_NOMINDECL:
+		ret = msph_sphophi_foreach_post_nomindecl(f, sc,
+		    (struct msph_tree_nomindecl *)dir);
+		break;
+	case MSPH_TREE_ASSERT:
+		ret = msph_sphophi_foreach_post_assert(f, sc,
+		    (struct msph_tree_assert *)dir);
+		break;
+	default:
+		SPHO_ASSERT(0);
+		break;
+	}
+
+	return (ret);
+}
+
+static int
+msph_sphophi_foreach_post_tpdef(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_tpdef *tpdef)
+{
+	int ret;
+
+	if ((ret = msph_sphophi_foreach_post_ident(f, sc, tpdef->id)) != 0)
+		return (ret);
+	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, tpdef->tp)) != 0)
+		return (ret);
+
+	return (f(sc, T(tpdef)));
+}
+
+static int
+msph_sphophi_foreach_post_nomindecl(msph_tree_sphophi_f f,
+    struct spho_scope *sc, struct msph_tree_nomindecl *nomd)
+{
+	int ret;
+
+	if ((ret = msph_sphophi_foreach_post_ident(f, sc, nomd->id)) != 0)
+		return (ret);
+
+	return (f(sc, T(nomd)));
+}
+
+static int
+msph_sphophi_foreach_post_membdecl(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_membdecl *membd)
+{
+	int ret;
+
+	if ((ret = msph_sphophi_foreach_post_ident(f, sc, membd->id)) != 0)
+		return (ret);
+	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, membd->tp)) != 0)
+		return (ret);
+
+	return (f(sc, T(membd)));
+}
+
+static int
+msph_sphophi_foreach_post_assert(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_assert *ass)
+{
+	int ret;
+
+	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, ass->ltp)) != 0)
+		return (ret);
+	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, ass->rtp)) != 0)
+		return (ret);
+
+	return (f(sc, T(ass)));
+}
+
+static int
+msph_sphophi_foreach_post_ident(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_ident *ident)
+{
+	return (f(sc, T(ident)));
+}
+
+static int
+msph_sphophi_foreach_post_tpexpr(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_tpexpr *tpexpr)
+{
+	int ret;
+
+	ret = -1;
+
+	switch (tpexpr->htxt.htr.type) {
+	case MSPH_TREE_CONJ:
+		ret = msph_sphophi_foreach_post_conj(f, sc,
+		    (struct msph_tree_conj *)tpexpr);
+		break;
+	case MSPH_TREE_DISJ:
+		ret = msph_sphophi_foreach_post_disj(f, sc,
+		    (struct msph_tree_disj *)tpexpr);
+		break;
+	case MSPH_TREE_IMPL:
+		ret = msph_sphophi_foreach_post_impl(f, sc,
+		    (struct msph_tree_impl *)tpexpr);
+		break;
+	case MSPH_TREE_ARROW:
+		ret = msph_sphophi_foreach_post_arrow(f, sc,
+		    (struct msph_tree_arrow *)tpexpr);
+		break;
+	case MSPH_TREE_NAME:
+		ret = msph_sphophi_foreach_post_name(f, sc,
+		    (struct msph_tree_name *)tpexpr);
+		break;
+	case MSPH_TREE_APPL:
+		ret = msph_sphophi_foreach_post_appl(f, sc,
+		    (struct msph_tree_appl *)tpexpr);
+		break;
+	case MSPH_TREE_TRAIT:
+		ret = msph_sphophi_foreach_post_trait(f, sc,
+		    (struct msph_tree_trait *)tpexpr);
+		break;
+	case MSPH_TREE_BOX:
+		ret = msph_sphophi_foreach_post_box(f, sc,
+		    (struct msph_tree_box *)tpexpr);
+		break;
+	case MSPH_TREE_FORALL:
+		ret = msph_sphophi_foreach_post_forall(f, sc,
+		    (struct msph_tree_forall *)tpexpr);
+		break;
+	case MSPH_TREE_PAREN:
+		ret = msph_sphophi_foreach_post_paren(f, sc,
+		    (struct msph_tree_paren *)tpexpr);
+		break;
+	case MSPH_TREE_TRUE:
+		ret = msph_sphophi_foreach_post_true(f, sc,
+		    (struct msph_tree_true *)tpexpr);
+		break;
+	case MSPH_TREE_FALSE:
+		ret = msph_sphophi_foreach_post_false(f, sc,
+		    (struct msph_tree_false *)tpexpr);
+		break;
+	default:
+		SPHO_ASSERT(0);
+		break;
+	}
+
+	return (ret);
+}
+
+static int
+msph_sphophi_foreach_post_conj(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_conj *conj)
+{
+	int ret;
+
+	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, conj->ltp)) != 0)
+		return (ret);
+	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, conj->rtp)) != 0)
+		return (ret);
+
+	return (f(sc, T(conj)));
+
+}
+
+static int
+msph_sphophi_foreach_post_disj(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_disj *disj)
+{
+	int ret;
+
+	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, disj->ltp)) != 0)
+		return (ret);
+	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, disj->rtp)) != 0)
+		return (ret);
+
+	return (f(sc, T(disj)));
+}
+
+static int
+msph_sphophi_foreach_post_impl(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_impl *impl)
+{
+	int ret;
+
+	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, impl->ltp)) != 0)
+		return (ret);
+	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, impl->rtp)) != 0)
+		return (ret);
+
+	return (f(sc, T(impl)));
+}
+
+static int
+msph_sphophi_foreach_post_arrow(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_arrow *arrow)
+{
+	int ret;
+
+	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, arrow->ltp)) != 0)
+		return (ret);
+	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, arrow->rtp)) != 0)
+		return (ret);
+
+	return (f(sc, T(arrow)));
+}
+
+static int
+msph_sphophi_foreach_post_name(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_name *name)
+{
+	int ret;
+
+	if ((ret = msph_sphophi_foreach_post_ident(f, sc, name->id)) != 0)
+		return (ret);
+
+	return (f(sc, T(name)));
+
+}
+
+static int
+msph_sphophi_foreach_post_appl(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_appl *appl)
+{
+	int ret;
+	struct msph_tree_tpexpr *tp;
+
+	ret = 0;
+	STAILQ_FOREACH(tp, &appl->head, entries) {
+		if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, tp)) != 0)
+			return (ret);
+	}
+
+	return (f(sc, T(appl)));
+}
+
+static int
+msph_sphophi_foreach_post_trait(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_trait *trait)
+{
+	int ret;
+	struct spho_scope *inner_sc;
+
+	inner_sc = GET_SCOPE(trait);
+
+	if ((ret = msph_sphophi_foreach_post_body(f, inner_sc, trait->body))
+	    != 0)
+		return (ret);
+
+	return (f(sc, T(trait)));
+}
+
+static int
+msph_sphophi_foreach_post_box(msph_tree_sphophi_f f,struct spho_scope *sc,
+    struct msph_tree_box *box)
+{
+	int ret;
+
+	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, box->inner)) != 0)
+		return (ret);
+
+	return (f(sc, T(box)));
+}
+
+static int
+msph_sphophi_foreach_post_forall(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_forall *forall)
+{
+	int ret;
+	struct spho_scope *inner_sc;
+	
+	inner_sc = GET_SCOPE(forall);
+
+	if ((ret = msph_sphophi_foreach_post_tpexpr(f, inner_sc, forall->inner))
+	    != 0)
+		return (ret);
+
+	return (f(sc, T(forall)));
+
+}
+
+static int
+msph_sphophi_foreach_post_paren(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_paren *paren)
+{
+	int ret;
+
+	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, paren->inner)) != 0)
+		return (ret);
+
+	return (f(sc, T(paren)));
+
+}
+
+static int
+msph_sphophi_foreach_post_true(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_true *tru)
+{
+	return (f(sc, T(tru)));
+}
+
+static int
+msph_sphophi_foreach_post_false(msph_tree_sphophi_f f, struct spho_scope *sc,
+    struct msph_tree_false *fls)
+{
+	return (f(sc, T(fls)));
+}
diff --git a/src/msph/token.c b/src/msph/token.c
index 01b5cd7..1c0adb2 100644
--- a/src/msph/token.c
+++ b/src/msph/token.c
@@ -110,12 +110,6 @@ static int	read_single_tok(struct msph_token *, struct msph_token_stream *);
 static const char	*tok_base_str(struct msph_token *);
 
 
-void msph_ctx_init(struct msph_ctx *ctx)
-{
-	ctx->err = 0;
-	ctx->err_info = 0;
-}
-
 struct msph_token_stream *
 msph_token_stream_file(struct msph_ctx *ctx, const char *name, FILE *f)
 {
diff --git a/src/msph/tree.c b/src/msph/tree.c
index 113dbfb..440fc53 100644
--- a/src/msph/tree.c
+++ b/src/msph/tree.c
@@ -21,7 +21,6 @@ struct tree_parse {
 
 #define CURR_TOKEN(parse)	(&parse->curr)
 
-#define T(ptr)			((struct msph_tree *)ptr)
 #define CTX(parse)		((parse)->s->ctx)
 
 static void	tree_parse_init(struct tree_parse *,
@@ -261,7 +260,8 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree)
 		break;
 	case MSPH_TREE_NOMINDECL:
 		nomd = (struct msph_tree_nomindecl *)tree;
-		if ((res = ind_fprintf(f, indent, "(nomindecl\n")) < 0)
+		if ((res = ind_fprintf(f, indent, "(nomindecl:%u,%u\n",
+		    TXT(nomd)->pos.line, TXT(nomd)->pos.col)) < 0)
 			return (res);
 		ret += res;
 		if ((res = tree_ind_fprint(f, indent+1, T(nomd->id))) < 0)
@@ -273,7 +273,8 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree)
 		break;
 	case MSPH_TREE_ASSERT:
 		ass = (struct msph_tree_assert *)tree;
-		if ((res = ind_fprintf(f, indent, "(assert\n")) < 0)
+		if ((res = ind_fprintf(f, indent, "(assert:%u,%u\n",
+		    TXT(ass)->pos.line, TXT(ass)->pos.col)) < 0)
 			return (res);
 		ret += res;
 		if ((res = tree_ind_fprint(f, indent+1, T(ass->ltp))) < 0)
@@ -288,7 +289,8 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree)
 		break;
 	case MSPH_TREE_TPDEF:
 		tpdef = (struct msph_tree_tpdef *)tree;
-		if ((res = ind_fprintf(f, indent, "(tpdef\n")) < 0)
+		if ((res = ind_fprintf(f, indent, "(tpdef:%u,%u\n",
+		    TXT(tpdef)->pos.line, TXT(tpdef)->pos.col)) < 0)
 			return (res);
 		ret += res;
 		if ((res = tree_ind_fprint(f, indent+1, T(tpdef->id))) < 0)
@@ -303,8 +305,11 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree)
 		break;
 	case MSPH_TREE_MEMBDECL:
 		membdecl = (struct msph_tree_membdecl *)tree;
-		if ((res = ind_fprintf(f, indent, "(membdecl:%s\n",
-		    membdecl->id->str)) < 0)
+		if ((res = ind_fprintf(f, indent, "(membdecl:%u,%u\n",
+		    TXT(membdecl)->pos.line, TXT(membdecl)->pos.col)) < 0)
+			return (res);
+		ret += res;
+		if ((res = tree_ind_fprint(f, indent+1, T(membdecl->id))) < 0)
 			return (res);
 		ret += res;
 		if ((res = tree_ind_fprint(f, indent+1, T(membdecl->tp))) < 0)
@@ -316,7 +321,8 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree)
 		break;
 	case MSPH_TREE_CONJ:
 		conj = (struct msph_tree_conj *)tree;
-		if ((res = ind_fprintf(f, indent, "(conj\n")) < 0)
+		if ((res = ind_fprintf(f, indent, "(conj:%u,%u\n",
+		    TXT(conj)->pos.line, TXT(conj)->pos.col)) < 0)
 			return (res);
 		ret += res;
 		if ((res = tree_ind_fprint(f, indent+1, T(conj->ltp))) < 0)
@@ -331,7 +337,8 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree)
 		break;
 	case MSPH_TREE_DISJ:
 		disj = (struct msph_tree_disj *)tree;
-		if ((res = ind_fprintf(f, indent, "(disj\n")) < 0)
+		if ((res = ind_fprintf(f, indent, "(disj:%u,%u\n",
+		    TXT(disj)->pos.line, TXT(disj)->pos.col)) < 0)
 			return (res);
 		ret += res;
 		if ((res = tree_ind_fprint(f, indent+1, T(disj->ltp))) < 0)
@@ -346,7 +353,8 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree)
 		break;
 	case MSPH_TREE_IMPL:
 		impl = (struct msph_tree_impl *)tree;
-		if ((res = ind_fprintf(f, indent, "(impl\n")) < 0)
+		if ((res = ind_fprintf(f, indent, "(impl:%u,%u\n",
+		    TXT(impl)->pos.line, TXT(impl)->pos.col)) < 0)
 			return (res);
 		ret += res;
 		if ((res = tree_ind_fprint(f, indent+1, T(impl->ltp))) < 0)
@@ -361,7 +369,8 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree)
 		break;
 	case MSPH_TREE_ARROW:
 		arrow = (struct msph_tree_arrow *)tree;
-		if ((res = ind_fprintf(f, indent, "(arrow\n")) < 0)
+		if ((res = ind_fprintf(f, indent, "(arrow:%u,%u\n",
+		    TXT(arrow)->pos.line, TXT(arrow)->pos.col)) < 0)
 			return (res);
 		ret += res;
 		if ((res = tree_ind_fprint(f, indent+1, T(arrow->ltp))) < 0)
@@ -376,7 +385,8 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree)
 		break;
 	case MSPH_TREE_BOX:
 		box = (struct msph_tree_box *)tree;
-		if ((res = ind_fprintf(f, indent, "(box\n")) < 0)
+		if ((res = ind_fprintf(f, indent, "(box:%u,%u\n",
+		    TXT(box)->pos.line, TXT(box)->pos.col)) < 0)
 			return (res);
 		ret += res;
 		if ((res = tree_ind_fprint(f, indent+1, T(box->inner))) < 0)
@@ -388,10 +398,11 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree)
 		break;
 	case MSPH_TREE_FORALL:
 		forall = (struct msph_tree_forall *)tree;
-		if ((res = ind_fprintf(f, indent, "(forall:\n")) < 0)
+		if ((res = ind_fprintf(f, indent, "(forall:%u,%u\n",
+		    TXT(forall)->pos.line, TXT(forall)->pos.col)) < 0)
 			return (res);
 		ret += res;
-		if ((res = tree_ind_fprint(f, indent+1, T(forall->ident))) < 0)
+		if ((res = tree_ind_fprint(f, indent+1, T(forall->id))) < 0)
 			return (res);
 		ret += res;
 		if ((res = tree_ind_fprint(f, indent+1, T(forall->inner))) < 0)
@@ -403,7 +414,8 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree)
 		break;
 	case MSPH_TREE_PAREN:
 		paren = (struct msph_tree_paren *)tree;
-		if ((res = ind_fprintf(f, indent, "(paren\n")) < 0)
+		if ((res = ind_fprintf(f, indent, "(paren:%u,%u\n",
+		    TXT(paren)->pos.line, TXT(paren)->pos.col)) < 0)
 			return (res);
 		ret += res;
 		if ((res = tree_ind_fprint(f, indent+1, T(paren->inner))) < 0)
@@ -415,7 +427,8 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree)
 		break;
 	case MSPH_TREE_APPL:
 		appl = (struct msph_tree_appl *)tree;
-		if ((res = ind_fprintf(f, indent, "(appl\n")) < 0)
+		if ((res = ind_fprintf(f, indent, "(appl:%u,%u\n",
+		    TXT(appl)->pos.line, TXT(appl)->pos.col)) < 0)
 			return (res);
 		ret += res;
 		if ((res = tree_ind_fprint(f, indent+1, T(appl->id))) < 0)
@@ -432,7 +445,8 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree)
 		break;
 	case MSPH_TREE_NAME:
 		name = (struct msph_tree_name *)tree;
-		if ((res = ind_fprintf(f, indent, "(name\n")) < 0)
+		if ((res = ind_fprintf(f, indent, "(name:%u,%u\n",
+		    TXT(name)->pos.line, TXT(name)->pos.col)) < 0)
 			return (res);
 		ret += res;
 		if ((res = tree_ind_fprint(f, indent+1, T(name->id))) < 0)
@@ -444,7 +458,8 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree)
 		break;
 	case MSPH_TREE_TRAIT:
 		trait = (struct msph_tree_trait *)tree;
-		if ((res = ind_fprintf(f, indent, "(trait\n")) < 0)
+		if ((res = ind_fprintf(f, indent, "(trait:%u,%u\n",
+		    TXT(trait)->pos.line, TXT(trait)->pos.col)) < 0)
 			return (res);
 		ret += res;
 		if ((res = tree_ind_fprint(f, indent+1, T(trait->body))) < 0)
@@ -456,18 +471,21 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree)
 		break;
 	case MSPH_TREE_IDENT:
 		ident = (struct msph_tree_ident *)tree;
-		if ((res = ind_fprintf(f, indent, "(ident:%s)\n", ident->str))
+		if ((res = ind_fprintf(f, indent, "(ident:%u,%u:%s)\n",
+		    TXT(ident)->pos.line, TXT(ident)->pos.col, ident->str))
 		    < 0)
 			return (res);
 		ret += res;
 		break;
 	case MSPH_TREE_TRUE:
-		if ((res = ind_fprintf(f, indent, "(true)\n")) < 0)
+		if ((res = ind_fprintf(f, indent, "(true:%u,%u)\n",
+		    TXT(tree)->pos.line, TXT(tree)->pos.col)) < 0)
 			return (res);
 		ret += res;
 		break;
 	case MSPH_TREE_FALSE:
-		if ((res = ind_fprintf(f, indent, "(false)\n")) < 0)
+		if ((res = ind_fprintf(f, indent, "(false:%u,%u)\n",
+		    TXT(tree)->pos.line, TXT(tree)->pos.col)) < 0)
 			return (res);
 		ret += res;
 		break;
@@ -526,6 +544,7 @@ tree_parse_unit(struct tree_parse *p, struct msph_tree *parent)
 	}
 	T(unit)->type = MSPH_TREE_UNIT;
 	T(unit)->parent = parent;
+	SCOPE_DECOR_INIT(&unit->dec);
 	unit->body = NULL;
 
 	if ((namelen = strlcpy(unit->name, p->s->name, sizeof(unit->name)))
@@ -623,6 +642,8 @@ tree_parse_tpdef(struct tree_parse *p, struct msph_tree *parent)
 	}
 	T(def)->type = MSPH_TREE_TPDEF;
 	T(def)->parent = parent;
+	TXT(def)->pos = CURR_TOKEN(p)->pos;
+	// TODO add scope decor when generalizing to type operators
 
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err);
 	if ((def->id = tree_parse_ident(p, T(def))) == NULL)
@@ -646,7 +667,6 @@ tree_parse_ident(struct tree_parse *p, struct msph_tree *parent)
 {
 	struct msph_tree_ident *id;
 
-	SPHO_DEBUG_PRINT("parsing ident\n");
 	EXPECT_CURR_TOKEN(p, TOK_IDENT, MSPH_TREE_IDENT, return (NULL));
 
 	if ((id = malloc(sizeof(*id))) == NULL) {
@@ -655,6 +675,8 @@ tree_parse_ident(struct tree_parse *p, struct msph_tree *parent)
 	}
 	T(id)->type = MSPH_TREE_IDENT;
 	T(id)->parent = parent;
+	TXT(id)->pos = CURR_TOKEN(p)->pos;
+	NOM_DECOR_INIT(&id->dec);
 
 	if (SPHO_STRLCPY(id->str, CURR_TOKEN(p)->data.str, sizeof(id->str))
 	    >= sizeof(id->str)) {
@@ -675,47 +697,36 @@ tree_parse_tpexpr(struct tree_parse *p, struct msph_tree *parent)
 
 	switch (CURR_TOKEN(p)->type) {
 	case TOK_AMP:
-		SPHO_DEBUG_PRINT("parsing conj\n");
 		tp = tree_parse_conj(p, parent);
 		break;
 	case TOK_PIPE:
-		SPHO_DEBUG_PRINT("parsing disj\n");
 		tp = tree_parse_disj(p, parent);
 		break;
 	case TOK_IMPL:
-		SPHO_DEBUG_PRINT("parsing impl\n");
 		tp = tree_parse_impl(p, parent);
 		break;
 	case TOK_RARROW:
-		SPHO_DEBUG_PRINT("parsing arrow\n");
 		tp = tree_parse_arrow(p, parent);
 		break;
 	case TOK_KW_BOX:
-		SPHO_DEBUG_PRINT("parsing box\n");
 		tp = tree_parse_box(p, parent);
 		break;
 	case TOK_KW_FORALL:
-		SPHO_DEBUG_PRINT("parsing forall\n");
 		tp = tree_parse_forall(p, parent);
 		break;
 	case TOK_IDENT:
-		SPHO_DEBUG_PRINT("parsing name\n");
 		tp = tree_parse_name(p, parent);
 		break;
 	case TOK_CONST_TRUE:
-		SPHO_DEBUG_PRINT("parsing true\n");
 		tp = tree_parse_true(p, parent);
 		break;
 	case TOK_CONST_FALSE:
-		SPHO_DEBUG_PRINT("parsing false\n");
 		tp = tree_parse_false(p, parent);
 		break;
 	case TOK_LPAREN:
-		SPHO_DEBUG_PRINT("parsing paren\n");
 		tp = tree_parse_paren(p, parent);
 		break;
 	case TOK_LBRACE:
-		SPHO_DEBUG_PRINT("parsing trait\n");
 		tp = tree_parse_trait(p, parent);
 		break;
 	default:
@@ -741,6 +752,8 @@ tree_parse_conj(struct tree_parse *p, struct msph_tree *parent)
 	}
 	T(conj)->type = MSPH_TREE_CONJ;
 	T(conj)->parent = parent;
+	TXT(conj)->pos = CURR_TOKEN(p)->pos;
+	TP_DECOR_INIT(&conj->htpe.dec);
 	conj->ltp = NULL;
 	conj->rtp = NULL;
 
@@ -775,6 +788,8 @@ tree_parse_disj(struct tree_parse *p, struct msph_tree *parent)
 	}
 	T(disj)->type = MSPH_TREE_DISJ;
 	T(disj)->parent = parent;
+	TXT(disj)->pos = CURR_TOKEN(p)->pos;
+	TP_DECOR_INIT(&disj->htpe.dec);
 	disj->ltp = NULL;
 	disj->rtp = NULL;
 
@@ -809,6 +824,8 @@ tree_parse_impl(struct tree_parse *p, struct msph_tree *parent)
 	}
 	T(impl)->type = MSPH_TREE_IMPL;
 	T(impl)->parent = parent;
+	TXT(impl)->pos = CURR_TOKEN(p)->pos;
+	TP_DECOR_INIT(&impl->htpe.dec);
 	impl->ltp = NULL;
 	impl->rtp = NULL;
 
@@ -843,6 +860,8 @@ tree_parse_arrow(struct tree_parse *p, struct msph_tree *parent)
 	}
 	T(arrow)->type = MSPH_TREE_ARROW;
 	T(arrow)->parent = parent;
+	TXT(arrow)->pos = CURR_TOKEN(p)->pos;
+	TP_DECOR_INIT(&arrow->htpe.dec);
 	arrow->ltp = NULL;
 	arrow->rtp = NULL;
 
@@ -877,6 +896,8 @@ tree_parse_box(struct tree_parse *p, struct msph_tree *parent)
 	}
 	T(box)->type = MSPH_TREE_BOX;
 	T(box)->parent = parent;
+	TXT(box)->pos = CURR_TOKEN(p)->pos;
+	TP_DECOR_INIT(&box->htpe.dec);
 	box->inner = NULL;
 
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_BOX, goto err);
@@ -903,11 +924,14 @@ tree_parse_forall(struct tree_parse *p, struct msph_tree *parent)
 	}
 	T(fa)->type = MSPH_TREE_FORALL;
 	T(fa)->parent = parent;
-	fa->ident = NULL;
+	TXT(fa)->pos = CURR_TOKEN(p)->pos;
+	TP_DECOR_INIT(&fa->htpe.dec);
+	SCOPE_DECOR_INIT(&fa->dec);
+	fa->id = NULL;
 	fa->inner = NULL;
 
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_FORALL, goto err);
-	if ((fa->ident = tree_parse_ident(p, T(fa))) == NULL)
+	if ((fa->id = tree_parse_ident(p, T(fa))) == NULL)
 		goto err;
 
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_FORALL, goto err);
@@ -964,6 +988,8 @@ tree_parse_name(struct tree_parse *p, struct msph_tree *parent)
 	T(name)->type = MSPH_TREE_NAME;
 	T(name)->parent = parent;
 
+	TXT(name)->pos = TXT(id)->pos;
+	TP_DECOR_INIT(&name->htpe.dec);
 	T(id)->parent = T(name);
 	name->id = id;
 
@@ -1001,6 +1027,7 @@ tree_parse_applargs(struct tree_parse *p, struct msph_tree_ident *id,
 	}
 	T(appl)->type = MSPH_TREE_APPL;
 	T(appl)->parent = parent;
+	TP_DECOR_INIT(&appl->htpe.dec);
 	appl->id = NULL;
 	STAILQ_INIT(&appl->head);
 
@@ -1035,7 +1062,9 @@ tree_parse_applargs(struct tree_parse *p, struct msph_tree_ident *id,
 	}
 
 	/* finally, appl takes ownership of id */
+	T(id)->parent = T(appl);
 	appl->id = id;
+	TXT(appl)->pos = TXT(id)->pos;
 
 	return ((struct msph_tree_tpexpr *)appl);
 err:
@@ -1057,6 +1086,8 @@ tree_parse_true(struct tree_parse *p, struct msph_tree *parent)
 	}
 	T(t)->type = MSPH_TREE_TRUE;
 	T(t)->parent = parent;
+	TXT(t)->pos = CURR_TOKEN(p)->pos;
+	TP_DECOR_INIT(&t->htpe.dec);
 
 	return ((struct msph_tree_tpexpr *)t);
 }
@@ -1074,6 +1105,8 @@ tree_parse_false(struct tree_parse *p, struct msph_tree *parent)
 	}
 	T(f)->type = MSPH_TREE_FALSE;
 	T(f)->parent = parent;
+	TXT(f)->pos = CURR_TOKEN(p)->pos;
+	TP_DECOR_INIT(&f->htpe.dec);
 
 	return ((struct msph_tree_tpexpr *)f);
 }
@@ -1092,6 +1125,8 @@ tree_parse_paren(struct tree_parse *p, struct msph_tree *parent)
 	}
 	T(par)->type = MSPH_TREE_PAREN;
 	T(par)->parent = parent;
+	TXT(par)->pos = CURR_TOKEN(p)->pos;
+	TP_DECOR_INIT(&par->htpe.dec);
 	par->inner = NULL;
 
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_PAREN, goto err);
@@ -1123,6 +1158,9 @@ tree_parse_trait(struct tree_parse *p, struct msph_tree *parent)
 	}
 	T(trait)->type = MSPH_TREE_TRAIT;
 	T(trait)->parent = parent;
+	TXT(trait)->pos = CURR_TOKEN(p)->pos;
+	TP_DECOR_INIT(&trait->htpe.dec);
+	SCOPE_DECOR_INIT(&trait->dec);
 	trait->body = NULL;
 
 	if ((trait->body = tree_parse_body(p, T(trait))) == NULL)
@@ -1153,9 +1191,10 @@ tree_parse_nomindecl(struct tree_parse *p, struct msph_tree *parent)
 	}
 	T(nomd)->type = MSPH_TREE_NOMINDECL;
 	T(nomd)->parent = parent;
+	TXT(nomd)->pos = CURR_TOKEN(p)->pos;
 	nomd->id = NULL;
 
-	EXPECT_READ_NEXT(res, p, MSPH_TREE_NOMINDECL, return (NULL));
+	EXPECT_READ_NEXT(res, p, MSPH_TREE_NOMINDECL, goto err);
 	if ((nomd->id = tree_parse_ident(p, T(nomd))) == NULL)
 		goto err;
 
@@ -1174,7 +1213,6 @@ tree_parse_membdecl(struct tree_parse *p, struct msph_tree *parent)
 
 	EXPECT_CURR_TOKEN(p, TOK_KW_MEMBER, MSPH_TREE_MEMBDECL,
 	    return (NULL));
-	EXPECT_READ_NEXT(res, p, MSPH_TREE_MEMBDECL, return (NULL));
 
 	if ((membd = malloc(sizeof(*membd))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
@@ -1182,9 +1220,11 @@ tree_parse_membdecl(struct tree_parse *p, struct msph_tree *parent)
 	}
 	T(membd)->type = MSPH_TREE_MEMBDECL;
 	T(membd)->parent = parent;
+	TXT(membd)->pos = CURR_TOKEN(p)->pos;
 	membd->id = NULL;
 	membd->tp = NULL;
 
+	EXPECT_READ_NEXT(res, p, MSPH_TREE_MEMBDECL, goto err);
 	if ((membd->id = tree_parse_ident(p, T(membd))) == NULL)
 		goto err;
 
@@ -1211,7 +1251,6 @@ tree_parse_assert(struct tree_parse *p, struct msph_tree *parent)
 
 	EXPECT_CURR_TOKEN(p, TOK_KW_ASSERT, MSPH_TREE_ASSERT,
 	    return (NULL));
-	EXPECT_READ_NEXT(res, p, MSPH_TREE_ASSERT, return (NULL));
 
 	if ((ass = malloc(sizeof(*ass))) == NULL) {
 		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
@@ -1219,9 +1258,11 @@ tree_parse_assert(struct tree_parse *p, struct msph_tree *parent)
 	}
 	T(ass)->type = MSPH_TREE_ASSERT;
 	T(ass)->parent = parent;
+	TXT(ass)->pos = CURR_TOKEN(p)->pos;
 	ass->ltp = NULL;
 	ass->rtp = NULL;
 
+	EXPECT_READ_NEXT(res, p, MSPH_TREE_ASSERT, goto err);
 	if ((ass->ltp = tree_parse_tpexpr(p, T(ass))) == NULL)
 		goto err;
 
@@ -1243,8 +1284,8 @@ err:
 static void
 free_the_tree(struct msph_tree *tree)
 {
-	/* no one will free the tree :´( */
+	/* will anyone ever free the tree? :´( */
 	SPHO_POSTCOND((void *)tree != (void *)free);
-	SPHO_POSTCOND(0);
+	// SPHO_POSTCOND(0);
 }
 
diff --git a/src/spho/ctx.c b/src/spho/ctx.c
index dacc076..fbb0e9d 100644
--- a/src/spho/ctx.c
+++ b/src/spho/ctx.c
@@ -16,10 +16,13 @@ struct spho_err {
 
 struct spho_err spho_errmsgs[] = {
 	{ SPHO_ERR_SYS,		"spho system error" },
+
 	{ SPHO_ERR_INTERNAL,	"spho internal error" },
 	{ SPHO_ERR_TOOBIG,	"parameter size too big" },
 	{ SPHO_ERR_ARGINVAL,	"invalid argument" },
-	{ SPHO_ERR_NAMEINUSE,	"name in use" },
+
+	{ SPHO_ERR_NOM_INUSE,	"name already declared in current scope" },
+	{ SPHO_ERR_NOM_NOTINSCOPE,	"name not in scope" },
 	{ -1, NULL }
 };
 
@@ -60,7 +63,6 @@ spho_ctx_destroy(struct spho_ctx *ctx)
 const char *
 spho_ctx_strerror(struct spho_ctx *ctx)
 {
-	int res;
 	const char *msg;
 
 	SPHO_PRECOND(ctx != NULL);
@@ -87,8 +89,8 @@ spho_ctx_sys_strerror(struct spho_ctx *ctx)
 
 #ifdef SPHO_DEBUG
 	res = snprintf(ctx->errbuf, sizeof(ctx->errbuf),
-	    "%s:%d:spho_syserr:%s (%d)", ctx->filebuf, ctx->errline,
-	    strerror(ctx->err_info), ctx->err_info);
+	    "spho_syserr: %s (%d) (%s:%d)", strerror(ctx->err_info),
+	    ctx->err_info, ctx->filebuf, ctx->errline);
 	if (res >= sizeof(ctx->errbuf))
 		ctx->errbuf[sizeof(ctx->errbuf) - 1] = '\0';
 #else
@@ -110,20 +112,20 @@ spho_ctx_intern_strerror(struct spho_ctx *ctx)
 
 	SPHO_PRECOND(ctx != NULL);
 
-	for (i = 0; spho_errmsgs[i].msg != NULL; i++) {
+	for (i = 0; spho_errmsgs[i].err != -1; i++) {
 		if (spho_errmsgs[i].err == ctx->err) {
 #ifdef SPHO_DEBUG
 			res = snprintf(ctx->errbuf, sizeof(ctx->errbuf),
-			    "%s:%d:spho_intern_err:%s", ctx->filebuf,
-			    ctx->errline, spho_errmsgs[i].msg);
+			    "spho_err: %s (%s:%d)", spho_errmsgs[i].msg,
+			    ctx->filebuf, ctx->errline);
 #else
 			res = snprintf(ctx->errbuf, sizeof(ctx->errbuf),
-			    "spho_intern_err:%s", ctx->errbuf);
+			    "spho_err: %s", ctx->errbuf);
 #endif
 		}
 	}
 
-	SPHO_POSTCOND(res != -1);
+	SPHO_POSTCOND(! (res == -1 && res >= (int)sizeof(ctx->errbuf)));
 
 	return (ctx->errbuf);
 }
diff --git a/src/spho/scope.c b/src/spho/scope.c
index 988e824..442834c 100644
--- a/src/spho/scope.c
+++ b/src/spho/scope.c
@@ -9,13 +9,18 @@
 
 static void spho_nom_term(struct spho_nom *);
 
+static int spho_scope_nom_get_norec(struct spho_scope *, const char *, size_t ,
+    struct spho_nom **);
+
 int
 spho_scope_init(struct spho_scope *sc, struct spho_ctx *ctx,
     struct spho_scope *p)
 {
 	SLIST_INIT(&sc->subs);
 	SLIST_INIT(&sc->noms);
+	TAILQ_INIT(&sc->tps);
 
+	sc->ctx = ctx;
 	sc->parent = p;
 
 	return (0);
@@ -70,7 +75,6 @@ spho_nom_term(struct spho_nom *nom)
 void
 spho_scope_destroy(struct spho_scope *sc)
 {
-	struct spho_scope *sub;
 	struct spho_scope *p;
 
 	p = sc->parent;
@@ -90,12 +94,13 @@ spho_scope_nom_add(struct spho_scope *sc, const char *nomstr, size_t sz)
 #endif
 	struct spho_nom *nom;
 
+	nom = NULL;
 
-	if (spho_scope_nom_get(sc, nomstr, sz, &nom) == -1)
+	if (spho_scope_nom_get_norec(sc, nomstr, sz, &nom) == -1)
 		return (NULL);
 
 	if (nom != NULL) {
-		SPHO_SC_ERR(sc, SPHO_ERR_NAMEINUSE);
+		SPHO_SC_ERR(sc, SPHO_ERR_NOM_INUSE);
 		return (NULL);
 	}
 
@@ -144,7 +149,50 @@ spho_scope_nom_get(struct spho_scope *sc, const char *nomstr, size_t sz,
 		return (-1);
 	}
 
-	out = NULL;
+	*out = NULL;
+	while (*out == NULL && sc != NULL) {
+		SLIST_FOREACH(nom, &sc->noms, next) {
+			if (strncmp(nom->s, nomstr, sz) == 0) {
+				*out = nom;
+				break;
+			}
+		}
+		sc = sc->parent;
+	}
+
+	return (0);
+}
+
+int
+spho_scope_nom_lookup(struct spho_scope *sc, const char *nomstr, size_t sz,
+    struct spho_nom **out)
+{
+	int ret;
+
+	if (spho_scope_nom_get(sc, nomstr, sz, out) == -1)
+		return (-1);
+
+	if (*out == NULL) {
+		SPHO_SC_ERR(sc, SPHO_ERR_NOM_NOTINSCOPE);
+		return (-1);
+	}
+
+	return (0);
+}
+static int
+spho_scope_nom_get_norec(struct spho_scope *sc, const char *nomstr, size_t sz,
+    struct spho_nom **out)
+{
+	struct spho_nom *nom;
+
+	nom = NULL;
+
+	if (sz > sizeof(nom->s)) {
+		SPHO_ERR(sc->ctx, SPHO_ERR_TOOBIG);
+		return (-1);
+	}
+
+	*out = NULL;
 	SLIST_FOREACH(nom, &sc->noms, next) {
 		if (strncmp(nom->s, nomstr, sz) == 0) {
 			*out = nom;
diff --git a/src/spho/tp.c b/src/spho/tp.c
index e207197..6f73d47 100644
--- a/src/spho/tp.c
+++ b/src/spho/tp.c
@@ -7,6 +7,9 @@
 #include "spho/tp.h"
 
 
+const struct tp_konst_data tp_konst_true = { TP_KONST_KEY_TRUE, "True" };
+const struct tp_konst_data tp_konst_false = { TP_KONST_KEY_FALSE, "False" };
+
 //struct spho_tp	*
 //spho_tp_create_disj(struct spho_ctx *, struct spho_tp *, struct spho_tp *,
 //    struct spho_tp *)
@@ -14,177 +17,239 @@
 //
 //}
 
-
-struct spho_tp *
-spho_tp_alloc(struct spho_scope *sc, int form)
+static struct spho_tp *
+spho_tp_alloc(struct spho_scope *sc)
 {
-	struct spho_tp *tp;
+	struct spho_tp_alloc *tp_alloc;
 
-	SPHO_PRECOND(SPHO_TP_FORM_IS_VALID(form));
-
-	if ((tp = calloc(1, sizeof(struct spho_tp))) == NULL) {
+	if ((tp_alloc = calloc(1, sizeof(*tp_alloc))) == NULL) {
 		SPHO_SC_ERR(sc, SPHO_ERR_SYS);
 		return (NULL);
 	}
 
-	tp->sc = sc;
-	tp->form = form;
+	((struct spho_tp *)tp_alloc)->sc = sc;
+	TAILQ_INSERT_TAIL(&sc->tps, tp_alloc, allocs);
+
+	return ((struct spho_tp *)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)
+{
+	struct spho_tp *tp;
+
+	if ((tp = spho_tp_alloc(sc)) == NULL)
+		return (NULL);
+
+	tp->form = SPHO_TP_FORM_CONJ;
+	tp->d.binop.left = ltp;
+	tp->d.binop.right = rtp;
 
 	return (tp);
 }
 
-
-int
-spho_tp_init_disj(struct spho_tp *tp, struct spho_tp *a, struct spho_tp *b)
+struct spho_tp *
+spho_tp_create_disj(struct spho_scope *sc, struct spho_tp *ltp,
+    struct spho_tp *rtp)
 {
-	if (tp->form != SPHO_TP_FORM_DISJ) {
-		SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
-		return (-1);
-	}
+	struct spho_tp *tp;
 
-	tp->data.binop.left = a;
-	tp->data.binop.right = b;
+	if ((tp = spho_tp_alloc(sc)) == NULL)
+		return (NULL);
 
-	return (0);
+	tp->form = SPHO_TP_FORM_DISJ;
+	tp->d.binop.left = ltp;
+	tp->d.binop.right = rtp;
+
+	return (tp);
 }
 
-int
-spho_tp_init_conj(struct spho_tp *tp, struct spho_tp *a, struct spho_tp *b)
+struct spho_tp *
+spho_tp_create_impl(struct spho_scope *sc, struct spho_tp *ltp,
+    struct spho_tp *rtp)
 {
-	if (tp->form != SPHO_TP_FORM_CONJ) {
-		SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
-		return (-1);
-	}
+	struct spho_tp *tp;
 
-	tp->data.binop.left = a;
-	tp->data.binop.right = b;
+	if ((tp = spho_tp_alloc(sc)) == NULL)
+		return (NULL);
 
-	return (0);
+	tp->form = SPHO_TP_FORM_IMPL;
+	tp->d.binop.left = ltp;
+	tp->d.binop.right = rtp;
+
+	return (tp);
 }
 
-int
-spho_tp_init_impl(struct spho_tp *tp, struct spho_tp *a, struct spho_tp *b)
+struct spho_tp *
+spho_tp_create_arrow(struct spho_scope *sc, struct spho_tp *ltp,
+    struct spho_tp *rtp)
 {
-	if (tp->form != SPHO_TP_FORM_IMPL) {
-		SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
-		return (-1);
-	}
+	struct spho_tp *tp;
 
-	tp->data.binop.left = a;
-	tp->data.binop.right = b;
+	if ((tp = spho_tp_alloc(sc)) == NULL)
+		return (NULL);
 
-	return (0);
+	tp->form = SPHO_TP_FORM_ARROW;
+	tp->d.binop.left = ltp;
+	tp->d.binop.right = rtp;
+
+	return (tp);
 }
 
-int
-spho_tp_init_arrow(struct spho_tp *tp, struct spho_tp *a, struct spho_tp *b)
+struct spho_tp *
+spho_tp_create_box(struct spho_scope *sc, struct spho_tp *inner)
 {
-	if (tp->form != SPHO_TP_FORM_ARROW) {
-		SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
-		return (-1);
-	}
+	struct spho_tp *tp;
 
-	tp->data.binop.left = a;
-	tp->data.binop.right = b;
+	if ((tp = spho_tp_alloc(sc)) == NULL)
+		return (NULL);
 
-	return (0);
+	tp->form = SPHO_TP_FORM_BOX;
+	tp->d.unop.operand = inner;
+
+	return (tp);
 }
 
-int
-spho_tp_init_box(struct spho_tp *tp, struct spho_tp *inr)
+struct spho_tp *
+spho_tp_create_forall(struct spho_scope *sc, struct spho_nom *nom,
+    struct spho_tp *tp)
 {
-	if (tp->form != SPHO_TP_FORM_BOX) {
-		SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
-		return (-1);
-	}
+	struct spho_tp *ret;
 
-	tp->data.box.inr = inr;
+	if ((ret = spho_tp_alloc(sc)) == NULL)
+		return (NULL);
 
-	return (0);
+	ret->form = SPHO_TP_FORM_FORALL;
+	ret->d.bind.nom = nom;
+	ret->d.bind.bound = tp;
+
+	return (ret);
 }
 
-int
-spho_tp_init_forall(struct spho_tp *tp, struct spho_var *var,
-    struct spho_tp *inr)
+struct spho_tp *
+spho_tp_create_true(struct spho_scope *sc)
 {
-	if (tp->form != SPHO_TP_FORM_FORALL) {
-		SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
-		return (-1);
-	}
+	struct spho_tp *ret;
 
-	tp->data.fa.var = var;
-	tp->data.fa.inr = inr;
+	if ((ret = spho_tp_alloc(sc)) == NULL)
+		return (NULL);
 
-	return (0);
+	ret->form = SPHO_TP_FORM_TRUE;
+	ret->d.konst = tp_konst_true;
+
+	return (ret);
 }
 
-int
-spho_tp_init_bappl(struct spho_tp *tp, struct spho_bind *bind,
+struct spho_tp *
+spho_tp_create_false(struct spho_scope *sc)
+{
+	struct spho_tp *ret;
+
+	if ((ret = spho_tp_alloc(sc)) == NULL)
+		return (NULL);
+
+	ret->form = SPHO_TP_FORM_FALSE;
+	ret->d.konst = tp_konst_false;
+
+	return (ret);
+}
+
+struct spho_tp *
+spho_tp_create_name(struct spho_scope *sc, struct spho_nom *nom)
+{
+	struct spho_tp *ret;
+
+	if ((ret = spho_tp_alloc(sc)) == NULL)
+		return (NULL);
+
+	ret->form = SPHO_TP_FORM_NOM;
+	ret->d.nom.nom = nom;
+
+	return (ret);
+}
+
+struct spho_tp *
+spho_tp_create_appl(struct spho_scope *sc, struct spho_nom *nom,
     struct spho_tp_l *args)
+{
+	struct spho_tp *ret;
+
+	if ((ret = spho_tp_alloc(sc)) == NULL)
+		return (NULL);
+
+	ret->form = SPHO_TP_FORM_APPL;
+	ret->d.appl.nom = nom;
+	ret->d.appl.args = args;
+
+	return (ret);
+}
+
+struct spho_tp *
+spho_tp_create_member(struct spho_scope *sc, struct spho_nom *nom,
+    struct spho_tp *tp)
+{
+	struct spho_tp *ret;
+
+	if ((ret = spho_tp_alloc(sc)) == NULL)
+		return (NULL);
+
+	ret->form = SPHO_TP_FORM_MEMBER;
+	ret->d.bind.nom = nom;
+	ret->d.bind.bound = tp;
+
+	return (ret);
+}
+
+/* Free type structure. External data (like nom) are freed elsewhere. */
+void
+spho_tp_destroy(struct spho_tp *tp)
 {
 	struct spho_tp *arg;
 
-	if (tp->form != SPHO_TP_FORM_BAPPL) {
-		SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
-		return (-1);
+	switch (tp->form) {
+	case SPHO_TP_FORM_TRUE:
+	case SPHO_TP_FORM_FALSE:
+	case SPHO_TP_FORM_NOM: 
+		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:
+	case SPHO_TP_FORM_MEMBER: 
+		spho_tp_destroy(tp->d.bind.bound);
+		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;
 	}
 
-	tp->data.bappl.bind = bind;
-	tp->data.bappl.args = args;
-
-	return (0);
+	spho_tp_free(tp);
 }
-
-int
-spho_tp_init_false(struct spho_tp *tp)
-{
-	if (tp->form != SPHO_TP_FORM_FALSE) {
-		SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
-		return (-1);
-	}
-
-	tp->data.konst.k = SPHO_K_FALSE;
-
-	return (0);
-}
-
-int
-spho_tp_init_true(struct spho_tp *tp)
-{
-	if (tp->form != SPHO_TP_FORM_TRUE) {
-		SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
-		return (-1);
-	}
-
-	tp->data.konst.k = SPHO_K_TRUE;
-
-	return (0);
-}
-
-int
-spho_tp_init_var(struct spho_tp *tp, struct spho_var *var)
-{
-	if (tp->form != SPHO_TP_FORM_VAR) {
-		SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
-		return (-1);
-	}
-
-	tp->data.var.v = var;
-
-	return (0);
-}
-
-int
-spho_tp_init_rec(struct spho_tp *tp, struct spho_rec *rec)
-{
-	if (tp->form != SPHO_TP_FORM_REC) {
-		SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
-		return (-1);
-	}
-
-	tp->data.rec.r = rec;
-
-	return (0);
-}
-
-