Quelle  Code_Lazy_Test.thy   Sprache: Isabelle

(* Author: Andreas Lochbihler, Digital Asset *)

section ‹Laziness tests›

theory Code_Lazy_Test imports
  "HOL-Library.Code_Lazy"
  "HOL-Library.Stream" 
  "HOL-Library.Code_Test"
  "HOL-Library.BNF_Corec"
begin

subsection ‹Linear codatatype›

code_lazy_type stream

value [code] "cycle ''ab''"
value [code] "let x = cycle ''ab''; y = snth x 10 in x"

datatype 'a llist = LNil (\\<^bold>[\<^bold>]\) | LCons (lhd: 'a) (ltl: "'a llist") (infixr ‹🚫#› 65)

subsection ‹Finite lazy lists›

code_lazy_type llist

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

definition llist :: "nat llist" where
  "llist = \<^bold>[1, 2, 3, hd [], 4\<^bold>]"

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

value [code] "llist"
value [code] "let x = lnth 2 llist in (x, llist)"
value [code] "llist"

fun lfilter :: "('a \ bool) \ 'a llist \ 'a llist" where
  "lfilter P \<^bold>[\<^bold>] = \<^bold>[\<^bold>]"
| "lfilter P (x \<^bold># xs) = (if P x then x \<^bold># lfilter P xs else lfilter P xs)"

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

definition lfilter_test :: "nat llist \ _" where "lfilter_test xs = lhd (lfilter even xs)"
  🍋 ‹Filtering 🍋‹llist› for 🍋‹even› fails because only the datatype is lazy, not the
  filter function itself.›
ML_val ‹ (@{code lfilter_test} @{code llist}; raise Fail "Failure expected") handle Match => () ›

subsection ‹Records as free type›

record ('a, 'b) rec = 
  rec1 :: 'a
  rec2 :: 'b

free_constructors rec_ext for rec.rec_ext
  subgoal by(rule rec.cases_scheme)
  subgoal by(rule rec.ext_inject)
  done

code_lazy_type rec_ext

definition rec_test1 where "rec_test1 = rec1 (\rec1 = Suc 5, rec2 = True\\rec1 := 0\)"
definition rec_test2 :: "(bool, bool) rec" where "rec_test2 = \rec1 = hd [], rec2 = True\"
test_code "rec_test1 = 0" in PolyML Scala
value [code] "rec_test2"

subsection ‹Branching codatatypes›

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

code_lazy_type tree

fun mk_tree :: "nat \ tree" where
  mk_tree_0: "mk_tree 0 = L"
|            "mk_tree (Suc n) = (let t = mk_tree n in t \ t)"

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 _ L = L"
  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"

value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
value [code] "let t = mk_tree 4; _ = subtree [True, True, False, False] t in t"

subsection ‹Corecursion›

corec (friend) plus :: "'a :: plus stream \ 'a stream \ 'a stream" where
  "plus xs ys = (shd xs + shd ys) ## plus (stl xs) (stl ys)"

corec (friend) times :: "'a :: {plus, times} stream \ 'a stream \ 'a stream" where
  "times xs ys = (shd xs * shd ys) ## plus (times (stl xs) ys) (times xs (stl ys))"

subsection ‹Pattern-matching tests›

definition f1 :: "bool \ bool \ bool \ nat llist \ unit" where
  "f1 _ _ _ _ = ()"

lemma f1_code1 [code]: 
  "f1 True c d \<^bold>[\<^bold>] = ()"
  "f1 b True d \<^bold>[n\<^bold>] = Code.abort (STR ''2'') (\_. ())"
  "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\_. ())"
  "f1 b c d ns = Code.abort (STR ''4'') (\_. ())" 
  by (simp_all add: f1_def)

value [code] "f1 True False False \<^bold>[\<^bold>]"
deactivate_lazy_type llist
value [code] "f1 True False False \<^bold>[\<^bold>]"
declare f1_code1(4) [code del]
value [code] "f1 True False False \<^bold>[\<^bold>]"
activate_lazy_type llist
value [code] "f1 True False False \<^bold>[\<^bold>]"

declare [[code drop: f1]]
lemma f1_code2 [code]:
  "f1 True c d \<^bold>[\<^bold>] = Code.abort (STR ''1'') (\_. ())"
  "f1 b True d \<^bold>[n\<^bold>] = ()"
  "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\_. ())"
  "f1 b c d ns = Code.abort (STR ''4'') (\_. ())" 
  by (simp_all add: f1_def)

value [code] "f1 True True True \<^bold>[0\<^bold>]"
declare f1_code2(4)[code del]
value [code] "f1 True True True \<^bold>[0\<^bold>]"

declare [[code drop: f1]]
lemma f1_code3 [code]:
  "f1 True c d \<^bold>[\<^bold>] = Code.abort (STR ''1'') (\_. ())"
  "f1 b True d \<^bold>[n\<^bold>] = Code.abort (STR ''2'') (\_. ())"
  "f1 b c True \<^bold>[n, m\<^bold>] = ()"
  "f1 b c d ns = Code.abort (STR ''4'') (\_. ())"
  by (simp_all add: f1_def)

value [code] "f1 True True True \<^bold>[0, 1\<^bold>]"
declare f1_code3(4)[code del]
value [code] "f1 True True True \<^bold>[0, 1\<^bold>]"

declare [[code drop: f1]]
lemma f1_code4 [code]:
  "f1 True c d \<^bold>[\<^bold>] = Code.abort (STR ''1'') (\_. ())"
  "f1 b True d \<^bold>[n\<^bold>] = Code.abort (STR ''2'') (\_. ())" 
  "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\_. ())"
  "f1 b c d ns = ()" 
  by (simp_all add: f1_def)

value [code] "f1 True True True \<^bold>[0, 1, 2\<^bold>]"
value [code] "f1 True True False \<^bold>[0, 1\<^bold>]"
value [code] "f1 True False True \<^bold>[0\<^bold>]"
value [code] "f1 False True True \<^bold>[\<^bold>]"

definition f2 :: "nat llist llist list \ unit" where "f2 _ = ()"

lemma f2_code1 [code]:
  "f2 [\<^bold>[\<^bold>[\<^bold>]\<^bold>]] = ()"
  "f2 [\<^bold>[\<^bold>[Suc n\<^bold>]\<^bold>]] = ()"
  "f2 [\<^bold>[\<^bold>[0, Suc n\<^bold>]\<^bold>]] = ()"
  "f2 xs = Code.abort (STR ''a'') (\_. ())"
  by (simp_all add: f2_def)

value [code] "f2 [\<^bold>[\<^bold>[\<^bold>]\<^bold>]]"
value [code] "f2 [\<^bold>[\<^bold>[4\<^bold>]\<^bold>]]"
value [code] "f2 [\<^bold>[\<^bold>[0, 1\<^bold>]\<^bold>]]"
ML_val ‹ (@{code f2} []; error "Fail expected") handle Fail _ => () ›

definition f3 :: "nat set llist \ unit" where "f3 _ = ()"

lemma f3_code1 [code]:
  "f3 \<^bold>[\<^bold>] = ()"
  "f3 \<^bold>[A\<^bold>] = ()"
  by (simp_all add: f3_def)

value [code] "f3 \<^bold>[\<^bold>]"
value [code] "f3 \<^bold>[{}\<^bold>]"
value [code] "f3 \<^bold>[UNIV\<^bold>]"

end