--- 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
--- 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) =>
--- 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
--- 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
--- 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
--- 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
--- 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)
--- 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
--- 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))
--- 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