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
Andreas@68639
     1
(* Author: Andreas Lochbihler, Digital Asset *)
Andreas@68639
     2
Andreas@68639
     3
theory Code_Lazy_Demo imports
Andreas@68639
     4
  "HOL-Library.Code_Lazy"
Andreas@68639
     5
  "HOL-Library.Debug"
Andreas@68639
     6
  "HOL-Library.RBT_Impl"
Andreas@68639
     7
begin
Andreas@68639
     8
Andreas@68639
     9
text \<open>This theory demonstrates the use of the @{theory "HOL-Library.Code_Lazy"} theory.\<close>
Andreas@68639
    10
Andreas@68639
    11
section \<open>Streams\<close>
Andreas@68639
    12
Andreas@68639
    13
text \<open>Lazy evaluation for streams\<close>
Andreas@68639
    14
Andreas@68639
    15
codatatype 'a stream = 
Andreas@68639
    16
  SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
Andreas@68639
    17
Andreas@68639
    18
primcorec up :: "nat \<Rightarrow> nat stream" where
Andreas@68639
    19
  "up n = n ## up (n + 1)"
Andreas@68639
    20
Andreas@68639
    21
primrec stake :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a list" where
Andreas@68639
    22
  "stake 0 xs = []"
Andreas@68639
    23
| "stake (Suc n) xs = shd xs # stake n (stl xs)"
Andreas@68639
    24
Andreas@68639
    25
code_thms up stake \<comment> \<open>The original code equations\<close>
Andreas@68639
    26
Andreas@68639
    27
code_lazy_type stream
Andreas@68639
    28
Andreas@68639
    29
code_thms up stake \<comment> \<open>The lazified code equations\<close>
Andreas@68639
    30
Andreas@68639
    31
value "stake 5 (up 3)"
Andreas@68639
    32
Andreas@68639
    33
Andreas@68639
    34
section \<open>Finite lazy lists\<close>
Andreas@68639
    35
Andreas@68639
    36
text \<open>Lazy types need not be infinite. We can also have lazy types that are finite.\<close>
Andreas@68639
    37
Andreas@68639
    38
datatype 'a llist
Andreas@68639
    39
  = LNil ("\<^bold>\<lbrakk>\<^bold>\<rbrakk>") 
Andreas@68639
    40
  | LCons (lhd: 'a) (ltl: "'a llist") (infixr "###" 65)
Andreas@68639
    41
Andreas@68639
    42
syntax "_llist" :: "args => 'a list"    ("\<^bold>\<lbrakk>(_)\<^bold>\<rbrakk>")
Andreas@68639
    43
translations
Andreas@68639
    44
  "\<^bold>\<lbrakk>x, xs\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>xs\<^bold>\<rbrakk>"
Andreas@68639
    45
  "\<^bold>\<lbrakk>x\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>\<^bold>\<rbrakk>"
Andreas@68639
    46
Andreas@68639
    47
fun lnth :: "nat \<Rightarrow> 'a llist \<Rightarrow> 'a" where
Andreas@68639
    48
  "lnth 0 (x ### xs) = x"
Andreas@68639
    49
| "lnth (Suc n) (x ### xs) = lnth n xs"
Andreas@68639
    50
Andreas@68639
    51
definition llist :: "nat llist" where
Andreas@68639
    52
  "llist = \<^bold>\<lbrakk>1, 2, 3, hd [], 4\<^bold>\<rbrakk>"
Andreas@68639
    53
Andreas@68639
    54
code_lazy_type llist
Andreas@68639
    55
Andreas@68639
    56
value [code] "llist"
Andreas@68639
    57
value [code] "lnth 2 llist"
Andreas@68639
    58
value [code] "let x = lnth 2 llist in (x, llist)"
Andreas@68639
    59
Andreas@68639
    60
fun lfilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
Andreas@68639
    61
  "lfilter P \<^bold>\<lbrakk>\<^bold>\<rbrakk> = \<^bold>\<lbrakk>\<^bold>\<rbrakk>"
Andreas@68639
    62
| "lfilter P (x ### xs) = 
Andreas@68639
    63
   (if P x then x ### lfilter P xs else lfilter P xs)"
Andreas@68639
    64
Andreas@68639
    65
export_code lfilter in SML
Andreas@68639
    66
Andreas@68639
    67
value [code] "lfilter odd llist"
Andreas@68639
    68
Andreas@68639
    69
value [code] "lhd (lfilter odd llist)"
Andreas@68639
    70
Andreas@68639
    71
Andreas@68639
    72
section \<open>Iterator for red-black trees\<close>
Andreas@68639
    73
Andreas@68639
    74
text \<open>Thanks to laziness, we do not need to program a complicated iterator for a tree. 
Andreas@68639
    75
  A conversion function to lazy lists is enough.\<close>
Andreas@68639
    76
Andreas@68639
    77
primrec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist"
Andreas@68639
    78
  (infixr "@@" 65) where
Andreas@68639
    79
  "\<^bold>\<lbrakk>\<^bold>\<rbrakk> @@ ys = ys"
Andreas@68639
    80
| "(x ### xs) @@ ys = x ### (xs @@ ys)"
Andreas@68639
    81
Andreas@68639
    82
primrec rbt_iterator :: "('a, 'b) rbt \<Rightarrow> ('a \<times> 'b) llist" where
Andreas@68639
    83
  "rbt_iterator rbt.Empty = \<^bold>\<lbrakk>\<^bold>\<rbrakk>"
Andreas@68639
    84
| "rbt_iterator (Branch _ l k v r) = 
Andreas@68639
    85
   (let _ = Debug.flush (STR ''tick'') in 
Andreas@68639
    86
   rbt_iterator l @@ (k, v) ### rbt_iterator r)"
Andreas@68639
    87
Andreas@68639
    88
definition tree :: "(nat, unit) rbt"
Andreas@68639
    89
  where "tree = fold (\<lambda>k. rbt_insert k ()) [0..<100] rbt.Empty"
Andreas@68639
    90
Andreas@68639
    91
definition find_min :: "('a :: linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) option" where
Andreas@68639
    92
  "find_min rbt = 
Andreas@68639
    93
  (case rbt_iterator rbt of \<^bold>\<lbrakk>\<^bold>\<rbrakk> \<Rightarrow> None 
Andreas@68639
    94
   | kv ### _ \<Rightarrow> Some kv)"
Andreas@68639
    95
Andreas@68639
    96
value "find_min tree" \<comment> \<open>Observe that @{const rbt_iterator} is evaluated only for going down 
Andreas@68639
    97
  to the first leaf, not for the whole tree (as seen by the ticks).\<close>
Andreas@68639
    98
Andreas@68639
    99
text \<open>With strict lists, the whole tree is converted into a list.\<close>
Andreas@68639
   100
Andreas@68639
   101
deactivate_lazy_type llist
Andreas@68639
   102
value "find_min tree"
Andreas@68639
   103
activate_lazy_type llist
Andreas@68639
   104
Andreas@68639
   105
Andreas@68639
   106
Andreas@68639
   107
section \<open>Branching datatypes\<close>
Andreas@68639
   108
Andreas@68639
   109
datatype tree
Andreas@68639
   110
  = L              ("\<spadesuit>") 
Andreas@68639
   111
  | Node tree tree (infix "\<triangle>" 900)
Andreas@68639
   112
Andreas@68639
   113
notation (output) Node ("\<triangle>(//\<^bold>l: _//\<^bold>r: _)")
Andreas@68639
   114
Andreas@68639
   115
code_lazy_type tree
Andreas@68639
   116
Andreas@68639
   117
fun mk_tree :: "nat \<Rightarrow> tree" where mk_tree_0:
Andreas@68639
   118
  "mk_tree 0 = \<spadesuit>"
Andreas@68639
   119
| "mk_tree (Suc n) = (let t = mk_tree n in t \<triangle> t)"
Andreas@68639
   120
Andreas@68639
   121
declare mk_tree.simps [code]
Andreas@68639
   122
Andreas@68639
   123
code_thms mk_tree
Andreas@68639
   124
Andreas@68639
   125
function subtree :: "bool list \<Rightarrow> tree \<Rightarrow> tree" where
Andreas@68639
   126
  "subtree [] t = t"
Andreas@68639
   127
| "subtree (True # p) (l \<triangle> r) = subtree p l"
Andreas@68639
   128
| "subtree (False # p) (l \<triangle> r) = subtree p r"
Andreas@68639
   129
| "subtree _ \<spadesuit> = \<spadesuit>"
Andreas@68639
   130
  by pat_completeness auto
Andreas@68639
   131
termination by lexicographic_order
Andreas@68639
   132
Andreas@68639
   133
value [code] "mk_tree 10"
Andreas@68639
   134
value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
Andreas@68639
   135
  \<comment> \<open>Since @{const mk_tree} shares the two subtrees of a node thanks to the let binding,
Andreas@68639
   136
      digging into one subtree spreads to the whole tree.\<close>
Andreas@68639
   137
value [code] "let t = mk_tree 3; _ = subtree [True, True, False, False] t in t"
Andreas@68639
   138
Andreas@68639
   139
lemma mk_tree_Suc_debug [code]: \<comment> \<open>Make the evaluation visible with tracing.\<close>
Andreas@68639
   140
  "mk_tree (Suc n) = 
Andreas@68639
   141
  (let _ = Debug.flush (STR ''tick''); t = mk_tree n in t \<triangle> t)"
Andreas@68639
   142
  by simp
Andreas@68639
   143
Andreas@68639
   144
value [code] "mk_tree 10"
Andreas@68639
   145
  \<comment> \<open>The recursive call to @{const mk_tree} is not guarded by a lazy constructor,
Andreas@68639
   146
      so all the suspensions are built up immediately.\<close>
Andreas@68639
   147
Andreas@68639
   148
lemma mk_tree_Suc [code]: "mk_tree (Suc n) = mk_tree n \<triangle> mk_tree n"
Andreas@68639
   149
  \<comment> \<open>In this code equation, there is no sharing and the recursive calls are guarded by a constructor.\<close>
Andreas@68639
   150
  by(simp add: Let_def)
Andreas@68639
   151
Andreas@68639
   152
value [code] "mk_tree 10"
Andreas@68639
   153
value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
Andreas@68639
   154
Andreas@68639
   155
lemma mk_tree_Suc_debug' [code]: 
Andreas@68639
   156
  "mk_tree (Suc n) = (let _ = Debug.flush (STR ''tick'') in mk_tree n \<triangle> mk_tree n)"
Andreas@68639
   157
  by(simp add: Let_def)
Andreas@68639
   158
Andreas@68639
   159
value [code] "mk_tree 10" \<comment> \<open>Only one tick thanks to the guarding constructor\<close>
Andreas@68639
   160
value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
Andreas@68639
   161
value [code] "let t = mk_tree 3; _ = subtree [True, True, False, False] t in t"
Andreas@68639
   162
Andreas@68639
   163
Andreas@68639
   164
section \<open>Pattern matching elimination\<close>
Andreas@68639
   165
Andreas@68639
   166
text \<open>The pattern matching elimination handles deep pattern matches and overlapping equations
Andreas@68639
   167
 and only eliminates necessary pattern matches.\<close>
Andreas@68639
   168
Andreas@68639
   169
function crazy :: "nat llist llist \<Rightarrow> tree \<Rightarrow> bool \<Rightarrow> unit" where
Andreas@68639
   170
  "crazy (\<^bold>\<lbrakk>0\<^bold>\<rbrakk> ### xs) _ _    = Debug.flush (1 :: integer)"
Andreas@68639
   171
| "crazy xs          \<spadesuit> True = Debug.flush (2 :: integer)"
Andreas@68639
   172
| "crazy xs          t  b   = Debug.flush (3 :: integer)"
Andreas@68639
   173
  by pat_completeness auto
Andreas@68639
   174
termination by lexicographic_order
Andreas@68639
   175
Andreas@68639
   176
code_thms crazy
Andreas@68639
   177
Andreas@68639
   178
end