1(* Author: Andreas Lochbihler, Digital Asset *)
2
3theory Code_Lazy_Demo imports
4  "HOL-Library.Code_Lazy"
5  "HOL-Library.Debug"
6  "HOL-Library.RBT_Impl"
7begin
8
9text \<open>This theory demonstrates the use of the \<^theory>\<open>HOL-Library.Code_Lazy\<close> theory.\<close>
10
11section \<open>Streams\<close>
12
13text \<open>Lazy evaluation for streams\<close>
14
15codatatype 'a stream = 
16  SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
17
18primcorec up :: "nat \<Rightarrow> nat stream" where
19  "up n = n ## up (n + 1)"
20
21primrec stake :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a list" where
22  "stake 0 xs = []"
23| "stake (Suc n) xs = shd xs # stake n (stl xs)"
24
25code_thms up stake \<comment> \<open>The original code equations\<close>
26
27code_lazy_type stream
28
29code_thms up stake \<comment> \<open>The lazified code equations\<close>
30
31value "stake 5 (up 3)"
32
33
34section \<open>Finite lazy lists\<close>
35
36text \<open>Lazy types need not be infinite. We can also have lazy types that are finite.\<close>
37
38datatype 'a llist
39  = LNil ("\<^bold>\<lbrakk>\<^bold>\<rbrakk>") 
40  | LCons (lhd: 'a) (ltl: "'a llist") (infixr "###" 65)
41
42syntax "_llist" :: "args => 'a list"    ("\<^bold>\<lbrakk>(_)\<^bold>\<rbrakk>")
43translations
44  "\<^bold>\<lbrakk>x, xs\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>xs\<^bold>\<rbrakk>"
45  "\<^bold>\<lbrakk>x\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>\<^bold>\<rbrakk>"
46
47fun lnth :: "nat \<Rightarrow> 'a llist \<Rightarrow> 'a" where
48  "lnth 0 (x ### xs) = x"
49| "lnth (Suc n) (x ### xs) = lnth n xs"
50
51definition llist :: "nat llist" where
52  "llist = \<^bold>\<lbrakk>1, 2, 3, hd [], 4\<^bold>\<rbrakk>"
53
54code_lazy_type llist
55
56value [code] "llist"
57value [code] "lnth 2 llist"
58value [code] "let x = lnth 2 llist in (x, llist)"
59
60fun lfilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
61  "lfilter P \<^bold>\<lbrakk>\<^bold>\<rbrakk> = \<^bold>\<lbrakk>\<^bold>\<rbrakk>"
62| "lfilter P (x ### xs) = 
63   (if P x then x ### lfilter P xs else lfilter P xs)"
64
65export_code lfilter in SML file_prefix lfilter
66
67value [code] "lfilter odd llist"
68
69value [code] "lhd (lfilter odd llist)"
70
71
72section \<open>Iterator for red-black trees\<close>
73
74text \<open>Thanks to laziness, we do not need to program a complicated iterator for a tree. 
75  A conversion function to lazy lists is enough.\<close>
76
77primrec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist"
78  (infixr "@@" 65) where
79  "\<^bold>\<lbrakk>\<^bold>\<rbrakk> @@ ys = ys"
80| "(x ### xs) @@ ys = x ### (xs @@ ys)"
81
82primrec rbt_iterator :: "('a, 'b) rbt \<Rightarrow> ('a \<times> 'b) llist" where
83  "rbt_iterator rbt.Empty = \<^bold>\<lbrakk>\<^bold>\<rbrakk>"
84| "rbt_iterator (Branch _ l k v r) = 
85   (let _ = Debug.flush (STR ''tick'') in 
86   rbt_iterator l @@ (k, v) ### rbt_iterator r)"
87
88definition tree :: "(nat, unit) rbt"
89  where "tree = fold (\<lambda>k. rbt_insert k ()) [0..<100] rbt.Empty"
90
91definition find_min :: "('a :: linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) option" where
92  "find_min rbt = 
93  (case rbt_iterator rbt of \<^bold>\<lbrakk>\<^bold>\<rbrakk> \<Rightarrow> None 
94   | kv ### _ \<Rightarrow> Some kv)"
95
96value "find_min tree" \<comment> \<open>Observe that \<^const>\<open>rbt_iterator\<close> is evaluated only for going down 
97  to the first leaf, not for the whole tree (as seen by the ticks).\<close>
98
99text \<open>With strict lists, the whole tree is converted into a list.\<close>
100
101deactivate_lazy_type llist
102value "find_min tree"
103activate_lazy_type llist
104
105
106
107section \<open>Branching datatypes\<close>
108
109datatype tree
110  = L              ("\<spadesuit>") 
111  | Node tree tree (infix "\<triangle>" 900)
112
113notation (output) Node ("\<triangle>(//\<^bold>l: _//\<^bold>r: _)")
114
115code_lazy_type tree
116
117fun mk_tree :: "nat \<Rightarrow> tree" where mk_tree_0:
118  "mk_tree 0 = \<spadesuit>"
119| "mk_tree (Suc n) = (let t = mk_tree n in t \<triangle> t)"
120
121declare mk_tree.simps [code]
122
123code_thms mk_tree
124
125function subtree :: "bool list \<Rightarrow> tree \<Rightarrow> tree" where
126  "subtree [] t = t"
127| "subtree (True # p) (l \<triangle> r) = subtree p l"
128| "subtree (False # p) (l \<triangle> r) = subtree p r"
129| "subtree _ \<spadesuit> = \<spadesuit>"
130  by pat_completeness auto
131termination by lexicographic_order
132
133value [code] "mk_tree 10"
134value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
135  \<comment> \<open>Since \<^const>\<open>mk_tree\<close> shares the two subtrees of a node thanks to the let binding,
136      digging into one subtree spreads to the whole tree.\<close>
137value [code] "let t = mk_tree 3; _ = subtree [True, True, False, False] t in t"
138
139lemma mk_tree_Suc_debug [code]: \<comment> \<open>Make the evaluation visible with tracing.\<close>
140  "mk_tree (Suc n) = 
141  (let _ = Debug.flush (STR ''tick''); t = mk_tree n in t \<triangle> t)"
142  by simp
143
144value [code] "mk_tree 10"
145  \<comment> \<open>The recursive call to \<^const>\<open>mk_tree\<close> is not guarded by a lazy constructor,
146      so all the suspensions are built up immediately.\<close>
147
148lemma mk_tree_Suc [code]: "mk_tree (Suc n) = mk_tree n \<triangle> mk_tree n"
149  \<comment> \<open>In this code equation, there is no sharing and the recursive calls are guarded by a constructor.\<close>
150  by(simp add: Let_def)
151
152value [code] "mk_tree 10"
153value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
154
155lemma mk_tree_Suc_debug' [code]: 
156  "mk_tree (Suc n) = (let _ = Debug.flush (STR ''tick'') in mk_tree n \<triangle> mk_tree n)"
157  by(simp add: Let_def)
158
159value [code] "mk_tree 10" \<comment> \<open>Only one tick thanks to the guarding constructor\<close>
160value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
161value [code] "let t = mk_tree 3; _ = subtree [True, True, False, False] t in t"
162
163
164section \<open>Pattern matching elimination\<close>
165
166text \<open>The pattern matching elimination handles deep pattern matches and overlapping equations
167 and only eliminates necessary pattern matches.\<close>
168
169function crazy :: "nat llist llist \<Rightarrow> tree \<Rightarrow> bool \<Rightarrow> unit" where
170  "crazy (\<^bold>\<lbrakk>0\<^bold>\<rbrakk> ### xs) _ _    = Debug.flush (1 :: integer)"
171| "crazy xs          \<spadesuit> True = Debug.flush (2 :: integer)"
172| "crazy xs          t  b   = Debug.flush (3 :: integer)"
173  by pat_completeness auto
174termination by lexicographic_order
175
176code_thms crazy
177
178end