# HG changeset patch # User haftmann # Date 1160464642 -7200 # Node ID dc5dc0e55938580f3847ed2eb86a8680f36e3222 # Parent f9a578316eef36f673c2bc83d894ff5a68eb6cde changed order diff -r f9a578316eef -r dc5dc0e55938 src/HOL/ex/Codegenerator.thy --- a/src/HOL/ex/Codegenerator.thy Tue Oct 10 09:17:21 2006 +0200 +++ b/src/HOL/ex/Codegenerator.thy Tue Oct 10 09:17:22 2006 +0200 @@ -5,7 +5,7 @@ header {* Test and Examples for code generator *} theory Codegenerator -imports Main Records +imports (*"~~/src/codegen/CodegenSetup"*) Main Records begin subsection {* booleans *} @@ -28,6 +28,14 @@ appl :: "('a \ 'b) * 'a \ 'b" "appl p = (let (f, x) = p in f x)" +lemma [code]: + "swap (x, y) = (y, x)" + unfolding swap_def Let_def by auto + +lemma [code]: + "appl (f, x) = f x" + unfolding appl_def Let_def by auto + subsection {* integers *} definition @@ -87,9 +95,9 @@ "h = g" code_constname - f "Mymod.f" - g "Mymod.A.f" - h "Mymod.A.B.f" + f "MymodA.f" + g "MymodB.f" + h "MymodC.f" definition "apply_tower = (\x. x (\x. x (\x. x)))" @@ -109,12 +117,6 @@ "0::nat" "1::nat" code_gen Pair fst snd Let split swap -code_gen "0::int" "1::int" - (SML) (Haskell) -code_gen n - (SML) (Haskell) -code_gen fac - (SML) (Haskell) code_gen "op + :: nat \ nat \ nat" "op - :: nat \ nat \ nat" @@ -124,17 +126,6 @@ code_gen appl code_gen - k - "op + :: int \ int \ int" - "op - :: int \ int \ int" - "op * :: int \ int \ int" - "op < :: int \ int \ bool" - "op <= :: int \ int \ bool" - fac - "op div :: int \ int \ int" - "op mod :: int \ int \ int" - (SML) (Haskell) -code_gen Inl Inr code_gen None Some @@ -155,6 +146,29 @@ code_gen foo1 foo3 code_gen + mystring +code_gen + f g h +code_gen + apply_tower Codegenerator.keywords shadow +code_gen "0::int" "1::int" + (SML) (Haskell) +code_gen n + (SML) (Haskell) +code_gen fac + (SML) (Haskell) +code_gen + k + "op + :: int \ int \ int" + "op - :: int \ int \ int" + "op * :: int \ int \ int" + "op < :: int \ int \ bool" + "op <= :: int \ int \ bool" + fac + "op div :: int \ int \ int" + "op mod :: int \ int \ int" + (SML) (Haskell) +code_gen "OperationalEquality.eq :: bool \ bool \ bool" "OperationalEquality.eq :: nat \ nat \ bool" "OperationalEquality.eq :: int \ int \ bool" @@ -165,12 +179,6 @@ "OperationalEquality.eq :: mut1 \ mut1 \ bool" "OperationalEquality.eq :: mut2 \ mut2 \ bool" "OperationalEquality.eq :: ('a\eq) point_scheme \ 'a point_scheme \ bool" -code_gen - mystring -code_gen - f g h -code_gen - apply_tower Codegenerator.keywords shadow code_gen (SML -)