21 set of type constructors lazily, even in target languages with eager evaluation. |
21 set of type constructors lazily, even in target languages with eager evaluation. |
22 The lazy type must be algebraic, i.e., values must be built from constructors and a |
22 The lazy type must be algebraic, i.e., values must be built from constructors and a |
23 corresponding case operator decomposes them. Every datatype and codatatype is algebraic |
23 corresponding case operator decomposes them. Every datatype and codatatype is algebraic |
24 and thus eligible for lazification. |
24 and thus eligible for lazification. |
25 \<close> |
25 \<close> |
26 |
|
27 subsection \<open>Eliminating pattern matches\<close> |
|
28 |
|
29 definition missing_pattern_match :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a" where |
|
30 [code del]: "missing_pattern_match m f = f ()" |
|
31 |
|
32 lemma missing_pattern_match_cong [cong]: |
|
33 "m = m' \<Longrightarrow> missing_pattern_match m f = missing_pattern_match m' f" |
|
34 by(rule arg_cong) |
|
35 |
|
36 lemma missing_pattern_match_code [code_unfold]: |
|
37 "missing_pattern_match = Code.abort" |
|
38 unfolding missing_pattern_match_def Code.abort_def .. |
|
39 |
|
40 ML_file "case_converter.ML" |
|
41 |
|
42 |
26 |
43 subsection \<open>The type \<open>lazy\<close>\<close> |
27 subsection \<open>The type \<open>lazy\<close>\<close> |
44 |
28 |
45 typedef 'a lazy = "UNIV :: 'a set" .. |
29 typedef 'a lazy = "UNIV :: 'a set" .. |
46 setup_lifting type_definition_lazy |
30 setup_lifting type_definition_lazy |