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

Fixes PR 11336.

Browse Source
This commit is contained in:
Casey Klein 2010-10-20 11:30:48 -07:00
parent 42687d26d1
commit 4577de0790
4 changed files with 143 additions and 33 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

45
collects/redex/private/reduction-semantics.rkt
View File

@ -1100,7 +1100,7 @@
(define-struct metafunction (proc))
(define-struct metafunc-case (cp rhs lhs-pat src-loc id))
(define-struct metafunc-case (lhs rhs lhs+ src-loc id))
;; Intermediate structures recording clause "extras" for typesetting.
(define-struct metafunc-extra-side-cond (expr))
@ -1213,7 +1213,7 @@
(when (and prev-metafunction (eq? (syntax-e #'name) (syntax-e prev-metafunction)))
(raise-syntax-error syn-error-name "the extended and extending metafunctions cannot share a name" orig-stx prev-metafunction))
(parse-extras #'((stuff ...) ...))
(let*-values ([(lhs-namess lhs-namess/ellipsess)
(let-values ([(lhs-namess lhs-namess/ellipsess)
(let loop ([lhss (syntax->list (syntax (lhs ...)))])
(if (null? lhss)
(values null null)
@ -1227,7 +1227,7 @@
(map (λ (sc/b rhs names names/ellipses)
(bind-withs
syn-error-name '()
#'lang lang-nts
#'effective-lang lang-nts
sc/b 'flatten
#`(list (term #,rhs))
names names/ellipses))
@ -1238,7 +1238,7 @@
(map (λ (sc/b rhs names names/ellipses)
(bind-withs
syn-error-name '()
#'lang lang-nts
#'effective-lang lang-nts
sc/b 'predicate
#`#t
names names/ellipses))
@ -1304,10 +1304,12 @@
[dsc `dom-side-conditions-rewritten])
(let ([cases (map (λ (pat rhs-fn rg-lhs src)
(make-metafunc-case
(compile-pattern lang pat #t) rhs-fn rg-lhs src (gensym)))
(λ (effective-lang) (compile-pattern effective-lang pat #t))
rhs-fn
rg-lhs src (gensym)))
sc
(list rhs-fns ...)
`(rg-side-conditions-rewritten ...)
(list (λ (effective-lang) rhs-fns) ...)
(list (λ (effective-lang) `rg-side-conditions-rewritten) ...)
`(clause-src ...))]
[parent-cases
#,(if prev-metafunction
@ -1522,8 +1524,12 @@
(syntax->list extras))))
(define (build-metafunction lang cases parent-cases wrap dom-contract-pat codom-contract-pat name relation?)
(let ([dom-compiled-pattern (and dom-contract-pat (compile-pattern lang dom-contract-pat #f))]
[codom-compiled-pattern (compile-pattern lang codom-contract-pat #f)])
(let* ([dom-compiled-pattern (and dom-contract-pat (compile-pattern lang dom-contract-pat #f))]
[codom-compiled-pattern (compile-pattern lang codom-contract-pat #f)]
[all-cases (append cases parent-cases)]
[lhss-at-lang (map (λ (case) ((metafunc-case-lhs case) lang)) all-cases)]
[rhss-at-lang (map (λ (case) ((metafunc-case-rhs case) lang)) all-cases)]
[ids (map metafunc-case-id all-cases)])
(values
(wrap
(letrec ([cache (make-hash)]
@ -1556,22 +1562,25 @@
(redex-error name
"~s is not in my domain"
`(,name ,@exp))))
(let loop ([cases (append cases parent-cases)]
(let loop ([ids ids]
[lhss lhss-at-lang]
[rhss rhss-at-lang]
[num (- (length parent-cases))])
(cond
[(null? cases)
[(null? ids)
(if relation?
(begin
(cache-result exp #f #f)
#f)
(redex-error name "no clauses matched for ~s" `(,name . ,exp)))]
[else
(let ([pattern (metafunc-case-cp (car cases))]
[rhs (metafunc-case-rhs (car cases))]
[id (metafunc-case-id (car cases))])
(let ([pattern (car lhss)]
[rhs (car rhss)]
[id (car ids)]
[continue (λ () (loop (cdr ids) (cdr lhss) (cdr rhss) (+ num 1)))])
(let ([mtchs (match-pattern pattern exp)])
(cond
[(not mtchs) (loop (cdr cases) (+ num 1))]
[(not mtchs) (continue)]
[relation?
(let ([ans
(ormap (λ (mtch) (ormap values (rhs traced-metafunc (mtch-bindings mtch))))
@ -1584,7 +1593,7 @@
(log-coverage id)
#t]
[else
(loop (cdr cases) (+ num 1))]))]
(continue)]))]
[else
(let ([anss (apply append
(filter values
@ -1594,7 +1603,7 @@
(for-each (λ (ans) (hash-set! ht ans #t)) anss)
(cond
[(null? anss)
(loop (cdr cases) (+ num 1))]
(continue)]
[(not (= 1 (hash-count ht)))
(redex-error name "~a matched ~s ~a different ways and returned different results"
(if (< num 0)
@ -1627,7 +1636,7 @@
traced-metafunc))
(if dom-compiled-pattern
(λ (exp) (and (match-pattern dom-compiled-pattern exp) #t))
(λ (exp) (and (ormap (λ (case) (match-pattern (metafunc-case-cp case) exp)) cases)
(λ (exp) (and (ormap (λ (lhs) (match-pattern lhs exp)) lhss-at-lang)
#t))))))
(define current-traced-metafunctions (make-parameter '()))

3
collects/redex/private/rg.rkt
View File

@ -850,7 +850,8 @@
(let ([lang-gen (compile lang what)])
(let-values ([(pats srcs)
(cond [(metafunc-proc? mf/rr)
(values (map metafunc-case-lhs-pat (metafunc-proc-cases mf/rr))
(values (map (λ (case) ((metafunc-case-lhs+ case) lang))
(metafunc-proc-cases mf/rr))
(metafunction-srcs mf/rr))]
[(reduction-relation? mf/rr)
(values (map (λ (rwp) ((rewrite-proc-lhs rwp) lang)) (reduction-relation-make-procs mf/rr))

52
collects/redex/tests/rg-test.rkt
View File

@ -800,6 +800,32 @@
generated)
'((4 4) (4 3) (3 4)))
; Extension reinterprets the LHSs of the base relation
; relative to the new language.
(let ()
(define-language L (x 1))
(define-extended-language M L (x 2))
(define R
(reduction-relation L (--> x yes)))
(define S (extend-reduction-relation R M))
(test (let/ec k (check-reduction-relation S k)) 2))
; Extension reinterprets the `where' clauses of the base relation
; relative to new language.
(let ()
(define-language L (x 1))
(define-extended-language M L (x 2))
(define R
(reduction-relation
L
(--> () ()
(where x 2))))
(define S (extend-reduction-relation R M))
(test (with-handlers ([exn:fail:redex:generation-failure? (const #f)])
(check-reduction-relation S (λ (_) #t) #:attempts 1 #:print? #f))
#t))
(let ([generated '()]
[fixed '()]
[fix add1])
@ -1000,6 +1026,32 @@
(check-metafunction f void #:prepare car #:print? #f)))
#rx"rg-test broke the contract")
; Extension reinterprets the LHSs of the base metafunction
; relative to the new language.
(let ()
(define-language L (x 1))
(define-extended-language M L (x 2))
(define-metafunction L
[(f x) yes])
(define-metafunction/extension f M
g : any -> any)
(test (let/ec k (check-metafunction g k)) '(2)))
; Extension reinterprets the `where' clauses of the base metafunction
; relative to the new language.
(let ()
(define-language L (x 1))
(define-extended-language M L (x 2))
(define-metafunction L
[(f)
_
(where x 2)])
(define-metafunction/extension f M
g : any -> any)
(test (with-handlers ([exn:fail:redex:generation-failure? (const #f)])
(check-metafunction g (λ (_) #t) #:attempts 1 #:print? #f))
#t))
(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+")

58
collects/redex/tests/tl-test.rkt
View File

@ -375,6 +375,14 @@
(test (with-handlers ((exn? (λ (x) 'exn-raised))) (term (f mis-match)) 'no-exn)
'exn-raised)
;; test redex-match in RHS and side-condition
(let ()
(define-metafunction empty-language
[(f)
,(and (redex-match empty-language number 7) #t)
(side-condition (redex-match empty-language number 7))])
(test (term (f)) #t))
(define-metafunction grammar
[(h (M_1 M_2)) ((h M_2) (h M_1))]
[(h number_1) ,(+ (term number_1) 1)])
@ -420,6 +428,37 @@
(in-domain? (f y)))
#f))
; Extension reinterprets the base meta-function's contract
; according to the new language.
(let ()
(define-language L (x 1))
(define-extended-language M L (x 2))
(define-metafunction L
f : x -> x
[(f x) x])
(define-metafunction/extension f M
[(g q) q])
(with-handlers ([(λ (x)
(and (exn:fail? x)
(regexp-match? #rx"no clauses matched"
(exn-message x))))
(λ (_) #f)])
(test (begin (term (g 2)) #t) #t))
(test (in-domain? (g 2)) #t))
; in-domain? interprets base meta-function LHSs according to
; the new language.
(let ()
(define-language L (x 1))
(define-extended-language M L (x 2))
(define-metafunction L
[(f x) x])
(define-metafunction/extension f M
[(g q) q])
(test (in-domain? (g 2)) #t))
;; mutually recursive metafunctions
(define-metafunction grammar
[(odd zero) #f]
@ -531,8 +570,6 @@
(test (term (g 11 17)) 11)
(test (term (h 11 17)) 11))
; We'd like this expression not to raise an error.
#;
(let ()
(define-language L
(v 1))
@ -552,8 +589,6 @@
[(g any) 2])
(test (term (g 0)) 2))
; We'd like this expression not to raise an error.
#;
(let ()
(define-language L
(v 1 (v)))
@ -570,7 +605,20 @@
g : v -> v
[(g 2) 2])
(term (g (2))))
(test (term (g (2))) 2))
(let ()
(define-language L (x 1))
(define-extended-language M L (x 2))
(define-metafunction L
[(f)
yes
(where x 2)]
[(f)
no])
(define-metafunction/extension f M
g : -> any)
(test (term (g)) 'yes))
(let ()
(define-metafunction empty-language