763 @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or |
763 @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or |
764 matching against @{text "Nil"}, this would make the code rather brittle. |
764 matching against @{text "Nil"}, this would make the code rather brittle. |
765 The reason is that the theory and the name of the data type can easily change. |
765 The reason is that the theory and the name of the data type can easily change. |
766 To make the code more robust, it is better to use the antiquotation |
766 To make the code more robust, it is better to use the antiquotation |
767 @{text "@{const_name \<dots>}"}. With this antiquotation you can harness the |
767 @{text "@{const_name \<dots>}"}. With this antiquotation you can harness the |
768 variable parts of the constant's name. Therefore a functions for |
768 variable parts of the constant's name. Therefore a function for |
769 matching against constants that have a polymorphic type should |
769 matching against constants that have a polymorphic type should |
770 be written as follows. |
770 be written as follows. |
771 *} |
771 *} |
772 |
772 |
773 ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true |
773 ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true |
774 | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true |
774 | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true |
775 | is_nil_or_all _ = false *} |
775 | is_nil_or_all _ = false *} |
776 |
776 |
777 text {* |
777 text {* |
778 Occasional you have to calculate what the ``base'' name of a given |
778 Occasionally you have to calculate what the ``base'' name of a given |
779 constant is. For this you can use the function @{ML Sign.extern_const} or |
779 constant is. For this you can use the function @{ML Sign.extern_const} or |
780 @{ML Long_Name.base_name}. For example: |
780 @{ML Long_Name.base_name}. For example: |
781 |
781 |
782 @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""} |
782 @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""} |
783 |
783 |
814 @{typ nat} => @{typ int} |
814 @{typ nat} => @{typ int} |
815 | Type (s, ts) => Type (s, map nat_to_int ts) |
815 | Type (s, ts) => Type (s, map nat_to_int ts) |
816 | _ => t)*} |
816 | _ => t)*} |
817 |
817 |
818 text {* |
818 text {* |
819 An example as follows: |
819 Here is an example: |
820 |
820 |
821 @{ML_response_fake [display,gray] |
821 @{ML_response_fake [display,gray] |
822 "map_types nat_to_int @{term \"a = (1::nat)\"}" |
822 "map_types nat_to_int @{term \"a = (1::nat)\"}" |
823 "Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\") |
823 "Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\") |
824 $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"} |
824 $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"} |
883 \begin{exercise} |
883 \begin{exercise} |
884 Check that the function defined in Exercise~\ref{fun:revsum} returns a |
884 Check that the function defined in Exercise~\ref{fun:revsum} returns a |
885 result that type-checks. |
885 result that type-checks. |
886 \end{exercise} |
886 \end{exercise} |
887 |
887 |
888 Remember Isabelle follows the Church-style typing for terms, i.e.~a term contains |
888 Remember Isabelle follows the Church-style typing for terms, i.e., a term contains |
889 enough typing information (constants, free variables and abstractions all have typing |
889 enough typing information (constants, free variables and abstractions all have typing |
890 information) so that it is always clear what the type of a term is. |
890 information) so that it is always clear what the type of a term is. |
891 Given a well-typed term, the function @{ML type_of} returns the |
891 Given a well-typed term, the function @{ML type_of} returns the |
892 type of a term. Consider for example: |
892 type of a term. Consider for example: |
893 |
893 |
933 end" |
933 end" |
934 "Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $ |
934 "Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $ |
935 Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"} |
935 Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"} |
936 |
936 |
937 Instead of giving explicitly the type for the constant @{text "plus"} and the free |
937 Instead of giving explicitly the type for the constant @{text "plus"} and the free |
938 variable @{text "x"}, the type-inference fills in the missing information. |
938 variable @{text "x"}, type-inference fills in the missing information. |
939 |
939 |
940 \begin{readmore} |
940 \begin{readmore} |
941 See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading, |
941 See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading, |
942 checking and pretty-printing of terms are defined. Functions related to the |
942 checking and pretty-printing of terms are defined. Functions related to |
943 type inference are implemented in @{ML_file "Pure/type.ML"} and |
943 type-inference are implemented in @{ML_file "Pure/type.ML"} and |
944 @{ML_file "Pure/type_infer.ML"}. |
944 @{ML_file "Pure/type_infer.ML"}. |
945 \end{readmore} |
945 \end{readmore} |
946 |
946 |
947 (FIXME: say something about sorts) |
947 (FIXME: say something about sorts) |
948 *} |
948 *} |