From 2d425075153de2f8d2fb2a890df8295293d7a422 Mon Sep 17 00:00:00 2001
From: Robby Findler <robby@racket-lang.org>
Date: Tue, 18 Mar 2014 22:35:48 -0500
Subject: [PATCH] new slate of stlc-sub bugs

---
 .../redex/examples/benchmark/stlc-sub/1.diff  |  21 +-
 .../redex/examples/benchmark/stlc-sub/2.diff  |   2 +-
 .../redex/examples/benchmark/stlc-sub/3.diff  |  20 +-
 .../redex/examples/benchmark/stlc-sub/4.diff  |   2 +-
 .../redex/examples/benchmark/stlc-sub/5.diff  |   9 +-
 .../redex/examples/benchmark/stlc-sub/6.diff  |   8 -
 .../redex/examples/benchmark/stlc-sub/7.diff  |  16 -
 .../redex/examples/benchmark/stlc-sub/8.diff  |   8 -
 .../redex/examples/benchmark/stlc-sub/9.diff  |   8 -
 .../benchmark/stlc-sub/stlc-sub-1.rkt         |  23 +-
 .../benchmark/stlc-sub/stlc-sub-2.rkt         |  18 +-
 .../benchmark/stlc-sub/stlc-sub-3.rkt         |  25 +-
 .../benchmark/stlc-sub/stlc-sub-4.rkt         |  18 +-
 .../benchmark/stlc-sub/stlc-sub-5.rkt         |  18 +-
 .../benchmark/stlc-sub/stlc-sub-6.rkt         | 325 -----------------
 .../benchmark/stlc-sub/stlc-sub-7.rkt         | 326 ------------------
 .../benchmark/stlc-sub/stlc-sub-8.rkt         | 325 -----------------
 .../benchmark/stlc-sub/stlc-sub-9.rkt         | 325 -----------------
 18 files changed, 58 insertions(+), 1439 deletions(-)
 delete mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/6.diff
 delete mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/7.diff
 delete mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/8.diff
 delete mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/9.diff
 delete mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt
 delete mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt
 delete mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt
 delete mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt

diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/1.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/1.diff
index 44da271767..fa4c87b271 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/1.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/1.diff
@@ -1,18 +1,7 @@
-3,4d2
+3c3
 < (define the-error "no error")
-< 
-7d4
-<          racket/match
-8a6
->          racket/match
-12a11,12
-> (define the-error "the order of the variable clauses is swapped")
-> 
+---
+> (define the-error "forgot the variable case")
 106,107d105
-<   [(subst x x M)
-<    M]
-109a108,109
->   [(subst x x M)
->    M]
-257a258
-> 
+<   [(subst x x v)
+<    v]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff
index 06a203de02..dc826fa6aa 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff
@@ -2,7 +2,7 @@
 < (define the-error "no error")
 ---
 > (define the-error "wrong order of arguments to replace call")
-113c113
+111c111
 <    (λ (x_new τ) (subst (replace M x_1 x_new) x_2 v))
 ---
 >    (λ (x_new τ) (subst (replace M x_new x_1) x_2 v))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/3.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/3.diff
index a98a344fa5..feb5a7b227 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/3.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/3.diff
@@ -1,16 +1,8 @@
-3,4d2
+3c3
 < (define the-error "no error")
-< 
-7d4
-<          racket/match
-8a6
->          racket/match
-12a11,12
-> (define the-error "substitutes rator into rand in application")
-> 
-119c119
-<    ((subst M x M_x) (subst N x M_x))]
 ---
->    ((subst M x M_x) (subst N x M))]
-257a258
-> 
+> (define the-error "swaps function and argument position in application")
+115c115
+<    ((subst M x v) (subst N x v))]
+---
+>    ((subst N x v) (subst M x v))]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/4.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/4.diff
index 30c87f897d..e388ce9f54 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/4.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/4.diff
@@ -2,7 +2,7 @@
 < (define the-error "no error")
 ---
 > (define the-error "variable not fresh enough")
-114c114
+112c112
 <    (where x_new ,(variable-not-in (term (x_1 e x_2))
 ---
 >    (where x_new ,(variable-not-in (term e)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/5.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/5.diff
index fb34398671..71f437d907 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/5.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/5.diff
@@ -1,7 +1,8 @@
 3c3
 < (define the-error "no error")
 ---
-> (define the-error "forget to do the replacement")
-108,109d107
-<   [(subst y x M)
-<    y]
+> (define the-error "replace all variables")
+106c106
+<   [(subst x x v)
+---
+>   [(subst x y v)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/6.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/6.diff
deleted file mode 100644
index 7760b87458..0000000000
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/6.diff
+++ /dev/null
@@ -1,8 +0,0 @@
-3c3
-< (define the-error "no error")
----
-> (define the-error "accidentally use the same metavariable name twice")
-110c110
-<   [(subst (λ (x τ) M) x M_x)
----
->   [(subst (λ (x τ) M) x M)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/7.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/7.diff
deleted file mode 100644
index ad0dc5a74c..0000000000
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/7.diff
+++ /dev/null
@@ -1,16 +0,0 @@
-3,4d2
-< (define the-error "no error")
-< 
-7d4
-<          racket/match
-8a6
->          racket/match
-12a11,12
-> (define the-error "swaps to/from expressions when recurring inside a constant")
-> 
-117c117
-<    (c (subst M x M_x))]
----
->    (c (subst M_x x M))]
-257a258
-> 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/8.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/8.diff
deleted file mode 100644
index 6f4fa28c21..0000000000
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/8.diff
+++ /dev/null
@@ -1,8 +0,0 @@
-3c3
-< (define the-error "no error")
----
-> (define the-error "replace all variables, not just substituted one")
-109c109
-<    y]
----
->    x]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/9.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/9.diff
deleted file mode 100644
index b9197822bd..0000000000
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/9.diff
+++ /dev/null
@@ -1,8 +0,0 @@
-3c3
-< (define the-error "no error")
----
-> (define the-error "swaps to/from expressions when recurring in the rhs of app")
-119c119
-<    ((subst M x M_x) (subst N x M_x))]
----
->    ((subst M_x x M) (subst N x M_x))]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt
index 3a892787d4..095335de8f 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt
@@ -1,15 +1,15 @@
 #lang racket/base
 
+(define the-error "forgot the variable case")
+
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
          racket/match
+         racket/list
          racket/contract
          racket/bool)
 
 (provide (all-defined-out))
-(define the-error "the order of the variable clauses is swapped")
-
 
 (define-language stlc
   (M N ::= 
@@ -102,22 +102,16 @@
         "+")))
 
 (define-metafunction stlc
-  subst : M x M -> M
-  [(subst y x M)
-   y]
-  [(subst x x M)
-   M]
-  [(subst (λ (x τ) M) x M_x)
+  subst : M x v -> M
+  [(subst (λ (x τ) M) x v)
    (λ (x τ) M)]
   [(subst (λ (x_1 τ) M) x_2 v)
    (λ (x_new τ) (subst (replace M x_1 x_new) x_2 v))
    (where x_new ,(variable-not-in (term (x_1 e x_2))
                                   (term x_1)))]
-  [(subst (c M) x M_x)
-   (c (subst M x M_x))]
-  [(subst (M N) x M_x)
-   ((subst M x M_x) (subst N x M_x))]
-  [(subst M x M_x)
+  [(subst (M N) x v)
+   ((subst M x v) (subst N x v))]
+  [(subst M x v)
    M])
 
 (define-metafunction stlc
@@ -255,7 +249,6 @@
        (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
   (match candidate
     [`(typeof • ,M ,τ)
-
      M]
     [#f #f]))
 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt
index 1541ffc2ae..92ef8c978d 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt
@@ -102,22 +102,18 @@
         "+")))
 
 (define-metafunction stlc
-  subst : M x M -> M
-  [(subst x x M)
-   M]
-  [(subst y x M)
-   y]
-  [(subst (λ (x τ) M) x M_x)
+  subst : M x v -> M
+  [(subst x x v)
+   v]
+  [(subst (λ (x τ) M) x v)
    (λ (x τ) M)]
   [(subst (λ (x_1 τ) M) x_2 v)
    (λ (x_new τ) (subst (replace M x_new x_1) x_2 v))
    (where x_new ,(variable-not-in (term (x_1 e x_2))
                                   (term x_1)))]
-  [(subst (c M) x M_x)
-   (c (subst M x M_x))]
-  [(subst (M N) x M_x)
-   ((subst M x M_x) (subst N x M_x))]
-  [(subst M x M_x)
+  [(subst (M N) x v)
+   ((subst M x v) (subst N x v))]
+  [(subst M x v)
    M])
 
 (define-metafunction stlc
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt
index 8e64003d7c..9642f34467 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt
@@ -1,15 +1,15 @@
 #lang racket/base
 
+(define the-error "swaps function and argument position in application")
+
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
          racket/match
+         racket/list
          racket/contract
          racket/bool)
 
 (provide (all-defined-out))
-(define the-error "substitutes rator into rand in application")
-
 
 (define-language stlc
   (M N ::= 
@@ -102,22 +102,18 @@
         "+")))
 
 (define-metafunction stlc
-  subst : M x M -> M
-  [(subst x x M)
-   M]
-  [(subst y x M)
-   y]
-  [(subst (λ (x τ) M) x M_x)
+  subst : M x v -> M
+  [(subst x x v)
+   v]
+  [(subst (λ (x τ) M) x v)
    (λ (x τ) M)]
   [(subst (λ (x_1 τ) M) x_2 v)
    (λ (x_new τ) (subst (replace M x_1 x_new) x_2 v))
    (where x_new ,(variable-not-in (term (x_1 e x_2))
                                   (term x_1)))]
-  [(subst (c M) x M_x)
-   (c (subst M x M_x))]
-  [(subst (M N) x M_x)
-   ((subst M x M_x) (subst N x M))]
-  [(subst M x M_x)
+  [(subst (M N) x v)
+   ((subst N x v) (subst M x v))]
+  [(subst M x v)
    M])
 
 (define-metafunction stlc
@@ -255,7 +251,6 @@
        (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
   (match candidate
     [`(typeof • ,M ,τ)
-
      M]
     [#f #f]))
 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt
index 62017f9703..39f6af665e 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt
@@ -102,22 +102,18 @@
         "+")))
 
 (define-metafunction stlc
-  subst : M x M -> M
-  [(subst x x M)
-   M]
-  [(subst y x M)
-   y]
-  [(subst (λ (x τ) M) x M_x)
+  subst : M x v -> M
+  [(subst x x v)
+   v]
+  [(subst (λ (x τ) M) x v)
    (λ (x τ) M)]
   [(subst (λ (x_1 τ) M) x_2 v)
    (λ (x_new τ) (subst (replace M x_1 x_new) x_2 v))
    (where x_new ,(variable-not-in (term e)
                                   (term x_1)))]
-  [(subst (c M) x M_x)
-   (c (subst M x M_x))]
-  [(subst (M N) x M_x)
-   ((subst M x M_x) (subst N x M_x))]
-  [(subst M x M_x)
+  [(subst (M N) x v)
+   ((subst M x v) (subst N x v))]
+  [(subst M x v)
    M])
 
 (define-metafunction stlc
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt
index e814e54c6f..b400ebe6c5 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt
@@ -1,6 +1,6 @@
 #lang racket/base
 
-(define the-error "forget to do the replacement")
+(define the-error "replace all variables")
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
@@ -102,20 +102,18 @@
         "+")))
 
 (define-metafunction stlc
-  subst : M x M -> M
-  [(subst x x M)
-   M]
-  [(subst (λ (x τ) M) x M_x)
+  subst : M x v -> M
+  [(subst x y v)
+   v]
+  [(subst (λ (x τ) M) x v)
    (λ (x τ) M)]
   [(subst (λ (x_1 τ) M) x_2 v)
    (λ (x_new τ) (subst (replace M x_1 x_new) x_2 v))
    (where x_new ,(variable-not-in (term (x_1 e x_2))
                                   (term x_1)))]
-  [(subst (c M) x M_x)
-   (c (subst M x M_x))]
-  [(subst (M N) x M_x)
-   ((subst M x M_x) (subst N x M_x))]
-  [(subst M x M_x)
+  [(subst (M N) x v)
+   ((subst M x v) (subst N x v))]
+  [(subst M x v)
    M])
 
 (define-metafunction stlc
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt
deleted file mode 100644
index 6689433302..0000000000
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt
+++ /dev/null
@@ -1,325 +0,0 @@
-#lang racket/base
-
-(define the-error "accidentally use the same metavariable name twice")
-
-(require redex/reduction-semantics
-         (only-in redex/private/generate-term pick-an-index)
-         racket/match
-         racket/list
-         racket/contract
-         racket/bool)
-
-(provide (all-defined-out))
-
-(define-language stlc
-  (M N ::= 
-     (λ (x σ) M)
-     (M N)
-     x
-     c)
-  (Γ (x σ Γ)
-     •)
-  (σ τ ::=
-     int
-     (list int)
-     (σ → τ))
-  (c d ::= cons nil hd tl + integer)
-  ((x y) variable-not-otherwise-mentioned)
-  
-  (v (λ (x τ) M)
-     c
-     (cons v)
-     ((cons v) v)
-     (+ v))
-  (E hole
-     (E M)
-     (v E)))
-
-(define-judgment-form stlc
-  #:mode (typeof I I O)
-  #:contract (typeof Γ M σ)
-  
-  [---------------------------
-   (typeof Γ c (const-type c))]
-  
-  [(where τ (lookup Γ x))
-   ----------------------
-   (typeof Γ x τ)]
-  
-  [(typeof (x σ Γ) M σ_2)
-   --------------------------------
-   (typeof Γ (λ (x σ) M) (σ → σ_2))]
-  
-  [(typeof Γ M (σ → σ_2))
-   (typeof Γ M_2 σ)
-   ----------------------
-   (typeof Γ (M M_2) σ_2)])
-
-(define-metafunction stlc
-  const-type : c -> σ
-  [(const-type nil)
-   (list int)]
-  [(const-type cons)
-   (int → ((list int) → (list int)))]
-  [(const-type hd)
-   ((list int) → int)]
-  [(const-type tl)
-   ((list int) → (list int))]
-  [(const-type +)
-   (int → (int → int))]
-  [(const-type integer)
-   int])
-
-(define-metafunction stlc
-  lookup : Γ x -> σ or #f
-  [(lookup (x σ Γ) x)
-   σ]
-  [(lookup (x σ Γ) x_2)
-   (lookup Γ x_2)]
-  [(lookup • x)
-   #f])
-
-(define red
-  (reduction-relation
-   stlc
-   (--> (in-hole E ((λ (x τ) M) v))
-        (in-hole E (subst M x v))
-        "βv")
-   (--> (in-hole E (hd ((cons v_1) v_2)))
-        (in-hole E v_1)
-        "hd")
-   (--> (in-hole E (tl ((cons v_1) v_2)))
-        (in-hole E v_2)
-        "tl")
-   (--> (in-hole E (hd nil))
-        "error"
-        "hd-err")
-   (--> (in-hole E (tl nil))
-        "error"
-        "tl-err")
-   (--> (in-hole E ((+ integer_1) integer_2))
-        (in-hole E ,(+ (term integer_1) (term integer_2)))
-        "+")))
-
-(define-metafunction stlc
-  subst : M x M -> M
-  [(subst x x M)
-   M]
-  [(subst y x M)
-   y]
-  [(subst (λ (x τ) M) x M)
-   (λ (x τ) M)]
-  [(subst (λ (x_1 τ) M) x_2 v)
-   (λ (x_new τ) (subst (replace M x_1 x_new) x_2 v))
-   (where x_new ,(variable-not-in (term (x_1 e x_2))
-                                  (term x_1)))]
-  [(subst (c M) x M_x)
-   (c (subst M x M_x))]
-  [(subst (M N) x M_x)
-   ((subst M x M_x) (subst N x M_x))]
-  [(subst M x M_x)
-   M])
-
-(define-metafunction stlc
-  [(replace (any_1 ...) x_1 x_new)
-   ((replace any_1 x_1 x_new) ...)]
-  [(replace x_1 x_1 x_new)
-   x_new]
-  [(replace any_1 x_1 x_new)
-   any_1])
-
-(define M? (redex-match stlc M))
-(define/contract (Eval M)
-  (-> M? (or/c M? "error"))
-  (define M-t (judgment-holds (typeof • ,M τ) τ))
-  (unless (pair? M-t)
-    (error 'Eval "doesn't typecheck: ~s" M))
-  (define res (apply-reduction-relation* red M))
-  (unless (= 1 (length res))
-    (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
-  (define ans (car res))
-  (if (equal? "error" ans)
-      "error"
-      (let ([ans-t (judgment-holds (typeof • ,ans τ) τ)])
-        (unless (equal? M-t ans-t)
-          (error 'Eval "internal error: type soundness fails for ~s" M))
-        ans)))
-
-(define x? (redex-match stlc x))
-
-(define v? (redex-match? stlc v))
-(define τ? (redex-match? stlc τ))
-(define/contract (type-check M)
-  (-> M? (or/c τ? #f))
-  (define M-t (judgment-holds (typeof • ,M τ) τ))
-  (cond
-    [(empty? M-t)
-     #f]
-    [(null? (cdr M-t))
-     (car M-t)]
-    [else
-     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
-
-(test-equal (type-check (term 5))
-            (term int))
-(test-equal (type-check (term (5 5)))
-            #f)
-
-(define (progress-holds? M)
-  (if (type-check M)
-      (or (v? M)
-          (not (null? (apply-reduction-relation red (term ,M)))))
-      #t))
-
-(define (interesting-term? M)
-  (and (type-check M)
-       (term (uses-bound-var? () ,M))))
-
-(define-metafunction stlc
-  [(uses-bound-var? (x_0 ... x_1 x_2 ...) x_1)
-   #t]
-  [(uses-bound-var? (x_0 ...) (λ (x τ) M))
-   (uses-bound-var? (x x_0 ...) M)]
-  [(uses-bound-var? (x ...) (M N))
-   ,(or (term (uses-bound-var? (x ...) M))
-        (term (uses-bound-var? (x ...) N)))]
-  [(uses-bound-var? (x ...) (cons M))
-   (uses-bound-var? (x ...) M)]
-  [(uses-bound-var? (x ...) any)
-   #f])
-
-(define (really-interesting-term? M)
-  (and (interesting-term? M)
-       (term (applies-bv? () ,M))))
-
-(define-metafunction stlc
-  [(applies-bv? (x_0 ... x_1 x_2 ...) (x_1 M))
-   #t]
-  [(applies-bv? (x_0 ...) (λ (x τ) M))
-   (applies-bv? (x x_0 ...) M)]
-  [(applies-bv? (x ...) (M N))
-   ,(or (term (applies-bv? (x ...) M))
-        (term (applies-bv? (x ...) N)))]
-  [(applies-bv? (x ...) (cons M))
-   (applies-bv? (x ...) M)]
-  [(applies-bv? (x ...) any)
-   #f])
-
-(define (reduction-step-count/func red v?)
-  (λ (term)
-    (let loop ([t term]
-               [n 0])
-      (define res (apply-reduction-relation red t))
-      (cond 
-        [(and (empty? res)
-              (v? t))
-         n]
-        [(and (empty? res)
-              (equal? t "error"))
-         n]
-        [(= (length res) 1)
-         (loop (car res) (add1 n))]
-        [else
-         (error 'reduction-step-count "failed reduction: ~s\n~s\n~s" term t res)]))))
-
-(define reduction-step-count
-  (reduction-step-count/func red v?))
-
-(define (generate-M-term)
-  (generate-term stlc M 5))
-
-(define (generate-M-term-from-red)
-  (generate-term #:source red 5))
-
-(define (generate-typed-term)
-  (match (generate-term stlc 
-                        #:satisfying
-                        (typeof • M τ)
-                        5)
-    [`(typeof • ,M ,τ)
-     M]
-    [#f #f]))
-
-(define (generate-typed-term-from-red)
-  (define candidate
-    (case (random 5)
-      [(0)
-       (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-      [(1)
-       (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-      [(2)
-       (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-      [(3)
-       (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-      [(4)
-       (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
-  (match candidate
-    [`(typeof • ,M ,τ)
-     M]
-    [#f #f]))
-
-(define (typed-generator)
-  (let ([g (redex-generator stlc 
-                            (typeof • M τ)
-                            5)])
-    (λ () 
-      (match (g)
-        [`(typeof • ,M ,τ)
-         M]
-        [#f #f]))))
-
-;; check : (or/c #f term) -> boolean[#f = counterexample found!]
-(define (check term)
-  (or (not term)
-      (v? term)
-      (let ([t-type (type-check term)])
-        (implies
-         t-type
-         (let ([red-res (apply-reduction-relation red term)])
-           (and (= (length red-res) 1)
-                (let ([red-t (car red-res)])
-                  (or (equal? red-t "error")
-                      (let ([red-type (type-check red-t)])
-                        (equal? t-type red-type))))))))))
-
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.0001)))
-
-(define (ordered-enum-generator)
-  (let ([index 0])
-    (λ ()
-      (begin0
-        (generate-term stlc M #:i-th index)
-        (set! index (add1 index))))))
-
-(define fixed
-  (term
-   (;; 1
-    ((λ (x int) x) 1)
-
-    ;; 9
-    ((λ (x (list int)) (tl x)) ((cons 1) nil))
-
-    ;; 2 -- xxx I don't think this is really an error because the (M
-    ;; N) case does everything that (c M) does since M can equal
-    ;; c. Otherwise the previous test case would work, because (tl x)
-    ;; would not be subst'd and it has no type
-
-    ;; 3
-    ((λ (x int) ((λ (y int) y) x)) 1)
-
-    ;; 4 -- xxx I don't think this is really an error because the
-    ;; normal λ rule always does renaming so this test below works
-    ;; fine and ends up with x1 in both places.
-
-    #;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
-
-    ;; 5 & 6 --- xxx These diffs are bogus because they don't actually
-    ;; make a change to any of the program.
-
-    ;; 7
-    ((λ (x int) (hd ((cons x) nil))) 1)
-
-    ;; 8 -- xxx This isn't an error for the same reason 4 isn't.
-    
-    )))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt
deleted file mode 100644
index b917b75b3c..0000000000
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt
+++ /dev/null
@@ -1,326 +0,0 @@
-#lang racket/base
-
-(require redex/reduction-semantics
-         (only-in redex/private/generate-term pick-an-index)
-         racket/list
-         racket/match
-         racket/contract
-         racket/bool)
-
-(provide (all-defined-out))
-(define the-error "swaps to/from expressions when recurring inside a constant")
-
-
-(define-language stlc
-  (M N ::= 
-     (λ (x σ) M)
-     (M N)
-     x
-     c)
-  (Γ (x σ Γ)
-     •)
-  (σ τ ::=
-     int
-     (list int)
-     (σ → τ))
-  (c d ::= cons nil hd tl + integer)
-  ((x y) variable-not-otherwise-mentioned)
-  
-  (v (λ (x τ) M)
-     c
-     (cons v)
-     ((cons v) v)
-     (+ v))
-  (E hole
-     (E M)
-     (v E)))
-
-(define-judgment-form stlc
-  #:mode (typeof I I O)
-  #:contract (typeof Γ M σ)
-  
-  [---------------------------
-   (typeof Γ c (const-type c))]
-  
-  [(where τ (lookup Γ x))
-   ----------------------
-   (typeof Γ x τ)]
-  
-  [(typeof (x σ Γ) M σ_2)
-   --------------------------------
-   (typeof Γ (λ (x σ) M) (σ → σ_2))]
-  
-  [(typeof Γ M (σ → σ_2))
-   (typeof Γ M_2 σ)
-   ----------------------
-   (typeof Γ (M M_2) σ_2)])
-
-(define-metafunction stlc
-  const-type : c -> σ
-  [(const-type nil)
-   (list int)]
-  [(const-type cons)
-   (int → ((list int) → (list int)))]
-  [(const-type hd)
-   ((list int) → int)]
-  [(const-type tl)
-   ((list int) → (list int))]
-  [(const-type +)
-   (int → (int → int))]
-  [(const-type integer)
-   int])
-
-(define-metafunction stlc
-  lookup : Γ x -> σ or #f
-  [(lookup (x σ Γ) x)
-   σ]
-  [(lookup (x σ Γ) x_2)
-   (lookup Γ x_2)]
-  [(lookup • x)
-   #f])
-
-(define red
-  (reduction-relation
-   stlc
-   (--> (in-hole E ((λ (x τ) M) v))
-        (in-hole E (subst M x v))
-        "βv")
-   (--> (in-hole E (hd ((cons v_1) v_2)))
-        (in-hole E v_1)
-        "hd")
-   (--> (in-hole E (tl ((cons v_1) v_2)))
-        (in-hole E v_2)
-        "tl")
-   (--> (in-hole E (hd nil))
-        "error"
-        "hd-err")
-   (--> (in-hole E (tl nil))
-        "error"
-        "tl-err")
-   (--> (in-hole E ((+ integer_1) integer_2))
-        (in-hole E ,(+ (term integer_1) (term integer_2)))
-        "+")))
-
-(define-metafunction stlc
-  subst : M x M -> M
-  [(subst x x M)
-   M]
-  [(subst y x M)
-   y]
-  [(subst (λ (x τ) M) x M_x)
-   (λ (x τ) M)]
-  [(subst (λ (x_1 τ) M) x_2 v)
-   (λ (x_new τ) (subst (replace M x_1 x_new) x_2 v))
-   (where x_new ,(variable-not-in (term (x_1 e x_2))
-                                  (term x_1)))]
-  [(subst (c M) x M_x)
-   (c (subst M_x x M))]
-  [(subst (M N) x M_x)
-   ((subst M x M_x) (subst N x M_x))]
-  [(subst M x M_x)
-   M])
-
-(define-metafunction stlc
-  [(replace (any_1 ...) x_1 x_new)
-   ((replace any_1 x_1 x_new) ...)]
-  [(replace x_1 x_1 x_new)
-   x_new]
-  [(replace any_1 x_1 x_new)
-   any_1])
-
-(define M? (redex-match stlc M))
-(define/contract (Eval M)
-  (-> M? (or/c M? "error"))
-  (define M-t (judgment-holds (typeof • ,M τ) τ))
-  (unless (pair? M-t)
-    (error 'Eval "doesn't typecheck: ~s" M))
-  (define res (apply-reduction-relation* red M))
-  (unless (= 1 (length res))
-    (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
-  (define ans (car res))
-  (if (equal? "error" ans)
-      "error"
-      (let ([ans-t (judgment-holds (typeof • ,ans τ) τ)])
-        (unless (equal? M-t ans-t)
-          (error 'Eval "internal error: type soundness fails for ~s" M))
-        ans)))
-
-(define x? (redex-match stlc x))
-
-(define v? (redex-match? stlc v))
-(define τ? (redex-match? stlc τ))
-(define/contract (type-check M)
-  (-> M? (or/c τ? #f))
-  (define M-t (judgment-holds (typeof • ,M τ) τ))
-  (cond
-    [(empty? M-t)
-     #f]
-    [(null? (cdr M-t))
-     (car M-t)]
-    [else
-     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
-
-(test-equal (type-check (term 5))
-            (term int))
-(test-equal (type-check (term (5 5)))
-            #f)
-
-(define (progress-holds? M)
-  (if (type-check M)
-      (or (v? M)
-          (not (null? (apply-reduction-relation red (term ,M)))))
-      #t))
-
-(define (interesting-term? M)
-  (and (type-check M)
-       (term (uses-bound-var? () ,M))))
-
-(define-metafunction stlc
-  [(uses-bound-var? (x_0 ... x_1 x_2 ...) x_1)
-   #t]
-  [(uses-bound-var? (x_0 ...) (λ (x τ) M))
-   (uses-bound-var? (x x_0 ...) M)]
-  [(uses-bound-var? (x ...) (M N))
-   ,(or (term (uses-bound-var? (x ...) M))
-        (term (uses-bound-var? (x ...) N)))]
-  [(uses-bound-var? (x ...) (cons M))
-   (uses-bound-var? (x ...) M)]
-  [(uses-bound-var? (x ...) any)
-   #f])
-
-(define (really-interesting-term? M)
-  (and (interesting-term? M)
-       (term (applies-bv? () ,M))))
-
-(define-metafunction stlc
-  [(applies-bv? (x_0 ... x_1 x_2 ...) (x_1 M))
-   #t]
-  [(applies-bv? (x_0 ...) (λ (x τ) M))
-   (applies-bv? (x x_0 ...) M)]
-  [(applies-bv? (x ...) (M N))
-   ,(or (term (applies-bv? (x ...) M))
-        (term (applies-bv? (x ...) N)))]
-  [(applies-bv? (x ...) (cons M))
-   (applies-bv? (x ...) M)]
-  [(applies-bv? (x ...) any)
-   #f])
-
-(define (reduction-step-count/func red v?)
-  (λ (term)
-    (let loop ([t term]
-               [n 0])
-      (define res (apply-reduction-relation red t))
-      (cond 
-        [(and (empty? res)
-              (v? t))
-         n]
-        [(and (empty? res)
-              (equal? t "error"))
-         n]
-        [(= (length res) 1)
-         (loop (car res) (add1 n))]
-        [else
-         (error 'reduction-step-count "failed reduction: ~s\n~s\n~s" term t res)]))))
-
-(define reduction-step-count
-  (reduction-step-count/func red v?))
-
-(define (generate-M-term)
-  (generate-term stlc M 5))
-
-(define (generate-M-term-from-red)
-  (generate-term #:source red 5))
-
-(define (generate-typed-term)
-  (match (generate-term stlc 
-                        #:satisfying
-                        (typeof • M τ)
-                        5)
-    [`(typeof • ,M ,τ)
-     M]
-    [#f #f]))
-
-(define (generate-typed-term-from-red)
-  (define candidate
-    (case (random 5)
-      [(0)
-       (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-      [(1)
-       (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-      [(2)
-       (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-      [(3)
-       (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-      [(4)
-       (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
-  (match candidate
-    [`(typeof • ,M ,τ)
-
-     M]
-    [#f #f]))
-
-(define (typed-generator)
-  (let ([g (redex-generator stlc 
-                            (typeof • M τ)
-                            5)])
-    (λ () 
-      (match (g)
-        [`(typeof • ,M ,τ)
-         M]
-        [#f #f]))))
-
-;; check : (or/c #f term) -> boolean[#f = counterexample found!]
-(define (check term)
-  (or (not term)
-      (v? term)
-      (let ([t-type (type-check term)])
-        (implies
-         t-type
-         (let ([red-res (apply-reduction-relation red term)])
-           (and (= (length red-res) 1)
-                (let ([red-t (car red-res)])
-                  (or (equal? red-t "error")
-                      (let ([red-type (type-check red-t)])
-                        (equal? t-type red-type))))))))))
-
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.0001)))
-
-(define (ordered-enum-generator)
-  (let ([index 0])
-    (λ ()
-      (begin0
-        (generate-term stlc M #:i-th index)
-        (set! index (add1 index))))))
-
-(define fixed
-  (term
-   (;; 1
-    ((λ (x int) x) 1)
-
-    ;; 9
-    ((λ (x (list int)) (tl x)) ((cons 1) nil))
-
-    ;; 2 -- xxx I don't think this is really an error because the (M
-    ;; N) case does everything that (c M) does since M can equal
-    ;; c. Otherwise the previous test case would work, because (tl x)
-    ;; would not be subst'd and it has no type
-
-    ;; 3
-    ((λ (x int) ((λ (y int) y) x)) 1)
-
-    ;; 4 -- xxx I don't think this is really an error because the
-    ;; normal λ rule always does renaming so this test below works
-    ;; fine and ends up with x1 in both places.
-
-    #;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
-
-    ;; 5 & 6 --- xxx These diffs are bogus because they don't actually
-    ;; make a change to any of the program.
-
-    ;; 7
-    ((λ (x int) (hd ((cons x) nil))) 1)
-
-    ;; 8 -- xxx This isn't an error for the same reason 4 isn't.
-    
-    )))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt
deleted file mode 100644
index 4ed5aeab63..0000000000
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt
+++ /dev/null
@@ -1,325 +0,0 @@
-#lang racket/base
-
-(define the-error "replace all variables, not just substituted one")
-
-(require redex/reduction-semantics
-         (only-in redex/private/generate-term pick-an-index)
-         racket/match
-         racket/list
-         racket/contract
-         racket/bool)
-
-(provide (all-defined-out))
-
-(define-language stlc
-  (M N ::= 
-     (λ (x σ) M)
-     (M N)
-     x
-     c)
-  (Γ (x σ Γ)
-     •)
-  (σ τ ::=
-     int
-     (list int)
-     (σ → τ))
-  (c d ::= cons nil hd tl + integer)
-  ((x y) variable-not-otherwise-mentioned)
-  
-  (v (λ (x τ) M)
-     c
-     (cons v)
-     ((cons v) v)
-     (+ v))
-  (E hole
-     (E M)
-     (v E)))
-
-(define-judgment-form stlc
-  #:mode (typeof I I O)
-  #:contract (typeof Γ M σ)
-  
-  [---------------------------
-   (typeof Γ c (const-type c))]
-  
-  [(where τ (lookup Γ x))
-   ----------------------
-   (typeof Γ x τ)]
-  
-  [(typeof (x σ Γ) M σ_2)
-   --------------------------------
-   (typeof Γ (λ (x σ) M) (σ → σ_2))]
-  
-  [(typeof Γ M (σ → σ_2))
-   (typeof Γ M_2 σ)
-   ----------------------
-   (typeof Γ (M M_2) σ_2)])
-
-(define-metafunction stlc
-  const-type : c -> σ
-  [(const-type nil)
-   (list int)]
-  [(const-type cons)
-   (int → ((list int) → (list int)))]
-  [(const-type hd)
-   ((list int) → int)]
-  [(const-type tl)
-   ((list int) → (list int))]
-  [(const-type +)
-   (int → (int → int))]
-  [(const-type integer)
-   int])
-
-(define-metafunction stlc
-  lookup : Γ x -> σ or #f
-  [(lookup (x σ Γ) x)
-   σ]
-  [(lookup (x σ Γ) x_2)
-   (lookup Γ x_2)]
-  [(lookup • x)
-   #f])
-
-(define red
-  (reduction-relation
-   stlc
-   (--> (in-hole E ((λ (x τ) M) v))
-        (in-hole E (subst M x v))
-        "βv")
-   (--> (in-hole E (hd ((cons v_1) v_2)))
-        (in-hole E v_1)
-        "hd")
-   (--> (in-hole E (tl ((cons v_1) v_2)))
-        (in-hole E v_2)
-        "tl")
-   (--> (in-hole E (hd nil))
-        "error"
-        "hd-err")
-   (--> (in-hole E (tl nil))
-        "error"
-        "tl-err")
-   (--> (in-hole E ((+ integer_1) integer_2))
-        (in-hole E ,(+ (term integer_1) (term integer_2)))
-        "+")))
-
-(define-metafunction stlc
-  subst : M x M -> M
-  [(subst x x M)
-   M]
-  [(subst y x M)
-   x]
-  [(subst (λ (x τ) M) x M_x)
-   (λ (x τ) M)]
-  [(subst (λ (x_1 τ) M) x_2 v)
-   (λ (x_new τ) (subst (replace M x_1 x_new) x_2 v))
-   (where x_new ,(variable-not-in (term (x_1 e x_2))
-                                  (term x_1)))]
-  [(subst (c M) x M_x)
-   (c (subst M x M_x))]
-  [(subst (M N) x M_x)
-   ((subst M x M_x) (subst N x M_x))]
-  [(subst M x M_x)
-   M])
-
-(define-metafunction stlc
-  [(replace (any_1 ...) x_1 x_new)
-   ((replace any_1 x_1 x_new) ...)]
-  [(replace x_1 x_1 x_new)
-   x_new]
-  [(replace any_1 x_1 x_new)
-   any_1])
-
-(define M? (redex-match stlc M))
-(define/contract (Eval M)
-  (-> M? (or/c M? "error"))
-  (define M-t (judgment-holds (typeof • ,M τ) τ))
-  (unless (pair? M-t)
-    (error 'Eval "doesn't typecheck: ~s" M))
-  (define res (apply-reduction-relation* red M))
-  (unless (= 1 (length res))
-    (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
-  (define ans (car res))
-  (if (equal? "error" ans)
-      "error"
-      (let ([ans-t (judgment-holds (typeof • ,ans τ) τ)])
-        (unless (equal? M-t ans-t)
-          (error 'Eval "internal error: type soundness fails for ~s" M))
-        ans)))
-
-(define x? (redex-match stlc x))
-
-(define v? (redex-match? stlc v))
-(define τ? (redex-match? stlc τ))
-(define/contract (type-check M)
-  (-> M? (or/c τ? #f))
-  (define M-t (judgment-holds (typeof • ,M τ) τ))
-  (cond
-    [(empty? M-t)
-     #f]
-    [(null? (cdr M-t))
-     (car M-t)]
-    [else
-     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
-
-(test-equal (type-check (term 5))
-            (term int))
-(test-equal (type-check (term (5 5)))
-            #f)
-
-(define (progress-holds? M)
-  (if (type-check M)
-      (or (v? M)
-          (not (null? (apply-reduction-relation red (term ,M)))))
-      #t))
-
-(define (interesting-term? M)
-  (and (type-check M)
-       (term (uses-bound-var? () ,M))))
-
-(define-metafunction stlc
-  [(uses-bound-var? (x_0 ... x_1 x_2 ...) x_1)
-   #t]
-  [(uses-bound-var? (x_0 ...) (λ (x τ) M))
-   (uses-bound-var? (x x_0 ...) M)]
-  [(uses-bound-var? (x ...) (M N))
-   ,(or (term (uses-bound-var? (x ...) M))
-        (term (uses-bound-var? (x ...) N)))]
-  [(uses-bound-var? (x ...) (cons M))
-   (uses-bound-var? (x ...) M)]
-  [(uses-bound-var? (x ...) any)
-   #f])
-
-(define (really-interesting-term? M)
-  (and (interesting-term? M)
-       (term (applies-bv? () ,M))))
-
-(define-metafunction stlc
-  [(applies-bv? (x_0 ... x_1 x_2 ...) (x_1 M))
-   #t]
-  [(applies-bv? (x_0 ...) (λ (x τ) M))
-   (applies-bv? (x x_0 ...) M)]
-  [(applies-bv? (x ...) (M N))
-   ,(or (term (applies-bv? (x ...) M))
-        (term (applies-bv? (x ...) N)))]
-  [(applies-bv? (x ...) (cons M))
-   (applies-bv? (x ...) M)]
-  [(applies-bv? (x ...) any)
-   #f])
-
-(define (reduction-step-count/func red v?)
-  (λ (term)
-    (let loop ([t term]
-               [n 0])
-      (define res (apply-reduction-relation red t))
-      (cond 
-        [(and (empty? res)
-              (v? t))
-         n]
-        [(and (empty? res)
-              (equal? t "error"))
-         n]
-        [(= (length res) 1)
-         (loop (car res) (add1 n))]
-        [else
-         (error 'reduction-step-count "failed reduction: ~s\n~s\n~s" term t res)]))))
-
-(define reduction-step-count
-  (reduction-step-count/func red v?))
-
-(define (generate-M-term)
-  (generate-term stlc M 5))
-
-(define (generate-M-term-from-red)
-  (generate-term #:source red 5))
-
-(define (generate-typed-term)
-  (match (generate-term stlc 
-                        #:satisfying
-                        (typeof • M τ)
-                        5)
-    [`(typeof • ,M ,τ)
-     M]
-    [#f #f]))
-
-(define (generate-typed-term-from-red)
-  (define candidate
-    (case (random 5)
-      [(0)
-       (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-      [(1)
-       (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-      [(2)
-       (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-      [(3)
-       (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-      [(4)
-       (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
-  (match candidate
-    [`(typeof • ,M ,τ)
-     M]
-    [#f #f]))
-
-(define (typed-generator)
-  (let ([g (redex-generator stlc 
-                            (typeof • M τ)
-                            5)])
-    (λ () 
-      (match (g)
-        [`(typeof • ,M ,τ)
-         M]
-        [#f #f]))))
-
-;; check : (or/c #f term) -> boolean[#f = counterexample found!]
-(define (check term)
-  (or (not term)
-      (v? term)
-      (let ([t-type (type-check term)])
-        (implies
-         t-type
-         (let ([red-res (apply-reduction-relation red term)])
-           (and (= (length red-res) 1)
-                (let ([red-t (car red-res)])
-                  (or (equal? red-t "error")
-                      (let ([red-type (type-check red-t)])
-                        (equal? t-type red-type))))))))))
-
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.0001)))
-
-(define (ordered-enum-generator)
-  (let ([index 0])
-    (λ ()
-      (begin0
-        (generate-term stlc M #:i-th index)
-        (set! index (add1 index))))))
-
-(define fixed
-  (term
-   (;; 1
-    ((λ (x int) x) 1)
-
-    ;; 9
-    ((λ (x (list int)) (tl x)) ((cons 1) nil))
-
-    ;; 2 -- xxx I don't think this is really an error because the (M
-    ;; N) case does everything that (c M) does since M can equal
-    ;; c. Otherwise the previous test case would work, because (tl x)
-    ;; would not be subst'd and it has no type
-
-    ;; 3
-    ((λ (x int) ((λ (y int) y) x)) 1)
-
-    ;; 4 -- xxx I don't think this is really an error because the
-    ;; normal λ rule always does renaming so this test below works
-    ;; fine and ends up with x1 in both places.
-
-    #;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
-
-    ;; 5 & 6 --- xxx These diffs are bogus because they don't actually
-    ;; make a change to any of the program.
-
-    ;; 7
-    ((λ (x int) (hd ((cons x) nil))) 1)
-
-    ;; 8 -- xxx This isn't an error for the same reason 4 isn't.
-    
-    )))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt
deleted file mode 100644
index a1ad155e0b..0000000000
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt
+++ /dev/null
@@ -1,325 +0,0 @@
-#lang racket/base
-
-(define the-error "swaps to/from expressions when recurring in the rhs of app")
-
-(require redex/reduction-semantics
-         (only-in redex/private/generate-term pick-an-index)
-         racket/match
-         racket/list
-         racket/contract
-         racket/bool)
-
-(provide (all-defined-out))
-
-(define-language stlc
-  (M N ::= 
-     (λ (x σ) M)
-     (M N)
-     x
-     c)
-  (Γ (x σ Γ)
-     •)
-  (σ τ ::=
-     int
-     (list int)
-     (σ → τ))
-  (c d ::= cons nil hd tl + integer)
-  ((x y) variable-not-otherwise-mentioned)
-  
-  (v (λ (x τ) M)
-     c
-     (cons v)
-     ((cons v) v)
-     (+ v))
-  (E hole
-     (E M)
-     (v E)))
-
-(define-judgment-form stlc
-  #:mode (typeof I I O)
-  #:contract (typeof Γ M σ)
-  
-  [---------------------------
-   (typeof Γ c (const-type c))]
-  
-  [(where τ (lookup Γ x))
-   ----------------------
-   (typeof Γ x τ)]
-  
-  [(typeof (x σ Γ) M σ_2)
-   --------------------------------
-   (typeof Γ (λ (x σ) M) (σ → σ_2))]
-  
-  [(typeof Γ M (σ → σ_2))
-   (typeof Γ M_2 σ)
-   ----------------------
-   (typeof Γ (M M_2) σ_2)])
-
-(define-metafunction stlc
-  const-type : c -> σ
-  [(const-type nil)
-   (list int)]
-  [(const-type cons)
-   (int → ((list int) → (list int)))]
-  [(const-type hd)
-   ((list int) → int)]
-  [(const-type tl)
-   ((list int) → (list int))]
-  [(const-type +)
-   (int → (int → int))]
-  [(const-type integer)
-   int])
-
-(define-metafunction stlc
-  lookup : Γ x -> σ or #f
-  [(lookup (x σ Γ) x)
-   σ]
-  [(lookup (x σ Γ) x_2)
-   (lookup Γ x_2)]
-  [(lookup • x)
-   #f])
-
-(define red
-  (reduction-relation
-   stlc
-   (--> (in-hole E ((λ (x τ) M) v))
-        (in-hole E (subst M x v))
-        "βv")
-   (--> (in-hole E (hd ((cons v_1) v_2)))
-        (in-hole E v_1)
-        "hd")
-   (--> (in-hole E (tl ((cons v_1) v_2)))
-        (in-hole E v_2)
-        "tl")
-   (--> (in-hole E (hd nil))
-        "error"
-        "hd-err")
-   (--> (in-hole E (tl nil))
-        "error"
-        "tl-err")
-   (--> (in-hole E ((+ integer_1) integer_2))
-        (in-hole E ,(+ (term integer_1) (term integer_2)))
-        "+")))
-
-(define-metafunction stlc
-  subst : M x M -> M
-  [(subst x x M)
-   M]
-  [(subst y x M)
-   y]
-  [(subst (λ (x τ) M) x M_x)
-   (λ (x τ) M)]
-  [(subst (λ (x_1 τ) M) x_2 v)
-   (λ (x_new τ) (subst (replace M x_1 x_new) x_2 v))
-   (where x_new ,(variable-not-in (term (x_1 e x_2))
-                                  (term x_1)))]
-  [(subst (c M) x M_x)
-   (c (subst M x M_x))]
-  [(subst (M N) x M_x)
-   ((subst M_x x M) (subst N x M_x))]
-  [(subst M x M_x)
-   M])
-
-(define-metafunction stlc
-  [(replace (any_1 ...) x_1 x_new)
-   ((replace any_1 x_1 x_new) ...)]
-  [(replace x_1 x_1 x_new)
-   x_new]
-  [(replace any_1 x_1 x_new)
-   any_1])
-
-(define M? (redex-match stlc M))
-(define/contract (Eval M)
-  (-> M? (or/c M? "error"))
-  (define M-t (judgment-holds (typeof • ,M τ) τ))
-  (unless (pair? M-t)
-    (error 'Eval "doesn't typecheck: ~s" M))
-  (define res (apply-reduction-relation* red M))
-  (unless (= 1 (length res))
-    (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
-  (define ans (car res))
-  (if (equal? "error" ans)
-      "error"
-      (let ([ans-t (judgment-holds (typeof • ,ans τ) τ)])
-        (unless (equal? M-t ans-t)
-          (error 'Eval "internal error: type soundness fails for ~s" M))
-        ans)))
-
-(define x? (redex-match stlc x))
-
-(define v? (redex-match? stlc v))
-(define τ? (redex-match? stlc τ))
-(define/contract (type-check M)
-  (-> M? (or/c τ? #f))
-  (define M-t (judgment-holds (typeof • ,M τ) τ))
-  (cond
-    [(empty? M-t)
-     #f]
-    [(null? (cdr M-t))
-     (car M-t)]
-    [else
-     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
-
-(test-equal (type-check (term 5))
-            (term int))
-(test-equal (type-check (term (5 5)))
-            #f)
-
-(define (progress-holds? M)
-  (if (type-check M)
-      (or (v? M)
-          (not (null? (apply-reduction-relation red (term ,M)))))
-      #t))
-
-(define (interesting-term? M)
-  (and (type-check M)
-       (term (uses-bound-var? () ,M))))
-
-(define-metafunction stlc
-  [(uses-bound-var? (x_0 ... x_1 x_2 ...) x_1)
-   #t]
-  [(uses-bound-var? (x_0 ...) (λ (x τ) M))
-   (uses-bound-var? (x x_0 ...) M)]
-  [(uses-bound-var? (x ...) (M N))
-   ,(or (term (uses-bound-var? (x ...) M))
-        (term (uses-bound-var? (x ...) N)))]
-  [(uses-bound-var? (x ...) (cons M))
-   (uses-bound-var? (x ...) M)]
-  [(uses-bound-var? (x ...) any)
-   #f])
-
-(define (really-interesting-term? M)
-  (and (interesting-term? M)
-       (term (applies-bv? () ,M))))
-
-(define-metafunction stlc
-  [(applies-bv? (x_0 ... x_1 x_2 ...) (x_1 M))
-   #t]
-  [(applies-bv? (x_0 ...) (λ (x τ) M))
-   (applies-bv? (x x_0 ...) M)]
-  [(applies-bv? (x ...) (M N))
-   ,(or (term (applies-bv? (x ...) M))
-        (term (applies-bv? (x ...) N)))]
-  [(applies-bv? (x ...) (cons M))
-   (applies-bv? (x ...) M)]
-  [(applies-bv? (x ...) any)
-   #f])
-
-(define (reduction-step-count/func red v?)
-  (λ (term)
-    (let loop ([t term]
-               [n 0])
-      (define res (apply-reduction-relation red t))
-      (cond 
-        [(and (empty? res)
-              (v? t))
-         n]
-        [(and (empty? res)
-              (equal? t "error"))
-         n]
-        [(= (length res) 1)
-         (loop (car res) (add1 n))]
-        [else
-         (error 'reduction-step-count "failed reduction: ~s\n~s\n~s" term t res)]))))
-
-(define reduction-step-count
-  (reduction-step-count/func red v?))
-
-(define (generate-M-term)
-  (generate-term stlc M 5))
-
-(define (generate-M-term-from-red)
-  (generate-term #:source red 5))
-
-(define (generate-typed-term)
-  (match (generate-term stlc 
-                        #:satisfying
-                        (typeof • M τ)
-                        5)
-    [`(typeof • ,M ,τ)
-     M]
-    [#f #f]))
-
-(define (generate-typed-term-from-red)
-  (define candidate
-    (case (random 5)
-      [(0)
-       (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-      [(1)
-       (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-      [(2)
-       (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-      [(3)
-       (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-      [(4)
-       (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
-  (match candidate
-    [`(typeof • ,M ,τ)
-     M]
-    [#f #f]))
-
-(define (typed-generator)
-  (let ([g (redex-generator stlc 
-                            (typeof • M τ)
-                            5)])
-    (λ () 
-      (match (g)
-        [`(typeof • ,M ,τ)
-         M]
-        [#f #f]))))
-
-;; check : (or/c #f term) -> boolean[#f = counterexample found!]
-(define (check term)
-  (or (not term)
-      (v? term)
-      (let ([t-type (type-check term)])
-        (implies
-         t-type
-         (let ([red-res (apply-reduction-relation red term)])
-           (and (= (length red-res) 1)
-                (let ([red-t (car red-res)])
-                  (or (equal? red-t "error")
-                      (let ([red-type (type-check red-t)])
-                        (equal? t-type red-type))))))))))
-
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.0001)))
-
-(define (ordered-enum-generator)
-  (let ([index 0])
-    (λ ()
-      (begin0
-        (generate-term stlc M #:i-th index)
-        (set! index (add1 index))))))
-
-(define fixed
-  (term
-   (;; 1
-    ((λ (x int) x) 1)
-
-    ;; 9
-    ((λ (x (list int)) (tl x)) ((cons 1) nil))
-
-    ;; 2 -- xxx I don't think this is really an error because the (M
-    ;; N) case does everything that (c M) does since M can equal
-    ;; c. Otherwise the previous test case would work, because (tl x)
-    ;; would not be subst'd and it has no type
-
-    ;; 3
-    ((λ (x int) ((λ (y int) y) x)) 1)
-
-    ;; 4 -- xxx I don't think this is really an error because the
-    ;; normal λ rule always does renaming so this test below works
-    ;; fine and ends up with x1 in both places.
-
-    #;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
-
-    ;; 5 & 6 --- xxx These diffs are bogus because they don't actually
-    ;; make a change to any of the program.
-
-    ;; 7
-    ((λ (x int) (hd ((cons x) nil))) 1)
-
-    ;; 8 -- xxx This isn't an error for the same reason 4 isn't.
-    
-    )))