# HG changeset patch # User bulwahn # Date 1244550037 -7200 # Node ID e8a64ab9fe99fdab0f19a1646673cdb8f02cb1d2 # Parent 9801a92d52d700208e7d7c85be29879fe82b90cd removed general graph functions in the predicate compiler diff -r 9801a92d52d7 -r e8a64ab9fe99 src/HOL/ex/predicate_compile.ML --- a/src/HOL/ex/predicate_compile.ML Tue Jun 09 13:56:28 2009 +0200 +++ b/src/HOL/ex/predicate_compile.ML Tue Jun 09 14:20:37 2009 +0200 @@ -24,7 +24,6 @@ val do_proofs: bool ref val analyze_compr: theory -> term -> term val eval_ref: (unit -> term Predicate.pred) option ref - (* val extend : (key -> 'a * key list) -> key list -> 'a Graph.T -> 'a Graph.T *) val add_equations : string -> theory -> theory end; @@ -1383,25 +1382,9 @@ (data, keys) end; -fun extend explore keys gr = - let - fun contains_node gr key = member (op =) (Graph.keys gr) key - fun extend' key gr = - let - val (node, preds) = explore key - in - gr |> (not (contains_node gr key)) ? - (Graph.new_node (key, node) - #> fold extend' preds - #> fold (Graph.add_edge o (pair key)) preds) - end - in fold extend' keys gr end - -fun mk_graph explore keys = extend explore keys Graph.empty - fun add_equations name thy = let - val thy' = PredData.map (extend (dependencies_of thy) [name]) thy; + val thy' = PredData.map (Graph.extend (dependencies_of thy) [name]) thy; (*val preds = Graph.all_preds (PredData.get thy') [name] |> filter_out (has_elim thy') *) fun strong_conn_of gr keys = Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr) @@ -1427,7 +1410,7 @@ val thy = (ProofContext.theory_of lthy) val const = prep_const thy raw_const val lthy' = lthy - val thy' = PredData.map (extend (dependencies_of thy) [const]) thy + val thy' = PredData.map (Graph.extend (dependencies_of thy) [const]) thy val preds = Graph.all_preds (PredData.get thy') [const] |> filter_out (has_elim thy') val _ = Output.tracing ("preds: " ^ commas preds) (*