# HG changeset patch
# User Andreas Lochbihler
# Date 1531722747 -7200
# Node ID 4a2b72b082dc12912be019c01a667e6b44c160e1
# Parent  87d1bff264df0c7edeb73f3df4dd7f641cfd73c0# Parent  f15daa73ee326e370965dbf7f9d1e895394e9523
merged

diff -r 87d1bff264df -r 4a2b72b082dc NEWS
--- a/NEWS	Sun Jul 15 21:58:50 2018 +0100
+++ b/NEWS	Mon Jul 16 08:32:27 2018 +0200
@@ -379,8 +379,9 @@
 
 * Theory HOL-Library.Code_Lazy provides a new preprocessor for the code
 generator to generate code for algebraic types with lazy evaluation
-semantics even in call-by-value target languages. See theory
-HOL-Codegenerator_Test.Code_Lazy_Test for some examples.
+semantics even in call-by-value target languages. See the theories
+HOL-ex.Code_Lazy_Demo and HOL-Codegenerator_Test.Code_Lazy_Test for
+some examples.
 
 * Theory HOL-Library.Landau_Symbols has been moved here from AFP.
 
diff -r 87d1bff264df -r 4a2b72b082dc src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Jul 15 21:58:50 2018 +0100
+++ b/src/HOL/ROOT	Mon Jul 16 08:32:27 2018 +0200
@@ -542,6 +542,7 @@
     Chinese
     Classical
     Code_Binary_Nat_examples
+    Code_Lazy_Demo
     Code_Timing
     Coercion_Examples
     Coherent
diff -r 87d1bff264df -r 4a2b72b082dc src/HOL/ex/Code_Lazy_Demo.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Code_Lazy_Demo.thy	Mon Jul 16 08:32:27 2018 +0200
@@ -0,0 +1,178 @@
+(* Author: Andreas Lochbihler, Digital Asset *)
+
+theory Code_Lazy_Demo imports
+  "HOL-Library.Code_Lazy"
+  "HOL-Library.Debug"
+  "HOL-Library.RBT_Impl"
+begin
+
+text \<open>This theory demonstrates the use of the @{theory "HOL-Library.Code_Lazy"} theory.\<close>
+
+section \<open>Streams\<close>
+
+text \<open>Lazy evaluation for streams\<close>
+
+codatatype 'a stream = 
+  SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
+
+primcorec up :: "nat \<Rightarrow> nat stream" where
+  "up n = n ## up (n + 1)"
+
+primrec stake :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a list" where
+  "stake 0 xs = []"
+| "stake (Suc n) xs = shd xs # stake n (stl xs)"
+
+code_thms up stake \<comment> \<open>The original code equations\<close>
+
+code_lazy_type stream
+
+code_thms up stake \<comment> \<open>The lazified code equations\<close>
+
+value "stake 5 (up 3)"
+
+
+section \<open>Finite lazy lists\<close>
+
+text \<open>Lazy types need not be infinite. We can also have lazy types that are finite.\<close>
+
+datatype 'a llist
+  = LNil ("\<^bold>\<lbrakk>\<^bold>\<rbrakk>") 
+  | LCons (lhd: 'a) (ltl: "'a llist") (infixr "###" 65)
+
+syntax "_llist" :: "args => 'a list"    ("\<^bold>\<lbrakk>(_)\<^bold>\<rbrakk>")
+translations
+  "\<^bold>\<lbrakk>x, xs\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>xs\<^bold>\<rbrakk>"
+  "\<^bold>\<lbrakk>x\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>\<^bold>\<rbrakk>"
+
+fun lnth :: "nat \<Rightarrow> 'a llist \<Rightarrow> 'a" where
+  "lnth 0 (x ### xs) = x"
+| "lnth (Suc n) (x ### xs) = lnth n xs"
+
+definition llist :: "nat llist" where
+  "llist = \<^bold>\<lbrakk>1, 2, 3, hd [], 4\<^bold>\<rbrakk>"
+
+code_lazy_type llist
+
+value [code] "llist"
+value [code] "lnth 2 llist"
+value [code] "let x = lnth 2 llist in (x, llist)"
+
+fun lfilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
+  "lfilter P \<^bold>\<lbrakk>\<^bold>\<rbrakk> = \<^bold>\<lbrakk>\<^bold>\<rbrakk>"
+| "lfilter P (x ### xs) = 
+   (if P x then x ### lfilter P xs else lfilter P xs)"
+
+export_code lfilter in SML
+
+value [code] "lfilter odd llist"
+
+value [code] "lhd (lfilter odd llist)"
+
+
+section \<open>Iterator for red-black trees\<close>
+
+text \<open>Thanks to laziness, we do not need to program a complicated iterator for a tree. 
+  A conversion function to lazy lists is enough.\<close>
+
+primrec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist"
+  (infixr "@@" 65) where
+  "\<^bold>\<lbrakk>\<^bold>\<rbrakk> @@ ys = ys"
+| "(x ### xs) @@ ys = x ### (xs @@ ys)"
+
+primrec rbt_iterator :: "('a, 'b) rbt \<Rightarrow> ('a \<times> 'b) llist" where
+  "rbt_iterator rbt.Empty = \<^bold>\<lbrakk>\<^bold>\<rbrakk>"
+| "rbt_iterator (Branch _ l k v r) = 
+   (let _ = Debug.flush (STR ''tick'') in 
+   rbt_iterator l @@ (k, v) ### rbt_iterator r)"
+
+definition tree :: "(nat, unit) rbt"
+  where "tree = fold (\<lambda>k. rbt_insert k ()) [0..<100] rbt.Empty"
+
+definition find_min :: "('a :: linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) option" where
+  "find_min rbt = 
+  (case rbt_iterator rbt of \<^bold>\<lbrakk>\<^bold>\<rbrakk> \<Rightarrow> None 
+   | kv ### _ \<Rightarrow> Some kv)"
+
+value "find_min tree" \<comment> \<open>Observe that @{const rbt_iterator} is evaluated only for going down 
+  to the first leaf, not for the whole tree (as seen by the ticks).\<close>
+
+text \<open>With strict lists, the whole tree is converted into a list.\<close>
+
+deactivate_lazy_type llist
+value "find_min tree"
+activate_lazy_type llist
+
+
+
+section \<open>Branching datatypes\<close>
+
+datatype tree
+  = L              ("\<spadesuit>") 
+  | Node tree tree (infix "\<triangle>" 900)
+
+notation (output) Node ("\<triangle>(//\<^bold>l: _//\<^bold>r: _)")
+
+code_lazy_type tree
+
+fun mk_tree :: "nat \<Rightarrow> tree" where mk_tree_0:
+  "mk_tree 0 = \<spadesuit>"
+| "mk_tree (Suc n) = (let t = mk_tree n in t \<triangle> t)"
+
+declare mk_tree.simps [code]
+
+code_thms mk_tree
+
+function subtree :: "bool list \<Rightarrow> tree \<Rightarrow> tree" where
+  "subtree [] t = t"
+| "subtree (True # p) (l \<triangle> r) = subtree p l"
+| "subtree (False # p) (l \<triangle> r) = subtree p r"
+| "subtree _ \<spadesuit> = \<spadesuit>"
+  by pat_completeness auto
+termination by lexicographic_order
+
+value [code] "mk_tree 10"
+value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
+  \<comment> \<open>Since @{const mk_tree} shares the two subtrees of a node thanks to the let binding,
+      digging into one subtree spreads to the whole tree.\<close>
+value [code] "let t = mk_tree 3; _ = subtree [True, True, False, False] t in t"
+
+lemma mk_tree_Suc_debug [code]: \<comment> \<open>Make the evaluation visible with tracing.\<close>
+  "mk_tree (Suc n) = 
+  (let _ = Debug.flush (STR ''tick''); t = mk_tree n in t \<triangle> t)"
+  by simp
+
+value [code] "mk_tree 10"
+  \<comment> \<open>The recursive call to @{const mk_tree} is not guarded by a lazy constructor,
+      so all the suspensions are built up immediately.\<close>
+
+lemma mk_tree_Suc [code]: "mk_tree (Suc n) = mk_tree n \<triangle> mk_tree n"
+  \<comment> \<open>In this code equation, there is no sharing and the recursive calls are guarded by a constructor.\<close>
+  by(simp add: Let_def)
+
+value [code] "mk_tree 10"
+value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
+
+lemma mk_tree_Suc_debug' [code]: 
+  "mk_tree (Suc n) = (let _ = Debug.flush (STR ''tick'') in mk_tree n \<triangle> mk_tree n)"
+  by(simp add: Let_def)
+
+value [code] "mk_tree 10" \<comment> \<open>Only one tick thanks to the guarding constructor\<close>
+value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
+value [code] "let t = mk_tree 3; _ = subtree [True, True, False, False] t in t"
+
+
+section \<open>Pattern matching elimination\<close>
+
+text \<open>The pattern matching elimination handles deep pattern matches and overlapping equations
+ and only eliminates necessary pattern matches.\<close>
+
+function crazy :: "nat llist llist \<Rightarrow> tree \<Rightarrow> bool \<Rightarrow> unit" where
+  "crazy (\<^bold>\<lbrakk>0\<^bold>\<rbrakk> ### xs) _ _    = Debug.flush (1 :: integer)"
+| "crazy xs          \<spadesuit> True = Debug.flush (2 :: integer)"
+| "crazy xs          t  b   = Debug.flush (3 :: integer)"
+  by pat_completeness auto
+termination by lexicographic_order
+
+code_thms crazy
+
+end
\ No newline at end of file