Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-27 01:33:57 -0800 (Thu, 27 Jan 2005)
Revision: 6513
Log message:
This is a somewhat significant change of the API for subterm addresses.
An address now is (isomorphic to) a list of the following components:
- Subterm i, where i is non-zero - a "normal" subterm, where positive
numbers count from the left and negaive numbers count from the
right
- ClauseAddr i - the address of the conclusion (i = 0 case), or of the
hypothesis (as usual, i >= 1 counts hyps from the left and
i <= -1 coult them from the right)
- ArgAddr - the addrerss of the sequent arg.
On command line, enter just "i" for "Subterm i", "Concl" or "Clause 0" for
"ClauseAddr 0", "Hyp i" or "Clause i" for "ClauseAddr i", and "Arg" for
"ArgAddr i".
Examples:
- OCaml code: "addrC [0; 1]" becomes "addrC [ Subterm 1; Subterm 2]"
"addrC (concl_addr t)" becomes "addrC [ ClauseAddr 0 ]"
or just "addrC concl_addr"
- Command line: "addrC [0; 1]" becomes "addrC [ 1; 2 ]" (I've updated
all the .prla files accordingly). Also one can now type
things like "addrC [Concl; 1]" for the first subterm of the
conclusion, or even things like [2; Concl; Hyp 2; 1] in the
case of nested sequents.