(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] ...)
       (begin
         (unless (identifier? #'lang)
           (raise-syntax-error 'term-match/single "expected an identifier in the language position" stx #'lang))
         (let ([lang-nts (language-id-nts #'lang 'reduction-relation)])
           (with-syntax ([(((names ...) (names/ellipses ...)) ...)
                          (map (λ (x) (let-values ([(names names/ellipses) (extract-names lang-nts 'term-match/single x)])
                                        (list names names/ellipses)))
                               (syntax->list (syntax (pattern ...))))]
                         [(side-conditions-rewritten ...)
                          (map (λ (x) (rewrite-side-conditions/check-errs lang-nts '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 #t)] ...)
                   (λ (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] ...)
       (begin
         (unless (identifier? #'lang)
           (raise-syntax-error 'term-match "expected an identifier" stx #'lang))
         (let ([lang-nts (language-id-nts #'lang 'reduction-relation)])
           (with-syntax ([(((names ...) (names/ellipses ...)) ...)
                          (map (λ (x) (let-values ([(names names/ellipses) (extract-names lang-nts 'term-match x)])
                                        (list names names/ellipses)))
                               (syntax->list (syntax (pattern ...))))]
                         [(side-conditions-rewritten ...)
                          (map (λ (x) (rewrite-side-conditions/check-errs lang-nts '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 #t)] ...)
                   (λ (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 (language-id-nts #'lang 'compatible-closure)
                                                                                    '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 (language-id-nts #'lang 'context-closure)
                                                                                    '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))
               #f)])
      (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-syntax (--> stx) (raise-syntax-error '--> "used outside of reduction-relation"))
  (define-syntax (fresh stx) (raise-syntax-error 'fresh "used outside of reduction-relation"))
  (define-syntax (where stx) (raise-syntax-error 'where "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)
         (identifier? #'id)
         (cons (cons #'id #'expr) (loop #'expr))]
        ;; FIXME: should follow the grammar of patterns!
        [(a . b)
         (append (loop #'a) (loop #'b))]
        [_else null])))
  
  (define-for-syntax (extract-term-let-binds lhs)
    (let loop ([lhs lhs])
      (syntax-case* lhs (term-let) (lambda (a b) (eq? (syntax-e a) (syntax-e b)))
        [(term-let ((x e1) ...) e2 ...)
         (append (map cons
                      (syntax->list #'(x ...))
                      (syntax->list #'(e1 ...)))
                 (loop #'(e2 ...)))]
        ;; 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 ...)
         (identifier? #'lang)
         (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 ...))))]
        [(_ lang args ...)
         (raise-syntax-error 'reduction-relation 
                             "expected an identifier for the language name"
                             stx 
                             #'lang)]))
    
    (define (before-where stx)
      (let loop ([lst (syntax->list stx)])
        (cond
          [(null? lst) null]
          [else
           (let ([fst (car lst)])
             (syntax-case (car lst) (where)
               [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)
               [where (cdr lst)]
               [else (loop (cdr lst))]))])))
    
    (define (rule->lws rule)
      (syntax-case rule ()
        [(arrow lhs rhs stuff ...)
         (let-values ([(label scs fvars wheres)
                       (let loop ([stuffs (syntax->list #'(stuff ...))]
                                  [label #f]
                                  [scs null]
                                  [fvars null]
                                  [wheres null])
                         (cond
                           [(null? stuffs) (values label (reverse scs) (reverse fvars) (reverse wheres))]
                           [else
                            (syntax-case (car stuffs) (where 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)
                                     wheres)]
                              [(where x e)
                               (loop (cdr stuffs)
                                     label
                                     scs
                                     fvars
                                     (cons #'(x e) wheres))]
                              [(side-condition sc)
                               (loop (cdr stuffs)
                                     label
                                     (cons #'sc scs)
                                     fvars
                                     wheres)]
                              [x
                               (identifier? #'x)
                               (loop (cdr stuffs)
                                     #''x
                                     scs
                                     fvars
                                     wheres)]
                              [x
                               (string? (syntax-e #'x))
                               (loop (cdr stuffs)
                                     #'x
                                     scs
                                     fvars
                                     wheres)])]))])
           (with-syntax ([(scs ...) scs]
                         [(fvars ...) fvars]
                         [((where-id where-expr) ...) wheres]
                         [((bind-id . bind-pat) ...) 
                          (append (extract-pattern-binds #'lhs)
                                  (extract-term-let-binds #'rhs))])
             #`(make-rule-pict 'arrow
                               (to-loc-wrapper lhs)
                               (to-loc-wrapper rhs)
                               #,label
                               (list (to-loc-wrapper/uq scs) ...)
                               (list (to-loc-wrapper fvars) ...)
                               (list (cons (to-loc-wrapper bind-id)
                                           (to-loc-wrapper bind-pat))
                                     ...
                                     (cons (to-loc-wrapper where-id)
                                           (to-loc-wrapper where-expr))
                                     ...))))]))
  
    (define (reduction-relation/helper stx lang-id 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-id lang-id]
                        [(top-level ...) (get-choices stx ht lang-id (syntax -->) name-ht lang-id)]
                        [(rule-names ...) (hash-table-map name-ht (λ (k v) k))]
                        [lws lws])
            (syntax 
             (make-reduction-relation
              lang-id
              (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] identifier[language-name] -> (listof relation-tree)
    (define (get-choices stx bm lang id name-table lang-id)
      (reverse
       (map (λ (x) (get-tree stx bm lang x name-table lang-id))
            (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 lang-id)
      (syntax-case case-stx ()
        [(arrow from to extras ...)
         (do-leaf stx 
                  lang 
                  name-table
                  (syntax from) 
                  (syntax to) 
                  (syntax->list (syntax (extras ...)))
                  lang-id)]
        [((lhs-arrow lhs-frm-id lhs-to-id) (rhs-arrow rhs-from rhs-to))
         (let ([lang-nts (language-id-nts lang-id 'reduction-relation)])
           (let-values ([(names names/ellipses) (extract-names lang-nts 'reduction-relation (syntax rhs-from))])
             (with-syntax ([(names ...) names]
                           [(names/ellipses ...) names/ellipses]
                           [side-conditions-rewritten (rewrite-side-conditions/check-errs
                                                       lang-nts
                                                       '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 lang-id)])
               (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 lang-id)
      (let ([lang-nts (language-id-nts lang-id 'reduction-relation)])
        (let-values ([(name fresh-vars side-conditions/wheres) (process-extras stx name-table extras)])
          (let-values ([(names names/ellipses) (extract-names lang-nts 'reduction-relation from)])
            (with-syntax ([side-conditions-rewritten 
                           (rewrite-side-conditions/check-errs 
                            lang-nts
                            'reduction-relation
                            from)]
                          [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)])
              #`(do-leaf-match
                 lang
                 name
                 `side-conditions-rewritten
                 (λ (main bindings)
                   ;; nested term-let's so that the bindings for the variables
                   ;; show up in the `fresh' side-conditions, the bindings for the variables
                   ;; show up in the wheres, and the wheres show up in the 'fresh' side-conditions
                   (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
                     (term-let (fresh-var-clauses ...)
                       #,(bind-wheres side-conditions/wheres
                                      #'(term to)))))))))))
    
    ;; the wheres and side-conditions come in backwards order
    (define (bind-wheres stx body)
      (let loop ([stx stx]
                 [body body])
        (syntax-case stx (side-condition where)
          [() body]
          [((where x e) y ...) 
           (loop #'(y ...) #`(term-let ([x (term e)]) #,body))]
          [((side-condition s ...) y ...)
           (loop #'(y ...) #`(and s ... #,body))])))
    
    (define (process-extras stx name-table extras)
      (let ([the-name #f]
            [the-name-stx #f]
            [fresh-vars '()]
            [side-conditions/wheres '()])
        (let loop ([extras extras])
          (cond
            [(null? extras) (values the-name fresh-vars side-conditions/wheres)]
            [else
             (syntax-case (car extras) (side-condition fresh where)
               [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/wheres (cons (car extras) side-conditions/wheres))
                  (loop (cdr extras)))]
               [(where x e)
                (begin
                  (set! side-conditions/wheres (cons (car extras) side-conditions/wheres))
                  (loop (cdr extras)))]
               [(where . x)
                (raise-syntax-error 'reduction-relation "malformed where clause" stx (car 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)
              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 #t)])
      (λ (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 #t)])
      (λ (main-exp exp f other-matches)
        (let ([mtchs (match-pattern cp exp)])
          (if mtchs
              (map/mt (λ (mtch) 
                        (let ([really-matched (proc main-exp (mtch-bindings mtch))])
                          (and really-matched
                               (list name (f really-matched)))))
                      mtchs
                      other-matches)
              other-matches)))))
  
  (define-syntax (test-match stx)
    (syntax-case stx ()
      [(_ lang-exp pattern)
       (identifier? #'lang-exp)
       (with-syntax ([side-condition-rewritten (rewrite-side-conditions/check-errs (language-id-nts #'lang-exp 'test-match) 'test-match (syntax pattern))])
         (syntax 
          (do-test-match lang-exp `side-condition-rewritten)))]
      [(_ lang-exp pattern expression)
       (identifier? #'lang-exp)
       (syntax 
        ((test-match lang-exp pattern) expression))]
      [(_ a b c)
       (raise-syntax-error 'test-match "expected an identifier (bound to a language) as first argument" stx #'a)]
      [(_ a b)
       (raise-syntax-error 'test-match "expected an identifier (bound to a language) as first argument" stx #'a)]))
  
  (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 #t)])
      (λ (exp)
        (match-pattern cpat exp))))
  
  (define-values (struct:metafunc-proc make-metafunc-proc metafunc-proc? metafunc-proc-ref metafunc-proc-set!)
    (make-struct-type 'metafunc-proc #f 7 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 metafunc-proc-multi-arg? (make-struct-field-accessor metafunc-proc-ref 3))
  (define metafunc-proc-name (make-struct-field-accessor metafunc-proc-ref 4))
  (define metafunc-proc-cps (make-struct-field-accessor metafunc-proc-ref 5))
  (define metafunc-proc-rhss (make-struct-field-accessor metafunc-proc-ref 6))
  (define-struct metafunction (proc))
  
  (define-syntax (define-metafunction stx)
    (syntax-case stx ()
      [(_ name lang-exp [lhs roc ...] ...)
       (with-syntax ([(lhs-w ...) (map (λ (x) (list x)) (syntax->list #'(lhs ...)))])
         (syntax/loc stx
           (internal-define-metafunction 
            #f #f name lang-exp
            [lhs-w roc ...] ...)))]))
  
    
  (define-syntax (define-metafunction/extension stx)
    (syntax-case stx ()
      [(_ name lang-exp prev [lhs roc ...] ...)
       (identifier? #'name)
       (with-syntax ([(lhs-w ...) (map (λ (x) (list x)) (syntax->list #'(lhs ...)))])
         (syntax/loc stx
           (internal-define-metafunction 
            prev #f name lang-exp
            [lhs-w roc ...] ...)))]))
  
  (define-syntax (define-multi-args-metafunction stx)
    (syntax-case stx ()
      [(_ name lang-exp [(lhs ...) roc ...] ...)
       (with-syntax ([s (list* #'internal-define-metafunction
                               #f #t
                               (cdr (syntax->list stx)))])
         (syntax/loc stx s))]
      [(_ name lang-exp clauses ...)
       (begin
         (unless (identifier? #'name)
           (raise-syntax-error 'define-multi-args-metafunction "expected a name" stx #'name))
         (for-each 
          (λ (clause)
            (syntax-case clause ()
              [((a ...) b) (void)]
              [(a b)
               (raise-syntax-error 'define-multi-args-metafunction "expected lhs clause to be a sequence (with parens)" 
                                   stx
                                   #'a)]
              [else
               (raise-syntax-error 'define-metafunction "expected a lhs and rhs clause" stx clause)]))
          (syntax->list (syntax (clauses ...))))
         (raise-syntax-error 'define-multi-args-metafunction "missing error message check" stx))]))
  
  (define-syntax (define-multi-args-metafunction/extension stx)
    (syntax-case stx ()
      [(_ name lang-exp prev [lhs roc ...] ...)
       (identifier? #'name)
       (syntax/loc stx
         (internal-define-metafunction 
          prev #t name lang-exp
          [lhs roc ...] ...))]))
  
  (define-syntax-set (internal-define-metafunction)
    (define (internal-define-metafunction/proc stx)
      (syntax-case stx ()
        [(_ prev-metafunction multi-args? name lang (lhs rhs stuff ...) ...)
         (and (identifier? #'name)
              (identifier? #'lang))
         (with-syntax ([(((tl-side-conds ...) ...) 
                         (tl-bindings ...))
                        (extract-side-conditions (syntax-e #'name) stx #'((stuff ...) ...))])
           (let ([lang-nts (language-id-nts #'lang 'define-metafunction)])
             (with-syntax ([(side-conditions-rewritten ...) 
                            (map (λ (x) (rewrite-side-conditions/check-errs
                                         lang-nts
                                         'define-metafunction x))
                                 (syntax->list (syntax ((side-condition lhs (and tl-side-conds ...)) ...))))]
                           [(rhs-fns ...)
                            (map (λ (lhs rhs bindings)
                                   (let-values ([(names names/ellipses) (extract-names lang-nts 'define-metafunction lhs)])
                                     (with-syntax ([(names ...) names]
                                                   [(names/ellipses ...) names/ellipses]
                                                   [rhs rhs]
                                                   [((tl-var tl-exp) ...) bindings])
                                       (syntax 
                                        (λ (name bindings)
                                          (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
                                            (term-let ([tl-var tl-exp] ...)
                                              (term-let-fn ((name name))
                                                           (term rhs)))))))))
                                 (syntax->list (syntax (lhs ...)))
                                 (syntax->list (syntax (rhs ...)))
                                 (syntax->list (syntax (tl-bindings ...))))]
                           [(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 ...) (if (syntax-e #'multi-args?)
                                              (syntax->list (syntax (lhs ...)))
                                              ;; if single arg, drop the extra parens, since they have the wrong
                                              ;; source locations anyways
                                              (map (λ (x) (car (syntax-e x)))
                                                   (syntax->list (syntax (lhs ...)))))])
               #`(begin
                   (define name2
                     (build-metafunction 
                      lang
                      (list `side-conditions-rewritten ...)
                      (list rhs-fns ...)
                      #,(if (syntax-e #'prev-metafunction)
                            (let ([term-fn (syntax-local-value #'prev-metafunction)])
                              #`(metafunc-proc-cps #,(term-fn-get-id term-fn)))
                            '())
                      #,(if (syntax-e #'prev-metafunction)
                            (let ([term-fn (syntax-local-value #'prev-metafunction)])
                              #`(metafunc-proc-rhss #,(term-fn-get-id term-fn)))
                            '())
                      (λ (f cps rhss) 
                        (make-metafunc-proc
                         (let ([name (lambda (x) (f x))]) name)
                         (list (list (to-loc-wrapper lhs-app)
                                     (list (to-loc-wrapper/uq side-cond) ...)
                                     (list (cons (to-loc-wrapper bind-id)
                                                 (to-loc-wrapper bind-pat))
                                           ...)
                                     (to-loc-wrapper rhs))
                               ...)
                         lang
                         multi-args?
                         'name
                         cps
                         rhss))
                      'name))
                   (term-define-fn name name2 multi-args?)))))]
        [(_ prev-metafunction multi-args? name lang clauses ...)
         (begin
           (unless (identifier? #'name)
             (raise-syntax-error 'define-metafunction "expected a name" stx #'name))
           (unless (identifier? #'lang)
             (raise-syntax-error 'define-metafunction "expected a name" stx #'lang))
           (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 ...))))
           (raise-syntax-error 'define-metafunction "missing error check for bad syntax" stx))]))
    
    
    (define (extract-side-conditions name stx stuffs)
      (let loop ([stuffs (syntax->list stuffs)]
                 [side-conditionss '()]
                 [bindingss '()])
          (cond
            [(null? stuffs) (list (reverse side-conditionss)
                                  (reverse bindingss))]
            [else 
             (let s-loop ([stuff (syntax->list (car stuffs))]
                          [side-conditions '()]
                          [bindings '()])
               (cond
                 [(null? stuff) (loop (cdr stuffs)
                                      (cons (reverse side-conditions) side-conditionss)
                                      (cons (reverse bindings) bindingss))]
                 [else 
                  (syntax-case (car stuff) (side-condition)
                    [(side-condition tl-side-conds ...) 
                     (s-loop (cdr stuff)
                             (append (syntax->list #'(tl-side-conds ...)) side-conditions)
                             bindings)]
                    [(where x e)
                     (s-loop (cdr stuff)
                             side-conditions
                             (cons #'(x e) bindings))]
                    [_
                     (raise-syntax-error 'define-metafunction 
                                         "expected a side-condition or where clause"
                                         (car stuff))])]))]))))
  
  (define (build-metafunction lang patterns rhss old-cps old-rhss wrap name)
    (let ([compiled-patterns (append old-cps
                                     (map (λ (pat) (compile-pattern lang pat #t)) patterns))])
      (wrap
       (letrec ([metafunc
                 (λ (exp)
                   (let loop ([patterns compiled-patterns]
                              [rhss (append old-rhss rhss)]
                              [num (- (length old-cps))])
                     (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 "~a matched ~s ~a different ways" 
                                      (if (< num 0)
                                          "a clause from an extended metafunction"
                                          (format "clause ~a" num))
                                      exp
                                      (length mtchs))]
                              [else
                               (rhs metafunc (mtch-bindings (car mtchs)))])))])))])
         metafunc)
       compiled-patterns
       rhss)))

  (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-id v))
             (raise-syntax-error
              #f
              "not bound as a metafunction"
              stx
              #'id)))]))
  
  ;; pull-out-names : symbol syntax -> list-of-identifier
  (define-for-syntax (pull-out-names form stx ids)
    (let loop ([names (syntax->list ids)]
               [acc '()])
      (cond
        [(null? names) acc]
        [else
         (let* ([name (car names)]
                [lst (syntax->list name)])
           (cond
             [(identifier? name) (loop (cdr names) (cons (syntax-e name) acc))]
             [(and (list? lst)
                   (andmap identifier? lst))
              (loop (cdr names) (append (map syntax-e lst) acc))]
             [(list? lst)
              (for-each (λ (x) (unless (identifier? x)
                                 (raise-syntax-error form "expected an identifier" stx x)))
                        lst)]
             [else
              (raise-syntax-error form 
                                  "expected an identifier or a sequence of identifiers"
                                  stx
                                  name)]))])))
  
  (define-syntax (define-language stx)
    (syntax-case stx ()
      [(_ name (names rhs ...) ...)
       (identifier? (syntax name))
       (with-syntax ([(nt-names ...) (pull-out-names 'define-language stx #'(names ...))])
         (syntax/loc stx
           (begin
             (define define-language-name (language (names rhs ...) ...))
             (define-syntax name
               (make-set!-transformer
                (make-language-id
                 (λ (stx)
                   (syntax-case stx (set!)
                     [(set! x e) (raise-syntax-error 'define-language "cannot set! identifier" stx #'e)]
                     [(x e (... ...)) #'(define-language-name e (... ...))]
                     [x 
                      (identifier? #'x)
                      #'define-language-name]))
                 '(nt-names ...)))))))]))
  
  (define-syntax (language stx)
    (syntax-case stx ()
      [(_ (name rhs ...) ...)
       (begin
         ;; verify `name' part has the right shape
         (for-each
          (λ (name)
            (cond
              [(identifier? name) (void)]
              [else
               (let ([lst (syntax->list name)])
                 (cond 
                   [(list? lst) 
                    (when (null? lst)
                      (raise-syntax-error 'language 
                                          "expected a sequence of identifiers with at least one identifier"
                                          stx
                                          name))
                    (for-each (λ (x) (unless (identifier? x)
                                       (raise-syntax-error 'language 
                                                           "expected an identifier"
                                                           stx
                                                           x)))
                              lst)]
                   [else
                    (raise-syntax-error 'language 
                                        "expected a sequence of identifiers"
                                        stx
                                        lst)]))]))
          (syntax->list #'(name ...)))
         (let ([all-names (apply append (map (λ (x) (if (identifier? x) (list x) (syntax->list x))) 
                                             (syntax->list #'(name ...))))])
           ;; verify the names are valid names
           (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 hide-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))))
            all-names)
           (with-syntax ([((r-rhs ...) ...) (map (lambda (rhss) (map (λ (x) (rewrite-side-conditions/check-errs (map syntax-e all-names) '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)) 
                                          all-names)
                                   (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))]
                           [(all-names ...) all-names]
                           [((uniform-names ...) ...)
                            (map (λ (x) (if (identifier? x) (list x) x))
                                 (syntax->list (syntax (name ...))))]
                           [(first-names ...)
                            (map (λ (x) (if (identifier? x) x (car (syntax->list x))))
                                 (syntax->list (syntax (name ...))))]
                           [((new-name orig-name) ...)
                            (apply
                             append
                             (map (λ (name-stx)
                                    (if (identifier? name-stx)
                                        '()
                                        (let ([l (syntax->list name-stx)])
                                          (map (λ (x) (list x (car l)))
                                               (cdr l)))))
                                  (syntax->list #'(name ...))))])
               (syntax/loc stx
                 (begin
                   (let ([all-names 1] ...)
                     (begin (void) refs ...))
                   (compile-language (list (list '(uniform-names ...) (to-loc-wrapper rhs) ...) ...)
                                     (list (make-nt 'first-names (list (make-rhs `r-rhs) ...)) ...
                                           (make-nt 'new-name (list (make-rhs 'orig-name))) ...))))))))]
      [(_ (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 (define-extended-language stx)
    (syntax-case stx ()
      [(_ name orig-lang (names rhs ...) ...)
       (begin
         (unless (identifier? (syntax name))
           (raise-syntax-error 'define-extended-langauge "expected an identifier" stx #'name))
         (unless (identifier? (syntax orig-lang))
           (raise-syntax-error 'define-extended-langauge "expected an identifier" stx #'orig-lang))
         (let ([old-names (language-id-nts #'orig-lang 'define-extended-language)])
           (with-syntax ([(new-nt-names ...) (append (pull-out-names 'define-language stx #'(names ...)) old-names)])
             #'(begin
                 (define define-language-name (extend-language orig-lang (names rhs ...) ...))
                 (define-syntax name
                   (make-set!-transformer
                    (make-language-id
                     (λ (stx)
                       (syntax-case stx (set!)
                         [(set! x e) (raise-syntax-error 'define-extended-language "cannot set! identifier" stx #'e)]
                         [(x e (... ...)) #'(define-language-name e (... ...))]
                         [x 
                          (identifier? #'x)
                          #'define-language-name]))
                     '(new-nt-names ...))))))))]))
  
  (define-syntax (extend-language stx)
    (syntax-case stx ()
      [(_ lang (name rhs ...) ...)
       (and (identifier? #'lang)
            (andmap identifier? (syntax->list (syntax/loc stx (name ...)))))
       (with-syntax ([((r-rhs ...) ...) (map (lambda (rhss) (map (λ (x) (rewrite-side-conditions/check-errs
                                                                         (language-id-nts #'lang 'extend-language)
                                                                         'extend-language x))
                                                                 (syntax->list rhss)))
                                             (syntax->list (syntax ((rhs ...) ...))))]
                     [((uniform-names ...) ...)
                      (map (λ (x) (if (identifier? x) (list x) x))
                           (syntax->list (syntax (name ...))))])
         (syntax/loc stx
           (do-extend-language lang 
                               (list (make-nt 'name (list (make-rhs `r-rhs) ...)) ...)
                               (list (list '(uniform-names ...) (to-loc-wrapper rhs) ...) ...))))]
      [(_ lang (name rhs ...) ...)
       (begin
         (unless (identifier? #'lang)
           (error 'extend-language "expected a name" stx #'lang))
         (for-each
          (lambda (name)
            (unless (identifier? name)
              (raise-syntax-error 'extend-language "expected a 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 '(....))
  
  ;; do-extend-language : compiled-lang (listof nt) ? -> compiled-lang
  (define (do-extend-language old-lang new-nts new-pict-infos)
    (unless (compiled-lang? old-lang)
      (error 'extend-language "expected a language as first argument, got ~e" old-lang))
    (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 (vector (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
  ;;  a) it uses the last argument instead of the empty list
  ;;  b) if `f' returns #f, that is not included in the result
  (define (map/mt f l mt-l)
    (let loop ([l l])
      (cond
        [(null? l) mt-l]
        [else
         (let ([this-one (f (car l))])
           (if this-one
               (cons this-one (loop (cdr 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 (find-best-number nums)))])))
  
  (define (find-best-number nums)
    (let loop ([sorted (sort nums <)]
               [i 1])
      (cond
        [(empty? sorted) i]
        [else 
         (let ([fst (car sorted)])
           (cond
             [(< i fst) i]
             [else (loop (cdr sorted) (+ i 1))]))])))
      
  (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 where ;; keywords for reduction-relation

           compatible-closure
           context-closure
           
           define-language
           define-extended-language
           define-metafunction
           define-metafunction/extension
           define-multi-args-metafunction
           define-multi-args-metafunction/extension
           
           (rename metafunction-form metafunction)
           metafunction? metafunction-proc
           metafunc-proc-lang
           metafunc-proc-pict-info
           metafunc-proc-name
           metafunc-proc-multi-arg?
           metafunc-proc-cps
           metafunc-proc-rhss
           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))