1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Feb 18 08:52:23 2013 +0100
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Feb 18 10:43:36 2013 +0100
1.3 @@ -748,20 +748,19 @@
1.4
1.5 fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0
1.6
1.7 -fun maximal_in_graph access_G facts =
1.8 +fun maximal_wrt_graph G keys =
1.9 let
1.10 - val facts = [] |> fold (cons o nickname_of_thm o snd) facts
1.11 - val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) facts
1.12 + val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) keys
1.13 fun insert_new seen name =
1.14 not (Symtab.defined seen name) ? insert (op =) name
1.15 fun find_maxes _ (maxs, []) = map snd maxs
1.16 | find_maxes seen (maxs, new :: news) =
1.17 find_maxes
1.18 - (seen |> num_keys (Graph.imm_succs access_G new) > 1
1.19 + (seen |> num_keys (Graph.imm_succs G new) > 1
1.20 ? Symtab.default (new, ()))
1.21 (if Symtab.defined tab new then
1.22 let
1.23 - val newp = Graph.all_preds access_G [new]
1.24 + val newp = Graph.all_preds G [new]
1.25 fun is_ancestor x yp = member (op =) yp x
1.26 val maxs =
1.27 maxs |> filter (fn (_, max) => not (is_ancestor max newp))
1.28 @@ -775,8 +774,12 @@
1.29 end
1.30 else
1.31 (maxs, Graph.Keys.fold (insert_new seen)
1.32 - (Graph.imm_preds access_G new) news))
1.33 - in find_maxes Symtab.empty ([], Graph.maximals access_G) end
1.34 + (Graph.imm_preds G new) news))
1.35 + in find_maxes Symtab.empty ([], Graph.maximals G) end
1.36 +
1.37 +fun maximal_wrt_access_graph access_G =
1.38 + map (nickname_of_thm o snd)
1.39 + #> maximal_wrt_graph access_G
1.40
1.41 fun is_fact_in_graph access_G get_th fact =
1.42 can (Graph.get_node access_G) (nickname_of_thm (get_th fact))
1.43 @@ -830,7 +833,7 @@
1.44 (access_G, [])
1.45 else
1.46 let
1.47 - val parents = maximal_in_graph access_G facts
1.48 + val parents = maximal_wrt_access_graph access_G facts
1.49 val feats =
1.50 features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
1.51 val hints =
1.52 @@ -888,7 +891,7 @@
1.53 in
1.54 peek_state ctxt (fn {access_G, ...} =>
1.55 let
1.56 - val parents = maximal_in_graph access_G facts
1.57 + val parents = maximal_wrt_access_graph access_G facts
1.58 val deps =
1.59 used_ths |> filter (is_fact_in_graph access_G I)
1.60 |> map nickname_of_thm
1.61 @@ -1003,7 +1006,7 @@
1.62 val ancestors =
1.63 old_facts
1.64 |> filter (fn (_, th) => crude_thm_ord (th, last_th) <> GREATER)
1.65 - val parents = maximal_in_graph access_G ancestors
1.66 + val parents = maximal_wrt_access_graph access_G ancestors
1.67 val (learns, (_, n, _, _)) =
1.68 ([], (parents, 0, next_commit_time (), false))
1.69 |> fold learn_new_fact new_facts