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

merge from branch branches/robby/redex-pat2; improved where patterns and a few bug fixes

Browse Source 
svn: r15294
This commit is contained in:
Robby Findler 2009-06-26 01:19:45 +00:00
parent 8ad431b778
commit 7804143400
9 changed files with 313 additions and 141 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
collects/redex/gui.ss
View File

@ -67,6 +67,7 @@
[term-node-set-color! (-> term-node? [term-node-set-color! (-> term-node?
(or/c string? (is-a?/c color%) false/c) (or/c string? (is-a?/c color%) false/c)
void?)] void?)]
[term-node-color (-> term-node? (or/c string? (is-a?/c color%) false/c))]
[term-node-expr (-> term-node? any)] [term-node-expr (-> term-node? any)]
[term-node-set-position! (-> term-node? real? real? void?)] [term-node-set-position! (-> term-node? real? real? void?)]
[term-node-x (-> term-node? real?)] [term-node-x (-> term-node? real?)]

10
collects/redex/private/color-test.ss
View File

@ -35,7 +35,8 @@ In the other window, you expect to see the currently unreducted terms in green a
(floor (- 255 (* val (/ 255 max-val)))) (floor (- 255 (* val (/ 255 max-val))))
0 0
(floor (* val (/ 255 max-val))))))) (floor (* val (/ 255 max-val)))))))
parents))) parents)
(term-node-color term-node)))
(define-language empty-language) (define-language empty-language)
@ -52,10 +53,9 @@ In the other window, you expect to see the currently unreducted terms in green a
(define-language empty-language) (define-language empty-language)
(define (last-color-pred sexp term-node) (define (last-color-pred sexp term-node)
(term-node-set-color! term-node (if (null? (term-node-children term-node))
(if (null? (term-node-children term-node)) "green"
"green" "white"))
"white")))
(traces (reduction-relation (traces (reduction-relation
empty-language empty-language

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

@ -221,32 +221,68 @@
(syntax/loc stx (do-reduction-relation extend-reduction-relation orig-reduction-relation #t lang args ...))])) (syntax/loc stx (do-reduction-relation extend-reduction-relation orig-reduction-relation #t lang args ...))]))
;; the withs, freshs, and side-conditions come in backwards order ;; the withs, freshs, and side-conditions come in backwards order
(define-for-syntax (bind-withs orig-name main stx body) (define-for-syntax (bind-withs orig-name main lang lang-nts stx where-mode body)
(let loop ([stx stx] (let loop ([stx stx]
[body body]) [body body]
[bindings '()])
(syntax-case stx (side-condition where fresh) (syntax-case stx (side-condition where fresh)
[() body] [() (values body bindings)]
[((where x e) y ...) [((where x e) y ...)
(loop #'(y ...) #`(term-let ([x (term e)]) #,body))] (let-values ([(names names/ellipses) (extract-names lang-nts 'reduction-relation #t #'x)])
(with-syntax ([(cpat) (generate-temporaries '(compiled-pattern))]
[side-conditions-rewritten (rewrite-side-conditions/check-errs
lang-nts
'reduction-relation
#f
#'x)]
[(names ...) names]
[(names/ellipses ...) names/ellipses])
(loop #'(y ...)
#`(let ([mtchs (match-pattern cpat (term e))])
(if mtchs
#,
(case where-mode
[(flatten)
#`(apply
append
(map (λ (mtch)
(let ([bindings (mtch-bindings mtch)])
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
#,body)))
mtchs))]
[(predicate)
#`(andmap (λ (mtch)
(let ([bindings (mtch-bindings mtch)])
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
#,body)))
mtchs)]
[else (error 'unknown-where-mode "~s" where-mode)])
#f))
(cons #`[cpat (compile-pattern #,lang `side-conditions-rewritten #t)]
bindings))))]
[((side-condition s ...) y ...) [((side-condition s ...) y ...)
(loop #'(y ...) #`(and s ... #,body))] (loop #'(y ...) #`(and s ... #,body) bindings)]
[((fresh x) y ...) [((fresh x) y ...)
(identifier? #'x) (identifier? #'x)
(loop #'(y ...) #`(term-let ([x (variable-not-in #,main 'x)]) #,body))] (loop #'(y ...)
#`(term-let ([x (variable-not-in #,main 'x)]) #,body)
bindings)]
[((fresh x name) y ...) [((fresh x name) y ...)
(identifier? #'x) (identifier? #'x)
(loop #'(y ...) (loop #'(y ...)
#`(term-let ([x (let ([the-name (term name)]) #`(term-let ([x (let ([the-name (term name)])
(verify-name-ok '#,orig-name the-name) (verify-name-ok '#,orig-name the-name)
(variable-not-in #,main the-name))]) (variable-not-in #,main the-name))])
#,body))] #,body)
bindings)]
[((fresh (y) (x ...)) z ...) [((fresh (y) (x ...)) z ...)
(loop #'(z ...) (loop #'(z ...)
#`(term-let ([(y #,'...) #`(term-let ([(y #,'...)
(variables-not-in #,main (variables-not-in #,main
(map (λ (_ignore_) 'y) (map (λ (_ignore_) 'y)
(term (x ...))))]) (term (x ...))))])
#,body))] #,body)
bindings)]
[((fresh (y) (x ...) names) z ...) [((fresh (y) (x ...) names) z ...)
(loop #'(z ...) (loop #'(z ...)
#`(term-let ([(y #,'...) #`(term-let ([(y #,'...)
@ -254,9 +290,8 @@
[len-counter (term (x ...))]) [len-counter (term (x ...))])
(verify-names-ok '#,orig-name the-names len-counter) (verify-names-ok '#,orig-name the-names len-counter)
(variables-not-in #,main the-names))]) (variables-not-in #,main the-names))])
#,body))]))) #,body)
bindings)])))
(define-struct successful (result))
(define-syntax-set (do-reduction-relation) (define-syntax-set (do-reduction-relation)
(define (do-reduction-relation/proc stx) (define (do-reduction-relation/proc stx)
@ -651,25 +686,67 @@
(let* ([lang-nts (language-id-nts lang-id orig-name)] (let* ([lang-nts (language-id-nts lang-id orig-name)]
[rw-sc (λ (pat) (rewrite-side-conditions/check-errs lang-nts orig-name #t pat))]) [rw-sc (λ (pat) (rewrite-side-conditions/check-errs lang-nts orig-name #t pat))])
(let-values ([(name sides/withs/freshs) (process-extras stx orig-name name-table extras)]) (let-values ([(name sides/withs/freshs) (process-extras stx orig-name name-table extras)])
(let-values ([(names names/ellipses) (extract-names lang-nts orig-name #t from)]) (let-values ([(names names/ellipses) (extract-names lang-nts orig-name #t from)]
[(body-code compile-pattern-bindings)
(bind-withs orig-name
#'main-exp
lang
lang-nts
sides/withs/freshs
'flatten
#`(list (term #,to)))]
[(test-case-body-code test-case-compile-pattern-bindings)
;; this contains some redundant code, eg. the test-case-compile-pattern-bindings
;; are (morally) the same as the compile-pattern-bindings
(bind-withs orig-name
#'#t
lang
lang-nts
sides/withs/freshs
'predicate
#'#t)])
(with-syntax ([side-conditions-rewritten (rw-sc from)] (with-syntax ([side-conditions-rewritten (rw-sc from)]
[lhs-w/extras (rw-sc #`(side-condition #,from #,(bind-withs orig-name #'#t sides/withs/freshs #'#t)))] [lhs-w/extras (rw-sc #`(side-condition
[to to] #,from
#,test-case-body-code))]
[name name] [name name]
[lang lang] [lang lang]
[(names ...) names] [(names ...) names]
[(names/ellipses ...) names/ellipses]) [(names/ellipses ...) names/ellipses]
#`(do-leaf-match [body-code body-code]
[(test-case-compile-pattern-bindings ...) test-case-compile-pattern-bindings]
[(compile-pattern-bindings ...) compile-pattern-bindings])
#`
(let ([case-id (gensym)])
(make-rewrite-proc
(λ (lang)
(let ([cp (compile-pattern lang `side-conditions-rewritten #t)]
compile-pattern-bindings ...)
(λ (main-exp exp f other-matches)
(let ([mtchs (match-pattern cp exp)])
(if mtchs
(let loop ([mtchs mtchs]
[acc other-matches])
(cond
[(null? mtchs) acc]
[else
(let* ([mtch (car mtchs)]
[bindings (mtch-bindings mtch)]
[really-matched
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
body-code)])
(cond
[really-matched
(when (relation-coverage)
(cover-case case-id name (relation-coverage)))
(loop (cdr mtchs)
(map/mt (λ (x) (list name (f x))) really-matched acc))]
[else
(loop (cdr mtchs) acc)]))]))
other-matches)))))
name name
`side-conditions-rewritten (λ (lang) (let (test-case-compile-pattern-bindings ...) `lhs-w/extras))
`lhs-w/extras case-id)))))))
(λ (main bindings)
;; nested term-let's so that the bindings for the variables
;; show up in the `fresh' side-conditions, the bindings for the variables
;; show up in the withs, and the withs show up in the 'fresh' side-conditions
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
#,(bind-withs orig-name #'main sides/withs/freshs
#'(make-successful (term to)))))))))))
(define (process-extras stx orig-name name-table extras) (define (process-extras stx orig-name name-table extras)
(let ([the-name #f] (let ([the-name #f]
@ -751,6 +828,8 @@
[_ [_
(raise-syntax-error orig-name "unknown extra" stx (car extras))])])))) (raise-syntax-error orig-name "unknown extra" stx (car extras))])]))))
;; table-cons! hash-table sym any -> void ;; table-cons! hash-table sym any -> void
;; extends ht at key by `cons'ing hd onto whatever is alrady bound to key (or the empty list, if nothing is) ;; extends ht at key by `cons'ing hd onto whatever is alrady bound to key (or the empty list, if nothing is)
(define (table-cons! ht key hd) (define (table-cons! ht key hd)
@ -859,7 +938,7 @@
acc)))])) acc)))]))
other-matches))))) other-matches)))))
(rewrite-proc-name child-make-proc) (rewrite-proc-name child-make-proc)
(subst lhs-frm-id (rewrite-proc-lhs child-make-proc) rhs-from) (λ (lang) (subst lhs-frm-id ((rewrite-proc-lhs child-make-proc) lang) rhs-from))
(rewrite-proc-id child-make-proc))) (rewrite-proc-id child-make-proc)))
(define relation-coverage (make-parameter #f)) (define relation-coverage (make-parameter #f))
@ -884,27 +963,6 @@
(reduction-relation-make-procs relation)) (reduction-relation-make-procs relation))
(make-coverage h))) (make-coverage h)))
(define (do-leaf-match name pat w/extras proc)
(let ([case-id (gensym)])
(make-rewrite-proc
(λ (lang)
(let ([cp (compile-pattern lang pat #t)])
(λ (main-exp exp f other-matches)
(let ([mtchs (match-pattern cp exp)])
(if mtchs
(map/mt (λ (mtch)
(let ([really-matched (proc main-exp (mtch-bindings mtch))])
(and really-matched
(when (relation-coverage)
(cover-case case-id name (relation-coverage)))
(list name (f (successful-result really-matched))))))
mtchs
other-matches)
other-matches)))))
name
w/extras
case-id)))
(define-syntax (test-match stx) (define-syntax (test-match stx)
(syntax-case stx () (syntax-case stx ()
[(_ lang-exp pattern) [(_ lang-exp pattern)
@ -986,7 +1044,6 @@
; ;
; ;
(define-syntax-set (define-metafunction define-metafunction/extension define-relation) (define-syntax-set (define-metafunction define-metafunction/extension define-relation)
(define (define-metafunction/proc stx) (define (define-metafunction/proc stx)
@ -1061,15 +1118,42 @@
(tl-side-cond/binds ...)) (tl-side-cond/binds ...))
(parse-extras #'((stuff ...) ...))]) (parse-extras #'((stuff ...) ...))])
(let ([lang-nts (language-id-nts #'lang 'define-metafunction)]) (let ([lang-nts (language-id-nts #'lang 'define-metafunction)])
(with-syntax ([(tl-withs ...) (map (λ (sc/b) (bind-withs syn-error-name '() sc/b #t)) (with-syntax ([(((cp-let-bindings ...) rhs/wheres) ...)
(syntax->list #'(tl-side-cond/binds ...)))]) (map (λ (sc/b rhs)
(let-values ([(body-code cp-let-bindings)
(bind-withs
syn-error-name '()
#'lang lang-nts
sc/b 'flatten
#`(list (term #,rhs)))])
(list cp-let-bindings body-code)))
(syntax->list #'(tl-side-cond/binds ...))
(syntax->list #'(rhs ...)))]
[(((rg-cp-let-bindings ...) rg-rhs/wheres) ...)
(map (λ (sc/b rhs)
(let-values ([(body-code cp-let-bindings)
(bind-withs
syn-error-name '()
#'lang lang-nts
sc/b 'predicate
#`#t)])
(list cp-let-bindings body-code)))
(syntax->list #'(tl-side-cond/binds ...))
(syntax->list #'(rhs ...)))])
(with-syntax ([(side-conditions-rewritten ...) (with-syntax ([(side-conditions-rewritten ...)
(map (λ (x) (rewrite-side-conditions/check-errs (map (λ (x) (rewrite-side-conditions/check-errs
lang-nts lang-nts
syn-error-name syn-error-name
#t #t
x)) x))
(syntax->list (syntax ((side-condition lhs tl-withs) ...))))] (syntax->list (syntax (lhs ...))))]
[(rg-side-conditions-rewritten ...)
(map (λ (x) (rewrite-side-conditions/check-errs
lang-nts
syn-error-name
#t
x))
(syntax->list (syntax ((side-condition lhs rg-rhs/wheres) ...))))]
[dom-side-conditions-rewritten [dom-side-conditions-rewritten
(and dom-ctcs (and dom-ctcs
(rewrite-side-conditions/check-errs (rewrite-side-conditions/check-errs
@ -1084,21 +1168,21 @@
#f #f
codom-contract)] codom-contract)]
[(rhs-fns ...) [(rhs-fns ...)
(map (λ (lhs rhs bindings) (map (λ (lhs rhs/where bindings)
(let-values ([(names names/ellipses) (let-values ([(names names/ellipses)
(extract-names lang-nts syn-error-name #t lhs)]) (extract-names lang-nts syn-error-name #t lhs)])
(with-syntax ([(names ...) names] (with-syntax ([(names ...) names]
[(names/ellipses ...) names/ellipses] [(names/ellipses ...) names/ellipses]
[rhs rhs] [rhs/where rhs/where]
[((tl-var tl-exp) ...) bindings]) [((tl-var tl-exp) ...) bindings])
(syntax (syntax
(λ (name bindings) (λ (name bindings)
(term-let-fn ((name name)) (term-let-fn ((name name))
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...) (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
(term-let ([tl-var (term tl-exp)] ...) (term-let ([tl-var (term tl-exp)] ...)
(term rhs))))))))) rhs/where))))))))
(syntax->list (syntax (lhs ...))) (syntax->list (syntax (lhs ...)))
(syntax->list (syntax (rhs ...))) (syntax->list (syntax (rhs/wheres ...)))
(syntax->list (syntax (tl-bindings ...))))] (syntax->list (syntax (tl-bindings ...))))]
[(name2 name-predicate) (generate-temporaries (syntax (name name)))] [(name2 name-predicate) (generate-temporaries (syntax (name name)))]
[((side-cond/lw/uq ...) ...) [((side-cond/lw/uq ...) ...)
@ -1123,41 +1207,44 @@
#`(begin #`(begin
(define-values (name2 name-predicate) (define-values (name2 name-predicate)
(let ([sc `(side-conditions-rewritten ...)] (let ([sc `(side-conditions-rewritten ...)]
[dsc `dom-side-conditions-rewritten]) [dsc `dom-side-conditions-rewritten]
(build-metafunction cp-let-bindings ... ...
lang rg-cp-let-bindings ... ...)
sc (let ([rg-sc `(rg-side-conditions-rewritten ...)])
(list rhs-fns ...) (build-metafunction
#,(if prev-metafunction lang
(let ([term-fn (syntax-local-value prev-metafunction)]) sc
#`(metafunc-proc-cps #,(term-fn-get-id term-fn))) (list rhs-fns ...)
#''()) #,(if prev-metafunction
#,(if prev-metafunction (let ([term-fn (syntax-local-value prev-metafunction)])
(let ([term-fn (syntax-local-value prev-metafunction)]) #`(metafunc-proc-cps #,(term-fn-get-id term-fn)))
#`(metafunc-proc-rhss #,(term-fn-get-id term-fn))) #''())
#''()) #,(if prev-metafunction
(λ (f/dom cps rhss) (let ([term-fn (syntax-local-value prev-metafunction)])
(make-metafunc-proc #`(metafunc-proc-rhss #,(term-fn-get-id term-fn)))
(let ([name (lambda (x) (f/dom x))]) name) #''())
(list (list lhs-for-lw (λ (f/dom cps rhss)
(list side-cond/lw/uq ...) (make-metafunc-proc
(list (cons bind-id/lw bind-pat/lw) ... (let ([name (lambda (x) (f/dom x))]) name)
(cons rhs-bind-id/lw rhs-bind-pat/lw/uq) ... (list (list lhs-for-lw
(cons where-id/lw where-pat/lw) ...) (list side-cond/lw/uq ...)
rhs/lw) (list (cons bind-id/lw bind-pat/lw) ...
...) (cons rhs-bind-id/lw rhs-bind-pat/lw/uq) ...
lang (cons where-id/lw where-pat/lw) ...)
#t ;; multi-args? rhs/lw)
'name ...)
cps lang
rhss #t ;; multi-args?
(let ([name (lambda (x) (name-predicate x))]) name) 'name
dsc cps
sc)) rhss
dsc (let ([name (lambda (x) (name-predicate x))]) name)
`codom-side-conditions-rewritten dsc
'name rg-sc))
#,relation?))) dsc
`codom-side-conditions-rewritten
'name
#,relation?))))
(term-define-fn name name2)) (term-define-fn name name2))
'disappeared-use 'disappeared-use
(map syntax-local-introduce (syntax->list #'(original-names ...)))))))))))))))] (map syntax-local-introduce (syntax->list #'(original-names ...)))))))))))))))]
@ -1317,8 +1404,9 @@
(cdr rhss) (cdr rhss)
(+ num 1))] (+ num 1))]
[relation? [relation?
(let ([ans (ormap (λ (mtch) (rhs traced-metafunc (mtch-bindings mtch))) (let ([ans
mtchs)]) (ormap (λ (mtch) (ormap values (rhs traced-metafunc (mtch-bindings mtch))))
mtchs)])
(unless (match-pattern codom-compiled-pattern ans) (unless (match-pattern codom-compiled-pattern ans)
(redex-error name "codomain test failed for ~s, call was ~s" ans `(,name ,@exp))) (redex-error name "codomain test failed for ~s, call was ~s" ans `(,name ,@exp)))
(cond (cond
@ -1329,19 +1417,34 @@
(loop (cdr patterns) (loop (cdr patterns)
(cdr rhss) (cdr rhss)
(+ num 1))]))] (+ num 1))]))]
[(not (null? (cdr mtchs)))
(redex-error name "~a matched ~s ~a different ways"
(if (< num 0)
"a clause from an extended metafunction"
(format "clause ~a" num))
`(,name ,@exp)
(length mtchs))]
[else [else
(let ([ans (rhs traced-metafunc (mtch-bindings (car mtchs)))]) (let ([anss (apply append
(unless (match-pattern codom-compiled-pattern ans) (filter values
(redex-error name "codomain test failed for ~s, call was ~s" ans `(,name ,@exp))) (map (λ (mtch) (rhs traced-metafunc (mtch-bindings mtch)))
(hash-set! cache exp ans) mtchs)))]
ans)])))]))] [ht (make-hash)])
(for-each (λ (ans) (hash-set! ht ans #t)) anss)
(cond
[(null? anss)
(loop (cdr patterns)
(cdr rhss)
(+ num 1))]
[(not (= 1 (hash-count ht)))
(redex-error name "~a matched ~s ~a different ways and returned different results"
(if (< num 0)
"a clause from an extended metafunction"
(format "clause ~a" num))
`(,name ,@exp)
(length mtchs))]
[else
(let ([ans (car anss)])
(unless (match-pattern codom-compiled-pattern ans)
(redex-error name
"codomain test failed for ~s, call was ~s"
ans
`(,name ,@exp)))
(hash-set! cache exp ans)
ans)]))])))]))]
[else [else
cache-ref])))] cache-ref])))]
[ot (current-trace-print-args)] [ot (current-trace-print-args)]

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

@ -710,7 +710,7 @@
(define-metafunction empty (define-metafunction empty
g : number ... -> (any ...) g : number ... -> (any ...)
[(g number_1 ... 1 number_2 ...) ()]) [(g number_1 ... 1 number_2 ...) (number_1 ...)])
(define-metafunction empty (define-metafunction empty
h : number -> number h : number -> number
@ -796,10 +796,10 @@
(let ([T (reduction-relation (let ([T (reduction-relation
L L
(==> number number (==> number number
(where num number) (where any_num number)
(side-condition (eq? (term num) 4)) (side-condition (eq? (term any_num) 4))
(where numb num) (where any_numb any_num)
(side-condition (eq? (term numb) 4))) (side-condition (eq? (term any_numb) 4)))
with with
[(--> (9 a) b) [(--> (9 a) b)
(==> a b)])]) (==> a b)])])

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

@ -778,7 +778,7 @@
#`(let ([r #,source-stx]) #`(let ([r #,source-stx])
(assert-rel 'redex-check r) (assert-rel 'redex-check r)
(values (values
(map rewrite-proc-lhs (reduction-relation-make-procs r)) (map (λ (x) ((rewrite-proc-lhs x) lang)) (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
@ -935,7 +935,8 @@
(assert-rel 'check-reduction-relation rel) (assert-rel 'check-reduction-relation rel)
(check-prop-srcs (check-prop-srcs
(reduction-relation-lang rel) (reduction-relation-lang rel)
(map rewrite-proc-lhs (reduction-relation-make-procs rel)) (map (λ (x) ((rewrite-proc-lhs x) (reduction-relation-lang rel)))
(reduction-relation-make-procs rel))
(reduction-relation-srcs rel) (reduction-relation-srcs rel)
(λ (term _) (property term)) (λ (term _) (property term))
decisions@ decisions@

5
collects/redex/private/test-util.ss
View File

@ -43,9 +43,10 @@
(define (test/proc run expected line filename) (define (test/proc run expected line filename)
;(printf "testing line ~s:~s\n" filename line) ;(printf "testing line ~s:~s\n" filename line)
(let ([got (run)]) (let ([got (with-handlers ((exn:fail? values)) (run))])
(set! tests (+ tests 1)) (set! tests (+ tests 1))
(unless (matches? got expected) (unless (and (not (exn? got))
(matches? got expected))
(set! failures (+ 1 failures)) (set! failures (+ 1 failures))
(fprintf (current-error-port) (fprintf (current-error-port)
"test/proc: file ~a line ~a:\n got ~s\nexpected ~s\n\n" "test/proc: file ~a line ~a:\n got ~s\nexpected ~s\n\n"

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

@ -303,7 +303,7 @@
;; match one clause two ways => error ;; match one clause two ways => error
(let () (let ()
(define-metafunction empty-language (define-metafunction empty-language
[(ll (number_1 ... number_2 ...)) 4]) [(ll (number_1 ... number_2 ...)) (number_1 ...)])
(test (with-handlers ((exn? (λ (x) 'exn-raised))) (test (with-handlers ((exn? (λ (x) 'exn-raised)))
(term (ll ())) (term (ll ()))
'no-exn) 'no-exn)
@ -477,8 +477,8 @@
(let () (let ()
(define-metafunction empty-language (define-metafunction empty-language
[(f variable) [(f variable)
(x x) (any_x any_x)
(where x (variable variable))]) (where any_x (variable variable))])
(test (term (f z)) (test (term (f z))
(term ((z z) (z z))))) (term ((z z) (z z)))))
@ -504,8 +504,8 @@
(let () (let ()
(define-metafunction empty-language (define-metafunction empty-language
[(err number_1 ... number_2 ...) 1]) [(err number_1 ... number_2 ...) (number_1 ...)])
(test (term (err)) 1) (test (term (err)) (term ()))
(test (with-handlers ((exn:fail:redex? (λ (x) 'right-exn)) (test (with-handlers ((exn:fail:redex? (λ (x) 'right-exn))
((λ (x) #t) (λ (x) 'wrong-exn))) ((λ (x) #t) (λ (x) 'wrong-exn)))
(term (err 1 2)) (term (err 1 2))
@ -611,6 +611,35 @@
(term (f 1))) (term (f 1)))
(test (get-output-string sp) "|(f 1)\n|0\n"))) (test (get-output-string sp) "|(f 1)\n|0\n")))
(let ()
(define-language var-lang [(x y z w) variable])
;; this should produce the second case,
;; since the where clause (should) fail to match
;; in the first case.
(define-metafunction var-lang
[(f x)
first-case
(where (AnotherAtom y) (Atom x))]
[(f x)
second-case])
(test (term (f a)) (term second-case)))
(let ()
;; this is an ambiguous function
;; and should signal an error if it is ever called
;; with multiple different arguments, but if the
;; arguments are all the same, it will return
;; the same result for any parse, and thus should be allowed.
(define-metafunction empty-language
[(f any_x ... any_y any_z ...)
any_y])
(test (term (f 1 1 1 1 1)) (term 1)))
; ;
; ;
@ -1441,8 +1470,8 @@
(test (apply-reduction-relation (test (apply-reduction-relation
(reduction-relation empty-language (reduction-relation empty-language
(--> number_1 (--> number_1
y any_y
(where y ,(+ 1 (term number_1))))) (where any_y ,(+ 1 (term number_1)))))
3) 3)
'(4)) '(4))
@ -1451,24 +1480,35 @@
(apply-reduction-relation (apply-reduction-relation
(reduction-relation empty-language (reduction-relation empty-language
(--> any (--> any
z any_z
(where y ,x) (where any_y ,x)
(where x 2) (where any_x 2)
(where z ,(+ (term y) (term x))))) (where any_z ,(+ (term any_y) (term any_x)))))
'whatever)) 'whatever))
'(7)) '(7))
;; tests `where' clauses bind in side-conditions
(test (let ([x 'unk])
(apply-reduction-relation
(reduction-relation empty-language
(--> any
the-result
(where any_y any)
(side-condition (eq? (term any_y) 'whatever))))
'whatever))
'(the-result))
;; test that where clauses bind in side-conditions that follow ;; test that where clauses bind in side-conditions that follow
(let ([save1 #f] (let ([save1 #f]
[save2 #f]) [save2 #f])
(term-let ([y (term outer-y)]) (term-let ([any_y (term outer-y)])
(test (begin (apply-reduction-relation (test (begin (apply-reduction-relation
(reduction-relation empty-language (reduction-relation empty-language
(--> number_1 (--> number_1
y any_y
(side-condition (set! save1 (term y))) (side-condition (set! save1 (term any_y)))
(where y inner-y) (where any_y inner-y)
(side-condition (set! save2 (term y))))) (side-condition (set! save2 (term any_y)))))
3) 3)
(list save1 save2)) (list save1 save2))
(list 'outer-y 'inner-y)))) (list 'outer-y 'inner-y))))
@ -1476,12 +1516,27 @@
(test (apply-reduction-relation (test (apply-reduction-relation
(reduction-relation empty-language (reduction-relation empty-language
(--> any (--> any
y any_y
(fresh x) (fresh x)
(where y x))) (where any_y x)))
'x) 'x)
'(x1)) '(x1))
(let ()
;; tests where's ability to have redex patterns, not just syntax-case patterns
(define-language var-lang [(x y z w) variable])
(define red
(reduction-relation
var-lang
(--> (x ...)
(y ... z ...)
(where (y ... w z ...) (x ...)))))
(test (apply-reduction-relation red (term (a b c)))
(list (term (a b)) (term (a c)) (term (b c)))))
(let ([r (reduction-relation (let ([r (reduction-relation
grammar grammar
(->1 1 2) (->1 1 2)
@ -1504,7 +1559,7 @@
(->4 a b)])]) (->4 a b)])])
; test that names are properly bound for side-conditions in shortcuts ; test that names are properly bound for side-conditions in shortcuts
(let* ([lhs (rewrite-proc-lhs (first (reduction-relation-make-procs r)))] (let* ([lhs ((rewrite-proc-lhs (first (reduction-relation-make-procs r))) grammar)]
[proc (third lhs)] [proc (third lhs)]
[name (cadadr lhs)] [name (cadadr lhs)]
[bind (λ (n) (make-bindings (list (make-bind name n))))]) [bind (λ (n) (make-bindings (list (make-bind name n))))])
@ -1523,7 +1578,7 @@
[else #f])) [else #f]))
; test shortcut in terms of shortcut ; test shortcut in terms of shortcut
(test (match (rewrite-proc-lhs (third (reduction-relation-make-procs r))) (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]) [else #f])
#t)) #t))

4
collects/redex/private/traces.ss
View File

@ -33,8 +33,10 @@
(define (term-node-labels term-node) (send (term-node-snip term-node) get-one-step-labels)) (define (term-node-labels term-node) (send (term-node-snip term-node) get-one-step-labels))
(define (term-node-set-color! term-node r?) (define (term-node-set-color! term-node r?)
(snip/eventspace (snip/eventspace
term-node
(λ () (λ ()
(send (term-node-snip term-node) set-bad r?)))) (send (term-node-snip term-node) set-bad r?))))
(define (term-node-color term-node) (send (term-node-snip term-node) get-bad))
(define (term-node-set-red! term-node r?) (define (term-node-set-red! term-node r?)
(term-node-set-color! term-node (and r? "pink"))) (term-node-set-color! term-node (and r? "pink")))
@ -692,6 +694,7 @@
[hb (box 0)]) [hb (box 0)])
(send admin get-view-size wb hb) (send admin get-view-size wb hb)
(send admin needs-update this 0 0 (unbox wb) (unbox hb)))))) (send admin needs-update this 0 0 (unbox wb) (unbox hb))))))
(define/public (get-bad) bad-color)
(define names-to-here '()) (define names-to-here '())
;; might have the same parent twice with a different name ;; might have the same parent twice with a different name
@ -886,6 +889,7 @@
term-node-labels term-node-labels
term-node-set-red! term-node-set-red!
term-node-set-color! term-node-set-color!
term-node-color
term-node-set-position! term-node-set-position!
term-node-x term-node-x
term-node-y term-node-y

11
collects/redex/redex.scrbl
View File

@ -903,8 +903,9 @@ expression, and the pattern variables in the @|ttpattern| are
bound in that expression. bound in that expression.
Raises an exception recognized by @scheme[exn:fail:redex?] if Raises an exception recognized by @scheme[exn:fail:redex?] if
no clauses match, if one of the clauses matches multiple ways, or no clauses match, if one of the clauses matches multiple ways
if the contract is violated. (and that leads to different results for the different matches),
or if the contract is violated.
Note that metafunctions are assumed to always return the same results Note that metafunctions are assumed to always return the same results
for the same inputs, and their results are cached, unless for the same inputs, and their results are cached, unless
@ -1450,6 +1451,12 @@ string. The @scheme[color-database<%>] is used to convert the string
to a @scheme[color%] object. to a @scheme[color%] object.
} }
@defproc[(term-node-color [tn term-node?]) (or/c string? (is-a?/c color%) false/c)]{
Returns the current highlighting of the node. See also @scheme[term-node-set-color!].
}
@defproc[(term-node-set-red! [tn term-node?] [red? boolean?]) void?]{ @defproc[(term-node-set-red! [tn term-node?] [red? boolean?]) void?]{
Changes the highlighting of the node; if its second argument Changes the highlighting of the node; if its second argument