553 To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} |
553 To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} |
554 to both functions. With @{ML make_imp} we obtain the intended term involving |
554 to both functions. With @{ML make_imp} we obtain the intended term involving |
555 the given arguments |
555 the given arguments |
556 |
556 |
557 @{ML_response [display,gray] "make_imp @{term S} @{term T} @{typ nat}" |
557 @{ML_response [display,gray] "make_imp @{term S} @{term T} @{typ nat}" |
558 "Const \<dots> $ |
558 "Const \<dots> $ |
559 Abs (\"x\", Type (\"nat\",[]), |
559 Abs (\"x\", Type (\"nat\",[]), |
560 Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ |
560 Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ (Free (\"T\",\<dots>) $ \<dots>))"} |
561 (Free (\"T\",\<dots>) $ \<dots>))"} |
|
562 |
561 |
563 whereas with @{ML make_wrong_imp} we obtain a term involving the @{term "P"} |
562 whereas with @{ML make_wrong_imp} we obtain a term involving the @{term "P"} |
564 and @{text "Q"} from the antiquotation. |
563 and @{text "Q"} from the antiquotation. |
565 |
564 |
566 @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T} @{typ nat}" |
565 @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T} @{typ nat}" |
567 "Const \<dots> $ |
566 "Const \<dots> $ |
568 Abs (\"x\", \<dots>, |
567 Abs (\"x\", \<dots>, |
569 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ |
568 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ |
570 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"} |
569 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"} |
571 |
570 |
572 Although types of terms can often be inferred, there are many |
571 Although types of terms can often be inferred, there are many |
573 situations where you need to construct types manually, especially |
572 situations where you need to construct types manually, especially |
574 when defining constants. For example the function returning a function |
573 when defining constants. For example the function returning a function |
575 type is as follows: |
574 type is as follows: |
576 |
575 |
577 *} |
576 *} |
578 |
577 |
579 ML{*fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2]) *} |
578 ML{*fun make_fun_type tau1 tau2 = Type ("fun", [tau1, tau2]) *} |
580 |
579 |
581 text {* This can be equally written with the combinator @{ML "-->"} as: *} |
580 text {* This can be equally written with the combinator @{ML "-->"} as: *} |
582 |
581 |
583 ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *} |
582 ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *} |
584 |
583 |
706 |
705 |
707 ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true |
706 ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true |
708 | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true |
707 | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true |
709 | is_nil_or_all _ = false *} |
708 | is_nil_or_all _ = false *} |
710 |
709 |
711 (* |
|
712 text {* |
710 text {* |
713 Occasional you have to calculate what the ``base'' name of a given |
711 Occasional you have to calculate what the ``base'' name of a given |
714 constant is. For this you can use the function @{ML Sign.extern_const} or |
712 constant is. For this you can use the function @{ML Sign.extern_const} or |
715 @{ML Sign.base_name}. For example: |
713 @{ML NameSpace.base_name}. For example: |
716 |
714 |
717 @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""} |
715 @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""} |
718 |
716 |
719 The difference between both functions is that @{ML extern_const in Sign} returns |
717 The difference between both functions is that @{ML extern_const in Sign} returns |
720 the smallest name that is still unique, whereas @{ML base_name in Sign} always |
718 the smallest name that is still unique, whereas @{ML base_name in NameSpace} always |
721 strips off all qualifiers. |
719 strips off all qualifiers. |
722 |
720 |
723 (FIXME: These are probably now NameSpace functions) |
|
724 |
|
725 \begin{readmore} |
721 \begin{readmore} |
726 FIXME: Find the right files to do with naming. |
722 Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"}; |
|
723 functions about signatures in @{ML_file "Pure/sign.ML"}. |
|
724 |
727 \end{readmore} |
725 \end{readmore} |
728 *} |
726 *} |
729 *) |
727 |
730 |
728 |
731 section {* Type-Checking *} |
729 section {* Type-Checking *} |
732 |
730 |
733 text {* |
731 text {* |
734 |
732 |
842 See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading, |
840 See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading, |
843 checking and pretty-printing of terms are defined. Fuctions related to the |
841 checking and pretty-printing of terms are defined. Fuctions related to the |
844 type inference are implemented in @{ML_file "Pure/type.ML"} and |
842 type inference are implemented in @{ML_file "Pure/type.ML"} and |
845 @{ML_file "Pure/type_infer.ML"}. |
843 @{ML_file "Pure/type_infer.ML"}. |
846 \end{readmore} |
844 \end{readmore} |
|
845 |
|
846 (FIXME: say something about sorts) |
847 *} |
847 *} |
848 |
848 |
849 |
849 |
850 section {* Theorems *} |
850 section {* Theorems *} |
851 |
851 |