# HG changeset patch
# User haftmann
# Date 1263487659 -3600
# Node ID 8674bb6f727b203812f2fecf4d18bb1f9ca8eb01
# Parent  62d70417f8ce16b3a2f3813a0b54e42121a6b20a
added Scala setup

diff -r 62d70417f8ce -r 8674bb6f727b src/HOL/Library/Code_Integer.thy
--- a/src/HOL/Library/Code_Integer.thy	Thu Jan 14 17:47:38 2010 +0100
+++ b/src/HOL/Library/Code_Integer.thy	Thu Jan 14 17:47:39 2010 +0100
@@ -18,13 +18,16 @@
   (SML "IntInf.int")
   (OCaml "Big'_int.big'_int")
   (Haskell "Integer")
+  (Scala "BigInt")
 
 code_instance int :: eq
   (Haskell -)
 
 setup {*
   fold (Numeral.add_code @{const_name number_int_inst.number_of_int}
-    true true) ["SML", "OCaml", "Haskell"]
+    true true Code_Printer.str) ["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"
 *}
 
 code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1"
@@ -40,63 +43,80 @@
      and "error/ \"Min\""
      and "error/ \"Bit0\""
      and "error/ \"Bit1\"")
+  (Scala "!error(\"Pls\")"
+     and "!error(\"Min\")"
+     and "!error(\"Bit0\")"
+     and "!error(\"Bit1\")")
+
 
 code_const Int.pred
   (SML "IntInf.- ((_), 1)")
   (OCaml "Big'_int.pred'_big'_int")
   (Haskell "!(_/ -/ 1)")
+  (Scala "!(_/ -/ 1)")
 
 code_const Int.succ
   (SML "IntInf.+ ((_), 1)")
   (OCaml "Big'_int.succ'_big'_int")
   (Haskell "!(_/ +/ 1)")
+  (Scala "!(_/ +/ 1)")
 
 code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   (SML "IntInf.+ ((_), (_))")
   (OCaml "Big'_int.add'_big'_int")
   (Haskell infixl 6 "+")
+  (Scala infixl 7 "+")
 
 code_const "uminus \<Colon> int \<Rightarrow> int"
   (SML "IntInf.~")
   (OCaml "Big'_int.minus'_big'_int")
   (Haskell "negate")
+  (Scala "!(- _)")
 
 code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   (SML "IntInf.- ((_), (_))")
   (OCaml "Big'_int.sub'_big'_int")
   (Haskell infixl 6 "-")
+  (Scala infixl 7 "-")
 
 code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   (SML "IntInf.* ((_), (_))")
   (OCaml "Big'_int.mult'_big'_int")
   (Haskell infixl 7 "*")
+  (Scala infixl 8 "*")
 
 code_const pdivmod
-  (SML "(fn k => fn l =>/ IntInf.divMod/ (IntInf.abs k,/ IntInf.abs l))")
-  (OCaml "(fun k -> fun l ->/ Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int k)/ (Big'_int.abs'_big'_int l))")
-  (Haskell "(\\k l ->/ divMod/ (abs k)/ (abs l))")
+  (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)")
 
 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 "==")
 
 code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   (SML "IntInf.<= ((_), (_))")
   (OCaml "Big'_int.le'_big'_int")
   (Haskell infix 4 "<=")
+  (Scala infixl 4 "<=")
 
 code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   (SML "IntInf.< ((_), (_))")
   (OCaml "Big'_int.lt'_big'_int")
   (Haskell infix 4 "<")
+  (Scala infixl 4 "<=")
 
 code_const Code_Numeral.int_of
   (SML "IntInf.fromInt")
   (OCaml "_")
   (Haskell "toEnum")
+  (Scala "!BigInt(_)")
 
 code_reserved SML IntInf
+code_reserved Scala BigInt
 
 text {* Evaluation *}
 
diff -r 62d70417f8ce -r 8674bb6f727b src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Thu Jan 14 17:47:38 2010 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Thu Jan 14 17:47:39 2010 +0100
@@ -226,7 +226,7 @@
 
 text {*
   For ML, we map @{typ nat} to target language integers, where we
-  assert that values are always non-negative.
+  ensure that values are always non-negative.
 *}
 
 code_type nat
@@ -245,9 +245,9 @@
 *}
 
 text {*
-  For Haskell we define our own @{typ nat} type.  The reason
-  is that we have to distinguish type class instances
-  for @{typ nat} and @{typ int}.
+  For Haskell ans Scala we define our own @{typ nat} type.  The reason
+  is that we have to distinguish type class instances for @{typ nat}
+  and @{typ int}.
 *}
 
 code_include Haskell "Nat" {*
@@ -286,8 +286,52 @@
 
 code_reserved Haskell Nat
 
+code_include Scala "Nat" {*
+object Nat {
+
+  def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
+  def apply(numeral: Int): Nat = Nat(BigInt(numeral))
+  def apply(numeral: String): Nat = Nat(BigInt(numeral))
+
+}
+
+class Nat private(private val value: BigInt) {
+
+  override def hashCode(): Int = this.value.hashCode()
+
+  override def equals(that: Any): Boolean = that match {
+    case that: Nat => this equals that
+    case _ => false
+  }
+
+  override def toString(): String = this.value.toString
+
+  def equals(that: Nat): Boolean = this.value == that.value
+
+  def as_BigInt: BigInt = this.value
+
+  def +(that: Nat): Nat = new Nat(this.value + that.value)
+  def -(that: Nat): Nat = Nat(this.value + that.value)
+  def *(that: Nat): Nat = new Nat(this.value * that.value)
+
+  def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)
+    else {
+      val (k, l) = this.value /% that.value
+      (new Nat(k), new Nat(l))
+    }
+
+  def <=(that: Nat): Boolean = this.value <= that.value
+
+  def <(that: Nat): Boolean = this.value < that.value
+
+}
+*}
+
+code_reserved Scala Nat
+
 code_type nat
   (Haskell "Nat.Nat")
+  (Scala "Nat.Nat")
 
 code_instance nat :: eq
   (Haskell -)
@@ -303,7 +347,9 @@
 
 setup {*
   fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat}
-    false true) ["SML", "OCaml", "Haskell"]
+    false true Code_Printer.str) ["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"
 *}
 
 text {*
@@ -349,10 +395,11 @@
   (SML "IntInf.max/ (/0,/ _)")
   (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
 
-text {* For Haskell, things are slightly different again. *}
+text {* For Haskell ans Scala, things are slightly different again. *}
 
 code_const int and nat
   (Haskell "toInteger" and "fromInteger")
+  (Scala "!_.as'_BigInt" and "!Nat.Nat((_))")
 
 text {* Conversion from and to indices. *}
 
@@ -360,11 +407,13 @@
   (SML "IntInf.toInt")
   (OCaml "_")
   (Haskell "fromEnum")
+  (Scala "!_.as'_BigInt")
 
 code_const Code_Numeral.nat_of
   (SML "IntInf.fromInt")
   (OCaml "_")
   (Haskell "toEnum")
+  (Scala "!Nat.Nat((_))")
 
 text {* Using target language arithmetic operations whenever appropriate *}
 
@@ -372,31 +421,45 @@
   (SML "IntInf.+ ((_), (_))")
   (OCaml "Big'_int.add'_big'_int")
   (Haskell infixl 6 "+")
+  (Scala infixl 7 "+")
+
+code_const "op - \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
+  (Haskell infixl 6 "-")
+  (Scala infixl 7 "-")
 
 code_const "op * \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
   (SML "IntInf.* ((_), (_))")
   (OCaml "Big'_int.mult'_big'_int")
   (Haskell infixl 7 "*")
+  (Scala infixl 8 "*")
 
 code_const divmod_aux
   (SML "IntInf.divMod/ ((_),/ (_))")
   (OCaml "Big'_int.quomod'_big'_int")
   (Haskell "divMod")
+  (Scala infixl 8 "/%")
+
+code_const divmod_nat
+  (Haskell "divMod")
+  (Scala infixl 8 "/%")
 
 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 "==")
 
 code_const "op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   (SML "IntInf.<= ((_), (_))")
   (OCaml "Big'_int.le'_big'_int")
   (Haskell infix 4 "<=")
+  (Scala infixl 4 "<=")
 
 code_const "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   (SML "IntInf.< ((_), (_))")
   (OCaml "Big'_int.lt'_big'_int")
   (Haskell infix 4 "<")
+  (Scala infixl 4 "<")
 
 consts_code
   "0::nat"                     ("0")