oops

.gitignore

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

CMakeLists.txt

@@ -5,10 +5,10 @@ set(CMAKE_C_STANDARD 99)
 set(CMAKE_C_STANDARD_REQUIRED True)
 string(JOIN " " CMAKE_C_FLAGS
 	"-Wall -Wextra -Wformat=2"
-       "-Wconversion -Wsign-conversion -Wimplicit-fallthrough"
-       "-Werror=implicit"
-       "-Werror=incompatible-pointer-types"
-       "-Werror=int-conversion")
+	"-Wconversion -Wsign-conversion -Wimplicit-fallthrough"
+	"-Werror=implicit"
+	"-Werror=incompatible-pointer-types"
+	"-Werror=int-conversion")
 set(CMAKE_VERBOSE_MAKEFILE ON)
 
 set(CMAKE_EXPORT_COMPILE_COMMANDS ON)

CMakePresets.json

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

README.md

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

docs/about/formalities.md

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

docs/about/progress.md

@@ -0,0 +1,87 @@
+# sappho short
+	- sappho types intro
+	- a quick look at msph and spho
+
+
+## The types
+
+We take a look at the grammar for sappho types
+
+```cmath
+s, t ::= s | t              (disjunction, a.k.a. union)
+       | s & t              (conjunction, a.k.a. intersection)
+       | s => t             (implication)
+       | s -> t             (arrow, a.k.a. function)
+       | forall x . t       (forall, polymorphic)
+       | box t              (box, c.f. modal logic)
+       | a [t..]            (type operator application)
+       | x                  (variable)
+       | n                  (nominal)
+       | true               (true, a.k.a. top)
+       | false              (false, a.k.a. bottom)
+       | { m : t }          (member, a.k.a. atomic record)
+       | ( t )
+
+
+x ∈ var
+n ∈ nominal
+a ∈ opname
+```
+
+The type `t <: s` would be syntactic sugar for `box (t => s)`
+
+### msph and spho
+
+**`msph`** is a minimal language for describing types in sappho and a partial
+implementation (as of 2025-06-25). The goal being to have a prototype for
+deciding subtyping by the end of the summer. Right now it includes
+
+* parser (prefix notation `&`, `|`, `=>`, `->`)
+* iterative decorators adding scope, type, and binding data.
+* interface with these decorations is implemented as a separate library,
+  **spho**.
+
+**`spho`** is the WIP type system implementation, as of now having bindings to 
+
+* handle type representation data structures
+* handle scoping of names and bindings
+* initial progress on subtyping implementation
+
+Left to do to get a prototype subtype checker working:
+
+* handling of subtyping sequent judgement rules
+* search heuristic for basic proof search
+* cyclic proof search
+
+Thoughts
+
+* maybe eventually add a basic term language and interpreter
+* can we use external software/libraries for proof search?
+
+# interpretation of types
+	- example programs in `msph`
+		- unified syntax for types and bounded polymorphism
+		- example: self typing
+		- example: conditional method existence
+		- example: capabilities?
+	- the meaning of `true` and existence of methods.
+		- undefined behaviour and `true`?
+	- how does this relate to the denotation stuff from before?
+
+# formal rules and the sequent calculus
+Check formalities.md.
+	- simple rules
+	- type constructor rules
+	- recursion and cyclic proofs
+
+# next steps?
+	- formals:
+		- formulate theorems
+			- if we use semantic subtyping, isn't it enough to
+			  prove subtyping sound with regards to set denotation?
+		- specify term language?
+	- implementation: sequent calculus based subtyping decider
+		- 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

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

example/ex1.msph

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

example/ex2.msph

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

example/ex3.msph

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

example/ex4.msph

@@ -1,20 +0,0 @@
-nominal M
-nominal N
-nominal O
-nominal P
-
-type A = {
-	member member1: & N M
-	member member2: | M N
-}
-
-type B = forall X. {
-	member member1 : & X A
-}
-
-member outer1 : box {
-	member member1: & B True
-	type T = & B A
-	member member2 : | (& T O) P
-	type S = & B False
-}

example/ex5.msph

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

example/graph.msph

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

example/non-parse/ex6.msph

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

example/self.msph

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

include/msph/msph.h

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

include/msph/token.h

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

include/msph/tree.h

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

include/spho/ctx.h

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

include/spho/err.h

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

include/spho/scope.h

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

src/msph/msph.c

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

src/msph/sphophi.c

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

src/msph/token.c

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

src/spho/bind.c

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

src/spho/ctx.c

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

src/spho/scope.c

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

src/spho/tp.c

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