Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-18 11:11:32 -0800 (Wed, 18 Jan 2006)
Revision: 8504
Log message:
Implemented Aleksey's scheme for options.
- Each rule/rewrite gets a set of labels.
They are defined, for example, as follows:
interactive foo {| intro ~labels:[<< foo >>] |} ...
- The "select" resource is an ordered list
opname * option_info, where
option_info =
OptionAllow
| OptionExclude
| OptionIgnore
- A rule is selected as follows, searching down the options
list, for each option:
1. (opname, OptionAllow) when opname in labels
Allowed
2. (opname, OptionExclude) when opname in labels
Rejected
An (opname, OptionIgnore) cancels all previous entries for the opname.
For efficiency, the resource implementation squashes the options list,
removing duplicate and OptionIgnore entries (preserving the semantics).
Note that rules without labels are always allowed.
If you want a rule to be off by default:
declare foo_option
let resource select += << foo_option >>, OptionExclude
interactive foo {| intro ~labels:[<< foo_option >>] |} : ...
You can override later several ways:
1. use the resource, usually private
private let resource select += << foo_option >>, OptionAllow
2. use a tactical locally
BY withAllowOptionT << foo_option >> (...)
3. use a tactic for the rest of the proof
BY addAllowOptionT << foo_option >> (...)
There are other tactics, if you want more control:
addOptionT : term -> string -> tactic
withOptionT : term -> string -> tactic
...
Notes:
- Currently, the withoutOptionT is still defined. It should
probably be defined as
withoutOptionT t =
withOptionT t "ignore"
- It might be nice to label every rule with its name.