Barebones interface for overriding default generators.
svn: r14519
This commit is contained in:
parent
4de8e28016
commit
2c8c8638ac
|
@ -347,6 +347,10 @@
|
||||||
(test (generate-term lang (side-condition a (odd? (term a))) 5) 43)
|
(test (generate-term lang (side-condition a (odd? (term a))) 5) 43)
|
||||||
(test (raised-exn-msg exn:fail:redex? (generate-term lang c 5))
|
(test (raised-exn-msg exn:fail:redex? (generate-term lang c 5))
|
||||||
#rx"unable to generate")
|
#rx"unable to generate")
|
||||||
|
(test (let/ec k
|
||||||
|
(generate-term lang (number_1 (side-condition any (k (term number_1)))) 5))
|
||||||
|
'number_1)
|
||||||
|
|
||||||
(test ; mismatch patterns work with side-condition failure/retry
|
(test ; mismatch patterns work with side-condition failure/retry
|
||||||
(generate-term/decisions
|
(generate-term/decisions
|
||||||
lang e 5 0
|
lang e 5 0
|
||||||
|
@ -840,6 +844,89 @@
|
||||||
(check-metafunction n (λ (_) #t) #:retries 42))
|
(check-metafunction n (λ (_) #t) #:retries 42))
|
||||||
#rx"check-metafunction: unable .* in 42"))
|
#rx"check-metafunction: unable .* in 42"))
|
||||||
|
|
||||||
|
;; custom generators
|
||||||
|
(let ()
|
||||||
|
(define-language L
|
||||||
|
(x variable))
|
||||||
|
|
||||||
|
(test
|
||||||
|
(generate-term
|
||||||
|
L x_1 0
|
||||||
|
#:custom (λ (pat sz i-h acc env att rec def)
|
||||||
|
(match pat
|
||||||
|
['x (values 'x env)]
|
||||||
|
[_ (def acc)])))
|
||||||
|
'x)
|
||||||
|
(test
|
||||||
|
(let/ec k
|
||||||
|
(equal?
|
||||||
|
(generate-term
|
||||||
|
L (x x) 0
|
||||||
|
#:custom (let ([once? #f])
|
||||||
|
(λ (pat sz i-h acc env att rec def)
|
||||||
|
(match pat
|
||||||
|
['x (if once?
|
||||||
|
(k #f)
|
||||||
|
(begin
|
||||||
|
(set! once? #t)
|
||||||
|
(values 'x env)))]
|
||||||
|
[_ (def acc)]))))
|
||||||
|
'(x x)))
|
||||||
|
#t)
|
||||||
|
|
||||||
|
(test
|
||||||
|
(hash-ref
|
||||||
|
(let/ec k
|
||||||
|
(generate-term
|
||||||
|
L (x (x)) 0
|
||||||
|
#:custom (λ (pat sz i-h acc env att rec def)
|
||||||
|
(match pat
|
||||||
|
[(struct binder ('x))
|
||||||
|
(values 'y (hash-set env pat 'y))]
|
||||||
|
[(list (struct binder ('x))) (k env)]
|
||||||
|
[_ (def acc)]))))
|
||||||
|
(make-binder 'x))
|
||||||
|
'y)
|
||||||
|
|
||||||
|
(test
|
||||||
|
(generate-term
|
||||||
|
L (in-hole hole 7) 0
|
||||||
|
#:custom (λ (pat sz i-h acc env att rec def)
|
||||||
|
(match pat
|
||||||
|
[`(in-hole hole 7)
|
||||||
|
(rec 'hole #:contractum 7)]
|
||||||
|
[_ (def acc)])))
|
||||||
|
7)
|
||||||
|
|
||||||
|
(test
|
||||||
|
(let/ec k
|
||||||
|
(generate-term
|
||||||
|
L any 10
|
||||||
|
#:attempt 42
|
||||||
|
#:custom (λ (pat sz i-h acc env att rec def) (k (list sz att)))))
|
||||||
|
'(10 42))
|
||||||
|
|
||||||
|
(test
|
||||||
|
(let/ec k
|
||||||
|
(generate-term
|
||||||
|
L x 10
|
||||||
|
#:custom (λ (pat sz i-h acc env att rec def)
|
||||||
|
(match pat
|
||||||
|
['x (rec 7 #:size 0)]
|
||||||
|
[7 (k sz)]
|
||||||
|
[_ (def att)]))))
|
||||||
|
0)
|
||||||
|
|
||||||
|
(test
|
||||||
|
(generate-term
|
||||||
|
L (q 7) 0
|
||||||
|
#:custom (λ (pat sz i-h acc env att rec def)
|
||||||
|
(match pat
|
||||||
|
['q (rec '(7 7) #:acc 8)]
|
||||||
|
[7 (values (or acc 7) env)]
|
||||||
|
[_ (def att)])))
|
||||||
|
'((8 8) 7)))
|
||||||
|
|
||||||
;; parse/unparse-pattern
|
;; parse/unparse-pattern
|
||||||
(let-syntax ([test-match (syntax-rules () [(_ p x) (test (match x [p #t] [_ #f]) #t)])])
|
(let-syntax ([test-match (syntax-rules () [(_ p x) (test (match x [p #t] [_ #f]) #t)])])
|
||||||
(define-language lang (x variable))
|
(define-language lang (x variable))
|
||||||
|
|
|
@ -178,12 +178,12 @@
|
||||||
[parsed (parse-language lang)])
|
[parsed (parse-language lang)])
|
||||||
(make-rg-lang parsed lits (unique-chars lits) (find-base-cases parsed))))
|
(make-rg-lang parsed lits (unique-chars lits) (find-base-cases parsed))))
|
||||||
|
|
||||||
(define (generate lang decisions@ retries what)
|
(define (generate lang decisions@ user-gen retries what)
|
||||||
(define-values/invoke-unit decisions@
|
(define-values/invoke-unit decisions@
|
||||||
(import) (export decisions^))
|
(import) (export decisions^))
|
||||||
|
|
||||||
(define ((generate-nt lang base-cases generate pref-prods)
|
(define ((generate-nt lang base-cases generate pref-prods)
|
||||||
name cross? size attempt in-hole state)
|
name cross? size attempt in-hole env)
|
||||||
(let*-values
|
(let*-values
|
||||||
([(term _)
|
([(term _)
|
||||||
(generate/pred
|
(generate/pred
|
||||||
|
@ -195,14 +195,12 @@
|
||||||
((if cross? base-cases-cross base-cases-non-cross)
|
((if cross? base-cases-cross base-cases-non-cross)
|
||||||
base-cases))
|
base-cases))
|
||||||
((next-non-terminal-decision) name cross? lang attempt pref-prods)))])
|
((next-non-terminal-decision) name cross? lang attempt pref-prods)))])
|
||||||
(generate (max 0 (sub1 size)) attempt
|
(generate (max 0 (sub1 size)) attempt empty-env in-hole (rhs-pattern rhs))))
|
||||||
(make-state #hash())
|
|
||||||
in-hole (rhs-pattern rhs))))
|
|
||||||
(λ (_ env) (mismatches-satisfied? env))
|
(λ (_ env) (mismatches-satisfied? env))
|
||||||
size attempt)])
|
size attempt)])
|
||||||
term))
|
term))
|
||||||
|
|
||||||
(define (generate-sequence ellipsis generate state length)
|
(define (generate-sequence ellipsis generate env length)
|
||||||
(define (split-environment env)
|
(define (split-environment env)
|
||||||
(foldl (λ (var seq-envs)
|
(foldl (λ (var seq-envs)
|
||||||
(let ([vals (hash-ref env var #f)])
|
(let ([vals (hash-ref env var #f)])
|
||||||
|
@ -213,17 +211,17 @@
|
||||||
(define (merge-environments seq-envs)
|
(define (merge-environments seq-envs)
|
||||||
(foldl (λ (var env)
|
(foldl (λ (var env)
|
||||||
(hash-set env var (map (λ (seq-env) (hash-ref seq-env var)) seq-envs)))
|
(hash-set env var (map (λ (seq-env) (hash-ref seq-env var)) seq-envs)))
|
||||||
(state-env state) (ellipsis-vars ellipsis)))
|
env (ellipsis-vars ellipsis)))
|
||||||
(let-values
|
(let-values
|
||||||
([(seq envs)
|
([(seq envs)
|
||||||
(let recur ([envs (split-environment (state-env state))])
|
(let recur ([envs (split-environment env)])
|
||||||
(if (null? envs)
|
(if (null? envs)
|
||||||
(values null null)
|
(values null null)
|
||||||
(let*-values
|
(let*-values
|
||||||
([(term state) (generate (make-state (car envs)) the-hole (ellipsis-pattern ellipsis))]
|
([(term env) (generate (car envs) the-hole (ellipsis-pattern ellipsis))]
|
||||||
[(terms envs) (recur (cdr envs))])
|
[(terms envs) (recur (cdr envs))])
|
||||||
(values (cons term terms) (cons (state-env state) envs)))))])
|
(values (cons term terms) (cons env envs)))))])
|
||||||
(values seq (make-state (merge-environments envs)))))
|
(values seq (merge-environments envs))))
|
||||||
|
|
||||||
(define (generate/pred name gen pred init-sz init-att)
|
(define (generate/pred name gen pred init-sz init-att)
|
||||||
(let ([pre-threshold-incr
|
(let ([pre-threshold-incr
|
||||||
|
@ -244,9 +242,9 @@
|
||||||
name
|
name
|
||||||
retries
|
retries
|
||||||
(if (= retries 1) "" "s"))
|
(if (= retries 1) "" "s"))
|
||||||
(let-values ([(term state) (gen size attempt)])
|
(let-values ([(term env) (gen size attempt)])
|
||||||
(if (pred term (state-env state))
|
(if (pred term env)
|
||||||
(values term state)
|
(values term env)
|
||||||
(retry (sub1 remaining)
|
(retry (sub1 remaining)
|
||||||
(if (incr-size? remaining) (add1 size) size)
|
(if (incr-size? remaining) (add1 size) size)
|
||||||
(+ attempt
|
(+ attempt
|
||||||
|
@ -254,13 +252,13 @@
|
||||||
post-threshold-incr
|
post-threshold-incr
|
||||||
pre-threshold-incr)))))))))
|
pre-threshold-incr)))))))))
|
||||||
|
|
||||||
(define (generate/prior name state generate)
|
(define (generate/prior name env generate)
|
||||||
(let* ([none (gensym)]
|
(let* ([none (gensym)]
|
||||||
[prior (hash-ref (state-env state) name none)])
|
[prior (hash-ref env name none)])
|
||||||
(if (eq? prior none)
|
(if (eq? prior none)
|
||||||
(let-values ([(term state) (generate)])
|
(let-values ([(term env) (generate)])
|
||||||
(values term (set-env state name term)))
|
(values term (hash-set env name term)))
|
||||||
(values prior state))))
|
(values prior env))))
|
||||||
|
|
||||||
(define (mismatches-satisfied? env)
|
(define (mismatches-satisfied? env)
|
||||||
(let ([groups (make-hasheq)])
|
(let ([groups (make-hasheq)])
|
||||||
|
@ -276,10 +274,7 @@
|
||||||
(and (not (hash-ref prior val #f))
|
(and (not (hash-ref prior val #f))
|
||||||
(hash-set! prior val #t)))))))
|
(hash-set! prior val #t)))))))
|
||||||
|
|
||||||
(define-struct state (env))
|
(define empty-env #hash())
|
||||||
(define new-state (make-state #hash()))
|
|
||||||
(define (set-env state name value)
|
|
||||||
(make-state (hash-set (state-env state) name value)))
|
|
||||||
|
|
||||||
(define (bindings env)
|
(define (bindings env)
|
||||||
(make-bindings
|
(make-bindings
|
||||||
|
@ -288,111 +283,139 @@
|
||||||
(cons (make-bind (binder-name key) val) bindings)
|
(cons (make-bind (binder-name key) val) bindings)
|
||||||
bindings))))
|
bindings))))
|
||||||
|
|
||||||
(define (generate-pat lang sexp pref-prods size attempt state in-hole pat)
|
(define (generate-pat lang sexp pref-prods user-gen user-acc size attempt env in-hole pat)
|
||||||
(define recur (curry generate-pat lang sexp pref-prods size attempt))
|
(define recur (curry generate-pat lang sexp pref-prods user-gen user-acc size attempt))
|
||||||
(define recur/pat (recur state in-hole))
|
(define recur/pat (recur env in-hole))
|
||||||
(define ((recur/pat/size-attempt pat) size attempt)
|
(define ((recur/pat/size-attempt pat) size attempt)
|
||||||
(generate-pat lang sexp pref-prods size attempt state in-hole pat))
|
(generate-pat lang sexp pref-prods user-gen user-acc size attempt env in-hole pat))
|
||||||
|
|
||||||
(define clang (rg-lang-clang lang))
|
(define clang (rg-lang-clang lang))
|
||||||
(define gen-nt
|
(define gen-nt
|
||||||
(generate-nt
|
(generate-nt
|
||||||
clang
|
clang
|
||||||
(rg-lang-base-cases lang)
|
(rg-lang-base-cases lang)
|
||||||
(curry generate-pat lang sexp pref-prods)
|
(curry generate-pat lang sexp pref-prods user-gen user-acc)
|
||||||
pref-prods))
|
pref-prods))
|
||||||
|
|
||||||
(match pat
|
(define (default-gen user-acc)
|
||||||
[`number (values ((next-number-decision) attempt) state)]
|
(match pat
|
||||||
[`natural (values ((next-natural-decision) attempt) state)]
|
[`number (values ((next-number-decision) attempt) env)]
|
||||||
[`integer (values ((next-integer-decision) attempt) state)]
|
[`natural (values ((next-natural-decision) attempt) env)]
|
||||||
[`real (values ((next-real-decision) attempt) state)]
|
[`integer (values ((next-integer-decision) attempt) env)]
|
||||||
[`(variable-except ,vars ...)
|
[`real (values ((next-real-decision) attempt) env)]
|
||||||
(generate/pred 'variable
|
[`(variable-except ,vars ...)
|
||||||
(recur/pat/size-attempt 'variable)
|
(generate/pred 'variable
|
||||||
(λ (var _) (not (memq var vars)))
|
(recur/pat/size-attempt 'variable)
|
||||||
size attempt)]
|
(λ (var _) (not (memq var vars)))
|
||||||
[`variable
|
size attempt)]
|
||||||
(values ((next-variable-decision)
|
[`variable
|
||||||
(rg-lang-chars lang) (rg-lang-lits lang) attempt)
|
(values ((next-variable-decision)
|
||||||
state)]
|
(rg-lang-chars lang) (rg-lang-lits lang) attempt)
|
||||||
[`variable-not-otherwise-mentioned
|
env)]
|
||||||
(generate/pred 'variable
|
[`variable-not-otherwise-mentioned
|
||||||
(recur/pat/size-attempt 'variable)
|
(generate/pred 'variable
|
||||||
(λ (var _) (not (memq var (compiled-lang-literals clang))))
|
(recur/pat/size-attempt 'variable)
|
||||||
size attempt)]
|
(λ (var _) (not (memq var (compiled-lang-literals clang))))
|
||||||
[`(variable-prefix ,prefix)
|
size attempt)]
|
||||||
(define (symbol-append prefix suffix)
|
[`(variable-prefix ,prefix)
|
||||||
(string->symbol (string-append (symbol->string prefix) (symbol->string suffix))))
|
(define (symbol-append prefix suffix)
|
||||||
(let-values ([(term state) (recur/pat 'variable)])
|
(string->symbol (string-append (symbol->string prefix) (symbol->string suffix))))
|
||||||
(values (symbol-append prefix term) state))]
|
(let-values ([(term env) (recur/pat 'variable)])
|
||||||
[`string
|
(values (symbol-append prefix term) env))]
|
||||||
(values ((next-string-decision) (rg-lang-chars lang) (rg-lang-lits lang) attempt)
|
[`string
|
||||||
state)]
|
(values ((next-string-decision) (rg-lang-chars lang) (rg-lang-lits lang) attempt)
|
||||||
[`(side-condition ,pat ,(? procedure? condition))
|
env)]
|
||||||
(generate/pred (unparse-pattern pat)
|
[`(side-condition ,pat ,(? procedure? condition))
|
||||||
(recur/pat/size-attempt pat)
|
(generate/pred (unparse-pattern pat)
|
||||||
(λ (_ env) (condition (bindings env)))
|
(recur/pat/size-attempt pat)
|
||||||
size attempt)]
|
(λ (_ env) (condition (bindings env)))
|
||||||
[`(name ,(? symbol? id) ,p)
|
size attempt)]
|
||||||
(let-values ([(term state) (recur/pat p)])
|
[`(name ,(? symbol? id) ,p)
|
||||||
(values term (set-env state (make-binder id) term)))]
|
(let-values ([(term env) (recur/pat p)])
|
||||||
[`hole (values in-hole state)]
|
(values term (hash-set env (make-binder id) term)))]
|
||||||
[`(in-hole ,context ,contractum)
|
[`hole (values in-hole env)]
|
||||||
(let-values ([(term state) (recur/pat contractum)])
|
[`(in-hole ,context ,contractum)
|
||||||
(recur state term context))]
|
(let-values ([(term env) (recur/pat contractum)])
|
||||||
[`(hide-hole ,pattern) (recur state the-hole pattern)]
|
(recur env term context))]
|
||||||
[`any
|
[`(hide-hole ,pattern) (recur env the-hole pattern)]
|
||||||
(let*-values ([(new-lang nt) ((next-any-decision) lang sexp)]
|
[`any
|
||||||
; Don't use preferred productions for the sexp language.
|
(let*-values ([(new-lang nt) ((next-any-decision) lang sexp)]
|
||||||
[(pref-prods) (if (eq? new-lang lang) pref-prods #f)]
|
; Don't use preferred productions for the sexp language.
|
||||||
[(term _) (generate-pat new-lang sexp pref-prods size attempt new-state the-hole nt)])
|
[(pref-prods) (if (eq? new-lang lang) pref-prods #f)]
|
||||||
(values term state))]
|
[(term _) (generate-pat new-lang
|
||||||
[(? (is-nt? clang))
|
sexp
|
||||||
(values (gen-nt pat #f size attempt in-hole state) state)]
|
pref-prods
|
||||||
[(struct binder ((and name (or (? (is-nt? clang) nt) (app (symbol-match named-nt-rx) (? (is-nt? clang) nt))))))
|
user-gen
|
||||||
(generate/prior pat state (λ () (values (gen-nt nt #f size attempt in-hole state) state)))]
|
user-acc
|
||||||
[(struct binder ((or (? built-in? b) (app (symbol-match named-nt-rx) (? built-in? b)))))
|
size
|
||||||
(generate/prior pat state (λ () (recur/pat b)))]
|
attempt
|
||||||
[(struct mismatch (name (app (symbol-match mismatch-nt-rx) (? symbol? (? (is-nt? clang) nt)))))
|
empty-env
|
||||||
(let ([term (gen-nt nt #f size attempt in-hole state)])
|
the-hole
|
||||||
(values term (set-env state pat term)))]
|
nt)])
|
||||||
[(struct mismatch (name (app (symbol-match mismatch-nt-rx) (? symbol? (? built-in? b)))))
|
(values term env))]
|
||||||
(let-values ([(term state) (recur/pat b)])
|
[(? (is-nt? clang))
|
||||||
(values term (set-env state pat term)))]
|
(values (gen-nt pat #f size attempt in-hole env) env)]
|
||||||
[`(cross ,(? symbol? cross-nt))
|
[(struct binder ((or (? (is-nt? clang) nt)
|
||||||
(values (gen-nt cross-nt #t size attempt in-hole state) state)]
|
(app (symbol-match named-nt-rx) (? (is-nt? clang) nt)))))
|
||||||
[(or (? symbol?) (? number?) (? string?) (? boolean?) (? null?)) (values pat state)]
|
(generate/prior pat env (λ () (recur/pat nt)))]
|
||||||
[(list-rest (and (struct ellipsis (name sub-pat class vars)) ellipsis) rest)
|
[(struct binder ((or (? built-in? b)
|
||||||
(let*-values ([(length) (let ([prior (hash-ref (state-env state) class #f)])
|
(app (symbol-match named-nt-rx) (? built-in? b)))))
|
||||||
(if prior prior ((next-sequence-decision) attempt)))]
|
(generate/prior pat env (λ () (recur/pat b)))]
|
||||||
[(seq state) (generate-sequence ellipsis recur state length)]
|
[(struct mismatch (name (app (symbol-match mismatch-nt-rx)
|
||||||
[(rest state) (recur (set-env (set-env state class length) name length)
|
(? 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)])
|
in-hole rest)])
|
||||||
(values (append seq rest) state))]
|
(values (append seq rest) env))]
|
||||||
[(list-rest pat rest)
|
[(list-rest pat rest)
|
||||||
(let*-values
|
(let*-values
|
||||||
([(pat-term state) (recur/pat pat)]
|
([(pat-term env) (recur/pat pat)]
|
||||||
[(rest-term state) (recur state in-hole rest)])
|
[(rest-term env) (recur env in-hole rest)])
|
||||||
(values (cons pat-term rest-term) state))]
|
(values (cons pat-term rest-term) env))]
|
||||||
[else
|
[else
|
||||||
(error what "unknown pattern ~s\n" pat)]))
|
(error what "unknown pattern ~s\n" pat)]))
|
||||||
|
|
||||||
|
(user-gen
|
||||||
|
pat size in-hole user-acc env attempt
|
||||||
|
(λ (pat #:size [size size] #:contractum [in-hole in-hole] #:acc [user-acc user-acc] #:env [env env])
|
||||||
|
(generate-pat lang sexp pref-prods user-gen user-acc size attempt env in-hole pat))
|
||||||
|
default-gen))
|
||||||
|
|
||||||
(let ([rg-lang (prepare-lang lang)]
|
(let ([rg-lang (prepare-lang lang)]
|
||||||
[rg-sexp (prepare-lang sexp)])
|
[rg-sexp (prepare-lang sexp)])
|
||||||
(λ (pat)
|
(λ (pat)
|
||||||
(let ([parsed (reassign-classes (parse-pattern pat lang 'top-level))])
|
(let ([parsed (reassign-classes (parse-pattern pat lang 'top-level))])
|
||||||
(λ (size attempt)
|
(λ (size attempt)
|
||||||
(let-values ([(term state)
|
(let-values ([(term env)
|
||||||
(generate/pred
|
(generate/pred
|
||||||
pat
|
pat
|
||||||
(λ (size attempt)
|
(λ (size attempt)
|
||||||
(generate-pat
|
(generate-pat
|
||||||
rg-lang rg-sexp ((next-pref-prods-decision) (rg-lang-clang rg-lang))
|
rg-lang
|
||||||
size attempt new-state the-hole parsed))
|
rg-sexp
|
||||||
|
((next-pref-prods-decision) (rg-lang-clang rg-lang))
|
||||||
|
user-gen
|
||||||
|
#f
|
||||||
|
size
|
||||||
|
attempt
|
||||||
|
empty-env
|
||||||
|
the-hole
|
||||||
|
parsed))
|
||||||
(λ (_ env) (mismatches-satisfied? env))
|
(λ (_ env) (mismatches-satisfied? env))
|
||||||
size attempt)])
|
size attempt)])
|
||||||
(values term (bindings (state-env state)))))))))
|
(values term (bindings env))))))))
|
||||||
|
|
||||||
(define-struct base-cases (cross non-cross))
|
(define-struct base-cases (cross non-cross))
|
||||||
|
|
||||||
|
@ -658,22 +681,31 @@
|
||||||
(unless (reduction-relation? x)
|
(unless (reduction-relation? x)
|
||||||
(raise-type-error 'redex-check "reduction-relation" x)))
|
(raise-type-error 'redex-check "reduction-relation" x)))
|
||||||
|
|
||||||
(define-for-syntax (term-generator lang pat decisions@ retries what)
|
(define (defer-all pat size in-hole acc env att recur defer)
|
||||||
|
(defer acc))
|
||||||
|
|
||||||
|
(define-for-syntax (term-generator lang pat decisions@ custom retries what)
|
||||||
(with-syntax ([pattern
|
(with-syntax ([pattern
|
||||||
(rewrite-side-conditions/check-errs
|
(rewrite-side-conditions/check-errs
|
||||||
(language-id-nts lang what)
|
(language-id-nts lang what)
|
||||||
what #t pat)])
|
what #t pat)])
|
||||||
#`((generate #,lang #,decisions@ #,retries '#,what) `pattern)))
|
#`((generate #,lang #,decisions@ #,custom #,retries '#,what) `pattern)))
|
||||||
|
|
||||||
(define-syntax (generate-term stx)
|
(define-syntax (generate-term stx)
|
||||||
(syntax-case stx ()
|
(syntax-case stx ()
|
||||||
[(_ lang pat size . kw-args)
|
[(_ lang pat size . kw-args)
|
||||||
(with-syntax ([(attempt retries)
|
(with-syntax ([(attempt retries custom)
|
||||||
(parse-kw-args `((#:attempt . 1)
|
(parse-kw-args `((#:attempt . 1)
|
||||||
(#:retries . ,#'default-retries))
|
(#:retries . ,#'default-retries)
|
||||||
|
(#:custom . ,#'defer-all))
|
||||||
(syntax kw-args)
|
(syntax kw-args)
|
||||||
stx)])
|
stx)])
|
||||||
(with-syntax ([generate (term-generator #'lang #'pat #'(generation-decisions) #'retries 'generate-term)])
|
(with-syntax ([generate (term-generator #'lang
|
||||||
|
#'pat
|
||||||
|
#'(generation-decisions)
|
||||||
|
#'custom
|
||||||
|
#'retries
|
||||||
|
'generate-term)])
|
||||||
(syntax/loc stx
|
(syntax/loc stx
|
||||||
(let-values ([(term _) (generate size attempt)])
|
(let-values ([(term _) (generate size attempt)])
|
||||||
term))))]
|
term))))]
|
||||||
|
@ -702,25 +734,35 @@
|
||||||
(let-values ([(names names/ellipses)
|
(let-values ([(names names/ellipses)
|
||||||
(extract-names (language-id-nts #'lang 'redex-check)
|
(extract-names (language-id-nts #'lang 'redex-check)
|
||||||
'redex-check #t #'pat)]
|
'redex-check #t #'pat)]
|
||||||
[(attempts-stx source-stx retries-stx)
|
[(attempts-stx source-stx retries-stx custom-stx)
|
||||||
(apply values
|
(apply values
|
||||||
(parse-kw-args `((#:attempts . ,#'default-check-attempts)
|
(parse-kw-args `((#:attempts . ,#'default-check-attempts)
|
||||||
(#:source . #f)
|
(#:source . #f)
|
||||||
(#:retries . ,#'default-retries))
|
(#:retries . ,#'default-retries)
|
||||||
|
(#:custom . ,#'defer-all))
|
||||||
(syntax kw-args)
|
(syntax kw-args)
|
||||||
stx))])
|
stx))])
|
||||||
(with-syntax ([(name ...) names]
|
(with-syntax ([(name ...) names]
|
||||||
[(name/ellipses ...) names/ellipses]
|
[(name/ellipses ...) names/ellipses]
|
||||||
[attempts attempts-stx]
|
|
||||||
[retries retries-stx]
|
|
||||||
[show (show-message stx)])
|
[show (show-message stx)])
|
||||||
(with-syntax ([property (syntax
|
(with-syntax ([property (syntax
|
||||||
(λ (_ bindings)
|
(λ (_ bindings)
|
||||||
(term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
|
(term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
|
||||||
property)))])
|
property)))])
|
||||||
(quasisyntax/loc stx
|
(quasisyntax/loc stx
|
||||||
(let ([att attempts]
|
(let ([att #,attempts-stx]
|
||||||
[ret retries])
|
[ret #,retries-stx]
|
||||||
|
[custom (contract
|
||||||
|
(-> any/c natural-number/c any/c any/c hash? natural-number/c
|
||||||
|
(->* (any/c)
|
||||||
|
(#:size natural-number/c
|
||||||
|
#:contractum any/c
|
||||||
|
#:acc any/c
|
||||||
|
#:env hash?)
|
||||||
|
(values any/c hash?))
|
||||||
|
(-> any/c (values any/c hash?))
|
||||||
|
(values any/c hash?))
|
||||||
|
#,custom-stx '+ '-)])
|
||||||
(assert-nat 'redex-check att)
|
(assert-nat 'redex-check att)
|
||||||
(assert-nat 'redex-check ret)
|
(assert-nat 'redex-check ret)
|
||||||
(unsyntax
|
(unsyntax
|
||||||
|
@ -739,14 +781,21 @@
|
||||||
(map rewrite-proc-lhs (reduction-relation-make-procs r))
|
(map rewrite-proc-lhs (reduction-relation-make-procs r))
|
||||||
(reduction-relation-srcs r)
|
(reduction-relation-srcs r)
|
||||||
(reduction-relation-lang r)))])])
|
(reduction-relation-lang r)))])])
|
||||||
(check-prop-srcs
|
(check-prop-srcs
|
||||||
lang pats srcs property random-decisions@ (max 1 (floor (/ att (length pats)))) ret
|
lang
|
||||||
|
pats
|
||||||
|
srcs
|
||||||
|
property
|
||||||
|
random-decisions@
|
||||||
|
custom
|
||||||
|
(max 1 (floor (/ att (length pats))))
|
||||||
|
ret
|
||||||
'redex-check
|
'redex-check
|
||||||
show
|
show
|
||||||
(test-match lang pat)
|
(test-match lang pat)
|
||||||
(λ (generated) (redex-error 'redex-check "~s does not match ~s" generated 'pat))))
|
(λ (generated) (redex-error 'redex-check "~s does not match ~s" generated 'pat))))
|
||||||
#`(check-prop
|
#`(check-prop
|
||||||
#,(term-generator #'lang #'pat #'random-decisions@ #'ret 'redex-check)
|
#,(term-generator #'lang #'pat #'random-decisions@ #'custom #'ret 'redex-check)
|
||||||
property att show)))
|
property att show)))
|
||||||
(void))))))]))
|
(void))))))]))
|
||||||
|
|
||||||
|
@ -793,9 +842,10 @@
|
||||||
[(_ name . kw-args)
|
[(_ name . kw-args)
|
||||||
(identifier? #'name)
|
(identifier? #'name)
|
||||||
(with-syntax ([m (metafunc/err #'name stx)]
|
(with-syntax ([m (metafunc/err #'name stx)]
|
||||||
[(attempts retries)
|
[(attempts retries custom)
|
||||||
(parse-kw-args `((#:attempts . ,#'default-check-attempts)
|
(parse-kw-args `((#:attempts . ,#'default-check-attempts)
|
||||||
(#:retries . ,#'default-retries))
|
(#:retries . ,#'default-retries)
|
||||||
|
(#:custom . ,#'defer-all))
|
||||||
(syntax kw-args)
|
(syntax kw-args)
|
||||||
stx)]
|
stx)]
|
||||||
[show (show-message stx)])
|
[show (show-message stx)])
|
||||||
|
@ -806,7 +856,7 @@
|
||||||
[att attempts])
|
[att attempts])
|
||||||
(assert-nat 'check-metafunction-contract att)
|
(assert-nat 'check-metafunction-contract att)
|
||||||
(check-prop
|
(check-prop
|
||||||
((generate lang decisions@ retries 'check-metafunction-contract)
|
((generate lang decisions@ custom retries 'check-metafunction-contract)
|
||||||
(if dom dom '(any (... ...))))
|
(if dom dom '(any (... ...))))
|
||||||
(λ (t _)
|
(λ (t _)
|
||||||
(with-handlers ([exn:fail:redex? (λ (_) #f)])
|
(with-handlers ([exn:fail:redex? (λ (_) #f)])
|
||||||
|
@ -814,10 +864,10 @@
|
||||||
att
|
att
|
||||||
show))))]))
|
show))))]))
|
||||||
|
|
||||||
(define (check-prop-srcs lang pats srcs prop decisions@ attempts retries what show
|
(define (check-prop-srcs lang pats srcs prop decisions@ custom attempts retries what show
|
||||||
[match #f]
|
[match #f]
|
||||||
[match-fail #f])
|
[match-fail #f])
|
||||||
(let ([lang-gen (generate lang decisions@ retries what)])
|
(let ([lang-gen (generate lang decisions@ custom retries what)])
|
||||||
(when (for/and ([pat pats] [src srcs])
|
(when (for/and ([pat pats] [src srcs])
|
||||||
(check
|
(check
|
||||||
(lang-gen pat)
|
(lang-gen pat)
|
||||||
|
@ -839,9 +889,10 @@
|
||||||
(syntax-case stx ()
|
(syntax-case stx ()
|
||||||
[(_ name property . kw-args)
|
[(_ name property . kw-args)
|
||||||
(with-syntax ([m (metafunc/err #'name stx)]
|
(with-syntax ([m (metafunc/err #'name stx)]
|
||||||
[(attempts retries)
|
[(attempts retries custom)
|
||||||
(parse-kw-args `((#:attempts . , #'default-check-attempts)
|
(parse-kw-args `((#:attempts . , #'default-check-attempts)
|
||||||
(#:retries . ,#'default-retries))
|
(#:retries . ,#'default-retries)
|
||||||
|
(#:custm . ,#'defer-all))
|
||||||
(syntax kw-args)
|
(syntax kw-args)
|
||||||
stx)]
|
stx)]
|
||||||
[show (show-message stx)])
|
[show (show-message stx)])
|
||||||
|
@ -855,6 +906,7 @@
|
||||||
(metafunc-srcs m)
|
(metafunc-srcs m)
|
||||||
(λ (term _) (property term))
|
(λ (term _) (property term))
|
||||||
(generation-decisions)
|
(generation-decisions)
|
||||||
|
custom
|
||||||
att
|
att
|
||||||
ret
|
ret
|
||||||
'check-metafunction
|
'check-metafunction
|
||||||
|
@ -867,10 +919,11 @@
|
||||||
(define-syntax (check-reduction-relation stx)
|
(define-syntax (check-reduction-relation stx)
|
||||||
(syntax-case stx ()
|
(syntax-case stx ()
|
||||||
[(_ relation property . kw-args)
|
[(_ relation property . kw-args)
|
||||||
(with-syntax ([(attempts retries decisions@)
|
(with-syntax ([(attempts retries decisions@ custom)
|
||||||
(parse-kw-args `((#:attempts . , #'default-check-attempts)
|
(parse-kw-args `((#:attempts . , #'default-check-attempts)
|
||||||
(#:retries . ,#'default-retries)
|
(#:retries . ,#'default-retries)
|
||||||
(#:decisions . ,#'random-decisions@))
|
(#:decisions . ,#'random-decisions@)
|
||||||
|
(#:custom . ,#'defer-all))
|
||||||
(syntax kw-args)
|
(syntax kw-args)
|
||||||
stx)]
|
stx)]
|
||||||
[show (show-message stx)])
|
[show (show-message stx)])
|
||||||
|
@ -886,6 +939,7 @@
|
||||||
(reduction-relation-srcs rel)
|
(reduction-relation-srcs rel)
|
||||||
(λ (term _) (property term))
|
(λ (term _) (property term))
|
||||||
decisions@
|
decisions@
|
||||||
|
custom
|
||||||
attempts
|
attempts
|
||||||
retries
|
retries
|
||||||
'check-reduction-relation
|
'check-reduction-relation
|
||||||
|
|
Loading…
Reference in New Issue
Block a user