1011 record of type @{ML_type Envir.env} containing a maxind, a type environment |
1011 record of type @{ML_type Envir.env} containing a maxind, a type environment |
1012 and a term environment). The former function is @{ML_ind match in Pattern}, |
1012 and a term environment). The former function is @{ML_ind match in Pattern}, |
1013 the latter @{ML_ind unify in Pattern} both implemented in the structure |
1013 the latter @{ML_ind unify in Pattern} both implemented in the structure |
1014 @{ML_struct Pattern}. An example for higher-order pattern unification is |
1014 @{ML_struct Pattern}. An example for higher-order pattern unification is |
1015 |
1015 |
1016 \ldots |
1016 @{ML_response_fake [display, gray] |
1017 *} |
1017 "let |
1018 |
1018 val trm1 = @{term_pat \"\<lambda>x y. g (?X y x) (f (?Y x))\"} |
1019 ML{*let |
1019 val trm2 = @{term_pat \"\<lambda>u v. g u (f u)\"} |
1020 val pat = @{term_pat "?X"} |
1020 val init = Envir.empty 0 |
1021 val trm = @{term "a"} |
1021 val env = Pattern.unify @{theory} (trm1, trm2) init |
1022 val init = (Vartab.empty, Vartab.empty) |
1022 in |
1023 in |
1023 pretty_env @{context} (Envir.term_env env) |
1024 Pattern.match @{theory} (pat, trm) init |
1024 end" |
1025 end *} |
1025 "[?X := \<lambda>y x. x, ?Y := \<lambda>x. x]"} |
1026 |
1026 |
1027 text {* |
1027 |
1028 An assumption of this function is that the terms to be unified have |
1028 An assumption of this function is that the terms to be unified have |
1029 already the same type. In case of failure, the exceptions that are raised |
1029 already the same type. In case of failure, the exceptions that are raised |
1030 are either @{text Pattern}, @{text MATCH} or @{text Unif}. |
1030 are either @{text Pattern}, @{text MATCH} or @{text Unif}. |
1031 |
1031 |
1032 As mentioned before, ``full'' higher-order unification, respectively, matching |
1032 As mentioned before, ``full'' higher-order unification, respectively, matching |