(index ("reduce" 0) ("rewrite-map-tree" 240) ("rewrite-fold-tree" 599) ("rewrite-fold-tree-partial" 1127) ("match-tree" 1667) ("unify-trees" 2252) ("substitute-vars" 2822) ("substitute-vars-open" 3042))
(def (sig (procedure "(reduce  M-TERM RULES)" (id reduce))) (p "The principal reduction procedure. " (tt "RULES") " is a list of rewriting rules that follow the grammar above. Returns the term after all matching rules have been applied."))
(def (sig (procedure "(rewrite-map-tree  TREE RULES)" (id rewrite-map-tree))) (p "Applies the given set of rewrite rules to all elements in the list " (tt "TREE") ".  If none of the rules match a particular element, and that element is a list, recursively invokes itself on all elements in the tail of that list, and the head of the list is left in place."))
(def (sig (procedure "(rewrite-fold-tree RULES F INIT )" (id rewrite-fold-tree))) (p "Returns a procedure that takes in a list, and applies the given set of rewrite rules to the elements of the list. If a rule pattern matches, the values of " (tt "INIT") " is replaced by the result of " (tt "(F T INIT)") " where " (tt "T") " is the rewritten term. If no rule matches a given element, and the element is a list, recursively invokes itself on all elements in the tail of that list, and the head of the list is left in place."))
(def (sig (procedure "(rewrite-fold-tree-partial RULES F INIT )" (id rewrite-fold-tree-partial))) (p "Returns a procedure that takes in a list, and applies the given set of rewrite rules to the elements of the list. If a rule pattern matches, the values of " (tt "INIT") " is replaced by the result of " (tt "(F T INIT)") " where " (tt "T") " is the rewritten term. If no rule matches a given element, and the element is a list, recursively invokes itself on all elements in the tail of that list, and the head of the list is discarded."))
(def (sig (procedure "(match-tree TREE1 TREE2 ENV)" (id match-tree))) (p "A non-linear match of two ordered trees, one of which may contain variables.") (p (tt "TREE1") " may contain variables (symbols with leading " (tt "$") " sign). " (tt "TREE1") " may contain several occurrences of the same variable.  All these occurrences must match the same value.  A variable match is entered into the environment. A variable " (tt "_") " is an exception: its match is never entered into the environment.  The function returns the resulting environment or " (tt "#f") " if the match fails."))
(def (sig (procedure "(unify-trees TREE1 TREE2 ENV)" (id unify-trees))) (p "A match/unification of two ordered trees, both of which may contain variables. The unifier is capable of finding cyclic substitutions. The trees may contain several occurrences of the same variable.  All these occurrences must match the same value.  A variable match is entered into the environment. A variable " (tt "_") " is an exception: its match is never entered into the environment.  " (tt "unify-trees") " returns the resulting environment or " (tt "#f") " if the unification fails."))
(def (sig (procedure "(substitute-vars TERM ENV)" (id substitute-vars))) (p "Finds all the vars in term and substitutes them with values given in the environment. It's an error if a term contains an unbound variable."))
(def (sig (procedure "(substitute-vars-open TERM ENV)" (id substitute-vars-open))) (p "Finds all the vars in term and substitutes them with values given in the environment. Leaves free variables as they are."))
