more copied code elimination

Author: rfindler

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

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,214 +72,95 @@ 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.}
 @;
 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]}