fixed a bug in recent Redex internal pattern rewrite
(discovered by the random testing done for the racket machine model)
This commit is contained in:
Robby Findler
parent
4fe30cf433
commit
5b2d378a77
|
|
@ -1269,7 +1269,7 @@
|
|||
[(nts) (language-id-nts #'lang-exp what)])
|
||||
(with-syntax ([(side-condition-rewritten (vars ...) (ids/depths ...))
|
||||
(rewrite-side-conditions/check-errs nts what #t #'pattern)])
|
||||
(with-syntax ([binders (map syntax-e (syntax->list #'(ids/depths ...)))]
|
||||
(with-syntax ([binders (map syntax-e (syntax->list #'(vars ...)))]
|
||||
[name (syntax-local-infer-name stx)])
|
||||
(syntax
|
||||
(do-test-match lang-exp `side-condition-rewritten 'binders 'name)))))]
|
||||
|
|
@ -2788,7 +2788,7 @@
|
|||
(set! visit-already-failed? #t)
|
||||
(inc-failures)
|
||||
(print-failed srcinfo)
|
||||
(fprintf (current-error-port) "found a term that failed #:pred: ~v\n" t)))))
|
||||
(eprintf "found a term that failed #:pred: ~v\n" t)))))
|
||||
(let-values ([(got got-cycle?) (apply-red red arg #:visit visit)])
|
||||
|
||||
(cond
|
||||
|
|
@ -2796,7 +2796,7 @@
|
|||
(not cycles-ok?))
|
||||
(inc-failures)
|
||||
(print-failed srcinfo)
|
||||
(fprintf (current-error-port) "found a cycle in the reduction graph\n")]
|
||||
(eprintf "found a cycle in the reduction graph\n")]
|
||||
[else
|
||||
(unless visit-already-failed?
|
||||
(let* ([⊆ (λ (s1 s2) (andmap (λ (x1) (memf (λ (x) (equiv? x1 x)) s2)) s1))]
|
||||
|
|
@ -2805,12 +2805,12 @@
|
|||
(inc-failures)
|
||||
(print-failed srcinfo)
|
||||
(for-each
|
||||
(λ (v2) (fprintf (current-error-port) "expected: ~v\n" v2))
|
||||
(λ (v2) (eprintf "expected: ~v\n" v2))
|
||||
expected)
|
||||
(if (empty? got)
|
||||
(fprintf (current-error-port) "got nothing\n")
|
||||
(eprintf "got nothing\n")
|
||||
(for-each
|
||||
(λ (v1) (fprintf (current-error-port) " actual: ~v\n" v1))
|
||||
(λ (v1) (eprintf " actual: ~v\n" v1))
|
||||
got)))))])))
|
||||
|
||||
(define-syntax (test-->>∃ stx)
|
||||
|
|
@ -2839,12 +2839,10 @@
|
|||
(inc-failures)
|
||||
(begin
|
||||
(if (procedure? goal)
|
||||
(fprintf (current-error-port)
|
||||
"no term satisfying ~a reachable from ~a" goal start)
|
||||
(fprintf (current-error-port)
|
||||
"term ~a not reachable from ~a" goal start))
|
||||
(eprintf "no term satisfying ~a reachable from ~a" goal start)
|
||||
(eprintf "term ~a not reachable from ~a" goal start))
|
||||
(when (search-failure-cutoff? result)
|
||||
(fprintf (current-error-port) " (within ~a steps)" steps))
|
||||
(eprintf " (within ~a steps)" steps))
|
||||
(newline (current-error-port))))))
|
||||
|
||||
(define-syntax (test-predicate stx)
|
||||
|
|
@ -2857,7 +2855,7 @@
|
|||
(unless (pred arg)
|
||||
(inc-failures)
|
||||
(print-failed srcinfo)
|
||||
(fprintf (current-error-port) " ~v does not hold for\n ~v\n"
|
||||
(eprintf " ~v does not hold for\n ~v\n"
|
||||
pred arg)))
|
||||
|
||||
(define-syntax (test-equal stx)
|
||||
|
|
@ -2870,16 +2868,15 @@
|
|||
(unless (equal? v1 v2)
|
||||
(inc-failures)
|
||||
(print-failed srcinfo)
|
||||
(fprintf (current-error-port) " actual: ~v\n" v1)
|
||||
(fprintf (current-error-port) "expected: ~v\n" v2)))
|
||||
(eprintf " actual: ~v\n" v1)
|
||||
(eprintf "expected: ~v\n" v2)))
|
||||
|
||||
(define (print-failed srcinfo)
|
||||
(let ([file (list-ref srcinfo 0)]
|
||||
[line (list-ref srcinfo 1)]
|
||||
[column (list-ref srcinfo 2)]
|
||||
[pos (list-ref srcinfo 3)])
|
||||
(fprintf (current-error-port)
|
||||
"FAILED ~a~a\n"
|
||||
(eprintf "FAILED ~a~a\n"
|
||||
(cond
|
||||
[(path? file)
|
||||
(let-values ([(base name dir) (split-path file)])
|
||||
|
|
|
|||
|
|
@ -344,6 +344,8 @@
|
|||
(define-struct id/depth (id depth mismatch?))
|
||||
|
||||
;; extract-names : syntax syntax -> (values (listof syntax) (listof syntax[x | (x ...) | ((x ...) ...) | ...]))
|
||||
;; this function is obsolete and uses of it are suspect. Things should be using
|
||||
;; rewrite-side-conditions/check-errs instead
|
||||
(define (extract-names all-nts what bind-names? orig-stx [mode 'rhs-only])
|
||||
(let* ([dups
|
||||
(let loop ([stx orig-stx]
|
||||
|
|
|
|||
|
|
@ -212,12 +212,10 @@
|
|||
pre-threshold-incr))))))))
|
||||
|
||||
(define (generate/prior name env gen)
|
||||
;(printf "generate/prior ~s ~s ~s\n" name env gen)
|
||||
(let* ([none (gensym)]
|
||||
[prior (hash-ref env name none)])
|
||||
(if (eq? prior none)
|
||||
(let-values ([(term env) (gen)])
|
||||
;(printf "generated ~s for ~s\n" term name)
|
||||
(values term (hash-set env name term)))
|
||||
(values prior env))))
|
||||
|
||||
|
|
@ -265,7 +263,7 @@
|
|||
|
||||
(define (bindings env)
|
||||
(make-bindings
|
||||
(for/fold ([bindings null]) ([(key val) env])
|
||||
(for/fold ([bindings null]) ([(key val) (in-hash env)])
|
||||
(if (symbol? key)
|
||||
(cons (make-bind key val) bindings)
|
||||
bindings))))
|
||||
|
|
@ -341,7 +339,7 @@
|
|||
(add/ret `(list ,@(reverse lpats-rewritten))
|
||||
vars)]
|
||||
[(? (compose not pair?)) (values pat '())])))
|
||||
|
||||
|
||||
(let* ([nt? (is-nt? (if any? sexpp langp))]
|
||||
[mismatches? #f]
|
||||
[generator
|
||||
|
|
@ -751,11 +749,8 @@
|
|||
(let ([m (metafunc name)])
|
||||
(if m m (raise-syntax-error #f "not a metafunction" stx name))))
|
||||
|
||||
(define-for-syntax (term-generator lang pat what)
|
||||
(with-syntax ([(pattern (vars ...) (vars/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs
|
||||
(language-id-nts lang what)
|
||||
what #t pat)])
|
||||
(define-for-syntax (term-generator lang pattern what)
|
||||
(with-syntax ([pattern pattern])
|
||||
#`((compile #,lang '#,what) `pattern)))
|
||||
|
||||
(define-syntax (generate-term stx)
|
||||
|
|
@ -781,8 +776,12 @@
|
|||
(reduction-relation-make-procs r)))])
|
||||
#'rest)]
|
||||
[(_ lang pat . rest)
|
||||
(values #`(list #,(term-generator #'lang #'pat form-name))
|
||||
#'rest)]))
|
||||
(with-syntax ([(pattern (vars ...) (vars/ellipses ...))
|
||||
(rewrite-side-conditions/check-errs
|
||||
(language-id-nts #'lang form-name)
|
||||
form-name #t #'pat)])
|
||||
(values #`(list #,(term-generator #'lang #'pattern form-name))
|
||||
#'rest))]))
|
||||
(define generator-syntax
|
||||
#`(make-generator #,raw-generators '#,form-name #,(client-name stx form-name) #,(src-loc-stx stx)))
|
||||
(syntax-case args ()
|
||||
|
|
@ -841,9 +840,12 @@
|
|||
(define-syntax (redex-check stx)
|
||||
(syntax-case stx ()
|
||||
[(form lang pat property . kw-args)
|
||||
(let-values ([(names names/ellipses)
|
||||
(extract-names (language-id-nts #'lang 'redex-check)
|
||||
'redex-check #t #'pat)]
|
||||
(let-values ([(pattern names names/ellipses)
|
||||
(with-syntax ([(pattern names names/ellipses)
|
||||
(rewrite-side-conditions/check-errs
|
||||
(language-id-nts #'lang 'redex-check)
|
||||
'redex-check #t #'pat)])
|
||||
(values #'pattern #'names #'names/ellipses))]
|
||||
[(attempts-stx source-stx retries-stx print?-stx size-stx fix-stx)
|
||||
(apply values
|
||||
(parse-kw-args (list attempts-keyword
|
||||
|
|
@ -891,7 +893,7 @@
|
|||
fix
|
||||
#:term-match term-match))
|
||||
#`(check-one
|
||||
#,(term-generator #'lang #'pat 'redex-check)
|
||||
#,(term-generator #'lang #'pattern 'redex-check)
|
||||
property att ret (and print? show) fix (and fix term-match)))))))))]))
|
||||
|
||||
(define (format-attempts a)
|
||||
|
|
|
|||
|
|
@ -55,6 +55,15 @@
|
|||
(UN (add1 UN)
|
||||
zero))
|
||||
|
||||
(test (let ([m (redex-match
|
||||
empty-language
|
||||
(side-condition (any_1 ...) #t)
|
||||
'())])
|
||||
(and m
|
||||
(= 1 (length m))
|
||||
(match-bindings (car m))))
|
||||
(list (make-bind 'any_1 '())))
|
||||
|
||||
(test (pair? (redex-match grammar M '(1 1))) #t)
|
||||
(test (pair? (redex-match grammar M '(1 1 1))) #f)
|
||||
(test (pair? (redex-match grammar
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user