author | wenzelm |
Wed, 12 Mar 2014 21:28:09 +0100 | |
changeset 56067 | 5c2435c79415 |
parent 56054 | d1130b831e93 |
child 56068 | f74d0a4d8ae3 |
permissions | -rw-r--r-- |
56053
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/General/change_table.ML |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
3 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
4 |
Generic tables with extra bookkeeping of changes relative to some |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
5 |
common base version, subject to implicit block structure. Support for |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
6 |
efficient join/merge of big global tables with small local updates. |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
7 |
*) |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
8 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
9 |
signature CHANGE_TABLE = |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
10 |
sig |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
11 |
structure Table: TABLE |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
12 |
type key = Table.key |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
13 |
exception DUP of key |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
14 |
exception SAME |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
15 |
type 'a T |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
16 |
val table_of: 'a T -> 'a Table.table |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
17 |
val empty: 'a T |
56054 | 18 |
val is_empty: 'a T -> bool |
56053
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
19 |
val change_base: bool -> 'a T -> 'a T |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
20 |
val join: (key -> 'a * 'a -> 'a) (*exception SAME*) -> 'a T * 'a T -> 'a T (*exception DUP*) |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
21 |
val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception DUP*) |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
22 |
val fold: (key * 'b -> 'a -> 'a) -> 'b T -> 'a -> 'a |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
23 |
val dest: 'a T -> (key * 'a) list |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
24 |
val lookup_key: 'a T -> key -> (key * 'a) option |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
25 |
val lookup: 'a T -> key -> 'a option |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
26 |
val defined: 'a T -> key -> bool |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
27 |
val update: key * 'a -> 'a T -> 'a T |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
28 |
val update_new: key * 'a -> 'a T -> 'a T (*exception DUP*) |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
29 |
val map_entry: key -> ('a -> 'a) -> 'a T -> 'a T |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
30 |
val map_default: key * 'a -> ('a -> 'a) -> 'a T -> 'a T |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
31 |
val delete_safe: key -> 'a T -> 'a T |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
32 |
end; |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
33 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
34 |
functor Change_Table(Key: KEY): CHANGE_TABLE = |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
35 |
struct |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
36 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
37 |
structure Table = Table(Key); |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
38 |
type key = Table.key; |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
39 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
40 |
exception SAME = Table.SAME; |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
41 |
exception DUP = Table.DUP; |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
42 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
43 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
44 |
(* optional change *) |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
45 |
|
56067 | 46 |
datatype change = No_Change | Change of {base: serial, depth: int, changes: Table.set}; |
56053
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
47 |
|
56067 | 48 |
fun make_change base depth changes = |
49 |
Change {base = base, depth = depth, changes = changes}; |
|
56053
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
50 |
|
56067 | 51 |
fun base_change true No_Change = |
52 |
make_change (serial ()) 0 Table.empty |
|
53 |
| base_change true (Change {base, depth, changes}) = |
|
54 |
make_change base (depth + 1) changes |
|
55 |
| base_change false (Change {base, depth, changes}) = |
|
56 |
if depth = 0 then No_Change else make_change base (depth - 1) changes |
|
57 |
| base_change false No_Change = raise Fail "Unbalanced block structure of change table"; |
|
56053
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
58 |
|
56067 | 59 |
fun update_change _ No_Change = No_Change |
60 |
| update_change key (Change {base, depth, changes}) = |
|
61 |
make_change base depth (Table.insert (K true) (key, ()) changes); |
|
56053
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
62 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
63 |
fun cannot_merge () = raise Fail "Attempt to merge tables with incompatible change base"; |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
64 |
|
56067 | 65 |
fun merge_change (No_Change, No_Change) = NONE |
66 |
| merge_change (Change change1, Change change2) = |
|
56053
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
67 |
let |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
68 |
val {base = base1, depth = depth1, changes = changes1} = change1; |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
69 |
val {base = base2, depth = depth2, changes = changes2} = change2; |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
70 |
in |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
71 |
if base1 = base1 andalso depth1 = depth2 then |
56067 | 72 |
SOME ((changes2, make_change base1 depth1 (Table.merge (K true) (changes1, changes2)))) |
56053
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
73 |
else cannot_merge () |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
74 |
end |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
75 |
| merge_change _ = cannot_merge (); |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
76 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
77 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
78 |
(* table with changes *) |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
79 |
|
56067 | 80 |
datatype 'a T = Change_Table of {change: change, table: 'a Table.table}; |
56053
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
81 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
82 |
fun table_of (Change_Table {table, ...}) = table; |
56054 | 83 |
|
56067 | 84 |
val empty = Change_Table {change = No_Change, table = Table.empty}; |
85 |
||
86 |
fun is_empty (Change_Table {change, table}) = |
|
87 |
(case change of No_Change => Table.is_empty table | _ => false); |
|
56053
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
88 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
89 |
fun make_change_table (change, table) = Change_Table {change = change, table = table}; |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
90 |
fun map_change_table f (Change_Table {change, table}) = make_change_table (f (change, table)); |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
91 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
92 |
fun change_base begin = (map_change_table o apfst) (base_change begin); |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
93 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
94 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
95 |
(* join and merge *) |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
96 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
97 |
fun join f (arg1, arg2) = |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
98 |
let |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
99 |
val Change_Table {change = change1, table = table1} = arg1; |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
100 |
val Change_Table {change = change2, table = table2} = arg2; |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
101 |
in |
56054 | 102 |
if pointer_eq (change1, change2) andalso pointer_eq (table1, table2) then arg1 |
103 |
else if is_empty arg2 then arg1 |
|
104 |
else if is_empty arg1 then arg2 |
|
56053
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
105 |
else |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
106 |
(case merge_change (change1, change2) of |
56067 | 107 |
NONE => make_change_table (No_Change, Table.join f (table1, table2)) |
56053
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
108 |
| SOME (changes2, change') => |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
109 |
let |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
110 |
fun update key table = |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
111 |
(case Table.lookup table2 key of |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
112 |
NONE => table |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
113 |
| SOME y => |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
114 |
(case Table.lookup table key of |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
115 |
NONE => Table.update (key, y) table |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
116 |
| SOME x => |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
117 |
(case (SOME (f key (x, y)) handle Table.SAME => NONE) of |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
118 |
NONE => table |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
119 |
| SOME z => Table.update (key, z) table))); |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
120 |
val table' = Table.fold (update o #1) changes2 table1; |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
121 |
in make_change_table (change', table') end) |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
122 |
end; |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
123 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
124 |
fun merge eq = |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
125 |
join (fn key => fn xy => if eq xy then raise Table.SAME else raise Table.DUP key); |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
126 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
127 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
128 |
(* derived operations *) |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
129 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
130 |
fun fold f arg = Table.fold f (table_of arg); |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
131 |
fun dest arg = Table.dest (table_of arg); |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
132 |
fun lookup_key arg = Table.lookup_key (table_of arg); |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
133 |
fun lookup arg = Table.lookup (table_of arg); |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
134 |
fun defined arg = Table.defined (table_of arg); |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
135 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
136 |
fun change_table key f = |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
137 |
map_change_table (fn (change, table) => (update_change key change, f table)); |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
138 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
139 |
fun update (key, x) = change_table key (Table.update (key, x)); |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
140 |
fun update_new (key, x) = change_table key (Table.update_new (key, x)); |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
141 |
fun map_entry key f = change_table key (Table.map_entry key f); |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
142 |
fun map_default (key, x) f = change_table key (Table.map_default (key, x) f); |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
143 |
fun delete_safe key = change_table key (Table.delete_safe key); |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
144 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
145 |
end; |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
146 |
|
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
147 |
structure Change_Table = Change_Table(type key = string val ord = fast_string_ord); |
030531cc4c62
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
diff
changeset
|
148 |