--- a/ProgTutorial/General.thy Sat Nov 07 10:08:09 2009 +0100
+++ b/ProgTutorial/General.thy Mon Nov 09 09:25:51 2009 +0100
@@ -674,26 +674,166 @@
\end{exercise}
*}
-section {* Matching and Unification (TBD) *}
+section {* Unification and Matching (TBD) *}
text {*
- Using the antiquotation from Section~\ref{sec:antiquote}.
+ Isabelle's terms and types contain schematic term variables
+ (term-constructor @{ML Var}) and schematic type variables (term-constructor
+ @{ML TVar}). Both are printed out as variables with a leading question
+ mark. They stand for unknown terms and types, which can be made more concrete
+ by instantiations. Such instantiations can be calculated by unification or
+ matching. While in case of types, unification and matching is relatively
+ straightforward, in case of terms the algorithms are substantially more
+ complicated, because terms need higher-order versions of the unification and
+ matching algorithms. Below we shall use the antiquotation @{text "@{typ_pat \<dots>}"} and
+ @{text "@{term_pat \<dots>}"} from Section~\ref{sec:antiquote} in order to
+ construct examples involving schematic variables.
+
+ Let us begin with describing unification and matching of types. Both
+ matching and unification of types return a type environment, ML-type
+ @{ML_type "Type.tyenv"}, which maps schematic type variables to types (and
+ sorts). Below we use the function @{ML_ind typ_unify in Sign} from the
+ structure @{ML_struct Sign} for unifying
+ the types @{text "?'a * nat"} and @{text "?'b list * ?'b"}. This will
+ produce the mapping @{text "[?'a := ?'b list, ?'b := nat]"}.
+*}
+
+ML{*val (tyenv_unif, _) = let
+ val ty1 = @{typ_pat "?'a * nat"}
+ val ty2 = @{typ_pat "?'b list * ?'b"}
+in
+ Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0)
+end*}
+
+text {*
+ The value @{ML_ind empty in Vartab} stands for the empty type environment,
+ which is the value for starting the unification without any
+ instantiations.\footnote{\bf FIXME: what is 0?}
+ We can print out the resulting
+ type environment with the built-in function @{ML_ind dest in Vartab}.
+
+ @{ML_response_fake [display,gray]
+ "Vartab.dest tyenv_unif"
+ "[((\"'a\", 0), ([\"HOL.type\"], \"?'b List.list\")),
+ ((\"'b\", 0), ([\"HOL.type\"], \"nat\"))]"}
+
+ For what follows we will use the following pretty-printing function
+ for @{ML_type "Type.tyenv"}s
*}
-ML{*val (env, _) =
- Sign.typ_unify @{theory} (@{typ_pat "?'b * ?'c"}, @{typ_pat "?'a * ?'b"}) (Vartab.empty, 0) *}
+ML{*fun pretty_tyenv ctxt tyenv =
+let
+ fun aux (v, (s, T)) =
+ Syntax.string_of_typ ctxt (TVar (v, s))
+ ^ " := " ^ Syntax.string_of_typ ctxt T
+in
+ tyenv |> Vartab.dest
+ |> map aux
+ |> commas
+ |> enclose "[" "]"
+ |> tracing
+end*}
-ML{*Vartab.dest env *}
+text {*
+ which prints for the type environment above
+
+ @{ML_response_fake [display, gray]
+ "pretty_tyenv @{context} tyenv_unif"
+ "[?'a := ?'b list, ?'b := nat]"}
-ML{*Envir.norm_type env @{typ_pat "?'a"}*}
+ Observe that the type environment that the function @{ML typ_unify in
+ 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 instantiations
+ are used because of performance reasons.
+
+
+ To apply a type environment in triangular form to a type, say @{text "?'a *
+ ?'b"}, you should use the function @{ML_ind norm_type in Envir}:
-ML{*val env =
- Sign.typ_match @{theory} (@{typ_pat "?'b * ?'c"}, @{typ_pat "?'a * ?'b"}) Vartab.empty *}
+ @{ML_response_fake [display, gray]
+ "Envir.norm_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"
+ "nat list * nat"}
+*}
-ML{*Envir.subst_type env @{typ_pat "?'a"} *}
+text {*
+ Matching of types can be done with the function @{ML_ind typ_match in Sign}
+ from the structure @{ML_struct Sign}. It also returns a @{ML_type
+ Type.tyenv}. For example
+*}
+
+ML{*val tyenv_match = let
+ val pat = @{typ_pat "?'a * ?'b"}
+ and ty = @{typ_pat "bool list * nat"}
+in
+ Sign.typ_match @{theory} (pat, ty) Vartab.empty
+end*}
text {*
- Note the difference. Norm for unify; Subst for match.
+ Printing out the calculated matcher gives
+
+ @{ML_response_fake [display,gray]
+ "pretty_tyenv @{context} tyenv_match"
+ "[?'a := bool list, ?'b := nat]"}
+
+ Applying the matcher to a type needs to be done with the function
+ @{ML_ind subst_type in Envir}.
+
+ @{ML_response_fake [display, gray]
+ "Envir.subst_type tyenv_match @{typ_pat \"?'a * ?'b\"}"
+ "bool list * nat"}
+
+ Be careful to observe the difference: use @{ML subst_type in Envir}
+ for matchers and @{ML norm_type in Envir} for unifiers. To show the
+ difference let us calculate the following matcher.
+*}
+
+ML{*val tyenv_match' = let
+ val pat = @{typ_pat "?'a * ?'b"}
+ and ty = @{typ_pat "?'b list * nat"}
+in
+ Sign.typ_match @{theory} (pat, ty) Vartab.empty
+end*}
+
+text {*
+ Now @{ML tyenv_unif} is equal to @{ML tyenv_match'}. Consider
+ again the type @{text "?'a * ?'b"}. If we apply
+ @{ML norm_type in Envir} to the matcher we obtain
+
+ @{ML_response_fake [display, gray]
+ "Envir.norm_type tyenv_match' @{typ_pat \"?'a * ?'b\"}"
+ "nat list * nat"}
+
+ which is not a matcher for the second matching problem, and if
+ we apply @{ML subst_type in Envir} to the unifier
+
+ @{ML_response_fake [display, gray]
+ "Envir.subst_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"
+ "?'b list * nat"}
+
+ which is not the correct unifier for the unification problem.
+
+ \begin{readmore}
+ Unification and matching of types is implemented
+ in @{ML_file "Pure/type.ML"}. The ``interface'' functions for them
+ 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.
+ Environments are lookup tables that are implemented in
+ @{ML_file "Pure/term_ord.ML"}.
+ \end{readmore}
+*}
+
+text {*
+ TBD below
+
+
+ \begin{readmore}
+ For term, unification and matching of higher-order patterns is implemented in
+ @{ML_file "Pure/pattern.ML"}. Full higher-order unification is implemented
+ in @{ML_file "Pure/unify.ML"}.
+ \end{readmore}
*}
section {* Type-Checking\label{sec:typechecking} *}