35 fun do_fact fact prevs = |
35 fun do_fact fact prevs = |
36 let |
36 let |
37 val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n" |
37 val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n" |
38 val _ = File.append path s |
38 val _ = File.append path s |
39 in [fact] end |
39 in [fact] end |
40 val thy_facts = |
40 val thy_map = |
41 all_non_tautological_facts_of thy Termtab.empty |
41 all_facts_of thy Termtab.empty |
42 |> not include_thy ? filter_out (has_thy thy o snd) |
42 |> not include_thy ? filter_out (has_thy thy o snd) |
43 |> thy_facts_from_thms |
43 |> thy_map_from_facts |
44 fun do_thy facts = |
44 fun do_thy facts = |
45 let |
45 let |
46 val thy = thy_of_fact thy (hd facts) |
46 val thy = thy_of_fact thy (hd facts) |
47 val parents = parent_facts thy thy_facts |
47 val parents = parent_facts thy thy_map |
48 in fold do_fact facts parents; () end |
48 in fold do_fact facts parents; () end |
49 in Symtab.fold (fn (_, facts) => K (do_thy facts)) thy_facts () end |
49 in fold_rev (fn (_, facts) => K (do_thy facts)) thy_map () end |
50 |
50 |
51 fun generate_features ctxt thy include_thy file_name = |
51 fun generate_features ctxt thy include_thy file_name = |
52 let |
52 let |
53 val path = file_name |> Path.explode |
53 val path = file_name |> Path.explode |
54 val _ = File.write path "" |
54 val _ = File.write path "" |
55 val css_table = clasimpset_rule_table_of ctxt |
55 val css_table = clasimpset_rule_table_of ctxt |
56 val facts = |
56 val facts = |
57 all_non_tautological_facts_of thy css_table |
57 all_facts_of thy css_table |
58 |> not include_thy ? filter_out (has_thy thy o snd) |
58 |> not include_thy ? filter_out (has_thy thy o snd) |
59 fun do_fact ((_, (_, status)), th) = |
59 fun do_fact ((_, (_, status)), th) = |
60 let |
60 let |
61 val name = Thm.get_name_hint th |
61 val name = Thm.get_name_hint th |
62 val feats = features_of (theory_of_thm th) status [prop_of th] |
62 val feats = features_of (theory_of_thm th) status [prop_of th] |
67 fun generate_isa_dependencies thy include_thy file_name = |
67 fun generate_isa_dependencies thy include_thy file_name = |
68 let |
68 let |
69 val path = file_name |> Path.explode |
69 val path = file_name |> Path.explode |
70 val _ = File.write path "" |
70 val _ = File.write path "" |
71 val ths = |
71 val ths = |
72 all_non_tautological_facts_of thy Termtab.empty |
72 all_facts_of thy Termtab.empty |
73 |> not include_thy ? filter_out (has_thy thy o snd) |
73 |> not include_thy ? filter_out (has_thy thy o snd) |
74 |> map snd |
74 |> map snd |
75 val all_names = ths |> map Thm.get_name_hint |
75 val all_names = |
|
76 ths |> filter_out (is_likely_tautology orf is_too_meta) |
|
77 |> map Thm.get_name_hint |
76 fun do_thm th = |
78 fun do_thm th = |
77 let |
79 let |
78 val name = Thm.get_name_hint th |
80 val name = Thm.get_name_hint th |
79 val deps = isabelle_dependencies_of all_names th |
81 val deps = isabelle_dependencies_of all_names th |
80 val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" |
82 val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" |
85 include_thy file_name = |
87 include_thy file_name = |
86 let |
88 let |
87 val path = file_name |> Path.explode |
89 val path = file_name |> Path.explode |
88 val _ = File.write path "" |
90 val _ = File.write path "" |
89 val facts = |
91 val facts = |
90 all_non_tautological_facts_of thy Termtab.empty |
92 all_facts_of thy Termtab.empty |
91 |> not include_thy ? filter_out (has_thy thy o snd) |
93 |> not include_thy ? filter_out (has_thy thy o snd) |
92 val ths = facts |> map snd |
94 val ths = facts |> map snd |
93 val all_names = ths |> map Thm.get_name_hint |
95 val all_names = |
|
96 ths |> filter_out (is_likely_tautology orf is_too_meta) |
|
97 |> map Thm.get_name_hint |
94 fun is_dep dep (_, th) = Thm.get_name_hint th = dep |
98 fun is_dep dep (_, th) = Thm.get_name_hint th = dep |
95 fun add_isa_dep facts dep accum = |
99 fun add_isa_dep facts dep accum = |
96 if exists (is_dep dep) accum then |
100 if exists (is_dep dep) accum then |
97 accum |
101 accum |
98 else case find_first (is_dep dep) facts of |
102 else case find_first (is_dep dep) facts of |
131 fun generate_commands ctxt thy file_name = |
135 fun generate_commands ctxt thy file_name = |
132 let |
136 let |
133 val path = file_name |> Path.explode |
137 val path = file_name |> Path.explode |
134 val _ = File.write path "" |
138 val _ = File.write path "" |
135 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
139 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
136 val facts = all_non_tautological_facts_of thy css_table |
140 val facts = all_facts_of thy css_table |
137 val (new_facts, old_facts) = |
141 val (new_facts, old_facts) = |
138 facts |> List.partition (has_thy thy o snd) |
142 facts |> List.partition (has_thy thy o snd) |
139 |>> sort (thm_ord o pairself snd) |
143 |>> sort (thm_ord o pairself snd) |
140 val ths = facts |> map snd |
144 val ths = facts |> map snd |
141 val all_names = ths |> map Thm.get_name_hint |
145 val all_names = |
|
146 ths |> filter_out (is_likely_tautology orf is_too_meta) |
|
147 |> map Thm.get_name_hint |
142 fun do_fact ((_, (_, status)), th) prevs = |
148 fun do_fact ((_, (_, status)), th) prevs = |
143 let |
149 let |
144 val name = Thm.get_name_hint th |
150 val name = Thm.get_name_hint th |
145 val feats = features_of thy status [prop_of th] |
151 val feats = features_of thy status [prop_of th] |
146 val deps = isabelle_dependencies_of all_names th |
152 val deps = isabelle_dependencies_of all_names th |
150 val update = |
156 val update = |
151 "! " ^ escape_meta name ^ ": " ^ core ^ "; " ^ |
157 "! " ^ escape_meta name ^ ": " ^ core ^ "; " ^ |
152 escape_metas deps ^ "\n" |
158 escape_metas deps ^ "\n" |
153 val _ = File.append path (query ^ update) |
159 val _ = File.append path (query ^ update) |
154 in [name] end |
160 in [name] end |
155 val thy_facts = old_facts |> thy_facts_from_thms |
161 val thy_map = old_facts |> thy_map_from_facts |
156 val parents = parent_facts thy thy_facts |
162 val parents = parent_facts thy thy_map |
157 in fold do_fact new_facts parents; () end |
163 in fold do_fact new_facts parents; () end |
158 |
164 |
159 fun generate_iter_suggestions ctxt (params as {provers, ...}) thy max_relevant |
165 fun generate_iter_suggestions ctxt (params as {provers, ...}) thy max_relevant |
160 file_name = |
166 file_name = |
161 let |
167 let |
162 val path = file_name |> Path.explode |
168 val path = file_name |> Path.explode |
163 val _ = File.write path "" |
169 val _ = File.write path "" |
164 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
170 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
165 val facts = all_non_tautological_facts_of thy css_table |
171 val facts = all_facts_of thy css_table |
166 val (new_facts, old_facts) = |
172 val (new_facts, old_facts) = |
167 facts |> List.partition (has_thy thy o snd) |
173 facts |> List.partition (has_thy thy o snd) |
168 |>> sort (thm_ord o pairself snd) |
174 |>> sort (thm_ord o pairself snd) |
169 fun do_fact (fact as (_, th)) old_facts = |
175 fun do_fact (fact as (_, th)) old_facts = |
170 let |
176 let |