--- a/ProgTutorial/General.thy Wed Nov 11 12:15:48 2009 +0100
+++ b/ProgTutorial/General.thy Thu Nov 12 10:06:26 2009 +0100
@@ -677,7 +677,7 @@
section {* Unification and Matching *}
text {*
- Isabelle's terms and types may contain schematic term variables
+ As seen earlier, Isabelle's terms and types may contain schematic term variables
(term-constructor @{ML Var}) and schematic type variables (term-constructor
@{ML TVar}). These variables stand for unknown entities, which can be made
more concrete by instantiations. Such instantiations might be a result of
@@ -708,10 +708,10 @@
text {*
The environment @{ML_ind "Vartab.empty"} in line 5 stands for the empty type
environment, which is needed for starting the unification without any
- (pre)instantiations. The @{text 0} is an integer index that we will explain
+ (pre)instantiations. The @{text 0} is an integer index that will be explained
below. In case of failure @{ML typ_unify in Sign} will throw the exception
- @{text TUNIFY}. We can print out the resulting type environment @{ML
- tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the
+ @{text TUNIFY}. We can print out the resulting type environment bound to
+ @{ML tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the
structure @{ML_struct Vartab}.
@{ML_response_fake [display,gray]
@@ -750,10 +750,11 @@
text {*
The first components in this list stand for the schematic type variables and
the second are the associated sorts and types. In this example the sort is
- the default sort @{text "HOL.type"}. We will use in what follows the
- pretty-printing function from Figure~\ref{fig:prettyenv} for @{ML_type
- "Type.tyenv"}s. For the type environment in the example this function prints
- out the more legible:
+ the default sort @{text "HOL.type"}. Instead of @{ML "Vartab.dest"}, we will
+ use in what follows our own pretty-printing function from
+ Figure~\ref{fig:prettyenv} for @{ML_type "Type.tyenv"}s. For the type
+ environment in the example this function prints out the more legible:
+
@{ML_response_fake [display, gray]
"pretty_tyenv @{context} tyenv_unif"
@@ -808,8 +809,8 @@
"index"
"1"}
- Let us now return again to the unification problem @{text "?'a * ?'b"} and
- @{text "?'b list * nat"} from the beginning of the section, and the
+ Let us now return to the unification problem @{text "?'a * ?'b"} and
+ @{text "?'b list * nat"} from the beginning of this section, and the
calculated type environment @{ML tyenv_unif}:
@{ML_response_fake [display, gray]
@@ -820,18 +821,15 @@
Sign} returns is in \emph{not} an instantiation in fully solved form: while @{text
"?'b"} is instantiated to @{typ nat}, this is not propagated to the
instantiation for @{text "?'a"}. In unification theory, this is often
- called an instantiation in \emph{triangular form}. These not fully solved
- instantiations are used because of performance reasons.
- To apply a type environment in triangular form to a type, say @{text "?'a *
+ called an instantiation in \emph{triangular form}. These triangular
+ instantiations, or triangular type environments, are used because of
+ performance reasons. To apply such a type environment to a type, say @{text "?'a *
?'b"}, you should use the function @{ML_ind norm_type in Envir}:
@{ML_response_fake [display, gray]
"Envir.norm_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"
"nat list * nat"}
- With this function the type variables @{text "?'a"} and @{text "?'b"} are
- correctly instantiated.
-
Matching of types can be done with the function @{ML_ind typ_match in Sign}
also from the structure @{ML_struct Sign}. This function returns a @{ML_type
Type.tyenv} as well, but might raise the exception @{text TYPE_MATCH} in case
@@ -854,7 +852,7 @@
Unlike unification, which uses the function @{ML norm_type in Envir},
applying the matcher to a type needs to be done with the function
- @{ML_ind subst_type in Envir}.
+ @{ML_ind subst_type in Envir}. For example
@{ML_response_fake [display, gray]
"Envir.subst_type tyenv_match @{typ_pat \"?'a * ?'b\"}"
@@ -862,7 +860,7 @@
Be careful to observe the difference: use always
@{ML subst_type in Envir} for matchers and @{ML norm_type in Envir}
- for unifiers. To make the difference explicit, let us calculate the
+ for unifiers. To show the difference, let us calculate the
following matcher:
*}
@@ -896,7 +894,7 @@
are in @{ML_file "Pure/sign.ML"}. Matching and unification produce type environments
as results. These are implemented in @{ML_file "Pure/envir.ML"}.
This file also includes the substitution and normalisation functions,
- that apply a type environment to a type. Type environments are lookup
+ which apply a type environment to a type. Type environments are lookup
tables which are implemented in @{ML_file "Pure/term_ord.ML"}.
\end{readmore}
*}
@@ -984,8 +982,8 @@
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
- first symbol under abstractions) is either a constant, or a schematic or a free
- variable. If it is a schematic variable then it can be only applied by
+ 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
twice with the same bound variable. The function @{ML_ind pattern in Pattern}
@@ -1009,8 +1007,8 @@
In this way, matching and unification can be implemented as functions that
produce a type and term environment (unification actually returns a
record of type @{ML_type Envir.env} containing a maxind, a type environment
- and a term environment). The former function is @{ML_ind match in Pattern},
- the latter @{ML_ind unify in Pattern} both implemented in the structure
+ and a term environment). The corresponding functions are @{ML_ind match in Pattern},
+ and @{ML_ind unify in Pattern} both implemented in the structure
@{ML_struct Pattern}. An example for higher-order pattern unification is
@{ML_response_fake [display, gray]
@@ -1029,29 +1027,25 @@
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, matching
- problems are in general undecidable and might in general not posses a single
- most general solution. Therefore Isabelle implements Huet's pre-unification
- algorithm which does not return a single result, rather a lazy list of potentially
- infinite unifiers. The corresponding function is called @{ML_ind unifiers in Unify}.
- An example is as follows
+ As mentioned before, ``full'' higher-order unification, respectively
+ higher-order matching problems, are 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.
+ 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
-
- For higher-order matching the function is called @{ML_ind matchers in Unify}.
- Also this function might potentially return sequences with more than one
- element.
-
Like @{ML unifiers in Unify}, this function does not raise an exception
- in case of failure. It also tries out first whether the matching problem
+ in case of failure. It also first tries out whether the matching problem
can be solved by first-order matching.
\begin{readmore}