From: admin <admin@vouivredigital.com>
Date: Fri, 5 Apr 2024 02:50:45 +0000 (+0900)
Subject: Implement a new type system
X-Git-Url: https://git.vouivredigital.com/?a=commitdiff_plain;h=701c145be66145d48118666f786165712d5abbdc;p=vouivre.git

Implement a new type system
---

diff --git a/vouivre/misc.scm b/vouivre/misc.scm
index accc3ba..7f51bfa 100644
--- a/vouivre/misc.scm
+++ b/vouivre/misc.scm
@@ -17,9 +17,11 @@
 
 (define-module (vouivre misc)
   #:use-module (ice-9 arrays)
+  #:use-module (ice-9 match)
   #:use-module (srfi srfi-1)
   #:export
-  (array-map
+  (alist<-plist
+   array-map
    array-map-indexed
    flip
    for-indices-in-range
@@ -30,6 +32,20 @@
    produce-array
    produce-typed-array))
 
+(define (alist<-plist plist)
+  "Convert a property list to an association list."
+  (cdr
+   (fold-right
+    (lambda (x prev)
+      (match-let (((p . bindings) prev))
+	(if (null? p)
+	    (cons (cons #f x) bindings)
+	    (begin
+	      (set-car! p x)
+	      (cons '() (cons p bindings))))))
+    '(() . ())
+    plist)))
+
 (define (flip f)
   "Returns a procedure behaving as `f', but with arguments taken in reverse
 order."
diff --git a/vouivre/rules.scm b/vouivre/rules.scm
new file mode 100644
index 0000000..28f36d3
--- /dev/null
+++ b/vouivre/rules.scm
@@ -0,0 +1,292 @@
+;;;; Copyright (C) 2024 Vouivre Digital Corporation
+;;;;
+;;;; This file is part of Vouivre.
+;;;;
+;;;; Vouivre is free software: you can redistribute it and/or
+;;;; modify it under the terms of the GNU General Public
+;;;; License as published by the Free Software Foundation, either
+;;;; version 3 of the License, or (at your option) any later version.
+;;;;
+;;;; Vouivre is distributed in the hope that it will be useful,
+;;;; but WITHOUT ANY WARRANTY; without even the implied warranty of
+;;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+;;;; General Public License for more details.
+;;;;
+;;;; You should have received a copy of the GNU General Public
+;;;; License along with Vouivre. If not, see <https://www.gnu.org/licenses/>.
+
+(define-module (vouivre type rules)
+  #:use-module (vouivre type system))
+
+;;;; 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-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)
+  (exact)
+  (weakening #:index 1)
+  (exact)
+  (exact))
+
+(define-derivation interchange ((Γ (: y B) (: x A) Δ ⊢ J)
+				(Γ ⊢ (type B))
+				(Γ ⊢ (type A))
+				(Γ (: x A) (: y B) Δ ⊢ J))
+  (substitution #:index 3 a y x y' A B)
+  (weakening #:index 2)
+  (weakening #:index 1)
+  (exact)
+  (exact)
+  (generic-element #:index 1)
+  (exact)
+  (weakening #:index 1)
+  (exact)
+  (substitution #:index 3 a y' x y A B)
+  (weakening #:index 1)
+  (exact)
+  (generic-element #:index 1)
+  (exact)
+  (weakening #:index 2)
+  (weakening #:index 1)
+  (exact)
+  (exact)
+  (exact))
+
+(define-derivation element-conversion ((Γ ⊢ (: a A'))
+				       (Γ ⊢ (: a A))
+				       (Γ ⊢ (≐ A A')))
+  (substitution a a x a' A A)
+  (exact)
+  (variable-conversion #:index 1 A A')
+  (type-symmetric)
+  (exact)
+  (generic-element #:index 1)
+  (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)
+  (exact)
+  (variable-conversion #:index 1 A A')
+  (type-symmetric)
+  (exact)
+  (generic-element #:index 1)
+  (formation-3)
+  (exact))
+
+(define-derivation identity ((Γ ⊢ (: (λ x x) (→ A A)))
+			     (Γ ⊢ (type A)))
+  (λ)
+  (exact)
+  (generic-element #:index 1)
+  (exact))
+
+(define-derivation not ((⊢ (: (λ x (((if x) false) true))
+			      (→ Bool Bool))))
+  (λ)
+  (bool-formation)
+  (substitution a true x y A Bool)
+  (weakening #:index 0)
+  (bool-formation)
+  (bool-introduction-1)
+  (ev #:index 1)
+  (substitution a false x y A Bool)
+  (weakening #:index 0)
+  (bool-formation)
+  (bool-introduction-2)
+  (ev #:index 1)
+  (ev #:index 0)
+  (bool-elimination)
+  (bool-formation))
diff --git a/vouivre/system.scm b/vouivre/system.scm
new file mode 100644
index 0000000..042570e
--- /dev/null
+++ b/vouivre/system.scm
@@ -0,0 +1,527 @@
+;;;; Copyright (C) 2024 Vouivre Digital Corporation
+;;;;
+;;;; This file is part of Vouivre.
+;;;;
+;;;; Vouivre is free software: you can redistribute it and/or
+;;;; modify it under the terms of the GNU General Public
+;;;; License as published by the Free Software Foundation, either
+;;;; version 3 of the License, or (at your option) any later version.
+;;;;
+;;;; Vouivre is distributed in the hope that it will be useful,
+;;;; but WITHOUT ANY WARRANTY; without even the implied warranty of
+;;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+;;;; General Public License for more details.
+;;;;
+;;;; You should have received a copy of the GNU General Public
+;;;; License along with Vouivre. If not, see <https://www.gnu.org/licenses/>.
+
+(define-module (vouivre type system)
+  #:use-module (ice-9 match)
+  #:use-module (ice-9 receive)
+  #:use-module (srfi srfi-1)
+  #:use-module (srfi srfi-9)
+  #:use-module (vouivre misc)
+  #:export
+  (*rules*
+   apply-rule
+   apply-rules
+   conclusion
+   d
+   define-derivation
+   define-rule
+   exact
+   list-hypotheses))
+
+(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))
+
+(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)
+  (call/cc
+   (lambda (break)
+     (fold (lambda (rule prev)
+	     (if-let (x (apply apply-rule prev (car rule) (cdr rule)))
+		     x
+		     (break #f)))
+	   derivation rules))))
+
+(define (split-in-three lst start end)
+  "Split the given list in three with `start' and `end' the indices delimiting
+the resulting middle list e.g. (a b c d e) 2 3 => (a b) (c) (d e)."
+  (let rec ((i 0)
+	    (xs '())
+	    (ys '())
+	    (zs lst))
+    (if (= i end)
+	(values (reverse xs)
+		(reverse ys)
+		zs)
+	(if (< i start)
+	    (rec (1+ i)
+		 (cons (car zs) xs)
+		 ys
+		 (cdr zs))
+	    (rec (1+ i)
+		 xs
+		 (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
+      (('type A)
+       (bind-symbols expr pattern bindings #f x y))
+      ((': a A)
+       (bind-symbols expr pattern bindings #f x y))
+      (('≐ A B)
+       (bind-symbols expr pattern bindings #f 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 ...)
+    ...))