100 |> map snd |
100 |> map snd |
101 val all_names = all_names ths |
101 val all_names = all_names ths |
102 fun do_thm th = |
102 fun do_thm th = |
103 let |
103 let |
104 val name = nickname_of th |
104 val name = nickname_of th |
105 val deps = isabelle_dependencies_of all_names th |
105 val deps = isar_dependencies_of all_names th |
106 val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" |
106 val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" |
107 in File.append path s end |
107 in File.append path s end |
108 in List.app do_thm ths end |
108 in List.app do_thm ths end |
109 |
109 |
110 fun generate_atp_dependencies ctxt (params as {provers, max_facts, ...}) thy |
110 fun generate_atp_dependencies ctxt (params as {provers, ...}) thy include_thy |
111 include_thy file_name = |
111 file_name = |
112 let |
112 let |
113 val path = file_name |> Path.explode |
113 val path = file_name |> Path.explode |
114 val _ = File.write path "" |
114 val _ = File.write path "" |
115 val prover = hd provers |
115 val prover = hd provers |
116 val facts = |
116 val facts = |
117 all_facts_of thy Termtab.empty |
117 all_facts_of thy Termtab.empty |
118 |> not include_thy ? filter_out (has_thy thy o snd) |
118 |> not include_thy ? filter_out (has_thy thy o snd) |
119 val ths = facts |> map snd |
119 val ths = facts |> map snd |
120 val all_names = all_names ths |
120 val all_names = all_names ths |
121 fun is_dep dep (_, th) = nickname_of th = dep |
|
122 fun add_isar_dep facts dep accum = |
|
123 if exists (is_dep dep) accum then |
|
124 accum |
|
125 else case find_first (is_dep dep) facts of |
|
126 SOME ((name, status), th) => accum @ [((name, status), th)] |
|
127 | NONE => accum (* shouldn't happen *) |
|
128 fun fix_name ((_, stature), th) = ((fn () => nickname_of th, stature), th) |
|
129 fun do_thm th = |
121 fun do_thm th = |
130 let |
122 let |
131 val name = nickname_of th |
123 val name = nickname_of th |
132 val goal = goal_of_thm thy th |
|
133 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
|
134 val deps = |
124 val deps = |
135 case isabelle_dependencies_of all_names th of |
125 atp_dependencies_of ctxt params prover false facts all_names th |
136 [] => [] |
|
137 | isar_dep as [_] => isar_dep (* can hardly beat that *) |
|
138 | isar_deps => |
|
139 let |
|
140 val facts = |
|
141 facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
|
142 val facts = |
|
143 facts |> iterative_relevant_facts ctxt params prover |
|
144 (the max_facts) NONE hyp_ts concl_t |
|
145 |> fold (add_isar_dep facts) isar_deps |
|
146 |> map fix_name |
|
147 in |
|
148 case run_prover_for_mash ctxt params prover facts goal of |
|
149 {outcome = NONE, used_facts, ...} => |
|
150 used_facts |> map fst |> sort string_ord |
|
151 | _ => isar_deps |
|
152 end |
|
153 val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" |
126 val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" |
154 in File.append path s end |
127 in File.append path s end |
155 in List.app do_thm ths end |
128 in List.app do_thm ths end |
156 |
129 |
157 fun generate_commands ctxt prover thy file_name = |
130 fun generate_commands ctxt prover thy file_name = |
167 val all_names = all_names ths |
140 val all_names = all_names ths |
168 fun do_fact ((_, stature), th) prevs = |
141 fun do_fact ((_, stature), th) prevs = |
169 let |
142 let |
170 val name = nickname_of th |
143 val name = nickname_of th |
171 val feats = features_of ctxt prover thy stature [prop_of th] |
144 val feats = features_of ctxt prover thy stature [prop_of th] |
172 val deps = isabelle_dependencies_of all_names th |
145 val deps = isar_dependencies_of all_names th |
173 val kind = Thm.legacy_get_kind th |
146 val kind = Thm.legacy_get_kind th |
174 val core = escape_metas prevs ^ "; " ^ escape_metas feats |
147 val core = escape_metas prevs ^ "; " ^ escape_metas feats |
175 val query = if kind <> "" then "? " ^ core ^ "\n" else "" |
148 val query = if kind <> "" then "? " ^ core ^ "\n" else "" |
176 val update = |
149 val update = |
177 "! " ^ escape_meta name ^ ": " ^ core ^ "; " ^ |
150 "! " ^ escape_meta name ^ ": " ^ core ^ "; " ^ |
205 val suggs = |
178 val suggs = |
206 old_facts |
179 old_facts |
207 |> Sledgehammer_MePo.iterative_relevant_facts ctxt params prover |
180 |> Sledgehammer_MePo.iterative_relevant_facts ctxt params prover |
208 max_relevant NONE hyp_ts concl_t |
181 max_relevant NONE hyp_ts concl_t |
209 |> map (fn ((name, _), _) => name ()) |
182 |> map (fn ((name, _), _) => name ()) |
210 |> sort string_ord |
|
211 val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n" |
183 val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n" |
212 in File.append path s end |
184 in File.append path s end |
213 else |
185 else |
214 () |
186 () |
215 in fact :: old_facts end |
187 in fact :: old_facts end |