From 7a0853e6510318fd42785eea143fb04ec42e2d60 Mon Sep 17 00:00:00 2001
From: Robby Findler <robby@racket-lang.org>
Date: Mon, 24 Jun 2013 03:45:27 -0500
Subject: [PATCH] adjust tut-subst.rkt so that it also supports untyped
 languages

---
 pkgs/redex/tests/tut-subst-test.rkt |  6 ++++++
 pkgs/redex/tut-subst.rkt            | 13 ++++++++++++-
 2 files changed, 18 insertions(+), 1 deletion(-)

diff --git a/pkgs/redex/tests/tut-subst-test.rkt b/pkgs/redex/tests/tut-subst-test.rkt
index 40c0aad86e..e0fb43d6dd 100644
--- a/pkgs/redex/tests/tut-subst-test.rkt
+++ b/pkgs/redex/tests/tut-subst-test.rkt
@@ -19,12 +19,18 @@
 (test-equal (term (subst (x y) (x (y z)))) (term (y (y z))))
 (test-equal (term (subst (x y) ((λ (x num) x) ((λ (y1 num) y1) (λ (x num) z)))))
             (term ((λ (x num) x) ((λ (y1 num) y1) (λ (x num) z)))))
+(test-equal (term (subst (x y) ((λ x x) ((λ y1 y1) (λ x z)))))
+            (term ((λ x x) ((λ y1 y1) (λ x z)))))
 (test-equal (term (subst (x y) (if0 (+ 1 x) x x)))
             (term (if0 (+ 1 y) y y)))
 (test-equal (term (subst (x (λ (z num) y)) (λ (y num) x)))
             (term (λ (y1 num) (λ (z num) y))))
+(test-equal (term (subst (x (λ z y)) (λ y x)))
+            (term (λ y1 (λ z y))))
 (test-equal (term (subst (x 1) (λ (y num) x)))
             (term (λ (y num) 1)))
+(test-equal (term (subst (x 1) (λ y x)))
+            (term (λ y 1)))
 (test-equal (term (subst (x y) (λ (y num) x)))
             (term (λ (y1 num) y)))
 (test-equal (term (subst (x (λ (y num) y)) (λ (z num) (z2 z))))
diff --git a/pkgs/redex/tut-subst.rkt b/pkgs/redex/tut-subst.rkt
index a61717da49..5f7e027e06 100644
--- a/pkgs/redex/tut-subst.rkt
+++ b/pkgs/redex/tut-subst.rkt
@@ -6,7 +6,13 @@ The substitution function in this file has been designed
 to work with any expression language so long as the only
 binding form is λ and the shape of λ terms is:
   
-      (λ (x t) ... e)
+      (λ (x any) ... e)
+
+(for types) or
+
+      (λ x ... e)
+
+for untyped.
 
 |#
 
@@ -39,6 +45,11 @@ binding form is λ and the shape of λ terms is:
          (adjust-active-inactive xs fvs-inactive fvs-active replacements))
        `(λ ,@(map (λ (x t) `(,x ,t)) new-xs ts)
           ,(loop body new-inactive new-active new-replacements))]
+      [`(λ ,(? symbol? xs) ... ,body)
+       (define-values (new-xs new-inactive new-active new-replacements)
+         (adjust-active-inactive xs fvs-inactive fvs-active replacements))
+       `(λ ,@new-xs
+          ,(loop body new-inactive new-active new-replacements))]
       [(? x? x)
        (cond
          [(hash-ref fvs-active x #f) => values]