diff -r 5f7ca76f94e3 -r 5dcee4d751ad ProgTutorial/General.thy --- a/ProgTutorial/General.thy Thu Nov 12 10:06:26 2009 +0100 +++ b/ProgTutorial/General.thy Thu Nov 12 20:35:14 2009 +0100 @@ -774,7 +774,7 @@ text {* The index @{text 0} in Line 5 is the maximal index of the schematic type - variables occurring in @{text ty1} and @{text ty2}. This index will be + variables occurring in @{text tys1} and @{text tys2}. This index will be increased whenever a new schematic type variable is introduced during unification. This is for example the case when two schematic type variables have different, incomparable sorts. Then a new schematic type variable is @@ -798,12 +798,12 @@ @{ML_response_fake [display,gray] "pretty_tyenv @{context} tyenv" - "[?'a::s1 := ?'a1::{s1,s2}, ?'b::s2 := ?'a1::{s1,s2}]"} + "[?'a::s1 := ?'a1::{s1, s2}, ?'b::s2 := ?'a1::{s1, s2}]"} As can be seen, the type variables @{text "?'a"} and @{text "?'b"} are instantiated - with a new type variable @{text "?'a1"} with sort @{text "{s1,s2}"}. Since a new + with a new type variable @{text "?'a1"} with sort @{text "{s1, s2}"}. Since a new type variable has been introduced the @{ML index}, originally being @{text 0}, - has been increased by @{text 1}. + has been increased to @{text 1}. @{ML_response [display,gray] "index" @@ -926,11 +926,11 @@ ML{*val (_, fo_env) = let val fo_pat = @{term_pat "(?X::(nat\nat\nat)\bool) ?Y"} - val trm = @{term "P::(nat\nat\nat)\bool"} - $ @{term "\a b. (Q::nat\nat\nat) b a"} + val trm_a = @{term "P::(nat\nat\nat)\bool"} + val trm_b = @{term "\a b. (Q::nat\nat\nat) b a"} val init = (Vartab.empty, Vartab.empty) in - Pattern.first_order_match @{theory} (fo_pat, trm) init + Pattern.first_order_match @{theory} (fo_pat, trm_a $ trm_b) init end *} text {* @@ -963,7 +963,7 @@ alpha-equivalence, but this kind of matching should be used with care, since it is not clear whether the result is meaningful. A meaningful example is matching @{text "\x. P x"} against the pattern @{text "\y. ?X y"}. In this - case first-order matching produces @{text "[?X := P]"}. + case, first-order matching produces @{text "[?X := P]"}. @{ML_response_fake [display, gray] "let @@ -981,11 +981,11 @@ text {* Unification of abstractions is more thoroughly studied in the context of higher-order pattern unification and higher-order pattern matching. A - \emph{\index*{pattern}} is a lambda term whose ``head symbol'' (that is the + \emph{\index*{pattern}} is an abstraction term whose ``head symbol'' (that is the first symbol under an abstraction) is either a constant, a schematic or a free variable. If it is a schematic variable then it can be only applied with - distinct bound variables. This excludes that a schematic variable is an - argument of another one and that a schematic variable is applied + distinct bound variables. This excludes terms where a schematic variable is an + argument of another one and where a schematic variable is applied twice with the same bound variable. The function @{ML_ind pattern in Pattern} in the structure @{ML_struct Pattern} tests whether a term satisfies these restrictions. @@ -1022,31 +1022,81 @@ end" "[?X := \y x. x, ?Y := \x. x]"} - - An assumption of this function is that the terms to be unified have - already the same type. In case of failure, the exceptions that are raised - are either @{text Pattern}, @{text MATCH} or @{text Unif}. - - As mentioned before, ``full'' higher-order unification, respectively - higher-order matching problems, are in general undecidable and might also not posses a + The function @{ML_ind "Envir.empty"} generates a record with a specified + max-index for the schematic variables (in the example the index is @{text + 0}) and empty type and term environments. The function @{ML_ind + "Envir.term_env"} pulls out the term environment from the result record. The + function for type environment is @{ML_ind "Envir.type_env"}. An assumption of + this function is that the terms to be unified have already the same type. In + case of failure, the exceptions that are raised are either @{text Pattern}, + @{text MATCH} or @{text Unif}. + + As mentioned before, unrestricted higher-order unification, respectively + higher-order matching, is in general undecidable and might also not posses a single most general solution. Therefore Isabelle implements the unification function @{ML_ind unifiers in Unify} so that it returns a lazy list of potentially infinite unifiers. An example is as follows - - \ldots - - In case of failure this function does not raise an exception, rather returns - the empty sequence. In order to find a reasonable solution for a unification - problem, Isabelle also tries first to solve the problem by higher-order - pattern unification. For higher-order matching the function is called - @{ML_ind matchers in Unify}. Also this function might potentially return - sequences with more than one matcher. - - \ldots - +*} + +ML{*val uni_seq = +let + val trm1 = @{term_pat "?X ?Y"} + val trm2 = @{term "f a"} + val init = Envir.empty 0 +in + Unify.unifiers (@{theory}, init, [(trm1, trm2)]) +end *} + +text {* + The unifiers can be extracted from the lazy sequence using the + function @{ML_ind "Seq.pull"}. In the example we obtain three + unifiers @{text "un1\un3"}. +*} + +ML{*val SOME ((un1, _), next1) = Seq.pull uni_seq; +val SOME ((un2, _), next2) = Seq.pull next1; +val SOME ((un3, _), next3) = Seq.pull next2; +val NONE = Seq.pull next3 *} + +text {* + \footnote{\bf FIXME: what is the list of term pairs in the unifier: flex-flex pairs?} + + We can print them out as follows. + + @{ML_response_fake [display, gray] + "pretty_env @{context} (Envir.term_env un1); +pretty_env @{context} (Envir.term_env un2); +pretty_env @{context} (Envir.term_env un3)" + "[?X := \a. a, ?Y := f a] +[?X := f, ?Y := a] +[?X := \b. f a]"} + + + In case of failure the function @{ML_ind unifiers in Unify} does not raise + an exception, rather returns the empty sequence. For example + + @{ML_response [display, gray] +"let + val trm1 = @{term \"a\"} + val trm2 = @{term \"b\"} + val init = Envir.empty 0 +in + Unify.unifiers (@{theory}, init, [(trm1, trm2)]) + |> Seq.pull +end" +"NONE"} + + In order to find a + reasonable solution for a unification problem, Isabelle also tries first to + solve the problem by higher-order pattern unification. + + For higher-order + matching the function is called @{ML_ind matchers in Unify} implemented + in the structure @{ML_struct Unify}. Also this + function returns sequences with possibly more than one matcher. Like @{ML unifiers in Unify}, this function does not raise an exception - in case of failure. It also first tries out whether the matching problem - can be solved by first-order matching. + in case of failure, but returns an empty sequence. It also first tries + out whether the matching problem can be solved by first-order matching. \begin{readmore} Unification and matching of higher-order patterns is implemented in @@ -2425,6 +2475,14 @@ ML {* Sign.intern_type @{theory} "list" *} ML {* Sign.intern_const @{theory} "prod_fun" *} + +text {* + @{ML_ind "Binding.str_of"} returns the string with markup; + @{ML_ind "Binding.name_of"} returns the string without markup +*} + + + section {* Summary *} text {*