equal
deleted
inserted
replaced
44 in [name] end |
44 in [name] end |
45 val thy_ths = old_facts |> thms_by_thy |
45 val thy_ths = old_facts |> thms_by_thy |
46 val parents = parent_thms thy_ths thy |
46 val parents = parent_thms thy_ths thy |
47 in fold do_fact new_facts parents; () end |
47 in fold do_fact new_facts parents; () end |
48 |
48 |
49 fun generate_iter_suggestions ctxt params thy max_relevant file_name = |
49 fun generate_iter_suggestions ctxt (params as {provers, ...}) thy max_relevant |
|
50 file_name = |
50 let |
51 let |
51 val path = file_name |> Path.explode |
52 val path = file_name |> Path.explode |
52 val _ = File.write path "" |
53 val _ = File.write path "" |
53 val facts = all_non_tautological_facts_of thy |
54 val facts = all_non_tautological_facts_of thy |
54 val (new_facts, old_facts) = |
55 val (new_facts, old_facts) = |
56 |>> sort (thm_ord o pairself snd) |
57 |>> sort (thm_ord o pairself snd) |
57 fun do_fact (fact as (_, th)) old_facts = |
58 fun do_fact (fact as (_, th)) old_facts = |
58 let |
59 let |
59 val name = Thm.get_name_hint th |
60 val name = Thm.get_name_hint th |
60 val goal = goal_of_thm thy th |
61 val goal = goal_of_thm thy th |
|
62 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
61 val kind = Thm.legacy_get_kind th |
63 val kind = Thm.legacy_get_kind th |
62 val _ = |
64 val _ = |
63 if kind <> "" then |
65 if kind <> "" then |
64 let |
66 let |
65 val suggs = |
67 val suggs = |
66 old_facts |> iter_facts ctxt params max_relevant goal |
68 old_facts |
67 |> map (fn ((name, _), _) => fact_name_of (name ())) |
69 |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params |
68 |> sort string_ord |
70 (hd provers) max_relevant NONE hyp_ts concl_t |
|
71 |> map (fn ((name, _), _) => fact_name_of (name ())) |
|
72 |> sort string_ord |
69 val s = fact_name_of name ^ ": " ^ space_implode " " suggs ^ "\n" |
73 val s = fact_name_of name ^ ": " ^ space_implode " " suggs ^ "\n" |
70 in File.append path s end |
74 in File.append path s end |
71 else |
75 else |
72 () |
76 () |
73 in fact :: old_facts end |
77 in fact :: old_facts end |