author wenzelm Sat Feb 25 15:33:36 2012 +0100 (2012-02-25) changeset 46675 f4ce220d2799 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
```