Theory Locale_Code_Ex

section ‹Example for locale-code›
theory Locale_Code_Ex
imports 
  Locale_Code   
  "../../Lib/Code_Target_ICF"
begin

definition [simp, code del]: "NOCODE ≡ id"

locale test = 
  fixes a b :: nat
  assumes "a=b"
begin
  text ‹Mutually recursive functions›
  fun g and f where
    "g 0 = NOCODE a"
  | "g (Suc n) = a + n + f n"
  | "f 0 = a+b"
  | "f (Suc n) = a + f n + b * f n + g n"

  text ‹Various definitions, depending on more or less parameters›
  definition "k x ≡ b + x :: nat"
  definition "j x y ≡ NOCODE x + y + f x :: nat"
  definition "i x y ≡ x + y :: nat"
  definition "h x y ≡ a+x+k y+i x y+j x y"

  lemmas "defs" = k_def j_def i_def h_def g.simps f.simps 

  lemma j_alt: "j x y ≡ f x + y + x" unfolding j_def by (simp add: ac_simps)

  lemma g_alt:
    "g 0 = a"
    "g (Suc n) = f n + n + a"
    by (auto simp: ac_simps)


  definition "c ≡ a + b"

  local_setup ‹Locale_Code.lc_decl_eq @{thms j_alt}›
  local_setup ‹Locale_Code.lc_decl_eq @{thms g_alt}›

end

text ‹Conflicting constant name›
definition "h_zero_zero ≡ True"

setup Locale_Code.open_block
  text ‹Various interpretations, with and without constructor patterns 
    and free variables›
  interpretation i0: test 0 0 apply unfold_locales by auto
  interpretation i1: test "Suc n" "Suc n" apply unfold_locales by auto
  interpretation i2: test 1 1 apply unfold_locales by auto
  interpretation i3: test 5 5 apply unfold_locales by auto
  interpretation i4: test "snd (x,3)" "1+2" apply unfold_locales by auto

  interpretation i5: test "i3.c" "i3.c" by unfold_locales simp

  text ‹Setup some alternative equations›
  lemma i0_f_pat: 
    "i0.f 0 = 0"
    "i0.f (Suc n) = i0.f n + i0.g n"
    by simp_all

  lemma i0_h_pat: "i0.h x y = x+i0.k y+i0.i x y+i0.j x y" 
    unfolding i0.h_def by auto

  declare [[ lc_add "i0.f" i0_f_pat and "i0.h" i0_h_pat]]
setup Locale_Code.close_block

definition "foo x y ≡ i0.h x y + i1.h x x y + i2.h x y + i3.h x y 
  + i4.h TYPE(bool) h_zero_zero x y + i5.h x y"

definition "bar x y ≡ i0.f x + i1.f x y + i2.f x + i3.f y 
  + i4.f TYPE(bool) False x + i5.f y"

code_thms foo
code_thms bar

text ‹value›
value "foo 3 4"
value "bar 3 4"

text ‹eval-tactic›
lemma "foo 3 4 = 34578" by eval
lemma "bar 3 4 = 354189" by eval

text ‹Exported code›
export_code foo bar checking SML
export_code foo bar checking OCaml?
export_code foo bar checking Haskell?
export_code foo bar checking Scala

text ‹Inlined code›
ML_val ‹
  @{code foo} (@{code nat_of_integer} 3) (@{code nat_of_integer} 4);
  @{code bar} (@{code nat_of_integer} 3) (@{code nat_of_integer} 4);
›

end