(module reduction-semantics mzscheme
(require "private/reduction-semantics.ss"
"private/matcher.ss"
"private/term.ss"
(lib "contract.ss"))
(provide reduction-relation
--> fresh where extend-reduction-relation
reduction-relation?
compatible-closure
context-closure
define-language
define-extended-language
plug
compiled-lang?
term
term-let
none?
define-metafunction
define-metafunction/extension
define-multi-args-metafunction
define-multi-args-metafunction/extension
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)
(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?))]))