code_include Scala: qualify module nmae
authorhaftmann
Thu Aug 26 10:16:22 2010 +0200 (2010-08-26)
changeset 38771f9cd27cbe8a4
parent 38770 1c70a502c590
child 38772 eb7bc47f062b
code_include Scala: qualify module nmae
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/Ref.thy
src/HOL/Library/Code_Natural.thy
src/HOL/Library/Efficient_Nat.thy
src/Tools/Code/code_scala.ML
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Wed Aug 25 22:47:04 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Thu Aug 26 10:16:22 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)/ => / Array.alloc((_))((_))")
     1.8 -code_const Array.make' (Scala "('_: Unit)/ =>/ Array.make((_))((_))")
     1.9 -code_const Array.len' (Scala "('_: Unit)/ =>/ Array.len((_))")
    1.10 -code_const Array.nth' (Scala "('_: Unit)/ =>/ Array.nth((_), (_))")
    1.11 -code_const Array.upd' (Scala "('_: Unit)/ =>/ Array.upd((_), (_), (_))")
    1.12 -code_const Array.freeze (Scala "('_: Unit)/ =>/ Array.freeze((_))")
    1.13 +code_const Array.new' (Scala "('_: Unit)/ => / Heap.Array.alloc((_))((_))")
    1.14 +code_const Array.make' (Scala "('_: Unit)/ =>/ Heap.Array.make((_))((_))")
    1.15 +code_const Array.len' (Scala "('_: Unit)/ =>/ Heap.Array.len((_))")
    1.16 +code_const Array.nth' (Scala "('_: Unit)/ =>/ Heap.Array.nth((_), (_))")
    1.17 +code_const Array.upd' (Scala "('_: Unit)/ =>/ Heap.Array.upd((_), (_), (_))")
    1.18 +code_const Array.freeze (Scala "('_: Unit)/ =>/ Heap.Array.freeze((_))")
    1.19  
    1.20  end
     2.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Aug 25 22:47:04 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Aug 26 10:16:22 2010 +0200
     2.3 @@ -478,8 +478,6 @@
     2.4  
     2.5  code_include Scala "Heap"
     2.6  {*import collection.mutable.ArraySeq
     2.7 -import Natural._
     2.8 -
     2.9  def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
    2.10  
    2.11  class Ref[A](x: A) {
    2.12 @@ -487,24 +485,33 @@
    2.13  }
    2.14  
    2.15  object Ref {
    2.16 -  def apply[A](x: A): Ref[A] = new Ref[A](x)
    2.17 -  def lookup[A](r: Ref[A]): A = r.value
    2.18 -  def update[A](r: Ref[A], x: A): Unit = { r.value = x }
    2.19 +  def apply[A](x: A): Ref[A] =
    2.20 +    new Ref[A](x)
    2.21 +  def lookup[A](r: Ref[A]): A =
    2.22 +    r.value
    2.23 +  def update[A](r: Ref[A], x: A): Unit =
    2.24 +    { r.value = x }
    2.25  }
    2.26  
    2.27  object Array {
    2.28 -  def alloc[A](n: Natural)(x: A): ArraySeq[A] = ArraySeq.fill(n.as_Int)(x)
    2.29 -  def make[A](n: Natural)(f: Natural => A): ArraySeq[A] = ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural(k)))
    2.30 -  def len[A](a: ArraySeq[A]): Natural = Natural(a.length)
    2.31 -  def nth[A](a: ArraySeq[A], n: Natural): A = a(n.as_Int)
    2.32 -  def upd[A](a: ArraySeq[A], n: Natural, x: A): Unit = a.update(n.as_Int, x)
    2.33 -  def freeze[A](a: ArraySeq[A]): List[A] = a.toList
    2.34 +  def alloc[A](n: Natural.Nat)(x: A): ArraySeq[A] =
    2.35 +    ArraySeq.fill(n.as_Int)(x)
    2.36 +  def make[A](n: Natural.Nat)(f: Natural.Nat => A): ArraySeq[A] =
    2.37 +    ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural.Nat(k)))
    2.38 +  def len[A](a: ArraySeq[A]): Natural.Nat =
    2.39 +    Natural.Nat(a.length)
    2.40 +  def nth[A](a: ArraySeq[A], n: Natural.Nat): A =
    2.41 +    a(n.as_Int)
    2.42 +  def upd[A](a: ArraySeq[A], n: Natural.Nat, x: A): Unit =
    2.43 +    a.update(n.as_Int, x)
    2.44 +  def freeze[A](a: ArraySeq[A]): List[A] =
    2.45 +    a.toList
    2.46  }*}
    2.47  
    2.48  code_reserved Scala bind Ref Array
    2.49  
    2.50  code_type Heap (Scala "Unit/ =>/ _")
    2.51 -code_const bind (Scala "bind")
    2.52 +code_const bind (Scala "Heap.bind")
    2.53  code_const return (Scala "('_: Unit)/ =>/ _")
    2.54  code_const Heap_Monad.raise' (Scala "!error((_))")
    2.55  
     3.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Wed Aug 25 22:47:04 2010 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Thu Aug 26 10:16:22 2010 +0200
     3.3 @@ -306,10 +306,10 @@
     3.4  
     3.5  text {* Scala *}
     3.6  
     3.7 -code_type ref (Scala "!Ref[_]")
     3.8 +code_type ref (Scala "!Heap.Ref[_]")
     3.9  code_const Ref (Scala "!error(\"bare Ref\")")
    3.10 -code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
    3.11 -code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
    3.12 -code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
    3.13 +code_const ref' (Scala "('_: Unit)/ =>/ Heap.Ref((_))")
    3.14 +code_const Ref.lookup (Scala "('_: Unit)/ =>/ Heap.Ref.lookup((_))")
    3.15 +code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.Ref.update((_), (_))")
    3.16  
    3.17  end
     4.1 --- a/src/HOL/Library/Code_Natural.thy	Wed Aug 25 22:47:04 2010 +0200
     4.2 +++ b/src/HOL/Library/Code_Natural.thy	Thu Aug 26 10:16:22 2010 +0200
     4.3 @@ -57,45 +57,45 @@
     4.4  code_include Scala "Natural" {*
     4.5  import scala.Math
     4.6  
     4.7 -object Natural {
     4.8 +object Nat {
     4.9  
    4.10 -  def apply(numeral: BigInt): Natural = new Natural(numeral max 0)
    4.11 -  def apply(numeral: Int): Natural = Natural(BigInt(numeral))
    4.12 -  def apply(numeral: String): Natural = Natural(BigInt(numeral))
    4.13 +  def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
    4.14 +  def apply(numeral: Int): Nat = Nat(BigInt(numeral))
    4.15 +  def apply(numeral: String): Nat = Nat(BigInt(numeral))
    4.16  
    4.17  }
    4.18  
    4.19 -class Natural private(private val value: BigInt) {
    4.20 +class Nat private(private val value: BigInt) {
    4.21  
    4.22    override def hashCode(): Int = this.value.hashCode()
    4.23  
    4.24    override def equals(that: Any): Boolean = that match {
    4.25 -    case that: Natural => this equals that
    4.26 +    case that: Nat => this equals that
    4.27      case _ => false
    4.28    }
    4.29  
    4.30    override def toString(): String = this.value.toString
    4.31  
    4.32 -  def equals(that: Natural): Boolean = this.value == that.value
    4.33 +  def equals(that: Nat): Boolean = this.value == that.value
    4.34  
    4.35    def as_BigInt: BigInt = this.value
    4.36    def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
    4.37        this.value.intValue
    4.38      else error("Int value out of range: " + this.value.toString)
    4.39  
    4.40 -  def +(that: Natural): Natural = new Natural(this.value + that.value)
    4.41 -  def -(that: Natural): Natural = Natural(this.value - that.value)
    4.42 -  def *(that: Natural): Natural = new Natural(this.value * that.value)
    4.43 +  def +(that: Nat): Nat = new Nat(this.value + that.value)
    4.44 +  def -(that: Nat): Nat = Nat(this.value - that.value)
    4.45 +  def *(that: Nat): Nat = new Nat(this.value * that.value)
    4.46  
    4.47 -  def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
    4.48 +  def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)
    4.49      else {
    4.50        val (k, l) = this.value /% that.value
    4.51 -      (new Natural(k), new Natural(l))
    4.52 +      (new Nat(k), new Nat(l))
    4.53      }
    4.54  
    4.55 -  def <=(that: Natural): Boolean = this.value <= that.value
    4.56 +  def <=(that: Nat): Boolean = this.value <= that.value
    4.57  
    4.58 -  def <(that: Natural): Boolean = this.value < that.value
    4.59 +  def <(that: Nat): Boolean = this.value < that.value
    4.60  
    4.61  }
    4.62  *}
    4.63 @@ -104,7 +104,7 @@
    4.64  
    4.65  code_type code_numeral
    4.66    (Haskell "Natural.Natural")
    4.67 -  (Scala "Natural")
    4.68 +  (Scala "Natural.Nat")
    4.69  
    4.70  setup {*
    4.71    fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
     5.1 --- a/src/HOL/Library/Efficient_Nat.thy	Wed Aug 25 22:47:04 2010 +0200
     5.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Aug 26 10:16:22 2010 +0200
     5.3 @@ -330,7 +330,7 @@
     5.4  
     5.5  code_type nat
     5.6    (Haskell "Nat.Nat")
     5.7 -  (Scala "Nat")
     5.8 +  (Scala "Nat.Nat")
     5.9  
    5.10  code_instance nat :: eq
    5.11    (Haskell -)
    5.12 @@ -397,7 +397,7 @@
    5.13  
    5.14  code_const int and nat
    5.15    (Haskell "toInteger" and "fromInteger")
    5.16 -  (Scala "!_.as'_BigInt" and "Nat")
    5.17 +  (Scala "!_.as'_BigInt" and "Nat.Nat")
    5.18  
    5.19  text {* Conversion from and to code numerals. *}
    5.20  
    5.21 @@ -405,14 +405,14 @@
    5.22    (SML "IntInf.toInt")
    5.23    (OCaml "_")
    5.24    (Haskell "!(fromInteger/ ./ toInteger)")
    5.25 -  (Scala "!Natural(_.as'_BigInt)")
    5.26 +  (Scala "!Natural.Nat(_.as'_BigInt)")
    5.27    (Eval "_")
    5.28  
    5.29  code_const Code_Numeral.nat_of
    5.30    (SML "IntInf.fromInt")
    5.31    (OCaml "_")
    5.32    (Haskell "!(fromInteger/ ./ toInteger)")
    5.33 -  (Scala "!Nat(_.as'_BigInt)")
    5.34 +  (Scala "!Nat.Nat(_.as'_BigInt)")
    5.35    (Eval "_")
    5.36  
    5.37  text {* Using target language arithmetic operations whenever appropriate *}
     6.1 --- a/src/Tools/Code/code_scala.ML	Wed Aug 25 22:47:04 2010 +0200
     6.2 +++ b/src/Tools/Code/code_scala.ML	Thu Aug 26 10:16:22 2010 +0200
     6.3 @@ -487,8 +487,8 @@
     6.4    literal_char = Library.enclose "'" "'" o char_scala,
     6.5    literal_string = quote o translate_string char_scala,
     6.6    literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
     6.7 -  literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
     6.8 -  literal_alternative_numeral = fn k => "Natural(" ^ numeral_scala k ^ ")",
     6.9 +  literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
    6.10 +  literal_alternative_numeral = fn k => "Natural.Nat(" ^ numeral_scala k ^ ")",
    6.11    literal_naive_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
    6.12    literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
    6.13    infix_cons = (6, "::")