Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-25 02:35:15 -0800 (Sat, 25 Jan 2003)
Revision: 4023
Log message:
- Now the msequents in tactic_args on RuleBox level are normalized
(e.g. cons-hashed).
- The proofs are normalized (e.g. redundant identity steps are eliminated)
before doing a node count.
- Removed some extremely old code that was there for handling old (1999!)
binary proof format. Obviously, it is no longer needed.
Note - there are to reasons for the msequent normalization:
- I am planning to add the code that during term normalization
would drop variables from hypotheses bindings, if the variable is unused.
This would means that sequents can become slightly different (still alpha-equal,
of course) as a result of being normalized. Since disk IO uses normalization
as well, this could potentially cause users tactics to behave differently when
saved and reloaded. By making sure ruleboxes are always normalized, we
can make sure user tactics are always applied to normalized sequents (both
before the disk IO and after), so they should still behave the same.
- This gave about 8-9% speed-up on "status_all()" - primarily (I guess) by
reducing the memory footprint.
| Changes | Path |
| +1 -3 | metaprl/editor/ml/package_info.ml |
| +6 -28 | metaprl/filter/boot/proof_boot.ml |
| +1 -3 | metaprl/filter/boot/proof_convert.ml |
| +0 -5 | metaprl/filter/boot/tactic_boot_sig.mlz |