Quelle  Code_Lazy_Demo.thy

(* Author: Andreas Lochbihler, Digital Asset *)

theory Code_Lazy_Demo imports
  "HOL-Library.Code_Lazy"
  "HOL-Library.Debug"
  "HOL-Library.RBT_Impl"
begin

text ‹This theory demonstrates the use of the 🍋‹HOL-Library.Code_Lazy› theory.›

section ‹Streams›

text ‹Lazy evaluation for streams›

codatatype 'a stream = 
  SCons (shd: 'a) (stl: "'a stream") (infixr ‹##› 65)

primcorec up :: "nat ==> nat stream" where
  "up n = n ## up (n + 1)"

primrec stake :: "nat ==> 'a stream ==> 'a list" where
  "stake 0 xs = []"
| "stake (Suc n) xs = shd xs # stake n (stl xs)"

code_thms up stake 🍋 ‹The original code equations›

code_lazy_type stream

code_thms up stake 🍋 ‹The lazified code equations›

value "stake 5 (up 3)"


section ‹Finite lazy lists›

text ‹Lazy types need not be infinite. We can also have lazy types that are finite.›

datatype 'a llist
  = LNil (‹🪙[🪙]›) 
  | LCons (lhd: 'a) (ltl: "'a llist") (infixr ‹###› 65)

syntax
  "_llist" :: "args => 'a list"  (‹(‹indent=1 notation=‹mixfix lazy list enumeration›\›\<^bold>[_🪙])›)
syntax_consts
  "_llist" == LCons
translations
  "🪙[x, xs🪙]" == "x###🪙[xs🪙]"
  "🪙[x🪙]" == "x###🪙[🪙]"

fun lnth :: "nat ==> 'a llist ==> 'a" where
  "lnth 0 (x ### xs) = x"
| "lnth (Suc n) (x ### xs) = lnth n xs"

definition llist :: "nat llist" where
  "llist = 🪙[1, 2, 3, hd [], 4🪙]"

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 ==> bool) ==> 'a llist ==> 'a llist" where
  "lfilter P 🪙[🪙] = 🪙[🪙]"
| "lfilter P (x ### xs) =
   (if P x then x ### lfilter P xs else lfilter P xs)"

export_code lfilter in SML file_prefix lfilter

value [code] "lfilter odd llist"

value [code] "lhd (lfilter odd llist)"


section ‹Iterator for red-black trees›

text ‹Thanks to laziness, we do not need to program a complicated iterator for a tree.
  A conversion function to lazy lists is enough.›

primrec lappend :: "'a llist ==> 'a llist ==> 'a llist"
  (infixr ‹@@› 65) where
  "🪙[🪙] @@ ys = ys"
| "(x ### xs) @@ ys = x ### (xs @@ ys)"

primrec rbt_iterator :: "('a, 'b) rbt ==> ('a × 'b) llist" where
  "rbt_iterator rbt.Empty = 🪙[🪙]"
| "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 (λk. rbt_insert k ()) [0..<100] rbt.Empty"

definition find_min :: "('a :: linorder, 'b) rbt ==> ('a × 'b) option" where
  "find_min rbt =
  (case rbt_iterator rbt of 🪙[🪙] ==> None
   | kv ### _ ==> Some kv)"

value "find_min tree" 🍋 ‹Observe that 🍋‹rbt_iterator› is evaluated only for going down 
  to the first leaf, not for the whole tree (as seen by the ticks).›

text ‹With strict lists, the whole tree is converted into a list.›

deactivate_lazy_type llist
value "find_min tree"
activate_lazy_type llist



section ‹Branching datatypes›

datatype tree
  = L              (‹♠›) 
  | Node tree tree (infix ‹△› 900)

notation (output) Node
  (‹(‹indent=1 notation=‹mixfix tree node›\›\‹open_block notation=‹mixfix tree branch›\›\<^bold>l: _)//(‹open_block notation=‹mixfix tree branch›\›\<^bold>r: _))›)

code_lazy_type tree

fun mk_tree :: "nat ==> tree" where mk_tree_0:
  "mk_tree 0 = ♠"
| "mk_tree (Suc n) = (let t = mk_tree n in t △ t)"

code_thms mk_tree

function subtree :: "bool list ==> tree ==> tree" where
  "subtree [] t = t"
| "subtree (True # p) (l △ r) = subtree p l"
| "subtree (False # p) (l △ r) = subtree p r"
| "subtree _ ♠ = ♠"
  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"
  🍋 ‹Since 🍋‹mk_tree› shares the two subtrees of a node thanks to the let binding,
      digging into one subtree spreads to the whole tree.›
value [code] "let t = mk_tree 3; _ = subtree [True, True, False, False] t in t"

declare mk_tree.simps(1) [code]

lemma mk_tree_Suc_debug [code]: 🍋 ‹Make the evaluation visible with tracing.›
  "mk_tree (Suc n) =
  (let _ = Debug.flush (STR ''tick''); t = mk_tree n in t △ t)"
  by simp

value [code] "mk_tree 10"
  🍋 ‹The recursive call to 🍋‹mk_tree› is not guarded by a lazy constructor,
      so all the suspensions are built up immediately.›

declare [[code drop: mk_tree]] mk_tree.simps(1) [code]

lemma mk_tree_Suc [code]: "mk_tree (Suc n) = mk_tree n △ mk_tree n"
  🍋 ‹In this code equation, there is no sharing and the recursive calls are guarded by a constructor.›
  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"

declare [[code drop: mk_tree]] mk_tree.simps(1) [code]

lemma mk_tree_Suc_debug' [code]: 
  "mk_tree (Suc n) = (let _ = Debug.flush (STR ''tick'') in mk_tree n △ mk_tree n)"
  by(simp add: Let_def)

value [code] "mk_tree 10" 🍋 ‹Only one tick thanks to the guarding constructor›
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 ‹Pattern matching elimination›

text ‹The pattern matching elimination handles deep pattern matches and overlapping equations
  and only eliminates necessary pattern matches.›

function crazy :: "nat llist llist ==> tree ==> bool ==> unit" where
  "crazy (🪙[0🪙] ### xs) _ _ = Debug.flush (1 :: integer)"
| "crazy xs ♠ 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