more examples for Code_Lazy
authorAndreas Lochbihler
Sun Jul 15 23:44:38 2018 +0200 (16 months ago)
changeset 68639357fca99a65a
parent 68629 f36858fdf768
child 68640 f15daa73ee32
more examples for Code_Lazy
NEWS
src/HOL/ROOT
src/HOL/ex/Code_Lazy_Demo.thy
     1.1 --- a/NEWS	Sun Jul 15 01:14:04 2018 +0100
     1.2 +++ b/NEWS	Sun Jul 15 23:44:38 2018 +0200
     1.3 @@ -376,8 +376,9 @@
     1.4  
     1.5  * Theory HOL-Library.Code_Lazy provides a new preprocessor for the code
     1.6  generator to generate code for algebraic types with lazy evaluation
     1.7 -semantics even in call-by-value target languages. See theory
     1.8 -HOL-Codegenerator_Test.Code_Lazy_Test for some examples.
     1.9 +semantics even in call-by-value target languages. See the theories
    1.10 +HOL-ex.Code_Lazy_Demo and HOL-Codegenerator_Test.Code_Lazy_Test for
    1.11 +some examples.
    1.12  
    1.13  * Theory HOL-Library.Landau_Symbols has been moved here from AFP.
    1.14  
     2.1 --- a/src/HOL/ROOT	Sun Jul 15 01:14:04 2018 +0100
     2.2 +++ b/src/HOL/ROOT	Sun Jul 15 23:44:38 2018 +0200
     2.3 @@ -534,6 +534,7 @@
     2.4      Chinese
     2.5      Classical
     2.6      Code_Binary_Nat_examples
     2.7 +    Code_Lazy_Demo
     2.8      Code_Timing
     2.9      Coercion_Examples
    2.10      Coherent
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/Code_Lazy_Demo.thy	Sun Jul 15 23:44:38 2018 +0200
     3.3 @@ -0,0 +1,178 @@
     3.4 +(* Author: Andreas Lochbihler, Digital Asset *)
     3.5 +
     3.6 +theory Code_Lazy_Demo imports
     3.7 +  "HOL-Library.Code_Lazy"
     3.8 +  "HOL-Library.Debug"
     3.9 +  "HOL-Library.RBT_Impl"
    3.10 +begin
    3.11 +
    3.12 +text \<open>This theory demonstrates the use of the @{theory "HOL-Library.Code_Lazy"} theory.\<close>
    3.13 +
    3.14 +section \<open>Streams\<close>
    3.15 +
    3.16 +text \<open>Lazy evaluation for streams\<close>
    3.17 +
    3.18 +codatatype 'a stream = 
    3.19 +  SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
    3.20 +
    3.21 +primcorec up :: "nat \<Rightarrow> nat stream" where
    3.22 +  "up n = n ## up (n + 1)"
    3.23 +
    3.24 +primrec stake :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a list" where
    3.25 +  "stake 0 xs = []"
    3.26 +| "stake (Suc n) xs = shd xs # stake n (stl xs)"
    3.27 +
    3.28 +code_thms up stake \<comment> \<open>The original code equations\<close>
    3.29 +
    3.30 +code_lazy_type stream
    3.31 +
    3.32 +code_thms up stake \<comment> \<open>The lazified code equations\<close>
    3.33 +
    3.34 +value "stake 5 (up 3)"
    3.35 +
    3.36 +
    3.37 +section \<open>Finite lazy lists\<close>
    3.38 +
    3.39 +text \<open>Lazy types need not be infinite. We can also have lazy types that are finite.\<close>
    3.40 +
    3.41 +datatype 'a llist
    3.42 +  = LNil ("\<^bold>\<lbrakk>\<^bold>\<rbrakk>") 
    3.43 +  | LCons (lhd: 'a) (ltl: "'a llist") (infixr "###" 65)
    3.44 +
    3.45 +syntax "_llist" :: "args => 'a list"    ("\<^bold>\<lbrakk>(_)\<^bold>\<rbrakk>")
    3.46 +translations
    3.47 +  "\<^bold>\<lbrakk>x, xs\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>xs\<^bold>\<rbrakk>"
    3.48 +  "\<^bold>\<lbrakk>x\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>\<^bold>\<rbrakk>"
    3.49 +
    3.50 +fun lnth :: "nat \<Rightarrow> 'a llist \<Rightarrow> 'a" where
    3.51 +  "lnth 0 (x ### xs) = x"
    3.52 +| "lnth (Suc n) (x ### xs) = lnth n xs"
    3.53 +
    3.54 +definition llist :: "nat llist" where
    3.55 +  "llist = \<^bold>\<lbrakk>1, 2, 3, hd [], 4\<^bold>\<rbrakk>"
    3.56 +
    3.57 +code_lazy_type llist
    3.58 +
    3.59 +value [code] "llist"
    3.60 +value [code] "lnth 2 llist"
    3.61 +value [code] "let x = lnth 2 llist in (x, llist)"
    3.62 +
    3.63 +fun lfilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
    3.64 +  "lfilter P \<^bold>\<lbrakk>\<^bold>\<rbrakk> = \<^bold>\<lbrakk>\<^bold>\<rbrakk>"
    3.65 +| "lfilter P (x ### xs) = 
    3.66 +   (if P x then x ### lfilter P xs else lfilter P xs)"
    3.67 +
    3.68 +export_code lfilter in SML
    3.69 +
    3.70 +value [code] "lfilter odd llist"
    3.71 +
    3.72 +value [code] "lhd (lfilter odd llist)"
    3.73 +
    3.74 +
    3.75 +section \<open>Iterator for red-black trees\<close>
    3.76 +
    3.77 +text \<open>Thanks to laziness, we do not need to program a complicated iterator for a tree. 
    3.78 +  A conversion function to lazy lists is enough.\<close>
    3.79 +
    3.80 +primrec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist"
    3.81 +  (infixr "@@" 65) where
    3.82 +  "\<^bold>\<lbrakk>\<^bold>\<rbrakk> @@ ys = ys"
    3.83 +| "(x ### xs) @@ ys = x ### (xs @@ ys)"
    3.84 +
    3.85 +primrec rbt_iterator :: "('a, 'b) rbt \<Rightarrow> ('a \<times> 'b) llist" where
    3.86 +  "rbt_iterator rbt.Empty = \<^bold>\<lbrakk>\<^bold>\<rbrakk>"
    3.87 +| "rbt_iterator (Branch _ l k v r) = 
    3.88 +   (let _ = Debug.flush (STR ''tick'') in 
    3.89 +   rbt_iterator l @@ (k, v) ### rbt_iterator r)"
    3.90 +
    3.91 +definition tree :: "(nat, unit) rbt"
    3.92 +  where "tree = fold (\<lambda>k. rbt_insert k ()) [0..<100] rbt.Empty"
    3.93 +
    3.94 +definition find_min :: "('a :: linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) option" where
    3.95 +  "find_min rbt = 
    3.96 +  (case rbt_iterator rbt of \<^bold>\<lbrakk>\<^bold>\<rbrakk> \<Rightarrow> None 
    3.97 +   | kv ### _ \<Rightarrow> Some kv)"
    3.98 +
    3.99 +value "find_min tree" \<comment> \<open>Observe that @{const rbt_iterator} is evaluated only for going down 
   3.100 +  to the first leaf, not for the whole tree (as seen by the ticks).\<close>
   3.101 +
   3.102 +text \<open>With strict lists, the whole tree is converted into a list.\<close>
   3.103 +
   3.104 +deactivate_lazy_type llist
   3.105 +value "find_min tree"
   3.106 +activate_lazy_type llist
   3.107 +
   3.108 +
   3.109 +
   3.110 +section \<open>Branching datatypes\<close>
   3.111 +
   3.112 +datatype tree
   3.113 +  = L              ("\<spadesuit>") 
   3.114 +  | Node tree tree (infix "\<triangle>" 900)
   3.115 +
   3.116 +notation (output) Node ("\<triangle>(//\<^bold>l: _//\<^bold>r: _)")
   3.117 +
   3.118 +code_lazy_type tree
   3.119 +
   3.120 +fun mk_tree :: "nat \<Rightarrow> tree" where mk_tree_0:
   3.121 +  "mk_tree 0 = \<spadesuit>"
   3.122 +| "mk_tree (Suc n) = (let t = mk_tree n in t \<triangle> t)"
   3.123 +
   3.124 +declare mk_tree.simps [code]
   3.125 +
   3.126 +code_thms mk_tree
   3.127 +
   3.128 +function subtree :: "bool list \<Rightarrow> tree \<Rightarrow> tree" where
   3.129 +  "subtree [] t = t"
   3.130 +| "subtree (True # p) (l \<triangle> r) = subtree p l"
   3.131 +| "subtree (False # p) (l \<triangle> r) = subtree p r"
   3.132 +| "subtree _ \<spadesuit> = \<spadesuit>"
   3.133 +  by pat_completeness auto
   3.134 +termination by lexicographic_order
   3.135 +
   3.136 +value [code] "mk_tree 10"
   3.137 +value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
   3.138 +  \<comment> \<open>Since @{const mk_tree} shares the two subtrees of a node thanks to the let binding,
   3.139 +      digging into one subtree spreads to the whole tree.\<close>
   3.140 +value [code] "let t = mk_tree 3; _ = subtree [True, True, False, False] t in t"
   3.141 +
   3.142 +lemma mk_tree_Suc_debug [code]: \<comment> \<open>Make the evaluation visible with tracing.\<close>
   3.143 +  "mk_tree (Suc n) = 
   3.144 +  (let _ = Debug.flush (STR ''tick''); t = mk_tree n in t \<triangle> t)"
   3.145 +  by simp
   3.146 +
   3.147 +value [code] "mk_tree 10"
   3.148 +  \<comment> \<open>The recursive call to @{const mk_tree} is not guarded by a lazy constructor,
   3.149 +      so all the suspensions are built up immediately.\<close>
   3.150 +
   3.151 +lemma mk_tree_Suc [code]: "mk_tree (Suc n) = mk_tree n \<triangle> mk_tree n"
   3.152 +  \<comment> \<open>In this code equation, there is no sharing and the recursive calls are guarded by a constructor.\<close>
   3.153 +  by(simp add: Let_def)
   3.154 +
   3.155 +value [code] "mk_tree 10"
   3.156 +value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
   3.157 +
   3.158 +lemma mk_tree_Suc_debug' [code]: 
   3.159 +  "mk_tree (Suc n) = (let _ = Debug.flush (STR ''tick'') in mk_tree n \<triangle> mk_tree n)"
   3.160 +  by(simp add: Let_def)
   3.161 +
   3.162 +value [code] "mk_tree 10" \<comment> \<open>Only one tick thanks to the guarding constructor\<close>
   3.163 +value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
   3.164 +value [code] "let t = mk_tree 3; _ = subtree [True, True, False, False] t in t"
   3.165 +
   3.166 +
   3.167 +section \<open>Pattern matching elimination\<close>
   3.168 +
   3.169 +text \<open>The pattern matching elimination handles deep pattern matches and overlapping equations
   3.170 + and only eliminates necessary pattern matches.\<close>
   3.171 +
   3.172 +function crazy :: "nat llist llist \<Rightarrow> tree \<Rightarrow> bool \<Rightarrow> unit" where
   3.173 +  "crazy (\<^bold>\<lbrakk>0\<^bold>\<rbrakk> ### xs) _ _    = Debug.flush (1 :: integer)"
   3.174 +| "crazy xs          \<spadesuit> True = Debug.flush (2 :: integer)"
   3.175 +| "crazy xs          t  b   = Debug.flush (3 :: integer)"
   3.176 +  by pat_completeness auto
   3.177 +termination by lexicographic_order
   3.178 +
   3.179 +code_thms crazy
   3.180 +
   3.181 +end
   3.182 \ No newline at end of file