From 3d5178bcb0b2a11903081f3e5a7c0947ef70d3fc Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Thu, 1 Nov 2012 14:38:36 -0500 Subject: [PATCH] adjust generate-term so that it has an '=' in its concrete syntax when generating something from a metafunction export redex-generator (and add docs) rename generate-types.rkt to typing-rules-no-ellipses.rkt --- ...types.rkt => typing-rules-no-ellipses.rkt} | 29 +++++---- collects/redex/private/generate-term.rkt | 15 +++-- collects/redex/private/judgment-form.rkt | 2 +- collects/redex/reduction-semantics.rkt | 1 + collects/redex/scribblings/ref.scrbl | 24 ++++++- collects/redex/tests/gen-test.rkt | 63 +++++++++---------- collects/redex/tests/rg-test.rkt | 6 +- 7 files changed, 86 insertions(+), 54 deletions(-) rename collects/redex/examples/define-judgment-form/{generate-types.rkt => typing-rules-no-ellipses.rkt} (71%) diff --git a/collects/redex/examples/define-judgment-form/generate-types.rkt b/collects/redex/examples/define-judgment-form/typing-rules-no-ellipses.rkt similarity index 71% rename from collects/redex/examples/define-judgment-form/generate-types.rkt rename to collects/redex/examples/define-judgment-form/typing-rules-no-ellipses.rkt index 0f7c898581..22cff83039 100644 --- a/collects/redex/examples/define-judgment-form/generate-types.rkt +++ b/collects/redex/examples/define-judgment-form/typing-rules-no-ellipses.rkt @@ -8,9 +8,8 @@ ;; 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 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. +;; since generation doesn't yet support ellipses, they have to be +;; eliminated from the judgment-form and the metafunctions it depends on. (define-language STLC (e (λ (x τ) e) @@ -77,12 +76,20 @@ (typeof () e τ) 5)) -(define (random-terms n) +(define (random-typed-terms n) + (define gen-one (redex-generator STLC (typeof () e τ) 5)) (for/list ([_ n]) - (match (random-typed-term) - [`(typeof () ,e ,t) - (define types (judgment-holds (typeof () ,e τ) τ)) - (unless (= 1 (length types)) - (error 'typeof "non-unique types: ~s in ~s\n" types e)) - (test-equal (car types) t) - e]))) + (extract-term-from-derivation + (gen-one)))) + +(define (extract-term-from-derivation t) + (match t + [`(typeof () ,e ,t) + ;; test to make sure the generator + ;; generated something that the + ;; judgment form actually accepts + (define types (judgment-holds (typeof () ,e τ) τ)) + (unless (= 1 (length types)) + (error 'typeof "non-unique types: ~s in ~s\n" types e)) + (test-equal (car types) t) + e])) diff --git a/collects/redex/private/generate-term.rkt b/collects/redex/private/generate-term.rkt index c4638ca384..cff8ddc97a 100644 --- a/collects/redex/private/generate-term.rkt +++ b/collects/redex/private/generate-term.rkt @@ -341,12 +341,19 @@ (let ([body-code (λ (res size) #`(generate-mf-pat language (jf/mf-id . args) #,res #,size))]) - (syntax-case #'rest () - [(res) + (syntax-case #'rest (=) + [(= res) #`(λ (size) - #,(body-code #'size))] - [(res size) + #,(body-code #'res #'size))] + [(= res size) (body-code #'res #'size)] + [(x . y) + (or (not (identifier? #'x)) + (not (free-identifier=? #'= #'x))) + (raise-syntax-error 'generate-term + "expected to find =" + stx + #'x)] [whatever (signal-error #'whatever)]))))] [(judgment-form-id? #'jf/mf-id) diff --git a/collects/redex/private/judgment-form.rkt b/collects/redex/private/judgment-form.rkt index 2505bc0cfc..b8dfb75502 100644 --- a/collects/redex/private/judgment-form.rkt +++ b/collects/redex/private/judgment-form.rkt @@ -413,7 +413,7 @@ ; Introduce the names before using them, to allow ; judgment form definition at the top-level. #`(begin - (define-syntaxes (judgment-form-runtime-proc judgment-form-lws) (values)) + (define-syntaxes (judgment-form-runtime-proc judgment-form-lws judgment-runtime-gen-clauses) (values)) #,definitions) definitions)) 'disappeared-use diff --git a/collects/redex/reduction-semantics.rkt b/collects/redex/reduction-semantics.rkt index 7fb73dae3b..c292e58cc1 100644 --- a/collects/redex/reduction-semantics.rkt +++ b/collects/redex/reduction-semantics.rkt @@ -64,6 +64,7 @@ generate-term check-metafunction check-reduction-relation + redex-generator exn:fail:redex:generation-failure? (struct-out exn:fail:redex:test) (struct-out counterexample)) diff --git a/collects/redex/scribblings/ref.scrbl b/collects/redex/scribblings/ref.scrbl index deb7b1213e..eda7ec61c1 100644 --- a/collects/redex/scribblings/ref.scrbl +++ b/collects/redex/scribblings/ref.scrbl @@ -1641,7 +1641,7 @@ metafunctions or unnamed reduction-relation cases) to application counts.} (generate-term term-spec)] ([term-spec (code:line language @#,ttpattern) (code:line language #:satisfying (judgment-form-id @#,ttpattern ...)) - (code:line language #:satisfying (metafunction-id @#,ttpattern ...) @#,ttpattern) + (code:line language #:satisfying (metafunction-id @#,ttpattern ...) = @#,ttpattern) (code:line #:source metafunction) (code:line #:source relation-expr)] [kw-args (code:line #:attempt-num attempts-expr) @@ -1824,6 +1824,27 @@ term that does not match @racket[pattern].} (add1 (abs n))) #:attempts 3)] +@defform/subs[(redex-generator language-id satisfying size-expr) + ([satisfying (judgment-form-id @#,ttpattern ...) + (code:line (metafunction-id @#,ttpattern ...) = @#,ttpattern)]) + #:contracts ([size-expr natural-number/c])]{ + + @italic{WARNING: @racket[redex-generator] is a new, experimental form, + and its API may change.} + + Returns a thunk that, each time it is called, either generates a random + s-expression based on @racket[satisfying] or fails to (and returns @racket[#f]). + The terms returned by a particular thunk are guaranteed to be distinct. + + @examples[#:eval + redex-eval + (define gen-sum (redex-generator nats (sum n_1 n_2 n_3) 5)) + (gen-sum) + (gen-sum) + (gen-sum) + (gen-sum)] +} + @defstruct[counterexample ([term any/c]) #:inspector #f]{ Produced by @racket[redex-check], @racket[check-reduction-relation], and @racket[check-metafunction] when testing falsifies a property.} @@ -1834,6 +1855,7 @@ Raised by @racket[redex-check], @racket[check-reduction-relation], and The @racket[exn:fail:redex:test-source] component contains the exception raised by the property, and the @racket[exn:fail:redex:test-term] component contains the term that induced the exception.} + @defform/subs[(check-reduction-relation relation property kw-args ...) ([kw-arg (code:line #:attempts attempts-expr) (code:line #:retries retries-expr) diff --git a/collects/redex/tests/gen-test.rkt b/collects/redex/tests/gen-test.rkt index 3983f848a6..a3a12c94a0 100644 --- a/collects/redex/tests/gen-test.rkt +++ b/collects/redex/tests/gen-test.rkt @@ -133,8 +133,7 @@ (test-equal (generate-term STLC #:satisfying - (lookup x ([x int] ([x (int → int)] •))) - (int → int) + (lookup x ([x int] ([x (int → int)] •))) = (int → int) 6) #f)) @@ -317,7 +316,7 @@ (void)])) (for ([_ 50]) - (define t (generate-term l #:satisfying (fltr n e) e_1 5)) + (define t (generate-term l #:satisfying (fltr n e) = e_1 5)) (match t [`((fltr ,n ,e) = ,e1) (test-equal (term (fltr ,n ,e)) e1)] @@ -332,9 +331,7 @@ [`((fltr ,n ,e) = ,e1) (test-equal (term (fltr ,n ,e)) e1)]) terms) - (void) - - ) + (void)) (let () @@ -360,30 +357,30 @@ [(is-a/b/c/d/e? e) T]) - (test-equal (generate-term L #:satisfying (is-a? a) any +inf.0) + (test-equal (generate-term L #:satisfying (is-a? a) = any +inf.0) '((is-a? a) = T)) - (test-equal (generate-term L #:satisfying (is-a? b) any +inf.0) + (test-equal (generate-term L #:satisfying (is-a? b) = any +inf.0) '((is-a? b) = F)) - (test-equal (generate-term L #:satisfying (is-a? c) any +inf.0) + (test-equal (generate-term L #:satisfying (is-a? c) = any +inf.0) '((is-a? c) = F)) - (test-equal (generate-term L #:satisfying (is-a/b? a) any +inf.0) + (test-equal (generate-term L #:satisfying (is-a/b? a) = any +inf.0) '((is-a/b? a) = T)) - (test-equal (generate-term L #:satisfying (is-a/b? b) any +inf.0) + (test-equal (generate-term L #:satisfying (is-a/b? b) = any +inf.0) '((is-a/b? b) = T)) - (test-equal (generate-term L #:satisfying (is-a/b? c) any +inf.0) + (test-equal (generate-term L #:satisfying (is-a/b? c) = any +inf.0) '((is-a/b? c) = F)) - (test-equal (generate-term L #:satisfying (is-a/b/c/d/e? a) any +inf.0) + (test-equal (generate-term L #:satisfying (is-a/b/c/d/e? a) = any +inf.0) '((is-a/b/c/d/e? a) = T)) - (test-equal (generate-term L #:satisfying (is-a/b/c/d/e? b) any +inf.0) + (test-equal (generate-term L #:satisfying (is-a/b/c/d/e? b) = any +inf.0) '((is-a/b/c/d/e? b) = T)) - (test-equal (generate-term L #:satisfying (is-a/b/c/d/e? c) any +inf.0) + (test-equal (generate-term L #:satisfying (is-a/b/c/d/e? c) = any +inf.0) '((is-a/b/c/d/e? c) = T)) - (test-equal (generate-term L #:satisfying (is-a/b/c/d/e? d) any +inf.0) + (test-equal (generate-term L #:satisfying (is-a/b/c/d/e? d) = any +inf.0) '((is-a/b/c/d/e? d) = T)) - (test-equal (generate-term L #:satisfying (is-a/b/c/d/e? e) any +inf.0) + (test-equal (generate-term L #:satisfying (is-a/b/c/d/e? e) = any +inf.0) '((is-a/b/c/d/e? e) = T)) - (test-equal (generate-term L #:satisfying (is-a/b/c/d/e? f) any +inf.0) + (test-equal (generate-term L #:satisfying (is-a/b/c/d/e? f) = any +inf.0) '((is-a/b/c/d/e? f) = F))) ;; errors for unsupprted pats @@ -394,7 +391,7 @@ (define-metafunction L [(f n) (g n)]) (test (with-handlers ((exn:fail? exn-message)) - (generate-term L #:satisfying (f any) any +inf.0) + (generate-term L #:satisfying (f any) = any +inf.0) "didn't raise an exception") #rx".*generate-term:.*side-condition.*")) (let () @@ -404,7 +401,7 @@ (define-metafunction L [(f n) (g n)]) (test (with-handlers ((exn:fail? exn-message)) - (generate-term L #:satisfying (f any) any +inf.0) + (generate-term L #:satisfying (f any) = any +inf.0) "didn't raise an exception") #rx".*generate-term:.*repeat.*")) @@ -441,7 +438,7 @@ (where q_3 (f q_2))]) (test (with-handlers ([exn:fail? exn-message]) - (generate-term L #:satisfying (f r_1) r_2 +inf.0)) + (generate-term L #:satisfying (f r_1) = r_2 +inf.0)) #rx".*generate-term:.*undatum.*")) @@ -451,7 +448,7 @@ [(n any) any]) (define-metafunction L [(f n) (n 1)]) - (test-equal (generate-term L #:satisfying (f any_1) any_2 +inf.0) + (test-equal (generate-term L #:satisfying (f any_1) = any_2 +inf.0) '((f 2) = (2 1)))) (let () @@ -460,7 +457,7 @@ [(n any) any]) (define-metafunction L [(f n) n]) - (test-equal (generate-term L #:satisfying (f any_1) any_2 +inf.0) + (test-equal (generate-term L #:satisfying (f any_1) = any_2 +inf.0) '((f 2) = 2))) (let () @@ -477,25 +474,25 @@ [(t n_1 n_2) 4]) - (test-equal (generate-term l #:satisfying (t 1 1) 1 +inf.0) + (test-equal (generate-term l #:satisfying (t 1 1) = 1 +inf.0) '((t 1 1) = 1)) - (test-equal (generate-term l #:satisfying (t 1 1) 2 +inf.0) + (test-equal (generate-term l #:satisfying (t 1 1) = 2 +inf.0) #f) - (test-equal (generate-term l #:satisfying (t 1 2) 2 +inf.0) + (test-equal (generate-term l #:satisfying (t 1 2) = 2 +inf.0) '((t 1 2) = 2)) - (test-equal (generate-term l #:satisfying (t 1 2) 3 +inf.0) + (test-equal (generate-term l #:satisfying (t 1 2) = 3 +inf.0) #f) - (test-equal (generate-term l #:satisfying (t 1 3) 3 +inf.0) + (test-equal (generate-term l #:satisfying (t 1 3) = 3 +inf.0) '((t 1 3) = 3)) - (test-equal (generate-term l #:satisfying (t 1 3) 4 +inf.0) + (test-equal (generate-term l #:satisfying (t 1 3) = 4 +inf.0) #f) - (test-equal (generate-term l #:satisfying (t 6 7) 4 +inf.0) + (test-equal (generate-term l #:satisfying (t 6 7) = 4 +inf.0) '((t 6 7) = 4)) - (test-equal (generate-term l #:satisfying (t 6 7) 3 +inf.0) + (test-equal (generate-term l #:satisfying (t 6 7) = 3 +inf.0) #f) - (test-equal (generate-term l #:satisfying (t 6 7) 2 +inf.0) + (test-equal (generate-term l #:satisfying (t 6 7) = 2 +inf.0) #f) - (test-equal (generate-term l #:satisfying (t 6 7) 1 +inf.0) + (test-equal (generate-term l #:satisfying (t 6 7) = 1 +inf.0) #f)) #; diff --git a/collects/redex/tests/rg-test.rkt b/collects/redex/tests/rg-test.rkt index 5615e98f5a..e322321d3b 100644 --- a/collects/redex/tests/rg-test.rkt +++ b/collects/redex/tests/rg-test.rkt @@ -1322,15 +1322,13 @@ (test (generate-term nats #:satisfying - (sum z z) - n + (sum z z) = n 5) '((sum z z) = z)) (test (generate-term nats #:satisfying - (sum (s z) (s z)) - n + (sum (s z) (s z)) = n 5) '((sum (s z) (s z)) = (s (s z)))))