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