adjust tut-subst.rkt so that it also supports

untyped languages

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))))

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]