Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-15 22:44:46 -0800 (Mon, 15 Mar 2004)
Revision: 5461
Log message:
Adding support for patterns that match _free_ FO variables.
With this commit, any free FO variable in a redex or contractum is taken
to be a pattern that would match an arbitrary _free_ FO variable. This is
probably not going to be useful in ITT-like domains, where variables usually
stand for arbitrary terms (and therefore there is not much difference between
free FO variables and SO variables), but in programming language domains this
capability of being able to have patters matching the object-level variables
should be extremely useful.
On IO, the 'v would still expand into 'v[] _SO_ variable when v is free.
Therefore, on IO the free _FO_ variables are denoted using the !v syntax.
The new syntax and new rewriting capabilities are not yet used (except in
the term table, which will now use !v matching) and are not very well tested
yet.