| changeset 479 | 7a84649d8839 |
| parent 478 | dfbd535cd1fd |
| child 481 | 32323727af96 |
| 478:dfbd535cd1fd | 479:7a84649d8839 |
|---|---|
642 |
642 |
643 @{ML_response [display,gray] |
643 @{ML_response [display,gray] |
644 "acc_incs 1 ||>> (fn x => (x, x + 2))" |
644 "acc_incs 1 ||>> (fn x => (x, x + 2))" |
645 "(((((\"\", 1), 2), 3), 4), 6)"} |
645 "(((((\"\", 1), 2), 3), 4), 6)"} |
646 |
646 |
647 An example for this combinator is for example the following code |
647 A more realistic example for this combinator is the following code |
648 *} |
648 *} |
649 |
649 |
650 ML {* |
650 ML{*val (((one_def, two_def), three_def), ctxt') = |
651 val (((one_def, two_def), three_def), ctxt') = |
|
652 @{context} |
651 @{context} |
653 |> Local_Defs.add_def ((@{binding "one"}, NoSyn), @{term "1::nat"}) |
652 |> Local_Defs.add_def ((@{binding "one"}, NoSyn), @{term "1::nat"}) |
654 ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"}) |
653 ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"}) |
655 ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"}) |
654 ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})*} |
656 *} |
655 |
657 |
656 text {* |
658 ML {* |
657 where we make three definitions, namely @{term "one \<equiv> 1::nat"}, @{term "two \<equiv> 2::nat"} |
659 @{context} |
658 and @{term "three \<equiv> 3::nat"}. The point of this code is that we augment the initial |
660 |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"}) |
659 context with the definitions. The result we are interested in is the |
661 ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"}) |
660 augmented context, that is @{ML_text "ctxt'"}, but also the side-results containing |
662 ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"}) |
661 information about the definitions---the function @{ML_ind add_def in Local_Defs} returns |
663 *} |
662 both as pairs. We can use this information for example to print out the definiens and |
664 |
663 the theorem corresponding to the definitions. For example for the first definition: |
665 ML {* |
664 |
666 val ((((One, One_thm), (Two, Two_thm)), (Three, Three_thm)), _)) = |
665 @{ML_response_fake [display, gray] |
667 @{context} |
666 "let |
668 |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"}) |
667 val (one_trm, one_thm) = one_def |
669 ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"}) |
668 in |
670 ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"}) |
669 pwriteln (pretty_term ctxt' one_trm); |
671 *} |
670 pwriteln (pretty_thm ctxt' one_thm) |
672 |
671 end" |
673 |
672 "one |
674 text {* |
673 one \<equiv> 1"} |
674 |
|
675 Recall that @{ML "|>"} is the reverse function application. Recall also that |
675 Recall that @{ML "|>"} is the reverse function application. Recall also that |
676 the related reverse function composition is @{ML "#>"}. In fact all the |
676 the related reverse function composition is @{ML "#>"}. In fact all the |
677 combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"} |
677 combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"} |
678 described above have related combinators for function composition, namely |
678 described above have related combinators for function composition, namely |
679 @{ML_ind "#->" in Basics}, @{ML_ind "#>>" in Basics}, @{ML_ind "##>" in |
679 @{ML_ind "#->" in Basics}, @{ML_ind "#>>" in Basics}, @{ML_ind "##>" in |
737 "Pure/library.ML"} |
737 "Pure/library.ML"} |
738 and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} |
738 and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} |
739 contains further information about combinators. |
739 contains further information about combinators. |
740 \end{readmore} |
740 \end{readmore} |
741 |
741 |
742 \footnote{\bf FIXME: find a good exercise for combinators} |
|
743 \begin{exercise} |
742 \begin{exercise} |
744 Find out what the combinator @{ML "K I"} does. |
743 Find out what the combinator @{ML "K I"} does. |
745 \end{exercise} |
744 \end{exercise} |
746 |
|
747 |
|
748 \footnote{\bf FIXME: say something about calling conventions} |
|
749 *} |
745 *} |
750 |
746 |
751 |
747 |
752 section {* ML-Antiquotations\label{sec:antiquote} *} |
748 section {* ML-Antiquotations\label{sec:antiquote} *} |
753 |
749 |
899 |
895 |
900 text {* |
896 text {* |
901 To use it you also have to install it using \isacommand{setup} like so |
897 To use it you also have to install it using \isacommand{setup} like so |
902 *} |
898 *} |
903 |
899 |
904 setup{* term_pat_setup *} |
900 setup %gray {* term_pat_setup *} |
905 |
901 |
906 text {* |
902 text {* |
907 The parser in Line 2 provides us with a context and a string; this string is |
903 The parser in Line 2 provides us with a context and a string; this string is |
908 transformed into a term using the function @{ML_ind read_term_pattern in |
904 transformed into a term using the function @{ML_ind read_term_pattern in |
909 Proof_Context} (Line 5); the next two lines transform the term into a string |
905 Proof_Context} (Line 5); the next two lines transform the term into a string |
932 |
928 |
933 text {* |
929 text {* |
934 which can be installed with |
930 which can be installed with |
935 *} |
931 *} |
936 |
932 |
937 setup{* type_pat_setup *} |
933 setup %gray {* type_pat_setup *} |
938 |
934 |
939 text {* |
935 text {* |
940 However, a word of warning is in order: Introducing new antiquotations |
936 However, a word of warning is in order: Introducing new antiquotations |
941 should be done only after careful deliberations. They can make your |
937 should be done only after careful deliberations. They can make your |
942 code harder to read, than making it easier. |
938 code harder to read, than making it easier. |
1396 \item Do not use references in Isabelle code. |
1392 \item Do not use references in Isabelle code. |
1397 \end{itemize} |
1393 \end{itemize} |
1398 \end{conventions} |
1394 \end{conventions} |
1399 |
1395 |
1400 *} |
1396 *} |
1401 |
|
1402 |
|
1403 (**************************************************) |
|
1404 (* bak *) |
|
1405 (**************************************************) |
|
1406 |
|
1407 (* |
|
1408 section {* Do Not Try This At Home! *} |
|
1409 |
|
1410 ML {* val my_thms = ref ([]: thm list) *} |
|
1411 |
|
1412 attribute_setup my_thm_bad = |
|
1413 {* Scan.succeed (Thm.declaration_attribute (fn th => fn ctxt => |
|
1414 (my_thms := th :: ! my_thms; ctxt))) *} "bad attribute" |
|
1415 |
|
1416 declare sym [my_thm_bad] |
|
1417 declare refl [my_thm_bad] |
|
1418 |
|
1419 ML "!my_thms" |
|
1420 *) |
|
1421 end |
1397 end |