separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
authorwenzelm
Thu Oct 29 16:06:15 2009 +0100 (2009-10-29)
changeset 33308cf62d1690d04
parent 33307 44af0fab4b10
child 33309 5f67433e6dd8
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/HOL/Tools/res_blacklist.ML
     1.1 --- a/src/HOL/HOL.thy	Thu Oct 29 16:05:51 2009 +0100
     1.2 +++ b/src/HOL/HOL.thy	Thu Oct 29 16:06:15 2009 +0100
     1.3 @@ -24,6 +24,7 @@
     1.4    "~~/src/Tools/coherent.ML"
     1.5    "~~/src/Tools/eqsubst.ML"
     1.6    "~~/src/Provers/quantifier1.ML"
     1.7 +  "Tools/res_blacklist.ML"
     1.8    ("Tools/simpdata.ML")
     1.9    "~~/src/Tools/random_word.ML"
    1.10    "~~/src/Tools/atomize_elim.ML"
    1.11 @@ -34,6 +35,7 @@
    1.12  begin
    1.13  
    1.14  setup {* Intuitionistic.method_setup @{binding iprover} *}
    1.15 +setup ResBlacklist.setup
    1.16  
    1.17  
    1.18  subsection {* Primitive logic *}
    1.19 @@ -833,19 +835,14 @@
    1.20    val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]
    1.21  end);
    1.22  
    1.23 -structure BasicClassical: BASIC_CLASSICAL = Classical; 
    1.24 -open BasicClassical;
    1.25 +structure Basic_Classical: BASIC_CLASSICAL = Classical; 
    1.26 +open Basic_Classical;
    1.27  
    1.28  ML_Antiquote.value "claset"
    1.29    (Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())");
    1.30 -
    1.31 -structure ResBlacklist = Named_Thms
    1.32 -  (val name = "noatp" val description = "theorems blacklisted for ATP");
    1.33  *}
    1.34  
    1.35 -text {*ResBlacklist holds theorems blacklisted to sledgehammer. 
    1.36 -  These theorems typically produce clauses that are prolific (match too many equality or
    1.37 -  membership literals) and relate to seldom-used facts. Some duplicate other rules.*}
    1.38 +setup Classical.setup
    1.39  
    1.40  setup {*
    1.41  let
    1.42 @@ -856,8 +853,6 @@
    1.43  in
    1.44    Hypsubst.hypsubst_setup
    1.45    #> ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
    1.46 -  #> Classical.setup
    1.47 -  #> ResBlacklist.setup
    1.48  end
    1.49  *}
    1.50  
     2.1 --- a/src/HOL/IsaMakefile	Thu Oct 29 16:05:51 2009 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Thu Oct 29 16:06:15 2009 +0100
     2.3 @@ -302,6 +302,7 @@
     2.4    Tools/choice_specification.ML \
     2.5    Tools/res_atp.ML \
     2.6    Tools/res_axioms.ML \
     2.7 +  Tools/res_blacklist.ML \
     2.8    Tools/res_clause.ML \
     2.9    Tools/res_hol_clause.ML \
    2.10    Tools/res_reconstruct.ML \
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/res_blacklist.ML	Thu Oct 29 16:06:15 2009 +0100
     3.3 @@ -0,0 +1,43 @@
     3.4 +(*  Title:      HOL/Tools/res_blacklist.ML
     3.5 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.6 +    Author:     Makarius
     3.7 +
     3.8 +Theorems blacklisted to sledgehammer.  These theorems typically
     3.9 +produce clauses that are prolific (match too many equality or
    3.10 +membership literals) and relate to seldom-used facts.  Some duplicate
    3.11 +other rules.
    3.12 +*)
    3.13 +
    3.14 +signature RES_BLACKLIST =
    3.15 +sig
    3.16 +  val setup: theory -> theory
    3.17 +  val blacklisted: Proof.context -> thm -> bool
    3.18 +  val add: attribute
    3.19 +  val del: attribute
    3.20 +end;
    3.21 +
    3.22 +structure ResBlacklist: RES_BLACKLIST =
    3.23 +struct
    3.24 +
    3.25 +structure Data = GenericDataFun
    3.26 +(
    3.27 +  type T = thm Termtab.table;
    3.28 +  val empty = Termtab.empty;
    3.29 +  val extend = I;
    3.30 +  fun merge _ tabs = Termtab.merge (K true) tabs;
    3.31 +);
    3.32 +
    3.33 +fun blacklisted ctxt th =
    3.34 +  Termtab.defined (Data.get (Context.Proof ctxt)) (Thm.full_prop_of th);
    3.35 +
    3.36 +fun add_thm th = Data.map (Termtab.update (Thm.full_prop_of th, th));
    3.37 +fun del_thm th = Data.map (Termtab.delete_safe (Thm.full_prop_of th));
    3.38 +
    3.39 +val add = Thm.declaration_attribute add_thm;
    3.40 +val del = Thm.declaration_attribute del_thm;
    3.41 +
    3.42 +val setup =
    3.43 +  Attrib.setup @{binding noatp} (Attrib.add_del add del) "sledgehammer blacklisting" #>
    3.44 +  PureThy.add_thms_dynamic (@{binding noatp}, map #2 o Termtab.dest o Data.get);
    3.45 +
    3.46 +end;