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

Format relation arguments and results properly for random generation.

Browse Source 
Also rempove some extraneous code in judgment-form.rkt.
This commit is contained in:
Burke Fetscher 2012-11-30 17:06:34 -06:00
parent 42fc3aeda0
commit 7c7c1fbafc
4 changed files with 27 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
collects/redex/private/generate-term.rkt
View File

@ -429,10 +429,20 @@
[(size)
(let* ([j-f (lookup-judgment-form-id #'jf/mf-id)]
[clauses (judgment-form-gen-clauses j-f)]
[nts (definition-nts #'lang-id stx 'redex-generator)])
[nts (definition-nts #'lang-id stx 'redex-generator)]
[relation? (judgment-form-relation? j-f)]
[args-stx (if relation?
(syntax/loc #'args (args))
#'args)])
(with-syntax ([(pat (names ...) (names/ellipses ...))
(rewrite-side-conditions/check-errs nts 'redex-generator #t #'args)])
#`(make-jf-gen/proc 'jf/mf-id #,clauses lang-id 'pat size)))]
(rewrite-side-conditions/check-errs nts 'redex-generator #t args-stx)])
(if relation?
#`(let ([gen-proc (make-jf-gen/proc 'jf/mf-id #,clauses lang-id 'pat size)])
(λ ()
(match (gen-proc)
[`(,jf-name (,trms (... ...)))
`(,jf-name ,@trms)])))
#`(make-jf-gen/proc 'jf/mf-id #,clauses lang-id 'pat size))))]
[_
(raise-syntax-error 'redex-generator
"expected an integer depth bound"

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

@ -1097,32 +1097,7 @@
(λ ()
#,(check-pats
#'(list comp-clauses ...)))))))
#`(values #,(do-compile-judgment-form-proc #'judgment-form-name
#'mode-arg
clauses
rule-names
contracts
nts
#'orig
#'full-def
syn-err-name)
#,(with-syntax* ([(comp-clauses ...)
(map (λ (c) (compile-gen-clause c mode nts syn-err-name
#'judgment-form-name #'lang))
clauses)])
(if (identifier? #'orig)
(with-syntax ([prev-mk (judgment-form-mk-gen-clauses (lookup-judgment-form-id #'orig))])
#`(λ (effective-lang judgment-form-runtime-gen-clauses)
(define mk-prev-clauses (prev-mk effective-lang judgment-form-runtime-gen-clauses))
(λ ()
(append
(mk-prev-clauses)
#,(check-pats
#'(list comp-clauses ...))))))
#`(λ (effective-lang judgment-form-runtime-gen-clauses)
(λ ()
#,(check-pats
#'(list comp-clauses ...))))))))]))
#`(values #,proc-stx #,gen-stx))]))
(define-for-syntax (rewrite-relation-prems clauses)
(map (λ (c)

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

@ -56,6 +56,11 @@
[(sum (s n_1) n_2 (s n_3))
(sum n_1 n_2 n_3)])
(define-relation nats
[(r-sum z n n)]
[(r-sum (s n_1) n_2 (s n_3))
(r-sum n_1 n_2 n_3)])
(test-equal (judgment-holds (sum z (s z) (s z)))
#t)
@ -72,7 +77,11 @@
(match (generate-term nats #:satisfying (sum n_1 n_2 n_3) 5)
[`(sum ,l ,r ,res)
(test-equal (judgment-holds (sum ,l ,r n) n)
`(,res))])))
`(,res))])
(match (generate-term nats #:satisfying (r-sum n_1 n_2 n_3) 5)
[`(r-sum ,l ,r ,res)
(test-equal (term (r-sum ,l ,r ,res))
#t)])))
(let ()

3
collects/redex/tests/tl-test.rkt
View File

@ -3014,6 +3014,9 @@
(parameterize ([relation-coverage (list c)])
(term (f 1))
(test (sorted-counts c) '(1 0 0))))
;; coverage for define-relation not working since
;; it was changed to compile to judgment-form
#;
(let ([c (make-coverage R)])
(parameterize ([relation-coverage (list c)])