equal
deleted
inserted
replaced
183 |
183 |
184 @{ML_response [display, gray] |
184 @{ML_response [display, gray] |
185 "@{typ \"bool\"}" |
185 "@{typ \"bool\"}" |
186 "bool"} |
186 "bool"} |
187 |
187 |
188 the pretty printed version of @{text "bool"}. However, in PolyML it is |
188 that is the pretty printed version of @{text "bool"}. However, in PolyML it is |
189 easy to install your own pretty printer. With the function below we |
189 easy to install your own pretty printer. With the function below we |
190 mimic the behaviour of the usual pretty printer for |
190 mimic the behaviour of the usual pretty printer for |
191 datatypes.\footnote{Thanks to David Matthews for providing this |
191 datatypes.\footnote{Thanks to David Matthews for providing this |
192 code.} |
192 code.} |
193 *} |
193 *} |
212 *} |
212 *} |
213 |
213 |
214 ML{*PolyML.addPrettyPrinter typ_raw_pretty_printer*} |
214 ML{*PolyML.addPrettyPrinter typ_raw_pretty_printer*} |
215 |
215 |
216 text {* |
216 text {* |
217 Now the type bool is printed out as expected. |
217 Now the type bool is printed out in full detail. |
218 |
218 |
219 @{ML_response [display,gray] |
219 @{ML_response [display,gray] |
220 "@{typ \"bool\"}" |
220 "@{typ \"bool\"}" |
221 "Type (\"bool\", [])"} |
221 "Type (\"bool\", [])"} |
222 |
222 |
226 "@{typ \"'a list\"}" |
226 "@{typ \"'a list\"}" |
227 "Type (\"List.list\", [TFree (\"'a\", [\"HOL.type\"])])"} |
227 "Type (\"List.list\", [TFree (\"'a\", [\"HOL.type\"])])"} |
228 |
228 |
229 we can see the full name of the type is actually @{text "List.list"}, indicating |
229 we can see the full name of the type is actually @{text "List.list"}, indicating |
230 that it is defined in the theory @{text "List"}. However, one has to be |
230 that it is defined in the theory @{text "List"}. However, one has to be |
231 careful with finding out the right name of a type, because even if |
231 careful with names of types, because even if |
232 @{text "fun"}, @{text "bool"} and @{text "nat"} are defined in the |
232 @{text "fun"}, @{text "bool"} and @{text "nat"} are defined in the |
233 theories @{text "HOL"} and @{text "Nat"}, respectively, they are |
233 theories @{text "HOL"} and @{text "Nat"}, respectively, they are |
234 still represented by their simple name. |
234 still represented by their simple name. |
235 |
235 |
236 @{ML_response [display,gray] |
236 @{ML_response [display,gray] |
672 for constructing the terms for the logical connectives.\footnote{Thanks to Roy |
672 for constructing the terms for the logical connectives.\footnote{Thanks to Roy |
673 Dyckhoff for suggesting this exercise and working out the details.} |
673 Dyckhoff for suggesting this exercise and working out the details.} |
674 \end{exercise} |
674 \end{exercise} |
675 *} |
675 *} |
676 |
676 |
|
677 section {* Matching and Unification (TBD) *} |
|
678 |
|
679 text {* |
|
680 Using the antiquotation from Section~\ref{sec:antiquote}. |
|
681 *} |
|
682 |
|
683 ML{*val (env, _) = |
|
684 Sign.typ_unify @{theory} (@{typ_pat "?'b * ?'c"}, @{typ_pat "?'a * ?'b"}) (Vartab.empty, 0) *} |
|
685 |
|
686 ML{*Vartab.dest env *} |
|
687 |
|
688 ML{*Envir.norm_type env @{typ_pat "?'a"}*} |
|
689 |
|
690 ML{*val env = |
|
691 Sign.typ_match @{theory} (@{typ_pat "?'b * ?'c"}, @{typ_pat "?'a * ?'b"}) Vartab.empty *} |
|
692 |
|
693 ML{*Envir.subst_type env @{typ_pat "?'a"} *} |
|
694 |
|
695 text {* |
|
696 Note the difference. Norm for unify; Subst for match. |
|
697 *} |
677 |
698 |
678 section {* Type-Checking\label{sec:typechecking} *} |
699 section {* Type-Checking\label{sec:typechecking} *} |
679 |
700 |
680 text {* |
701 text {* |
681 Remember Isabelle follows the Church-style typing for terms, i.e., a term contains |
702 Remember Isabelle follows the Church-style typing for terms, i.e., a term contains |