# HG changeset patch # User wenzelm # Date 1343054669 -7200 # Node ID 8eaaaf376dc9cfe0813bc38c566693c7ef88d224 # Parent 3c9890c19e901dfbbf418f463366066fc886f1b7# Parent 2d987dad7c3ec573806a4cea7394f1692d3b6aec merged diff -r 2d987dad7c3e -r 8eaaaf376dc9 src/HOL/TPTP/MaSh_Export.thy --- a/src/HOL/TPTP/MaSh_Export.thy Mon Jul 23 16:16:10 2012 +0200 +++ b/src/HOL/TPTP/MaSh_Export.thy Mon Jul 23 16:44:29 2012 +0200 @@ -11,7 +11,7 @@ sledgehammer_params [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??, - lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize] + lam_trans = combs_and_lifting, timeout = 1, dont_preplay, minimize] ML {* open MaSh_Export @@ -66,5 +66,4 @@ () *} - end diff -r 2d987dad7c3e -r 8eaaaf376dc9 src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Mon Jul 23 16:16:10 2012 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Mon Jul 23 16:44:29 2012 +0200 @@ -113,10 +113,6 @@ handle TYPE _ => @{prop True} end -fun all_non_tautological_facts_of thy css_table = - Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table - |> filter_out (Sledgehammer_Fact.is_likely_tautology_or_too_meta o snd) - fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name = let val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt @@ -126,7 +122,8 @@ val mono = not (is_type_enc_polymorphic type_enc) val path = file_name |> Path.explode val _ = File.write path "" - val facts = all_non_tautological_facts_of thy css_table + val facts = + Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table val atp_problem = facts |> map (fn ((_, loc), th) => diff -r 2d987dad7c3e -r 8eaaaf376dc9 src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Mon Jul 23 16:16:10 2012 +0200 +++ b/src/HOL/TPTP/mash_eval.ML Mon Jul 23 16:44:29 2012 +0200 @@ -26,9 +26,7 @@ val max_facts_slack = 2 -val all_names = - filter_out is_likely_tautology_or_too_meta - #> map (rpair () o nickname_of) #> Symtab.make +val all_names = map (rpair () o nickname_of) #> Symtab.make fun evaluate_mash_suggestions ctxt params thy file_name = let diff -r 2d987dad7c3e -r 8eaaaf376dc9 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Mon Jul 23 16:16:10 2012 +0200 +++ b/src/HOL/TPTP/mash_export.ML Mon Jul 23 16:44:29 2012 +0200 @@ -49,9 +49,7 @@ val thy_name_of_fact = hd o Long_Name.explode fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact -val all_names = - filter_out is_likely_tautology_or_too_meta - #> map (rpair () o nickname_of) #> Symtab.make +val all_names = map (rpair () o nickname_of) #> Symtab.make fun generate_accessibility thy include_thy file_name = let diff -r 2d987dad7c3e -r 8eaaaf376dc9 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Mon Jul 23 16:16:10 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Mon Jul 23 16:44:29 2012 +0200 @@ -88,11 +88,13 @@ val isabelle_info : string -> int -> (string, 'a) ho_term list val extract_isabelle_status : (string, 'a) ho_term list -> string option val extract_isabelle_rank : (string, 'a) ho_term list -> int + val inductionN : string val introN : string val inductiveN : string val elimN : string val simpN : string - val defN : string + val non_rec_defN : string + val rec_defN : string val rankN : string val minimum_rank : int val default_rank : int @@ -222,11 +224,14 @@ val isabelle_info_prefix = "isabelle_" +val inductionN = "induction" val introN = "intro" val inductiveN = "inductive" val elimN = "elim" val simpN = "simp" -val defN = "def" +val non_rec_defN = "non_rec_def" +val rec_defN = "rec_def" + val rankN = "rank" val minimum_rank = 0 @@ -503,9 +508,13 @@ fun suffix_tag top_level s = if top_level then case extract_isabelle_status info of - SOME s' => if s' = defN then s ^ ":lt" - else if s' = simpN andalso gen_simp then s ^ ":lr" - else s + SOME s' => + if s' = non_rec_defN then + s ^ ":lt" + else if (s' = simpN orelse s' = rec_defN) andalso gen_simp then + s ^ ":lr" + else + s | NONE => s else s diff -r 2d987dad7c3e -r 8eaaaf376dc9 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jul 23 16:16:10 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jul 23 16:44:29 2012 +0200 @@ -18,7 +18,9 @@ datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter datatype scope = Global | Local | Assum | Chained - datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def + datatype status = + General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | + Rec_Def type stature = scope * status datatype strictness = Strict | Non_Strict @@ -103,6 +105,7 @@ val helper_table : ((string * bool) * (status * thm) list) list val trans_lams_from_string : Proof.context -> type_enc -> string -> term list -> term list * term list + val string_of_status : status -> string val factsN : string val prepare_atp_problem : Proof.context -> atp_format -> formula_role -> type_enc -> mode -> string @@ -123,7 +126,8 @@ datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter datatype scope = Global | Local | Assum | Chained -datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def +datatype status = + General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def type stature = scope * status datatype order = @@ -1236,7 +1240,8 @@ |>> map2 (fn (name, (role, _)) => fn t => (name, (role, t))) facts val lam_facts = map2 (fn t => fn j => - ((lam_fact_prefix ^ Int.toString j, (Global, Def)), (Axiom, t))) + ((lam_fact_prefix ^ Int.toString j, + (Global, Non_Rec_Def)), (Axiom, t))) lambda_ts (1 upto length lambda_ts) in (facts, lam_facts) end @@ -1293,7 +1298,7 @@ ((name, stature as (_, status)), t) = let val role = - if is_format_with_defs format andalso status = Def andalso + if is_format_with_defs format andalso status = Non_Rec_Def andalso is_legitimate_tptp_def t then Definition else @@ -1664,18 +1669,18 @@ (* The Boolean indicates that a fairly sound type encoding is needed. *) val base_helper_table = - [(("COMBI", false), [(Def, @{thm Meson.COMBI_def})]), - (("COMBK", false), [(Def, @{thm Meson.COMBK_def})]), - (("COMBB", false), [(Def, @{thm Meson.COMBB_def})]), - (("COMBC", false), [(Def, @{thm Meson.COMBC_def})]), - (("COMBS", false), [(Def, @{thm Meson.COMBS_def})]), + [(("COMBI", false), [(Non_Rec_Def, @{thm Meson.COMBI_def})]), + (("COMBK", false), [(Non_Rec_Def, @{thm Meson.COMBK_def})]), + (("COMBB", false), [(Non_Rec_Def, @{thm Meson.COMBB_def})]), + (("COMBC", false), [(Non_Rec_Def, @{thm Meson.COMBC_def})]), + (("COMBS", false), [(Non_Rec_Def, @{thm Meson.COMBS_def})]), ((predicator_name, false), [(General, not_ffalse), (General, ftrue)]), (("fFalse", false), [(General, not_ffalse)]), (("fFalse", true), [(General, @{thm True_or_False})]), (("fTrue", false), [(General, ftrue)]), (("fTrue", true), [(General, @{thm True_or_False})]), (("If", true), - [(Def, @{thm if_True}), (Def, @{thm if_False}), + [(Non_Rec_Def, @{thm if_True}), (Non_Rec_Def, @{thm if_False}), (General, @{thm True_or_False})])] val helper_table = @@ -1683,7 +1688,7 @@ [(("fNot", false), @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1] fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]} - |> map (pair Def)), + |> map (pair Non_Rec_Def)), (("fconj", false), @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q" by (unfold fconj_def) fast+} @@ -1718,19 +1723,19 @@ ((app_op_name, true), [(General, @{lemma "EX x. ~ f x = g x | f = g" by blast})]), (("fconj", false), - @{thms fconj_table fconj_laws fdisj_laws} |> map (pair Def)), + @{thms fconj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)), (("fdisj", false), - @{thms fdisj_table fconj_laws fdisj_laws} |> map (pair Def)), + @{thms fdisj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)), (("fimplies", false), @{thms fimplies_table fconj_laws fdisj_laws fimplies_laws} - |> map (pair Def)), + |> map (pair Non_Rec_Def)), (("fequal", false), - (@{thms fequal_table} |> map (pair Def)) @ + (@{thms fequal_table} |> map (pair Non_Rec_Def)) @ (@{thms fequal_laws} |> map (pair General))), (("fAll", false), - @{thms fAll_table fComp_law fAll_law fEx_law} |> map (pair Def)), + @{thms fAll_table fComp_law fAll_law fEx_law} |> map (pair Non_Rec_Def)), (("fEx", false), - @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Def))] + @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Non_Rec_Def))] |> map (apsnd (map (apsnd zero_var_indexes))) fun bound_tvars type_enc sorts Ts = @@ -2104,28 +2109,29 @@ | do_formula pos (AAtom tm) = AAtom (do_term pos tm) in do_formula end +fun string_of_status General = "" + | string_of_status Induction = inductionN + | string_of_status Intro = introN + | string_of_status Inductive = inductiveN + | string_of_status Elim = elimN + | string_of_status Simp = simpN + | string_of_status Non_Rec_Def = non_rec_defN + | string_of_status Rec_Def = rec_defN + (* Each fact is given a unique fact number to avoid name clashes (e.g., because of monomorphization). The TPTP explicitly forbids name clashes, and some of the remote provers might care. *) fun line_for_fact ctxt prefix encode freshen pos mono type_enc rank - (j, {name, stature, role, iformula, atomic_types}) = - (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, role, - iformula - |> formula_from_iformula ctxt mono type_enc should_guard_var_in_formula - (if pos then SOME true else NONE) - |> close_formula_universally - |> bound_tvars type_enc true atomic_types, - NONE, - let val rank = rank j in - case snd stature of - Intro => isabelle_info introN rank - | Inductive => isabelle_info inductiveN rank - | Elim => isabelle_info elimN rank - | Simp => isabelle_info simpN rank - | Def => isabelle_info defN rank - | _ => isabelle_info "" rank - end) - |> Formula + (j, {name, stature = (_, status), role, iformula, atomic_types}) = + Formula (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ + encode name, + role, + iformula + |> formula_from_iformula ctxt mono type_enc + should_guard_var_in_formula (if pos then SOME true else NONE) + |> close_formula_universally + |> bound_tvars type_enc true atomic_types, + NONE, isabelle_info (string_of_status status) (rank j)) fun lines_for_subclass type_enc sub super = Formula (subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, Axiom, @@ -2355,7 +2361,7 @@ Axiom, eq_formula type_enc (atomic_types_of T) [] false (tag_with_type ctxt mono type_enc NONE T x_var) x_var, - NONE, isabelle_info defN helper_rank) + NONE, isabelle_info non_rec_defN helper_rank) end fun lines_for_mono_types ctxt mono type_enc Ts = @@ -2438,7 +2444,7 @@ val tag_with = tag_with_type ctxt mono type_enc NONE fun formula c = [Formula (ident, role, eq (tag_with res_T c) c, NONE, isabelle_info - defN helper_rank)] + non_rec_defN helper_rank)] in if pred_sym orelse not (should_encode_type ctxt mono level res_T) then [] @@ -2538,7 +2544,7 @@ in ([tm1, tm2], [Formula (uncurried_alias_eq_prefix ^ s2, role, eq |> maybe_negate, - NONE, isabelle_info defN helper_rank)]) + NONE, isabelle_info non_rec_defN helper_rank)]) |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I else pair_append (do_alias (ary - 1))) end @@ -2878,8 +2884,9 @@ fun is_conj (role, _) = (role = Conjecture orelse role = Hypothesis) val graph = Graph.empty - |> fold (fold (add_eq_deps (has_status defN)) o snd) problem - |> fold (fold (add_eq_deps (has_status simpN orf is_conj)) o snd) problem + |> fold (fold (add_eq_deps (has_status non_rec_defN)) o snd) problem + |> fold (fold (add_eq_deps (has_status rec_defN orf has_status simpN + orf is_conj)) o snd) problem |> fold (fold (add_intro_deps (has_status inductiveN)) o snd) problem |> fold (fold (add_intro_deps (has_status introN)) o snd) problem fun next_weight w = if w + w <= max_term_order_weight then w + w else w + 1 diff -r 2d987dad7c3e -r 8eaaaf376dc9 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Jul 23 16:16:10 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Jul 23 16:44:29 2012 +0200 @@ -200,10 +200,11 @@ else isa_ext -fun add_all_defs fact_names accum = +fun add_non_rec_defs fact_names accum = Vector.foldl (fn (facts, facts') => - union (op =) (filter (fn (_, (_, status)) => status = Def) facts) + union (op =) + (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts) facts') accum fact_names @@ -214,12 +215,12 @@ (* LEO 1.3.3 does not record definitions properly, leading to missing dependencies in the TSTP proof. Remove the next line once this is fixed. *) - add_all_defs fact_names + add_non_rec_defs fact_names else if rule = satallax_unsat_coreN then (fn [] => (* Satallax doesn't include definitions in its unsatisfiable cores, so we assume the worst and include them all here. *) - [(ext_name ctxt, (Global, General))] |> add_all_defs fact_names + [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names | facts => facts) else I) diff -r 2d987dad7c3e -r 8eaaaf376dc9 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Jul 23 16:16:10 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Jul 23 16:44:29 2012 +0200 @@ -23,7 +23,6 @@ val fact_from_ref : Proof.context -> unit Symtab.table -> thm list -> status Termtab.table -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list - val is_likely_tautology_or_too_meta : thm -> bool val backquote_thm : thm -> string val clasimpset_rule_table_of : Proof.context -> status Termtab.table val maybe_instantiate_inducts : @@ -50,8 +49,6 @@ del : (Facts.ref * Attrib.src list) list, only : bool} -val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator - (* experimental features *) val ignore_no_atp = Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false) @@ -147,10 +144,11 @@ fun multi_base_blacklist ctxt ho_atp = ["defs", "select_defs", "update_defs", "split", "splits", "split_asm", "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong", - "weak_case_cong"] + "weak_case_cong", "nibble_pair_of_char_simps", "nibble.simps", + "nibble.distinct"] |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ? append ["induct", "inducts"] - |> map (prefix ".") + |> map (prefix Long_Name.separator) val max_lambda_nesting = 3 (*only applies if not ho_atp*) @@ -162,12 +160,11 @@ (* Don't count nested lambdas at the level of formulas, since they are quantifiers. *) -fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*) - | formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) = - formula_has_too_many_lambdas false (T :: Ts) t - | formula_has_too_many_lambdas _ Ts t = +fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) = + formula_has_too_many_lambdas (T :: Ts) t + | formula_has_too_many_lambdas Ts t = if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then - exists (formula_has_too_many_lambdas false Ts) (#2 (strip_comb t)) + exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t)) else term_has_too_many_lambdas max_lambda_nesting t @@ -180,11 +177,17 @@ | apply_depth _ = 0 fun is_formula_too_complex ho_atp t = - apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas ho_atp [] t + apply_depth t > max_apply_depth orelse + (not ho_atp andalso formula_has_too_many_lambdas [] t) -(* FIXME: Extend to "Meson" and "Metis" *) +(* These theories contain auxiliary facts that could positively confuse + Sledgehammer if they were included. *) +val sledgehammer_prefixes = + ["ATP", "Meson", "Metis", "Sledgehammer"] |> map (suffix Long_Name.separator) + val exists_sledgehammer_const = - exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) + exists_Const (fn (s, _) => + exists (fn pref => String.isPrefix pref s) sledgehammer_prefixes) (* FIXME: make more reliable *) val exists_low_level_class_const = @@ -192,25 +195,11 @@ s = @{const_name equal_class.equal} orelse String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s) -fun is_metastrange_theorem th = - case head_of (concl_of th) of - Const (s, _) => (s <> @{const_name Trueprop} andalso - s <> @{const_name "=="}) - | _ => false - fun is_that_fact th = String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th) andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN | _ => false) (prop_of th) -fun is_theorem_bad_for_atps ho_atp thm = - is_metastrange_theorem thm orelse - let val t = prop_of thm in - is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse - exists_sledgehammer_const t orelse exists_low_level_class_const t orelse - is_that_fact thm - end - fun is_likely_tautology_or_too_meta th = let val is_boring_const = member (op =) atp_widely_irrelevant_consts @@ -229,6 +218,15 @@ is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th)) end +fun is_theorem_bad_for_atps ho_atp th = + is_likely_tautology_or_too_meta th orelse + let val t = prop_of th in + is_formula_too_complex ho_atp t orelse + exists_type type_has_top_sort t orelse + exists_sledgehammer_const t orelse exists_low_level_class_const t orelse + is_that_fact th + end + fun hackish_string_for_term thy t = Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) (Syntax.string_of_term_global thy) t @@ -299,8 +297,8 @@ |> maps (snd o snd) in Termtab.empty |> add Simp [atomize] snd simps - |> add Simp [] I rec_defs - |> add Def [] I nonrec_defs + |> add Rec_Def [] I rec_defs + |> add Non_Rec_Def [] I nonrec_defs (* Add once it is used: |> add Elim [] I elims *) @@ -458,7 +456,6 @@ else let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in all_facts ctxt ho_atp reserved add chained css - |> filter_out (is_likely_tautology_or_too_meta o snd) |> filter_out (member Thm.eq_thm_prop del o snd) |> maybe_filter_no_atps ctxt |> uniquify diff -r 2d987dad7c3e -r 8eaaaf376dc9 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jul 23 16:16:10 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jul 23 16:44:29 2012 +0200 @@ -29,7 +29,7 @@ open Sledgehammer_MaSh open Sledgehammer_Run -val cvc3N = "cvc3" +(* val cvc3N = "cvc3" *) val yicesN = "yices" val z3N = "z3" @@ -226,7 +226,7 @@ (* The first ATP of the list is used by Auto Sledgehammer. Because of the low timeout, it makes sense to put E first. *) fun default_provers_param_value ctxt = - [eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN, cvc3N] + [eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN] |> map_filter (remotify_prover_if_not_installed ctxt) |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (), max_default_remote_threads) @@ -404,11 +404,11 @@ else (); mash_learn ctxt (get_params Normal ctxt - (("timeout", - [string_of_real default_learn_atp_timeout]) :: + ([("timeout", + [string_of_real default_learn_atp_timeout]), + ("slice", ["false"])] @ override_params @ - [("slice", ["false"]), - ("minimize", ["true"]), + [("minimize", ["true"]), ("preplay_timeout", ["0"])])) fact_override (#facts (Proof.goal state)) (subcommand = learn_atpN orelse subcommand = relearn_atpN)) diff -r 2d987dad7c3e -r 8eaaaf376dc9 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Jul 23 16:16:10 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Jul 23 16:44:29 2012 +0200 @@ -59,7 +59,7 @@ val mash_can_suggest_facts : Proof.context -> bool val mash_suggested_facts : Proof.context -> params -> string -> int -> term list -> term - -> ('a * thm) list -> (('a * thm) * real) list * ('a * thm) list + -> fact list -> (fact * real) list * fact list val mash_learn_proof : Proof.context -> params -> string -> term -> ('a * thm) list -> thm list -> unit @@ -106,7 +106,7 @@ getenv "ISABELLE_HOME_USER" ^ "/mash" |> tap (Isabelle_System.mkdir o Path.explode) val mash_state_dir = mash_model_dir -fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode +fun mash_state_file () = mash_state_dir () ^ "/state" (*** Isabelle helpers ***) @@ -312,25 +312,44 @@ |> forall is_lambda_free ts ? cons "no_lams" |> forall (not o exists_Const is_exists) ts ? cons "no_skos" |> scope <> Global ? cons "local" - |> (case status of - General => I - | Induction => cons "induction" - | Intro => cons "intro" - | Inductive => cons "inductive" - | Elim => cons "elim" - | Simp => cons "simp" - | Def => cons "def") + |> (case string_of_status status of "" => I | s => cons s) (* Too many dependencies is a sign that a decision procedure is at work. There isn't much too learn from such proofs. *) -val max_dependencies = 10 +val max_dependencies = 20 val atp_dependency_default_max_fact = 50 -fun trim_dependencies deps = - if length deps <= max_dependencies then SOME deps else NONE +(* "type_definition_xxx" facts are characterized by their use of "CollectI". *) +val typedef_deps = [@{thm CollectI} |> nickname_of] + +(* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *) +val typedef_ths = + @{thms type_definition.Abs_inverse type_definition.Rep_inverse + type_definition.Rep type_definition.Rep_inject + type_definition.Abs_inject type_definition.Rep_cases + type_definition.Abs_cases type_definition.Rep_induct + type_definition.Abs_induct type_definition.Rep_range + type_definition.Abs_image} + |> map nickname_of -fun isar_dependencies_of all_names = - thms_in_proof (SOME all_names) #> trim_dependencies +fun is_size_def [dep] th = + (case first_field ".recs" dep of + SOME (pref, _) => + (case first_field ".size" (nickname_of th) of + SOME (pref', _) => pref = pref' + | NONE => false) + | NONE => false) + | is_size_def _ _ = false + +fun trim_dependencies th deps = + if length deps > max_dependencies orelse deps = typedef_deps orelse + exists (member (op =) typedef_ths) deps orelse is_size_def deps th then + NONE + else + SOME deps + +fun isar_dependencies_of all_names th = + th |> thms_in_proof (SOME all_names) |> trim_dependencies th fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover auto_level facts all_names th = @@ -376,7 +395,7 @@ end else (); - used_facts |> map fst |> trim_dependencies) + used_facts |> map fst |> trim_dependencies th) | _ => NONE end @@ -385,11 +404,11 @@ (* more friendly than "try o File.rm" for those who keep the files open in their text editor *) -fun wipe_out file = File.write file "" +fun wipe_out_file file = File.write (Path.explode file) "" -fun write_file (xs, f) file = +fun write_file heading (xs, f) file = let val path = Path.explode file in - wipe_out path; + File.write path heading; xs |> chunk_list 500 |> List.app (File.append path o space_implode "" o map f) end @@ -411,8 +430,8 @@ mash_home () ^ "/mash --quiet --outputDir " ^ mash_model_dir () ^ " --log " ^ log_file ^ " " ^ core ^ " >& " ^ err_file in - write_file ([], K "") sugg_file; - write_file write_cmds cmd_file; + write_file "" ([], K "") sugg_file; + write_file "" write_cmds cmd_file; trace_msg ctxt (fn () => "Running " ^ command); Isabelle_System.bash command; read_suggs (fn () => try File.read_lines (Path.explode sugg_file) |> these) @@ -422,8 +441,7 @@ | SOME "" => "Done" | SOME s => "Error: " ^ elide_string 1000 s)) |> not overlord - ? tap (fn _ => List.app (wipe_out o Path.explode) - [err_file, sugg_file, cmd_file]) + ? tap (fn _ => List.app wipe_out_file [err_file, sugg_file, cmd_file]) end fun str_of_add (name, parents, feats, deps) = @@ -506,7 +524,7 @@ fun load _ (state as (true, _)) = state | load ctxt _ = - let val path = mash_state_path () in + let val path = mash_state_file () |> Path.explode in (true, case try File.read_lines path of SOME (version' :: node_lines) => @@ -531,15 +549,13 @@ fun save ctxt {fact_G} = let - val path = mash_state_path () - fun fact_line_for name parents = - escape_meta name ^ ": " ^ escape_metas parents - val append_fact = File.append path o suffix "\n" oo fact_line_for - fun append_entry (name, ((), (parents, _))) () = - append_fact name (Graph.Keys.dest parents) + fun str_of_entry (name, parents) = + escape_meta name ^ ": " ^ escape_metas parents ^ "\n" + fun append_entry (name, ((), (parents, _))) = + cons (name, Graph.Keys.dest parents) + val entries = [] |> Graph.fold append_entry fact_G in - File.write path (version ^ "\n"); - Graph.fold append_entry fact_G (); + write_file (version ^ "\n") (entries, str_of_entry) (mash_state_file ()); trace_msg ctxt (fn () => "Saved fact graph (" ^ graph_info fact_G ^ ")") end @@ -551,12 +567,17 @@ fun mash_map ctxt f = Synchronized.change global_state (load ctxt ##> (f #> tap (save ctxt))) +fun mash_peek ctxt f = + Synchronized.change_result global_state (load ctxt #> `snd #>> f) + fun mash_get ctxt = Synchronized.change_result global_state (load ctxt #> `snd) fun mash_unlearn ctxt = Synchronized.change global_state (fn _ => - (mash_CLEAR ctxt; wipe_out (mash_state_path ()); (true, empty_state))) + (mash_CLEAR ctxt; + wipe_out_file (mash_state_file ()); + (true, empty_state))) end @@ -598,28 +619,43 @@ (* Generate more suggestions than requested, because some might be thrown out later for various reasons and "meshing" gives better results with some slack. *) -fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts) +fun max_suggs_of max_facts = max_facts + Int.min (50, max_facts) fun is_fact_in_graph fact_G (_, th) = can (Graph.get_node fact_G) (nickname_of th) +fun interleave 0 _ _ = [] + | interleave n [] ys = take n ys + | interleave n xs [] = take n xs + | interleave 1 (x :: _) _ = [x] + | interleave n (x :: xs) (y :: ys) = x :: y :: interleave (n - 2) xs ys + fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts concl_t facts = let val thy = Proof_Context.theory_of ctxt - val fact_G = #fact_G (mash_get ctxt) - val parents = maximal_in_graph fact_G facts - val feats = features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts) - val suggs = - if Graph.is_empty fact_G then [] - else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats) - val selected = + val (fact_G, suggs) = + mash_peek ctxt (fn {fact_G} => + if Graph.is_empty fact_G then + (fact_G, []) + else + let + val parents = maximal_in_graph fact_G facts + val feats = + features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts) + in + (fact_G, mash_QUERY ctxt overlord (max_suggs_of max_facts) + (parents, feats)) + end) + val sels = facts |> suggested_facts suggs (* The weights currently returned by "mash.py" are too extreme to make any sense. *) - |> map fst |> weight_mepo_facts - val unknown = facts |> filter_out (is_fact_in_graph fact_G) - in (selected, unknown) end + |> map fst + val (unk_global, unk_local) = + facts |> filter_out (is_fact_in_graph fact_G) + |> List.partition (fn ((_, (scope, _)), _) => scope = Global) + in (interleave max_facts unk_local sels |> weight_mepo_facts, unk_global) end fun add_to_fact_graph ctxt (name, parents, feats, deps) (adds, graph) = let @@ -638,7 +674,7 @@ val hard_timeout = time_mult learn_timeout_slack timeout val birth_time = Time.now () val death_time = Time.+ (birth_time, hard_timeout) - val desc = ("machine learner for Sledgehammer", "") + val desc = ("Machine learner for Sledgehammer", "") in Async_Manager.launch MaShN birth_time death_time desc task end fun freshish_name () = @@ -656,12 +692,22 @@ val name = freshish_name () val feats = features_of ctxt prover thy (Local, General) [t] val deps = used_ths |> map nickname_of - val {fact_G} = mash_get ctxt - val parents = maximal_in_graph fact_G facts in - mash_ADD ctxt overlord [(name, parents, feats, deps)]; (true, "") + mash_peek ctxt (fn {fact_G} => + let val parents = maximal_in_graph fact_G facts in + mash_ADD ctxt overlord [(name, parents, feats, deps)] + end); + (true, "") end) +val evil_theories = + ["Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Nitpick", + "New_DSequence", "New_Random_Sequence", "Quickcheck", + "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence", "SMT"] + +fun fact_has_evil_theory (_, th) = + member (op =) evil_theories (Context.theory_name (theory_of_thm th)) + fun sendback sub = Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub) @@ -676,7 +722,8 @@ Time.+ (Timer.checkRealTimer timer, commit_timeout) val {fact_G} = mash_get ctxt val (old_facts, new_facts) = - facts |> List.partition (is_fact_in_graph fact_G) + facts |> filter_out fact_has_evil_theory + |> List.partition (is_fact_in_graph fact_G) ||> sort (thm_ord o pairself snd) in if null new_facts andalso (not atp orelse null old_facts) then @@ -691,15 +738,14 @@ else let val all_names = - facts |> map snd - |> filter_out is_likely_tautology_or_too_meta - |> map (rpair () o nickname_of) - |> Symtab.make - val deps_of = - if atp then - atp_dependencies_of ctxt params prover auto_level facts all_names + facts |> map snd |> map (rpair () o nickname_of) |> Symtab.make + fun deps_of status th = + if status = Non_Rec_Def orelse status = Rec_Def then + SOME [] + else if atp then + atp_dependencies_of ctxt params prover auto_level facts all_names th else - isar_dependencies_of all_names + isar_dependencies_of all_names th fun do_commit [] [] state = state | do_commit adds reps {fact_G} = let @@ -727,13 +773,13 @@ else ()) fun learn_new_fact _ (accum as (_, (_, _, _, true))) = accum - | learn_new_fact ((_, stature), th) + | learn_new_fact ((_, stature as (_, status)), th) (adds, (parents, n, next_commit, _)) = let val name = nickname_of th val feats = features_of ctxt prover (theory_of_thm th) stature [prop_of th] - val deps = deps_of th |> these + val deps = deps_of status th |> these val n = n |> not (null deps) ? Integer.add 1 val adds = (name, parents, feats, deps) :: adds val (adds, next_commit) = @@ -759,11 +805,12 @@ |> fold learn_new_fact new_facts in commit true adds []; n end fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum - | relearn_old_fact (_, th) (reps, (n, next_commit, _)) = + | relearn_old_fact ((_, (_, status)), th) + (reps, (n, next_commit, _)) = let val name = nickname_of th val (n, reps) = - case deps_of th of + case deps_of status th of SOME deps => (n + 1, (name, deps) :: reps) | NONE => (n, reps) val (reps, next_commit) = @@ -774,7 +821,7 @@ val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout) in (reps, (n, next_commit, timed_out)) end val n = - if null old_facts then + if not atp orelse null old_facts then n else let