src/HOL/ex/Codegenerator.thy
changeset 20453 855f07fabd76
parent 20383 58f65fc90cf4
child 20597 65fe827aa595
     1.1 --- a/src/HOL/ex/Codegenerator.thy	Thu Aug 31 23:01:16 2006 +0200
     1.2 +++ b/src/HOL/ex/Codegenerator.thy	Fri Sep 01 08:36:51 2006 +0200
     1.3 @@ -90,21 +90,19 @@
     1.4    g "Mymod.A.f"
     1.5    h "Mymod.A.B.f"
     1.6  
     1.7 -code_generate (ml, haskell)
     1.8 -  n one "0::int" "0::nat" "1::int" "1::nat"
     1.9 -code_generate (ml, haskell)
    1.10 -  fac
    1.11 -code_generate
    1.12 -  xor
    1.13 -code_generate
    1.14 +code_gen xor
    1.15 +code_gen one "0::nat" "1::nat"
    1.16 +code_gen "0::int" "1::int" n fac
    1.17 +  (SML) (Haskell)
    1.18 +code_gen
    1.19    "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.20    "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.21    "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.22    "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
    1.23    "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
    1.24 -code_generate
    1.25 +code_gen
    1.26    Pair fst snd Let split swap swapp appl
    1.27 -code_generate (ml, haskell)
    1.28 +code_gen
    1.29    k
    1.30    "op + :: int \<Rightarrow> int \<Rightarrow> int"
    1.31    "op - :: int \<Rightarrow> int \<Rightarrow> int"
    1.32 @@ -114,15 +112,16 @@
    1.33    fac
    1.34    "op div :: int \<Rightarrow> int \<Rightarrow> int"
    1.35    "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
    1.36 -code_generate
    1.37 +  (SML) (Haskell)
    1.38 +code_gen
    1.39    Inl Inr
    1.40 -code_generate
    1.41 +code_gen
    1.42    None Some
    1.43 -code_generate
    1.44 +code_gen
    1.45    hd tl "op @" ps qs
    1.46 -code_generate
    1.47 +code_gen
    1.48    mut1 mut2
    1.49 -code_generate (ml, haskell)
    1.50 +code_gen
    1.51    "op @" filter concat foldl foldr hd tl
    1.52    last butlast list_all2
    1.53    map 
    1.54 @@ -143,9 +142,10 @@
    1.55    rotate1
    1.56    rotate
    1.57    splice
    1.58 -code_generate
    1.59 +  (SML) (Haskell)
    1.60 +code_gen
    1.61    foo1 foo3
    1.62 -code_generate (ml, haskell)
    1.63 +code_gen
    1.64    "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
    1.65    "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
    1.66    "op = :: int \<Rightarrow> int \<Rightarrow> bool"
    1.67 @@ -156,9 +156,9 @@
    1.68    "op = :: point \<Rightarrow> point \<Rightarrow> bool"
    1.69    "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
    1.70    "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
    1.71 -code_generate
    1.72 +code_gen
    1.73    f g h
    1.74  
    1.75 -code_serialize ml (-)
    1.76 +code_gen (SML -)
    1.77  
    1.78  end
    1.79 \ No newline at end of file