Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-14 03:27:05 -0800 (Fri, 14 Mar 2003)
Revision: 4169
Log message:
- This is a _major change_ in how sequent contexts are now handles in rule
arguments. Now arguments corresponding to sequent contexts are passed in as _integers_.
To tell the rewriter that the corresponding context should match n hypotheses,
pass n + 1 as an argument. Also, if a context is at the _end_ of the hypotheses list,
it should _not_ be passed as an argument - instead, rewriter will just put all the remaining
hyps into it.
To summarize, a typical intro-style rule now does not need any context args at all. A typical
elim-style rule will now need only one context arg ('H) and that argument will be a straight
integer. That integer will have the same meaning as in traditional tactics - e.g. just
the hypothesis number. The only difference is that the arguments to primitive rules _have_
to be positive. Use Sequent.get_pos_hyp_num or pos_hypT to make numbers positive.
- I changed the semantics of the int arg to assertAtT and second int arg to copyHypT. Now
that int means the hyp number the new hyp will have in the resulting subgoal (whether
input is positive or negative).
- I fixed some of the proofs Yegor accidentally broke, but not all. Xin, you might have to
fix some of the cyclic_group proofs yourself, sorry.
- Cleaned up the address part of the TermAddm and TermMan interfaced, killed some
unnecessary functionality.
- More changes to line_buffer in Rformat - hopefully this time I finally got it right.