author | wenzelm |
Mon, 07 Dec 2020 15:54:07 +0100 (2020-12-07) | |
changeset 72840 | 6b96464066a0 |
parent 56139 | b7add947a6ef |
child 77723 | b761c91c2447 |
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 |
56139
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
20 |
val change_ignore: 'a T -> 'a T |
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
|
21 |
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
|
22 |
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
|
23 |
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
|
24 |
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
|
25 |
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
|
26 |
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
|
27 |
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
|
28 |
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
|
29 |
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
|
30 |
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
|
31 |
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
|
32 |
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
|
33 |
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
|
34 |
|
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 |
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
|
36 |
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
|
37 |
|
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 |
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
|
39 |
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
|
40 |
|
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 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
|
42 |
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
|
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 |
|
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 |
(* 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
|
46 |
|
56139
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
47 |
datatype change = |
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
48 |
No_Change | Change of {base: serial, depth: int, changes: Table.set option}; |
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
|
49 |
|
56067 | 50 |
fun make_change base depth changes = |
51 |
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
|
52 |
|
56139
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
53 |
fun ignore_change (Change {base, depth, changes = SOME _}) = |
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
54 |
make_change base depth NONE |
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
55 |
| ignore_change change = change; |
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
56 |
|
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
57 |
fun update_change key (Change {base, depth, changes = SOME ch}) = |
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
58 |
make_change base depth (SOME (Table.insert (K true) (key, ()) ch)) |
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
59 |
| update_change _ change = change; |
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
60 |
|
56067 | 61 |
fun base_change true No_Change = |
56139
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
62 |
make_change (serial ()) 0 (SOME Table.empty) |
56067 | 63 |
| base_change true (Change {base, depth, changes}) = |
64 |
make_change base (depth + 1) changes |
|
65 |
| base_change false (Change {base, depth, changes}) = |
|
66 |
if depth = 0 then No_Change else make_change base (depth - 1) changes |
|
56139
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
67 |
| base_change false No_Change = raise Fail "Unbalanced change structure"; |
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
|
68 |
|
56139
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
69 |
fun cannot_merge () = raise Fail "Cannot merge: incompatible change structure"; |
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
|
70 |
|
56067 | 71 |
fun merge_change (No_Change, No_Change) = NONE |
72 |
| 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
|
73 |
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
|
74 |
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
|
75 |
val {base = base2, depth = depth2, changes = changes2} = change2; |
56139
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
76 |
val _ = if base1 = base2 andalso depth1 = depth2 then () else cannot_merge (); |
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
77 |
val (swapped, ch2) = |
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
78 |
(case (changes1, changes2) of |
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
79 |
(_, SOME ch2) => (false, ch2) |
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
80 |
| (SOME ch1, _) => (true, ch1) |
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
81 |
| _ => cannot_merge ()); |
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
82 |
in SOME (swapped, ch2, make_change base1 depth1 NONE) end |
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
|
83 |
| 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
|
84 |
|
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
|
85 |
|
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
|
86 |
(* 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
|
87 |
|
56067 | 88 |
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
|
89 |
|
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 table_of (Change_Table {table, ...}) = table; |
56054 | 91 |
|
56067 | 92 |
val empty = Change_Table {change = No_Change, table = Table.empty}; |
93 |
||
94 |
fun is_empty (Change_Table {change, table}) = |
|
95 |
(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
|
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 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
|
98 |
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
|
99 |
|
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 |
fun change_base begin = (map_change_table o apfst) (base_change begin); |
56139
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
101 |
fun change_ignore arg = (map_change_table o apfst) ignore_change arg; |
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
|
102 |
|
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
|
103 |
|
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
|
104 |
(* 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
|
105 |
|
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 |
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
|
107 |
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
|
108 |
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
|
109 |
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
|
110 |
in |
56054 | 111 |
if pointer_eq (change1, change2) andalso pointer_eq (table1, table2) then arg1 |
112 |
else if is_empty arg2 then arg1 |
|
113 |
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
|
114 |
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
|
115 |
(case merge_change (change1, change2) of |
56067 | 116 |
NONE => make_change_table (No_Change, Table.join f (table1, table2)) |
56139
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
117 |
| SOME (swapped, ch2, change') => |
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
|
118 |
let |
56139
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
119 |
fun maybe_swap (x, y) = if swapped then (y, x) else (x, y); |
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
120 |
val (tab1, tab2) = maybe_swap (table1, table2); |
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
121 |
fun update key tab = |
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
122 |
(case Table.lookup tab2 key of |
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
123 |
NONE => tab |
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
|
124 |
| SOME y => |
56139
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
125 |
(case Table.lookup tab key of |
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
126 |
NONE => Table.update (key, y) tab |
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
|
127 |
| SOME x => |
56139
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
128 |
(case (SOME (f key (maybe_swap (x, y))) handle Table.SAME => NONE) of |
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
129 |
NONE => tab |
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
130 |
| SOME z => Table.update (key, z) tab))); |
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56068
diff
changeset
|
131 |
in make_change_table (change', Table.fold (update o #1) ch2 tab1) end) |
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
|
132 |
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
|
133 |
|
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 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
|
135 |
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
|
136 |
|
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 |
|
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 |
(* 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
|
139 |
|
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 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
|
141 |
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
|
142 |
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
|
143 |
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
|
144 |
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
|
145 |
|
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 |
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
|
147 |
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
|
148 |
|
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
|
149 |
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
|
150 |
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
|
151 |
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
|
152 |
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
|
153 |
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
|
154 |
|
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
|
155 |
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
|
156 |
|
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
|
157 |
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
|
158 |