692 Let us begin with describing unification and matching of types. Both |
692 Let us begin with describing unification and matching of types. Both |
693 matching and unification of types return a type environment, ML-type |
693 matching and unification of types return a type environment, ML-type |
694 @{ML_type "Type.tyenv"}, which maps schematic type variables to types (and |
694 @{ML_type "Type.tyenv"}, which maps schematic type variables to types (and |
695 sorts). Below we use the function @{ML_ind typ_unify in Sign} from the |
695 sorts). Below we use the function @{ML_ind typ_unify in Sign} from the |
696 structure @{ML_struct Sign} for unifying |
696 structure @{ML_struct Sign} for unifying |
697 the types @{text "?'a * nat"} and @{text "?'b list * ?'b"}. This will |
697 the types @{text "?'a * ?'b"} and @{text "?'b list * nat"}. This will |
698 produce the mapping @{text "[?'a := ?'b list, ?'b := nat]"}. |
698 produce the mapping @{text "[?'a := ?'b list, ?'b := nat]"}. |
699 *} |
699 *} |
700 |
700 |
701 ML{*val (tyenv_unif, _) = let |
701 ML{*val (tyenv_unif, _) = let |
702 val ty1 = @{typ_pat "?'a * nat"} |
702 val ty1 = @{typ_pat "?'a * ?'b"} |
703 val ty2 = @{typ_pat "?'b list * ?'b"} |
703 val ty2 = @{typ_pat "?'b list * nat"} |
704 in |
704 in |
705 Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0) |
705 Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0) |
706 end*} |
706 end*} |
707 |
707 |
708 text {* |
708 text {* |
709 The value @{ML_ind empty in Vartab} stands for the empty type environment, |
709 The value @{ML_ind empty in Vartab} stands for the empty type environment, |
710 which is the value for starting the unification without any |
710 which is the value for starting the unification without any |
711 instantiations.\footnote{\bf FIXME: what is 0?} |
711 instantiations.\footnote{\bf FIXME: what is 0?} |
712 We can print out the resulting |
712 We can print out the resulting type environment @{ML tyenv_unif} |
713 type environment with the built-in function @{ML_ind dest in Vartab}. |
713 with the built-in function @{ML_ind dest in Vartab}. |
714 |
714 |
715 @{ML_response_fake [display,gray] |
715 @{ML_response_fake [display,gray] |
716 "Vartab.dest tyenv_unif" |
716 "Vartab.dest tyenv_unif" |
717 "[((\"'a\", 0), ([\"HOL.type\"], \"?'b List.list\")), |
717 "[((\"'a\", 0), ([\"HOL.type\"], \"?'b List.list\")), |
718 ((\"'b\", 0), ([\"HOL.type\"], \"nat\"))]"} |
718 ((\"'b\", 0), ([\"HOL.type\"], \"nat\"))]"} |
783 @{ML_response_fake [display, gray] |
783 @{ML_response_fake [display, gray] |
784 "Envir.subst_type tyenv_match @{typ_pat \"?'a * ?'b\"}" |
784 "Envir.subst_type tyenv_match @{typ_pat \"?'a * ?'b\"}" |
785 "bool list * nat"} |
785 "bool list * nat"} |
786 |
786 |
787 Be careful to observe the difference: use @{ML subst_type in Envir} |
787 Be careful to observe the difference: use @{ML subst_type in Envir} |
788 for matchers and @{ML norm_type in Envir} for unifiers. To show the |
788 for matchers and @{ML norm_type in Envir} for unifiers. To make the |
789 difference let us calculate the following matcher. |
789 difference explicit let us calculate the following matcher. |
790 *} |
790 *} |
791 |
791 |
792 ML{*val tyenv_match' = let |
792 ML{*val tyenv_match' = let |
793 val pat = @{typ_pat "?'a * ?'b"} |
793 val pat = @{typ_pat "?'a * ?'b"} |
794 and ty = @{typ_pat "?'b list * nat"} |
794 and ty = @{typ_pat "?'b list * nat"} |
796 Sign.typ_match @{theory} (pat, ty) Vartab.empty |
796 Sign.typ_match @{theory} (pat, ty) Vartab.empty |
797 end*} |
797 end*} |
798 |
798 |
799 text {* |
799 text {* |
800 Now @{ML tyenv_unif} is equal to @{ML tyenv_match'}. Consider |
800 Now @{ML tyenv_unif} is equal to @{ML tyenv_match'}. Consider |
801 again the type @{text "?'a * ?'b"}. If we apply |
801 again the type @{text "?'a * ?'b"}, which we used in the unification |
802 @{ML norm_type in Envir} to the matcher we obtain |
802 and matching problems. If we apply @{ML norm_type in Envir} to |
|
803 the matcher we obtain |
803 |
804 |
804 @{ML_response_fake [display, gray] |
805 @{ML_response_fake [display, gray] |
805 "Envir.norm_type tyenv_match' @{typ_pat \"?'a * ?'b\"}" |
806 "Envir.norm_type tyenv_match' @{typ_pat \"?'a * ?'b\"}" |
806 "nat list * nat"} |
807 "nat list * nat"} |
807 |
808 |
808 which is not a matcher for the second matching problem, and if |
809 which is not a matcher for the second matching problem, and if |
809 we apply @{ML subst_type in Envir} to the unifier |
810 we apply @{ML subst_type in Envir} to the unifier we obtain |
810 |
811 |
811 @{ML_response_fake [display, gray] |
812 @{ML_response_fake [display, gray] |
812 "Envir.subst_type tyenv_unif @{typ_pat \"?'a * ?'b\"}" |
813 "Envir.subst_type tyenv_unif @{typ_pat \"?'a * ?'b\"}" |
813 "?'b list * nat"} |
814 "?'b list * nat"} |
814 |
815 |
817 \begin{readmore} |
818 \begin{readmore} |
818 Unification and matching of types is implemented |
819 Unification and matching of types is implemented |
819 in @{ML_file "Pure/type.ML"}. The ``interface'' functions for them |
820 in @{ML_file "Pure/type.ML"}. The ``interface'' functions for them |
820 are in @{ML_file "Pure/sign.ML"}. Matching and unification produce type environments |
821 are in @{ML_file "Pure/sign.ML"}. Matching and unification produce type environments |
821 as results. These are implemented in @{ML_file "Pure/envir.ML"}. |
822 as results. These are implemented in @{ML_file "Pure/envir.ML"}. |
822 This file also includes the substitution and normalisation functions. |
823 This file also includes the substitution and normalisation functions, |
823 Environments are lookup tables that are implemented in |
824 that apply a type environment to a type. Type environments are lookup |
824 @{ML_file "Pure/term_ord.ML"}. |
825 tables which are implemented in @{ML_file "Pure/term_ord.ML"}. |
825 \end{readmore} |
826 \end{readmore} |
826 *} |
827 *} |
827 |
828 |
828 text {* |
829 text {* |
829 TBD below |
830 TBD below |