equal
deleted
inserted
replaced
53 fun find_sugg facts sugg = |
53 fun find_sugg facts sugg = |
54 find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts |
54 find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts |
55 fun sugg_facts hyp_ts concl_t facts = |
55 fun sugg_facts hyp_ts concl_t facts = |
56 map_filter (find_sugg facts o of_fact_name) |
56 map_filter (find_sugg facts o of_fact_name) |
57 #> take (max_relevant_slack * the max_relevant) |
57 #> take (max_relevant_slack * the max_relevant) |
58 #> Sledgehammer_Filter.maybe_instantiate_inducts ctxt hyp_ts concl_t |
58 #> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t |
59 #> map (apfst (apfst (fn name => name ()))) |
59 #> map (apfst (apfst (fn name => name ()))) |
60 fun meng_mash_facts fs1 fs2 = |
60 fun meng_mash_facts fs1 fs2 = |
61 let |
61 let |
62 val fact_eq = (op =) o pairself fst |
62 val fact_eq = (op =) o pairself fst |
63 fun score_in f fs = |
63 fun score_in f fs = |
104 val th = |
104 val th = |
105 case find_first (fn (_, th) => Thm.get_name_hint th = name) facts of |
105 case find_first (fn (_, th) => Thm.get_name_hint th = name) facts of |
106 SOME (_, th) => th |
106 SOME (_, th) => th |
107 | NONE => error ("No fact called \"" ^ name ^ "\"") |
107 | NONE => error ("No fact called \"" ^ name ^ "\"") |
108 val deps = dependencies_of all_names th |
108 val deps = dependencies_of all_names th |
109 val goal = goal_of_thm th |
109 val goal = goal_of_thm thy th |
110 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
110 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
111 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
111 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
112 val deps_facts = sugg_facts hyp_ts concl_t facts deps |
112 val deps_facts = sugg_facts hyp_ts concl_t facts deps |
113 val meng_facts = |
113 val meng_facts = |
114 meng_paulson_facts ctxt (max_relevant_slack * the max_relevant) goal |
114 meng_paulson_facts ctxt (max_relevant_slack * the max_relevant) goal |
131 | _ => () |
131 | _ => () |
132 fun total_of heading ok n = |
132 fun total_of heading ok n = |
133 " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^ |
133 " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^ |
134 Real.fmt (StringCvt.FIX (SOME 1)) |
134 Real.fmt (StringCvt.FIX (SOME 1)) |
135 (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)" |
135 (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)" |
136 val inst_inducts = Config.get ctxt Sledgehammer_Filter.instantiate_inducts |
136 val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts |
137 val options = |
137 val options = |
138 [prover_name, string_of_int (the max_relevant) ^ " facts", |
138 [prover_name, string_of_int (the max_relevant) ^ " facts", |
139 "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc, |
139 "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc, |
140 the_default "smart" lam_trans, ATP_Util.string_from_time timeout, |
140 the_default "smart" lam_trans, ATP_Util.string_from_time timeout, |
141 "instantiate_inducts" |> not inst_inducts ? prefix "dont_"] |
141 "instantiate_inducts" |> not inst_inducts ? prefix "dont_"] |