# HG changeset patch # User blanchet # Date 1406897037 -7200 # Node ID 2df9ed24114fe06139f3a8bbd0a27a0032d53dd4 # Parent c21e7bdb40ad4dd1efd90d92d4ecf79cf0ed85eb whitespace tuning diff -r c21e7bdb40ad -r 2df9ed24114f src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Aug 01 14:43:57 2014 +0200 @@ -100,9 +100,8 @@ else Local val may_be_induction = - exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) => - body_type T = @{typ bool} - | _ => false) + exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) => body_type T = @{typ bool} + | _ => false) (* TODO: get rid of *) fun normalize_vars t = @@ -117,14 +116,12 @@ fun norm (t $ u) = norm t ##>> norm u #>> op $ | norm (Const (s, T)) = normT T #>> curry Const s - | norm (Var (z as (_, T))) = - normT T + | norm (Var (z as (_, T))) = normT T #> (fn (T, (accumT, (known, n))) => - (case find_index (equal z) known of - ~1 => (Var ((Name.uu, n), T), (accumT, (z :: known, n + 1))) - | j => (Var ((Name.uu, n - j - 1), T), (accumT, (known, n))))) - | norm (Abs (_, T, t)) = - norm t ##>> normT T #>> (fn (t, T) => Abs (Name.uu, T, t)) + (case find_index (equal z) known of + ~1 => (Var ((Name.uu, n), T), (accumT, (z :: known, n + 1))) + | j => (Var ((Name.uu, n - j - 1), T), (accumT, (known, n))))) + | norm (Abs (_, T, t)) = norm t ##>> normT T #>> (fn (t, T) => Abs (Name.uu, T, t)) | norm (Bound j) = pair (Bound j) | norm (Free (s, T)) = normT T #>> curry Free s in fst (norm t (([], 0), ([], 0))) end @@ -162,50 +159,43 @@ fun fact_of_ref ctxt reserved chained css (xthm as (xref, args)) = let val ths = Attrib.eval_thms ctxt [xthm] - val bracket = - map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args - |> implode + val bracket = implode (map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args) fun nth_name j = (case xref of Facts.Fact s => backquote (simplify_spaces (unyxml s)) ^ bracket | Facts.Named (("", _), _) => "[" ^ bracket ^ "]" - | Facts.Named ((name, _), NONE) => - make_name reserved (length ths > 1) (j + 1) name ^ bracket + | Facts.Named ((name, _), NONE) => make_name reserved (length ths > 1) (j + 1) name ^ bracket | Facts.Named ((name, _), SOME intervals) => make_name reserved true (nth (maps (explode_interval (length ths)) intervals) j) name ^ bracket) fun add_nth th (j, rest) = let val name = nth_name j in - (j + 1, ((name, stature_of_thm false [] chained css name th), th) - :: rest) + (j + 1, ((name, stature_of_thm false [] chained css name th), th) :: rest) end in (0, []) |> fold add_nth ths |> snd end -(* Reject theorems with names like "List.filter.filter_list_def" or - "Accessible_Part.acc.defs", as these are definitions arising from packages. *) +(* Reject theorems with names like "List.filter.filter_list_def" or "Accessible_Part.acc.defs", as + these are definitions arising from packages. *) fun is_package_def s = let val ss = Long_Name.explode s in length ss > 2 andalso not (hd ss = "local") andalso exists (fn suf => String.isSuffix suf s) - ["_case_def", "_rec_def", "_size_def", "_size_overloaded_def"] + ["_case_def", "_rec_def", "_size_def", "_size_overloaded_def"] end (* FIXME: put other record thms here, or declare as "no_atp" *) fun multi_base_blacklist ctxt ho_atp = - ["defs", "select_defs", "update_defs", "split", "splits", "split_asm", - "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong", - "weak_case_cong", "nat_of_char_simps", "nibble.simps", + ["defs", "select_defs", "update_defs", "split", "splits", "split_asm", "ext_cases", "eq.simps", + "eq.refl", "nchotomy", "case_cong", "weak_case_cong", "nat_of_char_simps", "nibble.simps", "nibble.distinct"] - |> not (ho_atp orelse Config.get ctxt instantiate_inducts) ? - append ["induct", "inducts"] + |> not (ho_atp orelse Config.get ctxt instantiate_inducts) ? append ["induct", "inducts"] |> map (prefix Long_Name.separator) -(* The maximum apply depth of any "metis" call in "Metis_Examples" (on - 2007-10-31) was 11. *) +(* The maximum apply depth of any "metis" call in "Metis_Examples" (back in 2007) was 11. *) val max_apply_depth = 18 fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1) @@ -216,23 +206,20 @@ (* FIXME: Ad hoc list *) val technical_prefixes = - ["ATP", "Code_Evaluation", "Datatype", "Enum", "Lazy_Sequence", - "Limited_Sequence", "Meson", "Metis", "Nitpick", - "Quickcheck_Random", "Quickcheck_Exhaustive", "Quickcheck_Narrowing", + ["ATP", "Code_Evaluation", "Datatype", "Enum", "Lazy_Sequence", "Limited_Sequence", "Meson", + "Metis", "Nitpick", "Quickcheck_Random", "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence", "Sledgehammer", "SMT"] |> map (suffix Long_Name.separator) -fun is_technical_const (s, _) = - exists (fn pref => String.isPrefix pref s) technical_prefixes +fun is_technical_const s = exists (fn pref => String.isPrefix pref s) technical_prefixes (* FIXME: make more reliable *) val sep_class_sep = Long_Name.separator ^ "class" ^ Long_Name.separator -fun is_low_level_class_const (s, _) = +fun is_low_level_class_const s = s = @{const_name equal_class.equal} orelse String.isSubstring sep_class_sep s val sep_that = Long_Name.separator ^ Obtain.thatN - val skolem_thesis = Name.skolem Auto_Bind.thesisN fun is_that_fact th = @@ -258,11 +245,11 @@ | is_interesting_subterm _ = false fun interest_of_bool t = - if exists_Const (is_technical_const orf is_low_level_class_const orf - type_has_top_sort o snd) t then + if exists_Const ((is_technical_const o fst) orf (is_low_level_class_const o fst) orf + type_has_top_sort o snd) t then Deal_Breaker else if exists_type (exists_subtype (curry (op =) @{typ prop})) t orelse - not (exists_subterm is_interesting_subterm t) then + not (exists_subterm is_interesting_subterm t) then Boring else Interesting @@ -280,8 +267,7 @@ val t = prop_of th in - (interest_of_prop [] t <> Interesting andalso - not (Thm.eq_thm_prop (@{thm ext}, th))) orelse + (interest_of_prop [] t <> Interesting andalso not (Thm.eq_thm_prop (@{thm ext}, th))) orelse is_that_fact th end @@ -296,19 +282,18 @@ prefixes of all free variables. In the worse case scenario, where the fact won't be resolved correctly, the user can fix it manually, e.g., by giving a name to the offending fact. *) -fun all_prefixes_of s = - map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1) +fun all_prefixes_of s = map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1) fun close_form t = (t, [] |> Term.add_free_names t |> maps all_prefixes_of) |> fold (fn ((s, i), T) => fn (t', taken) => - let val s' = singleton (Name.variant_list taken) s in - ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const - else Logic.all_const) T - $ Abs (s', T, abstract_over (Var ((s, i), T), t')), - s' :: taken) - end) - (Term.add_vars t [] |> sort_wrt (fst o fst)) + let val s' = singleton (Name.variant_list taken) s in + ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const + else Logic.all_const) T + $ Abs (s', T, abstract_over (Var ((s, i), T), t')), + s' :: taken) + end) + (Term.add_vars t [] |> sort_wrt (fst o fst)) |> fst fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote @@ -321,26 +306,23 @@ Termtab.empty else let - fun add stature th = - Termtab.update (normalize_vars (prop_of th), stature) + fun add stature th = Termtab.update (normalize_vars (prop_of th), stature) - val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} = - ctxt |> claset_of |> Classical.rep_cs + val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} = ctxt |> claset_of |> Classical.rep_cs val intros = Item_Net.content safeIs @ Item_Net.content hazIs (* Add once it is used: - val elims = - Item_Net.content safeEs @ Item_Net.content hazEs + val elims = Item_Net.content safeEs @ Item_Net.content hazEs |> map Classical.classical_rule *) - val specs = ctxt |> Spec_Rules.get - val (rec_defs, nonrec_defs) = - specs |> filter (curry (op =) Spec_Rules.Equational o fst) - |> maps (snd o snd) - |> filter_out (member Thm.eq_thm_prop risky_defs) - |> List.partition (is_rec_def o prop_of) - val spec_intros = - specs |> filter (member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive] o fst) - |> maps (snd o snd) + val specs = Spec_Rules.get ctxt + val (rec_defs, nonrec_defs) = specs + |> filter (curry (op =) Spec_Rules.Equational o fst) + |> maps (snd o snd) + |> filter_out (member Thm.eq_thm_prop risky_defs) + |> List.partition (is_rec_def o prop_of) + val spec_intros = specs + |> filter (member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive] o fst) + |> maps (snd o snd) in Termtab.empty |> fold (add Simp o snd) simps @@ -357,7 +339,7 @@ fun normalize_eq (@{const Trueprop} $ (t as (t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2)) = if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t else t0 $ t2 $ t1 | normalize_eq (@{const Trueprop} $ (t as @{const Not} - $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) = + $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) = if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t else HOLogic.mk_not (t0 $ t2 $ t1) | normalize_eq (Const (@{const_name Pure.eq}, Type (_, [T, _])) $ t1 $ t2) = (if Term_Ord.fast_term_ord (t1, t2) <> GREATER then (t1, t2) else (t2, t1)) @@ -397,8 +379,7 @@ fun struct_induct_rule_on th = (case Logic.strip_horn (prop_of th) of - (prems, @{const Trueprop} - $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) => + (prems, @{const Trueprop} $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) => if not (is_TVar ind_T) andalso length prems > 1 andalso exists (exists_subterm (curry (op aconv) p)) prems andalso not (exists (exists_subterm (curry (op aconv) a)) prems) then @@ -415,13 +396,14 @@ if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T) | varify_noninducts t = t - val p_inst = - concl_prop |> map_aterms varify_noninducts |> close_form - |> lambda (Free ind_x) - |> hackish_string_of_term ctxt + val p_inst = concl_prop + |> map_aterms varify_noninducts + |> close_form + |> lambda (Free ind_x) + |> hackish_string_of_term ctxt in - ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", - stature), th |> Rule_Insts.read_instantiate ctxt [((p_name, 0), p_inst)] []) + ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", stature), + th |> Rule_Insts.read_instantiate ctxt [((p_name, 0), p_inst)] []) end fun type_match thy (T1, T2) = @@ -435,7 +417,7 @@ stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T)) |> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout - (instantiate_induct_rule ctxt stmt p_name ax))) + (instantiate_induct_rule ctxt stmt p_name ax))) end | NONE => [ax]) @@ -450,7 +432,9 @@ (hyp_ts |> filter_out (null o external_frees), concl_t) |> Logic.list_implies |> Object_Logic.atomize_term thy val ind_stmt_xs = external_frees ind_stmt - in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end + in + maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) + end else I @@ -463,10 +447,8 @@ val thy = Proof_Context.theory_of ctxt val global_facts = Global_Theory.facts_of thy val is_too_complex = - if generous orelse fact_count global_facts >= max_facts_for_complex_check then - K false - else - is_too_complex + if generous orelse fact_count global_facts >= max_facts_for_complex_check then K false + else is_too_complex val local_facts = Proof_Context.facts_of ctxt val named_locals = local_facts |> Facts.dest_static true [global_facts] val assms = Assumption.all_assms_of ctxt @@ -478,8 +460,7 @@ val unnamed_locals = union Thm.eq_thm_prop (Facts.props local_facts) chained |> filter is_good_unnamed_local |> map (pair "" o single) - val full_space = - Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts) + val full_space = Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts) val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp fun add_facts global foldx facts = @@ -531,12 +512,12 @@ end)) ths (n, accum)) end) in - (* The single-theorem names go before the multiple-theorem ones (e.g., - "xxx" vs. "xxx(3)"), so that single names are preferred when both are - available. *) - `I [] |> add_facts false fold local_facts (unnamed_locals @ named_locals) - |> add_facts true Facts.fold_static global_facts global_facts - |> op @ + (* The single-theorem names go before the multiple-theorem ones (e.g., "xxx" vs. "xxx(3)"), so + that single names are preferred when both are available. *) + `I [] + |> add_facts false fold local_facts (unnamed_locals @ named_locals) + |> add_facts true Facts.fold_static global_facts global_facts + |> op @ end fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts concl_t = @@ -544,13 +525,11 @@ [] else let - val chained = - chained - |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th]) + val chained = chained |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th]) in (if only then maps (map (fn ((name, stature), th) => ((K name, stature), th)) - o fact_of_ref ctxt reserved chained css) add + o fact_of_ref ctxt reserved chained css) add else let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del)