rule out same "technical" theories for MePo as for MaSh
authorblanchet
Fri Aug 03 17:56:35 2012 +0200 (2012-08-03 ago)
changeset 48667ac58317ef11f
parent 48666 0ba2e9be9f20
child 48668 5d63c23b4042
rule out same "technical" theories for MePo as for MaSh
src/HOL/TPTP/mash_export.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
     1.1 --- a/src/HOL/TPTP/mash_export.ML	Fri Aug 03 17:56:35 2012 +0200
     1.2 +++ b/src/HOL/TPTP/mash_export.ML	Fri Aug 03 17:56:35 2012 +0200
     1.3 @@ -37,10 +37,10 @@
     1.4  fun has_thy thy th =
     1.5    Context.theory_name thy = Context.theory_name (theory_of_thm th)
     1.6  
     1.7 -fun all_non_technical_facts ctxt thy =
     1.8 +fun all_facts ctxt thy =
     1.9    let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in
    1.10 -    all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
    1.11 -    |> filter_out (is_thm_technical o snd)
    1.12 +    nearly_all_facts (Proof_Context.init_global thy) false no_fact_override
    1.13 +                     Symtab.empty css [] [] @{prop True}
    1.14    end
    1.15  
    1.16  fun parent_facts thy thy_map =
    1.17 @@ -67,7 +67,7 @@
    1.18          val _ = File.append path s
    1.19        in [fact] end
    1.20      val thy_map =
    1.21 -      all_non_technical_facts ctxt thy
    1.22 +      all_facts ctxt thy
    1.23        |> not include_thy ? filter_out (has_thy thy o snd)
    1.24        |> thy_map_from_facts
    1.25      fun do_thy facts =
    1.26 @@ -82,7 +82,7 @@
    1.27      val path = file_name |> Path.explode
    1.28      val _ = File.write path ""
    1.29      val facts =
    1.30 -      all_non_technical_facts ctxt thy
    1.31 +      all_facts ctxt thy
    1.32        |> not include_thy ? filter_out (has_thy thy o snd)
    1.33      fun do_fact ((_, stature), th) =
    1.34        let
    1.35 @@ -98,7 +98,7 @@
    1.36      val path = file_name |> Path.explode
    1.37      val _ = File.write path ""
    1.38      val ths =
    1.39 -      all_non_technical_facts ctxt thy
    1.40 +      all_facts ctxt thy
    1.41        |> not include_thy ? filter_out (has_thy thy o snd)
    1.42        |> map snd
    1.43      val all_names = all_names ths
    1.44 @@ -117,7 +117,7 @@
    1.45      val _ = File.write path ""
    1.46      val prover = hd provers
    1.47      val facts =
    1.48 -      all_non_technical_facts ctxt thy
    1.49 +      all_facts ctxt thy
    1.50        |> not include_thy ? filter_out (has_thy thy o snd)
    1.51      val ths = facts |> map snd
    1.52      val all_names = all_names ths
    1.53 @@ -136,7 +136,7 @@
    1.54      val path = file_name |> Path.explode
    1.55      val _ = File.write path ""
    1.56      val prover = hd provers
    1.57 -    val facts = all_non_technical_facts ctxt thy
    1.58 +    val facts = all_facts ctxt thy
    1.59      val (new_facts, old_facts) =
    1.60        facts |> List.partition (has_thy thy o snd)
    1.61              |>> sort (thm_ord o pairself snd)
    1.62 @@ -167,7 +167,7 @@
    1.63      val path = file_name |> Path.explode
    1.64      val _ = File.write path ""
    1.65      val prover = hd provers
    1.66 -    val facts = all_non_technical_facts ctxt thy
    1.67 +    val facts = all_facts ctxt thy
    1.68      val (new_facts, old_facts) =
    1.69        facts |> List.partition (has_thy thy o snd)
    1.70              |>> sort (thm_ord o pairself snd)
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Aug 03 17:56:35 2012 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Aug 03 17:56:35 2012 +0200
     2.3 @@ -182,14 +182,17 @@
     2.4    apply_depth t > max_apply_depth orelse
     2.5    (not ho_atp andalso formula_has_too_many_lambdas [] t)
     2.6  
     2.7 -(* These theories contain auxiliary facts that could positively confuse
     2.8 -   Sledgehammer if they were included. *)
     2.9 -val sledgehammer_prefixes =
    2.10 -  ["ATP", "Meson", "Metis", "Sledgehammer"] |> map (suffix Long_Name.separator)
    2.11 +(* FIXME: Ad hoc list *)
    2.12 +val technical_prefixes =
    2.13 +  ["ATP", "Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Meson",
    2.14 +   "Metis", "Nitpick", "New_DSequence", "New_Random_Sequence", "Quickcheck",
    2.15 +   "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence",
    2.16 +   "Sledgehammer", "SMT"]
    2.17 +  |> map (suffix Long_Name.separator)
    2.18  
    2.19 -val exists_sledgehammer_const =
    2.20 -  exists_Const (fn (s, _) =>
    2.21 -      exists (fn pref => String.isPrefix pref s) sledgehammer_prefixes)
    2.22 +fun has_technical_prefix s =
    2.23 +  exists (fn pref => String.isPrefix pref s) technical_prefixes
    2.24 +val exists_technical_const = exists_Const (has_technical_prefix o fst)
    2.25  
    2.26  (* FIXME: make more reliable *)
    2.27  val exists_low_level_class_const =
    2.28 @@ -224,9 +227,8 @@
    2.29    is_likely_tautology_or_too_meta th orelse
    2.30    let val t = prop_of th in
    2.31      is_formula_too_complex ho_atp t orelse
    2.32 -    exists_type type_has_top_sort t orelse
    2.33 -    exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
    2.34 -    is_that_fact th
    2.35 +    exists_type type_has_top_sort t orelse exists_technical_const t orelse
    2.36 +    exists_low_level_class_const t orelse is_that_fact th
    2.37    end
    2.38  
    2.39  fun hackish_string_for_term thy t =
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Aug 03 17:56:35 2012 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Aug 03 17:56:35 2012 +0200
     3.3 @@ -45,7 +45,6 @@
     3.4    val atp_dependencies_of :
     3.5      Proof.context -> params -> string -> int -> fact list -> unit Symtab.table
     3.6      -> thm -> bool * string list option
     3.7 -  val is_thm_technical : thm -> bool
     3.8    val mash_CLEAR : Proof.context -> unit
     3.9    val mash_ADD :
    3.10      Proof.context -> bool
    3.11 @@ -402,14 +401,6 @@
    3.12        | _ => (false, isar_deps)
    3.13      end
    3.14  
    3.15 -val technical_theories =
    3.16 -  ["Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Nitpick",
    3.17 -   "New_DSequence", "New_Random_Sequence", "Quickcheck",
    3.18 -   "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence", "SMT"]
    3.19 -
    3.20 -val is_thm_technical =
    3.21 -  member (op =) technical_theories o Context.theory_name o theory_of_thm
    3.22 -
    3.23  
    3.24  (*** Low-level communication with MaSh ***)
    3.25  
    3.26 @@ -727,8 +718,7 @@
    3.27        Time.+ (Timer.checkRealTimer timer, commit_timeout)
    3.28      val {fact_G} = mash_get ctxt
    3.29      val (old_facts, new_facts) =
    3.30 -      facts |> filter_out (is_thm_technical o snd)
    3.31 -            |> List.partition (is_fact_in_graph fact_G)
    3.32 +      facts |> List.partition (is_fact_in_graph fact_G)
    3.33              ||> sort (thm_ord o pairself snd)
    3.34    in
    3.35      if null new_facts andalso (not atp orelse null old_facts) then