181 facts |
181 facts |
182 |> map (fn (_, th) => |
182 |> map (fn (_, th) => |
183 (fact_name_of (Thm.get_name_hint th), |
183 (fact_name_of (Thm.get_name_hint th), |
184 th |> Sledgehammer_Util.thms_in_proof (SOME name_tabs) |
184 th |> Sledgehammer_Util.thms_in_proof (SOME name_tabs) |
185 |> map fact_name_of)) |
185 |> map fact_name_of)) |
186 val all_problem_names = problem |> maps (map ident_of_problem_line o snd) |
186 val all_problem_names = |
|
187 problem |> maps (map ident_of_problem_line o snd) |
|
188 |> distinct (op =) |
|
189 val all_problem_name_set = Symtab.make (map (rpair ()) all_problem_names) |
187 val infers = |
190 val infers = |
188 infers |> filter (member (op =) all_problem_names o fst) |
191 infers |> filter (Symtab.defined all_problem_name_set o fst) |
189 |> map (apsnd (filter (member (op =) all_problem_names))) |
192 |> map (apsnd (filter (Symtab.defined all_problem_name_set))) |
|
193 val maybe_add_edge = perhaps o try o String_Graph.add_edge_acyclic |
190 val ordered_names = |
194 val ordered_names = |
191 String_Graph.empty |
195 String_Graph.empty |
192 |> fold (String_Graph.new_node o rpair ()) all_problem_names |
196 |> fold (String_Graph.new_node o rpair ()) all_problem_names |
193 |> fold (fn (to, froms) => |
197 |> fold (fn (to, froms) => |
194 fold (fn from => String_Graph.add_edge (from, to)) froms) |
198 fold (fn from => maybe_add_edge (from, to)) froms) |
195 infers |
199 infers |
196 |> fold (fn (to, from) => String_Graph.add_edge_acyclic (from, to)) |
200 |> fold (fn (to, from) => maybe_add_edge (from, to)) |
197 (tl all_problem_names ~~ fst (split_last all_problem_names)) |
201 (tl all_problem_names ~~ fst (split_last all_problem_names)) |
198 |> String_Graph.topological_order |
202 |> String_Graph.topological_order |
199 val order_tab = |
203 val order_tab = |
200 Symtab.empty |
204 Symtab.empty |
201 |> fold (Symtab.insert (op =)) |
205 |> fold (Symtab.insert (op =)) |