145 |
145 |
146 You can print out error messages with the function @{ML_ind error in Library}; |
146 You can print out error messages with the function @{ML_ind error in Library}; |
147 for example: |
147 for example: |
148 |
148 |
149 @{ML_response_fake [display,gray] |
149 @{ML_response_fake [display,gray] |
150 "if 0=1 then true else (error \"foo\")" |
150 "if 0 = 1 then true else (error \"foo\")" |
151 "Exception- ERROR \"foo\" raised |
151 "Exception- ERROR \"foo\" raised |
152 At command \"ML\"."} |
152 At command \"ML\"."} |
153 |
153 |
154 This function raises the exception @{text ERROR}, which will then |
154 This function raises the exception @{text ERROR}, which will then |
155 be displayed by the infrastructure. Note that this exception is meant |
155 be displayed by the infrastructure. Note that this exception is meant |
643 |
643 |
644 @{ML_response [display,gray] |
644 @{ML_response [display,gray] |
645 "acc_incs 1 ||>> (fn x => (x, x + 2))" |
645 "acc_incs 1 ||>> (fn x => (x, x + 2))" |
646 "(((((\"\", 1), 2), 3), 4), 6)"} |
646 "(((((\"\", 1), 2), 3), 4), 6)"} |
647 |
647 |
|
648 An example where this combinator is useful is as follows |
|
649 |
|
650 @{ML_response_fake [display, gray] |
|
651 "let |
|
652 val ((names1, names2), _) = |
|
653 @{context} |
|
654 |> Variable.variant_fixes (replicate 4 \"x\") |
|
655 ||>> Variable.variant_fixes (replicate 5 \"x\") |
|
656 in |
|
657 (names1, names2) |
|
658 end" |
|
659 "([\"x\", \"xa\", \"xb\", \"xc\"], [\"xd\", \"xe\", \"xf\", \"xg\", \"xh\"])"} |
|
660 |
|
661 Its purpose is to create nine variants of the string @{ML "\"x\""} so |
|
662 that no variant will clash with another. Suppose for some reason we want |
|
663 to bind four variants to the lists @{ML_text "name1"} and the |
|
664 rest to @{ML_text "name2"}. In order to obtain non-clashing |
|
665 variants we have to thread the context through the function calls |
|
666 (the context records which variants have been previously created). |
|
667 For the first call we can use @{ML "|>"}, but in the |
|
668 second and any further call to @{ML_ind variant_fixes in Variable} we |
|
669 have to use @{ML "||>>"} in order to account for the result(s) |
|
670 obtained by previous calls. |
|
671 |
648 A more realistic example for this combinator is the following code |
672 A more realistic example for this combinator is the following code |
649 *} |
673 *} |
650 |
674 |
651 ML{*val (((one_def, two_def), three_def), ctxt') = |
675 ML{*val (((one_def, two_def), three_def), ctxt') = |
652 @{context} |
676 @{context} |
670 pwriteln (pretty_term ctxt' one_trm); |
694 pwriteln (pretty_term ctxt' one_trm); |
671 pwriteln (pretty_thm ctxt' one_thm) |
695 pwriteln (pretty_thm ctxt' one_thm) |
672 end" |
696 end" |
673 "one |
697 "one |
674 one \<equiv> 1"} |
698 one \<equiv> 1"} |
675 |
|
676 Recall that @{ML "|>"} is the reverse function application. Recall also that |
699 Recall that @{ML "|>"} is the reverse function application. Recall also that |
677 the related reverse function composition is @{ML "#>"}. In fact all the |
700 the related reverse function composition is @{ML "#>"}. In fact all the |
678 combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"} |
701 combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"} |
679 described above have related combinators for function composition, namely |
702 described above have related combinators for function composition, namely |
680 @{ML_ind "#->" in Basics}, @{ML_ind "#>>" in Basics}, @{ML_ind "##>" in |
703 @{ML_ind "#->" in Basics}, @{ML_ind "#>>" in Basics}, @{ML_ind "##>" in |