do not print object frame around Scala includes -- this is in the responsibility of the user
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, "::")