# HG changeset patch # User blanchet # Date 1405187644 -7200 # Node ID 278ab871319f4642863729f4da6dd4fd09bafefe # Parent 677b07d777c3caba72c05301c2851e9d864e6c7a# Parent 8840fa17e17c27635846ddc39e67a1cf20cf684a merge diff -r 8840fa17e17c -r 278ab871319f src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML Fri Jul 11 15:52:03 2014 +0200 +++ b/src/HOL/TPTP/atp_problem_import.ML Sat Jul 12 19:54:04 2014 +0200 @@ -62,11 +62,16 @@ end -(** Nitpick (alias Nitrox) **) +(** Nitpick **) fun aptrueprop f ((t0 as @{const Trueprop}) $ t1) = t0 $ f t1 | aptrueprop f t = f t +fun is_legitimate_tptp_def (@{const Trueprop} $ t) = is_legitimate_tptp_def t + | is_legitimate_tptp_def (Const (@{const_name HOL.eq}, _) $ t $ u) = + (is_Const t orelse is_Free t) andalso not (exists_subterm (curry (op =) t) u) + | is_legitimate_tptp_def _ = false + fun nitpick_tptp_file thy timeout file_name = let val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name @@ -74,7 +79,7 @@ val (defs, pseudo_defs) = defs |> map (ATP_Util.abs_extensionalize_term ctxt #> aptrueprop (hol_open_form I)) - |> List.partition (ATP_Util.is_legitimate_tptp_def + |> List.partition (is_legitimate_tptp_def o perhaps (try HOLogic.dest_Trueprop) o ATP_Util.unextensionalize_def) val nondefs = pseudo_defs @ nondefs diff -r 8840fa17e17c -r 278ab871319f src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Jul 11 15:52:03 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Sat Jul 12 19:54:04 2014 +0200 @@ -1275,30 +1275,17 @@ {name = name, stature = stature, role = role, iformula = iformula, atomic_types = atomic_Ts} end -fun is_format_with_defs (THF _) = true - | is_format_with_defs _ = false - -fun make_fact ctxt format type_enc iff_for_eq ((name, stature as (_, status)), t) = - let - val role = - if is_format_with_defs format andalso status = Non_Rec_Def andalso - is_legitimate_tptp_def t then - Definition - else - Axiom - in - (case make_formula ctxt format type_enc iff_for_eq name stature role t of - formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} => - if s = tptp_true then NONE else SOME formula - | formula => SOME formula) - end +fun make_fact ctxt format type_enc iff_for_eq ((name, stature), t) = + (case make_formula ctxt format type_enc iff_for_eq name stature Axiom t of + formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} => + if s = tptp_true then NONE else SOME formula + | formula => SOME formula) fun make_conjecture ctxt format type_enc = map (fn ((name, stature), (role, t)) => - let - val role' = if role <> Conjecture andalso is_legitimate_tptp_def t then Definition else role - val t' = t |> role' = Conjecture ? s_not - in make_formula ctxt format type_enc true name stature role' t' end) + let val t' = t |> role = Conjecture ? s_not in + make_formula ctxt format type_enc true name stature role t' + end) (** Finite and infinite type inference **) diff -r 8840fa17e17c -r 278ab871319f src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Fri Jul 11 15:52:03 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sat Jul 12 19:54:04 2014 +0200 @@ -132,8 +132,7 @@ Type_Infer.param 0 ("'" ^ perhaps (unprefix_and_unascii tvar_prefix) a, (if null clss then @{sort type} else map class_of_atp_class clss)))) end - | typ_of_atp_type ctxt (ty as AFun (a, tys)) = - (typ_of_atp_type ctxt a) --> (typ_of_atp_type ctxt tys) + | typ_of_atp_type ctxt (AFun (a, tys)) = typ_of_atp_type ctxt a --> typ_of_atp_type ctxt tys fun atp_type_of_atp_term (ATerm ((s, _), us)) = AType ((s, []), map atp_type_of_atp_term us) @@ -253,7 +252,7 @@ (case unprefix_and_unascii const_prefix s of SOME s' => let - val ((s', s''), mangled_us) = s' |> unmangled_const |>> `invert_const + val ((s', _), mangled_us) = s' |> unmangled_const |>> `invert_const val num_ty_args = length us - the_default 0 (Symtab.lookup sym_tab s) val (type_us, term_us) = chop num_ty_args us |>> append mangled_us val term_ts = map (do_term NONE) term_us @@ -475,25 +474,11 @@ fun is_axiom_used_in_proof pred = exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false) -fun add_non_rec_defs facts = - fold (fn fact as (_, (_, status)) => status = Non_Rec_Def ? insert (op =) fact) facts - val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg" -val leo2_unfold_def_rule = "unfold_def" fun add_fact ctxt facts ((_, ss), _, _, rule, deps) = - (if rule = leo2_extcnf_equal_neg_rule then + (if member (op =) [agsyhol_core_rule, leo2_extcnf_equal_neg_rule, satallax_core_rule] rule then insert (op =) (short_thm_name ctxt ext, (Global, General)) - else if rule = leo2_unfold_def_rule then - (* 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_non_rec_defs facts - else if rule = agsyhol_core_rule orelse rule = satallax_core_rule then - (fn [] => - (* agsyHOL and Satallax don't include definitions in their unsatisfiable cores, so we - assume the worst and include them all here. *) - [(short_thm_name ctxt ext, (Global, General))] |> add_non_rec_defs facts - | facts => facts) else I) #> (if null deps then union (op =) (resolve_facts facts ss) else I) diff -r 8840fa17e17c -r 278ab871319f src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Fri Jul 11 15:52:03 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Sat Jul 12 19:54:04 2014 +0200 @@ -190,8 +190,6 @@ (* Alt-Ergo *) -val alt_ergo_tff1 = TFF Polymorphic - val alt_ergo_config : atp_config = {exec = K (["WHY3_HOME"], ["why3"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => @@ -205,7 +203,7 @@ prem_role = Hypothesis, best_slices = fn _ => (* FUDGE *) - [(1.0, (((100, ""), alt_ergo_tff1, "poly_native", liftingN, false), ""))], + [(1.0, (((100, ""), TFF Polymorphic, "poly_native", liftingN, false), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} @@ -593,8 +591,6 @@ (* Zipperposition*) -val zipperposition_tff1 = TFF Polymorphic - val zipperposition_config : atp_config = {exec = K (["ZIPPERPOSITION_HOME"], ["zipperposition"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => @@ -605,7 +601,7 @@ prem_role = Hypothesis, best_slices = fn _ => (* FUDGE *) - [(1.0, (((100, ""), alt_ergo_tff1, "poly_native", liftingN, false), ""))], + [(1.0, (((100, ""), TFF Polymorphic, "poly_native", liftingN, false), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} diff -r 8840fa17e17c -r 278ab871319f src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Fri Jul 11 15:52:03 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_util.ML Sat Jul 12 19:54:04 2014 +0200 @@ -45,7 +45,6 @@ val cong_extensionalize_term : theory -> term -> term val abs_extensionalize_term : Proof.context -> term -> term val unextensionalize_def : term -> term - val is_legitimate_tptp_def : term -> bool val transform_elim_prop : term -> term val specialize_type : theory -> (string * typ) -> term -> term val strip_subgoal : thm -> int -> Proof.context -> (string * typ) list * term list * term @@ -382,12 +381,6 @@ | _ => t) | _ => t -fun is_legitimate_tptp_def (@{const Trueprop} $ t) = is_legitimate_tptp_def t - | is_legitimate_tptp_def (Const (@{const_name HOL.eq}, _) $ t $ u) = - (is_Const t orelse is_Free t) andalso - not (exists_subterm (curry (op =) t) u) - | is_legitimate_tptp_def _ = false - (* Converts an elim-rule into an equivalent theorem that does not have the predicate variable. Leaves other theorems unchanged. We simply instantiate the conclusion variable to "False". (Cf. "transform_elim_theorem" in diff -r 8840fa17e17c -r 278ab871319f src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 11 15:52:03 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Jul 12 19:54:04 2014 +0200 @@ -367,7 +367,7 @@ ret (Integer.max 0 (num_facts - max_suggs)) [] end -val number_of_nearest_neighbors = 1 (* FUDGE *) +val initial_number_of_nearest_neighbors = 1 fun k_nearest_neighbors dffreq num_facts num_feats depss featss max_suggs visible_facts goal_feats = let @@ -424,7 +424,7 @@ end fun while1 () = - if !k = number_of_nearest_neighbors then () else (do_k (!k); k := !k + 1; while1 ()) + if !k = initial_number_of_nearest_neighbors then () else (do_k (!k); k := !k + 1; while1 ()) handle EXIT () => () fun while2 () = @@ -478,7 +478,7 @@ end val k_nearest_neighbors_ext = - external_tool ("newknn/knn" ^ " " ^ string_of_int number_of_nearest_neighbors) + external_tool ("newknn/knn" ^ " " ^ string_of_int initial_number_of_nearest_neighbors) val naive_bayes_ext = external_tool "predict/nbayes" fun query_external ctxt algorithm max_suggs learns goal_feats = @@ -583,16 +583,19 @@ string_of_int (fold (Integer.add o length o snd) (Graph.dest G) 0) ^ " edge(s), " ^ string_of_int (length (Graph.maximals G)) ^ " maximal" +type ffds = string vector * int list vector * int list vector +type freqs = int vector * int Inttab.table vector * int vector + type mash_state = {access_G : (proof_kind * string list * string list) Graph.T, xtabs : xtab * xtab, - ffds : string vector * int list vector * int list vector, - freqs : int vector * int Inttab.table vector * int vector, + ffds : ffds, + freqs : freqs, dirty_facts : string list option} val empty_xtabs = (empty_xtab, empty_xtab) -val empty_ffds = (Vector.fromList [], Vector.fromList [], Vector.fromList []) -val empty_freqs = (Vector.fromList [], Vector.fromList [], Vector.fromList []) +val empty_ffds = (Vector.fromList [], Vector.fromList [], Vector.fromList []) : ffds +val empty_freqs = (Vector.fromList [], Vector.fromList [], Vector.fromList []) : freqs val empty_state = {access_G = Graph.empty, @@ -601,8 +604,8 @@ freqs = empty_freqs, dirty_facts = SOME []} : mash_state -fun recompute_ffds_freqs_from_learns learns ((num_facts, fact_tab), (num_feats, feat_tab)) - num_facts0 (fact_names0, featss0, depss0) freqs0 = +fun recompute_ffds_freqs_from_learns (learns : (string * string list * string list) list) + ((num_facts, fact_tab), (num_feats, feat_tab)) num_facts0 (fact_names0, featss0, depss0) freqs0 = let val fact_names = Vector.concat [fact_names0, Vector.fromList (map #1 learns)] val featss = Vector.concat [featss0,