376 that of the SML basis, which has constructors NONE and SOME instead of |
376 that of the SML basis, which has constructors NONE and SOME instead of |
377 None and Some, as well as exception Option.Option instead of OPTION. |
377 None and Some, as well as exception Option.Option instead of OPTION. |
378 The functions the, if_none, is_some, is_none have been adapted |
378 The functions the, if_none, is_some, is_none have been adapted |
379 accordingly, while Option.map replaces apsome. |
379 accordingly, while Option.map replaces apsome. |
380 |
380 |
381 * The exception LIST has been given up in favour of the standard |
381 * Pure/library.ML: the exception LIST has been given up in favour of |
382 exceptions Empty and Subscript, as well as Library.UnequalLengths. |
382 the standard exceptions Empty and Subscript, as well as |
383 Function like Library.hd and Library.tl are superceded by the standard |
383 Library.UnequalLengths. Function like Library.hd and Library.tl are |
384 hd and tl functions etc. |
384 superceded by the standard hd and tl functions etc. |
385 |
385 |
386 A number of basic functions are now no longer exported to the ML |
386 A number of basic list functions are no longer exported to the ML |
387 toplevel, as they are variants of standard functions. The following |
387 toplevel, as they are variants of predefined functions. The following |
388 suggests how one can translate existing code: |
388 suggests how one can translate existing code: |
389 |
389 |
390 rev_append xs ys = List.revAppend (xs, ys) |
390 rev_append xs ys = List.revAppend (xs, ys) |
391 nth_elem (i, xs) = List.nth (xs, i) |
391 nth_elem (i, xs) = List.nth (xs, i) |
392 last_elem xs = List.last xs |
392 last_elem xs = List.last xs |
393 flat xss = List.concat xss |
393 flat xss = List.concat xss |
394 seq fs = List.app fs |
394 seq fs = List.app fs |
395 partition P xs = List.partition P xs |
395 partition P xs = List.partition P xs |
396 filter P xs = List.filter P xs |
|
397 mapfilter f xs = List.mapPartial f xs |
396 mapfilter f xs = List.mapPartial f xs |
|
397 |
|
398 * Pure/library.ML: several combinators for linear functional |
|
399 transformations, notably reverse application and composition: |
|
400 |
|
401 x |> f f #> g |
|
402 (x, y) |-> f f #-> g |
|
403 |
|
404 * Pure/library.ML: canonical list combinators fold, fold_rev, and |
|
405 fold_yield support linear functional transformations and nesting. For |
|
406 example: |
|
407 |
|
408 fold f [x1, ..., xN] y = |
|
409 y |> f x1 |> ... |> f xN |
|
410 |
|
411 (fold o fold) f [xs1, ..., xsN] y = |
|
412 y |> fold f xs1 |> ... |> fold f xsN |
|
413 |
|
414 fold f [x1, ..., xN] = |
|
415 f x1 #> ... #> f xN |
|
416 |
|
417 (fold o fold) f [xs1, ..., xsN] = |
|
418 fold f xs1 #> ... #> fold f xsN |
|
419 |
|
420 * Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types, |
|
421 fold_types traverse types/terms from left to right, observing |
|
422 canonical argument order. Supercedes previous foldl_XXX versions, |
|
423 add_frees, add_vars have been adapted as well: INCOMPATIBILITY. |
398 |
424 |
399 * Pure: output via the Isabelle channels of writeln/warning/error |
425 * Pure: output via the Isabelle channels of writeln/warning/error |
400 etc. is now passed through Output.output, with a hook for arbitrary |
426 etc. is now passed through Output.output, with a hook for arbitrary |
401 transformations depending on the print_mode (cf. Output.add_mode -- |
427 transformations depending on the print_mode (cf. Output.add_mode -- |
402 the first active mode that provides a output function wins). Already |
428 the first active mode that provides a output function wins). Already |