diff --git a/.gitignore b/.gitignore
index dd51cb4..58189c6 100644
--- a/.gitignore
+++ b/.gitignore
@@ -52,7 +52,7 @@ Mkfile.old
 dkms.conf
 
 # CMake build directory
-build/
+build-*/
 
 
 # vim
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 573a310..f3c8263 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -4,27 +4,55 @@ project(log-e-sappho C)
 set(CMAKE_C_STANDARD 99)
 set(CMAKE_C_STANDARD_REQUIRED True)
 
+include(CheckSymbolExists)
+
 set(INCLUDE_DIR include)
 set(SRC_DIR src)
 
 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}/spho.h
+	${SPHO_HEADER_DIR}/scope.h
 	${SPHO_HEADER_DIR}/tp.h
+	${SPHO_HEADER_DIR}/spho.h
 )
 
 set(SPHO_SRC
   ${SRC_DIR}/spho/ctx.c
+  ${SRC_DIR}/spho/scope.c
+  ${SRC_DIR}/spho/tp.c
 )
 
+check_symbol_exists(strlcpy "string.h" HAVE_STRLCPY)
+
 add_library(spho STATIC ${SPHO_HEADER} ${SPHO_SRC})
 target_include_directories(spho PRIVATE ${INCLUDE_DIR})
+target_compile_definitions(spho PRIVATE
+	$<$<CONFIG:Debug>:SPHO_DEBUG>
+	$<$<BOOL:${HAVE_STRLCPY}>:SPHO_USE_STRLCPY>
+)
 
 add_executable(devcheck ${SRC_DIR}/run/devcheck.c)
 target_link_libraries(devcheck spho)
 target_include_directories(devcheck PRIVATE ${INCLUDE_DIR})
+target_compile_definitions(devcheck PRIVATE
+	$<$<CONFIG:Debug>:SPHO_DEBUG>
+)
+
+
+set(MSPH_SRC
+	${SRC_DIR}/msph/msph_token.c
+	${SRC_DIR}/msph/msph.c
+)
+
+set(MSPH_HEADER
+	${SRC_DIR}/msph/msph_token.h
+)
+
+add_executable(msph ${MSPH_HEADER} ${MSPH_SRC})
+target_include_directories(spho PRIVATE ${INCLUDE_DIR})
diff --git a/include/spho/ctx.h b/include/spho/ctx.h
index fbc27e5..9858e85 100644
--- a/include/spho/ctx.h
+++ b/include/spho/ctx.h
@@ -1,28 +1,31 @@
 #ifndef _SPHO_CTX_H
 #define _SPHO_CTX_H
 
-#include "spho/data.h"
+#include "spho/err.h"
+#include "spho/scope.h"
 
 #define SPHO_ERR_BUF_LEN	2048
 #define SPHO_ERR_FILEBUF_LEN	128
 
 struct spho_ctx {
+	struct spho_scope glob;
+
 	int	err;
 	int	err_info;
-
-	struct spho_nom_l	noms;
-	struct spho_const_l	cnsts;
+	char	errbuf[SPHO_ERR_BUF_LEN];
 
 #ifdef SPHO_DEBUG
-	char filebuf[SPHO_ERR_FILEBUF_LEN];
-	int errline;
-#else
-	char errbuf[SPHO_ERR_BUF_LEN];
+	char	filebuf[SPHO_ERR_FILEBUF_LEN];
+	int	errline;
 #endif
+
 };
 
 struct spho_ctx		*spho_ctx_create(void);
 void			spho_ctx_destroy(struct spho_ctx *);
 const char		*spho_ctx_strerror(struct spho_ctx *);
 
+
+struct spho_nom *spho_nom_add(struct spho_ctx *, char *, size_t);
+struct spho_nom *spho_nom_get(struct spho_ctx *, char *, size_t);
 #endif
diff --git a/include/spho/data.h b/include/spho/data.h
index 837f273..0cd02c8 100644
--- a/include/spho/data.h
+++ b/include/spho/data.h
@@ -1,36 +1,12 @@
 #ifndef _SPHO_DATA_H
 #define _SPHO_DATA_H
 
-#include <sys/queue.h>
-
-struct spho_name {
-	char str[128];
-};
-
-struct spho_var {
-	struct spho_name name;
-};
-
-struct spho_cnst {
-	struct spho_name name;
-};
-
 struct spho_nom {
-	struct spho_name name;
+	char			s[128];
+	SLIST_ENTRY(spho_nom)	next;
 };
 
-struct spho_nom_le {
-	struct spho_nom			nom;
-	SLIST_ENTRY(spho_nom_le)	next;
-};
-
-struct spho_cnst_le {
-	struct spho_cnst		cnst;
-	SLIST_ENTRY(spho_cnst_le)	next;
-};
+SLIST_HEAD(spho_nom_l, spho_nom);
 
 
-SLIST_HEAD(spho_nom_l, spho_nom_le);
-SLIST_HEAD(spho_const_l, spho_cnst_le);
-
-#endif
+#endif /* _SPHO_DATA_H */
diff --git a/include/spho/err.h b/include/spho/err.h
index b11db1b..b4dcc33 100644
--- a/include/spho/err.h
+++ b/include/spho/err.h
@@ -1,32 +1,40 @@
 #ifndef _SPHO_ERR_H
 #define _SPHO_ERR_H
 
-#define SPHO_ERR_SYSTEM         0x000001
+#include <errno.h>
 
-#define SPHO_ERR_INTERNAL       0x010001
+#ifdef SPHO_DEBUG
+#include <stdio.h>
+#endif
 
-#define SPHO_ERR_IS_SYSERR(err)		(SPHO_ERR_SYSTEM == err)
+#define SPHO_ERR_SYS		0x000001
+
+#define SPHO_ERR_INTERNAL	0x010001
+#define SPHO_ERR_TOOBIG		0x010002
+#define SPHO_ERR_ARGINVAL	0x010003
+#define SPHO_ERR_NAMEINUSE	0x010004
+
+#define SPHO_ERR_IS_SYSERR(err)		(SPHO_ERR_SYS == err)
 
 #ifdef SPHO_DEBUG
 
-#define SPHO_ERR(ctx, err)						\
+#define SPHO_ERR(ctx, e)						\
 	do {								\
-		ctx->err = err;						\
-		if (err == SPHO_ERR_SYSTEM)				\
-			ctx->err_info = errno;				\
-		snprintf(ctx->filebuf, sizeof(ctx->filebuf), "%s",	\
+		(ctx)->err = (e);					\
+		if ((e) == SPHO_ERR_SYS)				\
+			(ctx)->err_info = errno;			\
+		snprintf((ctx)->filebuf, sizeof((ctx)->filebuf),	\
 		    __FILE__);						\
-		ctx->filebuf[sizeof(ctx->filebuf) - 1] = '\0';		\
-		ctx->errline = __LINE__;				\
+		(ctx)->errline = __LINE__;				\
 	} while (0)
 
 #else /* SPHO_DEBUG */
 
-#define SPHO_ERR(ctx, err)						\
+#define SPHO_ERR(ctx, e)						\
 	do {								\
-		ctx->err = err;						\
-		if (err == SPHO_ERR_SYSTEM)				\
-			ctx->err_info = errno;				\
+		(ctx)->err = (e);					\
+		if ((e) == SPHO_ERR_SYS)				\
+			(ctx)->err_info = errno;			\
 	} while (0)
 
 #endif /* SPHO_DEBUG */
@@ -34,30 +42,40 @@
 /* debug stuff */
 #ifdef SPHO_DEBUG
 
-/* PRECOND/ASSERT/POSTCOND */
-#define SPHO_PRECOND(cond) do {                                               \
-  if (! (cond) ) {                                                            \
-    fprintf(stderr, "SPHO_PRECOND(" #cond ")@" __FILE__ ":" __LINE__          \
-      " failed. Aborting.");                                                  \
-    abort();                                                                  \
-  }                                                                           \
-} while (0)
+#define SPHO_STRINGIFY(a)	#a
+#define SPHO_MACRO_STR(b)	SPHO_STRINGIFY(b)
 
-#define SPHO_ASSERT(cond) do {                                                \
-  if (! (cond) ) {                                                            \
-    fprintf(stderr, "SPHO_ASSERT(" #cond ")@" __FILE__ ":" __LINE__           \
-      " failed. Aborting.");                                                  \
-    abort();                                                                  \
-  }                                                                           \
-} while (0)
+#define __LINE__S		SPHO_MACRO_STR(__LINE__)
 
-#define SPHO_POSTCOND(cond) do {                                              \
-  if (! (cond) ) {                                                            \
-    fprintf(stderr, "SPHO_POSTCOND(" #cond ")@" __FILE__ ":" __LINE__         \
-      " failed. Aborting.");                                                  \
-    abort();                                                                  \
-  }                                                                           \
-} while (0)
+#define SPHO_PRECOND(cond) \
+	do {								\
+		if (! (cond) ) {					\
+			fprintf(stderr, "SPHO_PRECOND(" #cond ")@"	\
+			    __FILE__ ":" __LINE__S			\
+			    " failed. Aborting.\n");			\
+			abort();					\
+		}							\
+	} while (0)
+
+#define SPHO_ASSERT(cond) \
+	do {								\
+		if (! (cond) ) {					\
+			fprintf(stderr, "SPHO_ASSERT(" #cond ")@"	\
+			    __FILE__ ":" __LINE__S			\
+			    " failed. Aborting.\n");			\
+			abort();					\
+		}							\
+	} while (0)
+
+#define SPHO_POSTCOND(cond) \
+	do {								\
+		if (! (cond) ) {					\
+			fprintf(stderr, "SPHO_POSTCOND(" #cond ")@"	\
+			    __FILE__ ":" __LINE__S			\
+			    " failed. Aborting.\n");			\
+			abort();					\
+		}							\
+	} while (0)
 
 #else
 #define SPHO_PRECOND(cond)
diff --git a/include/spho/loc.h b/include/spho/loc.h
index 05f6008..bf6e425 100644
--- a/include/spho/loc.h
+++ b/include/spho/loc.h
@@ -31,4 +31,4 @@ struct spho_loc *spho_loc_create_line(struct spho_ctx *, char *, int);
 struct spho_loc *spho_loc_create_linecol(struct spho_ctx *, char *, int, int);
 void            spho_loc_destroy(struct spho_loc *);
 
-#endif
\ No newline at end of file
+#endif
diff --git a/include/spho/scope.h b/include/spho/scope.h
new file mode 100644
index 0000000..e0d62ff
--- /dev/null
+++ b/include/spho/scope.h
@@ -0,0 +1,34 @@
+#ifndef _SPHO_SCOPE_H
+#define _SPHO_SCOPE_H
+
+#include "spho/data.h"
+
+SLIST_HEAD(spho_scope_l, spho_scope);
+
+struct spho_scope {
+	struct spho_ctx		*ctx;
+	struct spho_scope	*parent;
+
+	struct spho_scope_l	subs;
+	struct spho_nom_l	noms;
+
+	SLIST_ENTRY(spho_scope)	next;
+};
+
+#define SPHO_SC_ERR(sc, err)	SPHO_ERR((sc)->ctx, (err))
+
+int	spho_scope_init(struct spho_scope *, struct spho_ctx *,
+	    struct spho_scope *);
+void	spho_scope_term(struct spho_scope *);
+
+struct spho_scope	*spho_scope_global(struct spho_ctx *);
+struct spho_scope	*spho_scope_create(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 *);
+
+#endif /* _SPHO_SCOPE_H */
diff --git a/include/spho/spho.h b/include/spho/spho.h
index b33b975..f8582dc 100644
--- a/include/spho/spho.h
+++ b/include/spho/spho.h
@@ -1,6 +1,8 @@
 #ifndef _SPHO_SPHO_H
 #define _SPHO_SPHO_H
 
+#include <sys/queue.h>
+
 #include "spho/err.h"
 #include "spho/ctx.h"
 
diff --git a/include/spho/tp.h b/include/spho/tp.h
index 0098237..19a7ffb 100644
--- a/include/spho/tp.h
+++ b/include/spho/tp.h
@@ -3,13 +3,42 @@
 
 /* base defs */
 
-struct spho_alias {
-	struct spho_name	name;
-	struct spho_tp		*tp;
+#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_name	mname;
+	struct spho_nom		mnom;
 	struct spho_tp		*tp;
 };
 
@@ -20,21 +49,21 @@ struct tp_bin_data {
 };
 
 struct tp_box_data {
-	struct spho_tp *tp;
+	struct spho_tp *inr;
 };
 
 struct tp_forall_data {
 	struct spho_var		*var;
-	struct spho_tp		*tp;
+	struct spho_tp		*inr;
 };
 
-struct tp_alias_data {
-	struct spho_alias	*alias;
-	struct spho_tp_list	*l;
+struct tp_bappl_data {
+	struct spho_bind	*bind;
+	struct spho_tp_l	*args;
 };
 
-struct tp_const_data {
-	struct spho_const	*c;
+struct tp_konst_data {
+	const struct spho_konst	*k;
 };
 
 struct tp_var_data {
@@ -54,8 +83,8 @@ union tp_data {
 	struct tp_bin_data	binop;
 	struct tp_box_data	box;
 	struct tp_forall_data	fa;
-	struct tp_alias_data	alias;
-	struct tp_const_data	cnst;
+	struct tp_bappl_data	bappl;
+	struct tp_konst_data	konst;
 	struct tp_var_data	var;
 	struct tp_nominal_data	nom;
 	struct tp_record_data	rec;
@@ -67,8 +96,9 @@ union tp_data {
 #define SPHO_TP_FORM_CONJ	0x11
 #define SPHO_TP_FORM_IMPL	0x12
 #define SPHO_TP_FORM_BOX	0x13
-#define SPHO_TP_FORM_FORALL	0x14
-#define SPHO_TP_FORM_ALIAS	0x15
+#define SPHO_TP_FORM_ARROW	0x14
+#define SPHO_TP_FORM_FORALL	0x15
+#define SPHO_TP_FORM_BAPPL	0x16
 
 #define SPHO_TP_FORM_FALSE	0x20
 #define SPHO_TP_FORM_TRUE	0x21
@@ -77,43 +107,48 @@ union tp_data {
 
 #define SPHO_TP_FORM_REC	0x23
 
-// TODO explain
-#define SPHO_TP_FORM_SUB	0x96
+// #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 {
-	int		form;
-	union tp_data	data;
+	struct spho_scope	*sc;
+
+	int			form;
+	union tp_data		data;
+
+	STAILQ_ENTRY(spho_tp)	next;
 };
 
-struct spho_nom *spho_nom_add(struct spho_ctx *, char *, size_t);
-struct spho_nom *spho_nom_get_or_add(struct spho_ctx *, char *, size_t);
-// struct spho_nom *spho_tp_nom_get(char *, size_t);
+STAILQ_HEAD(spho_tp_l, spho_tp);
 
-struct spho_var	*spho_var_create(struct spho_ctx *, char *, size_t);
-struct spho_var	*spho_var_get(struct spho_ctx *, char *, size_t);
+#define SPHO_TP_ERR(tp, err)	SPHO_ERR((tp)->sc->ctx, (err))
 
-struct spho_alias	*spho_alias_add(struct spho_ctx *, char *, size_t);
-struct spho_alias	*spho_alias_get(struct spho_ctx *, 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_ctx *, struct spho_tp *,
-		    struct spho_tp *, struct spho_tp *);
-struct spho_tp	*spho_tp_create_conj(struct spho_ctx *, struct spho_tp *,
-		    struct spho_tp *, struct spho_tp *);
-struct spho_tp	*spho_tp_create_impl(struct spho_ctx *, struct spho_tp *,
-		    struct spho_tp *, struct spho_tp *);
-struct spho_tp	*spho_tp_create_box(struct spho_ctx *, struct spho_tp *,
-		    struct spho_tp *);
-struct spho_tp	*spho_tp_create_forall(struct spho_ctx *, struct spho_name *,
-		    struct spho_tp *);
-struct spho_tp	*spho_tp_create_alias(struct spho_ctx *, struct spho_alias *,
-		    struct spho_tp *);
-struct spho_tp	*spho_tp_create_const(struct spho_ctx *, struct spho_const *);
-struct spho_tp	*spho_tp_create_nominal(struct spho_ctx *,
-		    struct spho_nom *);
-struct spho_tp	*spho_tp_create_var(struct spho_ctx *, struct spho_var *);
-struct spho_tp	*spho_tp_create_record(struct spho_ctx *, struct spho_rec *);
-//struct spho_tp	*spho_tp_create_sub(struct spho_ctx *, struct spho_tp *,
+//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_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 *);
 
 void	spho_tp_destroy(struct spho_tp*);
diff --git a/include/spho/util.h b/include/spho/util.h
new file mode 100644
index 0000000..2871761
--- /dev/null
+++ b/include/spho/util.h
@@ -0,0 +1,18 @@
+#ifndef _SPHO_UTIL_H
+#define _SPHO_UTIL_H
+
+
+#define SPHO_UTIL_SLIST_DESTROY(l, elmtype, next, term)			\
+do {									\
+	struct elmtype *elm;						\
+	while (! SLIST_EMPTY(l)) {					\
+		elm = SLIST_FIRST(l);					\
+		SLIST_REMOVE_HEAD(l, next);				\
+		term(elm);						\
+		free(elm);						\
+	}								\
+} while (0)
+
+
+#endif
+
diff --git a/src/msph/README.md b/src/msph/README.md
new file mode 100644
index 0000000..00011ea
--- /dev/null
+++ b/src/msph/README.md
@@ -0,0 +1,93 @@
+# msph/micro sappho
+
+Micro sappho is a minimalistic language for demonstration of the SPHO type
+system. It is implemented using a simple parser and lexer that implements the
+grammar below. The indended use is to allow experimentation and familiarization
+with the SPHO types and subtyping.
+
+## Grammar
+
+Grammar in pseudo-bnf
+
+```
+
+MSph ::= Body
+
+Body ::= Dirs
+
+Dir ::= Typedef             (directives, with lack of a better name)
+      | Memberdef
+      | Nominaldecl
+      | Checkdir
+
+Typedef ::= 'type' Name '=' TExpr                   (type definition/binding)
+          | 'type' Name '[' Names ']' '=' TExpr
+          | 'type' Name                             (declaration, donno if useful)
+
+Memberdef ::= 'member' Name ':' TExpr
+
+Nominaldecl ::= 'nominal' Name
+
+Checkdir ::= 'check' TExpr '<:' TExpr
+
+TExpr ::= 'True'
+        | 'False'
+        | Var
+        | Nominal
+        | Trait
+        | TExpr '&' TExpr
+        | TExpr '|' TExpr
+        | TExpr '=>' TExpr
+        | TExpr '->' TExpr
+        | 'box' TExpr
+        | 'forall' Name '.' TExpr
+        | '(' TExpr ')'
+
+Trait ::= '{' Body '}'                  (trait, this introduces scoping)
+
+Var ::= Name                            (type variables)
+Nominal ::= Name                        (nominal type)
+
+Name ::= '[a-zA-Z0-9_]+' & !Reserved     (name/identifier)
+
+Reserved ::= 'type'                     (reserved/keywords)
+           | 'member'
+           | 'nominal'
+           | 'check'
+           | 'forall'
+           | 'box'
+           | 'True'
+           | 'False'
+```
+
+Precedence of binary operators:
+'&'  <
+'|'  <
+'->' <
+'=>'
+
+< means "binds closer"
+
+## Example
+
+A simple example msph program
+
+```
+
+nominal ExampleN
+
+type ExampleDecl
+type ExampleDecl2
+
+type Example = {
+    member example_m : C -> C
+    type FA = forall X. X -> X
+
+    type b = forall X. (box X => ExampleDecl) => ExampleDecl2
+}
+
+member example_global : Example & ExampleN
+
+type TripleConj[X, Y, Z] = X & Y & Z
+
+```
diff --git a/src/msph/msph.c b/src/msph/msph.c
new file mode 100644
index 0000000..8643a46
--- /dev/null
+++ b/src/msph/msph.c
@@ -0,0 +1,40 @@
+#include <stdio.h>
+
+
+
+#include "msph_token.h"
+
+#define PRINTERR(ctx) \
+	do { \
+		fprintf(stderr, "msph_err: %d (%d)\n", (ctx).err, (ctx).err_info); \
+	} while (0)
+
+
+int
+main(int argc, char **argv)
+{
+	int ret;
+	char *path;
+	struct msph_ctx ctx;
+	struct msph_token_stream *s;
+
+
+	if (argc != 2)
+		return (-1);
+
+
+	path = argv[1];
+
+	ctx.err = 0;
+	ctx.err_info = 0;
+
+	if ((s = msph_token_stream_fopen(&ctx, path)) == NULL) {
+		PRINTERR(ctx);
+		return (-1);
+	}
+
+
+	ret = msph_token_stream_close(s);
+
+	return (ret);
+}
diff --git a/src/msph/msph_token.c b/src/msph/msph_token.c
new file mode 100644
index 0000000..08c21aa
--- /dev/null
+++ b/src/msph/msph_token.c
@@ -0,0 +1,247 @@
+#include <sys/errno.h>
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+
+#include "spho/err.h"
+
+
+
+#define MSPH_ERR_SYS		0x0001
+#define MSPH_ERR_TOOLONG	0x0002
+
+#define MSPH_ERR(ctx, e)	SPHO_ERR(ctx, e)
+#define MSPH_TOKS_ERR(toks, e)	MSPH_ERR((toks)->ctx, e)
+
+struct msph_token_stream *
+msph_token_stream_fopen(struct msph_ctx *ctx, const char *path)
+{
+	FILE *f;
+	size_t res;
+	struct msph_token_stream *ret;
+
+	if ((f = fopen(path, "r")) == NULL) {
+		MSPH_ERR(ctx, MSPH_ERR_SYS);
+		return (NULL);
+	}
+
+	if ((ret = calloc(1, sizeof(struct msph_token_stream))) == NULL) {
+		MSPH_ERR(ctx, MSPH_ERR_SYS);
+		goto err;
+	}
+
+	ret->ctx = ctx;
+	ret->src.type = MSPH_TOKEN_SRC_FILE;
+	ret->src.inner.file.f = f;
+	ret->src.inner.file.eof = 0;
+	ret->src.inner.file.pos = ret->src.file.buf;
+	ret->src.inner.file.end = ret->src.file.buf;
+	ret->src.inner.file.read_ptr = ret->src.file.buf;
+
+	res = strlcpy(ret->src.file.name, path, sizeof(ret->src.file.name));
+	if (res >= sizeof(ret->src.file.name)) {
+		MSPH_ERR(ctx, MSPH_ERR_TOOLONG);
+		goto err;
+	}
+
+	return (ret);
+err:
+	if (fclose(f) == EOF)
+		abort();
+
+	if (ret != NULL)
+		free(ret);
+
+	return (NULL);
+}
+
+struct msph_token_stream *
+msph_token_stream_frombuf(struct msph_ctx *ctx, const char *buf, size_t len)
+{
+	struct msph_token_stream *ret;
+
+	if ((ret = calloc(1, sizeof(struct msph_token_stream))) == NULL) {
+		MSPH_ERR(ctx, MSPH_ERR_SYS);
+		return (NULL);
+	}
+
+	ret->ctx = ctx;
+	ret->type = MSPH_TOKEN_SRC_STR;
+	ret->src.str.s = buf;
+	ret->src.str.len = len;
+	ret->src.str.pos = 0;
+
+	return (ret);
+}
+
+
+int
+msph_token_stream_close(struct msph_token_stream *s)
+{
+	int ret;
+
+	ret = -1;
+
+	switch (s->type) {
+	case MSPH_TOKEN_SRC_FILE:
+		ret = fclose(s->src.file.f);
+		break;
+	case MSPH_TOKEN_SRC_STR:
+		ret = 0;
+		break;
+	default:
+		break;
+	}
+
+	return (ret);
+}
+
+
+/* -1 or num tokens read */
+ssize_t
+msph_token_stream_read_tok(struct msph_token *ptr, size_t n,
+    struct msph_token_stream *s)
+{
+	ssize_t ret;
+	size_t i;
+	int res;
+
+	ret = 0;
+	res = -1;
+	while ((res = read_single_tok(&ptr[i], s)) == 1) {
+		if (res == -1) {
+			ret = -1;
+			break;
+		}
+		ret++;
+	}
+
+	return (ret);
+}
+
+struct msph_token_matcher {
+	size_t		pos_off;
+	size_t		matchlen;
+
+	const int	tok_type;
+} msph_matcher[] = {
+	{ 0, 0, TOK_START },
+	{ 0, 0, TOK_IDENT },
+	{ 0, 0, TOK_END }
+};
+
+#define BUF_LEN(b)	(sizeof(b) / sizeof(b[0]))
+static int
+file_char_at(struct msph_ctx *ctx, struct msph_token_src *src, size_t i,
+    char *out)
+{
+	size_t nread;
+	size_t maxread;
+	struct msph_token_src_file *file;
+
+	ret = -1;
+	file = &src->inner.file;
+
+	if (file->pos + i < file->end) {
+		*out = file->buf[file->pos + i];
+		return (0);
+	}
+	if (file->end < file->pos &&
+	    ((file->pos + i) % BUF_LEN(file->buf)) < file->end) {
+		*out = file->buf[(file->pos + i) % BUF_LEN(file->buf)];
+		return (0);
+	}
+
+	if (file->eof) {
+		return (-1);
+	}
+
+	if (file->end < file->pos)
+		maxread = file->pos - file->end;
+	else
+		maxread = BUF_LEN(file->buf) - file->end;
+
+	maxread = file->end < file->pos ? file->pos - file->end :
+		BUF_LEN(file->buf) - file->end;
+
+	if (maxread == 0) {
+		MSPH_ERR(ctx, MSPH_ERR_TOOLONG);
+		return (-1);
+	}
+
+	ret = fread(&file->buf[file->end], sizeof(file->buf[0]), maxread,
+	    file->f);
+
+	if (ret == 0) {
+	       if (ferror(file->f)) {
+			MSPH_ERR(ctx, MSPH_ERR_SYS);
+			return (-1);
+	       }
+	       file->eof = 1;
+	       return (-1);
+	}
+}
+
+static int
+char_at(struct msph_token_src *src, size_t i, char *out)
+{
+	int ret;
+
+	switch (src->type) {
+	case MSPH_TOKEN_SRC_FILE:
+		ret = file_char_at(s, i, out);
+		break;
+	case MSPH_TOKEN_SRC_STR:
+		ret = str_char_at(s, i, out);
+		break;
+	default:
+		break;
+	}
+
+	return (ret);
+}
+
+static int
+tok_match(struct msph_token_matcher *m, struct msph_token_stream *s)
+{
+}
+
+static void
+tok_commit(struct msph_token *ptr, struct msph_token_stream *s,
+    struct msph_matcher *m)
+{
+	SPHO_PRECOND(p != NULL && m != NULL);
+	SPHO_PRECOND(m->matchlen != 0);
+
+}
+
+/* 1: success, 0: failed match, -1: error */
+static int
+read_single_tok(struct msph_token *ptr, struct msph_token_stream *s)
+{
+	int res;
+	size_t m;
+	size_t max_m;
+
+	max_m = 0;
+	for (m = 0; msph_matcher[m].type != TOK_END; m++) {
+		res = tok_match(&msph_matcher[m], s);
+
+		if (res == -1)
+			return (-1);
+
+		if (res == 0 &&
+		    msph_matcher[m].matchlen > msph_matcher[max_m].matchlen) {
+			max_m = m;
+		}
+	}
+
+	if (max_m == 0)
+		return (0);
+
+	tok_commit(ptr, &msph_matcher[max_m]);
+
+	return (1);
+}
+
diff --git a/src/msph/msph_token.h b/src/msph/msph_token.h
new file mode 100644
index 0000000..1e7a996
--- /dev/null
+++ b/src/msph/msph_token.h
@@ -0,0 +1,179 @@
+#ifndef _MSPH_EXPR_H
+#define _MSPH_EXPR_H
+
+/*
+ * TYPES:
+ * Conj
+ * Disj
+ * Impl
+ * Arrow
+ * Box
+ * (Sub)
+ * Forall
+ * 
+ * True
+ * False
+ * Var
+ * Nominal
+ *
+ * Record
+ *
+ * DEFINITIONS/DIRECTIVES:
+ * Type definition		(type A[X..] = T)
+ * Nominal definition		(nominal N)
+ * Member definition		(member mname : T)
+ *
+ * {
+ * member a: A
+ * member b: B
+ * }
+ *
+ * Subtyping check		(check A <: B, checks if A <: B)
+ *
+ * EXTRA DEFINITIONS
+ * Class definition		(class C[...] { ... }, shorthand)
+ * 
+ * EXPRESSIONS
+ * Conj
+ * Disj
+ * Impl
+ * Arrow
+ * Box
+ * (Sub)
+ * Forall
+ * 
+ * True
+ * False
+ * Var
+ * Nominal
+ *
+ * Trait			({ ... }, creates scoping)
+ *
+ *
+ * TOKENS
+ * lbrace		{
+ * rbrace		}
+ * lbrak		[
+ * rbrak		]
+ * lparen		(
+ * rparen		)
+ * colon		:
+ * equals		=
+ *
+ * op_and		&
+ * op_or		|
+ * op_impl		=>
+ * op_sub		<:
+ *
+ * kw_type		type
+ * kw_nominal		nominal
+ * kw_member		member
+ * kw_check		check
+ * kw_box		box
+ * kw_forall		forall
+ *
+ * k_true		True
+ * k_false		False
+ *
+ * ident		C, anid, ...
+ *
+ */
+
+struct msph_ctx {
+	int		err;
+	int		err_info;
+};
+
+enum msph_tok_type {
+	TOK_START,
+	TOK_LBRACE,		// {
+	TOK_RBRACE,		// }
+	TOK_LBRAK,		// [
+	TOK_RBRAK,		// ]
+	TOK_LPAREN,		// (
+	TOK_RPAREN,		// )
+	TOK_OP_COLON,		// :
+	TOK_OP_EQUALS,		// =
+
+	TOK_OP_AMP,		// &
+	TOK_OP_PIPE,		// |
+	TOK_OP_RARROW,		// =>
+	TOK_OP_SUB,		// <:
+
+	TOK_KW_TYPE,		// type
+	TOK_KW_NOMINAL,		// nominal
+	TOK_KW_MEMBER,		// member
+	TOK_KW_CHECK,		// check
+	TOK_KW_BOX,		// box
+	TOK_KW_FORALL,		// forall
+
+	TOK_CONST_TRUE,		// True
+	TOK_CONST_FALSE,	// False
+
+	TOK_IDENT,		// identifiers
+	TOK_END
+};
+
+#define MSPH_TOKEN_BUF_SZ	128
+
+struct token_s {
+	char	buf[MSPH_TOKEN_BUF_SZ];
+};
+
+union token_data {
+	struct token_s	s;
+};
+
+struct msph_token {
+	int			type;
+	union token_data	d;
+};
+
+#define MSPH_PATH_LEN		1024
+#define MSPH_FILE_BUF_LEN	4096
+#define MSPH_TOKEN_SRC_FILE	1
+
+struct msph_token_src_file {
+	FILE		*f;
+	int		eof;
+	size_t		pos; // TODO rename bufpos
+	size_t		end; // TODO rename bufend
+	size_t		read_pos;
+	char		buf[MSPH_FILE_BUF_LEN];
+
+	char		name[MSPH_PATH_LEN];
+};
+
+#define MSPH_TOKEN_SRC_STR	2
+struct msph_token_src_str {
+	const char	*s;
+	size_t		len;
+	size_t		pos;
+};
+
+union msph_token_src_data {
+	struct msph_token_src_file	file;
+	struct msph_token_src_str	str;
+};
+
+struct msph_token_src {
+	int				type
+	union msph_token_src_data	inner;
+};
+
+struct msph_token_stream {
+	struct msph_ctx		*ctx;
+
+	struct msph_token_src	src;
+};
+
+struct msph_token_stream	*msph_token_stream_fopen(struct msph_ctx *,
+				    const char *);
+struct msph_token_stream	*msph_token_stream_frombuf(struct msph_ctx *,
+				    const char *, size_t);
+
+int	msph_token_stream_close(struct msph_token_stream*);
+
+struct msph_token	*msph_token_source_pop(struct msph_token_stream *);
+
+#endif /* _MSPH_EXPR_H */
diff --git a/src/run/devcheck.c b/src/run/devcheck.c
index c975cc0..24c41ff 100644
--- a/src/run/devcheck.c
+++ b/src/run/devcheck.c
@@ -11,7 +11,7 @@ int main(void)
 
 	if ((ctx = spho_ctx_create()) == NULL)
 		return (-1);
-	
+
 	spho_ctx_destroy(ctx);
 
 	return (0);
diff --git a/src/spho/ctx.c b/src/spho/ctx.c
index e1a39c3..dacc076 100644
--- a/src/spho/ctx.c
+++ b/src/spho/ctx.c
@@ -4,7 +4,6 @@
 #include <stdlib.h>
 #include <string.h>
 
-#include "spho/err.h"
 #include "spho/ctx.h"
 
 static const char *spho_ctx_sys_strerror(struct spho_ctx *);
@@ -16,8 +15,11 @@ struct spho_err {
 };
 
 struct spho_err spho_errmsgs[] = {
-	{ SPHO_ERR_SYSTEM, "spho system error" },
-	{ SPHO_ERR_INTERNAL, "spho internal error" },
+	{ 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" },
 	{ -1, NULL }
 };
 
@@ -26,14 +28,20 @@ spho_ctx_create(void)
 {
 	struct spho_ctx *c;
 
+	c = NULL;
+
 	if ((c = malloc(sizeof(struct spho_ctx))) == NULL)
 		return (NULL);
 
 	c->err = 0;
 	c->err_info = 0;
 
-	SLIST_INIT(&c->noms);
-	SLIST_INIT(&c->cnsts);
+	if (spho_scope_init(&c->glob, c, NULL) == -1) {
+		free(c);
+		return (NULL);
+	}
+
+	SPHO_POSTCOND(c != NULL);
 
 	return (c);
 }
@@ -41,22 +49,11 @@ spho_ctx_create(void)
 void
 spho_ctx_destroy(struct spho_ctx *ctx)
 {
-	struct spho_nom_le *nom;
-	struct spho_cnst_le *cnst;
-
 	SPHO_PRECOND(ctx != NULL);
 
-	while (! SLIST_EMPTY(&ctx->noms)) {
-		nom = SLIST_FIRST(&ctx->noms);
-		SLIST_REMOVE_HEAD(&ctx->noms, next);
-		free(nom);
-	}
+	spho_scope_term(&ctx->glob);
 
-	while (! SLIST_EMPTY(&ctx->cnsts)) {
-		cnst = SLIST_FIRST(&ctx->cnsts);
-		SLIST_REMOVE_HEAD(&ctx->cnsts, next);
-		free(cnst);
-	}
+	free(ctx);
 }
 
 
diff --git a/src/spho/scope.c b/src/spho/scope.c
new file mode 100644
index 0000000..988e824
--- /dev/null
+++ b/src/spho/scope.c
@@ -0,0 +1,156 @@
+#include <sys/queue.h>
+
+#include <stdlib.h>
+#include <string.h>
+
+#include "spho/ctx.h"
+#include "spho/scope.h"
+#include "spho/util.h"
+
+static void spho_nom_term(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);
+
+	sc->parent = p;
+
+	return (0);
+}
+
+void
+spho_scope_term(struct spho_scope *sc)
+{
+	SPHO_UTIL_SLIST_DESTROY(&sc->subs, spho_scope, next, spho_scope_term);
+
+	SPHO_UTIL_SLIST_DESTROY(&sc->noms, spho_nom, next, spho_nom_term);
+
+	sc->parent = NULL;
+}
+
+struct spho_scope *
+spho_scope_global(struct spho_ctx *ctx)
+{
+	SPHO_PRECOND(ctx != NULL);
+
+	return (&ctx->glob);
+}
+
+
+struct spho_scope *
+spho_scope_create(struct spho_scope *sc)
+{
+	struct spho_scope *sub;
+
+	if ((sub = malloc(sizeof(struct spho_scope))) == NULL) {
+		SPHO_ERR(sc->ctx, SPHO_ERR_SYS);
+		return (NULL);
+	}
+
+	if (spho_scope_init(sub, sc->ctx, sc) == -1) {
+		free(sub);
+		return (NULL);
+	}
+
+	SLIST_INSERT_HEAD(&sc->subs, sub, next);
+
+	return (sub);
+}
+
+
+static void
+spho_nom_term(struct spho_nom *nom)
+{
+	return;
+}
+
+void
+spho_scope_destroy(struct spho_scope *sc)
+{
+	struct spho_scope *sub;
+	struct spho_scope *p;
+
+	p = sc->parent;
+	SLIST_REMOVE(&p->subs, sc, spho_scope, next);
+	spho_scope_term(sc);
+	free(sc);
+}
+
+
+struct spho_nom *
+spho_scope_nom_add(struct spho_scope *sc, const char *nomstr, size_t sz)
+{
+#ifdef SPHO_USE_STRLCPY
+	size_t res;
+#else
+	ssize_t res;
+#endif
+	struct spho_nom *nom;
+
+
+	if (spho_scope_nom_get(sc, nomstr, sz, &nom) == -1)
+		return (NULL);
+
+	if (nom != NULL) {
+		SPHO_SC_ERR(sc, SPHO_ERR_NAMEINUSE);
+		return (NULL);
+	}
+
+	if ((nom = malloc(sizeof(struct spho_nom))) == NULL) {
+		SPHO_SC_ERR(sc, SPHO_ERR_SYS);
+		return (NULL);
+	}
+
+#ifdef SPHO_USE_STRLCPY
+	res = strlcpy(nom->s, nomstr, sizeof(nom->s));
+	if (res >= sizeof(nom->s)) {
+		SPHO_SC_ERR(sc, SPHO_ERR_TOOBIG);
+		goto err;
+	}
+#else
+	res = snprintf(nom->s, sizeof(nom->s), "%s", nomstr);
+	if (res < 0) {
+		SPHO_SC_ERR(sc, SPHO_ERR_SYS);
+		goto err;
+	}
+	if (res >= (ssize_t)sizeof(nom->s)) {
+		SPHO_SC_ERR(sc, SPHO_ERR_TOOBIG);
+		goto err;
+	}
+#endif
+
+	SLIST_INSERT_HEAD(&sc->noms, nom, next);
+
+	return (nom);
+err:
+	free(nom);
+	return (NULL);
+}
+
+
+int
+spho_scope_nom_get(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;
+			break;
+		}
+	}
+
+	return (0);
+}
diff --git a/src/spho/tp.c b/src/spho/tp.c
index 74195de..e207197 100644
--- a/src/spho/tp.c
+++ b/src/spho/tp.c
@@ -1,9 +1,11 @@
+#include <sys/queue.h>
+
+#include <stdlib.h>
+
+#include "spho/ctx.h"
+#include "spho/scope.h"
 #include "spho/tp.h"
 
-struct spho_nom *
-spho_nom_add(struct spho_ctx *ctx, char *nom, size_t nomlen)
-{
-}
 
 //struct spho_tp	*
 //spho_tp_create_disj(struct spho_ctx *, struct spho_tp *, struct spho_tp *,
@@ -11,3 +13,178 @@ spho_nom_add(struct spho_ctx *ctx, char *nom, size_t nomlen)
 //{
 //
 //}
+
+
+struct spho_tp *
+spho_tp_alloc(struct spho_scope *sc, int form)
+{
+	struct spho_tp *tp;
+
+	SPHO_PRECOND(SPHO_TP_FORM_IS_VALID(form));
+
+	if ((tp = calloc(1, sizeof(struct spho_tp))) == NULL) {
+		SPHO_SC_ERR(sc, SPHO_ERR_SYS);
+		return (NULL);
+	}
+
+	tp->sc = sc;
+	tp->form = form;
+
+	return (tp);
+}
+
+
+int
+spho_tp_init_disj(struct spho_tp *tp, struct spho_tp *a, struct spho_tp *b)
+{
+	if (tp->form != SPHO_TP_FORM_DISJ) {
+		SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
+		return (-1);
+	}
+
+	tp->data.binop.left = a;
+	tp->data.binop.right = b;
+
+	return (0);
+}
+
+int
+spho_tp_init_conj(struct spho_tp *tp, struct spho_tp *a, struct spho_tp *b)
+{
+	if (tp->form != SPHO_TP_FORM_CONJ) {
+		SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
+		return (-1);
+	}
+
+	tp->data.binop.left = a;
+	tp->data.binop.right = b;
+
+	return (0);
+}
+
+int
+spho_tp_init_impl(struct spho_tp *tp, struct spho_tp *a, struct spho_tp *b)
+{
+	if (tp->form != SPHO_TP_FORM_IMPL) {
+		SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
+		return (-1);
+	}
+
+	tp->data.binop.left = a;
+	tp->data.binop.right = b;
+
+	return (0);
+}
+
+int
+spho_tp_init_arrow(struct spho_tp *tp, struct spho_tp *a, struct spho_tp *b)
+{
+	if (tp->form != SPHO_TP_FORM_ARROW) {
+		SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
+		return (-1);
+	}
+
+	tp->data.binop.left = a;
+	tp->data.binop.right = b;
+
+	return (0);
+}
+
+int
+spho_tp_init_box(struct spho_tp *tp, struct spho_tp *inr)
+{
+	if (tp->form != SPHO_TP_FORM_BOX) {
+		SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
+		return (-1);
+	}
+
+	tp->data.box.inr = inr;
+
+	return (0);
+}
+
+int
+spho_tp_init_forall(struct spho_tp *tp, struct spho_var *var,
+    struct spho_tp *inr)
+{
+	if (tp->form != SPHO_TP_FORM_FORALL) {
+		SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
+		return (-1);
+	}
+
+	tp->data.fa.var = var;
+	tp->data.fa.inr = inr;
+
+	return (0);
+}
+
+int
+spho_tp_init_bappl(struct spho_tp *tp, struct spho_bind *bind,
+    struct spho_tp_l *args)
+{
+	struct spho_tp *arg;
+
+	if (tp->form != SPHO_TP_FORM_BAPPL) {
+		SPHO_TP_ERR(tp, SPHO_ERR_ARGINVAL);
+		return (-1);
+	}
+
+	tp->data.bappl.bind = bind;
+	tp->data.bappl.args = args;
+
+	return (0);
+}
+
+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);
+}
+
+