369 Many problems in functional programming can be thought of |
367 Many problems in functional programming can be thought of |
370 as linear transformations, i.e.~a caluclation starts with a |
368 as linear transformations, i.e.~a caluclation starts with a |
371 particular value \isa{x\ {\isasymColon}\ foo} which is then transformed |
369 particular value \isa{x\ {\isasymColon}\ foo} which is then transformed |
372 by application of a function \isa{f\ {\isasymColon}\ foo\ {\isasymRightarrow}\ foo}, |
370 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}, |
371 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 |
372 and so on. As a canoncial example, take functions enriching |
375 theories by constants and definitions: |
373 a theory by constant declararion and primitive definitions: |
376 \verb|Sign.add_consts_i: (string * typ * mixfix) list -> theory|\isasep\isanewline% |
374 |
377 \verb|-> theory| |
375 \begin{quotation} |
378 and \verb|Theory.add_defs_i: bool -> bool|\isasep\isanewline% |
376 \verb|Sign.declare_const: Markup.property list -> bstring * typ * mixfix|\isasep\isanewline% |
379 \verb|-> (bstring * term) list -> theory -> theory|. |
377 \verb| -> theory -> term * theory| |
380 Written with naive application, an addition of a constant with |
378 |
381 a corresponding definition would look like: |
379 \verb|Thm.add_def: bool -> bstring * term -> theory -> thm * theory| |
382 \verb|Theory.add_defs_i false false [dummy_def]|\isasep\isanewline% |
380 \end{quotation} |
383 \verb| (Sign.add_consts_i [dummy_const] thy)|. |
381 |
384 With increasing numbers of applications, this code gets quite unreadable. |
382 Written with naive application, an addition of constant |
385 Using composition, at least the nesting of brackets may be reduced: |
383 \isa{bar} with type \isa{foo\ {\isasymRightarrow}\ foo} and |
386 \verb|(Theory.add_defs_i false false [dummy_def] o Sign.add_consts_i|\isasep\isanewline% |
384 a corresponding definition \isa{bar\ {\isasymequiv}\ {\isasymlambda}x{\isachardot}\ x} would look like: |
387 \verb| [dummy_const]) thy|. |
385 |
388 What remains unsatisfactory is that things are written down in the opposite order |
386 \begin{quotation} |
389 as they actually ``happen''.% |
387 \verb|(fn (t, thy) => Thm.add_def false|\isasep\isanewline% |
|
388 \verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline% |
|
389 \verb| (Sign.declare_const []|\isasep\isanewline% |
|
390 \verb| ("bar", @{typ "foo => foo"}, NoSyn) thy)|. |
|
391 \end{quotation} |
|
392 |
|
393 With increasing numbers of applications, this code gets quite |
|
394 unreadable. Further, it is unintuitive that things are |
|
395 written down in the opposite order as they actually ``happen''.% |
390 \end{isamarkuptext}% |
396 \end{isamarkuptext}% |
391 \isamarkuptrue% |
397 \isamarkuptrue% |
392 % |
398 % |
393 \isadelimML |
399 \isadelimML |
394 % |
400 % |
402 \isadelimML |
408 \isadelimML |
403 % |
409 % |
404 \endisadelimML |
410 \endisadelimML |
405 % |
411 % |
406 \begin{isamarkuptext}% |
412 \begin{isamarkuptext}% |
407 At this stage, Isabelle offers some combinators which allow for more convenient |
413 \noindent At this stage, Isabelle offers some combinators which allow |
408 notation, most notably reverse application: |
414 for more convenient notation, most notably reverse application: |
409 \isasep\isanewline% |
415 \begin{quotation} |
410 \verb|thy|\isasep\isanewline% |
416 \verb|thy|\isasep\isanewline% |
411 \verb||\verb,|,\verb|> Sign.add_consts_i [dummy_const]|\isasep\isanewline% |
417 \verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline% |
412 \verb||\verb,|,\verb|> Theory.add_defs_i false false [dummy_def]|% |
418 \verb||\verb,|,\verb|> (fn (t, thy) => thy|\isasep\isanewline% |
413 \end{isamarkuptext}% |
419 \verb||\verb,|,\verb|> Thm.add_def false|\isasep\isanewline% |
414 \isamarkuptrue% |
420 \verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))| |
415 % |
421 \end{quotation}% |
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}% |
422 \end{isamarkuptext}% |
421 \isamarkuptrue% |
423 \isamarkuptrue% |
422 % |
424 % |
423 \isadelimmlref |
425 \isadelimmlref |
424 % |
426 % |
430 \begin{mldecls} |
432 \begin{mldecls} |
431 \indexml{op |-$>$ }\verb|op |\verb,|,\verb|-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\ |
433 \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| \\ |
434 \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| \\ |
435 \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| \\ |
436 \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{mldecls}% |
437 \end{isamarkuptext}% |
438 \end{isamarkuptext}% |
438 \isamarkuptrue% |
439 \isamarkuptrue% |
439 % |
440 % |
440 \endisatagmlref |
441 \endisatagmlref |
443 \isadelimmlref |
444 \isadelimmlref |
444 % |
445 % |
445 \endisadelimmlref |
446 \endisadelimmlref |
446 % |
447 % |
447 \begin{isamarkuptext}% |
448 \begin{isamarkuptext}% |
448 \noindent FIXME transformations involving side results% |
449 \noindent Usually, functions involving theory updates also return |
|
450 side results; to use these conveniently, yet another |
|
451 set of combinators is at hand, most notably \verb|op |\verb,|,\verb|->| |
|
452 which allows curried access to side results: |
|
453 \begin{quotation} |
|
454 \verb|thy|\isasep\isanewline% |
|
455 \verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline% |
|
456 \verb||\verb,|,\verb|-> (fn t => Thm.add_def false|\isasep\isanewline% |
|
457 \verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline% |
|
458 |
|
459 \end{quotation} |
|
460 |
|
461 \noindent \verb|op |\verb,|,\verb|>>| allows for processing side results on their own: |
|
462 \begin{quotation} |
|
463 \verb|thy|\isasep\isanewline% |
|
464 \verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline% |
|
465 \verb||\verb,|,\verb|>> (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline% |
|
466 \verb||\verb,|,\verb|-> (fn def => Thm.add_def false ("bar_def", def))|\isasep\isanewline% |
|
467 |
|
468 \end{quotation} |
|
469 |
|
470 \noindent Orthogonally, \verb|op |\verb,|,\verb||\verb,|,\verb|>| applies a transformation |
|
471 in the presence of side results which are left unchanged: |
|
472 \begin{quotation} |
|
473 \verb|thy|\isasep\isanewline% |
|
474 \verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline% |
|
475 \verb||\verb,|,\verb||\verb,|,\verb|> Sign.add_path "foobar"|\isasep\isanewline% |
|
476 \verb||\verb,|,\verb|-> (fn t => Thm.add_def false|\isasep\isanewline% |
|
477 \verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline% |
|
478 \verb||\verb,|,\verb||\verb,|,\verb|> Sign.restore_naming thy|\isasep\isanewline% |
|
479 |
|
480 \end{quotation} |
|
481 |
|
482 \noindent \indexml{op ||$>$$>$}\verb|op |\verb,|,\verb||\verb,|,\verb|>>| accumulates side results: |
|
483 \begin{quotation} |
|
484 \verb|thy|\isasep\isanewline% |
|
485 \verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline% |
|
486 \verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const [] ("foobar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline% |
|
487 \verb||\verb,|,\verb|-> (fn (t1, t2) => Thm.add_def false|\isasep\isanewline% |
|
488 \verb| ("bar_def", Logic.mk_equals (t1, t2)))|\isasep\isanewline% |
|
489 |
|
490 \end{quotation}% |
|
491 \end{isamarkuptext}% |
|
492 \isamarkuptrue% |
|
493 % |
|
494 \isadelimmlref |
|
495 % |
|
496 \endisadelimmlref |
|
497 % |
|
498 \isatagmlref |
|
499 % |
|
500 \begin{isamarkuptext}% |
|
501 \begin{mldecls} |
|
502 \indexml{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\ |
|
503 \indexml{fold-map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\ |
|
504 \end{mldecls}% |
|
505 \end{isamarkuptext}% |
|
506 \isamarkuptrue% |
|
507 % |
|
508 \endisatagmlref |
|
509 {\isafoldmlref}% |
|
510 % |
|
511 \isadelimmlref |
|
512 % |
|
513 \endisadelimmlref |
|
514 % |
|
515 \begin{isamarkuptext}% |
|
516 \noindent This principles naturally lift to \isa{lists} using |
|
517 the \verb|fold| and \verb|fold_map| combinators. |
|
518 The first lifts a single function |
|
519 \isa{f\ {\isasymColon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b} to \isa{{\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b} |
|
520 such that |
|
521 \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}; |
|
522 the second accumulates side results in a list by lifting |
|
523 a single function |
|
524 \isa{f\ {\isasymColon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}c\ {\isasymtimes}\ {\isacharprime}b} to \isa{{\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}c\ list\ {\isasymtimes}\ {\isacharprime}b} |
|
525 such that |
|
526 \isa{y\ {\isacharbar}{\isachargreater}\ fold{\isacharunderscore}map\ 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}{\isacharbar}{\isachargreater}{\isachargreater}\ f\ x\isactrlisub {\isadigit{2}}\ {\isacharbar}{\isacharbar}{\isachargreater}{\isachargreater}\ {\isasymdots}\ {\isacharbar}{\isacharbar}{\isachargreater}{\isachargreater}\ f\ x\isactrlisub n\ {\isacharbar}{\isacharbar}{\isachargreater}\ {\isacharparenleft}fn\ {\isacharparenleft}{\isacharparenleft}z\isactrlisub {\isadigit{1}}{\isacharcomma}\ z\isactrlisub {\isadigit{2}}{\isacharparenright}{\isacharcomma}\ {\isasymdots}\ z\isactrlisub n{\isacharparenright}\ {\isacharequal}{\isachargreater}\ {\isacharbrackleft}z\isactrlisub {\isadigit{1}}{\isacharcomma}\ z\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ z\isactrlisub n{\isacharbrackright}{\isacharparenright}}; |
|
527 |
|
528 Example: FIXME |
|
529 \begin{quotation} |
|
530 \end{quotation}% |
449 \end{isamarkuptext}% |
531 \end{isamarkuptext}% |
450 \isamarkuptrue% |
532 \isamarkuptrue% |
451 % |
533 % |
452 \isadelimmlref |
534 \isadelimmlref |
453 % |
535 % |
566 \end{isamarkuptext}% |
648 \end{isamarkuptext}% |
567 \isamarkuptrue% |
649 \isamarkuptrue% |
568 % |
650 % |
569 \begin{isamarkuptext}% |
651 \begin{isamarkuptext}% |
570 Lists are often used as set-like data structures -- set-like in |
652 Lists are often used as set-like data structures -- set-like in |
571 then sense that they support notion of \verb|member|-ship, |
653 the sense that they support a notion of \verb|member|-ship, |
572 \verb|insert|-ing and \verb|remove|-ing, but are order-sensitive. |
654 \verb|insert|-ing and \verb|remove|-ing, but are order-sensitive. |
573 This is convenient when implementing a history-like mechanism: |
655 This is convenient when implementing a history-like mechanism: |
574 \verb|insert| adds an element \emph{to the front} of a list, |
656 \verb|insert| adds an element \emph{to the front} of a list, |
575 if not yet present; \verb|remove| removes \emph{all} occurences |
657 if not yet present; \verb|remove| removes \emph{all} occurences |
576 of a particular element. Correspondingly \verb|merge| implements a |
658 of a particular element. Correspondingly \verb|merge| implements a |