src/HOL/ex/Code_Lazy_Demo.thy
author Andreas Lochbihler
Sun Jul 15 23:44:38 2018 +0200 (18 months ago)
changeset 68639 357fca99a65a
child 69597 ff784d5a5bfb
permissions -rw-r--r--
more examples for Code_Lazy
     1 (* Author: Andreas Lochbihler, Digital Asset *)
     2 
     3 theory Code_Lazy_Demo imports
     4   "HOL-Library.Code_Lazy"
     5   "HOL-Library.Debug"
     6   "HOL-Library.RBT_Impl"
     7 begin
     8 
     9 text \<open>This theory demonstrates the use of the @{theory "HOL-Library.Code_Lazy"} theory.\<close>
    10 
    11 section \<open>Streams\<close>
    12 
    13 text \<open>Lazy evaluation for streams\<close>
    14 
    15 codatatype 'a stream = 
    16   SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
    17 
    18 primcorec up :: "nat \<Rightarrow> nat stream" where
    19   "up n = n ## up (n + 1)"
    20 
    21 primrec 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 
    25 code_thms up stake \<comment> \<open>The original code equations\<close>
    26 
    27 code_lazy_type stream
    28 
    29 code_thms up stake \<comment> \<open>The lazified code equations\<close>
    30 
    31 value "stake 5 (up 3)"
    32 
    33 
    34 section \<open>Finite lazy lists\<close>
    35 
    36 text \<open>Lazy types need not be infinite. We can also have lazy types that are finite.\<close>
    37 
    38 datatype 'a llist
    39   = LNil ("\<^bold>\<lbrakk>\<^bold>\<rbrakk>") 
    40   | LCons (lhd: 'a) (ltl: "'a llist") (infixr "###" 65)
    41 
    42 syntax "_llist" :: "args => 'a list"    ("\<^bold>\<lbrakk>(_)\<^bold>\<rbrakk>")
    43 translations
    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 
    47 fun lnth :: "nat \<Rightarrow> 'a llist \<Rightarrow> 'a" where
    48   "lnth 0 (x ### xs) = x"
    49 | "lnth (Suc n) (x ### xs) = lnth n xs"
    50 
    51 definition llist :: "nat llist" where
    52   "llist = \<^bold>\<lbrakk>1, 2, 3, hd [], 4\<^bold>\<rbrakk>"
    53 
    54 code_lazy_type llist
    55 
    56 value [code] "llist"
    57 value [code] "lnth 2 llist"
    58 value [code] "let x = lnth 2 llist in (x, llist)"
    59 
    60 fun 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 
    65 export_code lfilter in SML
    66 
    67 value [code] "lfilter odd llist"
    68 
    69 value [code] "lhd (lfilter odd llist)"
    70 
    71 
    72 section \<open>Iterator for red-black trees\<close>
    73 
    74 text \<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 
    77 primrec 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 
    82 primrec 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 
    88 definition tree :: "(nat, unit) rbt"
    89   where "tree = fold (\<lambda>k. rbt_insert k ()) [0..<100] rbt.Empty"
    90 
    91 definition 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 
    96 value "find_min tree" \<comment> \<open>Observe that @{const rbt_iterator} is evaluated only for going down 
    97   to the first leaf, not for the whole tree (as seen by the ticks).\<close>
    98 
    99 text \<open>With strict lists, the whole tree is converted into a list.\<close>
   100 
   101 deactivate_lazy_type llist
   102 value "find_min tree"
   103 activate_lazy_type llist
   104 
   105 
   106 
   107 section \<open>Branching datatypes\<close>
   108 
   109 datatype tree
   110   = L              ("\<spadesuit>") 
   111   | Node tree tree (infix "\<triangle>" 900)
   112 
   113 notation (output) Node ("\<triangle>(//\<^bold>l: _//\<^bold>r: _)")
   114 
   115 code_lazy_type tree
   116 
   117 fun 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 
   121 declare mk_tree.simps [code]
   122 
   123 code_thms mk_tree
   124 
   125 function 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
   131 termination by lexicographic_order
   132 
   133 value [code] "mk_tree 10"
   134 value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
   135   \<comment> \<open>Since @{const mk_tree} shares the two subtrees of a node thanks to the let binding,
   136       digging into one subtree spreads to the whole tree.\<close>
   137 value [code] "let t = mk_tree 3; _ = subtree [True, True, False, False] t in t"
   138 
   139 lemma 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 
   144 value [code] "mk_tree 10"
   145   \<comment> \<open>The recursive call to @{const mk_tree} is not guarded by a lazy constructor,
   146       so all the suspensions are built up immediately.\<close>
   147 
   148 lemma 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 
   152 value [code] "mk_tree 10"
   153 value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
   154 
   155 lemma 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 
   159 value [code] "mk_tree 10" \<comment> \<open>Only one tick thanks to the guarding constructor\<close>
   160 value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
   161 value [code] "let t = mk_tree 3; _ = subtree [True, True, False, False] t in t"
   162 
   163 
   164 section \<open>Pattern matching elimination\<close>
   165 
   166 text \<open>The pattern matching elimination handles deep pattern matches and overlapping equations
   167  and only eliminates necessary pattern matches.\<close>
   168 
   169 function 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
   174 termination by lexicographic_order
   175 
   176 code_thms crazy
   177 
   178 end