# HG changeset patch # User wenzelm # Date 1394558807 -3600 # Node ID 030531cc4c62999f07722da5aba80d0f79b9b882 # Parent 4873054cd1fca6ff02add2015ffac7e591227788 tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates; diff -r 4873054cd1fc -r 030531cc4c62 src/Pure/General/change_table.ML --- /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); + diff -r 4873054cd1fc -r 030531cc4c62 src/Pure/ROOT --- 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" diff -r 4873054cd1fc -r 030531cc4c62 src/Pure/ROOT.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";