private/reduction-semantics.ss
(module reduction-semantics mzscheme
  (require "matcher.ss"
           "struct.ss"
           "term.ss"
           "loc-wrapper.ss"
           (lib "list.ss")
           (lib "etc.ss"))
  (require-for-syntax (lib "name.ss" "syntax")
                      "rewrite-side-conditions.ss"
                      "term-fn.ss"
                      (lib "boundmap.ss" "syntax"))

  
  (define (language-nts lang)
    (hash-table-map (compiled-lang-ht lang) (λ (x y) x)))

  (define-syntax (term-match/single stx)
    (syntax-case stx ()
      [(_ lang [pattern rhs] ...)
       (with-syntax ([(((names ...) (names/ellipses ...)) ...)
                      (map (λ (x) (let-values ([(names names/ellipses) (extract-names 'term-match/single x)])
                                    (list names names/ellipses)))
                           (syntax->list (syntax (pattern ...))))]
                     [(side-conditions-rewritten ...)
                      (map (λ (x) (rewrite-side-conditions/check-errs 'term-match x))
                           (syntax->list (syntax (pattern ...))))]
                     [(cp-x ...) (generate-temporaries #'(pattern ...))])
       #'(let ([lang-x lang])
           (let ([cp-x (compile-pattern lang-x `side-conditions-rewritten)] ...)
             (λ (exp)
               (let/ec k
                 (let ([match (match-pattern cp-x exp)])
                   (when match
                     (unless (null? (cdr match))
                       (error 'term-match "pattern ~s matched term ~e multiple ways"
                              'pattern
                              exp))
                     (k (term-let ([names/ellipses (lookup-binding (mtch-bindings (car match)) 'names)] ...)
                          rhs))))
                 ...
                 (error 'term-match "no patterns matched ~e" exp))))))]))
  
  (define-syntax (term-match stx)
    (syntax-case stx ()
      [(_ lang [pattern rhs] ...)
       (with-syntax ([(((names ...) (names/ellipses ...)) ...)
                      (map (λ (x) (let-values ([(names names/ellipses) (extract-names 'term-match x)])
                                    (list names names/ellipses)))
                           (syntax->list (syntax (pattern ...))))]
                     [(side-conditions-rewritten ...)
                      (map (λ (x) (rewrite-side-conditions/check-errs 'term-match x))
                           (syntax->list (syntax (pattern ...))))]
                     [(cp-x ...) (generate-temporaries #'(pattern ...))])
         #'(let ([lang-x lang])
             (let ([cp-x (compile-pattern lang-x `side-conditions-rewritten)] ...)
               (λ (exp)
                 (append
                  (let ([matches (match-pattern cp-x exp)])
                    (if matches
                        (map (λ (match)
                               (term-let ([names/ellipses (lookup-binding (mtch-bindings match) 'names)] ...)
                                 rhs))
                             matches)
                        '())) ...)))))]))
  
  (define-syntax (compatible-closure stx)
    (syntax-case stx ()
      [(_ red lang nt)
       (identifier? (syntax nt))
       (with-syntax ([side-conditions-rewritten (rewrite-side-conditions/check-errs 'compatible-closure (syntax (cross nt)))])
         (syntax (do-context-closure red lang `side-conditions-rewritten 'compatible-closure)))]
      [(_ red lang nt)
       (raise-syntax-error 'compatible-closure "expected a non-terminal as last argument" stx (syntax nt))]))
  
  (define-syntax (context-closure stx)
    (syntax-case stx ()
      [(_ red lang pattern)
       (with-syntax ([side-conditions-rewritten (rewrite-side-conditions/check-errs 'context-closure (syntax pattern))])
         (syntax
          (do-context-closure
           red
           lang
           `side-conditions-rewritten
           'context-closure)))]))
  
  (define (do-context-closure red lang pat name)
    (unless (reduction-relation? red)
      (error name "expected <reduction-relation> as first argument, got ~e" red))
    (unless (compiled-lang? lang)
      (error name "expected <lang> as second argument, got ~e" lang))
    (let ([cp (compile-pattern
               lang
               `(in-hole (name ctxt ,pat)
                         (name exp any)))])
      (make-reduction-relation
       lang
       (map
        (λ (f)
          (λ (main-exp exp extend acc)
            (let loop ([ms (or (match-pattern cp exp) '())]
                       [acc acc])
              (cond
                [(null? ms) acc]
                [else
                 (let* ([mtch (car ms)]
                        [bindings (mtch-bindings mtch)])
                   (loop (cdr ms)
                         (f main-exp
                            (lookup-binding bindings 'exp)
                            (λ (x) (extend (plug (lookup-binding bindings 'ctxt) x)))
                            acc)))]))))
        (reduction-relation-procs red))
       (reduction-relation-rule-names red)
       (reduction-relation-lws red))))
  
  (define (build-metafunction lang patterns rhss wrap name)
    (let ([compiled-patterns (map (λ (pat) (compile-pattern lang pat)) patterns)])
      (wrap
       (λ (exp)
         (let loop ([patterns compiled-patterns]
                    [rhss rhss]
                    [num 0])
           (cond
             [(null? patterns) (error name "no clauses matched for ~s" exp)]
             [else (let ([pattern (car patterns)]
                         [rhs (car rhss)])
                     (let ([mtchs (match-pattern pattern exp)])
                       (cond
                         [(not mtchs) (loop (cdr patterns)
                                            (cdr rhss)
                                            (+ num 1))]
                         [(not (null? (cdr mtchs)))
                          (error name "clause ~a matched ~s two different ways" num exp)]
                         [else
                          (rhs (mtch-bindings (car mtchs)))])))]))))))
  
  (define (do-test-match lang pat)
    (unless (compiled-lang? lang)
      (error 'test-match "expected first argument to be a language, got ~e" lang))
    (let ([cpat (compile-pattern lang pat)])
      (λ (exp)
        (match-pattern cpat exp))))

  (define-syntax (--> stx) (raise-syntax-error '--> "used outside of reduction-relation"))
  (define-syntax (fresh stx) (raise-syntax-error 'fresh "used outside of reduction-relation"))

  (define (apply-reduction-relation/tag-with-names p v)
    (let loop ([procs (reduction-relation-procs p)]
               [acc '()])
      (cond
        [(null? procs) acc]
        [else 
         (loop (cdr procs)
               ((car procs) v v values acc))])))
  
  (define (apply-reduction-relation p v) (map cadr (apply-reduction-relation/tag-with-names p v)))

  (define-for-syntax (extract-pattern-binds lhs)
    (let loop ([lhs lhs])
      (syntax-case* lhs (name) (lambda (a b) (eq? (syntax-e a) (syntax-e b)))
        [(name id expr)
         (cons (cons #'id #'expr) (loop #'expr))]
        ;; FIXME: should follow the grammar of patterns!
        [(a . b)
         (append (loop #'a) (loop #'b))]
        [_else null])))

  (define-syntax-set (-reduction-relation)
    (define (-reduction-relation/proc stx)
      (syntax-case stx ()
        [(_ lang args ...)
         (with-syntax ([(rules ...) (before-where (syntax (args ...)))]
                       [(shortcuts ...) (after-where (syntax (args ...)))])
           (with-syntax ([(lws ...) (map rule->lws (syntax->list #'(rules ...)))])
             (reduction-relation/helper 
              stx
              (syntax lang)
              (syntax->list (syntax (rules ...)))
              (syntax->list (syntax (shortcuts ...)))
              #'(list lws ...))))]))
    
    (define (before-where stx)
      (let loop ([lst (syntax->list stx)])
        (cond
          [(null? lst) null]
          [else
           (let ([fst (car lst)])
             (syntax-case* (car lst) (where) (λ (x y) (eq? (syntax-e x) (syntax-e y)))
               [where null]
               [else (cons (car lst) (loop (cdr lst)))]))])))
    
    (define (after-where stx)
      (let loop ([lst (syntax->list stx)])
        (cond
          [(null? lst) null]
          [else
           (let ([fst (car lst)])
             (syntax-case* (car lst) (where) (λ (x y) (eq? (syntax-e x) (syntax-e y)))
               [where (cdr lst)]
               [else (loop (cdr lst))]))])))
    
    (define (rule->lws rule)
      (syntax-case rule ()
        [(arrow lhs rhs stuff ...)
         (let-values ([(label scs fvars)
                       (let loop ([stuffs (syntax->list #'(stuff ...))]
                                  [label #f]
                                  [scs null]
                                  [fvars null])
                         (cond
                           [(null? stuffs) (values label (reverse scs) (reverse fvars))]
                           [else
                            (syntax-case (car stuffs) (fresh variable-not-in)
                              [(fresh xs ...) 
                               (loop (cdr stuffs)
                                     label
                                     scs
                                     (append 
                                      (reverse (map (λ (x)
                                                      (syntax-case x ()
                                                        [x
                                                         (identifier? #'x)
                                                         #'x]
                                                        [(x whatever)
                                                         (identifier? #'x)
                                                         #'x]
                                                        [((y dots) (x dots2))
                                                         (datum->syntax-object 
                                                          #f 
                                                          `(,(syntax-object->datum #'y) ...) 
                                                          #'y)]
                                                        [((y dots) (x dots2) whatever)
                                                         (datum->syntax-object 
                                                          #f 
                                                          `(,(syntax-object->datum #'y) ...) 
                                                          #'y)]))
                                                    (syntax->list #'(xs ...))))
                                      fvars))]
                              [(side-condition sc)
                               (loop (cdr stuffs)
                                     label
                                     (cons #'sc scs)
                                     fvars)]
                              [x
                               (identifier? #'x)
                               (loop (cdr stuffs)
                                     #''x
                                     scs
                                     fvars)]
                              [x
                               (string? (syntax-e #'x))
                               (loop (cdr stuffs)
                                     #'x
                                     scs
                                     fvars)])]))])
           (with-syntax ([(scs ...) scs]
                         [(fvars ...) fvars]
                         [((bind-id . bind-pat) ...) (extract-pattern-binds #'lhs)])
             #`(make-rule-pict 'arrow
                               (to-loc-wrapper lhs)
                               (to-loc-wrapper rhs)
                               #,label
                               (list (to-loc-wrapper/sc scs) ...)
                               (list (to-loc-wrapper fvars) ...)
                               (list (cons (to-loc-wrapper bind-id)
                                           (to-loc-wrapper bind-pat))
                                     ...))))]))
  
    (define (reduction-relation/helper stx lang-exp rules shortcuts lws)
      (let ([ht (make-module-identifier-mapping)]
            [all-top-levels '()]
            [wheres (make-module-identifier-mapping)])
        (for-each (λ (shortcut)
                    (syntax-case shortcut ()
                      [((lhs-arrow lhs-from lhs-to)
                        (rhs-arrow rhs-from rhs-to))
                       (begin
                         (table-cons! wheres #'lhs-arrow #'rhs-arrow)
                         (table-cons! ht (syntax rhs-arrow) shortcut))]
                      [((a b c) d)
                       (raise-syntax-error 
                        'reduction-relation
                        "malformed shortcut, expected right-hand side to have three sub-expressions"
                        stx (syntax d))]
                      [(a b)
                       (raise-syntax-error 
                        'reduction-relation
                        "malformed shortcut, expected left-hand side to have three sub-expressions"
                        stx (syntax a))]
                      [(a b c d ...)
                       (raise-syntax-error 'reduction-relation
                                           "malformed shortcut, expected only two subparts for a shortcut definition, found an extra one"
                                           stx
                                           (syntax c))]
                      [_ (raise-syntax-error 'reduction-relation
                                             "malformed shortcut"
                                             stx shortcut)]))
                  shortcuts)
        (for-each (λ (rule)
                    (syntax-case rule ()
                      [(arrow . rst)
                       (begin
                         (set! all-top-levels (cons #'arrow all-top-levels))
                         (table-cons! ht (syntax arrow) rule))]))
                  rules)
        (unless (module-identifier-mapping-get ht (syntax -->) (λ () #f))
          (raise-syntax-error 'reduction-relation "no --> rules" stx))
        
        (for-each (λ (tl)
                    (let loop ([id tl])
                      (unless (module-identifier=? #'--> id)
                        (let ([nexts
                               (module-identifier-mapping-get
                                wheres id 
                                (λ () 
                                  (raise-syntax-error 
                                   'reduction-relation
                                   (format "the ~s relation is not defined"
                                           (syntax-object->datum id))
                                   stx
                                   id)))])
                          (for-each loop nexts)))))
                  all-top-levels)
        
        (let ([name-ht (make-hash-table)])
          (with-syntax ([lang-exp lang-exp]
                        [(top-level ...) (get-choices stx ht (syntax lang-x) (syntax -->) name-ht)]
                        [(rule-names ...) (hash-table-map name-ht (λ (k v) k))]
                        [lws lws])
            (syntax 
             (let ([lang-x lang-exp])
               (make-reduction-relation
                lang-x
                (list top-level ...)
                '(rule-names ...)
                lws)))))))
    
#|    ;; relation-tree = 
    ;;   leaf
    ;;  (make-node id[frm] pat[frm] id[to] pat[to] (listof relation-tree))
    (define-struct node (frm-id frm-pat to-id to-pat))
    (define-struct leaf (frm-pat to-pat))
  |#  
    ;; get-choices : stx[original-syntax-object] bm lang identifier ht[sym->syntax] -> (listof relation-tree)
    (define (get-choices stx bm lang id name-table)
      (reverse
       (map (λ (x) (get-tree stx bm lang x name-table))
            (module-identifier-mapping-get 
             bm id
             (λ ()
               (raise-syntax-error 'reduction-relation 
                                   (format "no rules use ~a" (syntax-object->datum id))
                                   stx 
                                   id))))))
    
    (define (get-tree stx bm lang case-stx name-table)
      (syntax-case case-stx ()
        [(arrow from to extras ...)
         (do-leaf stx 
                  lang 
                  name-table
                  (syntax from) 
                  (syntax to) 
                  (syntax->list (syntax (extras ...))))]
        [((lhs-arrow lhs-frm-id lhs-to-id) (rhs-arrow rhs-from rhs-to))
         (let-values ([(names names/ellipses) (extract-names 'reduction-relation (syntax rhs-from))])
           (with-syntax ([(names ...) names]
                         [(names/ellipses ...) names/ellipses]
                         [side-conditions-rewritten (rewrite-side-conditions/check-errs
                                                     'reduction-relation
                                                     (rewrite-node-pat (syntax-e (syntax lhs-frm-id))
                                                                       (syntax-object->datum (syntax rhs-from))))]
                         [lang lang]
                         [(child-procs ...) (get-choices stx bm lang (syntax lhs-arrow) name-table)])
             (syntax 
              (do-node-match
               lang
               'lhs-frm-id
               'lhs-to-id
               `side-conditions-rewritten
               (λ (bindings rhs-binder)
                 (term-let ([lhs-to-id rhs-binder]
                            [names/ellipses (lookup-binding bindings 'names)] ...)
                           (term rhs-to)))
               (list child-procs ...)))))]))
    
    (define (rewrite-node-pat id term)
      (let loop ([term term])
        (cond
          [(eq? id term) `(name ,id any)]
          [(pair? term) (cons (loop (car term))
                              (loop (cdr term)))]
          [else term])))

    (define (do-leaf stx lang name-table from to extras)
      (let-values ([(name fresh-vars side-conditions) (process-extras stx name-table extras)])
        (let-values ([(names names/ellipses) (extract-names 'reduction-relation from)])
          (with-syntax ([side-conditions-rewritten 
                         (rewrite-side-conditions/check-errs 
                          'reduction-relation
                          (if (null? side-conditions)
                              from
                              (with-syntax ([(sc ...) side-conditions]
                                            [from from])
                                (syntax (side-condition from (and sc ...))))))]
                        [to to]
                        [name name]
                        [lang lang]
                        [(names ...) names]
                        [(names/ellipses ...) names/ellipses]
                        [(fresh-var-clauses ...) 
                         (map (λ (fv-clause)
                                (syntax-case fv-clause ()
                                  [x
                                   (identifier? #'x)
                                   #'[x (variable-not-in main 'x)]]
                                  [(x name)
                                   (identifier? #'x)
                                   #'[x (let ([the-name (term name)])
                                          (verify-name-ok the-name)
                                          (variable-not-in main the-name))]]
                                  [((y) (x ...))
                                   #`[(y #,'...)
                                      (variables-not-in main 
                                                        (map (λ (_ignore_) 'y)
                                                             (term (x ...))))]]
                                  [((y) (x ...) names)
                                   #`[(y #,'...)
                                      (let ([the-names (term names)]
                                            [len-counter (term (x ...))])
                                        (verify-names-ok the-names len-counter)
                                        (variables-not-in main the-names))]]))
                              fresh-vars)])
            (syntax (do-leaf-match
                     lang
                     name
                     `side-conditions-rewritten
                     (λ (main bindings)
                       (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
                         ;; nested term-let's so that the bindings for the variables
                         ;; show up in the `fresh' side-conditions
                         (term-let (fresh-var-clauses ...)
                           (term to))))))))))
    
    (define (process-extras stx name-table extras)
      (let ([the-name #f]
            [the-name-stx #f]
            [fresh-vars '()]
            [side-conditions '()])
        (let loop ([extras extras])
          (cond
            [(null? extras) (values the-name fresh-vars side-conditions)]
            [else
             (syntax-case (car extras) (fresh)
               [name 
                (or (identifier? (car extras))
                    (string? (syntax-e (car extras))))
                (begin
                  (let* ([raw-name (syntax-e (car extras))]
                         [name-sym
                          (if (symbol? raw-name)
                              raw-name
                              (string->symbol raw-name))])
                    (when (hash-table-get name-table name-sym #f)
                      (raise-syntax-errors 'reduction-relation 
                                           "same name on multiple rules"
                                           stx
                                           (list (hash-table-get name-table name-sym)
                                                 (syntax name))))
                    (hash-table-put! name-table name-sym (syntax name))
                    
                    (when the-name
                      (raise-syntax-errors 'reduction-relation "expected only a single name" 
                                           stx
                                           (list the-name-stx (car extras))))
                    (set! the-name (if (symbol? raw-name)
                                       (symbol->string raw-name)
                                       raw-name))
                    (set! the-name-stx (car extras))
                    (loop (cdr extras))))]
               [(fresh var ...)
                (begin
                  (set! fresh-vars 
                        (append 
                         (map (λ (x)
                                (syntax-case x ()
                                  [x
                                   (identifier? #'x)
                                   #'x]
                                  [(x name)
                                   (identifier? #'x)
                                   #'(x name)]
                                  [((ys dots2) (xs dots1))
                                   (and (eq? (syntax-e #'dots1) (string->symbol "..."))
                                        (eq? (syntax-e #'dots2) (string->symbol "...")))
                                   #'((ys) (xs dots1))]
                                  [((ys dots2) (xs dots1) names)
                                   (and (eq? (syntax-e #'dots1) (string->symbol "..."))
                                        (eq? (syntax-e #'dots2) (string->symbol "...")))
                                   #'((ys) (xs dots1) names)]
                                  [x
                                   (raise-syntax-error 'reduction-relation 
                                                       "malformed fresh variable clause"
                                                       stx
                                                       #'x)]))
                              (syntax->list #'(var ...)))
                         fresh-vars))
                  (loop (cdr extras)))]
               [(side-condition exp ...)
                (begin 
                  (set! side-conditions
                        (append (syntax->list (syntax (exp ...))) side-conditions))
                  (loop (cdr extras)))]
               [_
                (raise-syntax-error 'reduction-relation "unknown extra" stx (car extras))])]))))

    ;; table-cons! hash-table sym any -> void
    ;; extends ht at key by `cons'ing hd onto whatever is alrady bound to key (or the empty list, if nothing is)
    (define (table-cons! ht key hd)
      (module-identifier-mapping-put! ht key (cons hd (module-identifier-mapping-get ht key (λ () '())))))
    
    (define (raise-syntax-errors sym str stx stxs)
      (raise (make-exn:fail:syntax 
              (string->immutable-string (format "~a: ~a~a" 
                                                sym 
                                                str
                                                (if (error-print-source-location)
                                                    (string-append ":" (stxs->list stxs))
                                                    "")))
              (current-continuation-marks)
              (apply list-immutable stxs))))
    
    (define (stxs->list stxs)
      (apply
       string-append
       (let loop ([stxs stxs])
         (cond
           [(null? stxs) '()]
           [else 
            (cons (format " ~s" (syntax-object->datum (car stxs)))
                  (loop (cdr stxs)))])))))
  
  (define (verify-name-ok the-name)
    (unless (symbol? the-name)
      (error 'reduction-relation "expected a single name, got ~s" the-name)))
  
  (define (verify-names-ok the-names len-counter)
    (unless (and (list? the-names)
                 (andmap symbol? the-names))
      (error 'reduction-relation
             "expected a sequence of names, got ~s"
             the-names))
    (unless (= (length len-counter)
               (length the-names))
      (error 'reduction-relation
             "expected the length of the sequence of names to be ~a, got ~s"
             (length len-counter)
             the-names)))
  
  (define (union-reduction-relations fst snd . rst)
    (let ([name-ht (make-hash-table)]
          [lst (list* fst snd rst)]
          [first-lang (reduction-relation-lang fst)])
      (for-each
       (λ (red)
         (unless (eq? first-lang (reduction-relation-lang red))
           (error 'union-reduction-relations 
                  "expected all of the reduction relations to use the same language"))
         (for-each (λ (name)
                     (when (hash-table-get name-ht name #f)
                       (error 'union-reduction-relations "multiple rules with the name ~s" name))
                     (hash-table-put! name-ht name #t))
                   (reduction-relation-rule-names red)))
       lst)
      (make-reduction-relation
       first-lang
       (reverse (apply append (map reduction-relation-procs lst)))
       (hash-table-map name-ht (λ (k v) k))
       (apply append (map reduction-relation-lws lst)))))
  
  (define (do-node-match lang lhs-frm-id lhs-to-id pat rhs-proc child-procs)
    (let ([cp (compile-pattern lang pat)])
      (λ (main-exp exp f other-matches)
        (let ([mtchs (match-pattern cp exp)])
          (if mtchs
              (let o-loop ([mtchs mtchs]
                           [acc other-matches])
                (cond
                  [(null? mtchs) acc]
                  [else
                   (let ([sub-exp (lookup-binding (mtch-bindings (car mtchs)) lhs-frm-id)])
                     (let i-loop ([child-procs child-procs]
                                  [acc acc])
                       (cond
                         [(null? child-procs) (o-loop (cdr mtchs) acc)]
                         [else (i-loop (cdr child-procs)
                                       ((car child-procs) main-exp
                                                          sub-exp
                                                          (λ (x) (f (rhs-proc (mtch-bindings (car mtchs)) x)))
                                                          acc))])))]))
              other-matches)))))
  
  (define (do-leaf-match lang name pat proc)
    (let ([cp (compile-pattern lang pat)])
      (λ (main-exp exp f other-matches)
        (let ([mtchs (match-pattern cp exp)])
          (if mtchs
              (map/mt (λ (mtch) (list name (f (proc main-exp (mtch-bindings mtch)))))
                      mtchs
                      other-matches)
              other-matches)))))
  
  (define-syntax (test-match stx)
    (syntax-case stx ()
      [(_ lang-exp pattern)
       (with-syntax ([side-condition-rewritten (rewrite-side-conditions/check-errs 'test-match (syntax pattern))])
         (syntax 
          (do-test-match lang-exp `side-condition-rewritten)))]
      [(_ lang-exp pattern expression)
       (syntax 
        ((test-match lang-exp pattern) expression))]))
  
  (define-values (struct:metafunc-proc make-metafunc-proc metafunc-proc? metafunc-proc-ref metafunc-proc-set!)
    (make-struct-type 'metafunc-proc #f 3 0 #f null (current-inspector) 0))
  (define metafunc-proc-pict-info (make-struct-field-accessor metafunc-proc-ref 1))
  (define metafunc-proc-lang (make-struct-field-accessor metafunc-proc-ref 2))
  (define-struct metafunction (proc))
  
  (define-syntax (define-metafunction stx)
    (syntax-case stx (side-condition)
      [(_ name lang-exp (lhs rhs (side-condition tl-side-conds) ...) ...)
       (identifier? #'name)
       (with-syntax ([(side-conditions-rewritten ...) 
                      (map (λ (x) (rewrite-side-conditions/check-errs 'define-metafunction x))
                           (syntax->list (syntax ((side-condition lhs (and tl-side-conds ...)) ...))))]
                     [(rhs-fns ...)
                      (map (λ (lhs rhs)
                             (let-values ([(names names/ellipses) (extract-names 'define-metafunction lhs)])
                               (with-syntax ([(names ...) names]
                                             [(names/ellipses ...) names/ellipses]
                                             [rhs rhs])
                                 (syntax 
                                  (λ (bindings) (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
                                                          (term-let-fn (#;(name name))
                                                                       (term rhs))))))))
                           (syntax->list (syntax (lhs ...)))
                           (syntax->list (syntax (rhs ...))))]
                     [(name2) (generate-temporaries (syntax (name)))]
                     [((side-cond ...) ...)
                      ;; For generating a pict, separate out side conditions wrapping the LHS and at the top-level
                      (map (lambda (lhs scs)
                             (append
                              (let loop ([lhs lhs])
                                (syntax-case lhs (side-condition term)
                                  [(side-condition pat (term sc))
                                   (cons #'sc (loop #'pat))]
                                  [_else null]))
                              scs))
                           (syntax->list #'(lhs ...))
                           (syntax->list #'((tl-side-conds ...) ...)))]
                     [(((bind-id . bind-pat) ...) ...)
                      ;; Also for pict, extract pattern bindings
                      (map extract-pattern-binds (syntax->list #'(lhs ...)))]
                     [(lhs-app ...) (map (lambda (lhs)
                                           (if (eq? 'any (syntax-e lhs))
                                               'otherwise
                                               (let loop ([lhs lhs])
                                                 (syntax-case lhs (side-condition term)
                                                   [(side-condition pat (term sc))
                                                    (loop #'pat)]
                                                   [_else
                                                    (quasisyntax/loc lhs
                                                      (#,(datum->syntax-object
                                                          #'name
                                                          (syntax-e #'name)
                                                          (list (syntax-source lhs)
                                                                (syntax-line lhs)
                                                                (syntax-column lhs)
                                                                (syntax-position lhs)
                                                                0))
                                                         #,lhs))]))))
                                         (syntax->list (syntax (lhs ...))))])
         (syntax
          (begin
            (define name2
              (let ([lang lang-exp])
                (build-metafunction 
                 lang
                 (list `side-conditions-rewritten ...)
                 (list rhs-fns ...)
                 (λ (f) (make-metafunc-proc
                         (let ([name (lambda (x) (f x))]) name)
                         (list (list (to-loc-wrapper lhs-app)
                                     (list (to-loc-wrapper side-cond) ...)
                                     (list (cons (to-loc-wrapper bind-id)
                                                 (to-loc-wrapper bind-pat))
                                           ...)
                                     (to-loc-wrapper rhs)) ...)
                         lang))
                 'name)))
            (term-define-fn name name2))))]
      [(_ name lang-exp clauses ...)
       (begin
         (unless (identifier? #'name)
           (raise-syntax-error 'define-metafunction "expected a name" stx #'name))
         (for-each 
          (λ (clause)
            (syntax-case clause ()
              [(a b) (void)]
              [else (raise-syntax-error 'define-metafunction "expected a lhs and rhs clause" stx clause)]))
          (syntax->list (syntax (clauses ...)))))]))
  
  (define-syntax (metafunction-form stx)
    (syntax-case stx ()
      [(_ id)
       (identifier? #'id)
       (let ([v (syntax-local-value #'id (lambda () #f))])
         (if (term-fn? v)
             #`(make-metafunction #,(term-fn-get v 0))
             (raise-syntax-error
              #f
              "not bound as a metafunction"
              stx
              #'id)))]))
  
  #;
  (define-syntax (metafunction stx)
    (syntax-case stx ()
      [(_ lang-exp (lhs rhs) ...)
       (with-syntax ([(side-conditions-rewritten ...) (map (λ (x) (rewrite-side-conditions/check-errs 'metafunction))
                                                           (syntax->list (syntax (lhs ...))))]
                     [(rhs-fns ...)
                      (map (λ (lhs rhs)
                             (let-values ([(names names/ellipses) (extract-names 'metafunction lhs)])
                               (with-syntax ([(names ...) names]
                                             [(names/ellipses ...) names/ellipses]
                                             [rhs rhs])
                                 (syntax 
                                  (λ (bindings) (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
                                                          (term rhs)))))))
                           (syntax->list (syntax (lhs ...)))
                           (syntax->list (syntax (rhs ...))))]
                     [name (or (syntax-local-infer-name stx) 'metafunction)])
         (syntax
          (build-metafunction 
           lang-exp
           (list `side-conditions-rewritten ...)
           (list rhs-fns ...)
           (λ (f) (let ([name (lambda (x) (f x))]) name))
           'name)))]))
  
  (define-syntax (language stx)
    (syntax-case stx ()
      [(_ (name rhs ...) ...)
       (andmap identifier? (syntax->list (syntax/loc stx (name ...))))
       (begin
         
         
         (for-each 
          (λ (name) 
            (let ([x (syntax-object->datum name)])
              (when (memq x '(any number string variable variable-except variable-prefix hole name in-hole in-named-hole side-condition cross ...))
                (raise-syntax-error 'language 
                                    (format "cannot use pattern language keyword ~a as non-terminal"
                                            x)
                                    stx
                                    name))
              (when (regexp-match #rx"_" (symbol->string x))
                (raise-syntax-error 'language
                                    "non-terminals cannot have _ in their names"
                                    stx
                                    name))))
          (syntax->list (syntax (name ...))))
                
         (with-syntax ([((r-rhs ...) ...) (map (lambda (rhss) (map (λ (x) (rewrite-side-conditions/check-errs 'language x)) (syntax->list rhss)))
                                               (syntax->list (syntax ((rhs ...) ...))))]
                       [(refs ...)
                        (let loop ([stx (syntax ((rhs ...) ...))])
                          (cond
                            [(identifier? stx)
                             (if (ormap (λ (x) (module-identifier=? x stx)) 
                                        (syntax->list (syntax (name ...))))
                                 (list stx)
                                 '())]
                            [(syntax? stx)
                             (loop (syntax-e stx))]
                            [(pair? stx)
                             (append (loop (car stx))
                                     (loop (cdr stx)))]
                            [else '()]))])
           (with-syntax ([(the-stx ...) (cdr (syntax-e stx))])
             (syntax/loc stx
               (begin
                 (begin
                   (let ([name 1] ...)
                     (begin (void) refs ...))
                   (compile-language (list (list 'name (to-loc-wrapper rhs) ...) ...)
                                     (list (make-nt 'name (list (make-rhs `r-rhs) ...)) ...))))))))]
      [(_ (name rhs ...) ...)
       (for-each
        (lambda (name)
          (unless (identifier? name)
            (raise-syntax-error 'language "expected name" stx name)))
        (syntax->list (syntax (name ...))))]
      [(_ x ...)
       (for-each
        (lambda (x)
          (syntax-case x ()
            [(name rhs ...)
             (void)]
            [_
             (raise-syntax-error 'language "malformed non-terminal" stx x)]))
        (syntax->list (syntax (x ...))))]))
  
  (define-syntax (extend-language stx)
    (syntax-case stx ()
      [(_ lang (name rhs ...) ...)
       (andmap identifier? (syntax->list (syntax/loc stx (name ...))))
       (with-syntax ([((r-rhs ...) ...) (map (lambda (rhss) (map (λ (x) (rewrite-side-conditions/check-errs 'extend-language x)) (syntax->list rhss)))
                                             (syntax->list (syntax ((rhs ...) ...))))])
         (syntax/loc stx
           (do-extend-language lang 
                               (list (make-nt 'name (list (make-rhs `r-rhs) ...)) ...)
                               (list (list 'name (to-loc-wrapper rhs) ...) ...))))]
      [(_ lang (name rhs ...) ...)
       (for-each
        (lambda (name)
          (unless (identifier? name)
            (raise-syntax-error 'extend-language "expected name" stx name)))
        (syntax->list (syntax (name ...))))]
      [(_ lang x ...)
       (for-each
        (lambda (x)
          (syntax-case x ()
            [(name rhs ...)
             (void)]
            [_
             (raise-syntax-error 'extend-language "malformed non-terminal" stx x)]))
        (syntax->list (syntax (x ...))))]))
  
  (define extend-nt-ellipses '(....))
  
  (define (do-extend-language old-lang new-nts new-pict-infos)
    (let ([old-nts (compiled-lang-lang old-lang)]
          [old-ht (make-hash-table)]
          [new-ht (make-hash-table)])
      (for-each (λ (nt) 
                  (hash-table-put! old-ht (nt-name nt) nt)
                  (hash-table-put! new-ht (nt-name nt) nt))
                old-nts)
      (for-each (λ (nt)
                  (cond
                    [(ormap (λ (rhs) (member (rhs-pattern rhs) extend-nt-ellipses))
                            (nt-rhs nt))
                     (unless (hash-table-get old-ht (nt-name nt) #f)
                       (error 'extend-language "the language extends the ~s non-terminal, but that non-terminal is not in the old language"
                              (nt-name nt)))
                     (hash-table-put! new-ht 
                                      (nt-name nt)
                                      (make-nt
                                       (nt-name nt)
                                       (append (nt-rhs (hash-table-get old-ht (nt-name nt)))
                                               (filter (λ (rhs) (not (member (rhs-pattern rhs) extend-nt-ellipses)))
                                                       (nt-rhs nt)))))]
                    [else
                     (hash-table-put! new-ht (nt-name nt) nt)]))
                new-nts)
      (compile-language (append (compiled-lang-pict-builder old-lang)
                                new-pict-infos)
                        (hash-table-map new-ht (λ (x y) y)))))
  
  (define (apply-reduction-relation* reductions exp)
    (let ([answers (make-hash-table 'equal)])
      (let loop ([exp exp])
        (let ([nexts (apply-reduction-relation reductions exp)])
          (let ([uniq (mk-uniq nexts)])
            (unless (= (length uniq) (length nexts))
              (error 'apply-reduction-relation*
                     "term ~s produced non unique results:~a"
                     exp
                     (apply
                      string-append
                      (map (λ (x) (format "\n~s" x)) nexts))))
            (cond
              [(null? uniq) (hash-table-put! answers exp #t)]
              [else (for-each loop uniq)]))))
      (hash-table-map answers (λ (x y) x))))
  
  ;; mk-uniq : (listof X) -> (listof X)
  ;; returns the uniq elements (according to equal?) in terms.
  (define (mk-uniq terms)
    (let ([ht (make-hash-table 'equal)])
      (for-each (λ (x) (hash-table-put! ht x #t)) terms)
      (hash-table-map ht (λ (k v) k))))
               
  
  ;; map/mt : (a -> b) (listof a) (listof b) -> (listof b)
  ;; map/mt is like map, except it uses the last argument
  ;; instaed of the empty list
  (define (map/mt f l mt-l)
    (let loop ([l l])
      (cond
        [(null? l) mt-l]
        [else (cons (f (car l)) (loop (cdr l)))])))
    
  (define re:gen-d #rx".*[^0-9]([0-9]+)$")
  (define (variable-not-in sexp var)
    (let* ([var-str (symbol->string var)]
           [var-prefix (let ([m (regexp-match #rx"^(.*[^0-9])[0-9]+$" var-str)])
                         (if m
                             (cadr m)
                             var-str))]
           [found-exact-var? #f]
           [nums (let loop ([sexp sexp]
                            [nums null])
                   (cond
                     [(pair? sexp) (loop (cdr sexp) (loop (car sexp) nums))]
                     [(symbol? sexp) 
                      (when (eq? sexp var)
                        (set! found-exact-var? #t))
                      (let* ([str (symbol->string sexp)]
                             [match (regexp-match re:gen-d str)])
                        (if (and match
                                 (is-prefix? var-prefix str))
                            (cons (string->number (cadr match)) nums)
                            nums))]
                     [else nums]))])
      (cond
        [(not found-exact-var?) var]
        [(null? nums) (string->symbol (format "~a1" var))]
        [else (string->symbol (format "~a~a" var-prefix (+ 1 (apply max nums))))])))
  
  (define (variables-not-in sexp vars)
    (let loop ([vars vars]
               [sexp sexp])
      (cond
        [(null? vars) null]
        [else 
         (let ([new-var (variable-not-in sexp (car vars))])
           (cons new-var
                 (loop (cdr vars)
                       (cons new-var sexp))))])))
  
  (define (is-prefix? str1 str2)
    (and (<= (string-length str1) (string-length str2))
         (equal? str1 (substring str2 0 (string-length str1)))))
  
  
  ;; The struct selector extracts the reduction relation rules, which
  ;; are in reverse order compared to the way the reduction relation was written
  ;; in the program text. So reverse them.
  (define (reduction-relation->rule-names x)
    (reverse (reduction-relation-rule-names x)))

(provide (rename -reduction-relation reduction-relation) 
           --> fresh ;; keywords for reduction-relation

           compatible-closure
           context-closure
           
           language
           extend-language
           define-metafunction
           (rename metafunction-form metafunction)
           metafunction? metafunction-proc
           metafunc-proc-lang
           metafunc-proc-pict-info           
           reduction-relation->rule-names)
  
  (provide test-match
           term-match
           term-match/single
           make-bindings bindings-table bindings?
           mtch? mtch-bindings mtch-context  mtch-hole
           make-rib rib? rib-name rib-exp
           reduction-relation?)
  
  (provide language-nts
           apply-reduction-relation
           apply-reduction-relation/tag-with-names
           apply-reduction-relation*
           union-reduction-relations
           variable-not-in
           variables-not-in))