|
(* 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>\<open>HOL-Library.Code_Lazy\<close> 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 \ 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 \<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>\\<^bold>\")
| LCons (lhd: 'a) (ltl: "'a llist") (infixr "###" 65)
syntax "_llist" :: "args => 'a list" ("\<^bold>\(_)\<^bold>\")
translations
"\<^bold>\x, xs\<^bold>\" == "x###\<^bold>\xs\<^bold>\"
"\<^bold>\x\<^bold>\" == "x###\<^bold>\\<^bold>\"
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 = \<^bold>\1, 2, 3, hd [], 4\<^bold>\"
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 \<^bold>\\<^bold>\ = \<^bold>\\<^bold>\"
| "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 \<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 \ 'a llist \ 'a llist"
(infixr "@@" 65) where
"\<^bold>\\<^bold>\ @@ ys = ys"
| "(x ### xs) @@ ys = x ### (xs @@ ys)"
primrec rbt_iterator :: "('a, 'b) rbt \ ('a \ 'b) llist" where
"rbt_iterator rbt.Empty = \<^bold>\\<^bold>\"
| "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 \<^bold>\<lbrakk>\<^bold>\<rbrakk> \<Rightarrow> None
| kv ### _ \<Rightarrow> Some kv)"
value "find_min tree" \<comment> \<open>Observe that \<^const>\<open>rbt_iterator\<close> 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 ("\")
| Node tree tree (infix "\" 900)
notation (output) Node ("\(//\<^bold>l: _//\<^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)"
declare mk_tree.simps [code]
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"
\<comment> \<open>Since \<^const>\<open>mk_tree\<close> 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>\<open>mk_tree\<close> 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 \ 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 \ 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 \ tree \ bool \ unit" where
"crazy (\<^bold>\0\<^bold>\ ### 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
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
