1.1 --- a/src/HOL/Code_Numeral.thy	Fri Jan 22 13:38:28 2010 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Fri Jan 22 13:38:28 2010 +0100
     1.3 @@ -296,15 +296,14 @@
     1.4  
     1.5  setup {*
     1.6    fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
     1.7 -    false false Code_Printer.str) ["SML", "Haskell"]
     1.8 +    false Code_Printer.literal_naive_numeral) ["SML", "Haskell"]
     1.9    #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.10 -    false true Code_Printer.str "OCaml"
    1.11 +    false Code_Printer.literal_numeral "OCaml"
    1.12    #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.13 -    false false Code_Printer.str "Scala"
    1.14 +    false Code_Printer.literal_naive_numeral "Scala"
    1.15  *}
    1.16  
    1.17  code_reserved SML Int int
    1.18 -code_reserved OCaml Big_int
    1.19  code_reserved Scala Int
    1.20  
    1.21  code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"

     2.1 --- a/src/HOL/Library/Code_Integer.thy	Fri Jan 22 13:38:28 2010 +0100
     2.2 +++ b/src/HOL/Library/Code_Integer.thy	Fri Jan 22 13:38:28 2010 +0100
     2.3 @@ -25,9 +25,9 @@
     2.4  
     2.5  setup {*
     2.6    fold (Numeral.add_code @{const_name number_int_inst.number_of_int}
     2.7 -    true true Code_Printer.str) ["SML", "OCaml", "Haskell", "Scala"]
     2.8 +    true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
     2.9    #> Numeral.add_code @{const_name number_int_inst.number_of_int}
    2.10 -    true true (fn s => (Pretty.block o map Code_Printer.str) ["BigInt", s]) "Scala"
    2.11 +    true Code_Printer.literal_numeral "Scala"
    2.12  *}
    2.13  
    2.14  code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1"
    2.15 @@ -88,7 +88,7 @@
    2.16  code_const pdivmod
    2.17    (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)")
    2.18    (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
    2.19 -  (Haskell "divMod/ (abs _)/ (abs _))")
    2.20 +  (Haskell "divMod/ (abs _)/ (abs _)")
    2.21    (Scala "!(_.abs '/% _.abs)")
    2.22  
    2.23  code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    2.24 @@ -113,10 +113,7 @@
    2.25    (SML "IntInf.fromInt")
    2.26    (OCaml "_")
    2.27    (Haskell "toEnum")
    2.28 -  (Scala "!BigInt(_)")
    2.29 -
    2.30 -code_reserved SML IntInf
    2.31 -code_reserved Scala BigInt
    2.32 +  (Scala "!BigInt((_))")
    2.33  
    2.34  text {* Evaluation *}
    2.35  

     3.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Jan 22 13:38:28 2010 +0100
     3.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Fri Jan 22 13:38:28 2010 +0100
     3.3 @@ -287,6 +287,8 @@
     3.4  code_reserved Haskell Nat
     3.5  
     3.6  code_include Scala "Nat" {*
     3.7 +import scala.Math
     3.8 +
     3.9  object Nat {
    3.10  
    3.11    def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
    3.12 @@ -309,7 +311,9 @@
    3.13    def equals(that: Nat): Boolean = this.value == that.value
    3.14  
    3.15    def as_BigInt: BigInt = this.value
    3.16 -  def as_Int: Int = this.value
    3.17 +  def as_Int: Int = if (this.value >= Math.MAX_INT && this.value <= Math.MAX_INT)
    3.18 +      this.value.intValue
    3.19 +    else error("Int value too big:" + this.value.toString)
    3.20  
    3.21    def +(that: Nat): Nat = new Nat(this.value + that.value)
    3.22    def -(that: Nat): Nat = Nat(this.value + that.value)
    3.23 @@ -348,9 +352,9 @@
    3.24  
    3.25  setup {*
    3.26    fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat}
    3.27 -    false true Code_Printer.str) ["SML", "OCaml", "Haskell"]
    3.28 +    false Code_Printer.literal_positive_numeral) ["SML", "OCaml", "Haskell"]
    3.29    #> Numeral.add_code @{const_name number_nat_inst.number_of_nat}
    3.30 -    false true (fn s => (Pretty.block o map Code_Printer.str) ["Nat.Nat", s]) "Scala"
    3.31 +    false Code_Printer.literal_positive_numeral "Scala"
    3.32  *}
    3.33  
    3.34  text {*

     4.1 --- a/src/HOL/Tools/numeral.ML	Fri Jan 22 13:38:28 2010 +0100
     4.2 +++ b/src/HOL/Tools/numeral.ML	Fri Jan 22 13:38:28 2010 +0100
     4.3 @@ -8,7 +8,7 @@
     4.4  sig
     4.5    val mk_cnumeral: int -> cterm
     4.6    val mk_cnumber: ctyp -> int -> cterm
     4.7 -  val add_code: string -> bool -> bool -> (string -> Pretty.T) -> string -> theory -> theory
     4.8 +  val add_code: string -> bool -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory
     4.9  end;
    4.10  
    4.11  structure Numeral: NUMERAL =
    4.12 @@ -56,7 +56,7 @@
    4.13  
    4.14  local open Basic_Code_Thingol in
    4.15  
    4.16 -fun add_code number_of negative unbounded print target thy =
    4.17 +fun add_code number_of negative print target thy =
    4.18    let
    4.19      fun dest_numeral pls' min' bit0' bit1' thm =
    4.20        let
    4.21 @@ -74,8 +74,7 @@
    4.22            | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
    4.23        in dest_num end;
    4.24      fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] =
    4.25 -      (print o Code_Printer.literal_numeral literals unbounded
    4.26 -        o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
    4.27 +      (Code_Printer.str o print literals o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
    4.28    in
    4.29      thy |> Code_Target.add_syntax_const target number_of
    4.30        (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min},

     5.1 --- a/src/Tools/Code/code_haskell.ML	Fri Jan 22 13:38:28 2010 +0100
     5.2 +++ b/src/Tools/Code/code_haskell.ML	Fri Jan 22 13:38:28 2010 +0100
     5.3 @@ -401,11 +401,14 @@
     5.4      let
     5.5        val s = ML_Syntax.print_char c;
     5.6      in if s = "'" then "\\'" else s end;
     5.7 +  fun numeral_haskell k = if k >= 0 then string_of_int k
     5.8 +    else Library.enclose "(" ")" (signed_string_of_int k);
     5.9  in Literals {
    5.10    literal_char = Library.enclose "'" "'" o char_haskell,
    5.11    literal_string = quote o translate_string char_haskell,
    5.12 -  literal_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
    5.13 -    else Library.enclose "(" ")" (signed_string_of_int k),
    5.14 +  literal_numeral = numeral_haskell,
    5.15 +  literal_positive_numeral = numeral_haskell,
    5.16 +  literal_naive_numeral = numeral_haskell,
    5.17    literal_list = enum "," "[" "]",
    5.18    infix_cons = (5, ":")
    5.19  } end;

     6.1 --- a/src/Tools/Code/code_ml.ML	Fri Jan 22 13:38:28 2010 +0100
     6.2 +++ b/src/Tools/Code/code_ml.ML	Fri Jan 22 13:38:28 2010 +0100
     6.3 @@ -354,9 +354,9 @@
     6.4  val literals_sml = Literals {
     6.5    literal_char = prefix "#" o quote o ML_Syntax.print_char,
     6.6    literal_string = quote o translate_string ML_Syntax.print_char,
     6.7 -  literal_numeral = fn unbounded => fn k =>
     6.8 -    if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)"
     6.9 -    else string_of_int k,
    6.10 +  literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
    6.11 +  literal_positive_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
    6.12 +  literal_naive_numeral = string_of_int,
    6.13    literal_list = enum "," "[" "]",
    6.14    infix_cons = (7, "::")
    6.15  };
    6.16 @@ -687,18 +687,17 @@
    6.17        val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
    6.18          then chr i else c
    6.19      in s end;
    6.20 -  fun bignum_ocaml k = if k <= 1073741823
    6.21 -    then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
    6.22 -    else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")"
    6.23 +  fun numeral_ocaml k = if k < 0
    6.24 +    then "(Big_int.minus_big_int " ^ numeral_ocaml (~ k) ^ ")"
    6.25 +    else if k <= 1073741823
    6.26 +      then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
    6.27 +      else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")"
    6.28  in Literals {
    6.29    literal_char = Library.enclose "'" "'" o char_ocaml,
    6.30    literal_string = quote o translate_string char_ocaml,
    6.31 -  literal_numeral = fn unbounded => fn k => if k >= 0 then
    6.32 -      if unbounded then bignum_ocaml k
    6.33 -      else string_of_int k
    6.34 -    else
    6.35 -      if unbounded then "(Big_int.minus_big_int " ^ bignum_ocaml (~ k) ^ ")"
    6.36 -      else (Library.enclose "(" ")" o prefix "-" o string_of_int o op ~) k,
    6.37 +  literal_numeral = numeral_ocaml,
    6.38 +  literal_positive_numeral = numeral_ocaml,
    6.39 +  literal_naive_numeral = numeral_ocaml,
    6.40    literal_list = enum ";" "[" "]",
    6.41    infix_cons = (6, "::")
    6.42  } end;
    6.43 @@ -975,7 +974,7 @@
    6.44        ]))
    6.45    #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
    6.46    #> fold (Code_Target.add_reserved target_SML)
    6.47 -      ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)]
    6.48 +      ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*), "IntInf"]
    6.49    #> fold (Code_Target.add_reserved target_OCaml) [
    6.50        "and", "as", "assert", "begin", "class",
    6.51        "constraint", "do", "done", "downto", "else", "end", "exception",
    6.52 @@ -985,6 +984,6 @@
    6.53        "sig", "struct", "then", "to", "true", "try", "type", "val",
    6.54        "virtual", "when", "while", "with"
    6.55      ]
    6.56 -  #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod"];
    6.57 +  #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"];
    6.58  
    6.59  end; (*struct*)

     7.1 --- a/src/Tools/Code/code_printer.ML	Fri Jan 22 13:38:28 2010 +0100
     7.2 +++ b/src/Tools/Code/code_printer.ML	Fri Jan 22 13:38:28 2010 +0100
     7.3 @@ -39,12 +39,15 @@
     7.4  
     7.5    type literals
     7.6    val Literals: { literal_char: string -> string, literal_string: string -> string,
     7.7 -        literal_numeral: bool -> int -> string,
     7.8 +        literal_numeral: int -> string, literal_positive_numeral: int -> string,
     7.9 +        literal_naive_numeral: int -> string,
    7.10          literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
    7.11      -> literals
    7.12    val literal_char: literals -> string -> string
    7.13    val literal_string: literals -> string -> string
    7.14 -  val literal_numeral: literals -> bool -> int -> string
    7.15 +  val literal_numeral: literals -> int -> string
    7.16 +  val literal_positive_numeral: literals -> int -> string
    7.17 +  val literal_naive_numeral: literals -> int -> string
    7.18    val literal_list: literals -> Pretty.T list -> Pretty.T
    7.19    val infix_cons: literals -> int * string
    7.20  
    7.21 @@ -163,7 +166,9 @@
    7.22  datatype literals = Literals of {
    7.23    literal_char: string -> string,
    7.24    literal_string: string -> string,
    7.25 -  literal_numeral: bool -> int -> string,
    7.26 +  literal_numeral: int -> string,
    7.27 +  literal_positive_numeral: int -> string,
    7.28 +  literal_naive_numeral: int -> string,
    7.29    literal_list: Pretty.T list -> Pretty.T,
    7.30    infix_cons: int * string
    7.31  };
    7.32 @@ -173,6 +178,8 @@
    7.33  val literal_char = #literal_char o dest_Literals;
    7.34  val literal_string = #literal_string o dest_Literals;
    7.35  val literal_numeral = #literal_numeral o dest_Literals;
    7.36 +val literal_positive_numeral = #literal_positive_numeral o dest_Literals;
    7.37 +val literal_naive_numeral = #literal_naive_numeral o dest_Literals;
    7.38  val literal_list = #literal_list o dest_Literals;
    7.39  val infix_cons = #infix_cons o dest_Literals;
    7.40  

     8.1 --- a/src/Tools/Code/code_scala.ML	Fri Jan 22 13:38:28 2010 +0100
     8.2 +++ b/src/Tools/Code/code_scala.ML	Fri Jan 22 13:38:28 2010 +0100
     8.3 @@ -404,17 +404,18 @@
     8.4      let
     8.5        val s = ML_Syntax.print_char c;
     8.6      in if s = "'" then "\\'" else s end;
     8.7 -  fun bigint_scala k = "(" ^ (if k <= 2147483647
     8.8 -    then string_of_int k else quote (string_of_int k)) ^ ")"
     8.9 +  fun numeral_scala k = if k < 0
    8.10 +    then if k <= 2147483647 then "- " ^ string_of_int (~ k)
    8.11 +      else quote ("- " ^ string_of_int (~ k))
    8.12 +    else if k <= 2147483647 then string_of_int k
    8.13 +      else quote (string_of_int k)
    8.14  in Literals {
    8.15    literal_char = Library.enclose "'" "'" o char_scala,
    8.16    literal_string = quote o translate_string char_scala,
    8.17 -  literal_numeral = fn unbounded => fn k => if k >= 0 then
    8.18 -      if unbounded then bigint_scala k
    8.19 -      else Library.enclose "(" ")" (string_of_int k)
    8.20 -    else
    8.21 -      if unbounded then "(- " ^ bigint_scala (~ k) ^ ")"
    8.22 -      else Library.enclose "(" ")" (signed_string_of_int k),
    8.23 +  literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
    8.24 +  literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
    8.25 +  literal_naive_numeral = fn k => if k >= 0
    8.26 +    then string_of_int k else "(- " ^ string_of_int (~ k) ^ ")",
    8.27    literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
    8.28    infix_cons = (6, "::")
    8.29  } end;
    8.30 @@ -442,7 +443,7 @@
    8.31        "true", "type", "val", "var", "while", "with"
    8.32      ]
    8.33    #> fold (Code_Target.add_reserved target) [
    8.34 -      "error", "apply", "List", "Nil"
    8.35 +      "error", "apply", "List", "Nil", "BigInt"
    8.36      ];
    8.37  
    8.38  end; (*struct*)