tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
authorwenzelm
Tue Mar 11 18:26:47 2014 +0100 (2014-03-11)
changeset 56053030531cc4c62
parent 56052 4873054cd1fc
child 56054 d1130b831e93
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
src/Pure/General/change_table.ML
src/Pure/ROOT
src/Pure/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/change_table.ML	Tue Mar 11 18:26:47 2014 +0100
     1.3 @@ -0,0 +1,142 @@
     1.4 +(*  Title:      Pure/General/change_table.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Generic tables with extra bookkeeping of changes relative to some
     1.8 +common base version, subject to implicit block structure.  Support for
     1.9 +efficient join/merge of big global tables with small local updates.
    1.10 +*)
    1.11 +
    1.12 +signature CHANGE_TABLE =
    1.13 +sig
    1.14 +  structure Table: TABLE
    1.15 +  type key = Table.key
    1.16 +  exception DUP of key
    1.17 +  exception SAME
    1.18 +  type 'a T
    1.19 +  val table_of: 'a T -> 'a Table.table
    1.20 +  val empty: 'a T
    1.21 +  val change_base: bool -> 'a T -> 'a T
    1.22 +  val join: (key -> 'a * 'a -> 'a) (*exception SAME*) -> 'a T * 'a T -> 'a T  (*exception DUP*)
    1.23 +  val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T  (*exception DUP*)
    1.24 +  val fold: (key * 'b -> 'a -> 'a) -> 'b T -> 'a -> 'a
    1.25 +  val dest: 'a T -> (key * 'a) list
    1.26 +  val lookup_key: 'a T -> key -> (key * 'a) option
    1.27 +  val lookup: 'a T -> key -> 'a option
    1.28 +  val defined: 'a T -> key -> bool
    1.29 +  val update: key * 'a -> 'a T -> 'a T
    1.30 +  val update_new: key * 'a -> 'a T -> 'a T  (*exception DUP*)
    1.31 +  val map_entry: key -> ('a -> 'a) -> 'a T -> 'a T
    1.32 +  val map_default: key * 'a -> ('a -> 'a) -> 'a T -> 'a T
    1.33 +  val delete_safe: key -> 'a T -> 'a T
    1.34 +end;
    1.35 +
    1.36 +functor Change_Table(Key: KEY): CHANGE_TABLE =
    1.37 +struct
    1.38 +
    1.39 +structure Table = Table(Key);
    1.40 +type key = Table.key;
    1.41 +
    1.42 +exception SAME = Table.SAME;
    1.43 +exception DUP = Table.DUP;
    1.44 +
    1.45 +
    1.46 +(* optional change *)
    1.47 +
    1.48 +datatype change = Change of {base: serial, depth: int, changes: Table.set};
    1.49 +
    1.50 +fun some_change base depth changes =
    1.51 +  SOME (Change {base = base, depth = depth, changes = changes});
    1.52 +
    1.53 +fun base_change true NONE =
    1.54 +      some_change (serial ()) 0 Table.empty
    1.55 +  | base_change true (SOME (Change {base, depth, changes})) =
    1.56 +      some_change base (depth + 1) changes
    1.57 +  | base_change false (SOME (Change {base, depth, changes})) =
    1.58 +      if depth = 0 then NONE else some_change base (depth - 1) changes
    1.59 +  | base_change false NONE = raise Fail "Unbalanced block structure of change table";
    1.60 +
    1.61 +fun update_change _ NONE = NONE
    1.62 +  | update_change key (SOME (Change {base, depth, changes})) =
    1.63 +      some_change base depth (Table.insert (K true) (key, ()) changes);
    1.64 +
    1.65 +fun cannot_merge () = raise Fail "Attempt to merge tables with incompatible change base";
    1.66 +
    1.67 +fun merge_change (NONE, NONE) = NONE
    1.68 +  | merge_change (SOME (Change change1), SOME (Change change2)) =
    1.69 +      let
    1.70 +        val {base = base1, depth = depth1, changes = changes1} = change1;
    1.71 +        val {base = base2, depth = depth2, changes = changes2} = change2;
    1.72 +      in
    1.73 +        if base1 = base1 andalso depth1 = depth2 then
    1.74 +          SOME ((changes2, some_change base1 depth1 (Table.merge (K true) (changes1, changes2))))
    1.75 +        else cannot_merge ()
    1.76 +      end
    1.77 +  | merge_change _ = cannot_merge ();
    1.78 +
    1.79 +
    1.80 +(* table with changes *)
    1.81 +
    1.82 +datatype 'a T = Change_Table of {change: change option, table: 'a Table.table};
    1.83 +
    1.84 +fun table_of (Change_Table {table, ...}) = table;
    1.85 +val empty = Change_Table {change = NONE, table = Table.empty};
    1.86 +
    1.87 +fun make_change_table (change, table) = Change_Table {change = change, table = table};
    1.88 +fun map_change_table f (Change_Table {change, table}) = make_change_table (f (change, table));
    1.89 +
    1.90 +fun change_base begin = (map_change_table o apfst) (base_change begin);
    1.91 +
    1.92 +
    1.93 +(* join and merge *)
    1.94 +
    1.95 +fun join f (arg1, arg2) =
    1.96 +  let
    1.97 +    val Change_Table {change = change1, table = table1} = arg1;
    1.98 +    val Change_Table {change = change2, table = table2} = arg2;
    1.99 +  in
   1.100 +    if pointer_eq (table1, table2) orelse Table.is_empty table2 then arg1
   1.101 +    else if Table.is_empty table1 then arg2
   1.102 +    else
   1.103 +      (case merge_change (change1, change2) of
   1.104 +        NONE => make_change_table (NONE, Table.join f (table1, table2))
   1.105 +      | SOME (changes2, change') =>
   1.106 +          let
   1.107 +            fun update key table =
   1.108 +              (case Table.lookup table2 key of
   1.109 +                NONE => table
   1.110 +              | SOME y =>
   1.111 +                  (case Table.lookup table key of
   1.112 +                    NONE => Table.update (key, y) table
   1.113 +                  | SOME x =>
   1.114 +                      (case (SOME (f key (x, y)) handle Table.SAME => NONE) of
   1.115 +                        NONE => table
   1.116 +                      | SOME z => Table.update (key, z) table)));
   1.117 +            val table' = Table.fold (update o #1) changes2 table1;
   1.118 +          in make_change_table (change', table') end)
   1.119 +  end;
   1.120 +
   1.121 +fun merge eq =
   1.122 +  join (fn key => fn xy => if eq xy then raise Table.SAME else raise Table.DUP key);
   1.123 +
   1.124 +
   1.125 +(* derived operations *)
   1.126 +
   1.127 +fun fold f arg = Table.fold f (table_of arg);
   1.128 +fun dest arg = Table.dest (table_of arg);
   1.129 +fun lookup_key arg = Table.lookup_key (table_of arg);
   1.130 +fun lookup arg = Table.lookup (table_of arg);
   1.131 +fun defined arg = Table.defined (table_of arg);
   1.132 +
   1.133 +fun change_table key f =
   1.134 +  map_change_table (fn (change, table) => (update_change key change, f table));
   1.135 +
   1.136 +fun update (key, x)        = change_table key (Table.update (key, x));
   1.137 +fun update_new (key, x)    = change_table key (Table.update_new (key, x));
   1.138 +fun map_entry key f        = change_table key (Table.map_entry key f);
   1.139 +fun map_default (key, x) f = change_table key (Table.map_default (key, x) f);
   1.140 +fun delete_safe key        = change_table key (Table.delete_safe key);
   1.141 +
   1.142 +end;
   1.143 +
   1.144 +structure Change_Table = Change_Table(type key = string val ord = fast_string_ord);
   1.145 +
     2.1 --- a/src/Pure/ROOT	Tue Mar 11 14:28:39 2014 +0100
     2.2 +++ b/src/Pure/ROOT	Tue Mar 11 18:26:47 2014 +0100
     2.3 @@ -71,6 +71,7 @@
     2.4      "General/basics.ML"
     2.5      "General/binding.ML"
     2.6      "General/buffer.ML"
     2.7 +    "General/change_table.ML"
     2.8      "General/completion.ML"
     2.9      "General/file.ML"
    2.10      "General/graph.ML"
     3.1 --- a/src/Pure/ROOT.ML	Tue Mar 11 14:28:39 2014 +0100
     3.2 +++ b/src/Pure/ROOT.ML	Tue Mar 11 18:26:47 2014 +0100
     3.3 @@ -64,6 +64,7 @@
     3.4  use "PIDE/xml.ML";
     3.5  use "PIDE/yxml.ML";
     3.6  
     3.7 +use "General/change_table.ML";
     3.8  use "General/graph.ML";
     3.9  
    3.10  use "System/options.ML";