Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-23 02:11:41 -0800 (Tue, 23 Mar 2004)
Revision: 5523
Log message:
!!! WARNING : This commit breaks the .prlb compativility. !!!
!!! This commit makes the "check_status" run about 1.5 times faster !!!
This commit make a major change in how the Term_match_table is imlemented.
Instead of the hash table at the top only (with linear lookup for subterms)
this implementation uses the same functional term shape-indexed lookup tables
at both the top and subterm level. During lookup, this implementation keeps
an explicit list of "fallback" choices, which makes it easier to return more
than one match. This implementation is much closer to the one presented
in the paper submitted to TPHOLs.
This makes a few changes to the semantics of the dT tactic:
- Previously dT (both elim and intro) would only fall back to another tactic
if it had the same _term_, now it will fall back to all that have the same
_pattern_. For example, previously the entries for 'x='y in T, 'a in T and
'b in T (for a specific T) were all considered separately and at most one
would be tried, but now when applying the dT to a (t in T), all 3 could be
tried.
- Previously, if a pattern had both entires with select argument and entries
without select argument, then the non-select entries were tried only when dT 0
was called without the select argument. Now the non-select entries are always
tried.
This makes a change to the semantics of reduceC as well - now reduceC will try
_all_ matches (from the most specific to the least specific), not just the most
specific ones.
The display forms are now handled as a resource, instead of being a "special"
beast. This may cause the inheritance rules for display forms to change slightly,
and a few extra "extend" directives might have to be added to compensate.