(module reduction-semantics mzscheme
  (require "private/reduction-semantics.ss"
           "private/matcher.ss"
           "private/term.ss"
           (lib "contract.ss"))
  
  (provide reduction-relation 
           --> fresh where ;; keywords for reduction-relation
           
           compatible-closure
           context-closure
           
           language
           extend-language
           plug
	   compiled-lang?
           term
           term-let
           none?
           define-metafunction
           define-multi-args-metafunction
           metafunction)
  
  (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/contract
   [reduction-relation->rule-names (-> reduction-relation? (listof symbol?))]
   [language-nts (-> compiled-lang? (listof symbol?))]
   [set-cache-size! (-> number? void?)]
   [apply-reduction-relation (-> reduction-relation? any/c (listof any/c))]
   [apply-reduction-relation/tag-with-names
    (-> reduction-relation? any/c (listof (list/c (union false/c string?) any/c)))]
   [apply-reduction-relation* (-> reduction-relation? any/c (listof any/c))]
   [union-reduction-relations (->* (reduction-relation? reduction-relation?)
                                   (listof reduction-relation?)
                                   (reduction-relation?))]
   
   [lookup-binding (case-> 
                    (-> bindings? symbol? any)
                    (-> bindings? symbol? (-> any) any))]
   [variable-not-in (any/c symbol? . -> . symbol?)]
   [variables-not-in (any/c (listof symbol?) . -> . (listof symbol?))]))