diff --git a/collects/redex/private/judgment-form.rkt b/collects/redex/private/judgment-form.rkt index 5a9755dfe2..10b1c4503a 100644 --- a/collects/redex/private/judgment-form.rkt +++ b/collects/redex/private/judgment-form.rkt @@ -1291,11 +1291,13 @@ (free-identifier=? stx (quote-syntax ...)))) (define-for-syntax (where-keyword? id) - (or (free-identifier=? id #'where) - (free-identifier=? id #'where/hidden))) + (and (identifier? id) + (or (free-identifier=? id #'where) + (free-identifier=? id #'where/hidden)))) (define-for-syntax (side-condition-keyword? id) - (or (free-identifier=? id #'side-condition) - (free-identifier=? id #'side-condition/hidden))) + (and (identifier? id) + (or (free-identifier=? id #'side-condition) + (free-identifier=? id #'side-condition/hidden)))) ; ; ; ; @@ -1357,7 +1359,7 @@ (append (syntax->datum #'new-names) ns))))] [(side-cond . rest) (side-condition-keyword? #'side-cond) - ;; TODO - side condition handling + ;; TODO - enable side conditions for judgment form only (values ps-rw eqs ns)] [(prem-name . prem-body) (and (judgment-form-id? #'prem-name) in-judgment-form?) @@ -1370,9 +1372,9 @@ ;; TODO - fix when implementing ellipses (values ps-rw eqs ns)] [term - (not in-judgment-form?) ;; in a relation + (not in-judgment-form?) ;; in a relation ;; TODO - eliminate this (relations become SCs) (let-values ([(term-rws mf-cs) (rewrite-terms (list #'term) ns)]) - (values (append mf-cs ps-rw) + (values (append mf-cs ps-rw) eqs ns))] [else (raise-syntax-error what "malformed premise" prem)]))) @@ -1397,7 +1399,9 @@ [((mf-clauses ...) ...) (map (λ (fs) (map (λ (f-id) (with-syntax ([f-id f-id]) - #'(metafunc-proc-gen-clauses f-id))) + (if (judgment-form-id? #'f-id) + #'(error 'generate-term "generation disabled for relations in term positions") + #'(metafunc-proc-gen-clauses f-id)))) (syntax->list fs))) (syntax->list #'((f ...) ...)))]) (values (syntax->list #'(body-pat ...)) diff --git a/collects/redex/private/term.rkt b/collects/redex/private/term.rkt index 6cc5dbb85f..7a72fec386 100644 --- a/collects/redex/private/term.rkt +++ b/collects/redex/private/term.rkt @@ -70,17 +70,17 @@ [(_ mf) #'(λ (x) (mf x))])) -(define-syntax (mf-map stx) - (syntax-case stx () - [(_ inner-apps) - #'(λ (l) (map inner-apps l))])) - (define-syntax (jf-apply stx) (syntax-case stx () [(_ jf) (judgment-form-id? #'jf) (judgment-form-term-proc (syntax-local-value #'jf (λ () #f)))])) +(define-syntax (mf-map stx) + (syntax-case stx () + [(_ inner-apps) + #'(λ (l) (map inner-apps l))])) + (define-for-syntax currently-expanding-term-fn (make-parameter #f)) @@ -318,7 +318,11 @@ [(mf-apply f) (and (identifier? #'mf-apply) (eq? (syntax-e #'mf-apply) 'mf-apply)) - #'(metafunc f)])) + #'(metafunc f)] + [(jf-apply f) + (and (identifier? #'jf-apply) + (eq? (syntax-e #'jf-apply) 'jf-apply)) + #'(jform f)])) (define-syntax (term-let-fn stx) (syntax-case stx () diff --git a/collects/redex/tests/gen-test.rkt b/collects/redex/tests/gen-test.rkt index 2cf6e17b97..5bc579a718 100644 --- a/collects/redex/tests/gen-test.rkt +++ b/collects/redex/tests/gen-test.rkt @@ -474,7 +474,7 @@ (test (with-handlers ([exn:fail? exn-message]) (generate-term L #:satisfying (f r_1) = r_2 +inf.0)) #rx".*generate-term:.*undatum.*")) - + (let () (define-language L (n 2)) @@ -499,14 +499,14 @@ (define-language l (n number)) (define-metafunction l - [(t n n) - 1] - [(t n 2) - 2] - [(t 1 n) - 3] - [(t n_1 n_2) - 4]) + [(t n n) + 1] + [(t n 2) + 2] + [(t 1 n) + 3] + [(t n_1 n_2) + 4]) (test-equal (generate-term l #:satisfying (t 1 1) = 1 +inf.0) '((t 1 1) = 1)) @@ -567,3 +567,34 @@ (raise e))]) (for ([n 10]) (g))))) + +(let () + (define-language L0) + (define-relation L0 + [(a any)]) + (define-relation L0 + [(b any)]) + (define-relation L0 + [(c any) (a (b any))]) + + (define-metafunction L0 + [(f any) + (a ny)]) + + (define-judgment-form L0 + #:mode (J I O) + [(J any_1 any_2) + (J (a any_1) any_2)] + [(J #t #f)]) + + (test (with-handlers ([exn:fail? exn-message]) + (generate-term L0 #:satisfying (c any) +inf.0)) + #rx".*generate-term:.*relation.*") + + (test (with-handlers ([exn:fail? exn-message]) + (generate-term L0 #:satisfying (f any_1) = any_2 +inf.0)) + #rx".*generate-term:.*relation.*") + + (test (with-handlers ([exn:fail? exn-message]) + (generate-term L0 #:satisfying (J any_1 any_2) +inf.0)) + #rx".*generate-term:.*relation.*")) diff --git a/collects/redex/tests/tl-test.rkt b/collects/redex/tests/tl-test.rkt index 4460150227..95409d4c6f 100644 --- a/collects/redex/tests/tl-test.rkt +++ b/collects/redex/tests/tl-test.rkt @@ -1254,6 +1254,31 @@ (test (term (b 1)) #t) (test (term (b 2)) #t) (test (term (b 3)) #f)) + + (let () + (define-relation empty-language + [(a any)]) + (define-relation empty-language + [(b any)]) + (define-relation empty-language + [(c any) (a (b any))]) + + (define-metafunction empty-language + [(f any) + (c any)]) + + (define-judgment-form empty-language + #:mode (J I O) + [(J any_1 (a any_1))]) + + (test (term (a 1)) #t) + (test (term (b 2)) #t) + (test (term (c 3)) #t) + (test (term (c (b (a x)))) #t) + (test (term (f q)) #t) + (test (judgment-holds (J Z #t)) #t) + (test (judgment-holds (J Z Z)) #f) + ) (exec-syntax-error-tests "syn-err-tests/relation-definition.rktd")