diff --git a/collects/redex/private/reduction-semantics.ss b/collects/redex/private/reduction-semantics.ss index de51a92e84..a15b483871 100644 --- a/collects/redex/private/reduction-semantics.ss +++ b/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 ...)))] - [(shortcuts ...) (after-with (syntax (args ...)))]) - (with-syntax ([(lws ...) (map rule->lws (syntax->list #'(rules ...)))]) - (reduction-relation/helper - stx - (syntax-e #'id) - #'orig-reduction-relation - (syntax lang) - (syntax->list (syntax (rules ...))) - (syntax->list (syntax (shortcuts ...))) - #'(list lws ...) - (syntax-e #'allow-zero-rules?))))] + (let-values ([(args domain-pattern) + (syntax-case #'(w/domain-args ...) () + [(#:domain pat args ...) + (values (syntax (args ...)) #'pat)] + [else + (values (syntax (w/domain-args ...)) #'any)])]) + (with-syntax ([(rules ...) (before-with args)] + [(shortcuts ...) (after-with args)]) + (with-syntax ([(lws ...) (map rule->lws (syntax->list #'(rules ...)))]) + (reduction-relation/helper + stx + (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 diff --git a/collects/redex/private/struct.ss b/collects/redex/private/struct.ss index 5eef043219..794a3d1efe 100644 --- a/collects/redex/private/struct.ss +++ b/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)] diff --git a/collects/redex/private/tl-test.ss b/collects/redex/private/tl-test.ss index a2a4df215b..ebc38402aa 100644 --- a/collects/redex/private/tl-test.ss +++ b/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)) ; diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl index 89abfcefe1..7d3cd917e3 100644 --- a/collects/redex/redex.scrbl +++ b/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-case (--> pattern exp extras ...)) + (reduction-relation language domain reduction-case ...) + ((domain (code:line) + (code:line #:domain pattern)) + (reduction-case (--> pattern exp extras ...)) (extras name (fresh ...) (side-condition ...) @@ -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), -reduces to the e2s. +Tests to see if @scheme[e1] is equal to @scheme[e2]. +} -> (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)