From e6ab32593e089418b730fc2a998b45ec265cc632 Mon Sep 17 00:00:00 2001 From: Burke Fetscher Date: Thu, 1 Nov 2012 11:28:46 -0500 Subject: [PATCH] add redex-generator form and some tests update examples/generate-types --- .../define-judgment-form/generate-types.rkt | 8 +- collects/redex/private/generate-term.rkt | 89 ++++++++++++------- collects/redex/tests/gen-test.rkt | 44 ++++++--- collects/redex/tests/rg-test.rkt | 4 +- 4 files changed, 97 insertions(+), 48 deletions(-) diff --git a/collects/redex/examples/define-judgment-form/generate-types.rkt b/collects/redex/examples/define-judgment-form/generate-types.rkt index 050cdab50f..0f7c898581 100644 --- a/collects/redex/examples/define-judgment-form/generate-types.rkt +++ b/collects/redex/examples/define-judgment-form/generate-types.rkt @@ -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) diff --git a/collects/redex/private/generate-term.rkt b/collects/redex/private/generate-term.rkt index 1ef069df5e..c4638ca384 100644 --- a/collects/redex/private/generate-term.rkt +++ b/collects/redex/private/generate-term.rkt @@ -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)) diff --git a/collects/redex/tests/gen-test.rkt b/collects/redex/tests/gen-test.rkt index 9d3b62a095..56986c6c9b 100644 --- a/collects/redex/tests/gen-test.rkt +++ b/collects/redex/tests/gen-test.rkt @@ -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 () diff --git a/collects/redex/tests/rg-test.rkt b/collects/redex/tests/rg-test.rkt index ac723e8bb1..5615e98f5a 100644 --- a/collects/redex/tests/rg-test.rkt +++ b/collects/redex/tests/rg-test.rkt @@ -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)