# HG changeset patch # User bulwahn # Date 1341920708 -7200 # Node ID b16d22bfad07666819c69ae944eddb9cf8ab814b # Parent fcca683838089418a5277e0e0180fafbe2caffc0# Parent 999d6a829c2873e0b7be1b0c177965e51d3bec3b merged diff -r fcca68383808 -r b16d22bfad07 Admin/isatest/isatest-makeall --- a/Admin/isatest/isatest-makeall Mon Jul 09 10:04:07 2012 +0200 +++ b/Admin/isatest/isatest-makeall Tue Jul 10 13:45:08 2012 +0200 @@ -10,8 +10,6 @@ # max time until test is aborted (in sec) MAXTIME=28800 -PUBLISH_TEST="$HOME/home/isabelle-repository/repos/testtool/publish_test.py" - ## diagnostics PRG="$(basename "$0")" @@ -178,16 +176,10 @@ then # test log and cleanup echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 - if [ -x $PUBLISH_TEST ]; then - $PUBLISH_TEST -r $IDENT -s "SUCCESS" -a log $TESTLOG -n Makeall_isatest_$SHORT - fi gzip -f $TESTLOG else # test log echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 - if [ -x $PUBLISH_TEST ]; then - $PUBLISH_TEST -r $IDENT -s "FAIL" -a log $TESTLOG -n Makeall_isatest_$SHORT - fi # error log echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG diff -r fcca68383808 -r b16d22bfad07 Admin/isatest/minimal-test --- a/Admin/isatest/minimal-test Mon Jul 09 10:04:07 2012 +0200 +++ b/Admin/isatest/minimal-test Tue Jul 10 13:45:08 2012 +0200 @@ -15,7 +15,6 @@ LOG="$LOGDIR/test-${DATE}-${HOST}.log" TEST_NAME="minimal-test" -PUBLISH_TEST="/home/isabelle-repository/repos/testtool/publish_test.py" ## diagnostics @@ -48,12 +47,8 @@ ) > "$LOG" 2>&1 if [ "$?" -eq 0 ]; then - [ -x "$PUBLISH_TEST" ] && \ - "$PUBLISH_TEST" -r "$IDENT" -s SUCCESS -a log "$LOG" -n "$TEST_NAME" gzip -f "$LOG" else - [ -x "$PUBLISH_TEST" ] && \ - "$PUBLISH_TEST" -r "$IDENT" -s FAIL -a log "$LOG" -n "$TEST_NAME" fail "Minimal test failed, see $LOG" fi diff -r fcca68383808 -r b16d22bfad07 src/HOL/TPTP/ATP_Theory_Export.thy --- a/src/HOL/TPTP/ATP_Theory_Export.thy Mon Jul 09 10:04:07 2012 +0200 +++ b/src/HOL/TPTP/ATP_Theory_Export.thy Tue Jul 10 13:45:08 2012 +0200 @@ -20,19 +20,49 @@ val ctxt = @{context} *} + +(* MaSh *) + ML {* if do_it then - "/tmp/axs_tc_native.dfg" - |> generate_tptp_inference_file_for_theory ctxt thy (DFG Polymorphic) - "tc_native" + "/tmp/mash_sample_problem.out" + |> generate_mash_problem_file_for_theory thy +else + () +*} + +ML {* +if do_it then + "/tmp/mash_accessibility.out" + |> generate_mash_accessibility_file_for_theory thy false else () *} ML {* if do_it then - "/tmp/infs_poly_guards.tptp" - |> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_guards" + "/tmp/mash_features.out" + |> generate_mash_feature_file_for_theory thy false +else + () +*} + +ML {* +if do_it then + "/tmp/mash_dependencies.out" + |> generate_mash_dependency_file_for_theory thy false +else + () +*} + + +(* TPTP/DFG *) + +ML {* +if do_it then + "/tmp/infs_poly_guards_query_query.tptp" + |> generate_tptp_inference_file_for_theory ctxt thy FOF + "poly_guards_query_query" else () *} @@ -41,14 +71,16 @@ if do_it then "/tmp/infs_poly_tags_query_query.tptp" |> generate_tptp_inference_file_for_theory ctxt thy FOF - "poly_tags_query_query" + "poly_tags_query_query" else () *} ML {* if do_it then - "/tmp/graph.out" |> generate_tptp_graph_file_for_theory ctxt thy + "/tmp/axs_tc_native.dfg" + |> generate_tptp_inference_file_for_theory ctxt thy (DFG Polymorphic) + "tc_native" else () *} diff -r fcca68383808 -r b16d22bfad07 src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Mon Jul 09 10:04:07 2012 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Tue Jul 10 13:45:08 2012 +0200 @@ -2,8 +2,8 @@ Author: Jasmin Blanchette, TU Muenchen Copyright 2011 -Export Isabelle theories as first-order TPTP inferences, exploiting -Sledgehammer's translation. +Export Isabelle theories as MaSh (Machine-learning for Sledgehammer) or as +first-order TPTP inferences. *) signature ATP_THEORY_EXPORT = @@ -12,35 +12,63 @@ val theorems_mentioned_in_proof_term : string list option -> thm -> string list - val generate_tptp_graph_file_for_theory : - Proof.context -> theory -> string -> unit + val generate_mash_accessibility_file_for_theory : + theory -> bool -> string -> unit + val generate_mash_feature_file_for_theory : theory -> bool -> string -> unit + val generate_mash_dependency_file_for_theory : + theory -> bool -> string -> unit + val generate_mash_problem_file_for_theory : theory -> string -> unit val generate_tptp_inference_file_for_theory : Proof.context -> theory -> atp_format -> string -> string -> unit end; -structure ATP_Theory_Export : ATP_THEORY_EXPORT = +structure ATP_Theory_Export (* ### : ATP_THEORY_EXPORT *) = struct open ATP_Problem open ATP_Proof open ATP_Problem_Generate open ATP_Systems +open ATP_Util -val fact_name_of = prefix fact_prefix o ascii_of +fun stringN_of_int 0 _ = "" + | stringN_of_int k n = + stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10) + +fun escape_meta_char c = + if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse + c = #")" then + String.str c + else if c = #"'" then + "~" + else + (* fixed width, in case more digits follow *) + "\\" ^ stringN_of_int 3 (Char.ord c) +val escape_meta = String.translate escape_meta_char + +val fact_name_of = escape_meta +val thy_name_of = escape_meta +val const_name_of = prefix const_prefix o escape_meta +val type_name_of = prefix type_const_prefix o escape_meta +val class_name_of = prefix class_prefix o escape_meta + +val thy_name_of_thm = theory_of_thm #> Context.theory_name + +fun has_thy thy th = (Context.theory_name thy = thy_name_of_thm th) fun facts_of thy = let val ctxt = Proof_Context.init_global thy in - Sledgehammer_Filter.all_facts ctxt false - Symtab.empty true [] [] + Sledgehammer_Filter.all_facts ctxt false Symtab.empty true [] [] (Sledgehammer_Filter.clasimpset_rule_table_of ctxt) |> filter (curry (op =) @{typ bool} o fastype_of o Object_Logic.atomize_term thy o prop_of o snd) + |> rev end (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few fixes that seem to be missing over there; or maybe the two code portions are not doing the same? *) -fun fold_body_thms thm_name all_names f = +fun fold_body_thms thm_name f = let fun app n (PBody {thms, ...}) = thms |> fold (fn (_, (name, prop, body)) => fn x => @@ -48,11 +76,9 @@ val body' = Future.join body val n' = n + (if name = "" orelse - (is_some all_names andalso - not (member (op =) (the all_names) name)) orelse (* uncommon case where the proved theorem occurs twice (e.g., "Transitive_Closure.trancl_into_trancl") *) - n = 1 andalso name = thm_name then + (n = 1 andalso name = thm_name) then 0 else 1) @@ -60,39 +86,222 @@ in (x' |> n = 1 ? f (name, prop, body')) end) in fold (app 0) end -fun theorems_mentioned_in_proof_term all_names thm = +fun theorems_mentioned_in_proof_term all_names th = let - fun collect (s, _, _) = if s <> "" then insert (op =) s else I + val is_name_ok = + case all_names of + SOME names => member (op =) names + | NONE => (fn s => s <> "" andalso not (String.isPrefix "Pure." s)) + fun collect (s, _, _) = is_name_ok s ? insert (op =) s val names = - [] |> fold_body_thms (Thm.get_name_hint thm) all_names collect - [Thm.proof_body_of thm] + [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th] |> map fact_name_of in names end -fun interesting_const_names ctxt = - let val thy = Proof_Context.theory_of ctxt in +fun raw_interesting_const_names thy = + let val ctxt = Proof_Context.init_global thy in Sledgehammer_Filter.const_names_in_fact thy (Sledgehammer_Provers.is_built_in_const_for_prover ctxt eN) end -fun generate_tptp_graph_file_for_theory ctxt thy file_name = +fun interesting_const_names thy = + raw_interesting_const_names thy + #> map const_name_of + #> sort_distinct string_ord + +fun interesting_type_and_class_names t = + let + val bad = [@{type_name prop}, @{type_name bool}, @{type_name fun}] + val add_classes = + subtract (op =) @{sort type} #> map class_name_of #> union (op =) + fun maybe_add_type (Type (s, Ts)) = + (not (member (op =) bad s) ? insert (op =) (type_name_of s)) + #> fold maybe_add_type Ts + | maybe_add_type (TFree (_, S)) = add_classes S + | maybe_add_type (TVar (_, S)) = add_classes S + in [] |> fold_types maybe_add_type t end + +fun theory_ord p = + if Theory.eq_thy p then EQUAL + else if Theory.subthy p then LESS + else if Theory.subthy (swap p) then GREATER + else EQUAL + +val thm_ord = theory_ord o pairself theory_of_thm + +fun parent_thms thy_ths thy = + Theory.parents_of thy + |> map (thy_name_of o Context.theory_name) + |> map_filter (AList.lookup (op =) thy_ths) + |> map List.last + |> map (fact_name_of o Thm.get_name_hint) + +val thms_by_thy = + map (snd #> `thy_name_of_thm) + #> AList.group (op =) + #> sort (int_ord + o pairself (length o Theory.ancestors_of o theory_of_thm o hd o snd)) + #> map (apsnd (sort thm_ord)) + +fun generate_mash_accessibility_file_for_theory thy include_thy file_name = let val path = file_name |> Path.explode val _ = File.write path "" - val axioms = Theory.all_axioms_of thy |> map fst - fun do_thm thm = + fun do_thm th prevs = + let + val s = th ^ ": " ^ space_implode " " prevs ^ "\n" + val _ = File.append path s + in [th] end + val thy_ths = + facts_of thy + |> not include_thy ? filter_out (has_thy thy o snd) + |> thms_by_thy + fun do_thy ths = let - val name = Thm.get_name_hint thm + val thy = theory_of_thm (hd ths) + val parents = parent_thms thy_ths thy + val ths = ths |> map (fact_name_of o Thm.get_name_hint) + val _ = fold do_thm ths parents + in () end + val _ = List.app (do_thy o snd) thy_ths + in () end + +fun has_bool @{typ bool} = true + | has_bool (Type (_, Ts)) = exists has_bool Ts + | has_bool _ = false + +fun has_fun (Type (@{type_name fun}, _)) = true + | has_fun (Type (_, Ts)) = exists has_fun Ts + | has_fun _ = false + +val is_conn = member (op =) + [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj}, + @{const_name HOL.implies}, @{const_name Not}, + @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}, + @{const_name HOL.eq}] + +val has_bool_arg_const = + exists_Const (fn (c, T) => + not (is_conn c) andalso exists has_bool (binder_types T)) + +fun higher_inst_const thy (c, T) = + case binder_types T of + [] => false + | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts + +val binders = [@{const_name All}, @{const_name Ex}] + +fun is_fo_term thy t = + let + val t = + t |> Envir.beta_eta_contract + |> transform_elim_prop + |> Object_Logic.atomize_term thy + in + Term.is_first_order binders t andalso + not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T + | _ => false) t orelse + has_bool_arg_const t orelse exists_Const (higher_inst_const thy) t) + end + +val is_skolem = String.isSubstring Sledgehammer_Filter.pseudo_skolem_prefix +val is_abs = String.isSubstring Sledgehammer_Filter.pseudo_abs_name + +(* TODO: Add types, subterms *) +fun features_of thy (status, th) = + let val prop = Thm.prop_of th in + interesting_const_names thy prop @ + interesting_type_and_class_names prop + |> (fn feats => + case List.partition is_skolem feats of + ([], feats) => feats + | (_, feats) => "skolem" :: feats) + |> (fn feats => + case List.partition is_abs feats of + ([], feats) => feats + | (_, feats) => "abs" :: feats) + |> not (is_fo_term thy prop) ? cons "ho" + |> (case status of + General => I + | Induction => cons "induction" + | Intro => cons "intro" + | Inductive => cons "inductive" + | Elim => cons "elim" + | Simp => cons "simp" + | Def => cons "def") + end + +fun generate_mash_feature_file_for_theory thy include_thy file_name = + let + val path = file_name |> Path.explode + val _ = File.write path "" + val facts = facts_of thy |> not include_thy ? filter_out (has_thy thy o snd) + fun do_fact ((_, (_, status)), th) = + let + val name = Thm.get_name_hint th + val feats = features_of thy (status, th) + val s = fact_name_of name ^ ": " ^ space_implode " " feats ^ "\n" + in File.append path s end + val _ = List.app do_fact facts + in () end + +val dependencies_of = theorems_mentioned_in_proof_term o SOME + +val known_tautologies = + [@{thm All_def}, @{thm Ex_def}, @{thm Ex1_def}, @{thm Ball_def}, + @{thm Bex_def}, @{thm If_def}] + +fun is_likely_tautology thy th = + (member Thm.eq_thm_prop known_tautologies th orelse + th |> prop_of |> raw_interesting_const_names thy + |> forall (is_skolem orf is_abs)) andalso + not (Thm.eq_thm_prop (@{thm ext}, th)) + +fun generate_mash_dependency_file_for_theory thy include_thy file_name = + let + val path = file_name |> Path.explode + val _ = File.write path "" + val ths = + facts_of thy |> not include_thy ? filter_out (has_thy thy o snd) + |> map snd + val all_names = + ths |> filter_out (is_likely_tautology thy) |> map Thm.get_name_hint + fun do_thm th = + let + val name = Thm.get_name_hint th + val deps = dependencies_of all_names th + val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n" + in File.append path s end + val _ = List.app do_thm ths + in () end + +fun generate_mash_problem_file_for_theory thy file_name = + let + val path = file_name |> Path.explode + val _ = File.write path "" + val facts = facts_of thy + val (new_facts, old_facts) = + facts |> List.partition (has_thy thy o snd) + |>> sort (thm_ord o pairself snd) + val ths = facts |> map snd + val all_names = + ths |> filter_out (is_likely_tautology thy) |> map Thm.get_name_hint + fun do_fact ((_, (_, status)), th) prevs = + let + val name = Thm.get_name_hint th + val feats = features_of thy (status, th) + val deps = dependencies_of all_names th + val th = fact_name_of name val s = - "[" ^ Thm.legacy_get_kind thm ^ "] " ^ - (if member (op =) axioms name then "A" else "T") ^ " " ^ - prefix fact_prefix (ascii_of name) ^ ": " ^ - commas (theorems_mentioned_in_proof_term NONE thm) ^ "; " ^ - commas (map (prefix const_prefix o ascii_of) - (interesting_const_names ctxt (Thm.prop_of thm))) ^ " \n" - in File.append path s end - val thms = facts_of thy |> map snd - val _ = map do_thm thms + th ^ ": " ^ + space_implode " " prevs ^ "; " ^ + space_implode " " feats ^ "; " ^ + space_implode " " deps ^ "\n" + val _ = File.append path s + in [th] end + val thy_ths = old_facts |> thms_by_thy + val parents = parent_thms thy_ths thy + val _ = fold do_fact new_facts parents in () end fun inference_term [] = NONE @@ -128,8 +337,9 @@ val ord = effective_term_order ctxt atp val _ = problem |> lines_for_atp_problem format ord (K []) |> File.write_list prob_file + val path = getenv (List.last (fst exec)) ^ "/" ^ snd exec val command = - File.shell_path (Path.explode (getenv (hd (fst exec)) ^ "/" ^ snd exec)) ^ + File.shell_path (Path.explode path) ^ " " ^ arguments ctxt false "" (seconds 1.0) (ord, K [], K []) ^ " " ^ File.shell_path prob_file in @@ -140,13 +350,13 @@ end handle TimeLimit.TimeOut => SOME TimedOut -val likely_tautology_prefixes = +val tautology_prefixes = [@{theory HOL}, @{theory Meson}, @{theory ATP}, @{theory Metis}] |> map (fact_name_of o Context.theory_name) fun is_problem_line_tautology ctxt format (Formula (ident, _, phi, _, _)) = exists (fn prefix => String.isPrefix prefix ident) - likely_tautology_prefixes andalso + tautology_prefixes andalso is_none (run_some_atp ctxt format [(factsN, [Formula (ident, Conjecture, phi, NONE, [])])]) | is_problem_line_tautology _ _ _ = false @@ -193,7 +403,9 @@ val atp_problem = atp_problem |> map (apsnd (filter_out (is_problem_line_tautology ctxt format))) - val all_names = facts |> map (Thm.get_name_hint o snd) + val ths = facts |> map snd + val all_names = + ths |> filter_out (is_likely_tautology thy) |> map Thm.get_name_hint val infers = facts |> map (fn (_, th) => (fact_name_of (Thm.get_name_hint th), diff -r fcca68383808 -r b16d22bfad07 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jul 09 10:04:07 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jul 10 13:45:08 2012 +0200 @@ -196,9 +196,9 @@ val schematic_var_prefix = "V_" val fixed_var_prefix = "v_" val tvar_prefix = "T_" -val tfree_prefix = "t_" +val tfree_prefix = "tf_" val const_prefix = "c_" -val type_const_prefix = "tc_" +val type_const_prefix = "t_" val native_type_prefix = "n_" val class_prefix = "cl_" diff -r fcca68383808 -r b16d22bfad07 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Jul 09 10:04:07 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue Jul 10 13:45:08 2012 +0200 @@ -39,6 +39,8 @@ val trace : bool Config.T val ignore_no_atp : bool Config.T val instantiate_inducts : bool Config.T + val pseudo_abs_name : string + val pseudo_skolem_prefix : string val no_relevance_override : relevance_override val const_names_in_fact : theory -> (string * typ -> term list -> bool * term list) -> term @@ -108,8 +110,8 @@ val no_relevance_override = {add = [], del = [], only = false} val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator -val abs_name = sledgehammer_prefix ^ "abs" -val skolem_prefix = sledgehammer_prefix ^ "sko" +val pseudo_abs_name = sledgehammer_prefix ^ "abs" +val pseudo_skolem_prefix = sledgehammer_prefix ^ "sko" val theory_const_suffix = Long_Name.separator ^ " 1" (* unfolding these can yield really huge terms *) @@ -359,7 +361,7 @@ (* Add a pconstant to the table, but a [] entry means a standard connective, which we ignore.*) fun add_pconst_to_table also_skolem (s, p) = - if (not also_skolem andalso String.isPrefix skolem_prefix s) then I + if (not also_skolem andalso String.isPrefix pseudo_skolem_prefix s) then I else Symtab.map_default (s, [p]) (insert (op =) p) (* Set constants tend to pull in too many irrelevant facts. We limit the damage @@ -393,14 +395,15 @@ (* Since lambdas on the right-hand side of equalities are usually extensionalized later by "abs_extensionalize_term", we don't penalize them here. *) - ? add_pconst_to_table true (abs_name, PType (order_of_type T + 1, []))) + ? add_pconst_to_table true (pseudo_abs_name, + PType (order_of_type T + 1, []))) #> fold (do_term false) (t' :: ts) | (_, ts) => fold (do_term false) ts fun do_quantifier will_surely_be_skolemized abs_T body_t = do_formula pos body_t #> (if also_skolems andalso will_surely_be_skolemized then - add_pconst_to_table true - (Misc_Legacy.gensym skolem_prefix, PType (order_of_type abs_T, [])) + add_pconst_to_table true (pseudo_skolem_prefix ^ serial_string (), + PType (order_of_type abs_T, [])) else I) and do_term_or_formula ext_arg T = @@ -529,9 +532,9 @@ fun generic_pconst_weight local_const_multiplier abs_weight skolem_weight theory_const_weight chained_const_weight weight_for f const_tab chained_const_tab (c as (s, PType (m, _))) = - if s = abs_name then + if s = pseudo_abs_name then abs_weight - else if String.isPrefix skolem_prefix s then + else if String.isPrefix pseudo_skolem_prefix s then skolem_weight else if String.isSuffix theory_const_suffix s then theory_const_weight @@ -571,7 +574,7 @@ | stature_bonus _ _ = 0.0 fun is_odd_const_name s = - s = abs_name orelse String.isPrefix skolem_prefix s orelse + s = pseudo_abs_name orelse String.isPrefix pseudo_skolem_prefix s orelse String.isSuffix theory_const_suffix s fun fact_weight fudge stature const_tab relevant_consts chained_consts