From f8cbe1ad23b3466254c67b29b07598abe269e85e Mon Sep 17 00:00:00 2001
From: Robby Findler <robby@racket-lang.org>
Date: Fri, 9 Dec 2011 20:08:57 -0600
Subject: [PATCH] add the List Machine benchmark by Appel, Dockins, and Leroy

---
 collects/redex/examples/README                |  11 +-
 .../redex/examples/list-machine/README.txt    |  16 ++
 .../list-machine/list-machine-typing.rkt      | 178 ++++++++++++++++++
 .../examples/list-machine/list-machine.rkt    |  98 ++++++++++
 .../redex/examples/list-machine/p-sample.rkt  |  38 ++++
 .../redex/examples/list-machine/slides.rkt    |  85 +++++++++
 collects/redex/examples/list-machine/test.rkt | 158 ++++++++++++++++
 7 files changed, 580 insertions(+), 4 deletions(-)
 create mode 100644 collects/redex/examples/list-machine/README.txt
 create mode 100644 collects/redex/examples/list-machine/list-machine-typing.rkt
 create mode 100644 collects/redex/examples/list-machine/list-machine.rkt
 create mode 100644 collects/redex/examples/list-machine/p-sample.rkt
 create mode 100644 collects/redex/examples/list-machine/slides.rkt
 create mode 100644 collects/redex/examples/list-machine/test.rkt

diff --git a/collects/redex/examples/README b/collects/redex/examples/README
index 3d4ddcee1a..c4cee3af2d 100644
--- a/collects/redex/examples/README
+++ b/collects/redex/examples/README
@@ -21,7 +21,7 @@ to demonstrate various different uses of PLT Redex:
   closure. Also, one of the first examples from Matthias
   Felleisen and Matthew Flatt's monograph
 
-  cont-mark-transform: the continuation mark transformation from
+  cont-mark-transform/: the continuation mark transformation from
   McCarthy's ICFP '09 paper “Automatically RESTful Web Applications
   Or, Marking Modular Serializable Continuations" 
 
@@ -31,13 +31,16 @@ to demonstrate various different uses of PLT Redex:
 
   define-judgment-form: example uses of `define-judgment-form'
 
-  delim-cont: The model from Flatt, Yu, Findler, and Felleisen's ICFP
+  delim-cont/: The model from Flatt, Yu, Findler, and Felleisen's ICFP
   '07 paper "Adding Delimited and Composable Control to a Production
   Programming Environment"
 
   letrec.rkt: shows how to model letrec with a store and
   some infinite looping terms
 
+  list-machine/: the List Machine benchmark by Appel, Dockins, and
+  Leroy.
+
   omega.rkt: the call by value lambda calculus with call/cc.
   Includes omega and two call/cc-based infinite loops, one of
   which has an ever-expanding term size and one of which has
@@ -46,10 +49,10 @@ to demonstrate various different uses of PLT Redex:
   pi-calculus.rkt: a formulation of the pi calculus, following
   Milner's 1990 paper, "Functions as Processes"
 
-  racket-machine: an operational semantics for (much of) Racket 
+  racket-machine/: an operational semantics for (much of) Racket
   bytecode
 
-  r6rs: an implementation of the R6RS Scheme formal semantics
+  r6rs/: an implementation of the R6RS Scheme formal semantics
 
   semaphores.rkt: a simple threaded language with semaphores
 
diff --git a/collects/redex/examples/list-machine/README.txt b/collects/redex/examples/list-machine/README.txt
new file mode 100644
index 0000000000..c2832620e0
--- /dev/null
+++ b/collects/redex/examples/list-machine/README.txt
@@ -0,0 +1,16 @@
+This is the model from
+
+  A List-machine Benchmark for Mechanized Metatheory
+  Andrew W. Appel, Robert Dockins, and Xavier Leroy
+
+Specifically, it contains all of the formal definitions in sections 3
+and 4 (list-machine.rkt), section 5 (list-machine-typing.rkt), the
+example from section 6 (sample.rkt), and the lub definition in 8.1
+(also in list-machine-typing.rkt).
+
+All of the relations and functions are directly executable in Redex
+(using the lub definition from 8.1, not the one in 5).
+
+The file test.rkt contains unit tests, roughly one per case in each of
+the definitions, and the file slides.rkt is a Slideshow presentation
+that shows the instruction reduction relation and the type system.
diff --git a/collects/redex/examples/list-machine/list-machine-typing.rkt b/collects/redex/examples/list-machine/list-machine-typing.rkt
new file mode 100644
index 0000000000..a2f21deba7
--- /dev/null
+++ b/collects/redex/examples/list-machine/list-machine-typing.rkt
@@ -0,0 +1,178 @@
+#lang racket
+(require redex
+         "list-machine.rkt")
+
+(provide list-machine-typing
+         check-program
+         check-blocks
+         check-block
+         check-instr
+         :set :lookup
+         ⊂ ⊔ Γ-⊂
+         dom l-⊂)
+
+(define-extended-language list-machine-typing list-machine
+  (τ nil (list τ) (listcons τ))
+  (Γ empty (v : τ Γ))
+  (Π empty (l : Γ Π)))
+
+(define-judgment-form list-machine-typing
+  #:contract (check-program p Π)
+  #:mode (check-program I I)
+  [(check-blocks Π p)
+   (where #t (l-⊂ (dom Π) (dom p)))
+   (:lookup Π l0 (v0 : nil empty))
+   -----
+   (check-program p Π)])
+
+(define-judgment-form list-machine-typing
+  #:contract (Γ-⊂ Γ Γ)
+  #:mode (Γ-⊂ I I)
+  [-----
+   (Γ-⊂ Γ empty)]
+  [(:lookup Γ_1 v τ_1) 
+   (⊂ τ_1 τ_2)
+   (Γ-⊂ Γ_1 Γ_2)
+   ----
+   (Γ-⊂ Γ_1 (v : τ_2 Γ_2))])
+
+(define-judgment-form list-machine-typing
+  #:contract (check-blocks Π p)
+  #:mode (check-blocks I I)
+  [(:lookup Π l Γ)
+   (check-block Π Γ ι)
+   (check-blocks Π p)
+   -----
+   (check-blocks Π (l : ι p)) ]
+  [-----
+   (check-blocks Π end)])
+
+(define-judgment-form list-machine-typing
+  #:contract (check-block Π Γ ι)
+  #:mode (check-block I I I)
+  [-----
+   (check-block Π Γ halt)]
+  [(check-instr Π Γ ι_1 Γ_2) 
+   (check-block Π Γ_2 ι_2)
+   -----
+   (check-block Π Γ (begin ι_1 ι_2))]
+  [(:lookup Π l Γ_2)
+   (Γ-⊂ Γ Γ_2)
+   -----
+   (check-block Π Γ (jump l))])
+
+(define-judgment-form list-machine-typing
+  #:contract (check-instr Π Γ ι Γ)
+  #:mode (check-instr I I I O)
+  [(check-instr Π Γ ι_1 Γ_1)
+   (check-instr Π Γ_1 ι_2 Γ_2)
+   -----
+   (check-instr Π Γ (begin ι_1 ι_2) Γ_2)]
+  [(:lookup Γ v (list τ))
+   (:lookup Π l Γ_1)
+   (:set Γ v nil Γ_3)
+   (Γ-⊂ Γ_3 Γ_1)
+   (:set Γ_3 v (listcons τ) Γ_2)
+   -----
+   (check-instr Π Γ (branch-if-nil v l) Γ_2)]
+  [(:lookup Γ v (listcons τ))
+   (:lookup Π l Γ_1)
+   (:set Γ v nil Γ_2)
+   (Γ-⊂ Γ_2 Γ_1)
+   -----
+   (check-instr Π Γ (branch-if-nil v l) Γ)]
+  [(:lookup Γ v nil)
+   (:lookup Π l Γ_1)
+   (Γ-⊂ Γ Γ_1)
+   -----
+   (check-instr Π Γ (branch-if-nil v l) Γ)]
+  [(:lookup Γ v (listcons τ)) (:set Γ v_2 τ Γ_2)
+   -----
+   (check-instr Π Γ (fetch-field v 0 v_2) Γ_2)]
+  [(:lookup Γ v (listcons τ)) (:set Γ v_2 (list τ) Γ_2)
+   -----
+   (check-instr Π Γ (fetch-field v 1 v_2) Γ_2)]
+  [(:lookup Γ v_0 τ_0) (:lookup Γ v_0 τ_1)
+   (⊔ (list τ_0) τ_1 (list τ)) (:set Γ v (listcons τ) Γ_2)
+   -----
+   (check-instr Π Γ (cons v_0 v_1 v) Γ_2)])
+(define-judgment-form list-machine-typing
+  #:contract (⊂ τ τ)
+  #:mode (⊂ O I)
+  [-----
+   (⊂ τ τ)]
+  [-----
+   (⊂ nil (list τ))]
+  [(⊂ τ τ_2)
+   -----
+   (⊂ (list τ) (list τ_2))]
+  [(⊂ τ τ_2)
+   -----
+   (⊂ (listcons τ) (list τ_2))]
+  [(⊂ τ τ_2)
+   -----
+   (⊂ (listcons τ) (listcons τ_2))])
+
+(define-judgment-form list-machine-typing
+  #:contract (⊔ τ τ τ)
+  #:mode (⊔ I I O)
+  [-----
+   (⊔ τ τ τ)]
+  [-----
+   (⊔ (list τ) nil (list τ))]
+  [-----
+   (⊔ nil (list τ) (list τ))]
+  [(⊔ (list τ_1) (list τ_2) τ_3)
+   -----
+   (⊔ (list τ_1) (listcons τ_2) τ_3)]
+  [(⊔ (list τ_1) (list τ_2) τ_3)
+   -----
+   (⊔ (listcons τ_1) (list τ_2) τ_3)]
+  [(⊔ τ_1 τ_2 τ_3)
+   -----
+   (⊔ (list τ_1) (list τ_2) (list τ_3))]
+  [-----
+   (⊔ (listcons τ) nil (list τ))]
+  [-----
+   (⊔ nil (listcons τ) (list τ))]
+  [(⊔ τ_1 τ_2 τ_3)
+   -----
+   (⊔ (listcons τ_1) (listcons τ_2) (listcons τ_3))])
+
+(define-judgment-form list-machine-typing
+  #:contract (:lookup any v any)
+  #:mode (:lookup I I O)
+  [-----
+   (:lookup (v : any_τ any_Γ) v any_τ)]
+  [(where #t (different v_1 v_2))
+   (:lookup any_Γ v_2 any_τ2)
+   -----
+   (:lookup (v_1 : any_τ1 any_Γ) v_2 any_τ2)])
+
+(define-judgment-form list-machine-typing
+  #:contract (:set Γ v τ Γ)
+  #:mode (:set I I I O)
+  [-----
+   (:set (v : any_τ any_Γ) v any_τ2 (v : any_τ2 any_Γ))]
+  [(where #t (different v v_2))
+   (:set any_Γ v_2 any_τ2 any_Γ2)
+   -----
+   (:set (v : any_τ any_Γ) v_2 any_τ2 (v : any_τ any_Γ2))]
+  [-----
+   (:set empty v any_τ (v : any_τ empty))])
+
+(define-metafunction list-machine-typing
+  dom : any -> (l ...)
+  [(dom (l_1 : any_1 any_2))
+   (l_1 l_2 ...)
+   (where (l_2 ...) (dom any_2))]
+  [(dom any) ()])
+
+(define-metafunction list-machine-typing
+  l-⊂ : (l ...) (l ...) -> any
+  [(l-⊂ (l_1 ...) (l_2 ...))
+   ,(let ([ht (make-hash)])
+      (for ([l (in-list (term (l_2 ...)))])
+        (hash-set! ht l #t))
+      (for/and ([l (in-list (term (l_1 ...)))])
+        (hash-ref ht l #f)))])
diff --git a/collects/redex/examples/list-machine/list-machine.rkt b/collects/redex/examples/list-machine/list-machine.rkt
new file mode 100644
index 0000000000..57d3fdcf46
--- /dev/null
+++ b/collects/redex/examples/list-machine/list-machine.rkt
@@ -0,0 +1,98 @@
+#lang racket
+(require redex)
+
+(provide list-machine red 
+         var-lookup var-set
+         program-lookup
+         different)
+
+(define-language list-machine
+  (a nil
+     (cons a a))
+  (v variable-not-otherwise-mentioned)
+  (r empty
+     (r v ↦ a))
+  (l variable-not-otherwise-mentioned)
+  (ι (jump l)
+     (branch-if-nil v l)
+     (fetch-field v 0 v)
+     (fetch-field v 1 v)
+     (cons v v v)
+     halt
+     (begin ι ι))
+  (p (l : ι p)
+     end))
+
+(define-judgment-form list-machine
+  #:contract (var-lookup r v a)
+  #:mode (var-lookup I I O)
+  [-----
+   (var-lookup (r v ↦ a) v a)]
+  [(where #t (different v_1 v_2))
+   (var-lookup r v_2 a_2)
+   -----
+   (var-lookup (r v_1 ↦ a_1) v_2 a_2)])
+
+(define-judgment-form list-machine
+  #:contract (var-set r v a r)
+  #:mode (var-set I I I O)
+  [-----
+   (var-set (r v ↦ a) v a_2 (r v ↦ a_2))]
+  [(where #t (different v v_2))
+   (var-set r v_2 a_2 r_2)
+   -----
+   (var-set (r v ↦ a) v_2 a_2 (r_2 v ↦ a))]
+  [-----
+   (var-set empty v a (empty v ↦ a))])
+
+(define-judgment-form list-machine
+  #:contract (program-lookup p l ι)
+  #:mode (program-lookup I I O)
+  [-----
+   (program-lookup (l : ι p) l ι)]
+  [(where #t (different l l_2))
+   (program-lookup p l_2 ι_2)
+   -----
+   (program-lookup (l : ι p) l_2 ι_2)])
+
+(define red 
+  (reduction-relation 
+   list-machine
+   #:domain (p r ι)
+   (--> (p r (begin (begin ι_1 ι_2) ι_3))
+        (p r (begin ι_1 (begin ι_2 ι_3)))
+        "step-seq")
+   (--> (p r (begin (fetch-field v 0 v_2) ι))
+        (p r_2 ι)
+        "step-fetch-field-0"
+        (judgment-holds (var-lookup r v (cons a_0 a_1)))
+        (judgment-holds (var-set r v_2 a_0 r_2)))
+   (--> (p r (begin (fetch-field v 1 v_2) ι))
+        (p r_2 ι)
+        "step-fetch-field-1"
+        (judgment-holds (var-lookup r v (cons a_0 a_1)))
+        (judgment-holds (var-set r v_2 a_1 r_2)))
+   (--> (p r (begin (cons v_0 v_1 v_2) ι))
+        (p r_2 ι)
+        "step-cons"
+        (judgment-holds (var-lookup r v_0 a_0))
+        (judgment-holds (var-lookup r v_1 a_1))
+        (judgment-holds (var-set r v_2 (cons a_0 a_1) r_2)))
+   (--> (p r (begin (branch-if-nil v l) ι))
+        (p r ι)
+        "step-branch-not-taken"
+        (judgment-holds (var-lookup r v (cons a_0 a_1))))
+   (--> (p r (begin (branch-if-nil v l) ι))
+        (p r ι_2)
+        "step-branch-taken"
+        (judgment-holds (var-lookup r v nil))
+        (judgment-holds (program-lookup p l ι_2)))
+   (--> (p r (jump l))
+        (p r ι_2)
+        "step-jump"
+        (judgment-holds (program-lookup p l ι_2)))))
+
+
+(define-metafunction list-machine
+  different : any any -> any
+  [(different any_1 any_2) ,(not (equal? (term any_1) (term any_2)))])
diff --git a/collects/redex/examples/list-machine/p-sample.rkt b/collects/redex/examples/list-machine/p-sample.rkt
new file mode 100644
index 0000000000..ebab2981ac
--- /dev/null
+++ b/collects/redex/examples/list-machine/p-sample.rkt
@@ -0,0 +1,38 @@
+#lang racket
+(require redex
+         "list-machine.rkt" 
+         "list-machine-typing.rkt")
+
+(define p-sample
+  (term (l0 : (begin (cons v0 v0 v1)
+                     (begin (cons v0 v1 v1)
+                            (begin (cons v0 v1 v1)
+                                   (jump l1))))
+            (l1 : (begin (branch-if-nil v1 l2)
+                         (begin (fetch-field v1 1 v1)
+                                (begin (branch-if-nil v0 l1)
+                                       (jump l2))))
+                (l2 : halt
+                    end)))))
+
+;; Eval : p -> r | 'crashed | 'multiple-results
+(define (Eval p)
+  (define l0 (car (judgment-holds (program-lookup ,p l0 ι) ι))) 
+  (define result (apply-reduction-relation* red (term (,p (empty v0 ↦ nil) ,l0))))
+  (cond
+    [(= 1 (length result))
+     (with-handlers ((exn:fail:redex? (λ (x) 'crashed)))
+       (redex-let list-machine
+                  ([(p r halt) (car result)])
+                  (term r)))]
+    [else 'multiple-results]))
+
+(Eval p-sample)
+
+(define Π-sample
+  (term (l0 : (v0 : nil empty)
+            (l1 : (v0 : nil (v1 : (list nil) empty))
+                (l2 : empty empty)))))
+
+(judgment-holds (check-program ,p-sample ,Π-sample))
+
diff --git a/collects/redex/examples/list-machine/slides.rkt b/collects/redex/examples/list-machine/slides.rkt
new file mode 100644
index 0000000000..2c9011f731
--- /dev/null
+++ b/collects/redex/examples/list-machine/slides.rkt
@@ -0,0 +1,85 @@
+#lang racket
+(require slideshow
+         redex
+         "list-machine.rkt"
+         "list-machine-typing.rkt")
+
+(define (with-rewriters t)
+  (define rewrite-lookup
+    (match-lambda
+      [(list op id r v a cp)
+       (list "" r "(" v ") = " a)]))
+  (define set-rewrite
+    (match-lambda
+      [(list op id r1 v a r2 cp)
+       (list "" r1 "[" v ":=" a "] = " r2)]))
+  (define subset-rewrite
+    (match-lambda
+      [(list op id left right cp)
+       (list "" left " ⊂ " right "")]))
+  (define (turn which subscr)
+    (hbl-append (text which (default-style) (default-font-size))
+                (text subscr (cons 'subscript (default-style)) (default-font-size))
+                (text " " (default-style) (default-font-size))))
+  (with-compound-rewriters
+   (['var-lookup rewrite-lookup]
+    ['var-set set-rewrite]
+    ['program-lookup rewrite-lookup]
+    [':lookup rewrite-lookup]
+    [':set set-rewrite]
+    ['check-program
+     (match-lambda 
+       [(list op id p Π cp)
+        (list (turn "⊨" "prog") p " : " Π)])]
+    ['check-blocks
+     (match-lambda
+       [(list op ip  Π p cp)
+        (list "" Π (turn "⊢" "blocks") p)])]
+    ['check-block
+     (match-lambda
+       [(list op id Π Γ ι cp)
+        (list "" Π ";" Γ (turn "⊢" "blocks") ι)])]
+    ['check-instr
+     (match-lambda
+       [(list op id Π Γ1 ι Γ2 cp)
+        (list "" Π (turn "⊢" "instr") Γ1 "{" ι "}" Γ2)])]
+    ['l-⊂ subset-rewrite]
+    ['Γ-⊂ subset-rewrite]
+    ['⊔ 
+     (match-lambda
+       [(list op id τ1 τ2 τ3 cp)
+        (list "" τ1 "⊔" τ2 " = " τ3)])]
+    ['dom
+     (λ (lws)
+       (define arg (list-ref lws 2))
+       (list "dom(" arg ")"))])
+   (t)))
+
+(define (scale-to-fit p)
+  (scale p (min (/ (- 1024 margin margin) (pict-width p))
+                (/ (- 768 margin margin) (pict-height p)))))
+
+(slide 
+ (with-rewriters
+  (λ ()
+    (scale-to-fit 
+     (ht-append
+      40
+      (language->pict list-machine #:nts '(a p ι))
+      (reduction-relation->pict red))))))
+
+(slide
+ (with-rewriters
+  (λ ()
+    (scale-to-fit
+     (judgment-form->pict check-instr)))))
+
+(slide
+ (with-rewriters
+  (λ ()
+    (scale-to-fit
+     (vc-append
+      40
+      (judgment-form->pict check-block)
+      (judgment-form->pict check-blocks)
+      (judgment-form->pict check-program))))))
diff --git a/collects/redex/examples/list-machine/test.rkt b/collects/redex/examples/list-machine/test.rkt
new file mode 100644
index 0000000000..d8cbf458f9
--- /dev/null
+++ b/collects/redex/examples/list-machine/test.rkt
@@ -0,0 +1,158 @@
+#lang racket
+(require "list-machine.rkt"
+         "list-machine-typing.rkt"
+         redex)
+
+(test-equal (judgment-holds (var-lookup (empty x ↦ nil) x a) a)
+            (list (term nil)))
+(test-equal (judgment-holds (var-lookup (empty x ↦ nil) y a) a)
+            (list))
+(test-equal (judgment-holds (var-lookup ((empty y ↦ (cons nil nil)) x ↦ nil) y a) a)
+            (list (term (cons nil nil))))
+
+(test-equal (judgment-holds (var-set empty x nil r) r)
+            (list (term (empty x ↦ nil))))
+(test-equal (judgment-holds (var-set (empty x ↦ nil) x (cons nil nil) r) r)
+            (list (term (empty x ↦ (cons nil nil)))))
+(test-equal (judgment-holds (var-set (empty x ↦ nil) y (cons nil nil) r) r)
+            (list (term ((empty y ↦ (cons nil nil)) x ↦ nil))))
+
+(test-equal (judgment-holds (program-lookup (l1 : halt end) l1 ι) ι)
+            (list (term halt)))
+(test-equal (judgment-holds (program-lookup (l1 : halt (l2 : (begin halt halt) end)) l2 ι) ι)
+            (list (term (begin halt halt))))
+
+(test--> red
+         (term (end empty (begin (begin (jump l1) (jump l2)) (jump l3))))
+         (term (end empty (begin (jump l1) (begin (jump l2) (jump l3))))))
+(test--> red
+         (term (end 
+                ((empty x ↦ (cons (cons nil nil) nil)) y ↦ nil)
+                (begin (fetch-field x 0 y) halt)))
+         (term (end 
+                ((empty x ↦ (cons (cons nil nil) nil)) y ↦ (cons nil nil))
+                halt)))
+(test--> red
+         (term (end 
+                ((empty x ↦ (cons nil (cons nil nil))) y ↦ nil)
+                (begin (fetch-field x 1 y) halt)))
+         (term (end 
+                ((empty x ↦ (cons nil (cons nil nil))) y ↦ (cons nil nil))
+                halt)))
+(test--> red
+         (term (end ((empty x ↦ nil) y ↦ nil) (begin (cons x y z) halt)))
+         (term (end (((empty z ↦ (cons nil nil)) x ↦ nil) y ↦ nil) halt)))
+(test--> red
+         (term (end (empty x ↦ (cons nil nil)) (begin (branch-if-nil x l) halt)))
+         (term (end (empty x ↦ (cons nil nil)) halt)))
+(test--> red
+         (term ((l : (begin halt halt) end) (empty x ↦ nil) (begin (branch-if-nil x l) halt)))
+         (term ((l : (begin halt halt) end) (empty x ↦ nil) (begin halt halt))))
+(test--> red
+         (term ((l : (begin halt halt) end) (empty x ↦ nil) (jump l)))
+         (term ((l : (begin halt halt) end) (empty x ↦ nil) (begin halt halt))))
+
+(test-equal (judgment-holds (:lookup (x : nil empty) x τ) τ)
+            (list (term nil)))
+(test-equal (judgment-holds (:lookup (x : nil empty) y τ) τ)
+            (list))
+(test-equal (judgment-holds (:lookup (x : nil (y : (list nil) empty)) y τ) τ)
+            (list (term (list nil))))
+
+(test-equal (judgment-holds (:set empty x nil Γ) Γ)
+            (list (term (x : nil empty))))
+(test-equal (judgment-holds (:set (x : nil empty) x (list nil) Γ) Γ)
+            (list (term (x : (list nil) empty))))
+(test-equal (judgment-holds (:set (x : nil empty) y (list nil) Γ) Γ)
+            (list (term (x : nil (y : (list nil) empty)))))
+
+(test-equal (judgment-holds (⊂ nil nil)) #t)
+(test-equal (judgment-holds (⊂ nil (list nil))) #t)
+(test-equal (judgment-holds (⊂ (list nil) (list (list nil)))) #t)
+(test-equal (judgment-holds (⊂ (listcons nil) (list (list nil)))) #t)
+(test-equal (judgment-holds (⊂ (listcons nil) (listcons (list nil)))) #t)
+
+(redex-check
+ list-machine-typing
+ τ
+ (for* ([τ_1 (in-list (judgment-holds (⊂ τ_1 τ) τ_1))]
+        [τ_2 (in-list (judgment-holds (⊂ τ_2 τ) τ_2))])
+   (for/and ([τ_3 (judgment-holds (⊔ ,τ_1 ,τ_2 τ_3) τ_3)])
+     (judgment-holds (⊂ τ_3 τ))))
+ #:attempts 100)
+
+(test-equal (judgment-holds (Γ-⊂ (x : nil empty) (x : nil empty)))
+            #t)
+(test-equal (judgment-holds (Γ-⊂ (x : nil empty) (x : (list nil) empty)))
+            #t)
+(test-equal (judgment-holds (Γ-⊂ (x : nil (y : (list nil) empty)) (x : (list nil) empty)))
+            #t)
+(test-equal (judgment-holds (Γ-⊂ (y : (list nil) (x : nil empty)) (x : (list nil) empty)))
+            #t)
+
+(test-equal (judgment-holds (check-instr (l0 : (x : (list nil) empty) empty)
+                                         (x : (list nil) empty)
+                                         (branch-if-nil x l0)
+                                         Γ)
+                            Γ)
+            (list (term (x : (listcons nil) empty))))
+(test-equal (judgment-holds (check-instr (l0 : (x : nil empty) empty)
+                                         (x : (listcons nil) empty)
+                                         (branch-if-nil x l0)
+                                         Γ)
+                            Γ)
+            (list (term (x : (listcons nil) empty))))
+(test-equal (judgment-holds (check-instr (l0 : (x : nil empty) empty)
+                                         (x : nil empty)
+                                         (branch-if-nil x l0)
+                                         Γ)
+                            Γ)
+            (list (term (x : nil empty))))
+
+(test-equal (judgment-holds (check-instr empty
+                                         (x : (listcons nil) empty)
+                                         (fetch-field x 0 y)
+                                         Γ)
+                            Γ)
+            (list (term (x : (listcons nil) (y : nil empty)))))
+(test-equal (judgment-holds (check-instr empty
+                                         (x : (listcons nil) empty)
+                                         (fetch-field x 1 y)
+                                         Γ)
+                            Γ)
+            (list (term (x : (listcons nil) (y : (list nil) empty)))))
+(test-equal (judgment-holds (check-instr empty
+                                         (x : (listcons nil) 
+                                            (y : (list (list nil)) 
+                                               (z : nil empty)))
+                                         (cons x y z)
+                                         Γ)
+                            Γ)
+            (list (term (x : (listcons nil) 
+                           (y : (list (list nil)) 
+                              (z : (listcons (list nil))
+                                 empty))))))
+
+(test-equal (judgment-holds (check-block empty empty halt)) #t)
+(test-equal (judgment-holds (check-block empty
+                                         (x : (listcons nil) empty)
+                                         (begin (fetch-field x 0 y) halt)))
+            #t)
+(test-equal (judgment-holds (check-block (l0 : empty empty)
+                                         (x : nil empty)
+                                         (jump l0)))
+            #t)
+(test-equal (judgment-holds (check-blocks empty end)) #t)
+(test-equal (judgment-holds (check-blocks (l0 : empty empty) (l0 : halt end))) #t)
+(test-equal (judgment-holds (check-program (l0 : halt end) (l0 : (v0 : nil empty) empty)))
+            #t)
+
+(test-equal (term (dom (l0 : halt (l1 : halt end))))
+            (term (l0 l1)))
+(test-equal (term (dom (l0 : empty (l2 : empty end))))
+            (term (l0 l2)))
+(test-equal (term (l-⊂ (l0 l1 l2) (l2 l3 l0 l1 l11)))
+            #t)
+(test-equal (term (l-⊂ (l0 l1 l2 l33) (l2 l3 l0 l1 l11)))
+            #f)
+(test-results)