diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt index d3e08f1f8e..fcafa37d73 100644 --- a/collects/redex/private/reduction-semantics.rkt +++ b/collects/redex/private/reduction-semantics.rkt @@ -1424,6 +1424,33 @@ defs)) (syntax defs))))))])) +(define-for-syntax (relation-split-out-rhs raw-rhsss orig-stx) + (for/list ([rhss (in-list (syntax->list raw-rhsss))]) + (define rhses '()) + (define sc/wheres '()) + (for ([rhs (in-list (syntax->list rhss))]) + (define (found-one) + (set! sc/wheres (cons rhs sc/wheres))) + (syntax-case rhs (side-condition side-condition/hidden where where/hidden judgment-holds) + [(side-condition . stuff) (found-one)] + [(side-condition/hidden . stuff) (found-one)] + [(where . stuff) (found-one)] + [(where/hidden . stuff) (found-one)] + [(judgment-holds . stuff) (found-one)] + [_ + (cond + [(null? sc/wheres) + (set! rhses (cons rhs rhses))] + [else + (raise-syntax-error 'define-relation + (format "found a '~a' clause not at the end; followed by a normal, right-hand side clause" + (syntax-e (car (syntax-e (car sc/wheres))))) + (last sc/wheres) + #f + (list rhs))])])) + (list (reverse rhses) + (reverse sc/wheres)))) + (define-syntax (generate-metafunction stx) (syntax-case stx () [(_ orig-stx lang prev-metafunction name name-predicate dom-ctcs codom-contracts pats relation? syn-error-name) @@ -1438,7 +1465,10 @@ (with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats] [(lhs-for-lw ...) (lhs-lws pats)]) (with-syntax ([((rhs stuff ...) ...) (if relation? - #'(((AND raw-rhses ...)) ...) + (with-syntax ([(((rhses ...) (where/sc ...)) ...) + (relation-split-out-rhs #'((raw-rhses ...) ...) + #'orig-stx)]) + #'(((AND rhses ...) where/sc ...) ...)) #'((raw-rhses ...) ...))] [(lhs ...) #'((lhs-clauses ...) ...)]) (parse-extras #'((stuff ...) ...)) @@ -2157,7 +2187,9 @@ [(not mtchs) (continue)] [relation? (let ([ans - (ormap (λ (mtch) (ormap values (rhs traced-metafunc (mtch-bindings mtch)))) + (ormap (λ (mtch) + (define rhs-ans (rhs traced-metafunc (mtch-bindings mtch))) + (and rhs-ans (ormap values rhs-ans))) mtchs)]) (unless (ormap (λ (codom-compiled-pattern) (match-pattern codom-compiled-pattern ans)) codom-compiled-patterns) diff --git a/collects/redex/private/rewrite-side-conditions.rkt b/collects/redex/private/rewrite-side-conditions.rkt index 57d0413ea6..587b3bfdb7 100644 --- a/collects/redex/private/rewrite-side-conditions.rkt +++ b/collects/redex/private/rewrite-side-conditions.rkt @@ -44,7 +44,7 @@ (extract-names all-nts what bind-names? orig-stx) (let loop ([term orig-stx]) - (syntax-case term (side-condition variable-except variable-prefix hole name in-hole hide-hole side-condition cross unquote) + (syntax-case term (side-condition variable-except variable-prefix hole name in-hole hide-hole cross unquote) [(side-condition pre-pat (and)) ;; rewriting metafunctions (and possibly other things) that have no where, etc clauses ;; end up with side-conditions that are empty 'and' expressions, so we just toss them here. diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl index 0b0faa51f1..18ce506ad9 100644 --- a/collects/redex/redex.scrbl +++ b/collects/redex/redex.scrbl @@ -701,14 +701,14 @@ otherwise. shortcuts) ([domain (code:line) (code:line #:domain @#,ttpattern)] [base-arrow (code:line) (code:line #:arrow base-arrow-name)] - [reduction-case (arrow-name @#,ttpattern @#,tttterm extras ...)] - [extras rule-name - (fresh fresh-clause ...) - (side-condition racket-expression) - (where @#,ttpattern @#,tttterm) - (judgment-holds (judgment-form-id pat/term ...)) - (side-condition/hidden racket-expression) - (where/hidden @#,ttpattern @#,tttterm)] + [reduction-case (arrow-name @#,ttpattern @#,tttterm red-extras ...)] + [red-extras rule-name + (fresh fresh-clause ...) + (side-condition racket-expression) + (where @#,ttpattern @#,tttterm) + (judgment-holds (judgment-form-id pat/term ...)) + (side-condition/hidden racket-expression) + (where/hidden @#,ttpattern @#,tttterm)] [shortcuts (code:line) (code:line with shortcut ...)] [shortcut [(old-arrow-name @#,ttpattern @#,tttterm) @@ -974,7 +974,7 @@ reduce it further). judgment-holds) (define-metafunction language metafunction-contract - [(name @#,ttpattern ...) @#,tttterm extras ...] + [(name @#,ttpattern ...) @#,tttterm metafunction-extras ...] ...) ([metafunction-contract (code:line) (code:line id : @#,ttpattern ... -> range)] @@ -982,12 +982,12 @@ reduce it further). (code:line @#,ttpattern or range) (code:line @#,ttpattern ∨ range) (code:line @#,ttpattern ∪ range)] - [extras (side-condition racket-expression) - (side-condition/hidden racket-expression) - (where pat @#,tttterm) - (where/hidden pat @#,tttterm) - (judgment-holds - (judgment-form-id pat/term ...))])]{ + [metafunction-extras (side-condition racket-expression) + (side-condition/hidden racket-expression) + (where pat @#,tttterm) + (where/hidden pat @#,tttterm) + (judgment-holds + (judgment-form-id pat/term ...))])]{ The @racket[define-metafunction] form builds a function on sexpressions according to the pattern and right-hand-side @@ -1061,7 +1061,7 @@ match. @defform[(define-metafunction/extension f language metafunction-contract - [(g @#,ttpattern ...) @#,tttterm extras ...] + [(g @#,ttpattern ...) @#,tttterm metafunction-extras ...] ...)]{ Defines a metafunction @racket[g] as an extension of an existing @@ -1271,7 +1271,9 @@ is an error elsewhere. @defform/subs[#:literals (⊂ ⊆ × x) (define-relation language relation-contract - [(name @#,ttpattern ...) @#,tttterm ...] ...) + [(name @#,ttpattern ...) + @#,tttterm ... + metafunction-extras ...] ...) ([relation-contract (code:line) (code:line form-id ⊂ @#,ttpattern x ... x @#,ttpattern) (code:line form-id ⊆ @#,ttpattern × ... × @#,ttpattern)])]{ diff --git a/collects/redex/tests/syn-err-tests/relation-definition.rktd b/collects/redex/tests/syn-err-tests/relation-definition.rktd index f63798e65b..3ff90b76ec 100644 --- a/collects/redex/tests/syn-err-tests/relation-definition.rktd +++ b/collects/redex/tests/syn-err-tests/relation-definition.rktd @@ -12,4 +12,15 @@ (#rx"expected a pattern" ([cross ×]) - (define-relation syn-err-lang foo ⊆ c cross)) \ No newline at end of file + (define-relation syn-err-lang foo ⊆ c cross)) + +(#rx"found a 'where' clause not at the end" + ([first-where (where any_c any_a)] + [first-post-where (R () ())]) + (define-relation syn-err-lang + [(R () ())] + [(R (any_a) (any_b)) + (R anc_c any_d) + first-where + (where any_d any_b) + first-post-where])) diff --git a/collects/redex/tests/test-util.rkt b/collects/redex/tests/test-util.rkt index 693e15caba..bfe6f7db42 100644 --- a/collects/redex/tests/test-util.rkt +++ b/collects/redex/tests/test-util.rkt @@ -83,7 +83,8 @@ (syntax-case stx () [(_ loc-name ... non-loc-name ...) #'body]))]) - (subst loc-piece ... non-loc-piece ...)))])) + (subst loc-piece ... non-loc-piece ...) + (void)))])) (define (source-location stx) (list (syntax-source stx) diff --git a/collects/redex/tests/tl-test.rkt b/collects/redex/tests/tl-test.rkt index 335347b056..c4e9fb99b8 100644 --- a/collects/redex/tests/tl-test.rkt +++ b/collects/redex/tests/tl-test.rkt @@ -1137,6 +1137,49 @@ (test (term (subtype (int int → int) (int num → int))) #f) (test (term (subtype (int num → int) (int int → int))) #t) (test (term (subtype (int int → int) (int int → num))) #t)) + + (let () + (define-relation empty-language + [(R () ())] + [(R (any_a) (any_b)) + (R any_c any_d) + (where any_c any_a) + (where any_d any_b)]) + + (test (term (R () ())) #t) + (test (term (R (()) (()))) #t) + (test (term (R (()) ())) #f)) + + (let () + (define-relation empty-language + [(R () ())] + [(R (any_a) (any_b)) + (R any_c any_d) + (where/hidden any_c any_a) + (where/hidden any_d any_b)]) + + (test (term (R () ())) #t) + (test (term (R (()) (()))) #t) + (test (term (R (()) ())) #f)) + + (let () + (define-relation empty-language + [(R any_a any_b) + (side-condition (equal? (term any_a) + (term any_b)))]) + + (test (term (R (xx) (xx))) #t) + (test (term (R (()) ())) #f)) + + (let () + (define-relation empty-language + [(R any_a any_b) + (side-condition/hidden + (equal? (term any_a) + (term any_b)))]) + + (test (term (R (xx) (xx))) #t) + (test (term (R (()) ())) #f)) (exec-syntax-error-tests "syn-err-tests/relation-definition.rktd")