added graph encode/decode operations;
authorwenzelm
Tue Sep 25 14:32:41 2012 +0200 (2012-09-25)
changeset 4956011430dd89e35
parent 49559 c3a6e110679b
child 49561 26fc70e983c2
added graph encode/decode operations;
tuned signature;
src/Pure/General/graph.ML
src/Pure/General/graph.scala
src/Pure/ROOT.ML
src/Pure/display.ML
src/Tools/subtyping.ML
     1.1 --- a/src/Pure/General/graph.ML	Tue Sep 25 12:17:58 2012 +0200
     1.2 +++ b/src/Pure/General/graph.ML	Tue Sep 25 14:32:41 2012 +0200
     1.3 @@ -22,7 +22,6 @@
     1.4    val empty: 'a T
     1.5    val is_empty: 'a T -> bool
     1.6    val keys: 'a T -> key list
     1.7 -  val dest: 'a T -> (key * key list) list
     1.8    val get_first: (key * ('a * (Keys.T * Keys.T)) -> 'b option) -> 'a T -> 'b option
     1.9    val fold: (key * ('a * (Keys.T * Keys.T)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
    1.10    val get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T))        (*exception UNDEF*)
    1.11 @@ -48,6 +47,8 @@
    1.12    val add_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
    1.13    val del_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
    1.14    val restrict: (key -> bool) -> 'a T -> 'a T
    1.15 +  val dest: 'a T -> ((key * 'a) * key list) list
    1.16 +  val make: ((key * 'a) * key list) list -> 'a T                      (*exception DUP | UNDEF*)
    1.17    val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUP*)
    1.18    val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
    1.19      'a T * 'a T -> 'a T                                               (*exception DUP*)
    1.20 @@ -61,6 +62,8 @@
    1.21    val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
    1.22    exception DEP of key * key
    1.23    val schedule: ((key * 'b) list -> key * 'a -> 'b) -> 'a T -> 'b list  (*exception DEP*)
    1.24 +  val encode: key XML.Encode.T -> 'a XML.Encode.T -> 'a T XML.Encode.T
    1.25 +  val decode: key XML.Decode.T -> 'a XML.Decode.T -> 'a T XML.Decode.T
    1.26  end;
    1.27  
    1.28  functor Graph(Key: KEY): GRAPH =
    1.29 @@ -108,7 +111,6 @@
    1.30  val empty = Graph Table.empty;
    1.31  fun is_empty (Graph tab) = Table.is_empty tab;
    1.32  fun keys (Graph tab) = Table.keys tab;
    1.33 -fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, Keys.dest succs)) (Table.dest tab);
    1.34  
    1.35  fun get_first f (Graph tab) = Table.get_first f tab;
    1.36  fun fold_graph f (Graph tab) = Table.fold f tab;
    1.37 @@ -215,12 +217,22 @@
    1.38    else G;
    1.39  
    1.40  fun diff_edges G1 G2 =
    1.41 -  flat (dest G1 |> map (fn (x, ys) => ys |> map_filter (fn y =>
    1.42 -    if is_edge G2 (x, y) then NONE else SOME (x, y))));
    1.43 +  fold_graph (fn (x, (_, (_, succs))) =>
    1.44 +    Keys.fold (fn y => not (is_edge G2 (x, y)) ? cons (x, y)) succs) G1 [];
    1.45  
    1.46  fun edges G = diff_edges G empty;
    1.47  
    1.48  
    1.49 +(* dest and make *)
    1.50 +
    1.51 +fun dest G = fold_graph (fn (x, (i, (_, succs))) => cons ((x, i), Keys.dest succs)) G [];
    1.52 +
    1.53 +fun make entries =
    1.54 +  empty
    1.55 +  |> fold (new_node o fst) entries
    1.56 +  |> fold (fn ((x, _), ys) => fold (fn y => add_edge (x, y)) ys) entries;
    1.57 +
    1.58 +
    1.59  (* join and merge *)
    1.60  
    1.61  fun no_edges (i, _) = (i, (Keys.empty, Keys.empty));
    1.62 @@ -312,6 +324,19 @@
    1.63    in map (the o Table.lookup results) xs end;
    1.64  
    1.65  
    1.66 +(* XML data representation *)
    1.67 +
    1.68 +fun encode key info G =
    1.69 +  dest G |>
    1.70 +    let open XML.Encode
    1.71 +    in list (pair (pair key info) (list key)) end;
    1.72 +
    1.73 +fun decode key info body =
    1.74 +  body |>
    1.75 +    let open XML.Decode
    1.76 +    in list (pair (pair key info) (list key)) end |> make;
    1.77 +
    1.78 +
    1.79  (*final declarations of this structure!*)
    1.80  val map = map_nodes;
    1.81  val fold = fold_graph;
     2.1 --- a/src/Pure/General/graph.scala	Tue Sep 25 12:17:58 2012 +0200
     2.2 +++ b/src/Pure/General/graph.scala	Tue Sep 25 14:32:41 2012 +0200
     2.3 @@ -21,9 +21,35 @@
     2.4    def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
     2.5      new Graph[Key, A](SortedMap.empty(ord))
     2.6  
     2.7 +  def make[Key, A](entries: List[((Key, A), List[Key])])(implicit ord: Ordering[Key])
     2.8 +    : Graph[Key, A] =
     2.9 +  {
    2.10 +    val graph1 =
    2.11 +      (empty[Key, A](ord) /: entries) { case (graph, ((x, info), _)) => graph.new_node(x, info) }
    2.12 +    val graph2 =
    2.13 +      (graph1 /: entries) { case (graph, ((x, _), ys)) => (graph /: ys)(_.add_edge(x, _)) }
    2.14 +    graph2
    2.15 +  }
    2.16 +
    2.17    def string[A]: Graph[String, A] = empty(Ordering.String)
    2.18    def int[A]: Graph[Int, A] = empty(Ordering.Int)
    2.19    def long[A]: Graph[Long, A] = empty(Ordering.Long)
    2.20 +
    2.21 +
    2.22 +  /* XML data representation */
    2.23 +
    2.24 +  def encode[Key, A](key: XML.Encode.T[Key], info: XML.Encode.T[A]): XML.Encode.T[Graph[Key, A]] =
    2.25 +    ((graph: Graph[Key, A]) => {
    2.26 +      import XML.Encode._
    2.27 +      list(pair(pair(key, info), list(key)))(graph.dest)
    2.28 +    })
    2.29 +
    2.30 +  def decode[Key, A](key: XML.Decode.T[Key], info: XML.Decode.T[A])(implicit ord: Ordering[Key])
    2.31 +      : XML.Decode.T[Graph[Key, A]] =
    2.32 +    ((body: XML.Body) => {
    2.33 +      import XML.Decode._
    2.34 +      make(list(pair(pair(key, info), list(key)))(body))(ord)
    2.35 +    })
    2.36  }
    2.37  
    2.38  
    2.39 @@ -44,11 +70,12 @@
    2.40    def entries: Iterator[(Key, Entry)] = rep.iterator
    2.41    def keys: Iterator[Key] = entries.map(_._1)
    2.42  
    2.43 -  def dest: List[(Key, List[Key])] =
    2.44 -    (for ((x, (_, (_, succs))) <- entries) yield (x, succs.toList)).toList
    2.45 +  def dest: List[((Key, A), List[Key])] =
    2.46 +    (for ((x, (i, (_, succs))) <- entries) yield ((x, i), succs.toList)).toList
    2.47  
    2.48    override def toString: String =
    2.49 -    dest.map(p => p._1.toString + " -> " + p._2.map(_.toString).mkString("{", ", ", "}"))
    2.50 +    dest.map({ case ((x, _), ys) =>
    2.51 +        x.toString + " -> " + ys.iterator.map(_.toString).mkString("{", ", ", "}") })
    2.52        .mkString("Graph(", ", ", ")")
    2.53  
    2.54    private def get_entry(x: Key): Entry =
     3.1 --- a/src/Pure/ROOT.ML	Tue Sep 25 12:17:58 2012 +0200
     3.2 +++ b/src/Pure/ROOT.ML	Tue Sep 25 14:32:41 2012 +0200
     3.3 @@ -50,7 +50,6 @@
     3.4  use "General/same.ML";
     3.5  use "General/ord_list.ML";
     3.6  use "General/balanced_tree.ML";
     3.7 -use "General/graph.ML";
     3.8  use "General/linear_set.ML";
     3.9  use "General/buffer.ML";
    3.10  use "General/pretty.ML";
    3.11 @@ -66,6 +65,8 @@
    3.12  use "PIDE/xml.ML";
    3.13  use "PIDE/yxml.ML";
    3.14  
    3.15 +use "General/graph.ML";
    3.16 +
    3.17  
    3.18  (* concurrency within the ML runtime *)
    3.19  
     4.1 --- a/src/Pure/display.ML	Tue Sep 25 12:17:58 2012 +0200
     4.2 +++ b/src/Pure/display.ML	Tue Sep 25 14:32:41 2012 +0200
     4.3 @@ -194,7 +194,8 @@
     4.4      val classes = Sorts.classes_of class_algebra;
     4.5      val arities = Sorts.arities_of class_algebra;
     4.6  
     4.7 -    val clsses = Name_Space.dest_table ctxt (class_space, Symtab.make (Graph.dest classes));
     4.8 +    val clsses =
     4.9 +      Name_Space.dest_table ctxt (class_space, Symtab.make (map (apfst fst) (Graph.dest classes)));
    4.10      val tdecls = Name_Space.dest_table ctxt types;
    4.11      val arties = Name_Space.dest_table ctxt (Type.type_space tsig, arities);
    4.12  
     5.1 --- a/src/Tools/subtyping.ML	Tue Sep 25 12:17:58 2012 +0200
     5.2 +++ b/src/Tools/subtyping.ML	Tue Sep 25 14:32:41 2012 +0200
     5.3 @@ -908,7 +908,7 @@
     5.4              Syntax.string_of_typ ctxt T1 ^ "!\n\nCannot add coercion of type: " ^
     5.5              Syntax.string_of_typ ctxt (T1 --> T2));
     5.6          val new_edges =
     5.7 -          flat (Graph.dest G'' |> map (fn (x, ys) => ys |> map_filter (fn y =>
     5.8 +          flat (Graph.dest G'' |> map (fn ((x, _), ys) => ys |> map_filter (fn y =>
     5.9              if Graph.is_edge G' (x, y) then NONE else SOME (x, y))));
    5.10          val G_and_new = Graph.add_edge (a, b) G';
    5.11