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.
      

Changes  Path
+2 -2 metaprl/support/tactics/auto_tactic.ml
+8 -8 metaprl/support/tactics/dtactic.ml
+2 -2 metaprl/support/tactics/dtactic.mli
+2 -2 metaprl/support/tactics/forward.ml
+5 -5 metaprl/support/tactics/top_conversionals.ml
+1 -1 metaprl/support/tactics/top_conversionals.mli
+61 -93 metaprl/support/tactics/top_options.ml
+4 -9 metaprl/support/tactics/top_options.mli
+2 -4 metaprl/support/tactics/top_resource.mlz
+20 -1 metaprl/tactics/proof/option_sig.ml
+19 -30 metaprl/tactics/proof/tactic_boot.ml
+9 -4 metaprl/tactics/proof/tactic_boot_sig.ml
+4 -2 metaprl/tactics/proof/tacticals_boot.ml
+4 -4 metaprl/theories/itt/core/itt_int_arith.ml
+2 -2 metaprl/theories/itt/core/itt_int_base.ml
+2 -2 metaprl/theories/itt/core/itt_sqsimple.ml
+2 -2 metaprl/theories/itt/core/itt_squash.ml
+2 -2 metaprl/theories/itt/extensions/base/itt_list3.ml
+13 -11 metaprl/theories/itt/reflection/experimental/itt_hoas_relax1.ml
+2 -2 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_bterm2.ml
+2 -2 metaprl/theories/itt/reflection/experimental/itt_hoas_util.ml
+4 -4 metaprl/theories/meta/extensions/meta_dtactic.ml