1.1 --- a/src/HOL/Integ/IntDef.thy	Tue Jan 17 10:26:50 2006 +0100
     1.2 +++ b/src/HOL/Integ/IntDef.thy	Tue Jan 17 16:36:57 2006 +0100
     1.3 @@ -896,11 +896,47 @@
     1.4    "op <=" :: "int => int => bool" ("(_ <=/ _)")
     1.5    "neg"                         ("(_ < 0)")
     1.6  
     1.7 +code_syntax_tyco int
     1.8 +  ml (atom "IntInf.int")
     1.9 +  haskell (atom "Integer")
    1.10 +
    1.11 +code_syntax_const
    1.12 +  0 :: "int"
    1.13 +    ml ("0 : IntInf.int")
    1.14 +    haskell (atom "0")
    1.15 +  1 :: "int"
    1.16 +    ml ("1 : IntInf.int")
    1.17 +    haskell (atom "1")
    1.18 +
    1.19 +code_syntax_const
    1.20 +  "op +" :: "int \<Rightarrow> int \<Rightarrow> int"
    1.21 +    ml (infixl 8 "+")
    1.22 +    haskell (infixl 6 "+")
    1.23 +  "op *" :: "int \<Rightarrow> int \<Rightarrow> int"
    1.24 +    ml (infixl 9 "*")
    1.25 +    haskell (infixl 7 "*")
    1.26 +  uminus :: "int \<Rightarrow> int"
    1.27 +    ml (atom "~")
    1.28 +    haskell (atom "negate")
    1.29 +  "op <" :: "int \<Rightarrow> int \<Rightarrow> bool"
    1.30 +    ml (infix 6 "<")
    1.31 +    haskell (infix 4 "<")
    1.32 +  "op <=" :: "int \<Rightarrow> int \<Rightarrow> bool"
    1.33 +    ml (infix 6 "<=")
    1.34 +    haskell (infix 4 "<=")
    1.35 +  "neg" :: "int \<Rightarrow> bool"
    1.36 +    ml ("_ < 0")
    1.37 +    haskell ("_ < 0")
    1.38 +
    1.39  ML {*
    1.40  fun mk_int_to_nat bin =
    1.41    Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT)
    1.42    $ (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin);
    1.43  
    1.44 +fun bin_to_int bin = HOLogic.dest_binum bin
    1.45 +  handle TERM _
    1.46 +    => error ("not a number: " ^ Sign.string_of_term thy bin);
    1.47 +
    1.48  fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of",
    1.49        Type ("fun", [_, T as Type ("IntDef.int", [])])) $ bin) =
    1.50          (SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)),
    1.51 @@ -911,12 +947,14 @@
    1.52            Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $
    1.53              (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin)))
    1.54    | number_of_codegen _ _ _ _ _ _ _ = NONE;
    1.55 +
    1.56  *}
    1.57  
    1.58  setup {*[
    1.59    Codegen.add_codegen "number_of_codegen" number_of_codegen,
    1.60    CodegenPackage.add_appconst
    1.61 -    ("Numeral.number_of", ((1, 1), CodegenPackage.appgen_number_of HOLogic.dest_binum mk_int_to_nat))
    1.62 +    ("Numeral.number_of", ((1, 1), CodegenPackage.appgen_number_of mk_int_to_nat bin_to_int "IntDef.int" "nat")),
    1.63 +  CodegenPackage.set_int_tyco "IntDef.int"
    1.64  ]*}
    1.65  
    1.66  quickcheck_params [default_type = int]