a first sketch for Imperative HOL witht Scala

--- a/src/HOL/Imperative_HOL/Array.thy	Fri Jul 16 10:23:21 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Fri Jul 16 13:58:29 2010 +0200
@@ -479,4 +479,19 @@
 code_const Array.nth' (Haskell "Heap.readArray")
 code_const Array.upd' (Haskell "Heap.writeArray")
 
+
+text {* Scala *}
+
+code_type array (Scala "!Array[_]")
+code_const Array (Scala "!error(\"bare Array\")")
+code_const Array.new' (Scala "('_: Unit)/ => / Array.fill((_))((_))")
+code_const Array.of_list (Scala "('_: Unit)/ =>/ _.toArray")
+code_const Array.make' (Scala "('_: Unit)/ =>/ Array.tabulate((_),/ (_))")
+code_const Array.len' (Scala "('_: Unit)/ =>/ _.length")
+code_const Array.nth' (Scala "('_: Unit)/ =>/ _((_))")
+code_const Array.upd' (Scala "('_: Unit)/ =>/ _.update((_),/ (_))")
+code_const Array.freeze (Scala "('_: Unit)/ =>/ _.toList")
+
+code_reserved Scala Array
+
 end

--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 16 10:23:21 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 16 13:58:29 2010 +0200
@@ -469,14 +469,26 @@
 
 subsubsection {* Scala *}
 
-code_include Haskell "Heap"
-{*def bind[A, B](f: Unit => A, g: A => Unit => B, u: Unit): B = g (f ()) ()*}
+code_include Scala "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
+}
+
+object Ref {
+  def apply[A](x: A): Ref[A] = new Ref[A](x)
+}
+
+def lookup[A](r: Ref[A]): A = r.value
+
+def update[A](r: Ref[A], x: A): Unit = { r.value = x }*}
 
 code_reserved Scala Heap
 
 code_type Heap (Scala "Unit/ =>/ _")
-code_const bind (Scala "Heap.bind")
-code_const return (Scala "!(()/ =>/ _)")
+code_const bind (Scala "!Heap.bind((_), (_))")
+code_const return (Scala "('_: Unit)/ =>/ _")
 code_const Heap_Monad.raise' (Scala "!error(_)")
 
 

--- a/src/HOL/Imperative_HOL/Ref.thy	Fri Jul 16 10:23:21 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Fri Jul 16 13:58:29 2010 +0200
@@ -293,4 +293,13 @@
 code_const Ref.lookup (Haskell "Heap.readSTRef")
 code_const Ref.update (Haskell "Heap.writeSTRef")
 
+
+text {* Scala *}
+
+code_type ref (Scala "!Heap.Ref[_]")
+code_const Ref (Scala "!error(\"bare Ref\")")
+code_const ref (Scala "('_: Unit)/ =>/ Heap.Ref((_))")
+code_const Ref.lookup (Scala "('_: Unit)/ =>/ Heap.lookup((_))")
+code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.update((_), (_))")
+
 end