From 778981937ae1f1b1408820a2398299abee5ee7d2 Mon Sep 17 00:00:00 2001
From: Robby Findler <robby@racket-lang.org>
Date: Sun, 3 Aug 2008 14:24:04 +0000
Subject: [PATCH] fixed a bug in contract matching for metafunctions

svn: r11048
---
 collects/redex/private/reduction-semantics.ss |  2 +-
 collects/redex/private/tl-test.ss             | 54 +++++++++++++++----
 collects/redex/redex.scrbl                    | 43 ++++++++++++---
 3 files changed, 80 insertions(+), 19 deletions(-)

diff --git a/collects/redex/private/reduction-semantics.ss b/collects/redex/private/reduction-semantics.ss
index b1a9a27710..de51a92e84 100644
--- a/collects/redex/private/reduction-semantics.ss
+++ b/collects/redex/private/reduction-semantics.ss
@@ -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
diff --git a/collects/redex/private/tl-test.ss b/collects/redex/private/tl-test.ss
index 21664c1c9d..a2a4df215b 100644
--- a/collects/redex/private/tl-test.ss
+++ b/collects/redex/private/tl-test.ss
@@ -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))
diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl
index 551549bc3d..89abfcefe1 100644
--- a/collects/redex/redex.scrbl
+++ b/collects/redex/redex.scrbl
@@ -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