parsing prefix version (binary operators) of msph

.clangd

@@ -0,0 +1,2 @@
+Diagnostics:
+  UnusedIncludes: None

.gitignore

@@ -51,9 +51,11 @@ Module.symvers
 Mkfile.old
 dkms.conf
 
-# CMake build directory
-build/
+# CMake build dirs
+build-*/
 
+# CMake compile commands
+compile_commands.json
 
 # vim
 .*.swp

CMakeLists.txt

@@ -3,6 +3,17 @@ project(log-e-sappho C)
 
 set(CMAKE_C_STANDARD 99)
 set(CMAKE_C_STANDARD_REQUIRED True)
+string(JOIN " " CMAKE_C_FLAGS
+	"-Wall -Wextra -Wformat=2"
+       "-Wconversion -Wsign-conversion -Wimplicit-fallthrough"
+       "-Werror=implicit -Werror=incompatible-pointer-types"
+       "-Werror=int-conversion")
+set(CMAKE_VERBOSE_MAKEFILE ON)
+
+set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
+
+
+include(CheckSymbolExists)
 
 set(INCLUDE_DIR include)
 set(SRC_DIR src)
@@ -10,21 +21,56 @@ 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/token.c
+	${SRC_DIR}/msph/tree.c
+	${SRC_DIR}/msph/msph.c
+)
+
+set(MSPH_HEADER
+	${INCLUDE_DIR}/msph/token.h
+	${INCLUDE_DIR}/msph/tree.h
+	${INCLUDE_DIR}/msph/common.h
+	${INCLUDE_DIR}/msph/err.h
+)
+
+add_executable(msph ${MSPH_SRC} ${MSPH_HEADER})
+target_include_directories(msph PRIVATE ${INCLUDE_DIR})
+target_link_libraries(msph spho)
+target_compile_definitions(msph PRIVATE
+	$<$<CONFIG:Debug>:SPHO_DEBUG>
+	$<$<BOOL:${HAVE_STRLCPY}>:SPHO_USE_STRLCPY>
+)

example/ex1.msph

@@ -0,0 +1,4 @@
+
+nominal C
+
+

example/ex2.msph

@@ -0,0 +1 @@
+type A = & C D

example/ex3.msph

@@ -0,0 +1,13 @@
+
+type X = & C (| D E)
+
+type Y = {
+	member x : X
+	type Z = & X {
+ 		type T = C
+		assert C <: D
+	}
+	member r : (box forall S. (=> S Y))
+	member s : C[X, Y, z]
+	member f : -> A B
+}

include/msph/common.h

@@ -0,0 +1,25 @@
+#ifndef _MSPH_COMMON_H
+#define _MSPH_COMMON_H
+
+#include "msph/err.h"
+
+#define MSPH_IDENT_LEN	128
+#define MSPH_NAME_LEN	1024
+
+struct msph_ctx {
+	int	err;
+	int	err_info;
+	char	errbuf[SPHO_ERR_BUF_LEN];
+
+#ifdef SPHO_DEBUG
+	char	filebuf[SPHO_ERR_FILEBUF_LEN];
+	int	errline;
+#endif
+};
+
+struct msph_text_pos {
+	unsigned int	line;
+	unsigned int	col;
+};
+
+#endif

include/msph/err.h

@@ -0,0 +1,36 @@
+#ifndef _MSPH_ERR_H
+#define _MSPH_ERR_H
+
+#include "spho/err.h"
+
+
+#define MSPH_ERR_SYS		0x0001
+#define MSPH_ERR_INVAL		0x0002
+#define MSPH_ERR_TOOLONG	0x0003
+
+#define MSPH_ERR_TOKEN_TOOLONG	0x1001
+#define MSPH_ERR_TOKEN_EOF	0x1002
+#define MSPH_ERR_TOKEN_NOMATCH	0x1003
+#define MSPH_ERR_TOKEN_INVAL	0x1004
+
+#define MSPH_ERR_TREE_TOOLONG	0x2001
+#define MSPH_ERR_TREE_EOF	0x2002
+#define MSPH_ERR_TREE_NOMATCH	0x2003
+
+
+// TODO add more diagnostics
+
+#define MSPH_ERR(ctx, e)	SPHO_ERR(ctx, e)
+#define MSPH_TOKS_ERR(toks, e)	MSPH_ERR((toks)->ctx, e)
+
+#define MSPH_ERR_INFO(ctx, e, info)	SPHO_ERR_INFO(ctx, e, info)
+
+
+#define MSPH_ERR_RESET(ctx) \
+	do { \
+		ctx->err = 0; \
+		ctx->err_info = 0; \
+	} while (0)
+
+
+#endif

include/msph/token.h

@@ -0,0 +1,146 @@
+#ifndef _MSPH_EXPR_H
+#define _MSPH_EXPR_H
+
+#include <sys/queue.h>
+
+#include "msph/common.h"
+
+/*
+ *
+ *
+ * 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, ...
+ *
+ */
+
+
+enum msph_tok_type {
+	TOK_LBRACE,		// {
+	TOK_RBRACE,		// }
+	TOK_LBRAK,		// [
+	TOK_RBRAK,		// ]
+	TOK_LPAREN,		// (
+	TOK_RPAREN,		// )
+	TOK_COLON,		// :
+	TOK_EQUALS,		// =
+	TOK_COMMA,		// ,
+	TOK_DOT,		// .
+
+	TOK_AMP,		// &
+	TOK_PIPE,		// |
+	TOK_IMPL,		// =>
+	TOK_RARROW,		// ->
+	TOK_SUB,		// <:
+
+	TOK_KW_TYPE,		// type
+	TOK_KW_NOMINAL,		// nominal
+	TOK_KW_MEMBER,		// member
+	TOK_KW_ASSERT,		// assert
+	TOK_KW_BOX,		// box
+	TOK_KW_FORALL,		// forall
+
+	TOK_CONST_TRUE,		// True
+	TOK_CONST_FALSE,	// False
+
+	TOK_IDENT,		// identifiers
+	TOK_INVAL,		// special: invalid, use to mark invalid toks
+	TOK_WSPACE,		// special: whitespace
+	TOK_END			// special: end of array/token stream
+};
+
+#define MSPH_TAB_WIDTH		8
+
+union msph_token_data {
+	char	str[MSPH_IDENT_LEN];
+};
+
+struct msph_token {
+	int			type;
+	struct msph_text_pos	pos;
+	union msph_token_data	data;
+
+	SLIST_ENTRY(msph_token)	entries;
+};
+
+#define MSPH_FILE_NAME_LEN	1024
+#define MSPH_FILE_BUF_LEN	2048
+#define MSPH_TOKEN_SRC_FILE	1
+
+struct msph_token_src_file {
+	FILE		*f;
+
+	/* circular buffer for reading */
+	size_t		pos;
+	size_t		end;
+	char		buf[MSPH_FILE_BUF_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;
+	struct msph_text_pos		pos;
+	union msph_token_src_data	inner;
+};
+
+struct msph_token_stream {
+	struct msph_ctx		*ctx;
+
+	char			name[MSPH_NAME_LEN];
+	struct msph_token_src	src;
+};
+
+void msph_ctx_init(struct msph_ctx *);
+
+struct msph_token_stream	*msph_token_stream_file(struct msph_ctx *,
+				    const char *, FILE *);
+struct msph_token_stream	*msph_token_stream_frombuf(struct msph_ctx *,
+				    const char *, const char *, size_t);
+
+int	msph_token_stream_close(struct msph_token_stream*);
+
+ssize_t	msph_token_stream_read(struct msph_token *, size_t,
+	    struct msph_token_stream *);
+int	msph_token_stream_eof(struct msph_token_stream *);
+int	msph_token_stream_print(struct msph_token_stream *, FILE *);
+
+ssize_t	msph_token_str(char *, size_t, struct msph_token *);
+
+struct msph_token *	msph_token_copy(struct msph_ctx *, struct msph_token *);
+
+
+#endif /* _MSPH_EXPR_H */

include/msph/tree.h

@@ -0,0 +1,257 @@
+#ifndef _MSPH_TREE_H
+#define _MSPH_TREE_H
+
+#include <sys/queue.h>
+
+#include "msph/common.h"
+#include "msph/token.h"
+
+/*
+ * TYPES:
+ * Conj
+ * Disj
+ * Impl
+ * Arrow
+ * Box
+ * (Sub)
+ * Forall
+ *
+ * True
+ * False
+ * Var
+ * Nominal
+ *
+ * Record
+ *
+ * DEFINITIONS/DIRECTIVES:
+ * Type definition             (type A[X..] = T)
+ * Nominal definition          (nominal N)
+ * Member definition           (member mname : T)
+ *
+ * {
+ * member a: A
+ * member b: B
+ * }
+ *
+ * Subtyping assert             (assert A <: B, asserts that A <: B)
+ *
+ * EXTRA DEFINITIONS
+ * Class definition            (class C[...] { ... }, shorthand)
+ *
+ * EXPRESSIONS
+ * Conj
+ * Disj
+ * Impl
+ * Arrow
+ * Box
+ * (Sub)
+ * Forall
+ *
+ * True
+ * False
+ * Var
+ * Nominal
+ *
+ * Trait                       ({ ... }, creates scoping)
+ */
+
+#define MSPH_TREE_ROOT		0x0000
+#define MSPH_TREE_UNIT		0x0001
+
+#define MSPH_TREE_BODY		0x0010
+
+#define MSPH_TREE_DIR		0x0020
+#define MSPH_TREE_TPDEF		0x0021
+#define MSPH_TREE_NOMINDECL	0x0022
+#define MSPH_TREE_MEMBDECL	0x0023
+#define MSPH_TREE_ASSERT	0x0024
+
+#define MSPH_TREE_TPEXPR	0x0040
+#define MSPH_TREE_TRUE		0x0041
+#define MSPH_TREE_FALSE		0x0042
+#define MSPH_TREE_NAME		0x0043
+#define MSPH_TREE_APPL		0x0044
+#define MSPH_TREE_TRAIT		0x0045
+#define MSPH_TREE_CONJ		0x0046
+#define MSPH_TREE_DISJ		0x0047
+#define MSPH_TREE_IMPL		0x0048
+#define MSPH_TREE_ARROW		0x0049
+#define MSPH_TREE_BOX		0x004a
+#define MSPH_TREE_FORALL	0x004b
+#define MSPH_TREE_PAREN		0x004c
+
+#define MSPH_TREE_IDENT		0x0100
+
+
+struct msph_tree {
+	int			type;
+	struct msph_tree	*parent;
+};
+
+struct msph_tree_root;
+struct msph_tree_text;
+struct msph_tree_body;
+struct msph_tree_dir;
+struct msph_tree_tpdef;
+struct msph_tree_nomindecl;
+struct msph_tree_assert;
+struct msph_tree_ident;
+struct msph_tree_tpexpr;
+
+struct msph_tree_root {
+	struct msph_tree	tr;
+
+	struct msph_ctx		*ctx;
+
+	STAILQ_HEAD(msph_tree_unit_l, msph_tree_unit)	head;
+};
+
+struct msph_tree_unit {
+	struct msph_tree	tr;
+
+	char			name[MSPH_NAME_LEN];
+	struct msph_tree_body	*body;
+	STAILQ_ENTRY(msph_tree_unit)	entries;
+};
+
+struct msph_tree_text {
+	struct msph_tree	tr;
+	struct msph_text_pos	pos;
+};
+
+struct msph_tree_body {
+	struct msph_tree		tr;
+
+	STAILQ_HEAD(msph_tree_dir_l, msph_tree_dir)	head;
+};
+
+struct msph_tree_dir {
+	struct msph_tree		tr;
+
+	STAILQ_ENTRY(msph_tree_dir)	entries;
+};
+
+struct msph_tree_tpdef {
+	struct msph_tree_dir		dir;
+
+	struct msph_tree_ident		*id;
+	struct msph_tree_tpexpr		*tp;
+};
+
+struct msph_tree_nomindecl {
+	struct msph_tree_dir	dir;
+
+	struct msph_tree_ident	*id;
+};
+
+struct msph_tree_membdecl {
+	struct msph_tree_dir	dir;
+
+	struct msph_tree_ident	*id;
+	struct msph_tree_tpexpr	*tp;
+};
+
+struct msph_tree_assert {
+	struct msph_tree_dir	dir;
+
+	struct msph_tree_tpexpr	*ltp;
+	struct msph_tree_tpexpr	*rtp;
+};
+
+struct msph_tree_tpexpr {
+	struct msph_tree		tr;
+
+	STAILQ_ENTRY(msph_tree_tpexpr)	entries;
+};
+
+
+struct msph_tree_true {
+	struct msph_tree_tpexpr	tp;
+};
+
+struct msph_tree_false {
+	struct msph_tree_tpexpr	tp;
+};
+
+struct msph_tree_name {
+	struct msph_tree_tpexpr	tp;
+
+	struct msph_tree_ident	*id;
+};
+
+struct msph_tree_appl {
+	struct msph_tree_tpexpr	tp;
+
+	struct msph_tree_ident	*id;
+	STAILQ_HEAD(msph_tree_tpexpr_l, msph_tree_tpexpr) head;
+};
+
+struct msph_tree_trait {
+	struct msph_tree_tpexpr	tp;
+
+	struct msph_tree_body	*body;
+};
+
+struct msph_tree_conj {
+	struct msph_tree_tpexpr	tp;
+
+	struct msph_tree_tpexpr	*ltp;
+	struct msph_tree_tpexpr	*rtp;
+};
+
+struct msph_tree_disj {
+	struct msph_tree_tpexpr	tp;
+
+	struct msph_tree_tpexpr	*ltp;
+	struct msph_tree_tpexpr	*rtp;
+};
+
+struct msph_tree_impl {
+	struct msph_tree_tpexpr	tp;
+
+	struct msph_tree_tpexpr	*ltp;
+	struct msph_tree_tpexpr	*rtp;
+};
+
+struct msph_tree_arrow {
+	struct msph_tree_tpexpr	tp;
+
+	struct msph_tree_tpexpr	*ltp;
+	struct msph_tree_tpexpr	*rtp;
+};
+
+struct msph_tree_box {
+	struct msph_tree_tpexpr	tp;
+
+	struct msph_tree_tpexpr	*inner;
+};
+
+struct msph_tree_forall {
+	struct msph_tree_tpexpr	tp;
+
+	struct msph_tree_ident	*ident;
+	struct msph_tree_tpexpr	*inner;
+};
+
+struct msph_tree_paren {
+	struct msph_tree_tpexpr	tp;
+
+	struct msph_tree_tpexpr	*inner;
+};
+
+struct msph_tree_ident {
+	struct msph_tree tr;
+
+	char str[MSPH_IDENT_LEN];
+	STAILQ_ENTRY(msph_tree_ident) entries;
+};
+
+
+
+struct msph_tree_root	*msph_tree_makeroot(struct msph_ctx *);
+
+int	msph_tree_parse(struct msph_token_stream *, struct msph_tree_root *);
+
+ssize_t	msph_tree_fprint(FILE *, struct msph_tree *);
+
+#endif

include/spho/ctx.h

@@ -1,25 +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 *);
-char			*spho_ctx_strerror(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

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_const_le {
-	struct spho_cnst		cnst;
-	SLIST_ENTRY(spho_const_le)	next;
-};
+SLIST_HEAD(spho_nom_l, spho_nom);
 
 
-SLIST_HEAD(spho_nom_l, spho_nom_le);
-SLIST_HEAD(spho_const_l, spho_const_le);
-
-#endif
+#endif /* _SPHO_DATA_H */

include/spho/err.h

@@ -1,67 +1,107 @@
 #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)
+
+#define SPHO_ERR_BUF_LEN	2048
+
+#define SPHO_ERR(ctx, e)						\
+	do {								\
+		(ctx)->err = (e);					\
+		if ((e) == SPHO_ERR_SYS)				\
+			SPHO_ERR_INFO(ctx, e, errno);			\
+		else							\
+			SPHO_ERR_INFO(ctx, e, 0);			\
+	} while (0)
 
 #ifdef SPHO_DEBUG
 
-#define SPHO_ERR(ctx, err)						\
+#define SPHO_ERR_FILEBUF_LEN	128
+
+#define SPHO_ERR_INFO(ctx, e, info)					\
 	do {								\
-		ctx->err = err;						\
-		if (err == SPHO_ERR_SYSTEM)				\
-			ctx->err_info = errno;				\
-		snprintf(ctx->filebuf, sizeof(ctx->filebuf), "%s",	\
+		(ctx)->err = (e);					\
+		(ctx)->err_info = (info);				\
+		snprintf((ctx)->filebuf, sizeof((ctx)->filebuf),	\
 		    __FILE__);						\
-		ctx->errline = __LINE__;				\
+		(ctx)->errline = __LINE__;				\
 	} while (0)
 
+#define SPHO_STRINGIFY(a)	#a
+#define SPHO_MACRO_STR(b)	SPHO_STRINGIFY(b)
+
+#define __LINE__S		SPHO_MACRO_STR(__LINE__)
+
+#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)
+
+
+#ifdef SPHO_ENABLE_DEBUG_PRINT
+
+#define SPHO_DEBUG_PRINT(fmt, ...) \
+	do { \
+		fprintf(stderr, fmt __VA_OPT__(,) __VA_ARGS__); \
+	} while (0)
+
+#else /* SPHO_ENABLE_DEBUG_PRINT */
+
+#define SPHO_DEBUG_PRINT(fmt, ...)
+
+#endif /* SPHO_ENABLE_DEBUG_PRINT */
+
 #else /* SPHO_DEBUG */
 
-#define SPHO_ERR(ctx, err)						\
+#define SPHO_ERR_INFO(ctx, e, info)					\
 	do {								\
-		ctx->err = err;						\
-		if (err == SPHO_ERR_SYSTEM)				\
-			ctx->err_info = errno;				\
+		(ctx)->err = (e);					\
+		(ctx)->err_info = (info);				\
 	} while (0)
 
-#endif /* SPHO_DEBUG */
-
-/* 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_ASSERT(cond) do {                                                \
-  if (! (cond) ) {                                                            \
-    fprintf(stderr, "SPHO_ASSERT(" #cond ")@" __FILE__ ":" __LINE__           \
-      " failed. Aborting.");                                                  \
-    abort();                                                                  \
-  }                                                                           \
-} while (0)
-
-#define SPHO_POSTCOND(cond) do {                                              \
-  if (! (cond) ) {                                                            \
-    fprintf(stderr, "SPHO_POSTCOND(" #cond ")@" __FILE__ ":" __LINE__         \
-      " failed. Aborting.");                                                  \
-    abort();                                                                  \
-  }                                                                           \
-} while (0)
-
-#else
 #define SPHO_PRECOND(cond)
 #define SPHO_ASSERT(cond)
 #define SPHO_POSTCOND(cond)
-#endif
+#define SPHO_DEBUG_PRINT(fmt, ...)
 
-#endif
+#endif /* SPHO_DEBUG */
+
+#endif /* _SPHO_ERR_H */

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
+#endif

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 */

include/spho/spho.h

@@ -4,29 +4,6 @@
 #include <sys/queue.h>
 
 #include "spho/err.h"
-
-#include "spho/data.h"
-
-#define SPHO_ERR_BUF_LEN	2048
-#define SPHO_ERR_FILEBUF_LEN	128
-
-struct spho_ctx {
-	int	err;
-	int	err_info;
-
-	struct spho_nom_l	noms;
-	struct spho_const_l	cnsts;
-
-#ifdef SPHO_DEBUG
-	char filebuf[SPHO_ERR_FILEBUF_LEN];
-	int errline;
-#else
-	char errbuf[SPHO_ERR_BUF_LEN];
-#endif
-};
-
-struct spho_ctx		*spho_ctx_create(void);
-void			spho_ctx_destroy(struct spho_ctx *);
-char			*spho_ctx_strerror(struct spho_ctx *);
+#include "spho/ctx.h"
 
 #endif

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,10 +83,10 @@ 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_nominal_data	nom; // XXX
 	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,49 @@ 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);
 
-struct spho_alias	*spho_alias_add(struct spho_ctx *, char *, size_t);
-struct spho_alias	*spho_alias_get(struct spho_ctx *, char *, size_t);
+#define SPHO_TP_ERR(tp, err)	SPHO_ERR((tp)->sc->ctx, (err))
 
-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_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_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*);

include/spho/util.h

@@ -0,0 +1,25 @@
+#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)
+
+#ifdef SPHO_USE_STRLCPY
+#define SPHO_STRLCPY(dst, src, len)	strlcpy(dst, src, len)
+#else
+#define SPHO_STRLCPY(dst, src, len) \
+	(size_t)snprintf(dst, len, "%s", src)
+#endif
+
+
+#endif
+

src/msph/README.md

@@ -0,0 +1,105 @@
+# 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
+
+And yes, it is ambiguous at places. More specification coming when there is
+time.
+
+```
+
+MSph ::= Body
+
+Body ::= Dirs
+
+Dir ::= Typedef             (directives, with lack of a better name)
+      | Memberdef
+      | Nominaldecl
+      | Assert
+
+Typedef ::= 'type' Name '=' TExpr                   (type definition/binding)
+          | 'type' Name '[' Names ']' '=' TExpr
+          | 'type' Name                             (declaration, donno if useful)
+
+Memberdef ::= 'member' Name ':' TExpr
+
+Nominaldecl ::= 'nominal' Name
+
+Assert ::= 'assert' TExpr '<:' TExpr
+
+TExpr ::= 'True'
+        | 'False'
+        | Var
+        | Nominal
+        | Trait
+        | Appl
+        | 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)
+Appl ::= Name '[' TExprs ']'
+
+Name ::= '[a-zA-Z0-9_]+' & !Reserved     (name/identifier)
+
+Reserved ::= 'type'                     (reserved/keywords)
+           | 'member'
+           | 'nominal'
+           | 'assert'
+           | '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
+
+assert Example <: ExampleN
+
+```
+
+// A <: B => ...
+// ==
+// box (A => B) => ...
+

src/msph/msph.c

@@ -0,0 +1,151 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include <unistd.h>
+
+#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)
+
+struct msph_opts {
+	int		tokenize_only;
+	const char	*in_path;
+	const char	*out_path;
+} run_opts = {
+	0,
+	NULL,
+	NULL
+};
+
+
+#define USAGE \
+	"msph: micro sappho\n" \
+	"\tUsage: msph [-t] [-o out_path] [in_path]\n" \
+	"\n" \
+	"\t-t	- print tokenization\n" \
+	"\t-o	- output path\n"
+
+
+void
+print_usage(void)
+{
+	printf("%s", USAGE);
+}
+
+int run(struct msph_opts *);
+
+int
+main(int argc, char *argv[])
+{
+	int opt;
+
+	while ((opt = getopt(argc, argv, "hto:")) != -1) {
+		switch (opt) {
+		case 't':
+			run_opts.tokenize_only = 1;
+			break;
+		case 'o':
+			run_opts.out_path = optarg;
+			break;
+		case 'h':
+			print_usage();
+			exit(EXIT_SUCCESS);
+		case '?':
+		default:
+			print_usage();
+			exit(EXIT_FAILURE);
+		}
+	}
+
+	argc -= optind;
+	argv += optind;
+
+	if (argc > 1) {
+		print_usage();
+		exit(EXIT_FAILURE);
+	}
+
+	if (argc == 1)
+		run_opts.in_path = argv[0];
+
+	if (run(&run_opts))
+		exit(EXIT_FAILURE);
+}
+
+
+int
+run(struct msph_opts *opts)
+{
+	int ret;
+	struct msph_ctx ctx;
+	struct msph_token_stream *s;
+	struct msph_tree_root *root;
+	FILE *in, *out;
+
+	in = out = NULL;
+
+	msph_ctx_init(&ctx);
+
+	if (opts->in_path == NULL) {
+		in = stdin; opts->in_path = "stdin";
+	} else {
+		if ((in = fopen(opts->in_path, "r")) == NULL) {
+			MSPH_ERR(&ctx, MSPH_ERR_SYS);
+			goto err;
+		}
+	}
+
+	if (opts->out_path == NULL) {
+		out = stdout;
+	} else {
+		if ((out = fopen(opts->out_path, "w")) == NULL) {
+			MSPH_ERR(&ctx, MSPH_ERR_SYS);
+			goto err;
+		}
+	}
+
+	if ((s = msph_token_stream_file(&ctx, opts->in_path, in)) == NULL) {
+		goto err;
+	}
+
+	printf("msph v0, parsing %s\n", opts->in_path);
+
+	if (opts->tokenize_only) {
+		if ((ret = msph_token_stream_print(s, out)) == -1)
+			goto err;
+
+		goto exit;
+	}
+
+	if ((root = msph_tree_makeroot(&ctx)) == NULL) {
+		goto err;
+	}
+
+	if (msph_tree_parse(s, root) == -1)
+		goto err;
+
+	printf("msph tree successfully parsed :)\n");
+
+	if (msph_tree_fprint(out, (struct msph_tree *)root) < 0)
+		goto err;
+
+exit:
+	if (msph_token_stream_close(s) == -1)
+		goto err;
+
+	return (0);
+
+err:
+	PRINTERR(ctx);
+
+	if (in)
+		fclose(in);
+	if (out)
+		fclose(out);
+	return (-1);
+}

src/msph/token.c

@@ -0,0 +1,784 @@
+#include <sys/errno.h>
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+#include <ctype.h>
+
+#include "msph/err.h"
+#include "msph/token.h"
+
+struct msph_matcher {
+	size_t		off;
+	size_t		matchlen;
+
+	const int	type;
+};
+
+struct msph_matcher token_matchers[] = {
+	{ 0, 0, -1 },
+	{ 0, 0, TOK_LBRACE },
+	{ 0, 0, TOK_RBRACE },
+	{ 0, 0, TOK_LBRAK },
+	{ 0, 0, TOK_RBRAK },
+	{ 0, 0, TOK_LPAREN },
+	{ 0, 0, TOK_RPAREN },
+	{ 0, 0, TOK_COLON },
+	{ 0, 0, TOK_EQUALS },
+	{ 0, 0, TOK_COMMA },
+	{ 0, 0, TOK_DOT },
+
+	{ 0, 0, TOK_AMP },
+	{ 0, 0, TOK_PIPE },
+	{ 0, 0, TOK_IMPL },
+	{ 0, 0, TOK_RARROW },
+	{ 0, 0, TOK_SUB },
+
+	{ 0, 0, TOK_KW_TYPE },
+	{ 0, 0, TOK_KW_NOMINAL },
+	{ 0, 0, TOK_KW_MEMBER },
+	{ 0, 0, TOK_KW_ASSERT },
+	{ 0, 0, TOK_KW_BOX },
+	{ 0, 0, TOK_KW_FORALL },
+
+	{ 0, 0, TOK_CONST_TRUE },
+	{ 0, 0, TOK_CONST_FALSE },
+
+	{ 0, 0, TOK_IDENT },
+	{ 0, 0, TOK_END }
+};
+struct msph_matcher wspace = { 0, 0, TOK_WSPACE };
+
+struct msph_token_info {
+	const int type;
+	const char *dbg_str;
+	const char *str;
+} token_info[] = {
+#define TOK_INFO(tok, s)	{ tok , #tok, s }
+	TOK_INFO(TOK_LBRACE, "{"),
+	TOK_INFO(TOK_RBRACE, "}"),
+	TOK_INFO(TOK_LBRAK, "["),
+	TOK_INFO(TOK_RBRAK, "]"),
+	TOK_INFO(TOK_LPAREN, "("),
+	TOK_INFO(TOK_RPAREN, ")"),
+	TOK_INFO(TOK_COLON, ":"),
+	TOK_INFO(TOK_EQUALS, "="),
+	TOK_INFO(TOK_COMMA, ","),
+	TOK_INFO(TOK_DOT, "."),
+
+	TOK_INFO(TOK_AMP, "&"),
+	TOK_INFO(TOK_PIPE, "|"),
+	TOK_INFO(TOK_IMPL, "=>"),
+	TOK_INFO(TOK_RARROW, "->"),
+	TOK_INFO(TOK_SUB, "<:"),
+
+	TOK_INFO(TOK_KW_TYPE, "type"),
+	TOK_INFO(TOK_KW_NOMINAL, "nominal"),
+	TOK_INFO(TOK_KW_MEMBER, "member"),
+	TOK_INFO(TOK_KW_ASSERT, "assert"),
+	TOK_INFO(TOK_KW_BOX, "box"),
+	TOK_INFO(TOK_KW_FORALL, "forall"),
+
+	TOK_INFO(TOK_CONST_TRUE, "True"),
+	TOK_INFO(TOK_CONST_FALSE, "False"),
+
+	TOK_INFO(TOK_IDENT, NULL),
+	{ TOK_END , NULL, NULL }
+#undef TOK_INFO
+};
+
+
+
+#define BUF_LEN(b)	((sizeof(b) / sizeof((b)[0])))
+
+static ssize_t	src_file_fill_buf(struct msph_ctx *,
+		    struct msph_token_src_file *);
+static int	tok_match(struct msph_ctx *, struct msph_token_src *,
+		    struct msph_matcher *);
+static int	tok_commit(struct msph_ctx *, struct msph_token_src *, 
+		    struct msph_matcher *, struct msph_token *);
+static void	tok_update_pos(struct msph_ctx *, struct msph_token_src *,
+		    struct msph_matcher *m);
+static int	char_at(struct msph_ctx *, struct msph_token_src *, size_t,
+		    char *);
+static int	fromcbuf_charcpy(char *, const char *, size_t, size_t, size_t);
+static int	file_char_at(struct msph_ctx *, struct msph_token_src *, size_t,
+		    char *out);
+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)
+{
+	size_t res;
+	struct msph_token_stream *ret;
+
+	if (ctx == NULL || f == NULL) {
+		MSPH_ERR(ctx, MSPH_ERR_INVAL);
+		return (NULL);
+	}
+
+
+	if ((ret = calloc(1, sizeof(struct msph_token_stream))) == NULL) {
+		MSPH_ERR(ctx, MSPH_ERR_SYS);
+		goto err;
+	}
+
+	ret->ctx = ctx;
+	if ((res = strlcpy(ret->name, name, BUF_LEN(ret->name)))
+	    >= BUF_LEN(ret->name)) {
+		MSPH_ERR(ctx, MSPH_ERR_TOOLONG);
+		goto err;
+	}
+	ret->src.type = MSPH_TOKEN_SRC_FILE;
+	ret->src.pos = (struct msph_text_pos) { .line = 1, .col = 1 };
+	ret->src.inner.file.f = f;
+	ret->src.inner.file.pos = 0;
+	ret->src.inner.file.end = 0;
+
+	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 *name,
+    const char *buf, size_t len)
+{
+	size_t res;
+	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;
+	if ((res = strlcpy(ret->name, name, BUF_LEN(ret->name)))
+	    >= BUF_LEN(ret->name)) {
+		MSPH_ERR(ctx, MSPH_ERR_TOOLONG);
+		goto err;
+	}
+	ret->src.type = MSPH_TOKEN_SRC_STR;
+	ret->src.pos = (struct msph_text_pos) { .line = 1, .col = 1 };
+	ret->src.inner.str.s = buf;
+	ret->src.inner.str.len = strnlen(buf, len);
+	ret->src.inner.str.pos = 0;
+
+	return (ret);
+
+err:
+	free(ret);
+
+	return (NULL);
+}
+
+ssize_t
+msph_token_str(char *buf, size_t len,
+    struct msph_token *tok)
+{
+	ssize_t ret;
+	const char *base;
+
+	base = tok_base_str(tok);
+	if (base == NULL) {
+		return (-1);
+	}
+	ret = (ssize_t)snprintf(buf, len, "%s", base);
+
+	if (ret < 0 || ret >= (ssize_t)len)
+		return (ret);
+
+	len -= (size_t)ret;
+	buf += ret;
+
+	switch (tok->type) {
+	case TOK_IDENT:
+		ret += (ssize_t)snprintf(buf, len, "(%s)", tok->data.str);
+		break;
+	default:
+		break;
+	}
+
+	return (ret);
+}
+
+#define MSPH_TOKEN_PRINT_BUF_LEN	2 * MSPH_IDENT_LEN
+int
+msph_token_stream_print(struct msph_token_stream *s, FILE *out)
+{
+	ssize_t ret;
+	struct msph_token tok;
+	char tokstr[MSPH_TOKEN_PRINT_BUF_LEN];
+
+	while ((ret = msph_token_stream_read(&tok, 1, s)) > 0) {
+
+		ret = msph_token_str(tokstr, BUF_LEN(tokstr), &tok);
+		if (ret < 0) {
+			MSPH_ERR_INFO(s->ctx, MSPH_ERR_TOKEN_INVAL, tok.type);
+			break;
+		}
+
+		if ((size_t)ret < BUF_LEN(tokstr))
+			fprintf(out, "%s\n", tokstr);
+		else
+			fprintf(out, "%s...(trunkated)", tokstr);
+	}
+
+	return ((int)ret);
+}
+
+
+int
+msph_token_stream_close(struct msph_token_stream *s)
+{
+	int ret;
+
+	ret = -1;
+
+	switch (s->src.type) {
+	case MSPH_TOKEN_SRC_FILE:
+		ret = fclose(s->src.inner.file.f);
+		break;
+	case MSPH_TOKEN_SRC_STR:
+		ret = 0;
+		break;
+	default:
+		break;
+	}
+
+	return (ret);
+}
+
+/* read at most n tokens from s into p.
+ * return -1 on error, or num tokens read
+ */
+ssize_t
+msph_token_stream_read(struct msph_token *ptr, size_t n,
+    struct msph_token_stream *s)
+{
+	size_t ret;
+	int res;
+
+	ret = 0;
+	res = -1;
+	while (ret < n && (res = read_single_tok(&ptr[ret], s)) != 0) {
+		if (res == -1)
+			return (-1);
+		ret++;
+	}
+
+	return ((ssize_t)ret);
+}
+
+/* 1: matched token, 0: failed to match token, -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;
+	struct msph_ctx *ctx;
+	struct msph_token_src *src;
+
+	ctx = s->ctx;
+	src = &s->src;
+
+	/* Skipping whitespace */
+	if (tok_match(ctx, src, &wspace) == -1)
+		return (-1);
+	SPHO_DEBUG_PRINT("wspace.matchlen=%zu\n", wspace.matchlen);
+	if (wspace.matchlen > 0 &&
+	    tok_commit(ctx, src, &wspace, NULL) == -1)
+		return (-1);
+
+	max_m = 0;
+	for (m = 1; token_matchers[m].type != TOK_END; m++) {
+		res = tok_match(ctx, src, &token_matchers[m]);
+
+		if (res == -1)
+			return (-1);
+
+		if (res == 0 && token_matchers[m].matchlen >
+		                token_matchers[max_m].matchlen) {
+			max_m = m;
+		}
+	}
+
+	if (max_m == 0) {
+		if (msph_token_stream_eof(s))
+			return (0);
+		MSPH_ERR(s->ctx, MSPH_ERR_TOKEN_NOMATCH);
+		return (-1);
+	}
+
+	if (tok_commit(ctx, src, &token_matchers[max_m], ptr) == -1)
+		return (-1);
+
+	return (1);
+}
+
+int
+msph_token_stream_eof(struct msph_token_stream *s)
+{
+	struct msph_token_src_file *file;
+	struct msph_token_src_str *str;
+
+	switch (s->src.type) {
+	case MSPH_TOKEN_SRC_FILE:
+		file = &s->src.inner.file;
+		return (file->pos == file->end && feof(file->f));
+	case MSPH_TOKEN_SRC_STR:
+		str = &s->src.inner.str;
+		return (str->pos == str->len);
+	default:
+		MSPH_ERR(s->ctx, MSPH_ERR_INVAL);
+		return (-1);
+	}
+}
+
+struct msph_token *
+msph_token_copy(struct msph_ctx *ctx, struct msph_token *token)
+{
+	size_t i;
+	struct msph_token *copy;
+	struct msph_token_info *info;
+
+	info = NULL;
+
+	for (i = 0; token_info[i].type != TOK_END; i++) {
+		if (token_info[i].type == token->type) {
+			info = &token_info[i];
+			break;
+		}
+	}
+
+	if (info == NULL) {
+		MSPH_ERR_INFO(ctx, MSPH_ERR_TOKEN_INVAL, token->type);
+		return (NULL);
+	}
+
+	if ((copy = malloc(sizeof(*copy))) == NULL) {
+		MSPH_ERR(ctx, MSPH_ERR_SYS);
+		return (NULL);
+	}
+
+	memcpy(copy, token, sizeof(*copy));
+
+	return (copy);
+}
+
+static ssize_t
+src_file_fill_buf(struct msph_ctx *ctx, struct msph_token_src_file *file)
+{
+	ssize_t ret;
+	size_t nread, maxread;
+
+	ret = nread = maxread = 0;
+	do {
+		if (file->end < file->pos)
+			maxread = file->pos - file->end;
+		else
+			maxread = BUF_LEN(file->buf) - file->end;
+
+		if (maxread == 0) {
+			MSPH_ERR(ctx, MSPH_ERR_TOKEN_TOOLONG);
+			return (-1);
+		}
+
+		nread = fread(&file->buf[file->end], sizeof(file->buf[0]),
+		    maxread, file->f);
+
+		ret += nread;
+		file->end = (file->end + nread) % BUF_LEN(file->buf);
+
+		SPHO_DEBUG_PRINT("src_file_fill_buf: valid range (%zu, %zu)\n",
+		    file->pos, file->end);
+
+		if (nread < maxread) {
+			if (ferror(file->f)) {
+				MSPH_ERR(ctx, MSPH_ERR_SYS);
+				return (-1);
+			}
+			break;
+		}
+
+	} while (file->end != file->pos);
+
+	return (ret);
+}
+
+/* reads a single char from the circular buffer in src */
+static int
+file_char_at(struct msph_ctx *ctx, struct msph_token_src *src, size_t i,
+    char *out)
+{
+	ssize_t fill;
+	struct msph_token_src_file *file;
+
+	SPHO_PRECOND(src != NULL);
+	SPHO_PRECOND(src->type == MSPH_TOKEN_SRC_FILE);
+
+	file = &src->inner.file;
+	fill = 0;
+
+	do {
+		/* simplest case */
+		if (file->pos + i < file->end) {
+			*out = file->buf[file->pos + i];
+			return (1);
+		}
+		/* wrap around */
+		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 (1);
+		}
+
+		if (feof(file->f))
+			return (0);
+		if ((fill = src_file_fill_buf(ctx, file)) == -1)
+			return (-1);
+
+	} while (fill > 0);
+
+	return (0);
+}
+
+static int
+char_at(struct msph_ctx *ctx, struct msph_token_src *src, size_t i, char *out)
+{
+	int ret;
+	struct msph_token_src_str *str;
+
+	ret = -1;
+	switch (src->type) {
+	case MSPH_TOKEN_SRC_FILE:
+		ret = file_char_at(ctx, src, i, out);
+		break;
+	case MSPH_TOKEN_SRC_STR:
+		str = &src->inner.str;
+		if (str->pos + i < str->len) {
+			*out = str->s[str->pos + i];
+			ret = 1;
+		} else {
+			ret = 0;
+		}
+		break;
+	default:
+		break;
+	}
+
+#ifdef SPHO_ENABLE_DEBUG_PRINT
+	if (isspace(*out)) {
+		const char *charrep;
+		switch (*out) {
+		case '\n':
+			charrep = "\\n";
+			break;
+		case '\t':
+			charrep = "\\t";
+			break;
+		case '\r':
+			charrep = "\\r";
+			break;
+		case '\v':
+			charrep = "\\v";
+			break;
+		case '\f':
+			charrep = "\\f";
+			break;
+		default:
+			charrep = "WOOOOOOOOOOPS";
+			break;
+		}
+		SPHO_DEBUG_PRINT("char_at: ret=%d, *out=%s\n", ret, charrep);
+	} else {
+		SPHO_DEBUG_PRINT("char_at: ret=%d, *out=%c\n", ret, *out);
+	}
+#endif
+	return (ret);
+}
+
+static int
+fromcbuf_charcpy(char *dst, const char *src, size_t src_len, size_t src_pos,
+    size_t ncpy)
+{
+	size_t cpy1, cpy2;
+	if (src_len < ncpy) {
+		return (-1);
+	}
+
+	cpy1 = (src_pos + ncpy < src_len) ? ncpy : src_len - src_pos;
+	cpy2 = ncpy - cpy1;
+
+	SPHO_DEBUG_PRINT("fromcbuf_charcpy: cpy1=%zu cpy2=%zu\n", cpy1, cpy2);
+
+	memcpy(dst, &src[src_pos], cpy1 * sizeof(src[0]));
+
+	if (! cpy2)
+		return (0);
+
+	memcpy(dst, &src[0], cpy2 * sizeof(src[0]));
+
+	return (0);
+}
+
+static int
+tok_match(struct msph_ctx *ctx, struct msph_token_src *src,
+    struct msph_matcher *m)
+{
+	int res;
+	char chr;
+	const char *match_str;
+	size_t off, len;
+	SPHO_PRECOND(m != NULL && src != NULL);
+
+	m->matchlen = 0;
+
+#define MATCH_CHAR(c) \
+	do { \
+		SPHO_DEBUG_PRINT("tok_match: '%c'\n", c); \
+		if ((res = char_at(ctx, src, 0, &chr)) == -1) \
+			return (-1); \
+		else if (res == 0) \
+			return (0); \
+		SPHO_DEBUG_PRINT("tok_match: char_at(0)='%c'\n", c); \
+\
+		if (chr == (c)) { \
+			m->matchlen = 1; \
+		} \
+		SPHO_DEBUG_PRINT("tok_match: matchlen=%zu\n", m->matchlen); \
+		return (0); \
+	} while (0)
+
+#define MATCH_STR(str) \
+	do { \
+		match_str = str; \
+		len = strlen(match_str); \
+		for (off = 0; off < len; off++) { \
+			if ((res = char_at(ctx, src, off, &chr)) == -1) \
+				return (-1); \
+			else if (res == 0) \
+				return (0); \
+\
+			if (chr != match_str[off]) \
+				break; \
+		} \
+		if (off == len) \
+			m->matchlen = len; \
+		return (0); \
+	} while (0)
+
+	switch (m->type) {
+	case TOK_LBRACE:
+		MATCH_CHAR('{');
+	case TOK_RBRACE:
+		MATCH_CHAR('}');
+	case TOK_LBRAK:
+		MATCH_CHAR('[');
+	case TOK_RBRAK:
+		MATCH_CHAR(']');
+	case TOK_LPAREN:
+		MATCH_CHAR('(');
+	case TOK_RPAREN:
+		MATCH_CHAR(')');
+	case TOK_COLON:
+		MATCH_CHAR(':');
+	case TOK_DOT:
+		MATCH_CHAR('.');
+	case TOK_COMMA:
+		MATCH_CHAR(',');
+	case TOK_EQUALS:
+		MATCH_CHAR('=');
+	case TOK_AMP:
+		MATCH_CHAR('&');
+	case TOK_PIPE:
+		MATCH_CHAR('|');
+	case TOK_IMPL:
+		MATCH_STR("=>");
+	case TOK_RARROW:
+		MATCH_STR("->");
+	case TOK_SUB:
+		MATCH_STR("<:");
+	case TOK_KW_TYPE:
+		MATCH_STR("type");
+	case TOK_KW_NOMINAL:
+		MATCH_STR("nominal");
+	case TOK_KW_MEMBER:
+		MATCH_STR("member");
+	case TOK_KW_ASSERT:
+		MATCH_STR("assert");
+	case TOK_KW_BOX:
+		MATCH_STR("box");
+	case TOK_KW_FORALL:
+		MATCH_STR("forall");
+	case TOK_CONST_TRUE:
+		MATCH_STR("True");
+	case TOK_CONST_FALSE:
+		MATCH_STR("False");
+	case TOK_IDENT:
+		off = 0;
+		while ((res = char_at(ctx, src, off++, &chr)) == 1) {
+			if (! isalnum(chr))
+				break;
+			m->matchlen++;
+		}
+		if (res == -1)
+			return (-1);
+		return (0);
+	case TOK_WSPACE:
+		off = 0;
+		while((res = char_at(ctx, src, off++, &chr)) == 1) {
+			if (! isspace(chr))
+				break;
+			m->matchlen++;
+		}
+		if (res == -1)
+			return (-1);
+		return (0);
+	default:
+		SPHO_ASSERT(0);
+		return (-1);
+		break;
+	}
+#undef MATCH_CHAR
+#undef MATCH_STR
+}
+
+#define TOK_HAS_DATA(type)	(type == TOK_IDENT)
+static int
+tok_commit(struct msph_ctx *ctx, struct msph_token_src *src,
+    struct msph_matcher *m, struct msph_token *ptr)
+{
+	size_t pos_old;
+	struct msph_text_pos tok_pos;
+	struct msph_token_src_str *str;
+	struct msph_token_src_file *file;
+
+	SPHO_PRECOND(ctx != NULL && m != NULL);
+	SPHO_PRECOND(m->matchlen != 0);
+
+	tok_pos = src->pos;
+	tok_update_pos(ctx, src, m);
+
+	switch (src->type) {
+	case MSPH_TOKEN_SRC_FILE:
+		file = &src->inner.file;
+		pos_old = file->pos;
+
+		file->pos += m->matchlen;
+		file->pos %= BUF_LEN(file->buf);
+		SPHO_ASSERT(file->pos <= file->end ||
+		    (file->pos < pos_old && file->pos < BUF_LEN(file->buf)));
+
+		if (ptr == NULL)
+			return (0);
+
+		ptr->type = m->type;
+		ptr->pos = tok_pos;
+		if (! TOK_HAS_DATA(ptr->type))
+			return (0);
+
+		if (m->matchlen >= sizeof(ptr->data.str)) {
+			MSPH_ERR(ctx, MSPH_ERR_TOKEN_TOOLONG);
+			return (-1);
+		}
+
+		if (fromcbuf_charcpy(ptr->data.str, file->buf,
+			    sizeof(file->buf), pos_old, m->matchlen) == -1) {
+			MSPH_ERR(ctx, MSPH_ERR_TOKEN_TOOLONG);
+			return (-1);
+		}
+
+		ptr->data.str[m->matchlen] = '\0';
+		return (0);
+
+	case MSPH_TOKEN_SRC_STR:
+		str = &src->inner.str;
+		pos_old = str->pos;
+
+		str->pos += m->matchlen;
+		SPHO_ASSERT(str->pos <= str->len);
+
+		if (ptr == NULL)
+			return (0);
+
+		ptr->type = m->type;
+		ptr->pos = tok_pos;
+		if (! TOK_HAS_DATA(ptr->type))
+			return (0);
+		
+		if (m->matchlen >= sizeof(ptr->data.str)) {
+			MSPH_ERR(ctx, MSPH_ERR_TOKEN_TOOLONG);
+			return (-1);
+		}
+
+		memcpy(ptr->data.str, str->s, m->matchlen *
+		    sizeof(str->s[0]));
+		ptr->data.str[m->matchlen] = '\0';
+
+		return (0);
+	default:
+		return (-1);
+	}
+}
+
+static void
+tok_update_pos(struct msph_ctx *ctx, struct msph_token_src *src,
+    struct msph_matcher *m)
+{
+	int res;
+	char c;
+	size_t i;
+
+	for (i = 0; i < m->matchlen; i++) {
+		res = char_at(ctx, src, i, &c);
+		SPHO_ASSERT(res == 1);
+
+		switch (c) {
+		case '\t':
+			src->pos.col += MSPH_TAB_WIDTH;
+			break;
+		case '\n':
+			src->pos.line++;
+			src->pos.col = 1;
+			break;
+		case '\r':
+			break;
+		default:
+			src->pos.col++;
+			break;
+		}
+	}
+}
+
+static const char *
+tok_base_str(struct msph_token *tok)
+{
+	size_t i;
+	for (i = 0; token_info[i].type != TOK_END; i++) {
+		if (token_info[i].type == tok->type)
+			return (token_info[i].dbg_str);
+	}
+
+	return (NULL);
+}
+
+
+

src/run/devcheck.c

@@ -0,0 +1,18 @@
+
+#include <stdio.h>
+
+#include "spho/spho.h"
+
+int main(void)
+{
+	struct spho_ctx *ctx;
+
+	ctx = NULL;
+
+	if ((ctx = spho_ctx_create()) == NULL)
+		return (-1);
+
+	spho_ctx_destroy(ctx);
+
+	return (0);
+}

src/spho/ctx.c

@@ -1,5 +1,7 @@
+#include <sys/queue.h>
 
 #include <stdio.h>
+#include <stdlib.h>
 #include <string.h>
 
 #include "spho/ctx.h"
@@ -8,13 +10,16 @@ static const char *spho_ctx_sys_strerror(struct spho_ctx *);
 static const char *spho_ctx_intern_strerror(struct spho_ctx *);
 
 struct spho_err {
-	int	num;
-	char	*msg;
+	int		err;
+	const char	*msg;
 };
 
 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 }
 };
 
@@ -23,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);
 }
@@ -38,30 +49,19 @@ 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(&c->noms)) {
-		nom = SLIST_FIRST(&c->noms);
-		SLIST_REMOVE_HEAD(&c->noms, next);
-		free(nom);
-	}
+	spho_scope_term(&ctx->glob);
 
-	while (! SLIST_EMPTY(&c->cnsts)) {
-		cnst = SLIST_FIRST(&c->cnsts);
-		SLIST_REMOVE_HEAD(&c->cnsts, next);
-		free(cnst);
-	}
+	free(ctx);
 }
 
 
 const char *
 spho_ctx_strerror(struct spho_ctx *ctx)
 {
-	char *msg;
 	int res;
+	const char *msg;
 
 	SPHO_PRECOND(ctx != NULL);
 
@@ -81,6 +81,10 @@ spho_ctx_strerror(struct spho_ctx *ctx)
 static const char *
 spho_ctx_sys_strerror(struct spho_ctx *ctx)
 {
+	int res;
+
+	SPHO_POSTCOND(ctx != NULL);
+
 #ifdef SPHO_DEBUG
 	res = snprintf(ctx->errbuf, sizeof(ctx->errbuf),
 	    "%s:%d:spho_syserr:%s (%d)", ctx->filebuf, ctx->errline,
@@ -89,8 +93,8 @@ spho_ctx_sys_strerror(struct spho_ctx *ctx)
 		ctx->errbuf[sizeof(ctx->errbuf) - 1] = '\0';
 #else
 	res = snprintf(ctx->errbuf, sizeof(ctx->errbuf),
-	    "spho_syserr:%s (%d)", ctx->filebuf, ctx->errline,
-	    strerror(ctx->err_info), ctx->err_info);
+	    "spho_syserr:%s (%d)", strerror(ctx->err_info),
+	    ctx->err_info);
 	if (res >= sizeof(ctx->errbuf))
 		ctx->errbuf[sizeof(ctx->errbuf) - 1] = '\0';
 #endif

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);
+}

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);
+}
+
+