# HG changeset patch # User haftmann # Date 1150279992 -7200 # Node ID 2b4c09941e0466395d4319bd19030af8e80785fa # Parent e3a03f1f54eb12e8f4d21d9df95345bac0aa5e43 slight adaptions diff -r e3a03f1f54eb -r 2b4c09941e04 src/HOL/ex/Classpackage.thy --- a/src/HOL/ex/Classpackage.thy Wed Jun 14 12:12:37 2006 +0200 +++ b/src/HOL/ex/Classpackage.thy Wed Jun 14 12:13:12 2006 +0200 @@ -314,9 +314,9 @@ "x = ((2::nat) \ \ \ 3, (2::int) \ \ \ \
3, [1::nat, 2] \ \ \ [1, 2, 3])" "y = (2 :: int, \
2 :: int) \ \ \ (3, \
3)" -code_generate "op \" "\" "inv" -code_generate x -code_generate y +code_generate (ml, haskell) "op \" "\" "inv" +code_generate (ml, haskell) x +code_generate (ml, haskell) y code_serialize ml (-) diff -r e3a03f1f54eb -r 2b4c09941e04 src/HOL/ex/Codegenerator.thy --- a/src/HOL/ex/Codegenerator.thy Wed Jun 14 12:12:37 2006 +0200 +++ b/src/HOL/ex/Codegenerator.thy Wed Jun 14 12:13:12 2006 +0200 @@ -14,7 +14,7 @@ xor :: "bool \ bool \ bool" "xor p q = ((p | q) & \ (p & q))" -code_generate (ml) xor +code_generate (ml, haskell) xor subsection {* natural numbers *} @@ -24,9 +24,9 @@ n :: nat "n = 42" -code_generate (ml) n +code_generate (ml, haskell) n -code_generate (ml) +code_generate (ml, haskell) "0::nat" "one" n "op + :: nat \ nat \ nat" "op - :: nat \ nat \ nat" @@ -44,7 +44,7 @@ appl :: "('a \ 'b) * 'a \ 'b" "appl p = (let (f, x) = p in f x)" -code_generate (ml) Pair fst snd Let split swap swapp appl +code_generate (ml, haskell) Pair fst snd Let split swap swapp appl definition k :: "int" @@ -56,7 +56,7 @@ recdef fac "measure nat" "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))" -code_generate (ml) +code_generate (ml, haskell) "0::int" k "op + :: int \ int \ int" "op - :: int \ int \ int" @@ -67,11 +67,11 @@ subsection {* sums *} -code_generate (ml) Inl Inr +code_generate (ml, haskell) Inl Inr subsection {* options *} -code_generate (ml) None Some +code_generate (ml, haskell) None Some subsection {* lists *} @@ -81,7 +81,7 @@ qs :: "nat list" "qs == rev ps" -code_generate (ml) hd tl "op @" ps qs +code_generate (ml, haskell) hd tl "op @" ps qs subsection {* mutual datatypes *} @@ -98,11 +98,11 @@ "mut2 mut2.Tip = mut2.Tip" "mut2 (mut2.Top x) = mut2.Top (mut1 x)" -code_generate (ml) mut1 mut2 +code_generate (ml, haskell) mut1 mut2 subsection {* equalities *} -code_generate (ml) +code_generate (ml, haskell) "op = :: bool \ bool \ bool" "op = :: nat \ nat \ bool" "op = :: int \ int \ bool" @@ -129,7 +129,7 @@ "Codegenerator.g" "Mymod.A.f" "Codegenerator.h" "Mymod.A.B.f" -code_generate (ml) f g h +code_generate (ml, haskell) f g h code_serialize ml (-)