bring back the language definitions as they were before (with anys intead of es in various functions).

I got a bit overzealous in my changes! :)

Author: rfindler

redex-doc/redex/scribblings/long-tut/code/common.rkt

@@ -32,25 +32,25 @@
 (define-language Lambda
   (e ::=
      x 
-     (lambda (x_!_ ...) e)
-     (e e ...))
+     (lambda (x) e)
+     (e e))
   (x ::= variable-not-otherwise-mentioned))
 
 (define lambda? (redex-match? Lambda e))
 
 (module+ test
   (define e1 (term y))
   (define e2 (term (lambda (y) y)))
-  (define e3 (term (lambda (x y) y)))
+  (define e3 (term (lambda (x) (lambda (y) y))))
   (define e4 (term (,e2 e3)))
 
   (test-equal (lambda? e1) #true)
   (test-equal (lambda? e2) #true)
   (test-equal (lambda? e3) #true)
   (test-equal (lambda? e4) #true)
 
-  (define eb1 (term (lambda (x x) y)))
-  (define eb2 (term (lambda (x y) 3)))
+  (define eb1 (term (lambda () y)))
+  (define eb2 (term (lambda (x) (lambda (y) 3))))
 
   (test-equal (lambda? eb1) #false)
   (test-equal (lambda? eb2) #false))
@@ -74,7 +74,11 @@
 (module+ test
   (test-equal (term (=α (lambda (x) x) (lambda (y) y))) #true)
   (test-equal (term (=α (lambda (x) (x 1)) (lambda (y) (y 1)))) #true)
-  (test-equal (term (=α (lambda (x) x) (lambda (y) z))) #false))
+  (test-equal (term (=α (lambda (x) x) (lambda (y) z))) #false)
+  (test-equal (term (=α (lambda (x) x) (lambda (x) (lambda (x) x)))) #false)
+  (test-equal (term (=α (lambda (x) x) (lambda (x) (x x)))) #false)
+  (test-equal (term (=α (lambda (x) (lambda (y) (x y))) (lambda (x) (lambda (y) (y x))))) #false)
+  (test-equal (term (=α (lambda (x) (lambda (y) (x y))) (lambda (a) (lambda (b) (a b))))) #true))
 
 (define-metafunction Lambda
   =α : any any -> boolean
@@ -92,38 +96,37 @@
 
 (module+ test
   (define sd1 (term (K 1)))
-  (define sd2 (term 1))
 
   (test-equal (SD? sd1) #true))
 
 (define-metafunction SD
   sd : any -> any
-  [(sd any_1) (sd/a any_1 ())])
+  [(sd any) (sd/a any ())])
 
 (module+ test
   (test-equal (term (sd/a x ())) (term x))
-  (test-equal (term (sd/a x ((y) (z) (x)))) (term (K 2 0)))
+  (test-equal (term (sd/a x (y z x))) (term (K 2)))
   (test-equal (term (sd/a ((lambda (x) x) (lambda (y) y)) ()))
-              (term ((lambda () (K 0 0)) (lambda () (K 0 0)))))
+              (term ((lambda (K 0)) (lambda (K 0)))))
   (test-equal (term (sd/a (lambda (x) (x (lambda (y) y))) ()))
-              (term (lambda () ((K 0 0) (lambda () (K 0 0))))))
-  (test-equal (term (sd/a (lambda (z x) (x (lambda (y) z))) ()))
-              (term (lambda () ((K 0 1) (lambda () (K 1 0)))))))
+              (term (lambda ((K 0) (lambda (K 0))))))
+  (test-equal (term (sd/a (lambda (z) (lambda (x) (x (lambda (y) z)))) ()))
+              (term (lambda (lambda ((K 0) (lambda (K 2))))))))
 
 (define-metafunction SD
-  sd/a : any ((x ...) ...) -> any
-  [(sd/a x ((x_1 ...) ... (x_0 ... x x_2 ...) (x_3 ...) ...))
+  sd/a : any (x ...) -> any
+  [(sd/a x (x_1 ... x x_2 ...))
    ;; bound variable 
-   (K n_rib n_pos)
-   (where n_rib ,(length (term ((x_1 ...) ...))))
-   (where n_pos ,(length (term (x_0 ...))))
-   (where #false (in x (x_1 ... ...)))]
-  [(sd/a (lambda (x ...) any_1) (any_rest ...))
-   (lambda () (sd/a any_1 ((x ...) any_rest ...)))]
-  [(sd/a (any_fun any_arg ...) (any_rib ...))
-   ((sd/a any_fun (any_rib ...)) (sd/a any_arg (any_rib ...)) ...)]
-  [(sd/a any_1 any)
-   ;; free variable, constant, etc 
+   (K n)
+   (where n ,(length (term (x_1 ...))))
+   (where #false (in x (x_1 ...)))]
+  [(sd/a (lambda (x) any_body) (x_rest ...))
+   (lambda (sd/a any_body (x x_rest ...)))
+   (where n ,(length (term (x_rest ...))))]
+  [(sd/a (any_fun any_arg) (x_rib ...))
+   ((sd/a any_fun (x_rib ...)) (sd/a any_arg (x_rib ...)))]
+  [(sd/a any_1 (x ...))
+   ;; free variable or constant, etc
    any_1])
 
 
@@ -134,10 +137,10 @@
   (test-equal (term (subst ([1 x][2 y]) x)) 1)
   (test-equal (term (subst ([1 x][2 y]) y)) 2)
   (test-equal (term (subst ([1 x][2 y]) z)) (term z))
-  (test-equal (term (subst ([1 x][2 y]) (lambda (z w) (x y))))
-              (term (lambda (z w) (1 2))))
-  (test-equal (term (subst ([1 x][2 y]) (lambda (z w) (lambda (x) (x y)))))
-              (term (lambda (z w) (lambda (x) (x 2))))
+  (test-equal (term (subst ([1 x][2 y]) (lambda (z) (lambda (w) (x y)))))
+              (term (lambda (z) (lambda (w) (1 2)))))
+  (test-equal (term (subst ([1 x][2 y]) (lambda (z) (lambda (w) (lambda (x) (x y))))))
+              (term (lambda (z) (lambda (w) (lambda (x) (x 2)))))
               #:equiv =α/racket)
   (test-equal (term (subst ((2 x)) ((lambda (x) (1 x)) x)))
               (term ((lambda (x) (1 x)) 2))
@@ -150,23 +153,23 @@
   subst : ((any x) ...) any -> any
   [(subst [(any_1 x_1) ... (any_x x) (any_2 x_2) ...] x) any_x]
   [(subst [(any_1 x_1) ... ] x) x]
-  [(subst [(any_1 x_1) ... ] (lambda (x ...) any_body))
-   (lambda (x_new ...)
+  [(subst [(any_1 x_1) ... ] (lambda (x) any_body))
+   (lambda (x_new)
      (subst ((any_1 x_1) ...)
-            (subst-raw ((x_new x) ...) any_body)))
-   (where  (x_new ...)  ,(variables-not-in (term (any_body any_1 ...)) (term (x ...)))) ]
+            (subst-raw (x_new x) any_body)))
+   (where  x_new ,(variable-not-in (term (any_body any_1 ...)) (term x)))]
   [(subst [(any_1 x_1) ... ] (any ...)) ((subst [(any_1 x_1) ... ] any) ...)]
   [(subst [(any_1 x_1) ... ] any_*) any_*])
 
 (define-metafunction Lambda
-  subst-raw : ((x x) ...) any -> any
-  [(subst-raw ((x_n1 x_o1) ... (x_new x) (x_n2 x_o2) ...) x) x_new]
-  [(subst-raw ((x_n1 x_o1) ... ) x) x]
-  [(subst-raw ((x_n1 x_o1) ... ) (lambda (x ...) any))
-   (lambda (x ...) (subst-raw ((x_n1 x_o1) ... ) any))]
-  [(subst-raw [(any_1 x_1) ... ] (any ...))
-   ((subst-raw [(any_1 x_1) ... ] any) ...)]
-  [(subst-raw [(any_1 x_1) ... ] any_*) any_*])
+  subst-raw : (x x) any -> any
+  [(subst-raw (x_new x_) x_) x_new]
+  [(subst-raw (x_new x_) x) x]
+  [(subst-raw (x_new x_) (lambda (x) any))
+   (lambda (x) (subst-raw (x_new x_) any))]
+  [(subst-raw (x_new x_) (any ...))
+   ((subst-raw (x_new x_) any) ...)]
+  [(subst-raw (x_new x_) any_*) any_*])
 
 ;; -----------------------------------------------------------------------------
 (module+ test

redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt

@@ -133,8 +133,8 @@ subst (if time, otherwise it's provide)
   (test-equal (SD? sd1) #true))
 
 (define-metafunction SD
-  sd : e -> e
-  [(sd e) (sd/a e ())])
+  sd : any -> any
+  [(sd any) (sd/a any ())])
 
 (module+ test
   (test-equal (term (sd/a x ())) (term x))
@@ -147,31 +147,31 @@ subst (if time, otherwise it's provide)
               (term (lambda (lambda ((K 0) (lambda (K 2))))))))
 
 (define-metafunction SD
-  sd/a : e (x ...) -> e
+  sd/a : any (x ...) -> any
   [(sd/a x (x_1 ... x x_2 ...))
    ;; bound variable 
    (K n)
    (where n ,(length (term (x_1 ...))))
    (where #false (in x (x_1 ...)))]
-  [(sd/a (lambda (x) e) (x_rest ...))
-   (lambda (sd/a e (x x_rest ...)))
+  [(sd/a (lambda (x) any_body) (x_rest ...))
+   (lambda (sd/a any_body (x x_rest ...)))
    (where n ,(length (term (x_rest ...))))]
-  [(sd/a (e_fun e_arg) (x_rib ...))
-   ((sd/a e_fun (x_rib ...)) (sd/a e_arg (x_rib ...)))]
+  [(sd/a (any_fun any_arg) (x_rib ...))
+   ((sd/a any_fun (x_rib ...)) (sd/a any_arg (x_rib ...)))]
   [(sd/a any_1 (x ...))
-   ;; free variable or constant
+   ;; free variable or constant, etc
    any_1])
 
 ;; -----------------------------------------------------------------------------
 ;; (=α e_1 e_2) determines whether e_1 and e_2 are α equivalent
 
 (module+ test
   (test-equal (term (=α (lambda (x) x) (lambda (y) y))) #true)
-  (test-equal (term (=α (lambda (x) (x z)) (lambda (y) (y z)))) #true)
+  (test-equal (term (=α (lambda (x) (x 1)) (lambda (y) (y 1)))) #true)
   (test-equal (term (=α (lambda (x) x) (lambda (y) z))) #false))
 
 (define-metafunction SD
-  =α : e e -> boolean
+  =α : any any -> boolean
   [(=α e_1 e_2) ,(equal? (term (sd e_1)) (term (sd e_2)))])
 
 (define (=α/racket x y) (term (=α ,x ,y)))

redex-doc/redex/scribblings/long-tut/lab-mon-aft.scrbl

@@ -39,7 +39,7 @@ Here is the definition of @deftech{environment}:
 Before you get started, make sure you can create examples of
 @tech{environment}s and confirm their well-formedness.}
 
-@exercise["ex:let"]{Develop the metafunction @racket[let], which extends
+@exercise["ex:let"]{Develop the metafunction @racket[let*], which extends
  the language with a notational shorthand, also known as syntactic sugar. 
 
  Once you have this metafunction, you can write expressions such as 
@@ -48,12 +48,12 @@ Before you get started, make sure you can create examples of
 #reader scribble/comment-reader
 (racketblock
 (term 
-  (let ((x (lambda (a b c) a))
+ (let* ((x (lambda (a b c) a))
         (y (lambda (x) x)))
     (x y y y)))
 ))
 @;%
- Like Racket's @racket[let], the function elaborates surface syntax into
+ Like Racket's @racket[let*], the function elaborates surface syntax into
  core syntax:
 @;%
 @(begin
@@ -74,8 +74,8 @@ Before you get started, make sure you can create examples of
 (racketblock
 (term 
  (fv 
-  (let ((x (lambda (a b c) a))
-        (y (lambda (x) x)))
+  (let* ((x (lambda (a b c) a))
+         (y (lambda (x) x)))
     (x y y y))))
 ))
 @;%
@@ -86,8 +86,8 @@ Before you get started, make sure you can create examples of
 (racketblock
 (term 
  (bv
-  (let ((x (lambda (a b c) a))
-        (y (lambda (x) x)))
+  (let* ((x (lambda (a b c) a))
+         (y (lambda (x) x)))
     (x y y y))))
 ))
 @;%

redex-doc/redex/scribblings/long-tut/mon-aft.scrbl

@@ -349,33 +349,33 @@ add binders:
   (test-equal (SD? sd1) #true))
 
 (define-metafunction SD
-  sd : any -> any
-  [(sd any_1) (sd/a any_1 ())])
+  sd : e -> e
+  [(sd e) (sd/a e ())])
 
 (module+ test
   (test-equal (term (sd/a x ())) (term x))
-  (test-equal (term (sd/a x ((y) (z) (x)))) (term (K 2 0)))
+  (test-equal (term (sd/a x (y z x))) (term (K 2)))
   (test-equal (term (sd/a ((lambda (x) x) (lambda (y) y)) ()))
-              (term ((lambda () (K 0 0)) (lambda () (K 0 0)))))
+              (term ((lambda (K 0)) (lambda (K 0)))))
   (test-equal (term (sd/a (lambda (x) (x (lambda (y) y))) ()))
-              (term (lambda () ((K 0 0) (lambda () (K 0 0))))))
-  (test-equal (term (sd/a (lambda (z x) (x (lambda (y) z))) ()))
-              (term (lambda () ((K 0 1) (lambda () (K 1 0)))))))
+              (term (lambda ((K 0) (lambda (K 0))))))
+  (test-equal (term (sd/a (lambda (z) (lambda (x) (x (lambda (y) z)))) ()))
+              (term (lambda (lambda ((K 0) (lambda (K 2))))))))
 
 (define-metafunction SD
-  sd/a : any ((x ...) ...) -> any
-  [(sd/a x ((x_1 ...) ... (x_0 ... x x_2 ...) (x_3 ...) ...))
+  sd/a : e (x ...) -> e
+  [(sd/a x (x_1 ... x x_2 ...))
    ;; bound variable 
-   (K n_rib n_pos)
-   (where n_rib ,(length (term ((x_1 ...) ...))))
-   (where n_pos ,(length (term (x_0 ...))))
-   (where #false (in x (x_1 ... ...)))]
-  [(sd/a (lambda (x ...) any_1) (any_rest ...))
-   (lambda () (sd/a any_1 ((x ...) any_rest ...)))]
-  [(sd/a (any_fun any_arg ...) (any_rib ...))
-   ((sd/a any_fun (any_rib ...)) (sd/a any_arg (any_rib ...)) ...)]
-  [(sd/a any_1 any)
-   ;; free variable, constant, etc 
+   (K n)
+   (where n ,(length (term (x_1 ...))))
+   (where #false (in x (x_1 ...)))]
+  [(sd/a (lambda (x) e) (x_rest ...))
+   (lambda (sd/a e (x x_rest ...)))
+   (where n ,(length (term (x_rest ...))))]
+  [(sd/a (e_fun e_arg) (x_rib ...))
+   ((sd/a e_fun (x_rib ...)) (sd/a e_arg (x_rib ...)))]
+  [(sd/a any_1 (x ...))
+   ;; free variable or constant
    any_1])
 ))
 @;%