another refinement chapter in the neverending numeral story
authorhaftmann
Sat Jul 24 18:08:41 2010 +0200 (2010-07-24)
changeset 379589728342bcd56
parent 37948 94e9302a7fd0
child 37959 6fe5fa827f18
another refinement chapter in the neverending numeral story
src/HOL/Code_Numeral.thy
src/HOL/Library/Code_Integer.thy
src/HOL/Library/Efficient_Nat.thy
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_printer.ML
src/Tools/Code/code_scala.ML
     1.1 --- a/src/HOL/Code_Numeral.thy	Fri Jul 23 18:42:46 2010 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Sat Jul 24 18:08:41 2010 +0200
     1.3 @@ -123,7 +123,7 @@
     1.4    by (rule HOL.eq_refl)
     1.5  
     1.6  
     1.7 -subsection {* Indices as datatype of ints *}
     1.8 +subsection {* Code numerals as datatype of ints *}
     1.9  
    1.10  instantiation code_numeral :: number
    1.11  begin
    1.12 @@ -293,67 +293,74 @@
    1.13  
    1.14  subsection {* Code generator setup *}
    1.15  
    1.16 -text {* Implementation of indices by bounded integers *}
    1.17 +text {* Implementation of code numerals by bounded integers *}
    1.18  
    1.19  code_type code_numeral
    1.20    (SML "int")
    1.21    (OCaml "Big'_int.big'_int")
    1.22    (Haskell "Integer")
    1.23 -  (Scala "Int")
    1.24 +  (Scala "BigInt")
    1.25  
    1.26  code_instance code_numeral :: eq
    1.27    (Haskell -)
    1.28  
    1.29  setup {*
    1.30 -  fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.31 -    false Code_Printer.literal_naive_numeral) ["SML", "Scala"]
    1.32 +  Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.33 +    false Code_Printer.literal_naive_numeral "SML"
    1.34    #> fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.35 -    false Code_Printer.literal_numeral) ["OCaml", "Haskell"]
    1.36 +    false Code_Printer.literal_numeral) ["OCaml", "Haskell", "Scala"]
    1.37  *}
    1.38  
    1.39  code_reserved SML Int int
    1.40 -code_reserved Scala Int
    1.41 +code_reserved Eval Integer
    1.42  
    1.43  code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
    1.44    (SML "Int.+/ ((_),/ (_))")
    1.45    (OCaml "Big'_int.add'_big'_int")
    1.46    (Haskell infixl 6 "+")
    1.47    (Scala infixl 7 "+")
    1.48 +  (Eval infixl 8 "+")
    1.49  
    1.50  code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
    1.51    (SML "Int.max/ (_/ -/ _,/ 0 : int)")
    1.52    (OCaml "Big'_int.max'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)/ Big'_int.zero'_big'_int")
    1.53    (Haskell "max/ (_/ -/ _)/ (0 :: Integer)")
    1.54    (Scala "!(_/ -/ _).max(0)")
    1.55 +  (Eval "Integer.max/ (_/ -/ _)/ 0")
    1.56  
    1.57  code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
    1.58    (SML "Int.*/ ((_),/ (_))")
    1.59    (OCaml "Big'_int.mult'_big'_int")
    1.60    (Haskell infixl 7 "*")
    1.61    (Scala infixl 8 "*")
    1.62 +  (Eval infixl 8 "*")
    1.63  
    1.64  code_const div_mod_code_numeral
    1.65 -  (SML "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
    1.66 +  (SML "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (Int.div (n, m), Int.mod (n, m)))")
    1.67    (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
    1.68    (Haskell "divMod")
    1.69 -  (Scala "!((n: Int) => (m: Int) =>/ if (m == 0)/ (0, n) else/ (n '/ m, n % m))")
    1.70 +  (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
    1.71 +  (Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
    1.72  
    1.73  code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.74    (SML "!((_ : Int.int) = _)")
    1.75    (OCaml "Big'_int.eq'_big'_int")
    1.76    (Haskell infixl 4 "==")
    1.77    (Scala infixl 5 "==")
    1.78 +  (Eval "!((_ : int) = _)")
    1.79  
    1.80  code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.81    (SML "Int.<=/ ((_),/ (_))")
    1.82    (OCaml "Big'_int.le'_big'_int")
    1.83    (Haskell infix 4 "<=")
    1.84    (Scala infixl 4 "<=")
    1.85 +  (Eval infixl 6 "<=")
    1.86  
    1.87  code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.88    (SML "Int.</ ((_),/ (_))")
    1.89    (OCaml "Big'_int.lt'_big'_int")
    1.90    (Haskell infix 4 "<")
    1.91    (Scala infixl 4 "<")
    1.92 +  (Eval infixl 6 "<")
    1.93  
    1.94  end
     2.1 --- a/src/HOL/Library/Code_Integer.thy	Fri Jul 23 18:42:46 2010 +0200
     2.2 +++ b/src/HOL/Library/Code_Integer.thy	Sat Jul 24 18:08:41 2010 +0200
     2.3 @@ -14,6 +14,142 @@
     2.4    operations for abstract integer operations.
     2.5  *}
     2.6  
     2.7 +text {*
     2.8 +  Preliminary: alternative representation of @{typ code_numeral}
     2.9 +  for @{text Haskell} and @{text Scala}.
    2.10 +*}
    2.11 +
    2.12 +code_include Haskell "Natural" {*
    2.13 +newtype Natural = Natural Integer deriving (Eq, Show, Read);
    2.14 +
    2.15 +instance Num Natural where {
    2.16 +  fromInteger k = Natural (if k >= 0 then k else 0);
    2.17 +  Natural n + Natural m = Natural (n + m);
    2.18 +  Natural n - Natural m = fromInteger (n - m);
    2.19 +  Natural n * Natural m = Natural (n * m);
    2.20 +  abs n = n;
    2.21 +  signum _ = 1;
    2.22 +  negate n = error "negate Natural";
    2.23 +};
    2.24 +
    2.25 +instance Ord Natural where {
    2.26 +  Natural n <= Natural m = n <= m;
    2.27 +  Natural n < Natural m = n < m;
    2.28 +};
    2.29 +
    2.30 +instance Real Natural where {
    2.31 +  toRational (Natural n) = toRational n;
    2.32 +};
    2.33 +
    2.34 +instance Enum Natural where {
    2.35 +  toEnum k = fromInteger (toEnum k);
    2.36 +  fromEnum (Natural n) = fromEnum n;
    2.37 +};
    2.38 +
    2.39 +instance Integral Natural where {
    2.40 +  toInteger (Natural n) = n;
    2.41 +  divMod n m = quotRem n m;
    2.42 +  quotRem (Natural n) (Natural m)
    2.43 +    | (m == 0) = (0, Natural n)
    2.44 +    | otherwise = (Natural k, Natural l) where (k, l) = quotRem n m;
    2.45 +};
    2.46 +*}
    2.47 +
    2.48 +code_reserved Haskell Natural
    2.49 +
    2.50 +code_include Scala "Natural" {*
    2.51 +import scala.Math
    2.52 +
    2.53 +object Natural {
    2.54 +
    2.55 +  def apply(numeral: BigInt): Natural = new Natural(numeral max 0)
    2.56 +  def apply(numeral: Int): Natural = Natural(BigInt(numeral))
    2.57 +  def apply(numeral: String): Natural = Natural(BigInt(numeral))
    2.58 +
    2.59 +}
    2.60 +
    2.61 +class Natural private(private val value: BigInt) {
    2.62 +
    2.63 +  override def hashCode(): Int = this.value.hashCode()
    2.64 +
    2.65 +  override def equals(that: Any): Boolean = that match {
    2.66 +    case that: Natural => this equals that
    2.67 +    case _ => false
    2.68 +  }
    2.69 +
    2.70 +  override def toString(): String = this.value.toString
    2.71 +
    2.72 +  def equals(that: Natural): Boolean = this.value == that.value
    2.73 +
    2.74 +  def as_BigInt: BigInt = this.value
    2.75 +  def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
    2.76 +      this.value.intValue
    2.77 +    else this.value.intValue
    2.78 +
    2.79 +  def +(that: Natural): Natural = new Natural(this.value + that.value)
    2.80 +  def -(that: Natural): Natural = Natural(this.value - that.value)
    2.81 +  def *(that: Natural): Natural = new Natural(this.value * that.value)
    2.82 +
    2.83 +  def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
    2.84 +    else {
    2.85 +      val (k, l) = this.value /% that.value
    2.86 +      (new Natural(k), new Natural(l))
    2.87 +    }
    2.88 +
    2.89 +  def <=(that: Natural): Boolean = this.value <= that.value
    2.90 +
    2.91 +  def <(that: Natural): Boolean = this.value < that.value
    2.92 +
    2.93 +}
    2.94 +*}
    2.95 +
    2.96 +code_reserved Scala Natural
    2.97 +
    2.98 +code_type code_numeral
    2.99 +  (Haskell "Natural.Natural")
   2.100 +  (Scala "Natural")
   2.101 +
   2.102 +setup {*
   2.103 +  fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
   2.104 +    false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"]
   2.105 +*}
   2.106 +
   2.107 +code_instance code_numeral :: eq
   2.108 +  (Haskell -)
   2.109 +
   2.110 +code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   2.111 +  (Haskell infixl 6 "+")
   2.112 +  (Scala infixl 7 "+")
   2.113 +
   2.114 +code_const "op - \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   2.115 +  (Haskell infixl 6 "-")
   2.116 +  (Scala infixl 7 "-")
   2.117 +
   2.118 +code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   2.119 +  (Haskell infixl 7 "*")
   2.120 +  (Scala infixl 8 "*")
   2.121 +
   2.122 +code_const div_mod_code_numeral
   2.123 +  (Haskell "divMod")
   2.124 +  (Scala infixl 8 "/%")
   2.125 +
   2.126 +code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   2.127 +  (Haskell infixl 4 "==")
   2.128 +  (Scala infixl 5 "==")
   2.129 +
   2.130 +code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   2.131 +  (Haskell infix 4 "<=")
   2.132 +  (Scala infixl 4 "<=")
   2.133 +
   2.134 +code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   2.135 +  (Haskell infix 4 "<")
   2.136 +  (Scala infixl 4 "<")
   2.137 +
   2.138 +text {*
   2.139 +  Setup for @{typ int} proper.
   2.140 +*}
   2.141 +
   2.142 +
   2.143  code_type int
   2.144    (SML "IntInf.int")
   2.145    (OCaml "Big'_int.big'_int")
   2.146 @@ -26,8 +162,6 @@
   2.147  setup {*
   2.148    fold (Numeral.add_code @{const_name number_int_inst.number_of_int}
   2.149      true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
   2.150 -  #> Numeral.add_code @{const_name number_int_inst.number_of_int}
   2.151 -    true Code_Printer.literal_numeral "Scala"
   2.152  *}
   2.153  
   2.154  code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1"
   2.155 @@ -48,72 +182,82 @@
   2.156       and "!error(\"Bit0\")"
   2.157       and "!error(\"Bit1\")")
   2.158  
   2.159 -
   2.160  code_const Int.pred
   2.161    (SML "IntInf.- ((_), 1)")
   2.162    (OCaml "Big'_int.pred'_big'_int")
   2.163    (Haskell "!(_/ -/ 1)")
   2.164    (Scala "!(_/ -/ 1)")
   2.165 +  (Eval "!(_/ -/ 1)")
   2.166  
   2.167  code_const Int.succ
   2.168    (SML "IntInf.+ ((_), 1)")
   2.169    (OCaml "Big'_int.succ'_big'_int")
   2.170    (Haskell "!(_/ +/ 1)")
   2.171    (Scala "!(_/ +/ 1)")
   2.172 +  (Eval "!(_/ +/ 1)")
   2.173  
   2.174  code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   2.175    (SML "IntInf.+ ((_), (_))")
   2.176    (OCaml "Big'_int.add'_big'_int")
   2.177    (Haskell infixl 6 "+")
   2.178    (Scala infixl 7 "+")
   2.179 +  (Eval infixl 8 "+")
   2.180  
   2.181  code_const "uminus \<Colon> int \<Rightarrow> int"
   2.182    (SML "IntInf.~")
   2.183    (OCaml "Big'_int.minus'_big'_int")
   2.184    (Haskell "negate")
   2.185    (Scala "!(- _)")
   2.186 +  (Eval "~/ _")
   2.187  
   2.188  code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   2.189    (SML "IntInf.- ((_), (_))")
   2.190    (OCaml "Big'_int.sub'_big'_int")
   2.191    (Haskell infixl 6 "-")
   2.192    (Scala infixl 7 "-")
   2.193 +  (Eval infixl 8 "-")
   2.194  
   2.195  code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   2.196    (SML "IntInf.* ((_), (_))")
   2.197    (OCaml "Big'_int.mult'_big'_int")
   2.198    (Haskell infixl 7 "*")
   2.199    (Scala infixl 8 "*")
   2.200 +  (Eval infixl 9 "*")
   2.201  
   2.202  code_const pdivmod
   2.203    (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)")
   2.204    (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
   2.205    (Haskell "divMod/ (abs _)/ (abs _)")
   2.206 -  (Scala "!(_.abs '/% _.abs)")
   2.207 +  (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
   2.208 +  (Eval "Integer.div'_mod/ (abs _)/ (abs _)")
   2.209  
   2.210  code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   2.211    (SML "!((_ : IntInf.int) = _)")
   2.212    (OCaml "Big'_int.eq'_big'_int")
   2.213    (Haskell infixl 4 "==")
   2.214    (Scala infixl 5 "==")
   2.215 +  (Eval infixl 6 "=")
   2.216  
   2.217  code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   2.218    (SML "IntInf.<= ((_), (_))")
   2.219    (OCaml "Big'_int.le'_big'_int")
   2.220    (Haskell infix 4 "<=")
   2.221    (Scala infixl 4 "<=")
   2.222 +  (Eval infixl 6 "<=")
   2.223  
   2.224  code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   2.225    (SML "IntInf.< ((_), (_))")
   2.226    (OCaml "Big'_int.lt'_big'_int")
   2.227    (Haskell infix 4 "<")
   2.228 -  (Scala infixl 4 "<=")
   2.229 +  (Scala infixl 4 "<")
   2.230 +  (Eval infixl 6 "<")
   2.231  
   2.232  code_const Code_Numeral.int_of
   2.233    (SML "IntInf.fromInt")
   2.234    (OCaml "_")
   2.235 -  (Haskell "_")
   2.236 -  (Scala "!BigInt((_))")
   2.237 +  (Haskell "toInteger")
   2.238 +  (Scala "!_.as'_BigInt")
   2.239 +  (Eval "_")
   2.240  
   2.241  text {* Evaluation *}
   2.242  
     3.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Jul 23 18:42:46 2010 +0200
     3.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Sat Jul 24 18:08:41 2010 +0200
     3.3 @@ -50,19 +50,9 @@
     3.4    "n * m = nat (of_nat n * of_nat m)"
     3.5    unfolding of_nat_mult [symmetric] by simp
     3.6  
     3.7 -text {* Specialized @{term "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} 
     3.8 -  and @{term "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} operations. *}
     3.9 -
    3.10 -definition divmod_aux ::  "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
    3.11 -  [code del]: "divmod_aux = divmod_nat"
    3.12 -
    3.13 -lemma [code]:
    3.14 -  "divmod_nat n m = (if m = 0 then (0, n) else divmod_aux n m)"
    3.15 -  unfolding divmod_aux_def divmod_nat_div_mod by simp
    3.16 -
    3.17 -lemma divmod_aux_code [code]:
    3.18 -  "divmod_aux n m = (nat (of_nat n div of_nat m), nat (of_nat n mod of_nat m))"
    3.19 -  unfolding divmod_aux_def divmod_nat_div_mod zdiv_int [symmetric] zmod_int [symmetric] by simp
    3.20 +lemma divmod_nat_code [code]:
    3.21 +  "divmod_nat n m = prod_fun nat nat (pdivmod (of_nat n) (of_nat m))"
    3.22 +  by (simp add: prod_fun_def split_def pdivmod_def nat_div_distrib nat_mod_distrib divmod_nat_div_mod)
    3.23  
    3.24  lemma eq_nat_code [code]:
    3.25    "eq_class.eq n m \<longleftrightarrow> eq_class.eq (of_nat n \<Colon> int) (of_nat m)"
    3.26 @@ -233,6 +223,7 @@
    3.27  code_type nat
    3.28    (SML "IntInf.int")
    3.29    (OCaml "Big'_int.big'_int")
    3.30 +  (Eval "int")
    3.31  
    3.32  types_code
    3.33    nat ("int")
    3.34 @@ -281,7 +272,9 @@
    3.35  instance Integral Nat where {
    3.36    toInteger (Nat n) = n;
    3.37    divMod n m = quotRem n m;
    3.38 -  quotRem (Nat n) (Nat m) = (Nat k, Nat l) where (k, l) = quotRem n m;
    3.39 +  quotRem (Nat n) (Nat m)
    3.40 +    | (m == 0) = (0, Nat n)
    3.41 +    | otherwise = (Nat k, Nat l) where (k, l) = quotRem n m;
    3.42  };
    3.43  *}
    3.44  
    3.45 @@ -353,9 +346,7 @@
    3.46  
    3.47  setup {*
    3.48    fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat}
    3.49 -    false Code_Printer.literal_positive_numeral) ["SML", "OCaml", "Haskell"]
    3.50 -  #> Numeral.add_code @{const_name number_nat_inst.number_of_nat}
    3.51 -    false Code_Printer.literal_positive_numeral "Scala"
    3.52 +    false Code_Printer.literal_positive_numeral) ["SML", "OCaml", "Haskell", "Scala"]
    3.53  *}
    3.54  
    3.55  text {*
    3.56 @@ -400,6 +391,7 @@
    3.57  code_const nat
    3.58    (SML "IntInf.max/ (/0,/ _)")
    3.59    (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
    3.60 +  (Eval "Integer.max/ _/ 0")
    3.61  
    3.62  text {* For Haskell and Scala, things are slightly different again. *}
    3.63  
    3.64 @@ -407,19 +399,21 @@
    3.65    (Haskell "toInteger" and "fromInteger")
    3.66    (Scala "!_.as'_BigInt" and "Nat")
    3.67  
    3.68 -text {* Conversion from and to indices. *}
    3.69 +text {* Conversion from and to code numerals. *}
    3.70  
    3.71  code_const Code_Numeral.of_nat
    3.72    (SML "IntInf.toInt")
    3.73    (OCaml "_")
    3.74 -  (Haskell "toInteger")
    3.75 -  (Scala "!_.as'_Int")
    3.76 +  (Haskell "!(fromInteger/ ./ toInteger)")
    3.77 +  (Scala "!Natural(_.as'_BigInt)")
    3.78 +  (Eval "_")
    3.79  
    3.80  code_const Code_Numeral.nat_of
    3.81    (SML "IntInf.fromInt")
    3.82    (OCaml "_")
    3.83 -  (Haskell "fromInteger")
    3.84 -  (Scala "Nat")
    3.85 +  (Haskell "!(fromInteger/ ./ toInteger)")
    3.86 +  (Scala "!Nat(_.as'_BigInt)")
    3.87 +  (Eval "_")
    3.88  
    3.89  text {* Using target language arithmetic operations whenever appropriate *}
    3.90  
    3.91 @@ -428,6 +422,7 @@
    3.92    (OCaml "Big'_int.add'_big'_int")
    3.93    (Haskell infixl 6 "+")
    3.94    (Scala infixl 7 "+")
    3.95 +  (Eval infixl 8 "+")
    3.96  
    3.97  code_const "op - \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
    3.98    (Haskell infixl 6 "-")
    3.99 @@ -438,34 +433,35 @@
   3.100    (OCaml "Big'_int.mult'_big'_int")
   3.101    (Haskell infixl 7 "*")
   3.102    (Scala infixl 8 "*")
   3.103 +  (Eval infixl 9 "*")
   3.104  
   3.105 -code_const divmod_aux
   3.106 +code_const divmod_nat
   3.107    (SML "IntInf.divMod/ ((_),/ (_))")
   3.108    (OCaml "Big'_int.quomod'_big'_int")
   3.109    (Haskell "divMod")
   3.110    (Scala infixl 8 "/%")
   3.111 -
   3.112 -code_const divmod_nat
   3.113 -  (Haskell "divMod")
   3.114 -  (Scala infixl 8 "/%")
   3.115 +  (Eval "Integer.div'_mod")
   3.116  
   3.117  code_const "eq_class.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   3.118    (SML "!((_ : IntInf.int) = _)")
   3.119    (OCaml "Big'_int.eq'_big'_int")
   3.120    (Haskell infixl 4 "==")
   3.121    (Scala infixl 5 "==")
   3.122 +  (Eval infixl 6 "=")
   3.123  
   3.124  code_const "op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   3.125    (SML "IntInf.<= ((_), (_))")
   3.126    (OCaml "Big'_int.le'_big'_int")
   3.127    (Haskell infix 4 "<=")
   3.128    (Scala infixl 4 "<=")
   3.129 +  (Eval infixl 6 "<=")
   3.130  
   3.131  code_const "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   3.132    (SML "IntInf.< ((_), (_))")
   3.133    (OCaml "Big'_int.lt'_big'_int")
   3.134    (Haskell infix 4 "<")
   3.135    (Scala infixl 4 "<")
   3.136 +  (Eval infixl 6 "<")
   3.137  
   3.138  consts_code
   3.139    "0::nat"                     ("0")
     4.1 --- a/src/Tools/Code/code_haskell.ML	Fri Jul 23 18:42:46 2010 +0200
     4.2 +++ b/src/Tools/Code/code_haskell.ML	Sat Jul 24 18:08:41 2010 +0200
     4.3 @@ -415,6 +415,7 @@
     4.4    literal_string = quote o translate_string char_haskell,
     4.5    literal_numeral = numeral_haskell,
     4.6    literal_positive_numeral = numeral_haskell,
     4.7 +  literal_alternative_numeral = numeral_haskell,
     4.8    literal_naive_numeral = numeral_haskell,
     4.9    literal_list = enum "," "[" "]",
    4.10    infix_cons = (5, ":")
     5.1 --- a/src/Tools/Code/code_ml.ML	Fri Jul 23 18:42:46 2010 +0200
     5.2 +++ b/src/Tools/Code/code_ml.ML	Sat Jul 24 18:08:41 2010 +0200
     5.3 @@ -360,6 +360,7 @@
     5.4    literal_string = quote o translate_string ML_Syntax.print_char,
     5.5    literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
     5.6    literal_positive_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
     5.7 +  literal_alternative_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
     5.8    literal_naive_numeral = string_of_int,
     5.9    literal_list = enum "," "[" "]",
    5.10    infix_cons = (7, "::")
    5.11 @@ -702,6 +703,7 @@
    5.12    literal_string = quote o translate_string char_ocaml,
    5.13    literal_numeral = numeral_ocaml,
    5.14    literal_positive_numeral = numeral_ocaml,
    5.15 +  literal_alternative_numeral = numeral_ocaml,
    5.16    literal_naive_numeral = numeral_ocaml,
    5.17    literal_list = enum ";" "[" "]",
    5.18    infix_cons = (6, "::")
     6.1 --- a/src/Tools/Code/code_printer.ML	Fri Jul 23 18:42:46 2010 +0200
     6.2 +++ b/src/Tools/Code/code_printer.ML	Sat Jul 24 18:08:41 2010 +0200
     6.3 @@ -39,7 +39,9 @@
     6.4  
     6.5    type literals
     6.6    val Literals: { literal_char: string -> string, literal_string: string -> string,
     6.7 -        literal_numeral: int -> string, literal_positive_numeral: int -> string,
     6.8 +        literal_numeral: int -> string,
     6.9 +        literal_positive_numeral: int -> string,
    6.10 +        literal_alternative_numeral: int -> string,
    6.11          literal_naive_numeral: int -> string,
    6.12          literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
    6.13      -> literals
    6.14 @@ -47,6 +49,7 @@
    6.15    val literal_string: literals -> string -> string
    6.16    val literal_numeral: literals -> int -> string
    6.17    val literal_positive_numeral: literals -> int -> string
    6.18 +  val literal_alternative_numeral: literals -> int -> string
    6.19    val literal_naive_numeral: literals -> int -> string
    6.20    val literal_list: literals -> Pretty.T list -> Pretty.T
    6.21    val infix_cons: literals -> int * string
    6.22 @@ -171,6 +174,7 @@
    6.23    literal_string: string -> string,
    6.24    literal_numeral: int -> string,
    6.25    literal_positive_numeral: int -> string,
    6.26 +  literal_alternative_numeral: int -> string,
    6.27    literal_naive_numeral: int -> string,
    6.28    literal_list: Pretty.T list -> Pretty.T,
    6.29    infix_cons: int * string
    6.30 @@ -182,6 +186,7 @@
    6.31  val literal_string = #literal_string o dest_Literals;
    6.32  val literal_numeral = #literal_numeral o dest_Literals;
    6.33  val literal_positive_numeral = #literal_positive_numeral o dest_Literals;
    6.34 +val literal_alternative_numeral = #literal_alternative_numeral o dest_Literals;
    6.35  val literal_naive_numeral = #literal_naive_numeral o dest_Literals;
    6.36  val literal_list = #literal_list o dest_Literals;
    6.37  val infix_cons = #infix_cons o dest_Literals;
     7.1 --- a/src/Tools/Code/code_scala.ML	Fri Jul 23 18:42:46 2010 +0200
     7.2 +++ b/src/Tools/Code/code_scala.ML	Sat Jul 24 18:08:41 2010 +0200
     7.3 @@ -402,7 +402,7 @@
     7.4      else let val k = ord c
     7.5      in if k < 32 orelse k > 126 then "\\" ^ radixstring (8, "0", k) else c end
     7.6    fun numeral_scala k = if k < 0
     7.7 -    then if k <= 2147483647 then "- " ^ string_of_int (~ k)
     7.8 +    then if k > ~ 2147483647 then "- " ^ string_of_int (~ k)
     7.9        else quote ("- " ^ string_of_int (~ k))
    7.10      else if k <= 2147483647 then string_of_int k
    7.11        else quote (string_of_int k)
    7.12 @@ -411,8 +411,8 @@
    7.13    literal_string = quote o translate_string char_scala,
    7.14    literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
    7.15    literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
    7.16 -  literal_naive_numeral = fn k => if k >= 0
    7.17 -    then string_of_int k else "(- " ^ string_of_int (~ k) ^ ")",
    7.18 +  literal_alternative_numeral = fn k => "Natural(" ^ numeral_scala k ^ ")",
    7.19 +  literal_naive_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
    7.20    literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
    7.21    infix_cons = (6, "::")
    7.22  } end;