adaptions to codegen_package
authorhaftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 188519502ce541f01
parent 18850 92ef83e5eaea
child 18852 f1e2602ca7ba
adaptions to codegen_package
src/HOL/Library/EfficientNat.thy
src/HOL/Library/ExecutableSet.thy
src/HOL/Orderings.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Library/EfficientNat.thy	Mon Jan 30 08:20:06 2006 +0100
     1.2 +++ b/src/HOL/Library/EfficientNat.thy	Mon Jan 30 08:20:56 2006 +0100
     1.3 @@ -51,26 +51,26 @@
     1.4  *}
     1.5    int ("(_)")
     1.6  
     1.7 -(* code_syntax_tyco nat
     1.8 -  ml (target_atom "InfInt.int")
     1.9 +code_primconst nat
    1.10 +ml {*
    1.11 +fun nat i = if i < 0 then 0 : IntInf.int else i;
    1.12 +*}
    1.13 +haskell {*
    1.14 +nat i = if i < 0 then 0 else i
    1.15 +*}
    1.16 +
    1.17 +code_syntax_tyco nat
    1.18 +  ml (target_atom "IntInf.int")
    1.19    haskell (target_atom "Integer")
    1.20  
    1.21  code_syntax_const 0 :: nat
    1.22 -  ml ("0 : InfInt.int")
    1.23 +  ml (target_atom "(0:IntInf.int)")
    1.24    haskell (target_atom "0")
    1.25  
    1.26  code_syntax_const Suc
    1.27    ml (infixl 8 "_ + 1")
    1.28    haskell (infixl 6 "_ + 1")
    1.29  
    1.30 -code_primconst nat
    1.31 -ml {*
    1.32 -fun nat i = if i < 0 then 0 else i;
    1.33 -*}
    1.34 -haskell {*
    1.35 -nat i = if i < 0 then 0 else i
    1.36 -*} *)
    1.37 -
    1.38  text {*
    1.39  Case analysis on natural numbers is rephrased using a conditional
    1.40  expression:
     2.1 --- a/src/HOL/Library/ExecutableSet.thy	Mon Jan 30 08:20:06 2006 +0100
     2.2 +++ b/src/HOL/Library/ExecutableSet.thy	Mon Jan 30 08:20:56 2006 +0100
     2.3 @@ -62,7 +62,7 @@
     2.4  fun Ball S P = Library.forall P S;
     2.5  *}
     2.6  
     2.7 -code_generate ("op mem")
     2.8 +code_generate "op mem"
     2.9  
    2.10  code_primconst "insert"
    2.11    depending_on ("List.const.member")
    2.12 @@ -77,8 +77,9 @@
    2.13  *}
    2.14  
    2.15  code_primconst "op Un"
    2.16 -  depending_on ("List.const.insert")
    2.17 +  depending_on ("Set.const.insert")
    2.18  ml {*
    2.19 +nonfix union;
    2.20  fun union xs [] = xs
    2.21    | union [] ys = ys
    2.22    | union (x::xs) ys = union xs (insert x ys);
    2.23 @@ -92,6 +93,7 @@
    2.24  code_primconst "op Int"
    2.25    depending_on ("List.const.member")
    2.26  ml {*
    2.27 +nonfix inter;
    2.28  fun inter [] ys = []
    2.29    | inter (x::xs) ys =
    2.30        if List.member x ys
    2.31 @@ -139,32 +141,32 @@
    2.32    img xs (y:ys) = img (insert (f y) xs) ys;
    2.33  *}
    2.34  
    2.35 +code_primconst "INTER"
    2.36 +  depending_on ("Set.const.inter")
    2.37 +ml {*
    2.38 +fun INTER [] f = []
    2.39 +  | INTER (x::xs) f = inter (f x) (INTER xs f);
    2.40 +*}
    2.41 +haskell {*
    2.42 +INTER [] f = []
    2.43 +INTER (x:xs) f = inter (f x) (INTER xs f);
    2.44 +*}
    2.45 +
    2.46  code_primconst "UNION"
    2.47 -  depending_on ("List.const.union")
    2.48 +  depending_on ("Set.const.union")
    2.49  ml {*
    2.50  fun UNION [] f = []
    2.51 -  | UNION (x::xs) f = union (f x) (UNION xs);
    2.52 +  | UNION (x::xs) f = union (f x) (UNION xs f);
    2.53  *}
    2.54  haskell {*
    2.55  UNION [] f = []
    2.56 -UNION (x:xs) f = union (f x) (UNION xs);
    2.57 -*}
    2.58 -
    2.59 -code_primconst "INTER"
    2.60 -  depending_on ("List.const.inter")
    2.61 -ml {*
    2.62 -fun INTER [] f = []
    2.63 -  | INTER (x::xs) f = inter (f x) (INTER xs);
    2.64 -*}
    2.65 -haskell {*
    2.66 -INTER [] f = []
    2.67 -INTER (x:xs) f = inter (f x) (INTER xs);
    2.68 +UNION (x:xs) f = union (f x) (UNION xs f);
    2.69  *}
    2.70  
    2.71  code_primconst "Ball"
    2.72  ml {*
    2.73  fun Ball [] f = true
    2.74 -  | Ball (x::xs) f = f x andalso Ball f xs;
    2.75 +  | Ball (x::xs) f = f x andalso Ball xs f;
    2.76  *}
    2.77  haskell {*
    2.78  Ball = all . flip
    2.79 @@ -173,7 +175,7 @@
    2.80  code_primconst "Bex"
    2.81  ml {*
    2.82  fun Bex [] f = false
    2.83 -  | Bex (x::xs) f = f x orelse Bex f xs;
    2.84 +  | Bex (x::xs) f = f x orelse Bex xs f;
    2.85  *}
    2.86  haskell {*
    2.87  Ball = any . flip
     3.1 --- a/src/HOL/Orderings.thy	Mon Jan 30 08:20:06 2006 +0100
     3.2 +++ b/src/HOL/Orderings.thy	Mon Jan 30 08:20:56 2006 +0100
     3.3 @@ -706,7 +706,7 @@
     3.4  subsection {* Code generator setup *}
     3.5  
     3.6  code_alias
     3.7 -  "op <=" "Orderings.op_le"
     3.8 -  "op <" "Orderings.op_lt"
     3.9 +  "op <=" "IntDef.op_le"
    3.10 +  "op <" "IntDef.op_lt"
    3.11  
    3.12  end
     4.1 --- a/src/HOL/Set.thy	Mon Jan 30 08:20:06 2006 +0100
     4.2 +++ b/src/HOL/Set.thy	Mon Jan 30 08:20:56 2006 +0100
     4.3 @@ -2244,4 +2244,10 @@
     4.4    ord_eq_less_trans
     4.5    trans
     4.6  
     4.7 +subsection {* Code generator setup *}
     4.8 +
     4.9 +code_alias
    4.10 +  "op Int" "Set.inter"
    4.11 +  "op Un" "Set.union"
    4.12 +
    4.13  end