Theory Coinductive.Lazy_TLList

(*  Title:       Lazy_TLList.thy
    Author:      Andreas Lochbihler
*)

section ‹Code generator setup to implement terminated lazy lists lazily›

theory Lazy_TLList imports
  TLList
  Lazy_LList
begin

code_identifier code_module Lazy_TLList ⇀
  (SML) TLList and
  (OCaml) TLList and
  (Haskell) TLList and
  (Scala) TLList

definition Lazy_tllist :: "(unit ⇒ 'a × ('a, 'b) tllist + 'b) ⇒ ('a, 'b) tllist"
where [code del]:
  "Lazy_tllist xs = (case xs () of Inl (x, ys) ⇒ TCons x ys | Inr b ⇒ TNil b)"

definition force :: "('a, 'b) tllist ⇒ 'a × ('a, 'b) tllist + 'b"
where [simp, code del]: "force xs = (case xs of TNil b ⇒ Inr b | TCons x ys ⇒ Inl (x, ys))"

code_datatype Lazy_tllist

declare ― ‹Restore consistency in code equations between @{const partial_term_of} and @{const narrowing} for @{typ "('a, 'b) tllist"}›
   [[code drop: "partial_term_of :: (_, _) tllist itself => _"]]

lemma partial_term_of_tllist_code [code]:
  fixes tytok :: "('a :: partial_term_of, 'b :: partial_term_of) tllist itself" shows
  "partial_term_of tytok (Quickcheck_Narrowing.Narrowing_variable p tt) ≡
   Code_Evaluation.Free (STR ''_'') (Typerep.typerep TYPE(('a, 'b) tllist))"
  "partial_term_of tytok (Quickcheck_Narrowing.Narrowing_constructor 0 [b]) ≡
   Code_Evaluation.App
     (Code_Evaluation.Const (STR ''TLList.tllist.TNil'') (Typerep.typerep TYPE('b ⇒ ('a, 'b) tllist)))
     (partial_term_of TYPE('b) b)"
  "partial_term_of tytok (Quickcheck_Narrowing.Narrowing_constructor 1 [head, tail]) ≡
   Code_Evaluation.App
     (Code_Evaluation.App
        (Code_Evaluation.Const
           (STR ''TLList.tllist.TCons'')
           (Typerep.typerep TYPE('a ⇒ ('a, 'b) tllist ⇒ ('a, 'b) tllist)))
        (partial_term_of TYPE('a) head))
     (partial_term_of TYPE(('a, 'b) tllist) tail)"
by-(rule partial_term_of_anything)+

declare Lazy_tllist_def [simp]
declare sum.splits [split]

lemma TNil_Lazy_tllist [code]: 
  "TNil b = Lazy_tllist (λ_. Inr b)"
by simp

lemma TCons_Lazy_tllist [code, code_unfold]:
  "TCons x xs = Lazy_tllist (λ_. Inl (x, xs))"
by simp

lemma Lazy_tllist_inverse [simp, code]:
  "force (Lazy_tllist xs) = xs ()"
by(simp)

declare [[code drop: "equal_class.equal :: (_, _) tllist ⇒ _"]]

lemma equal_tllist_Lazy_tllist [code]:
  "equal_class.equal (Lazy_tllist xs) (Lazy_tllist ys) =
  (case xs () of 
     Inr b ⇒ (case ys () of Inr b' ⇒ b = b' | _ ⇒ False)
   | Inl (x, xs') ⇒
     (case ys () of Inr b' ⇒ False | Inl (y, ys') ⇒ if x = y then equal_class.equal xs' ys' else False))"
by(auto simp add: equal_tllist_def)

declare
  [[code drop: thd ttl]]
  thd_def [code]
  ttl_def [code]

declare [[code drop: is_TNil]]

lemma is_TNil_code [code]:
  "is_TNil (Lazy_tllist xs) ⟷ 
  (case xs () of Inl _ ⇒ False | Inr _ ⇒ True)"
by simp

declare [[code drop: corec_tllist]]

lemma corec_tllist_Lazy_tllist [code]:
  "corec_tllist IS_TNIL TNIL THD endORmore TTL_end TTL_more b = Lazy_tllist
  (λ_. if IS_TNIL b then Inr (TNIL b)
       else Inl (THD b, if endORmore b then TTL_end b else corec_tllist IS_TNIL TNIL THD endORmore TTL_end TTL_more (TTL_more b)))"
by(rule tllist.expand) simp_all

declare [[code drop: unfold_tllist]]

lemma unfold_tllist_Lazy_tllist [code]:
  "unfold_tllist IS_TNIL TNIL THD TTL b = Lazy_tllist
  (λ_. if IS_TNIL b then Inr (TNIL b)
       else Inl (THD b, unfold_tllist IS_TNIL TNIL THD TTL (TTL b)))"
by(rule tllist.expand) auto

declare [[code drop: case_tllist]]

lemma case_tllist_Lazy_tllist [code]:
  "case_tllist n c (Lazy_tllist xs) = 
  (case xs () of Inl (x, ys) ⇒ c x ys | Inr b ⇒ n b)"
by simp

declare [[code drop: tllist_of_llist]]

lemma tllist_of_llist_Lazy_llist [code]:
  "tllist_of_llist b (Lazy_llist xs) =
  Lazy_tllist (λ_. case xs () of None ⇒ Inr b | Some (x, ys) ⇒ Inl (x, tllist_of_llist b ys))"
by(simp add: Lazy_llist_def split: option.splits)

declare [[code drop: terminal]]

lemma terminal_Lazy_tllist [code]:
  "terminal (Lazy_tllist xs) = 
  (case xs () of Inl (_, ys) ⇒ terminal ys | Inr b ⇒ b)"
by simp

declare [[code drop: tmap]]

lemma tmap_Lazy_tllist [code]:
  "tmap f g (Lazy_tllist xs) =
  Lazy_tllist (λ_. case xs () of Inl (x, ys) ⇒ Inl (f x, tmap f g ys) | Inr b ⇒ Inr (g b))"
by simp

declare [[code drop: tappend]]

lemma tappend_Lazy_tllist [code]:
  "tappend (Lazy_tllist xs) ys =
  Lazy_tllist (λ_. case xs () of Inl (x, xs') ⇒ Inl (x, tappend xs' ys) | Inr b ⇒ force (ys b))"
by(auto split: tllist.split)

declare [[code drop: lappendt]]

lemma lappendt_Lazy_llist [code]:
  "lappendt (Lazy_llist xs) ys =
  Lazy_tllist (λ_. case xs () of None ⇒ force ys | Some (x, xs') ⇒ Inl (x, lappendt xs' ys))"
by(auto simp add: Lazy_llist_def split: option.split tllist.split)

declare [[code drop: TLList.tfilter']]

lemma tfilter'_Lazy_tllist [code]:
  "TLList.tfilter' b P (Lazy_tllist xs) =
   Lazy_tllist (λ_. case xs () of Inl (x, xs') ⇒ if P x then Inl (x, TLList.tfilter' b P xs') else force (TLList.tfilter' b P xs') | Inr b' ⇒ Inr b')"
by(simp split: tllist.split)

declare [[code drop: TLList.tconcat']]

lemma tconcat_Lazy_tllist [code]:
  "TLList.tconcat' b (Lazy_tllist xss) =
  Lazy_tllist (λ_. case xss () of Inr b' ⇒ Inr b' | Inl (xs, xss') ⇒ force (lappendt xs (TLList.tconcat' b xss')))"
by(simp split: tllist.split)

declare [[code drop: tllist_all2]]

lemma tllist_all2_Lazy_tllist [code]:
  "tllist_all2 P Q (Lazy_tllist xs) (Lazy_tllist ys) ⟷
  (case xs () of 
    Inr b ⇒ (case ys () of Inr b' ⇒ Q b b' | Inl _ ⇒ False)
  | Inl (x, xs') ⇒ (case ys () of Inr _ ⇒ False | Inl (y, ys') ⇒ P x y ∧ tllist_all2 P Q xs' ys'))"
by(simp add: tllist_all2_TNil1 tllist_all2_TNil2)

declare [[code drop: llist_of_tllist]]

lemma llist_of_tllist_Lazy_tllist [code]:
  "llist_of_tllist (Lazy_tllist xs) =
  Lazy_llist (λ_. case xs () of Inl (x, ys) ⇒ Some (x, llist_of_tllist ys) | Inr b ⇒ None)"
by(simp add: Lazy_llist_def)

declare [[code drop: tnth]]

lemma tnth_Lazy_tllist [code]:
  "tnth (Lazy_tllist xs) n =
  (case xs () of Inr b ⇒ undefined n | Inl (x, ys) ⇒ if n = 0 then x else tnth ys (n - 1))"
by(cases n)(auto simp add: tnth_TNil)

declare [[code drop: gen_tlength]]

lemma gen_tlength_Lazy_tllist [code]:
  "gen_tlength n (Lazy_tllist xs) =
  (case xs () of Inr b ⇒ enat n | Inl (_, xs') ⇒ gen_tlength (n + 1) xs')"
by(simp add: gen_tlength_code)

declare [[code drop: tdropn]]

lemma tdropn_Lazy_tllist [code]:
  "tdropn n (Lazy_tllist xs) =
  Lazy_tllist (λ_. if n = 0 then xs () else case xs () of Inr b ⇒ Inr b | Inl (x, xs') ⇒ force (tdropn (n - 1) xs'))"
by(cases n)(auto split: tllist.split)

declare Lazy_tllist_def [simp del]
declare sum.splits [split del]

text ‹Simple ML test for laziness›

ML_val ‹
  val zeros = @{code unfold_tllist} (K false) (K 0) (K 0) I ();
  val thd = @{code thd} zeros;
  val ttl = @{code ttl} zeros;
  val ttl' = @{code force} ttl;
  
  val tdropn = @{code tdropn} (@{code Suc} @{code "0::nat"}) zeros;
  
  val tfilter = @{code tfilter} 1 (K false) zeros;
›

hide_const (open) force

end