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

Special typesetting for metafunction `where' clauses in which the

Browse Source 
right-hand side is a call to `variable-not-in' or `variables-not-in'

svn: r17920
This commit is contained in:
Casey Klein 2010-02-01 13:46:32 +00:00
parent 99bebecd75
commit db0ec3eb07
7 changed files with 126 additions and 77 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

59
collects/redex/private/fresh.ss Normal file
View File

@ -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?))])

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

@ -3,7 +3,8 @@
(lib "utils.ss" "texpict") (lib "utils.ss" "texpict")
scheme/gui/base scheme/gui/base
scheme/class scheme/class
(only-in scheme/list drop-right last) scheme/match
(only-in scheme/list drop-right last partition)
"reduction-semantics.ss" "reduction-semantics.ss"
"struct.ss" "struct.ss"
"loc-wrapper.ss" "loc-wrapper.ss"
@ -793,20 +794,24 @@
[scs (map (lambda (eqn) [scs (map (lambda (eqn)
(if (null? (list-ref eqn 1)) (if (null? (list-ref eqn 1))
#f #f
(side-condition-pict null (let-values ([(fresh where/sc) (partition metafunc-extra-fresh? (list-ref eqn 1))])
(map (lambda (p) (side-condition-pict (foldl (λ (clause picts)
(if (pair? p) (foldr (λ (l ps) (cons (wrapper->pict l) ps))
(cons (wrapper->pict (car p)) picts (metafunc-extra-fresh-vars clause)))
(wrapper->pict (cdr p))) '() fresh)
(wrapper->pict p))) (map (match-lambda
(list-ref eqn 1)) [(struct metafunc-extra-where (lhs rhs))
(if (memq style '(up-down/vertical-side-conditions (cons (wrapper->pict lhs) (wrapper->pict rhs))]
left-right/vertical-side-conditions)) [(struct metafunc-extra-side-cond (expr))
0 (wrapper->pict expr)])
(if (memq style '(up-down/compact-side-conditions where/sc)
left-right/compact-side-conditions)) (if (memq style '(up-down/vertical-side-conditions
max-line-w/pre-sc left-right/vertical-side-conditions))
+inf.0))))) 0
(if (memq style '(up-down/compact-side-conditions
left-right/compact-side-conditions))
max-line-w/pre-sc
+inf.0))))))
eqns)]) eqns)])
(case style (case style
[(left-right left-right/vertical-side-conditions left-right/compact-side-conditions left-right/beside-side-conditions) [(left-right left-right/vertical-side-conditions left-right/compact-side-conditions left-right/beside-side-conditions)

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

@ -3,6 +3,7 @@
(require "matcher.ss" (require "matcher.ss"
"struct.ss" "struct.ss"
"term.ss" "term.ss"
"fresh.ss"
"loc-wrapper.ss" "loc-wrapper.ss"
"error.ss" "error.ss"
mzlib/trace mzlib/trace
@ -1016,6 +1017,11 @@
(define-struct metafunc-case (cp rhs lhs-pat src-loc id)) (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) (define-syntax (in-domain? stx)
(syntax-case stx () (syntax-case stx ()
[(_ (name exp ...)) [(_ (name exp ...))
@ -1249,11 +1255,25 @@
(map (λ (hm) (map (λ (hm)
(map (map
(λ (lst) (λ (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) [(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) [(side-condition x)
(to-lw/uq/proc #'x)])) #`(make-metafunc-extra-side-cond
#,(to-lw/uq/proc #'x))]))
(reverse (syntax->list hm)))) (reverse (syntax->list hm))))
(syntax->list #'(... seq-of-tl-side-cond/binds)))] (syntax->list #'(... seq-of-tl-side-cond/binds)))]
@ -1265,8 +1285,8 @@
[(x-lhs-for-lw ...) #'(... seq-of-lhs-for-lw)]) [(x-lhs-for-lw ...) #'(... seq-of-lhs-for-lw)])
#'(list (list x-lhs-for-lw #'(list (list x-lhs-for-lw
(list (cons bind-id/lw bind-pat/lw) ... (list (make-metafunc-extra-where bind-id/lw bind-pat/lw) ...
(cons rhs-bind-id/lw rhs-bind-pat/lw/uq) ... (make-metafunc-extra-where rhs-bind-id/lw rhs-bind-pat/lw/uq) ...
where/sc/lw ...) where/sc/lw ...)
rhs/lw) rhs/lw)
...)))]) ...)))])
@ -1943,61 +1963,6 @@
(cons this-one (loop (cdr l))) (cons this-one (loop (cdr l)))
(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) (define (reduction-relation->rule-names x)
(reverse (reduction-relation-rule-names x))) (reverse (reduction-relation-rule-names x)))
@ -2169,6 +2134,10 @@
metafunc-proc? metafunc-proc?
(struct-out metafunc-case) (struct-out metafunc-case)
(struct-out metafunc-extra-side-cond)
(struct-out metafunc-extra-where)
(struct-out metafunc-extra-fresh)
(struct-out binds)) (struct-out binds))
(provide test-match (provide test-match

5
collects/redex/reduction-semantics.ss
View File

@ -54,6 +54,9 @@
(struct-out exn:fail:redex:test) (struct-out exn:fail:redex:test)
(struct-out counterexample)) (struct-out counterexample))
(provide variable-not-in
variables-not-in)
(provide/contract (provide/contract
[current-traced-metafunctions (parameter/c (or/c 'all (listof symbol?)))] [current-traced-metafunctions (parameter/c (or/c 'all (listof symbol?)))]
[reduction-relation->rule-names (-> reduction-relation? (listof symbol?))] [reduction-relation->rule-names (-> reduction-relation? (listof symbol?))]
@ -71,7 +74,5 @@
[lookup-binding (case-> [lookup-binding (case->
(-> bindings? symbol? any) (-> bindings? symbol? any)
(-> bindings? symbol? (-> any) 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?))] [relation-coverage (parameter/c (listof coverage?))]
[covered-cases (-> coverage? (listof (cons/c string? natural-number/c)))]) [covered-cases (-> coverage? (listof (cons/c string? natural-number/c)))])

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

@ -163,5 +163,20 @@
(test (render-lw lang (to-lw (x_^abcdef x_q^abcdef))) (test (render-lw lang (to-lw (x_^abcdef x_q^abcdef)))
"superscripts.png") "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: ") (printf "bitmap-test.ss: ")
(done) (done)

BIN
collects/redex/tests/bmps-macosx/var-not-in-rebound.png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 3.2 KiB

BIN
collects/redex/tests/bmps-macosx/var-not-in.png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 5.0 KiB