svn: r11058

collects/redex/private/reduction-semantics.ss

@@ -131,7 +131,8 @@
                               acc)))]))))))
       (reduction-relation-make-procs red))
      (reduction-relation-rule-names red)
-     (reduction-relation-lws red))))
+     (reduction-relation-lws red)
+     `any)))
 
 (define-syntax (--> stx) (raise-syntax-error '--> "used outside of reduction-relation"))
 (define-syntax (fresh stx) (raise-syntax-error 'fresh "used outside of reduction-relation"))
@@ -187,20 +188,27 @@
 (define-syntax-set (do-reduction-relation)
   (define (do-reduction-relation/proc stx)
     (syntax-case stx ()
-      [(_ id orig-reduction-relation allow-zero-rules? lang args ...)
+      [(_ id orig-reduction-relation allow-zero-rules? lang w/domain-args ...)
        (identifier? #'lang)
-       (with-syntax ([(rules ...) (before-with (syntax (args ...)))]
+       (let-values ([(args domain-pattern)
-                     [(shortcuts ...) (after-with (syntax (args ...)))])
+                     (syntax-case #'(w/domain-args ...) ()
-         (with-syntax ([(lws ...) (map rule->lws (syntax->list #'(rules ...)))])
+                       [(#:domain pat args ...)
-           (reduction-relation/helper 
+                        (values (syntax (args ...)) #'pat)]
-            stx
+                       [else
-            (syntax-e #'id)
+                        (values (syntax (w/domain-args ...)) #'any)])])
-            #'orig-reduction-relation
+         (with-syntax ([(rules ...) (before-with args)]
-            (syntax lang)
+                       [(shortcuts ...) (after-with args)])
-            (syntax->list (syntax (rules ...)))
+           (with-syntax ([(lws ...) (map rule->lws (syntax->list #'(rules ...)))])
-            (syntax->list (syntax (shortcuts ...)))
+             (reduction-relation/helper 
-            #'(list lws ...)
+              stx
-            (syntax-e #'allow-zero-rules?))))]
+              (syntax-e #'id)
+              #'orig-reduction-relation
+              (syntax lang)
+              (syntax->list (syntax (rules ...)))
+              (syntax->list (syntax (shortcuts ...)))
+              #'(list lws ...)
+              (syntax-e #'allow-zero-rules?)
+              domain-pattern))))]
       [(_ id orig-reduction-relation lang args ...)
        (raise-syntax-error (syntax-e #'id) 
                            "expected an identifier for the language name"
@@ -311,7 +319,7 @@
                                          (to-lw where-expr))
                                    ...))))]))
   
-  (define (reduction-relation/helper stx orig-name orig-red-expr lang-id rules shortcuts lws allow-zero-rules?)
+  (define (reduction-relation/helper stx orig-name orig-red-expr lang-id rules shortcuts lws allow-zero-rules? domain-pattern)
     (let ([ht (make-module-identifier-mapping)]
           [all-top-levels '()]
           [withs (make-module-identifier-mapping)])
@@ -370,17 +378,27 @@
                         (for-each loop nexts)))))
                 all-top-levels)
       
-      (let ([name-ht (make-hasheq)])
+      (let ([name-ht (make-hasheq)]
+            [lang-nts (language-id-nts lang-id orig-name)])
         (with-syntax ([lang-id lang-id]
                       [(top-level ...) (get-choices stx orig-name ht lang-id (syntax -->) name-ht lang-id allow-zero-rules?)]
                       [(rule-names ...) (hash-map name-ht (λ (k v) k))]
-                      [lws lws])
+                      [lws lws]
+                      
+                      [domain-pattern-side-conditions-rewritten
+                       (rewrite-side-conditions/check-errs
+                        lang-nts
+                        orig-name
+                        #t
+                        domain-pattern)])
+                      
           #`(build-reduction-relation
              #,orig-red-expr
              lang-id
              (list top-level ...)
              '(rule-names ...)
-             lws)))))
+             lws
+             `domain-pattern-side-conditions-rewritten)))))
   
   #|    
     ;; relation-tree = 
@@ -653,7 +671,8 @@
      first-lang
      (reverse (apply append (map reduction-relation-make-procs lst)))
      (hash-map name-ht (λ (k v) k))
-     (apply append (map reduction-relation-lws lst)))))
+     (apply append (map reduction-relation-lws lst))
+     `any)))
 
 (define (do-node-match lhs-frm-id lhs-to-id pat rhs-proc child-make-proc)
   ;; need call to make-rewrite-proc

collects/redex/private/struct.ss

@@ -40,7 +40,9 @@
                                                           '()
                                                           '()))
 
-(define (build-reduction-relation orig-reduction-relation lang make-procs rule-names lws)
+;; the domain pattern isn't actually used here.
+;; I started to add it, but didn't finish. -robby
+(define (build-reduction-relation orig-reduction-relation lang make-procs rule-names lws domain-pattern)
   (cond
     [orig-reduction-relation
      (let* ([new-names (map rewrite-proc-name make-procs)]

collects/redex/private/tl-test.ss

@@ -406,7 +406,8 @@
     (define-metafunction x-lang
       f : x x -> x
       [(f x_1 x_2) x_1])
-    (test (term (f p q)) (term p)))
+    (test (term (f p q)) (term p))
+    (test (in-domain? (f p q)) #t))
   
 
 ;                                                                                                                                

collects/redex/redex.scrbl

@@ -486,8 +486,10 @@ is signaled. If no patterns match, an error is signaled.
 }
 
 @defform/subs[#:literals (--> fresh side-condition where) 
-              (reduction-relation language reduction-case ...)
+              (reduction-relation language domain reduction-case ...)
-              ((reduction-case (--> pattern exp extras ...))
+              ((domain (code:line) 
+	               (code:line #:domain pattern))
+               (reduction-case (--> pattern exp extras ...))
                (extras name
                        (fresh <fresh-clause> ...)
                        (side-condition <guard> ...)
@@ -727,24 +729,34 @@ legtimate inputs according to @scheme[metafunction-name]'s contract,
 and @scheme[#f] otherwise.
 }
 
-> (test-equal e1 e2)                            SYNTAX
+@defidform[-->]{ Recognized specially within
+  @scheme[reduction-relation]. A @scheme[-->] form is an
+  error elsewhere.  }
 
-Tests to see if e1 is equal to e2.
+@defidform[fresh]{ Recognized specially within
+  @scheme[reduction-relation]. A @scheme[-->] form is an
+  error elsewhere.  }
 
-> (test--> reduction-relation e1 e2 ...)        SYNTAX
+@defform[(test-equal e1 e2)]{
 
-Tests to see if the value of e1 (which should be a term),
+Tests to see if @scheme[e1] is equal to @scheme[e2].
-reduces to the e2s.
+}
 
-> (test-predicate p? e)                         SYNTAX
+@defform[(test--> reduction-relation e1 e2 ...)]{
 
-Tests to see if the value of `e' matches the predicate p?.
+Tests to see if the value of @scheme[e1] (which should be a term),
+reduces to the @scheme[e2]s under @scheme[reduction-relation].
+}
 
-> test-results :: (-> void?)
+@defform[(test-predicate p? e)]{
+Tests to see if the value of @scheme[e] matches the predicate @scheme[p?].
+}
 
+@defproc[(test-results) void?]{
 Prints out how many tests passed and failed, and resets the
 counters so that next time this function is called, it
 prints the test results for the next round of tests.
+}
 
 > plug :: (any? any? . -> . any)