# HG changeset patch
# User haftmann
# Date 1279987721 -7200
# Node ID 9728342bcd568402905beb4402d4e113233c9f50
# Parent  94e9302a7fd014e69bbef770fa6a9c5ebf04f890
another refinement chapter in the neverending numeral story

diff -r 94e9302a7fd0 -r 9728342bcd56 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Jul 23 18:42:46 2010 +0200
+++ b/src/HOL/Code_Numeral.thy	Sat Jul 24 18:08:41 2010 +0200
@@ -123,7 +123,7 @@
   by (rule HOL.eq_refl)
 
 
-subsection {* Indices as datatype of ints *}
+subsection {* Code numerals as datatype of ints *}
 
 instantiation code_numeral :: number
 begin
@@ -293,67 +293,74 @@
 
 subsection {* Code generator setup *}
 
-text {* Implementation of indices by bounded integers *}
+text {* Implementation of code numerals by bounded integers *}
 
 code_type code_numeral
   (SML "int")
   (OCaml "Big'_int.big'_int")
   (Haskell "Integer")
-  (Scala "Int")
+  (Scala "BigInt")
 
 code_instance code_numeral :: eq
   (Haskell -)
 
 setup {*
-  fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
-    false Code_Printer.literal_naive_numeral) ["SML", "Scala"]
+  Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
+    false Code_Printer.literal_naive_numeral "SML"
   #> fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
-    false Code_Printer.literal_numeral) ["OCaml", "Haskell"]
+    false Code_Printer.literal_numeral) ["OCaml", "Haskell", "Scala"]
 *}
 
 code_reserved SML Int int
-code_reserved Scala Int
+code_reserved Eval Integer
 
 code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   (SML "Int.+/ ((_),/ (_))")
   (OCaml "Big'_int.add'_big'_int")
   (Haskell infixl 6 "+")
   (Scala infixl 7 "+")
+  (Eval infixl 8 "+")
 
 code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   (SML "Int.max/ (_/ -/ _,/ 0 : int)")
   (OCaml "Big'_int.max'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)/ Big'_int.zero'_big'_int")
   (Haskell "max/ (_/ -/ _)/ (0 :: Integer)")
   (Scala "!(_/ -/ _).max(0)")
+  (Eval "Integer.max/ (_/ -/ _)/ 0")
 
 code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   (SML "Int.*/ ((_),/ (_))")
   (OCaml "Big'_int.mult'_big'_int")
   (Haskell infixl 7 "*")
   (Scala infixl 8 "*")
+  (Eval infixl 8 "*")
 
 code_const div_mod_code_numeral
-  (SML "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
+  (SML "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (Int.div (n, m), Int.mod (n, m)))")
   (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
   (Haskell "divMod")
-  (Scala "!((n: Int) => (m: Int) =>/ if (m == 0)/ (0, n) else/ (n '/ m, n % m))")
+  (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
+  (Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
 
 code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   (SML "!((_ : Int.int) = _)")
   (OCaml "Big'_int.eq'_big'_int")
   (Haskell infixl 4 "==")
   (Scala infixl 5 "==")
+  (Eval "!((_ : int) = _)")
 
 code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   (SML "Int.<=/ ((_),/ (_))")
   (OCaml "Big'_int.le'_big'_int")
   (Haskell infix 4 "<=")
   (Scala infixl 4 "<=")
+  (Eval infixl 6 "<=")
 
 code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   (SML "Int.</ ((_),/ (_))")
   (OCaml "Big'_int.lt'_big'_int")
   (Haskell infix 4 "<")
   (Scala infixl 4 "<")
+  (Eval infixl 6 "<")
 
 end
diff -r 94e9302a7fd0 -r 9728342bcd56 src/HOL/Library/Code_Integer.thy
--- a/src/HOL/Library/Code_Integer.thy	Fri Jul 23 18:42:46 2010 +0200
+++ b/src/HOL/Library/Code_Integer.thy	Sat Jul 24 18:08:41 2010 +0200
@@ -14,6 +14,142 @@
   operations for abstract integer operations.
 *}
 
+text {*
+  Preliminary: alternative representation of @{typ code_numeral}
+  for @{text Haskell} and @{text Scala}.
+*}
+
+code_include Haskell "Natural" {*
+newtype Natural = Natural Integer deriving (Eq, Show, Read);
+
+instance Num Natural where {
+  fromInteger k = Natural (if k >= 0 then k else 0);
+  Natural n + Natural m = Natural (n + m);
+  Natural n - Natural m = fromInteger (n - m);
+  Natural n * Natural m = Natural (n * m);
+  abs n = n;
+  signum _ = 1;
+  negate n = error "negate Natural";
+};
+
+instance Ord Natural where {
+  Natural n <= Natural m = n <= m;
+  Natural n < Natural m = n < m;
+};
+
+instance Real Natural where {
+  toRational (Natural n) = toRational n;
+};
+
+instance Enum Natural where {
+  toEnum k = fromInteger (toEnum k);
+  fromEnum (Natural n) = fromEnum n;
+};
+
+instance Integral Natural where {
+  toInteger (Natural n) = n;
+  divMod n m = quotRem n m;
+  quotRem (Natural n) (Natural m)
+    | (m == 0) = (0, Natural n)
+    | otherwise = (Natural k, Natural l) where (k, l) = quotRem n m;
+};
+*}
+
+code_reserved Haskell Natural
+
+code_include Scala "Natural" {*
+import scala.Math
+
+object Natural {
+
+  def apply(numeral: BigInt): Natural = new Natural(numeral max 0)
+  def apply(numeral: Int): Natural = Natural(BigInt(numeral))
+  def apply(numeral: String): Natural = Natural(BigInt(numeral))
+
+}
+
+class Natural private(private val value: BigInt) {
+
+  override def hashCode(): Int = this.value.hashCode()
+
+  override def equals(that: Any): Boolean = that match {
+    case that: Natural => this equals that
+    case _ => false
+  }
+
+  override def toString(): String = this.value.toString
+
+  def equals(that: Natural): Boolean = this.value == that.value
+
+  def as_BigInt: BigInt = this.value
+  def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
+      this.value.intValue
+    else this.value.intValue
+
+  def +(that: Natural): Natural = new Natural(this.value + that.value)
+  def -(that: Natural): Natural = Natural(this.value - that.value)
+  def *(that: Natural): Natural = new Natural(this.value * that.value)
+
+  def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
+    else {
+      val (k, l) = this.value /% that.value
+      (new Natural(k), new Natural(l))
+    }
+
+  def <=(that: Natural): Boolean = this.value <= that.value
+
+  def <(that: Natural): Boolean = this.value < that.value
+
+}
+*}
+
+code_reserved Scala Natural
+
+code_type code_numeral
+  (Haskell "Natural.Natural")
+  (Scala "Natural")
+
+setup {*
+  fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
+    false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"]
+*}
+
+code_instance code_numeral :: eq
+  (Haskell -)
+
+code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
+  (Haskell infixl 6 "+")
+  (Scala infixl 7 "+")
+
+code_const "op - \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
+  (Haskell infixl 6 "-")
+  (Scala infixl 7 "-")
+
+code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
+  (Haskell infixl 7 "*")
+  (Scala infixl 8 "*")
+
+code_const div_mod_code_numeral
+  (Haskell "divMod")
+  (Scala infixl 8 "/%")
+
+code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+  (Haskell infixl 4 "==")
+  (Scala infixl 5 "==")
+
+code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+  (Haskell infix 4 "<=")
+  (Scala infixl 4 "<=")
+
+code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+  (Haskell infix 4 "<")
+  (Scala infixl 4 "<")
+
+text {*
+  Setup for @{typ int} proper.
+*}
+
+
 code_type int
   (SML "IntInf.int")
   (OCaml "Big'_int.big'_int")
@@ -26,8 +162,6 @@
 setup {*
   fold (Numeral.add_code @{const_name number_int_inst.number_of_int}
     true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
-  #> Numeral.add_code @{const_name number_int_inst.number_of_int}
-    true Code_Printer.literal_numeral "Scala"
 *}
 
 code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1"
@@ -48,72 +182,82 @@
      and "!error(\"Bit0\")"
      and "!error(\"Bit1\")")
 
-
 code_const Int.pred
   (SML "IntInf.- ((_), 1)")
   (OCaml "Big'_int.pred'_big'_int")
   (Haskell "!(_/ -/ 1)")
   (Scala "!(_/ -/ 1)")
+  (Eval "!(_/ -/ 1)")
 
 code_const Int.succ
   (SML "IntInf.+ ((_), 1)")
   (OCaml "Big'_int.succ'_big'_int")
   (Haskell "!(_/ +/ 1)")
   (Scala "!(_/ +/ 1)")
+  (Eval "!(_/ +/ 1)")
 
 code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   (SML "IntInf.+ ((_), (_))")
   (OCaml "Big'_int.add'_big'_int")
   (Haskell infixl 6 "+")
   (Scala infixl 7 "+")
+  (Eval infixl 8 "+")
 
 code_const "uminus \<Colon> int \<Rightarrow> int"
   (SML "IntInf.~")
   (OCaml "Big'_int.minus'_big'_int")
   (Haskell "negate")
   (Scala "!(- _)")
+  (Eval "~/ _")
 
 code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   (SML "IntInf.- ((_), (_))")
   (OCaml "Big'_int.sub'_big'_int")
   (Haskell infixl 6 "-")
   (Scala infixl 7 "-")
+  (Eval infixl 8 "-")
 
 code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   (SML "IntInf.* ((_), (_))")
   (OCaml "Big'_int.mult'_big'_int")
   (Haskell infixl 7 "*")
   (Scala infixl 8 "*")
+  (Eval infixl 9 "*")
 
 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 _)")
-  (Scala "!(_.abs '/% _.abs)")
+  (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
+  (Eval "Integer.div'_mod/ (abs _)/ (abs _)")
 
 code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   (SML "!((_ : IntInf.int) = _)")
   (OCaml "Big'_int.eq'_big'_int")
   (Haskell infixl 4 "==")
   (Scala infixl 5 "==")
+  (Eval infixl 6 "=")
 
 code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   (SML "IntInf.<= ((_), (_))")
   (OCaml "Big'_int.le'_big'_int")
   (Haskell infix 4 "<=")
   (Scala infixl 4 "<=")
+  (Eval infixl 6 "<=")
 
 code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   (SML "IntInf.< ((_), (_))")
   (OCaml "Big'_int.lt'_big'_int")
   (Haskell infix 4 "<")
-  (Scala infixl 4 "<=")
+  (Scala infixl 4 "<")
+  (Eval infixl 6 "<")
 
 code_const Code_Numeral.int_of
   (SML "IntInf.fromInt")
   (OCaml "_")
-  (Haskell "_")
-  (Scala "!BigInt((_))")
+  (Haskell "toInteger")
+  (Scala "!_.as'_BigInt")
+  (Eval "_")
 
 text {* Evaluation *}
 
diff -r 94e9302a7fd0 -r 9728342bcd56 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Fri Jul 23 18:42:46 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Sat Jul 24 18:08:41 2010 +0200
@@ -50,19 +50,9 @@
   "n * m = nat (of_nat n * of_nat m)"
   unfolding of_nat_mult [symmetric] by simp
 
-text {* Specialized @{term "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} 
-  and @{term "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} operations. *}
-
-definition divmod_aux ::  "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
-  [code del]: "divmod_aux = divmod_nat"
-
-lemma [code]:
-  "divmod_nat n m = (if m = 0 then (0, n) else divmod_aux n m)"
-  unfolding divmod_aux_def divmod_nat_div_mod by simp
-
-lemma divmod_aux_code [code]:
-  "divmod_aux n m = (nat (of_nat n div of_nat m), nat (of_nat n mod of_nat m))"
-  unfolding divmod_aux_def divmod_nat_div_mod zdiv_int [symmetric] zmod_int [symmetric] by simp
+lemma divmod_nat_code [code]:
+  "divmod_nat n m = prod_fun nat nat (pdivmod (of_nat n) (of_nat m))"
+  by (simp add: prod_fun_def split_def pdivmod_def nat_div_distrib nat_mod_distrib divmod_nat_div_mod)
 
 lemma eq_nat_code [code]:
   "eq_class.eq n m \<longleftrightarrow> eq_class.eq (of_nat n \<Colon> int) (of_nat m)"
@@ -233,6 +223,7 @@
 code_type nat
   (SML "IntInf.int")
   (OCaml "Big'_int.big'_int")
+  (Eval "int")
 
 types_code
   nat ("int")
@@ -281,7 +272,9 @@
 instance Integral Nat where {
   toInteger (Nat n) = n;
   divMod n m = quotRem n m;
-  quotRem (Nat n) (Nat m) = (Nat k, Nat l) where (k, l) = quotRem n m;
+  quotRem (Nat n) (Nat m)
+    | (m == 0) = (0, Nat n)
+    | otherwise = (Nat k, Nat l) where (k, l) = quotRem n m;
 };
 *}
 
@@ -353,9 +346,7 @@
 
 setup {*
   fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat}
-    false Code_Printer.literal_positive_numeral) ["SML", "OCaml", "Haskell"]
-  #> Numeral.add_code @{const_name number_nat_inst.number_of_nat}
-    false Code_Printer.literal_positive_numeral "Scala"
+    false Code_Printer.literal_positive_numeral) ["SML", "OCaml", "Haskell", "Scala"]
 *}
 
 text {*
@@ -400,6 +391,7 @@
 code_const nat
   (SML "IntInf.max/ (/0,/ _)")
   (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
+  (Eval "Integer.max/ _/ 0")
 
 text {* For Haskell and Scala, things are slightly different again. *}
 
@@ -407,19 +399,21 @@
   (Haskell "toInteger" and "fromInteger")
   (Scala "!_.as'_BigInt" and "Nat")
 
-text {* Conversion from and to indices. *}
+text {* Conversion from and to code numerals. *}
 
 code_const Code_Numeral.of_nat
   (SML "IntInf.toInt")
   (OCaml "_")
-  (Haskell "toInteger")
-  (Scala "!_.as'_Int")
+  (Haskell "!(fromInteger/ ./ toInteger)")
+  (Scala "!Natural(_.as'_BigInt)")
+  (Eval "_")
 
 code_const Code_Numeral.nat_of
   (SML "IntInf.fromInt")
   (OCaml "_")
-  (Haskell "fromInteger")
-  (Scala "Nat")
+  (Haskell "!(fromInteger/ ./ toInteger)")
+  (Scala "!Nat(_.as'_BigInt)")
+  (Eval "_")
 
 text {* Using target language arithmetic operations whenever appropriate *}
 
@@ -428,6 +422,7 @@
   (OCaml "Big'_int.add'_big'_int")
   (Haskell infixl 6 "+")
   (Scala infixl 7 "+")
+  (Eval infixl 8 "+")
 
 code_const "op - \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
   (Haskell infixl 6 "-")
@@ -438,34 +433,35 @@
   (OCaml "Big'_int.mult'_big'_int")
   (Haskell infixl 7 "*")
   (Scala infixl 8 "*")
+  (Eval infixl 9 "*")
 
-code_const divmod_aux
+code_const divmod_nat
   (SML "IntInf.divMod/ ((_),/ (_))")
   (OCaml "Big'_int.quomod'_big'_int")
   (Haskell "divMod")
   (Scala infixl 8 "/%")
-
-code_const divmod_nat
-  (Haskell "divMod")
-  (Scala infixl 8 "/%")
+  (Eval "Integer.div'_mod")
 
 code_const "eq_class.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   (SML "!((_ : IntInf.int) = _)")
   (OCaml "Big'_int.eq'_big'_int")
   (Haskell infixl 4 "==")
   (Scala infixl 5 "==")
+  (Eval infixl 6 "=")
 
 code_const "op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   (SML "IntInf.<= ((_), (_))")
   (OCaml "Big'_int.le'_big'_int")
   (Haskell infix 4 "<=")
   (Scala infixl 4 "<=")
+  (Eval infixl 6 "<=")
 
 code_const "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   (SML "IntInf.< ((_), (_))")
   (OCaml "Big'_int.lt'_big'_int")
   (Haskell infix 4 "<")
   (Scala infixl 4 "<")
+  (Eval infixl 6 "<")
 
 consts_code
   "0::nat"                     ("0")
diff -r 94e9302a7fd0 -r 9728342bcd56 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Fri Jul 23 18:42:46 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Sat Jul 24 18:08:41 2010 +0200
@@ -415,6 +415,7 @@
   literal_string = quote o translate_string char_haskell,
   literal_numeral = numeral_haskell,
   literal_positive_numeral = numeral_haskell,
+  literal_alternative_numeral = numeral_haskell,
   literal_naive_numeral = numeral_haskell,
   literal_list = enum "," "[" "]",
   infix_cons = (5, ":")
diff -r 94e9302a7fd0 -r 9728342bcd56 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Fri Jul 23 18:42:46 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Sat Jul 24 18:08:41 2010 +0200
@@ -360,6 +360,7 @@
   literal_string = quote o translate_string ML_Syntax.print_char,
   literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
   literal_positive_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
+  literal_alternative_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
   literal_naive_numeral = string_of_int,
   literal_list = enum "," "[" "]",
   infix_cons = (7, "::")
@@ -702,6 +703,7 @@
   literal_string = quote o translate_string char_ocaml,
   literal_numeral = numeral_ocaml,
   literal_positive_numeral = numeral_ocaml,
+  literal_alternative_numeral = numeral_ocaml,
   literal_naive_numeral = numeral_ocaml,
   literal_list = enum ";" "[" "]",
   infix_cons = (6, "::")
diff -r 94e9302a7fd0 -r 9728342bcd56 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Fri Jul 23 18:42:46 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Sat Jul 24 18:08:41 2010 +0200
@@ -39,7 +39,9 @@
 
   type literals
   val Literals: { literal_char: string -> string, literal_string: string -> string,
-        literal_numeral: int -> string, literal_positive_numeral: int -> string,
+        literal_numeral: int -> string,
+        literal_positive_numeral: int -> string,
+        literal_alternative_numeral: int -> string,
         literal_naive_numeral: int -> string,
         literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
     -> literals
@@ -47,6 +49,7 @@
   val literal_string: literals -> string -> string
   val literal_numeral: literals -> int -> string
   val literal_positive_numeral: literals -> int -> string
+  val literal_alternative_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
@@ -171,6 +174,7 @@
   literal_string: string -> string,
   literal_numeral: int -> string,
   literal_positive_numeral: int -> string,
+  literal_alternative_numeral: int -> string,
   literal_naive_numeral: int -> string,
   literal_list: Pretty.T list -> Pretty.T,
   infix_cons: int * string
@@ -182,6 +186,7 @@
 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_alternative_numeral = #literal_alternative_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;
diff -r 94e9302a7fd0 -r 9728342bcd56 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Fri Jul 23 18:42:46 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Sat Jul 24 18:08:41 2010 +0200
@@ -402,7 +402,7 @@
     else let val k = ord c
     in if k < 32 orelse k > 126 then "\\" ^ radixstring (8, "0", k) else c end
   fun numeral_scala k = if k < 0
-    then if k <= 2147483647 then "- " ^ string_of_int (~ k)
+    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)
@@ -411,8 +411,8 @@
   literal_string = quote o translate_string char_scala,
   literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
   literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
-  literal_naive_numeral = fn k => if k >= 0
-    then string_of_int k else "(- " ^ string_of_int (~ k) ^ ")",
+  literal_alternative_numeral = fn k => "Natural(" ^ numeral_scala k ^ ")",
+  literal_naive_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
   literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
   infix_cons = (6, "::")
 } end;