From 995429c09c4e6c05158e66c2b23547353b7ebc5c Mon Sep 17 00:00:00 2001
From: admin <admin@vouivredigital.com>
Date: Thu, 13 Jun 2024 11:24:31 +0900
Subject: [PATCH] Implement a dependent type system

---
 vouivre/misc.scm   |    9 +
 vouivre/rules.scm  |  960 ++++++++++++++++++++++++-------
 vouivre/system.scm | 1365 +++++++++++++++++++++++++++++---------------
 3 files changed, 1645 insertions(+), 689 deletions(-)

diff --git a/vouivre/misc.scm b/vouivre/misc.scm
index 7f51bfa..c4c758d 100644
--- a/vouivre/misc.scm
+++ b/vouivre/misc.scm
@@ -23,6 +23,7 @@
   (alist<-plist
    array-map
    array-map-indexed
+   but-last
    flip
    for-indices-in-range
    if-let
@@ -32,6 +33,14 @@
    produce-array
    produce-typed-array))
 
+(define (but-last lst)
+  (if (null? lst)
+      (error "List must contain at least one element.")
+      (if (null? (cdr lst))
+	  '()
+	  (cons (car lst)
+		(but-last (cdr lst))))))
+
 (define (alist<-plist plist)
   "Convert a property list to an association list."
   (cdr
diff --git a/vouivre/rules.scm b/vouivre/rules.scm
index 5a784f3..f775379 100644
--- a/vouivre/rules.scm
+++ b/vouivre/rules.scm
@@ -20,201 +20,94 @@
 
 ;;;; Structural Rules
 
-(define-rule formation-1 ()
-  ((Γ ⊢ (type A))
-   (Γ (: x A) ⊢ (type (B x)))))
-
-(define-rule formation-2 ()
-  ((Γ ⊢ (type A))
-   (Γ ⊢ (≐ A B))))
-
-(define-rule formation-3 ()
-  ((Γ ⊢ (type B))
-   (Γ ⊢ (≐ A B))))
-
-(define-rule formation-4 ()
-  ((Γ ⊢ (type A))
-   (Γ ⊢ (: a A))))
-
-(define-rule formation-5 ()
-  ((Γ ⊢ (: a A))
-   (Γ ⊢ (≐ a b A))))
-
-(define-rule formation-6 ()
-  ((Γ ⊢ (: b A))
-   (Γ ⊢ (≐ a b A))))
-
-(define-rule type-reflexive ()
-  ((Γ ⊢ (≐ A A))
-   (Γ ⊢ (type A))))
-
-(define-rule type-symmetric ()
-  ((Γ ⊢ (≐ B A))
-   (Γ ⊢ (≐ A B))))
-
-(define-rule type-transitive ()
-  ((Γ ⊢ (≐ A C))
-   (Γ ⊢ (≐ A B))
-   (Γ ⊢ (≐ B C))))
-
-(define-rule :-reflexive ()
-  ((Γ ⊢ (≐ a a A))
-   (Γ ⊢ (: a A))))
-
-(define-rule :-symmetric ()
-  ((Γ ⊢ (≐ b a A))
-   (Γ ⊢ (≐ a b A))))
-
-(define-rule :-transitive ()
-  ((Γ ⊢ (≐ a c A))
-   (Γ ⊢ (≐ a b A))
-   (Γ ⊢ (≐ b c A))))
-
-(define-rule variable-conversion ()
-  ((Γ (: x A') Δ ⊢ J)
-   (Γ ⊢ (≐ A A'))
-   (Γ (: x A) Δ ⊢ J)))
-
-(define-rule substitution ()
-  ((Γ (/ Δ a x) ⊢ (/ J a x))
-   (Γ ⊢ (: a A))
-   (Γ (: x A) Δ ⊢ J)))
-
-(define-rule substitution-type-congruence ()
-  ((Γ (/ Δ a x) ⊢ (≐ (/ B a x) (/ B a' x)))
-   (Γ ⊢ (≐ a a' A))
-   (Γ (: x A) Δ ⊢ (type B))))
-
-(define-rule substitution-:-congruence ()
-  ((Γ (/ Δ a x) ⊢ (≐ (/ b a x) (/ b a' x) (/ B a x)))
-   (Γ ⊢ (≐ a a' A))
-   (Γ (: x A) Δ ⊢ (: b B))))
-
-(define-rule weakening ()
-  ((Γ (: x A) Δ ⊢ J)
-   (Γ ⊢ (type A))
-   (Γ Δ ⊢ J)))
-
-(define-rule generic-element ()
-  ((Γ (: x A) ⊢ (: x A))
-   (Γ ⊢ (type A))))
-
-;;;; Ordinary Function Type
-
-(define-rule → ()
-  ((Γ ⊢ (type (→ A B)))
-   (Γ ⊢ (type A))
-   (Γ ⊢ (type B))))
-
-(define-rule →-eq ()
-  ((Γ ⊢ (≐ (→ A B)
-	   (→ A' B')))
-   (Γ ⊢ (≐ A A'))
-   (Γ ⊢ (≐ B B'))))
-
-(define-rule λ ()
-  ((Γ ⊢ (: (λ x (b x))
-	   (→ A B)))
-   (Γ ⊢ (type B))
-   (Γ (: x A) ⊢ (: (b x) B))))
-
-(define-rule λ-eq ()
-  ((Γ ⊢ (≐ (λ x (b x))
-	   (λ x (b' x))
-	   (→ A B)))
-   (Γ (: x A) ⊢ (≐ (b x) (b' x) B))))
-
-(define-rule ev ()
-  ((Γ (: x A) ⊢ (: (f x) B))
-   (Γ ⊢ (: f (→ A B)))))
-
-(define-rule ev-eq ()
-  ((Γ (: x A) ⊢ (≐ (f x) (f' x) B))
-   (Γ ⊢ (≐ f f' (→ A B)))))
-
-(define-rule β ()
-  ((Γ (: x A) ⊢ (≐ ((λ y (b y)) x)
-		   (b x)
-		   B))
-   (Γ ⊢ (type B))
-   (Γ (: x A) ⊢ (: (b x) B))))
-
-(define-rule η ()
-  ((Γ ⊢ (≐ (λ x (f x))
-	   f
-	   (→ A B)))
-   (Γ ⊢ (: f (→ A B)))))
-
-;;;; Boolean Type
-
-(define-rule bool-formation ()
-  ((⊢ (type Bool))))
-
-(define-rule bool-introduction-1 ()
-  ((⊢ (: true Bool))))
-
-(define-rule bool-introduction-2 ()
-  ((⊢ (: false Bool))))
-
-(define-rule bool-elimination ()
-  ((⊢ (: if (→ Bool (→ A (→ A A)))))
-   (⊢ (type A))))
-
-(define-rule bool-computation-1 ()
-  ((⊢ (≐ (((if true) x) y)
-	 x
-	 Bool))))
-
-(define-rule bool-computation-2 ()
-  ((⊢ (≐ (((if false) x) y)
-	 y
-	 Bool))))
-
-;;;; Ordinary Pair Type
-
-(define-rule pair-formation ()
-  ((⊢ (type (Pair A B)))
-   (⊢ (type A))
-   (⊢ (type B))))
-
-(define-rule pair-introduction ()
-  ((⊢ (: (pair a b) (Pair A B)))
-   (⊢ (: a A))
-   (⊢ (: b B))))
-
-(define-rule pair-elimination-1 ()
-  ((⊢ (: first (→ (Pair A B)
-		    A)))
-   (⊢ (type A))
-   (⊢ (type B))))
-
-(define-rule pair-elimination-2 ()
-  ((⊢ (: second (→ (Pair A B)
-		    B)))
-   (⊢ (type A))
-   (⊢ (type B))))
-
-(define-rule pair-computation-1 ()
-  ((⊢ (≐ (first (pair a b))
-	 a A))
-   (⊢ (: a A))
-   (⊢ (: b B))))
-
-(define-rule pair-computation-2 ()
-  ((⊢ (≐ (second (pair a b))
-	 b B))
-   (⊢ (: a A))
-   (⊢ (: b B))))
-
-;;;; Derivations
+(define-rule formation-1
+  (Γ ⊢ (type A))
+  (Γ (: x A) ⊢ (type (B x))))
+
+(define-rule formation-2
+  (Γ ⊢ (type A))
+  (Γ ⊢ (≐ A B)))
+
+(define-rule formation-3
+  (Γ ⊢ (type B))
+  (Γ ⊢ (≐ A B)))
+
+(define-rule formation-4
+  (Γ ⊢ (type A))
+  (Γ ⊢ (: a A)))
+
+(define-rule formation-5
+  (Γ ⊢ (: a A))
+  (Γ ⊢ (≐ a b A)))
+
+(define-rule formation-6
+  (Γ ⊢ (: b A))
+  (Γ ⊢ (≐ a b A)))
+
+(define-rule type-reflexive
+  (Γ ⊢ (≐ A A))
+  (Γ ⊢ (type A)))
+
+(define-rule type-symmetric
+  (Γ ⊢ (≐ B A))
+  (Γ ⊢ (≐ A B)))
+
+(define-rule type-transitive
+  (Γ ⊢ (≐ A C))
+  (Γ ⊢ (≐ A B))
+  (Γ ⊢ (≐ B C)))
+
+(define-rule element-reflexive
+  (Γ ⊢ (≐ a a A))
+  (Γ ⊢ (: a A)))
+
+(define-rule element-symmetric
+  (Γ ⊢ (≐ b a A))
+  (Γ ⊢ (≐ a b A)))
+
+(define-rule element-transitive
+  (Γ ⊢ (≐ a c A))
+  (Γ ⊢ (≐ a b A))
+  (Γ ⊢ (≐ b c A)))
+
+(define-rule variable-conversion
+  (Γ (: x A') Δ ⊢ J)
+  (Γ ⊢ (≐ A A'))
+  (Γ (: x A) Δ ⊢ J))
+
+(define-rule substitution
+  (Γ (/ Δ a x) ⊢ (/ J a x))
+  (Γ ⊢ (: a A))
+  (Γ (: x A) Δ ⊢ J))
+
+(define-rule substitution-type-congruence
+  (Γ (/ Δ a x) ⊢ (≐ (/ B a x) (/ B a' x)))
+  (Γ ⊢ (≐ a a' A))
+  (Γ (: x A) Δ ⊢ (type B)))
+
+(define-rule substitution-element-congruence
+  (Γ (/ Δ a x) ⊢ (≐ (/ b a x) (/ b a' x) (/ B a x)))
+  (Γ ⊢ (≐ a a' A))
+  (Γ (: x A) Δ ⊢ (: b B)))
+
+(define-rule weakening
+  (Γ (: x A) Δ ⊢ J)
+  (Γ ⊢ (type A))
+  (Γ Δ ⊢ J))
+
+(define-rule generic-element
+  (Γ (: x A) ⊢ (: x A))
+  (Γ ⊢ (type A)))
+
+;;;; Structural Derivations
 
 (define-derivation change-of-variables ((Γ (: x' A) Δ ⊢ J)
 					(Γ ⊢ (type A))
 					(Γ (: x A) Δ ⊢ J))
-  (substitution #:index 2 a x' x x A A)
-  (generic-element #:index 1)
+  (substitution #:start 1 a x' x x A A)
+  (generic-element)
   (exact)
-  (weakening #:index 1)
+  (weakening #:end 1)
   (exact)
   (exact))
 
@@ -222,22 +115,22 @@
 				(Γ ⊢ (type B))
 				(Γ ⊢ (type A))
 				(Γ (: x A) (: y B) Δ ⊢ J))
-  (substitution #:index 3 a y x y' A B)
-  (weakening #:index 2)
-  (weakening #:index 1)
+  (substitution #:start 2 a y x y' A B)
+  (weakening #:start 1)
+  (weakening)
   (exact)
   (exact)
-  (generic-element #:index 1)
+  (generic-element)
   (exact)
-  (weakening #:index 1)
+  (weakening #:end 1)
   (exact)
-  (substitution #:index 3 a y' x y A B)
-  (weakening #:index 1)
+  (substitution #:start 2 a y' x y A B)
+  (weakening #:end 1)
   (exact)
-  (generic-element #:index 1)
+  (generic-element)
   (exact)
-  (weakening #:index 2)
-  (weakening #:index 1)
+  (weakening #:start 1 #:end 2)
+  (weakening)
   (exact)
   (exact)
   (exact))
@@ -247,60 +140,683 @@
 				       (Γ ⊢ (≐ A A')))
   (substitution a a x a' A A)
   (exact)
-  (variable-conversion #:index 1 A A')
+  (variable-conversion A A')
   (type-symmetric)
   (exact)
-  (generic-element #:index 1)
+  (generic-element)
   (formation-3 A A)
   (exact))
 
 (define-derivation congruence ((Γ ⊢ (≐ a b A'))
 			       (Γ ⊢ (≐ a b A))
 			       (Γ ⊢ (≐ A A')))
-  (substitution-:-congruence #:index 1 a a a' b x x A A)
+  (substitution-element-congruence a a a' b x x A A)
+  (exact)
+  (variable-conversion A A')
+  (type-symmetric)
+  (exact)
+  (generic-element)
+  (formation-3 A A)
+  (exact))
+
+;;;; Dependent Function Type
+
+(define-rule Π
+  (Γ ⊢ (type (Π (: x A) (B x))))
+  (Γ (: x A) ⊢ (type (B x))))
+
+(define-rule Π-eq
+  (Γ ⊢ (≐ (Π (: x A) (B x))
+	  (Π (: x A') (B' x))))
+  (Γ ⊢ (≐ A A'))
+  (Γ (: x A) ⊢ (≐ (B x) (B' x))))
+
+(define-rule λ
+  (Γ ⊢ (: (λ x (b x))
+	  (Π (: x A) (B x))))
+  (Γ (: x A) ⊢ (: (b x) (B x))))
+
+(define-rule λ-eq
+  (Γ ⊢ (≐ (λ x (b x))
+	  (λ x (b' x))
+	  (Π (: x A) (B x))))
+  (Γ (: x A) ⊢ (≐ (b x)
+		  (b' x)
+		  (B x))))
+
+(define-rule evaluation
+  (Γ (: x A) ⊢ (: (f x) (B x)))
+  (Γ ⊢ (: f (Π (: x A) (B x)))))
+
+(define-rule evaluation-eq
+  (Γ (: x A) ⊢ (≐ (f x) (f' x) (B x)))
+  (Γ ⊢ (≐ f f' (Π (: x A) (B x)))))
+
+(define-rule β
+  (Γ (: x A) ⊢ (≐ ((λ y (b y)) x)
+		  (b x)
+		  (B x)))
+  (Γ (: x A) ⊢ (: (b x) (B x))))
+
+(define-rule η
+  (Γ ⊢ (≐ (λ x (f x))
+	  f
+	  (Π (: x A) (B x))))
+  (Γ ⊢ (: f (Π (: x A) (B x)))))
+
+;;;; Ordinary Function Type
+
+(define-derivation → ((Γ ⊢ (:= (→ A B) (type (Π (: x A) B))))
+		      (Γ ⊢ (type A))
+		      (Γ ⊢ (type B)))
+  (Π)
+  (weakening)
+  (exact)
+  (exact))
+
+(define-derivation →-eq ((Γ ⊢ (≐ (→ A B) (→ A' B')))
+			 (Γ ⊢ (≐ A A'))
+			 (Γ ⊢ (≐ B B')))
+  (type-transitive B (Π (: x A) B))
+  (definition)
+  (formation-2 B A')
+  (exact)
+  (formation-2 B B')
+  (exact)
+  (type-transitive B (Π (: x A') B'))
+  (Π-eq)
+  (exact)
+  (weakening)
+  (formation-2 B A')
+  (exact)
+  (exact)
+  (type-symmetric)
+  (definition)
+  (formation-3 A A)
+  (exact)
+  (formation-3 A B)
+  (exact))
+
+(define-derivation →-λ ((Γ ⊢ (: (λ x (b x)) (→ A B)))
+			(Γ (: x A) ⊢ (: (b x) B))
+			(Γ ⊢ (type A))
+			(Γ ⊢ (type B)))
+  (element-conversion A (Π (: x A) B))
+  (λ)
+  (exact)
+  (type-symmetric)
+  (definition)
+  (exact)
+  (exact))
+
+(define-derivation →-λ-eq ((Γ ⊢ (≐ (λ x (b x))
+				   (λ x (b' x))
+				   (→ A B)))
+			   (Γ (: x A) ⊢ (≐ (b x) (b' x) B))
+			   (Γ ⊢ (type A))
+			   (Γ ⊢ (type B)))
+  (congruence A (Π (: x A) B))
+  (λ-eq)
+  (exact)
+  (type-symmetric)
+  (definition)
+  (exact)
+  (exact))
+
+(define-derivation →-evaluation ((Γ (: x A) ⊢ (: (f x) B))
+				 (Γ ⊢ (: f (→ A B)))
+				 (Γ ⊢ (type A))
+				 (Γ ⊢ (type B)))
+  (evaluation f f)
+  (element-conversion A (→ A B))
+  (exact)
+  (definition)
+  (exact)
+  (exact))
+
+(define-derivation →-evaluation-eq ((Γ (: x A) ⊢ (≐ (f x) (f' x) B))
+				    (Γ ⊢ (≐ f f' (→ A B)))
+				    (Γ ⊢ (type A))
+				    (Γ ⊢ (type B)))
+  (evaluation-eq f f f' f')
+  (congruence A (→ A B))
+  (exact)
+  (definition)
+  (exact)
+  (exact))
+
+(define-derivation →-β ((Γ (: x A) ⊢ (≐ ((λ x (b x)) x)
+					(b x)
+					B))
+			(Γ (: x A) ⊢ (: (b x) B)))
+  (β)
+  (exact))
+
+(define-derivation →-η ((Γ ⊢ (≐ (λ x (f x)) f (→ A B)))
+			(Γ ⊢ (: f (→ A B)))
+			(Γ ⊢ (type A))
+			(Γ ⊢ (type B)))
+  (congruence A (Π (: x A) B))
+  (η)
+  (element-conversion A (→ A B))
+  (exact)
+  (definition)
+  (exact)
   (exact)
-  (variable-conversion #:index 1 A A')
   (type-symmetric)
+  (definition)
   (exact)
-  (generic-element #:index 1)
-  (formation-3)
   (exact))
 
+;;;; Identity Type
+
+(define-rule =-formation
+  (Γ (: x A) ⊢ (type (= a x)))
+  (Γ ⊢ (: a A)))
+
+(define-rule =-introduction
+  (Γ ⊢ (: refl (= a a)))
+  (Γ ⊢ (: a A)))
+
+(define-rule =-elimination
+  (Γ ⊢ (: ind-eq
+	    (→ (P a refl)
+	       (Π (: x A)
+		  (Π (: p (= a x))
+		     (P x p))))))
+  (Γ ⊢ (: a A))
+  (Γ (: x A) (: p (= a x)) ⊢ (type (P x p))))
+
+(define-rule =-computation
+  (Γ (: u (P a refl)) ⊢ (≐ (((ind-eq u) a) refl)
+			     u
+			     (P a refl)))
+  (Γ ⊢ (: a A))
+  (Γ (: x A) (: p (= a x)) ⊢ (type (P x p))))
+
+;;;; Dependent Pair Type
+
+(define-rule Σ-formation
+  (Γ ⊢ (type (Σ (: x A) (B x))))
+  (Γ (: x A) ⊢ (type (B x))))
+
+(define-rule Σ-eq
+  (Γ ⊢ (≐ (Σ (: x A) (B x))
+	  (Σ (: x A') (B' x))))
+  (Γ ⊢ (≐ A A'))
+  (Γ (: x A) ⊢ (≐ (B x) (B' x))))
+
+(define-rule Σ-introduction
+  (Γ ⊢ (: pair (Π (: x A)
+		  (→ (B x)
+		     (Σ (: y A)
+			(B y))))))
+  (Γ (: x A) ⊢ (type (B x))))
+
+(define-rule Σ-elimination
+  (Γ ⊢ (: ind-Σ (→ (Π (: x A)
+		      (Π (: y (B x))
+			 (P ((pair x) y))))
+		   (Π (: z (Σ (: x A)
+			      (B x)))
+		      (P z)))))
+  (Γ (: x A) ⊢ (type (B x)))
+  (Γ (: z (Σ (: x A) (B x))) ⊢ (type (P z))))
+
+(define-rule Σ-computation
+  (Γ (: x A) (: y (B x)) (: g (Π (: x A)
+				 (Π (: y (B x))
+				    (P ((pair x) y)))))
+     ⊢ (≐ ((ind-Σ g) ((pair x) y))
+	  ((g x) y)
+	  (P ((pair x) y))))
+  (Γ (: z (Σ (: x A) (B x))) ⊢ (type (P z))))
+
+;;;; Natural Numbers
+
+(define-rule ℕ-formation
+  (⊢ (type ℕ)))
+
+(define-rule ℕ-introduction-1
+  (⊢ (: 0 ℕ)))
+
+(define-rule ℕ-introduction-2
+  (⊢ (: succ (→ ℕ ℕ))))
+
+(define-rule ℕ-elimination
+  (Γ ⊢ (: (ind-ℕ p0 ps)
+	  (Π (: n ℕ)
+	     (P n))))
+  (Γ (: n ℕ) ⊢ (type (P n)))
+  (Γ ⊢ (: p0 (P 0)))
+  (Γ ⊢ (: ps (Π (: n ℕ)
+		(→ (P n)
+		   (P (succ n)))))))
+
+(define-rule ℕ-computation-1
+  (Γ ⊢ (≐ ((ind-ℕ p0 ps) 0)
+	  p0
+	  (P 0)))
+  (Γ (: n ℕ) ⊢ (type (P n)))
+  (Γ ⊢ (: p0 (P 0)))
+  (Γ ⊢ (: ps (Π (: n ℕ)
+		(→ (P n)
+		   (P (succ n)))))))
+
+(define-rule ℕ-computation-2
+  (Γ (: n ℕ) ⊢ (≐ ((ind-ℕ p0 ps) (succ n))
+		  (ps n ((ind-ℕ p0 ps) n))
+		  (P (succ n))))
+  (Γ (: n ℕ) ⊢ (type (P n)))
+  (Γ ⊢ (: p0 (P 0)))
+  (Γ ⊢ (: ps (Π (: n ℕ)
+		(→ (P n)
+		   (P (succ n)))))))
+
+;;;; Boolean Type
+
+(define-rule bool-formation
+  (⊢ (type Bool)))
+
+(define-rule bool-introduction-1
+  (⊢ (: false Bool)))
+
+(define-rule bool-introduction-2
+  (⊢ (: true Bool)))
+					
+(define-rule bool-elimination
+  (Γ ⊢ (: (ind-Bool p0 p1)
+	  (Π (: x Bool)
+	     (P x))))
+  (Γ (: x Bool) ⊢ (type (P x)))
+  (Γ ⊢ (: p0 (P false)))
+  (Γ ⊢ (: p1 (P true))))
+
+(define-rule bool-computation-1
+  (Γ ⊢ (≐ ((ind-Bool p0 p1) false)
+	  p0
+	  (P false)))
+  (Γ (: x Bool) ⊢ (type (P x)))
+  (Γ ⊢ (: p0 (P false)))
+  (Γ ⊢ (: p1 (P true))))
+
+(define-rule bool-computation-2
+  (Γ ⊢ (≐ ((ind-Bool p0 p1) true)
+	  p1
+	  (P true)))
+  (Γ (: x Bool) ⊢ (type (P x)))
+  (Γ ⊢ (: p0 (P false)))
+  (Γ ⊢ (: p1 (P true))))
+
+;;;; List Type
+
+(define-rule list-formation
+  (Γ ⊢ (type (List A)))
+  (Γ ⊢ (type A)))
+
+(define-rule list-introduction-1
+  (Γ ⊢ (: nil (List A)))
+  (Γ ⊢ (type A)))
+
+(define-rule list-introduction-2
+  (Γ ⊢ (: cons (→ A (→ (List A)
+		     (List A)))))
+  (Γ ⊢ (type A)))
+
+(define-rule list-elimination
+  (Γ ⊢ (: (ind-List p0 ps)
+	  (Π (: xs (List A))
+	     (P xs))))
+  (Γ ⊢ (type A))
+  (Γ (: xs (List A)) ⊢ (type (P xs)))
+  (Γ ⊢ (: p0 (P nil)))
+  (Γ ⊢ (: ps (Π (: x A)
+		(Π (: xs (List A))
+		   (→ (P xs)
+		      (P ((cons x) xs))))))))
+
+(define-rule list-computation-1
+  (Γ ⊢ (≐ ((ind-List p0 ps) nil)
+	  p0
+	  (P nil)))
+  (Γ ⊢ (type A))
+  (Γ (: xs (List A)) ⊢ (type (P xs)))
+  (Γ ⊢ (: p0 (P nil)))
+  (Γ ⊢ (: ps (Π (: x A)
+		(Π (: xs (List A))
+		   (→ (P xs)
+		      (P ((cons x) xs))))))))
+
+(define-rule list-computation-2
+  (Γ (: x A) (: xs (List A)) ⊢ (≐ ((ind-List p0 ps) ((cons x) xs))
+				  (((ps x) xs) ((ind-List p0 ps) xs))
+				  (P ((cons x) xs))))
+  (Γ ⊢ (type A))
+  (Γ (: xs (List A)) ⊢ (type (P xs)))
+  (Γ ⊢ (: p0 (P nil)))
+  (Γ ⊢ (: ps (Π (: x A)
+		(Π (: xs (List A))
+		   (→ (P xs)
+		      (P ((cons x) xs))))))))
+
+;;;; Vector Type
+
+(define-rule vector-formation
+  (Γ ⊢ (type (Vector A n)))
+  (Γ ⊢ (type A))
+  (Γ ⊢ (: n ℕ)))
+
+(define-rule vector-introduction-1
+  (Γ ⊢ (: #() (Vector A 0)))
+  (Γ ⊢ (type A)))
+
+(define-rule vector-introduction-2
+  (Γ ⊢ (: :: (Π (: n ℕ)
+		(→ A (→ (Vector A n)
+			(Vector A (succ n)))))))
+  (Γ ⊢ (type A)))
+
+(define-rule vector-elimination
+  (Γ ⊢ (: (ind-Vector p0 ps)
+	  (Π (: n ℕ)
+	     (Π (: xs (Vector A n))
+		(P xs)))))
+  (Γ ⊢ (type A))
+  (Γ (: n ℕ) (: xs (Vector A n)) ⊢ (type (P xs)))
+  (Γ ⊢ (: p0 (P #())))
+  (Γ ⊢ (: ps (Π (: n ℕ)
+		(Π (: x A)
+		   (Π (: xs (Vector A n))
+		      (→ (P xs)
+			 (P (((:: n) x) xs)))))))))
+
+(define-rule vector-computation-1
+  (Γ ⊢ (≐ ((ind-Vector p0 ps) #())
+	  p0
+	  (P #())))
+  (Γ ⊢ (type A))
+  (Γ (: n ℕ) (: xs (Vector A n)) ⊢ (type (P xs)))
+  (Γ ⊢ (: p0 (P #())))
+  (Γ ⊢ (: ps (Π (: n ℕ)
+		(Π (: x A)
+		   (Π (: xs (Vector A n))
+		      (→ (P xs)
+			 (P (((:: n) x) xs)))))))))
+
+(define-rule vector-computation-2
+  (Γ (: x A) (: n ℕ) (: xs (Vector A n)) ⊢ (≐ (((ind-Vector p0 ps) n) (((:: n) x) xs))
+					      ((((ps n) x) xs)
+					       (((ind-Vector p0 ps) n) xs))
+					      (P (((:: n) x) xs))))
+  (Γ ⊢ (type A))
+  (Γ (: n ℕ) (: xs (Vector A n)) ⊢ (type (P xs)))
+  (Γ ⊢ (: p0 (P #())))
+  (Γ ⊢ (: ps (Π (: n ℕ)
+		(Π (: x A)
+		   (Π (: xs (Vector A n))
+		      (→ (P xs)
+			 (P (((:: n) x) xs)))))))))
+
+;;;; More Derivations
+
 (define-derivation identity ((Γ ⊢ (: (λ x x) (→ A A)))
 			     (Γ ⊢ (type A)))
-  (λ)
+  (→-λ)
+  (generic-element)
+  (exact)
   (exact)
-  (generic-element #:index 1)
   (exact))
 
-(define-derivation not ((⊢ (: (λ x (((if x) false) true))
-			      (→ Bool Bool))))
+(define-derivation if ((Γ ⊢ (: (λ z (λ x (λ y ((ind-Bool y x) z))))
+			       (Π (: z Bool)
+				  (→ (P true)
+				     (→ (P false)
+					(P z))))))
+		       (Γ (: z Bool) ⊢ (type (P z))))
   (λ)
+  (→-λ #:start 1)
+  (→-λ #:start 2)
+  (interchange #:end 2)
   (bool-formation)
-  (substitution a true x y A Bool)
-  (weakening #:index 0)
+  (substitution A Bool a true x z)
+  (bool-introduction-2)
+  (exact)
+  (interchange #:start 1)
+  (weakening)
+  (substitution A Bool a true x z)
+  (bool-introduction-2)
+  (exact)
+  (bool-formation)
+  (weakening)
+  (substitution A Bool a true x z)
+  (bool-introduction-2)
+  (exact)
+  (substitution A Bool a false x z)
+  (bool-introduction-1)
+  (exact)
+  (evaluation #:start 2 f (ind-Bool y x))
+  (bool-elimination #:start 2 (P false) (P false) (P true) (P true))
+  (weakening #:end 1)
+  (substitution A Bool a true x z)
+  (bool-introduction-2)
+  (exact)
+  (weakening #:end 1)
+  (substitution A Bool a false x z)
+  (bool-introduction-1)
+  (exact)
+  (exact)
+  (weakening #:end 1)
+  (substitution A Bool a true x z)
+  (bool-introduction-2)
+  (exact)
+  (generic-element)
+  (substitution A Bool a false x z)
+  (bool-introduction-1)
+  (exact)
+  (weakening #:start 1)
+  (weakening)
+  (substitution A Bool a true x z)
+  (bool-introduction-2)
+  (exact)
+  (substitution A Bool a false x z)
+  (bool-introduction-1)
+  (exact)
+  (generic-element)
+  (substitution A Bool a true x z)
+  (bool-introduction-2)
+  (exact)
+  (weakening #:end 1)
   (bool-formation)
+  (weakening)
+  (substitution A Bool a true x z)
+  (bool-introduction-2)
+  (exact)
+  (substitution A Bool a false x z)
   (bool-introduction-1)
-  (ev #:index 1)
-  (substitution a false x y A Bool)
-  (weakening #:index 0)
+  (exact)
+  (weakening #:start 1)
+  (weakening)
+  (bool-formation)
+  (substitution #:start 1 A Bool a true x z)
+  (bool-introduction-2 #:start 1)
+  (exact)
+  (exact)
+  (weakening)
   (bool-formation)
+  (substitution A Bool a true x z)
   (bool-introduction-2)
-  (ev #:index 1)
-  (ev #:index 0)
-  (bool-elimination)
+  (exact)
+  (→ #:start 1)
+  (weakening)
+  (bool-formation)
+  (substitution A Bool a false x z)
+  (bool-introduction-1)
+  (exact)
+  (exact))
+
+(define-derivation not ((Γ ⊢ (: (ind-Bool true false)
+				(→ Bool Bool))))
+  (element-conversion A (Π (: x Bool) Bool))
+  (bool-elimination (P false) Bool (P true) Bool)
+  (weakening)
+  (bool-formation)
+  (bool-formation)
+  (bool-introduction-2)
+  (bool-introduction-1)
+  (type-symmetric)
+  (definition)
+  (bool-formation)
   (bool-formation))
 
 (define-derivation constant ((Γ (: y B) ⊢ (: (λ x y) (→ A B)))
 			     (Γ ⊢ (type A))
 			     (Γ ⊢ (type B)))
+  (→-λ #:start 1)
+  (weakening #:start 1)
+  (weakening)
+  (exact)
+  (exact)
+  (generic-element)
+  (exact)
+  (weakening)
+  (exact)
+  (exact)
+  (weakening)
+  (exact)
+  (exact))
+
+(define-derivation =-inverse ((Γ ⊢ (: (λ x (ind-eq refl))
+				      (Π (: x A)
+					 (Π (: y A)
+					    (→ (= x y)
+					       (= y x))))))
+			      (Γ ⊢ (type A))
+			      (Γ ⊢ (: x A)))
   (λ)
-  (weakening #:index 1)
+  (substitution #:start 1 a refl x u A (= x x))
+  (=-introduction #:start 1 A A)
+  (generic-element)
+  (exact)
+  (→-evaluation #:start 1 f ind-eq)
+  (element-conversion #:start 1 A (→ (= x x) (Π (: y A) (Π (: p (= x y)) (= y x)))))
+  (=-elimination #:start 1)
+  (generic-element)
+  (exact)
+  (weakening #:start 2)
+  (=-formation #:start 1)
+  (generic-element)
+  (exact)
+  (interchange)
+  (exact)
+  (exact)
+  (=-formation #:start 1)
+  (generic-element)
+  (exact)
+  (→-eq #:start 1)
+  (type-reflexive #:start 1)
+  (=-formation)
   (exact)
+  (Π-eq #:start 1)
+  (weakening)
   (exact)
-  (weakening #:index 2)
-  (weakening #:index 1)
+  (type-reflexive)
   (exact)
+  (type-symmetric #:start 2)
+  (definition #:start 2)
+  (=-formation #:start 1)
+  (generic-element)
   (exact)
-  (generic-element #:index 1)
+  (interchange)
+  (exact)
+  (exact)
+  (=-formation #:start 1)
+  (generic-element)
+  (exact)
+  (=-formation)
+  (exact)
+  (Π #:start 1)
+  (→ #:start 2)
+  (=-formation #:start 1)
+  (generic-element)
+  (exact)
+  (interchange)
+  (exact)
+  (exact)
+  (=-formation #:start 1)
+  (generic-element)
   (exact))
+
+(define-derivation add (((: m ℕ) ⊢ (: (ind-ℕ m ((λ n succ) m)) (→ ℕ ℕ))))
+  (element-conversion #:start 1 A (Π (: x ℕ) ℕ))
+  (ℕ-elimination #:start 1 (P 0) ℕ (P n) ℕ (P (succ n)) ℕ)
+  (weakening #:start 1)
+  (weakening)
+  (ℕ-formation)
+  (ℕ-formation)
+  (weakening)
+  (ℕ-formation)
+  (ℕ-formation)
+  (generic-element)
+  (ℕ-formation)
+  (element-conversion #:start 1 A (→ ℕ ℕ))
+  (→-evaluation f (λ n succ))
+  (→-λ)
+  (weakening)
+  (ℕ-formation)
+  (ℕ-introduction-2)
+  (ℕ-formation)
+  (→)
+  (ℕ-formation)
+  (ℕ-formation)
+  (ℕ-formation)
+  (→)
+  (ℕ-formation)
+  (ℕ-formation)
+  (definition #:start 1)
+  (weakening)
+  (ℕ-formation)
+  (ℕ-formation)
+  (weakening)
+  (ℕ-formation)
+  (ℕ-formation)
+  (weakening)
+  (ℕ-formation)
+  (type-symmetric)
+  (definition)
+  (ℕ-formation)
+  (ℕ-formation))
+
+(define-derivation add-2-length ((Γ ⊢ (:= add-2-length
+					  (: (λ x (λ xs succ))
+					     (Π (: x A)
+						(Π (: xs (List A))
+						   (→ ℕ ℕ))))))
+				 (Γ ⊢ (type A)))
+  (λ)
+  (λ #:start 1)
+  (weakening #:start 1)
+  (weakening)
+  (exact)
+  (list-formation)
+  (exact)
+  (weakening)
+  (exact)
+  (ℕ-introduction-2))
+
+(define-derivation length ((Γ ⊢ (: (λ xs ((ind-List 0 add-2-length) xs))
+				   (→ (List A) ℕ)))
+			   (Γ ⊢ (type A)))
+  (→-λ)
+  (evaluation f (ind-List 0 add-2-length))
+  (list-elimination (P nil) ℕ x x (P ((cons x) xs)) ℕ)
+  (exact)
+  (weakening)
+  (list-formation)
+  (exact)
+  (ℕ-formation)
+  (ℕ-introduction-1)
+  (add-2-length)
+  (exact)
+  (list-formation)
+  (exact)
+  (ℕ-formation))
diff --git a/vouivre/system.scm b/vouivre/system.scm
index 042570e..567ba2d 100644
--- a/vouivre/system.scm
+++ b/vouivre/system.scm
@@ -22,225 +22,432 @@
   #:use-module (srfi srfi-9)
   #:use-module (vouivre misc)
   #:export
-  (*rules*
+  (d
    apply-rule
-   apply-rules
-   conclusion
-   d
+   derivation?
+   derivation-tree
+   derivation-steps
    define-derivation
    define-rule
-   exact
-   list-hypotheses))
+   define-derivation-list
+   *rules*
+   *definition-rules*))
 
-(define *rules* (make-hash-table))
-(define reserved-symbols '(: ≐ ⊢ type /))
-
-(define-record-type derivation
-  (make-derivation tree points)
-  derivation?
-  (tree derivation-tree)
-  (points derivation-points derivation-points-set!))
-
-(define-record-type evaluation
-  (make-evaluation function value)
-  evaluation?
-  (function evaluation-function)
-  (value evaluation-value))
+;;;; miscellaneous routines
 
 (define (papply proc . args)
   (lambda (. rest)
     (apply proc (append args rest))))
 
-(define (all pred lst)
-  "Like `every', but return the list of all `pred' return values on success."
-  (call/cc
-   (lambda (break)
-     (reverse
-      (fold
-       (lambda (x prev)
-	 (if-let (y (pred x))
-		 (cons y prev)
-		 (break #f)))
-       '() lst)))))
-
-(define (unreserved-symbol? x)
-  (and (symbol? x)
-       (not (member x reserved-symbols))))
-
-(define (parse-unreserved-symbol expr)
-  (if (and (symbol? expr)
-	   (not (member expr reserved-symbols)))
-      expr
-      #f))
-
-(define (parse-type-variable expr)
-  (parse-unreserved-symbol expr))
-
-(define (parse-type expr)
-  (match expr
-    ((? parse-unreserved-symbol A)
-     expr)
-    (((? parse-unreserved-symbol B)
-      (? parse-type x)
-      ..1)
-     expr)
-    (_ #f)))
-
-(define (parse-type-variable-declaration expr)
-  (match expr
-    ((': (? parse-type-variable x)
-	 (? parse-type A))
-     (list ': x A))
-    (_ #f)))
-
-(define (parse-context expr)
-  (match expr
-    (((? parse-type-variable-declaration X) ...)
-     expr)
-    (((? parse-unreserved-symbol Γ)
-      (? parse-type-variable-declaration X)
-      ...
-      (? parse-unreserved-symbol Δ))
-     expr)
-    (((? parse-unreserved-symbol Γ)
-      (? parse-type-variable-declaration X)
-      ...
-      ('/ (? parse-unreserved-symbol Δ)
-	  (? unreserved-symbol? x)
-	  (? unreserved-symbol? y)))
-     expr)
-    (((? parse-unreserved-symbol Γ)
-      (? parse-type-variable-declaration X)
-      ...)
-     expr)
-    (_ #f)))
-
-(define (parse-element expr)
-  (match expr
-    ((? parse-unreserved-symbol a)
-     expr)
-    (((? parse-unreserved-symbol b)
-      (? parse-element x)
-      ...)
-     expr)
-    (((? parse-element b)
-      (? parse-type-variable x))
-     expr)
-    (_ #f)))
-
-(define (parse-judgment expr)
-  (match expr
-    ((context ... '⊢ J)
-     (and (parse-context context)
-	  (match J
-	    ;; generic judgment thesis
-	    ((? unreserved-symbol? J)
-	     expr)
-	    (('/ (? unreserved-symbol? J)
-		 (? unreserved-symbol? a)
-		 (? unreserved-symbol? x))
-	     expr)
-	    ;; type
-	    (('type (? parse-type A))
-	     expr)
-	    ;; judgmentally equal types
-	    (('≐ ('/ (? parse-type A)
-		     (? unreserved-symbol? x)
-		     (? unreserved-symbol? y))
-		 ('/ (? parse-type B)
-		     (? unreserved-symbol? x')
-		     (? unreserved-symbol? y)))
-	     expr)
-	    (('≐ (? parse-type A)
-		 (? parse-type B))
-	     expr)
-	    ;; judgmentally equal elements of a type
-	    (('≐ ('/ (? parse-element a)
-		     (? unreserved-symbol? x)
-		     (? unreserved-symbol? y))
-		 ('/ (? parse-element b)
-		     (? unreserved-symbol? x')
-		     (? unreserved-symbol? y))
-		 ('/ (? parse-type A)
-		     (? unreserved-symbol? x)
-		     (? unreserved-symbol? y)))
-	     expr)
-	    (('≐ (? parse-element a)
-		 (? parse-element b)
-		 (? parse-type A))
-	     expr)
-	    ;; element of a type
-	    ((': (? parse-element a)
-		 (? parse-type A))
-	     expr)
-	    ;;
-	    (_ #f))))
-    (_ #f)))
-
-(define (parse literals judgments)
-  "Parse literals and judgments of a rule returning them as a cons cell on
-success and `#f' on failure."
-  (and (list? literals)
-       (every symbol? literals)
-       (match judgments
-	 ((C Hs ...)
-	  (and=> (all parse-judgment judgments)
-		 (papply cons literals)))
-	 (_ #f))))
-
-(defmacro define-rule (name literals judgments)
-  (let ((x (parse literals judgments)))
-    (ifn x
-	 (error "SYNTAX ERROR")
-	 (begin
-	   (hash-set! *rules* name `,x)
-	   `(hash-set! *rules* ',name ',x)))))
-
-(define* (apply-rule derivation name #:key index . args)
-  (if (eq? name 'exact)
-      (exact derivation)
-      (if-let (rule (hash-ref *rules* name))
-	      (match-let (((literals . (C Hs ...)) rule))
-		(let* ((ps (derivation-points derivation))
-		       (p (car ps))
-		       (expr (car p)))
-		  (and=>
-		   (match-judgment
-		    expr C
-		    ;; When `#:index' is provided the evaluator adds it to
-		    ;; the head of the `args' list (see the documentation
-		    ;; `define*') followed by its value, and they must be
-		    ;; removed.
-		    (alist<-plist (ifn index args (cddr args)))
-		    index)
-		   (lambda (bindings)
-		     (and=>
-		      (call/cc
-		       (lambda (break)
-			 ;; Each hypothesis, with bindings replaced, is wrapped
-			 ;; in a cons cell, to be added to the derivation
-			 ;; points.
-			 (map (lambda (hypothesis)
-				(list (or (replace-in-judgment hypothesis bindings)
-					  (break #f))))
-			      Hs)))
-		      (lambda (points)
-			(set-cdr! p points)
-			;; Remove the current point, adding its leaves as new
-			;; points.
-			(derivation-points-set! derivation (append points
-								   (cdr ps)))
-			derivation))))))
-	      (error "Rule undefined."))))
-
-(define (apply-rules derivation rules)
+(define-syntax-rule (second-value expr)
+  (receive (x y . rest)
+      expr y))
+
+(define (unzip lst)
+  (map reverse
+   (let rec ((lst lst)
+	     (acc (map (const '())
+		       (car lst))))
+     (if (null? lst)
+	 acc
+	 (rec (cdr lst)
+	      (map cons (car lst) acc))))))
+
+;;;; data
+
+(define *constructors* (make-hash-table))
+(define *rules* (make-hash-table))
+(define *definition-rules* (make-hash-table))
+(define *types* (make-hash-table))
+(define *ctxs* (make-parameter #f))
+
+(define-record-type derivation
+  (make-derivation tree steps)
+  derivation?
+  (tree derivation-tree)
+  (steps derivation-steps))
+
+(define-record-type substitution
+  (make-substitution pattern source destination)
+  substitution?
+  (pattern substitution-pattern)
+  (source substitution-source)
+  (destination substitution-destination))
+
+(define element-of-:xX second)
+(define judgment-context (papply take-while (compose not (papply eq? '⊢))))
+(define judgment-content last)
+(define meta-conclusion car)
+(define meta-hypotheses cdr)
+(define constructor-ref (papply hash-ref *constructors*))
+(define (context-ref ctx var)
+  (find (lambda (:xX)
+	  (eq? var (element-of-:xX :xX)))
+	ctx))
+(define rule-ref (papply hash-ref *rules*))
+(define type-ref (papply hash-ref *types*))
+
+;; NOTE: The requirement that for declared types and constructors we can list
+;;       the kind of its arguments, if any, imposes additional constraints that
+;;       must be checked in `define-rule'. Incidentally, we can dispense with
+;;       some checks here because we know that interned metas satisfy these
+;;       constraints.
+(define (meta-arguments-kinds meta)
+  (let ((content (judgment-content (meta-conclusion meta))))
+    (ifn (list? content)
+	 (parse-error
+	  "meta-arguments-kinds: requires a type kind of judgment.")
+	 (case (first content)
+	   ((type)
+	    (case (car (second content))
+	      ((→)
+	       '(type type))
+	      ((Π)
+	       '(binding type))
+	      ((=)
+	       '(element element))
+	      ((Σ)
+	       '(binding type))
+	      ((List)
+	       '(type))
+	      ((Vector)
+	       '(type element))
+	      (else (parse-error "unsupported type."))))
+	   (else
+	    (parse-error
+	     "meta-arguments-kinds: requires a type kind of judgment."))))))
+
+(define (d judgment)
+  (make-derivation (cons judgment #f) '()))
+
+(define (derivation-point derivation)
   (call/cc
    (lambda (break)
-     (fold (lambda (rule prev)
-	     (if-let (x (apply apply-rule prev (car rule) (cdr rule)))
-		     x
-		     (break #f)))
-	   derivation rules))))
+     (let rec ((tree (derivation-tree derivation)))
+       (ifn (cdr tree)
+	    (break (car tree))
+	    (ifn (list? (cdr tree))
+		 #f
+		 (fold (lambda (x _)
+			 (rec x))
+		       #f (cdr tree))))))))
+
+(define (expand-derivation-point derivation step stuff)
+  (match-let (((expanded? . tree)
+	       (let rec ((tree (derivation-tree derivation)))
+		 (ifn (cdr tree)
+		      (cons #t (cons (car tree) stuff))
+		      (ifn (list? (cdr tree))
+			   (cons #f tree)
+			   (match-let (((expanded? . rlst)
+					(fold (lambda (x prev)
+						(if (car prev)
+						    (cons #t (cons x (cdr prev)))
+						    (let ((r (rec x)))
+						      (cons (car r)
+							    (cons (cdr r) (cdr prev))))))
+					      '(#f . ())
+					      (cdr tree))))
+			     (cons expanded? (cons (car tree) (reverse rlst)))))))))
+    (values (make-derivation tree (cons step (derivation-steps derivation)))
+	    expanded?)))
+
+(define (list-hypotheses derivation)
+  (delete-duplicates
+   (let rec ((tree (derivation-tree derivation))
+	     (lst '()))
+     (if (or (not (cdr tree))
+	     (not (list? (cdr tree))))
+	 (cons (car tree) lst)
+	 (fold rec lst (cdr tree))))
+   equal?)) 
+
+;;;; parsing routines
+
+;;; In what follows, we want to do for judgments what `map' and `fold' do for
+;;; lists – to evaluate a function on the judgment's intrinsics. We proceed by
+;;; implementing map/fold routines in a "Russian doll" kind of way from big to
+;;; small (although they appear in this file in reverse order i.e from callee to
+;;; caller): judgment, content and context, type, and element. For each of these
+;;; we have a "dispatch" routine to abstract away the structural analysis and
+;;; validation that is common to the corresponding map and fold. Follows, a
+;;; simple application of `judgment-map'. The others work in a similar fashion.
+;;;
+;;; (define (prime x) (string->symbol (string-append (symbol->string x) "'")))
+;;;
+;;; (judgment-map (lambda (kind x y)
+;;;     	(case kind
+;;; 		  ((type)
+;;; 		   (prime y))
+;;; 		  (else x)))
+;;; 	      #f
+;;; 	      '(Λ ⊢ (type A))
+;;; 	      '(Ξ ⊢ (type B)))
+;;; => (Λ ⊢ (type B'))
+;;;
+;;; As you can see, there are two differences with `map'. The first is `kind',
+;;; which binds to the kind of intrinsics currently being mapped (either
+;;; 'element, 'type, 'Γ, or 'Δ). The second is the range, `#f' here, which
+;;; allows the split of variable declarations between Γs and Δs.
+
+(define (parse-error str . format-args)
+  (error (string-append "parsing error: "
+			(apply format #f str format-args))))
+
+(define just cdr)
+
+(define (pre-destruct kind expr)
+  (define fmt "destruct: unknown expression ~a of kind ~a.")
+  ;; Since the name can be any expression including `#f' we wrap it as a
+  ;; "Maybe" so that we can distinguish the absence of a name from the name
+  ;; `#f'.
+  (ifn (list? expr)
+       (values (cons 'just expr) '())
+       (if (or (null? expr)
+	       (null? (cdr expr)))
+	   (parse-error fmt expr kind)
+	   (if (list? (car expr))
+	       (if (eq? kind 'type)
+		   (parse-error fmt expr kind)
+		   ;; When instead of a name we have an s-expression the
+		   ;; expression must have a size of exactly two.
+		   (ifn (null? (cddr expr))
+			(parse-error fmt expr kind)
+			(values #f (cdr expr))))
+	       (values (cons 'just (car expr))
+		       (cdr expr))))))
+
+(define (destruct kind expr)
+  "Destructure an element or type into its head, tail, and meta data, raising an
+   error if the expression has an unexpected format.
+
+   kind: The kind of expression to destructure. This is either 'type or
+         'element.
+
+   expr: The expression to destructure.
+
+   Returns Maybe name, List arguments, and either `#f' or the name's meta data,
+   as multiple values."
+  (define referee (if (eq? kind 'element) constructor-ref type-ref))
+  (define fmt "destruct: unknown expression ~a of kind ~a.")
+  (receive (maybe-name args) (pre-destruct kind expr)
+    (ifn maybe-name
+	 (values maybe-name args #f)
+	 (if-let (meta (referee (just maybe-name)))
+		 (let ((n-args (length args))
+		       (n-meta-args (length (second-value
+					     (pre-destruct
+					      kind
+					      (element-of-:xX
+					       (judgment-content
+						(meta-conclusion meta))))))))
+		   (if (= n-args n-meta-args)
+		       (values maybe-name args meta)
+		       ;; We allow constructors declared with no arguments to be
+		       ;; curried applications.
+		       (if (and (eq? kind 'element)
+				(= 1 n-args)
+				(zero? n-meta-args))
+			   (values maybe-name args meta)
+			   (parse-error "destruct: declared expression ~a has ~a arguments, but expected ~a." expr n-args n-meta-args))))
+		 (values maybe-name args #f)))))
+
+(define (element-dispatch function exprs)
+  "Dispatch a function based on the given elements or raise an error if they
+   have an unexpcted format. There are three kinds of expressions: declared
+   constructors, undeclared constructors, and curried application to an
+   argument.
+
+   function: A function of one argument called with 'declared, 'undeclared, or
+             'applied if, respectively, expressions are: all declared, any are
+             undeclared, or all are applied.
+
+   exprs: List of expressions.
+
+   Returns the result of the function application."
+  (define element-destruct (papply destruct 'element))
+  (receive (maybe-names argss metas)
+      (unzip3 (map (lambda (expr) (receive vals (element-destruct expr) vals))
+		   exprs))
+    ;; All declared constructors must have the same meta data and their number
+    ;; of arguments must match.
+    (unless (apply eq? (remove not metas))
+      (parse-error "element-dispatch: declared constructors don't match."))
+    (if (every (lambda (maybe-name args meta)
+		 (or (not maybe-name)
+		     (and meta
+			  (= 1 (length args))
+			  (zero? (length (second-value
+					  (pre-destruct
+					   'element
+					   (element-of-:xX
+					    (judgment-content
+					     (meta-conclusion meta))))))))))
+	       maybe-names argss metas)
+	(function 'applied maybe-names argss metas)
+	(if (every identity metas)
+	    (function 'declared maybe-names argss metas)
+	    (function 'undeclared maybe-names argss metas)))))
+
+(define (element-map function expr . more)
+  "Map a function on the given elements or raise an error if they have unexpected
+   format.
+
+   function: A function that will always be called with 'element as its first
+             argument, to be consistant with `type-map', and then with the
+             corresponding intrinsics of each expression.
+
+   expr . more: One or more expressions.
+
+   Returns an element that is the result of mapping the function to the
+   corresponding intrinsics."
+  (let ((exprs (cons expr more)))
+    (element-dispatch
+     (lambda (kind maybe-names argss metas)
+       (case kind
+	 ((declared)
+	  (if (null? (car argss))
+	      (apply function 'element exprs)
+	      (cons (just (car maybe-names)) ; all expressions have the same name
+		    (apply map
+			   (lambda formals
+			     (apply element-map function formals))
+			   argss))))
+	 ((undeclared)
+	  (apply function 'element exprs))
+	 ((applied)
+	  ;; Each expression is of the form '(f x).
+	  (list (apply element-map function (map first exprs))
+		(apply element-map function (map second exprs))))))
+     exprs)))
+
+(define (element-fold function init expr . more)
+  "Fold a function over the given elements or raise an error if they have
+   unexpected format.
+
+   function: A function that will always be called with 'element as its first
+             argument, to be consistant with `type-fold', and then with the
+             corresponding intrinsics of each expression, followed by the
+             latest accumulator.
+
+   expr . more: One or more expressions.
+
+   Returns an element that is the result of folding the function over the
+   corresponding intrinsics."
+  (let ((exprs (cons expr more)))
+    (element-dispatch
+     (lambda (kind maybe-names argss metas)
+       (case kind
+	 ((declared)
+	  (if (null? (car argss))
+	      (apply function 'element `(,@exprs ,init))
+	      (apply fold
+		     (lambda formals
+		       (apply element-fold function
+			      (last formals)
+			      (but-last formals)))
+		     init argss)))
+	 ((undeclared)
+	  (apply function 'element `(,@exprs ,init)))
+	 ((applied)
+	  (apply element-fold function
+		 (apply element-fold function init
+			(map first exprs))
+		 (map second exprs)))))
+     exprs)))
+
+(define (type-dispatch function exprs)
+  "Dispatch a function based on the given types or raise an error if they
+   have an unexpcted format. There are two kinds of expressions: declared
+   types, and undeclared types.
+
+   function: A function of one argument called with 'declared or 'undeclared if,
+             respectively, expressions are: all declared, or any are undeclared.
+
+   exprs: List of expressions.
+
+   Returns the result of the function application."
+  (define type-destruct (papply destruct 'type))
+  (receive (maybe-names argss metas)
+      (unzip3 (map (lambda (expr) (receive vals (type-destruct expr) vals)) exprs))
+    ;; All declared types must have the same meta data and their number
+    ;; of arguments must match.
+    (unless (apply eq? (remove not metas))
+      (parse-error "type-dispatch: declared types don't match."))
+    (if (every identity metas)
+	(function 'declared maybe-names argss metas)
+	(function 'undeclared maybe-names argss metas))))
+
+(define (type-map function expr . more)
+  "Map a function to type-expressions. See the documentation of `element-map' which
+   has analogous behaviour except for the function who's called on a kind that
+   alternates between 'type and 'element based on the intrinsic."
+  (let ((exprs (cons expr more)))
+    (type-dispatch
+     (lambda (kind maybe-names argss metas)
+       (case kind
+	 ((declared)
+	  (if (null? (car argss))
+	      (apply function 'type exprs)
+	      (cons (just (car maybe-names)) ; all expressions have the same name
+		    (apply map
+			   (lambda formals
+			     (if (eq? 'binding (car formals))
+				 (match (cdr formals)
+				   (((': xs Xs) ...)
+				    (list ':
+					  (apply element-map function xs)
+					  (apply type-map function Xs)))
+				   (_
+				    (parse-error "type-map: declared types don't match.")))
+				 (apply (case (car formals)
+					  ((element)
+					   element-map)
+					  ((type)
+					   type-map))
+					function (cdr formals))))
+			   (cons (meta-arguments-kinds (type-ref (car expr)))
+				 argss)))))
+	 ((undeclared)
+	  (apply function 'type exprs))))
+     exprs)))
+
+(define (type-fold function init expr . more)
+  "Fold a function over type-expressions. See the documentation of `element-fold'
+   which has analogous behaviour except for the function who's called on a kind
+   that alternates between 'type and 'element based on the intrinsic."
+  (let ((exprs (cons expr more)))
+    (type-dispatch
+     (lambda (kind maybe-names argss metas)
+       (case kind
+	 ((declared)
+	  (if (null? (car argss))
+	      (apply function 'type `(,@exprs ,init))
+	      (apply fold
+		     (lambda formals
+		       (if (eq? 'binding (car formals))
+			   (match (but-last (cdr formals))
+			     (((': xs Xs) ...)
+			      (apply element-fold function
+				     (apply type-fold function
+					    (last formals)
+					    Xs)
+				     xs))
+			     (_
+			      (parse-error "type-fold: declared types don't match.")))
+			   (apply (case (car formals)
+				    ((element)
+				     element-fold)
+				    ((type)
+				     type-fold))
+				  function
+				  (last formals)
+				  (but-last (cdr formals)))))
+		     init (cons (meta-arguments-kinds (type-ref (car expr)))
+				argss))))
+	 ((undeclared)
+	  (apply function 'type `(,@exprs ,init)))))
+     exprs)))
 
 (define (split-in-three lst start end)
   "Split the given list in three with `start' and `end' the indices delimiting
@@ -263,265 +470,489 @@ the resulting middle list e.g. (a b c d e) 2 3 => (a b) (c) (d e)."
 		 (cons (car zs) ys)
 		 (cdr zs))))))
 
-(define (sub e x y)
- (define (sub% e x y)
-   (if (eq? e x)
-       y
-       (if (symbol? e)
-	   e
-	   (map (lambda (e) (sub e x y)) e))))
- (ifn x e (sub% e x y)))
-
-(define* (match-context expr pattern bindings #:optional index)
-  "Match a context pattern to a context expression, binding symbols in the
-process. Return `#f' if the pattern fails to match or the updated bindings
-otherwise.
-
-expr:     Context expression.
-
-pattern:  Context pattern. For examples, look at the left side of `⊢' in
-          instances of `define-rule'.
-
-bindings: Association list of symbols to matched sub-expressions.
-
-index:    Index of the first type variable in the expression that corresponds to
-          an explicit type variable in the pattern. This is for cases like the
-          expression (: x1 A1) ... (: xn An) with the pattern (Γ (: x X) Δ)
-          where it is unclear from the pattern alone which variable `x'
-          corresponds to."
-  ;; NOTE: By construction, `expr' has the proper syntax.
-  (let* ((m (length expr))
-	 (index (or index m))
-	 (bind-symbols
-	  (lambda* (Γ xs As Δ #:optional u v)
-	    (let ((n (length xs)))
-	      (if (> n (- m index))
-		  #f
-		  (receive (gammas explicit deltas)
-		      (split-in-three expr index (+ index n))
-		    (fold (lambda (x A z prev)
-			    (match-let (((': x' A') z))
-			      (acons x x' (acons A A' prev))))
-			  (ifn Γ 
-			       (ifn Δ
-				    bindings
-				    (acons Δ (sub deltas u v)
-					   bindings))
-			       (ifn Δ
-				    (acons Γ gammas bindings)
-				    (acons Γ gammas (acons Δ (sub deltas u v)
-							   bindings))))
-			  xs As explicit)))))))
-    (match pattern
-      (()
-       (and (= 0 m) bindings))
-      (((? symbol? Γ) (': x A) ...)
-       (bind-symbols Γ x A #f))
-      (((? symbol? Γ) (': x A) ... ('/ Δ u v))
-       (bind-symbols Γ x A Δ u v))
-      (((? symbol? Γ) (': x A) ... Δ)
-       (bind-symbols Γ x A Δ))
-      (((': x A) ...)
-       (bind-symbols #f x A #f))
-      (((': x A) ... ('/ Δ u v))
-       (bind-symbols #f x A Δ u v))
-      (((': x A) ... Δ)
-       (bind-symbols #f x A Δ))
-      (_ (error "Unsupported context pattern syntax.")))))
-
-(define (match-content expr pattern bindings)
-  "See the documentation for `match-context', only here we match the content of
-judgments, i.e. anything right of a `⊢' in instances of `define-rule', and no
-ambiguity arises."
-  ;; NOTE: By construction, `expr' has the proper syntax.
-  (define (equal-expr? v e x y)
-    (or (and (not y)
-	     (eq? v e))
-	(and (eq? v y)
-	     (eq? e x))
-	(and (list? v)
-	     (list? e)
-	     (= (length v)
-		(length e))
-	     (every (lambda (v e)
-		      (equal-expr? v e x y))
-		    v e))))
-  (define* (bind-symbols expr pattern bindings
-			 #:optional generic-judgment? x y)
-    (cond
-     ((member pattern reserved-symbols)
-      (and (eq? pattern expr)
-	   bindings))
-     (generic-judgment?
-      (if (assoc-ref bindings pattern)
-	  (error "Generic judgment thesis already bound.")
-	  (acons pattern (sub expr x y) bindings)))
-     ((symbol? pattern)
-      (if-let (val (assoc-ref bindings pattern))
-	      (and (equal-expr? val expr x y)
-		   bindings)
-	      (acons pattern (sub expr x y) bindings)))
-     ((list? pattern)
-      (match pattern
-	(('/ B x' y')
-	 (let ((x' (assoc-ref bindings x'))
-	       (y' (assoc-ref bindings y')))
-	   (unless (and x' y')
-	     (error "Unbound substitution element."))
-	   (bind-symbols expr B bindings #f x' y')))
-	(((? unreserved-symbol? b)
-	  x)
-	 (if (list? expr)
-	     (and
-	      (= 2 (length expr))
-	      (or (not (assoc-ref bindings b))
-		  (equal-expr? (first expr)
-			       (assoc-ref bindings b)
-			       #f #f))
-	      (or (not (assoc-ref bindings x))
-		  (equal-expr? (second expr)
-			       (assoc-ref bindings x)
-			       #f #f))
-	      (acons b
-		     (make-evaluation (first expr)
-				      (second expr))
-		     bindings))
-	     ;; a symbol
-	     (acons b
-		    (make-evaluation #f expr)
-		    bindings)))
-	(else
-	 (and (list? expr)
-	      (= (length pattern)
-		 (length expr))
-	      (call/cc
-	       (lambda (break)
-		 (fold-right (lambda (e p prev)
-			       (if prev
-				   (bind-symbols e p prev #f x y)
-				   (break #f)))
-			     bindings expr pattern)))))))))
-  (define* (match-content% expr pattern bindings
-			   #:optional generic-judgment? x y)
-    (match pattern
+(define (context-dispatch function ranges exprs)
+  (define (expand-range range start end)
+    (ifn range
+	 (list start end)
+	 (list (or (first range) start)
+	       (or (second range) end))))
+  (apply function
+	 (receive (Γs :xXss Δs)
+	     (unzip3
+	      (map (lambda (range expr)
+		     (match expr
+		       (((? symbol? Γ) :xXs ... (? symbol? Δ))
+			(receive (a b c)
+			    (apply split-in-three
+				   :xXs
+				   (expand-range range 0 (length :xXs)))
+			  (list (cons Γ a) b `(,@c ,Δ))))
+		       (((? symbol? Γ) :xXs ... ('/ (? symbol? Δ) x y))
+			(receive (a b c)
+			    (apply split-in-three
+				   :xXs
+				   (expand-range range 0 (length :xXs)))
+			  (list (cons Γ a) b `(,@c ,Δ))))
+		       (((? symbol? Γ) :xXs ...)
+			(receive (a b c)
+			    (apply split-in-three
+				   :xXs
+				   (expand-range range 0 (length :xXs)))
+			  (list (cons Γ a) b c)))
+		       ((:xXs ...)
+			(receive (a b c)
+			    (apply split-in-three
+				   :xXs
+				   (expand-range range 0 (length :xXs)))
+			  (list a b c)))
+		       (_ (parse-error "context-fold: unknown expression."))))
+		   (or ranges (list-tabulate (length exprs) not))
+		   exprs))
+	   (if (apply = (map length :xXss))
+	       (list Γs :xXss Δs)
+	       (parse-error "context-dispatch: contexts should have the same range, but got ~{~a~^ ~}." :xXss)))))
+
+(define (context-map function ranges expr . more)
+  (context-dispatch
+   (lambda (Γs :xXss Δs)
+     (append
+      (if (null? (car Γs)) '() (apply function 'Γ Γs))
+      (reverse
+       (cdr
+	(apply fold
+	       (lambda formals
+		 (let* ((:xXs (but-last formals)) ; one decl per judgment
+			(z (last formals))
+			(ctxs (car z))
+			(prev (cdr z)))
+		   (if (any identity (map (lambda (ctx :xX)
+					    (context-ref ctx (second :xX)))
+					  ctxs :xXs))
+		       (parse-error "context-map: variable can only be declared once.")
+		       (cons (map cons :xXs ctxs)
+			     (cons
+			      (list ':
+				    (apply function 'variable (map second :xXs))
+				    (apply type-map function (map third :xXs)))
+			      prev)))))
+	       (cons (list-tabulate (length :xXss) (const '()))
+		     '())
+	       :xXss)))
+      (if (null? (car Δs)) '() (apply function 'Δ Δs))))
+   ranges (cons expr more)))
+
+(define (context-fold function ranges init expr . more)
+  (context-dispatch
+   (lambda (Γs :xXss Δs)
+     ;; See `context-map' for the format of Γs :xXss Δs.
+     (apply
+      (ifn (null? (car Δs)) function (lambda formals (last formals)))
+      'Δ
+      `(,@Δs
+	,(apply fold
+		(lambda formals
+		  (let* ((:xXs (but-last formals)) ; one decl per judgment
+			 (prev (last formals)))
+		    (if (any identity
+			     (map (lambda (ctx :xX)
+				    (context-ref ctx (element-of-:xX :xX)))
+				  (*ctxs*)
+				  :xXs))
+			(parse-error "context-fold: variable can only be declared once.")
+			(begin
+			  (*ctxs* (map cons :xXs (*ctxs*)))
+			  (apply function 'variable
+				 `(,@(map element-of-:xX :xXs)
+				   ,(apply function 'type `(,@(map third :xXs)
+							    ,prev))))))))
+		(apply (ifn (null? (car Γs)) function (lambda formals (last formals)))
+		       'Γ `(,@Γs ,init))
+		:xXss))))
+   ranges (cons expr more)))
+
+(define (content-dispatch function exprs)
+  (define (content-match expr)
+    (match expr
+      ;; generic judgment
+      (('/ (? symbol? J) (? symbol? a) (? symbol? b))
+       (list 'generic (make-substitution J a b)))
+      ((? symbol? J)
+       (list 'generic J))
+      ;; type
       (('type A)
-       (bind-symbols expr pattern bindings #f x y))
-      ((': a A)
-       (bind-symbols expr pattern bindings #f x y))
+       (list 'type A))
+      ;; judgmentally equal types
+      (('≐ ('/ A
+	       (? symbol? x)
+	       (? symbol? y))
+	   ('/ B
+	       (? symbol? x')
+	       (? symbol? y)))
+       (list 'type-eq
+	     (make-substitution A x y)
+	     (make-substitution B x' y)))
       (('≐ A B)
-       (bind-symbols expr pattern bindings #f x y))
+       (list 'type-eq A B))
+      ;; judgmentally equal elements of a type
+      (('≐ ('/ a
+	       (? symbol? x)
+	       (? symbol? y))
+	   ('/ b
+	       (? symbol? x')
+	       (? symbol? y))
+	   ('/ A
+	       (? symbol? x)
+	       (? symbol? y)))
+       (list 'element-eq
+	     (make-substitution a x y)
+	     (make-substitution b x' y)
+	     (make-substitution A x y)))
       (('≐ a b A)
-       (bind-symbols expr pattern bindings #f x y))
-      ((? symbol? J)
-       (bind-symbols expr J bindings #t x y))
-      (('/ J (? symbol? x) (? symbol? y))
-       (let ((x (assoc-ref bindings x))
-	     (y (assoc-ref bindings y)))
-	 (unless (and x y)
-	   (error "Unbound substitution element."))
-	 (match-content% expr J bindings (symbol? J) x y)))
-      (_ (error "Unsupported content pattern syntax."))))
-  (match-content% expr pattern bindings))
-
-(define* (match-judgment expr pattern bindings #:optional index)
-  ;; NOTE: By construction, `expr' has the proper syntax.
-  (match pattern
-    ((ctx ... '⊢ J)
-     (match expr
-       ((ctx' ... '⊢ J')
-	(and=> (match-context ctx' ctx bindings index)
-	       (lambda (bindings)
-		 (match-content J' J bindings))))))
-    (_ (error "Unsupported judgment pattern syntax."))))
-
-(define (replace-in-judgment pattern bindings)
-  "Replace all bound symbols (leaves) in the pattern (tree)."
-  (define (replace-in-ctx x)
-    (if (symbol? x)
-	(or (assoc-ref bindings x)
-	    x)
-	(map replace-in-ctx x)))
-  (define (replace-in-content x)
-    (match x
-      ((? symbol? x)
-       (if-let (y (assoc-ref bindings x))
-	       (ifn (evaluation? y)
-		    y
-		    (if (evaluation-function y)
-			(evaluation-function y)
-			(error "Can't separate function from value.")))
-	       x))
-      (((? unreserved-symbol? b)
-	(? symbol? y))
-       (let ((z (assoc-ref bindings b)))
-	 (ifn (evaluation-function z)
-	      (evaluation-value z)
-	      (list (evaluation-function z)
-		    (evaluation-value z)))))
-      (else
-       (map replace-in-content x))))
-  (match pattern
-    ((ctx ... '⊢ J)
-     (append
-      (concatenate
-       (map (lambda (x)
-	      (if (list? x)
-		  (list (replace-in-ctx x))
-		  (let ((y (replace-in-ctx x)))
-		    (if (symbol? y)
-			(list y)
-			y))))
-	    ctx))
-      (list '⊢ (replace-in-content J))))
-    (_ (error "Unsupported judgment pattern syntax."))))
-
-(define (d expr)
-  (let ((tree (list expr)))
-    (make-derivation tree (list tree))))
-
-(define (exact derivation)
-  (let* ((ps (derivation-points derivation))
-	 (p (car ps)))
-    (set-cdr! p '.)
-    (derivation-points-set! derivation (cdr ps))
-    derivation))
-
-(define (list-hypotheses derivation)
-  (delete-duplicates
-   (let rec ((tree (derivation-tree derivation)))
-     (if (eq? '. (cdr tree))
-	 (list (car tree))
-	 (fold-right
-	  (lambda (x prev)
-	    (append (rec x) prev))
-	  '()
-	  (cdr tree))))
-   equal?))
-
-(define conclusion (compose car derivation-tree))
-
-(defmacro define-derivation% (name conclusion hypotheses . rules)
-  (let ((C (parse-judgment conclusion))
-	(Hs (all parse-judgment hypotheses)))
-    (ifn (and C Hs)
-	 (error "SYNTAX")
-	 (if-let (derivation (apply-rules (d C) rules))
-		 (let ((Hs' (list-hypotheses derivation)))
-		   (ifn (and (null? (lset-difference equal? Hs' Hs))
-			     (null? (lset-difference equal? Hs Hs')))
-			(error "DERIVATION 1")
-			(begin
-			  (hash-set! *rules*
-				     name
-				     (cons '() `(,conclusion ,@hypotheses)))
-			  `(hash-set! *rules*
-				      ',name
-				      (cons '() '(,conclusion ,@hypotheses))))))
-		 (error "DERIVATION 2")))))
-
-(define-syntax-rule (define-derivation name
-		      (conclusion hypothesis ...)
-		      (rule arg ...) ...)
-  (define-derivation% name conclusion (hypothesis ...)
-    (rule arg ...)
-    ...))
+       (list 'element-eq a b A))
+      ;; element of a type
+      ((': a A)
+       (list 'element a A))
+      (_ (parse-error "content-dispatch: unknown expression."))))
+  (let* ((xs (map content-match exprs))
+	 (generic? (papply eq? 'generic))
+	 (kinds (map car xs)))
+    (unless (apply eq? (remove generic? kinds))
+      (parse-error "content-dispatch: contents don't match."))
+    (ifn (any generic? kinds)
+	 (apply function (find (compose not generic?)
+			       kinds)
+		(unzip (map cdr xs)))
+	 (apply function 'generic
+		(map (lambda (kind x)
+		       (if (generic? kind)
+			   (second x)
+			   (match x
+			     (('type A)
+			      x)
+			     (('type-eq A B)
+			      (list '≐ A B))
+			     (('element-eq a b A)
+			      (list '≐ a b A))
+			     (('element a A)
+			      (list ': a A)))))
+		     kinds xs)))))
+
+(define (content-map function expr . more)
+  (content-dispatch
+   (lambda (kind . args)
+     (case kind
+       ((generic)
+	(apply function 'generic args))
+       ((type)
+	(list 'type (apply type-map function (first args))))
+       ((element)
+	(list ':
+	      (apply element-map function (first args))
+	      (apply type-map function (second args))))
+       ((type-eq)
+	(list '≐
+	      (apply type-map function (first args))
+	      (apply type-map function (second args))))
+       ((element-eq)
+	(list '≐
+	      (apply element-map function (first args))
+	      (apply element-map function (second args))
+	      (apply type-map function (third args))))))
+   (cons expr more)))
+
+(define (content-fold function init expr . more)
+  (content-dispatch
+   (lambda (kind . args)
+     (case kind
+       ((generic)
+	(apply function 'generic `(,@args ,init)))
+       ((type)
+	(apply type-fold function init (first args)))
+       ((element)
+	(apply element-fold function
+	       (apply type-fold function init (second args))
+	       (first args)))
+       ((type-eq)
+	(apply type-fold function
+	       (apply type-fold function init (second args))
+	       (first args)))
+       ((element-eq)
+	(apply element-fold function
+	       (apply element-fold function
+		      (apply type-fold function init (third args))
+		      (first args))
+	       (second args)))))
+   (cons expr more)))
+
+(define (judgment-dispatch function exprs)
+  (match exprs
+    (((contexts ... '⊢ contents) ...)
+     (function contexts contents))
+    (_ (parse-error "judgment-dispatch: unknown expression."))))
+
+(define (judgment-map function ranges expr . more)
+  (judgment-dispatch (lambda (ctxs cnts)
+		       (append (apply context-map function ranges ctxs)
+			       (list '⊢)
+			       (list (apply content-map function cnts))))
+		     (cons expr more)))
+
+(define (judgment-fold function ranges init expr . more)
+  (parameterize ((*ctxs* (map (const '()) (cons expr more))))
+   (judgment-dispatch (lambda (ctxs cnts)
+			(apply content-fold function
+			       (apply context-fold function ranges init ctxs)
+			       cnts))
+		      (cons expr more))))
+
+(defmacro define-rule (name judgment . more)
+  (begin
+    (when (eq? name 'exact)
+      (parse-error "define-rule: the rule name \"exact\" is reserved."))
+    (for-each (lambda (judgment)
+		(judgment-fold
+		 (lambda (kind x prev)
+		   prev)
+		 #f #f judgment))
+	      (cons judgment more))
+    ;; We declare types or constructors when they occur.
+    (let ((content (judgment-content judgment)))
+      (when (list? content)
+	(let ((kind (case (first content)
+		      ((type) 'type)
+		      ((:) 'element)
+		      (else 'else))))
+	  (when (member kind '(type element))
+	    (if-let (maybe-name (pre-destruct kind (second content)))
+		    (unless (and (eq? 'element kind)
+				 (judgment-fold
+				  (lambda (kind' x prev)
+				    (ifn (eq? kind kind')
+					 prev
+					 (or prev (context-ref (car (*ctxs*))
+							       (just maybe-name)))))
+				  #f #f judgment))
+		      (unless (any (lambda (judgment)
+				     (judgment-fold
+				      (lambda (kind' x prev)
+					(ifn (eq? kind kind')
+					     prev
+					     (or prev (equal? x (just maybe-name)))))
+				      #f #f judgment))
+				   more)
+			(hash-set! (if (eq? kind 'type)
+				       *types*
+				       *constructors*)
+				   (just maybe-name)
+				   (cons judgment more)))))))))
+    (hash-set! *rules* name `,(cons judgment more))
+    `(begin
+       (hash-set! *rules* ',name ',(cons judgment more))
+       (values))))
+
+(define (replace-judgment mappings judgment)
+  (judgment-map
+   (lambda (kind x)
+     (or 
+      (if (member kind '(Γ Δ))
+	  (assoc-ref mappings (car x))
+	  (if (member kind '(element variable type generic))
+	      (assoc-ref mappings x)
+	      x))
+      (parse-error "replace-judgment: expression ~a not mapped in ~a." x mappings)))
+   #f judgment))
+
+(define (substitute mapper x y mapping)
+  (acons (substitution-pattern x)
+	 (mapper
+	  (lambda (kind z)
+	    (if (and (eq? kind 'type)
+		     (receive (maybe-name args meta) (destruct 'type z)
+		       (and (not meta) (= 1 (length args)))))
+		(ifn (equal? (second z) (assoc-ref mapping (substitution-source x)))
+		     z
+		     (list (first z)
+			   (assoc-ref mapping (substitution-destination x))))
+		(ifn (equal? z (assoc-ref mapping (substitution-source x)))
+		     z
+		     (assoc-ref mapping (substitution-destination x)))))
+	  y)
+	 mapping))
+
+(define* (apply-rule derivation name #:key start end . args)
+  (let ((err1 "apply-rule: derivation is pointless.")
+	(err2 "apply-rule: substitutions are only allowed in rules.")
+	(err3 "apply-rule: can't apply a specific judgment rule to a generic judgment expression.")
+	(err4 "define-derivation: rule ~s is undefined."))
+    (expand-derivation-point
+     derivation
+     (if start
+	 (if end
+	     `(,name #:start ,start #:end ,end ,@args)
+	     `(,name #:start ,start ,@args))
+	 `(,name ,@args))
+     (let ((Jp (derivation-point derivation)))
+       (unless Jp
+	 (parse-error err1))
+       (if (eq? name 'exact)
+	   #t
+	   (if-let (m (ifn (eq? name 'definition)
+			   (rule-ref name)
+			   (hash-ref *definition-rules* (just (pre-destruct 'type (second (judgment-content Jp)))))))
+		   ;; NOTE: Computing the mapping is essential to be sure
+		   ;; the meta-conclusion matches the judgment point even
+		   ;; in cases where there are no hypotheses.
+		   (let ((mapping
+			  (judgment-fold
+			   (lambda (kind x y prev)
+			     (case kind
+			       ((Γ)
+				(if (substitution? y)
+				    (parse-error err2)
+				    (ifn (substitution? x)
+					 (acons (car x) y prev)
+					 (ifn (null? (cdr y))
+					      (parse-error "TBD")
+					      (acons (substitution-pattern x)
+						     y prev)))))
+			       ((Δ)
+				(if (substitution? y)
+				    (parse-error err2)
+				    (ifn (substitution? x)
+					 (acons (car x) y prev)
+					 (ifn (null? (cdr y))
+					      (parse-error "TBD")
+					      (acons (substitution-pattern x)
+						     y prev)))))
+			       ((element)
+				(if (substitution? y)
+				    (parse-error err2)
+				    (ifn (substitution? x)
+					 (acons x y prev)
+					 (substitute element-map x y prev))))
+			       ((type)
+				(if (substitution? y)
+				    (parse-error err2)
+				    (ifn (substitution? x)
+					 (acons x y prev)
+					 (substitute type-map x y prev))))
+			       ((generic)
+				(if (and (not (list? y))
+					 (list? x))
+				    ;; if y is generic so must x.
+				    (parse-error err3)
+				    (ifn (substitution? x)
+					 (acons x y prev)
+					 (if (not (list? y))
+					     (acons (substitution-pattern x)
+						    y prev)
+					     (substitute content-map x y prev)))))
+			       ((variable)
+				(acons x y prev))
+			       (else
+				prev)))
+			   (list #f (list start end))
+ 			   ;; When `#:start'/`#:end' is provided the evaluator
+			   ;; adds it to the head of the `args' list (see the
+			   ;; documentation for `define*') followed by its value,
+			   ;; and must be removed.
+			   (alist<-plist
+			    (if start
+				(if end
+				    (drop args 4)
+				    (drop args 2))
+				(if end
+				    (drop args 2)
+				    args)))
+
+			   (meta-conclusion m)
+			   Jp)))
+		     (map
+		      (lambda (judgment)
+			(cons (replace-judgment mapping judgment)
+			      #f))
+		      (meta-hypotheses m)))
+		   (parse-error err4 name)))))))
+
+(defmacro define-derivation% (name kind maybe-assignment conclusion hypotheses rule . more)
+  (let ((derivation
+	 (fold (lambda (step derivation)
+		 (apply apply-rule derivation step))
+	       (d conclusion)
+	       (cons rule more))))
+    (ifn (lset= equal? hypotheses (list-hypotheses derivation))
+	 (parse-error
+	  "define-derivation: expected remaining hypotheses ~a, but got ~a."
+	  hypotheses (list-hypotheses derivation))
+	 (if maybe-assignment
+	     (begin
+	       (hash-set!
+		*rules*
+		name
+		(cons `(,@(judgment-context conclusion)
+			⊢
+			,(if (eq? kind 'type)
+			     (list 'type (just maybe-assignment))
+			     (list ':
+				   (just maybe-assignment)
+				   (third (judgment-content conclusion)))))
+		      hypotheses))
+	       (hash-set!
+		*definition-rules*
+		name
+		(cons `(,@(judgment-context conclusion)
+			⊢
+			,(if (eq? kind 'type)
+			     (list '≐
+				   (just maybe-assignment) 
+				   (second (judgment-content conclusion)))
+			     (list '≐
+				   (just maybe-assignment) 
+				   (second (judgment-content conclusion))
+				   (third (judgment-content conclusion))))) 
+		      hypotheses))
+	       (hash-set! (if (eq? kind 'type) *types* *constructors*)
+			  (just (pre-destruct 'type (just maybe-assignment)))
+			  (rule-ref name))
+	       '(values)
+	       )
+	     (begin
+	       (hash-set! *rules* name (cons conclusion hypotheses))
+	       '(values))))))
+
+;; NOTE: A derivation must have at least one derivation rule (can't derive a
+;;       statement out of nothing).
+(define-syntax define-derivation
+  (syntax-rules (:= ⊢ type :)
+    ((_ name ((Γ ⊢ (:= a (type expr)))
+	      hypothesis ...)
+	(rule-1 arg-1 ...)
+	(rule-2 arg-2 ...)
+	...)
+     (define-derivation% name type (just . a) (Γ ⊢ (type expr)) (hypothesis ...)
+       (rule-1 arg-1 ...)
+       (rule-2 arg-2 ...)
+       ...))
+    ((_ name ((Γ ⊢ (:= a (: b B)))
+	      hypothesis ...)
+	(rule-1 arg-1 ...)
+	(rule-2 arg-2 ...)
+	...)
+     (define-derivation% name element (just . a) (Γ ⊢ (: b B)) (hypothesis ...)
+       (rule-1 arg-1 ...)
+       (rule-2 arg-2 ...)
+       ...))
+    ((_ name (conclusion hypothesis ...)
+	(rule-1 arg-1 ...)
+	(rule-2 arg-2 ...)
+	...)
+     (define-derivation% name #f #f conclusion (hypothesis ...)
+       (rule-1 arg-1 ...)
+       (rule-2 arg-2 ...)
+       ...))))
+
+(define (define-derivation-list name derivation)
+  (let ((tree (derivation-tree derivation)))
+   `(define-derivation ,name
+      (,(car tree) ,@(list-hypotheses derivation))
+      ,@(reverse (derivation-steps derivation)))))
-- 
2.39.5