Merge pull request 'type fixes and bindings + notes on subtyping' (#1) from subt-resurrection into main

Reviewed-on: #1

.clangd

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

.gitignore

@@ -51,12 +51,6 @@ Module.symvers
 Mkfile.old
 dkms.conf
 
-# CMake build dirs
-build-*/
-
-# CMake compile commands
-compile_commands.json
-
 # vim
 .*.swp
 .*.swo
@@ -64,3 +58,18 @@ compile_commands.json
 # vscode
 .vscode
 .cache
+
+# CMake
+build*/
+compile_commands.json
+
+# clangd
+.clangd
+
+# ctags tagfile
+tags
+
+# other stuff
+local/
+
+

CMakeLists.txt

@@ -6,7 +6,8 @@ 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=implicit"
+       "-Werror=incompatible-pointer-types"
        "-Werror=int-conversion")
 set(CMAKE_VERBOSE_MAKEFILE ON)
 
@@ -21,17 +22,20 @@ set(SRC_DIR src)
 set(SPHO_HEADER_DIR ${INCLUDE_DIR}/spho)
 
 set(SPHO_HEADER
+	${SPHO_HEADER_DIR}/bind.h
 	${SPHO_HEADER_DIR}/ctx.h
 	${SPHO_HEADER_DIR}/err.h
-	${SPHO_HEADER_DIR}/loc.h
 	${SPHO_HEADER_DIR}/scope.h
-	${SPHO_HEADER_DIR}/tp.h
 	${SPHO_HEADER_DIR}/spho.h
+	${SPHO_HEADER_DIR}/subt.h
+	${SPHO_HEADER_DIR}/tp.h
 )
 
 set(SPHO_SRC
+  ${SRC_DIR}/spho/bind.c
   ${SRC_DIR}/spho/ctx.c
   ${SRC_DIR}/spho/scope.c
+  ${SRC_DIR}/spho/subt.c
   ${SRC_DIR}/spho/tp.c
 )
 
@@ -53,19 +57,18 @@ target_compile_definitions(devcheck PRIVATE
 
 
 set(MSPH_SRC
+	${SRC_DIR}/msph/msph.c
+	${SRC_DIR}/msph/sphophi.c
 	${SRC_DIR}/msph/token.c
 	${SRC_DIR}/msph/tree.c
-	${SRC_DIR}/msph/sphophi.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
-	${INCLUDE_DIR}/msph/decor.h
 	${INCLUDE_DIR}/msph/sphophi.h
+	${INCLUDE_DIR}/msph/token.h
+	${INCLUDE_DIR}/msph/tree.h
 )
 
 add_executable(msph ${MSPH_SRC} ${MSPH_HEADER})

README.md

@@ -2,25 +2,24 @@
 
 experimental type system implementation
 
-## sappho grammar
+## getting and building
 
-```
+```sh
-s, t ::= s | t              (disjunction, a.k.a. union)
+git clone ssh://git@gitta.log-e.se:222/lnsol/log-e-sappho.git
-       | s & t              (conjunction, a.k.a. intersection)
+cd ./log-e-sappho
-       | s => t             (implication)
+cmake . -B build
-       | s -> t             (arrow, a.k.a. function)
+cd build
-       | forall x . t       (forall, polymorphic)
+make
-       | box t              (box, modular 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)
-
-
-x ∈ var
-n ∈ nominal
-a ∈ opname
 ```
 
+## repository content
+
+This repository contains:
+
+* a library implementation of *sappho* called `spho`.
+* a simple language parser (and soon type checker), called `msph`, developed in
+  tandem with `spho`.
+* documentation of the sappho type system in `docs/`
+
+
+

docs/about/contributions.md

@@ -0,0 +1,15 @@
+# Contributions
+
+* We introduce a type system able to express predicated types, a unified way to
+  express existance of method- and traits depending on some predicate on the
+  subtyping relation.
+* We define our subtyping relation as a natural extension to type systems based
+  on semantic subtyping.
+* We express our subtyping using a novel approach based on the sequent calculus.
+* We show the correctness of our subtyping relation and type system.
+* We explain how this type system may be used to succinctly describe programs
+  involving for example capabilities and constructions such as type classes.
+* We have implemented the type system and give examples of how its use
+  simplifies expressing many properties in object oriented languages, including
+  things like...
+

docs/about/cycle.md

@@ -0,0 +1,39 @@
+# Cyclic proofs and sappho
+
+It seems that cyclic proofs and sappho would be a good fit. The decision
+process of sappho's subtyping relation is based on the sequent calculus. Cyclic
+proofs is a system of proof search which looks for cycles in a proof tree where
+recursion leads to infinite growth of its branches. It would allow us to avoid
+explicitly using co-induction and thus simplify the description of the
+subtyping relation substantially.
+
+
+## Cyclic proofs summarized
+
+A pre-proof tree is made up of nodes representing the sequents and
+edges corresponding to the pairing of a premise with the conclusion of the
+proof rules used to derive it.
+
+In an infinite pre-proof tree there might be cycles. These are paths along
+which equivalent nodes repeat infinitely often. If we are able to identify such
+a path, and the proof makes "progress" each round of the cycle, we can admiss
+it as a proof. If this can be done for all infinite paths, the pre-proof tree
+admissable as an actual proof tree.
+
+
+In order to use this strategy to decide our subtyping relation, we need:
+* Proof rules
+* Proof tree cycle detection
+* Admissability check, i.e. does the cycle make progress.
+
+See here for more info:
+
+* [fxpl/ln notes on cyclic
+proofs][github.com/fxpl/ln/blob/main/sequel/papper/notes/cyclic-proofs.md]
+* [slides on cyclic proofs, part 1][
+http://www0.cs.ucl.ac.uk/staff/J.Brotherston/slides/PARIS_FLoC_07_18_part1.pdf
+]
+* [slides on cyclic proofs, part 2][
+http://www0.cs.ucl.ac.uk/staff/J.Brotherston/slides/PARIS_FLoC_07_18_part2.pdf
+]
+

docs/about/formalities.md

@@ -0,0 +1,398 @@
+# description of sappho formals
+
+## sappho grammar
+
+```
+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. modular 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)
+
+
+x ∈ var
+n ∈ nominal
+a ∈ opname
+```
+
+## sappho subtyping rules
+
+```cmath
+// trace pairs: none
+---- [identity]
+s, γ ⊢ s, δ
+
+// trace pairs: none
+---- [true-right]
+γ ⊢ true, δ
+
+// trace pairs: none
+---- [false-left]
+false, γ ⊢ δ
+
+// trace pairs: none
+s, t, γ ⊢ δ
+---- [conj-left]
+s & t, γ ⊢ δ
+
+// trace pairs: none
+γ ⊢ s, t, δ
+---- [disj-right]
+γ ⊢ s | t, δ
+
+// trace pairs: none
+s, γ ⊢ δ
+t, γ ⊢ δ
+---- [disj-left]
+s | t, γ ⊢ δ
+
+// trace pairs: none
+γ ⊢ s, δ
+γ ⊢ t, δ
+---- [conj-right]
+γ ⊢ s & t, δ
+
+// XXX
+// remove s => t? always make progress
+// trace pairs: none
+s => t, s, t, γ ⊢ δ
+---- [impl-left]
+s => t, s, γ ⊢ δ
+
+// trace pairs: none
+s, γ ⊢ t, δ
+---- [impl-right]
+γ ⊢ s => t, δ
+
+// box works as a kind of "forall" for concrete types
+// trace pairs: none
+box t, t, γ ⊢ δ
+---- [box-left]
+box t, γ ⊢ δ
+
+// (.)-- filters the contexts.
+// trace pairs: premise[0] -- conclusion
+γ-- ⊢ t, δ--
+---- [box-right]
+γ ⊢ box t, δ
+
+
+// using cyclic proof strategy, rule for dealing with aliases/type operators
+// becomes really simple. However, this requires well-formedness rules on types
+// to exclude typedefs like
+// type A = A
+// Or that our cycle detection excludes paths between "identical" states.
+// trace pairs: none
+γ ⊢ expand(a[t..]), δ
+----
+γ ⊢ a[t..], δ
+
+expand(a[t..]), γ ⊢ δ
+----
+a[t..], γ ⊢ δ
+
+
+// member types are filtered according to member name
+// trace pairs: premise[0] -- conclusion
+γ >> m ⊢ δ >> m
+---- [member]
+γ ⊢ δ
+
+
+// foralls are unwrapped and variable substituted with fresh name
+// i.e. we treat the bound variable nominally
+// trace pairs: premise[1] -- conclusion
+n fresh
+γ [n] ⊢ δ [n]
+---- [forall]
+γ ⊢ δ
+
+// 1 + n! premises
+// trace pairs: i ∈ [1..(n! + 1)], premise[i] -- conclusion
+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, δ
+```
+
+### context operators
+
+* box filtering
+```
+(t, γ)-- =def= t, γ--       if t == box s, for some s
+               γ--          otherwise
+```
+
+* member unwrapping
+```
+(t, γ) >> m =def= s, (γ >> m)       if t == { m : s }, for some s
+                  t, (γ >> m)       if t == box s, for some s
+                  γ >> m            otherwise
+```
+
+* forall-unwrapping and substitution
+```
+(t, γ) [n] =def= s [n/x], (γ [n])   if t == forall x . s, for some x, s
+                 t, (γ [n])         if t == box s, for some s
+                 γ [n]              otherwise
+```
+
+### trace pairs
+Trace pairs are related to cyclic proofs. They identify the pairs of 
+`premise -- conclusion` that are *productive*, i.e. leads to some progress
+making a cycle in the proof tree admissable as a cyclic proof of the nodes in
+the cycle.
+
+The trace pairs are described in the comments for each subtyping rule.
+
+### Semantic function subtyping
+
+*Here we try to give an intuitive explainer of how to reason about function
+subtyping in the semantic subtyping domain.*
+
+Given function types
+```
+a_1 -> b_1, ..., a_n -> b_n
+```
+the conjunction (intersection) of `a_i -> b_i`, i.e.
+```
+intsec = (a_1 -> b_1) & ... & (a_n -> b_n)
+```
+represents the set of functions that combines the properties of all
+`a_i -> b_i` by themselves. To get an idea of what functions this describes,
+let's start with reasoning about values, that is, functions in `intsec`.
+First we note that any function in this set accepts any argument that are in
+either of the `a_i`s.  That is, it can take any argument in the set represented
+by
+```
+a = a_1 | ... | a_n
+```
+Furthermore, a function `f` in `intsec` "promises" to map any value in `a_i` to
+a value in its corresponding `b_i`.
+Specifically, given `I ⊆ {1..n}`, a value `v` in the intersection
+```
+a_I_intsec = &[i ∈ I] a_i
+```
+is mapped to a value in
+```
+b_I_intsec = &[i ∈ I] b_i
+```
+that is,
+```
+v ∈ &[i ∈ I] a_i   implies   f(v) ∈ &[i ∈ I] b_i
+```
+
+*In the following we will "abuse notation" a bit. Try to look at it like
+talking to an old friend, and you just instinctively know exactly what they
+mean without explaining...*
+
+Now, given a type `c -> d`, how do we know if
+```
+intsec = &[i ∈ {1..n}] a_i -> b_i <: c -> d
+```
+?
+Or equivalently, friend speaking, if
+```
+∩[i ∈ {1..n}] a_i -> b_i ⊆ c -> d
+```
+?
+
+Immediately, it should be obvious that
+```
+c ⊆ a (= ∪[i ∈ {1..}] a_i)
+```
+Furthermore, it is necessary that any function in `intsec` will have to map all
+values in `c` into `d`, specifically
+```
+f ∈ intsec, v ∈ c   implies   f(v) ∈ d
+```
+Note that this does not mean that any function in `a_i -> b_i` must map all
+values in `a_i` into `d`, since it's not necessary that `a_i \ c = ø`.
+Specifically, it is not necessary that `b_i ⊆ d`. However, taking `I ⊆ {1..n}`,
+assuming
+```
+a_I_intsec = &[i ∈ I] a_i ⊆ c
+```
+then, necessarily
+```
+b_I_intsec = &[i ∈ I] b_i ⊆ d
+```
+
+Conversely, if
+```
+b_I_intsect ⊆ d
+```
+then any function in `intsec` maps `a_I_intsec` into `d`. If `a_I_intsec`
+happens to intersect with `c`, it "covers" a part of `c`. I.e. the set `I` can
+be understood as promising to map a part of `c` into `d`.
+
+Defining this formally, we say that `I_cand ⊆ {1..n}` is a (`d`-)*candidate* if,
+```
+∩[i ∈ I_cand] b_i ⊆ d
+```
+We can thus see a candidate `I_cand` as a combination, or more specifically,
+intersection of the function types `{a_i -> b_i | i ∈ I_cand}`, that according
+to the reasoning above promises to map a part of the domain into `d`, namely
+```
+∩[i ∈ I_cand] a_i
+```
+A candidate thus "covers" part of the domain or formally speaking, `I`
+(`d`-)covers a domain `s` if `I` is a (`d`-)candidate and
+```
+s ⊆ ∩[i ∈ I] a_i
+```
+If `IS ⊆ P({1..n})` then we say that `IS` (`d`-)covers `s` if all of `s` is
+covered by some `I ∈ IS`, that is
+```
+s ⊆ ∪[I ∈ IS | I is d-candidate] ∩[i ∈ I] a_i
+```
+
+Given the function types `{a_i -> b_i | i ∈ {1..n}}` and its set of candidates
+`IC = {I_cand_1..I_cand_k}`, it is fairly easy to see that
+```
+&[i ∈ {1..n}] (a_i -> b_i)  <:  c -> d
+```
+iff `IC` `d`-covers `c`:
+```
+c   ⊆   ( ∪[I_cand ∈ IC]  ∩[i ∈ I_cand] a_i )
+```
+Using some *pro gamer moves*, we can see that this is equivalent to
+```
+c   ⊆   ( ∩[I_cand ∈ IC]  ∪[i ∉ I_cand] a_i )
+```
+This gives us the final form for our subtyping rule
+```
+c, γ*    ⊢    a_i | ... | a_n, δ*
+forall I ⊆ {1..n}.
+	&[i ∈ I] b_i, γ*    ⊢    d, δ*
+	  or
+	c, γ*    ⊢    |[i ∉ I] a_i, δ*
+---- [loads-o-fun]
+a_1 -> b_1, ..., a_n -> b_n, γ ⊢ c -> d, δ
+```
+
+### Recursive subtyping
+
+Type aliases creates the possibility of recursive types, and thus we need to
+handle recursive subtyping
+
+Handling subtyping co-inductively would enable us to handle the relation
+```
+type A = { x : { y : A } }
+type B = { y : { x : B } }
+
+A <: { x : B }
+{ x : B } <: A
+```
+
+
+We have made progress if we "switch context"
+
+If we make progress and end up at the same sequent, co-induction gives us the
+conclusion.
+
+Some actions/rules lead to equivalent contexts, i.e. does not switch
+context/make progress.
+
+### Other
+
+True ~ { x : True } on the left
+False ~ { x : False } on the right
+
+or rather
+
+True ~ { x : True } in positive position
+False ~ { x : False } in negative position
+
+
+
+
+
+### implication
+```
+
+γ ⊢ s => t, u => s, δ
+
+if s, then u => s holds
+if ¬s, then s => t holds
+
+```
+
+
+altho
+```
+γ ⊢ s => t, s, δ
+```
+
+Given the msph program
+```
+nominal n
+
+type Woops[e] = {
+	member f : (e <: false => n) | (e <: false)
+}
+
+type Noooes = {
+	member f : true
+}
+```
+we can prove that, for any type `t`
+```
+Noooes <: Woops[t]
+```
+
+The derivation looks like this:
+```
+---- [identity]
+true, t <: false ⊢ n, (t <: false)
+---- [impl-right]
+true ⊢ (t <: false => n), (t <: false)
+---- [disj-right]
+true ⊢ (t <: false => n) | (t <: false)
+---- [member]
+{ f : true } ⊢ { f : (t <: false => n) | (t <: false) }
+---- [expand-right]
+{ f : true } ⊢ Woops[t]
+---- [expand-left]
+Nooes ⊢ Woops[t]
+---- [impl-right]
+⊢ Nooes => Woops[t]
+---- [box-right]
+⊢ Nooes <: Woops[t]
+```
+
+This looks a bit dangerous at first. However, if we translate the implication to
+using disjunction and negation, we get
+```
+(t <: false => N) | (t <: false) == (¬(t <: false) | n) | (t <: false)
+```
+
+Considering the two cases
+```
+(1) t == false
+(2) t != false
+```
+we see that in (1)
+```
+(¬(t <: false) | n) | (t <: false) ==
+(¬(true) | n) | (true) ==
+true
+```
+and in (2)
+```
+(¬(t <: false) | n) | (t <: false) ==
+(¬(false) | n) | false ==
+(true | n) | false ==
+true
+```
+

docs/about/interpret.md

@@ -0,0 +1,88 @@
+# interpretation of sappho
+
+Different aspects of sappho interpreted.
+
+## What is true?
+
+Our "set interpretation" of types says `true` represents the full universe of
+"things".
+
+What are these things?
+
+For all intents and purposes, a programmer can look at them as the values of
+our language.
+
+What does this mean in practical terms?
+
+Well, it means something of type `true` is "a value".
+
+What is "a value" then?
+
+That's a good question. It can be anything really.
+
+An integer?
+
+Yep!
+
+A function?
+
+Yes, m'am!
+
+A solution to the halting problem?
+
+Well, yeah! But good luck constructing that.
+
+A...
+
+I think you get my point. A value can be anything from a simple integer to
+nuclear apocalypse. The thing is, from the point of view of our program, it
+means "we cannot really say anything here".
+
+But couldn't that be dangerous?
+
+Depends on what you mean by dangerous.
+
+I mean, to be able to give everything a type?
+
+Well, let me ask you this: do you like rat poison?
+
+What? To eat?
+
+Yeah!
+
+Nooo, that'd be dangerous!
+
+Yeah, exactly my point.
+
+What?
+
+You know what rat poison is obviously, despite it being dangerous?
+
+Well, yeah...
+
+Maybe you got it already, but my point is: rat poison is dangerous, but you
+still know about it, and its existance. So, something being dangerous does not
+mean you have this blank spot of knowledge that you just keep ignoring because
+of this perceived danger.
+
+
+
+
+
+### interpretation of ⊢
+what is the interpretation of
+
+γ ⊢ δ?
+
+
+given a concrete type k
+
+conjunction of γ hold for k
+
+then 
+
+disjunction of δ hold for k
+
+
+
+

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/subt/rec-lockstep.msph

@@ -0,0 +1,9 @@
+
+type A = { x : { y : A } }
+
+type B = { y : { x : B } }
+
+
+assert { x : B } <: A
+
+assert A <: { x : B }

include/msph/decor.h

@@ -1,33 +0,0 @@
-#ifndef _MSPH_DECOR_H
-#define _MSPH_DECOR_H
-
-struct msph_tp_decor {
-	struct spho_tp		*tp;
-};
-
-#define TP_DECOR_INIT(ptr) \
-	do { \
-		(ptr)->tp = NULL; \
-	} while (0)
-
-struct msph_scope_decor {
-	struct spho_scope	*sc;
-};
-
-#define SCOPE_DECOR_INIT(ptr) \
-	do { \
-		(ptr)->sc = NULL; \
-	} while (0)
-
-struct msph_nom_decor {
-	struct spho_nom		*nom;
-};
-
-#define NOM_DECOR_INIT(ptr) \
-	do { \
-		(ptr)->nom = NULL; \
-	} while (0)
-
-#define GET_SCOPE(ptr)	((ptr)->dec.sc)
-
-#endif /* _MSPH_DECOR_H */

include/msph/sphophi.h

@@ -7,6 +7,7 @@ int	msph_sphophi_init(struct msph_tree_root *);
 int	msph_sphophi_scope(struct msph_tree_root *);
 int	msph_sphophi_nom_lookup(struct msph_tree_root *);
 int	msph_sphophi_tp(struct msph_tree_root *);
+int	msph_sphophi_tp_prebind(struct msph_tree_root *);
 
 int	msph_sphophi(struct msph_tree_root *);
 

include/msph/tree.h

@@ -5,56 +5,13 @@
 
 #include "msph/common.h"
 #include "msph/token.h"
-#include "msph/decor.h"
 
-/*
+/* tree decorations */
- * TYPES:
+struct msph_decor {
- * Conj
+	struct spho_scope	*sc;
- * Disj
+	struct spho_tp		*tp;
- * Impl
+	struct spho_nom		*nom;
- * 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
@@ -70,8 +27,8 @@
 #define MSPH_TREE_TPEXPR	0x0040
 #define MSPH_TREE_TRUE		0x0041
 #define MSPH_TREE_FALSE		0x0042
-#define MSPH_TREE_NAME		0x0043
+#define MSPH_TREE_TPNAME	0x0043
-#define MSPH_TREE_APPL		0x0044
+#define MSPH_TREE_TPAPPL	0x0044
 #define MSPH_TREE_TRAIT		0x0045
 #define MSPH_TREE_CONJ		0x0046
 #define MSPH_TREE_DISJ		0x0047
@@ -82,11 +39,64 @@
 #define MSPH_TREE_PAREN		0x004c
 
 #define MSPH_TREE_IDENT		0x0100
+#define MSPH_TREE_NAMEDECL	0x0101
+#define MSPH_TREE_NAMEREF	0x0102
 
+#define MSPH_TREE_FLAG_OFFSET		16
+
+#define MSPH_TREE_FLAG_SCOPE		(1 << (MSPH_TREE_FLAG_OFFSET))
+#define MSPH_TREE_FLAG_TP		(1 << (MSPH_TREE_FLAG_OFFSET + 1))
+#define MSPH_TREE_FLAG_NOM		(1 << (MSPH_TREE_FLAG_OFFSET + 2))
+
+#define MSPH_TREE_MASK_FLAGS		((~0x0u) << MSPH_TREE_FLAG_OFFSET)
+#define MSPH_TREE_MASK_ID		((~0x0u) ^ MSPH_TREE_MASK_FLAGS)
+
+#define ADD_FLAG(tree, flag)	\
+	do { \
+		TREE(tree)->type |= flag; \
+	} while (0)
+#define HAS_FLAG(tree, flag)	(TREE(tree)->type & (flag))
+
+#define TREE(tree)		((struct msph_tree *)tree)
+#define TEXT(tree)		((struct msph_tree_text *)tree)
+#define IDENT(tree)		((struct msph_tree_ident *)tree)
+#define TPEXPR(tree)		((struct msph_tree_tpexpr *)tree)
+
+#define HAS_SCOPE(tree)		HAS_FLAG((tree), MSPH_TREE_FLAG_SCOPE)
+#define HAS_TP(tree)		HAS_FLAG((tree), MSPH_TREE_FLAG_TP)
+#define HAS_NOM(tree)		HAS_FLAG((tree), MSPH_TREE_FLAG_NOM)
+
+#define HAS_PARAMS(tpdef)	(! STAILQ_EMPTY(&(tpdef)->params))
+
+#define TREE_ID(tree)		(((struct msph_tree *)tree)->type & \
+				    MSPH_TREE_MASK_ID)
+
+#define DECOR(tree)		(TREE(tree)->decor)
+#define SCOPE(tree)		(TREE(tree)->decor.sc)
+#define TP(tree)		(TREE(tree)->decor.tp)
+#define NOM(tree)		(TREE(tree)->decor.nom)
+
+#define DECOR_INIT(tree) \
+	do { \
+		DECOR(tree) = (struct msph_decor) { NULL, NULL, NULL }; \
+	} while (0)
 
 struct msph_tree {
-	int			type;
+	unsigned int		type;
 	struct msph_tree	*parent;
+	struct msph_decor	decor;
+};
+
+
+struct msph_tree_text {
+	struct msph_tree	hd_tr;
+	struct msph_text_pos	pos;
+};
+
+struct msph_tree_ident {
+	struct msph_tree_text	hd_txt;
+
+	char str[MSPH_IDENT_LEN];
 };
 
 struct msph_tree_root;
@@ -100,7 +110,7 @@ struct msph_tree_ident;
 struct msph_tree_tpexpr;
 
 struct msph_tree_root {
-	struct msph_tree	htr;
+	struct msph_tree	hd_tr;
 
 	struct msph_ctx		*ctx;
 
@@ -108,155 +118,144 @@ struct msph_tree_root {
 };
 
 struct msph_tree_unit {
-	struct msph_tree	htr;
+	struct msph_tree	hd_tr;
 
 	char			name[MSPH_NAME_LEN];
 	struct msph_tree_body	*body;
-	struct msph_scope_decor	dec;
 
 	STAILQ_ENTRY(msph_tree_unit)	entries;
 };
 
-struct msph_tree_text {
-	struct msph_tree	htr;
-	struct msph_text_pos	pos;
-};
-
 struct msph_tree_body {
-	struct msph_tree		htr;
+	struct msph_tree		hd_tr;
 
 	STAILQ_HEAD(msph_tree_dir_l, msph_tree_dir)	head;
 };
 
 struct msph_tree_dir {
-	struct msph_tree_text		htxt;
+	struct msph_tree_text		hd_txt;
 
 	STAILQ_ENTRY(msph_tree_dir)	entries;
 };
 
 struct msph_tree_tpdef {
-	struct msph_tree_dir		hdir;
+	struct msph_tree_dir		hd_dir;
 
-	struct msph_tree_ident		*id;
+	struct msph_tree_namedecl	*name;
+	STAILQ_HEAD(msph_tree_namedecl_l, msph_tree_namedecl)	params;
 	struct msph_tree_tpexpr		*tp;
 };
 
 struct msph_tree_nomindecl {
-	struct msph_tree_dir	hdir;
+	struct msph_tree_dir	hd_dir;
 
-	struct msph_tree_ident	*id;
+	struct msph_tree_namedecl	*name;
 };
 
 struct msph_tree_membdecl {
-	struct msph_tree_dir	hdir;
+	struct msph_tree_dir	hd_dir;
 
-	struct msph_tree_ident	*id;
+	struct msph_tree_namedecl	*name;
-	struct msph_tree_tpexpr	*tp;
+	struct msph_tree_tpexpr		*tp;
 };
 
 struct msph_tree_assert {
-	struct msph_tree_dir	hdir;
+	struct msph_tree_dir	hd_dir;
 
 	struct msph_tree_tpexpr	*ltp;
 	struct msph_tree_tpexpr	*rtp;
 };
 
-struct msph_tree_tpexpr {
+struct msph_tree_namedecl {
-	struct msph_tree_text		htxt;
+	struct msph_tree_ident		hd_id;
 
-	STAILQ_ENTRY(msph_tree_tpexpr)	entries;
+	STAILQ_ENTRY(msph_tree_namedecl)	entries;
-
-	struct msph_tp_decor		dec;
 };
 
+struct msph_tree_tpexpr {
+	struct msph_tree_text		hd_txt;
+
+	STAILQ_ENTRY(msph_tree_tpexpr)	entries;
+};
 
 struct msph_tree_true {
-	struct msph_tree_tpexpr	htpe;
+	struct msph_tree_tpexpr	hd_tpe;
 };
 
 struct msph_tree_false {
-	struct msph_tree_tpexpr	htpe;
+	struct msph_tree_tpexpr	hd_tpe;
 };
 
-struct msph_tree_name {
+struct msph_tree_nameref {
-	struct msph_tree_tpexpr	htpe;
+	struct msph_tree_ident	hd_id;
-
-	struct msph_tree_ident	*id;
 };
 
-struct msph_tree_appl {
+struct msph_tree_tpname {
-	struct msph_tree_tpexpr	htpe;
+	struct msph_tree_tpexpr		hd_tpe;
 
-	struct msph_tree_ident	*id;
+	struct msph_tree_nameref	*name;
-	STAILQ_HEAD(msph_tree_tpexpr_l, msph_tree_tpexpr) head;
+};
+
+struct msph_tree_tpappl {
+	struct msph_tree_tpexpr	hd_tpe;
+
+	struct msph_tree_nameref	*name;
+	STAILQ_HEAD(msph_tree_tpexpr_l, msph_tree_tpexpr) args;
 };
 
 struct msph_tree_trait {
-	struct msph_tree_tpexpr	htpe;
+	struct msph_tree_tpexpr	hd_tpe;
 
 	struct msph_tree_body	*body;
-
-	struct msph_scope_decor	dec;
 };
 
 struct msph_tree_conj {
-	struct msph_tree_tpexpr	htpe;
+	struct msph_tree_tpexpr	hd_tpe;
 
 	struct msph_tree_tpexpr	*ltp;
 	struct msph_tree_tpexpr	*rtp;
 };
 
 struct msph_tree_disj {
-	struct msph_tree_tpexpr	htpe;
+	struct msph_tree_tpexpr	hd_tpe;
 
 	struct msph_tree_tpexpr	*ltp;
 	struct msph_tree_tpexpr	*rtp;
 };
 
 struct msph_tree_impl {
-	struct msph_tree_tpexpr	htpe;
+	struct msph_tree_tpexpr	hd_tpe;
 
 	struct msph_tree_tpexpr	*ltp;
 	struct msph_tree_tpexpr	*rtp;
 };
 
 struct msph_tree_arrow {
-	struct msph_tree_tpexpr	htpe;
+	struct msph_tree_tpexpr	hd_tpe;
 
 	struct msph_tree_tpexpr	*ltp;
 	struct msph_tree_tpexpr	*rtp;
 };
 
 struct msph_tree_box {
-	struct msph_tree_tpexpr	htpe;
+	struct msph_tree_tpexpr	hd_tpe;
 
 	struct msph_tree_tpexpr	*inner;
 };
 
 struct msph_tree_forall {
-	struct msph_tree_tpexpr	htpe;
+	struct msph_tree_tpexpr	hd_tpe;
 
-	struct msph_tree_ident	*id;
+	struct msph_tree_namedecl	*name;
-	struct msph_tree_tpexpr	*inner;
+	struct msph_tree_tpexpr		*inner;
-
-	struct msph_scope_decor	dec;
 };
 
 struct msph_tree_paren {
-	struct msph_tree_tpexpr	htpe;
+	struct msph_tree_tpexpr	hd_tpe;
 
 	struct msph_tree_tpexpr	*inner;
 };
 
-struct msph_tree_ident {
-	struct msph_tree_text	htxt;
-
-	char str[MSPH_IDENT_LEN];
-	STAILQ_ENTRY(msph_tree_ident) entries;
-
-	struct msph_nom_decor	dec;
-};
-
 
 struct msph_tree_root	*msph_tree_makeroot(struct msph_ctx *);
 
@@ -264,7 +263,4 @@ int	msph_tree_parse(struct msph_token_stream *, struct msph_tree_root *);
 
 ssize_t	msph_tree_fprint(FILE *, struct msph_tree *);
 
-#define T(ptr)			((struct msph_tree *)ptr)
-#define TXT(ptr)		((struct msph_tree_text *)ptr)
-
 #endif

include/spho/bind.h

@@ -0,0 +1,54 @@
+#ifndef _SPHO_BIND_H
+#define _SPHO_BIND_H
+
+#include <sys/queue.h>
+
+#include "spho/scope.h"
+
+#define SPHO_BIND_UNDECLARED	0x0
+#define SPHO_BIND_UNDEFINED	0x01
+#define SPHO_BIND_TP		0x11
+#define SPHO_BIND_TP_OP		0x12
+#define SPHO_BIND_MEMB_TP	0x13
+
+union spho_prebind_val {
+	const void		*undef;
+	const struct spho_tp	*tp;
+	const struct spho_tp_op	*op;
+};
+
+struct spho_prebind_pair {
+	const struct spho_nom		*nom;
+
+	int				kind;
+	union spho_prebind_val		val;
+};
+
+struct spho_prebind {
+	struct spho_scope		*sc;
+
+	size_t				sz;
+	struct spho_prebind_pair	*binds;
+};
+
+struct spho_prebind	*spho_prebind_create(struct spho_scope *);
+
+int spho_prebind_undef(struct spho_prebind *, const struct spho_nom *);
+int spho_prebind_tp(struct spho_prebind *, const struct spho_nom *,
+    const struct spho_tp *);
+int spho_prebind_tp_op(struct spho_prebind *, const struct spho_nom *,
+    const struct spho_tp_op *);
+int spho_prebind_member_tp(struct spho_prebind *, const struct spho_nom *,
+    const struct spho_tp *);
+
+struct spho_prebind *spho_prebind_dupl(const struct spho_prebind *);
+
+void spho_prebind_free(struct spho_prebind *);
+
+
+struct spho_bind {
+	struct spho_prebind	*loc;
+	struct spho_bind	*parent;
+};
+
+#endif

include/spho/err.h

@@ -14,6 +14,8 @@
 #define SPHO_ERR_ARGINVAL	0x010003
 #define SPHO_ERR_NOM_INUSE	0x020001
 #define SPHO_ERR_NOM_NOTINSCOPE	0x020002
+#define SPHO_ERR_BIND_DUPL	0x030001
+#define SPHO_ERR_BIND_NOTFOUND	0x030002
 
 #define SPHO_ERR_IS_SYSERR(err)		(SPHO_ERR_SYS == err)
 
@@ -41,54 +43,6 @@
 		(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 */
 

include/spho/scope.h

@@ -7,40 +7,18 @@
 
 #define SPHO_NOM_LEN	128
 
+/* name */
 struct spho_nom {
 	char			s[SPHO_NOM_LEN];
-	SLIST_ENTRY(spho_nom)	next;
+	SLIST_ENTRY(spho_nom)	next; // TODO change to allocs
 };
 
 SLIST_HEAD(spho_nom_l, spho_nom);
 
+
 #define TP_KONST_KEY_TRUE	0x43445 /* don't change!!!!! */
 #define TP_KONST_KEY_FALSE	0x66a57 /* don't change!1! */
 
-
-struct spho_var {
-	struct spho_nom		nom;
-
-	STAILQ_ENTRY(spho_var)	next;
-};
-
-STAILQ_HEAD(spho_var_l, spho_var);
-
-struct spho_bind {
-	struct spho_nom		nom;
-	struct spho_tpop	*op;
-};
-
-struct spho_tpop {
-	struct spho_var_l	params;
-	struct spho_tp		*def;
-};
-
-struct spho_rec {
-	struct spho_nom		mnom;
-	struct spho_tp		*tp;
-};
-
 /* type data */
 struct tp_binop_data {
 	struct spho_tp		*left;
@@ -51,11 +29,6 @@ struct tp_unop_data {
 	struct spho_tp		*operand;
 };
 
-struct tp_binding_data {
-	struct spho_nom		*nom;
-	struct spho_tp		*bound;
-};
-
 struct tp_nom_data {
 	struct spho_nom		*nom;
 };
@@ -70,6 +43,16 @@ struct tp_konst_data {
 	const char	*str;
 };
 
+struct tp_forall_data {
+	struct spho_nom		*nom;
+	struct spho_tp		*tp;
+};
+
+struct tp_member_data {
+	struct spho_nom		*nom;
+	struct spho_tp		*tp;
+};
+
 extern const struct tp_konst_data tp_konst_true;
 extern const struct tp_konst_data tp_konst_false;
 
@@ -80,22 +63,30 @@ extern const struct tp_konst_data tp_konst_false;
 union tp_data {
 	struct tp_binop_data	binop;
 	struct tp_unop_data	unop;
-	struct tp_binding_data	bind;
 	struct tp_appl_data	appl;
 	struct tp_nom_data	nom;
 	struct tp_konst_data	konst;
+	struct tp_forall_data	fa;
+	struct tp_member_data	memb;
 };
 
 /* sappho type */
 struct spho_tp {
 	struct spho_scope	*sc;
 
-	int			form;
+	int			kind;
 	union tp_data		d;
 
 	STAILQ_ENTRY(spho_tp)	entries;
 };
 
+struct spho_tp_op {
+	struct spho_scope	*sc;
+
+	struct spho_scope	*op_sc;
+	struct spho_tp		*op_tp;
+};
+
 STAILQ_HEAD(spho_tp_l, spho_tp);
 
 struct spho_tp_ptr {
@@ -106,24 +97,33 @@ struct spho_tp_ptr {
 STAILQ_HEAD(spho_tp_ptr_l, spho_tp_ptr);
 
 struct spho_tp_alloc {
-	struct spho_tp	tp;
+	union {
+		struct spho_tp		tp;
+		struct spho_tp_op	tp_op;
+	}		alloc;
 
 	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;
+
 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;
 
+	struct spho_prebind	*bind_loc;
+
 	SLIST_ENTRY(spho_scope)	next;
 };
 
@@ -140,9 +140,16 @@ 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,
+int	spho_scope_nom_lookup_str(struct spho_scope *, const char *, size_t,
-		    struct spho_nom **);
+	    struct spho_nom **);
-int		spho_scope_nom_lookup(struct spho_scope *, const char *, size_t,
+int	spho_scope_nom_lookup_str_strict(struct spho_scope *, const char *,
-		    struct spho_nom **);
+	    size_t, struct spho_nom **);
+
+int	spho_scope_prebind_init(struct spho_scope *);
+int	spho_scope_prebind_tp(struct spho_scope *, struct spho_nom *,
+	    struct spho_tp *);
+int	spho_scope_prebind_tp_op(struct spho_scope *, struct spho_nom *,
+	    struct spho_tp_op *);
+int	spho_scope_prebind_undef(struct spho_scope *, struct spho_nom *);
 
 #endif /* _SPHO_SCOPE_H */

include/spho/spho.h

@@ -6,4 +6,81 @@
 #include "spho/err.h"
 #include "spho/ctx.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 /* ifdef SPHO_USE_STRLCPY */
+
+#define SPHO_STRINGIFY(a)	#a
+#define SPHO_MACRO_STR(b)	SPHO_STRINGIFY(b)
+#define __LINE__S		SPHO_MACRO_STR(__LINE__)
+
+
+#define SPHO_RIP(msg, ...) \
+	do { \
+		fprintf(stderr, "SPHO_RIP(" msg ")@" \
+		    __FILE__ ":" __LINE__S \
+		    " failed. Aborting.\n" __VA_OPT__(,) __VA_ARGS__); \
+		abort(); \
+	} while (0)
+
+
+#ifdef SPHO_DEBUG
+
+#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
+#define SPHO_DEBUG_PRINT(fmt, ...)
+#endif /* ifdef SPHO_ENABLE_DEBUG_PRINT */
+
+#endif /* ifdef SPHO_DEBUG */
+
 #endif

include/spho/subt.h

@@ -0,0 +1,9 @@
+#ifndef _SPHO_SUBT_H
+#define _SPHO_SUBT_H
+
+#include "spho/scope.h"
+
+int spho_is_subt(struct spho_ctx *, const struct spho_tp *,
+    const struct spho_tp *);
+
+#endif /* ifndef _SPHO_SUBT_H */

include/spho/tp.h

@@ -12,20 +12,24 @@
 #define SPHO_TP_FORM_BOX	0x14
 #define SPHO_TP_FORM_FORALL	0x15
 #define SPHO_TP_FORM_APPL	0x16
+#define SPHO_TP_FORM_MEMBER	0x17
+#define SPHO_TP_FORM_NOMINAL	0x18
 
 #define SPHO_TP_FORM_TRUE	0x20
 #define SPHO_TP_FORM_FALSE	0x21
-#define SPHO_TP_FORM_NOM	0x23
+#define SPHO_TP_FORM_NAME	0x23
 
-#define SPHO_TP_FORM_MEMBER	0x24
+#define SPHO_TP_FORM_VAR	0x40
 
-// #define SPHO_TP_FORM_SUB	0x96
+#define SPHO_TP_FORM_MASK	0xff
+
+#define SPHO_TP_MOD_FIRST	(SPHO_TP_FORM_MASK + 1)
+
+// #define SPHO_TP_MOD_VAR		(SPHO_TP_FLAG_FIRST)
+// #define SPHO_TP_MOD_NOMINAL	(SPHO_TP_FLAG_FIRST << 1)
 
 #define SPHO_TP_ERR(tp, err)	SPHO_ERR((tp)->sc->ctx, (err))
 
-//struct spho_var	*spho_var_create(struct spho_scope *, char *, size_t);
-//struct spho_var	*spho_var_get(struct spho_scope *, char *, size_t);
-
 struct spho_tp	*spho_tp_create_conj(struct spho_scope *, struct spho_tp *,
 		    struct spho_tp *);
 struct spho_tp	*spho_tp_create_disj(struct spho_scope *, struct spho_tp *,
@@ -45,10 +49,11 @@ struct spho_tp	*spho_tp_create_appl(struct spho_scope *, struct spho_nom *,
 		    struct spho_tp_l *);
 struct spho_tp	*spho_tp_create_member(struct spho_scope *, struct spho_nom *,
 		    struct spho_tp *);
-//struct spho_tp	*spho_tp_create_const(struct spho_scope *, struct spho_const *);
+struct spho_tp	*spho_tp_create_var(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_nominal(struct spho_scope *, struct spho_nom *);
-// struct spho_tp	*spho_tp_create_sub(struct spho_scope *, struct spho_tp *,
+
-//		    struct spho_tp *);
+struct spho_tp_op *spho_tp_op_create(struct spho_scope *,
+    struct spho_scope *, struct spho_tp *);
 
 void	spho_tp_destroy(struct spho_tp *);
 

include/spho/util.h

@@ -1,25 +0,0 @@
-#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/token.c

@@ -5,9 +5,12 @@
 #include <string.h>
 #include <ctype.h>
 
+#include "spho/spho.h"
+
 #include "msph/err.h"
 #include "msph/token.h"
 
+
 struct msph_matcher {
 	size_t		off;
 	size_t		matchlen;

src/spho/bind.c

@@ -0,0 +1,165 @@
+#include <sys/queue.h>
+#include <string.h>
+
+#include "spho/spho.h"
+#include "spho/scope.h"
+#include "spho/bind.h"
+
+struct spho_prebind *
+spho_prebind_create(struct spho_scope *sc)
+{
+	size_t i;
+	struct spho_nom *nom;
+	struct spho_prebind *bind;
+
+	SPHO_PRECOND(sc != NULL);
+
+	if ((bind = calloc(1, sizeof(*bind))) == NULL) {
+		SPHO_ERR(sc->ctx, SPHO_ERR_SYS);
+		return (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->n_noms;
+
+
+	i = 0;
+	SLIST_FOREACH(nom, &sc->noms, next) {
+		SPHO_ASSERT(i < bind->sz);
+		bind->binds[i++] = (struct spho_prebind_pair) { NULL, 0, NULL };
+	}
+
+	return (bind);
+}
+
+int
+spho_prebind_undef(struct spho_prebind *bind,
+    const struct spho_nom *nom)
+{
+	size_t i;
+	SPHO_PRECOND(bind != NULL);
+	SPHO_PRECOND(nom != NULL);
+
+	for (i = 0; i < bind->sz; i++) {
+		if (nom == bind->binds[i].nom) {
+			if (bind->binds[i].kind != SPHO_BIND_UNDECLARED) {
+				SPHO_ERR(bind->sc->ctx, SPHO_ERR_BIND_DUPL);
+				return (-1);
+			}
+			bind->binds[i].kind = SPHO_BIND_UNDEFINED;
+		}
+	}
+
+	return (0);
+}
+int
+spho_prebind_tp(struct spho_prebind *bind, const struct spho_nom *nom,
+    const struct spho_tp *tp)
+{
+	size_t i;
+
+	SPHO_PRECOND(bind != NULL);
+	SPHO_PRECOND(nom != NULL);
+	SPHO_PRECOND(tp != NULL);
+
+	for (i = 0; i < bind->sz; i++) {
+		if (nom == bind->binds[i].nom) {
+			if (bind->binds[i].kind != SPHO_BIND_UNDECLARED) {
+				SPHO_ERR(bind->sc->ctx, SPHO_ERR_BIND_DUPL);
+				return (-1);
+			}
+			bind->binds[i].kind = SPHO_BIND_TP;
+			bind->binds[i].val = (union spho_prebind_val) tp;
+			return (0);
+		}
+	}
+
+	SPHO_ERR(bind->sc->ctx, SPHO_ERR_BIND_NOTFOUND);
+	return (-1);
+}
+
+int
+spho_prebind_tp_op(struct spho_prebind *bind, const struct spho_nom *nom,
+    const struct spho_tp_op *op)
+{
+	size_t i;
+
+	SPHO_PRECOND(bind != NULL);
+	SPHO_PRECOND(nom != NULL);
+	SPHO_PRECOND(op != NULL);
+
+	for (i = 0; i < bind->sz; i++) {
+		if (nom == bind->binds[i].nom) {
+			if (bind->binds[i].kind != SPHO_BIND_UNDECLARED) {
+				SPHO_ERR(bind->sc->ctx, SPHO_ERR_BIND_DUPL);
+				return (-1);
+			}
+			bind->binds[i].kind = SPHO_BIND_TP_OP;
+			bind->binds[i].val = (union spho_prebind_val) op;
+			return (0);
+		}
+	}
+
+	SPHO_ERR(bind->sc->ctx, SPHO_ERR_BIND_NOTFOUND);
+	return (-1);
+}
+
+int
+spho_prebind_member_tp(struct spho_prebind *bind, const struct spho_nom *nom,
+    const struct spho_tp *memb_tp)
+{
+	size_t i;
+
+	SPHO_PRECOND(bind != NULL);
+	SPHO_PRECOND(nom != NULL);
+	SPHO_PRECOND(memb_tp != NULL);
+
+	for (i = 0; i < bind->sz; i++) {
+		if (nom == bind->binds[i].nom) {
+			if (bind->binds[i].kind != SPHO_BIND_UNDECLARED) {
+				SPHO_ERR(bind->sc->ctx, SPHO_ERR_BIND_DUPL);
+				return (-1);
+			}
+			bind->binds[i].kind = SPHO_BIND_MEMB_TP;
+			bind->binds[i].val = (union spho_prebind_val) memb_tp;
+			return (0);
+		}
+	}
+
+	SPHO_ERR(bind->sc->ctx, SPHO_ERR_BIND_NOTFOUND);
+	return (-1);
+}
+
+struct spho_prebind *
+spho_prebind_dupl(const struct spho_prebind *bind)
+{
+	struct spho_prebind *cp;
+
+	if ((cp = calloc(1, sizeof(*cp))) == NULL) {
+		SPHO_ERR(bind->sc->ctx, SPHO_ERR_SYS);
+		return (NULL);
+	}
+
+	if ((cp->binds = calloc(bind->sz, sizeof(*cp->binds))) == NULL) {
+		SPHO_ERR(bind->sc->ctx, SPHO_ERR_SYS);
+		free(cp);
+		return (NULL);
+	}
+
+	memcpy(cp->binds, bind->binds, bind->sz * sizeof(*bind->binds));
+
+	return (cp);
+}
+
+void
+spho_prebind_free(struct spho_prebind *bind)
+{
+	free(bind->binds);
+	free(bind);
+}

src/spho/ctx.c

@@ -4,7 +4,7 @@
 #include <stdlib.h>
 #include <string.h>
 
-#include "spho/ctx.h"
+#include "spho/spho.h"
 
 static const char *spho_ctx_sys_strerror(struct spho_ctx *);
 static const char *spho_ctx_intern_strerror(struct spho_ctx *);
@@ -23,6 +23,10 @@ struct spho_err spho_errmsgs[] = {
 
 	{ SPHO_ERR_NOM_INUSE,	"name already declared in current scope" },
 	{ SPHO_ERR_NOM_NOTINSCOPE,	"name not in scope" },
+
+	{ SPHO_ERR_BIND_NOTFOUND, "binding name not found in scope" },
+	{ SPHO_ERR_BIND_DUPL, "duplicate binding" },
+
 	{ -1, NULL }
 };
 
@@ -91,7 +95,7 @@ spho_ctx_sys_strerror(struct spho_ctx *ctx)
 	res = snprintf(ctx->errbuf, sizeof(ctx->errbuf),
 	    "spho_syserr: %s (%d) (%s:%d)", strerror(ctx->err_info),
 	    ctx->err_info, ctx->filebuf, ctx->errline);
-	if (res >= sizeof(ctx->errbuf))
+	if (res >= (ssize_t)sizeof(ctx->errbuf))
 		ctx->errbuf[sizeof(ctx->errbuf) - 1] = '\0';
 #else
 	res = snprintf(ctx->errbuf, sizeof(ctx->errbuf),

src/spho/scope.c

@@ -3,26 +3,33 @@
 #include <stdlib.h>
 #include <string.h>
 
+#include "spho/spho.h"
 #include "spho/ctx.h"
 #include "spho/scope.h"
-#include "spho/util.h"
+#include "spho/bind.h"
 
 static void spho_nom_term(struct spho_nom *);
 
-static int spho_scope_nom_get_norec(struct spho_scope *, const char *, size_t ,
+static int scope_nom_lookup_str_local(struct spho_scope *, const char *,
-    struct spho_nom **);
+    size_t, struct spho_nom **);
+static int scope_nom_in_local(struct spho_scope *, struct spho_nom *);
 
 int
 spho_scope_init(struct spho_scope *sc, struct spho_ctx *ctx,
     struct spho_scope *p)
 {
-	SLIST_INIT(&sc->subs);
-	SLIST_INIT(&sc->noms);
-	TAILQ_INIT(&sc->tps);
-
 	sc->ctx = ctx;
 	sc->parent = p;
 
+	SLIST_INIT(&sc->subs);
+
+	SLIST_INIT(&sc->noms);
+	sc->n_noms = 0;
+
+	TAILQ_INIT(&sc->tps);
+
+	sc->bind_loc = NULL;
+
 	return (0);
 }
 
@@ -34,6 +41,10 @@ spho_scope_term(struct spho_scope *sc)
 	SPHO_UTIL_SLIST_DESTROY(&sc->noms, spho_nom, next, spho_nom_term);
 
 	sc->parent = NULL;
+
+	if (sc->bind_loc == NULL)
+		spho_prebind_free(sc->bind_loc);
+	sc->bind_loc = NULL;
 }
 
 struct spho_scope *
@@ -67,7 +78,7 @@ spho_scope_create(struct spho_scope *sc)
 
 
 static void
-spho_nom_term(struct spho_nom *nom)
+spho_nom_term(__attribute__((unused)) struct spho_nom *nom)
 {
 	return;
 }
@@ -87,16 +98,12 @@ spho_scope_destroy(struct spho_scope *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;
 
 	nom = NULL;
 
-	if (spho_scope_nom_get_norec(sc, nomstr, sz, &nom) == -1)
+	if (scope_nom_lookup_str_local(sc, nomstr, sz, &nom) == -1)
 		return (NULL);
 
 	if (nom != NULL) {
@@ -109,25 +116,14 @@ spho_scope_nom_add(struct spho_scope *sc, const char *nomstr, size_t sz)
 		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);
+	sc->n_noms++;
 
 	return (nom);
 err:
@@ -137,7 +133,7 @@ err:
 
 
 int
-spho_scope_nom_get(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;
@@ -164,12 +160,10 @@ spho_scope_nom_get(struct spho_scope *sc, const char *nomstr, size_t sz,
 }
 
 int
-spho_scope_nom_lookup(struct spho_scope *sc, const char *nomstr, size_t sz,
+spho_scope_nom_lookup_str_strict(struct spho_scope *sc, const char *nomstr,
-    struct spho_nom **out)
+    size_t sz, struct spho_nom **out)
 {
-	int ret;
+	if (spho_scope_nom_lookup_str(sc, nomstr, sz, out) == -1)
-
-	if (spho_scope_nom_get(sc, nomstr, sz, out) == -1)
 		return (-1);
 
 	if (*out == NULL) {
@@ -179,9 +173,56 @@ spho_scope_nom_lookup(struct spho_scope *sc, const char *nomstr, size_t sz,
 
 	return (0);
 }
+
+int
+spho_scope_prebind_init(struct spho_scope *sc)
+{
+	if ((sc->bind_loc = spho_prebind_create(sc)) 
+	    == NULL) {
+		return (-1);
+	}
+
+	return (0);
+}
+
+int
+spho_scope_prebind_tp(struct spho_scope *sc, struct spho_nom *nom,
+    struct spho_tp *tp)
+{
+	if (! scope_nom_in_local(sc, nom)) {
+		SPHO_ERR(sc->ctx, SPHO_ERR_NOM_NOTINSCOPE);
+		return (-1);
+	}
+
+	return (spho_prebind_tp(sc->bind_loc, nom, tp));
+}
+
+int
+spho_scope_prebind_tp_op(struct spho_scope *sc, struct spho_nom *nom,
+    struct spho_tp_op *tp_op)
+{
+	if (! scope_nom_in_local(sc, nom)) {
+		SPHO_ERR(sc->ctx, SPHO_ERR_NOM_NOTINSCOPE);
+		return (-1);
+	}
+
+	return (spho_prebind_tp_op(sc->bind_loc, nom, tp_op));
+}
+
+int
+spho_scope_prebind_undef(struct spho_scope *sc, struct spho_nom *nom)
+{
+	if (! scope_nom_in_local(sc, nom)) {
+		SPHO_ERR(sc->ctx, SPHO_ERR_NOM_NOTINSCOPE);
+		return (-1);
+	}
+
+	return (spho_prebind_undef(sc->bind_loc, nom));
+}
+
 static int
-spho_scope_nom_get_norec(struct spho_scope *sc, const char *nomstr, size_t sz,
+scope_nom_lookup_str_local(struct spho_scope *sc, const char *nomstr,
-    struct spho_nom **out)
+    size_t sz, struct spho_nom **out)
 {
 	struct spho_nom *nom;
 
@@ -202,3 +243,16 @@ spho_scope_nom_get_norec(struct spho_scope *sc, const char *nomstr, size_t sz,
 
 	return (0);
 }
+
+static int
+scope_nom_in_local(struct spho_scope *sc, struct spho_nom *nom)
+{
+	struct spho_nom *sc_nom;
+
+	SLIST_FOREACH(sc_nom, &sc->noms, next) {
+		if (sc_nom == nom)
+			return (1);
+	}
+
+	return (0);
+}

src/spho/subt.c

@@ -0,0 +1,239 @@
+/*
+ * Subtyping
+ */
+#include <stdlib.h>
+
+#include "spho/bind.h"
+#include "spho/bind.h"
+#include "spho/spho.h"
+
+#include "spho/subt.h"
+
+/* bound type */
+struct bound {
+	struct spho_bind		*bind;
+	const struct spho_tp		*tp;
+};
+
+/* sequent */
+struct sqnt {
+	struct spho_ctx		*ctx;
+
+	size_t			sz;
+	size_t			filled;
+	struct bound		*elms;
+};
+
+/* sequent turnstile */
+struct tstl {
+	struct sqnt		left;
+	struct sqnt		right;
+};
+
+
+static struct bound *bound_tp(const struct spho_tp *);
+
+
+/* read scopes and create bound type */
+struct bound *
+bound_tp(const struct spho_tp *tp)
+{
+	struct spho_scope	*sc;
+	struct spho_bind	*bind, *more_bind;
+
+	struct bound	*ret;
+
+	SPHO_PRECOND(tp != NULL);
+	SPHO_PRECOND(tp->sc != NULL);
+	SPHO_PRECOND(tp->sc->bind_loc != NULL);
+
+	sc = tp->sc;
+	bind = NULL;
+
+	if ((ret = calloc(1, sizeof(*ret))) == NULL) {
+		SPHO_ERR(sc->ctx, SPHO_ERR_SYS);
+		return (NULL);
+	}
+	ret->tp = tp;
+
+	
+	if ((ret->bind = calloc(1, sizeof(*ret->bind))) == NULL) {
+		SPHO_ERR(sc->ctx, SPHO_ERR_SYS);
+		goto err;
+	}
+
+	/* initialize parent and duplicate scope-local bindings */
+	ret->bind->parent = NULL;
+	if ((ret->bind->loc = spho_prebind_dupl(sc->bind_loc)) == NULL) {
+		goto err;
+	}
+
+	/* iterate up through parent scopes and gather their local bindings */
+	bind = ret->bind;
+	while ((sc = sc->parent) != NULL) {
+		if ((more_bind = calloc(1, sizeof(*more_bind))) == NULL) {
+			SPHO_ERR(sc->ctx, SPHO_ERR_SYS);
+			goto err;
+		}
+		more_bind->parent = NULL;
+		if ((more_bind->loc = spho_prebind_dupl(sc->bind_loc))
+		    == NULL) {
+			goto err;
+		}
+		bind->parent = more_bind;
+		bind = bind->parent;
+	}
+
+	return (ret);
+
+err:
+	while (ret->bind != NULL) {
+		bind = ret->bind;
+		ret->bind = ret->bind->parent;
+
+		spho_prebind_free(bind->loc);
+		free(bind);
+	}
+
+	return (NULL);
+}
+
+static int
+sqnt_init(struct spho_ctx *ctx, size_t initsz, struct sqnt *seq)
+{
+	if (initsz == 0)
+		initsz = 0x10; /* just feels good */
+
+	seq->ctx = ctx;
+
+	if ((seq->elms = calloc(initsz, sizeof(*seq->elms))) == NULL) {
+		SPHO_ERR(seq->ctx, SPHO_ERR_SYS);
+		goto err;
+	}
+
+	seq->sz = initsz;
+	seq->filled = 0;
+
+	return (0);
+err:
+	if (seq->elms != NULL)
+		free(seq->elms);
+	seq->elms = NULL;
+
+	return (-1);
+}
+
+static int
+sqnt_makebig(struct sqnt *seq)
+{
+	size_t		new_sz;
+	struct bound *new_elms;
+
+	SPHO_PRECOND(seq != NULL);
+	SPHO_PRECOND(seq->sz > 0);
+	SPHO_PRECOND(seq->sz <= (SIZE_MAX >> 1));
+	SPHO_PRECOND(seq->elms != NULL);
+
+	new_sz = seq->sz << 1;
+
+	if ((new_elms = realloc(seq->elms, new_sz)) == NULL) {
+		SPHO_ERR(seq->ctx, SPHO_ERR_SYS);
+		return (-1);
+	}
+
+	seq->sz = new_sz;
+	seq->elms = new_elms;
+
+	return (0);
+}
+
+static int
+sqnt_add_bound(struct sqnt *seq, struct bound *elm)
+{
+	SPHO_PRECOND(seq->filled <= seq->sz);
+
+	if (seq->filled >= seq->sz && (sqnt_makebig(seq) == -1))
+		return (-1);
+
+	seq->elms[seq->filled++] = *elm;
+
+	SPHO_POSTCOND(seq->filled <= seq->sz);
+
+	return (0);
+}
+
+static int
+tstl_init(struct spho_ctx *ctx, size_t lsz, size_t rsz,
+    struct tstl *ts)
+{
+	if (sqnt_init(ctx, lsz, &ts->left) == -1)
+		return (-1);
+	if (sqnt_init(ctx, rsz, &ts->right) == -1)
+		return (-1);
+
+	return (0);
+}
+
+static struct tstl *
+tstl_alloc(struct spho_ctx *ctx)
+{
+	struct tstl *ts;
+
+	if ((ts = calloc(1, sizeof(*ts))) == NULL) {
+		SPHO_ERR(ctx, SPHO_ERR_SYS);
+		return (NULL);
+	}
+	if (tstl_init(ctx, 0, 0, ts) == -1) {
+		free(ts);
+		return (NULL);
+	}
+
+	return (ts);
+}
+
+static int
+tstl_add_left(struct tstl *ts, struct bound *tp)
+{
+	return (sqnt_add_bound(&ts->left, tp));
+}
+
+static int
+tstl_add_right(struct tstl *ts, struct bound *tp)
+{
+	return (sqnt_add_bound(&ts->right, tp));
+}
+
+static int
+tstl_decide(struct tstl *ts)
+{
+	SPHO_RIP("implement");
+}
+
+int
+spho_is_subt(struct spho_ctx *ctx, const struct spho_tp *tp_left,
+    const struct spho_tp *tp_right)
+{
+	struct tstl ts;
+	struct bound *left, *right;
+
+	if ((left = bound_tp(tp_left)) == NULL)
+		return (-1);
+	if ((right = bound_tp(tp_right)) == NULL)
+		return (-1);
+
+	// TODO check well-definedness of types (e.g. no undefs)
+
+	if ((tstl_init(ctx, 0, 0, &ts)) == -1)
+		return (-1);
+
+	if (tstl_add_left(&ts, left) == -1)
+		return (-1);
+	if (tstl_add_right(&ts, right) == -1)
+		return (-1);
+
+	if (tstl_decide(&ts) == -1)
+		return (-1);
+
+	return (-1);
+}
+

src/spho/tp.c

@@ -2,21 +2,13 @@
 
 #include <stdlib.h>
 
-#include "spho/ctx.h"
+#include "spho/spho.h"
-#include "spho/scope.h"
 #include "spho/tp.h"
 
 
 const struct tp_konst_data tp_konst_true = { TP_KONST_KEY_TRUE, "True" };
 const struct tp_konst_data tp_konst_false = { TP_KONST_KEY_FALSE, "False" };
 
-//struct spho_tp	*
-//spho_tp_create_disj(struct spho_ctx *, struct spho_tp *, struct spho_tp *,
-//    struct spho_tp *)
-//{
-//
-//}
-
 static struct spho_tp *
 spho_tp_alloc(struct spho_scope *sc)
 {
@@ -33,6 +25,22 @@ spho_tp_alloc(struct spho_scope *sc)
 	return ((struct spho_tp *)tp_alloc);
 }
 
+static struct spho_tp_op *
+spho_tp_op_alloc(struct spho_scope *sc)
+{
+	struct spho_tp_alloc *tp_alloc;
+
+	if ((tp_alloc = calloc(1, sizeof(*tp_alloc))) == NULL) {
+		SPHO_SC_ERR(sc, SPHO_ERR_SYS);
+		return (NULL);
+	}
+
+	((struct spho_tp_op *)tp_alloc)->sc = sc;
+	TAILQ_INSERT_TAIL(&sc->tps, tp_alloc, allocs);
+
+	return ((struct spho_tp_op *)tp_alloc);
+}
+
 static void
 spho_tp_free(struct spho_tp *tp)
 {
@@ -56,7 +64,7 @@ spho_tp_create_conj(struct spho_scope *sc, struct spho_tp *ltp,
 	if ((tp = spho_tp_alloc(sc)) == NULL)
 		return (NULL);
 
-	tp->form = SPHO_TP_FORM_CONJ;
+	tp->kind = SPHO_TP_FORM_CONJ;
 	tp->d.binop.left = ltp;
 	tp->d.binop.right = rtp;
 
@@ -72,7 +80,7 @@ spho_tp_create_disj(struct spho_scope *sc, struct spho_tp *ltp,
 	if ((tp = spho_tp_alloc(sc)) == NULL)
 		return (NULL);
 
-	tp->form = SPHO_TP_FORM_DISJ;
+	tp->kind = SPHO_TP_FORM_DISJ;
 	tp->d.binop.left = ltp;
 	tp->d.binop.right = rtp;
 
@@ -88,7 +96,7 @@ spho_tp_create_impl(struct spho_scope *sc, struct spho_tp *ltp,
 	if ((tp = spho_tp_alloc(sc)) == NULL)
 		return (NULL);
 
-	tp->form = SPHO_TP_FORM_IMPL;
+	tp->kind = SPHO_TP_FORM_IMPL;
 	tp->d.binop.left = ltp;
 	tp->d.binop.right = rtp;
 
@@ -104,7 +112,7 @@ spho_tp_create_arrow(struct spho_scope *sc, struct spho_tp *ltp,
 	if ((tp = spho_tp_alloc(sc)) == NULL)
 		return (NULL);
 
-	tp->form = SPHO_TP_FORM_ARROW;
+	tp->kind = SPHO_TP_FORM_ARROW;
 	tp->d.binop.left = ltp;
 	tp->d.binop.right = rtp;
 
@@ -119,7 +127,7 @@ spho_tp_create_box(struct spho_scope *sc, struct spho_tp *inner)
 	if ((tp = spho_tp_alloc(sc)) == NULL)
 		return (NULL);
 
-	tp->form = SPHO_TP_FORM_BOX;
+	tp->kind = SPHO_TP_FORM_BOX;
 	tp->d.unop.operand = inner;
 
 	return (tp);
@@ -134,9 +142,9 @@ spho_tp_create_forall(struct spho_scope *sc, struct spho_nom *nom,
 	if ((ret = spho_tp_alloc(sc)) == NULL)
 		return (NULL);
 
-	ret->form = SPHO_TP_FORM_FORALL;
+	ret->kind = SPHO_TP_FORM_FORALL;
-	ret->d.bind.nom = nom;
+	ret->d.fa.nom = nom;
-	ret->d.bind.bound = tp;
+	ret->d.fa.tp = tp;
 
 	return (ret);
 }
@@ -149,7 +157,7 @@ spho_tp_create_true(struct spho_scope *sc)
 	if ((ret = spho_tp_alloc(sc)) == NULL)
 		return (NULL);
 
-	ret->form = SPHO_TP_FORM_TRUE;
+	ret->kind = SPHO_TP_FORM_TRUE;
 	ret->d.konst = tp_konst_true;
 
 	return (ret);
@@ -163,7 +171,7 @@ spho_tp_create_false(struct spho_scope *sc)
 	if ((ret = spho_tp_alloc(sc)) == NULL)
 		return (NULL);
 
-	ret->form = SPHO_TP_FORM_FALSE;
+	ret->kind = SPHO_TP_FORM_FALSE;
 	ret->d.konst = tp_konst_false;
 
 	return (ret);
@@ -177,7 +185,7 @@ spho_tp_create_name(struct spho_scope *sc, struct spho_nom *nom)
 	if ((ret = spho_tp_alloc(sc)) == NULL)
 		return (NULL);
 
-	ret->form = SPHO_TP_FORM_NOM;
+	ret->kind = SPHO_TP_FORM_NAME;
 	ret->d.nom.nom = nom;
 
 	return (ret);
@@ -192,7 +200,7 @@ spho_tp_create_appl(struct spho_scope *sc, struct spho_nom *nom,
 	if ((ret = spho_tp_alloc(sc)) == NULL)
 		return (NULL);
 
-	ret->form = SPHO_TP_FORM_APPL;
+	ret->kind = SPHO_TP_FORM_APPL;
 	ret->d.appl.nom = nom;
 	ret->d.appl.args = args;
 
@@ -208,23 +216,72 @@ spho_tp_create_member(struct spho_scope *sc, struct spho_nom *nom,
 	if ((ret = spho_tp_alloc(sc)) == NULL)
 		return (NULL);
 
-	ret->form = SPHO_TP_FORM_MEMBER;
+	ret->kind = SPHO_TP_FORM_MEMBER;
-	ret->d.bind.nom = nom;
+	ret->d.memb.nom = nom;
-	ret->d.bind.bound = tp;
+	ret->d.memb.tp = tp;
 
 	return (ret);
 }
 
+struct spho_tp *
+spho_tp_create_nominal(struct spho_scope *sc, struct spho_nom *nom)
+{
+	struct spho_tp *ret;
+
+	if ((ret = spho_tp_alloc(sc)) == NULL)
+		return (NULL);
+
+	ret->kind = SPHO_TP_FORM_NOMINAL;
+	ret->d.nom.nom = nom;
+
+	return (ret);
+}
+
+struct spho_tp *
+spho_tp_create_var(struct spho_scope *sc, struct spho_nom *nom)
+{
+	struct spho_tp *ret;
+
+	if ((ret = spho_tp_alloc(sc)) == NULL)
+		return (NULL);
+
+	ret->kind = SPHO_TP_FORM_VAR;
+	ret->d.nom.nom = nom;
+
+	return (ret);
+}
+
+
+struct spho_tp_op *
+spho_tp_op_create(struct spho_scope *sc, struct spho_scope *op_sc, struct spho_tp *tp)
+{
+	struct spho_tp_op *op;
+
+	SPHO_PRECOND(sc != NULL);
+	SPHO_PRECOND(op_sc != NULL);
+	SPHO_PRECOND(tp != NULL);
+
+	if ((op = spho_tp_op_alloc(sc)) == NULL)
+		return (NULL);
+
+	op->sc = sc;
+	op->op_sc = op_sc;
+	op->op_tp = tp;
+
+	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->form) {
+	switch (tp->kind & SPHO_TP_FORM_MASK) {
 	case SPHO_TP_FORM_TRUE:
 	case SPHO_TP_FORM_FALSE:
-	case SPHO_TP_FORM_NOM: 
+	case SPHO_TP_FORM_NAME: 
+	case SPHO_TP_FORM_VAR:
 		break;
 	case SPHO_TP_FORM_CONJ:
 	case SPHO_TP_FORM_DISJ:
@@ -237,8 +294,10 @@ spho_tp_destroy(struct spho_tp *tp)
 		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.bind.bound);
+		spho_tp_destroy(tp->d.memb.tp);
 		break;
 	case SPHO_TP_FORM_APPL:
 		STAILQ_FOREACH(arg, tp->d.appl.args, entries) {