117 |
117 |
118 @{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")" |
118 @{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")" |
119 "Exception- ERROR \"foo\" raised |
119 "Exception- ERROR \"foo\" raised |
120 At command \"ML\"."} |
120 At command \"ML\"."} |
121 |
121 |
|
122 (FIXME @{ML Toplevel.debug} @{ML Toplevel.profiling}) |
|
123 *} |
|
124 |
|
125 (* |
|
126 ML {* |
|
127 fun dodgy_fun () = (raise (ERROR "bar"); 1) |
|
128 *} |
|
129 |
|
130 ML {* set Toplevel.debug *} |
|
131 |
|
132 ML {* fun f1 () = dodgy_fun () *} |
|
133 |
|
134 ML {* f1 () *} |
|
135 *) |
|
136 |
|
137 text {* |
122 Most often you want to inspect data of type @{ML_type term}, @{ML_type cterm} |
138 Most often you want to inspect data of type @{ML_type term}, @{ML_type cterm} |
123 or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them, |
139 or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them, |
124 but for quick-and-dirty solutions they are far too unwieldy. A simple way to transform |
140 but for quick-and-dirty solutions they are far too unwieldy. A simple way to transform |
125 a term into a string is to use the function @{ML Syntax.string_of_term}. |
141 a term into a string is to use the function @{ML Syntax.string_of_term}. |
126 |
142 |
194 ML{*fun str_of_thms ctxt thms = |
210 ML{*fun str_of_thms ctxt thms = |
195 commas (map (str_of_thm ctxt) thms) |
211 commas (map (str_of_thm ctxt) thms) |
196 |
212 |
197 fun str_of_thms_raw ctxt thms = |
213 fun str_of_thms_raw ctxt thms = |
198 commas (map (str_of_thm_raw ctxt) thms)*} |
214 commas (map (str_of_thm_raw ctxt) thms)*} |
199 |
|
200 text {* |
|
201 (FIXME @{ML Toplevel.debug} @{ML Toplevel.profiling} @{ML Toplevel.debug}) |
|
202 *} |
|
203 |
215 |
204 section {* Combinators\label{sec:combinators} *} |
216 section {* Combinators\label{sec:combinators} *} |
205 |
217 |
206 text {* |
218 text {* |
207 For beginners perhaps the most puzzling parts in the existing code of Isabelle are |
219 For beginners perhaps the most puzzling parts in the existing code of Isabelle are |
475 "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"} |
487 "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"} |
476 |
488 |
477 Again, this way or referencing simpsets makes you independent from additions |
489 Again, this way or referencing simpsets makes you independent from additions |
478 of lemmas to the simpset by the user that potentially cause loops. |
490 of lemmas to the simpset by the user that potentially cause loops. |
479 |
491 |
|
492 On the ML-level of Isabelle, you often have to work with qualified names; |
|
493 these are strings with some additional information, such positional information |
|
494 and qualifiers. Such bindings can be generated with the antiquotation |
|
495 @{text "@{bindin \<dots>}"}. |
|
496 |
|
497 @{ML_response [display,gray] |
|
498 "@{binding \"name\"}" |
|
499 "name"} |
|
500 |
|
501 An example where a binding is needed is the function @{ML define in LocalTheory}. |
|
502 Below this function defines the constant @{term "TrueConj"} as the conjunction |
|
503 @{term "True \<and> True"}. |
|
504 *} |
|
505 |
|
506 local_setup %gray {* |
|
507 snd o LocalTheory.define Thm.internalK |
|
508 ((@{binding "TrueConj"}, NoSyn), |
|
509 (Attrib.empty_binding, @{term "True \<and> True"})) *} |
|
510 |
|
511 text {* |
480 While antiquotations have many applications, they were originally introduced in order |
512 While antiquotations have many applications, they were originally introduced in order |
481 to avoid explicit bindings for theorems such as: |
513 to avoid explicit bindings for theorems such as: |
482 *} |
514 *} |
483 |
515 |
484 ML{*val allI = thm "allI" *} |
516 ML{*val allI = thm "allI" *} |
490 statically at compile-time. However, this static linkage also limits their |
522 statically at compile-time. However, this static linkage also limits their |
491 usefulness in cases where data needs to be build up dynamically. In the |
523 usefulness in cases where data needs to be build up dynamically. In the |
492 course of this chapter you will learn more about these antiquotations: |
524 course of this chapter you will learn more about these antiquotations: |
493 they can simplify Isabelle programming since one can directly access all |
525 they can simplify Isabelle programming since one can directly access all |
494 kinds of logical elements from th ML-level. |
526 kinds of logical elements from th ML-level. |
495 *} |
|
496 |
|
497 text {* |
|
498 (FIXME: say something about @{text "@{binding \<dots>}"} |
|
499 *} |
527 *} |
500 |
528 |
501 section {* Terms and Types *} |
529 section {* Terms and Types *} |
502 |
530 |
503 text {* |
531 text {* |
614 |
642 |
615 @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T}" |
643 @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T}" |
616 "Const \<dots> $ |
644 "Const \<dots> $ |
617 Abs (\"x\", \<dots>, |
645 Abs (\"x\", \<dots>, |
618 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ |
646 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ |
619 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"} |
647 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"} |
620 |
648 |
621 (FIXME: handy functions for constructing terms: @{ML list_comb}, @{ML lambda}, |
649 There are a number of handy functions that are frequently used for |
|
650 constructing terms. One is the function @{ML list_comb} which a term |
|
651 and a list of terms as argument, and produces as output the term |
|
652 list applied to the term. For example |
|
653 |
|
654 @{ML_response_fake [display,gray] |
|
655 "list_comb (@{term \"P::nat\"}, [@{term \"True\"}, @{term \"False\"}])" |
|
656 "Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"} |
|
657 |
|
658 (FIXME: handy functions for constructing terms: @{ML lambda}, |
622 @{ML subst_free}) |
659 @{ML subst_free}) |
623 *} |
660 *} |
624 |
661 |
625 |
662 ML {* lambda @{term "x::nat"} @{term "P x"}*} |
626 text {* |
663 |
|
664 |
|
665 text {* |
|
666 As can be seen this function does not take the typing annotation into account. |
|
667 |
627 \begin{readmore} |
668 \begin{readmore} |
628 There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and |
669 There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and |
629 @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms |
670 @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms |
630 and types easier.\end{readmore} |
671 and types easier.\end{readmore} |
631 |
672 |