Closes PR 11383
This commit is contained in:
Casey Klein
parent
8bf096b1e3
commit
df810e8e10
|
|
@ -1,10 +1,19 @@
|
|||
#lang scheme
|
||||
#lang racket
|
||||
|
||||
(define (parse-kw-args formals actuals source)
|
||||
(require (for-template racket/base racket/contract))
|
||||
|
||||
(define (parse-kw-args formals actuals source form-name)
|
||||
(let loop ([current (for/hash ([arg formals]) (values (car arg) #f))]
|
||||
[rest actuals])
|
||||
(syntax-case rest ()
|
||||
[() (map (λ (arg) (or (hash-ref current (car arg)) (cdr arg))) formals)]
|
||||
[() (map (λ (arg)
|
||||
(match (hash-ref current (car arg))
|
||||
[#f (cadr arg)]
|
||||
[x (match (cdr (cdr arg))
|
||||
['() x]
|
||||
[`((,ctc ,desc))
|
||||
(apply-contract ctc x desc form-name)])]))
|
||||
formals)]
|
||||
[(kw . rest)
|
||||
(not (keyword? (syntax-e (syntax kw))))
|
||||
(raise-syntax-error #f "expected a keyword" source (syntax kw))]
|
||||
|
|
@ -25,4 +34,19 @@
|
|||
(syntax rest))]
|
||||
[else (raise-syntax-error #f "bad keyword argument syntax" source rest)])))
|
||||
|
||||
(provide parse-kw-args)
|
||||
(define (apply-contract ctc expr desc form)
|
||||
#`(contract #,ctc #,expr
|
||||
#,(let ([m (syntax-source-module expr)])
|
||||
(cond [(module-path-index? m)
|
||||
(format "~a" (module-path-index-resolve m))]
|
||||
[(or (symbol? m) (path? m))
|
||||
(format "~a" m)]
|
||||
[else (format "~s client" form)]))
|
||||
'#,form #,desc
|
||||
#(#,(syntax-source expr)
|
||||
#,(syntax-line expr)
|
||||
#,(syntax-column expr)
|
||||
#,(syntax-position expr)
|
||||
#,(syntax-span expr))))
|
||||
|
||||
(provide parse-kw-args apply-contract)
|
||||
|
|
|
|||
|
|
@ -102,21 +102,6 @@
|
|||
;; E = 0 => p = 1, which breaks random-natural
|
||||
(/ 1 (+ (max 1 E) 1)))
|
||||
|
||||
(define-for-syntax (apply-contract ctc expr desc redex-form)
|
||||
#`(contract #,ctc #,expr
|
||||
#,(let ([m (syntax-source-module expr)])
|
||||
(cond [(module-path-index? m)
|
||||
(format "~a" (module-path-index-resolve m))]
|
||||
[(or (symbol? m) (path? m))
|
||||
(format "~a" m)]
|
||||
[else (format "~s client" redex-form)]))
|
||||
'#,redex-form #,desc
|
||||
#(#,(syntax-source expr)
|
||||
#,(syntax-line expr)
|
||||
#,(syntax-column expr)
|
||||
#,(syntax-position expr)
|
||||
#,(syntax-span expr))))
|
||||
|
||||
; Determines a size measure for numbers, sequences, etc., using the
|
||||
; attempt count.
|
||||
(define default-attempt->size
|
||||
|
|
@ -666,15 +651,6 @@
|
|||
(let ([m (metafunc name)])
|
||||
(if m m (raise-syntax-error #f "not a metafunction" stx name))))
|
||||
|
||||
(define (assert-nat name x)
|
||||
(if (and (integer? x) (>= x 0))
|
||||
x
|
||||
(raise-type-error name "natural number" x)))
|
||||
(define (assert-rel name x)
|
||||
(if (reduction-relation? x)
|
||||
x
|
||||
(raise-type-error name "reduction-relation" x)))
|
||||
|
||||
(define-for-syntax (term-generator lang pat what)
|
||||
(with-syntax ([pattern
|
||||
(rewrite-side-conditions/check-errs
|
||||
|
|
@ -684,25 +660,20 @@
|
|||
|
||||
(define-syntax (generate-term stx)
|
||||
(syntax-case stx ()
|
||||
[(name lang pat size . kw-args)
|
||||
(with-syntax ([(attempt retries)
|
||||
(parse-kw-args `((#:attempt-num . 1)
|
||||
(#:retries . ,#'default-retries))
|
||||
(syntax kw-args)
|
||||
stx)])
|
||||
[(_ lang pat size . kw-args)
|
||||
(with-syntax ([generator (syntax/loc stx (generate-term lang pat))])
|
||||
(syntax/loc stx
|
||||
((generate-term lang pat) size #:attempt-num attempt #:retries retries)))]
|
||||
(generator size . kw-args)))]
|
||||
[(name lang pat)
|
||||
(with-syntax ([make-gen (term-generator #'lang
|
||||
#'pat
|
||||
(syntax-e #'name))])
|
||||
(syntax/loc stx
|
||||
(let ([generate make-gen])
|
||||
#`(let ([generate #,(term-generator #'lang #'pat (syntax-e #'name))])
|
||||
(with-contract
|
||||
name #:result
|
||||
(->* (natural-number/c)
|
||||
(#:attempt-num natural-number/c #:retries natural-number/c)
|
||||
any)
|
||||
(λ (size #:attempt-num [attempt-num 1] #:retries [retries default-retries])
|
||||
(let ([att (assert-nat 'name attempt-num)]
|
||||
[ret (assert-nat 'name retries)])
|
||||
(let-values ([(term _) (generate size att ret)])
|
||||
term))))))]))
|
||||
(let-values ([(term _) (generate size attempt-num retries)])
|
||||
term))))]))
|
||||
|
||||
(define-for-syntax (show-message stx)
|
||||
(syntax-case stx ()
|
||||
|
|
@ -720,27 +691,41 @@
|
|||
"~a: ~a~a"
|
||||
'what (if loc (string-append loc "\n") "") msg)))]))
|
||||
|
||||
(define-for-syntax (contracted-fix stx form [ctc #'(-> any/c any/c)])
|
||||
(and stx (apply-contract ctc stx "#:attempt-size argument" form)))
|
||||
(define-for-syntax (contracted-attempt-size stx form)
|
||||
(apply-contract #'(-> natural-number/c natural-number/c) stx "#:prepare argument" form))
|
||||
(define-for-syntax attempts-keyword
|
||||
(list '#:attempts #'default-check-attempts
|
||||
(list #'natural-number/c "#:attempts argument")))
|
||||
(define-for-syntax source-keyword
|
||||
(list '#:source #f))
|
||||
(define-for-syntax retries-keyword
|
||||
(list '#:retries #'default-retries
|
||||
(list #'natural-number/c "#:retries argument")))
|
||||
(define-for-syntax print?-keyword
|
||||
(list '#:print? #t))
|
||||
(define-for-syntax attempt-size-keyword
|
||||
(list '#:attempt-size #'default-attempt->size
|
||||
(list #'(-> natural-number/c natural-number/c) "#:attempt-size argument")))
|
||||
(define-for-syntax (prepare-keyword lists?)
|
||||
(list '#:prepare #f
|
||||
(list (if lists? #'(-> list? list?) #'(-> any/c any/c))
|
||||
"#:prepare argument")))
|
||||
|
||||
(define-syntax (redex-check stx)
|
||||
(syntax-case stx ()
|
||||
[(_ lang pat property . kw-args)
|
||||
[(form lang pat property . kw-args)
|
||||
(let-values ([(names names/ellipses)
|
||||
(extract-names (language-id-nts #'lang 'redex-check)
|
||||
'redex-check #t #'pat)]
|
||||
[(attempts-stx source-stx retries-stx print?-stx size-stx fix-stx)
|
||||
(apply values
|
||||
(parse-kw-args `((#:attempts . ,#'default-check-attempts)
|
||||
(#:source . #f)
|
||||
(#:retries . ,#'default-retries)
|
||||
(#:print? . #t)
|
||||
(#:attempt-size . ,#'default-attempt->size)
|
||||
(#:prepare . #f))
|
||||
(parse-kw-args (list attempts-keyword
|
||||
source-keyword
|
||||
retries-keyword
|
||||
print?-keyword
|
||||
attempt-size-keyword
|
||||
(prepare-keyword #f))
|
||||
(syntax kw-args)
|
||||
stx))])
|
||||
stx
|
||||
(syntax-e #'form)))])
|
||||
(with-syntax ([(name ...) names]
|
||||
[(name/ellipses ...) names/ellipses]
|
||||
[show (show-message stx)])
|
||||
|
|
@ -750,20 +735,21 @@
|
|||
(term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
|
||||
property))))])
|
||||
(quasisyntax/loc stx
|
||||
(let ([att (assert-nat 'redex-check #,attempts-stx)]
|
||||
[ret (assert-nat 'redex-check #,retries-stx)]
|
||||
(let ([att #,attempts-stx]
|
||||
[ret #,retries-stx]
|
||||
[print? #,print?-stx]
|
||||
[fix #,(contracted-fix fix-stx 'redex-check)]
|
||||
[fix #,fix-stx]
|
||||
[term-match (λ (generated)
|
||||
(cond [(test-match lang pat generated) => values]
|
||||
[else (redex-error 'redex-check "~s does not match ~s" generated 'pat)]))])
|
||||
(parameterize ([attempt->size #,(contracted-attempt-size size-stx 'redex-check)])
|
||||
(parameterize ([attempt->size #,size-stx])
|
||||
#,(if source-stx
|
||||
#`(let-values ([(metafunc/red-rel num-cases)
|
||||
#,(cond [(and (identifier? source-stx) (metafunc source-stx))
|
||||
=> (λ (x) #`(values #,x (length (metafunc-proc-cases #,x))))]
|
||||
[else
|
||||
#`(let ([r (assert-rel 'redex-check #,source-stx)])
|
||||
#`(let ([r #,(apply-contract #'reduction-relation? source-stx
|
||||
"#:source argument" (syntax-e #'form))])
|
||||
(values r (length (reduction-relation-make-procs r))))])])
|
||||
(check-lhs-pats
|
||||
lang
|
||||
|
|
@ -882,26 +868,27 @@
|
|||
|
||||
(define-syntax (check-metafunction stx)
|
||||
(syntax-case stx ()
|
||||
[(_ name property . kw-args)
|
||||
[(form name property . kw-args)
|
||||
(let-values ([(attempts retries print? size fix)
|
||||
(apply values
|
||||
(parse-kw-args `((#:attempts . , #'default-check-attempts)
|
||||
(#:retries . ,#'default-retries)
|
||||
(#:print? . #t)
|
||||
(#:attempt-size . ,#'default-attempt->size)
|
||||
(#:prepare . #f))
|
||||
(parse-kw-args (list attempts-keyword
|
||||
retries-keyword
|
||||
print?-keyword
|
||||
attempt-size-keyword
|
||||
(prepare-keyword #t))
|
||||
(syntax kw-args)
|
||||
stx))]
|
||||
stx
|
||||
(syntax-e #'form)))]
|
||||
[(m) (metafunc/err #'name stx)])
|
||||
(quasisyntax/loc stx
|
||||
(parameterize ([attempt->size #,(contracted-attempt-size size 'check-metafunction)])
|
||||
(let ([att (assert-nat 'check-metafunction #,attempts)]
|
||||
[ret (assert-nat 'check-metafunction #,retries)]
|
||||
[fix #,(contracted-fix fix 'check-metafunction #'(-> (listof any/c) (listof any/c)))])
|
||||
(parameterize ([attempt->size #,size])
|
||||
(let ([att #,attempts]
|
||||
[ret #,retries]
|
||||
[fix #,fix])
|
||||
(check-lhs-pats
|
||||
(metafunc-proc-lang #,m)
|
||||
#,m
|
||||
(term-prop property)
|
||||
(term-prop #,(apply-contract #'(-> (listof any/c) any) #'property #f (syntax-e #'form)))
|
||||
att
|
||||
ret
|
||||
'check-metafunction
|
||||
|
|
@ -919,26 +906,27 @@
|
|||
|
||||
(define-syntax (check-reduction-relation stx)
|
||||
(syntax-case stx ()
|
||||
[(_ relation property . kw-args)
|
||||
[(form relation property . kw-args)
|
||||
(let-values ([(attempts retries print? size fix)
|
||||
(apply values
|
||||
(parse-kw-args `((#:attempts . , #'default-check-attempts)
|
||||
(#:retries . ,#'default-retries)
|
||||
(#:print? . #t)
|
||||
(#:attempt-size . ,#'default-attempt->size)
|
||||
(#:prepare . #f))
|
||||
(parse-kw-args (list attempts-keyword
|
||||
retries-keyword
|
||||
print?-keyword
|
||||
attempt-size-keyword
|
||||
(prepare-keyword #f))
|
||||
(syntax kw-args)
|
||||
stx))])
|
||||
stx
|
||||
(syntax-e #'form)))])
|
||||
(quasisyntax/loc stx
|
||||
(parameterize ([attempt->size #,(contracted-attempt-size size 'check-reduction-relation)])
|
||||
(let ([att (assert-nat 'check-reduction-relation #,attempts)]
|
||||
[ret (assert-nat 'check-reduction-relation #,retries)]
|
||||
[rel (assert-rel 'check-reduction-relation relation)]
|
||||
[fix #,(contracted-fix fix 'check-reduction-relation)])
|
||||
(parameterize ([attempt->size #,size])
|
||||
(let ([att #,attempts]
|
||||
[ret #,retries]
|
||||
[rel #,(apply-contract #'reduction-relation? #'relation #f (syntax-e #'form))]
|
||||
[fix #,fix])
|
||||
(check-lhs-pats
|
||||
(reduction-relation-lang rel)
|
||||
rel
|
||||
(term-prop property)
|
||||
(term-prop #,(apply-contract #'(-> any/c any) #'property #f (syntax-e #'form)))
|
||||
att
|
||||
ret
|
||||
'check-reduction-relation
|
||||
|
|
|
|||
|
|
@ -5,11 +5,11 @@
|
|||
|
||||
(reset-count)
|
||||
|
||||
(let* ([formals `((#:b . ,#'1) (#:c . ,#'2))]
|
||||
(let* ([formals `((#:b ,#'1) (#:c ,#'2))]
|
||||
[parse
|
||||
(λ (actuals)
|
||||
(map syntax-e
|
||||
(parse-kw-args formals (cdr (syntax-e actuals)) actuals)))])
|
||||
(parse-kw-args formals (cdr (syntax-e actuals)) actuals 'dontcare)))])
|
||||
(let-syntax ([msg-src
|
||||
(syntax-rules ()
|
||||
[(_ expr)
|
||||
|
|
@ -43,4 +43,20 @@
|
|||
(test msg #rx"a: invalid keyword")
|
||||
(test src (list kw))))))
|
||||
|
||||
(define-namespace-anchor test-module)
|
||||
|
||||
(let* ([default #'3]
|
||||
[formals `((#:a ,default (,#'(-> number? string?) "#:a arg")))]
|
||||
[parse (λ (actuals) (parse-kw-args formals actuals actuals 'test-form))])
|
||||
(test (first (parse #'())) default)
|
||||
(define arg
|
||||
(eval (first (parse #'(#:a (λ (x) 3))))
|
||||
(namespace-anchor->namespace test-module)))
|
||||
(test (with-handlers ([exn:fail:contract:blame? exn-message])
|
||||
(arg 3))
|
||||
#rx"keyword-macros-test.*broke the contract.*on #:a arg")
|
||||
(test (with-handlers ([exn:fail:contract:blame? exn-message])
|
||||
(arg "NaN"))
|
||||
#rx"test-form.*broke the contract.*on #:a arg"))
|
||||
|
||||
(print-tests-passed 'keyword-macros-test.ss)
|
||||
|
|
|
|||
|
|
@ -19,6 +19,29 @@
|
|||
(sort (hash-map ht cons)
|
||||
(λ (x y) (string<=? (format "~a" (car x)) (format "~a" (car y))))))
|
||||
|
||||
;; output : (-> (-> void) string)
|
||||
(define (output thunk)
|
||||
(let ([p (open-output-string)])
|
||||
(parameterize ([current-output-port p])
|
||||
(unless (void? (thunk))
|
||||
(error 'output "expected void result")))
|
||||
(begin0
|
||||
(get-output-string p)
|
||||
(close-output-port p))))
|
||||
|
||||
(define-syntax (test-contract-violation stx)
|
||||
(syntax-case stx ()
|
||||
[(form expr)
|
||||
(syntax/loc stx (form "" expr))]
|
||||
[(_ name expr)
|
||||
(with-syntax ([expected
|
||||
(syntax/loc stx
|
||||
(regexp (format "rg-test.*broke the contract .* ~a" name)))])
|
||||
#'(test (raised-exn-msg
|
||||
exn:fail?
|
||||
(begin (output (λ () expr)) 'no-violation))
|
||||
expected))]))
|
||||
|
||||
(let ()
|
||||
(define-language lc
|
||||
(e x (e e) (λ (x) e))
|
||||
|
|
@ -197,7 +220,8 @@
|
|||
(test (with-handlers ([exn:fail:syntax? exn-message])
|
||||
(parameterize ([current-namespace ns])
|
||||
(expand #'(generate-term M n))))
|
||||
#rx"generate-term: expected a identifier defined by define-language( in: M)?$"))
|
||||
#rx"generate-term: expected a identifier defined by define-language( in: M)?$")
|
||||
(test-contract-violation (generate-term L n 1.5)))
|
||||
|
||||
;; variable-except pattern
|
||||
(let ()
|
||||
|
|
@ -534,16 +558,6 @@
|
|||
(test (generate-term/decisions L a 0 1 (decisions #:seq '()))
|
||||
(term ())))
|
||||
|
||||
;; output : (-> (-> void) string)
|
||||
(define (output thunk)
|
||||
(let ([p (open-output-string)])
|
||||
(parameterize ([current-output-port p])
|
||||
(unless (void? (thunk))
|
||||
(error 'output "expected void result")))
|
||||
(begin0
|
||||
(get-output-string p)
|
||||
(close-output-port p))))
|
||||
|
||||
;; redex-check
|
||||
(let ()
|
||||
(define-language lang
|
||||
|
|
@ -706,10 +720,19 @@
|
|||
#:source (reduction-relation lang (--> 0 1))
|
||||
#:print? #f)
|
||||
(counterexample 1))
|
||||
(test (raised-exn-msg
|
||||
exn:fail:contract:blame?
|
||||
(redex-check lang natural #t #:prepare (λ () 0)))
|
||||
#rx"rg-test broke the contract")
|
||||
|
||||
(test-contract-violation
|
||||
"#:attempts argument"
|
||||
(redex-check lang natural #t #:attempts 3.5))
|
||||
(test-contract-violation
|
||||
"#:retries argument"
|
||||
(redex-check lang natural #t #:retries 3.5))
|
||||
(test-contract-violation
|
||||
"#:attempt-size argument"
|
||||
(redex-check lang natural #t #:attempt-size -))
|
||||
(test-contract-violation
|
||||
"#:prepare argument"
|
||||
(redex-check lang natural #t #:prepare (λ (_) (values))))
|
||||
|
||||
(test (raised-exn-msg
|
||||
exn:fail:redex?
|
||||
|
|
@ -908,7 +931,22 @@
|
|||
(test (raised-exn-msg
|
||||
exn:fail:redex:generation-failure?
|
||||
(check-reduction-relation U (λ (_) #t)))
|
||||
#rx"^check-reduction-relation: unable")))
|
||||
#rx"^check-reduction-relation: unable"))
|
||||
|
||||
(let ([R (reduction-relation L (--> any any))])
|
||||
(test-contract-violation
|
||||
"#:attempts argument"
|
||||
(check-reduction-relation R values #:attempts -1))
|
||||
(test-contract-violation
|
||||
"#:retries argument"
|
||||
(check-reduction-relation R values #:retries -1))
|
||||
(test-contract-violation
|
||||
"#:attempt-size argument"
|
||||
(check-reduction-relation R values #:attempt-size (λ (_) (values 1 2))))
|
||||
(test-contract-violation
|
||||
"#:prepare argument"
|
||||
(check-reduction-relation R values #:prepare (λ (_) (values 1 2))))
|
||||
(test-contract-violation (check-reduction-relation R #t))))
|
||||
|
||||
; check-metafunction
|
||||
(let ()
|
||||
|
|
@ -1018,13 +1056,23 @@
|
|||
#:prepare (λ (_) (error 'fixer))
|
||||
#:print? #f)))
|
||||
#rx"fixing \\(0\\)")
|
||||
(test (raised-exn-msg
|
||||
exn:fail?
|
||||
|
||||
(let ()
|
||||
(define-metafunction empty
|
||||
[(f 0) 0])
|
||||
(check-metafunction f void #:prepare car #:print? #f)))
|
||||
#rx"rg-test broke the contract")
|
||||
(test-contract-violation
|
||||
"#:attempts argument"
|
||||
(check-metafunction f void #:attempts 3.5))
|
||||
(test-contract-violation
|
||||
"#:retries argument"
|
||||
(check-metafunction f void #:retries 3.5))
|
||||
(test-contract-violation
|
||||
"#:attempt-size argument"
|
||||
(check-metafunction f void #:attempt-size 3.5))
|
||||
(test-contract-violation
|
||||
"#:prepare argument"
|
||||
(check-metafunction f void #:prepare car #:print? #f))
|
||||
(test-contract-violation (check-metafunction f (λ () #t))))
|
||||
|
||||
; Extension reinterprets the LHSs of the base metafunction
|
||||
; relative to the new language.
|
||||
|
|
@ -1055,10 +1103,6 @@
|
|||
(test (output (λ () (check-metafunction m (λ (_) #t)))) #rx"no counterexamples")
|
||||
(test (output (λ () (check-metafunction m (curry eq? 1))))
|
||||
#px"check-metafunction:.*counterexample found after 1 attempt with clause at .*:\\d+:\\d+")
|
||||
(test (raised-exn-msg
|
||||
exn:fail:contract?
|
||||
(check-metafunction m (λ (_) #t) #:attempts 'NaN))
|
||||
#rx"check-metafunction: expected")
|
||||
(test (raised-exn-msg
|
||||
exn:fail:redex:generation-failure?
|
||||
(check-metafunction n (λ (_) #t) #:retries 42))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user