starting subt implementation

CMakeLists.txt

@@ -27,6 +27,7 @@ set(SPHO_HEADER
 	${SPHO_HEADER_DIR}/err.h
 	${SPHO_HEADER_DIR}/scope.h
 	${SPHO_HEADER_DIR}/spho.h
+	${SPHO_HEADER_DIR}/subt.h
 	${SPHO_HEADER_DIR}/tp.h
 )
 
@@ -34,6 +35,7 @@ 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
 )
 

docs/about/formalities.md

@@ -24,29 +24,36 @@ 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]
@@ -54,24 +61,24 @@ s | t, γ ⊢ δ
 
 // XXX
 // remove s => t? always make progress
+// trace pairs: none
 s => t, s, t, γ ⊢ δ
 ---- [impl-left]
 s => t, s, γ ⊢ δ
 
-// discussion about implication below
-// check how "normal sequent calculus handles this"
+// 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, δ
@@ -82,6 +89,7 @@ box t, γ ⊢ δ
 // 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..], δ
@@ -92,6 +100,7 @@ a[t..], γ ⊢ δ
 
 
 // member types are filtered according to member name
+// trace pairs: premise[0] -- conclusion
 γ >> m ⊢ δ >> m
 ---- [member]
 γ ⊢ δ
@@ -99,11 +108,14 @@ a[t..], γ ⊢ δ
 
 // 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 }, δ*
@@ -113,7 +125,6 @@ c, γ*  ⊢ a_1, ..., a_n
 a_1 -> b_1, ..., a_n -> b_n, γ ⊢ c -> d, δ
 ```
 
-
 ### context operators
 
 * box filtering
@@ -136,6 +147,14 @@ a_1 -> b_1, ..., a_n -> b_n, γ ⊢ c -> d, δ
                  γ [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

include/spho/bind.h

@@ -31,11 +31,6 @@ struct spho_prebind {
 	struct spho_prebind_pair	*binds;
 };
 
-struct spho_bind {
-	struct spho_prebind	*local;
-	struct spho_bind	*parent;
-};
-
 struct spho_prebind	*spho_prebind_create(struct spho_scope *);
 
 int spho_prebind_undef(struct spho_prebind *, const struct spho_nom *);
@@ -48,6 +43,12 @@ int spho_prebind_member_tp(struct spho_prebind *, const struct spho_nom *,
 
 struct spho_prebind *spho_prebind_dupl(const struct spho_prebind *);
 
-void spho_prebind_destroy(struct spho_prebind *);
+void spho_prebind_free(struct spho_prebind *);
+
+
+struct spho_bind {
+	struct spho_prebind	*loc;
+	struct spho_bind	*parent;
+};
 
 #endif

include/spho/scope.h

@@ -122,7 +122,7 @@ struct spho_scope {
 	struct spho_nom_l	noms;
 	struct spho_tp_alloc_l	tps;
 
-	struct spho_prebind	*bind;
+	struct spho_prebind	*bind_loc;
 
 	SLIST_ENTRY(spho_scope)	next;
 };

include/spho/subt.h

@@ -0,0 +1,6 @@
+#ifndef _SPHO_SUBT_H
+#define _SPHO_SUBT_H
+
+#include "spho/bind.h"
+
+#endif /* ifndef _SPHO_SUBT_H */

src/msph/sphophi.c

@@ -419,7 +419,7 @@ msph_tree_sphophi_tp_prebind(struct spho_scope *sc,
 		if (HAS_PARAMS(tpdef)) {
 			SPHO_ASSERT(HAS_SCOPE(tpdef));
 			SPHO_ASSERT(SCOPE(tpdef) != NULL);
-			SPHO_ASSERT(SCOPE(tpdef)->bind != NULL);
+			SPHO_ASSERT(SCOPE(tpdef)->bind_loc != NULL);
 
 			STAILQ_FOREACH(name, &tpdef->params, entries) {
 				if (spho_scope_prebind_undef(SCOPE(tpdef),

src/spho/bind.c

@@ -158,7 +158,7 @@ spho_prebind_dupl(const struct spho_prebind *bind)
 }
 
 void
-spho_prebind_destroy(struct spho_prebind *bind)
+spho_prebind_free(struct spho_prebind *bind)
 {
 	free(bind->binds);
 	free(bind);

src/spho/scope.c

@@ -28,7 +28,7 @@ spho_scope_init(struct spho_scope *sc, struct spho_ctx *ctx,
 
 	TAILQ_INIT(&sc->tps);
 
-	sc->bind = NULL;
+	sc->bind_loc = NULL;
 
 	return (0);
 }
@@ -42,9 +42,9 @@ spho_scope_term(struct spho_scope *sc)
 
 	sc->parent = NULL;
 
-	if (sc->bind == NULL)
-		spho_prebind_destroy(sc->bind);
-	sc->bind = NULL;
+	if (sc->bind_loc == NULL)
+		spho_prebind_free(sc->bind_loc);
+	sc->bind_loc = NULL;
 }
 
 struct spho_scope *
@@ -177,7 +177,7 @@ 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 = spho_prebind_create(sc)) 
+	if ((sc->bind_loc = spho_prebind_create(sc)) 
 	    == NULL) {
 		return (-1);
 	}
@@ -194,7 +194,7 @@ spho_scope_prebind_tp(struct spho_scope *sc, struct spho_nom *nom,
 		return (-1);
 	}
 
-	return (spho_prebind_tp(sc->bind, nom, tp));
+	return (spho_prebind_tp(sc->bind_loc, nom, tp));
 }
 
 int
@@ -206,7 +206,7 @@ spho_scope_prebind_tp_op(struct spho_scope *sc, struct spho_nom *nom,
 		return (-1);
 	}
 
-	return (spho_prebind_tp_op(sc->bind, nom, tp_op));
+	return (spho_prebind_tp_op(sc->bind_loc, nom, tp_op));
 }
 
 int
@@ -217,7 +217,7 @@ spho_scope_prebind_undef(struct spho_scope *sc, struct spho_nom *nom)
 		return (-1);
 	}
 
-	return (spho_prebind_undef(sc->bind, nom));
+	return (spho_prebind_undef(sc->bind_loc, nom));
 }
 
 static int

src/spho/subt.c

@@ -0,0 +1,205 @@
+/*
+ * Subtyping
+ */
+#include <stdlib.h>
+
+#include "spho/bind.h"
+#include "spho/bind.h"
+#include "spho/spho.h"
+
+#include "spho/subt.h"
+
+struct bound_tp {
+	struct spho_bind		*bind;
+	const struct spho_tp		*tp;
+};
+
+struct seqnt {
+	struct spho_ctx		*ctx;
+
+	size_t			sz;
+	size_t			filled;
+	struct bound_tp		*elms;
+};
+
+struct seqnt_tstl {
+	struct seqnt		left;
+	struct seqnt		right;
+};
+
+
+static struct bound_tp *spho_bound_tp(const struct spho_tp *);
+
+
+/* read scopes and create bound type */
+struct bound_tp *
+spho_bound_tp(const struct spho_tp *tp)
+{
+	struct spho_scope	*sc;
+	struct spho_bind	*bind, *more_bind;
+
+	struct bound_tp	*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 struct seqnt *
+seqnt_alloc(struct spho_ctx *ctx, size_t initsz)
+{
+	struct seqnt *seq;
+	if (initsz == 0)
+		initsz = 32; /* just feels good */
+
+	if ((seq = calloc(1, sizeof(*seq))) == NULL) {
+		SPHO_ERR(ctx, SPHO_ERR_SYS);
+		return (NULL);
+	}
+	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 (seq);
+err:
+	if (seq != NULL) {
+		if (seq->elms != NULL)
+			free(seq->elms);
+		free(seq);
+	}
+
+	return (NULL);
+}
+
+static int
+seqnt_makebig(struct seqnt *seq)
+{
+	size_t		new_sz;
+	struct bound_tp *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
+seqnt_insert_from_ptr(struct seqnt *seq, struct bound_tp *elm)
+{
+	SPHO_PRECOND(seq->filled <= seq->sz);
+
+	if (seq->filled >= seq->sz && (seqnt_makebig(seq) == -1))
+		return (-1);
+
+	seq->elms[seq->filled++] = *elm;
+
+	SPHO_POSTCOND(seq->filled <= seq->sz);
+
+	return (0);
+}
+
+static int
+seqnt_insert_bind_tp(struct seqnt *seq, struct spho_bind *elm_bind,
+    struct spho_tp *elm_tp)
+{
+	SPHO_PRECOND(seq->filled <= seq->sz);
+
+	if (seq->filled >= seq->sz && (seqnt_makebig(seq) == -1))
+		return (-1);
+
+	seq->elms[seq->filled++] = (struct bound_tp){ elm_bind, elm_tp };
+
+	SPHO_POSTCOND(seq->filled <= seq->sz);
+
+	return (0);
+}
+
+
+int
+spho_is_subt(struct spho_tp *tp_left, struct spho_tp *tp_right)
+{
+	struct bound_tp *left, *right;
+
+	if ((left = spho_bound_tp(tp_left)) == NULL)
+		return (-1);
+	if ((right = spho_bound_tp(tp_right)) == NULL)
+		return (-1);
+
+	// TODO check well-definedness (e.g. no undefs)
+
+	// XXX skip boxing step
+	
+	// TODO create seqnt and seqnt_tstl
+	// TODO run decider
+
+	return (-1);
+}
+