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

1. Fixed bug in reduction-semantics.ss.

Browse Source 
2. Fixed bug in generation of 'any pattern.
3. Added `check-metafunction' form.

svn: r11984
This commit is contained in:
Casey Klein 2008-10-09 19:09:11 +00:00
parent 18f05a6823
commit b2ce9f4cd3
3 changed files with 119 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
collects/redex/private/reduction-semantics.ss
View File

@ -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))

60
collects/redex/private/rg-test.ss
View File

@ -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)])])

86
collects/redex/private/rg.ss
View File

@ -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?)])