Improved performance of the test case generator
svn: r17894
This commit is contained in:
Casey Klein
parent
dc93732d6f
commit
0e6c28e4b1
|
|
@ -45,17 +45,18 @@
|
|||
(list->string (build-list length (λ (_) (pick-char attempt random))))))
|
||||
|
||||
(define (pick-any lang sexp [random random])
|
||||
(let ([c-lang (rg-lang-clang lang)]
|
||||
[c-sexp (rg-lang-clang sexp)])
|
||||
(if (and (not (null? (compiled-lang-lang c-lang))) (zero? (random 5)))
|
||||
(values lang (pick-from-list (map nt-name (compiled-lang-lang c-lang)) random))
|
||||
(values sexp (nt-name (car (compiled-lang-lang c-sexp)))))))
|
||||
(if (and (> (dict-count (rg-lang-non-cross lang)) 0) (zero? (random 5)))
|
||||
(let ([nts (rg-lang-non-cross lang)])
|
||||
(values lang (pick-from-list (dict-map nts (λ (nt _) nt)) random)))
|
||||
(values sexp 'sexp)))
|
||||
|
||||
(define (pick-string lang-lits attempt [random random])
|
||||
(random-string lang-lits (random-natural 1/5 random) attempt random))
|
||||
|
||||
(define (pick-nts name cross? lang attempt)
|
||||
(nt-rhs (nt-by-name lang name cross?)))
|
||||
;; next-non-terminal-decision selects a subset of a non-terminal's productions.
|
||||
;; This implementation, the default, chooses them all, but many of the
|
||||
;; generator's test cases restrict the productions.
|
||||
(define pick-nts values)
|
||||
|
||||
(define (pick-from-list l [random random]) (list-ref l (random (length l))))
|
||||
|
||||
|
|
@ -132,19 +133,15 @@
|
|||
(define (pick-sequence-length attempt)
|
||||
(random-natural (expected-value->p (attempt->size attempt))))
|
||||
|
||||
(define (zip . lists)
|
||||
(apply (curry map list) lists))
|
||||
|
||||
(define (min-prods nt base-table)
|
||||
(let* ([sizes (hash-ref base-table (nt-name nt))]
|
||||
(define (min-prods nt prods base-table)
|
||||
(let* ([sizes (hash-ref base-table nt)]
|
||||
[min-size (apply min/f sizes)])
|
||||
(map cadr (filter (λ (x) (equal? min-size (car x))) (zip sizes (nt-rhs nt))))))
|
||||
(map cadr (filter (λ (x) (equal? min-size (car x))) (map list sizes prods)))))
|
||||
|
||||
(define-struct rg-lang (clang lits base-cases))
|
||||
(define-struct rg-lang (non-cross cross base-cases))
|
||||
(define (prepare-lang lang)
|
||||
(let ([lits (map symbol->string (compiled-lang-literals lang))]
|
||||
[parsed (parse-language lang)])
|
||||
(make-rg-lang parsed lits (find-base-cases parsed))))
|
||||
(let ([parsed (parse-language lang)])
|
||||
(values parsed (map symbol->string (compiled-lang-literals lang)) (find-base-cases parsed))))
|
||||
|
||||
(define-struct (exn:fail:redex:generation-failure exn:fail:redex) ())
|
||||
(define (raise-gen-fail who what attempts)
|
||||
|
|
@ -152,52 +149,31 @@
|
|||
who what attempts (if (= attempts 1) "" "s"))])
|
||||
(raise (make-exn:fail:redex:generation-failure str (current-continuation-marks)))))
|
||||
|
||||
(define (generate lang decisions@ what)
|
||||
(define-values/invoke-unit decisions@
|
||||
(define (compile lang what)
|
||||
(define-values/invoke-unit (generation-decisions)
|
||||
(import) (export decisions^))
|
||||
|
||||
(define ((generate-nt lang base-cases generate retries)
|
||||
name cross? size attempt in-hole env)
|
||||
(define (gen-nt lang name cross? retries size attempt in-hole)
|
||||
(let*-values
|
||||
([(term _)
|
||||
([(productions)
|
||||
(hash-ref ((if cross? rg-lang-cross rg-lang-non-cross) lang) name)]
|
||||
[(term _)
|
||||
(generate/pred
|
||||
name
|
||||
(λ (size attempt)
|
||||
(let ([rhs (pick-from-list
|
||||
(let ([gen (pick-from-list
|
||||
(if (zero? size)
|
||||
(min-prods (nt-by-name lang name cross?)
|
||||
(min-prods name productions
|
||||
((if cross? base-cases-cross base-cases-non-cross)
|
||||
base-cases))
|
||||
((next-non-terminal-decision) name cross? lang attempt)))])
|
||||
(generate (max 0 (sub1 size)) attempt empty-env in-hole (rhs-pattern rhs))))
|
||||
(rg-lang-base-cases lang)))
|
||||
((next-non-terminal-decision) productions)))])
|
||||
(gen retries (max 0 (sub1 size)) attempt empty-env in-hole)))
|
||||
(λ (_ env) (mismatches-satisfied? env))
|
||||
size attempt retries)])
|
||||
term))
|
||||
|
||||
(define (generate-sequence ellipsis generate env length)
|
||||
(define (split-environment env)
|
||||
(foldl (λ (var seq-envs)
|
||||
(let ([vals (hash-ref env var #f)])
|
||||
(if vals
|
||||
(map (λ (seq-env val) (hash-set seq-env var val)) seq-envs vals)
|
||||
seq-envs)))
|
||||
(build-list length (λ (_) #hash())) (ellipsis-vars ellipsis)))
|
||||
(define (merge-environments seq-envs)
|
||||
(foldl (λ (var env)
|
||||
(hash-set env var (map (λ (seq-env) (hash-ref seq-env var)) seq-envs)))
|
||||
env (ellipsis-vars ellipsis)))
|
||||
(let-values
|
||||
([(seq envs)
|
||||
(let recur ([envs (split-environment env)])
|
||||
(if (null? envs)
|
||||
(values null null)
|
||||
(let*-values
|
||||
([(term env) (generate (car envs) the-hole (ellipsis-pattern ellipsis))]
|
||||
[(terms envs) (recur (cdr envs))])
|
||||
(values (cons term terms) (cons env envs)))))])
|
||||
(values seq (merge-environments envs))))
|
||||
|
||||
(define (generate/pred name gen pred init-sz init-att retries)
|
||||
#;(gen init-sz init-att)
|
||||
(let ([pre-threshold-incr
|
||||
(ceiling
|
||||
(/ (- retry-threshold init-att)
|
||||
|
|
@ -206,8 +182,7 @@
|
|||
(λ (remain)
|
||||
(zero?
|
||||
(modulo (sub1 remain)
|
||||
(ceiling (* proportion-at-size
|
||||
retries)))))])
|
||||
(ceiling (* proportion-at-size retries)))))])
|
||||
(let retry ([remaining (add1 retries)]
|
||||
[size init-sz]
|
||||
[attempt init-att])
|
||||
|
|
@ -223,14 +198,37 @@
|
|||
post-threshold-incr
|
||||
pre-threshold-incr)))))))))
|
||||
|
||||
(define (generate/prior name env generate)
|
||||
(define (generate/prior name env gen)
|
||||
(let* ([none (gensym)]
|
||||
[prior (hash-ref env name none)])
|
||||
(if (eq? prior none)
|
||||
(let-values ([(term env) (generate)])
|
||||
(let-values ([(term env) (gen)])
|
||||
(values term (hash-set env name term)))
|
||||
(values prior env))))
|
||||
|
||||
(define (generate-sequence gen env vars length)
|
||||
(define (split-environment env)
|
||||
(foldl (λ (var seq-envs)
|
||||
(let ([vals (hash-ref env var #f)])
|
||||
(if vals
|
||||
(map (λ (seq-env val) (hash-set seq-env var val)) seq-envs vals)
|
||||
seq-envs)))
|
||||
(build-list length (λ (_) #hash())) vars))
|
||||
(define (merge-environments seq-envs)
|
||||
(foldl (λ (var env)
|
||||
(hash-set env var (map (λ (seq-env) (hash-ref seq-env var)) seq-envs)))
|
||||
env vars))
|
||||
(let-values
|
||||
([(seq envs)
|
||||
(let recur ([envs (split-environment env)])
|
||||
(if (null? envs)
|
||||
(values null null)
|
||||
(let*-values
|
||||
([(term env) (gen (car envs) the-hole)]
|
||||
[(terms envs) (recur (cdr envs))])
|
||||
(values (cons term terms) (cons env envs)))))])
|
||||
(values seq (merge-environments envs))))
|
||||
|
||||
(define (mismatches-satisfied? env)
|
||||
(let ([groups (make-hasheq)])
|
||||
(define (get-group group)
|
||||
|
|
@ -250,129 +248,141 @@
|
|||
(define (bindings env)
|
||||
(make-bindings
|
||||
(for/fold ([bindings null]) ([(key val) env])
|
||||
(if (binder? key)
|
||||
(cons (make-bind (binder-name key) val) bindings)
|
||||
bindings))))
|
||||
(if (binder? key)
|
||||
(cons (make-bind (binder-name key) val) bindings)
|
||||
bindings))))
|
||||
|
||||
(define (generate-pat lang sexp retries size attempt env in-hole pat)
|
||||
(define recur (curry generate-pat lang sexp retries size attempt))
|
||||
(define recur/pat (recur env in-hole))
|
||||
(define ((recur/pat/size-attempt pat) size attempt)
|
||||
(generate-pat lang sexp retries size attempt env in-hole pat))
|
||||
|
||||
(define clang (rg-lang-clang lang))
|
||||
(define gen-nt
|
||||
(generate-nt
|
||||
clang
|
||||
(rg-lang-base-cases lang)
|
||||
(curry generate-pat lang sexp retries)
|
||||
retries))
|
||||
|
||||
(match pat
|
||||
[`number (values ((next-number-decision) attempt) env)]
|
||||
[`natural (values ((next-natural-decision) attempt) env)]
|
||||
[`integer (values ((next-integer-decision) attempt) env)]
|
||||
[`real (values ((next-real-decision) attempt) env)]
|
||||
[`(variable-except ,vars ...)
|
||||
(generate/pred 'variable
|
||||
(recur/pat/size-attempt 'variable)
|
||||
(λ (var _) (not (memq var vars)))
|
||||
size attempt retries)]
|
||||
[`variable
|
||||
(values ((next-variable-decision) (rg-lang-lits lang) attempt)
|
||||
env)]
|
||||
[`variable-not-otherwise-mentioned
|
||||
(generate/pred 'variable
|
||||
(recur/pat/size-attempt 'variable)
|
||||
(λ (var _) (not (memq var (compiled-lang-literals clang))))
|
||||
size attempt retries)]
|
||||
[`(variable-prefix ,prefix)
|
||||
(define (symbol-append prefix suffix)
|
||||
(string->symbol (string-append (symbol->string prefix) (symbol->string suffix))))
|
||||
(let-values ([(term env) (recur/pat 'variable)])
|
||||
(values (symbol-append prefix term) env))]
|
||||
[`string
|
||||
(values ((next-string-decision) (rg-lang-lits lang) attempt)
|
||||
env)]
|
||||
[`(side-condition ,pat ,(? procedure? condition) ,guard-src-loc)
|
||||
(generate/pred `(side-condition ,(unparse-pattern pat) ,guard-src-loc)
|
||||
(recur/pat/size-attempt pat)
|
||||
(λ (_ env) (condition (bindings env)))
|
||||
size attempt retries)]
|
||||
[`(name ,(? symbol? id) ,p)
|
||||
(let-values ([(term env) (recur/pat p)])
|
||||
(values term (hash-set env (make-binder id) term)))]
|
||||
[`hole (values in-hole env)]
|
||||
[`(in-hole ,context ,contractum)
|
||||
(let-values ([(term env) (recur/pat contractum)])
|
||||
(recur env term context))]
|
||||
[`(hide-hole ,pattern) (recur env the-hole pattern)]
|
||||
[`any
|
||||
(let*-values ([(new-lang nt) ((next-any-decision) lang sexp)]
|
||||
[(term _) (generate-pat new-lang
|
||||
sexp
|
||||
retries
|
||||
size
|
||||
attempt
|
||||
empty-env
|
||||
the-hole
|
||||
nt)])
|
||||
(values term env))]
|
||||
[(? (is-nt? clang))
|
||||
(values (gen-nt pat #f size attempt in-hole env) env)]
|
||||
[(struct binder ((or (? (is-nt? clang) nt)
|
||||
(app (symbol-match named-nt-rx) (? (is-nt? clang) nt)))))
|
||||
(generate/prior pat env (λ () (recur/pat nt)))]
|
||||
[(struct binder ((or (? built-in? b)
|
||||
(app (symbol-match named-nt-rx) (? built-in? b)))))
|
||||
(generate/prior pat env (λ () (recur/pat b)))]
|
||||
[(struct mismatch (name (app (symbol-match mismatch-nt-rx)
|
||||
(? symbol? (? (is-nt? clang) nt)))))
|
||||
(let-values ([(term _) (recur/pat nt)])
|
||||
(values term (hash-set env pat term)))]
|
||||
[(struct mismatch (name (app (symbol-match mismatch-nt-rx)
|
||||
(? symbol? (? built-in? b)))))
|
||||
(let-values ([(term _) (recur/pat b)])
|
||||
(values term (hash-set env pat term)))]
|
||||
[`(cross ,(? symbol? cross-nt))
|
||||
(values (gen-nt cross-nt #t size attempt in-hole env) env)]
|
||||
[(or (? symbol?) (? number?) (? string?) (? boolean?) (? null?)) (values pat env)]
|
||||
[(list-rest (and (struct ellipsis (name sub-pat class vars)) ellipsis) rest)
|
||||
(let*-values ([(length) (let ([prior (hash-ref env class #f)])
|
||||
(if prior prior ((next-sequence-decision) attempt)))]
|
||||
[(seq env) (generate-sequence ellipsis recur env length)]
|
||||
[(rest env) (recur (hash-set (hash-set env class length) name length)
|
||||
in-hole rest)])
|
||||
(values (append seq rest) env))]
|
||||
[(list-rest pat rest)
|
||||
(let*-values
|
||||
([(pat-term env) (recur/pat pat)]
|
||||
[(rest-term env) (recur env in-hole rest)])
|
||||
(values (cons pat-term rest-term) env))]
|
||||
[else
|
||||
(error what "unknown pattern ~s\n" pat)]))
|
||||
|
||||
(let ([rg-lang (prepare-lang lang)]
|
||||
[rg-sexp (prepare-lang sexp)])
|
||||
(λ (pat)
|
||||
(let ([parsed (reassign-classes (parse-pattern pat lang 'top-level))])
|
||||
(λ (size attempt retries)
|
||||
(let-values ([(term env)
|
||||
(generate/pred
|
||||
pat
|
||||
(λ (size attempt)
|
||||
(generate-pat
|
||||
rg-lang
|
||||
rg-sexp
|
||||
retries
|
||||
size
|
||||
attempt
|
||||
empty-env
|
||||
the-hole
|
||||
parsed))
|
||||
(λ (_ env) (mismatches-satisfied? env))
|
||||
size attempt retries)])
|
||||
(values term (bindings env))))))))
|
||||
(let*-values ([(langp lits lang-bases) (prepare-lang lang)]
|
||||
[(sexpp _ sexp-bases) (prepare-lang sexp)]
|
||||
[(lit-syms) (compiled-lang-literals lang)])
|
||||
(letrec-values
|
||||
([(compile)
|
||||
(λ (pat any?)
|
||||
(let ([nt? (is-nt? (if any? sexpp langp))])
|
||||
; retries size attempt env in-hole -> (values term env)
|
||||
(match pat
|
||||
[`number (λ (r s a e h) (values ((next-number-decision) a) e))]
|
||||
[`natural (λ (r s a e h) (values ((next-natural-decision) a) e))]
|
||||
[`integer (λ (r s a e h) (values ((next-integer-decision) a) e))]
|
||||
[`real (λ (r s a e h) (values ((next-real-decision) a) e))]
|
||||
[`(variable-except ,vars ...)
|
||||
(let ([g (compile 'variable any?)])
|
||||
(λ (r s a e h)
|
||||
(generate/pred pat
|
||||
(λ (s a) (g r s a e h))
|
||||
(λ (var _) (not (memq var vars)))
|
||||
s a r)))]
|
||||
[`variable
|
||||
(λ (r s a e h)
|
||||
(values ((next-variable-decision) lits a) e))]
|
||||
[`variable-not-otherwise-mentioned
|
||||
(let ([g (compile 'variable any?)])
|
||||
(λ (r s a e h)
|
||||
(generate/pred pat
|
||||
(λ (s a) (g r s a e h))
|
||||
(λ (var _) (not (memq var lit-syms)))
|
||||
s a r)))]
|
||||
[`(variable-prefix ,prefix)
|
||||
(define (symbol-append prefix suffix)
|
||||
(string->symbol (string-append (symbol->string prefix) (symbol->string suffix))))
|
||||
(let ([g (compile 'variable any?)])
|
||||
(λ (r s a e h)
|
||||
(let-values ([(term _) (g r s a e h)])
|
||||
(values (symbol-append prefix term) e))))]
|
||||
[`string
|
||||
(λ (r s a e h)
|
||||
(values ((next-string-decision) lits a) e))]
|
||||
[`(side-condition ,pat ,(? procedure? condition) ,guard-src-loc)
|
||||
(let ([g (compile pat any?)])
|
||||
(λ (r s a e h)
|
||||
(generate/pred `(side-condition ,(unparse-pattern pat) ,guard-src-loc)
|
||||
(λ (s a) (g r s a e h))
|
||||
(λ (_ env) (condition (bindings env)))
|
||||
s a r)))]
|
||||
[`(name ,(? symbol? id) ,p)
|
||||
(let ([g (compile p any?)])
|
||||
(λ (r s a e h)
|
||||
(let-values ([(term env) (g r s a e h)])
|
||||
(values term (hash-set env (make-binder id) term)))))]
|
||||
[`hole (λ (r s a e h) (values h e))]
|
||||
[`(in-hole ,context ,contractum)
|
||||
(let ([ctx (compile context any?)]
|
||||
[ctm (compile contractum any?)])
|
||||
(λ (r s a e h)
|
||||
(let-values ([(term env) (ctm r s a e h)])
|
||||
(ctx r s a env term))))]
|
||||
[`(hide-hole ,pattern)
|
||||
(let ([g (compile pattern any?)])
|
||||
(λ (r s a e h)
|
||||
(g r s a e the-hole)))]
|
||||
[`any
|
||||
(λ (r s a e h)
|
||||
(let*-values ([(lang nt) ((next-any-decision) langc sexpc)]
|
||||
[(term) (gen-nt lang nt #f r s a the-hole)])
|
||||
(values term e)))]
|
||||
[(or (? symbol? (? nt? p)) `(cross ,(? symbol? p)))
|
||||
(let ([cross? (not (symbol? pat))])
|
||||
(λ (r s a e h)
|
||||
(values (gen-nt (if any? sexpc langc) p cross? r s a h) e)))]
|
||||
[(struct binder ((or (app (symbol-match named-nt-rx) (? symbol? p)) p)))
|
||||
(let ([g (compile p any?)])
|
||||
(λ (r s a e h)
|
||||
(generate/prior pat e (λ () (g r s a e h)))))]
|
||||
[(struct mismatch (_ (app (symbol-match mismatch-nt-rx) p)))
|
||||
(let ([g (compile p any?)])
|
||||
(λ (r s a e h)
|
||||
(let-values ([(term _) (g r s a e h)])
|
||||
(values term (hash-set e pat term)))))]
|
||||
[(or (? symbol?) (? number?) (? string?) (? boolean?) (? null?))
|
||||
(λ (r s a e h) (values pat e))]
|
||||
[(list-rest (struct ellipsis (name sub-pat class vars)) rest)
|
||||
(let ([elemg (compile sub-pat any?)]
|
||||
[tailg (compile rest any?)])
|
||||
(λ (r s a e h)
|
||||
(let*-values ([(len)
|
||||
(let ([prior (hash-ref e class #f)])
|
||||
(if prior prior ((next-sequence-decision) a)))]
|
||||
[(seq env)
|
||||
(generate-sequence (λ (e h) (elemg r s a e h)) e vars len)]
|
||||
[(tail env)
|
||||
(let ([e (hash-set (hash-set env class len) name len)])
|
||||
(tailg r s a e h))])
|
||||
(values (append seq tail) env))))]
|
||||
[(list-rest hdp tlp)
|
||||
(let ([hdg (compile hdp any?)]
|
||||
[tlg (compile tlp any?)])
|
||||
(λ (r s a e h)
|
||||
(let*-values
|
||||
([(hd env) (hdg r s a e h)]
|
||||
[(tl env) (tlg r s a env h)])
|
||||
(values (cons hd tl) env))))]
|
||||
[else
|
||||
(error what "unknown pattern ~s\n" pat)])))]
|
||||
[(compile-non-terminals)
|
||||
(λ (nts any?)
|
||||
(make-immutable-hash
|
||||
(map (λ (nt) (cons (nt-name nt)
|
||||
(map (λ (p) (compile (rhs-pattern p) any?))
|
||||
(nt-rhs nt))))
|
||||
nts)))]
|
||||
[(compile-language)
|
||||
(λ (lang bases any?)
|
||||
(make-rg-lang
|
||||
(compile-non-terminals (compiled-lang-lang lang) any?)
|
||||
(compile-non-terminals (compiled-lang-cclang lang) any?)
|
||||
bases))]
|
||||
[(langc sexpc compile-pattern)
|
||||
(values
|
||||
(compile-language langp lang-bases #f)
|
||||
(compile-language sexpp sexp-bases #t)
|
||||
(λ (pat) (compile pat #f)))])
|
||||
(λ (pat)
|
||||
(let ([g (compile-pattern (reassign-classes (parse-pattern pat lang 'top-level)))]
|
||||
[mm-ok? (λ (_ env) (mismatches-satisfied? env))])
|
||||
(λ (size attempt retries)
|
||||
(let*-values ([(gen) (λ (s a) (g retries s a empty-env the-hole))]
|
||||
[(term env) (generate/pred pat gen mm-ok? size attempt retries)])
|
||||
(values term (bindings env)))))))))
|
||||
|
||||
(define-struct base-cases (cross non-cross))
|
||||
|
||||
|
|
@ -643,12 +653,12 @@
|
|||
x
|
||||
(raise-type-error 'redex-check "reduction-relation" x)))
|
||||
|
||||
(define-for-syntax (term-generator lang pat decisions@ what)
|
||||
(define-for-syntax (term-generator lang pat what)
|
||||
(with-syntax ([pattern
|
||||
(rewrite-side-conditions/check-errs
|
||||
(language-id-nts lang what)
|
||||
what #t pat)])
|
||||
#`((generate #,lang #,decisions@ '#,what) `pattern)))
|
||||
#`((compile #,lang '#,what) `pattern)))
|
||||
|
||||
(define-syntax (generate-term stx)
|
||||
(syntax-case stx ()
|
||||
|
|
@ -663,7 +673,6 @@
|
|||
[(name lang pat)
|
||||
(with-syntax ([make-gen (term-generator #'lang
|
||||
#'pat
|
||||
#'(generation-decisions)
|
||||
(syntax-e #'name))])
|
||||
(syntax/loc stx
|
||||
(let ([generate make-gen])
|
||||
|
|
@ -726,7 +735,6 @@
|
|||
lang
|
||||
metafunc/red-rel
|
||||
property
|
||||
random-decisions@
|
||||
(max 1 (floor (/ att num-cases)))
|
||||
ret
|
||||
'redex-check
|
||||
|
|
@ -734,7 +742,7 @@
|
|||
(test-match lang pat)
|
||||
(λ (generated) (redex-error 'redex-check "~s does not match ~s" generated 'pat))))
|
||||
#`(check-prop
|
||||
#,(term-generator #'lang #'pat #'random-decisions@ 'redex-check)
|
||||
#,(term-generator #'lang #'pat 'redex-check)
|
||||
property att ret (and print? show)))))))))]))
|
||||
|
||||
(define (format-attempts a)
|
||||
|
|
@ -804,10 +812,9 @@
|
|||
(syntax/loc stx
|
||||
(let ([lang (metafunc-proc-lang m)]
|
||||
[dom (metafunc-proc-dom-pat m)]
|
||||
[decisions@ (generation-decisions)]
|
||||
[att (assert-nat 'check-metafunction-contract attempts)])
|
||||
(check-prop
|
||||
((generate lang decisions@ 'check-metafunction-contract)
|
||||
((compile lang 'check-metafunction-contract)
|
||||
(if dom dom '(any (... ...))))
|
||||
(λ (t _)
|
||||
(with-handlers ([exn:fail:redex? (λ (_) #f)])
|
||||
|
|
@ -816,10 +823,10 @@
|
|||
retries
|
||||
show))))]))
|
||||
|
||||
(define (check-lhs-pats lang mf/rr prop decisions@ attempts retries what show
|
||||
(define (check-lhs-pats lang mf/rr prop attempts retries what show
|
||||
[match #f]
|
||||
[match-fail #f])
|
||||
(let ([lang-gen (generate lang decisions@ what)])
|
||||
(let ([lang-gen (compile lang what)])
|
||||
(let-values ([(pats srcs)
|
||||
(cond [(metafunc-proc? mf/rr)
|
||||
(values (map metafunc-case-lhs-pat (metafunc-proc-cases mf/rr))
|
||||
|
|
@ -869,7 +876,6 @@
|
|||
(metafunc-proc-lang m)
|
||||
m
|
||||
(λ (term _) (property term))
|
||||
(generation-decisions)
|
||||
att
|
||||
ret
|
||||
'check-metafunction
|
||||
|
|
@ -887,10 +893,9 @@
|
|||
(define-syntax (check-reduction-relation stx)
|
||||
(syntax-case stx ()
|
||||
[(_ relation property . kw-args)
|
||||
(with-syntax ([(attempts retries decisions@ print?)
|
||||
(with-syntax ([(attempts retries print?)
|
||||
(parse-kw-args `((#:attempts . , #'default-check-attempts)
|
||||
(#:retries . ,#'default-retries)
|
||||
(#:decisions . ,#'random-decisions@)
|
||||
(#:print? . #t))
|
||||
(syntax kw-args)
|
||||
stx)]
|
||||
|
|
@ -903,7 +908,6 @@
|
|||
(reduction-relation-lang rel)
|
||||
rel
|
||||
(λ (term _) (property term))
|
||||
decisions@
|
||||
attempts
|
||||
retries
|
||||
'check-reduction-relation
|
||||
|
|
@ -945,6 +949,7 @@
|
|||
(struct-out mismatch)
|
||||
(struct-out class)
|
||||
(struct-out binder)
|
||||
(struct-out rg-lang)
|
||||
(struct-out base-cases)
|
||||
(struct-out counterexample)
|
||||
(struct-out exn:fail:redex:test))
|
||||
|
|
|
|||
|
|
@ -70,15 +70,6 @@
|
|||
(test (hash-ref (base-cases-non-cross (find-base-cases L)) 'x)
|
||||
'(0 0)))
|
||||
|
||||
(let ()
|
||||
(define-language lang
|
||||
(e number x y)
|
||||
(x variable)
|
||||
(y y))
|
||||
(test (min-prods (car (compiled-lang-lang lang))
|
||||
(base-cases-non-cross (find-base-cases lang)))
|
||||
(list (car (nt-rhs (car (compiled-lang-lang lang)))))))
|
||||
|
||||
(define (make-random . nums)
|
||||
(let ([nums (box nums)])
|
||||
(λ ([m +inf.0])
|
||||
|
|
@ -126,10 +117,7 @@
|
|||
(make-exn-not-raised))))]))
|
||||
|
||||
(define (patterns . selectors)
|
||||
(map (λ (selector)
|
||||
(λ (name cross? lang sizes)
|
||||
(list (selector (nt-rhs (nt-by-name lang name cross?))))))
|
||||
selectors))
|
||||
(map (curry compose list) selectors))
|
||||
|
||||
(define (iterator name items)
|
||||
(let ([bi (box items)])
|
||||
|
|
@ -249,6 +237,7 @@
|
|||
(f (n_1 ..._1 n_2 ..._2 n_2 ..._1))
|
||||
(g (z_1 ..._!_1 z_2 ... (z_1 z_2) ...))
|
||||
(n number)
|
||||
(q literal)
|
||||
(z 4))
|
||||
(test
|
||||
(generate-term/decisions
|
||||
|
|
@ -264,6 +253,18 @@
|
|||
'(4 4 4 4 (4 4) (4 4)))
|
||||
(test (raised-exn-msg exn:fail:redex:generation-failure? (generate-term lang e 5 #:retries 42))
|
||||
#rx"generate-term: unable to generate pattern e in 42")
|
||||
(test (raised-exn-msg
|
||||
exn:fail:redex:generation-failure?
|
||||
(parameterize ([generation-decisions
|
||||
(decisions #:var (list (λ _ 'x) (λ _ 'x)))])
|
||||
(generate-term lang (variable-except x) 5 #:retries 1)))
|
||||
#rx"generate-term: unable to generate pattern \\(variable-except x\\) in 1")
|
||||
(test (raised-exn-msg
|
||||
exn:fail:redex:generation-failure?
|
||||
(parameterize ([generation-decisions
|
||||
(decisions #:var (λ _ 'literal))])
|
||||
(generate-term lang variable-not-otherwise-mentioned 5 #:retries 1)))
|
||||
#rx"generate-term: unable to generate pattern variable-not-otherwise-mentioned in 1")
|
||||
(test (generate-term/decisions lang f 5 0 (decisions #:seq (list (λ (_) 0)))) null)
|
||||
(test (generate-term/decisions
|
||||
lang ((0 ..._!_1) ... (1 ..._!_1) ...) 5 0
|
||||
|
|
@ -419,8 +420,8 @@
|
|||
(define-language empty)
|
||||
|
||||
;; `any' pattern
|
||||
(let ([four (prepare-lang four)]
|
||||
[sexp (prepare-lang sexp)])
|
||||
(let ([four (make-rg-lang '((e . ()) (f . ())) '((e-e . ()) (f-f . ())) 'dont-care)]
|
||||
[sexp (make-rg-lang 'dont-care 'dont-care 'dont-care)])
|
||||
(test (call-with-values (λ () (pick-any four sexp (make-random 0 1))) list)
|
||||
(list four 'f))
|
||||
(test (call-with-values (λ () (pick-any four sexp (make-random 1))) list)
|
||||
|
|
@ -436,6 +437,7 @@
|
|||
'("foo" "bar" "baz"))
|
||||
(test (generate-term/decisions
|
||||
empty any 5 0 (decisions #:nt (patterns first)
|
||||
#:any (λ (langc sexpc) (values sexpc 'sexp))
|
||||
#:var (list (λ _ 'x))))
|
||||
'x))
|
||||
|
||||
|
|
@ -660,6 +662,7 @@
|
|||
exn:fail:redex:generation-failure?
|
||||
(redex-check lang (side-condition any #f) #t #:retries 42 #:attempts 1))
|
||||
#rx"^redex-check: unable .* in 42")
|
||||
|
||||
(let ([unable-loc #px"^redex-check: unable to generate LHS of clause at .*:\\d+:\\d+ in 42"])
|
||||
(let-syntax ([test-gen-fail
|
||||
(syntax-rules ()
|
||||
|
|
@ -770,11 +773,12 @@
|
|||
(test (begin
|
||||
(output
|
||||
(λ ()
|
||||
(check-reduction-relation
|
||||
R (λ (term) (set! generated (cons term generated)))
|
||||
#:decisions (decisions #:seq (list (λ _ 0) (λ _ 0) (λ _ 0))
|
||||
#:num (list (λ _ 1) (λ _ 1) (λ _ 0)))
|
||||
#:attempts 1)))
|
||||
(parameterize ([generation-decisions
|
||||
(decisions #:seq (list (λ _ 0) (λ _ 0) (λ _ 0))
|
||||
#:num (list (λ _ 1) (λ _ 1) (λ _ 0)))])
|
||||
(check-reduction-relation
|
||||
R (λ (term) (set! generated (cons term generated)))
|
||||
#:attempts 1))))
|
||||
generated)
|
||||
(reverse '((+ (+)) 0))))
|
||||
|
||||
|
|
@ -804,10 +808,11 @@
|
|||
(==> a b)])])
|
||||
(test (output
|
||||
(λ ()
|
||||
(check-reduction-relation
|
||||
T (curry equal? '(9 4))
|
||||
#:attempts 1
|
||||
#:decisions (decisions #:num (build-list 5 (λ (x) (λ _ x)))))))
|
||||
(parameterize ([generation-decisions
|
||||
(decisions #:num (build-list 5 (λ (x) (λ _ x))))])
|
||||
(check-reduction-relation
|
||||
T (curry equal? '(9 4))
|
||||
#:attempts 1))))
|
||||
#rx"no counterexamples"))
|
||||
|
||||
(let ([U (reduction-relation L (--> (side-condition any #f) any))])
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user