code literals: distinguish numeral classes by different entries

--- a/src/HOL/Code_Numeral.thy	Fri Jan 22 13:38:28 2010 +0100
+++ b/src/HOL/Code_Numeral.thy	Fri Jan 22 13:38:28 2010 +0100
@@ -296,15 +296,14 @@
 
 setup {*
   fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
-    false false Code_Printer.str) ["SML", "Haskell"]
+    false Code_Printer.literal_naive_numeral) ["SML", "Haskell"]
   #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
-    false true Code_Printer.str "OCaml"
+    false Code_Printer.literal_numeral "OCaml"
   #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
-    false false Code_Printer.str "Scala"
+    false Code_Printer.literal_naive_numeral "Scala"
 *}
 
 code_reserved SML Int int
-code_reserved OCaml Big_int
 code_reserved Scala Int
 
 code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"

--- a/src/HOL/Library/Code_Integer.thy	Fri Jan 22 13:38:28 2010 +0100
+++ b/src/HOL/Library/Code_Integer.thy	Fri Jan 22 13:38:28 2010 +0100
@@ -25,9 +25,9 @@
 
 setup {*
   fold (Numeral.add_code @{const_name number_int_inst.number_of_int}
-    true true Code_Printer.str) ["SML", "OCaml", "Haskell", "Scala"]
+    true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
   #> Numeral.add_code @{const_name number_int_inst.number_of_int}
-    true true (fn s => (Pretty.block o map Code_Printer.str) ["BigInt", s]) "Scala"
+    true Code_Printer.literal_numeral "Scala"
 *}
 
 code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1"
@@ -88,7 +88,7 @@
 code_const pdivmod
   (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)")
   (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
-  (Haskell "divMod/ (abs _)/ (abs _))")
+  (Haskell "divMod/ (abs _)/ (abs _)")
   (Scala "!(_.abs '/% _.abs)")
 
 code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
@@ -113,10 +113,7 @@
   (SML "IntInf.fromInt")
   (OCaml "_")
   (Haskell "toEnum")
-  (Scala "!BigInt(_)")
-
-code_reserved SML IntInf
-code_reserved Scala BigInt
+  (Scala "!BigInt((_))")
 
 text {* Evaluation *}
 

--- a/src/HOL/Library/Efficient_Nat.thy	Fri Jan 22 13:38:28 2010 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Fri Jan 22 13:38:28 2010 +0100
@@ -287,6 +287,8 @@
 code_reserved Haskell Nat
 
 code_include Scala "Nat" {*
+import scala.Math
+
 object Nat {
 
   def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
@@ -309,7 +311,9 @@
   def equals(that: Nat): Boolean = this.value == that.value
 
   def as_BigInt: BigInt = this.value
-  def as_Int: Int = this.value
+  def as_Int: Int = if (this.value >= Math.MAX_INT && this.value <= Math.MAX_INT)
+      this.value.intValue
+    else error("Int value too big:" + this.value.toString)
 
   def +(that: Nat): Nat = new Nat(this.value + that.value)
   def -(that: Nat): Nat = Nat(this.value + that.value)
@@ -348,9 +352,9 @@
 
 setup {*
   fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat}
-    false true Code_Printer.str) ["SML", "OCaml", "Haskell"]
+    false Code_Printer.literal_positive_numeral) ["SML", "OCaml", "Haskell"]
   #> Numeral.add_code @{const_name number_nat_inst.number_of_nat}
-    false true (fn s => (Pretty.block o map Code_Printer.str) ["Nat.Nat", s]) "Scala"
+    false Code_Printer.literal_positive_numeral "Scala"
 *}
 
 text {*

--- a/src/HOL/Tools/numeral.ML	Fri Jan 22 13:38:28 2010 +0100
+++ b/src/HOL/Tools/numeral.ML	Fri Jan 22 13:38:28 2010 +0100
@@ -8,7 +8,7 @@
 sig
   val mk_cnumeral: int -> cterm
   val mk_cnumber: ctyp -> int -> cterm
-  val add_code: string -> bool -> bool -> (string -> Pretty.T) -> string -> theory -> theory
+  val add_code: string -> bool -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory
 end;
 
 structure Numeral: NUMERAL =
@@ -56,7 +56,7 @@
 
 local open Basic_Code_Thingol in
 
-fun add_code number_of negative unbounded print target thy =
+fun add_code number_of negative print target thy =
   let
     fun dest_numeral pls' min' bit0' bit1' thm =
       let
@@ -74,8 +74,7 @@
           | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
       in dest_num end;
     fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] =
-      (print o Code_Printer.literal_numeral literals unbounded
-        o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
+      (Code_Printer.str o print literals o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
   in
     thy |> Code_Target.add_syntax_const target number_of
       (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min},

--- a/src/Tools/Code/code_haskell.ML	Fri Jan 22 13:38:28 2010 +0100
+++ b/src/Tools/Code/code_haskell.ML	Fri Jan 22 13:38:28 2010 +0100
@@ -401,11 +401,14 @@
     let
       val s = ML_Syntax.print_char c;
     in if s = "'" then "\\'" else s end;
+  fun numeral_haskell k = if k >= 0 then string_of_int k
+    else Library.enclose "(" ")" (signed_string_of_int k);
 in Literals {
   literal_char = Library.enclose "'" "'" o char_haskell,
   literal_string = quote o translate_string char_haskell,
-  literal_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
-    else Library.enclose "(" ")" (signed_string_of_int k),
+  literal_numeral = numeral_haskell,
+  literal_positive_numeral = numeral_haskell,
+  literal_naive_numeral = numeral_haskell,
   literal_list = enum "," "[" "]",
   infix_cons = (5, ":")
 } end;

--- a/src/Tools/Code/code_ml.ML	Fri Jan 22 13:38:28 2010 +0100
+++ b/src/Tools/Code/code_ml.ML	Fri Jan 22 13:38:28 2010 +0100
@@ -354,9 +354,9 @@
 val literals_sml = Literals {
   literal_char = prefix "#" o quote o ML_Syntax.print_char,
   literal_string = quote o translate_string ML_Syntax.print_char,
-  literal_numeral = fn unbounded => fn k =>
-    if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)"
-    else string_of_int k,
+  literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
+  literal_positive_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
+  literal_naive_numeral = string_of_int,
   literal_list = enum "," "[" "]",
   infix_cons = (7, "::")
 };
@@ -687,18 +687,17 @@
       val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
         then chr i else c
     in s end;
-  fun bignum_ocaml k = if k <= 1073741823
-    then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
-    else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")"
+  fun numeral_ocaml k = if k < 0
+    then "(Big_int.minus_big_int " ^ numeral_ocaml (~ k) ^ ")"
+    else if k <= 1073741823
+      then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
+      else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")"
 in Literals {
   literal_char = Library.enclose "'" "'" o char_ocaml,
   literal_string = quote o translate_string char_ocaml,
-  literal_numeral = fn unbounded => fn k => if k >= 0 then
-      if unbounded then bignum_ocaml k
-      else string_of_int k
-    else
-      if unbounded then "(Big_int.minus_big_int " ^ bignum_ocaml (~ k) ^ ")"
-      else (Library.enclose "(" ")" o prefix "-" o string_of_int o op ~) k,
+  literal_numeral = numeral_ocaml,
+  literal_positive_numeral = numeral_ocaml,
+  literal_naive_numeral = numeral_ocaml,
   literal_list = enum ";" "[" "]",
   infix_cons = (6, "::")
 } end;
@@ -975,7 +974,7 @@
       ]))
   #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
   #> fold (Code_Target.add_reserved target_SML)
-      ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)]
+      ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*), "IntInf"]
   #> fold (Code_Target.add_reserved target_OCaml) [
       "and", "as", "assert", "begin", "class",
       "constraint", "do", "done", "downto", "else", "end", "exception",
@@ -985,6 +984,6 @@
       "sig", "struct", "then", "to", "true", "try", "type", "val",
       "virtual", "when", "while", "with"
     ]
-  #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod"];
+  #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"];
 
 end; (*struct*)

--- a/src/Tools/Code/code_printer.ML	Fri Jan 22 13:38:28 2010 +0100
+++ b/src/Tools/Code/code_printer.ML	Fri Jan 22 13:38:28 2010 +0100
@@ -39,12 +39,15 @@
 
   type literals
   val Literals: { literal_char: string -> string, literal_string: string -> string,
-        literal_numeral: bool -> int -> string,
+        literal_numeral: int -> string, literal_positive_numeral: int -> string,
+        literal_naive_numeral: int -> string,
         literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
     -> literals
   val literal_char: literals -> string -> string
   val literal_string: literals -> string -> string
-  val literal_numeral: literals -> bool -> int -> string
+  val literal_numeral: literals -> int -> string
+  val literal_positive_numeral: literals -> int -> string
+  val literal_naive_numeral: literals -> int -> string
   val literal_list: literals -> Pretty.T list -> Pretty.T
   val infix_cons: literals -> int * string
 
@@ -163,7 +166,9 @@
 datatype literals = Literals of {
   literal_char: string -> string,
   literal_string: string -> string,
-  literal_numeral: bool -> int -> string,
+  literal_numeral: int -> string,
+  literal_positive_numeral: int -> string,
+  literal_naive_numeral: int -> string,
   literal_list: Pretty.T list -> Pretty.T,
   infix_cons: int * string
 };
@@ -173,6 +178,8 @@
 val literal_char = #literal_char o dest_Literals;
 val literal_string = #literal_string o dest_Literals;
 val literal_numeral = #literal_numeral o dest_Literals;
+val literal_positive_numeral = #literal_positive_numeral o dest_Literals;
+val literal_naive_numeral = #literal_naive_numeral o dest_Literals;
 val literal_list = #literal_list o dest_Literals;
 val infix_cons = #infix_cons o dest_Literals;
 

--- a/src/Tools/Code/code_scala.ML	Fri Jan 22 13:38:28 2010 +0100
+++ b/src/Tools/Code/code_scala.ML	Fri Jan 22 13:38:28 2010 +0100
@@ -404,17 +404,18 @@
     let
       val s = ML_Syntax.print_char c;
     in if s = "'" then "\\'" else s end;
-  fun bigint_scala k = "(" ^ (if k <= 2147483647
-    then string_of_int k else quote (string_of_int k)) ^ ")"
+  fun numeral_scala k = if k < 0
+    then if k <= 2147483647 then "- " ^ string_of_int (~ k)
+      else quote ("- " ^ string_of_int (~ k))
+    else if k <= 2147483647 then string_of_int k
+      else quote (string_of_int k)
 in Literals {
   literal_char = Library.enclose "'" "'" o char_scala,
   literal_string = quote o translate_string char_scala,
-  literal_numeral = fn unbounded => fn k => if k >= 0 then
-      if unbounded then bigint_scala k
-      else Library.enclose "(" ")" (string_of_int k)
-    else
-      if unbounded then "(- " ^ bigint_scala (~ k) ^ ")"
-      else Library.enclose "(" ")" (signed_string_of_int k),
+  literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
+  literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
+  literal_naive_numeral = fn k => if k >= 0
+    then string_of_int k else "(- " ^ string_of_int (~ k) ^ ")",
   literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
   infix_cons = (6, "::")
 } end;
@@ -442,7 +443,7 @@
       "true", "type", "val", "var", "while", "with"
     ]
   #> fold (Code_Target.add_reserved target) [
-      "error", "apply", "List", "Nil"
+      "error", "apply", "List", "Nil", "BigInt"
     ];
 
 end; (*struct*)