From 1ed7e8c23413b9dc490b6c8d118fe369ba383f76 Mon Sep 17 00:00:00 2001 From: Burke Fetscher Date: Wed, 6 Mar 2013 16:00:05 -0600 Subject: [PATCH] Redex: generation for judgment-form side-conditions - enable generation for the above by compiling to a disequation with "#f" - wrap bare terms in relation definitons in side-conditions (require they not be "#f") --- collects/redex/private/judgment-form.rkt | 29 +++++----- .../redex/private/reduction-semantics.rkt | 13 ----- collects/redex/tests/gen-test.rkt | 54 +++++++++++++++++++ 3 files changed, 68 insertions(+), 28 deletions(-) diff --git a/collects/redex/private/judgment-form.rkt b/collects/redex/private/judgment-form.rkt index 10b1c4503a..aa125b3298 100644 --- a/collects/redex/private/judgment-form.rkt +++ b/collects/redex/private/judgment-form.rkt @@ -490,7 +490,7 @@ (define-for-syntax (do-extended-judgment-form lang syn-err-name body orig stx is-relation?) (define nts (definition-nts lang stx syn-err-name)) (define-values (judgment-form-name dup-form-names mode position-contracts clauses rule-names) - (parse-judgment-form-body body syn-err-name stx (identifier? orig))) + (parse-judgment-form-body body syn-err-name stx (identifier? orig) is-relation?)) (define definitions #`(begin (define-syntax #,judgment-form-name @@ -519,7 +519,7 @@ (define-for-syntax (jf-is-relation? jf-id) (judgment-form-relation? (lookup-judgment-form-id jf-id))) -(define-for-syntax (parse-judgment-form-body body syn-err-name full-stx extension?) +(define-for-syntax (parse-judgment-form-body body syn-err-name full-stx extension? is-relation?) (define-syntax-class pos-mode #:literals (I O) (pattern I) @@ -535,10 +535,11 @@ (define-syntax-class horizontal-line (pattern x:id #:when (horizontal-line? #'x))) (define-syntax-class name - (pattern x #:when (or (and (symbol? (syntax-e #'x)) - (not (horizontal-line? #'x)) - (not (eq? '... (syntax-e #'x)))) - (string? (syntax-e #'x))))) + (pattern x #:when (and (not is-relation?) + (or (and (symbol? (syntax-e #'x)) + (not (horizontal-line? #'x)) + (not (eq? '... (syntax-e #'x)))) + (string? (syntax-e #'x)))))) (define (parse-rules rules) (define-values (backward-rules backward-names) (for/fold ([parsed-rules '()] @@ -1357,10 +1358,14 @@ (values (append mf-cs ps-rw) (cons #`(eqn 'pat-rw '#,(car term-rws)) eqs) (append (syntax->datum #'new-names) ns))))] - [(side-cond . rest) + [(side-cond rest) (side-condition-keyword? #'side-cond) - ;; TODO - enable side conditions for judgment form only - (values ps-rw eqs ns)] + (if in-judgment-form? + (let-values ([(term-rws mf-cs) (rewrite-terms (list #'rest) ns)]) + (values (append mf-cs ps-rw) + (cons #`(dqn #f '#,(car term-rws)) eqs) + ns)) + (values ps-rw eqs ns))] [(prem-name . prem-body) (and (judgment-form-id? #'prem-name) in-judgment-form?) (rewrite-jf #'prem-name #'prem-body ns ps-rw eqs)] @@ -1371,12 +1376,6 @@ (eq? '... (syntax-e #'var)) ;; TODO - fix when implementing ellipses (values ps-rw eqs ns)] - [term - (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) - eqs - ns))] [else (raise-syntax-error what "malformed premise" prem)]))) (values prems-rev new-eqs new-names)) diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt index 67d698d0fa..4a816882d2 100644 --- a/collects/redex/private/reduction-semantics.rkt +++ b/collects/redex/private/reduction-semantics.rkt @@ -1387,19 +1387,6 @@ (cons #'lhs-pat prev-lhs-pats))))) (reverse rev-clauses)) -(define-for-syntax (make-rl-clauses lhss rhss nts syn-error-name name lang) - (for/list ([lhs (in-list lhss)] - [rhs (in-list rhss)]) - (with-syntax ([(lhs-pat (names ...) (names/ellipses ...)) - (rewrite-side-conditions/check-errs nts syn-error-name #t lhs)]) - (define-values (ps-rw eqs p-names) - (rewrite-prems #f (syntax->list rhs) nts (syntax->datum #'(names ...)) 'define-relation)) - (with-syntax ([(eq ...) eqs] - [(prem-bod ...) ps-rw]) - #`((clause 'lhs-pat (list eq ...) (list prem-bod ...) #,lang '#,name) - unused-by-relation))))) - - (define-for-syntax (check-arity-consistency mode contracts full-def) (when (and contracts (not (= (length mode) (length contracts)))) (raise-syntax-error diff --git a/collects/redex/tests/gen-test.rkt b/collects/redex/tests/gen-test.rkt index c55d24ce08..26760f40bb 100644 --- a/collects/redex/tests/gen-test.rkt +++ b/collects/redex/tests/gen-test.rkt @@ -605,3 +605,57 @@ (test (with-handlers ([exn:fail? exn-message]) (generate-term L0 #:satisfying (J any_1 any_2) +inf.0)) #rx".*generate-term:.*relation.*")) + +(let () + + (define-syntax-rule (is-not-false e) + (test-equal (not e) #f)) + + (define-syntax-rule (is-false e) + (test-equal e #f)) + + (define-language L0) + + (define-relation L0 + [(R number) + number] + [(R string)]) + + (define-relation L0 + [(R2 number) + #f] + [(R2 string)]) + + (define-relation L0 + [(R3 any) + any]) + + (is-not-false (generate-term L0 #:satisfying (R 5) +inf.0)) + (is-not-false (generate-term L0 #:satisfying (R "hello") +inf.0)) + (is-false (generate-term L0 #:satisfying (R #t) +inf.0)) + (is-false (generate-term L0 #:satisfying (R #f) +inf.0)) + + (is-false (generate-term L0 #:satisfying (R2 5) +inf.0)) + (is-not-false (generate-term L0 #:satisfying (R2 "hello") +inf.0)) + (is-false (generate-term L0 #:satisfying (R2 #t) +inf.0)) + (is-false (generate-term L0 #:satisfying (R2 #f) +inf.0)) + + (is-not-false (generate-term L0 #:satisfying (R3 5) +inf.0)) + (is-not-false (generate-term L0 #:satisfying (R3 "hello") +inf.0)) + (is-not-false (generate-term L0 #:satisfying (R3 #t) +inf.0)) + (is-false (generate-term L0 #:satisfying (R3 #f) +inf.0)) + + + (define-judgment-form L0 + #:mode (J I) + [(J (any)) + (side-condition any)] + [(J (any_1 any_2)) + (J any_1) + (J any_2)]) + + (is-not-false (generate-term L0 #:satisfying (J (1)) +inf.0)) + (is-not-false (generate-term L0 #:satisfying (J ((1) (2))) +inf.0)) + (is-false (generate-term L0 #:satisfying (J ((1) (#f))) 5)) + (is-false (generate-term L0 #:satisfying (J ((#f) (2))) 5)) + (is-not-false (generate-term L0 #:satisfying (J ((#t) (2))) 5))) \ No newline at end of file