--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sat Feb 27 21:56:55 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sat Feb 27 22:41:22 2010 +0100
@@ -257,7 +257,7 @@
fun obtain_specification_graph options thy t =
let
fun is_nondefining_const (c, T) = member (op =) logic_operator_names c
- fun has_code_pred_intros (c, T) = is_some (try (Predicate_Compile_Core.intros_of thy) c)
+ fun has_code_pred_intros (c, T) = can (Predicate_Compile_Core.intros_of thy) c
fun case_consts (c, T) = is_some (Datatype.info_of_case thy c)
fun is_datatype_constructor (c, T) = is_some (Datatype.info_of_constr thy (c, T))
fun defiants_of specs =
@@ -272,14 +272,22 @@
|> map Const
(*
|> filter is_defining_constname*)
- fun extend t =
- let
- val specs = get_specification options thy t
- (*|> Predicate_Compile_Set.unfold_set_notation*)
- (*val _ = print_specification options thy constname specs*)
- in (specs, defiants_of specs) end;
+ fun extend t gr =
+ if can (Term_Graph.get_node gr) t then gr
+ else
+ let
+ val specs = get_specification options thy t
+ (*|> Predicate_Compile_Set.unfold_set_notation*)
+ (*val _ = print_specification options thy constname specs*)
+ val us = defiants_of specs
+ in
+ gr
+ |> Term_Graph.new_node (t, specs)
+ |> fold extend us
+ |> fold (fn u => Term_Graph.add_edge (t, u)) us
+ end
in
- Term_Graph.extend extend t Term_Graph.empty
+ extend t Term_Graph.empty
end;
--- a/src/Pure/General/graph.ML Sat Feb 27 21:56:55 2010 +0100
+++ b/src/Pure/General/graph.ML Sat Feb 27 22:41:22 2010 +0100
@@ -48,7 +48,6 @@
val topological_order: 'a T -> key list
val add_edge_trans_acyclic: key * key -> 'a T -> 'a T (*exception CYCLES*)
val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception CYCLES*)
- val extend: (key -> 'a * key list) -> key -> 'a T -> 'a T
end;
functor Graph(Key: KEY): GRAPH =
@@ -279,22 +278,6 @@
|> fold add_edge_trans_acyclic (diff_edges G2 G1);
-(* constructing graphs *)
-
-fun extend explore =
- let
- fun ext x G =
- if can (get_entry G) x then G
- else
- let val (info, ys) = explore x in
- G
- |> new_node (x, info)
- |> fold ext ys
- |> fold (fn y => add_edge (x, y)) ys
- end
- in ext end;
-
-
(*final declarations of this structure!*)
val fold = fold_graph;