src/HOL/ex/Codegenerator.thy
changeset 19888 2b4c09941e04
parent 19817 bb16bf9ae3fd
child 20187 af47971ea304
     1.1 --- a/src/HOL/ex/Codegenerator.thy	Wed Jun 14 12:12:37 2006 +0200
     1.2 +++ b/src/HOL/ex/Codegenerator.thy	Wed Jun 14 12:13:12 2006 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4    xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
     1.5    "xor p q = ((p | q) & \<not> (p & q))"
     1.6  
     1.7 -code_generate (ml) xor
     1.8 +code_generate (ml, haskell) xor
     1.9  
    1.10  subsection {* natural numbers *}
    1.11  
    1.12 @@ -24,9 +24,9 @@
    1.13    n :: nat
    1.14    "n = 42"
    1.15  
    1.16 -code_generate (ml) n
    1.17 +code_generate (ml, haskell) n
    1.18  
    1.19 -code_generate (ml)
    1.20 +code_generate (ml, haskell)
    1.21    "0::nat" "one" n
    1.22    "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.23    "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.24 @@ -44,7 +44,7 @@
    1.25    appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b"
    1.26    "appl p = (let (f, x) = p in f x)"
    1.27  
    1.28 -code_generate (ml) Pair fst snd Let split swap swapp appl
    1.29 +code_generate (ml, haskell) Pair fst snd Let split swap swapp appl
    1.30  
    1.31  definition
    1.32    k :: "int"
    1.33 @@ -56,7 +56,7 @@
    1.34  recdef fac "measure nat"
    1.35    "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
    1.36  
    1.37 -code_generate (ml)
    1.38 +code_generate (ml, haskell)
    1.39    "0::int" k
    1.40    "op + :: int \<Rightarrow> int \<Rightarrow> int"
    1.41    "op - :: int \<Rightarrow> int \<Rightarrow> int"
    1.42 @@ -67,11 +67,11 @@
    1.43  
    1.44  subsection {* sums *}
    1.45  
    1.46 -code_generate (ml) Inl Inr
    1.47 +code_generate (ml, haskell) Inl Inr
    1.48  
    1.49  subsection {* options *}
    1.50  
    1.51 -code_generate (ml) None Some
    1.52 +code_generate (ml, haskell) None Some
    1.53  
    1.54  subsection {* lists *}
    1.55  
    1.56 @@ -81,7 +81,7 @@
    1.57    qs :: "nat list"
    1.58    "qs == rev ps"
    1.59  
    1.60 -code_generate (ml) hd tl "op @" ps qs
    1.61 +code_generate (ml, haskell) hd tl "op @" ps qs
    1.62  
    1.63  subsection {* mutual datatypes *}
    1.64  
    1.65 @@ -98,11 +98,11 @@
    1.66    "mut2 mut2.Tip = mut2.Tip"
    1.67    "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
    1.68  
    1.69 -code_generate (ml) mut1 mut2
    1.70 +code_generate (ml, haskell) mut1 mut2
    1.71  
    1.72  subsection {* equalities *}
    1.73  
    1.74 -code_generate (ml)
    1.75 +code_generate (ml, haskell)
    1.76    "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
    1.77    "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
    1.78    "op = :: int \<Rightarrow> int \<Rightarrow> bool"
    1.79 @@ -129,7 +129,7 @@
    1.80    "Codegenerator.g" "Mymod.A.f"
    1.81    "Codegenerator.h" "Mymod.A.B.f"
    1.82  
    1.83 -code_generate (ml) f g h
    1.84 +code_generate (ml, haskell) f g h
    1.85  
    1.86  code_serialize ml (-)
    1.87