From 6284f9b6717405071411d66448992097691eb635 Mon Sep 17 00:00:00 2001
From: Robby Findler <robby@racket-lang.org>
Date: Wed, 4 Jan 2023 16:31:44 -0600
Subject: [PATCH 1/9] updated monday

---
 .../scribblings/long-tut/code/mon-aft.rkt     | 135 +++++++-----------
 .../redex/scribblings/long-tut/mon-aft.scrbl  | 130 +++++++----------
 .../redex/scribblings/long-tut/mon-mor.scrbl  |   5 +-
 3 files changed, 109 insertions(+), 161 deletions(-)

diff --git a/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt b/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt
index cb0589fd..9b410dfe 100644
--- a/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt
+++ b/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt
@@ -22,31 +22,17 @@ subst (if time, otherwise it's provide)
 ;; -----------------------------------------------------------------------------
 (require redex)
 
-(define-language Lambda0
-  (e ::=
-     x 
-     (lambda (x ...) e)
-     (e e ...))
-  (x ::= variable-not-otherwise-mentioned))
-
-(define-language Lambda-bad
-  (e ::=
-     x 
-     (side-condition (lambda (x_ ...) e) (term (unique-vars (x_ ...))))
-     (e e ...))
-  (x ::= variable-not-otherwise-mentioned))
-
 (define-language Lambda
   (e ::=
      x 
-     (lambda (x_!_ ...) e)
-     (e e ...))
+     (lambda (x) e)
+     (e e))
   (x ::= variable-not-otherwise-mentioned))
 
 (define e1 (term y))
 (define e2 (term (lambda (y) y)))
-(define e3 (term (lambda (x y) y)))
-(define e4 (term (,e2 e3)))
+(define e3 (term (lambda (x) (lambda (y) y))))
+(define e4 (term (,e2 ,e3)))
 
 (define in-Lambda? (redex-match? Lambda e))
 
@@ -56,8 +42,8 @@ subst (if time, otherwise it's provide)
   (test-equal (in-Lambda? e3) #true)
   (test-equal (in-Lambda? e4) #true))
 
-(define eb1 (term (lambda (x x) y)))
-(define eb2 (term (lambda (x y) 3)))
+(define eb1 (term (lambda (y) (lambda () y))))
+(define eb2 (term (lambda (x) (lambda (y) 3))))
 
 (module+ test
   (test-equal (in-Lambda? eb1) #false)
@@ -95,19 +81,18 @@ subst (if time, otherwise it's provide)
 (module+ test
   (test-equal (term (fv x)) (term (x)))
   (test-equal (term (fv (lambda (x) x))) (term ()))
-  (test-equal (term (fv (lambda (x) (y z x)))) (term (y z))))
+  (test-equal (term (fv (lambda (x) ((y z) x)))) (term (y z))))
 
 (define-metafunction Lambda
-  fv : any -> (x ...)
+  fv : e -> (x ...)
   [(fv x) (x)]
-  [(fv (lambda (x ...) any_body))
-   (subtract (x_e ...) x ...)
-   (where (x_e ...) (fv any_body))]
-  [(fv (any_f any_a ...))
-   (x_f ... x_a ... ...)
-   (where (x_f ...) (fv any_f))
-   (where ((x_a ...) ...) ((fv any_a) ...))]
-  [(fv any) ()])
+  [(fv (lambda (x) e_body))
+   (subtract (x_e ...) x)
+   (where (x_e ...) (fv e_body))]
+  [(fv (e_f e_a))
+   (x_f ... x_a ...)
+   (where (x_f ...) (fv e_f))
+   (where (x_a ...) (fv e_a))])
 
 ;; -----------------------------------------------------------------------------
 ;; (subtract (x ...) x_1 ...) removes x_1 ... from (x ...)
@@ -137,11 +122,10 @@ subst (if time, otherwise it's provide)
 ;; (sd e) computes the static distance version of e
 
 (define-extended-language SD Lambda
-  (e ::= .... (K n n) (lambda n e))
+  (e ::= .... (K n) (lambda e) n)
   (n ::= natural))
 
-(define sd1 (term (K 0 1)))
-(define sd2 (term 1))
+(define sd1 (term (K 0)))
 
 (define SD? (redex-match? SD e))
 
@@ -149,53 +133,46 @@ subst (if time, otherwise it's provide)
   (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 1 (K 0 0)) (lambda 1 (K 0 0)))))
+              (term ((lambda (K 0)) (lambda (K 0)))))
   (test-equal (term (sd/a (lambda (x) (x (lambda (y) y))) ()))
-              (term (lambda 1 ((K 0 0) (lambda 1 (K 0 0))))))
-  (test-equal (term (sd/a (lambda (z x) (x (lambda (y) z))) ()))
-              (term (lambda 2 ((K 0 1) (lambda 1 (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 n (sd/a any_1 ((x ...) any_rest ...)))
-   (where n ,(length (term (x ...))))]
-  [(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])
 
 ;; -----------------------------------------------------------------------------
 ;; (=α e_1 e_2) determines whether e_1 and e_2 are α equivalent
 
-(define-extended-language Lambda/n Lambda
-  (e ::= .... n)
-  (n ::= natural))
-
-(define in-Lambda/n? (redex-match? Lambda/n e))
-
 (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 z)) (lambda (y) (y z)))) #true)
   (test-equal (term (=α (lambda (x) x) (lambda (y) z))) #false))
 
 (define-metafunction SD
-  =α : any any -> boolean
-  [(=α any_1 any_2) ,(equal? (term (sd any_1)) (term (sd any_2)))])
+  =α : e e -> boolean
+  [(=α e_1 e_2) ,(equal? (term (sd e_1)) (term (sd e_2)))])
 
 (define (=α/racket x y) (term (=α ,x ,y)))
 
@@ -206,38 +183,36 @@ subst (if time, otherwise it's provide)
   (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))
               #:equiv =α/racket))
-              
-              
 
 (define-metafunction Lambda
   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) (term (x ...)))) ]
+            (subst-raw (x_new x) any_body)))
+   (where  x_new ,(variable-not-in (term any_body) (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
diff --git a/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl b/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
index dbfe876b..d123c692 100644
--- a/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
+++ b/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
@@ -32,7 +32,7 @@ The @racket[define-language] from specifies syntax trees via tree grammars:
 (racketblock
 (define-language Lambda 
   (e ::= x 
-         (lambda (x ...) e)
+         (lambda (x) e)
          (e e ...))
   (x ::= variable-not-otherwise-mentioned))
 ))
@@ -51,7 +51,7 @@ them (typos do sneak in). Instances are generated with @racket[term]:
 @examples[#:label #f #:eval redex-eval
 (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)))
 
 e4
@@ -85,8 +85,8 @@ Now you can formulate language tests:
 (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 (x) (lambda () y))))
+(define eb2 (term (lambda (x) (lambda (y) 3))))
 
 (test-equal (lambda? eb1) #false)
 (test-equal (lambda? eb2) #false)
@@ -105,8 +105,8 @@ To make basic statements about (parts of) your language, define
 metafunctions. Roughly, a metafunction is a function on the terms of a
 specific language. 
 
-We don't want parameter sequences with repeated variables. Can we say this
-with a metafunction?
+A first meta-function might determine whether or not some sequence
+of variables has any duplicates.
 @;%
 @(begin
 #reader scribble/comment-reader
@@ -160,25 +160,6 @@ they are about, work through examples, write down the latter as tests,
 Submodules delegate the tests to where they belong and they allow us to
   document functions by example. 
 
-Sadly, our language definition cannot use the @racket[unique-vars] metafunction.
-(In order to define the metafunction, we first need to define the language.)
-
-Fortunately, language definitions can employ more than Kleene patterns: 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-(define-language Lambda
-  (e ::=
-     x 
-     (lambda (x_!_ ...) e)
-     (e e ...))
-  (x ::= variable-not-otherwise-mentioned))
-))
-@;%
-@racket[x_!_ ...] means @racket[x] must differ from all other elements of
-this sequence 
-
 Here are two more metafunctions that use patterns in interesting ways: 
 @;%
 @(begin
@@ -227,23 +208,23 @@ specifies which language constructs bind and which ones don't:
 (racketblock
 ;; (fv e) computes the sequence of free variables of e
 ;; a variable occurrence of @racket[x] is free in @racket[e] 
-;; if no @racket[(lambda (... x ...) ...)] @emph{dominates} its occurrence 
+;; if no @racket[(lambda (x) ...)] @emph{dominates} its occurrence 
 
 (module+ test
   (test-equal (term (fv x)) (term (x)))
   (test-equal (term (fv (lambda (x) x))) (term ()))
-  (test-equal (term (fv (lambda (x) (y z x)))) (term (y z))))
+  (test-equal (term (fv (lambda (x) ((y z) x)))) (term (y z))))
 
 (define-metafunction Lambda
   fv : e -> (x ...)
   [(fv x) (x)]
-  [(fv (lambda (x ...) e))
-   (subtract (x_e ...) x ...)
-   (where (x_e ...) (fv e))]
-  [(fv (e_f e_a ...))
-   (x_f ... x_a ... ...)
+  [(fv (lambda (x) e_body))
+   (subtract (x_e ...) x)
+   (where (x_e ...) (fv e_body))]
+  [(fv (e_f e_a))
+   (x_f ... x_a ...)
    (where (x_f ...) (fv e_f))
-   (where ((x_a ...) ...) ((fv e_a) ...))])
+   (where (x_a ...) (fv e_a))])
 ))
 @;%
 
@@ -263,11 +244,10 @@ The function is a good example of accumulator-functions in Redex:
 ;; (sd e) computes the static distance version of e
 
 (define-extended-language SD Lambda
-  (e ::= .... (K n))
+  (e ::= .... (K n) (lambda e) n)
   (n ::= natural))
 
 (define sd1 (term (K 1)))
-(define sd2 (term 1))
 
 (define SD? (redex-match? SD e))
 
@@ -285,33 +265,33 @@ The function is a good example of accumulator-functions in Redex:
 (racketblock
 (define-metafunction SD
   sd : e -> e
-  [(sd e_1) (sd/a e_1 ())])
+  [(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 : e ((x ...) ...) -> e
-  [(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 ...) e_1) (e_rest ...))
-   (lambda () (sd/a e_1 ((x ...) e_rest ...)))]
-  [(sd/a (e_fun e_arg ...) (e_rib ...))
-   ((sd/a e_fun (e_rib ...)) (sd/a e_arg (e_rib ...)) ...)]
-  [(sd/a e_1 any)
-   ;; a free variable is left alone 
-   e_1])
+   (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])
 ))
 @;%
 
@@ -322,15 +302,9 @@ Now α equivalence is straightforward:
 (racketblock
 ;; (=α e_1 e_2) determines whether e_1 and e_2 are α equivalent
 
-(define-extended-language Lambda/n Lambda
-  (e ::= .... n)
-  (n ::= natural))
-
-(define in-Lambda/n? (redex-match? Lambda/n e))
-
 (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 z)) (lambda (y) (y z)))) #true)
   (test-equal (term (=α (lambda (x) x) (lambda (y) z))) #false))
 
 (define-metafunction SD
@@ -423,38 +397,36 @@ future extensions in mind.
   (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))
               #:equiv =α/racket))
-              
-              
 
 (define-metafunction Lambda
   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) (term (x ...)))) ]
+            (subst-raw (x_new x) any_body)))
+   (where  x_new ,(variable-not-in (term any_body) (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_*])
 
 ))
 @;%
diff --git a/redex-doc/redex/scribblings/long-tut/mon-mor.scrbl b/redex-doc/redex/scribblings/long-tut/mon-mor.scrbl
index 2a6d6fe1..ffff876e 100644
--- a/redex-doc/redex/scribblings/long-tut/mon-mor.scrbl
+++ b/redex-doc/redex/scribblings/long-tut/mon-mor.scrbl
@@ -74,8 +74,9 @@ All of the above is mathematics but it is just that,
 mathematics. It might be considered theory of computation,
 but it is not theory of programming languages. But we can
 use these ideas to create a theory of programming languages.
-Plotkin's 1974 TCS paper on call-by-name versus
-call-by-value shows how to create a theory of programming
+@link["https://homepages.inf.ed.ac.uk/gdp/publications/cbn_cbv_lambda.pdf"]{
+ Plotkin's 1974 TCS paper on call-by-name versus
+ call-by-value} shows how to create a theory of programming
 languages.
 
 In addition, Plotkin's paper also sketches several research programs,

From 47fe76681906c04c514b4baa88da23aa240505b3 Mon Sep 17 00:00:00 2001
From: Robby Findler <robby@racket-lang.org>
Date: Thu, 5 Jan 2023 20:38:50 -0600
Subject: [PATCH 2/9] fix bug in substitution

---
 redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt b/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt
index 9b410dfe..4c2dd97b 100644
--- a/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt
+++ b/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt
@@ -190,6 +190,9 @@ subst (if time, otherwise it's provide)
               #:equiv =α/racket)
   (test-equal (term (subst ((2 x)) ((lambda (x) (1 x)) x)))
               (term ((lambda (x) (1 x)) 2))
+              #:equiv =α/racket)
+  (test-equal (term (subst (((lambda (x) y) x)) (lambda (y) x)))
+              (term (lambda (y1) (lambda (x) y)))
               #:equiv =α/racket))
 
 (define-metafunction Lambda
@@ -200,7 +203,7 @@ subst (if time, otherwise it's provide)
    (lambda (x_new)
      (subst ((any_1 x_1) ...)
             (subst-raw (x_new x) any_body)))
-   (where  x_new ,(variable-not-in (term any_body) (term x)))]
+   (where  x_new ,(variable-not-in (term (any_1 ... any_body)) (term x)))]
   [(subst [(any_1 x_1) ... ] (any ...)) ((subst [(any_1 x_1) ... ] any) ...)]
   [(subst [(any_1 x_1) ... ] any_*) any_*])
 

From c1b1a2c0578af9074181ebe2dad5d74b95519999 Mon Sep 17 00:00:00 2001
From: Robby Findler <robby@racket-lang.org>
Date: Mon, 9 Jan 2023 15:16:21 -0600
Subject: [PATCH 3/9] bring back the language definitions as they were before
 (with `any`s intead of `e`s in various functions).

I got a bit overzealous in my changes! :)
---
 .../scribblings/long-tut/code/common.rkt      | 85 ++++++++++---------
 .../scribblings/long-tut/code/mon-aft.rkt     | 20 ++---
 .../scribblings/long-tut/lab-mon-aft.scrbl    | 14 +--
 .../redex/scribblings/long-tut/mon-aft.scrbl  | 38 ++++-----
 4 files changed, 80 insertions(+), 77 deletions(-)

diff --git a/redex-doc/redex/scribblings/long-tut/code/common.rkt b/redex-doc/redex/scribblings/long-tut/code/common.rkt
index 648b68dc..28754311 100644
--- a/redex-doc/redex/scribblings/long-tut/code/common.rkt
+++ b/redex-doc/redex/scribblings/long-tut/code/common.rkt
@@ -32,8 +32,8 @@
 (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))
@@ -41,7 +41,7 @@
 (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)
@@ -49,8 +49,8 @@
   (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
diff --git a/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt b/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt
index 4c2dd97b..57f272c3 100644
--- a/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt
+++ b/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,19 +147,19 @@ 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])
 
 ;; -----------------------------------------------------------------------------
@@ -167,11 +167,11 @@ subst (if time, otherwise it's provide)
 
 (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)))
diff --git a/redex-doc/redex/scribblings/long-tut/lab-mon-aft.scrbl b/redex-doc/redex/scribblings/long-tut/lab-mon-aft.scrbl
index 5f0d30b7..341f2ab3 100644
--- a/redex-doc/redex/scribblings/long-tut/lab-mon-aft.scrbl
+++ b/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))))
 ))
 @;%
diff --git a/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl b/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
index d123c692..65f4761b 100644
--- a/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
+++ b/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])
 ))
 @;%

From d3462754a0116ebf7ee214140dd4f4ddfd1edfd1 Mon Sep 17 00:00:00 2001
From: Robby Findler <robby@racket-lang.org>
Date: Mon, 9 Jan 2023 20:33:20 -0600
Subject: [PATCH 4/9] add infrastructure to avoid all these out-of-sync copies
 of code

and use it to uncopy the code in mon-aft.scrbl
---
 .../scribblings/long-tut/code/mon-aft.rkt     |   3 +-
 .../redex/scribblings/long-tut/mon-aft.scrbl  |  72 +++--------
 .../redex/scribblings/long-tut/shared.rkt     | 116 +++++++++++++++++-
 3 files changed, 136 insertions(+), 55 deletions(-)

diff --git a/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt b/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt
index 57f272c3..21289af6 100644
--- a/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt
+++ b/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt
@@ -47,7 +47,8 @@ subst (if time, otherwise it's provide)
 
 (module+ test
   (test-equal (in-Lambda? eb1) #false)
-  (test-equal (in-Lambda? eb2) #false))
+  (test-equal (in-Lambda? eb2) #false)
+  ) ;; close paren must be on this line or else mon-aft.scrbl won't run properly
 
 ;; -----------------------------------------------------------------------------
 ;; (unique-vars x ...) is the sequence of variables x ... free of duplicates?
diff --git a/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl b/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
index 65f4761b..f5b45844 100644
--- a/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
+++ b/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
@@ -25,18 +25,10 @@ To start a program with Redex, start your file with
 @codeblock{#lang racket
            (require redex)}
 
-The @racket[define-language] from specifies syntax trees via tree grammars: 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-(define-language Lambda 
-  (e ::= x 
-         (lambda (x) e)
-         (e e ...))
-  (x ::= variable-not-otherwise-mentioned))
-))
-@;%
+The @racket[define-language] from specifies syntax trees via tree grammars:
+
+@codeblock-from-file["code/mon-aft.rkt" #rx"define-language Lambda" #:eval redex-eval]
+
 The trees are somewhat concrete, which makes it easy to work with them, but
 it is confusing on those incredibly rare occasions when we want truly
 abstract syntax. 
@@ -46,54 +38,28 @@ or integers (all of Racket's integers) or naturals (all of Racket's natural
 numbers)---and many other things. 
 
 After you have a syntax, use the grammar to generate instances and check
-them (typos do sneak in). Instances are generated with @racket[term]: 
-@;
-@examples[#:label #f #:eval redex-eval
-(define e1 (term y))
-(define e2 (term (lambda (y) y)))
-(define e3 (term (lambda (x) (lambda (y) y))))
-(define e4 (term (,e2 ,e3)))
+them (typos do sneak in). Instances are generated with @racket[term]:
+@codeblock-from-file["code/mon-aft.rkt"
+                     #rx"define e1 [(]term"
+                     #:eval redex-eval
+                     #:exp-count 4
+                     #:extra-code ("e4")]
 
-e4
-]
 Mouse over @racket[define]. It is @emph{not} a Redex form, it comes from
 Racket. Take a close look at the last definition. Comma anyone? 
 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-(redex-match? Lambda e e4)
-))
-@;%
-
 Define yourself a predicate that tests membership: 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-(define lambda? (redex-match? Lambda e))
-))
-@;%
-Now you can formulate language tests: 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-(test-equal (lambda? e1) #true)
-(test-equal (lambda? e2) #true)
-(test-equal (lambda? e3) #true)
-(test-equal (lambda? e4) #true)
+@codeblock-from-file["code/mon-aft.rkt" #rx"define in-Lambda[?]" #:eval redex-eval]
 
-(define eb1 (term (lambda (x) (lambda () y))))
-(define eb2 (term (lambda (x) (lambda (y) 3))))
+Now you can formulate language tests:
+@codeblock-from-file["code/mon-aft.rkt" #rx"test-equal [(]in-Lambda[?] e1"
+                     #:eval redex-eval #:exp-count 4]
+@codeblock-from-file["code/mon-aft.rkt" #rx"define eb1"
+                     #:eval redex-eval #:exp-count 2]
+@codeblock-from-file["code/mon-aft.rkt" #rx"test-equal [(]in-Lambda[?] eb1"
+                     #:eval redex-eval #:exp-count 2
+                     #:extra-code ("(test-results)")]
 
-(test-equal (lambda? eb1) #false)
-(test-equal (lambda? eb2) #false)
-
-(test-results)
-))
-@;%
 Make sure your language contains the terms that you want and does
 @emph{not} contain those you want to exclude. Why should @racket[eb1] and
 @racket[eb2] not be in @racket[Lambda]'s set of expressions? 
diff --git a/redex-doc/redex/scribblings/long-tut/shared.rkt b/redex-doc/redex/scribblings/long-tut/shared.rkt
index 85621583..623f4b94 100644
--- a/redex-doc/redex/scribblings/long-tut/shared.rkt
+++ b/redex-doc/redex/scribblings/long-tut/shared.rkt
@@ -1,4 +1,12 @@
 #lang at-exp racket/base
+(module+ test (require rackunit))
+
+#; #;
+(this is to facilitate
+      some testing code
+      that appears below)
+(it helps test
+    codeblock-from-file)
 
 (provide
   goals  ;; bulletize goals 
@@ -10,16 +18,21 @@
     scribble/example
     racket/sandbox
     scribble/core
-    scriblib/figure))
+    scriblib/figure)
+  codeblock-from-file)
 
 ;; -----------------------------------------------------------------------------
 (require
   "exercise/ex.rkt"
   (for-label racket/base redex/reduction-semantics)
+  (for-syntax racket/base racket/match racket/list
+              syntax/parse syntax/strip-context)
   scribble/manual
   scribble/core
   scribble/example
   racket/sandbox
+  racket/runtime-path
+  racket/list
   scriblib/figure)
 
 
@@ -51,3 +64,104 @@ to the top of your file:
 @;%
  }
 )
+
+;; codeblock-from-file pulls a specific hunk of lines from
+;; one of the files in code/ and generates a use of `examples`
+;; with that code in it.
+;;
+;; Supply:
+;; - the name of the file as a relative path to the source
+;;   location of the use of codeblock-from-file,
+;; - a regular expression that the first line to include must match
+;; - the evaluator to evaluate the program, with #:eval
+;; - the number of expressions that should follow (according to the
+;;   rules of read) with #:exp-count, which defaults to 1
+;; - and a sequence of strings to tack onto the end of the expression
+;;   these are treated as if they are extra lines in the file with
+;;   #:extra-code
+;;
+;; if the expression begins with define, define-language or a few
+;; other keywords (see the match expression below), then the code
+;; is wrapped with eval:no-prompt (see examples for docs)
+;; the highlighting and linking is based on the for-label bindings
+;; that are at the use of codeblock-from-file
+(define-syntax (codeblock-from-file stx)
+  (syntax-parse stx
+    [(_ file:string rx-start:regexp #:eval eval
+        (~optional (~seq #:exp-count number-of-expressions:integer))
+        (~optional (~seq #:extra-code (extra-code:string ...))))
+
+     #`(examples #:label #f
+                 #:eval eval
+                 #,@(get-code (syntax-e #'file)
+                              (syntax-e #'rx-start)
+                              (if (attribute number-of-expressions)
+                                  (syntax-e #'number-of-expressions)
+                                  1)
+                              (if (attribute extra-code)
+                                  (map
+                                   syntax-e
+                                   (syntax->list #'(extra-code ...)))
+                                  '())
+                              stx))]))
+
+(begin-for-syntax
+  (define (get-code file rx:start number-of-expressions extra-code stx)
+    (define src (syntax-source stx))
+    (define-values (src-dir _1 _2) (split-path src))
+    (define-values (in out) (make-pipe))
+    (define-values (start-line end-line no-prompt?s)
+      (get-start-and-end-lines file rx:start
+                               number-of-expressions
+                               stx
+                               src-dir))
+    (call-with-input-file (build-path src-dir file)
+      (λ (port)
+        (for/list ([l (in-lines port)]
+                   [i (in-range end-line)]
+                   #:unless (< i start-line))
+          (displayln l out))))
+    (for ([extra-code-item (in-list extra-code)])
+      (displayln extra-code-item out))
+    (close-output-port out)
+    (port-count-lines! in)
+    (for/list ([no-prompt? (in-list (append no-prompt?s
+                                            (make-list (length extra-code)
+                                                       #f)))])
+      (define e (replace-context stx (read-syntax src in)))
+      (if no-prompt?
+          `(eval:no-prompt ,e)
+          e)))
+
+  (define (get-start-and-end-lines file rx:start number-of-expressions stx src-dir)
+    (define start-line
+      (call-with-input-file (build-path src-dir file)
+        (λ (port)
+          (define count 0)
+          (let/ec escape
+            (for ([l (in-lines port)])
+              (when (regexp-match? rx:start l)
+                (escape))
+              (set! count (+ count 1)))
+            (raise-syntax-error 'codeblock-from-file
+                                (format "didn't find a line matching ~s" rx:start)
+                                stx))
+          count)))
+    (define-values (no-prompt?s end-line)
+      (call-with-input-file (build-path src-dir file)
+        (λ (port)
+          (port-count-lines! port)
+          (for ([i (in-range start-line)])
+            (read-line port))
+          (define no-prompt?s
+            (for/list ([i (in-range number-of-expressions)])
+              (define exp (read port))
+              (when (eof-object? exp) (error 'codeblock-from-file "expression #~a not present in file" i))
+              (match exp
+                [`(define . ,stuff) #t]
+                [`(define-language . ,stuff) #t]
+                [`(test-equal . ,stuff) #t]
+                [_ #f])))
+          (define-values (line col pos) (port-next-location port))
+          (values no-prompt?s line))))
+    (values start-line end-line no-prompt?s)))

From 355abe811701e1915527b43ee4e506a9e16052cd Mon Sep 17 00:00:00 2001
From: Robby Findler <robby@racket-lang.org>
Date: Tue, 10 Jan 2023 20:45:23 -0600
Subject: [PATCH 5/9] more copied code elimination

---
 .../scribblings/long-tut/code/mon-aft.rkt     |   5 +
 .../redex/scribblings/long-tut/mon-aft.scrbl  | 247 +++++-------------
 .../redex/scribblings/long-tut/shared.rkt     |  89 ++++---
 3 files changed, 127 insertions(+), 214 deletions(-)

diff --git a/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt b/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt
index 21289af6..74fd9456 100644
--- a/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt
+++ b/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt
@@ -53,10 +53,12 @@ subst (if time, otherwise it's provide)
 ;; -----------------------------------------------------------------------------
 ;; (unique-vars x ...) is the sequence of variables x ... free of duplicates?
 
+;; unique-vars tests start
 (module+ test 
   (test-equal (term (unique-vars x y)) #true)
   (test-equal (term (unique-vars x y x)) #false))
 
+;; unique-vars metafunction start
 (define-metafunction Lambda 
   unique-vars : x ... -> boolean 
   [(unique-vars) #true]
@@ -84,6 +86,7 @@ subst (if time, otherwise it's provide)
   (test-equal (term (fv (lambda (x) x))) (term ()))
   (test-equal (term (fv (lambda (x) ((y z) x)))) (term (y z))))
 
+;; fv metafunction start
 (define-metafunction Lambda
   fv : e -> (x ...)
   [(fv x) (x)]
@@ -130,9 +133,11 @@ subst (if time, otherwise it's provide)
 
 (define SD? (redex-match? SD e))
 
+;; SD? test case
 (module+ test
   (test-equal (SD? sd1) #true))
 
+;; SD metafunction
 (define-metafunction SD
   sd : any -> any
   [(sd any) (sd/a any ())])
diff --git a/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl b/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
index f5b45844..15110c55 100644
--- a/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
+++ b/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
@@ -27,7 +27,7 @@ To start a program with Redex, start your file with
 
 The @racket[define-language] from specifies syntax trees via tree grammars:
 
-@codeblock-from-file["code/mon-aft.rkt" #rx"define-language Lambda" #:eval redex-eval]
+@code-from-file["code/mon-aft.rkt" #rx"define-language Lambda" #:eval redex-eval]
 
 The trees are somewhat concrete, which makes it easy to work with them, but
 it is confusing on those incredibly rare occasions when we want truly
@@ -39,26 +39,26 @@ numbers)---and many other things.
 
 After you have a syntax, use the grammar to generate instances and check
 them (typos do sneak in). Instances are generated with @racket[term]:
-@codeblock-from-file["code/mon-aft.rkt"
-                     #rx"define e1 [(]term"
-                     #:eval redex-eval
-                     #:exp-count 4
-                     #:extra-code ("e4")]
+@code-from-file["code/mon-aft.rkt"
+                #rx"define e1 [(]term"
+                #:eval redex-eval
+                #:exp-count 4
+                #:extra-code ("e4")]
 
 Mouse over @racket[define]. It is @emph{not} a Redex form, it comes from
 Racket. Take a close look at the last definition. Comma anyone? 
 
 Define yourself a predicate that tests membership: 
-@codeblock-from-file["code/mon-aft.rkt" #rx"define in-Lambda[?]" #:eval redex-eval]
+@code-from-file["code/mon-aft.rkt" #rx"define in-Lambda[?]" #:eval redex-eval]
 
 Now you can formulate language tests:
-@codeblock-from-file["code/mon-aft.rkt" #rx"test-equal [(]in-Lambda[?] e1"
-                     #:eval redex-eval #:exp-count 4]
-@codeblock-from-file["code/mon-aft.rkt" #rx"define eb1"
-                     #:eval redex-eval #:exp-count 2]
-@codeblock-from-file["code/mon-aft.rkt" #rx"test-equal [(]in-Lambda[?] eb1"
-                     #:eval redex-eval #:exp-count 2
-                     #:extra-code ("(test-results)")]
+@code-from-file["code/mon-aft.rkt" #rx"test-equal [(]in-Lambda[?] e1"
+                #:eval redex-eval #:exp-count 4]
+@code-from-file["code/mon-aft.rkt" #rx"define eb1"
+                #:eval redex-eval #:exp-count 2]
+@code-from-file["code/mon-aft.rkt" #rx"test-equal [(]in-Lambda[?] eb1"
+                #:eval redex-eval #:exp-count 2
+                #:extra-code ("(test-results)")]
 
 Make sure your language contains the terms that you want and does
 @emph{not} contain those you want to exclude. Why should @racket[eb1] and
@@ -72,127 +72,60 @@ metafunctions. Roughly, a metafunction is a function on the terms of a
 specific language. 
 
 A first meta-function might determine whether or not some sequence
-of variables has any duplicates.
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-(define-metafunction Lambda 
-  unique-vars : x ... -> boolean)
-))
-@;%
- The second line is a Redex contract, not a type. It says
+of variables has any duplicates. The second line is a Redex contract, not a type. It says
  @racket[unique-vars] consumes a sequence of @racket[x]s and produces a
  @racket[boolean]. 
 
-How do we say we don't want repeated variables? With patterns. 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-(define-metafunction Lambda 
-  unique-vars : x ... -> boolean 
-  [(unique-vars) #true]
-  [(unique-vars x x_1 ... x x_2 ...) #false]
-  [(unique-vars x x_1 ...) (unique-vars x_1 ...)])
-))
-@;%
- Patterns are powerful. More later. 
+The remaining lines say that we don't want repeated variables with patterns.
+@code-from-file["code/mon-aft.rkt"
+                #rx";; unique-vars metafunction start"
+                #:eval redex-eval
+                #:skip-lines 1]
+Patterns are powerful. More later. 
 
 But, don't just define metafunctions, develop them properly: state what
 they are about, work through examples, write down the latter as tests,
 @emph{then} define the function. 
 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-;; are the identifiers in the given sequence unique?
-
-(module+ test 
-  (test-equal (term (unique-vars x y)) #true)
-  (test-equal (term (unique-vars x y x)) #false))
-
-(define-metafunction Lambda 
-  unique-vars : x ... -> boolean 
-  [(unique-vars) #true]
-  [(unique-vars x x_1 ... x x_2 ...) #false]
-  [(unique-vars x x_1 ...) (unique-vars x_1 ...)])
-
-(module+ test
-  (test-results))
-))
-@;%
-Submodules delegate the tests to where they belong and they allow us to
-  document functions by example. 
-
-Here are two more metafunctions that use patterns in interesting ways: 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-;; (subtract (x ...) x_1 ...) removes x_1 ... from (x ...)
-
-(module+ test
-  (test-equal (term (subtract (x y z x) x z)) (term (y))))
 
-(define-metafunction Lambda
-  subtract : (x ...) x ... -> (x ...)
-  [(subtract (x ...)) (x ...)]
-  [(subtract (x ...) x_1 x_2 ...)
-   (subtract (subtract1 (x ...) x_1) x_2 ...)])
+Wrap the tests in a @racket[module+] with the name @racketidfont{test}
+to delegate the tests to a submodule where they belong, allowing us to
+document functions by example without introducing tests into client modules
+that require the module for the definitions:
+@;
+@code-from-file["code/mon-aft.rkt"
+                #rx";; unique-vars metafunction start"
+                #:eval redex-eval
+                #:skip-lines 1]
 
-;; (subtract1 (x ...) x_1) removes x_1  from (x ...)
-(module+ test
-  (test-equal (term (subtract1 (x y z x) x)) (term (y z))))
 
-(define-metafunction Lambda
-  subtract1 : (x ...) x -> (x ...)
-  [(subtract1 (x_1 ... x x_2 ...) x)
-   (x_1 ... x_2new ...)
-   (where (x_2new ...) (subtract1 (x_2 ...) x))
-   (where #false (in x (x_1 ...)))]
-  [(subtract1 (x ...) x_1) (x ...)])
-
-(define-metafunction Lambda
-  in : x (x ...) -> boolean
-  [(in x (x_1 ... x x_2 ...)) #true]
-  [(in x (x_1 ...)) #false])
+Here are two more metafunctions that use patterns in interesting ways:
 
-))
-@;%
+@code-from-file["code/mon-aft.rkt"
+                #rx"[(]subtract [(]x [.][.][.][)] x_1 [.][.][.][)] removes"
+                #:exp-count 4
+                #:skip-lines 2]
 
 @; -----------------------------------------------------------------------------
 @section{Developing a Language 2}
 
 One of the first things a language designer ought to specify is
 @deftech{scope}. People often do so with a free-variables function that
-specifies which language constructs bind and which ones don't:
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-;; (fv e) computes the sequence of free variables of e
-;; a variable occurrence of @racket[x] is free in @racket[e] 
-;; if no @racket[(lambda (x) ...)] @emph{dominates} its occurrence 
+specifies which language constructs bind and which ones don't.
 
-(module+ test
-  (test-equal (term (fv x)) (term (x)))
-  (test-equal (term (fv (lambda (x) x))) (term ()))
-  (test-equal (term (fv (lambda (x) ((y z) x)))) (term (y z))))
+@racket[(fv e)] computes the sequence of free variables of e
+a variable occurrence of @racket[x] is free in @racket[e] 
+if no @racket[(lambda (x) ...)] @emph{dominates} its occurrence 
 
-(define-metafunction Lambda
-  fv : e -> (x ...)
-  [(fv x) (x)]
-  [(fv (lambda (x) e_body))
-   (subtract (x_e ...) x)
-   (where (x_e ...) (fv e_body))]
-  [(fv (e_f e_a))
-   (x_f ... x_a ...)
-   (where (x_f ...) (fv e_f))
-   (where (x_a ...) (fv e_a))])
-))
-@;%
+
+@code-from-file["code/mon-aft.rkt"
+                #rx"[(]fv e[)] computes the sequence of free variables of e"
+                #:skip-lines 1]
+
+@code-from-file["code/mon-aft.rkt"
+                #rx";; fv metafunction start"
+                #:eval redex-eval
+                #:skip-lines 1]
 
 @margin-note{You may know it as the de Bruijn index representation.}
 @;
@@ -200,86 +133,34 @@ The best approach is to specify an α equivalence relation, that is, the
 relation that virtually eliminates variables from phrases and replaces them
 with arrows to their declarations. In the world of lambda calculus-based
 languages, this transformation is often a part of the compiler, the
-so-called static-distance phase.
+so-called static-distance phase. The function is a good example of
+accumulator-functions in Redex.
 
-The function is a good example of accumulator-functions in Redex: 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-;; (sd e) computes the static distance version of e
-
-(define-extended-language SD Lambda
-  (e ::= .... (K n) (lambda e) n)
-  (n ::= natural))
-
-(define sd1 (term (K 1)))
-
-(define SD? (redex-match? SD e))
-
-(module+ test
-  (test-equal (SD? sd1) #true))
-))
-@;%
   We have to add a means to the language to say ``arrow back to the variable
   declaration.'' We do @emph{not} edit the language definition but
   @emph{extend} the language definition instead. 
 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-(define-metafunction SD
-  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)))
-  (test-equal (term (sd/a ((lambda (x) x) (lambda (y) y)) ()))
-              (term ((lambda (K 0)) (lambda (K 0)))))
-  (test-equal (term (sd/a (lambda (x) (x (lambda (y) y))) ()))
-              (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))))))))
+@code-from-file["code/mon-aft.rkt"
+                #rx"define-extended-language SD Lambda"
+                #:eval redex-eval
+                #:exp-count 3]
+@code-from-file["code/mon-aft.rkt"
+                #rx";; SD[?] test case"
+                #:skip-lines 1]
 
-(define-metafunction SD
-  sd/a : e (x ...) -> e
-  [(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 ...)))
-   (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])
-))
 @;%
 
+@code-from-file["code/mon-aft.rkt"
+                #rx";; SD metafunction"
+                #:exp-count 3]
+
 Now α equivalence is straightforward: 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-;; (=α 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) (lambda (y) z))) #false))
 
-(define-metafunction SD
-  =α : e e -> boolean
-  [(=α e_1 e_2) ,(equal? (term (sd e_1)) (term (sd e_2)))])
+@code-from-file["code/mon-aft.rkt"
+                #rx"determines whether e_1 and e_2 are α equivalent"
+                #:exp-count 3]
 
-(define (=α/racket x y) (term (=α ,x ,y)))
-))
-@;%
 
 @; -----------------------------------------------------------------------------
 @section{Extending a Language: @racket[any]}
diff --git a/redex-doc/redex/scribblings/long-tut/shared.rkt b/redex-doc/redex/scribblings/long-tut/shared.rkt
index 623f4b94..1cd0c60d 100644
--- a/redex-doc/redex/scribblings/long-tut/shared.rkt
+++ b/redex-doc/redex/scribblings/long-tut/shared.rkt
@@ -19,13 +19,13 @@
     racket/sandbox
     scribble/core
     scriblib/figure)
-  codeblock-from-file)
+  code-from-file)
 
 ;; -----------------------------------------------------------------------------
 (require
   "exercise/ex.rkt"
   (for-label racket/base redex/reduction-semantics)
-  (for-syntax racket/base racket/match racket/list
+  (for-syntax racket/base racket/match racket/list racket/port
               syntax/parse syntax/strip-context)
   scribble/manual
   scribble/core
@@ -73,9 +73,14 @@ to the top of your file:
 ;; - the name of the file as a relative path to the source
 ;;   location of the use of codeblock-from-file,
 ;; - a regular expression that the first line to include must match
-;; - the evaluator to evaluate the program, with #:eval
+;; - the evaluator to evaluate the program, with #:eval; if #:eval
+;;   is not present, the code is not evaluated and instead of `examples`
+;;   being used, `codeblock` is used.
 ;; - the number of expressions that should follow (according to the
 ;;   rules of read) with #:exp-count, which defaults to 1
+;; - the number of lines to skip, counting the matching line
+;;   (useful to add comments to give the regexp something to grab onto)
+;;   with #:skip-lines
 ;; - and a sequence of strings to tack onto the end of the expression
 ;;   these are treated as if they are extra lines in the file with
 ;;   #:extra-code
@@ -85,36 +90,48 @@ to the top of your file:
 ;; is wrapped with eval:no-prompt (see examples for docs)
 ;; the highlighting and linking is based on the for-label bindings
 ;; that are at the use of codeblock-from-file
-(define-syntax (codeblock-from-file stx)
+(define-syntax (code-from-file stx)
   (syntax-parse stx
-    [(_ file:string rx-start:regexp #:eval eval
+    [(_ file:string rx-start:regexp 
+        (~optional (~seq #:eval eval))
         (~optional (~seq #:exp-count number-of-expressions:integer))
+        (~optional (~seq #:skip-lines number-of-lines-to-skip:integer))
         (~optional (~seq #:extra-code (extra-code:string ...))))
-
-     #`(examples #:label #f
-                 #:eval eval
-                 #,@(get-code (syntax-e #'file)
-                              (syntax-e #'rx-start)
-                              (if (attribute number-of-expressions)
-                                  (syntax-e #'number-of-expressions)
-                                  1)
-                              (if (attribute extra-code)
-                                  (map
-                                   syntax-e
-                                   (syntax->list #'(extra-code ...)))
-                                  '())
-                              stx))]))
+     (define doing-eval? (attribute eval))
+     (define code
+       (get-code (syntax-e #'file)
+                 (syntax-e #'rx-start)
+                 (if (attribute number-of-expressions)
+                     (syntax-e #'number-of-expressions)
+                     1)
+                 (if (attribute number-of-lines-to-skip)
+                     (syntax-e #'number-of-lines-to-skip)
+                     0)
+                 (if (attribute extra-code)
+                     (map
+                      syntax-e
+                      (syntax->list #'(extra-code ...)))
+                     '())
+                 doing-eval?
+                 stx))
+     (if doing-eval?
+         #`(examples #:label #f
+                     #:eval eval
+                     #,@code)
+         #`(codeblock #:context #'#,stx
+                      #,@code))]))
 
 (begin-for-syntax
-  (define (get-code file rx:start number-of-expressions extra-code stx)
+  (define (get-code file rx:start number-of-expressions number-of-lines-to-skip extra-code doing-eval? stx)
     (define src (syntax-source stx))
     (define-values (src-dir _1 _2) (split-path src))
     (define-values (in out) (make-pipe))
-    (define-values (start-line end-line no-prompt?s)
+    (define-values (start-pos start-line end-line no-prompt?s)
       (get-start-and-end-lines file rx:start
                                number-of-expressions
                                stx
                                src-dir))
+    (set! start-line (+ start-line number-of-lines-to-skip))
     (call-with-input-file (build-path src-dir file)
       (λ (port)
         (for/list ([l (in-lines port)]
@@ -125,16 +142,23 @@ to the top of your file:
       (displayln extra-code-item out))
     (close-output-port out)
     (port-count-lines! in)
-    (for/list ([no-prompt? (in-list (append no-prompt?s
-                                            (make-list (length extra-code)
-                                                       #f)))])
-      (define e (replace-context stx (read-syntax src in)))
-      (if no-prompt?
-          `(eval:no-prompt ,e)
-          e)))
+    (set-port-next-location! in start-line 0 start-pos)
+    (cond
+      [doing-eval?
+       (for/list ([no-prompt? (in-list (append no-prompt?s
+                                               (make-list (length extra-code)
+                                                          #f)))])
+         (define e (replace-context stx (read-syntax (build-path src-dir file) in)))
+         (if no-prompt?
+             `(eval:no-prompt ,e)
+             e))]
+      [else
+       (define sp (open-output-string))
+       (copy-port in sp)
+       (list (get-output-string sp))]))
 
   (define (get-start-and-end-lines file rx:start number-of-expressions stx src-dir)
-    (define start-line
+    (define-values (start-line start-pos)
       (call-with-input-file (build-path src-dir file)
         (λ (port)
           (define count 0)
@@ -146,7 +170,8 @@ to the top of your file:
             (raise-syntax-error 'codeblock-from-file
                                 (format "didn't find a line matching ~s" rx:start)
                                 stx))
-          count)))
+          (define-values (line col pos) (port-next-location port))
+          (values count pos))))
     (define-values (no-prompt?s end-line)
       (call-with-input-file (build-path src-dir file)
         (λ (port)
@@ -160,8 +185,10 @@ to the top of your file:
               (match exp
                 [`(define . ,stuff) #t]
                 [`(define-language . ,stuff) #t]
+                [`(define-extended-language . ,stuff) #t]
+                [`(define-metafunction . ,stuff) #t]
                 [`(test-equal . ,stuff) #t]
                 [_ #f])))
           (define-values (line col pos) (port-next-location port))
           (values no-prompt?s line))))
-    (values start-line end-line no-prompt?s)))
+    (values start-pos start-line end-line no-prompt?s)))

From cf630a579877b6c4e53645d5f0facaa11d7a1b8b Mon Sep 17 00:00:00 2001
From: Robby Findler <robby@racket-lang.org>
Date: Wed, 11 Jan 2023 16:11:56 -0600
Subject: [PATCH 6/9] finish uncopying monday afternoon

---
 .../scribblings/long-tut/code/common.rkt      |  2 +-
 .../scribblings/long-tut/code/mon-aft.rkt     | 59 ++---------
 .../redex/scribblings/long-tut/mon-aft.scrbl  | 97 ++-----------------
 .../redex/scribblings/long-tut/shared.rkt     | 16 +--
 4 files changed, 24 insertions(+), 150 deletions(-)

diff --git a/redex-doc/redex/scribblings/long-tut/code/common.rkt b/redex-doc/redex/scribblings/long-tut/code/common.rkt
index 28754311..4d94bed9 100644
--- a/redex-doc/redex/scribblings/long-tut/code/common.rkt
+++ b/redex-doc/redex/scribblings/long-tut/code/common.rkt
@@ -89,7 +89,7 @@
 
 ;; (sd e) computes the static distance version of e
 (define-extended-language SD Lambda
-  (e ::= .... (K n))
+  (e ::= .... (K n) (lambda e))
   (n ::= natural))
 
 (define SD? (redex-match? SD e))
diff --git a/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt b/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt
index 74fd9456..af952793 100644
--- a/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt
+++ b/redex-doc/redex/scribblings/long-tut/code/mon-aft.rkt
@@ -139,8 +139,8 @@ subst (if time, otherwise it's provide)
 
 ;; SD metafunction
 (define-metafunction SD
-  sd : any -> any
-  [(sd any) (sd/a any ())])
+  sd : e -> e
+  [(sd e) (sd/a e ())])
 
 (module+ test
   (test-equal (term (sd/a x ())) (term x))
@@ -153,19 +153,18 @@ subst (if time, otherwise it's provide)
               (term (lambda (lambda ((K 0) (lambda (K 2))))))))
 
 (define-metafunction SD
-  sd/a : any (x ...) -> any
+  sd/a : e (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) any_body) (x_rest ...))
-   (lambda (sd/a any_body (x x_rest ...)))
+  [(sd/a (lambda (x) e_body) (x_rest ...))
+   (lambda (sd/a e_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 (e_fun e_arg) (x ...))
+   ((sd/a e_fun (x ...)) (sd/a e_arg (x ...)))]
   [(sd/a any_1 (x ...))
-   ;; free variable or constant, etc
    any_1])
 
 ;; -----------------------------------------------------------------------------
@@ -177,52 +176,10 @@ subst (if time, otherwise it's provide)
   (test-equal (term (=α (lambda (x) x) (lambda (y) z))) #false))
 
 (define-metafunction SD
-  =α : any any -> boolean
+  =α : e e -> boolean
   [(=α e_1 e_2) ,(equal? (term (sd e_1)) (term (sd e_2)))])
 
 (define (=α/racket x y) (term (=α ,x ,y)))
 
-;; -----------------------------------------------------------------------------
-;; (subst ([e x] ...) e_*) substitutes e ... for x ... in e_* (hygienically)
-
-(module+ test
-  (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) (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))
-              #:equiv =α/racket)
-  (test-equal (term (subst (((lambda (x) y) x)) (lambda (y) x)))
-              (term (lambda (y1) (lambda (x) y)))
-              #:equiv =α/racket))
-
-(define-metafunction Lambda
-  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) ...)
-            (subst-raw (x_new x) any_body)))
-   (where  x_new ,(variable-not-in (term (any_1 ... any_body)) (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_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
   (test-results))
diff --git a/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl b/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
index 15110c55..331ea5b8 100644
--- a/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
+++ b/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
@@ -156,7 +156,6 @@ accumulator-functions in Redex.
 
 Now α equivalence is straightforward: 
 
-
 @code-from-file["code/mon-aft.rkt"
                 #rx"determines whether e_1 and e_2 are α equivalent"
                 #:exp-count 3]
@@ -165,6 +164,7 @@ Now α equivalence is straightforward:
 @; -----------------------------------------------------------------------------
 @section{Extending a Language: @racket[any]}
 
+
 Suppose we wish to extend @racket[Lambda] with @racket[if] and Booleans,
 like this: 
 @;%
@@ -178,7 +178,7 @@ like this:
      (if e e e)))
 ))
 @;%
- Guess what? @racket[(term (fv (lambda (x y) (if x y false))))] doesn't
+ Guess what? @racket[(term (sd (lambda (x y) (if x y false))))] doesn't
  work because @racket[false] and @racket[if] are not covered. 
 
 We want metafunctions that are as generic as possible for computing such
@@ -187,45 +187,11 @@ equivalences.
 
 Redex contracts come with @racket[any] and Redex patterns really are over
 Racket's S-expressions. This definition now works for extensions that don't
-add binders: 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-(module+ test
-  (test-equal (SD? sd1) #true))
-
-(define-metafunction SD
-  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)))
-  (test-equal (term (sd/a ((lambda (x) x) (lambda (y) y)) ()))
-              (term ((lambda (K 0)) (lambda (K 0)))))
-  (test-equal (term (sd/a (lambda (x) (x (lambda (y) y))) ()))
-              (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 : e (x ...) -> e
-  [(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 ...)))
-   (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])
-))
-@;%
+add binders:
+
+@code-from-file["code/common.rkt"
+                #rx"define-extended-language SD Lambda"
+                #:exp-count 6]
 
 @; -----------------------------------------------------------------------------
 @section{Substitution}
@@ -234,49 +200,6 @@ The last thing we need is substitution, because it @emph{is} the syntactic
 equivalent of function application. We define it with @emph{any} having
 future extensions in mind.  
 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-;; (subst ([e x] ...) e_*) substitutes e ... for x ... in e_* (hygienically)
-
-(module+ test
-  (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) (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))
-              #:equiv =α/racket))
-
-(define-metafunction Lambda
-  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) ...)
-            (subst-raw (x_new x) any_body)))
-   (where  x_new ,(variable-not-in (term any_body) (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_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_*])
-
-))
-@;%
-
-
-}
+@code-from-file["code/common.rkt"
+                #rx"substitutes e [.][.][.] for x [.][.][.] in e_[*]"
+                #:exp-count 3]
diff --git a/redex-doc/redex/scribblings/long-tut/shared.rkt b/redex-doc/redex/scribblings/long-tut/shared.rkt
index 1cd0c60d..bce37cd9 100644
--- a/redex-doc/redex/scribblings/long-tut/shared.rkt
+++ b/redex-doc/redex/scribblings/long-tut/shared.rkt
@@ -1,12 +1,4 @@
 #lang at-exp racket/base
-(module+ test (require rackunit))
-
-#; #;
-(this is to facilitate
-      some testing code
-      that appears below)
-(it helps test
-    codeblock-from-file)
 
 (provide
   goals  ;; bulletize goals 
@@ -26,7 +18,7 @@
   "exercise/ex.rkt"
   (for-label racket/base redex/reduction-semantics)
   (for-syntax racket/base racket/match racket/list racket/port
-              syntax/parse syntax/strip-context)
+              syntax/parse syntax/strip-context compiler/cm-accomplice)
   scribble/manual
   scribble/core
   scribble/example
@@ -125,6 +117,8 @@ to the top of your file:
   (define (get-code file rx:start number-of-expressions number-of-lines-to-skip extra-code doing-eval? stx)
     (define src (syntax-source stx))
     (define-values (src-dir _1 _2) (split-path src))
+    (define file-with-code-to-show (build-path src-dir file))
+    (register-external-file file-with-code-to-show)
     (define-values (in out) (make-pipe))
     (define-values (start-pos start-line end-line no-prompt?s)
       (get-start-and-end-lines file rx:start
@@ -132,7 +126,7 @@ to the top of your file:
                                stx
                                src-dir))
     (set! start-line (+ start-line number-of-lines-to-skip))
-    (call-with-input-file (build-path src-dir file)
+    (call-with-input-file file-with-code-to-show
       (λ (port)
         (for/list ([l (in-lines port)]
                    [i (in-range end-line)]
@@ -148,7 +142,7 @@ to the top of your file:
        (for/list ([no-prompt? (in-list (append no-prompt?s
                                                (make-list (length extra-code)
                                                           #f)))])
-         (define e (replace-context stx (read-syntax (build-path src-dir file) in)))
+         (define e (replace-context stx (read-syntax file-with-code-to-show in)))
          (if no-prompt?
              `(eval:no-prompt ,e)
              e))]

From d8333a5c934b99e9f7cfb5242d2643dc695ff45b Mon Sep 17 00:00:00 2001
From: Robby Findler <robby@racket-lang.org>
Date: Fri, 28 Apr 2023 19:12:06 -0500
Subject: [PATCH 7/9] fix an error and tighten a pattern

---
 redex-doc/redex/scribblings/long-tut/mon-aft.scrbl | 4 +---
 redex-doc/redex/scribblings/long-tut/shared.rkt    | 2 +-
 2 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl b/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
index 331ea5b8..b98e2ad7 100644
--- a/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
+++ b/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
@@ -94,11 +94,9 @@ document functions by example without introducing tests into client modules
 that require the module for the definitions:
 @;
 @code-from-file["code/mon-aft.rkt"
-                #rx";; unique-vars metafunction start"
-                #:eval redex-eval
+                #rx";; unique-vars tests start"
                 #:skip-lines 1]
 
-
 Here are two more metafunctions that use patterns in interesting ways:
 
 @code-from-file["code/mon-aft.rkt"
diff --git a/redex-doc/redex/scribblings/long-tut/shared.rkt b/redex-doc/redex/scribblings/long-tut/shared.rkt
index bce37cd9..487ccc58 100644
--- a/redex-doc/redex/scribblings/long-tut/shared.rkt
+++ b/redex-doc/redex/scribblings/long-tut/shared.rkt
@@ -87,7 +87,7 @@ to the top of your file:
     [(_ file:string rx-start:regexp 
         (~optional (~seq #:eval eval))
         (~optional (~seq #:exp-count number-of-expressions:integer))
-        (~optional (~seq #:skip-lines number-of-lines-to-skip:integer))
+        (~optional (~seq #:skip-lines number-of-lines-to-skip:nat))
         (~optional (~seq #:extra-code (extra-code:string ...))))
      (define doing-eval? (attribute eval))
      (define code

From 59be2afeaeda60d8fb876a067d7965fcbdb0dcb8 Mon Sep 17 00:00:00 2001
From: Robby Findler <robby@racket-lang.org>
Date: Fri, 28 Apr 2023 19:25:47 -0500
Subject: [PATCH 8/9] update tuesday morning code

---
 .../scribblings/long-tut/code/tue-mor.rkt     | 53 +++++++++++--------
 1 file changed, 30 insertions(+), 23 deletions(-)

diff --git a/redex-doc/redex/scribblings/long-tut/code/tue-mor.rkt b/redex-doc/redex/scribblings/long-tut/code/tue-mor.rkt
index 1d5cf088..fa8e8e26 100644
--- a/redex-doc/redex/scribblings/long-tut/code/tue-mor.rkt
+++ b/redex-doc/redex/scribblings/long-tut/code/tue-mor.rkt
@@ -4,9 +4,9 @@
 
 (define-extended-language Lambda-calculus Lambda
   (e ::= .... n)
-  (v ::= n (lambda (x ...) e))
+  (v ::= n (lambda (x) e))
   (n ::= number)
-  (C ::= hole (e ... C e ...) (lambda (x_!_ ...) C)))
+  (C ::= hole (e ... C e ...) (lambda (x) C)))
 
 (define lambda? (redex-match? Lambda-calculus e))
 (define context? (redex-match? Lambda-calculus C))
@@ -16,13 +16,17 @@
 (define-metafunction Lambda-calculus
   ;;  let : ((x e) ...) e -> e but e plus hole 
   let : ((x any) ...) any -> any
-  [(let ([x_lhs any_rhs] ...) any_body)
-   ((lambda (x_lhs ...) any_body) any_rhs ...)])
+  [(let () any_body) any_body]
+  [(let ([x_lhs any_rhs] [x_lhs-more any_rhs-more] ...) any_body)
+   ((lambda (x_lhs)
+      (let ([x_lhs-more any_rhs-more] ...)
+        any_body))
+    any_rhs)])
 
 (module+ test
-  (define C1 (term ((lambda (x y) x) hole 1)))
-  (define C2 (term ((lambda (x y) hole) 0 1)))
-  (define C3 (term (let ([x hole][y 3]) (lambda (a) (a (x 1 y 2))))))
+  (define C1 (term (((lambda (x) (lambda (y) x)) hole) 1)))
+  (define C2 (term (((lambda (x) (lambda (y) hole)) 0) 1)))
+  (define C3 (term (let ([x hole][y 3]) (lambda (a) (a (((x 1) y) 2))))))
   
   (test-equal (context? C1) #true)
   (test-equal (context? C2) #true)
@@ -30,7 +34,7 @@
   
   (define e1 (term (in-hole ,C1 1)))
   (define e2 (term (in-hole ,C2 x)))
-  (define e3 (term (in-hole ,C3 (lambda (x y z) x))))
+  (define e3 (term (in-hole ,C3 (lambda (x) (lambda (y) (lambda (z) x))))))
   
   (test-equal (lambda? e1) #true)
   (test-equal (lambda? e2) #true)
@@ -48,23 +52,26 @@
   ;; reduces to TWO expressions 
   (define e4 ;; a term that contains TWO βv redexes 
     (term
-     ((lambda (x y)
-        [(lambda (f) (f (x 1 y 2)))
-         (lambda (w) 42)])
-      [(lambda (x) x) (lambda (a b c) a)]
+     (((lambda (x)
+         (lambda (y)
+           [(lambda (f) (f (((x 1) y) 2)))
+            (lambda (w) 42)]))
+       [(lambda (x) x) (lambda (a) (lambda (b) (lambda (c) a)))])
       3)))
   (define e4-one-step
     (term
-     ((lambda (x y)
-        ((lambda (f) (f (x 1 y 2)))
-         (lambda (w) 42)))
-      (lambda (a b c) a)
+     (((lambda (x)
+         (lambda (y)
+           ((lambda (f) (f (((x 1) y) 2)))
+            (lambda (w) 42))))
+       (lambda (a) (lambda (b) (lambda (c) a))))
       3)))
   (define e4-other-step
     (term
-     ((lambda (x y)
-        ((lambda (w) 42) (x 1 y 2)))
-      ((lambda (x) x) (lambda (a b c) a))
+     (((lambda (x)
+         (lambda (y)
+           ((lambda (w) 42) (((x 1) y) 2))))
+       ((lambda (x) x) (lambda (a) (lambda (b) (lambda (c) a)))))
       3)))
   
   (test--> -->βv #:equiv =α/racket e4 e4-other-step e4-one-step)
@@ -73,8 +80,8 @@
 (define -->βv 
   (reduction-relation
    Lambda-calculus
-   (--> (in-hole C ((lambda (x_1 ..._n) e) v_1 ..._n))
-        (in-hole C (subst ([v_1 x_1] ...) e))
+   (--> (in-hole C ((lambda (x) e) v))
+        (in-hole C (subst ([v x]) e))
         βv)))
 
 #;
@@ -94,8 +101,8 @@
 (define s-->βv
   (reduction-relation
    Standard
-   (--> (in-hole E ((lambda (x_1 ..._n) e) v_1 ..._n))
-        (in-hole E (subst ((v_1 x_1) ...) e)))))
+   (--> (in-hole E ((lambda (x) e) v))
+        (in-hole E (subst ([v x]) e)))))
 
 ;; -----------------------------------------------------------------------------
 ;; a semantics

From d9a873bdc651543bea021f69755315b97c371915 Mon Sep 17 00:00:00 2001
From: Robby Findler <robby@racket-lang.org>
Date: Fri, 28 Apr 2023 20:01:00 -0500
Subject: [PATCH 9/9] progress on tuesday morning

---
 .../scribblings/long-tut/code/common.rkt      |  2 +-
 .../scribblings/long-tut/code/tue-mor.rkt     |  7 ++-
 .../redex/scribblings/long-tut/tue-mor.scrbl  | 48 ++++++-------------
 3 files changed, 20 insertions(+), 37 deletions(-)

diff --git a/redex-doc/redex/scribblings/long-tut/code/common.rkt b/redex-doc/redex/scribblings/long-tut/code/common.rkt
index 4d94bed9..f7dcc537 100644
--- a/redex-doc/redex/scribblings/long-tut/code/common.rkt
+++ b/redex-doc/redex/scribblings/long-tut/code/common.rkt
@@ -27,7 +27,7 @@
  subst)
 
 ;; -----------------------------------------------------------------------------
-(require redex)
+(require redex/reduction-semantics)
 
 (define-language Lambda
   (e ::=
diff --git a/redex-doc/redex/scribblings/long-tut/code/tue-mor.rkt b/redex-doc/redex/scribblings/long-tut/code/tue-mor.rkt
index fa8e8e26..1b4b8ecd 100644
--- a/redex-doc/redex/scribblings/long-tut/code/tue-mor.rkt
+++ b/redex-doc/redex/scribblings/long-tut/code/tue-mor.rkt
@@ -1,6 +1,6 @@
 #lang racket
-(require redex "common.rkt" (only-in "mon-aft.rkt" fv))
 (provide eval-value)
+(require redex "common.rkt" (only-in "mon-aft.rkt" fv))
 
 (define-extended-language Lambda-calculus Lambda
   (e ::= .... n)
@@ -24,6 +24,7 @@
     any_rhs)])
 
 (module+ test
+  ;; context tests
   (define C1 (term (((lambda (x) (lambda (y) x)) hole) 1)))
   (define C2 (term (((lambda (x) (lambda (y) hole)) 0) 1)))
   (define C3 (term (let ([x hole][y 3]) (lambda (a) (a (((x 1) y) 2))))))
@@ -32,13 +33,15 @@
   (test-equal (context? C2) #true)
   (test-equal (context? C3) #true)
   
+  ;; plugging tests
   (define e1 (term (in-hole ,C1 1)))
   (define e2 (term (in-hole ,C2 x)))
   (define e3 (term (in-hole ,C3 (lambda (x) (lambda (y) (lambda (z) x))))))
   
   (test-equal (lambda? e1) #true)
   (test-equal (lambda? e2) #true)
-  (test-equal (lambda? e3) #true))
+  (test-equal (lambda? e3) #true)
+  )
 
 ;; -----------------------------------------------------------------------------
 ;; model the λβv calculus, reductions only 
diff --git a/redex-doc/redex/scribblings/long-tut/tue-mor.scrbl b/redex-doc/redex/scribblings/long-tut/tue-mor.scrbl
index 86468ea8..474bc732 100644
--- a/redex-doc/redex/scribblings/long-tut/tue-mor.scrbl
+++ b/redex-doc/redex/scribblings/long-tut/tue-mor.scrbl
@@ -3,6 +3,10 @@
 @(require "shared.rkt"
           racket/runtime-path)
 @(define-runtime-path traces.png "traces.png")
+@(define redex-eval (let ([e (make-base-eval)])
+                      (e '(require redex/reduction-semantics
+                                   redex/scribblings/long-tut/code/common))
+                      e))
 
 @; ---------------------------------------------------------------------------------------------------
 @title[#:tag "tue-mor"]{Reductions and Semantics}
@@ -43,45 +47,21 @@ compatible with all syntactic constructions.
 An alternative and equivalent method is to introduce the notion of a
 context and to use it to generate the reduction relation (or equivalence)
 from the notion of reduction:
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-(require "common.rkt")
-
-(define-extended-language Lambda-calculus Lambda
-  (e ::= .... n)
-  (n ::= natural)
-  (v ::= (lambda (x ...) e))
-   
-  ;; a context is an expression with one hole in lieu of a sub-expression 
-  (C ::=
-     hole
-     (e ... C e ...)
-     (lambda (x_!_ ...) C)))
 
-(define Context? (redex-match? Lambda-calculus C))
+@code-from-file["code/tue-mor.rkt"
+                #rx"define-extended-language"
+                #:eval redex-eval
+                #:exp-count 3]
+@code-from-file["code/tue-mor.rkt"
+                #rx";; context tests"
+                #:exp-count 6]
 
-(module+ test
-  (define C1 (term ((lambda (x y) x) hole 1)))
-  (define C2 (term ((lambda (x y) hole) 0 1)))
-  (test-equal (Context? C1) #true)
-  (test-equal (Context? C2) #true))
-))
 @;%
 Filling the hole of context with an expression yields an expression: 
-@;%
-@(begin
-#reader scribble/comment-reader
-(racketblock
-(module+ test
-  (define e1 (term (in-hole ,C1 1)))
-  (define e2 (term (in-hole ,C2 x)))
+@code-from-file["code/tue-mor.rkt"
+                #rx";; plugging tests"
+                #:exp-count 6]
 
-  (test-equal (in-Lambda/n? e1) #true)
-  (test-equal (in-Lambda/n? e2) #true))
-))
-@;%
 What does filling the hole of a context with a context yield?
 
 @; -----------------------------------------------------------------------------