Theory Coinductive.Lazy_LList

(*  Title:       Lazy_LList.thy
    Author:      Andreas Lochbihler
*)
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 ― ‹Restore consistency in code equations between @{const partial_term_of} and @{const narrowing} for @{typ "'a llist"}›
   [[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