suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

fixed a bug in contract matching for metafunctions

Browse Source 
svn: r11048
This commit is contained in:
Robby Findler 2008-08-03 14:24:04 +00:00
parent 7fbaf9ecce
commit 778981937a
3 changed files with 80 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
collects/redex/private/reduction-semantics.ss
View File

@ -992,7 +992,7 @@
(define (build-metafunction lang patterns rhss old-cps old-rhss wrap dom-contract-pat rng-contract-pat name)
(let ([compiled-patterns (append old-cps
(map (λ (pat) (compile-pattern lang pat #t)) patterns))]
[dom-compiled-pattern (and dom-contract-pat (compile-pattern lang dom-contract-pat #t))]
[dom-compiled-pattern (and dom-contract-pat (compile-pattern lang dom-contract-pat #f))]
[rng-compiled-pattern (compile-pattern lang rng-contract-pat #t)])
(values
(wrap

54
collects/redex/private/tl-test.ss
View File

@ -400,6 +400,14 @@
(where number_3 (+ (term number_1) (term number_2)))])
(test (term (f (11 17))) 28))
(let ()
(define-language x-lang
(x variable))
(define-metafunction x-lang
f : x x -> x
[(f x_1 x_2) x_1])
(test (term (f p q)) (term p)))
;
;
@ -858,16 +866,42 @@
1)
(require (lib "list.ss"))
(define-metafunction lc-lang
free-vars : e -> (listof x)
[(free-vars (e_1 e_2 ...))
,(apply append (term ((free-vars e_1) (free-vars e_2) ...)))]
[(free-vars x_1) ,(list (term x_1))]
[(free-vars (lambda (x_1 ...) e_1))
,(foldr remq (term (free-vars e_1)) (term (x_1 ...)))])
(test (term (free-vars (lambda (x) (x y))))
(list 'y))
(let ()
(define-metafunction lc-lang
free-vars : e -> (listof x)
[(free-vars (e_1 e_2 ...))
(∪ (free-vars e_1) (free-vars e_2) ...)]
[(free-vars x) (x)]
[(free-vars (lambda (x ...) e))
(- (free-vars e) (x ...))])
(define-metafunction lc-lang
∪ : (x ...) ... -> (x ...)
[(∪ (x_1 ...) (x_2 ...) (x_3 ...) ...)
(∪ (x_1 ... x_2 ...) (x_3 ...) ...)]
[(∪ (x_1 ...))
(x_1 ...)]
[(∪) ()])
(define-metafunction lc-lang
- : (x ...) (x ...) -> (x ...)
[(- (x ...) ()) (x ...)]
[(- (x_1 ... x_2 x_3 ...) (x_2 x_4 ...))
(- (x_1 ... x_3 ...) (x_2 x_4 ...))
(side-condition (not (memq (term x_2) (term (x_3 ...)))))]
[(- (x_1 ...) (x_2 x_3 ...))
(- (x_1 ...) (x_3 ...))])
(test (term (∪)) (term ()))
(test (term (∪ (x y) (z a) (b c))) (term (x y z a b c)))
(test (term (- (x y) ())) (term (x y)))
(test (term (- (x y) (x))) (term (y)))
(test (term (- (y x) (x))) (term (y)))
(test (term (- (x x x x x) (x))) (term ()))
(test (term (free-vars (lambda (x) (x y)))) (list 'y))
(test (term (free-vars (a (b (c (d e)))))) (term (a b c d e))))
(test (variable-not-in (term (x y z)) 'x)
(term x1))

43
collects/redex/redex.scrbl
View File

@ -659,17 +659,17 @@ argument to each side-condition should be a Scheme
expression, and the pattern variables in the <pattern> are
bound in that expression.
As an example, this metafunction finds the free variables in
As an example, these metafunctions finds the free variables in
an expression in the lc-lang above:
@schemeblock[
(define-metafunction lc-lang
free-vars : e -> (x ...)
[(free-vars (e_1 e_2 ...))
,(apply append (term ((free-vars e_1) (free-vars e_2) ...)))]
[(free-vars x_1) ,(list (term x_1))]
[(free-vars (lambda (x_1 ...) e_1))
,(foldr remq (term (free-vars e_1)) (term (x_1 ...)))])
(define-metafunction lc-lang
free-vars : e -> (listof x)
[(free-vars (e_1 e_2 ...))
(∪ (free-vars e_1) (free-vars e_2) ...)]
[(free-vars x) (x)]
[(free-vars (lambda (x ...) e))
(- (free-vars e) (x ...))])
]
The first argument to define-metafunction is the grammar
@ -681,6 +681,33 @@ application are the free variables of each of the subterms;
the free variables of a variable is just the variable
itself, and the free variables of a lambda expression are
the free variables of the body, minus the bound parameters.
Here are the helper metafunctions used above.
@schemeblock[
(define-metafunction lc-lang
∪ : (x ...) ... -> (x ...)
[(∪ (x_1 ...) (x_2 ...) (x_3 ...) ...)
(∪ (x_1 ... x_2 ...) (x_3 ...) ...)]
[(∪ (x_1 ...))
(x_1 ...)]
[(∪) ()])
(define-metafunction lc-lang
- : (x ...) (x ...) -> (x ...)
[(- (x ...) ()) (x ...)]
[(- (x_1 ... x_2 x_3 ...) (x_2 x_4 ...))
(- (x_1 ... x_3 ...) (x_2 x_4 ...))
(side-condition (not (memq (term x_2) (term (x_3 ...)))))]
[(- (x_1 ...) (x_2 x_3 ...))
(- (x_1 ...) (x_3 ...))])
]
Note the side-condition in the second case of @scheme[-]. It
ensures that there is a unique match for that case. Without
it, @scheme[(term (- (x x) x))] would lead to an ambiguous
match.
}
@defform[(define-metafunction/extension extending-name language-exp