added examples for nested let
authorhaftmann
Wed Oct 11 09:33:18 2006 +0200 (2006-10-11)
changeset 209685294baa98468
parent 20967 1df105407f87
child 20969 341808e0b7f2
added examples for nested let
src/HOL/ex/Codegenerator.thy
     1.1 --- a/src/HOL/ex/Codegenerator.thy	Wed Oct 11 08:57:47 2006 +0200
     1.2 +++ b/src/HOL/ex/Codegenerator.thy	Wed Oct 11 09:33:18 2006 +0200
     1.3 @@ -42,11 +42,13 @@
     1.4    k :: "int"
     1.5    "k = -42"
     1.6  
     1.7 -consts
     1.8 -  fac :: "int => int"
     1.9 +function
    1.10 +  fac :: "int => int" where
    1.11 +  "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
    1.12 +  by pat_completeness auto
    1.13 +termination by (auto_term "measure nat")
    1.14  
    1.15 -recdef fac "measure nat"
    1.16 -  "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
    1.17 +declare fac.simps [code]
    1.18  
    1.19  subsection {* sums *}
    1.20  
    1.21 @@ -84,6 +86,17 @@
    1.22  definition
    1.23    "mystring = ''my home is my castle''"
    1.24  
    1.25 +subsection {* nested lets and such *}
    1.26 +
    1.27 +definition
    1.28 +  "abs_let x = (let (y, z) = x in (\<lambda>u. case u of () \<Rightarrow> (y + y)))"
    1.29 +
    1.30 +definition
    1.31 +  "nested_let x = (let (y, z) = x in let w = y z in w * w)"
    1.32 +
    1.33 +definition
    1.34 +  "case_let x = (let (y, z) = x in case y of () => z)"
    1.35 +
    1.36  subsection {* heavy usage of names *}
    1.37  
    1.38  definition
    1.39 @@ -151,6 +164,8 @@
    1.40    f g h
    1.41  code_gen
    1.42    apply_tower Codegenerator.keywords shadow
    1.43 +code_gen
    1.44 +  abs_let nested_let case_let
    1.45  code_gen "0::int" "1::int"
    1.46    (SML) (Haskell)
    1.47  code_gen n