--- 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
--- 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 **)
--- 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)
--- 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}
--- 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
--- 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,