(module stepper mzscheme
(require (lib "pretty.ss")
(lib "mred.ss" "mred")
(lib "class.ss")
(lib "framework.ss" "framework")
(lib "list.ss")
(lib "graph.ss" "mrlib")
(lib "contract.ss")
(lib "etc.ss")
"sexp-diffs.ss"
"size-snip.ss"
"reduction-semantics.ss")
(provide stepper stepper/seed)
(define dot-spacing 20)
(define dot-size 10)
(define initial-color "white")
(define in-path-color "orchid")
(define visible-color "purple")
(define cycle-color "yellow")
(define visible-cycle-color "gold")
(define (pick-label candidate fallback)
(cond
[(andmap (λ (x) (send normal-control-font screen-glyph-exists? x #t))
(string->list candidate))
candidate]
[else
fallback]))
(define initial-button-label (pick-label "↩→↕" "<->-"))
(define forward-label (pick-label "→" "->"))
(define updown-label (pick-label "↕" "^"))
(define back-label (pick-label "↩" "<-"))
(define stepper
(opt-lambda (lang red term [pp default-pretty-printer])
(stepper/seed lang red (list term) pp)))
(define stepper/seed
(opt-lambda (lang red seed [pp default-pretty-printer])
(define term (car seed))
(define all-nodes-ht (make-hash-table 'equal))
(define root (new node%
[pp pp]
[all-nodes-ht all-nodes-ht]
[term term]
[red red]
[change-path (λ (new-node) (change-path new-node))]
[init-cw (initial-char-width)]))
(define path (list (list root)))
(define f (new frame%
[label "PLT Redex Stepper"]
[width 700]
[height 450]))
(define dp (new vertical-panel% [parent f]))
(define upper-hp (new horizontal-panel% [parent dp]))
(define lower-hp (new horizontal-panel% [alignment '(center center)] [parent f] [stretchable-height #f]))
(define pb (new columnar-pasteboard%
[shrink-down? #f]
[moved (λ (a b c d)
(when (procedure? moved)
(moved a b c d)))]))
(define ec (new forward-size-editor-canvas% [parent upper-hp] [editor pb] [style '(no-vscroll)]))
(define bp-outer (new vertical-panel% [parent upper-hp] [stretchable-width #f]))
(define bp (new vertical-panel% [parent bp-outer] [stretchable-width #f]))
(define bp-spacer (new grow-box-spacer-pane% [parent bp-outer]))
(define zoom-out-pb (new zoom-out-pasteboard%))
(define zoom-out-ec (new editor-canvas%
[stretchable-height #t]
[parent lower-hp]
[style '(hide-vscroll)]
[editor zoom-out-pb]))
(define choice-vp (new vertical-panel% [alignment '(center center)] [parent lower-hp] [stretchable-width #f]))
(define reduction-names (reduction-relation->rule-names red))
(define reds-choice
(and (not (null? reduction-names))
(new choice%
[parent choice-vp]
[font small-control-font]
[label #f]
[choices (cons "Single Step"
(map (λ (x) (format "Reduce until ~a" x))
reduction-names))])))
(define red-name-message
(and (not (null? (reduction-relation->rule-names red)))
(new message%
[parent choice-vp]
[stretchable-width #t]
[font small-control-font]
[label ""])))
(define stupid-internal-definition-syntax1 (new grow-box-spacer-pane% [parent lower-hp]))
(define (update-buttons)
(let ([last-column (car (last-pair path))])
(let ([last-column last-column])
(let loop ([children (send bp get-children)]
[n 0])
(cond
[(= n (length last-column))
(send bp change-children
(λ (l)
(filter (λ (p) (not (memq p children))) l)))
(void)]
[(null? children)
(new button-object%
[parent bp]
[n n])
(loop children
(+ n 1))]
[else
(loop (cdr children)
(+ n 1))])))
(let ([button-objects (send bp get-children)])
(if (null? (cdr button-objects))
(send (car button-objects) hide-vertical)
(for-each (λ (x) (send x show-vertical))
button-objects))
(for-each (λ (node button-object)
(cond
[(not (null? (send node get-cycle)))
(send button-object step-goes-back #t)
(send button-object enable-step #f)]
[else
(send button-object step-goes-back #f)
(send button-object enable-step (not (null? (send node get-successors))))]))
last-column
button-objects))))
(define button-object%
(class vertical-panel%
(init-field n)
(super-new [style '(border)]
[alignment '(left center)])
(inherit change-children)
(define/public (hide-vertical)
(change-children (λ (x) (remq expand-button x))))
(define/public (show-vertical)
(change-children (λ (x) (if (memq expand-button x)
x
(append x (list expand-button))))))
(define/public (enable-step on?)
(send step-button enable on?))
(define/public (step-goes-back back?)
(send step-button set-label
(if back?
back-label
forward-label)))
(define step-button
(new button%
[label initial-button-label]
[callback (λ (x y) (forward-step n))]
[parent this]))
(define expand-button
(new button%
[label initial-button-label]
[callback (λ (x y) (expand n))]
[parent this]))
(send step-button set-label forward-label)
(send expand-button set-label updown-label)))
(define (forward-step n)
(let* ([last-pr (last-pair path)]
[last-column (car last-pr)]
[click-target (list-ref last-column n)])
(cond
[(not (null? (send click-target get-cycle)))
(void)]
[else
(let ([new-path-tail (iterate-until-done click-target)])
(for-each (λ (x) (send x set-in-path? (eq? x click-target))) last-column)
(for-each (λ (new-children)
(for-each (λ (x) (send x set-in-path? #t)) new-children))
new-path-tail)
(set-car! last-pr (list click-target))
(set-cdr! last-pr new-path-tail)
(update-everything)
(update-highlight-to-end))])))
(define (iterate-until-done click-target)
(let ([looking-for
(cond
[(or (not reds-choice)
(zero? (send reds-choice get-selection)))
#f]
[else (list-ref reduction-names (- (send reds-choice get-selection) 1))])])
(let loop ([next-node click-target]
[new-nodes (list)]
[cutoff (if looking-for
100
1)])
(cond
[(zero? cutoff) (reverse new-nodes)]
[else
(let ([new-children (begin (send next-node force)
(send next-node get-children))])
(cond
[(null? new-children)
(reverse new-nodes)]
[(null? (cdr new-children))
(cond
[(send (car new-children) in-cycle?)
(reverse (cons new-children new-nodes))]
[(equal? (find-reduction-label next-node (car new-children))
looking-for)
(reverse (cons new-children new-nodes))]
[else
(loop (car new-children)
(cons new-children new-nodes)
(- cutoff 1))])]
[else
(reverse (cons new-children new-nodes))]))]))))
(define (expand n)
(let* ([last-pr (last-pair path)]
[last-column (car last-pr)]
[survivor (list-ref last-column n)])
(for-each (λ (x) (send x set-in-path? (eq? x survivor))) last-column)
(set-car! last-pr (list survivor))
(update-everything)
(update-highlight-to-end)))
(define (moved left top right bottom)
(let ([bx (box 0)])
(let loop ([path path])
(cond
[(null? path) (void)]
[else
(let* ([path-ele (car path)]
[snip (send (car path-ele) get-big-snip)]
[visible?
(or (begin (send pb get-snip-location snip bx #f #f)
(<= left (unbox bx) right))
(begin (send pb get-snip-location snip bx #f #t)
(<= left (unbox bx) right)))])
(for-each (λ (node) (send node set-visible? visible?))
path-ele))
(loop (cdr path))]))))
(define (get-path-to-root node)
(let loop ([node node]
[acc null])
(let ([parents (send node get-parents)])
(cond
[(null? parents) (cons (list node) acc)]
[node (loop (car parents)
(cons (list node) acc))]))))
(define (change-path new-node)
(cond
[(ormap (λ (l) (memq new-node l)) path)
(let* ([snip (send new-node get-big-snip)]
[br (box 0)])
(send pb get-snip-location snip br #f #t)
(let ([bw (box 0)]
[bh (box 0)])
(send (send (send ec get-editor) get-admin) get-view #f #f bw bh)
(let* ([x (max 0 (- (unbox br) (unbox bw)))])
(send ec scroll-to x 0.0 (- (unbox bw) 4) (- (unbox bh) 1) #t 'end))))]
[else
(let ([new-path (get-path-to-root new-node)])
(let loop ([new-path new-path]
[path path])
(cond
[(or (null? path)
(null? new-path)
(not (equal? (car path) (car new-path))))
(for-each (λ (old-ele) (for-each (λ (x) (send x set-in-path? #f)) old-ele))
path)
(for-each (λ (old-ele) (for-each (λ (x) (send x set-in-path? #t)) old-ele))
new-path)]
[else
(loop (cdr new-path) (cdr path))]))
(set! path new-path)
(update-everything))])
(update-highlight-to-node-and-parent new-node))
(define (update-everything)
(send pb begin-edit-sequence)
(pb-change-columns)
(pb-last-column-visible)
(send pb end-edit-sequence)
(update-buttons))
(define (update-highlight-to-end)
(let-values ([(one-col-before last-column)
(let loop ([path path]
[one-before #f]
[last-one #f])
(cond
[(null? path) (values one-before last-one)]
[else (loop (cdr path)
last-one
(car path))]))])
(when (and one-col-before
last-column
(= 1 (length one-col-before))
(= 1 (length last-column)))
(set-highlight (car one-col-before)
(car last-column)))))
(define (update-highlight-to-node-and-parent node)
(let* ([all-parents (send node get-parents)]
[visible-parent
(ormap (λ (x) (and (memq x all-parents) x))
(apply append path))])
(when visible-parent
(set-highlight visible-parent node))))
(define (set-highlight parent child)
(for-each
(λ (col)
(for-each (λ (node) (send (send node get-big-snip) clear-diffs))
col))
path)
(let-values ([(to-color1 to-color2)
(find-differences
(send parent get-term)
(send child get-term)
(send (send parent get-big-snip) get-char-width)
(send (send child get-big-snip) get-char-width))])
(send (send parent get-big-snip) highlight-diffs to-color1)
(send (send child get-big-snip) highlight-diffs to-color2)
(void))
(when red-name-message
(let ([label (map (λ (x) (if x (format "[~a]" x) "≪unknown≫"))
(find-reduction-label parent child))])
(cond
[(null? label) (void)]
[(null? (cdr label))
(send red-name-message set-label (car label))]
[else
(apply
string-append
(car label)
(map (λ (x) (format " and ~a" x))
(cdr label)))]))))
(define (find-reduction-label parent child)
(let ([children (send parent get-children)])
(and children
(let loop ([children children]
[red-names (send parent get-successor-names)])
(cond
[(null? children) #f]
[else
(if (eq? (car children) child)
(car red-names)
(loop (cdr children)
(cdr red-names)))])))))
(define (pb-change-columns)
(send pb change-columns (map (λ (l) (map (λ (x) (send x get-big-snip)) l))
path))
(send zoom-out-pb refresh-tree root))
(define (pb-last-column-visible)
(for-each
(λ (x)
(let ([admin (send pb get-admin)])
(when admin
(let ([w (box 0)]
[h (box 0)]
[sr (box 0)]
[s (send x get-big-snip)])
(send admin get-view #f #f w h)
(send pb get-snip-location s #f sr #t)
'(send ec scroll-to
(max 0 (- (unbox sr) (unbox w)))
0
(unbox w)
(unbox h)
#t)))))
(car (last-pair path))))
(hash-table-put! all-nodes-ht term root)
(send root set-in-path? #t)
(let loop ([term (car seed)]
[last-nexts #f]
[terms (cdr seed)])
(when last-nexts
(expand (find-i term last-nexts void)))
(cond
[(null? terms) (void)]
[else
(let* ([nexts (apply-reduction-relation red term)]
[ith (find-i (car terms)
nexts
(λ ()
(error 'stepper "term ~s does not reduce to ~s"
term
(car terms))))])
(forward-step 0)
(loop (car terms)
nexts
(cdr terms)))]))
(send f show #t)
(pb-change-columns)
(update-buttons)))
(define (find-i term terms fail)
(let loop ([i 0]
[terms terms])
(cond
[(null? terms) (fail)]
[(equal? (car terms) term) i]
[else (loop (+ i 1) (cdr terms))])))
(define node%
(class object%
(init-field term
red
change-path
all-nodes-ht
pp
init-cw)
(init [parent #f])
(define parents (if parent
(list parent)
'()))
(define cycle '())
(define children #f)
(define big-snip (mk-big-snip term this pp init-cw))
(define dot-snip (new dot-snip% [node this]))
(define in-path? #f)
(define visible? #f)
(define successors #f)
(define successor-names #f)
(define/public (get-successors)
(unless successors
(let ([names/succs (apply-reduction-relation/tag-with-names red term)]
[ht (make-hash-table 'equal)])
(for-each (λ (name/succ)
(let ([name (car name/succ)]
[succ (cadr name/succ)])
(hash-table-put! ht succ (cons name (hash-table-get ht succ '())))))
names/succs)
(let ([merged-names/succs
(let loop ([succs (map cadr names/succs)])
(cond
[(null? succs) null]
[else
(let ([succ (car succs)])
(if (hash-table-get ht succ)
(cons (begin0 (list (hash-table-get ht succ) succ)
(hash-table-put! ht succ #f))
(loop (cdr succs)))
(loop (cdr succs))))]))])
(set! successor-names (map car merged-names/succs))
(set! successors (map cadr merged-names/succs)))))
successors)
(define/public (get-successor-names)
(get-successors) successor-names)
(define/public (move-path)
(change-path this))
(define/public (set-in-path? p?)
(set! in-path? p?)
(update-color))
(define/public (set-visible? v?)
(set! visible? v?)
(update-color))
(define/private (update-color)
(send dot-snip set-color
(cond
[(and visible? in-path? (not (null? cycle)))
visible-cycle-color]
[(not (null? cycle))
cycle-color]
[(and visible? in-path?)
visible-color]
[in-path?
in-path-color]
[else
initial-color])))
(define/public (get-cycle) cycle)
(define/public (add-cycle c) (set! cycle (cons c (remq c cycle))))
(define/public (in-cycle?) (not (null? cycle)))
(define/public (get-term) term)
(define/public (get-big-snip) big-snip)
(define/public (get-dot-snip) dot-snip)
(define/public (get-parents) parents)
(define/public (add-parent p)
(add-links (send p get-dot-snip) dot-snip)
(set! parents (cons p parents)))
(define/public (get-children) (or children '()))
(define/public (force)
(unless children
(set! children
(map (λ (x) (make-child x)) (get-successors)))))
(define/private (make-child term)
(let ([already-there (hash-table-get all-nodes-ht term #f)]
[mk-child-node
(λ ()
(new node%
[pp pp]
[term term]
[red red]
[change-path change-path]
[all-nodes-ht all-nodes-ht]
[parent this]
[init-cw init-cw]))])
(cond
[(and already-there
(or (eq? this already-there)
(is-parent? already-there)))
(let ([n (mk-child-node)])
(send n add-cycle already-there)
(send already-there add-cycle n)
n)]
[already-there
(send already-there add-parent this)
already-there]
[else
(let ([child-node (mk-child-node)])
(hash-table-put! all-nodes-ht term child-node)
child-node)])))
(define/private (is-parent? node)
(let loop ([parents (get-parents)])
(ormap (λ (p)
(or (eq? p node)
(loop (send p get-parents))))
parents)))
(super-new)
(when cycle
(send dot-snip set-color cycle-color))
(when parent
(add-links (send parent get-dot-snip) dot-snip))))
(define zoom-out-pasteboard%
(class (graph-pasteboard-mixin pasteboard%)
(inherit insert move-to get-canvas get-admin)
(inherit find-snip set-caret-owner global-to-local)
(define/override (on-event evt)
(when (send evt button-down?)
(let ([x (box (send evt get-x))]
[y (box (send evt get-y))])
(global-to-local x y)
(let ([s (find-snip (unbox x) (unbox y))])
(when s
(set-caret-owner s 'immediate)))))
(super on-event evt))
(define/public (refresh-tree root)
(let ([level-ht (make-hash-table)]
[node-to-level-ht (make-hash-table)]
[max-n 0])
(let loop ([tree root]
[n 0])
(let ([old-level (hash-table-get node-to-level-ht tree #f)])
(cond
[(not old-level)
(hash-table-put! node-to-level-ht tree n)
(hash-table-put! level-ht n (cons tree (hash-table-get level-ht n '())))]
[(< old-level n)
(hash-table-put! level-ht old-level (remq tree (hash-table-get level-ht old-level)))
(hash-table-put! level-ht n (cons tree (hash-table-get level-ht n '())))
(hash-table-put! node-to-level-ht tree n)]
[else
(void)])
(set! max-n (max n max-n))
(for-each (λ (x) (loop x (+ n 1))) (send tree get-children))))
(let* ([tallest-column (apply max (hash-table-map level-ht (λ (x y) (length y))))]
[canvas (get-canvas)]
[_1 (send canvas min-client-height (* tallest-column dot-spacing))]
[vertical-space
(let-values ([(w h) (send canvas get-client-size)]) h)])
(let loop ([n 0])
(when (<= n max-n)
(let ([nodes (reverse (hash-table-get level-ht n))])
(let loop ([nodes nodes]
[y (/ (- vertical-space
(* (length nodes) dot-spacing))
2)])
(cond
[(null? nodes) (void)]
[else
(let* ([node (car nodes)]
[dot-snip (send node get-dot-snip)])
(insert dot-snip (* n dot-spacing) y) (move-to dot-snip (* n dot-spacing) y) (loop (cdr nodes) (+ y dot-spacing)))])))
(loop (+ n 1)))))))
(super-new)
(inherit set-draw-arrow-heads?)
(set-draw-arrow-heads? #f)))
(define (set-box/f b v) (when (box? b) (set-box! b v)))
(define dot-snip%
(class (graph-snip-mixin snip%)
(init-field node)
(inherit get-admin)
(define color initial-color)
(define/public (set-color c)
(unless (equal? color c)
(set! color c)
(let ([admin (get-admin)])
(when admin
(send admin needs-update this 0 0 dot-size dot-size)))))
(define/override (get-extent dc x y wb hb descentb spaceb lspaceb rspaceb)
(set-box/f wb dot-size)
(set-box/f hb dot-size)
(set-box/f descentb 0)
(set-box/f spaceb 0)
(set-box/f lspaceb 0)
(set-box/f rspaceb 0))
(define/override (draw dc x y left top right bottom dx dy draw-caret)
(let ([smoothing (send dc get-smoothing)]
[brush (send dc get-brush)])
(send dc set-smoothing 'aligned)
(send dc set-brush color 'solid)
(send dc draw-ellipse x y dot-size dot-size)
(send dc set-brush brush)
(send dc set-smoothing smoothing)))
(define/override (on-event dc x y editorx editory evt)
(when (send evt button-up?)
(send node move-path)))
(define/override (copy) (new snip%))
(super-new)
(inherit set-snipclass set-flags get-flags)
(set-flags (cons 'handles-events (get-flags)))
(set-snipclass dot-snipclass)))
(define dot-snipclass
(new
(class snip-class%
(define/override (read f)
(new dot-snip%))
(super-new))))
(send dot-snipclass set-classname "plt-redex:dot")
(send dot-snipclass set-version 1)
(send (get-the-snip-class-list) add dot-snipclass)
(define forward-size-editor-canvas%
(class canvas:color%
(inherit get-editor)
(define/override (on-size w h)
(send (get-editor) update-heights))
(super-new)))
(define (mk-big-snip sexp node pp init-cw)
(let* ([txt (new scheme:text%)]
[txt (new text:keymap%)]
[s (new big-snip%
[pp pp]
[node node]
[editor txt]
[expr sexp]
[char-width init-cw])])
(send txt set-autowrap-bitmap #f)
(send txt freeze-colorer)
(send s format-expr)
s))
(define big-snip%
(class size-editor-snip%
(inherit get-editor)
(init-field node)
(define/public (get-node) node)
(define clear-thunks '())
(define/augment (on-width-changed w)
(clear-diffs)
(inner (void) on-width-changed w))
(define/public (highlight-diffs to-color)
(clear-diffs)
(set! clear-thunks
(map
(λ (p) (send (get-editor) highlight-range
(car p)
(cdr p)
(send the-color-database find-color "NavajoWhite")))
to-color)))
(define/public (clear-diffs)
(for-each (λ (t) (t)) clear-thunks)
(set! clear-thunks null))
(super-new)))
(define columnar-pasteboard%
(class (resizing-pasteboard-mixin pasteboard%)
(init-field moved)
(define current-columns '())
(inherit insert remove find-snip)
(define/override (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)
(unless before?
(let ([admin (get-admin)])
(when admin
(let ([bx (box 0)]
[by (box 0)]
[bw (box 0)]
[bh (box 0)])
(send admin get-view bx by bw bh)
(moved (unbox bx)
(unbox by)
(+ (unbox bx) (unbox bw))
(+ (unbox by) (unbox bh))))))))
(define/public (change-columns orig-new-columns)
(let loop ([current-columns current-columns]
[new-columns orig-new-columns])
(cond
[(and (null? current-columns)
(null? new-columns))
(void)]
[(null? new-columns)
(insert/remove current-columns '())]
[(null? current-columns)
(insert/remove '() new-columns)]
[(equal? (car current-columns)
(car new-columns))
(loop (cdr current-columns)
(cdr new-columns))]
[else
(insert/remove current-columns new-columns)]))
(set! current-columns orig-new-columns)
(update-heights))
(define/private (insert/remove to-remove to-insert)
(let ([flat-to-remove (apply append to-remove)]
[flat-to-insert (apply append to-insert)])
(for-each
(λ (x) (unless (memq x flat-to-insert)
(remove x)))
flat-to-remove)
(for-each (λ (x) (insert x)) flat-to-insert)))
(inherit get-admin move-to resize)
(define/public (update-heights)
(let ([admin (get-admin)])
(let-values ([(w h) (get-view-size)])
(let loop ([columns current-columns]
[x 0])
(cond
[(null? columns) (void)]
[else
(let* ([column (car columns)]
[base-space (quotient h (length column))]
[widest
(let loop ([snips column]
[extra-space (modulo h (length column))]
[y 0]
[widest 0])
(cond
[(null? snips) widest]
[else
(let* ([snip (car snips)]
[sw (get-snip-width snip)]
[h (+ base-space
(if (zero? extra-space)
0
1))])
(move-to snip x y)
(resize snip sw h)
(loop (cdr snips)
(if (zero? extra-space)
0
(- extra-space 1))
(+ y h)
(max widest sw)))]))])
(loop (cdr columns)
(+ x widest)))])))))
(inherit get-snip-location)
(define/public (get-snip-width snip)
(let ([lb (box 0)]
[rb (box 0)])
(get-snip-location snip lb #f #f)
(get-snip-location snip rb #f #t)
(- (unbox rb) (unbox lb))))
(define/private (get-view-size)
(let ([admin (get-admin)])
(if admin
(let ([wb (box 0)]
[hb (box 0)])
(send admin get-view #f #f wb hb)
(values (unbox wb) (- (unbox hb) 2)))
(values 10 10))))
(super-new))))