equal
deleted
inserted
replaced
11 section \<open>Streams\<close> |
11 section \<open>Streams\<close> |
12 |
12 |
13 text \<open>Lazy evaluation for streams\<close> |
13 text \<open>Lazy evaluation for streams\<close> |
14 |
14 |
15 codatatype 'a stream = |
15 codatatype 'a stream = |
16 SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65) |
16 SCons (shd: 'a) (stl: "'a stream") (infixr \<open>##\<close> 65) |
17 |
17 |
18 primcorec up :: "nat \<Rightarrow> nat stream" where |
18 primcorec up :: "nat \<Rightarrow> nat stream" where |
19 "up n = n ## up (n + 1)" |
19 "up n = n ## up (n + 1)" |
20 |
20 |
21 primrec stake :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a list" where |
21 primrec stake :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a list" where |
34 section \<open>Finite lazy lists\<close> |
34 section \<open>Finite lazy lists\<close> |
35 |
35 |
36 text \<open>Lazy types need not be infinite. We can also have lazy types that are finite.\<close> |
36 text \<open>Lazy types need not be infinite. We can also have lazy types that are finite.\<close> |
37 |
37 |
38 datatype 'a llist |
38 datatype 'a llist |
39 = LNil ("\<^bold>\<lbrakk>\<^bold>\<rbrakk>") |
39 = LNil (\<open>\<^bold>\<lbrakk>\<^bold>\<rbrakk>\<close>) |
40 | LCons (lhd: 'a) (ltl: "'a llist") (infixr "###" 65) |
40 | LCons (lhd: 'a) (ltl: "'a llist") (infixr \<open>###\<close> 65) |
41 |
41 |
42 nonterminal llist_args |
42 nonterminal llist_args |
43 syntax |
43 syntax |
44 "" :: "'a \<Rightarrow> llist_args" ("_") |
44 "" :: "'a \<Rightarrow> llist_args" (\<open>_\<close>) |
45 "_llist_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args" ("_,/ _") |
45 "_llist_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args" (\<open>_,/ _\<close>) |
46 "_llist" :: "llist_args => 'a list" ("\<^bold>\<lbrakk>(_)\<^bold>\<rbrakk>") |
46 "_llist" :: "llist_args => 'a list" (\<open>\<^bold>\<lbrakk>(_)\<^bold>\<rbrakk>\<close>) |
47 syntax_consts |
47 syntax_consts |
48 "_llist_args" "_llist" == LCons |
48 "_llist_args" "_llist" == LCons |
49 translations |
49 translations |
50 "\<^bold>\<lbrakk>x, xs\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>xs\<^bold>\<rbrakk>" |
50 "\<^bold>\<lbrakk>x, xs\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>xs\<^bold>\<rbrakk>" |
51 "\<^bold>\<lbrakk>x\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>\<^bold>\<rbrakk>" |
51 "\<^bold>\<lbrakk>x\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>\<^bold>\<rbrakk>" |
79 |
79 |
80 text \<open>Thanks to laziness, we do not need to program a complicated iterator for a tree. |
80 text \<open>Thanks to laziness, we do not need to program a complicated iterator for a tree. |
81 A conversion function to lazy lists is enough.\<close> |
81 A conversion function to lazy lists is enough.\<close> |
82 |
82 |
83 primrec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" |
83 primrec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" |
84 (infixr "@@" 65) where |
84 (infixr \<open>@@\<close> 65) where |
85 "\<^bold>\<lbrakk>\<^bold>\<rbrakk> @@ ys = ys" |
85 "\<^bold>\<lbrakk>\<^bold>\<rbrakk> @@ ys = ys" |
86 | "(x ### xs) @@ ys = x ### (xs @@ ys)" |
86 | "(x ### xs) @@ ys = x ### (xs @@ ys)" |
87 |
87 |
88 primrec rbt_iterator :: "('a, 'b) rbt \<Rightarrow> ('a \<times> 'b) llist" where |
88 primrec rbt_iterator :: "('a, 'b) rbt \<Rightarrow> ('a \<times> 'b) llist" where |
89 "rbt_iterator rbt.Empty = \<^bold>\<lbrakk>\<^bold>\<rbrakk>" |
89 "rbt_iterator rbt.Empty = \<^bold>\<lbrakk>\<^bold>\<rbrakk>" |
111 |
111 |
112 |
112 |
113 section \<open>Branching datatypes\<close> |
113 section \<open>Branching datatypes\<close> |
114 |
114 |
115 datatype tree |
115 datatype tree |
116 = L ("\<spadesuit>") |
116 = L (\<open>\<spadesuit>\<close>) |
117 | Node tree tree (infix "\<triangle>" 900) |
117 | Node tree tree (infix \<open>\<triangle>\<close> 900) |
118 |
118 |
119 notation (output) Node ("\<triangle>(//\<^bold>l: _//\<^bold>r: _)") |
119 notation (output) Node (\<open>\<triangle>(//\<^bold>l: _//\<^bold>r: _)\<close>) |
120 |
120 |
121 code_lazy_type tree |
121 code_lazy_type tree |
122 |
122 |
123 fun mk_tree :: "nat \<Rightarrow> tree" where mk_tree_0: |
123 fun mk_tree :: "nat \<Rightarrow> tree" where mk_tree_0: |
124 "mk_tree 0 = \<spadesuit>" |
124 "mk_tree 0 = \<spadesuit>" |