src/HOL/Codegenerator_Test/Code_Lazy_Test.thy

+(* Author: Andreas Lochbihler, Digital Asset *)
+
+section \<open>Laziness tests\<close>
+
+theory Code_Lazy_Test imports
+  "HOL-Library.Code_Lazy"
+  "HOL-Library.Stream" 
+  "HOL-Library.Code_Test"
+  "HOL-Library.BNF_Corec"
+begin
+
+subsection \<open>Linear codatatype\<close>
+
+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 "\<^bold>#" 65)
+
+subsection \<open>Finite lazy lists\<close>
+
+code_lazy_type llist
+
+no_notation lazy_llist ("_")
+syntax "_llist" :: "args => 'a list"    ("\<^bold>[(_)\<^bold>]")
+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 \<Rightarrow> 'a llist \<Rightarrow> '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 \<Rightarrow> bool) \<Rightarrow> 'a llist \<Rightarrow> '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 \<Rightarrow> _" where "lfilter_test xs = lhd (lfilter even xs)"
+  \<comment> \<open>Filtering @{term llist} for @{term even} fails because only the datatype is lazy, not the
+  filter function itself.\<close>
+ML_val \<open> (@{code lfilter_test} @{code llist}; raise Fail "Failure expected") handle Match => () \<close>
+
+subsection \<open>Records as free type\<close>
+
+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 (\<lparr>rec1 = Suc 5, rec2 = True\<rparr>\<lparr>rec1 := 0\<rparr>)"
+definition rec_test2 :: "(bool, bool) rec" where "rec_test2 = \<lparr>rec1 = hd [], rec2 = True\<rparr>"
+test_code "rec_test1 = 0" in PolyML Scala
+value [code] "rec_test2"
+
+subsection \<open>Branching codatatypes\<close>
+
+codatatype tree = L | Node tree tree (infix "\<triangle>" 900)
+
+code_lazy_type tree
+
+fun mk_tree :: "nat \<Rightarrow> tree" where
+  mk_tree_0: "mk_tree 0 = L"
+|            "mk_tree (Suc n) = (let t = mk_tree n in t \<triangle> t)"
+
+function subtree :: "bool list \<Rightarrow> tree \<Rightarrow> tree" where
+  "subtree [] t = t"
+| "subtree (True # p) (l \<triangle> r) = subtree p l"
+| "subtree (False # p) (l \<triangle> 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"
+
+lemma mk_tree_Suc: "mk_tree (Suc n) = mk_tree n \<triangle> mk_tree n"
+  by(simp add: Let_def)
+lemmas [code] = mk_tree_0 mk_tree_Suc
+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 \<open>Corecursion\<close>
+
+corec (friend) plus :: "'a :: plus stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where
+  "plus xs ys = (shd xs + shd ys) ## plus (stl xs) (stl ys)"
+
+corec (friend) times :: "'a :: {plus, times} stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where
+  "times xs ys = (shd xs * shd ys) ## plus (times (stl xs) ys) (times xs (stl ys))"
+
+subsection \<open>Pattern-matching tests\<close>
+
+definition f1 :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> nat llist \<Rightarrow> unit" where
+  "f1 _ _ _ _ = ()"
+
+declare [[code drop: f1]]
+lemma f1_code1 [code]: 
+  "f1 b c d    ns     = Code.abort (STR ''4'') (\<lambda>_. ())" 
+  "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\<lambda>_. ())" 
+  "f1 b True d \<^bold>[n\<^bold>]    = Code.abort (STR ''2'') (\<lambda>_. ())" 
+  "f1 True c d \<^bold>[\<^bold>]     = ()"
+  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(1) [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 b c d    ns     = Code.abort (STR ''4'') (\<lambda>_. ())" 
+  "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\<lambda>_. ())" 
+  "f1 b True d \<^bold>[n\<^bold>]    = ()"
+  "f1 True c d \<^bold>[\<^bold>]     = Code.abort (STR ''1'') (\<lambda>_. ())"
+  by(simp_all add: f1_def)
+
+value [code] "f1 True True True \<^bold>[0\<^bold>]"
+declare f1_code2(1)[code del]
+value [code] "f1 True True True \<^bold>[0\<^bold>]"
+
+declare [[code drop: f1]]
+lemma f1_code3 [code]:
+  "f1 b c d    ns     = Code.abort (STR ''4'') (\<lambda>_. ())"
+  "f1 b c True \<^bold>[n, m\<^bold>] = ()" 
+  "f1 b True d \<^bold>[n\<^bold>]    = Code.abort (STR ''2'') (\<lambda>_. ())"
+  "f1 True c d \<^bold>[\<^bold>]     = Code.abort (STR ''1'') (\<lambda>_. ())"
+  by(simp_all add: f1_def)
+
+value [code] "f1 True True True \<^bold>[0, 1\<^bold>]"
+declare f1_code3(1)[code del]
+value [code] "f1 True True True \<^bold>[0, 1\<^bold>]"
+
+declare [[code drop: f1]]
+lemma f1_code4 [code]:
+  "f1 b c d    ns     = ()" 
+  "f1 b c True \<^bold>[n, m\<^bold>] = Code.abort (STR ''3'') (\<lambda>_. ())"
+  "f1 b True d \<^bold>[n\<^bold>]    = Code.abort (STR ''2'') (\<lambda>_. ())" 
+  "f1 True c d \<^bold>[\<^bold>]     = Code.abort (STR ''1'') (\<lambda>_. ())"
+  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 \<Rightarrow> unit" where "f2 _ = ()"
+
+declare [[code drop: f2]]
+lemma f2_code1 [code]:
+  "f2 xs = Code.abort (STR ''a'') (\<lambda>_. ())"
+  "f2 [\<^bold>[\<^bold>[\<^bold>]\<^bold>]] = ()"
+  "f2 [\<^bold>[\<^bold>[Suc n\<^bold>]\<^bold>]] = ()"
+  "f2 [\<^bold>[\<^bold>[0, Suc n\<^bold>]\<^bold>]] = ()"
+  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 \<open> (@{code f2} []; error "Fail expected") handle Fail _ => () \<close>
+
+definition f3 :: "nat set llist \<Rightarrow> unit" where "f3 _ = ()"
+
+declare [[code drop: 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