# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1257584889 -3600
# Node ID 272ba2cceeb29665451328b49787ded94ad10cb6
# Parent  76b1b679e845772eed1e6edd16aacd3d95b130a8
added a section about unification and matching

diff -r 76b1b679e845 -r 272ba2cceeb2 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Sat Nov 07 01:44:11 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Sat Nov 07 10:08:09 2009 +0100
@@ -275,7 +275,7 @@
   where @{text 1} and @{text x} are displayed with their inferred type.
   Even more type information can be printed by setting 
   the reference @{ML_ind show_all_types in Syntax} to @{ML true}. 
-  We obtain then
+  In this case we obtain
 *}
 (*<*)ML %linenos {*show_all_types := true*}
 (*>*)
@@ -285,8 +285,8 @@
   "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"}
 
   where @{term Pair} is the term-constructor for products. 
-  Other references that influence printing are @{ML_ind show_brackets in Syntax} 
-  and @{ML_ind show_sorts in Syntax}. 
+  Other references that influence printing of terms are 
+  @{ML_ind show_brackets in Syntax} and @{ML_ind show_sorts in Syntax}. 
 *}
 (*<*)ML %linenos {*show_types := false; show_all_types := false*}
 (*>*)
@@ -774,7 +774,7 @@
 *}
 
 
-section {* ML-Antiquotations *}
+section {* ML-Antiquotations\label{sec:antiquote} *}
 
 text {*
   Recall from Section \ref{sec:include} that code in Isabelle is always
@@ -845,11 +845,11 @@
 ML{*val foo_thm = @{lemma "True" and "True" by simp simp} *}
 
 text {*
-  which can be printed out as follows
+  The result can be printed out as follows.
 
   @{ML_response_fake [gray,display]
 "foo_thm |> string_of_thms @{context}
-         |> tracing"
+        |> tracing"
   "True, True"}
 
   You can also refer to the current simpset via an antiquotation. To illustrate 
@@ -949,8 +949,22 @@
   "@{term_pat \"Suc (?x::nat)\"}"
   "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}
 
-  which shows the internal representation of the term @{text "Suc ?x"}.
+  which shows the internal representation of the term @{text "Suc ?x"}. Similarly
+  we can write an antiquotation for type patterns.
+*}
+
+ML %linenosgray{*let
+  val parser = Args.context -- Scan.lift Args.name_source
 
+  fun typ_pat (ctxt, str) =
+     str |> Syntax.parse_typ ctxt
+         |> ML_Syntax.print_typ
+         |> ML_Syntax.atomic
+in
+  ML_Antiquote.inline "typ_pat" (parser >> typ_pat)
+end*}
+
+text {*
   \begin{readmore}
   The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions
   for most antiquotations. Most of the basic operations on ML-syntax are implemented 
@@ -1267,8 +1281,8 @@
 text {*
   This code declares a data container where the theorems are stored,
   an attribute @{text foo} (with the @{text add} and @{text del} options
-  for adding and deleting theorems) and an internal ML-interface to retrieve and 
-  modify the theorems.
+  for adding and deleting theorems) and an internal ML-interface for retrieving and 
+  modifying the theorems.
   Furthermore, the theorems are made available on the user-level under the name 
   @{text foo}. For example you can declare three lemmas to be a member of the 
   theorem list @{text foo} by:
diff -r 76b1b679e845 -r 272ba2cceeb2 ProgTutorial/General.thy
--- a/ProgTutorial/General.thy	Sat Nov 07 01:44:11 2009 +0100
+++ b/ProgTutorial/General.thy	Sat Nov 07 10:08:09 2009 +0100
@@ -185,7 +185,7 @@
   "@{typ \"bool\"}"
   "bool"}
 
-  the pretty printed version of @{text "bool"}. However, in PolyML it is 
+  that is the pretty printed version of @{text "bool"}. However, in PolyML it is 
   easy to install your own pretty printer. With the function below we 
   mimic the behaviour of the usual pretty printer for 
   datatypes.\footnote{Thanks to David Matthews for providing this
@@ -214,7 +214,7 @@
 ML{*PolyML.addPrettyPrinter typ_raw_pretty_printer*}
 
 text {*
-  Now the type bool is printed out as expected.
+  Now the type bool is printed out in full detail.
 
   @{ML_response [display,gray]
   "@{typ \"bool\"}"
@@ -228,7 +228,7 @@
 
   we can see the full name of the type is actually @{text "List.list"}, indicating
   that it is defined in the theory @{text "List"}. However, one has to be 
-  careful with finding out the right name of a type, because even if
+  careful with names of types, because even if
   @{text "fun"}, @{text "bool"} and @{text "nat"} are defined in the 
   theories @{text "HOL"} and @{text "Nat"}, respectively, they are 
   still represented by their simple name.
@@ -674,6 +674,27 @@
   \end{exercise}
 *}
 
+section {* Matching and Unification (TBD) *}
+
+text {* 
+  Using the antiquotation from Section~\ref{sec:antiquote}.
+*}
+
+ML{*val (env, _) = 
+  Sign.typ_unify @{theory} (@{typ_pat "?'b * ?'c"}, @{typ_pat "?'a * ?'b"}) (Vartab.empty, 0) *}
+
+ML{*Vartab.dest env  *}
+
+ML{*Envir.norm_type env @{typ_pat "?'a"}*}
+
+ML{*val env = 
+  Sign.typ_match @{theory} (@{typ_pat "?'b * ?'c"}, @{typ_pat "?'a * ?'b"}) Vartab.empty *}
+
+ML{*Envir.subst_type env  @{typ_pat "?'a"} *}
+
+text {*
+  Note the difference. Norm for unify; Subst for match.
+*}
 
 section {* Type-Checking\label{sec:typechecking} *}
 
diff -r 76b1b679e845 -r 272ba2cceeb2 progtutorial.pdf
Binary file progtutorial.pdf has changed