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