tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/change_table.ML	Tue Mar 11 18:26:47 2014 +0100
@@ -0,0 +1,142 @@
+(*  Title:      Pure/General/change_table.ML
+    Author:     Makarius
+
+Generic tables with extra bookkeeping of changes relative to some
+common base version, subject to implicit block structure.  Support for
+efficient join/merge of big global tables with small local updates.
+*)
+
+signature CHANGE_TABLE =
+sig
+  structure Table: TABLE
+  type key = Table.key
+  exception DUP of key
+  exception SAME
+  type 'a T
+  val table_of: 'a T -> 'a Table.table
+  val empty: 'a T
+  val change_base: bool -> 'a T -> 'a T
+  val join: (key -> 'a * 'a -> 'a) (*exception SAME*) -> 'a T * 'a T -> 'a T  (*exception DUP*)
+  val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T  (*exception DUP*)
+  val fold: (key * 'b -> 'a -> 'a) -> 'b T -> 'a -> 'a
+  val dest: 'a T -> (key * 'a) list
+  val lookup_key: 'a T -> key -> (key * 'a) option
+  val lookup: 'a T -> key -> 'a option
+  val defined: 'a T -> key -> bool
+  val update: key * 'a -> 'a T -> 'a T
+  val update_new: key * 'a -> 'a T -> 'a T  (*exception DUP*)
+  val map_entry: key -> ('a -> 'a) -> 'a T -> 'a T
+  val map_default: key * 'a -> ('a -> 'a) -> 'a T -> 'a T
+  val delete_safe: key -> 'a T -> 'a T
+end;
+
+functor Change_Table(Key: KEY): CHANGE_TABLE =
+struct
+
+structure Table = Table(Key);
+type key = Table.key;
+
+exception SAME = Table.SAME;
+exception DUP = Table.DUP;
+
+
+(* optional change *)
+
+datatype change = Change of {base: serial, depth: int, changes: Table.set};
+
+fun some_change base depth changes =
+  SOME (Change {base = base, depth = depth, changes = changes});
+
+fun base_change true NONE =
+      some_change (serial ()) 0 Table.empty
+  | base_change true (SOME (Change {base, depth, changes})) =
+      some_change base (depth + 1) changes
+  | base_change false (SOME (Change {base, depth, changes})) =
+      if depth = 0 then NONE else some_change base (depth - 1) changes
+  | base_change false NONE = raise Fail "Unbalanced block structure of change table";
+
+fun update_change _ NONE = NONE
+  | update_change key (SOME (Change {base, depth, changes})) =
+      some_change base depth (Table.insert (K true) (key, ()) changes);
+
+fun cannot_merge () = raise Fail "Attempt to merge tables with incompatible change base";
+
+fun merge_change (NONE, NONE) = NONE
+  | merge_change (SOME (Change change1), SOME (Change change2)) =
+      let
+        val {base = base1, depth = depth1, changes = changes1} = change1;
+        val {base = base2, depth = depth2, changes = changes2} = change2;
+      in
+        if base1 = base1 andalso depth1 = depth2 then
+          SOME ((changes2, some_change base1 depth1 (Table.merge (K true) (changes1, changes2))))
+        else cannot_merge ()
+      end
+  | merge_change _ = cannot_merge ();
+
+
+(* table with changes *)
+
+datatype 'a T = Change_Table of {change: change option, table: 'a Table.table};
+
+fun table_of (Change_Table {table, ...}) = table;
+val empty = Change_Table {change = NONE, table = Table.empty};
+
+fun make_change_table (change, table) = Change_Table {change = change, table = table};
+fun map_change_table f (Change_Table {change, table}) = make_change_table (f (change, table));
+
+fun change_base begin = (map_change_table o apfst) (base_change begin);
+
+
+(* join and merge *)
+
+fun join f (arg1, arg2) =
+  let
+    val Change_Table {change = change1, table = table1} = arg1;
+    val Change_Table {change = change2, table = table2} = arg2;
+  in
+    if pointer_eq (table1, table2) orelse Table.is_empty table2 then arg1
+    else if Table.is_empty table1 then arg2
+    else
+      (case merge_change (change1, change2) of
+        NONE => make_change_table (NONE, Table.join f (table1, table2))
+      | SOME (changes2, change') =>
+          let
+            fun update key table =
+              (case Table.lookup table2 key of
+                NONE => table
+              | SOME y =>
+                  (case Table.lookup table key of
+                    NONE => Table.update (key, y) table
+                  | SOME x =>
+                      (case (SOME (f key (x, y)) handle Table.SAME => NONE) of
+                        NONE => table
+                      | SOME z => Table.update (key, z) table)));
+            val table' = Table.fold (update o #1) changes2 table1;
+          in make_change_table (change', table') end)
+  end;
+
+fun merge eq =
+  join (fn key => fn xy => if eq xy then raise Table.SAME else raise Table.DUP key);
+
+
+(* derived operations *)
+
+fun fold f arg = Table.fold f (table_of arg);
+fun dest arg = Table.dest (table_of arg);
+fun lookup_key arg = Table.lookup_key (table_of arg);
+fun lookup arg = Table.lookup (table_of arg);
+fun defined arg = Table.defined (table_of arg);
+
+fun change_table key f =
+  map_change_table (fn (change, table) => (update_change key change, f table));
+
+fun update (key, x)        = change_table key (Table.update (key, x));
+fun update_new (key, x)    = change_table key (Table.update_new (key, x));
+fun map_entry key f        = change_table key (Table.map_entry key f);
+fun map_default (key, x) f = change_table key (Table.map_default (key, x) f);
+fun delete_safe key        = change_table key (Table.delete_safe key);
+
+end;
+
+structure Change_Table = Change_Table(type key = string val ord = fast_string_ord);
+

--- a/src/Pure/ROOT	Tue Mar 11 14:28:39 2014 +0100
+++ b/src/Pure/ROOT	Tue Mar 11 18:26:47 2014 +0100
@@ -71,6 +71,7 @@
     "General/basics.ML"
     "General/binding.ML"
     "General/buffer.ML"
+    "General/change_table.ML"
     "General/completion.ML"
     "General/file.ML"
     "General/graph.ML"

--- a/src/Pure/ROOT.ML	Tue Mar 11 14:28:39 2014 +0100
+++ b/src/Pure/ROOT.ML	Tue Mar 11 18:26:47 2014 +0100
@@ -64,6 +64,7 @@
 use "PIDE/xml.ML";
 use "PIDE/yxml.ML";
 
+use "General/change_table.ML";
 use "General/graph.ML";
 
 use "System/options.ML";