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

add redex-generator form and some tests

Browse Source 
update examples/generate-types
This commit is contained in:
Burke Fetscher 2012-11-01 11:28:46 -05:00
parent ee97c08e0a
commit e6ab32593e
4 changed files with 97 additions and 48 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
collects/redex/examples/define-judgment-form/generate-types.rkt
View File

@ -3,10 +3,12 @@
(require redex/pict
redex/reduction-semantics)
(provide (all-defined-out))
;; This file makes some small changes to the system in
;; typing-rules.rkt (in the same directory) to allow generation
;; of terms that satisfy the "typeof" judgment-form. Specifically,
;; since gerenation of this type doesn't yet support ellipses,
;; since this kind of random generation doesn't yet support ellipses,
;; they have to be eliminated form the judgment-form and the
;; metafunctions it depends on.
@ -75,7 +77,7 @@
(typeof () e τ)
5))
(define (test-some-terms n)
(define (random-terms n)
(for/list ([_ n])
(match (random-typed-term)
[`(typeof () ,e ,t)
@ -84,5 +86,3 @@
(error 'typeof "non-unique types: ~s in ~s\n" types e))
(test-equal (car types) t)
e])))
(test-some-terms 15)

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

@ -353,9 +353,9 @@
(syntax-case #'rest ()
[()
#`(λ (size)
(generate-jf-pat (jf/mf-id . args) size))]
(generate-jf-pat language (jf/mf-id . args) size))]
[(size)
#'(generate-jf-pat (jf/mf-id . args) size)]
#'(generate-jf-pat language (jf/mf-id . args) size)]
[(x . y) (raise-syntax-error 'generate-term
"#:satisfying does not yet support additional keyword arguments"
stx #'x)])]
@ -405,24 +405,67 @@
(syntax-case stx ()
[(g-m-p lang-id (mf-name . lhs-pats) rhs-pat size)
#`(parameterize ([unsupported-pat-err-name 'generate-term])
((get-mf-generator lang-id (mf-name . lhs-pats) rhs-pat size)))]))
((make-redex-generator lang-id (mf-name . lhs-pats) = rhs-pat size)))]))
(define-syntax (generate-jf-pat stx)
(syntax-case stx ()
[(g-p (jf-name . pat-raw) size)
[(g-j-p lang-id (jf-name . pat-raw) size)
#`(parameterize ([unsupported-pat-err-name 'generate-term])
((get-jf-generator (jf-name . pat-raw) size)))]))
((make-redex-generator lang-id (jf-name . pat-raw) size)))]))
(define-syntax (get-jf-generator stx)
(define-syntax (redex-generator stx)
(syntax-case stx ()
[(g-j-g (jf-name . pat-raw) size)
(let* ([j-f (lookup-judgment-form-id #'jf-name)]
[lang (judgment-form-lang j-f)]
[clauses (judgment-form-gen-clauses j-f)]
[nts (definition-nts lang stx 'generate-term)])
(with-syntax ([(pat (names ...) (names/ellipses ...))
(rewrite-side-conditions/check-errs nts 'generate-term #t #'pat-raw)])
#`(make-jf-gen/proc 'jf-name #,clauses #,lang 'pat size)))]))
[(form-name args ...)
#`(#%expression (make-redex-generator args ...))]))
(define-syntax (make-redex-generator stx)
(syntax-case stx ()
[(_ lang-id (jf/mf-id . args) . rest)
(cond
[(judgment-form-id? #'jf/mf-id)
(syntax-case #'rest ()
[(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)])
(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)))]
[_
(raise-syntax-error 'redex-generator
"expected an integer depth bound"
stx
#'rest)])]
[(metafunc #'jf/mf-id)
(syntax-case #'rest ()
[(= res size)
(and (identifier? #'=)
(equal? '= (syntax->datum #'=)))
(let ()
(define mf (syntax-local-value #'jf/mf-id (λ () #f)))
(define nts (definition-nts #'lang-id stx 'redex-generator))
(with-syntax ([(lhs-pat (lhs-names ...) (lhs-names/ellipses ...))
(rewrite-side-conditions/check-errs nts (syntax-e #'g-m-p) #t #'args)]
[(rhs-pat (rhs-names ...) (rhs-names/ellipses ...))
(rewrite-side-conditions/check-errs nts (syntax-e #'g-m-p) #t #'res)]
[mf-id (term-fn-get-id mf)])
#`(make-mf-gen/proc 'mf-id mf-id lang-id 'lhs-pat 'rhs-pat size)))]
[_
(raise-syntax-error 'redex-generator
"expected \"=\" followed by a result pattern and an integer depth bound"
stx
#'rest)])]
[else
(raise-syntax-error 'redex-generator
"expected either a metafunction or a judgment-form identifier"
stx
#'jf/mf-id)])]
[(_ not-lang-id . rest)
(not (identifier? #'not-lang-id))
(raise-syntax-error 'redex-generator
"expected an identifier in the language position"
stx
#'not-lang-id)]))
(define (make-jf-gen/proc jf-id mk-clauses lang pat size)
(define gen (search/next (mk-clauses) pat size lang))
@ -437,21 +480,6 @@
(parameterize ([current-logger generation-logger])
(termify (gen)))))
(define-syntax (get-mf-generator stx)
(syntax-case stx ()
[(g-m-g lang-id (mf-name . lhs-pats) rhs-pat size)
(let ()
(define mf (syntax-local-value #'mf-name (λ () #f)))
(unless (term-fn? mf)
(raise-syntax-error 'generate-mf-pat "expected an identifier bound to a metafunction" stx #'mf-name))
(define nts (language-id-nts #'lang-id (syntax-e #'g-m-p)))
(with-syntax ([(lhs-pat (lhs-names ...) (lhs-names/ellipses ...))
(rewrite-side-conditions/check-errs nts (syntax-e #'g-m-p) #t #'lhs-pats)]
[(rhs-pat (rhs-names ...) (rhs-names/ellipses ...))
(rewrite-side-conditions/check-errs nts (syntax-e #'g-m-p) #t #'rhs-pat)]
[mf-id (term-fn-get-id mf)])
#`(make-mf-gen/proc 'mf-id mf-id lang-id 'lhs-pat 'rhs-pat size)))]))
(define (make-mf-gen/proc fn metafunc-proc lang lhs-pat rhs-pat size)
(define gen (search/next ((metafunc-proc-gen-clauses metafunc-proc))
`(list ,lhs-pat ,rhs-pat)
@ -480,7 +508,6 @@
get-most-recent-trace
update-gen-trace!
exn:fail:redex:generation-failure?
get-jf-generator
get-mf-generator
redex-generator
(struct-out counterexample)
(struct-out exn:fail:redex:test))

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

@ -241,7 +241,7 @@
(test-equal (judgment-holds (typeof ([x_2 int] ([x_1 (int → int)] •)) (x_1 5) int))
#t)
(for ([_ 500])
(for ([_ 100])
(define term (generate-term STLC #:satisfying (typeof Γ e τ) 6))
(match term
[`(typeof ,g ,e ,t)
@ -258,6 +258,17 @@
(test-equal tp `(,t))]
[#f
(void)]))
(define g (redex-generator STLC (typeof • e τ) 5))
(define terms (filter values (for/list ([_ 400]) (g))))
(test-equal (length terms)
(length (remove-duplicates terms)))
(map (match-lambda
[`(typeof ,g ,e ,t)
(define tp (judgment-holds (typeof ,g ,e τ) τ))
(test-equal tp `(,t))])
terms)
(void)
)
(let ()
@ -267,17 +278,17 @@
(n number))
(define-metafunction l
filter : n e -> e
[(filter n •)
fltr : n e -> e
[(fltr n •)
•]
[(filter n (n e))
(filter n e)]
[(filter n (n_0 e))
(n_0 (filter n e))])
[(fltr n (n e))
(fltr n e)]
[(fltr n (n_0 e))
(n_0 (fltr n e))])
(define-judgment-form l
#:mode (filtered I I O)
[(filtered e n (filter n e))])
[(filtered e n (fltr n e))])
(test-equal (generate-term l #:satisfying (filtered (1 (2 (3 (4 •)))) 3 (1 (2 (4 •)))) +inf.0)
'(filtered (1 (2 (3 (4 •)))) 3 (1 (2 (4 •)))))
@ -294,12 +305,23 @@
(void)]))
(for ([_ 50])
(define t (generate-term l #:satisfying (filter n e) e_1 5))
(define t (generate-term l #:satisfying (fltr n e) e_1 5))
(match t
[`((filter ,n ,e) = ,e1)
(test-equal (term (filter ,n ,e)) e1)]
[`((fltr ,n ,e) = ,e1)
(test-equal (term (fltr ,n ,e)) e1)]
[#f
(void)]))
(define g (redex-generator l (fltr n e_1) = e_2 5))
(define terms (filter values (for/list ([_ 50]) (g))))
(test-equal (length terms)
(length (remove-duplicates terms)))
(map (match-lambda
[`((fltr ,n ,e) = ,e1)
(test-equal (term (fltr ,n ,e)) e1)])
terms)
(void)
)
(let ()

4
collects/redex/tests/rg-test.rkt
View File

@ -1301,13 +1301,13 @@
-------------------------
(sum (s n_1) n_2 n_3)])
(test (generate-term L
(test (generate-term nats
#:satisfying
(sum z z n)
5)
'(sum z z z))
(test (generate-term L
(test (generate-term nats
#:satisfying
(sum (s z) (s z) n)
5)