suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Redex: generation for judgment-form side-conditions

Browse Source 
- 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")
This commit is contained in:
Burke Fetscher 2013-03-06 16:00:05 -06:00
parent 4997800a76
commit 1ed7e8c234
3 changed files with 68 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
collects/redex/private/judgment-form.rkt
View File

@ -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))

13
collects/redex/private/reduction-semantics.rkt
View File

@ -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

54
collects/redex/tests/gen-test.rkt
View File

@ -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)))