4 begin |
4 begin |
5 |
5 |
6 chapter {* First Steps *} |
6 chapter {* First Steps *} |
7 |
7 |
8 text {* |
8 text {* |
|
9 \begin{flushright} |
|
10 {\em |
|
11 ``We will most likely never realize the full importance of painting the Tower,\\ |
|
12 that it is the essential element in the conservation of metal works and the\\ |
|
13 more meticulous the paint job, the longer the Tower shall endure.''} \\[1ex] |
|
14 Gustave Eiffel, In The 300-Meter Tower.\footnote{The Eiffel Tower has been |
|
15 re-painted 18 times since its initial construction, an average of once every |
|
16 seven years. It takes more than a year for a team of 25 painters to paint the Tower |
|
17 from top to bottom.}\\[1ex] |
|
18 \end{flushright} |
|
19 |
9 Isabelle programming is done in ML. Just like lemmas and proofs, ML-code for |
20 Isabelle programming is done in ML. Just like lemmas and proofs, ML-code for |
10 Isabelle must be part of a theory. If you want to follow the code given in |
21 Isabelle must be part of a theory. If you want to follow the code given in |
11 this chapter, we assume you are working inside the theory starting with |
22 this chapter, we assume you are working inside the theory starting with |
12 |
23 |
13 \begin{quote} |
24 \begin{quote} |
670 |
681 |
671 (FIXME: say something about calling conventions) |
682 (FIXME: say something about calling conventions) |
672 *} |
683 *} |
673 |
684 |
674 |
685 |
675 section {* Antiquotations *} |
686 section {* ML-Antiquotations *} |
676 |
687 |
677 text {* |
688 text {* |
678 The main advantage of embedding all code in a theory is that the code can |
689 The main advantage of embedding all code in a theory is that the code can |
679 contain references to entities defined on the logical level of Isabelle. By |
690 contain references to entities defined on the logical level of Isabelle. By |
680 this we mean definitions, theorems, terms and so on. This kind of reference is |
691 this we mean definitions, theorems, terms and so on. This kind of reference |
681 realised with antiquotations, sometimes also referred to as ML-antiquotations. |
692 is realised with ML-antiquotations, often also referred to as just |
|
693 antiquotations.\footnote{There are two kinds of antiquotations in Isabelle, |
|
694 which have very different purpose and infrastructures. The first kind, |
|
695 described in this section, are \emph{ML-antiquotations}. They are used to |
|
696 refer to entities (like terms, types etc) from Isabelle's logic layer inside |
|
697 ML-code. The other kind of antiquotations are \emph{document} antiquotations. They |
|
698 are used only in the text parts of Isabelle and their purpose is to print |
|
699 logical entities inside \LaTeX-documents. They are part of the user level |
|
700 and therefore we are not interested in them in this Tutorial, except in |
|
701 Appendix \ref{rec:docantiquotations} where we show how to implement your own |
|
702 document antiquotations.} |
682 For example, one can print out the name of the current |
703 For example, one can print out the name of the current |
683 theory by typing |
704 theory by typing |
684 |
705 |
685 |
706 |
686 @{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""} |
707 @{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""} |
780 give a pointer to \isacommand{local\_setup}; if not, then explain |
801 give a pointer to \isacommand{local\_setup}; if not, then explain |
781 why @{ML snd} is needed) |
802 why @{ML snd} is needed) |
782 |
803 |
783 It is also possible to define your own antiquotations. But you should |
804 It is also possible to define your own antiquotations. But you should |
784 exercise care when introducing new ones, as they can also make your code |
805 exercise care when introducing new ones, as they can also make your code |
785 also difficult to read. In the next section we will see how the (build in) |
806 also difficult to read. In the next chapter we will see how the (build in) |
786 antiquotation @{text "@{term \<dots>}"} can be used to construct terms. A |
807 antiquotation @{text "@{term \<dots>}"} can be used to construct terms. A |
787 restriction of this antiquotation is that it does not allow you to use |
808 restriction of this antiquotation is that it does not allow you to use |
788 schematic variables. If you want to have an antiquotation that does not have |
809 schematic variables. If you want to have an antiquotation that does not have |
789 this restriction, you can implement your own using the function @{ML_ind |
810 this restriction, you can implement your own using the function @{ML_ind |
790 ML_Antiquote.inline}. The code is as follows. |
811 ML_Antiquote.inline}. The code for the antiquotation @{text "term_pat"} is |
|
812 as follows. |
791 *} |
813 *} |
792 |
814 |
793 ML %linenosgray{*ML_Antiquote.inline "term_pat" |
815 ML %linenosgray{*ML_Antiquote.inline "term_pat" |
794 (Args.context -- Scan.lift Args.name_source >> |
816 (Args.context -- Scan.lift Args.name_source >> |
795 (fn (ctxt, s) => |
817 (fn (ctxt, s) => |
799 |
821 |
800 text {* |
822 text {* |
801 The parser in Line 2 provides us with a context and a string; this string is |
823 The parser in Line 2 provides us with a context and a string; this string is |
802 transformed into a term using the function @{ML_ind read_term_pattern in |
824 transformed into a term using the function @{ML_ind read_term_pattern in |
803 ProofContext} (Line 4); the next two lines print the term so that the |
825 ProofContext} (Line 4); the next two lines print the term so that the |
804 ML-system can understand them. An example of this antiquotation is as |
826 ML-system can understand them. The function @{ML atomic in ML_Syntax} |
805 follows. |
827 just encloses the term in parentheses. An example for the usage of this |
|
828 antiquotation is: |
806 |
829 |
807 @{ML_response_fake [display,gray] |
830 @{ML_response_fake [display,gray] |
808 "@{term_pat \"Suc (?x::nat)\"}" |
831 "@{term_pat \"Suc (?x::nat)\"}" |
809 "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"} |
832 "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"} |
810 |
833 |
811 which is the internal representation of the term @{text "Suc ?x"}. |
834 which shows the internal representation of the term @{text "Suc ?x"}. |
812 |
835 |
813 \begin{readmore} |
836 \begin{readmore} |
814 The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions |
837 The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions |
815 for most antiquotations. |
838 for most antiquotations. Most of the basic operations on ML-syntax are implemented |
|
839 in @{ML_file "Pure/ML/ml_syntax.ML"}. |
816 \end{readmore} |
840 \end{readmore} |
817 |
841 *} |
818 Note one source of possible confusion about antiquotations. There are two kinds |
842 |
819 of them in Isabelle, which have very different purpose and infrastructures. The |
843 section {* Storing Data (TBD) *} |
820 first kind, described in this section, are \emph{ML-antiquotations}. They are |
844 |
821 used to refer to entities (like terms, types etc) from Isabelle's logic layer |
845 text {* |
822 inside ML-code. They are ``linked'' statically at compile-time, which limits |
846 Isabelle provides a mechanism to store (and retrieve) arbitrary data. Before we |
823 sometimes their usefulness in cases where, for example, terms needs to be |
847 explain this mechanism. |
824 built up dynamically. |
848 *} |
825 |
849 |
826 The other kind of antiquotations are \emph{document} antiquotations. |
850 ML{*signature UNIVERSAL_TYPE = |
827 They are used only in the text parts of Isabelle and their purpose is to print |
851 sig |
828 logical entities inside \LaTeX-documents. They are part of the user level and |
852 type t |
829 therefore we are not interested in them in this Tutorial, except in |
853 |
830 Appendix \ref{rec:docantiquotations} where we show how to implement your |
854 val embed: unit -> ('a -> t) * (t -> 'a option) |
831 own document antiquotations. |
855 end*} |
832 *} |
856 |
|
857 ML{*structure U:> UNIVERSAL_TYPE = |
|
858 struct |
|
859 type t = exn |
|
860 |
|
861 fun 'a embed () = |
|
862 let |
|
863 exception E of 'a |
|
864 fun project (e: t): 'a option = |
|
865 case e of |
|
866 E a => SOME a |
|
867 | _ => NONE |
|
868 in |
|
869 (E, project) |
|
870 end |
|
871 end*} |
|
872 |
|
873 text {* |
|
874 The idea is that type t is the universal type and that each call to embed |
|
875 returns a new pair of functions (inject, project), where inject embeds a |
|
876 value into the universal type and project extracts the value from the |
|
877 universal type. A pair (inject, project) returned by embed works together in |
|
878 that project u will return SOME v if and only if u was created by inject |
|
879 v. If u was created by a different function inject', then project returns |
|
880 NONE. |
|
881 |
|
882 in library.ML |
|
883 *} |
|
884 |
|
885 ML_val{*structure Object = struct type T = exn end; *} |
|
886 |
|
887 ML{*functor Test (U: UNIVERSAL_TYPE): sig end = |
|
888 struct |
|
889 val (intIn: int -> U.t, intOut) = U.embed () |
|
890 val r: U.t ref = ref (intIn 13) |
|
891 val s1 = |
|
892 case intOut (!r) of |
|
893 NONE => "NONE" |
|
894 | SOME i => Int.toString i |
|
895 val (realIn: real -> U.t, realOut) = U.embed () |
|
896 val _ = r := realIn 13.0 |
|
897 val s2 = |
|
898 case intOut (!r) of |
|
899 NONE => "NONE" |
|
900 | SOME i => Int.toString i |
|
901 val s3 = |
|
902 case realOut (!r) of |
|
903 NONE => "NONE" |
|
904 | SOME x => Real.toString x |
|
905 val _ = tracing (implode [s1, " ", s2, " ", s3, "\n"]) |
|
906 end*} |
|
907 |
|
908 ML_val{*structure t = Test(U) *} |
|
909 |
|
910 ML_val{*structure Datatab = Table(type key = int val ord = int_ord);*} |
|
911 |
|
912 ML {* LocalTheory.restore *} |
|
913 ML {* LocalTheory.set_group *} |
|
914 |
|
915 |
833 |
916 |
834 (* |
917 (* |
835 section {* Do Not Try This At Home! *} |
918 section {* Do Not Try This At Home! *} |
836 |
919 |
837 ML {* val my_thms = ref ([]: thm list) *} |
920 ML {* val my_thms = ref ([]: thm list) *} |