From b2ce9f4cd3a3ed2e18773656229612a44d308b0d Mon Sep 17 00:00:00 2001 From: Casey Klein Date: Thu, 9 Oct 2008 19:09:11 +0000 Subject: [PATCH] 1. Fixed bug in reduction-semantics.ss. 2. Fixed bug in generation of 'any pattern. 3. Added `check-metafunction' form. svn: r11984 --- collects/redex/private/reduction-semantics.ss | 11 ++- collects/redex/private/rg-test.ss | 60 ++++++++++--- collects/redex/private/rg.ss | 86 +++++++++++++------ 3 files changed, 119 insertions(+), 38 deletions(-) diff --git a/collects/redex/private/reduction-semantics.ss b/collects/redex/private/reduction-semantics.ss index 39ef1d1a55..b57539df09 100644 --- a/collects/redex/private/reduction-semantics.ss +++ b/collects/redex/private/reduction-semantics.ss @@ -758,7 +758,7 @@ (symbol->string (bind-name y)))))) (define-values (struct:metafunc-proc make-metafunc-proc metafunc-proc? metafunc-proc-ref metafunc-proc-set!) - (make-struct-type 'metafunc-proc #f 8 0 #f null (current-inspector) 0)) + (make-struct-type 'metafunc-proc #f 9 0 #f null (current-inspector) 0)) (define metafunc-proc-pict-info (make-struct-field-accessor metafunc-proc-ref 1)) (define metafunc-proc-lang (make-struct-field-accessor metafunc-proc-ref 2)) (define metafunc-proc-multi-arg? (make-struct-field-accessor metafunc-proc-ref 3)) @@ -766,6 +766,7 @@ (define metafunc-proc-cps (make-struct-field-accessor metafunc-proc-ref 5)) (define metafunc-proc-rhss (make-struct-field-accessor metafunc-proc-ref 6)) (define metafunc-proc-in-dom? (make-struct-field-accessor metafunc-proc-ref 7)) +(define metafunc-proc-dom-pat (make-struct-field-accessor metafunc-proc-ref 8)) (define-struct metafunction (proc)) (define-syntax (in-domain? stx) @@ -865,14 +866,14 @@ (and dom-ctcs (rewrite-side-conditions/check-errs lang-nts - #t 'define-metafunction + #f dom-ctcs))] [codom-side-conditions-rewritten (rewrite-side-conditions/check-errs lang-nts - #t 'define-metafunction + #f codom-contract)] [(rhs-fns ...) (map (λ (lhs rhs bindings) @@ -935,7 +936,8 @@ 'name cps rhss - (let ([name (lambda (x) (name-predicate x))]) name))) + (let ([name (lambda (x) (name-predicate x))]) name) + `dom-side-conditions-rewritten)) `dom-side-conditions-rewritten `codom-side-conditions-rewritten 'name)) @@ -1711,6 +1713,7 @@ metafunc-proc-cps metafunc-proc-rhss metafunc-proc-in-dom? + metafunc-proc-dom-pat (struct-out binds)) diff --git a/collects/redex/private/rg-test.ss b/collects/redex/private/rg-test.ss index d6bca72153..d36b9036cf 100644 --- a/collects/redex/private/rg-test.ss +++ b/collects/redex/private/rg-test.ss @@ -414,6 +414,7 @@ (define-language four (e 4) (f 5)) + (define-language empty) ;; `any' pattern (test (call-with-values (λ () (pick-any four (make-random (list 0 1)))) list) @@ -426,7 +427,10 @@ #:nt (patterns fifth second second second) #:seq (list (λ _ 3)) #:str (list (λ _ "foo") (λ _ "bar") (λ _ "baz")))) - '("foo" "bar" "baz"))) + '("foo" "bar" "baz")) + (test (generate/decisions empty any 5 0 (decisions #:nt (patterns first) + #:var (list (λ _ 'x)))) + 'x)) ;; `hide-hole' pattern (let () @@ -460,19 +464,55 @@ (get-output-string p) (close-output-port p)))) +;; check (let () (define-language lang (d 5) (e e 4)) - (test (current-error-port-output (λ () (check lang d 2 0 #f))) - "failed after 1 attempts: 5") - (test (check lang d 2 0 #t) #t) - (test (check lang (d e) 2 0 (and (eq? (term d) 5) (eq? (term e) 4))) #t) - (test (check lang (d ...) 2 0 (zero? (modulo (foldl + 0 (term (d ...))) 5))) #t) - (test (current-error-port-output (λ () (check lang (d e) 2 0 #f))) - "failed after 1 attempts: (5 4)") - (test (exn:fail-message (check lang d 2 0 (error 'pred-raised))) - #rx"term 5 raises")) + (test (current-error-port-output (λ () (check lang d 2 #f))) + "failed after 1 attempts:\n5\n") + (test (check lang d #t) #t) + (test (check lang (d e) 2 (and (eq? (term d) 5) (eq? (term e) 4))) #t) + (test (check lang (d ...) 2 (zero? (modulo (foldl + 0 (term (d ...))) 5))) #t) + (test (current-error-port-output (λ () (check lang (d e) 2 #f))) + "failed after 1 attempts:\n(5 4)\n") + (test (current-error-port-output (λ () (check lang d 2 (error 'pred-raised)))) + "failed after 1 attempts:\n5\n")) + +;; check-metafunction +;; TODO: handle no metafunctions with no contract +(let () + (define-language empty) + (define-metafunction empty + f : (side-condition number_1 (odd? (term number_1))) -> number + [(f 1) 1] + [(f 3) 'NaN]) + + (define-metafunction empty + g : number ... -> (any ...) + [(g number_1 ... 1 number_2 ...) ()]) + + (define-metafunction empty + h : number -> number + [(h any) any]) + + (define-metafunction empty + [(i any ...) (any ...)]) + + ;; Dom(f) < Ctc(f) + (test (current-error-port-output (λ () (check-metafunction f (decisions #:num (list (λ _ 2) (λ _ 5)))))) + "failed after 1 attempts:\n(5)\n") + ;; Rng(f) > Codom(f) + (test (current-error-port-output (λ () (check-metafunction f (decisions #:num (list (λ _ 3)))))) + "failed after 1 attempts:\n(3)\n") + ;; LHS matches multiple ways + (test (current-error-port-output (λ () (check-metafunction g (decisions #:num (list (λ _ 1) (λ _ 1)) + #:seq (list (λ _ 2)))))) + "failed after 1 attempts:\n(1 1)\n") + ;; OK -- generated from Dom(h) + (test (check-metafunction h) #t) + ;; OK -- generated from pattern 'any + (test (check-metafunction i) #t)) ;; parse/unparse-pattern (let-syntax ([test-match (syntax-rules () [(_ p x) (test (match x [p #t] [_ #f]) #t)])]) diff --git a/collects/redex/private/rg.ss b/collects/redex/private/rg.ss index 3ce57de2e6..1b994a9f6b 100644 --- a/collects/redex/private/rg.ss +++ b/collects/redex/private/rg.ss @@ -21,7 +21,10 @@ To do a better job of not generating programs with free variables, "reduction-semantics.ss" "underscore-allowed.ss" "term.ss" + "error.ss" (for-syntax "rewrite-side-conditions.ss") + (for-syntax "term-fn.ss") + (for-syntax "reduction-semantics.ss") mrlib/tex-table) (define random-numbers '(0 1 -1 17 8)) @@ -39,6 +42,10 @@ To do a better job of not generating programs with free variables, (hash-map uniq (λ (k v) k)))) (define generation-retries 100) + +(define default-check-attempts 100) +(define check-growth-base 5) + (define ascii-chars-threshold 50) (define tex-chars-threshold 500) (define chinese-chars-threshold 2000) @@ -89,7 +96,7 @@ To do a better job of not generating programs with free variables, (list->string (build-list length (λ (_) (pick-char attempt lang-chars random)))))) (define (pick-any lang [random random]) - (if (zero? (random 5)) + (if (and (not (null? (compiled-lang-lang lang))) (zero? (random 5))) (values lang (pick-from-list (map nt-name (compiled-lang-lang lang)) random)) (values sexp (nt-name (car (compiled-lang-lang sexp)))))) @@ -114,7 +121,7 @@ To do a better job of not generating programs with free variables, (error 'generate "unable to generate pattern ~s in ~s attempts" (unparse-pattern pat) generation-retries)) -(define (generate* lang pat size [decisions@ random-decisions@]) +(define (generate* lang pat [decisions@ random-decisions@]) (define-values/invoke-unit decisions@ (import) (export decisions^)) @@ -240,7 +247,7 @@ To do a better job of not generating programs with free variables, [`(hide-hole ,pattern) ((recur pattern the-hole) state)] [`any (let*-values ([(lang nt) ((next-any-decision) lang)] - [(term _) ((generate* lang nt size decisions@) attempt)]) + [(term _) ((generate* lang nt decisions@) size attempt)]) (values term state))] [(? (is-nt? lang)) (generate-nt pat pat bound-vars size attempt in-hole state)] @@ -306,7 +313,7 @@ To do a better job of not generating programs with free variables, (state-fvt state)) (state-env state))) - (λ (attempt) + (λ (size attempt) (let-values ([(term state) (generate/pred pat @@ -554,43 +561,53 @@ To do a better job of not generating programs with free variables, (define-syntax (check stx) (syntax-case stx () - [(_ lang pat attempts size property) + [(_ lang pat property) + (syntax/loc stx (check lang pat default-check-attempts property))] + [(_ lang pat attempts property) (let-values ([(names names/ellipses) (extract-names (language-id-nts #'lang 'generate) 'check #t #'pat)]) (with-syntax ([(name ...) names] [(name/ellipses ...) names/ellipses]) (syntax/loc stx - (let ([generator (term-generator lang pat size random-decisions@)]) - (let loop ([remaining attempts]) - (if (zero? remaining) - #t - (let ([attempt (add1 (- attempts remaining))]) - (let-values ([(term bindings) (generator attempt)]) - (term-let ([name/ellipses (lookup-binding bindings 'name)] ...) - (if (with-handlers - ([exn:fail? (λ (exn) (error 'check "term ~s raises ~s" term exn))]) - property) - (loop (sub1 remaining)) - (fprintf (current-error-port) - "failed after ~s attempts: ~s" - attempt term)))))))))))])) + (check-property + (term-generator lang pat random-decisions@) + (λ (_ bindings) + (with-handlers ([exn:fail? (λ (_) #f)]) + (term-let ([name/ellipses (lookup-binding bindings 'name)] ...) + property))) + attempts))))])) + +(define (check-property generate property attempts) + (let loop ([remaining attempts]) + (if (zero? remaining) + #t + (let ([attempt (add1 (- attempts remaining))]) + (let-values ([(term bindings) + (generate (floor (/ (log attempt) (log check-growth-base))) attempt)]) + (if (property term bindings) + (loop (sub1 remaining)) + (begin + (fprintf (current-error-port) + "failed after ~s attempts:\n" + attempt) + (pretty-print term (current-error-port))))))))) (define-syntax generate (syntax-rules () [(_ lang pat size attempt) - (let-values ([(term _) ((term-generator lang pat size random-decisions@) attempt)]) + (let-values ([(term _) ((term-generator lang pat random-decisions@) size attempt)]) term)] [(_ lang pat size) (generate lang pat size 0)])) (define-syntax generate/decisions (syntax-rules () [(_ lang pat size attempt decisions@) - (let-values ([(term _) ((term-generator lang pat size decisions@) attempt)]) + (let-values ([(term _) ((term-generator lang pat decisions@) size attempt)]) term)])) (define-syntax (term-generator stx) (syntax-case stx () - [(_ lang pat size decisions@) + [(_ lang pat decisions@) (with-syntax ([pattern (rewrite-side-conditions/check-errs (language-id-nts #'lang 'generate) @@ -599,7 +616,28 @@ To do a better job of not generating programs with free variables, (generate* (parse-language lang) (reassign-classes (parse-pattern `pattern lang 'top-level)) - size decisions@)))])) + decisions@)))])) + +(define-syntax (check-metafunction stx) + (syntax-case stx () + [(_ name) (syntax/loc stx (check-metafunction name random-decisions@))] + [(_ name decisions@) + (identifier? #'name) + (with-syntax ([m (let ([tf (syntax-local-value #'name (λ () #f))]) + (if (term-fn? tf) + (term-fn-get-id tf) + (raise-syntax-error #f "not a metafunction" stx #'name)))]) + (syntax + (let ([lang (metafunc-proc-lang m)] + [dom (metafunc-proc-dom-pat m)]) + (check-property + (generate* (parse-language lang) + (reassign-classes (parse-pattern (if dom dom '(any (... ...))) lang 'top-level)) + decisions@) + (λ (t _) + (with-handlers ([exn:fail:redex? (λ (_) #f)]) + (begin (term (name ,@t)) #t))) + 100))))])) (define-signature decisions^ (next-variable-decision @@ -623,7 +661,7 @@ To do a better job of not generating programs with free variables, pick-nt unique-chars pick-any sexp generate parse-pattern class-reassignments reassign-classes unparse-pattern (struct-out ellipsis) (struct-out mismatch) (struct-out class) - (struct-out binder) generate/decisions) + (struct-out binder) generate/decisions check-metafunction) (provide/contract [find-base-cases (-> compiled-lang? hash?)]) \ No newline at end of file