169 in |
169 in |
170 map #name (Net.entries rules) |
170 map #name (Net.entries rules) |
171 end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"} |
171 end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"} |
172 |
172 |
173 The code about simpsets extracts the theorem names stored in the |
173 The code about simpsets extracts the theorem names stored in the |
174 current simpset. We get hold of the current simpset with the antiquotation |
174 current simpset. You can get hold of the current simpset with the antiquotation |
175 @{text "@{simpset}"}. The function @{ML rep_ss in MetaSimplifier} returns a record |
175 @{text "@{simpset}"}. The function @{ML rep_ss in MetaSimplifier} returns a record |
176 containing all information about the simpset. The rules of a simpset are |
176 containing all information about the simpset. The rules of a simpset are |
177 stored in a \emph{discrimination net} (a data structure for fast |
177 stored in a \emph{discrimination net} (a data structure for fast |
178 indexing). From this net we can extract the entries using the function @{ML |
178 indexing). From this net you can extract the entries using the function @{ML |
179 Net.entries}. |
179 Net.entries}. |
180 |
180 |
181 |
181 |
182 \begin{readmore} |
182 \begin{readmore} |
183 The infrastructure for simpsets is implemented in @{ML_file "Pure/meta_simplifier.ML"} |
183 The infrastructure for simpsets is implemented in @{ML_file "Pure/meta_simplifier.ML"} |
256 Consider for example the pairs |
256 Consider for example the pairs |
257 |
257 |
258 @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>), |
258 @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>), |
259 Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"} |
259 Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"} |
260 |
260 |
261 where an coercion is inserted in the second component and |
261 where a coercion is inserted in the second component and |
262 |
262 |
263 @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" |
263 @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" |
264 "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"} |
264 "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"} |
265 |
265 |
266 where it is not (since it is already constructed by a meta-implication). |
266 where it is not (since it is already constructed by a meta-implication). |
343 |
343 |
344 @{ML_response_fake [display,gray] "@{const_name \"Nil\"}" "List.list.Nil"} |
344 @{ML_response_fake [display,gray] "@{const_name \"Nil\"}" "List.list.Nil"} |
345 |
345 |
346 (FIXME: Is it useful to explain @{text "@{const_syntax}"}?) |
346 (FIXME: Is it useful to explain @{text "@{const_syntax}"}?) |
347 |
347 |
348 Although to some extend types of terms can be inferred, there are many |
348 Although types of terms can often be inferred, there are many |
349 situations where you need to construct types manually, especially |
349 situations where you need to construct types manually, especially |
350 when defining constants. For example the function returning a function |
350 when defining constants. For example the function returning a function |
351 type is as follows: |
351 type is as follows: |
352 |
352 |
353 *} |
353 *} |
385 number representing their sum. |
385 number representing their sum. |
386 \end{exercise} |
386 \end{exercise} |
387 |
387 |
388 A handy function for manipulating terms is @{ML map_types}: it takes a |
388 A handy function for manipulating terms is @{ML map_types}: it takes a |
389 function and applies it to every type in the term. You can, for example, |
389 function and applies it to every type in the term. You can, for example, |
390 change every @{typ nat} into an @{typ int} using the function |
390 change every @{typ nat} in a term into an @{typ int} using the function |
391 *} |
391 *} |
392 |
392 |
393 ML{*fun nat_to_int t = |
393 ML{*fun nat_to_int t = |
394 (case t of |
394 (case t of |
395 @{typ nat} => @{typ int} |
395 @{typ nat} => @{typ int} |
409 |
409 |
410 section {* Type-Checking *} |
410 section {* Type-Checking *} |
411 |
411 |
412 text {* |
412 text {* |
413 |
413 |
414 You can freely construct and manipulate terms, since they are just |
414 You can freely construct and manipulate @{ML_type "term"}s, since they are just |
415 arbitrary unchecked trees. However, you eventually want to see if a |
415 arbitrary unchecked trees. However, you eventually want to see if a |
416 term is well-formed, or type-checks, relative to a theory. |
416 term is well-formed, or type-checks, relative to a theory. |
417 Type-checking is done via the function @{ML cterm_of}, which converts |
417 Type-checking is done via the function @{ML cterm_of}, which converts |
418 a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} term. |
418 a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} term. |
419 Unlike @{ML_type term}s, which are just trees, @{ML_type |
419 Unlike @{ML_type term}s, which are just trees, @{ML_type |
693 #> (fn x => x + 3)*} |
695 #> (fn x => x + 3)*} |
694 |
696 |
695 text {* |
697 text {* |
696 which is the function composed of first the increment-by-one function and then |
698 which is the function composed of first the increment-by-one function and then |
697 increment-by-two, followed by increment-by-three. Again, the reverse function |
699 increment-by-two, followed by increment-by-three. Again, the reverse function |
698 composition allows one to read the code top-down. |
700 composition allows you to read the code top-down. |
699 |
701 |
700 The remaining combinators described in this section add convenience for the |
702 The remaining combinators described in this section add convenience for the |
701 ``waterfall method'' of writing functions. The combinator @{ML tap} allows |
703 ``waterfall method'' of writing functions. The combinator @{ML tap} allows |
702 one to get hold of an intermediate result (to do some side-calculations for |
704 you to get hold of an intermediate result (to do some side-calculations for |
703 instance). The function |
705 instance). The function |
704 |
706 |
705 *} |
707 *} |
706 |
708 |
707 ML %linenumbers{*fun inc_by_three x = |
709 ML %linenumbers{*fun inc_by_three x = |
708 x |> (fn x => x + 1) |
710 x |> (fn x => x + 1) |
709 |> tap (fn x => tracing (makestring x)) |
711 |> tap (fn x => tracing (makestring x)) |
710 |> (fn x => x + 2)*} |
712 |> (fn x => x + 2)*} |
711 |
713 |
712 text {* increments the argument first by one and then by two. In the middle (Line 3), |
714 text {* |
713 however, it uses @{ML tap} for printing the ``plus-one'' intermediate |
715 increments the argument first by @{text "1"} and then by @{text "2"}. In the |
714 result inside the tracing buffer. The function @{ML tap} can only |
716 middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one'' |
715 be used for side-calculations, because any value that is computed cannot |
717 intermediate result inside the tracing buffer. The function @{ML tap} can |
716 be merged back into the ``main waterfall''. To do this, you can use the next |
718 only be used for side-calculations, because any value that is computed |
717 combinator. |
719 cannot be merged back into the ``main waterfall''. To do this, you can use |
|
720 the next combinator. |
718 |
721 |
719 The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value |
722 The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value |
720 and returns the result together with the value (as a pair). For example |
723 and returns the result together with the value (as a pair). For example |
721 the function |
724 the function |
722 *} |
725 *} |
750 *} |
753 *} |
751 |
754 |
752 ML{*fun (x, y) |-> f = f x y*} |
755 ML{*fun (x, y) |-> f = f x y*} |
753 |
756 |
754 text {* and can be used to write the following roundabout version |
757 text {* and can be used to write the following roundabout version |
755 of the @{text double} function |
758 of the @{text double} function: |
756 *} |
759 *} |
757 |
760 |
758 ML{*fun double x = |
761 ML{*fun double x = |
759 x |> (fn x => (x, x)) |
762 x |> (fn x => (x, x)) |
760 |-> (fn x => fn y => x + y)*} |
763 |-> (fn x => fn y => x + y)*} |
762 text {* |
765 text {* |
763 Recall that @{ML "|>"} is the reverse function applications. Recall also that the related |
766 Recall that @{ML "|>"} is the reverse function applications. Recall also that the related |
764 reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"}, |
767 reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"}, |
765 @{ML "|>>"} and @{ML "||>"} described above have related combinators for function |
768 @{ML "|>>"} and @{ML "||>"} described above have related combinators for function |
766 composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"}, |
769 composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"}, |
767 for example, the function @{text double} can also be written as |
770 for example, the function @{text double} can also be written as: |
768 *} |
771 *} |
769 |
772 |
770 ML{*val double = |
773 ML{*val double = |
771 (fn x => (x, x)) |
774 (fn x => (x, x)) |
772 #-> (fn x => fn y => x + y)*} |
775 #-> (fn x => fn y => x + y)*} |