817 @{ML_response_fake [display, gray] |
817 @{ML_response_fake [display, gray] |
818 "pretty_tyenv @{context} tyenv_unif" |
818 "pretty_tyenv @{context} tyenv_unif" |
819 "[?'a := ?'b list, ?'b := nat]"} |
819 "[?'a := ?'b list, ?'b := nat]"} |
820 |
820 |
821 Observe that the type environment which the function @{ML typ_unify in |
821 Observe that the type environment which the function @{ML typ_unify in |
822 Sign} returns is in \emph{not} an instantiation in fully solved form: while @{text |
822 Sign} returns is \emph{not} an instantiation in fully solved form: while @{text |
823 "?'b"} is instantiated to @{typ nat}, this is not propagated to the |
823 "?'b"} is instantiated to @{typ nat}, this is not propagated to the |
824 instantiation for @{text "?'a"}. In unification theory, this is often |
824 instantiation for @{text "?'a"}. In unification theory, this is often |
825 called an instantiation in \emph{triangular form}. These triangular |
825 called an instantiation in \emph{triangular form}. These triangular |
826 instantiations, or triangular type environments, are used because of |
826 instantiations, or triangular type environments, are used because of |
827 performance reasons. To apply such a type environment to a type, say @{text "?'a * |
827 performance reasons. To apply such a type environment to a type, say @{text "?'a * |
857 |
857 |
858 @{ML_response_fake [display, gray] |
858 @{ML_response_fake [display, gray] |
859 "Envir.subst_type tyenv_match @{typ_pat \"?'a * ?'b\"}" |
859 "Envir.subst_type tyenv_match @{typ_pat \"?'a * ?'b\"}" |
860 "bool list * nat"} |
860 "bool list * nat"} |
861 |
861 |
862 Be careful to observe the difference: use always |
862 Be careful to observe the difference: always use |
863 @{ML subst_type in Envir} for matchers and @{ML norm_type in Envir} |
863 @{ML subst_type in Envir} for matchers and @{ML norm_type in Envir} |
864 for unifiers. To show the difference, let us calculate the |
864 for unifiers. To show the difference, let us calculate the |
865 following matcher: |
865 following matcher: |
866 *} |
866 *} |
867 |
867 |
933 in |
933 in |
934 Pattern.first_order_match @{theory} (fo_pat, trm_a $ trm_b) init |
934 Pattern.first_order_match @{theory} (fo_pat, trm_a $ trm_b) init |
935 end *} |
935 end *} |
936 |
936 |
937 text {* |
937 text {* |
938 In this example we annotated explicitly types because then |
938 In this example we annotated types explicitly because then |
939 the type environment is empty and can be ignored. The |
939 the type environment is empty and can be ignored. The |
940 resulting term environment is |
940 resulting term environment is |
941 |
941 |
942 @{ML_response_fake [display, gray] |
942 @{ML_response_fake [display, gray] |
943 "pretty_env @{context} fo_env" |
943 "pretty_env @{context} fo_env" |
958 |> tracing |
958 |> tracing |
959 end" |
959 end" |
960 "P (\<lambda>a b. Q b a)"} |
960 "P (\<lambda>a b. Q b a)"} |
961 |
961 |
962 First-order matching is useful for matching against applications and |
962 First-order matching is useful for matching against applications and |
963 variables. It can deal also with abstractions and a limited form of |
963 variables. It can also deal with abstractions and a limited form of |
964 alpha-equivalence, but this kind of matching should be used with care, since |
964 alpha-equivalence, but this kind of matching should be used with care, since |
965 it is not clear whether the result is meaningful. A meaningful example is |
965 it is not clear whether the result is meaningful. A meaningful example is |
966 matching @{text "\<lambda>x. P x"} against the pattern @{text "\<lambda>y. ?X y"}. In this |
966 matching @{text "\<lambda>x. P x"} against the pattern @{text "\<lambda>y. ?X y"}. In this |
967 case, first-order matching produces @{text "[?X := P]"}. |
967 case, first-order matching produces @{text "[?X := P]"}. |
968 |
968 |
982 text {* |
982 text {* |
983 Unification of abstractions is more thoroughly studied in the context |
983 Unification of abstractions is more thoroughly studied in the context |
984 of higher-order pattern unification and higher-order pattern matching. A |
984 of higher-order pattern unification and higher-order pattern matching. A |
985 \emph{\index*{pattern}} is an abstraction term whose ``head symbol'' (that is the |
985 \emph{\index*{pattern}} is an abstraction term whose ``head symbol'' (that is the |
986 first symbol under an abstraction) is either a constant, a schematic or a free |
986 first symbol under an abstraction) is either a constant, a schematic or a free |
987 variable. If it is a schematic variable then it can be only applied with |
987 variable. If it is a schematic variable then it can only have distinct bound |
988 distinct bound variables. This excludes terms where a schematic variable is an |
988 variables as arguments. This excludes terms where a schematic variable is an |
989 argument of another one and where a schematic variable is applied |
989 argument of another one and where a schematic variable is applied |
990 twice with the same bound variable. The function @{ML_ind pattern in Pattern} |
990 twice with the same bound variable. The function @{ML_ind pattern in Pattern} |
991 in the structure @{ML_struct Pattern} tests whether a term satisfies these |
991 in the structure @{ML_struct Pattern} tests whether a term satisfies these |
992 restrictions. |
992 restrictions. |
993 |
993 |