--- 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
--- 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")
--- 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
--- 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}
--- 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 *}
--- 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, "::")