Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-09 19:07:26 -0800 (Thu, 09 Jan 2003)
Revision: 3987
Log message:
- Added a version of a dest_bterm function (dest_bterm_and_rename)
that will alpha-rename the returned bterm to avoid clashes with
the specified set of variables.
- Changed the "match_redex" part of the rewriter to always use
dest_bterm_and_rename instead of dest_bterm. It now collects all the
bound variables that are explicitly mentioned (e.g. all of them except
those matched by a context) and makes sure dest_bterm_and_rename avoid
any possibility of clashes. It will also avoid clashes between
the hypotheses variable and the hypotheses contents (this last part
is somewhat contrary to the logical binding structure, but can not hurt).
Example, when matching ...; n: {n:Z| n>=0}; ... against a redex pattern
H; u: {v:T| P[v]}; J[u] >- C[u], the rewriter now will rename the "inner"
n into n_1.
This does not fix as many variable clash issues as I hoped for - it seems
many of those are coming from the build_contractum part of the rewriter.
I plan to address those later (I will probably post a proposed solution to
the newsgroup later today).