981 |
981 |
982 @{ML_response [display, gray] |
982 @{ML_response [display, gray] |
983 "let |
983 "let |
984 val trm_list = |
984 val trm_list = |
985 [@{term_pat \"?X\"}, @{term_pat \"a\"}, |
985 [@{term_pat \"?X\"}, @{term_pat \"a\"}, |
986 @{term_pat \"\<lambda>a b. ?X a b\"}, @{term_pat \"\<lambda>a b. (op +) a b\"}, |
986 @{term_pat \"f (\<lambda>a b. ?X a b) c\"}, |
|
987 @{term_pat \"\<lambda>a b. (op +) a b\"}, |
987 @{term_pat \"\<lambda>a. (op +) a ?Y\"}, @{term_pat \"?X ?Y\"}, |
988 @{term_pat \"\<lambda>a. (op +) a ?Y\"}, @{term_pat \"?X ?Y\"}, |
988 @{term_pat \"\<lambda>a b. ?X a b ?Y\"}, @{term_pat \"\<lambda>a. ?X a a\"}] |
989 @{term_pat \"\<lambda>a b. ?X a b ?Y\"}, @{term_pat \"\<lambda>a. ?X a a\"}, |
|
990 @{term_pat \"?X a\"}] |
989 in |
991 in |
990 map Pattern.pattern trm_list |
992 map Pattern.pattern trm_list |
991 end" |
993 end" |
992 "[true, true, true, true, true, false, false, false]"} |
994 "[true, true, true, true, true, false, false, false, false]"} |
993 |
995 |
994 The point of the restriction to patterns is that unification and matching |
996 The point of the restriction to patterns is that unification and matching |
995 are decidable and produce most general unifiers, respectively matchers. |
997 are decidable and produce most general unifiers, respectively matchers. |
996 Note that \emph{both} terms to be unified have to be higher-order patterns |
998 Note that \emph{both} terms to be unified have to be higher-order patterns |
997 for this to work. The exception @{ML_ind Pattern in Pattern} indicates failure |
999 for this to work. The exception @{ML_ind Pattern in Pattern} indicates failure |