finish uncopying monday afternoon

Author: rfindler

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

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

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]

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,14 +117,16 @@ 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
                                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)
+    (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))]