fix subst function

- its contract said it accepted M's as the third argument, but it
  worked only for v's
- remove two redundant cases

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.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 (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

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/tests.rkt

@@ -4,4 +4,5 @@
             typeof
             red
             reduction-step-count
-            Eval)
+            Eval
+            subst)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/tests-lib.rkt

@@ -2,12 +2,34 @@
 (require redex/reduction-semantics)
 (provide stlc-tests)
 
+(define (consistent-with? t1 t2)
+  (define table (make-hash))
+  (let loop ([t1 t1]
+             [t2 t2])
+    (cond
+      [(and (pair? t1) (pair? t2))
+       (and (consistent-with? (car t1) (car t2))
+            (consistent-with? (cdr t1) (cdr t2)))]
+      [(and (symbol? t1) (symbol? t2))
+       (cond
+         [(equal? t1 t2) #t]
+         [else
+          (define bound (hash-ref table t1 #f))
+          (cond
+            [bound (equal? bound t2)]
+            [else 
+             (hash-set! table t1 t2)
+             #t])])]
+      [else (equal? t1 t2)])))
+          
+
 (define-syntax-rule
   (stlc-tests uses-bound-var?
               typeof
               red
               reduction-step-count
-              Eval)
+              Eval
+              subst)
   (begin
     
     (test-equal (term (uses-bound-var? () 5))
@@ -23,6 +45,26 @@
     (test-equal (term (uses-bound-var? () ((λ (x int) xy) 5)))
                 #f)
     
+    (test-equal (term (subst ((+ 1) 1) x 2))
+                (term ((+ 1) 1)))
+    (test-equal (term (subst ((+ x) x) x 2))
+                (term ((+ 2) 2)))
+    (test-equal (term (subst ((+ y) x) x 2))
+                (term ((+ y) 2)))
+    (test-equal (term (subst ((+ y) z) x 2))
+                (term ((+ y) z)))
+    (test-equal (term (subst ((λ (x int) x) x) x 2))
+                (term ((λ (x int) x) 2)))
+    (test-equal (consistent-with? (term (subst ((λ (y int) x) x) x 2))
+                                  (term ((λ (y int) 2) 2)))
+                #t)
+    (test-equal (consistent-with? (term (subst ((λ (y int) x) x) x (λ (q int) z)))
+                                  (term ((λ (y int) (λ (q int) z)) (λ (q int) z))))
+                #t)
+    (test-equal (consistent-with? (term (subst ((λ (y int) x) x) x (λ (q int) y)))
+                                  (term ((λ (y2 int) (λ (q int) y)) (λ (q int) y))))
+                #t)
+    
     (test-equal (judgment-holds (typeof • 5 τ) τ)
                 (list (term int)))
     (test-equal (judgment-holds (typeof • nil τ) τ)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/tests.rkt

@@ -4,4 +4,5 @@
             typeof
             red
             reduction-step-count
-            Eval)
+            Eval
+            subst)