1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Wed Sep 01 09:03:34 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Wed Sep 01 11:09:50 2010 +0200
     1.3 @@ -484,11 +484,11 @@
     1.4  
     1.5  code_type array (Scala "!collection.mutable.ArraySeq[_]")
     1.6  code_const Array (Scala "!error(\"bare Array\")")
     1.7 -code_const Array.new' (Scala "('_: Unit)/ => / Heap.Array.alloc((_))((_))")
     1.8 -code_const Array.make' (Scala "('_: Unit)/ =>/ Heap.Array.make((_))((_))")
     1.9 -code_const Array.len' (Scala "('_: Unit)/ =>/ Heap.Array.len((_))")
    1.10 -code_const Array.nth' (Scala "('_: Unit)/ =>/ Heap.Array.nth((_), (_))")
    1.11 -code_const Array.upd' (Scala "('_: Unit)/ =>/ Heap.Array.upd((_), (_), (_))")
    1.12 -code_const Array.freeze (Scala "('_: Unit)/ =>/ Heap.Array.freeze((_))")
    1.13 +code_const Array.new' (Scala "('_: Unit)/ => / Array.alloc((_))((_))")
    1.14 +code_const Array.make' (Scala "('_: Unit)/ =>/ Array.make((_))((_))")
    1.15 +code_const Array.len' (Scala "('_: Unit)/ =>/ Array.len((_))")
    1.16 +code_const Array.nth' (Scala "('_: Unit)/ =>/ Array.nth((_), (_))")
    1.17 +code_const Array.upd' (Scala "('_: Unit)/ =>/ Array.upd((_), (_), (_))")
    1.18 +code_const Array.freeze (Scala "('_: Unit)/ =>/ Array.freeze((_))")
    1.19  
    1.20  end

     2.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Sep 01 09:03:34 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Sep 01 11:09:50 2010 +0200
     2.3 @@ -477,9 +477,9 @@
     2.4  subsubsection {* Scala *}
     2.5  
     2.6  code_include Scala "Heap"
     2.7 -{*import collection.mutable.ArraySeq
     2.8 -
     2.9 -def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
    2.10 +{*object Heap {
    2.11 +  def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
    2.12 +}
    2.13  
    2.14  class Ref[A](x: A) {
    2.15    var value = x
    2.16 @@ -495,21 +495,23 @@
    2.17  }
    2.18  
    2.19  object Array {
    2.20 -  def alloc[A](n: Natural.Nat)(x: A): ArraySeq[A] =
    2.21 +  import collection.mutable.ArraySeq
    2.22 +  def alloc[A](n: Natural)(x: A): ArraySeq[A] =
    2.23      ArraySeq.fill(n.as_Int)(x)
    2.24 -  def make[A](n: Natural.Nat)(f: Natural.Nat => A): ArraySeq[A] =
    2.25 -    ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural.Nat(k)))
    2.26 -  def len[A](a: ArraySeq[A]): Natural.Nat =
    2.27 -    Natural.Nat(a.length)
    2.28 -  def nth[A](a: ArraySeq[A], n: Natural.Nat): A =
    2.29 +  def make[A](n: Natural)(f: Natural => A): ArraySeq[A] =
    2.30 +    ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural(k)))
    2.31 +  def len[A](a: ArraySeq[A]): Natural =
    2.32 +    Natural(a.length)
    2.33 +  def nth[A](a: ArraySeq[A], n: Natural): A =
    2.34      a(n.as_Int)
    2.35 -  def upd[A](a: ArraySeq[A], n: Natural.Nat, x: A): Unit =
    2.36 +  def upd[A](a: ArraySeq[A], n: Natural, x: A): Unit =
    2.37      a.update(n.as_Int, x)
    2.38    def freeze[A](a: ArraySeq[A]): List[A] =
    2.39      a.toList
    2.40 -}*}
    2.41 +}
    2.42 +*}
    2.43  
    2.44 -code_reserved Scala bind Ref Array
    2.45 +code_reserved Scala Heap Ref Array
    2.46  
    2.47  code_type Heap (Scala "Unit/ =>/ _")
    2.48  code_const bind (Scala "Heap.bind")

     3.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Wed Sep 01 09:03:34 2010 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Wed Sep 01 11:09:50 2010 +0200
     3.3 @@ -306,10 +306,10 @@
     3.4  
     3.5  text {* Scala *}
     3.6  
     3.7 -code_type ref (Scala "!Heap.Ref[_]")
     3.8 +code_type ref (Scala "!Ref[_]")
     3.9  code_const Ref (Scala "!error(\"bare Ref\")")
    3.10 -code_const ref' (Scala "('_: Unit)/ =>/ Heap.Ref((_))")
    3.11 -code_const Ref.lookup (Scala "('_: Unit)/ =>/ Heap.Ref.lookup((_))")
    3.12 -code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.Ref.update((_), (_))")
    3.13 +code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
    3.14 +code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
    3.15 +code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
    3.16  
    3.17  end

     4.1 --- a/src/HOL/Library/Code_Natural.thy	Wed Sep 01 09:03:34 2010 +0200
     4.2 +++ b/src/HOL/Library/Code_Natural.thy	Wed Sep 01 11:09:50 2010 +0200
     4.3 @@ -56,47 +56,45 @@
     4.4  code_reserved Haskell Natural
     4.5  
     4.6  code_include Scala "Natural"
     4.7 -{*import scala.Math
     4.8 -
     4.9 -object Nat {
    4.10 +{*object Natural {
    4.11  
    4.12 -  def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
    4.13 -  def apply(numeral: Int): Nat = Nat(BigInt(numeral))
    4.14 -  def apply(numeral: String): Nat = Nat(BigInt(numeral))
    4.15 +  def apply(numeral: BigInt): Natural = new Natural(numeral max 0)
    4.16 +  def apply(numeral: Int): Natural = Natural(BigInt(numeral))
    4.17 +  def apply(numeral: String): Natural = Natural(BigInt(numeral))
    4.18  
    4.19  }
    4.20  
    4.21 -class Nat private(private val value: BigInt) {
    4.22 +class Natural private(private val value: BigInt) {
    4.23  
    4.24    override def hashCode(): Int = this.value.hashCode()
    4.25  
    4.26    override def equals(that: Any): Boolean = that match {
    4.27 -    case that: Nat => this equals that
    4.28 +    case that: Natural => this equals that
    4.29      case _ => false
    4.30    }
    4.31  
    4.32    override def toString(): String = this.value.toString
    4.33  
    4.34 -  def equals(that: Nat): Boolean = this.value == that.value
    4.35 +  def equals(that: Natural): Boolean = this.value == that.value
    4.36  
    4.37    def as_BigInt: BigInt = this.value
    4.38    def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
    4.39        this.value.intValue
    4.40      else error("Int value out of range: " + this.value.toString)
    4.41  
    4.42 -  def +(that: Nat): Nat = new Nat(this.value + that.value)
    4.43 -  def -(that: Nat): Nat = Nat(this.value - that.value)
    4.44 -  def *(that: Nat): Nat = new Nat(this.value * that.value)
    4.45 +  def +(that: Natural): Natural = new Natural(this.value + that.value)
    4.46 +  def -(that: Natural): Natural = Natural(this.value - that.value)
    4.47 +  def *(that: Natural): Natural = new Natural(this.value * that.value)
    4.48  
    4.49 -  def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)
    4.50 +  def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
    4.51      else {
    4.52        val (k, l) = this.value /% that.value
    4.53 -      (new Nat(k), new Nat(l))
    4.54 +      (new Natural(k), new Natural(l))
    4.55      }
    4.56  
    4.57 -  def <=(that: Nat): Boolean = this.value <= that.value
    4.58 +  def <=(that: Natural): Boolean = this.value <= that.value
    4.59  
    4.60 -  def <(that: Nat): Boolean = this.value < that.value
    4.61 +  def <(that: Natural): Boolean = this.value < that.value
    4.62  
    4.63  }
    4.64  *}
    4.65 @@ -105,7 +103,7 @@
    4.66  
    4.67  code_type code_numeral
    4.68    (Haskell "Natural.Natural")
    4.69 -  (Scala "Natural.Nat")
    4.70 +  (Scala "Natural")
    4.71  
    4.72  setup {*
    4.73    fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}

     5.1 --- a/src/HOL/Library/Efficient_Nat.thy	Wed Sep 01 09:03:34 2010 +0200
     5.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Wed Sep 01 11:09:50 2010 +0200
     5.3 @@ -281,9 +281,7 @@
     5.4  code_reserved Haskell Nat
     5.5  
     5.6  code_include Scala "Nat"
     5.7 -{*import scala.Math
     5.8 -
     5.9 -object Nat {
    5.10 +{*object Nat {
    5.11  
    5.12    def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
    5.13    def apply(numeral: Int): Nat = Nat(BigInt(numeral))
    5.14 @@ -330,7 +328,7 @@
    5.15  
    5.16  code_type nat
    5.17    (Haskell "Nat.Nat")
    5.18 -  (Scala "Nat.Nat")
    5.19 +  (Scala "Nat")
    5.20  
    5.21  code_instance nat :: equal
    5.22    (Haskell -)
    5.23 @@ -397,7 +395,7 @@
    5.24  
    5.25  code_const int and nat
    5.26    (Haskell "toInteger" and "fromInteger")
    5.27 -  (Scala "!_.as'_BigInt" and "Nat.Nat")
    5.28 +  (Scala "!_.as'_BigInt" and "Nat")
    5.29  
    5.30  text {* Conversion from and to code numerals. *}
    5.31  
    5.32 @@ -405,14 +403,14 @@
    5.33    (SML "IntInf.toInt")
    5.34    (OCaml "_")
    5.35    (Haskell "!(fromInteger/ ./ toInteger)")
    5.36 -  (Scala "!Natural.Nat(_.as'_BigInt)")
    5.37 +  (Scala "!Natural(_.as'_BigInt)")
    5.38    (Eval "_")
    5.39  
    5.40  code_const Code_Numeral.nat_of
    5.41    (SML "IntInf.fromInt")
    5.42    (OCaml "_")
    5.43    (Haskell "!(fromInteger/ ./ toInteger)")
    5.44 -  (Scala "!Nat.Nat(_.as'_BigInt)")
    5.45 +  (Scala "!Nat(_.as'_BigInt)")
    5.46    (Eval "_")
    5.47  
    5.48  text {* Using target language arithmetic operations whenever appropriate *}

     6.1 --- a/src/Tools/Code/code_scala.ML	Wed Sep 01 09:03:34 2010 +0200
     6.2 +++ b/src/Tools/Code/code_scala.ML	Wed Sep 01 11:09:50 2010 +0200
     6.3 @@ -477,8 +477,7 @@
     6.4        in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
     6.5  
     6.6      (* serialization *)
     6.7 -    val p_includes = if null presentation_names
     6.8 -      then map (fn (base, p) => print_module base [] p) includes else [];
     6.9 +    val p_includes = if null presentation_names then map snd includes else [];
    6.10      val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
    6.11      fun write width NONE = writeln_pretty width
    6.12        | write width (SOME p) = File.write p o string_of_pretty width;
    6.13 @@ -506,8 +505,8 @@
    6.14    literal_char = Library.enclose "'" "'" o char_scala,
    6.15    literal_string = quote o translate_string char_scala,
    6.16    literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
    6.17 -  literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
    6.18 -  literal_alternative_numeral = fn k => "Natural.Nat(" ^ numeral_scala k ^ ")",
    6.19 +  literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
    6.20 +  literal_alternative_numeral = fn k => "Natural(" ^ numeral_scala k ^ ")",
    6.21    literal_naive_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
    6.22    literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
    6.23    infix_cons = (6, "::")