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

merged 1115:1124 from branches/redex-names, adds support for named reductions that get drawn in the traces window

Browse Source 
svn: r1126
This commit is contained in:
Jacob Matthews 2005-10-22 02:47:51 +00:00
parent f3a67ccb9a
commit a255e439ea
4 changed files with 304 additions and 80 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

197
collects/mrlib/graph.ss
View File

@ -19,6 +19,7 @@
get-parents get-parents
add-parent add-parent
remove-parent remove-parent
has-self-loop?
find-shortest-path)) find-shortest-path))
@ -36,6 +37,17 @@
(union false/c (is-a?/c pen%)) (union false/c (is-a?/c pen%))
(union false/c (is-a?/c brush%)) (union false/c (is-a?/c brush%))
(union false/c (is-a?/c brush%)) (union false/c (is-a?/c brush%))
number?
number?
. -> .
void?)
((is-a?/c graph-snip<%>)
(is-a?/c graph-snip<%>)
(union false/c (is-a?/c pen%))
(union false/c (is-a?/c pen%))
(union false/c (is-a?/c brush%))
(union false/c (is-a?/c brush%))
(union false/c string?)
. -> . . -> .
void?) void?)
((is-a?/c graph-snip<%>) ((is-a?/c graph-snip<%>)
@ -47,7 +59,21 @@
number? number?
number? number?
. -> . . -> .
void?)))) void?)))
(add-links/text-colors
((is-a?/c graph-snip<%>)
(is-a?/c graph-snip<%>)
(union false/c (is-a?/c pen%))
(union false/c (is-a?/c pen%))
(union false/c (is-a?/c brush%))
(union false/c (is-a?/c brush%))
(union false/c (is-a?/c color%))
(union false/c (is-a?/c color%))
number?
number?
(union false/c string?)
. -> .
void?)))
(define self-offset 10) (define self-offset 10)
@ -72,8 +98,12 @@
(define default-light-pen (send the-pen-list find-or-create-pen "light blue" 1 'solid)) (define default-light-pen (send the-pen-list find-or-create-pen "light blue" 1 'solid))
(define default-dark-brush (send the-brush-list find-or-create-brush "light blue" 'solid)) (define default-dark-brush (send the-brush-list find-or-create-brush "light blue" 'solid))
(define default-light-brush (send the-brush-list find-or-create-brush "white" 'solid)) (define default-light-brush (send the-brush-list find-or-create-brush "white" 'solid))
(define default-dark-text "blue")
(define default-light-text "light blue")
(define-struct link (snip dark-pen light-pen dark-brush light-brush dx dy))
;; label is boolean or string
(define-struct link (snip dark-pen light-pen dark-brush light-brush dark-text light-text dx dy label))
;; add-links : (is-a?/c graph-snip<%>) (is-a?/c graph-snip<%>) -> void ;; add-links : (is-a?/c graph-snip<%>) (is-a?/c graph-snip<%>) -> void
;; : (is-a?/c graph-snip<%>) (is-a?/c graph-snip<%>) pen pen brush brush -> void ;; : (is-a?/c graph-snip<%>) (is-a?/c graph-snip<%>) pen pen brush brush -> void
@ -82,12 +112,20 @@
[(parent child) (add-links parent child #f #f #f #f)] [(parent child) (add-links parent child #f #f #f #f)]
[(parent child dark-pen light-pen dark-brush light-brush) [(parent child dark-pen light-pen dark-brush light-brush)
(add-links parent child dark-pen light-pen dark-brush light-brush 0 0)] (add-links parent child dark-pen light-pen dark-brush light-brush 0 0)]
[(parent child dark-pen light-pen dark-brush light-brush label)
(add-links parent child dark-pen light-pen dark-brush light-brush 0 0 label)]
[(parent child dark-pen light-pen dark-brush light-brush dx dy) [(parent child dark-pen light-pen dark-brush light-brush dx dy)
(add-links parent child dark-pen light-pen dark-brush light-brush dx dy #f)]
[(parent child dark-pen light-pen dark-brush light-brush dx dy label)
(send parent add-child child) (send parent add-child child)
(send child add-parent parent dark-pen light-pen dark-brush light-brush dx dy)])) (send child add-parent parent dark-pen light-pen dark-brush light-brush dx dy label)]))
(define (graph-snip-mixin %) (define (add-links/text-colors parent child dark-pen light-pen dark-brush light-brush dark-text light-text dx dy label)
(class* % (graph-snip<%>) (send parent add-child child)
(send child add-parent parent dark-pen light-pen dark-brush light-brush dark-text light-text dx dy label))
(define graph-snip-mixin
(mixin ((class->interface editor-snip%)) (graph-snip<%>)
(field (children null)) (field (children null))
(define/public (get-children) children) (define/public (get-children) children)
(define/public (add-child child) (define/public (add-child child)
@ -106,6 +144,10 @@
[(parent dark-pen light-pen dark-brush light-brush) [(parent dark-pen light-pen dark-brush light-brush)
(add-parent parent dark-pen light-pen dark-brush light-brush 0 0)] (add-parent parent dark-pen light-pen dark-brush light-brush 0 0)]
[(parent dark-pen light-pen dark-brush light-brush dx dy) [(parent dark-pen light-pen dark-brush light-brush dx dy)
(add-parent parent dark-pen light-pen dark-brush light-brush dx dy #f)]
[(parent dark-pen light-pen dark-brush light-brush dx dy)
(add-parent parent dark-pen light-pen dark-brush light-brush #f #f dx dy #f)]
[(parent dark-pen light-pen dark-brush light-brush dark-text light-text dx dy label)
(unless (memf (lambda (parent-link) (eq? (link-snip parent-link) parent)) parent-links) (unless (memf (lambda (parent-link) (eq? (link-snip parent-link) parent)) parent-links)
(set! parent-links (set! parent-links
(cons (make-link parent (cons (make-link parent
@ -113,8 +155,11 @@
(or light-pen default-light-pen) (or light-pen default-light-pen)
(or dark-brush default-dark-brush) (or dark-brush default-dark-brush)
(or light-brush default-light-brush) (or light-brush default-light-brush)
(or dark-text default-dark-text)
(or light-text default-light-text)
dx dx
dy) dy
label)
parent-links)))])) parent-links)))]))
(define/public (remove-parent parent) (define/public (remove-parent parent)
(when (memf (lambda (parent-link) (eq? (link-snip parent-link) parent)) parent-links) (when (memf (lambda (parent-link) (eq? (link-snip parent-link) parent)) parent-links)
@ -124,6 +169,9 @@
parent-links parent-links
(lambda (parent parent-link) (eq? (link-snip parent-link) parent)))))) (lambda (parent parent-link) (eq? (link-snip parent-link) parent))))))
(define/public (has-self-loop?)
(memq this (get-children)))
(define/public (find-shortest-path other) (define/public (find-shortest-path other)
(define visited-ht (make-hash-table)) (define visited-ht (make-hash-table))
(define (first-view? n) (define (first-view? n)
@ -147,7 +195,29 @@
(map (lambda (child) (cons child path)) (filter first-view? (send (car path) get-children))) (map (lambda (child) (cons child path)) (filter first-view? (send (car path) get-children)))
acc)))]))]))) acc)))]))])))
(super-instantiate ()) (init-field [left-margin 1]
[right-margin 1]
[top-margin 1]
[bottom-margin 1]
[left-inset 0]
[right-inset 0]
[top-inset 0]
[bottom-inset 0]
)
(super-new [left-margin left-margin]
[right-margin right-margin]
[top-margin top-margin]
[bottom-margin bottom-margin]
[left-inset left-inset]
[right-inset right-inset]
[top-inset top-inset]
[bottom-inset bottom-inset]
)
(inherit set-snipclass) (inherit set-snipclass)
(set-snipclass snipclass))) (set-snipclass snipclass)))
@ -176,19 +246,19 @@
arrowhead-long-side arrowhead-long-side
arrowhead-short-side)) arrowhead-short-side))
(inherit dc-location-to-editor-location get-canvas) (inherit dc-location-to-editor-location get-canvas get-dc)
(field (currently-overs null)) (field (currently-overs null))
(define/override (on-event evt) (define/override (on-event evt)
(cond (cond
[(send evt leaving?) [(send evt leaving?)
(change-currently-overs null) (change-currently-overs null (get-dc))
(super on-event evt)] (super on-event evt)]
[(or (send evt entering?) [(or (send evt entering?)
(send evt moving?)) (send evt moving?))
(let ([ex (send evt get-x)] (let ([ex (send evt get-x)]
[ey (send evt get-y)]) [ey (send evt get-y)])
(let-values ([(x y) (dc-location-to-editor-location ex ey)]) (let-values ([(x y) (dc-location-to-editor-location ex ey)])
(change-currently-overs (find-snips-under-mouse x y)))) (change-currently-overs (find-snips-under-mouse x y) (get-dc))))
(super on-event evt)] (super on-event evt)]
[else [else
(super on-event evt)])) (super on-event evt)]))
@ -203,11 +273,11 @@
#;(super on-interactive-move evt)) #;(super on-interactive-move evt))
(define/override (interactive-adjust-move snip x y) (define/override (interactive-adjust-move snip x y)
(invalidate-to-children/parents snip) (invalidate-to-children/parents snip (get-dc))
(super interactive-adjust-move snip x y)) (super interactive-adjust-move snip x y))
(define/augment (after-insert snip before x y) (define/augment (after-insert snip before x y)
(invalidate-to-children/parents snip) (invalidate-to-children/parents snip (get-dc))
#;(super after-insert snip before x y)) #;(super after-insert snip before x y))
;; invalidate-selected-snips : -> void ;; invalidate-selected-snips : -> void
@ -216,7 +286,7 @@
(define/private (invalidate-selected-snips) (define/private (invalidate-selected-snips)
(let loop ([snip (find-next-selected-snip #f)]) (let loop ([snip (find-next-selected-snip #f)])
(when snip (when snip
(invalidate-to-children/parents snip) (invalidate-to-children/parents snip (get-dc))
(loop (find-next-selected-snip snip))))) (loop (find-next-selected-snip snip)))))
(define/private (add-to-rect from to rect) (define/private (add-to-rect from to rect)
@ -236,7 +306,6 @@
(max (+ yf hf) (+ yt ht) (rect-bottom rect)) (max (+ yf hf) (+ yt ht) (rect-bottom rect))
(max (+ yf hf) (+ yt ht)))))) (max (+ yf hf) (+ yt ht))))))
;; find-snips-under-mouse : num num -> (listof graph-snip<%>) ;; find-snips-under-mouse : num num -> (listof graph-snip<%>)
(define/private (find-snips-under-mouse x y) (define/private (find-snips-under-mouse x y)
(let loop ([snip (find-first-snip)]) (let loop ([snip (find-first-snip)])
@ -251,7 +320,7 @@
[else null]))) [else null])))
;; change-currently-overs : (listof snip) -> void ;; change-currently-overs : (listof snip) -> void
(define/private (change-currently-overs new-currently-overs) (define/private (change-currently-overs new-currently-overs dc)
(unless (set-equal new-currently-overs currently-overs) (unless (set-equal new-currently-overs currently-overs)
(let ([old-currently-overs currently-overs]) (let ([old-currently-overs currently-overs])
(set! currently-overs new-currently-overs) (set! currently-overs new-currently-overs)
@ -259,11 +328,11 @@
(on-mouse-over-snips currently-overs) (on-mouse-over-snips currently-overs)
(for-each (for-each
(lambda (old-currently-over) (lambda (old-currently-over)
(invalidate-to-children/parents old-currently-over)) (invalidate-to-children/parents old-currently-over dc))
old-currently-overs) old-currently-overs)
(for-each (for-each
(lambda (new-currently-over) (lambda (new-currently-over)
(invalidate-to-children/parents new-currently-over)) (invalidate-to-children/parents new-currently-over dc))
new-currently-overs)))) new-currently-overs))))
(define/public (on-mouse-over-snips snips) (define/public (on-mouse-over-snips snips)
@ -277,24 +346,29 @@
(andmap (lambda (s2) (memq s2 los1)) los2) (andmap (lambda (s2) (memq s2 los1)) los2)
#t)) #t))
;; invalidate-to-children/parents : snip -> void ;; invalidate-to-children/parents : snip dc -> void
;; invalidates the region containing this snip and ;; invalidates the region containing this snip and
;; all of its children and parents. ;; all of its children and parents.
(inherit invalidate-bitmap-cache) (inherit invalidate-bitmap-cache)
(define/private (invalidate-to-children/parents snip) (define/private (invalidate-to-children/parents snip dc)
(when (is-a? snip graph-snip<%>) (when (is-a? snip graph-snip<%>)
(let* ([parents-and-children (append (get-all-parents snip) (let* ([parents-and-children (append (get-all-parents snip)
(get-all-children snip))] (get-all-children snip))]
[rects (eliminate-redundancies (get-rectangles snip parents-and-children))] [rects (eliminate-redundancies (get-rectangles snip parents-and-children))]
[union (union-rects rects)] [union (union-rects rects)]
[text-height (call-with-values
(λ () (send dc get-text-extent "Label" #f #f 0))
(λ (w h a s) h))]
[invalidate-rect [invalidate-rect
(lambda (rect) (lambda (rect)
(invalidate-bitmap-cache (rect-left rect) (invalidate-bitmap-cache (- (rect-left rect) text-height)
(rect-top rect) (- (rect-top rect) text-height)
(- (rect-right rect) (+ (- (rect-right rect)
(rect-left rect)) (rect-left rect))
(- (rect-bottom rect) text-height)
(rect-top rect))))]) (+ (- (rect-bottom rect)
(rect-top rect))
text-height)))])
(cond (cond
[(< (rect-area union) [(< (rect-area union)
(apply + (map (lambda (x) (rect-area x)) rects))) (apply + (map (lambda (x) (rect-area x)) rects)))
@ -338,19 +412,23 @@
(let* ([c/p (car c/p-snips)] (let* ([c/p (car c/p-snips)]
[rect [rect
(if (eq? c/p main-snip) (if (eq? c/p main-snip)
(let-values ([(sx sy sw sh) (get-position c/p)]) (let-values ([(sx sy sw sh) (get-position c/p)]
[(_1 h _2 _3) (send (get-dc) get-text-extent "yX")])
(make-rect (- sx self-offset) (make-rect (- sx self-offset)
sy sy
(+ (+ sx sw) self-offset) (+ (+ sx sw) self-offset)
(+ (+ sy sh) self-offset))) (+ (+ sy sh) self-offset h)))
(union-rects (list main-snip-rect (union-rects (list main-snip-rect
(snip->rect c/p))))]) (snip->rect c/p))))])
(cons rect (loop (cdr c/p-snips))))])))) (cons rect (loop (cdr c/p-snips))))]))))
(define/private (snip->rect snip) (define/private (snip->rect snip)
(let-values ([(sx sy sw sh) (get-position snip)]) (let-values ([(sx sy sw sh) (get-position snip)]
(make-rect sx sy (+ sx sw) (+ sy sh)))) [(_1 h _2 _3) (send (get-dc) get-text-extent "yX")])
(make-rect sx
sy
(+ sx sw)
(max (+ sy sh) (+ sy (/ sh 2) (* 2 (sin (/ arrowhead-angle-width 2)) arrowhead-long-side) h)))))
(define/private (rect-area rect) (define/private (rect-area rect)
(* (- (rect-right rect) (* (- (rect-right rect)
@ -553,11 +631,15 @@
(cond (cond
[(eq? from to) [(eq? from to)
(set-pen/brush from-link dark-lines?) (set-pen/brush from-link dark-lines?)
(draw-self-connection dx dy (link-snip from-link))] (draw-self-connection dx dy (link-snip from-link) from-link dark-lines?)]
[else [else
(draw-non-self-connection dx dy from-link dark-lines? to)]))))) (draw-non-self-connection dx dy from-link dark-lines? to)])))))
(define (draw-self-connection dx dy snip) (define (get-text-length txt)
(let-values ([(text-len h d v) (send dc get-text-extent txt)])
text-len))
(define (draw-self-connection dx dy snip the-link dark-lines?)
(let*-values ([(sx sy sw sh) (get-position snip)] (let*-values ([(sx sy sw sh) (get-position snip)]
[(s1x s1y) (values (+ sx sw) (+ sy (* sh 1/2)))] [(s1x s1y) (values (+ sx sw) (+ sy (* sh 1/2)))]
[(s2x s2y) (values (+ sx sw self-offset) (+ sy (* 3/4 sh) (* 1/2 self-offset)))] [(s2x s2y) (values (+ sx sw self-offset) (+ sy (* 3/4 sh) (* 1/2 self-offset)))]
@ -578,6 +660,19 @@
(send dc draw-spline (+ dx s1x) (+ dy s1y) (+ dx b12x) (+ dy b12y) (+ dx s2x) (+ dy s2y)) (send dc draw-spline (+ dx s1x) (+ dy s1y) (+ dx b12x) (+ dy b12y) (+ dx s2x) (+ dy s2y))
(send dc draw-spline (+ dx s2x) (+ dy s2y) (+ dx b23x) (+ dy b23y) (+ dx s3x) (+ dy s3y)) (send dc draw-spline (+ dx s2x) (+ dy s2y) (+ dx b23x) (+ dy b23y) (+ dx s3x) (+ dy s3y))
(send dc draw-line (+ dx s3x) (+ dy s3y) (+ dx s6x) (+ dy s6y)) (send dc draw-line (+ dx s3x) (+ dy s3y) (+ dx s6x) (+ dy s6y))
(let* ((textlen (get-text-length (link-label the-link)))
(linelen (- s6x s3x))
(offset (* 1/2 (- linelen textlen))))
(when #t (> sw textlen)
(send dc draw-text
(link-label the-link)
(+ dx s3x offset)
(+ dy s3y)
#f
0
0)))
(send dc draw-spline (+ dx s4x) (+ dy s4y) (+ dx b45x) (+ dy b45y) (+ dx s5x) (+ dy s5y)) (send dc draw-spline (+ dx s4x) (+ dy s4y) (+ dx b45x) (+ dy b45y) (+ dx s5x) (+ dy s5y))
(send dc draw-spline (+ dx s5x) (+ dy s5y) (+ dx b56x) (+ dy b56y) (+ dx s6x) (+ dy s6y)) (send dc draw-spline (+ dx s5x) (+ dy s5y) (+ dx b56x) (+ dy b56y) (+ dx s6x) (+ dy s6y))
(send dc draw-polygon points dx dy))) (send dc draw-polygon points dx dy)))
@ -613,7 +708,8 @@
(find-intersection x1 y1 x2 y2 (find-intersection x1 y1 x2 y2
rt tt rt bt))]) rt tt rt bt))])
(when (and from-x from-y to-x to-y) (when (and from-x from-y to-x to-y)
(let () (let ((from-pt (make-rectangular from-x from-y))
(to-pt (make-rectangular to-x to-y)))
(define (arrow-point-ok? point-x point-y) (define (arrow-point-ok? point-x point-y)
(and (in-rectangle? point-x point-y (and (in-rectangle? point-x point-y
(min lt rt lf rf) (min tt bt tf bf) (min lt rt lf rf) (min tt bt tf bf)
@ -640,7 +736,31 @@
(arrow-point-ok? (send point4 get-x) (send point4 get-y))) (arrow-point-ok? (send point4 get-x) (send point4 get-y)))
;; the arrowhead is not overlapping the snips, so draw it ;; the arrowhead is not overlapping the snips, so draw it
;; (this is only an approximate test, but probably good enough) ;; (this is only an approximate test, but probably good enough)
(send dc draw-polygon points dx dy))])))))))) (send dc draw-polygon points dx dy))
(when (named-link? from-link)
(let*-values ([(text-len h d v) (send dc get-text-extent (link-label from-link))]
[(x) (/ (+ from-x to-x) 2)]
[(y) (/ (+ from-y to-y) 2)]
[(theta) (- (angle (- to-pt from-pt)))]
[(flip?) #f #;(negative? (- to-x from-x))]
[(text-angle)
(if flip?
(+ theta pi)
theta)]
[(x)
(- x (* h (cos (if flip? (+ (- theta) pi) (- theta)))))]
[(y)
(- y (* h (sin (if flip? (+ (- theta) pi) (- theta)))))]
[(sqr) (λ (x) (* x x))])
(when (> (sqrt (+ (sqr (- to-x from-x)) (sqr (- to-y from-y)))) text-len)
(send dc draw-text (link-label from-link)
(+ dx x)
(+ dy y)
#f
0
text-angle))
))]))))))))
(define (named-link? l) (link-label l))
(define (set-pen/brush from-link dark-lines?) (define (set-pen/brush from-link dark-lines?)
(send dc set-brush (send dc set-brush
@ -650,12 +770,17 @@
(send dc set-pen (send dc set-pen
(if dark-lines? (if dark-lines?
(link-dark-pen from-link) (link-dark-pen from-link)
(link-light-pen from-link)))) (link-light-pen from-link)))
(send dc set-text-foreground
(if dark-lines?
(link-dark-text from-link)
(link-light-text from-link))))
;;; body of on-paint ;;; body of on-paint
(when before? (when before?
(let ([old-pen (send dc get-pen)] (let ([old-pen (send dc get-pen)]
[old-brush (send dc get-brush)] [old-brush (send dc get-brush)]
[old-fg (send dc get-text-foreground)]
[os (send dc get-smoothing)]) [os (send dc get-smoothing)])
(send dc set-smoothing 'aligned) (send dc set-smoothing 'aligned)
@ -676,6 +801,7 @@
(send dc set-smoothing os) (send dc set-smoothing os)
(send dc set-pen old-pen) (send dc set-pen old-pen)
(send dc set-text-foreground old-fg)
(send dc set-brush old-brush))) (send dc set-brush old-brush)))
(super on-paint before? dc left top right bottom dx dy draw-caret))) (super on-paint before? dc left top right bottom dx dy draw-caret)))
@ -765,6 +891,7 @@
(send point3 set-y t6y) (send point3 set-y t6y)
(send point4 set-x t5x) (send point4 set-x t5x)
(send point4 set-y t5y))) (send point4 set-y t5y)))
;; HERE!!!
(define/private (should-hilite? snip) (define/private (should-hilite? snip)
(let ([check-one-way (let ([check-one-way

35
collects/reduction-semantics/doc.txt
View File

@ -228,7 +228,7 @@ for two `term-let'-bound identifiers bound to lists of
different lengths to appear together inside an ellipsis. different lengths to appear together inside an ellipsis.
> (reduction language pattern bodies ...) SYNTAX > (reduction language pattern bodies ...) SYNTAX
> (reduction/name language pattern bodies ...) SYNTAX
This form defines a reduction. The first position must This form defines a reduction. The first position must
evaluate to a language defined by the `language' form. The evaluate to a language defined by the `language' form. The
pattern determines which terms this reductions apply to and pattern determines which terms this reductions apply to and
@ -261,7 +261,12 @@ the result of evaluating the last argument to reduction.
See `plug' below and lc-subst is defined by using the See `plug' below and lc-subst is defined by using the
subst.ss library below. subst.ss library below.
The reduction/name form is the same as reduction, but
additionally evaluates the `name' expression and names the
reduction to be its result, which must be a string.
> (reduction/context language context pattern bodies ...) SYNTAX > (reduction/context language context pattern bodies ...) SYNTAX
> (reduction/context/name name language context pattern bodies ...) SYNTAX
reduction/context is a short-hand form of reduction. It reduction/context is a short-hand form of reduction. It
automatically adds the `in-hole' pattern and the call to automatically adds the `in-hole' pattern and the call to
@ -276,6 +281,10 @@ example is this:
(term (v_i ...)) (term (v_i ...))
(term e_body)))) (term e_body))))
reduction/context/name is the same as reduction/context, but
additionally evaluates the `name' expression and names the
reduction to be its result, which must be a string.
> red? : (any? . -> . boolean?) > red? : (any? . -> . boolean?)
Returns #t if its argument is a reduction (produced by `reduction', Returns #t if its argument is a reduction (produced by `reduction',
@ -387,23 +396,24 @@ followed by an ellipsis. Nested ellipses produce nested lists.
The _gui.ss_ library provides three functions: The _gui.ss_ library provides three functions:
> (traces language reductions expr [pp]) > (traces language reductions expr [pp] [colors])
This function calls traces/multiple with language, reductions This function calls traces/multiple with language, reductions
and (list expr). and (list expr), and its optional arguments if supplied.
> (traces/multiple lang reductions exprs [pp]) > (traces/multiple lang reductions exprs [pp] [colors])
This function calls traces/pred with the predicate This function calls traces/pred with the predicate
(lambda (x) #t) (lambda (x) #t)
> (traces/pred lang reductions exprs pred [pp]) > (traces/pred lang reductions exprs pred [pp] [colors])
lang : language lang : language
reductions : (listof reduction) reductions : (listof reduction)
exprs : (listof sexp) exprs : (listof sexp)
pred : (sexp -> boolean) pred : (sexp -> boolean)
pp : (any -> string) pp : (any -> string)
| (any port number (is-a?/c text%) -> void) | (any port number (is-a?/c text%) -> void)
colors : (listof (list string string))
This function opens a new window and inserts each This function opens a new window and inserts each
expr. Then, reduces the terms until either expr. Then, reduces the terms until either
@ -427,11 +437,16 @@ instead invoked with a single argument, the s-expression to
render, and it must return a string which the GUI will use render, and it must return a string which the GUI will use
as a representation of the given expression for display. as a representation of the given expression for display.
The default pp uses MzLib's pretty-print function. See The default pp, provided as default-pretty-printer, uses
threads.ss in the examples directory for an example use MzLib's pretty-print function. See threads.ss in the
of the one-argument form of this argument and examples directory for an example use of the one-argument
ho-contracts.ss in the examples directory for an example form of this argument and ho-contracts.ss in the examples
use of its four-argument form. directory for an example use of its four-argument form.
The colors argument, if provided, specifies a list of
reduction-name/color-string pairs. The traces gui will color
arrows drawn because of the given reduction name with the
given color instead of using the default color.
You can save the contents of the window as a postscript file You can save the contents of the window as a postscript file
from the menus. from the menus.

94
collects/reduction-semantics/gui.ss
View File

@ -11,31 +11,32 @@
(lib "pretty.ss") (lib "pretty.ss")
(lib "class.ss") (lib "class.ss")
(lib "contract.ss") (lib "contract.ss")
(lib "list.ss")) (lib "list.ss")
(lib "match.ss"))
(provide/contract (provide/contract
[traces (opt-> (compiled-lang? [traces (opt-> (compiled-lang?
(listof red?) (listof red?)
any/c) any/c)
(procedure?) (procedure? (listof any/c))
any)] any)]
[traces/pred (opt-> (compiled-lang? [traces/pred (opt-> (compiled-lang?
(listof red?) (listof red?)
(listof any/c) (listof any/c)
(any/c . -> . boolean?)) (any/c . -> . boolean?))
(procedure?) (procedure? (listof any/c))
any)] any)]
[traces/multiple (opt-> (compiled-lang? [traces/multiple (opt-> (compiled-lang?
(listof red?) (listof red?)
(listof any/c)) (listof any/c))
(procedure?) (procedure? (listof any/c))
any)]) any)])
(provide reduction-steps-cutoff initial-font-size initial-char-width (provide reduction-steps-cutoff initial-font-size initial-char-width
dark-pen-color light-pen-color dark-brush-color light-brush-color) dark-pen-color light-pen-color dark-brush-color light-brush-color
dark-text-color light-text-color
(rename default-pp default-pretty-printer))
(preferences:set-default 'plt-reducer:show-bottom #t boolean?) (preferences:set-default 'plt-reducer:show-bottom #t boolean?)
@ -43,6 +44,9 @@
(define light-pen-color (make-parameter "lightblue")) (define light-pen-color (make-parameter "lightblue"))
(define dark-brush-color (make-parameter "lightblue")) (define dark-brush-color (make-parameter "lightblue"))
(define light-brush-color (make-parameter "white")) (define light-brush-color (make-parameter "white"))
(define dark-text-color (make-parameter "blue"))
(define light-text-color (make-parameter "lightblue"))
;; after (about) this many steps, stop automatic, initial reductions ;; after (about) this many steps, stop automatic, initial reductions
(define reduction-steps-cutoff (make-parameter 20)) (define reduction-steps-cutoff (make-parameter 20))
@ -68,15 +72,15 @@
(pretty-print v port))) (pretty-print v port)))
(define traces (define traces
(opt-lambda (lang reductions expr [pp default-pp]) (opt-lambda (lang reductions expr [pp default-pp] [colors '()])
(traces/multiple lang reductions (list expr) pp))) (traces/multiple lang reductions (list expr) pp colors)))
(define traces/multiple (define traces/multiple
(opt-lambda (lang reductions exprs [pp default-pp]) (opt-lambda (lang reductions exprs [pp default-pp] [colors '()])
(traces/pred lang reductions exprs (lambda (x) #t) pp))) (traces/pred lang reductions exprs (lambda (x) #t) pp colors)))
(define traces/pred (define traces/pred
(opt-lambda (lang reductions exprs pred [pp default-pp]) (opt-lambda (lang reductions exprs pred [pp default-pp] [colors '()])
(define main-eventspace (current-eventspace)) (define main-eventspace (current-eventspace))
(define graph-pb (make-object graph-pasteboard%)) (define graph-pb (make-object graph-pasteboard%))
(define f (instantiate red-sem-frame% () (define f (instantiate red-sem-frame% ()
@ -137,7 +141,10 @@
;; only changed on the reduction thread ;; only changed on the reduction thread
;; frontier : (listof (is-a?/c graph-editor-snip%)) ;; frontier : (listof (is-a?/c graph-editor-snip%))
(define frontier (map (lambda (expr) (build-snip snip-cache #f expr pred pp)) exprs)) (define frontier (map (lambda (expr) (build-snip snip-cache #f expr pred pp
(dark-pen-color) (light-pen-color)
(dark-text-color) (light-text-color) #f))
exprs))
;; set-font-size : number -> void ;; set-font-size : number -> void
;; =eventspace main thread= ;; =eventspace main thread=
@ -150,6 +157,38 @@
(send scheme-delta set-size-add size) (send scheme-delta set-size-add size)
(send scheme-standard set-delta scheme-delta))) (send scheme-standard set-delta scheme-delta)))
;; color-spec-list->color-scheme : (list (union string? #f)^4) -> (list string?^4)
;; converts a list of user-specified colors (including false) into a list of color strings, filling in
;; falses with the default colors
(define (color-spec-list->color-scheme l)
(map (λ (c d) (or c d))
l
(list (dark-pen-color) (light-pen-color) (dark-text-color) (light-text-color))))
(define name->color-ht
(let ((ht (make-hash-table 'equal)))
(for-each
(λ (c)
(hash-table-put! ht (car c)
(color-spec-list->color-scheme
(match (cdr c)
[(color)
(list color color (dark-text-color) (light-text-color))]
[(dark-arrow-color light-arrow-color)
(list dark-arrow-color light-arrow-color (dark-text-color) (light-text-color))]
[(dark-arrow-color light-arrow-color text-color)
(list dark-arrow-color light-arrow-color text-color text-color)]
[(_ _ _ _)
(cdr c)]))))
colors)
ht))
;; red->colors : reduction -> (values string string string string)
(define (red->colors red)
(apply values (hash-table-get name->color-ht (reduction->name red)
(λ () (list (dark-pen-color) (light-pen-color) (dark-text-color) (light-text-color))))))
;; reduce-frontier : -> void ;; reduce-frontier : -> void
;; =reduction thread= ;; =reduction thread=
;; updates frontier with the new snip after a single reduction ;; updates frontier with the new snip after a single reduction
@ -166,11 +205,14 @@
[new-snips [new-snips
(filter (filter
(lambda (x) x) (lambda (x) x)
(map (lambda (sexp) (map (lambda (red+sexp)
(call-on-eventspace-main-thread (let-values ([(red sexp) (apply values red+sexp)])
(λ () (call-on-eventspace-main-thread
(build-snip snip-cache snip sexp pred pp)))) (λ ()
(reduce reductions (send snip get-expr))))] (let-values ([(dark-arrow-color light-arrow-color dark-label-color light-label-color) (red->colors red)])
(build-snip snip-cache snip sexp pred pp light-arrow-color dark-arrow-color dark-label-color light-label-color
(reduction->name red)))))))
(reduce/tag-with-reduction reductions (send snip get-expr))))]
[new-y [new-y
(call-on-eventspace-main-thread (call-on-eventspace-main-thread
(lambda () ; =eventspace main thread= (lambda () ; =eventspace main thread=
@ -440,11 +482,13 @@
;; sexp ;; sexp
;; sexp -> boolean ;; sexp -> boolean
;; (any port number -> void) ;; (any port number -> void)
;; color
;; (union #f string)
;; -> (union #f (is-a?/c graph-editor-snip%)) ;; -> (union #f (is-a?/c graph-editor-snip%))
;; returns #f if a snip corresponding to the expr has already been created. ;; returns #f if a snip corresponding to the expr has already been created.
;; also adds in the links to the parent snip ;; also adds in the links to the parent snip
;; =eventspace main thread= ;; =eventspace main thread=
(define (build-snip cache parent-snip expr pred pp) (define (build-snip cache parent-snip expr pred pp light-arrow-color dark-arrow-color dark-label-color light-label-color label)
(let-values ([(snip new?) (let-values ([(snip new?)
(let/ec k (let/ec k
(k (k
@ -457,11 +501,15 @@
(k new-snip #t)))) (k new-snip #t))))
#f))]) #f))])
(when parent-snip (when parent-snip
(add-links parent-snip snip (add-links/text-colors parent-snip snip
(send the-pen-list find-or-create-pen (dark-pen-color) 0 'solid) (send the-pen-list find-or-create-pen dark-arrow-color 0 'solid)
(send the-pen-list find-or-create-pen (light-pen-color) 0 'solid) (send the-pen-list find-or-create-pen light-arrow-color 0 'solid)
(send the-brush-list find-or-create-brush (dark-brush-color) 'solid) (send the-brush-list find-or-create-brush (dark-brush-color) 'solid)
(send the-brush-list find-or-create-brush (light-brush-color) 'solid))) (send the-brush-list find-or-create-brush (light-brush-color) 'solid)
(make-object color% dark-label-color)
(make-object color% light-label-color)
0 0
label))
(and new? snip))) (and new? snip)))
;; make-snip : (union #f (is-a?/c graph-snip<%>)) ;; make-snip : (union #f (is-a?/c graph-snip<%>))

54
collects/reduction-semantics/reduction-semantics.ss
View File

@ -13,15 +13,23 @@ incompatible changes to be done:
(lib "etc.ss")) (lib "etc.ss"))
(require-for-syntax (lib "list.ss")) (require-for-syntax (lib "list.ss"))
;; type red = (make-red compiled-pat ((listof (cons sym tst) (union string #f)) -> any)
(define-struct red (contractum reduct name))
(provide reduction (provide reduction
reduction/name
reduction/context reduction/context
reduction/context/name
language language
plug plug
compiled-lang? compiled-lang?
red? red?
term term
term-let term-let
none?) none?
(rename red-name reduction->name))
(provide match-pattern (provide match-pattern
compile-pattern compile-pattern
@ -33,6 +41,8 @@ incompatible changes to be done:
(provide/contract (provide/contract
(language->predicate (compiled-lang? symbol? . -> . (any/c . -> . boolean?))) (language->predicate (compiled-lang? symbol? . -> . (any/c . -> . boolean?)))
(reduce ((listof (lambda (x) (red? x))) any/c . -> . (listof any/c))) (reduce ((listof (lambda (x) (red? x))) any/c . -> . (listof any/c)))
(reduce/tag-with-reduction ((listof (lambda (x) (red? x))) any/c . -> . (listof any/c)))
(give-name ((λ (x) (red? x)) string? . -> . red?))
(variable-not-in (any/c symbol? . -> . symbol?)) (variable-not-in (any/c symbol? . -> . symbol?))
(compatible-closure ((lambda (x) (red? x)) (compatible-closure ((lambda (x) (red? x))
compiled-lang? compiled-lang?
@ -46,12 +56,14 @@ incompatible changes to be done:
(lambda (x) (red? x))))) (lambda (x) (red? x)))))
;; type red = (make-red compiled-pat ((listof (cons sym tst)) -> any)
(define-struct red (contractum reduct))
;; build-red : language pattern ((listof (cons sym tst)) -> any) -> red ;; give-name : red (union string #f) -> red
(define (build-red lang contractum reduct) ;; gives the reduction the given name
(make-red (compile-pattern lang contractum) reduct)) (define (give-name red name) (make-red (red-contractum red) (red-reduct red) name))
;; build-red : language pattern ((listof (cons sym tst)) -> any) (union string #f) -> red
(define (build-red lang contractum reduct name)
(make-red (compile-pattern lang contractum) reduct name))
(define (compatible-closure red lang nt) (define (compatible-closure red lang nt)
(context-closure red lang `(cross ,nt))) (context-closure red lang `(cross ,nt)))
@ -67,7 +79,7 @@ incompatible changes to be done:
[res ((red-reduct red) bindings)]) [res ((red-reduct red) bindings)])
(plug context res)))))) (plug context res))))))
(define-syntax-set (reduction/context reduction language) (define-syntax-set (reduction/context reduction reduction/name reduction/context/name language)
;; (reduction/context lang ctxt pattern expression ...) ;; (reduction/context lang ctxt pattern expression ...)
(define (reduction/context/proc stx) (define (reduction/context/proc stx)
@ -89,7 +101,15 @@ incompatible changes to be done:
(term context) (term context)
(begin (begin
(void) (void)
bodies ...))))))))])) bodies ...))))
#f))))]))
(define (reduction/context/name/proc stx)
(syntax-case stx ()
[(_ name-exp lang-exp ctxt pattern bodies ...)
#'(give-name (reduction/context lang-exp ctxt pattern bodies ...)
name-exp)]))
;; (reduction lang pattern expression ...) ;; (reduction lang pattern expression ...)
(define (reduction/proc stx) (define (reduction/proc stx)
@ -106,7 +126,13 @@ incompatible changes to be done:
`side-condition-rewritten `side-condition-rewritten
(lambda (bindings) (lambda (bindings)
(term-let ([name-ellipses (lookup-binding bindings 'name)] ...) (term-let ([name-ellipses (lookup-binding bindings 'name)] ...)
bodies ...))))))])) bodies ...))
#f))))]))
(define (reduction/name/proc stx)
(syntax-case stx ()
[(_ name-exp lang-exp pattern bodies ...)
#`(give-name (reduction lang-exp pattern bodies ...) name-exp)]))
(define (language/proc stx) (define (language/proc stx)
(syntax-case stx () (syntax-case stx ()
@ -236,6 +262,14 @@ incompatible changes to be done:
;; reduce : (listof red) exp -> (listof exp) ;; reduce : (listof red) exp -> (listof exp)
(define (reduce reductions exp) (define (reduce reductions exp)
(reduce/internal reductions exp (λ (red) (λ (mtch) ((red-reduct red) (mtch-bindings mtch))))))
; reduce/tag-with-reductions : (listof red) exp -> (listof (list red exp))
(define (reduce/tag-with-reduction reductions exp)
(reduce/internal reductions exp (λ (red) (λ (mtch) (list red ((red-reduct red) (mtch-bindings mtch)))))))
; reduce/internal : (listof red) exp (red -> match -> X) -> listof X
(define (reduce/internal reductions exp f)
(let loop ([reductions reductions] (let loop ([reductions reductions]
[acc null]) [acc null])
(cond (cond
@ -245,7 +279,7 @@ incompatible changes to be done:
(if mtchs (if mtchs
(loop (cdr reductions) (loop (cdr reductions)
(map/mt (map/mt
(lambda (mtch) ((red-reduct red) (mtch-bindings mtch))) (f red)
mtchs mtchs
acc)) acc))
(loop (cdr reductions) acc))))]))) (loop (cdr reductions) acc))))])))