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

Improved error reporting for side-conditions Redex can't satisfy

Browse Source 
svn: r16128
This commit is contained in:
Casey Klein 2009-09-25 15:16:29 +00:00
parent df409ae42f
commit 29a3ed2a20
11 changed files with 186 additions and 123 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
collects/redex/private/error.ss
View File

@ -4,4 +4,5 @@
(let ([str (format "~a: ~a" name (apply format fmt args))])
(raise (make-exn:fail:redex str (current-continuation-marks)))))
(provide redex-error
exn:fail:redex?)
exn:fail:redex?
(struct-out exn:fail:redex))

19
collects/redex/private/matcher-test.ss
View File

@ -417,21 +417,21 @@
'(a (b (c (d e))))
none)))
(test-empty `(+ 1 (side-condition any ,(lambda (bindings) #t)))
(test-empty `(+ 1 (side-condition any ,(lambda (bindings) #t) #t))
'(+ 1 b)
(list (make-test-mtch (make-bindings (list (make-bind 'any 'b))) '(+ 1 b) none)))
(test-empty `(+ 1 (side-condition any ,(lambda (bindings) #f)))
(test-empty `(+ 1 (side-condition any ,(lambda (bindings) #f) #f))
'(+ 1 b)
#f)
(test-empty `(+ 1 (side-condition b ,(lambda (bindings) #t)))
(test-empty `(+ 1 (side-condition b ,(lambda (bindings) #t) #t))
'(+ 1 b)
(list (make-test-mtch (make-bindings '()) '(+ 1 b) none)))
(test-empty `(+ 1 (side-condition a ,(lambda (bindings) #t)))
(test-empty `(+ 1 (side-condition a ,(lambda (bindings) #t)) #t)
'(+ 1 b)
#f)
(test-empty `(side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a)))
(test-empty `(side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a)) (eq? (term x) 'a))
'a
(list
(make-test-mtch (make-bindings (list (make-bind 'x 'a)
@ -439,7 +439,7 @@
'a
none)))
(test-empty `(+ 1 (side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a))))
(test-empty `(+ 1 (side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a)) (eq? (term x) 'a)))
'(+ 1 a)
(list
(make-test-mtch (make-bindings (list (make-bind 'x 'a)
@ -447,16 +447,17 @@
'(+ 1 a)
none)))
(test-empty `(side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a)))
(test-empty `(side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a)) (eq? (term x) 'a))
'b
#f)
(test-empty `(+ 1 (side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a))))
(test-empty `(+ 1 (side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a)) (eq? (term x) 'a)))
'(+ 1 b)
#f)
(test-empty `(side-condition ((any_1 ..._a) (any_2 ..._a))
,(lambda (bindings) (error 'should-not-be-called)))
,(lambda (bindings) (error 'should-not-be-called))
(error 'should-not-be-called))
'((1 2 3) (4 5))
#f)

16
collects/redex/private/matcher.ss
View File

@ -211,7 +211,7 @@ before the pattern compiler is invoked.
(loop p1)
(loop p2)]
[`(hide-hole ,p) (loop p)]
[`(side-condition ,p ,g)
[`(side-condition ,p ,g ,e)
(loop p)]
[`(cross ,s) (void)]
[_
@ -247,7 +247,7 @@ before the pattern compiler is invoked.
[`(in-hole ,context ,contractum)
(recur contractum)]
[`(hide-hole ,arg) #f]
[`(side-condition ,pat ,condition)
[`(side-condition ,pat ,condition ,expr)
(recur pat)]
[(? list?)
(ormap recur pattern)]
@ -414,10 +414,10 @@ before the pattern compiler is invoked.
(let ([m (loop p)])
(lambda (l)
`(hide-hole ,(m l))))]
[`(side-condition ,pat ,condition)
[`(side-condition ,pat ,condition ,expr)
(let ([patf (loop pat)])
(lambda (l)
`(side-condition ,(patf l) ,condition)))]
`(side-condition ,(patf l) ,condition ,expr)))]
[(? list?)
(let ([f/pats
(let l-loop ([pattern pattern])
@ -505,7 +505,7 @@ before the pattern compiler is invoked.
(recur context)]
[`(hide-hole ,p)
(recur p)]
[`(side-condition ,pat ,condition)
[`(side-condition ,pat ,condition ,expr)
(recur pat)]
[(? list?)
#t]
@ -554,7 +554,7 @@ before the pattern compiler is invoked.
(recur context)]
[`(hide-hole ,p)
(recur p)]
[`(side-condition ,pat ,condition)
[`(side-condition ,pat ,condition ,expr)
(recur pat)]
[(? list?)
#f]
@ -765,7 +765,7 @@ before the pattern compiler is invoked.
matches))))
#f))]
[`(side-condition ,pat ,condition)
[`(side-condition ,pat ,condition ,expr)
(let-values ([(match-pat has-hole?) (compile-pattern/default-cache pat)])
(values
(lambda (exp hole-info)
@ -1485,7 +1485,7 @@ before the pattern compiler is invoked.
(loop pat (cons (make-bind name '()) ribs)))]
[`(in-hole ,context ,contractum) (loop context (loop contractum ribs))]
[`(hide-hole ,p) (loop p ribs)]
[`(side-condition ,pat ,test) (loop pat ribs)]
[`(side-condition ,pat ,test ,expr) (loop pat ribs)]
[(? list?)
(let-values ([(rewritten has-hole?) (rewrite-ellipses non-underscore-binder? pattern (lambda (x) (values x #f)))])
(let i-loop ([r-exps rewritten]

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

@ -162,6 +162,7 @@
acc)))])))))
(rewrite-proc-name make-proc)
(rewrite-proc-lhs make-proc)
(rewrite-proc-lhs-src make-proc)
(rewrite-proc-id make-proc)))
(reduction-relation-make-procs red))
(reduction-relation-rule-names red)
@ -693,9 +694,11 @@
'predicate
#'#t)])
(with-syntax ([side-conditions-rewritten (rw-sc from)]
[lhs-w/extras (rw-sc #`(side-condition
#,from
#,test-case-body-code))]
[lhs-w/extras (rw-sc #`(side-condition #,from #,test-case-body-code))]
[lhs-source (format "~a:~a:~a"
(syntax-source from)
(syntax-line from)
(syntax-column from))]
[name name]
[lang lang]
[(names ...) names]
@ -733,6 +736,7 @@
other-matches)))))
name
(λ (lang) (let (test-case-compile-pattern-bindings ...) `lhs-w/extras))
lhs-source
case-id)))))))
(define (process-extras stx orig-name name-table extras)
@ -926,6 +930,7 @@
other-matches)))))
(rewrite-proc-name child-make-proc)
(λ (lang) (subst lhs-frm-id ((rewrite-proc-lhs child-make-proc) lang) rhs-from))
(rewrite-proc-lhs child-make-proc)
(rewrite-proc-id child-make-proc)))
(define relation-coverage (make-parameter #f))
@ -989,7 +994,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 10 0 #f null (current-inspector) 0))
(make-struct-type 'metafunc-proc #f 11 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))
@ -999,6 +1004,7 @@
(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 metafunc-proc-lhs-pats (make-struct-field-accessor metafunc-proc-ref 9))
(define metafunc-proc-src-locs (make-struct-field-accessor metafunc-proc-ref 10))
(define-struct metafunction (proc))
(define-syntax (in-domain? stx)
@ -1105,7 +1111,7 @@
(tl-side-cond/binds ...))
(parse-extras #'((stuff ...) ...))])
(with-syntax ([(((cp-let-bindings ...) rhs/wheres) ...)
(map (λ (sc/b rhs)
(map (λ (sc/b rhs)
(let-values ([(body-code cp-let-bindings)
(bind-withs
syn-error-name '()
@ -1140,6 +1146,13 @@
#t
x))
(syntax->list (syntax ((side-condition lhs rg-rhs/wheres) ...))))]
[(clause-src ...)
(map (λ (lhs)
(format "~a:~a:~a"
(syntax-source lhs)
(syntax-line lhs)
(syntax-column lhs)))
pats)]
[dom-side-conditions-rewritten
(and dom-ctcs
(rewrite-side-conditions/check-errs
@ -1252,7 +1265,8 @@
rhss
(let ([name (lambda (x) (name-predicate x))]) name)
dsc
rg-sc))
rg-sc
`(clause-src ...)))
dsc
`codom-side-conditions-rewritten
'name
@ -1279,7 +1293,7 @@
;; initial test determines if a contract is specified or not
(cond
[(pair? (syntax-e (car (syntax->list rest))))
(values #f #f #'any (check-clauses stx syn-error-name rest relation?))]
(values #f #f #'any (check-clauses stx syn-error-name (syntax->list rest) relation?))]
[else
(syntax-case rest ()
[(id colon more ...)
@ -2140,6 +2154,8 @@
metafunc-proc-in-dom?
metafunc-proc-dom-pat
metafunc-proc-lhs-pats
metafunc-proc-src-locs
metafunc-proc?
(struct-out binds))

10
collects/redex/private/rewrite-side-conditions.ss
View File

@ -42,14 +42,18 @@
(with-syntax ([pat (loop (syntax pre-pat))])
(let-values ([(names names/ellipses) (extract-names all-nts what bind-names? (syntax pat))])
(with-syntax ([(name ...) names]
[(name/ellipses ...) names/ellipses])
[(name/ellipses ...) names/ellipses]
[src-loc (parameterize ([print-syntax-width 0])
(format "~s" #'exp))])
(syntax/loc term
(side-condition
pat
,(lambda (bindings)
(term-let
([name/ellipses (lookup-binding bindings 'name)] ...)
exp)))))))]
exp))
; For use in error messages.
src-loc)))))]
[(side-condition a ...) (expected-exact 'side-condition 2 term)]
[side-condition (expected-arguments 'side-condition term)]
[(variable-except a ...) #`(variable-except #,@(map loop (syntax->list (syntax (a ...)))))]
@ -101,7 +105,7 @@
(loop (syntax pat1)
(loop (syntax pat2) names depth)
depth)]
[(side-condition pat e)
[(side-condition pat . rest)
(loop (syntax pat) names depth)]
[(pat ...)
(let i-loop ([pats (syntax->list (syntax (pat ...)))]

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

@ -267,7 +267,7 @@
null)
(test (generate-term/decisions lang d 5 0 (decisions #:seq (list (λ (_) 2))))
'(4 4 4 4 (4 4) (4 4)))
(test (raised-exn-msg exn:fail:redex? (generate-term lang e 5 #:retries 42))
(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 (generate-term/decisions lang f 5 0 (decisions #:seq (list (λ (_) 0)))) null)
(test (generate-term/decisions
@ -319,7 +319,7 @@
(decisions #:num (list (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 2))))
'(1 1 2))
(test
(raised-exn-msg exn:fail:redex? (generate-term lang b 5000))
(raised-exn-msg exn:fail:redex:generation-failure? (generate-term lang b 5000))
#rx"unable"))
(let ()
@ -342,10 +342,10 @@
(x variable))
(test (generate-term lang b 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))
#rx"unable to generate")
(test (raised-exn-msg exn:fail:redex:generation-failure? (generate-term lang c 5))
#px"unable to generate pattern \\(side-condition a\\_1 #<syntax:.*\\/rg-test\\.ss:\\d+:\\d+>\\)")
(test (let/ec k
(generate-term lang (number_1 (side-condition any (k (term number_1)))) 5))
(generate-term lang (number_1 (side-condition 7 (k (term number_1)))) 5))
'number_1)
(test ; mismatch patterns work with side-condition failure/retry
@ -665,7 +665,19 @@
(redex-check lang (n) (eq? 42 (term n))
#:attempts 1
#:source mf)))
#rx"counterexample found after 1 attempt with clause #2:\n\\(0\\)\n"))
#px"counterexample found after 1 attempt with clause at .*:\\d+:\\d+:\n\\(0\\)\n"))
(let ()
(define-metafunction lang
[(f)
dontcare
(side-condition #f)])
(test (raised-exn-msg
exn:fail:redex:generation-failure?
(redex-check lang any #t
#:attempts 1
#:source f))
#px"unable to generate LHS of clause at .*:\\d+:\\d+"))
(let ()
(define-metafunction lang
@ -684,18 +696,29 @@
(redex-check lang n #t #:source (reduction-relation lang (--> x 1))))
#rx"x does not match n")
(test (raised-exn-msg
exn:fail:redex?
exn:fail:redex:generation-failure?
(redex-check lang (side-condition any #f) #t #:retries 42 #:attempts 1))
#rx"^redex-check: unable .* in 42")
(test (raised-exn-msg
exn:fail:redex?
(redex-check lang any #t
#:source (reduction-relation
lang
(--> (side-condition any #f) any))
#:retries 42
#:attempts 1))
#rx"^redex-check: unable .* in 42"))
(let-syntax ([test-gen-fail
(syntax-rules ()
[(_ rhs expected)
(test
(raised-exn-msg
exn:fail:redex:generation-failure?
(redex-check lang any #t
#:source (reduction-relation
lang
rhs)
#:retries 42
#:attempts 1))
expected)])])
(test-gen-fail
(--> (side-condition any #f) any)
#px"^redex-check: unable to generate LHS of clause at .*:\\d+:\\d+ in 42")
(test-gen-fail
(--> (side-condition any #f) any impossible)
#rx"^redex-check: unable to generate LHS of impossible in 42")))
;; check-metafunction-contract
(let ()
@ -749,7 +772,7 @@
;; Unable to generate domain
(test (raised-exn-msg
exn:fail:redex?
exn:fail:redex:generation-failure?
(check-metafunction-contract j #:attempts 1 #:retries 42))
#rx"^check-metafunction-contract: unable .* in 42"))
@ -788,7 +811,11 @@
#rx"counterexample found after 1 attempt with name:\n1\n")
(test (output
(λ () (check-reduction-relation S (curry eq? 1))))
#rx"counterexample found after 1 attempt with unnamed:\n3\n"))
#px"counterexample found after 1 attempt with clause at .*:\\d+:\\d+:\n3\n"))
(test (output
(λ () (check-reduction-relation (reduction-relation L (--> 1 2) (--> 3 4 name)) (curry eq? 1))))
#px"counterexample found after 1 attempt with name:\n3\n")
(let ([T (reduction-relation
L
@ -810,7 +837,7 @@
(let ([U (reduction-relation L (--> (side-condition any #f) any))])
(test (raised-exn-msg
exn:fail:redex?
exn:fail:redex:generation-failure?
(check-reduction-relation U (λ (_) #t)))
#rx"^check-reduction-relation: unable")))
@ -847,13 +874,13 @@
(test (output (λ () (check-metafunction m (λ (_) #t)))) #rx"no counterexamples")
(test (output (λ () (check-metafunction m (curry eq? 1))))
#rx"check-metafunction:.*counterexample found after 1 attempt with clause #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?
exn:fail:redex:generation-failure?
(check-metafunction n (λ (_) #t) #:retries 42))
#rx"check-metafunction: unable .* in 42"))

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

@ -171,6 +171,12 @@
[parsed (parse-language lang)])
(make-rg-lang parsed lits (find-base-cases parsed))))
(define-struct (exn:fail:redex:generation-failure exn:fail:redex) ())
(define (raise-gen-fail who what attempts)
(let ([str (format "~a: unable to generate ~a in ~a attempt~a"
who what attempts (if (= attempts 1) "" "s"))])
(raise (make-exn:fail:redex:generation-failure str (current-continuation-marks)))))
(define (generate lang decisions@ user-gen retries what)
(define-values/invoke-unit decisions@
(import) (export decisions^))
@ -231,10 +237,7 @@
[size init-sz]
[attempt init-att])
(if (zero? remaining)
(redex-error what "unable to generate pattern ~s in ~a attempt~a"
name
retries
(if (= retries 1) "" "s"))
(raise-gen-fail what (format "pattern ~a" name) retries)
(let-values ([(term env) (gen size attempt)])
(if (pred term env)
(values term env)
@ -317,8 +320,8 @@
[`string
(values ((next-string-decision) (rg-lang-lits lang) attempt)
env)]
[`(side-condition ,pat ,(? procedure? condition))
(generate/pred (unparse-pattern pat)
[`(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)]
@ -575,6 +578,9 @@
[(and (? (λ (_) (not (eq? mode 'cross)))) `(cross ,(and (? (is-nt? lang)) nt)))
(let ([nt-str (symbol->string nt)])
(values `(cross ,(string->symbol (string-append nt-str "-" nt-str))) vars))]
[`(side-condition ,pat ,guard ,guard-src-loc)
(let-values ([(parsed vars) (recur pat vars)])
(values `(side-condition ,parsed ,guard ,guard-src-loc) vars))]
[(cons first rest)
(let-values ([(first-parsed vars) (recur first vars)])
(let-values ([(rest-parsed vars) (recur rest vars)])
@ -667,11 +673,13 @@
(if m m (raise-syntax-error #f "not a metafunction" stx name))))
(define (assert-nat name x)
(unless (and (integer? x) (>= x 0))
(raise-type-error name "natural number" x)))
(if (and (integer? x) (>= x 0))
x
(raise-type-error name "natural number" x)))
(define (assert-rel name x)
(unless (reduction-relation? x)
(raise-type-error 'redex-check "reduction-relation" x)))
(if (reduction-relation? x)
x
(raise-type-error 'redex-check "reduction-relation" x)))
(define (defer-all pat size in-hole acc env att recur defer)
(defer acc))
@ -742,8 +750,8 @@
(term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
property)))])
(quasisyntax/loc stx
(let ([att #,attempts-stx]
[ret #,retries-stx]
(let ([att (assert-nat 'redex-check #,attempts-stx)]
[ret (assert-nat 'redex-check #,retries-stx)]
[custom (contract
(-> any/c natural-number/c any/c any/c hash? natural-number/c
(->* (any/c)
@ -755,32 +763,21 @@
(-> any/c (values any/c hash?))
(values any/c hash?))
#,custom-stx '+ '-)])
(assert-nat 'redex-check att)
(assert-nat 'redex-check ret)
(unsyntax
(if source-stx
#`(let-values
([(pats srcs src-lang)
#,(cond [(and (identifier? source-stx) (metafunc source-stx))
=>
(λ (m) #`(values (metafunc-proc-lhs-pats #,m)
(metafunc-srcs #,m)
(metafunc-proc-lang #,m)))]
[else
#`(let ([r #,source-stx])
(assert-rel 'redex-check r)
(values
(map (λ (x) ((rewrite-proc-lhs x) lang)) (reduction-relation-make-procs r))
(reduction-relation-srcs r)
(reduction-relation-lang r)))])])
(check-prop-srcs
#`(let-values ([(metafunc/red-rel num-cases)
#,(cond [(and (identifier? source-stx) (metafunc source-stx))
=> (λ (x) #`(values #,x (length (metafunc-proc-lhs-pats #,x))))]
[else
#`(let ([r (assert-rel 'redex-check #,source-stx)])
(values r (length (reduction-relation-make-procs r))))])])
(check-lhs-pats
lang
pats
srcs
metafunc/red-rel
property
random-decisions@
custom
(max 1 (floor (/ att (length pats))))
(max 1 (floor (/ att num-cases)))
ret
'redex-check
show
@ -845,8 +842,7 @@
(let ([lang (metafunc-proc-lang m)]
[dom (metafunc-proc-dom-pat m)]
[decisions@ (generation-decisions)]
[att attempts])
(assert-nat 'check-metafunction-contract att)
[att (assert-nat 'check-metafunction-contract attempts)])
(check-prop
((generate lang decisions@ custom retries 'check-metafunction-contract)
(if dom dom '(any (... ...))))
@ -856,26 +852,33 @@
att
show))))]))
(define (check-prop-srcs lang pats srcs prop decisions@ custom attempts retries what show
(define (check-lhs-pats lang mf/rr prop decisions@ custom attempts retries what show
[match #f]
[match-fail #f])
(let ([lang-gen (generate lang decisions@ custom retries what)])
(when (for/and ([pat pats] [src srcs])
(check
(lang-gen pat)
prop
attempts
show
#:source src
#:match match
#:match-fail match-fail))
(show
(format "no counterexamples in ~a (with each clause)\n"
(format-attempts attempts))))))
(define (metafunc-srcs m)
(build-list (length (metafunc-proc-lhs-pats m))
(compose (curry format "clause #~s") add1)))
(let-values ([(pats srcs)
(cond [(metafunc-proc? mf/rr)
(values (metafunc-proc-lhs-pats mf/rr)
(metafunction-srcs mf/rr))]
[(reduction-relation? mf/rr)
(values (map (λ (rwp) ((rewrite-proc-lhs rwp) lang)) (reduction-relation-make-procs mf/rr))
(reduction-relation-srcs mf/rr))])])
(when (for/and ([pat pats] [src srcs])
(with-handlers ([exn:fail:redex:generation-failure?
; Produce an error message that blames the LHS as a whole.
(λ (_)
(raise-gen-fail what (format "LHS of ~a" src) retries))])
(check
(lang-gen pat)
prop
attempts
show
#:source src
#:match match
#:match-fail match-fail)))
(show
(format "no counterexamples in ~a (with each clause)\n"
(format-attempts attempts)))))))
(define-syntax (check-metafunction stx)
(syntax-case stx ()
@ -889,13 +892,11 @@
stx)]
[show (show-message stx)])
(syntax/loc stx
(let ([att attempts]
[ret retries])
(assert-nat 'check-metafunction att)
(check-prop-srcs
(let ([att (assert-nat 'check-metafunction attempts)]
[ret (assert-nat 'check-metafunction retries)])
(check-lhs-pats
(metafunc-proc-lang m)
(metafunc-proc-lhs-pats m)
(metafunc-srcs m)
m
(λ (term _) (property term))
(generation-decisions)
custom
@ -905,9 +906,14 @@
show))))]))
(define (reduction-relation-srcs r)
(map (λ (proc) (or (rewrite-proc-name proc) 'unnamed))
(map (λ (proc) (or (rewrite-proc-name proc)
(format "clause at ~a" (rewrite-proc-lhs-src proc))))
(reduction-relation-make-procs r)))
(define (metafunction-srcs m)
(map (curry format "clause at ~a")
(metafunc-proc-src-locs m)))
(define-syntax (check-reduction-relation stx)
(syntax-case stx ()
[(_ relation property . kw-args)
@ -921,15 +927,11 @@
[show (show-message stx)])
(syntax/loc stx
(let ([att attempts]
[ret retries]
[rel relation])
(assert-nat 'check-reduction-relation att)
(assert-rel 'check-reduction-relation rel)
(check-prop-srcs
[ret (assert-nat 'check-reduction-relation retries)]
[rel (assert-rel 'check-reduction-relation relation)])
(check-lhs-pats
(reduction-relation-lang rel)
(map (λ (x) ((rewrite-proc-lhs x) (reduction-relation-lang rel)))
(reduction-relation-make-procs rel))
(reduction-relation-srcs rel)
rel
(λ (term _) (property term))
decisions@
custom
@ -969,7 +971,8 @@
generate-term
check-metafunction-contract
check-reduction-relation
check-metafunction)
check-metafunction
exn:fail:redex:generation-failure?)
(provide (struct-out ellipsis)
(struct-out mismatch)

11
collects/redex/private/struct.ss
View File

@ -11,7 +11,8 @@
build-reduction-relation
reduction-relation?
empty-reduction-relation
make-rewrite-proc rewrite-proc? rewrite-proc-name rewrite-proc-lhs rewrite-proc-id
make-rewrite-proc rewrite-proc? rewrite-proc-name
rewrite-proc-lhs rewrite-proc-lhs-src rewrite-proc-id
(struct-out rule-pict))
(define-struct rule-pict (arrow lhs rhs label side-conditions/pattern-binds fresh-vars))
@ -24,15 +25,16 @@
(define-values (make-rewrite-proc
rewrite-proc?
rewrite-proc-name rewrite-proc-lhs rewrite-proc-id)
rewrite-proc-name rewrite-proc-lhs rewrite-proc-lhs-src rewrite-proc-id)
(let ()
(define-values (type constructor predicate accessor mutator)
(make-struct-type 'rewrite-proc #f 4 0 #f '() #f 0))
(make-struct-type 'rewrite-proc #f 5 0 #f '() #f 0))
(values constructor
predicate
(make-struct-field-accessor accessor 1 'name)
(make-struct-field-accessor accessor 2 'lhs)
(make-struct-field-accessor accessor 3 'id))))
(make-struct-field-accessor accessor 3 'lhs-src)
(make-struct-field-accessor accessor 4 'id))))
;; lang : compiled-language
;; make-procs = (listof (compiled-lang -> proc))
@ -78,6 +80,7 @@
ress))))
(rewrite-proc-name make-proc)
(rewrite-proc-lhs make-proc)
(rewrite-proc-lhs-src make-proc)
(rewrite-proc-id make-proc))
(loop (cdr make-procs)
(+ i 1))))]))])

2
collects/redex/private/tl-test.ss
View File

@ -1606,7 +1606,7 @@
; test shortcut in terms of shortcut
(test (match ((rewrite-proc-lhs (third (reduction-relation-make-procs r))) grammar)
[`(((side-condition 5 ,(? procedure?)) 2) 1) #t]
[`(((side-condition 5 ,(? procedure?) ,_) 2) 1) #t]
[else #f])
#t))

9
collects/redex/redex.scrbl
View File

@ -1129,7 +1129,8 @@ sub-term---regenerating the sub-term if necessary. The optional keyword
argument @scheme[retries-expr] (default @scheme[100]) bounds the number of times that
@scheme[generate-term] retries the generation of any sub-term. If
@scheme[generate-term] is unable to produce a satisfying term after
@scheme[retries-expr] attempts, it raises an error}
@scheme[retries-expr] attempts, it raises an exception recognized by
@scheme[exn:fail:redex:generation-failure?].}
@defform/subs[(redex-check language @#,ttpattern property-expr kw-arg ...)
([kw-arg (code:line #:attempts attempts-expr)
@ -1222,6 +1223,12 @@ when @scheme[relation] is a relation on @scheme[L] with @scheme[n] rules.}
[retries-expr natural-number/c])]{
Like @scheme[check-reduction-relation] but for metafunctions.}
@defproc[(exn:fail:redex:generation-failure? [v any/c]) boolean?]{
Recognizes the exceptions raised by @scheme[generate-term],
@scheme[redex-check], etc. when those forms are unable to produce
a term matching some pattern.
}
@deftech{Debugging PLT Redex Programs}
It is easy to write grammars and reduction rules that are

3
collects/redex/reduction-semantics.ss
View File

@ -47,7 +47,8 @@
generate-term
check-metafunction
check-metafunction-contract
check-reduction-relation)
check-reduction-relation
exn:fail:redex:generation-failure?)
(provide/contract
[current-traced-metafunctions (parameter/c (or/c 'all (listof symbol?)))]