merged
authorwenzelm
Sat Feb 25 15:33:36 2012 +0100 (2012-02-25)
changeset 46675f4ce220d2799
parent 46674 bc03b533b061
parent 46668 9034b44844bd
child 46676 b4bc54d4624b
child 46689 f559866a7aa2
merged
     1.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Sat Feb 25 09:07:53 2012 +0100
     1.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Sat Feb 25 15:33:36 2012 +0100
     1.3 @@ -143,8 +143,6 @@
     1.4                   [(factsN, [Formula (ident, Conjecture, phi, NONE, [])])])
     1.5    | is_problem_line_tautology _ _ _ = false
     1.6  
     1.7 -structure String_Graph = Graph(type key = string val ord = string_ord);
     1.8 -
     1.9  fun order_facts ord = sort (ord o pairself ident_of_problem_line)
    1.10  fun order_problem_facts _ [] = []
    1.11    | order_problem_facts ord ((heading, lines) :: problem) =
     2.1 --- a/src/Pure/General/graph.ML	Sat Feb 25 09:07:53 2012 +0100
     2.2 +++ b/src/Pure/General/graph.ML	Sat Feb 25 15:33:36 2012 +0100
     2.3 @@ -43,7 +43,6 @@
     2.4    val is_maximal: 'a T -> key -> bool
     2.5    val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
     2.6    val default_node: key * 'a -> 'a T -> 'a T
     2.7 -  val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
     2.8    val del_node: key -> 'a T -> 'a T                                   (*exception UNDEF*)
     2.9    val is_edge: 'a T -> key * key -> bool
    2.10    val add_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
    2.11 @@ -175,7 +174,7 @@
    2.12  fun is_maximal G x = Keys.is_empty (imm_succs G x);
    2.13  
    2.14  
    2.15 -(* nodes *)
    2.16 +(* node operations *)
    2.17  
    2.18  fun new_node (x, info) (Graph tab) =
    2.19    Graph (Table.update_new (x, (info, (Keys.empty, Keys.empty))) tab);
    2.20 @@ -183,12 +182,6 @@
    2.21  fun default_node (x, info) (Graph tab) =
    2.22    Graph (Table.default (x, (info, (Keys.empty, Keys.empty))) tab);
    2.23  
    2.24 -fun del_nodes xs (Graph tab) =
    2.25 -  Graph (tab
    2.26 -    |> fold Table.delete xs
    2.27 -    |> Table.map (fn _ => fn (i, (preds, succs)) =>
    2.28 -      (i, (fold Keys.remove xs preds, fold Keys.remove xs succs))));
    2.29 -
    2.30  fun del_node x (G as Graph tab) =
    2.31    let
    2.32      fun del_adjacent which y =
    2.33 @@ -205,7 +198,7 @@
    2.34    fold_graph (fn (x, _) => not (pred x) ? del_node x) G G;
    2.35  
    2.36  
    2.37 -(* edges *)
    2.38 +(* edge operations *)
    2.39  
    2.40  fun is_edge G (x, y) = Keys.member (imm_succs G x) y handle UNDEF _ => false;
    2.41  
    2.42 @@ -326,4 +319,5 @@
    2.43  end;
    2.44  
    2.45  structure Graph = Graph(type key = string val ord = fast_string_ord);
    2.46 +structure String_Graph = Graph(type key = string val ord = string_ord);
    2.47  structure Int_Graph = Graph(type key = int val ord = int_ord);
     3.1 --- a/src/Pure/General/graph.scala	Sat Feb 25 09:07:53 2012 +0100
     3.2 +++ b/src/Pure/General/graph.scala	Sat Feb 25 15:33:36 2012 +0100
     3.3 @@ -20,11 +20,14 @@
     3.4  
     3.5    def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
     3.6      new Graph[Key, A](SortedMap.empty(ord))
     3.7 +
     3.8 +  def string[A]: Graph[String, A] = empty(Ordering.String)
     3.9 +  def int[A]: Graph[Int, A] = empty(Ordering.Int)
    3.10 +  def long[A]: Graph[Long, A] = empty(Ordering.Long)
    3.11  }
    3.12  
    3.13  
    3.14  class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))])
    3.15 -  extends Iterable[(Key, (A, (SortedSet[Key], SortedSet[Key])))]
    3.16  {
    3.17    type Keys = SortedSet[Key]
    3.18    type Entry = (A, (Keys, Keys))
    3.19 @@ -32,17 +35,20 @@
    3.20    def ordering: Ordering[Key] = rep.ordering
    3.21    def empty_keys: Keys = SortedSet.empty[Key](ordering)
    3.22  
    3.23 -  override def iterator: Iterator[(Key, Entry)] = rep.iterator
    3.24 +
    3.25 +  /* graphs */
    3.26  
    3.27    def is_empty: Boolean = rep.isEmpty
    3.28  
    3.29 -  def keys: List[Key] = rep.keySet.toList
    3.30 +  def entries: Iterator[(Key, Entry)] = rep.iterator
    3.31 +  def keys: Iterator[Key] = entries.map(_._1)
    3.32  
    3.33    def dest: List[(Key, List[Key])] =
    3.34 -    (for ((x, (_, (_, succs))) <- iterator) yield (x, succs.toList)).toList
    3.35 +    (for ((x, (_, (_, succs))) <- entries) yield (x, succs.toList)).toList
    3.36  
    3.37 -
    3.38 -  /* entries */
    3.39 +  override def toString: String =
    3.40 +    dest.map(p => p._1.toString + " -> " + p._2.map(_.toString).mkString("{", ", ", "}"))
    3.41 +      .mkString("Graph(", ", ", ")")
    3.42  
    3.43    private def get_entry(x: Key): Entry =
    3.44      rep.get(x) match {
    3.45 @@ -96,7 +102,7 @@
    3.46    /*strongly connected components; see: David King and John Launchbury,
    3.47      "Structuring Depth First Search Algorithms in Haskell"*/
    3.48    def strong_conn: List[List[Key]] =
    3.49 -    reachable(imm_preds, all_succs(keys))._1.filterNot(_.isEmpty).reverse
    3.50 +    reachable(imm_preds, all_succs(keys.toList))._1.filterNot(_.isEmpty).reverse
    3.51  
    3.52  
    3.53    /* minimal and maximal elements */
    3.54 @@ -113,7 +119,7 @@
    3.55    def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty
    3.56  
    3.57  
    3.58 -  /* nodes */
    3.59 +  /* node operations */
    3.60  
    3.61    def new_node(x: Key, info: A): Graph[Key, A] =
    3.62    {
    3.63 @@ -143,10 +149,10 @@
    3.64    }
    3.65  
    3.66    def restrict(pred: Key => Boolean): Graph[Key, A] =
    3.67 -    (this /: iterator){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
    3.68 +    (this /: entries){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
    3.69  
    3.70  
    3.71 -  /* edges */
    3.72 +  /* edge operations */
    3.73  
    3.74    def is_edge(x: Key, y: Key): Boolean =
    3.75      try { imm_succs(x)(y) }
     4.1 --- a/src/Pure/Thy/thy_info.ML	Sat Feb 25 09:07:53 2012 +0100
     4.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Feb 25 15:33:36 2012 +0100
     4.3 @@ -146,7 +146,7 @@
     4.4        val succs = thy_graph Graph.all_succs [name];
     4.5        val _ = Output.urgent_message (loader_msg "removing" succs);
     4.6        val _ = List.app (perform Remove) succs;
     4.7 -      val _ = change_thys (Graph.del_nodes succs);
     4.8 +      val _ = change_thys (fold Graph.del_node succs);
     4.9      in () end);
    4.10  
    4.11  fun kill_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>
     5.1 --- a/src/Tools/Code/code_thingol.ML	Sat Feb 25 09:07:53 2012 +0100
     5.2 +++ b/src/Tools/Code/code_thingol.ML	Sat Feb 25 15:33:36 2012 +0100
     5.3 @@ -938,7 +938,7 @@
     5.4          val Fun (_, ((vs_ty, [(([], t), _)]), _)) =
     5.5            Graph.get_node program1 Term.dummy_patternN;
     5.6          val deps = Graph.immediate_succs program1 Term.dummy_patternN;
     5.7 -        val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
     5.8 +        val program2 = Graph.del_node Term.dummy_patternN program1;
     5.9          val deps_all = Graph.all_succs program2 deps;
    5.10          val program3 = Graph.restrict (member (op =) deps_all) program2;
    5.11        in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end;
     6.1 --- a/src/Tools/subtyping.ML	Sat Feb 25 09:07:53 2012 +0100
     6.2 +++ b/src/Tools/subtyping.ML	Sat Feb 25 15:33:36 2012 +0100
     6.3 @@ -522,7 +522,7 @@
     6.4          val T = Type_Infer.deref tye (hd nodes);
     6.5          val P = new_imm_preds G nodes;
     6.6          val S = new_imm_succs G nodes;
     6.7 -        val G' = Typ_Graph.del_nodes (tl nodes) G;
     6.8 +        val G' = fold Typ_Graph.del_node (tl nodes) G;
     6.9          fun check_and_gen super T' =
    6.10            let val U = Type_Infer.deref tye T';
    6.11            in