- 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 "")
           (lib "")
  (provide stepper stepper/seed)
  (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
    (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))
      ;; all-nodes-ht : hash-table[sexp -o> (is-a/c node%)]
      (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))]))
    ;; 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
               [(or (not reds-choice)
                    (zero? (send reds-choice get-selection)))
               [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 (map (λ (x) (if x (format "[~a]" x) "≪unknown≫"))
                          (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 root set-in-path? #t)
    (let loop ([term (car seed)]
               [last-nexts #f]
               [terms (cdr seed)])
        [(null? terms) 
         (when last-nexts
           (expand (find-i term last-nexts void)))]
         (let* ([nexts (apply-reduction-relation red term)]
                [ith (find-i (car terms)
                             (λ ()
                               (error 'stepper "term ~s does not reduce to ~s"
                                      (car terms))))])
           (forward-step ith)
           (loop (car terms)
                 (cdr terms)))]))
    (send f show #t)

  (define (find-i term terms fail)
    (let loop ([i 0]
               [terms terms])
        [(null? terms) (fail)]
        [(equal? (car terms) term) i]
        [else (loop (+ i 1) (cdr terms))])))
  (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 pp))
      (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%
                      [pp pp]
                      [term term]
                      [red red]
                      [change-path change-path]
                      [all-nodes-ht all-nodes-ht]
                      [parent this]))])
            [(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)
             (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 pp)
    (let* (#;[txt (new scheme:text%)]
             [txt (new text:keymap%)]
           [s (new big-snip% 
                   [pp pp]
                   [node node]
                   [editor txt]
                   [expr sexp]
                   [char-width columns])])
      (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))))