diff --git a/collects/redex/private/fresh.ss b/collects/redex/private/fresh.ss new file mode 100644 index 0000000000..a4c31fd005 --- /dev/null +++ b/collects/redex/private/fresh.ss @@ -0,0 +1,59 @@ +#lang scheme + +(define re:gen-d #rx".*[^0-9]([0-9]+)$") +(define (variable-not-in sexp var) + (let* ([var-str (symbol->string var)] + [var-prefix (let ([m (regexp-match #rx"^(.*[^0-9])[0-9]+$" var-str)]) + (if m + (cadr m) + var-str))] + [found-exact-var? #f] + [nums (let loop ([sexp sexp] + [nums null]) + (cond + [(pair? sexp) (loop (cdr sexp) (loop (car sexp) nums))] + [(symbol? sexp) + (when (eq? sexp var) + (set! found-exact-var? #t)) + (let* ([str (symbol->string sexp)] + [match (regexp-match re:gen-d str)]) + (if (and match + (is-prefix? var-prefix str)) + (cons (string->number (cadr match)) nums) + nums))] + [else nums]))]) + (cond + [(not found-exact-var?) var] + [(null? nums) (string->symbol (format "~a1" var))] + [else (string->symbol (format "~a~a" var-prefix (find-best-number nums)))]))) + +(define (find-best-number nums) + (let loop ([sorted (sort nums <)] + [i 1]) + (cond + [(empty? sorted) i] + [else + (let ([fst (car sorted)]) + (cond + [(< i fst) i] + [(> i fst) (loop (cdr sorted) i)] + [(= i fst) (loop (cdr sorted) (+ i 1))]))]))) + +(define (variables-not-in sexp vars) + (let loop ([vars vars] + [sexp sexp]) + (cond + [(null? vars) null] + [else + (let ([new-var (variable-not-in sexp (car vars))]) + (cons new-var + (loop (cdr vars) + (cons new-var sexp))))]))) + +(define (is-prefix? str1 str2) + (and (<= (string-length str1) (string-length str2)) + (equal? str1 (substring str2 0 (string-length str1))))) + +(provide/contract + [variable-not-in (any/c symbol? . -> . symbol?)] + [variables-not-in (any/c (listof symbol?) . -> . (listof symbol?))]) \ No newline at end of file diff --git a/collects/redex/private/pict.ss b/collects/redex/private/pict.ss index 83006b1449..2eeb5a549a 100644 --- a/collects/redex/private/pict.ss +++ b/collects/redex/private/pict.ss @@ -3,7 +3,8 @@ (lib "utils.ss" "texpict") scheme/gui/base scheme/class - (only-in scheme/list drop-right last) + scheme/match + (only-in scheme/list drop-right last partition) "reduction-semantics.ss" "struct.ss" "loc-wrapper.ss" @@ -793,20 +794,24 @@ [scs (map (lambda (eqn) (if (null? (list-ref eqn 1)) #f - (side-condition-pict null - (map (lambda (p) - (if (pair? p) - (cons (wrapper->pict (car p)) - (wrapper->pict (cdr p))) - (wrapper->pict p))) - (list-ref eqn 1)) - (if (memq style '(up-down/vertical-side-conditions - left-right/vertical-side-conditions)) - 0 - (if (memq style '(up-down/compact-side-conditions - left-right/compact-side-conditions)) - max-line-w/pre-sc - +inf.0))))) + (let-values ([(fresh where/sc) (partition metafunc-extra-fresh? (list-ref eqn 1))]) + (side-condition-pict (foldl (λ (clause picts) + (foldr (λ (l ps) (cons (wrapper->pict l) ps)) + picts (metafunc-extra-fresh-vars clause))) + '() fresh) + (map (match-lambda + [(struct metafunc-extra-where (lhs rhs)) + (cons (wrapper->pict lhs) (wrapper->pict rhs))] + [(struct metafunc-extra-side-cond (expr)) + (wrapper->pict expr)]) + where/sc) + (if (memq style '(up-down/vertical-side-conditions + left-right/vertical-side-conditions)) + 0 + (if (memq style '(up-down/compact-side-conditions + left-right/compact-side-conditions)) + max-line-w/pre-sc + +inf.0)))))) eqns)]) (case style [(left-right left-right/vertical-side-conditions left-right/compact-side-conditions left-right/beside-side-conditions) diff --git a/collects/redex/private/reduction-semantics.ss b/collects/redex/private/reduction-semantics.ss index 1316509c9f..c71664ba42 100644 --- a/collects/redex/private/reduction-semantics.ss +++ b/collects/redex/private/reduction-semantics.ss @@ -3,6 +3,7 @@ (require "matcher.ss" "struct.ss" "term.ss" + "fresh.ss" "loc-wrapper.ss" "error.ss" mzlib/trace @@ -1016,6 +1017,11 @@ (define-struct metafunc-case (cp rhs lhs-pat src-loc id)) +;; Intermediate structures recording clause "extras" for typesetting. +(define-struct metafunc-extra-side-cond (expr)) +(define-struct metafunc-extra-where (lhs rhs)) +(define-struct metafunc-extra-fresh (vars)) + (define-syntax (in-domain? stx) (syntax-case stx () [(_ (name exp ...)) @@ -1249,11 +1255,25 @@ (map (λ (hm) (map (λ (lst) - (syntax-case lst (side-condition where) + (syntax-case lst (side-condition where unquote) + [(where pat (unquote (f _ _))) + (and (or (identifier? #'pat) + (andmap identifier? (syntax->list #'pat))) + (or (free-identifier=? #'f #'variable-not-in) + (free-identifier=? #'f #'variables-not-in))) + (with-syntax ([(ids ...) + (map to-lw/proc + (if (identifier? #'pat) + (list #'pat) + (syntax->list #'pat)))]) + #`(make-metafunc-extra-fresh + (list ids ...)))] [(where pat exp) - #`(cons #,(to-lw/proc #'pat) #,(to-lw/proc #'exp))] + #`(make-metafunc-extra-where + #,(to-lw/proc #'pat) #,(to-lw/proc #'exp))] [(side-condition x) - (to-lw/uq/proc #'x)])) + #`(make-metafunc-extra-side-cond + #,(to-lw/uq/proc #'x))])) (reverse (syntax->list hm)))) (syntax->list #'(... seq-of-tl-side-cond/binds)))] @@ -1265,8 +1285,8 @@ [(x-lhs-for-lw ...) #'(... seq-of-lhs-for-lw)]) #'(list (list x-lhs-for-lw - (list (cons bind-id/lw bind-pat/lw) ... - (cons rhs-bind-id/lw rhs-bind-pat/lw/uq) ... + (list (make-metafunc-extra-where bind-id/lw bind-pat/lw) ... + (make-metafunc-extra-where rhs-bind-id/lw rhs-bind-pat/lw/uq) ... where/sc/lw ...) rhs/lw) ...)))]) @@ -1943,61 +1963,6 @@ (cons this-one (loop (cdr l))) (loop (cdr l))))]))) -(define re:gen-d #rx".*[^0-9]([0-9]+)$") -(define (variable-not-in sexp var) - (let* ([var-str (symbol->string var)] - [var-prefix (let ([m (regexp-match #rx"^(.*[^0-9])[0-9]+$" var-str)]) - (if m - (cadr m) - var-str))] - [found-exact-var? #f] - [nums (let loop ([sexp sexp] - [nums null]) - (cond - [(pair? sexp) (loop (cdr sexp) (loop (car sexp) nums))] - [(symbol? sexp) - (when (eq? sexp var) - (set! found-exact-var? #t)) - (let* ([str (symbol->string sexp)] - [match (regexp-match re:gen-d str)]) - (if (and match - (is-prefix? var-prefix str)) - (cons (string->number (cadr match)) nums) - nums))] - [else nums]))]) - (cond - [(not found-exact-var?) var] - [(null? nums) (string->symbol (format "~a1" var))] - [else (string->symbol (format "~a~a" var-prefix (find-best-number nums)))]))) - -(define (find-best-number nums) - (let loop ([sorted (sort nums <)] - [i 1]) - (cond - [(empty? sorted) i] - [else - (let ([fst (car sorted)]) - (cond - [(< i fst) i] - [(> i fst) (loop (cdr sorted) i)] - [(= i fst) (loop (cdr sorted) (+ i 1))]))]))) - -(define (variables-not-in sexp vars) - (let loop ([vars vars] - [sexp sexp]) - (cond - [(null? vars) null] - [else - (let ([new-var (variable-not-in sexp (car vars))]) - (cons new-var - (loop (cdr vars) - (cons new-var sexp))))]))) - -(define (is-prefix? str1 str2) - (and (<= (string-length str1) (string-length str2)) - (equal? str1 (substring str2 0 (string-length str1))))) - - (define (reduction-relation->rule-names x) (reverse (reduction-relation-rule-names x))) @@ -2169,6 +2134,10 @@ metafunc-proc? (struct-out metafunc-case) + (struct-out metafunc-extra-side-cond) + (struct-out metafunc-extra-where) + (struct-out metafunc-extra-fresh) + (struct-out binds)) (provide test-match diff --git a/collects/redex/reduction-semantics.ss b/collects/redex/reduction-semantics.ss index ad0c601b0e..e58415cf84 100644 --- a/collects/redex/reduction-semantics.ss +++ b/collects/redex/reduction-semantics.ss @@ -54,6 +54,9 @@ (struct-out exn:fail:redex:test) (struct-out counterexample)) +(provide variable-not-in + variables-not-in) + (provide/contract [current-traced-metafunctions (parameter/c (or/c 'all (listof symbol?)))] [reduction-relation->rule-names (-> reduction-relation? (listof symbol?))] @@ -71,7 +74,5 @@ [lookup-binding (case-> (-> bindings? symbol? any) (-> bindings? symbol? (-> any) any))] - [variable-not-in (any/c symbol? . -> . symbol?)] - [variables-not-in (any/c (listof symbol?) . -> . (listof symbol?))] [relation-coverage (parameter/c (listof coverage?))] [covered-cases (-> coverage? (listof (cons/c string? natural-number/c)))]) diff --git a/collects/redex/tests/bitmap-test.ss b/collects/redex/tests/bitmap-test.ss index e5f73397d9..5b2bf981d7 100644 --- a/collects/redex/tests/bitmap-test.ss +++ b/collects/redex/tests/bitmap-test.ss @@ -163,5 +163,20 @@ (test (render-lw lang (to-lw (x_^abcdef x_q^abcdef))) "superscripts.png") +;; `variable-not-in' in `where' RHS rendered as `fresh' +(define-metafunction lang + [(f (name n 1)) + (x x_1 x_2 x_3) + (where x ,(variable-not-in 'y 'x)) + (where (x_1 x_2) ,(variables-not-in 'z '(x1 x2))) + (where x_3 (variables-not-in 'z '(x1 x2)))]) +(test (render-metafunction f) "var-not-in.png") +(let ([variable-not-in list]) + (define-metafunction lang + [(g 1) + x + (where x ,(variable-not-in 'y 'x))]) + (test (render-metafunction g) "var-not-in-rebound.png")) + (printf "bitmap-test.ss: ") (done) diff --git a/collects/redex/tests/bmps-macosx/var-not-in-rebound.png b/collects/redex/tests/bmps-macosx/var-not-in-rebound.png new file mode 100644 index 0000000000..79e5b401f5 Binary files /dev/null and b/collects/redex/tests/bmps-macosx/var-not-in-rebound.png differ diff --git a/collects/redex/tests/bmps-macosx/var-not-in.png b/collects/redex/tests/bmps-macosx/var-not-in.png new file mode 100644 index 0000000000..e6efc40fec Binary files /dev/null and b/collects/redex/tests/bmps-macosx/var-not-in.png differ