# HG changeset patch
# User haftmann
# Date 1282810582 -7200
# Node ID f9cd27cbe8a477504feda22f5a08bfd60bcf13e2
# Parent  1c70a502c590221542c0ce79ee18e5d63aedb5d8
code_include Scala: qualify module nmae

diff -r 1c70a502c590 -r f9cd27cbe8a4 src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Wed Aug 25 22:47:04 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Thu Aug 26 10:16:22 2010 +0200
@@ -484,11 +484,11 @@
 
 code_type array (Scala "!collection.mutable.ArraySeq[_]")
 code_const Array (Scala "!error(\"bare Array\")")
-code_const Array.new' (Scala "('_: Unit)/ => / Array.alloc((_))((_))")
-code_const Array.make' (Scala "('_: Unit)/ =>/ Array.make((_))((_))")
-code_const Array.len' (Scala "('_: Unit)/ =>/ Array.len((_))")
-code_const Array.nth' (Scala "('_: Unit)/ =>/ Array.nth((_), (_))")
-code_const Array.upd' (Scala "('_: Unit)/ =>/ Array.upd((_), (_), (_))")
-code_const Array.freeze (Scala "('_: Unit)/ =>/ Array.freeze((_))")
+code_const Array.new' (Scala "('_: Unit)/ => / Heap.Array.alloc((_))((_))")
+code_const Array.make' (Scala "('_: Unit)/ =>/ Heap.Array.make((_))((_))")
+code_const Array.len' (Scala "('_: Unit)/ =>/ Heap.Array.len((_))")
+code_const Array.nth' (Scala "('_: Unit)/ =>/ Heap.Array.nth((_), (_))")
+code_const Array.upd' (Scala "('_: Unit)/ =>/ Heap.Array.upd((_), (_), (_))")
+code_const Array.freeze (Scala "('_: Unit)/ =>/ Heap.Array.freeze((_))")
 
 end
diff -r 1c70a502c590 -r f9cd27cbe8a4 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Aug 25 22:47:04 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Aug 26 10:16:22 2010 +0200
@@ -478,8 +478,6 @@
 
 code_include Scala "Heap"
 {*import collection.mutable.ArraySeq
-import Natural._
-
 def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
 
 class Ref[A](x: A) {
@@ -487,24 +485,33 @@
 }
 
 object Ref {
-  def apply[A](x: A): Ref[A] = new Ref[A](x)
-  def lookup[A](r: Ref[A]): A = r.value
-  def update[A](r: Ref[A], x: A): Unit = { r.value = x }
+  def apply[A](x: A): Ref[A] =
+    new Ref[A](x)
+  def lookup[A](r: Ref[A]): A =
+    r.value
+  def update[A](r: Ref[A], x: A): Unit =
+    { r.value = x }
 }
 
 object Array {
-  def alloc[A](n: Natural)(x: A): ArraySeq[A] = ArraySeq.fill(n.as_Int)(x)
-  def make[A](n: Natural)(f: Natural => A): ArraySeq[A] = ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural(k)))
-  def len[A](a: ArraySeq[A]): Natural = Natural(a.length)
-  def nth[A](a: ArraySeq[A], n: Natural): A = a(n.as_Int)
-  def upd[A](a: ArraySeq[A], n: Natural, x: A): Unit = a.update(n.as_Int, x)
-  def freeze[A](a: ArraySeq[A]): List[A] = a.toList
+  def alloc[A](n: Natural.Nat)(x: A): ArraySeq[A] =
+    ArraySeq.fill(n.as_Int)(x)
+  def make[A](n: Natural.Nat)(f: Natural.Nat => A): ArraySeq[A] =
+    ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural.Nat(k)))
+  def len[A](a: ArraySeq[A]): Natural.Nat =
+    Natural.Nat(a.length)
+  def nth[A](a: ArraySeq[A], n: Natural.Nat): A =
+    a(n.as_Int)
+  def upd[A](a: ArraySeq[A], n: Natural.Nat, x: A): Unit =
+    a.update(n.as_Int, x)
+  def freeze[A](a: ArraySeq[A]): List[A] =
+    a.toList
 }*}
 
 code_reserved Scala bind Ref Array
 
 code_type Heap (Scala "Unit/ =>/ _")
-code_const bind (Scala "bind")
+code_const bind (Scala "Heap.bind")
 code_const return (Scala "('_: Unit)/ =>/ _")
 code_const Heap_Monad.raise' (Scala "!error((_))")
 
diff -r 1c70a502c590 -r f9cd27cbe8a4 src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Wed Aug 25 22:47:04 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Thu Aug 26 10:16:22 2010 +0200
@@ -306,10 +306,10 @@
 
 text {* Scala *}
 
-code_type ref (Scala "!Ref[_]")
+code_type ref (Scala "!Heap.Ref[_]")
 code_const Ref (Scala "!error(\"bare Ref\")")
-code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
-code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
-code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
+code_const ref' (Scala "('_: Unit)/ =>/ Heap.Ref((_))")
+code_const Ref.lookup (Scala "('_: Unit)/ =>/ Heap.Ref.lookup((_))")
+code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.Ref.update((_), (_))")
 
 end
diff -r 1c70a502c590 -r f9cd27cbe8a4 src/HOL/Library/Code_Natural.thy
--- a/src/HOL/Library/Code_Natural.thy	Wed Aug 25 22:47:04 2010 +0200
+++ b/src/HOL/Library/Code_Natural.thy	Thu Aug 26 10:16:22 2010 +0200
@@ -57,45 +57,45 @@
 code_include Scala "Natural" {*
 import scala.Math
 
-object Natural {
+object Nat {
 
-  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))
+  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 Natural private(private val value: BigInt) {
+class Nat 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 that: Nat => this equals that
     case _ => false
   }
 
   override def toString(): String = this.value.toString
 
-  def equals(that: Natural): Boolean = this.value == that.value
+  def equals(that: Nat): 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 error("Int value out of range: " + this.value.toString)
 
-  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: 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: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
+  def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)
     else {
       val (k, l) = this.value /% that.value
-      (new Natural(k), new Natural(l))
+      (new Nat(k), new Nat(l))
     }
 
-  def <=(that: Natural): Boolean = this.value <= that.value
+  def <=(that: Nat): Boolean = this.value <= that.value
 
-  def <(that: Natural): Boolean = this.value < that.value
+  def <(that: Nat): Boolean = this.value < that.value
 
 }
 *}
@@ -104,7 +104,7 @@
 
 code_type code_numeral
   (Haskell "Natural.Natural")
-  (Scala "Natural")
+  (Scala "Natural.Nat")
 
 setup {*
   fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
diff -r 1c70a502c590 -r f9cd27cbe8a4 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Wed Aug 25 22:47:04 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Thu Aug 26 10:16:22 2010 +0200
@@ -330,7 +330,7 @@
 
 code_type nat
   (Haskell "Nat.Nat")
-  (Scala "Nat")
+  (Scala "Nat.Nat")
 
 code_instance nat :: eq
   (Haskell -)
@@ -397,7 +397,7 @@
 
 code_const int and nat
   (Haskell "toInteger" and "fromInteger")
-  (Scala "!_.as'_BigInt" and "Nat")
+  (Scala "!_.as'_BigInt" and "Nat.Nat")
 
 text {* Conversion from and to code numerals. *}
 
@@ -405,14 +405,14 @@
   (SML "IntInf.toInt")
   (OCaml "_")
   (Haskell "!(fromInteger/ ./ toInteger)")
-  (Scala "!Natural(_.as'_BigInt)")
+  (Scala "!Natural.Nat(_.as'_BigInt)")
   (Eval "_")
 
 code_const Code_Numeral.nat_of
   (SML "IntInf.fromInt")
   (OCaml "_")
   (Haskell "!(fromInteger/ ./ toInteger)")
-  (Scala "!Nat(_.as'_BigInt)")
+  (Scala "!Nat.Nat(_.as'_BigInt)")
   (Eval "_")
 
 text {* Using target language arithmetic operations whenever appropriate *}
diff -r 1c70a502c590 -r f9cd27cbe8a4 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Wed Aug 25 22:47:04 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Aug 26 10:16:22 2010 +0200
@@ -487,8 +487,8 @@
   literal_char = Library.enclose "'" "'" o char_scala,
   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_alternative_numeral = fn k => "Natural(" ^ numeral_scala k ^ ")",
+  literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
+  literal_alternative_numeral = fn k => "Natural.Nat(" ^ 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, "::")