316 ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn) #> snd) |
316 ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn) #> snd) |
317 "} |
317 "} |
318 \end{mldecls} |
318 \end{mldecls} |
319 *} |
319 *} |
320 |
320 |
321 |
|
322 subsection {* Association lists *} |
|
323 |
|
324 text {* |
|
325 \begin{mldecls} |
|
326 @{index_ML_exn AList.DUP} \\ |
|
327 @{index_ML AList.lookup: "('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option"} \\ |
|
328 @{index_ML AList.defined: "('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool"} \\ |
|
329 @{index_ML AList.update: "('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list"} \\ |
|
330 @{index_ML AList.default: "('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list"} \\ |
|
331 @{index_ML AList.delete: "('a * 'b -> bool) -> 'a -> ('b * 'c) list -> ('b * 'c) list"} \\ |
|
332 @{index_ML AList.map_entry: "('a * 'b -> bool) -> 'a |
|
333 -> ('c -> 'c) -> ('b * 'c) list -> ('b * 'c) list"} \\ |
|
334 @{index_ML AList.map_default: "('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b) |
|
335 -> ('a * 'b) list -> ('a * 'b) list"} \\ |
|
336 @{index_ML AList.join: "('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b) (*exception DUP*) |
|
337 -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)"} \\ |
|
338 @{index_ML AList.merge: "('a * 'a -> bool) -> ('b * 'b -> bool) |
|
339 -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)"} |
|
340 \end{mldecls} |
|
341 *} |
|
342 |
|
343 text {* |
|
344 Association lists can be seens as an extension of set-like lists: |
|
345 on the one hand, they may be used to implement finite mappings, |
|
346 on the other hand, they remain order-sensitive and allow for |
|
347 multiple key-value-pair with the same key: @{ML AList.lookup} |
|
348 returns the \emph{first} value corresponding to a particular |
|
349 key, if present. @{ML AList.update} updates |
|
350 the \emph{first} occurence of a particular key; if no such |
|
351 key exists yet, the key-value-pair is added \emph{to the front}. |
|
352 @{ML AList.delete} only deletes the \emph{first} occurence of a key. |
|
353 @{ML AList.merge} provides an operation suitable for merges of context data |
|
354 (\secref{sec:context-theory}), where an equality parameter on |
|
355 values determines whether a merge should be considered a conflict. |
|
356 A slightly generalized operation if implementend by the @{ML AList.join} |
|
357 function which allows for explicit conflict resolution. |
|
358 *} |
|
359 |
|
360 subsection {* Tables *} |
|
361 |
|
362 text {* |
|
363 \begin{mldecls} |
|
364 @{index_ML_type "'a Symtab.table"} \\ |
|
365 @{index_ML_exn Symtab.DUP: string} \\ |
|
366 @{index_ML_exn Symtab.SAME} \\ |
|
367 @{index_ML_exn Symtab.UNDEF: string} \\ |
|
368 @{index_ML Symtab.empty: "'a Symtab.table"} \\ |
|
369 @{index_ML Symtab.lookup: "'a Symtab.table -> string -> 'a option"} \\ |
|
370 @{index_ML Symtab.defined: "'a Symtab.table -> string -> bool"} \\ |
|
371 @{index_ML Symtab.update: "(string * 'a) -> 'a Symtab.table -> 'a Symtab.table"} \\ |
|
372 @{index_ML Symtab.default: "string * 'a -> 'a Symtab.table -> 'a Symtab.table"} \\ |
|
373 @{index_ML Symtab.delete: "string |
|
374 -> 'a Symtab.table -> 'a Symtab.table (*exception Symtab.UNDEF*)"} \\ |
|
375 @{index_ML Symtab.map_entry: "string -> ('a -> 'a) |
|
376 -> 'a Symtab.table -> 'a Symtab.table"} \\ |
|
377 @{index_ML Symtab.map_default: "(string * 'a) -> ('a -> 'a) |
|
378 -> 'a Symtab.table -> 'a Symtab.table"} \\ |
|
379 @{index_ML Symtab.join: "(string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*) |
|
380 -> 'a Symtab.table * 'a Symtab.table |
|
381 -> 'a Symtab.table (*exception Symtab.DUP*)"} \\ |
|
382 @{index_ML Symtab.merge: "('a * 'a -> bool) |
|
383 -> 'a Symtab.table * 'a Symtab.table |
|
384 -> 'a Symtab.table (*exception Symtab.DUP*)"} |
|
385 \end{mldecls} |
|
386 *} |
|
387 |
|
388 text {* |
|
389 Tables are an efficient representation of finite mappings without |
|
390 any notion of order; due to their efficiency they should be used |
|
391 whenever such pure finite mappings are neccessary. |
|
392 |
|
393 The key type of tables must be given explicitly by instantiating |
|
394 the @{ML_functor Table} functor which takes the key type |
|
395 together with its @{ML_type order}; for convience, we restrict |
|
396 here to the @{ML_struct Symtab} instance with @{ML_type string} |
|
397 as key type. |
|
398 |
|
399 Most table functions correspond to those of association lists. |
|
400 *} |
|
401 |
|
402 end |
321 end |