Skip to content

Commit 8376c2e

Browse files
rfindlerrfindler
committed
more copied code elimination
1 parent 38cdd5a commit 8376c2e

File tree

3 files changed

+127
-214
lines changed

3 files changed

+127
-214
lines changed

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

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,10 +53,12 @@ subst (if time, otherwise it's provide)
5353
;; -----------------------------------------------------------------------------
5454
;; (unique-vars x ...) is the sequence of variables x ... free of duplicates?
5555

56+
;; unique-vars tests start
5657
(module+ test
5758
(test-equal (term (unique-vars x y)) #true)
5859
(test-equal (term (unique-vars x y x)) #false))
5960

61+
;; unique-vars metafunction start
6062
(define-metafunction Lambda
6163
unique-vars : x ... -> boolean
6264
[(unique-vars) #true]
@@ -84,6 +86,7 @@ subst (if time, otherwise it's provide)
8486
(test-equal (term (fv (lambda (x) x))) (term ()))
8587
(test-equal (term (fv (lambda (x) ((y z) x)))) (term (y z))))
8688

89+
;; fv metafunction start
8790
(define-metafunction Lambda
8891
fv : e -> (x ...)
8992
[(fv x) (x)]
@@ -130,9 +133,11 @@ subst (if time, otherwise it's provide)
130133

131134
(define SD? (redex-match? SD e))
132135

136+
;; SD? test case
133137
(module+ test
134138
(test-equal (SD? sd1) #true))
135139

140+
;; SD metafunction
136141
(define-metafunction SD
137142
sd : any -> any
138143
[(sd any) (sd/a any ())])

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

Lines changed: 64 additions & 183 deletions
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ To start a program with Redex, start your file with
2727

2828
The @racket[define-language] from specifies syntax trees via tree grammars:
2929

30-
@codeblock-from-file["code/mon-aft.rkt" #rx"define-language Lambda" #:eval redex-eval]
30+
@code-from-file["code/mon-aft.rkt" #rx"define-language Lambda" #:eval redex-eval]
3131

3232
The trees are somewhat concrete, which makes it easy to work with them, but
3333
it is confusing on those incredibly rare occasions when we want truly
@@ -39,26 +39,26 @@ numbers)---and many other things.
3939

4040
After you have a syntax, use the grammar to generate instances and check
4141
them (typos do sneak in). Instances are generated with @racket[term]:
42-
@codeblock-from-file["code/mon-aft.rkt"
43-
#rx"define e1 [(]term"
44-
#:eval redex-eval
45-
#:exp-count 4
46-
#:extra-code ("e4")]
42+
@code-from-file["code/mon-aft.rkt"
43+
#rx"define e1 [(]term"
44+
#:eval redex-eval
45+
#:exp-count 4
46+
#:extra-code ("e4")]
4747

4848
Mouse over @racket[define]. It is @emph{not} a Redex form, it comes from
4949
Racket. Take a close look at the last definition. Comma anyone?
5050

5151
Define yourself a predicate that tests membership:
52-
@codeblock-from-file["code/mon-aft.rkt" #rx"define in-Lambda[?]" #:eval redex-eval]
52+
@code-from-file["code/mon-aft.rkt" #rx"define in-Lambda[?]" #:eval redex-eval]
5353

5454
Now you can formulate language tests:
55-
@codeblock-from-file["code/mon-aft.rkt" #rx"test-equal [(]in-Lambda[?] e1"
56-
#:eval redex-eval #:exp-count 4]
57-
@codeblock-from-file["code/mon-aft.rkt" #rx"define eb1"
58-
#:eval redex-eval #:exp-count 2]
59-
@codeblock-from-file["code/mon-aft.rkt" #rx"test-equal [(]in-Lambda[?] eb1"
60-
#:eval redex-eval #:exp-count 2
61-
#:extra-code ("(test-results)")]
55+
@code-from-file["code/mon-aft.rkt" #rx"test-equal [(]in-Lambda[?] e1"
56+
#:eval redex-eval #:exp-count 4]
57+
@code-from-file["code/mon-aft.rkt" #rx"define eb1"
58+
#:eval redex-eval #:exp-count 2]
59+
@code-from-file["code/mon-aft.rkt" #rx"test-equal [(]in-Lambda[?] eb1"
60+
#:eval redex-eval #:exp-count 2
61+
#:extra-code ("(test-results)")]
6262

6363
Make sure your language contains the terms that you want and does
6464
@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
7272
specific language.
7373

7474
A first meta-function might determine whether or not some sequence
75-
of variables has any duplicates.
76-
@;%
77-
@(begin
78-
#reader scribble/comment-reader
79-
(racketblock
80-
(define-metafunction Lambda
81-
unique-vars : x ... -> boolean)
82-
))
83-
@;%
84-
The second line is a Redex contract, not a type. It says
75+
of variables has any duplicates. The second line is a Redex contract, not a type. It says
8576
@racket[unique-vars] consumes a sequence of @racket[x]s and produces a
8677
@racket[boolean].
8778

88-
How do we say we don't want repeated variables? With patterns.
89-
@;%
90-
@(begin
91-
#reader scribble/comment-reader
92-
(racketblock
93-
(define-metafunction Lambda
94-
unique-vars : x ... -> boolean
95-
[(unique-vars) #true]
96-
[(unique-vars x x_1 ... x x_2 ...) #false]
97-
[(unique-vars x x_1 ...) (unique-vars x_1 ...)])
98-
))
99-
@;%
100-
Patterns are powerful. More later.
79+
The remaining lines say that we don't want repeated variables with patterns.
80+
@code-from-file["code/mon-aft.rkt"
81+
#rx";; unique-vars metafunction start"
82+
#:eval redex-eval
83+
#:skip-lines 1]
84+
Patterns are powerful. More later.
10185

10286
But, don't just define metafunctions, develop them properly: state what
10387
they are about, work through examples, write down the latter as tests,
10488
@emph{then} define the function.
10589

106-
@;%
107-
@(begin
108-
#reader scribble/comment-reader
109-
(racketblock
110-
;; are the identifiers in the given sequence unique?
111-
112-
(module+ test
113-
(test-equal (term (unique-vars x y)) #true)
114-
(test-equal (term (unique-vars x y x)) #false))
115-
116-
(define-metafunction Lambda
117-
unique-vars : x ... -> boolean
118-
[(unique-vars) #true]
119-
[(unique-vars x x_1 ... x x_2 ...) #false]
120-
[(unique-vars x x_1 ...) (unique-vars x_1 ...)])
121-
122-
(module+ test
123-
(test-results))
124-
))
125-
@;%
126-
Submodules delegate the tests to where they belong and they allow us to
127-
document functions by example.
128-
129-
Here are two more metafunctions that use patterns in interesting ways:
130-
@;%
131-
@(begin
132-
#reader scribble/comment-reader
133-
(racketblock
134-
;; (subtract (x ...) x_1 ...) removes x_1 ... from (x ...)
135-
136-
(module+ test
137-
(test-equal (term (subtract (x y z x) x z)) (term (y))))
13890

139-
(define-metafunction Lambda
140-
subtract : (x ...) x ... -> (x ...)
141-
[(subtract (x ...)) (x ...)]
142-
[(subtract (x ...) x_1 x_2 ...)
143-
(subtract (subtract1 (x ...) x_1) x_2 ...)])
91+
Wrap the tests in a @racket[module+] with the name @racketidfont{test}
92+
to delegate the tests to a submodule where they belong, allowing us to
93+
document functions by example without introducing tests into client modules
94+
that require the module for the definitions:
95+
@;
96+
@code-from-file["code/mon-aft.rkt"
97+
#rx";; unique-vars metafunction start"
98+
#:eval redex-eval
99+
#:skip-lines 1]
144100

145-
;; (subtract1 (x ...) x_1) removes x_1 from (x ...)
146-
(module+ test
147-
(test-equal (term (subtract1 (x y z x) x)) (term (y z))))
148101

149-
(define-metafunction Lambda
150-
subtract1 : (x ...) x -> (x ...)
151-
[(subtract1 (x_1 ... x x_2 ...) x)
152-
(x_1 ... x_2new ...)
153-
(where (x_2new ...) (subtract1 (x_2 ...) x))
154-
(where #false (in x (x_1 ...)))]
155-
[(subtract1 (x ...) x_1) (x ...)])
156-
157-
(define-metafunction Lambda
158-
in : x (x ...) -> boolean
159-
[(in x (x_1 ... x x_2 ...)) #true]
160-
[(in x (x_1 ...)) #false])
102+
Here are two more metafunctions that use patterns in interesting ways:
161103

162-
))
163-
@;%
104+
@code-from-file["code/mon-aft.rkt"
105+
#rx"[(]subtract [(]x [.][.][.][)] x_1 [.][.][.][)] removes"
106+
#:exp-count 4
107+
#:skip-lines 2]
164108

165109
@; -----------------------------------------------------------------------------
166110
@section{Developing a Language 2}
167111

168112
One of the first things a language designer ought to specify is
169113
@deftech{scope}. People often do so with a free-variables function that
170-
specifies which language constructs bind and which ones don't:
171-
@;%
172-
@(begin
173-
#reader scribble/comment-reader
174-
(racketblock
175-
;; (fv e) computes the sequence of free variables of e
176-
;; a variable occurrence of @racket[x] is free in @racket[e]
177-
;; if no @racket[(lambda (x) ...)] @emph{dominates} its occurrence
114+
specifies which language constructs bind and which ones don't.
178115

179-
(module+ test
180-
(test-equal (term (fv x)) (term (x)))
181-
(test-equal (term (fv (lambda (x) x))) (term ()))
182-
(test-equal (term (fv (lambda (x) ((y z) x)))) (term (y z))))
116+
@racket[(fv e)] computes the sequence of free variables of e
117+
a variable occurrence of @racket[x] is free in @racket[e]
118+
if no @racket[(lambda (x) ...)] @emph{dominates} its occurrence
183119

184-
(define-metafunction Lambda
185-
fv : e -> (x ...)
186-
[(fv x) (x)]
187-
[(fv (lambda (x) e_body))
188-
(subtract (x_e ...) x)
189-
(where (x_e ...) (fv e_body))]
190-
[(fv (e_f e_a))
191-
(x_f ... x_a ...)
192-
(where (x_f ...) (fv e_f))
193-
(where (x_a ...) (fv e_a))])
194-
))
195-
@;%
120+
121+
@code-from-file["code/mon-aft.rkt"
122+
#rx"[(]fv e[)] computes the sequence of free variables of e"
123+
#:skip-lines 1]
124+
125+
@code-from-file["code/mon-aft.rkt"
126+
#rx";; fv metafunction start"
127+
#:eval redex-eval
128+
#:skip-lines 1]
196129

197130
@margin-note{You may know it as the de Bruijn index representation.}
198131
@;
199132
The best approach is to specify an α equivalence relation, that is, the
200133
relation that virtually eliminates variables from phrases and replaces them
201134
with arrows to their declarations. In the world of lambda calculus-based
202135
languages, this transformation is often a part of the compiler, the
203-
so-called static-distance phase.
136+
so-called static-distance phase. The function is a good example of
137+
accumulator-functions in Redex.
204138

205-
The function is a good example of accumulator-functions in Redex:
206-
@;%
207-
@(begin
208-
#reader scribble/comment-reader
209-
(racketblock
210-
;; (sd e) computes the static distance version of e
211-
212-
(define-extended-language SD Lambda
213-
(e ::= .... (K n) (lambda e) n)
214-
(n ::= natural))
215-
216-
(define sd1 (term (K 1)))
217-
218-
(define SD? (redex-match? SD e))
219-
220-
(module+ test
221-
(test-equal (SD? sd1) #true))
222-
))
223-
@;%
224139
We have to add a means to the language to say ``arrow back to the variable
225140
declaration.'' We do @emph{not} edit the language definition but
226141
@emph{extend} the language definition instead.
227142

228-
@;%
229-
@(begin
230-
#reader scribble/comment-reader
231-
(racketblock
232-
(define-metafunction SD
233-
sd : e -> e
234-
[(sd e) (sd/a e ())])
235-
236-
(module+ test
237-
(test-equal (term (sd/a x ())) (term x))
238-
(test-equal (term (sd/a x (y z x))) (term (K 2)))
239-
(test-equal (term (sd/a ((lambda (x) x) (lambda (y) y)) ()))
240-
(term ((lambda (K 0)) (lambda (K 0)))))
241-
(test-equal (term (sd/a (lambda (x) (x (lambda (y) y))) ()))
242-
(term (lambda ((K 0) (lambda (K 0))))))
243-
(test-equal (term (sd/a (lambda (z) (lambda (x) (x (lambda (y) z)))) ()))
244-
(term (lambda (lambda ((K 0) (lambda (K 2))))))))
143+
@code-from-file["code/mon-aft.rkt"
144+
#rx"define-extended-language SD Lambda"
145+
#:eval redex-eval
146+
#:exp-count 3]
147+
@code-from-file["code/mon-aft.rkt"
148+
#rx";; SD[?] test case"
149+
#:skip-lines 1]
245150

246-
(define-metafunction SD
247-
sd/a : e (x ...) -> e
248-
[(sd/a x (x_1 ... x x_2 ...))
249-
;; bound variable
250-
(K n)
251-
(where n ,(length (term (x_1 ...))))
252-
(where #false (in x (x_1 ...)))]
253-
[(sd/a (lambda (x) e) (x_rest ...))
254-
(lambda (sd/a e (x x_rest ...)))
255-
(where n ,(length (term (x_rest ...))))]
256-
[(sd/a (e_fun e_arg) (x_rib ...))
257-
((sd/a e_fun (x_rib ...)) (sd/a e_arg (x_rib ...)))]
258-
[(sd/a any_1 (x ...))
259-
;; free variable or constant
260-
any_1])
261-
))
262151
@;%
263152

153+
@code-from-file["code/mon-aft.rkt"
154+
#rx";; SD metafunction"
155+
#:exp-count 3]
156+
264157
Now α equivalence is straightforward:
265-
@;%
266-
@(begin
267-
#reader scribble/comment-reader
268-
(racketblock
269-
;; (=α e_1 e_2) determines whether e_1 and e_2 are α equivalent
270158

271-
(module+ test
272-
(test-equal (term (=α (lambda (x) x) (lambda (y) y))) #true)
273-
(test-equal (term (=α (lambda (x) (x z)) (lambda (y) (y z)))) #true)
274-
(test-equal (term (=α (lambda (x) x) (lambda (y) z))) #false))
275159

276-
(define-metafunction SD
277-
=α : e e -> boolean
278-
[(=α e_1 e_2) ,(equal? (term (sd e_1)) (term (sd e_2)))])
160+
@code-from-file["code/mon-aft.rkt"
161+
#rx"determines whether e_1 and e_2 are α equivalent"
162+
#:exp-count 3]
279163

280-
(define (=α/racket x y) (term (=α ,x ,y)))
281-
))
282-
@;%
283164

284165
@; -----------------------------------------------------------------------------
285166
@section{Extending a Language: @racket[any]}

0 commit comments

Comments
 (0)