1.1 --- a/src/HOL/TPTP/MaSh_Export.thy Thu Jul 26 10:48:03 2012 +0200
1.2 +++ b/src/HOL/TPTP/MaSh_Export.thy Thu Jul 26 10:48:03 2012 +0200
1.3 @@ -23,9 +23,10 @@
1.4 val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
1.5 val prover = hd provers
1.6 *}
1.7 +
1.8 ML {*
1.9 if do_it then
1.10 - generate_accessibility thy false "/tmp/mash_accessibility"
1.11 + generate_accessibility @{context} thy false "/tmp/mash_accessibility"
1.12 else
1.13 ()
1.14 *}
1.15 @@ -39,7 +40,7 @@
1.16
1.17 ML {*
1.18 if do_it then
1.19 - generate_isar_dependencies thy false "/tmp/mash_dependencies"
1.20 + generate_isar_dependencies @{context} thy false "/tmp/mash_dependencies"
1.21 else
1.22 ()
1.23 *}
2.1 --- a/src/HOL/TPTP/mash_export.ML Thu Jul 26 10:48:03 2012 +0200
2.2 +++ b/src/HOL/TPTP/mash_export.ML Thu Jul 26 10:48:03 2012 +0200
2.3 @@ -37,6 +37,12 @@
2.4 fun has_thy thy th =
2.5 Context.theory_name thy = Context.theory_name (theory_of_thm th)
2.6
2.7 +fun all_non_technical_facts ctxt thy =
2.8 + let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in
2.9 + all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
2.10 + |> filter_out (is_thm_technical o snd)
2.11 + end
2.12 +
2.13 fun parent_facts thy thy_map =
2.14 let
2.15 fun add_last thy =
2.16 @@ -65,9 +71,8 @@
2.17 val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n"
2.18 val _ = File.append path s
2.19 in [fact] end
2.20 - val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
2.21 val thy_map =
2.22 - all_facts ctxt false Symtab.empty [] [] css
2.23 + all_non_technical_facts ctxt thy
2.24 |> not include_thy ? filter_out (has_thy thy o snd)
2.25 |> thy_map_from_facts
2.26 fun do_thy facts =
2.27 @@ -81,9 +86,8 @@
2.28 let
2.29 val path = file_name |> Path.explode
2.30 val _ = File.write path ""
2.31 - val css = clasimpset_rule_table_of ctxt
2.32 val facts =
2.33 - all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
2.34 + all_non_technical_facts ctxt thy
2.35 |> not include_thy ? filter_out (has_thy thy o snd)
2.36 fun do_fact ((_, stature), th) =
2.37 let
2.38 @@ -98,9 +102,8 @@
2.39 let
2.40 val path = file_name |> Path.explode
2.41 val _ = File.write path ""
2.42 - val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
2.43 val ths =
2.44 - all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
2.45 + all_non_technical_facts ctxt thy
2.46 |> not include_thy ? filter_out (has_thy thy o snd)
2.47 |> map snd
2.48 val all_names = all_names ths
2.49 @@ -118,9 +121,8 @@
2.50 val path = file_name |> Path.explode
2.51 val _ = File.write path ""
2.52 val prover = hd provers
2.53 - val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
2.54 val facts =
2.55 - all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
2.56 + all_non_technical_facts ctxt thy
2.57 |> not include_thy ? filter_out (has_thy thy o snd)
2.58 val ths = facts |> map snd
2.59 val all_names = all_names ths
2.60 @@ -137,9 +139,7 @@
2.61 val path = file_name |> Path.explode
2.62 val _ = File.write path ""
2.63 val prover = hd provers
2.64 - val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
2.65 - val facts =
2.66 - all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
2.67 + val facts = all_non_technical_facts ctxt thy
2.68 val (new_facts, old_facts) =
2.69 facts |> List.partition (has_thy thy o snd)
2.70 |>> sort (thm_ord o pairself snd)
2.71 @@ -168,9 +168,7 @@
2.72 val path = file_name |> Path.explode
2.73 val _ = File.write path ""
2.74 val prover = hd provers
2.75 - val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
2.76 - val facts =
2.77 - all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
2.78 + val facts = all_non_technical_facts ctxt thy
2.79 val (new_facts, old_facts) =
2.80 facts |> List.partition (has_thy thy o snd)
2.81 |>> sort (thm_ord o pairself snd)
3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jul 26 10:48:03 2012 +0200
3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jul 26 10:48:03 2012 +0200
3.3 @@ -45,6 +45,7 @@
3.4 val atp_dependencies_of :
3.5 Proof.context -> params -> string -> int -> fact list -> unit Symtab.table
3.6 -> thm -> 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 @@ -399,6 +400,14 @@
3.12 | _ => NONE
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 @@ -700,14 +709,6 @@
3.27 (true, "")
3.28 end)
3.29
3.30 -val evil_theories =
3.31 - ["Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Nitpick",
3.32 - "New_DSequence", "New_Random_Sequence", "Quickcheck",
3.33 - "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence", "SMT"]
3.34 -
3.35 -fun fact_has_evil_theory (_, th) =
3.36 - member (op =) evil_theories (Context.theory_name (theory_of_thm th))
3.37 -
3.38 fun sendback sub =
3.39 Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub)
3.40
3.41 @@ -722,7 +723,7 @@
3.42 Time.+ (Timer.checkRealTimer timer, commit_timeout)
3.43 val {fact_G} = mash_get ctxt
3.44 val (old_facts, new_facts) =
3.45 - facts |> filter_out fact_has_evil_theory
3.46 + facts |> filter_out (is_thm_technical o snd)
3.47 |> List.partition (is_fact_in_graph fact_G)
3.48 ||> sort (thm_ord o pairself snd)
3.49 in