# HG changeset patch
# User haftmann
# Date 1283335304 -7200
# Node ID 5d49165a192e776efa13c9d52905b1842fb3a5f0
# Parent  53d1ee3d98b843c2975aec869d090d00116a8f67# Parent  e55deaa22fffb29ec94bafbc704f237e8c95be8b
merged

diff -r 53d1ee3d98b8 -r 5d49165a192e src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Wed Sep 01 12:01:19 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Wed Sep 01 12:01:44 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)/ => / 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((_))")
+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((_))")
 
 end
diff -r 53d1ee3d98b8 -r 5d49165a192e src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Sep 01 12:01:19 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Sep 01 12:01:44 2010 +0200
@@ -477,9 +477,9 @@
 subsubsection {* Scala *}
 
 code_include Scala "Heap"
-{*import collection.mutable.ArraySeq
-
-def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
+{*object Heap {
+  def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
+}
 
 class Ref[A](x: A) {
   var value = x
@@ -495,21 +495,23 @@
 }
 
 object Array {
-  def alloc[A](n: Natural.Nat)(x: A): ArraySeq[A] =
+  import collection.mutable.ArraySeq
+  def alloc[A](n: Natural)(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 =
+  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.Nat, x: A): Unit =
+  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
-}*}
+}
+*}
 
-code_reserved Scala bind Ref Array
+code_reserved Scala Heap Ref Array
 
 code_type Heap (Scala "Unit/ =>/ _")
 code_const bind (Scala "Heap.bind")
diff -r 53d1ee3d98b8 -r 5d49165a192e src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Wed Sep 01 12:01:19 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Wed Sep 01 12:01:44 2010 +0200
@@ -306,10 +306,10 @@
 
 text {* Scala *}
 
-code_type ref (Scala "!Heap.Ref[_]")
+code_type ref (Scala "!Ref[_]")
 code_const Ref (Scala "!error(\"bare Ref\")")
-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((_), (_))")
+code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
+code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
+code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
 
 end
diff -r 53d1ee3d98b8 -r 5d49165a192e src/HOL/Library/Code_Natural.thy
--- a/src/HOL/Library/Code_Natural.thy	Wed Sep 01 12:01:19 2010 +0200
+++ b/src/HOL/Library/Code_Natural.thy	Wed Sep 01 12:01:44 2010 +0200
@@ -56,47 +56,45 @@
 code_reserved Haskell Natural
 
 code_include Scala "Natural"
-{*import scala.Math
-
-object Nat {
+{*object Natural {
 
-  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))
+  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 Nat private(private val value: BigInt) {
+class Natural 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 that: Natural => this equals that
     case _ => false
   }
 
   override def toString(): String = this.value.toString
 
-  def equals(that: Nat): Boolean = this.value == that.value
+  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 error("Int value out of range: " + this.value.toString)
 
-  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 = 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, Nat) = if (that.value == 0) (new Nat(0), this)
+  def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
     else {
       val (k, l) = this.value /% that.value
-      (new Nat(k), new Nat(l))
+      (new Natural(k), new Natural(l))
     }
 
-  def <=(that: Nat): Boolean = this.value <= that.value
+  def <=(that: Natural): Boolean = this.value <= that.value
 
-  def <(that: Nat): Boolean = this.value < that.value
+  def <(that: Natural): Boolean = this.value < that.value
 
 }
 *}
@@ -105,7 +103,7 @@
 
 code_type code_numeral
   (Haskell "Natural.Natural")
-  (Scala "Natural.Nat")
+  (Scala "Natural")
 
 setup {*
   fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
diff -r 53d1ee3d98b8 -r 5d49165a192e src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Wed Sep 01 12:01:19 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Wed Sep 01 12:01:44 2010 +0200
@@ -281,9 +281,7 @@
 code_reserved Haskell Nat
 
 code_include Scala "Nat"
-{*import scala.Math
-
-object Nat {
+{*object Nat {
 
   def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
   def apply(numeral: Int): Nat = Nat(BigInt(numeral))
@@ -330,7 +328,7 @@
 
 code_type nat
   (Haskell "Nat.Nat")
-  (Scala "Nat.Nat")
+  (Scala "Nat")
 
 code_instance nat :: equal
   (Haskell -)
@@ -397,7 +395,7 @@
 
 code_const int and nat
   (Haskell "toInteger" and "fromInteger")
-  (Scala "!_.as'_BigInt" and "Nat.Nat")
+  (Scala "!_.as'_BigInt" and "Nat")
 
 text {* Conversion from and to code numerals. *}
 
@@ -405,14 +403,14 @@
   (SML "IntInf.toInt")
   (OCaml "_")
   (Haskell "!(fromInteger/ ./ toInteger)")
-  (Scala "!Natural.Nat(_.as'_BigInt)")
+  (Scala "!Natural(_.as'_BigInt)")
   (Eval "_")
 
 code_const Code_Numeral.nat_of
   (SML "IntInf.fromInt")
   (OCaml "_")
   (Haskell "!(fromInteger/ ./ toInteger)")
-  (Scala "!Nat.Nat(_.as'_BigInt)")
+  (Scala "!Nat(_.as'_BigInt)")
   (Eval "_")
 
 text {* Using target language arithmetic operations whenever appropriate *}
diff -r 53d1ee3d98b8 -r 5d49165a192e src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Wed Sep 01 12:01:19 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Wed Sep 01 12:01:44 2010 +0200
@@ -388,8 +388,7 @@
       in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
 
     (* serialization *)
-    val p_includes = if null presentation_names
-      then map (fn (base, p) => print_module base [] p) includes else [];
+    val p_includes = if null presentation_names then map snd includes else [];
     val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
     fun write width NONE = writeln_pretty width
       | write width (SOME p) = File.write p o string_of_pretty width;
@@ -415,8 +414,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.Nat(" ^ numeral_scala k ^ ")",
-  literal_alternative_numeral = fn k => "Natural.Nat(" ^ numeral_scala k ^ ")",
+  literal_positive_numeral = fn k => "Nat(" ^ numeral_scala 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, "::")