--- 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\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y"}
- val trm = @{term "P::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool"}
- $ @{term "\<lambda>a b. (Q::nat\<Rightarrow>nat\<Rightarrow>nat) b a"}
+ val trm_a = @{term "P::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool"}
+ val trm_b = @{term "\<lambda>a b. (Q::nat\<Rightarrow>nat\<Rightarrow>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 "\<lambda>x. P x"} against the pattern @{text "\<lambda>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 := \<lambda>y x. x, ?Y := \<lambda>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\<dots>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 := \<lambda>a. a, ?Y := f a]
+[?X := f, ?Y := a]
+[?X := \<lambda>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 {*