|
13841
|
1 |
%
|
|
|
2 |
\begin{isabellebody}%
|
|
|
3 |
\def\isabellecontext{Trie{\isadigit{2}}}%
|
|
|
4 |
\isamarkupfalse%
|
|
|
5 |
%
|
|
|
6 |
\begin{isamarkuptext}%
|
|
|
7 |
Die above definition of \isa{update} has the disadvantage
|
|
|
8 |
that it often creates junk: each association list it passes through is
|
|
|
9 |
extended at the left end with a new (letter,value) pair without
|
|
|
10 |
removing any old association of that letter which may already be
|
|
|
11 |
present. Logically, such cleaning up is unnecessary because \isa{assoc} always searches the list from the left. However, it constitutes
|
|
|
12 |
a space leak: the old associations cannot be garbage collected because
|
|
|
13 |
physically they are still reachable. This problem can be solved by
|
|
|
14 |
means of a function%
|
|
|
15 |
\end{isamarkuptext}%
|
|
|
16 |
\isamarkuptrue%
|
|
|
17 |
\isacommand{consts}\ overwrite\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}b{\isacharparenright}\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}b{\isacharparenright}\ list{\isachardoublequote}\isamarkupfalse%
|
|
|
18 |
%
|
|
|
19 |
\begin{isamarkuptext}%
|
|
|
20 |
that does not just add new pairs at the front but replaces old
|
|
|
21 |
associations by new pairs if possible.
|
|
|
22 |
|
|
|
23 |
Define \isa{overwrite}, modify \isa{modify} to employ \isa{overwrite}, and show the same relationship between \isa{modify} and
|
|
|
24 |
\isa{lookup} as before.%
|
|
|
25 |
\end{isamarkuptext}%
|
|
|
26 |
\isamarkuptrue%
|
|
|
27 |
\isamarkupfalse%
|
|
|
28 |
\end{isabellebody}%
|
|
|
29 |
%%% Local Variables:
|
|
|
30 |
%%% mode: latex
|
|
|
31 |
%%% TeX-master: "root"
|
|
|
32 |
%%% End:
|