677 section {* Matching and Unification (TBD) *}

   677 section {* Unification and Matching (TBD) *}

   680   Using the antiquotation from Section~\ref{sec:antiquote}.

   680   Isabelle's terms and types contain schematic term variables

   681 *}

   681   (term-constructor @{ML Var}) and schematic type variables (term-constructor

   682 

   682   @{ML TVar}). Both are printed out as variables with a leading question

   683 ML{*val (env, _) = 

   683   mark. They stand for unknown terms and types, which can be made more concrete

   684   Sign.typ_unify @{theory} (@{typ_pat "?'b * ?'c"}, @{typ_pat "?'a * ?'b"}) (Vartab.empty, 0) *}

   684   by instantiations. Such instantiations can be calculated by unification or

   685 

   685   matching. While in case of types, unification and matching is relatively

   686 ML{*Vartab.dest env  *}

   686   straightforward, in case of terms the algorithms are substantially more

   687 

   687   complicated, because terms need higher-order versions of the unification and

   688 ML{*Envir.norm_type env @{typ_pat "?'a"}*}

   688   matching algorithms. Below we shall use the antiquotation @{text "@{typ_pat \<dots>}"} and

   689 

   689   @{text "@{term_pat \<dots>}"} from Section~\ref{sec:antiquote} in order to

   690 ML{*val env = 

   690   construct examples involving schematic variables.

   691   Sign.typ_match @{theory} (@{typ_pat "?'b * ?'c"}, @{typ_pat "?'a * ?'b"}) Vartab.empty *}

   691 

   692 

   692   Let us begin with describing unification and matching of types.  Both

   693 ML{*Envir.subst_type env  @{typ_pat "?'a"} *}

   693   matching and unification of types return a type environment, ML-type

   694 

   694   @{ML_type "Type.tyenv"}, which maps schematic type variables to types (and

   695 text {*

   695   sorts). Below we use the function @{ML_ind typ_unify in Sign} from the 

   696   Note the difference. Norm for unify; Subst for match.

   696   structure @{ML_struct Sign} for unifying

   697   the types @{text "?'a * nat"} and @{text "?'b list * ?'b"}. This will

   698   produce the mapping @{text "[?'a := ?'b list, ?'b := nat]"}.

   699 *}

   700 

   701 ML{*val (tyenv_unif, _) = let

   702   val ty1 = @{typ_pat "?'a * nat"}

   703   val ty2 = @{typ_pat "?'b list * ?'b"}

   704 in

   705   Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0) 

   706 end*}

   707 

   708 text {* 

   709   The value @{ML_ind empty in Vartab} stands for the empty type environment, 

   710   which is the value for starting the unification without any 

   711   instantiations.\footnote{\bf FIXME: what is 0?} 

   712   We can print out the resulting 

   713   type environment with the built-in function @{ML_ind dest in Vartab}.

   714 

   715   @{ML_response_fake [display,gray]

   716   "Vartab.dest tyenv_unif"

   717   "[((\"'a\", 0), ([\"HOL.type\"], \"?'b List.list\")), 

   718  ((\"'b\", 0), ([\"HOL.type\"], \"nat\"))]"}

   719 

   720   For what follows we will use the following pretty-printing function

   721   for @{ML_type "Type.tyenv"}s

   722 *}

   723 

   724 ML{*fun pretty_tyenv ctxt tyenv =

   725 let

   726   fun aux (v, (s, T)) =

   727         Syntax.string_of_typ ctxt (TVar (v, s)) 

   728         ^ " := " ^ Syntax.string_of_typ ctxt T

   729 in

   730   tyenv |> Vartab.dest

   731         |> map aux 

   732         |> commas

   733         |> enclose "[" "]"

   734         |> tracing

   735 end*}

   736 

   737 text {*

   738   which prints for the type environment above

   739 

   740   @{ML_response_fake [display, gray]

   741   "pretty_tyenv @{context} tyenv_unif"

   742   "[?'a := ?'b list, ?'b := nat]"}

   743 

   744   Observe that the type environment that the function @{ML typ_unify in

   745   Sign} returns is in \emph{not} an instantiation in fully solved form: while @{text

   746   "?'b"} is instantiated to @{typ nat}, this is not propagated to the

   747   instantiation for @{text "?'a"}.  In unification theory, this is often

   748   called an instantiation in \emph{triangular form}. These instantiations

   749   are used because of performance reasons.

   750 

   751 

   752   To apply a type environment in triangular form to a type, say @{text "?'a *

   753   ?'b"}, you should use the function @{ML_ind norm_type in Envir}:

   754 

   755   @{ML_response_fake [display, gray]

   756   "Envir.norm_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"

   757   "nat list * nat"}

   758 *}

   759 

   760 text {* 

   761   Matching of types can be done with the function @{ML_ind typ_match in Sign}

   762   from the structure @{ML_struct Sign}. It also returns a @{ML_type

   763   Type.tyenv}. For example

   764 *}

   765 

   766 ML{*val tyenv_match = let

   767   val pat = @{typ_pat "?'a * ?'b"}

   768   and ty  = @{typ_pat "bool list * nat"}

   769 in

   770   Sign.typ_match @{theory} (pat, ty) Vartab.empty 

   771 end*}

   772 

   773 text {*

   774   Printing out the calculated matcher gives

   775 

   776   @{ML_response_fake [display,gray]

   777   "pretty_tyenv @{context} tyenv_match"

   778   "[?'a := bool list, ?'b := nat]"}

   779   

   780   Applying the matcher to a type needs to be done with the function

   781   @{ML_ind subst_type in Envir}.

   782 

   783   @{ML_response_fake [display, gray]

   784   "Envir.subst_type tyenv_match @{typ_pat \"?'a * ?'b\"}"

   785   "bool list * nat"}

   786 

   787   Be careful to observe the difference: use @{ML subst_type in Envir} 

   788   for matchers and @{ML norm_type in Envir} for unifiers. To show the 

   789   difference let us calculate the following matcher.

   790 *}

   791 

   792 ML{*val tyenv_match' = let

   793   val pat = @{typ_pat "?'a * ?'b"}

   794   and ty  = @{typ_pat "?'b list * nat"}

   795 in

   796   Sign.typ_match @{theory} (pat, ty) Vartab.empty 

   797 end*}

   798 

   799 text {*

   800   Now @{ML tyenv_unif} is equal to @{ML tyenv_match'}. Consider

   801   again the type @{text "?'a * ?'b"}. If we apply 

   802   @{ML norm_type in Envir} to the matcher we obtain

   803 

   804   @{ML_response_fake [display, gray]

   805   "Envir.norm_type tyenv_match' @{typ_pat \"?'a * ?'b\"}"

   806   "nat list * nat"}

   807 

   808   which is not a matcher for the second matching problem, and if

   809   we apply @{ML subst_type in Envir} to the unifier

   810 

   811   @{ML_response_fake [display, gray]

   812   "Envir.subst_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"

   813   "?'b list * nat"}

   814   

   815   which is not the correct unifier for the unification problem.

   816 

   817   \begin{readmore}

   818   Unification and matching of types is implemented

   819   in @{ML_file "Pure/type.ML"}. The ``interface'' functions for them

   820   are in @{ML_file "Pure/sign.ML"}. Matching and unification produce type environments

   821   as results. These are implemented in @{ML_file "Pure/envir.ML"}.

   822   This file also includes the substitution and normalisation functions. 

   823   Environments are lookup tables that are implemented in 

   824   @{ML_file "Pure/term_ord.ML"}.

   825   \end{readmore}

   826 *}

   827 

   828 text {*

   829   TBD below

   830 

   831 

   832   \begin{readmore}

   833   For term, unification and matching of higher-order patterns is implemented in 

   834   @{ML_file "Pure/pattern.ML"}. Full higher-order unification is implemented

   835   in @{ML_file "Pure/unify.ML"}. 

   836   \end{readmore}