src/HOL/ex/Codegenerator.thy
changeset 20936 dc5dc0e55938
parent 20807 bd3b60f9a343
child 20952 070d176a8e2d
     1.1 --- a/src/HOL/ex/Codegenerator.thy	Tue Oct 10 09:17:21 2006 +0200
     1.2 +++ b/src/HOL/ex/Codegenerator.thy	Tue Oct 10 09:17:22 2006 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Test and Examples for code generator *}
     1.5  
     1.6  theory Codegenerator
     1.7 -imports Main Records
     1.8 +imports (*"~~/src/codegen/CodegenSetup"*) Main Records
     1.9  begin
    1.10  
    1.11  subsection {* booleans *}
    1.12 @@ -28,6 +28,14 @@
    1.13    appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b"
    1.14    "appl p = (let (f, x) = p in f x)"
    1.15  
    1.16 +lemma [code]:
    1.17 +  "swap (x, y) = (y, x)"
    1.18 +  unfolding swap_def Let_def by auto
    1.19 +
    1.20 +lemma [code]:
    1.21 +  "appl (f, x) = f x"
    1.22 +  unfolding appl_def Let_def by auto
    1.23 +
    1.24  subsection {* integers *}
    1.25  
    1.26  definition
    1.27 @@ -87,9 +95,9 @@
    1.28    "h = g"
    1.29  
    1.30  code_constname
    1.31 -  f "Mymod.f"
    1.32 -  g "Mymod.A.f"
    1.33 -  h "Mymod.A.B.f"
    1.34 +  f "MymodA.f"
    1.35 +  g "MymodB.f"
    1.36 +  h "MymodC.f"
    1.37  
    1.38  definition
    1.39    "apply_tower = (\<lambda>x. x (\<lambda>x. x (\<lambda>x. x)))"
    1.40 @@ -109,12 +117,6 @@
    1.41    "0::nat" "1::nat"
    1.42  code_gen
    1.43    Pair fst snd Let split swap
    1.44 -code_gen "0::int" "1::int"
    1.45 -  (SML) (Haskell)
    1.46 -code_gen n
    1.47 -  (SML) (Haskell)
    1.48 -code_gen fac
    1.49 -  (SML) (Haskell)
    1.50  code_gen
    1.51    "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.52    "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.53 @@ -124,17 +126,6 @@
    1.54  code_gen
    1.55    appl
    1.56  code_gen
    1.57 -  k
    1.58 -  "op + :: int \<Rightarrow> int \<Rightarrow> int"
    1.59 -  "op - :: int \<Rightarrow> int \<Rightarrow> int"
    1.60 -  "op * :: int \<Rightarrow> int \<Rightarrow> int"
    1.61 -  "op < :: int \<Rightarrow> int \<Rightarrow> bool"
    1.62 -  "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
    1.63 -  fac
    1.64 -  "op div :: int \<Rightarrow> int \<Rightarrow> int"
    1.65 -  "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
    1.66 -  (SML) (Haskell)
    1.67 -code_gen
    1.68    Inl Inr
    1.69  code_gen
    1.70    None Some
    1.71 @@ -155,6 +146,29 @@
    1.72  code_gen
    1.73    foo1 foo3
    1.74  code_gen
    1.75 +  mystring
    1.76 +code_gen
    1.77 +  f g h
    1.78 +code_gen
    1.79 +  apply_tower Codegenerator.keywords shadow
    1.80 +code_gen "0::int" "1::int"
    1.81 +  (SML) (Haskell)
    1.82 +code_gen n
    1.83 +  (SML) (Haskell)
    1.84 +code_gen fac
    1.85 +  (SML) (Haskell)
    1.86 +code_gen
    1.87 +  k
    1.88 +  "op + :: int \<Rightarrow> int \<Rightarrow> int"
    1.89 +  "op - :: int \<Rightarrow> int \<Rightarrow> int"
    1.90 +  "op * :: int \<Rightarrow> int \<Rightarrow> int"
    1.91 +  "op < :: int \<Rightarrow> int \<Rightarrow> bool"
    1.92 +  "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
    1.93 +  fac
    1.94 +  "op div :: int \<Rightarrow> int \<Rightarrow> int"
    1.95 +  "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
    1.96 +  (SML) (Haskell)
    1.97 +code_gen
    1.98    "OperationalEquality.eq :: bool \<Rightarrow> bool \<Rightarrow> bool"
    1.99    "OperationalEquality.eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
   1.100    "OperationalEquality.eq :: int \<Rightarrow> int \<Rightarrow> bool"
   1.101 @@ -165,12 +179,6 @@
   1.102    "OperationalEquality.eq :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
   1.103    "OperationalEquality.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
   1.104    "OperationalEquality.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
   1.105 -code_gen
   1.106 -  mystring
   1.107 -code_gen
   1.108 -  f g h
   1.109 -code_gen
   1.110 -  apply_tower Codegenerator.keywords shadow
   1.111  
   1.112  code_gen (SML -)
   1.113