From 4577de0790296f1b0c64d51fffc52ee84f60c602 Mon Sep 17 00:00:00 2001 From: Casey Klein Date: Wed, 20 Oct 2010 11:30:48 -0700 Subject: [PATCH] Fixes PR 11336. --- .../redex/private/reduction-semantics.rkt | 63 +++++++++++-------- collects/redex/private/rg.rkt | 3 +- collects/redex/tests/rg-test.rkt | 52 +++++++++++++++ collects/redex/tests/tl-test.rkt | 58 +++++++++++++++-- 4 files changed, 143 insertions(+), 33 deletions(-) diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt index 579698fe5c..e806198c40 100644 --- a/collects/redex/private/reduction-semantics.rkt +++ b/collects/redex/private/reduction-semantics.rkt @@ -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,21 +1213,21 @@ (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 loop ([lhss (syntax->list (syntax (lhs ...)))]) - (if (null? lhss) - (values null null) - (let-values ([(namess namess/ellipsess) - (loop (cdr lhss))] - [(names names/ellipses) - (extract-names lang-nts syn-error-name #t (car lhss))]) - (values (cons names namess) - (cons names/ellipses namess/ellipsess)))))]) + (let-values ([(lhs-namess lhs-namess/ellipsess) + (let loop ([lhss (syntax->list (syntax (lhs ...)))]) + (if (null? lhss) + (values null null) + (let-values ([(namess namess/ellipsess) + (loop (cdr lhss))] + [(names names/ellipses) + (extract-names lang-nts syn-error-name #t (car lhss))]) + (values (cons names namess) + (cons names/ellipses namess/ellipsess)))))]) (with-syntax ([(rhs/wheres ...) (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 '())) diff --git a/collects/redex/private/rg.rkt b/collects/redex/private/rg.rkt index e65d0eb2a4..9106e763e2 100644 --- a/collects/redex/private/rg.rkt +++ b/collects/redex/private/rg.rkt @@ -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)) diff --git a/collects/redex/tests/rg-test.rkt b/collects/redex/tests/rg-test.rkt index 578eb71730..b31a2698de 100644 --- a/collects/redex/tests/rg-test.rkt +++ b/collects/redex/tests/rg-test.rkt @@ -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+") diff --git a/collects/redex/tests/tl-test.rkt b/collects/redex/tests/tl-test.rkt index 29033b51d3..76ce4b7b6c 100644 --- a/collects/redex/tests/tl-test.rkt +++ b/collects/redex/tests/tl-test.rkt @@ -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