13739
|
1 |
(*<*)
|
|
2 |
theory Trie2 = Main:
|
|
3 |
(*>*)
|
|
4 |
|
|
5 |
text {* Die above definition of @{term update} has the disadvantage
|
|
6 |
that it often creates junk: each association list it passes through is
|
|
7 |
extended at the left end with a new (letter,value) pair without
|
|
8 |
removing any old association of that letter which may already be
|
|
9 |
present. Logically, such cleaning up is unnecessary because @{term
|
|
10 |
assoc} always searches the list from the left. However, it constitutes
|
|
11 |
a space leak: the old associations cannot be garbage collected because
|
|
12 |
physically they are still reachable. This problem can be solved by
|
|
13 |
means of a function *}
|
|
14 |
|
|
15 |
consts overwrite :: "'a \<Rightarrow> 'b \<Rightarrow> ('a * 'b) list \<Rightarrow> ('a * 'b) list"
|
|
16 |
|
|
17 |
text {* that does not just add new pairs at the front but replaces old
|
|
18 |
associations by new pairs if possible.
|
|
19 |
|
|
20 |
Define @{term overwrite}, modify @{term modify} to employ @{term
|
|
21 |
overwrite}, and show the same relationship between @{term modify} and
|
|
22 |
@{term lookup} as before. *}
|
|
23 |
|
|
24 |
(*<*)
|
|
25 |
end;
|
|
26 |
(*>*)
|