author | haftmann |
Wed, 21 Jan 2009 16:47:32 +0100 | |
changeset 29581 | b3b33e0298eb |
parent 29160 | 86e9f91a0ba4 |
child 29612 | 4f68e0f8f4fd |
permissions | -rw-r--r-- |
18537 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{ML}% |
|
4 |
% |
|
5 |
\isadelimtheory |
|
6 |
\isanewline |
|
18543 | 7 |
\isanewline |
18537 | 8 |
% |
9 |
\endisadelimtheory |
|
10 |
% |
|
11 |
\isatagtheory |
|
12 |
\isacommand{theory}\isamarkupfalse% |
|
18543 | 13 |
\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}% |
14 |
\endisatagtheory |
|
15 |
{\isafoldtheory}% |
|
16 |
% |
|
17 |
\isadelimtheory |
|
18 |
% |
|
19 |
\endisadelimtheory |
|
20 |
% |
|
26437 | 21 |
\isamarkupchapter{Advanced ML programming% |
18543 | 22 |
} |
23 |
\isamarkuptrue% |
|
24 |
% |
|
24089 | 25 |
\isamarkupsection{Style% |
26 |
} |
|
27 |
\isamarkuptrue% |
|
28 |
% |
|
18543 | 29 |
\begin{isamarkuptext}% |
26459 | 30 |
Like any style guide, also this one should not be interpreted dogmatically, but |
31 |
with care and discernment. It consists of a collection of |
|
32 |
recommendations which have been turned out useful over long years of |
|
33 |
Isabelle system development and are supposed to support writing of readable |
|
34 |
and managable code. Special cases encourage derivations, |
|
35 |
as far as you know what you are doing. |
|
36 |
\footnote{This style guide is loosely based on |
|
37 |
\url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html}} |
|
21148 | 38 |
|
39 |
\begin{description} |
|
40 |
||
41 |
\item[fundamental law of programming] |
|
42 |
Whenever writing code, keep in mind: A program is |
|
43 |
written once, modified ten times, and read |
|
26459 | 44 |
hundred times. So simplify its writing, |
21148 | 45 |
always keep future modifications in mind, |
21172 | 46 |
and never jeopardize readability. Every second you hesitate |
21148 | 47 |
to spend on making your code more clear you will |
48 |
have to spend ten times understanding what you have |
|
49 |
written later on. |
|
50 |
||
51 |
\item[white space matters] |
|
52 |
Treat white space in your code as if it determines |
|
53 |
the meaning of code. |
|
54 |
||
55 |
\begin{itemize} |
|
56 |
||
57 |
\item The space bar is the easiest key to find on the keyboard, |
|
24089 | 58 |
press it as often as necessary. \verb|2 + 2| is better |
59 |
than \verb|2+2|, likewise \verb|f (x, y)| is |
|
60 |
better than \verb|f(x,y)|. |
|
21148 | 61 |
|
24089 | 62 |
\item Restrict your lines to 80 characters. This will allow |
63 |
you to keep the beginning of a line in view while watching |
|
64 |
its end.\footnote{To acknowledge the lax practice of |
|
65 |
text editing these days, we tolerate as much as 100 |
|
66 |
characters per line, but anything beyond 120 is not |
|
67 |
considered proper source text.} |
|
21148 | 68 |
|
24089 | 69 |
\item Ban tabulators; they are a context-sensitive formatting |
70 |
feature and likely to confuse anyone not using your favorite |
|
71 |
editor.\footnote{Some modern programming language even |
|
72 |
forbid tabulators altogether according to the formal syntax |
|
73 |
definition.} |
|
21148 | 74 |
|
75 |
\item Get rid of trailing whitespace. Instead, do not |
|
24089 | 76 |
suppress a trailing newline at the end of your files. |
21148 | 77 |
|
78 |
\item Choose a generally accepted style of indentation, |
|
79 |
then use it systematically throughout the whole |
|
80 |
application. An indentation of two spaces is appropriate. |
|
81 |
Avoid dangling indentation. |
|
82 |
||
83 |
\end{itemize} |
|
84 |
||
85 |
\item[cut-and-paste succeeds over copy-and-paste] |
|
24089 | 86 |
\emph{Never} copy-and-paste code when programming. If you |
21148 | 87 |
need the same piece of code twice, introduce a |
88 |
reasonable auxiliary function (if there is no |
|
89 |
such function, very likely you got something wrong). |
|
90 |
Any copy-and-paste will turn out to be painful |
|
26459 | 91 |
when something has to be changed later on. |
21148 | 92 |
|
93 |
\item[comments] |
|
94 |
are a device which requires careful thinking before using |
|
95 |
it. The best comment for your code should be the code itself. |
|
96 |
Prefer efforts to write clear, understandable code |
|
97 |
over efforts to explain nasty code. |
|
98 |
||
99 |
\item[functional programming is based on functions] |
|
26459 | 100 |
Model things as abstract as appropriate. Avoid unnecessarrily |
101 |
concrete datatype representations. For example, consider a function |
|
102 |
taking some table data structure as argument and performing |
|
103 |
lookups on it. Instead of taking a table, it could likewise |
|
104 |
take just a lookup function. Accustom |
|
24089 | 105 |
your way of coding to the level of expressiveness a functional |
106 |
programming language is giving onto you. |
|
21148 | 107 |
|
108 |
\item[tuples] |
|
109 |
are often in the way. When there is no striking argument |
|
110 |
to tuple function arguments, just write your function curried. |
|
111 |
||
112 |
\item[telling names] |
|
24089 | 113 |
Any name should tell its purpose as exactly as possible, while |
114 |
keeping its length to the absolutely necessary minimum. Always |
|
115 |
give the same name to function arguments which have the same |
|
116 |
meaning. Separate words by underscores (\verb|int_of_string|, not \verb|intOfString|).\footnote{Some |
|
117 |
recent tools for Emacs include special precautions to cope with |
|
118 |
bumpy names in \isa{camelCase}, e.g.\ for improved on-screen |
|
119 |
readability. It is easier to abstain from using such names in the |
|
120 |
first place.} |
|
21148 | 121 |
|
122 |
\end{description}% |
|
18543 | 123 |
\end{isamarkuptext}% |
124 |
\isamarkuptrue% |
|
125 |
% |
|
24089 | 126 |
\isamarkupsection{Thread-safe programming% |
127 |
} |
|
128 |
\isamarkuptrue% |
|
129 |
% |
|
130 |
\begin{isamarkuptext}% |
|
29160 | 131 |
Recent versions of Poly/ML (5.2.1 or later) support robust |
132 |
multithreaded execution, based on native operating system threads of |
|
133 |
the underlying platform. Thus threads will actually be executed in |
|
134 |
parallel on multi-core systems. A speedup-factor of approximately |
|
135 |
1.5--3 can be expected on a regular 4-core machine.\footnote{There |
|
136 |
is some inherent limitation of the speedup factor due to garbage |
|
137 |
collection, which is still sequential. It helps to provide initial |
|
138 |
heap space generously, using the \texttt{-H} option of Poly/ML.} |
|
139 |
Threads also help to organize advanced operations of the system, |
|
140 |
with explicit communication between sub-components, real-time |
|
141 |
conditions, time-outs etc. |
|
24089 | 142 |
|
29160 | 143 |
Threads lack the memory protection of separate processes, and |
24089 | 144 |
operate concurrently on shared heap memory. This has the advantage |
145 |
that results of independent computations are immediately available |
|
29160 | 146 |
to other threads, without requiring untyped character streams, |
147 |
awkward serialization etc. |
|
24089 | 148 |
|
149 |
On the other hand, some programming guidelines need to be observed |
|
150 |
in order to make unprotected parallelism work out smoothly. While |
|
151 |
the ML system implementation is responsible to maintain basic |
|
152 |
integrity of the representation of ML values in memory, the |
|
153 |
application programmer needs to ensure that multithreaded execution |
|
154 |
does not break the intended semantics. |
|
155 |
||
156 |
\medskip \paragraph{Critical shared resources.} Actually only those |
|
157 |
parts outside the purely functional world of ML are critical. In |
|
158 |
particular, this covers |
|
159 |
||
160 |
\begin{itemize} |
|
161 |
||
162 |
\item global references (or arrays), i.e.\ those that persist over |
|
163 |
several invocations of associated operations,\footnote{This is |
|
164 |
independent of the visibility of such mutable values in the toplevel |
|
165 |
scope.} |
|
166 |
||
167 |
\item direct I/O on shared channels, notably \isa{stdin}, \isa{stdout}, \isa{stderr}. |
|
168 |
||
169 |
\end{itemize} |
|
170 |
||
171 |
The majority of tools implemented within the Isabelle/Isar framework |
|
172 |
will not require any of these critical elements: nothing special |
|
173 |
needs to be observed when staying in the purely functional fragment |
|
174 |
of ML. Note that output via the official Isabelle channels does not |
|
29160 | 175 |
count as direct I/O, so the operations \verb|writeln|, \verb|warning|, \verb|tracing| etc.\ are safe. |
176 |
||
177 |
Moreover, ML bindings within the toplevel environment (\verb|type|, \verb|val|, \verb|structure| etc.) due to |
|
178 |
run-time invocation of the compiler are also safe, because |
|
179 |
Isabelle/Isar manages this as part of the theory or proof context. |
|
24089 | 180 |
|
29160 | 181 |
\paragraph{Multithreading in Isabelle/Isar.} The theory loader |
182 |
automatically exploits the overall parallelism of independent nodes |
|
183 |
in the development graph, as well as the inherent irrelevance of |
|
184 |
proofs for goals being fully specified in advance. This means, |
|
185 |
checking of individual Isar proofs is parallelized by default. |
|
186 |
Beyond that, very sophisticated proof tools may use local |
|
187 |
parallelism internally, via the general programming model of |
|
188 |
``future values'' (see also \hyperlink{file.~~/src/Pure/Concurrent/future.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}future{\isachardot}ML}}}}). |
|
24089 | 189 |
|
29160 | 190 |
Any ML code that works relatively to the present background theory |
24089 | 191 |
is already safe. Contextual data may be easily stored within the |
24090 | 192 |
theory or proof context, thanks to the generic data concept of |
193 |
Isabelle/Isar (see \secref{sec:context-data}). This greatly |
|
24089 | 194 |
diminishes the demand for global state information in the first |
195 |
place. |
|
196 |
||
197 |
\medskip In rare situations where actual mutable content needs to be |
|
198 |
manipulated, Isabelle provides a single \emph{critical section} that |
|
199 |
may be entered while preventing any other thread from doing the |
|
200 |
same. Entering the critical section without contention is very |
|
201 |
fast, and several basic system operations do so frequently. This |
|
202 |
also means that each thread should leave the critical section |
|
203 |
quickly, otherwise parallel execution performance may degrade |
|
204 |
significantly. |
|
205 |
||
29160 | 206 |
Despite this potential bottle-neck, centralized locking is |
207 |
convenient, because it prevents deadlocks without demanding special |
|
208 |
precautions. Explicit communication demands other means, though. |
|
209 |
The high-level abstraction of synchronized variables \hyperlink{file.~~/src/Pure/Concurrent/synchronized.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}synchronized{\isachardot}ML}}}} enables parallel |
|
210 |
components to communicate via shared state; see also \hyperlink{file.~~/src/Pure/Concurrent/mailbox.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}mailbox{\isachardot}ML}}}} as canonical example. |
|
24089 | 211 |
|
212 |
\paragraph{Good conduct of impure programs.} The following |
|
213 |
guidelines enable non-functional programs to participate in |
|
214 |
multithreading. |
|
215 |
||
216 |
\begin{itemize} |
|
217 |
||
218 |
\item Minimize global state information. Using proper theory and |
|
219 |
proof context data will actually return to functional update of |
|
220 |
values, without any special precautions for multithreading. Apart |
|
221 |
from the fully general functors for theory and proof data (see |
|
222 |
\secref{sec:context-data}) there are drop-in replacements that |
|
24090 | 223 |
emulate primitive references for common cases of \emph{configuration |
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24090
diff
changeset
|
224 |
options} for type \verb|bool|/\verb|int|/\verb|string| (see structure \verb|Config| and \verb|Attrib.config_bool| etc.), and lists of theorems (see functor |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24090
diff
changeset
|
225 |
\verb|NamedThmsFun|). |
24089 | 226 |
|
227 |
\item Keep components with local state information |
|
228 |
\emph{re-entrant}. Instead of poking initial values into (private) |
|
229 |
global references, create a new state record on each invocation, and |
|
230 |
pass that through any auxiliary functions of the component. The |
|
231 |
state record may well contain mutable references, without requiring |
|
232 |
any special synchronizations, as long as each invocation sees its |
|
233 |
own copy. Occasionally, one might even return to plain functional |
|
234 |
updates on non-mutable record values here. |
|
235 |
||
236 |
\item Isolate process configuration flags. The main legitimate |
|
237 |
application of global references is to configure the whole process |
|
238 |
in a certain way, essentially affecting all threads. A typical |
|
239 |
example is the \verb|show_types| flag, which tells the pretty printer |
|
240 |
to output explicit type information for terms. Such flags usually |
|
241 |
do not affect the functionality of the core system, but only the |
|
24090 | 242 |
view being presented to the user. |
24089 | 243 |
|
244 |
Occasionally, such global process flags are treated like implicit |
|
245 |
arguments to certain operations, by using the \verb|setmp| combinator |
|
24090 | 246 |
for safe temporary assignment. Its traditional purpose was to |
247 |
ensure proper recovery of the original value when exceptions are |
|
248 |
raised in the body, now the functionality is extended to enter the |
|
249 |
\emph{critical section} (with its usual potential of degrading |
|
250 |
parallelism). |
|
24089 | 251 |
|
252 |
Note that recovery of plain value passing semantics via \verb|setmp|~\isa{ref\ value} assumes that this \isa{ref} is |
|
253 |
exclusively manipulated within the critical section. In particular, |
|
254 |
any persistent global assignment of \isa{ref\ {\isacharcolon}{\isacharequal}\ value} needs to |
|
255 |
be marked critical as well, to prevent intruding another threads |
|
256 |
local view, and a lost-update in the global scope, too. |
|
257 |
||
258 |
\end{itemize} |
|
259 |
||
260 |
Recall that in an open ``LCF-style'' system like Isabelle/Isar, the |
|
261 |
user participates in constructing the overall environment. This |
|
24090 | 262 |
means that state-based facilities offered by one component will |
263 |
require special caution later on. So minimizing critical elements, |
|
264 |
by staying within the plain value-oriented view relative to theory |
|
265 |
or proof contexts most of the time, will also reduce the chance of |
|
24089 | 266 |
mishaps occurring to end-users.% |
267 |
\end{isamarkuptext}% |
|
268 |
\isamarkuptrue% |
|
269 |
% |
|
270 |
\isadelimmlref |
|
271 |
% |
|
272 |
\endisadelimmlref |
|
273 |
% |
|
274 |
\isatagmlref |
|
275 |
% |
|
276 |
\begin{isamarkuptext}% |
|
277 |
\begin{mldecls} |
|
26854
9b4aec46ad78
improved treatment of "_" thanks to underscore.sty;
wenzelm
parents:
26460
diff
changeset
|
278 |
\indexml{NAMED\_CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\ |
24089 | 279 |
\indexml{CRITICAL}\verb|CRITICAL: (unit -> 'a) -> 'a| \\ |
280 |
\indexml{setmp}\verb|setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\ |
|
281 |
\end{mldecls} |
|
282 |
||
283 |
\begin{description} |
|
284 |
||
285 |
\item \verb|NAMED_CRITICAL|~\isa{name\ f} evaluates \isa{f\ {\isacharparenleft}{\isacharparenright}} |
|
24090 | 286 |
while staying within the critical section of Isabelle/Isar. No |
287 |
other thread may do so at the same time, but non-critical parallel |
|
288 |
execution will continue. The \isa{name} argument serves for |
|
289 |
diagnostic purposes and might help to spot sources of congestion. |
|
24089 | 290 |
|
291 |
\item \verb|CRITICAL| is the same as \verb|NAMED_CRITICAL| with empty |
|
292 |
name argument. |
|
293 |
||
294 |
\item \verb|setmp|~\isa{ref\ value\ f\ x} evaluates \isa{f\ x} |
|
295 |
while staying within the critical section and having \isa{ref\ {\isacharcolon}{\isacharequal}\ value} assigned temporarily. This recovers a value-passing |
|
296 |
semantics involving global references, regardless of exceptions or |
|
297 |
concurrency. |
|
298 |
||
299 |
\end{description}% |
|
300 |
\end{isamarkuptext}% |
|
301 |
\isamarkuptrue% |
|
302 |
% |
|
303 |
\endisatagmlref |
|
304 |
{\isafoldmlref}% |
|
305 |
% |
|
306 |
\isadelimmlref |
|
307 |
% |
|
308 |
\endisadelimmlref |
|
309 |
% |
|
18543 | 310 |
\isamarkupchapter{Basic library functions% |
311 |
} |
|
312 |
\isamarkuptrue% |
|
313 |
% |
|
314 |
\begin{isamarkuptext}% |
|
22293 | 315 |
Beyond the proposal of the SML/NJ basis library, Isabelle comes |
316 |
with its own library, from which selected parts are given here. |
|
26459 | 317 |
These should encourage a study of the Isabelle sources, |
318 |
in particular files \emph{Pure/library.ML} and \emph{Pure/General/*.ML}.% |
|
22293 | 319 |
\end{isamarkuptext}% |
320 |
\isamarkuptrue% |
|
321 |
% |
|
322 |
\isamarkupsection{Linear transformations% |
|
323 |
} |
|
324 |
\isamarkuptrue% |
|
325 |
% |
|
326 |
\isadelimmlref |
|
327 |
% |
|
328 |
\endisadelimmlref |
|
329 |
% |
|
330 |
\isatagmlref |
|
331 |
% |
|
332 |
\begin{isamarkuptext}% |
|
333 |
\begin{mldecls} |
|
24089 | 334 |
\indexml{op |$>$ }\verb|op |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\ |
22293 | 335 |
\end{mldecls}% |
336 |
\end{isamarkuptext}% |
|
337 |
\isamarkuptrue% |
|
338 |
% |
|
339 |
\endisatagmlref |
|
340 |
{\isafoldmlref}% |
|
341 |
% |
|
342 |
\isadelimmlref |
|
343 |
% |
|
344 |
\endisadelimmlref |
|
345 |
% |
|
22322 | 346 |
\isadelimML |
347 |
% |
|
348 |
\endisadelimML |
|
349 |
% |
|
350 |
\isatagML |
|
351 |
% |
|
352 |
\endisatagML |
|
353 |
{\isafoldML}% |
|
354 |
% |
|
355 |
\isadelimML |
|
356 |
% |
|
357 |
\endisadelimML |
|
358 |
% |
|
22293 | 359 |
\begin{isamarkuptext}% |
26460 | 360 |
\noindent Many problems in functional programming can be thought of |
22322 | 361 |
as linear transformations, i.e.~a caluclation starts with a |
26459 | 362 |
particular value \verb|x : foo| which is then transformed |
363 |
by application of a function \verb|f : foo -> foo|, |
|
364 |
continued by an application of a function \verb|g : foo -> bar|, |
|
25151 | 365 |
and so on. As a canoncial example, take functions enriching |
366 |
a theory by constant declararion and primitive definitions: |
|
367 |
||
26459 | 368 |
\smallskip\begin{mldecls} |
29581 | 369 |
\verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix|\isasep\isanewline% |
26459 | 370 |
\verb| -> theory -> term * theory| \\ |
371 |
\verb|Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory| |
|
372 |
\end{mldecls} |
|
25151 | 373 |
|
26460 | 374 |
\noindent Written with naive application, an addition of constant |
25151 | 375 |
\isa{bar} with type \isa{foo\ {\isasymRightarrow}\ foo} and |
26459 | 376 |
a corresponding definition \isa{bar\ {\isasymequiv}\ {\isasymlambda}x{\isachardot}\ x} would look like: |
25151 | 377 |
|
26459 | 378 |
\smallskip\begin{mldecls} |
379 |
\verb|(fn (t, thy) => Thm.add_def false false|\isasep\isanewline% |
|
25151 | 380 |
\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline% |
381 |
\verb| (Sign.declare_const []|\isasep\isanewline% |
|
29008 | 382 |
\verb| ((Binding.name "bar", @{typ "foo => foo"}), NoSyn) thy)| |
26459 | 383 |
\end{mldecls} |
25151 | 384 |
|
26460 | 385 |
\noindent With increasing numbers of applications, this code gets quite |
25151 | 386 |
unreadable. Further, it is unintuitive that things are |
387 |
written down in the opposite order as they actually ``happen''.% |
|
22322 | 388 |
\end{isamarkuptext}% |
389 |
\isamarkuptrue% |
|
390 |
% |
|
391 |
\begin{isamarkuptext}% |
|
25151 | 392 |
\noindent At this stage, Isabelle offers some combinators which allow |
393 |
for more convenient notation, most notably reverse application: |
|
26459 | 394 |
|
395 |
\smallskip\begin{mldecls} |
|
22322 | 396 |
\verb|thy|\isasep\isanewline% |
29008 | 397 |
\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline% |
25151 | 398 |
\verb||\verb,|,\verb|> (fn (t, thy) => thy|\isasep\isanewline% |
25608 | 399 |
\verb||\verb,|,\verb|> Thm.add_def false false|\isasep\isanewline% |
25151 | 400 |
\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))| |
26459 | 401 |
\end{mldecls}% |
22293 | 402 |
\end{isamarkuptext}% |
403 |
\isamarkuptrue% |
|
404 |
% |
|
405 |
\isadelimmlref |
|
406 |
% |
|
407 |
\endisadelimmlref |
|
408 |
% |
|
409 |
\isatagmlref |
|
410 |
% |
|
411 |
\begin{isamarkuptext}% |
|
412 |
\begin{mldecls} |
|
24089 | 413 |
\indexml{op |-$>$ }\verb|op |\verb,|,\verb|-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\ |
414 |
\indexml{op |$>$$>$ }\verb|op |\verb,|,\verb|>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c| \\ |
|
415 |
\indexml{op ||$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|> : ('c * 'a) * ('a -> 'b) -> 'c * 'b| \\ |
|
416 |
\indexml{op ||$>$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b| \\ |
|
25151 | 417 |
\end{mldecls}% |
418 |
\end{isamarkuptext}% |
|
419 |
\isamarkuptrue% |
|
420 |
% |
|
421 |
\endisatagmlref |
|
422 |
{\isafoldmlref}% |
|
423 |
% |
|
424 |
\isadelimmlref |
|
425 |
% |
|
426 |
\endisadelimmlref |
|
427 |
% |
|
428 |
\begin{isamarkuptext}% |
|
429 |
\noindent Usually, functions involving theory updates also return |
|
430 |
side results; to use these conveniently, yet another |
|
431 |
set of combinators is at hand, most notably \verb|op |\verb,|,\verb|->| |
|
432 |
which allows curried access to side results: |
|
26459 | 433 |
|
434 |
\smallskip\begin{mldecls} |
|
25151 | 435 |
\verb|thy|\isasep\isanewline% |
29008 | 436 |
\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline% |
25608 | 437 |
\verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline% |
25151 | 438 |
\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline% |
439 |
||
26459 | 440 |
\end{mldecls} |
25151 | 441 |
|
442 |
\noindent \verb|op |\verb,|,\verb|>>| allows for processing side results on their own: |
|
26459 | 443 |
|
444 |
\smallskip\begin{mldecls} |
|
25151 | 445 |
\verb|thy|\isasep\isanewline% |
29008 | 446 |
\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline% |
25151 | 447 |
\verb||\verb,|,\verb|>> (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline% |
25608 | 448 |
\verb||\verb,|,\verb|-> (fn def => Thm.add_def false false ("bar_def", def))|\isasep\isanewline% |
25151 | 449 |
|
26459 | 450 |
\end{mldecls} |
25151 | 451 |
|
452 |
\noindent Orthogonally, \verb|op |\verb,|,\verb||\verb,|,\verb|>| applies a transformation |
|
453 |
in the presence of side results which are left unchanged: |
|
26459 | 454 |
|
455 |
\smallskip\begin{mldecls} |
|
25151 | 456 |
\verb|thy|\isasep\isanewline% |
29008 | 457 |
\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline% |
25151 | 458 |
\verb||\verb,|,\verb||\verb,|,\verb|> Sign.add_path "foobar"|\isasep\isanewline% |
25608 | 459 |
\verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline% |
25151 | 460 |
\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline% |
461 |
\verb||\verb,|,\verb||\verb,|,\verb|> Sign.restore_naming thy|\isasep\isanewline% |
|
462 |
||
26459 | 463 |
\end{mldecls} |
25151 | 464 |
|
26459 | 465 |
\noindent \verb|op |\verb,|,\verb||\verb,|,\verb|>>| accumulates side results: |
466 |
||
467 |
\smallskip\begin{mldecls} |
|
25151 | 468 |
\verb|thy|\isasep\isanewline% |
29008 | 469 |
\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline% |
470 |
\verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const [] ((Binding.name "foobar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline% |
|
25608 | 471 |
\verb||\verb,|,\verb|-> (fn (t1, t2) => Thm.add_def false false|\isasep\isanewline% |
25151 | 472 |
\verb| ("bar_def", Logic.mk_equals (t1, t2)))|\isasep\isanewline% |
473 |
||
26459 | 474 |
\end{mldecls}% |
25151 | 475 |
\end{isamarkuptext}% |
476 |
\isamarkuptrue% |
|
477 |
% |
|
478 |
\isadelimmlref |
|
479 |
% |
|
480 |
\endisadelimmlref |
|
481 |
% |
|
482 |
\isatagmlref |
|
483 |
% |
|
484 |
\begin{isamarkuptext}% |
|
485 |
\begin{mldecls} |
|
486 |
\indexml{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\ |
|
26854
9b4aec46ad78
improved treatment of "_" thanks to underscore.sty;
wenzelm
parents:
26460
diff
changeset
|
487 |
\indexml{fold\_map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\ |
22293 | 488 |
\end{mldecls}% |
489 |
\end{isamarkuptext}% |
|
490 |
\isamarkuptrue% |
|
491 |
% |
|
22322 | 492 |
\endisatagmlref |
493 |
{\isafoldmlref}% |
|
494 |
% |
|
495 |
\isadelimmlref |
|
496 |
% |
|
497 |
\endisadelimmlref |
|
498 |
% |
|
499 |
\begin{isamarkuptext}% |
|
26459 | 500 |
\noindent This principles naturally lift to \emph{lists} using |
25151 | 501 |
the \verb|fold| and \verb|fold_map| combinators. |
502 |
The first lifts a single function |
|
26459 | 503 |
\begin{quote}\footnotesize |
504 |
\verb|f : 'a -> 'b -> 'b| to \verb|'a list -> 'b -> 'b| |
|
505 |
\end{quote} |
|
25151 | 506 |
such that |
26459 | 507 |
\begin{quote}\footnotesize |
508 |
\verb|y |\verb,|,\verb|> fold f [x1, x2, ..., x_n]| \\ |
|
509 |
\hspace*{2ex}\isa{{\isasymleadsto}} \verb|y |\verb,|,\verb|> f x1 |\verb,|,\verb|> f x2 |\verb,|,\verb|> ... |\verb,|,\verb|> f x_n| |
|
510 |
\end{quote} |
|
26460 | 511 |
\noindent The second accumulates side results in a list by lifting |
25151 | 512 |
a single function |
26459 | 513 |
\begin{quote}\footnotesize |
514 |
\verb|f : 'a -> 'b -> 'c * 'b| to \verb|'a list -> 'b -> 'c list * 'b| |
|
515 |
\end{quote} |
|
25151 | 516 |
such that |
26459 | 517 |
\begin{quote}\footnotesize |
518 |
\verb|y |\verb,|,\verb|> fold_map f [x1, x2, ..., x_n]| \\ |
|
519 |
\hspace*{2ex}\isa{{\isasymleadsto}} \verb|y |\verb,|,\verb|> f x1 |\verb,|,\verb||\verb,|,\verb|>> f x2 |\verb,|,\verb||\verb,|,\verb|>> ... |\verb,|,\verb||\verb,|,\verb|>> f x_n| \\ |
|
520 |
\hspace*{6ex}\verb||\verb,|,\verb||\verb,|,\verb|> (fn ((z1, z2), ..., z_n) => [z1, z2, ..., z_n])| |
|
521 |
\end{quote} |
|
25185 | 522 |
|
26459 | 523 |
\noindent Example: |
524 |
||
525 |
\smallskip\begin{mldecls} |
|
25185 | 526 |
\verb|let|\isasep\isanewline% |
527 |
\verb| val consts = ["foo", "bar"];|\isasep\isanewline% |
|
528 |
\verb|in|\isasep\isanewline% |
|
529 |
\verb| thy|\isasep\isanewline% |
|
530 |
\verb| |\verb,|,\verb|> fold_map (fn const => Sign.declare_const []|\isasep\isanewline% |
|
29008 | 531 |
\verb| ((Binding.name const, @{typ "foo => foo"}), NoSyn)) consts|\isasep\isanewline% |
25185 | 532 |
\verb| |\verb,|,\verb|>> map (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline% |
533 |
\verb| |\verb,|,\verb|-> (fn defs => fold_map (fn def =>|\isasep\isanewline% |
|
25608 | 534 |
\verb| Thm.add_def false false ("", def)) defs)|\isasep\isanewline% |
26459 | 535 |
\verb|end| |
536 |
\end{mldecls}% |
|
22322 | 537 |
\end{isamarkuptext}% |
538 |
\isamarkuptrue% |
|
539 |
% |
|
540 |
\isadelimmlref |
|
541 |
% |
|
542 |
\endisadelimmlref |
|
543 |
% |
|
544 |
\isatagmlref |
|
545 |
% |
|
22293 | 546 |
\begin{isamarkuptext}% |
547 |
\begin{mldecls} |
|
24089 | 548 |
\indexml{op \#$>$ }\verb|op #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\ |
549 |
\indexml{op \#-$>$ }\verb|op #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd| \\ |
|
550 |
\indexml{op \#$>$$>$ }\verb|op #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b| \\ |
|
551 |
\indexml{op \#\#$>$ }\verb|op ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd| \\ |
|
552 |
\indexml{op \#\#$>$$>$ }\verb|op ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd| \\ |
|
22293 | 553 |
\end{mldecls}% |
554 |
\end{isamarkuptext}% |
|
555 |
\isamarkuptrue% |
|
556 |
% |
|
22322 | 557 |
\endisatagmlref |
558 |
{\isafoldmlref}% |
|
559 |
% |
|
560 |
\isadelimmlref |
|
561 |
% |
|
562 |
\endisadelimmlref |
|
563 |
% |
|
564 |
\begin{isamarkuptext}% |
|
22550 | 565 |
\noindent All those linear combinators also exist in higher-order |
566 |
variants which do not expect a value on the left hand side |
|
567 |
but a function.% |
|
22322 | 568 |
\end{isamarkuptext}% |
569 |
\isamarkuptrue% |
|
570 |
% |
|
571 |
\isadelimmlref |
|
572 |
% |
|
573 |
\endisadelimmlref |
|
574 |
% |
|
575 |
\isatagmlref |
|
576 |
% |
|
22293 | 577 |
\begin{isamarkuptext}% |
578 |
\begin{mldecls} |
|
24089 | 579 |
\indexml{op ` }\verb|op ` : ('b -> 'a) -> 'b -> 'a * 'b| \\ |
22293 | 580 |
\indexml{tap}\verb|tap: ('b -> 'a) -> 'b -> 'b| \\ |
581 |
\end{mldecls}% |
|
582 |
\end{isamarkuptext}% |
|
583 |
\isamarkuptrue% |
|
584 |
% |
|
585 |
\endisatagmlref |
|
586 |
{\isafoldmlref}% |
|
587 |
% |
|
588 |
\isadelimmlref |
|
589 |
% |
|
590 |
\endisadelimmlref |
|
591 |
% |
|
22550 | 592 |
\begin{isamarkuptext}% |
25185 | 593 |
\noindent These operators allow to ``query'' a context |
594 |
in a series of context transformations: |
|
595 |
||
26459 | 596 |
\smallskip\begin{mldecls} |
25185 | 597 |
\verb|thy|\isasep\isanewline% |
598 |
\verb||\verb,|,\verb|> tap (fn _ => writeln "now adding constant")|\isasep\isanewline% |
|
29008 | 599 |
\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline% |
25185 | 600 |
\verb||\verb,|,\verb||\verb,|,\verb|>> `(fn thy => Sign.declared_const thy|\isasep\isanewline% |
29008 | 601 |
\verb| (Sign.full_name thy (Binding.name "foobar")))|\isasep\isanewline% |
25185 | 602 |
\verb||\verb,|,\verb|-> (fn (t, b) => if b then I|\isasep\isanewline% |
603 |
\verb| else Sign.declare_const []|\isasep\isanewline% |
|
29008 | 604 |
\verb| ((Binding.name "foobar", @{typ "foo => foo"}), NoSyn) #> snd)|\isasep\isanewline% |
25185 | 605 |
|
26459 | 606 |
\end{mldecls}% |
22550 | 607 |
\end{isamarkuptext}% |
608 |
\isamarkuptrue% |
|
609 |
% |
|
22293 | 610 |
\isamarkupsection{Options and partiality% |
611 |
} |
|
612 |
\isamarkuptrue% |
|
613 |
% |
|
614 |
\isadelimmlref |
|
615 |
% |
|
616 |
\endisadelimmlref |
|
617 |
% |
|
618 |
\isatagmlref |
|
619 |
% |
|
620 |
\begin{isamarkuptext}% |
|
621 |
\begin{mldecls} |
|
26854
9b4aec46ad78
improved treatment of "_" thanks to underscore.sty;
wenzelm
parents:
26460
diff
changeset
|
622 |
\indexml{is\_some}\verb|is_some: 'a option -> bool| \\ |
9b4aec46ad78
improved treatment of "_" thanks to underscore.sty;
wenzelm
parents:
26460
diff
changeset
|
623 |
\indexml{is\_none}\verb|is_none: 'a option -> bool| \\ |
22293 | 624 |
\indexml{the}\verb|the: 'a option -> 'a| \\ |
625 |
\indexml{these}\verb|these: 'a list option -> 'a list| \\ |
|
26854
9b4aec46ad78
improved treatment of "_" thanks to underscore.sty;
wenzelm
parents:
26460
diff
changeset
|
626 |
\indexml{the\_list}\verb|the_list: 'a option -> 'a list| \\ |
9b4aec46ad78
improved treatment of "_" thanks to underscore.sty;
wenzelm
parents:
26460
diff
changeset
|
627 |
\indexml{the\_default}\verb|the_default: 'a -> 'a option -> 'a| \\ |
22293 | 628 |
\indexml{try}\verb|try: ('a -> 'b) -> 'a -> 'b option| \\ |
629 |
\indexml{can}\verb|can: ('a -> 'b) -> 'a -> bool| \\ |
|
630 |
\end{mldecls}% |
|
631 |
\end{isamarkuptext}% |
|
632 |
\isamarkuptrue% |
|
633 |
% |
|
634 |
\endisatagmlref |
|
635 |
{\isafoldmlref}% |
|
636 |
% |
|
637 |
\isadelimmlref |
|
638 |
% |
|
639 |
\endisadelimmlref |
|
640 |
% |
|
641 |
\begin{isamarkuptext}% |
|
24089 | 642 |
Standard selector functions on \isa{option}s are provided. The |
643 |
\verb|try| and \verb|can| functions provide a convenient interface for |
|
26459 | 644 |
handling exceptions -- both take as arguments a function \verb|f| |
645 |
together with a parameter \verb|x| and handle any exception during |
|
646 |
the evaluation of the application of \verb|f| to \verb|x|, either |
|
24089 | 647 |
return a lifted result (\verb|NONE| on failure) or a boolean value |
648 |
(\verb|false| on failure).% |
|
22293 | 649 |
\end{isamarkuptext}% |
650 |
\isamarkuptrue% |
|
651 |
% |
|
652 |
\isamarkupsection{Common data structures% |
|
653 |
} |
|
654 |
\isamarkuptrue% |
|
655 |
% |
|
656 |
\isamarkupsubsection{Lists (as set-like data structures)% |
|
657 |
} |
|
658 |
\isamarkuptrue% |
|
659 |
% |
|
660 |
\begin{isamarkuptext}% |
|
661 |
\begin{mldecls} |
|
662 |
\indexml{member}\verb|member: ('b * 'a -> bool) -> 'a list -> 'b -> bool| \\ |
|
663 |
\indexml{insert}\verb|insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list| \\ |
|
664 |
\indexml{remove}\verb|remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list| \\ |
|
665 |
\indexml{merge}\verb|merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list| \\ |
|
666 |
\end{mldecls}% |
|
667 |
\end{isamarkuptext}% |
|
668 |
\isamarkuptrue% |
|
669 |
% |
|
670 |
\begin{isamarkuptext}% |
|
22503 | 671 |
Lists are often used as set-like data structures -- set-like in |
25151 | 672 |
the sense that they support a notion of \verb|member|-ship, |
22503 | 673 |
\verb|insert|-ing and \verb|remove|-ing, but are order-sensitive. |
674 |
This is convenient when implementing a history-like mechanism: |
|
675 |
\verb|insert| adds an element \emph{to the front} of a list, |
|
676 |
if not yet present; \verb|remove| removes \emph{all} occurences |
|
677 |
of a particular element. Correspondingly \verb|merge| implements a |
|
678 |
a merge on two lists suitable for merges of context data |
|
679 |
(\secref{sec:context-theory}). |
|
680 |
||
681 |
Functions are parametrized by an explicit equality function |
|
682 |
to accomplish overloaded equality; in most cases of monomorphic |
|
24089 | 683 |
equality, writing \verb|op =| should suffice.% |
22293 | 684 |
\end{isamarkuptext}% |
685 |
\isamarkuptrue% |
|
686 |
% |
|
687 |
\isamarkupsubsection{Association lists% |
|
688 |
} |
|
689 |
\isamarkuptrue% |
|
690 |
% |
|
691 |
\begin{isamarkuptext}% |
|
692 |
\begin{mldecls} |
|
693 |
\indexmlexception{AList.DUP}\verb|exception AList.DUP| \\ |
|
694 |
\indexml{AList.lookup}\verb|AList.lookup: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option| \\ |
|
695 |
\indexml{AList.defined}\verb|AList.defined: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool| \\ |
|
696 |
\indexml{AList.update}\verb|AList.update: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\ |
|
697 |
\indexml{AList.default}\verb|AList.default: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\ |
|
698 |
\indexml{AList.delete}\verb|AList.delete: ('a * 'b -> bool) -> 'a -> ('b * 'c) list -> ('b * 'c) list| \\ |
|
26854
9b4aec46ad78
improved treatment of "_" thanks to underscore.sty;
wenzelm
parents:
26460
diff
changeset
|
699 |
\indexml{AList.map\_entry}\verb|AList.map_entry: ('a * 'b -> bool) -> 'a|\isasep\isanewline% |
22293 | 700 |
\verb| -> ('c -> 'c) -> ('b * 'c) list -> ('b * 'c) list| \\ |
26854
9b4aec46ad78
improved treatment of "_" thanks to underscore.sty;
wenzelm
parents:
26460
diff
changeset
|
701 |
\indexml{AList.map\_default}\verb|AList.map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)|\isasep\isanewline% |
22293 | 702 |
\verb| -> ('a * 'b) list -> ('a * 'b) list| \\ |
703 |
\indexml{AList.join}\verb|AList.join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b) (*exception DUP*)|\isasep\isanewline% |
|
704 |
\verb| -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)| \\ |
|
705 |
\indexml{AList.merge}\verb|AList.merge: ('a * 'a -> bool) -> ('b * 'b -> bool)|\isasep\isanewline% |
|
706 |
\verb| -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)| |
|
707 |
\end{mldecls}% |
|
708 |
\end{isamarkuptext}% |
|
709 |
\isamarkuptrue% |
|
710 |
% |
|
711 |
\begin{isamarkuptext}% |
|
22503 | 712 |
Association lists can be seens as an extension of set-like lists: |
713 |
on the one hand, they may be used to implement finite mappings, |
|
714 |
on the other hand, they remain order-sensitive and allow for |
|
715 |
multiple key-value-pair with the same key: \verb|AList.lookup| |
|
716 |
returns the \emph{first} value corresponding to a particular |
|
717 |
key, if present. \verb|AList.update| updates |
|
718 |
the \emph{first} occurence of a particular key; if no such |
|
719 |
key exists yet, the key-value-pair is added \emph{to the front}. |
|
720 |
\verb|AList.delete| only deletes the \emph{first} occurence of a key. |
|
721 |
\verb|AList.merge| provides an operation suitable for merges of context data |
|
722 |
(\secref{sec:context-theory}), where an equality parameter on |
|
723 |
values determines whether a merge should be considered a conflict. |
|
724 |
A slightly generalized operation if implementend by the \verb|AList.join| |
|
725 |
function which allows for explicit conflict resolution.% |
|
22293 | 726 |
\end{isamarkuptext}% |
727 |
\isamarkuptrue% |
|
728 |
% |
|
729 |
\isamarkupsubsection{Tables% |
|
730 |
} |
|
731 |
\isamarkuptrue% |
|
732 |
% |
|
733 |
\begin{isamarkuptext}% |
|
734 |
\begin{mldecls} |
|
735 |
\indexmltype{'a Symtab.table}\verb|type 'a Symtab.table| \\ |
|
23653 | 736 |
\indexmlexception{Symtab.DUP}\verb|exception Symtab.DUP of string| \\ |
22293 | 737 |
\indexmlexception{Symtab.SAME}\verb|exception Symtab.SAME| \\ |
23653 | 738 |
\indexmlexception{Symtab.UNDEF}\verb|exception Symtab.UNDEF of string| \\ |
22293 | 739 |
\indexml{Symtab.empty}\verb|Symtab.empty: 'a Symtab.table| \\ |
23653 | 740 |
\indexml{Symtab.lookup}\verb|Symtab.lookup: 'a Symtab.table -> string -> 'a option| \\ |
741 |
\indexml{Symtab.defined}\verb|Symtab.defined: 'a Symtab.table -> string -> bool| \\ |
|
742 |
\indexml{Symtab.update}\verb|Symtab.update: (string * 'a) -> 'a Symtab.table -> 'a Symtab.table| \\ |
|
743 |
\indexml{Symtab.default}\verb|Symtab.default: string * 'a -> 'a Symtab.table -> 'a Symtab.table| \\ |
|
744 |
\indexml{Symtab.delete}\verb|Symtab.delete: string|\isasep\isanewline% |
|
22293 | 745 |
\verb| -> 'a Symtab.table -> 'a Symtab.table (*exception Symtab.UNDEF*)| \\ |
26854
9b4aec46ad78
improved treatment of "_" thanks to underscore.sty;
wenzelm
parents:
26460
diff
changeset
|
746 |
\indexml{Symtab.map\_entry}\verb|Symtab.map_entry: string -> ('a -> 'a)|\isasep\isanewline% |
22293 | 747 |
\verb| -> 'a Symtab.table -> 'a Symtab.table| \\ |
26854
9b4aec46ad78
improved treatment of "_" thanks to underscore.sty;
wenzelm
parents:
26460
diff
changeset
|
748 |
\indexml{Symtab.map\_default}\verb|Symtab.map_default: (string * 'a) -> ('a -> 'a)|\isasep\isanewline% |
22293 | 749 |
\verb| -> 'a Symtab.table -> 'a Symtab.table| \\ |
23653 | 750 |
\indexml{Symtab.join}\verb|Symtab.join: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)|\isasep\isanewline% |
22293 | 751 |
\verb| -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline% |
23653 | 752 |
\verb| -> 'a Symtab.table (*exception Symtab.DUP*)| \\ |
22293 | 753 |
\indexml{Symtab.merge}\verb|Symtab.merge: ('a * 'a -> bool)|\isasep\isanewline% |
754 |
\verb| -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline% |
|
23653 | 755 |
\verb| -> 'a Symtab.table (*exception Symtab.DUP*)| |
22293 | 756 |
\end{mldecls}% |
757 |
\end{isamarkuptext}% |
|
758 |
\isamarkuptrue% |
|
759 |
% |
|
760 |
\begin{isamarkuptext}% |
|
22503 | 761 |
Tables are an efficient representation of finite mappings without |
762 |
any notion of order; due to their efficiency they should be used |
|
763 |
whenever such pure finite mappings are neccessary. |
|
764 |
||
765 |
The key type of tables must be given explicitly by instantiating |
|
766 |
the \verb|TableFun| functor which takes the key type |
|
767 |
together with its \verb|order|; for convience, we restrict |
|
768 |
here to the \verb|Symtab| instance with \verb|string| |
|
769 |
as key type. |
|
770 |
||
771 |
Most table functions correspond to those of association lists.% |
|
18543 | 772 |
\end{isamarkuptext}% |
773 |
\isamarkuptrue% |
|
774 |
% |
|
775 |
\isadelimtheory |
|
776 |
% |
|
777 |
\endisadelimtheory |
|
778 |
% |
|
779 |
\isatagtheory |
|
780 |
\isacommand{end}\isamarkupfalse% |
|
18537 | 781 |
% |
782 |
\endisatagtheory |
|
783 |
{\isafoldtheory}% |
|
784 |
% |
|
785 |
\isadelimtheory |
|
786 |
% |
|
787 |
\endisadelimtheory |
|
18543 | 788 |
\isanewline |
18537 | 789 |
\end{isabellebody}% |
790 |
%%% Local Variables: |
|
791 |
%%% mode: latex |
|
792 |
%%% TeX-master: "root" |
|
793 |
%%% End: |