lol

.gitignore

@@ -52,8 +52,6 @@ Mkfile.old
 dkms.conf
 
 # vim
-.swp
-.swo
 .*.swp
 .*.swo
 

CMakePresets.json

@@ -1,82 +0,0 @@
-{
-  "version": 10,
-  "cmakeMinimumRequired": {
-    "major": 3,
-    "minor": 31,
-    "patch": 0
-  },
-  "configurePresets": [
-    {
-      "name": "debug",
-      "displayName": "Debug",
-      "description": "Debug config",
-      "generator": "Unix Makefiles",
-      "binaryDir": "${sourceDir}/build-${presetName}/",
-      "cacheVariables": {
-        "CMAKE_BUILD_TYPE": "Debug"
-      }
-    },
-    {
-      "name": "release",
-      "displayName": "Release",
-      "description": "Release config",
-      "generator": "Unix Makefiles",
-      "binaryDir": "${sourceDir}/build-${presetName}/",
-      "cacheVariables": {
-        "CMAKE_BUILD_TYPE": "Release"
-      }
-    }
-  ],
-  "buildPresets": [
-    {
-      "name": "debug",
-      "configurePreset": "debug"
-    },
-    {
-      "name": "release",
-      "configurePreset": "release"
-    }
-  ],
-  "$comment": [{
-    "testPresets": [
-      {
-        "name": "default",
-        "configurePreset": "default",
-        "output": {"outputOnFailure": true},
-        "execution": {"noTestsAction": "error", "stopOnFailure": true}
-      }
-    ],
-    "packagePresets": [
-      {
-        "name": "default",
-        "configurePreset": "default",
-        "generators": [
-          "TGZ"
-        ]
-      }
-    ],
-    "workflowPresets": [
-      {
-        "name": "default",
-        "steps": [
-          {
-            "type": "configure",
-            "name": "default"
-          },
-          {
-            "type": "build",
-            "name": "default"
-          },
-          {
-            "type": "test",
-            "name": "default"
-          },
-          {
-            "type": "package",
-            "name": "default"
-          }
-        ]
-      }
-    ]
-  }]
-}

README.md

@@ -4,73 +4,14 @@ experimental type system implementation
 
 ## getting and building
 
-This will get you a basic build configured for development and debugging in the
-subdirectory `build-debug/` of repository base:
 ```sh
 git clone https://gitta.log-e.se/lnsol/log-e-sappho.git
 cd ./log-e-sappho
-cmake . --preset=debug
+cmake . -B build
-cd build-debug
+cd build
 make
 ```
 
-To get sane error messages from editors using `clangd` for diagnostics, i.e.
-using the same compilation flags configured for the build by cmake, in the repo
-base directory link `compile_commands.json`:
-```sh
-ln -s build-debug/compile_commands.json
-```
-
-## "Code style"
-
-I learned C from a guy that used to hack on OpenBSD, and just got used to
-writing it this way. If you wanna hack on this yourself, use your judgement.
-Look at the rest of the code and make yours look similar. Like, who cares about
-rules really? Here are some guidelines tho.
-
-**80 columns text width.**
-
-Use **8 spaces wide TABS** (yes, actual TABS, not just 8 spaces) for
-indentation and when inside `while`-/`if`-/etc. **conditions that span multiple
-lines, indent 4 spaces + 0 or more TABS**, as to separate condition from body
-of the conditional statement.
-
-(Look at the following examples using a tab width of 8, otherwise they won't
-make much sense.)
-
-I.e. do
-```c
-if (1 /* this is a very long condition */
-    == 2 /* spanning multiple lines */
-	    || 2 < 3 /* and we indent like this */) {
-	this = the_way;
-	/* as to increase distinguishability of condition from body */
-}
-```
-not
-```c
-if ( /* ... */
-	2 < 3) {
-	eyes = bleeding;
-}
-```
-
-Conditional statements without `{ .. }` is okay (preferred) if the condition
-fits on one line.
-
-I.e. do
-```c
-if (1 /* short condition that fits on one line */)
-	u = the_best;
-```
-and
-```c
-if (the_variable_that_has_that_long_name = function_with_a_long_name_too(
-	    arg_is_shorter_tho)) {
-	gesture = clapping;
-}
-```
-
 ## repository content
 
 This repository contains:

docs/about/formalities.md

@@ -8,7 +8,7 @@ s, t ::= s | t              (disjunction, a.k.a. union)
        | s => t             (implication)
        | s -> t             (arrow, a.k.a. function)
        | forall x . t       (forall, polymorphic)
-       | box t              (box, c.f. modal logic)
+       | box t              (box, c.f. modular logic)
        | a [t..]            (type operator application)
        | x                  (variable)
        | n                  (nominal)
@@ -37,23 +37,23 @@ s, γ ⊢ s, δ
 ---- [false-left]
 false, γ ⊢ δ
 
-// trace pairs: none?
+// trace pairs: none
 s, t, γ ⊢ δ
 ---- [conj-left]
 s & t, γ ⊢ δ
 
-// trace pairs: none?
+// trace pairs: none
 γ ⊢ s, t, δ
 ---- [disj-right]
 γ ⊢ s | t, δ
 
-// trace pairs: none?
+// trace pairs: none
 s, γ ⊢ δ
 t, γ ⊢ δ
 ---- [disj-left]
 s | t, γ ⊢ δ
 
-// trace pairs: none?
+// trace pairs: none
 γ ⊢ s, δ
 γ ⊢ t, δ
 ---- [conj-right]
@@ -61,12 +61,12 @@ s | t, γ ⊢ δ
 
 // XXX
 // remove s => t? always make progress
-// trace pairs: none?
+// trace pairs: none
 s => t, s, t, γ ⊢ δ
 ---- [impl-left]
 s => t, s, γ ⊢ δ
 
-// trace pairs: none?
+// trace pairs: none
 s, γ ⊢ t, δ
 ---- [impl-right]
 γ ⊢ s => t, δ
@@ -89,7 +89,7 @@ box t, γ ⊢ δ
 // to exclude typedefs like
 // type A = A
 // Or that our cycle detection excludes paths between "identical" states.
-// trace pairs: none?
+// trace pairs: none
 γ ⊢ expand(a[t..]), δ
 ----
 γ ⊢ a[t..], δ
@@ -114,10 +114,9 @@ n fresh
 ---- [forall]
 γ ⊢ δ
 
-// TODO can we choose a simpler rule instead?
 // 1 + n! premises
 // trace pairs: i ∈ [1..(n! + 1)], premise[i] -- conclusion
-c, γ*  ⊢ a_1, ..., a_n, δ*
+c, γ*  ⊢ a_1, ..., a_n
 ∀ I ⊆ {1, ..., n}.
 	c, γ* ⊢ { a_i | i ∈ I }, δ*
 	OR
@@ -126,7 +125,6 @@ c, γ*  ⊢ a_1, ..., a_n, δ*
 a_1 -> b_1, ..., a_n -> b_n, γ ⊢ c -> d, δ
 ```
 
-
 ### context operators
 
 * box filtering

docs/about/progress.md

@@ -1,9 +1,11 @@
-# sappho short
+# draft of presentation
+
+## sappho short
 	- sappho types intro
 	- a quick look at msph and spho
 
 
-## The types
+### The types
 
 We take a look at the grammar for sappho types
 
@@ -13,7 +15,7 @@ s, t ::= s | t              (disjunction, a.k.a. union)
        | s => t             (implication)
        | s -> t             (arrow, a.k.a. function)
        | forall x . t       (forall, polymorphic)
-       | box t              (box, c.f. modal logic)
+       | box t              (box, c.f. modular logic)
        | a [t..]            (type operator application)
        | x                  (variable)
        | n                  (nominal)
@@ -28,7 +30,7 @@ n ∈ nominal
 a ∈ opname
 ```
 
-The type `t <: s` would be syntactic sugar for `box (t => s)`
+The type `t <: s` would be expressive sugar for `box (t => s)`
 
 ### msph and spho
 
@@ -58,7 +60,7 @@ Thoughts
 * maybe eventually add a basic term language and interpreter
 * can we use external software/libraries for proof search?
 
-# interpretation of types
+## interpretation of types
 	- example programs in `msph`
 		- unified syntax for types and bounded polymorphism
 		- example: self typing
@@ -73,8 +75,7 @@ Check formalities.md.
 	- simple rules
 	- type constructor rules
 	- recursion and cyclic proofs
-
+* next steps?
-# next steps?
 	- formals:
 		- formulate theorems
 			- if we use semantic subtyping, isn't it enough to
@@ -84,4 +85,3 @@ Check formalities.md.
 		- simple rules, should be fairly simple
 		- type constructors, straightforward hopefully
 		- recursion and cyclic proofs... `¯\_(ツ)_/¯`
-	- describe use of language with type system (interpretation of types)

example/comparable.msph

@@ -1,16 +0,0 @@
-nominal lt
-nominal eq
-nominal gt
-
-type ord = lt | eq | gt
-
-type comparable[t] = {
-	member cmp : t -> ord
-}
-
-
-type integer = {
-	member cmp : integer -> ord
-}
-
-assert integer <: comparable[integer]

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

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

example/ex5.msph

@@ -0,0 +1,21 @@
+nominal N
+nominal M
+
+
+type T[X, Y] = {
+	// body
+}
+
+type A = T[N, M] // binding X -> N, Y -> M
+type B = T[M, N] // binding X -> M, Y -> N
+
+// converted to
+
+type A = ⟨ X -> N, Y -> M ⟩ {
+	// body
+}
+type B = ⟨ X -> M, Y -> N ⟩ {
+	// body
+}
+
+

example/graph.msph

@@ -1,10 +0,0 @@
-type gnode[e] = {
-	member edges : iterable[e]
-}
-
-type gedge[n] = {
-	member src : n
-	member dst : n
-}
-
-type graph[n, e] = (n <: gnode[e]) & (e <: gedge[n])

example/non-parse/ex6.msph

@@ -0,0 +1,21 @@
+type A[X, Y] = {
+	type B[Z] = {
+		mb : X & Z
+	}
+
+	ma : B[Y]
+}
+
+
+m : A[M, N]
+
+
+m : ⟨X -> M, Y -> N⟩ {
+	ma : B[Y]
+}
+
+m : ⟨X -> M, Y -> N⟩ {
+	ma : ⟨Z -> Y⟩  {
+		mb : X & Z
+	}
+}

example/self.msph

@@ -1,19 +0,0 @@
-type Accumulator[Self] = (Self <: Accumulator[Self]) & {
-	member add : Int -> Self
-}
-
-type MyAccum = {
-	member add : Int -> MyAccum
-}
-
-assert MyAccum <: Accumulator[MyAccum]
-
-
-
-
-
-type Acchmmmmulator[Self] = (Self <: Acchmmmmulator[Self]) => {
-	member add : Int -> Self
-}
-
-

include/msph/common.h

@@ -1,5 +1,5 @@
-#ifndef _MSPH_H
+#ifndef _MSPH_COMMON_H
-#define _MSPH_H
+#define _MSPH_COMMON_H
 
 #include "msph/err.h"
 #include "spho/ctx.h"
@@ -25,4 +25,4 @@ struct msph_text_pos {
 	unsigned int	col;
 };
 
-#endif /* ifndef _MSPH_H */
+#endif

include/msph/token.h

@@ -3,7 +3,7 @@
 
 #include <sys/queue.h>
 
-#include "msph/msph.h"
+#include "msph/common.h"
 
 /*
  *
@@ -39,8 +39,6 @@
 
 
 enum msph_tok_type {
-	TOK_INVAL = -1,		// special: invalid, use to mark invalid toks
-	TOK_EOF = 0,		// special: end-of-file
 	TOK_LBRACE,		// {
 	TOK_RBRACE,		// }
 	TOK_LBRAK,		// [
@@ -69,10 +67,9 @@ enum msph_tok_type {
 	TOK_CONST_FALSE,	// False
 
 	TOK_IDENT,		// identifiers
-	TOK_WSPACE,		// whitespace
+	TOK_INVAL,		// special: invalid, use to mark invalid toks
-
+	TOK_WSPACE,		// special: whitespace
-	TOK_NOPE		// special indicator: end of info array,
+	TOK_END			// special: end of array/token stream
-				//		      start of parsing
 };
 
 #define MSPH_TAB_WIDTH		8

include/msph/tree.h

@@ -3,7 +3,7 @@
 
 #include <sys/queue.h>
 
-#include "msph/msph.h"
+#include "msph/common.h"
 #include "msph/token.h"
 
 /* tree decorations */
@@ -37,8 +37,6 @@ struct msph_decor {
 #define MSPH_TREE_BOX		0x004a
 #define MSPH_TREE_FORALL	0x004b
 #define MSPH_TREE_PAREN		0x004c
-#define MSPH_TREE_SUBT		0x004d
-
 
 #define MSPH_TREE_IDENT		0x0100
 #define MSPH_TREE_NAMEDECL	0x0101
@@ -164,7 +162,8 @@ struct msph_tree_membdecl {
 struct msph_tree_assert {
 	struct msph_tree_dir	hd_dir;
 
-	struct msph_tree_tpexpr	*tp;
+	struct msph_tree_tpexpr	*ltp;
+	struct msph_tree_tpexpr	*rtp;
 };
 
 struct msph_tree_namedecl {
@@ -210,7 +209,6 @@ struct msph_tree_trait {
 	struct msph_tree_body	*body;
 };
 
-/* XXX should probably merge all binary type ops into one */
 struct msph_tree_conj {
 	struct msph_tree_tpexpr	hd_tpe;
 
@@ -232,13 +230,6 @@ struct msph_tree_impl {
 	struct msph_tree_tpexpr	*rtp;
 };
 
-struct msph_tree_subt {
-	struct msph_tree_tpexpr	hd_tpe;
-
-	struct msph_tree_tpexpr	*ltp;
-	struct msph_tree_tpexpr	*rtp;
-};
-
 struct msph_tree_arrow {
 	struct msph_tree_tpexpr	hd_tpe;
 
@@ -268,11 +259,7 @@ struct msph_tree_paren {
 
 struct msph_tree_root	*msph_tree_makeroot(struct msph_ctx *);
 
-#define MSPH_PARSE_PREFIX	1
+int	msph_tree_parse(struct msph_token_stream *, struct msph_tree_root *);
-#define MSPH_PARSE_INFIX	2
-
-int	msph_tree_parse(struct msph_token_stream *, struct msph_tree_root *,
-	    int);
 
 ssize_t	msph_tree_fprint(FILE *, struct msph_tree *);
 

include/spho/ctx.h

@@ -14,8 +14,6 @@ struct spho_ctx {
 	int	err_info;
 	char	errbuf[SPHO_ERR_BUF_LEN];
 
-	unsigned int	nom_cnt;
-
 #ifdef SPHO_DEBUG
 	char	filebuf[SPHO_ERR_FILEBUF_LEN];
 	int	errline;
@@ -24,7 +22,6 @@ struct spho_ctx {
 };
 
 struct spho_ctx		*spho_ctx_create(void);
-void			spho_ctx_init(struct spho_ctx *);
 void			spho_ctx_destroy(struct spho_ctx *);
 const char		*spho_ctx_strerror(struct spho_ctx *);
 

include/spho/err.h

@@ -39,7 +39,7 @@
 		(ctx)->err = (e);					\
 		(ctx)->err_info = (info);				\
 		snprintf((ctx)->filebuf, sizeof((ctx)->filebuf),	\
-		    __FILE__ ":%s", __func__);				\
+		    __FILE__);						\
 		(ctx)->errline = __LINE__;				\
 	} while (0)
 

include/spho/scope.h

@@ -7,22 +7,13 @@
 
 #define SPHO_NOM_LEN	128
 
-
-union spho_ext_data {
-	void		*ptr;
-	uint64_t	n;
-};
-
 /* name */
 struct spho_nom {
-	unsigned int		id;
 	char			s[SPHO_NOM_LEN];
-
+	SLIST_ENTRY(spho_nom)	next; // TODO change to allocs
-	union spho_ext_data	ext_data;
-
-	SLIST_ENTRY(spho_nom)	entries; 
 };
 
+SLIST_HEAD(spho_nom_l, spho_nom);
 
 
 #define TP_KONST_KEY_TRUE	0x43445 /* don't change!!!!! */
@@ -85,7 +76,6 @@ struct spho_tp {
 
 	int			kind;
 	union tp_data		d;
-	union spho_ext_data	ext_data;
 
 	STAILQ_ENTRY(spho_tp)	entries;
 };
@@ -95,20 +85,30 @@ struct spho_tp_op {
 
 	struct spho_scope	*op_sc;
 	struct spho_tp		*op_tp;
-	union spho_ext_data	ext_data;
 };
 
 STAILQ_HEAD(spho_tp_l, spho_tp);
 
+struct spho_tp_ptr {
+	struct spho_tp *p;
+	STAILQ_ENTRY(spho_tp_ptr)	entries;
+};
+
+STAILQ_HEAD(spho_tp_ptr_l, spho_tp_ptr);
+
 struct spho_tp_alloc {
 	union {
 		struct spho_tp		tp;
 		struct spho_tp_op	tp_op;
 	}		alloc;
 
-	STAILQ_ENTRY(spho_tp_alloc)	entries;
+	TAILQ_ENTRY(spho_tp_alloc)	allocs;
 };
 
+TAILQ_HEAD(spho_tp_alloc_l, spho_tp_alloc);
+
+SLIST_HEAD(spho_scope_l, spho_scope);
+
 /* defined in spho/bind.h */
 struct spho_bind;
 
@@ -116,38 +116,33 @@ struct spho_scope {
 	struct spho_ctx		*ctx;
 	struct spho_scope	*parent;
 
-	STAILQ_HEAD(
+	struct spho_scope_l	subs;
-	    spho_scope_l,
-	    spho_scope)		subs;
-	STAILQ_HEAD(
-	    spho_tp_alloc_l,
-	    spho_tp_alloc)	tps;
-	SLIST_HEAD(
-	    spho_nom_l,
-	    spho_nom)		noms;
-	size_t			nom_cnt;
-	struct spho_prebind	*bind_loc;
-	union spho_ext_data	ext_data;
 
-	STAILQ_ENTRY(spho_scope)	entries;
+	size_t			n_noms;
+	struct spho_nom_l	noms;
+	struct spho_tp_alloc_l	tps;
+
+	struct spho_prebind	*bind_loc;
+
+	SLIST_ENTRY(spho_scope)	next;
 };
 
 #define SPHO_SC_ERR(sc, err)	SPHO_ERR((sc)->ctx, (err))
 
-void	spho_scope_init(struct spho_scope *, struct spho_ctx *,
+int	spho_scope_init(struct spho_scope *, struct spho_ctx *,
 	    struct spho_scope *);
-void	spho_scope_cleanup(struct spho_scope *);
+void	spho_scope_term(struct spho_scope *);
 
 struct spho_scope	*spho_scope_global(struct spho_ctx *);
-struct spho_scope	*spho_scope_create_subscope(struct spho_scope *);
+struct spho_scope	*spho_scope_create(struct spho_scope *);
 
 
-void spho_scope_free(struct spho_scope *);
+void spho_scope_destroy(struct spho_scope *);
 
 struct spho_nom	*spho_scope_nom_add(struct spho_scope *, const char *, size_t);
-int	spho_scope_nom_lookup(struct spho_scope *, const char *, size_t,
+int	spho_scope_nom_lookup_str(struct spho_scope *, const char *, size_t,
 	    struct spho_nom **);
-int	spho_scope_nom_lookup_strict(struct spho_scope *, const char *,
+int	spho_scope_nom_lookup_str_strict(struct spho_scope *, const char *,
 	    size_t, struct spho_nom **);
 
 int	spho_scope_prebind_init(struct spho_scope *);

src/msph/msph.c

@@ -2,20 +2,28 @@
 #include <stdio.h>
 #include <unistd.h>
 
-#include "msph/msph.h"
+#include "msph/err.h"
 #include "msph/token.h"
 #include "msph/tree.h"
 #include "msph/sphophi.h"
 
+struct msph_opts {
+	int		tokenize_only;
+	const char	*in_path;
+	const char	*out_path;
+} run_opts = {
+	0,
+	NULL,
+	NULL
+};
+
 
 #define USAGE \
-"msph: micro sappho\n" \
+	"msph: micro sappho\n" \
-"	Usage: msph [-t] [-o out_path] [-p i|p] [in_path]\n" \
+	"\tUsage: msph [-t] [-o out_path] [in_path]\n" \
-"\n" \
+	"\n" \
-"	-t			- print tokenization\n" \
+	"\t-t	- print tokenization\n" \
-"	-o			- output path\n" \
+	"\t-o	- output path\n"
-"	-p i[nfix]|p[refix]	- infix or prefix &, |, =>, -> parsing\n" \
-"				  (default infix)\n"
 
 void
 print_usage(void)
@@ -23,64 +31,6 @@ print_usage(void)
 	printf("%s", USAGE);
 }
 
-struct err_info {
-	int		err;
-	const char	*msg;
-} errinfo[] = {
-	{ MSPH_ERR_SYS, "system error" },
-	{ MSPH_ERR_INVAL, "invalid argument" },
-	{ MSPH_ERR_TOOLONG, "input too long" },
-
-	{ MSPH_ERR_TOKEN_TOOLONG, "token too long" },
-	{ MSPH_ERR_TOKEN_EOF, "tokenizer reached end of file" },
-	{ MSPH_ERR_TOKEN_NOMATCH, "no matching token" },
-	{ MSPH_ERR_TOKEN_INVAL, "token invalid" },
-
-	{ MSPH_ERR_TREE_TOOLONG, "parsed data too long" },
-	{ MSPH_ERR_TREE_EOF, "parsing reached unexpected end of file" },
-	{ MSPH_ERR_TREE_NOMATCH, "parser matching failed" },
-
-	{ MSPH_ERR_TYPE_INVAL, "invalid type" },
-
-	{ MSPH_ERR_SPHOPHI, "spho error" },
-	{ -1, NULL }
-};
-
-void
-print_error(struct msph_ctx *ctx)
-{
-	size_t i;
-	const char *err_msg;
-
-	err_msg = NULL;
-	for (i = 0; errinfo[i].err != -1; i++) {
-		if (ctx->err == errinfo[i].err) {
-			err_msg = errinfo[i].msg;
-			break;
-		}
-	}
-	if (err_msg == NULL) {
-		err_msg = "unknown error";
-	}
-
-	fprintf(stderr, "ERROR(%x, %d):%s\n", ctx->err, ctx->err_info, err_msg);
-
-	if (ctx->err == MSPH_ERR_SPHOPHI)
-		fprintf(stderr, "\t%s\n", spho_ctx_strerror(ctx->spho));
-}
-
-struct msph_opts {
-	int		tokenize_only;
-	int		parser;
-	const char	*in_path;
-	const char	*out_path;
-} run_opts = {
-	0,
-	MSPH_PARSE_INFIX,
-	NULL,
-	NULL
-};
-
 int run(struct msph_opts *);
 
 int
@@ -88,7 +38,7 @@ main(int argc, char *argv[])
 {
 	int opt;
 
-	while ((opt = getopt(argc, argv, "hto:p:")) != -1) {
+	while ((opt = getopt(argc, argv, "hto:")) != -1) {
 		switch (opt) {
 		case 't':
 			run_opts.tokenize_only = 1;
@@ -96,19 +46,6 @@ main(int argc, char *argv[])
 		case 'o':
 			run_opts.out_path = optarg;
 			break;
-		case 'p':
-			switch (optarg[0]) {
-			case 'p':
-				run_opts.parser = MSPH_PARSE_PREFIX;
-				break;
-			case 'i':
-				run_opts.parser = MSPH_PARSE_INFIX;
-				break;
-			default:
-				print_usage();
-				exit(EXIT_FAILURE);
-			}
-			break;
 		case 'h':
 			print_usage();
 			exit(EXIT_SUCCESS);
@@ -144,7 +81,6 @@ run(struct msph_opts *opts)
 	struct msph_tree_root *root;
 	FILE *in, *out;
 
-
 	in = out = NULL;
 	s = NULL;
 	root = NULL;
@@ -186,7 +122,7 @@ run(struct msph_opts *opts)
 		goto err;
 	}
 
-	if (msph_tree_parse(s, root, opts->parser) == -1)
+	if (msph_tree_parse(s, root) == -1)
 		goto err;
 
 	printf("msph tree successfully parsed :)\n");
@@ -204,7 +140,13 @@ exit:
 	return (0);
 
 err:
-	print_error(&ctx);
+	if (root != NULL && ctx.err == MSPH_ERR_SPHOPHI) {
+		fprintf(stderr, "ERROR:%s\n",
+		    spho_ctx_strerror(ctx.spho));
+	} else {
+		fprintf(stderr, "ERROR:msph_err: %x (%d)\n", (ctx).err,
+		    (ctx).err_info);
+	}
 
 	if (in)
 		fclose(in);
@@ -214,7 +156,6 @@ err:
 }
 
 
-
 void
 msph_ctx_init(struct msph_ctx *ctx)
 {

src/msph/sphophi.c

@@ -15,7 +15,7 @@ static int	msph_tree_sphophi_decor_tpexpr_nom(struct spho_scope *,
 		    struct msph_tree *);
 static int	msph_tree_sphophi_decor_tp(struct spho_scope *,
 		    struct msph_tree *);
-static int	msph_tree_sphophi_prebind(struct spho_scope *,
+static int	msph_tree_sphophi_tp_prebind(struct spho_scope *,
 		    struct msph_tree *);
 
 /* is the tree a name binding? */
@@ -65,8 +65,6 @@ static int	msph_sphophi_foreach_pre_disj(msph_tree_sphophi_f,
 		    struct spho_scope *, struct msph_tree_disj *);
 static int	msph_sphophi_foreach_pre_impl(msph_tree_sphophi_f,
 		    struct spho_scope *, struct msph_tree_impl *);
-static int	msph_sphophi_foreach_pre_subt(msph_tree_sphophi_f,
-		    struct spho_scope *, struct msph_tree_subt *);
 static int	msph_sphophi_foreach_pre_arrow(msph_tree_sphophi_f,
 		    struct spho_scope *, struct msph_tree_arrow *);
 static int	msph_sphophi_foreach_pre_box(msph_tree_sphophi_f,
@@ -111,8 +109,6 @@ static int	msph_sphophi_foreach_post_disj(msph_tree_sphophi_f,
 		    struct spho_scope *, struct msph_tree_disj *);
 static int	msph_sphophi_foreach_post_impl(msph_tree_sphophi_f,
 		    struct spho_scope *, struct msph_tree_impl *);
-static int	msph_sphophi_foreach_post_subt(msph_tree_sphophi_f,
-		    struct spho_scope *, struct msph_tree_subt *);
 static int	msph_sphophi_foreach_post_arrow(msph_tree_sphophi_f,
 		    struct spho_scope *, struct msph_tree_arrow *);
 static int	msph_sphophi_foreach_post_box(msph_tree_sphophi_f,
@@ -158,7 +154,7 @@ msph_sphophi_tp(struct msph_tree_root *root)
 int
 msph_sphophi_tp_prebind(struct msph_tree_root *root)
 {
-	return (msph_sphophi_foreach_pre(msph_tree_sphophi_prebind,
+	return (msph_sphophi_foreach_pre(msph_tree_sphophi_tp_prebind,
 		    root));
 }
 
@@ -195,25 +191,25 @@ msph_tree_sphophi_decor_scope(struct spho_scope *sc, struct msph_tree *tree)
 	case MSPH_TREE_UNIT:
 	case MSPH_TREE_TRAIT:
 	case MSPH_TREE_FORALL:
-		if ((SCOPE(tree) = spho_scope_create_subscope(sc)) == NULL)
+		if ((SCOPE(tree) = spho_scope_create(sc)) == NULL)
-			return (-1);
+			ret = -1;
 		ADD_FLAG(tree, MSPH_TREE_FLAG_SCOPE);
 		break;
 	case MSPH_TREE_TPDEF:
 		tpdef = (struct msph_tree_tpdef *)tree;
-		if (STAILQ_EMPTY(&tpdef->params))
+		if (! STAILQ_EMPTY(&tpdef->params) &&
-			break;
+		    ((SCOPE(tpdef) = spho_scope_create(sc)) == NULL)) {
-		if (((SCOPE(tpdef) = spho_scope_create_subscope(sc)) == NULL))
+			ret = -1;
-			return (-1);
+		}
 		ADD_FLAG(tree, MSPH_TREE_FLAG_SCOPE);
 		break;
-	case MSPH_TREE_NAMEDECL:
+	case MSPH_TREE_IDENT:
-		SPHO_ASSERT(IS_BINDING(tree->parent));
+		if (! IS_BINDING(tree->parent))
+			break;
 		ident = (struct msph_tree_ident *)tree;
 		if ((NOM(ident) = spho_scope_nom_add(sc, ident->str,
-			    sizeof(ident->str))) == NULL) {
+			    sizeof(ident->str))) == NULL)
-			return (-1);
+			ret = -1;
-		}
 		ADD_FLAG(tree, MSPH_TREE_FLAG_NOM);
 		break;
 	default:
@@ -234,14 +230,12 @@ msph_tree_sphophi_decor_tpexpr_nom(struct spho_scope *sc,
 
 	switch (TREE_ID(tree)) {
 	case MSPH_TREE_IDENT:
-		SPHO_ASSERT(IS_TPEXPR(tree->parent));
+		if (! IS_TPEXPR(tree->parent))
-
+			break;
 		ident = (struct msph_tree_ident *)tree;
-		if (spho_scope_nom_lookup_strict(sc, ident->str,
+		ret = spho_scope_nom_lookup_str_strict(sc, ident->str,
-		    sizeof(ident->str), &NOM(ident)) == -1) {
+			    sizeof(ident->str), &NOM(ident));
-			return (-1);
+
-		}
-		ADD_FLAG(ident, MSPH_TREE_FLAG_NOM);
 		break;
 	default:
 		break;
@@ -267,7 +261,6 @@ msph_tree_sphophi_decor_tp(struct spho_scope *sc, struct msph_tree *tree)
 	struct msph_tree_trait *trait;
 	struct msph_tree_dir *dir;
 	struct msph_tree_membdecl *membd;
-	struct msph_tree_subt *subt;
 
 	struct spho_tp_l *tps;
 	struct spho_tp *tp, *tp_memb;
@@ -278,59 +271,43 @@ msph_tree_sphophi_decor_tp(struct spho_scope *sc, struct msph_tree *tree)
 	dir = NULL;
 	membd = NULL;
 
-	if (! IS_TPEXPR(tree))
+	if (! (tree->type & MSPH_TREE_TPEXPR))
 		return (0);
 
 	switch (TREE_ID(tree)) {
 	case MSPH_TREE_CONJ:
 		conj = (struct msph_tree_conj *)tree;
 		if ((TP(conj) = spho_tp_create_conj(sc, TP(conj->ltp),
-			    TP(conj->rtp))) == NULL) {
+		    TP(conj->rtp))) == NULL)
 			goto cleanup;
-		}
 		ADD_FLAG(conj, MSPH_TREE_FLAG_TP);
 		break;
 	case MSPH_TREE_DISJ:
 		disj = (struct msph_tree_disj *)tree;
 		if ((TP(disj) = spho_tp_create_conj(sc, TP(disj->ltp),
-			    TP(disj->rtp))) == NULL) {
+		    TP(disj->rtp))) == NULL)
 			goto cleanup;
-		}
 		ADD_FLAG(disj, MSPH_TREE_FLAG_TP);
 		break;
 	case MSPH_TREE_IMPL:
 		impl = (struct msph_tree_impl *)tree;
 		if ((TP(impl) = spho_tp_create_conj(sc, TP(impl->ltp),
-			    TP(impl->rtp))) == NULL) {
+		    TP(impl->rtp))) == NULL)
 			goto cleanup;
-		}
 		ADD_FLAG(impl, MSPH_TREE_FLAG_TP);
 		break;
-	case MSPH_TREE_SUBT:
-		/* a <: b == box(a => b) */
-		subt = (struct msph_tree_subt *)tree;
-		if ((tp = spho_tp_create_impl(sc, TP(subt->ltp),
-			    TP(subt->rtp))) == NULL) {
-			goto cleanup;
-		}
-		if ((TP(subt) = spho_tp_create_box(sc, tp)) == NULL)
-			goto cleanup;
-		ADD_FLAG(subt, MSPH_TREE_FLAG_TP);
-		break;
 	case MSPH_TREE_ARROW:
 		arrow = (struct msph_tree_arrow *)tree;
 		if ((TP(arrow) = spho_tp_create_conj(sc, TP(arrow->ltp),
-		    TP(arrow->rtp))) == NULL) {
+		    TP(arrow->rtp))) == NULL)
 			goto cleanup;
-		}
 		ADD_FLAG(arrow, MSPH_TREE_FLAG_TP);
 		break;
 	case MSPH_TREE_TPNAME:
 		tpname = (struct msph_tree_tpname *)tree;
 		if ((TP(tpname) = spho_tp_create_name(sc, NOM(tpname->name)))
-		    == NULL) {
+		    == NULL)
 			goto cleanup;
-		}
 		ADD_FLAG(tpname, MSPH_TREE_FLAG_TP);
 		break;
 	case MSPH_TREE_TPAPPL:
@@ -406,7 +383,7 @@ msph_tree_sphophi_decor_tp(struct spho_scope *sc, struct msph_tree *tree)
 		ADD_FLAG(trait, MSPH_TREE_FLAG_TP);
 		break;
 	default:
-		SPHO_RIP("impossible-default-reached");
+		SPHO_ASSERT(0);
 		break;
 	}
 
@@ -420,7 +397,7 @@ cleanup:
 }
 
 static int
-msph_tree_sphophi_prebind(struct spho_scope *sc,
+msph_tree_sphophi_tp_prebind(struct spho_scope *sc,
     struct msph_tree *tree)
 {
 	int ret;
@@ -456,8 +433,8 @@ msph_tree_sphophi_prebind(struct spho_scope *sc,
 				return (-1);
 			}
 
-			if ((ret = spho_scope_prebind_tp_op(sc,
+			if ((ret = spho_scope_prebind_tp_op(sc, NOM(name), op))
-				    NOM(tpdef->name), op)) == -1) {
+			    == -1) {
 				return (-1);
 			}
 		} else {
@@ -467,8 +444,6 @@ msph_tree_sphophi_prebind(struct spho_scope *sc,
 			}
 		}
 		break;
-	case MSPH_TREE_NOMINDECL:
-		break;
 	default:
 		break;
 	}
@@ -653,7 +628,9 @@ msph_sphophi_foreach_pre_assert(msph_tree_sphophi_f f, struct spho_scope *sc,
 	if ((ret = f(sc, TREE(ass))) != 0)
 		return (ret);
 
-	if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, ass->tp)) != 0)
+	if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, ass->ltp)) != 0)
+		return (ret);
+	if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, ass->rtp)) != 0)
 		return (ret);
 
 	return (ret);
@@ -703,10 +680,6 @@ msph_sphophi_foreach_pre_tpexpr(msph_tree_sphophi_f f, struct spho_scope *sc,
 		ret = msph_sphophi_foreach_pre_impl(f, sc,
 		    (struct msph_tree_impl *)tpexpr);
 		break;
-	case MSPH_TREE_SUBT:
-		ret = msph_sphophi_foreach_pre_subt(f, sc,
-		    (struct msph_tree_subt *)tpexpr);
-		break;
 	case MSPH_TREE_ARROW:
 		ret = msph_sphophi_foreach_pre_arrow(f, sc,
 		    (struct msph_tree_arrow *)tpexpr);
@@ -744,7 +717,7 @@ msph_sphophi_foreach_pre_tpexpr(msph_tree_sphophi_f f, struct spho_scope *sc,
 		    (struct msph_tree_false *)tpexpr);
 		break;
 	default:
-		SPHO_RIP("impossible-default-reached");
+		SPHO_RIP("default-reach");
 		break;
 	}
 
@@ -802,23 +775,6 @@ msph_sphophi_foreach_pre_impl(msph_tree_sphophi_f f, struct spho_scope *sc,
 	return (msph_sphophi_foreach_pre_tpexpr(f, sc, impl->rtp));
 }
 
-static int
-msph_sphophi_foreach_pre_subt(msph_tree_sphophi_f f, struct spho_scope *sc,
-    struct msph_tree_subt *subt)
-{
-	int ret;
-
-	SPHO_PRECOND(sc != NULL);
-	SPHO_PRECOND(subt != NULL);
-
-	if ((ret = f(sc, TREE(subt))) != 0)
-		return (ret);
-
-	if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, subt->ltp)) != 0)
-		return (ret);
-	return (msph_sphophi_foreach_pre_tpexpr(f, sc, subt->rtp));
-}
-
 static int
 msph_sphophi_foreach_pre_arrow(msph_tree_sphophi_f f, struct spho_scope *sc,
     struct msph_tree_arrow *arrow)
@@ -1136,7 +1092,9 @@ msph_sphophi_foreach_post_assert(msph_tree_sphophi_f f, struct spho_scope *sc,
 	SPHO_PRECOND(sc != NULL);
 	SPHO_PRECOND(ass != NULL);
 
-	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, ass->tp)) != 0)
+	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, ass->ltp)) != 0)
+		return (ret);
+	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, ass->rtp)) != 0)
 		return (ret);
 
 	return (f(sc, TREE(ass)));
@@ -1186,10 +1144,6 @@ msph_sphophi_foreach_post_tpexpr(msph_tree_sphophi_f f, struct spho_scope *sc,
 		ret = msph_sphophi_foreach_post_impl(f, sc,
 		    (struct msph_tree_impl *)tpexpr);
 		break;
-	case MSPH_TREE_SUBT:
-		ret = msph_sphophi_foreach_post_subt(f, sc,
-		    (struct msph_tree_subt *)tpexpr);
-		break;
 	case MSPH_TREE_ARROW:
 		ret = msph_sphophi_foreach_post_arrow(f, sc,
 		    (struct msph_tree_arrow *)tpexpr);
@@ -1286,22 +1240,6 @@ msph_sphophi_foreach_post_impl(msph_tree_sphophi_f f, struct spho_scope *sc,
 	return (f(sc, TREE(impl)));
 }
 
-static int
-msph_sphophi_foreach_post_subt(msph_tree_sphophi_f f, struct spho_scope *sc,
-    struct msph_tree_subt *subt)
-{
-	int ret;
-
-	SPHO_PRECOND(sc != NULL);
-	SPHO_PRECOND(subt != NULL);
-
-	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, subt->ltp)) != 0)
-		return (ret);
-	if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, subt->rtp)) != 0)
-		return (ret);
-
-	return (f(sc, TREE(subt)));
-}
 static int
 msph_sphophi_foreach_post_arrow(msph_tree_sphophi_f f, struct spho_scope *sc,
     struct msph_tree_arrow *arrow)

src/msph/token.c

@@ -7,7 +7,7 @@
 
 #include "spho/spho.h"
 
-#include "msph/msph.h"
+#include "msph/err.h"
 #include "msph/token.h"
 
 
@@ -48,7 +48,7 @@ struct msph_matcher token_matchers[] = {
 	{ 0, 0, TOK_CONST_FALSE },
 
 	{ 0, 0, TOK_IDENT },
-	{ 0, 0, TOK_NOPE }
+	{ 0, 0, TOK_END }
 };
 struct msph_matcher wspace = { 0, 0, TOK_WSPACE };
 
@@ -86,7 +86,7 @@ struct msph_token_info {
 	TOK_INFO(TOK_CONST_FALSE, "False"),
 
 	TOK_INFO(TOK_IDENT, NULL),
-	{ TOK_NOPE , NULL, NULL }
+	{ TOK_END , NULL, NULL }
 #undef TOK_INFO
 };
 
@@ -305,7 +305,7 @@ read_single_tok(struct msph_token *ptr, struct msph_token_stream *s)
 		return (-1);
 
 	max_m = 0;
-	for (m = 1; token_matchers[m].type != TOK_NOPE; m++) {
+	for (m = 1; token_matchers[m].type != TOK_END; m++) {
 		res = tok_match(ctx, src, &token_matchers[m]);
 
 		if (res == -1)
@@ -358,7 +358,7 @@ msph_token_copy(struct msph_ctx *ctx, struct msph_token *token)
 
 	info = NULL;
 
-	for (i = 0; token_info[i].type != TOK_NOPE; i++) {
+	for (i = 0; token_info[i].type != TOK_END; i++) {
 		if (token_info[i].type == token->type) {
 			info = &token_info[i];
 			break;
@@ -769,7 +769,7 @@ static const char *
 tok_base_str(struct msph_token *tok)
 {
 	size_t i;
-	for (i = 0; token_info[i].type != TOK_NOPE; i++) {
+	for (i = 0; token_info[i].type != TOK_END; i++) {
 		if (token_info[i].type == tok->type)
 			return (token_info[i].dbg_str);
 	}

src/spho/bind.c

@@ -19,21 +19,20 @@ spho_prebind_create(struct spho_scope *sc)
 		return (NULL);
 	}
 
-	if ((bind->binds = calloc(sc->nom_cnt, sizeof(*bind->binds))) == NULL) {
+	if ((bind->binds = calloc(sc->n_noms, sizeof(*bind->binds))) == NULL) {
 		SPHO_ERR(sc->ctx, SPHO_ERR_SYS);
 		free(bind);
 		return (NULL);
 	}
 
 	bind->sc = sc;
-	bind->sz = sc->nom_cnt;
+	bind->sz = sc->n_noms;
 
 
 	i = 0;
-	SLIST_FOREACH(nom, &sc->noms, entries) {
+	SLIST_FOREACH(nom, &sc->noms, next) {
 		SPHO_ASSERT(i < bind->sz);
-		bind->binds[i++] =
+		bind->binds[i++] = (struct spho_prebind_pair) { NULL, 0, NULL };
-		       	(struct spho_prebind_pair) { nom, 0, { NULL } };
 	}
 
 	return (bind);

src/spho/ctx.c

@@ -37,31 +37,28 @@ spho_ctx_create(void)
 
 	c = NULL;
 
-	if ((c = calloc(1, sizeof(struct spho_ctx))) == NULL)
+	if ((c = malloc(sizeof(struct spho_ctx))) == NULL)
 		return (NULL);
 
-	spho_ctx_init(c);
+	c->err = 0;
+	c->err_info = 0;
+
+	if (spho_scope_init(&c->glob, c, NULL) == -1) {
+		free(c);
+		return (NULL);
+	}
+
+	SPHO_POSTCOND(c != NULL);
 
 	return (c);
 }
 
-void
-spho_ctx_init(struct spho_ctx *ctx)
-{
-	ctx->err = 0;
-	ctx->err_info = 0;
-
-	ctx->nom_cnt = 0;
-
-	spho_scope_init(&ctx->glob, ctx, NULL);
-}
-
 void
 spho_ctx_destroy(struct spho_ctx *ctx)
 {
 	SPHO_PRECOND(ctx != NULL);
 
-	spho_scope_cleanup(&ctx->glob);
+	spho_scope_term(&ctx->glob);
 
 	free(ctx);
 }

src/spho/scope.c

@@ -8,59 +8,41 @@
 #include "spho/scope.h"
 #include "spho/bind.h"
 
+static void spho_nom_term(struct spho_nom *);
+
 static int scope_nom_lookup_str_local(struct spho_scope *, const char *,
     size_t, struct spho_nom **);
 static int scope_nom_in_local(struct spho_scope *, struct spho_nom *);
 
-void
+int
 spho_scope_init(struct spho_scope *sc, struct spho_ctx *ctx,
     struct spho_scope *p)
 {
 	sc->ctx = ctx;
 	sc->parent = p;
 
-	STAILQ_INIT(&sc->subs);
+	SLIST_INIT(&sc->subs);
 
 	SLIST_INIT(&sc->noms);
-	sc->nom_cnt = 0;
+	sc->n_noms = 0;
 
-	STAILQ_INIT(&sc->tps);
+	TAILQ_INIT(&sc->tps);
 
 	sc->bind_loc = NULL;
+
+	return (0);
 }
 
 void
-spho_scope_cleanup(struct spho_scope *sc)
+spho_scope_term(struct spho_scope *sc)
 {
-	struct spho_scope *sub;
+	SPHO_UTIL_SLIST_DESTROY(&sc->subs, spho_scope, next, spho_scope_term);
-	struct spho_nom *nom;
-	struct spho_tp_alloc *tp_alloc;
 
-	/* XXX is doable without recursive call, but cba */
+	SPHO_UTIL_SLIST_DESTROY(&sc->noms, spho_nom, next, spho_nom_term);
-	while (! STAILQ_EMPTY(&sc->subs)) {
-		sub = STAILQ_FIRST(&sc->subs);
-		STAILQ_REMOVE_HEAD(&sc->subs, entries);
-		spho_scope_cleanup(sub);
-		free(sub);
-	}
-
-	/* all type structs are allocated from scope */
-	while (! STAILQ_EMPTY(&sc->tps)) {
-		tp_alloc = STAILQ_FIRST(&sc->tps);
-		STAILQ_REMOVE_HEAD(&sc->tps, entries);
-		free(tp_alloc);
-	}
-
-	/* names are allocated in scope too */
-	while (! SLIST_EMPTY(&sc->noms)) {
-		nom = SLIST_FIRST(&sc->noms);
-		SLIST_REMOVE_HEAD(&sc->noms, entries);
-		free(nom);
-	}
 
 	sc->parent = NULL;
 
-	if (sc->bind_loc != NULL)
+	if (sc->bind_loc == NULL)
 		spho_prebind_free(sc->bind_loc);
 	sc->bind_loc = NULL;
 }
@@ -75,7 +57,7 @@ spho_scope_global(struct spho_ctx *ctx)
 
 
 struct spho_scope *
-spho_scope_create_subscope(struct spho_scope *sc)
+spho_scope_create(struct spho_scope *sc)
 {
 	struct spho_scope *sub;
 
@@ -84,24 +66,35 @@ spho_scope_create_subscope(struct spho_scope *sc)
 		return (NULL);
 	}
 
-	spho_scope_init(sub, sc->ctx, sc);
+	if (spho_scope_init(sub, sc->ctx, sc) == -1) {
+		free(sub);
+		return (NULL);
+	}
 
-	STAILQ_INSERT_TAIL(&sc->subs, sub, entries);
+	SLIST_INSERT_HEAD(&sc->subs, sub, next);
 
 	return (sub);
 }
 
+
+static void
+spho_nom_term(__attribute__((unused)) struct spho_nom *nom)
+{
+	return;
+}
+
 void
-spho_scope_free(struct spho_scope *sc)
+spho_scope_destroy(struct spho_scope *sc)
 {
 	struct spho_scope *p;
 
 	p = sc->parent;
-	STAILQ_REMOVE(&p->subs, sc, spho_scope, entries);
+	SLIST_REMOVE(&p->subs, sc, spho_scope, next);
-	spho_scope_cleanup(sc);
+	spho_scope_term(sc);
 	free(sc);
 }
 
+
 struct spho_nom *
 spho_scope_nom_add(struct spho_scope *sc, const char *nomstr, size_t sz)
 {
@@ -128,10 +121,9 @@ spho_scope_nom_add(struct spho_scope *sc, const char *nomstr, size_t sz)
 		SPHO_SC_ERR(sc, SPHO_ERR_TOOBIG);
 		goto err;
 	}
-	nom->id = sc->ctx->nom_cnt++;
 
-	SLIST_INSERT_HEAD(&sc->noms, nom, entries);
+	SLIST_INSERT_HEAD(&sc->noms, nom, next);
-	sc->nom_cnt++;
+	sc->n_noms++;
 
 	return (nom);
 err:
@@ -141,7 +133,7 @@ err:
 
 
 int
-spho_scope_nom_lookup(struct spho_scope *sc, const char *nomstr, size_t sz,
+spho_scope_nom_lookup_str(struct spho_scope *sc, const char *nomstr, size_t sz,
     struct spho_nom **out)
 {
 	struct spho_nom *nom;
@@ -155,7 +147,7 @@ spho_scope_nom_lookup(struct spho_scope *sc, const char *nomstr, size_t sz,
 
 	*out = NULL;
 	while (*out == NULL && sc != NULL) {
-		SLIST_FOREACH(nom, &sc->noms, entries) {
+		SLIST_FOREACH(nom, &sc->noms, next) {
 			if (strncmp(nom->s, nomstr, sz) == 0) {
 				*out = nom;
 				break;
@@ -168,10 +160,10 @@ spho_scope_nom_lookup(struct spho_scope *sc, const char *nomstr, size_t sz,
 }
 
 int
-spho_scope_nom_lookup_strict(struct spho_scope *sc, const char *nomstr,
+spho_scope_nom_lookup_str_strict(struct spho_scope *sc, const char *nomstr,
     size_t sz, struct spho_nom **out)
 {
-	if (spho_scope_nom_lookup(sc, nomstr, sz, out) == -1)
+	if (spho_scope_nom_lookup_str(sc, nomstr, sz, out) == -1)
 		return (-1);
 
 	if (*out == NULL) {
@@ -185,8 +177,10 @@ spho_scope_nom_lookup_strict(struct spho_scope *sc, const char *nomstr,
 int
 spho_scope_prebind_init(struct spho_scope *sc)
 {
-	if ((sc->bind_loc = spho_prebind_create(sc)) == NULL)
+	if ((sc->bind_loc = spho_prebind_create(sc)) 
+	    == NULL) {
 		return (-1);
+	}
 
 	return (0);
 }
@@ -240,7 +234,7 @@ scope_nom_lookup_str_local(struct spho_scope *sc, const char *nomstr,
 	}
 
 	*out = NULL;
-	SLIST_FOREACH(nom, &sc->noms, entries) {
+	SLIST_FOREACH(nom, &sc->noms, next) {
 		if (strncmp(nom->s, nomstr, sz) == 0) {
 			*out = nom;
 			break;
@@ -255,7 +249,7 @@ scope_nom_in_local(struct spho_scope *sc, struct spho_nom *nom)
 {
 	struct spho_nom *sc_nom;
 
-	SLIST_FOREACH(sc_nom, &sc->noms, entries) {
+	SLIST_FOREACH(sc_nom, &sc->noms, next) {
 		if (sc_nom == nom)
 			return (1);
 	}

src/spho/tp.c

@@ -20,7 +20,7 @@ spho_tp_alloc(struct spho_scope *sc)
 	}
 
 	((struct spho_tp *)tp_alloc)->sc = sc;
-	STAILQ_INSERT_TAIL(&sc->tps, tp_alloc, entries);
+	TAILQ_INSERT_TAIL(&sc->tps, tp_alloc, allocs);
 
 	return ((struct spho_tp *)tp_alloc);
 }
@@ -36,11 +36,25 @@ spho_tp_op_alloc(struct spho_scope *sc)
 	}
 
 	((struct spho_tp_op *)tp_alloc)->sc = sc;
-	STAILQ_INSERT_TAIL(&sc->tps, tp_alloc, entries);
+	TAILQ_INSERT_TAIL(&sc->tps, tp_alloc, allocs);
 
 	return ((struct spho_tp_op *)tp_alloc);
 }
 
+static void
+spho_tp_free(struct spho_tp *tp)
+{
+	struct spho_scope *sc;
+	struct spho_tp_alloc *tp_alloc;
+
+	sc = tp->sc;
+	tp_alloc = (struct spho_tp_alloc *)tp;
+
+	TAILQ_REMOVE(&sc->tps, tp_alloc, allocs);
+
+	free(tp_alloc);
+}
+
 struct spho_tp *
 spho_tp_create_conj(struct spho_scope *sc, struct spho_tp *ltp,
     struct spho_tp *rtp)
@@ -256,3 +270,45 @@ spho_tp_op_create(struct spho_scope *sc, struct spho_scope *op_sc, struct spho_t
 
 	return (op);
 }
+
+/* Free type structure. External data (like nom) are freed elsewhere. */
+void
+spho_tp_destroy(struct spho_tp *tp)
+{
+	struct spho_tp *arg;
+
+	switch (tp->kind & SPHO_TP_FORM_MASK) {
+	case SPHO_TP_FORM_TRUE:
+	case SPHO_TP_FORM_FALSE:
+	case SPHO_TP_FORM_NAME: 
+	case SPHO_TP_FORM_VAR:
+		break;
+	case SPHO_TP_FORM_CONJ:
+	case SPHO_TP_FORM_DISJ:
+	case SPHO_TP_FORM_IMPL:
+	case SPHO_TP_FORM_ARROW:
+		spho_tp_destroy(tp->d.binop.left);
+		spho_tp_destroy(tp->d.binop.right);
+		break;
+	case SPHO_TP_FORM_BOX:
+		spho_tp_destroy(tp->d.unop.operand);
+		break;
+	case SPHO_TP_FORM_FORALL:
+		spho_tp_destroy(tp->d.fa.tp);
+		break;
+	case SPHO_TP_FORM_MEMBER: 
+		spho_tp_destroy(tp->d.memb.tp);
+		break;
+	case SPHO_TP_FORM_APPL:
+		STAILQ_FOREACH(arg, tp->d.appl.args, entries) {
+			spho_tp_destroy(arg);
+		}
+		free(tp->d.appl.args);
+		break;
+	default:
+		SPHO_ASSERT(0);
+		break;
+	}
+
+	spho_tp_free(tp);
+}