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