diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt index fcafa37d73..d384888941 100644 --- a/collects/redex/private/reduction-semantics.rkt +++ b/collects/redex/private/reduction-semantics.rkt @@ -1874,8 +1874,10 @@ [nts (definition-nts lang stx syn-err-name)] [judgment (syntax-case stx () [(_ judgment _) #'judgment])]) (check-judgment-arity judgment) - (bind-withs syn-err-name '() lang nts (list judgment) - 'flatten #`(list (term #,#'tmpl)) '() '()))] + #`(sort #,(bind-withs syn-err-name '() lang nts (list judgment) + 'flatten #`(list (term #,#'tmpl)) '() '()) + string<=? + #:key (λ (x) (format "~s" x))))] [(_ (not-form-name . _) . _) (not (judgment-form-id? #'form-name)) (raise-syntax-error #f "expected a judgment form name" stx #'not-form-name)])) @@ -1909,18 +1911,14 @@ [compiled-output-ctcs #,(contracts-compilation output-contracts)]) (λ (input) (check-judgment-form-contract `#,name input compiled-input-ctcs 'I '#,mode) - (define mtchs (match-pattern compiled-lhs input)) - (define outputs - (if mtchs - (for/fold ([outputs '()]) ([m mtchs]) - (define os - (term-let ([names/ellipses (lookup-binding (mtch-bindings m) 'names)] ...) - #,body)) - (if os (append os outputs) outputs)) - '())) - (for ([output outputs]) - (check-judgment-form-contract `#,name output compiled-output-ctcs 'O '#,mode)) - outputs))))])) + (combine-judgment-rhses + compiled-lhs + input + (λ (m) + (term-let ([names/ellipses (lookup-binding (mtch-bindings m) 'names)] ...) + #,body)) + (λ (output) + (check-judgment-form-contract `#,name output compiled-output-ctcs 'O '#,mode)))))))])) (with-syntax ([(clause-proc ...) (map compile-clause clauses)] [(clause-proc-ids ...) (generate-temporaries clauses)]) (with-syntax ([(backwards-ids ...) (reverse (syntax->list #'(clause-proc-ids ...)))]) @@ -1928,6 +1926,22 @@ (λ (input) (append (backwards-ids input) ...)))))) +(define (combine-judgment-rhses compiled-lhs input rhs check-output) + (define mtchs (match-pattern compiled-lhs input)) + (cond + [mtchs + (define output-table (make-hash)) + (for ([m (in-list mtchs)]) + (define os (rhs m)) + (when os + (for ([x (in-list os)]) + (hash-set! output-table x #t)))) + (define outputs (hash-map output-table (λ (k v) k))) + (for ([output (in-list outputs)]) + (check-output output)) + outputs] + [else '()])) + (define-for-syntax (do-compile-judgment-form-lws clauses) (syntax-case clauses () [(((_ . conc-body) . prems) ...) diff --git a/collects/redex/tests/tl-test.rkt b/collects/redex/tests/tl-test.rkt index c4e9fb99b8..236f498e83 100644 --- a/collects/redex/tests/tl-test.rkt +++ b/collects/redex/tests/tl-test.rkt @@ -2018,8 +2018,8 @@ (test (judgment-holds (sumo n_1 n_2 z) ([,'n_1 n_1] [,'n_2 n_2])) (list (term ([n_1 z] [n_2 z])))) (test (judgment-holds (sumo n_1 n_2 (s z)) ([,'n_1 n_1] [,'n_2 n_2])) - (list (term ([n_1 z] [n_2 (s z)])) - (term ([n_1 (s z)] [n_2 z])))) + (list (term ([n_1 (s z)] [n_2 z])) + (term ([n_1 z] [n_2 (s z)])))) (define-judgment-form nats #:mode (sumo-ls O O I) @@ -2043,7 +2043,7 @@ [(member n_i (n_0 ... n_i n_i+1 ...))]) (test (judgment-holds (member n (z (s z) z (s (s z)))) n) - (list (term z) (term (s z)) (term z) (term (s (s z))))) + (list (term (s (s z))) (term (s z)) (term z))) (define-judgment-form nats #:mode (has-zero I) @@ -2122,8 +2122,10 @@ [(map-add-some-noz (n ...) (n_+ ...)) (add-some-noz n n_+) ...]) - (test (judgment-holds (map-add-some-noz (z (s z) (s (s z))) (n ...)) - (n ...)) + (test (sort (judgment-holds (map-add-some-noz (z (s z) (s (s z))) (n ...)) + (n ...)) + string<=? + #:key (λ (x) (format "~s" x))) (list (term (z (s (s z)) (s (s (s z))))) (term (z (s (s z)) (s (s z)))) (term (z (s z) (s (s (s z)))))