Theory Code_Lazy_Test

(* 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 ("[]") | 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"    ("[(_)]")
translations
  "[x, xs]" == "x#[xs]"
  "[x]" == "x#[]"
  "[x]" == "CONST lazy_llist x"

definition llist :: "nat llist" where
  "llist = [1, 2, 3, hd [], 4]"

fun lnth :: "nat ⇒ 'a llist ⇒ 'a" where
  "lnth 0 (x # xs) = x"
| "lnth (Suc n) (x # 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 [] = []"
| "lfilter P (x # xs) = (if P x then x # 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 term‹llist› for term‹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"

lemma mk_tree_Suc: "mk_tree (Suc n) = mk_tree n △ 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 ‹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 _ _ _ _ = ()"

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

value [code] "f1 True False False []"
deactivate_lazy_type llist
value [code] "f1 True False False []"
declare f1_code1(1) [code del]
value [code] "f1 True False False []"
activate_lazy_type llist
value [code] "f1 True False False []"

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

value [code] "f1 True True True [0]"
declare f1_code2(1)[code del]
value [code] "f1 True True True [0]"

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

value [code] "f1 True True True [0, 1]"
declare f1_code3(1)[code del]
value [code] "f1 True True True [0, 1]"

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

value [code] "f1 True True True [0, 1, 2]"
value [code] "f1 True True False [0, 1]"
value [code] "f1 True False True [0]"
value [code] "f1 False True True []"

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

declare [[code drop: f2]]
lemma f2_code1 [code]:
  "f2 xs = Code.abort (STR ''a'') (λ_. ())"
  "f2 [[[]]] = ()"
  "f2 [[[Suc n]]] = ()"
  "f2 [[[0, Suc n]]] = ()"
  by(simp_all add: f2_def)

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

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

declare [[code drop: f3]]
lemma f3_code1 [code]:
  "f3 [] = ()"
  "f3 [A] = ()"
  by(simp_all add: f3_def)

value [code] "f3 []"
value [code] "f3 [{}]"
value [code] "f3 [UNIV]"

end