Quelle Code_Lazy_Demo.thy Sprache: Isabelle

(* 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 (\<open>\<^bold>\<lbrakk>\<^bold>\<rbrakk>\<close>)
  | LCons (lhd: 'a) (ltl: "'a llist") (infixr \###\ 65)

syntax
  "_llist" :: "args => 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix lazy list enumeration\<close>\<close>\<^bold>\<lbrakk>_\<^bold>\<rbrakk>)\<close>)
syntax_consts
  "_llist" == LCons
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 \<open>@@\<close> 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              (\<open>\<spadesuit>\<close>)
  | Node tree tree (infix \<open>\<triangle>\<close> 900)

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

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"
  \<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"

declare mk_tree.simps(1) [code]

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>

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"
  \<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"

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" \<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

quality93%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.