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