- tree diff

  - step until a particular reduction happens (or a choice point is reached)
  - break points: supply a function to traces that is a predicate on terms, indicating if
    this one is one where the -> button should stop.


(module stepper mzscheme
  (require (lib "")
           (lib "" "mred")
           (lib "")
           (lib "" "framework")
           (lib "")
           (lib "" "mrlib")
           (lib "")
  (provide stepper)
  (define columns 40)
  (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)
      [(andmap (λ (x) (send normal-control-font screen-glyph-exists? x #t))
               (string->list candidate))
  ;; initial-button-label is just used to give some space to the buttons on non-mac platforms
  (define initial-button-label (pick-label "↩→↕" "<->-"))
  (define forward-label (pick-label "→" "->"))
  (define updown-label (pick-label "↕" "^"))
  (define back-label (pick-label "↩" "<-"))
  (define (stepper lang red term)
    ;; all-nodes-ht : hash-table[sexp -o> (is-a/c node%)]
    (define all-nodes-ht (make-hash-table 'equal))
    (define root (new node% 
                      [all-nodes-ht all-nodes-ht]
                      [term term]
                      [red red]
                      [change-path (λ (new-node) (change-path new-node))]))
    ;; path : (listof (listof (is-a/c node%))
    ;; the currently visible columns in the pasteboard
    (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))
    (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])
              [(= n (length last-column)) 
               (send bp change-children
                     (λ (l)
                       (filter (λ (p) (not (memq p children))) l)))
              [(null? children)
               (new button-object% 
                    [parent bp]
                    [n n])
               (loop children
                     (+ n 1))]
               (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))
          (for-each (λ (node button-object)
                        [(not (null? (send node get-cycle)))
                         (send button-object step-goes-back #t)
                         (send button-object enable-step #f)]
                         (send button-object step-goes-back #f)
                         (send button-object enable-step (not (null? (send node get-successors))))]))
    (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)
                                      (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? 
        (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)])
          [(not (null? (send click-target get-cycle)))
           (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))
             (set-car! last-pr (list click-target))
             (set-cdr! last-pr new-path-tail)
    ;; iterate-until-done : node -> (listof (listof node))
    ;; iterates forward in the path until a choice point is reached
    ;; or until we hit a stopping point. return the new tail of the path
    (define (iterate-until-done click-target)
      (let ([looking-for
               [(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
            [(zero? cutoff) (reverse new-nodes)]
             (let ([new-children (begin (send next-node force)
                                        (send next-node get-children))])
                 [(null? new-children)
                  (reverse new-nodes)]
                 [(null? (cdr new-children))
                    [(send (car new-children) in-cycle?)
                     (reverse (cons new-children new-nodes))]
                    [(equal? (find-reduction-label next-node (car new-children))
                     (reverse (cons new-children new-nodes))]
                     (loop (car new-children)
                           (cons new-children new-nodes)
                           (- cutoff 1))])]
                  (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))
    (define (moved left top right bottom)
      (let ([bx (box 0)])
        (let loop ([path path])
            [(null? path) (void)]
             (let* ([path-ele (car path)]
                    [snip (send (car path-ele) get-big-snip)]
                     (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?))
             (loop (cdr path))]))))
    (define (get-path-to-root node)
      (let loop ([node node]
                 [acc null])
        (let ([parents (send node get-parents)])
            [(null? parents) (cons (list node) acc)]
            [node (loop (car parents) 
                        (cons (list node) acc))]))))
    (define (change-path new-node)
        [(ormap (λ (l) (memq new-node l)) path)
         ;; if this node is in the current path, just move the view
         (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))))]
         (let ([new-path (get-path-to-root new-node)])
           (let loop ([new-path new-path]
                      [path path])
               [(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))
                (for-each (λ (old-ele) (for-each (λ (x) (send x set-in-path? #t)) old-ele))
                (loop (cdr new-path) (cdr path))]))
           (set! path new-path)
      (update-highlight-to-node-and-parent new-node))
    (define (update-everything)
      (send pb begin-edit-sequence)
      (send pb end-edit-sequence)
    (define (update-highlight-to-end)
      (let-values ([(one-col-before last-column)
                    (let loop ([path path]
                               [one-before #f]
                               [last-one #f])
                        [(null? path) (values one-before last-one)]
                        [else (loop (cdr path)
                                    (car path))]))])
        (when (and one-col-before
                   (= 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)]
              (ormap (λ (x) (and (memq x all-parents) x))
                     (apply append path))])
        (when visible-parent
          (set-highlight visible-parent node))))
    (define (set-highlight parent child)
       (λ (col)
         (for-each (λ (node) (send (send node get-big-snip) clear-diffs))
      (let-values ([(to-color1 to-color2) 
                     (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)
      (when red-name-message
        (let ([label (find-reduction-label parent child)])
            [(null? label) (void)]
            [(null? (cdr label))
             (send red-name-message set-label (car label))]
              (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)])
                 [(null? children) #f]
                  (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)) 
      (send zoom-out-pb refresh-tree root))
    ;; makes the last column visible
    (define (pb-last-column-visible)
       (λ (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)))
                     (unbox w)
                     (unbox h)
       (car (last-pair path))))
    (hash-table-put! all-nodes-ht term root)
    (send f show #t)
    (send root set-in-path? #t)

  (define node%
    (class object%
      (init-field term 
      (init [parent #f])
      (define parents (if parent 
                          (list parent)
      ;; cycle : (listof node)
      ;; the nodes that have the same term as this one, due to a cycle in the reduction graph
      (define cycle '())
      (define children #f)
      (define big-snip (mk-big-snip term this))
      (define dot-snip (new dot-snip% [node this]))
      (define in-path? #f)
      (define visible? #f)
      (define successors #f)

      ;; #f => uninited, else
      ;; (listof (listof string))
      ;; one list element for each successor, one nested list element for each reduction that applied (typically 1)
      (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 '())))))
            (let ([merged-names/succs
                   (let loop ([succs (map cadr names/succs)])
                       [(null? succs) null]
                        (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)))))
      (define/public (get-successor-names)
        (get-successors) ;; force the variables to be defined
      (define/public (move-path)
        (change-path this))
      (define/public (set-in-path? p?)
        (set! in-path? p?)
      (define/public (set-visible? v?)
        (set! visible? v?)
      (define/private (update-color)
        (send dot-snip set-color 
                [(and visible? in-path? (not (null? cycle)))
                [(not (null? cycle))
                [(and visible? in-path?)
      (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)]
               (λ ()
                 (new node% 
                      [term term]
                      [red red]
                      [change-path change-path]
                      [all-nodes-ht all-nodes-ht]
                      [parent this]))])
            [(and already-there
                  (is-parent? already-there))
             (let ([n (mk-child-node)])
               (send n add-cycle already-there)
               (send already-there add-cycle n)
             (send already-there add-parent this)
             (let ([child-node (mk-child-node)])
               (hash-table-put! all-nodes-ht term child-node)
        (define/private (is-parent? node)
          (let loop ([parents (get-parents)])
            (ormap (λ (p)
                     (or (eq? p node)
                         (loop (send p get-parents))))
      (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)])
                [(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)]
              (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))]
                  (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)) 
                      [(null? nodes) (void)]
                       (let* ([node (car nodes)]
                              [dot-snip (send node get-dot-snip)])
                         (insert dot-snip (* n dot-spacing) y)   ;; in case the snip's been inserted already
                         (move-to dot-snip (* n dot-spacing) y)  ;; also do the move to
                         (loop (cdr nodes) (+ y dot-spacing)))])))
                (loop (+ n 1)))))))
      (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%))
      (inherit set-snipclass set-flags get-flags)
      (set-flags (cons 'handles-events (get-flags)))
      (set-snipclass dot-snipclass)))
  (define dot-snipclass
     (class snip-class%
       (define/override (read f)
         (new dot-snip%))
  (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))
  (define (mk-big-snip sexp node)
    (let* (#;[txt (new scheme:text%)]
             [txt (new text:standard-style-list%)]
           [s (new big-snip% 
                   [node node]
                   [editor txt]
                   [expr sexp]
                   [char-width columns]
                   [pp default-pretty-printer])])
      (send txt set-autowrap-bitmap #f)
      #;(send txt freeze-colorer)
      (send s format-expr)
  (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)
        (inner (void) on-width-changed w))
      (define/public (highlight-diffs to-color)
        (set! clear-thunks
               (λ (p) (send (get-editor) highlight-range
                            (car p)
                            (cdr p)
                            (send the-color-database find-color "NavajoWhite")))
      (define/public (clear-diffs)
        (for-each (λ (t) (t)) clear-thunks)
        (set! clear-thunks null))
  (define columnar-pasteboard% 
    (class (resizing-pasteboard-mixin pasteboard%)
      (init-field moved)
      (define current-columns '())
      (inherit insert remove find-snip)
      ;; strange to think that this is the way to catch
      ;; different snips becoming visible in the editor, but oh well.
      (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])
            [(and (null? current-columns)
                  (null? new-columns))
            [(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))]
             (insert/remove current-columns new-columns)]))
        (set! current-columns orig-new-columns)
      ;; insert/remove : (listof (listof snip)) (listof (listof snip)) -> void
      (define/private (insert/remove to-remove to-insert)
        (let ([flat-to-remove (apply append to-remove)]
              [flat-to-insert (apply append to-insert)])
           (λ (x) (unless (memq x flat-to-insert)
                    (remove x)))
          (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])
                [(null? columns) (void)]
                 (let* ([column (car columns)]
                        [base-space (quotient h (length column))]
                         (let loop ([snips column]
                                    [extra-space (modulo h (length column))]
                                    [y 0]
                                    [widest 0])
                             [(null? snips) widest]
                              (let* ([snip (car snips)]
                                     [sw (get-snip-width snip)]
                                     [h (+ base-space
                                           (if (zero? extra-space)
                                (move-to snip x y)
                                (resize snip sw h)
                                (loop (cdr snips)
                                      (if (zero? extra-space)
                                          (- 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))))