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

accidentally committed some changes on the branch, now moving back to trunk (w/ some conflicts, argh!): fixed a bug in the way redex expanded metafunctions (it had old code left in there) and improved error messages for domain failures in reduction relations

Browse Source 
svn: r15317
This commit is contained in:
Robby Findler 2009-06-27 13:47:02 +00:00
parent 440ab66ae7
commit ea6c99c69f
6 changed files with 258 additions and 217 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
collects/redex/private/bitmap-test.ss
View File

@ -36,6 +36,20 @@
(extend-reduction-relation red lang (--> 1 2))) (extend-reduction-relation red lang (--> 1 2)))
"extended-reduction-relation.png") "extended-reduction-relation.png")
;; this test should fail because it gets the order wrong
;; for the where/side-conditions
(define red2
(reduction-relation
lang
(--> (number_a number_b number_c)
any_z
(where (any_x any_y) (number_a number_b))
(side-condition (= (term number_c) 5))
(where any_z any_x))))
(test (render-reduction-relation red2)
"red2.png")
(define-metafunction lang (define-metafunction lang
[(S x v e) e]) [(S x v e) e])
@ -92,7 +106,6 @@
(render-metafunction Name)) (render-metafunction Name))
"metafunction-Name-vertical.png") "metafunction-Name-vertical.png")
;; makes sure that there is no overlap inside or across metafunction calls ;; makes sure that there is no overlap inside or across metafunction calls
;; or when there are unquotes involved ;; or when there are unquotes involved
(define-metafunction lang (define-metafunction lang

BIN
collects/redex/private/bmps/metafunction-Name-vertical.png
View File

Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 4.7 KiB

After

Width:  |  Height:  |  Size: 4.7 KiB

36
collects/redex/private/pict.ss
View File

@ -251,7 +251,10 @@
ltl-superimpose ltl-superimpose ltl-superimpose ltl-superimpose
(list* 2 (+ 2 (current-label-extra-space))) 2))) (list* 2 (+ 2 (current-label-extra-space))) 2)))
(define (side-condition-pict fresh-vars side-conditions pattern-binds max-w) ;; side-condition-pict : (listof pict) (listof (or/c (cons/c pict pict) pict)) number -> pict
;; the elements of pattern-binds/sc that are pairs are bindings (ie "x = <something>")
;; and the elements of pattern-binds/sc that are just picts are just plain side-conditions
(define (side-condition-pict fresh-vars pattern-binds/sc max-w)
(let* ([frsh (let* ([frsh
(if (null? fresh-vars) (if (null? fresh-vars)
null null
@ -264,16 +267,17 @@
fresh-vars)) fresh-vars))
(basic-text " fresh" (default-style)))))] (basic-text " fresh" (default-style)))))]
[binds (map (lambda (b) [binds (map (lambda (b)
(htl-append (if (pair? b)
(car b) (htl-append
(make-=) (car b)
(cdr b))) (make-=)
pattern-binds)] (cdr b))
b))
pattern-binds/sc)]
[lst (add-between [lst (add-between
'comma 'comma
(append (append
binds binds
side-conditions
frsh))]) frsh))])
(if (null? lst) (if (null? lst)
(blank) (blank)
@ -293,8 +297,8 @@
(define (rp->side-condition-pict rp max-w) (define (rp->side-condition-pict rp max-w)
(side-condition-pict (rule-pict-fresh-vars rp) (side-condition-pict (rule-pict-fresh-vars rp)
(rule-pict-side-conditions rp) (append (rule-pict-side-conditions rp)
(rule-pict-pattern-binds rp) (rule-pict-pattern-binds rp))
max-w)) max-w))
(define (rp->pict-label rp) (define (rp->pict-label rp)
@ -737,21 +741,21 @@
[eqns (select-cases all-eqns)] [eqns (select-cases all-eqns)]
[lhss (select-cases all-lhss)] [lhss (select-cases all-lhss)]
[scs (map (lambda (eqn) [scs (map (lambda (eqn)
(if (and (null? (list-ref eqn 1)) (if (null? (list-ref eqn 1))
(null? (list-ref eqn 2)))
#f #f
(side-condition-pict null (side-condition-pict null
(map wrapper->pict (list-ref eqn 1))
(map (lambda (p) (map (lambda (p)
(cons (wrapper->pict (car p)) (if (pair? p)
(wrapper->pict (cdr p)))) (cons (wrapper->pict (car p))
(list-ref eqn 2)) (wrapper->pict (cdr p)))
(wrapper->pict p)))
(list-ref eqn 1))
(if (memq style '(up-down/vertical-side-conditions (if (memq style '(up-down/vertical-side-conditions
left-right/vertical-side-conditions)) left-right/vertical-side-conditions))
0 0
+inf.0)))) +inf.0))))
eqns)] eqns)]
[rhss (map (lambda (eqn) (wrapper->pict (list-ref eqn 3))) eqns)] [rhss (map (lambda (eqn) (wrapper->pict (list-ref eqn 2))) eqns)]
[linebreak-list (or current-linebreaks [linebreak-list (or current-linebreaks
(map (lambda (x) #f) eqns))] (map (lambda (x) #f) eqns))]
[=-pict (make-=)] [=-pict (make-=)]

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

@ -1074,177 +1074,180 @@
(raise-syntax-error syn-error-name "no clauses" orig-stx)) (raise-syntax-error syn-error-name "no clauses" orig-stx))
(prune-syntax (prune-syntax
(let ([lang-nts (language-id-nts #'lang 'define-metafunction)]) ;; keep this near the beginning, so it signals the first error (PR 10062) (let ([lang-nts (language-id-nts #'lang 'define-metafunction)]) ;; keep this near the beginning, so it signals the first error (PR 10062)
(let-values ([(contract-name dom-ctcs codom-contract pats) (let-values ([(contract-name dom-ctcs codom-contract pats)
(split-out-contract orig-stx syn-error-name #'rest relation?)]) (split-out-contract orig-stx syn-error-name #'rest relation?)])
(with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats] (with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats]
[(lhs-for-lw ...) [(lhs-for-lw ...)
(with-syntax ([((lhs-for-lw _ ...) ...) pats]) (with-syntax ([((lhs-for-lw _ ...) ...) pats])
(map (λ (x) (to-lw/proc (datum->syntax #f (cdr (syntax-e x)) x))) (map (λ (x) (to-lw/proc (datum->syntax #f (cdr (syntax-e x)) x)))
(syntax->list #'(lhs-for-lw ...))))]) (syntax->list #'(lhs-for-lw ...))))])
(with-syntax ([((rhs stuff ...) ...) (if relation? (with-syntax ([((rhs stuff ...) ...) (if relation?
#'((,(and (term raw-rhses) ...)) ...) #'((,(and (term raw-rhses) ...)) ...)
#'((raw-rhses ...) ...))]) #'((raw-rhses ...) ...))])
(parameterize ([is-term-fn? (parameterize ([is-term-fn?
(let ([names (syntax->list #'(original-names ...))]) (let ([names (syntax->list #'(original-names ...))])
(λ (x) (and (not (null? names)) (λ (x) (and (not (null? names))
(identifier? (car names)) (identifier? (car names))
(free-identifier=? x (car names)))))]) (free-identifier=? x (car names)))))])
(with-syntax ([(rhs/lw ...) (map to-lw/proc (syntax->list #'(rhs ...)))] (with-syntax ([(rhs/lw ...) (map to-lw/proc (syntax->list #'(rhs ...)))]
[(lhs ...) #'((lhs-clauses ...) ...)] [(lhs ...) #'((lhs-clauses ...) ...)]
[name (let loop ([name (if contract-name [name (let loop ([name (if contract-name
contract-name contract-name
(car (syntax->list #'(original-names ...))))] (car (syntax->list #'(original-names ...))))]
[names (if contract-name [names (if contract-name
(syntax->list #'(original-names ...)) (syntax->list #'(original-names ...))
(cdr (syntax->list #'(original-names ...))))]) (cdr (syntax->list #'(original-names ...))))])
(cond (cond
[(null? names) name] [(null? names) name]
[else [else
(unless (eq? (syntax-e name) (syntax-e (car names))) (unless (eq? (syntax-e name) (syntax-e (car names)))
(raise (raise
(make-exn:fail:syntax (make-exn:fail:syntax
(if contract-name (if contract-name
"define-metafunction: expected each clause and the contract to use the same name" "define-metafunction: expected each clause and the contract to use the same name"
"define-metafunction: expected each clause to use the same name") "define-metafunction: expected each clause to use the same name")
(current-continuation-marks) (current-continuation-marks)
(list name (list name
(car names))))) (car names)))))
(loop name (cdr names))]))]) (loop name (cdr names))]))])
(with-syntax ([(((tl-side-conds ...) ...) (with-syntax ([(((tl-side-conds ...) ...)
(tl-bindings ...) (tl-bindings ...)
(tl-side-cond/binds ...)) (tl-side-cond/binds ...))
(parse-extras #'((stuff ...) ...))]) (parse-extras #'((stuff ...) ...))])
(with-syntax ([(((cp-let-bindings ...) rhs/wheres) ...) (with-syntax ([(((cp-let-bindings ...) rhs/wheres) ...)
(map (λ (sc/b rhs) (map (λ (sc/b rhs)
(let-values ([(body-code cp-let-bindings) (let-values ([(body-code cp-let-bindings)
(bind-withs (bind-withs
syn-error-name '() syn-error-name '()
#'lang lang-nts #'lang lang-nts
sc/b 'flatten sc/b 'flatten
#`(list (term #,rhs)))]) #`(list (term #,rhs)))])
(list cp-let-bindings body-code))) (list cp-let-bindings body-code)))
(syntax->list #'(tl-side-cond/binds ...)) (syntax->list #'(tl-side-cond/binds ...))
(syntax->list #'(rhs ...)))] (syntax->list #'(rhs ...)))]
[(((rg-cp-let-bindings ...) rg-rhs/wheres) ...) [(((rg-cp-let-bindings ...) rg-rhs/wheres) ...)
(map (λ (sc/b rhs) (map (λ (sc/b rhs)
(let-values ([(body-code cp-let-bindings) (let-values ([(body-code cp-let-bindings)
(bind-withs (bind-withs
syn-error-name '() syn-error-name '()
#'lang lang-nts #'lang lang-nts
sc/b 'predicate sc/b 'predicate
#`#t)]) #`#t)])
(list cp-let-bindings body-code))) (list cp-let-bindings body-code)))
(syntax->list #'(tl-side-cond/binds ...)) (syntax->list #'(tl-side-cond/binds ...))
(syntax->list #'(rhs ...)))])
(with-syntax ([(side-conditions-rewritten ...)
(map (λ (x) (rewrite-side-conditions/check-errs
lang-nts
syn-error-name
#t
x))
(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
(and dom-ctcs
(rewrite-side-conditions/check-errs
lang-nts
syn-error-name
#f
dom-ctcs))]
[codom-side-conditions-rewritten
(rewrite-side-conditions/check-errs
lang-nts
syn-error-name
#f
codom-contract)]
[(rhs-fns ...)
(map (λ (lhs rhs/where)
(let-values ([(names names/ellipses)
(extract-names lang-nts syn-error-name #t lhs)])
(with-syntax ([(names ...) names]
[(names/ellipses ...) names/ellipses]
[rhs/where rhs/where])
(syntax
(λ (name bindings)
(term-let-fn ((name name))
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
rhs/where)))))))
(syntax->list (syntax (lhs ...)))
(syntax->list (syntax (rhs/wheres ...))))]
[(name2 name-predicate) (generate-temporaries (syntax (name name)))]
[(((bind-id/lw . bind-pat/lw) ...) ...)
;; Also for pict, extract pattern bindings
(map (λ (x) (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/proc (cdr x))))
(extract-pattern-binds x)))
(syntax->list #'(lhs ...)))]
[((where/sc/lw ...) ...)
;; Also for pict, extract where bindings
(map (λ (hm)
(map
(λ (lst)
(syntax-case lst (side-condition where)
[(where pat exp)
#`(cons #,(to-lw/proc #'pat) #,(to-lw/proc #'exp))]
[(side-condition x)
(to-lw/uq/proc #'x)]))
(syntax->list hm)))
(syntax->list #'(tl-side-cond/binds ...)))]
[(((rhs-bind-id/lw . rhs-bind-pat/lw/uq) ...) ...)
;; Also for pict, extract pattern bindings
(map (λ (x) (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/uq/proc (cdr x))))
(extract-term-let-binds x)))
(syntax->list #'(rhs ...)))]) (syntax->list #'(rhs ...)))])
(with-syntax ([(side-conditions-rewritten ...) (syntax-property
(map (λ (x) (rewrite-side-conditions/check-errs #`(begin
lang-nts (define-values (name2 name-predicate)
syn-error-name (let ([sc `(side-conditions-rewritten ...)]
#t [dsc `dom-side-conditions-rewritten]
x)) cp-let-bindings ... ...
(syntax->list (syntax (lhs ...))))] rg-cp-let-bindings ... ...)
[(rg-side-conditions-rewritten ...) (let ([rg-sc `(rg-side-conditions-rewritten ...)])
(map (λ (x) (rewrite-side-conditions/check-errs (build-metafunction
lang-nts lang
syn-error-name sc
#t (list rhs-fns ...)
x)) #,(if prev-metafunction
(syntax->list (syntax ((side-condition lhs rg-rhs/wheres) ...))))] (let ([term-fn (syntax-local-value prev-metafunction)])
[dom-side-conditions-rewritten #`(metafunc-proc-cps #,(term-fn-get-id term-fn)))
(and dom-ctcs #''())
(rewrite-side-conditions/check-errs #,(if prev-metafunction
lang-nts (let ([term-fn (syntax-local-value prev-metafunction)])
syn-error-name #`(metafunc-proc-rhss #,(term-fn-get-id term-fn)))
#f #''())
dom-ctcs))] (λ (f/dom cps rhss)
[codom-side-conditions-rewritten (make-metafunc-proc
(rewrite-side-conditions/check-errs (let ([name (lambda (x) (f/dom x))]) name)
lang-nts (list (list lhs-for-lw
syn-error-name (list (cons bind-id/lw bind-pat/lw) ...
#f (cons rhs-bind-id/lw rhs-bind-pat/lw/uq) ...
codom-contract)] where/sc/lw ...)
[(rhs-fns ...) rhs/lw)
(map (λ (lhs rhs/where bindings) ...)
(let-values ([(names names/ellipses) lang
(extract-names lang-nts syn-error-name #t lhs)]) #t ;; multi-args?
(with-syntax ([(names ...) names] 'name
[(names/ellipses ...) names/ellipses] cps
[rhs/where rhs/where] rhss
[((tl-var tl-exp) ...) bindings]) (let ([name (lambda (x) (name-predicate x))]) name)
(syntax dsc
(λ (name bindings) rg-sc))
(term-let-fn ((name name)) dsc
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...) `codom-side-conditions-rewritten
(term-let ([tl-var (term tl-exp)] ...) 'name
rhs/where)))))))) #,relation?))))
(syntax->list (syntax (lhs ...))) (term-define-fn name name2))
(syntax->list (syntax (rhs/wheres ...))) 'disappeared-use
(syntax->list (syntax (tl-bindings ...))))] (map syntax-local-introduce (syntax->list #'(original-names ...)))))))))))))))]
[(name2 name-predicate) (generate-temporaries (syntax (name name)))]
[((side-cond/lw/uq ...) ...)
(map (lambda (scs) (map to-lw/uq/proc (syntax->list scs)))
(syntax->list #'((tl-side-conds ...) ...)))]
[(((bind-id/lw . bind-pat/lw) ...) ...)
;; Also for pict, extract pattern bindings
(map (λ (x) (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/proc (cdr x))))
(extract-pattern-binds x)))
(syntax->list #'(lhs ...)))]
[(((rhs-bind-id/lw . rhs-bind-pat/lw/uq) ...) ...)
;; Also for pict, extract pattern bindings
(map (λ (x) (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/uq/proc (cdr x))))
(extract-term-let-binds x)))
(syntax->list #'(rhs ...)))]
[(((where-id/lw where-pat/lw) ...) ...)
;; Also for pict, extract where bindings
(map (λ (lst) (map (λ (ab) (map to-lw/proc (syntax->list ab)))
(syntax->list lst)))
(syntax->list #'(tl-bindings ...)))])
(syntax-property
#`(begin
(define-values (name2 name-predicate)
(let ([sc `(side-conditions-rewritten ...)]
[dsc `dom-side-conditions-rewritten]
cp-let-bindings ... ...
rg-cp-let-bindings ... ...)
(let ([rg-sc `(rg-side-conditions-rewritten ...)])
(build-metafunction
lang
sc
(list rhs-fns ...)
#,(if prev-metafunction
(let ([term-fn (syntax-local-value prev-metafunction)])
#`(metafunc-proc-cps #,(term-fn-get-id term-fn)))
#''())
#,(if prev-metafunction
(let ([term-fn (syntax-local-value prev-metafunction)])
#`(metafunc-proc-rhss #,(term-fn-get-id term-fn)))
#''())
(λ (f/dom cps rhss)
(make-metafunc-proc
(let ([name (lambda (x) (f/dom x))]) name)
(list (list lhs-for-lw
(list side-cond/lw/uq ...)
(list (cons bind-id/lw bind-pat/lw) ...
(cons rhs-bind-id/lw rhs-bind-pat/lw/uq) ...
(cons where-id/lw where-pat/lw) ...)
rhs/lw)
...)
lang
#t ;; multi-args?
'name
cps
rhss
(let ([name (lambda (x) (name-predicate x))]) name)
dsc
rg-sc))
dsc
`codom-side-conditions-rewritten
'name
#,relation?))))
(term-define-fn name name2))
'disappeared-use
(map syntax-local-introduce (syntax->list #'(original-names ...)))))))))))))))]
[(_ prev-metafunction name lang clauses ...) [(_ prev-metafunction name lang clauses ...)
(begin (begin
(unless (identifier? #'name) (unless (identifier? #'name)
@ -1430,7 +1433,7 @@
(redex-error name "~a matched ~s ~a different ways and returned different results" (redex-error name "~a matched ~s ~a different ways and returned different results"
(if (< num 0) (if (< num 0)
"a clause from an extended metafunction" "a clause from an extended metafunction"
(format "clause ~a" num)) (format "clause #~a (counting from 0)" num))
`(,name ,@exp) `(,name ,@exp)
(length mtchs))] (length mtchs))]
[else [else

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

@ -50,27 +50,37 @@
;; I started to add it, but didn't finish. -robby ;; I started to add it, but didn't finish. -robby
(define (build-reduction-relation orig-reduction-relation lang make-procs rule-names lws domain-pattern) (define (build-reduction-relation orig-reduction-relation lang make-procs rule-names lws domain-pattern)
(let* ([make-procs/check-domain (let* ([make-procs/check-domain
(map (λ (make-proc) (let loop ([make-procs make-procs]
(make-rewrite-proc [i 0])
(λ (lang) (cond
(let ([compiled-domain-pat (compile-pattern lang domain-pattern #f)] [(null? make-procs) null]
[proc (make-proc lang)]) [else
(λ (tl-exp exp f acc) (let ([make-proc (car make-procs)])
(unless (match-pattern compiled-domain-pat tl-exp) (cons (make-rewrite-proc
(error 'reduction-relation "relation not defined for ~s" tl-exp)) (λ (lang)
(let ([ress (proc tl-exp exp f acc)]) (let ([compiled-domain-pat (compile-pattern lang domain-pattern #f)]
(for-each [proc (make-proc lang)])
(λ (res) (λ (tl-exp exp f acc)
(let ([term (cadr res)]) (unless (match-pattern compiled-domain-pat tl-exp)
(unless (match-pattern compiled-domain-pat term) (error 'reduction-relation "relation not defined for ~s" tl-exp))
(error 'reduction-relation "relation reduced to ~s, which is outside its domain" (let ([ress (proc tl-exp exp f acc)])
term)))) (for-each
ress) (λ (res)
ress)))) (let ([term (cadr res)])
(rewrite-proc-name make-proc) (unless (match-pattern compiled-domain-pat term)
(rewrite-proc-lhs make-proc) (error 'reduction-relation "relation reduced to ~s via ~a, which is outside its domain"
(rewrite-proc-id make-proc))) term
make-procs)]) (let ([name (rewrite-proc-name make-proc)])
(if name
(format "the rule named ~a" name)
(format "rule #~a (counting from 0)" i)))))))
ress)
ress))))
(rewrite-proc-name make-proc)
(rewrite-proc-lhs make-proc)
(rewrite-proc-id make-proc))
(loop (cdr make-procs)
(+ i 1))))]))])
(cond (cond
[orig-reduction-relation [orig-reduction-relation
(let* ([new-names (map rewrite-proc-name make-procs)] (let* ([new-names (map rewrite-proc-name make-procs)]

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

@ -639,14 +639,25 @@
(test (term (f 1 1 1 1 1)) (term 1))) (test (term (f 1 1 1 1 1)) (term 1)))
(let () (let ()
(define-metafunction empty-language (define-metafunction empty-language
[(ex variable_x) [(ex variable_x)
variable_x variable_x
(where quote variable_x)]) (where quote variable_x)])
(test (term (ex quote)) (term quote))) (test (term (ex quote)) (term quote)))
(let ()
(define-metafunction empty-language
[(f any ...)
(any ...)
(where variable_1 x)
(side-condition #f)
(where (number ...) y)]
[(f any ...)
12345])
(test (term (f 8)) 12345))
; ;
@ -924,7 +935,7 @@
(with-handlers ((exn? exn-message)) (with-handlers ((exn? exn-message))
(apply-reduction-relation red 1) (apply-reduction-relation red 1)
'no-exception-raised)) 'no-exception-raised))
"reduction-relation: relation reduced to x, which is outside its domain") "reduction-relation: relation reduced to x via rule #0 (counting from 0), which is outside its domain")
(let* ([red1 (let* ([red1
(reduction-relation (reduction-relation