Theory Lazy_LList
section ‹Code generator setup to implement lazy lists lazily›
theory Lazy_LList imports
Coinductive_List
begin
subsection ‹Lazy lists›
code_identifier code_module Lazy_LList ⇀
(SML) Coinductive_List and
(OCaml) Coinductive_List and
(Haskell) Coinductive_List and
(Scala) Coinductive_List
definition Lazy_llist :: "(unit ⇒ ('a × 'a llist) option) ⇒ 'a llist"
where [simp]:
"Lazy_llist xs = (case xs () of None ⇒ LNil | Some (x, ys) ⇒ LCons x ys)"
definition force :: "'a llist ⇒ ('a × 'a llist) option"
where [simp, code del]: "force xs = (case xs of LNil ⇒ None | LCons x ys ⇒ Some (x, ys))"
code_datatype Lazy_llist
declare
[[code drop: "partial_term_of :: _ llist itself => _"]]
lemma partial_term_of_llist_code [code]:
fixes tytok :: "'a :: partial_term_of llist itself" shows
"partial_term_of tytok (Quickcheck_Narrowing.Narrowing_variable p tt) ≡
Code_Evaluation.Free (STR ''_'') (Typerep.typerep TYPE('a llist))"
"partial_term_of tytok (Quickcheck_Narrowing.Narrowing_constructor 0 []) ≡
Code_Evaluation.Const (STR ''Coinductive_List.llist.LNil'') (Typerep.typerep TYPE('a llist))"
"partial_term_of tytok (Quickcheck_Narrowing.Narrowing_constructor 1 [head, tail]) ≡
Code_Evaluation.App
(Code_Evaluation.App
(Code_Evaluation.Const
(STR ''Coinductive_List.llist.LCons'')
(Typerep.typerep TYPE('a ⇒ 'a llist ⇒ 'a llist)))
(partial_term_of TYPE('a) head))
(partial_term_of TYPE('a llist) tail)"
by-(rule partial_term_of_anything)+
declare option.splits [split]
lemma Lazy_llist_inject [simp]:
"Lazy_llist xs = Lazy_llist ys ⟷ xs = ys"
by(auto simp add: fun_eq_iff)
lemma Lazy_llist_inverse [code, simp]:
"force (Lazy_llist xs) = xs ()"
by(auto)
lemma force_inverse [simp]:
"Lazy_llist (λ_. force xs) = xs"
by(auto split: llist.split)
lemma LNil_Lazy_llist [code]: "LNil = Lazy_llist (λ_. None)"
by(simp)
lemma LCons_Lazy_llist [code, code_unfold]: "LCons x xs = Lazy_llist (λ_. Some (x, xs))"
by simp
lemma lnull_lazy [code]: "lnull = Option.is_none ∘ force"
unfolding lnull_def
by (rule ext) (simp add: Option.is_none_def split: llist.split)
declare [[code drop: "equal_class.equal :: 'a :: equal llist ⇒ _"]]
lemma equal_llist_Lazy_llist [code]:
"equal_class.equal (Lazy_llist xs) (Lazy_llist ys) ⟷
(case xs () of None ⇒ (case ys () of None ⇒ True | _ ⇒ False)
| Some (x, xs') ⇒
(case ys () of None ⇒ False
| Some (y, ys') ⇒ if x = y then equal_class.equal xs' ys' else False))"
by(auto simp add: equal_llist_def)
declare [[code drop: corec_llist]]
lemma corec_llist_Lazy_llist [code]:
"corec_llist IS_LNIL LHD endORmore LTL_end LTL_more b =
Lazy_llist (λ_. if IS_LNIL b then None
else Some (LHD b,
if endORmore b then LTL_end b
else corec_llist IS_LNIL LHD endORmore LTL_end LTL_more (LTL_more b)))"
by(subst llist.corec_code) simp
declare [[code drop: unfold_llist]]
lemma unfold_llist_Lazy_llist [code]:
"unfold_llist IS_LNIL LHD LTL b =
Lazy_llist (λ_. if IS_LNIL b then None else Some (LHD b, unfold_llist IS_LNIL LHD LTL (LTL b)))"
by(subst unfold_llist.code) simp
declare [[code drop: case_llist]]
lemma case_llist_Lazy_llist [code]:
"case_llist n c (Lazy_llist xs) = (case xs () of None ⇒ n | Some (x, ys) ⇒ c x ys)"
by simp
declare [[code drop: lappend]]
lemma lappend_Lazy_llist [code]:
"lappend (Lazy_llist xs) ys =
Lazy_llist (λ_. case xs () of None ⇒ force ys | Some (x, xs') ⇒ Some (x, lappend xs' ys))"
by(auto split: llist.splits)
declare [[code drop: lmap]]
lemma lmap_Lazy_llist [code]:
"lmap f (Lazy_llist xs) = Lazy_llist (λ_. map_option (map_prod f (lmap f)) (xs ()))"
by simp
declare [[code drop: lfinite]]
lemma lfinite_Lazy_llist [code]:
"lfinite (Lazy_llist xs) = (case xs () of None ⇒ True | Some (x, ys) ⇒ lfinite ys)"
by simp
declare [[code drop: list_of_aux]]
lemma list_of_aux_Lazy_llist [code]:
"list_of_aux xs (Lazy_llist ys) =
(case ys () of None ⇒ rev xs | Some (y, ys) ⇒ list_of_aux (y # xs) ys)"
by(simp add: list_of_aux_code)
declare [[code drop: gen_llength]]
lemma gen_llength_Lazy_llist [code]:
"gen_llength n (Lazy_llist xs) = (case xs () of None ⇒ enat n | Some (_, ys) ⇒ gen_llength (n + 1) ys)"
by(simp add: gen_llength_code)
declare [[code drop: ltake]]
lemma ltake_Lazy_llist [code]:
"ltake n (Lazy_llist xs) =
Lazy_llist (λ_. if n = 0 then None else case xs () of None ⇒ None | Some (x, ys) ⇒ Some (x, ltake (n - 1) ys))"
by(cases n rule: enat_coexhaust) auto
declare [[code drop: ldropn]]
lemma ldropn_Lazy_llist [code]:
"ldropn n (Lazy_llist xs) =
Lazy_llist (λ_. if n = 0 then xs () else
case xs () of None ⇒ None | Some (x, ys) ⇒ force (ldropn (n - 1) ys))"
by(cases n)(auto simp add: eSuc_enat[symmetric] split: llist.split)
declare [[code drop: ltakeWhile]]
lemma ltakeWhile_Lazy_llist [code]:
"ltakeWhile P (Lazy_llist xs) =
Lazy_llist (λ_. case xs () of None ⇒ None | Some (x, ys) ⇒ if P x then Some (x, ltakeWhile P ys) else None)"
by auto
declare [[code drop: ldropWhile]]
lemma ldropWhile_Lazy_llist [code]:
"ldropWhile P (Lazy_llist xs) =
Lazy_llist (λ_. case xs () of None ⇒ None | Some (x, ys) ⇒ if P x then force (ldropWhile P ys) else Some (x, ys))"
by(auto split: llist.split)
declare [[code drop: lzip]]
lemma lzip_Lazy_llist [code]:
"lzip (Lazy_llist xs) (Lazy_llist ys) =
Lazy_llist (λ_. Option.bind (xs ()) (λ(x, xs'). map_option (λ(y, ys'). ((x, y), lzip xs' ys')) (ys ())))"
by auto
declare [[code drop: gen_lset]]
lemma lset_Lazy_llist [code]:
"gen_lset A (Lazy_llist xs) =
(case xs () of None ⇒ A | Some (y, ys) ⇒ gen_lset (insert y A) ys)"
by(auto simp add: gen_lset_code)
declare [[code drop: lmember]]
lemma lmember_Lazy_llist [code]:
"lmember x (Lazy_llist xs) =
(case xs () of None ⇒ False | Some (y, ys) ⇒ x = y ∨ lmember x ys)"
by(simp add: lmember_def)
declare [[code drop: llist_all2]]
lemma llist_all2_Lazy_llist [code]:
"llist_all2 P (Lazy_llist xs) (Lazy_llist ys) =
(case xs () of None ⇒ ys () = None
| Some (x, xs') ⇒ (case ys () of None ⇒ False
| Some (y, ys') ⇒ P x y ∧ llist_all2 P xs' ys'))"
by auto
declare [[code drop: lhd]]
lemma lhd_Lazy_llist [code]:
"lhd (Lazy_llist xs) = (case xs () of None ⇒ undefined | Some (x, xs') ⇒ x)"
by(simp add: lhd_def)
declare [[code drop: ltl]]
lemma ltl_Lazy_llist [code]:
"ltl (Lazy_llist xs) = Lazy_llist (λ_. case xs () of None ⇒ None | Some (x, ys) ⇒ force ys)"
by(auto split: llist.split)
declare [[code drop: llast]]
lemma llast_Lazy_llist [code]:
"llast (Lazy_llist xs) =
(case xs () of
None ⇒ undefined
| Some (x, xs') ⇒
(case force xs' of None ⇒ x | Some (x', xs'') ⇒ llast (LCons x' xs'')))"
by(auto simp add: llast_def zero_enat_def eSuc_def split: enat.split llist.splits)
declare [[code drop: ldistinct]]
lemma ldistinct_Lazy_llist [code]:
"ldistinct (Lazy_llist xs) =
(case xs () of None ⇒ True | Some (x, ys) ⇒ x ∉ lset ys ∧ ldistinct ys)"
by(auto)
declare [[code drop: lprefix]]
lemma lprefix_Lazy_llist [code]:
"lprefix (Lazy_llist xs) (Lazy_llist ys) =
(case xs () of
None ⇒ True
| Some (x, xs') ⇒
(case ys () of None ⇒ False | Some (y, ys') ⇒ x = y ∧ lprefix xs' ys'))"
by auto
declare [[code drop: lstrict_prefix]]
lemma lstrict_prefix_Lazy_llist [code]:
"lstrict_prefix (Lazy_llist xs) (Lazy_llist ys) ⟷
(case ys () of
None ⇒ False
| Some (y, ys') ⇒
(case xs () of None ⇒ True | Some (x, xs') ⇒ x = y ∧ lstrict_prefix xs' ys'))"
by auto
declare [[code drop: llcp]]
lemma llcp_Lazy_llist [code]:
"llcp (Lazy_llist xs) (Lazy_llist ys) =
(case xs () of None ⇒ 0
| Some (x, xs') ⇒ (case ys () of None ⇒ 0
| Some (y, ys') ⇒ if x = y then eSuc (llcp xs' ys') else 0))"
by auto
declare [[code drop: llexord]]
lemma llexord_Lazy_llist [code]:
"llexord r (Lazy_llist xs) (Lazy_llist ys) ⟷
(case xs () of
None ⇒ True
| Some (x, xs') ⇒
(case ys () of None ⇒ False | Some (y, ys') ⇒ r x y ∨ x = y ∧ llexord r xs' ys'))"
by auto
declare [[code drop: lfilter]]
lemma lfilter_Lazy_llist [code]:
"lfilter P (Lazy_llist xs) =
Lazy_llist (λ_. case xs () of None ⇒ None
| Some (x, ys) ⇒ if P x then Some (x, lfilter P ys) else force (lfilter P ys))"
by(auto split: llist.split)
declare [[code drop: lconcat]]
lemma lconcat_Lazy_llist [code]:
"lconcat (Lazy_llist xss) =
Lazy_llist (λ_. case xss () of None ⇒ None | Some (xs, xss') ⇒ force (lappend xs (lconcat xss')))"
by(auto split: llist.split)
declare option.splits [split del]
declare Lazy_llist_def [simp del]
text ‹Simple ML test for laziness›
ML_val ‹
val zeros = @{code iterates} (fn x => x + 1) 0;
val lhd = @{code lhd} zeros;
val ltl = @{code ltl} zeros;
val ltl' = @{code force} ltl;
val ltake = @{code ltake} (@{code eSuc} (@{code eSuc} @{code "0::enat"})) zeros;
val ldrop = @{code ldrop} (@{code eSuc} @{code "0::enat"}) zeros;
val list_of = @{code list_of} ltake;
val ltakeWhile = @{code ltakeWhile} (fn _ => true) zeros;
val ldropWhile = @{code ldropWhile} (fn _ => false) zeros;
val hd = @{code lhd} ldropWhile;
val lfilter = @{code lfilter} (fn _ => false) zeros;
›
hide_const (open) force
end