(module rewrite-side-conditions mzscheme
  (require (lib "list.ss"))
  (require-for-template mzscheme
                        "term.ss"
                        "matcher.ss")
  
  (provide rewrite-side-conditions
           extract-names)
  
  (define (rewrite-side-conditions what orig-stx)
    (let loop ([term orig-stx])
      (syntax-case term (side-condition)
        [(side-condition pre-pat exp)
         (with-syntax ([pat (loop (syntax pre-pat))])
           (let-values ([(names names/ellipses) (extract-names (syntax pat))])
             (with-syntax ([(name ...) names]
                           [(name/ellipses ...) names/ellipses])
               (syntax/loc term
                 (side-condition
                  pat
                  ,(lambda (bindings)
                     (term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
                               exp)))))))]
        [(terms ...)
         (map loop (syntax->list (syntax (terms ...))))]
        [else
         (when (pair? (syntax-e term))
           (let loop ([term term])
             (cond
               [(syntax? term) (loop (syntax-e term))]
               [(pair? term) (loop (cdr term))]
               [(null? term) (void)]
               [#t
                (raise-syntax-error what "dotted pairs not supported in patterns" orig-stx term)])))
         term])))
  
  (define-struct id/depth (id depth))
  
  ;; extract-names : syntax -> (values (listof syntax) (listof syntax[x | (x ...) | ((x ...) ...) | ...]))
  (define (extract-names orig-stx)
    (let* ([dups
            (let loop ([stx orig-stx]
                       [names null]
                       [depth 0])
              (syntax-case stx (name in-hole in-named-hole side-condition)
                [(name sym pat)
                 (identifier? (syntax sym))
                 (loop (syntax pat) 
                       (cons (make-id/depth (syntax sym) depth) names)
                       depth)]
                [(in-named-hole hlnm sym pat1 pat2)
                 (identifier? (syntax sym))
                 (loop (syntax pat1)
                       (loop (syntax pat2) names depth)
                       depth)]
                [(in-hole pat1 pat2)
                 (loop (syntax pat1)
                       (loop (syntax pat2) names depth)
                       depth)]
                [(side-condition pat e)
                 (loop (syntax pat) names depth)]
                [(pat ...)
                 (let i-loop ([pats (syntax->list (syntax (pat ...)))]
                              [names names])
                   (cond
                     [(null? pats) names]
                     [else 
                      (if (or (null? (cdr pats))
                              (not (identifier? (cadr pats)))
                              (not (module-identifier=? (quote-syntax ...)
                                                        (cadr pats))))
                          (i-loop (cdr pats)
                                  (loop (car pats) names depth))
                          (i-loop (cdr pats)
                                  (loop (car pats) names (+ depth 1))))]))]
                [x
                 (and (identifier? (syntax x))
                      (has-underscore? (syntax x)))
                 (cons (make-id/depth (syntax x) depth) names)]
                [else names]))]
           [no-dups (filter-duplicates dups)])
      (values (map id/depth-id no-dups)
              (map build-dots no-dups))))
  
  ;; build-dots : id/depth -> syntax[x | (x ...) | ((x ...) ...) | ...]
  (define (build-dots id/depth)
    (let loop ([depth (id/depth-depth id/depth)])
      (cond
        [(zero? depth) (id/depth-id id/depth)]
        [else (with-syntax ([rest (loop (- depth 1))]
                            [dots (quote-syntax ...)])
                (syntax (rest dots)))])))
  
  (define (has-underscore? x)
    (memq #\_ (string->list (symbol->string (syntax-e x)))))
  
  
  (define (filter-duplicates dups)
    (let loop ([dups dups])
      (cond
        [(null? dups) null]
        [else 
         (cons
          (car dups)
          (filter (lambda (x) 
                    (let ([same-id? (module-identifier=? (id/depth-id x)
                                                         (id/depth-id (car dups)))])
                      (when same-id?
                        (unless (equal? (id/depth-depth x)
                                        (id/depth-depth (car dups)))
                          (error 'reduction "found the same binder, ~s, at different depths, ~a and ~a"
                                 (syntax-object->datum (id/depth-id x))
                                 (id/depth-depth x)
                                 (id/depth-depth (car dups)))))
                      (not same-id?)))
                  (loop (cdr dups))))]))))