34 let |
34 let |
35 val name = Thm.get_name_hint th |
35 val name = Thm.get_name_hint th |
36 val feats = features_of thy status [prop_of th] |
36 val feats = features_of thy status [prop_of th] |
37 val deps = isabelle_dependencies_of all_names th |
37 val deps = isabelle_dependencies_of all_names th |
38 val kind = Thm.legacy_get_kind th |
38 val kind = Thm.legacy_get_kind th |
39 val name = fact_name_of name |
|
40 val core = |
39 val core = |
41 space_implode " " prevs ^ "; " ^ space_implode " " feats |
40 space_implode " " prevs ^ "; " ^ space_implode " " feats |
42 val query = if kind <> "" then "? " ^ core ^ "\n" else "" |
41 val query = if kind <> "" then "? " ^ core ^ "\n" else "" |
43 val update = |
42 val update = |
44 "! " ^ name ^ ": " ^ core ^ "; " ^ space_implode " " deps ^ "\n" |
43 "! " ^ escape_meta name ^ ": " ^ core ^ "; " ^ |
|
44 space_implode " " deps ^ "\n" |
45 val _ = File.append path (query ^ update) |
45 val _ = File.append path (query ^ update) |
46 in [name] end |
46 in [name] end |
47 val thy_ths = old_facts |> thms_by_thy |
47 val thy_facts = old_facts |> thy_facts_from_thms |
48 val parents = parent_facts thy_ths thy |
48 val parents = parent_facts thy thy_facts |
49 in fold do_fact new_facts parents; () end |
49 in fold do_fact new_facts parents; () end |
50 |
50 |
51 fun generate_iter_suggestions ctxt (params as {provers, ...}) thy max_relevant |
51 fun generate_iter_suggestions ctxt (params as {provers, ...}) thy max_relevant |
52 file_name = |
52 file_name = |
53 let |
53 let |
69 let |
69 let |
70 val suggs = |
70 val suggs = |
71 old_facts |
71 old_facts |
72 |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params |
72 |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params |
73 (hd provers) max_relevant NONE hyp_ts concl_t |
73 (hd provers) max_relevant NONE hyp_ts concl_t |
74 |> map (fn ((name, _), _) => fact_name_of (name ())) |
74 |> map (fn ((name, _), _) => name ()) |
75 |> sort string_ord |
75 |> sort string_ord |
76 val s = fact_name_of name ^ ": " ^ space_implode " " suggs ^ "\n" |
76 val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n" |
77 in File.append path s end |
77 in File.append path s end |
78 else |
78 else |
79 () |
79 () |
80 in fact :: old_facts end |
80 in fact :: old_facts end |
81 in fold do_fact new_facts old_facts; () end |
81 in fold do_fact new_facts old_facts; () end |