# HG changeset patch
# User haftmann
# Date 1279281517 -7200
# Node ID 336dae59af03b3432e7fe369ee7d67e482e89dc9
# Parent  27e7047d9ae6be8eeea1152ff82ecb2a65d6542a# Parent  ff1c9cb6dc5d17e7c736f8d26cdbe68fb6460712
merged

diff -r ff1c9cb6dc5d -r 336dae59af03 src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Fri Jul 16 13:57:46 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Fri Jul 16 13:58:37 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
diff -r ff1c9cb6dc5d -r 336dae59af03 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 16 13:57:46 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 16 13:58:37 2010 +0200
@@ -419,6 +419,81 @@
 code_const return (OCaml "!(fun/ ()/ ->/ _)")
 code_const Heap_Monad.raise' (OCaml "failwith")
 
+
+subsubsection {* Haskell *}
+
+text {* Adaption layer *}
+
+code_include Haskell "Heap"
+{*import qualified Control.Monad;
+import qualified Control.Monad.ST;
+import qualified Data.STRef;
+import qualified Data.Array.ST;
+
+type RealWorld = Control.Monad.ST.RealWorld;
+type ST s a = Control.Monad.ST.ST s a;
+type STRef s a = Data.STRef.STRef s a;
+type STArray s a = Data.Array.ST.STArray s Int a;
+
+newSTRef = Data.STRef.newSTRef;
+readSTRef = Data.STRef.readSTRef;
+writeSTRef = Data.STRef.writeSTRef;
+
+newArray :: Int -> a -> ST s (STArray s a);
+newArray k = Data.Array.ST.newArray (0, k);
+
+newListArray :: [a] -> ST s (STArray s a);
+newListArray xs = Data.Array.ST.newListArray (0, length xs) xs;
+
+newFunArray :: Int -> (Int -> a) -> ST s (STArray s a);
+newFunArray k f = Data.Array.ST.newListArray (0, k) (map f [0..k-1]);
+
+lengthArray :: STArray s a -> ST s Int;
+lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
+
+readArray :: STArray s a -> Int -> ST s a;
+readArray = Data.Array.ST.readArray;
+
+writeArray :: STArray s a -> Int -> a -> ST s ();
+writeArray = Data.Array.ST.writeArray;*}
+
+code_reserved Haskell Heap
+
+text {* Monad *}
+
+code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _")
+code_monad bind Haskell
+code_const return (Haskell "return")
+code_const Heap_Monad.raise' (Haskell "error")
+
+
+subsubsection {* Scala *}
+
+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 "('_: Unit)/ =>/ _")
+code_const Heap_Monad.raise' (Scala "!error(_)")
+
+
+subsubsection {* Target variants with less units *}
+
 setup {*
 
 let
@@ -483,58 +558,13 @@
 
 Code_Target.extend_target ("SML_imp", ("SML", imp_program))
 #> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program))
+#> Code_Target.extend_target ("Scala_imp", ("Scala", imp_program))
 
 end
 
 *}
 
 
-subsubsection {* Haskell *}
-
-text {* Adaption layer *}
-
-code_include Haskell "Heap"
-{*import qualified Control.Monad;
-import qualified Control.Monad.ST;
-import qualified Data.STRef;
-import qualified Data.Array.ST;
-
-type RealWorld = Control.Monad.ST.RealWorld;
-type ST s a = Control.Monad.ST.ST s a;
-type STRef s a = Data.STRef.STRef s a;
-type STArray s a = Data.Array.ST.STArray s Int a;
-
-newSTRef = Data.STRef.newSTRef;
-readSTRef = Data.STRef.readSTRef;
-writeSTRef = Data.STRef.writeSTRef;
-
-newArray :: Int -> a -> ST s (STArray s a);
-newArray k = Data.Array.ST.newArray (0, k);
-
-newListArray :: [a] -> ST s (STArray s a);
-newListArray xs = Data.Array.ST.newListArray (0, length xs) xs;
-
-newFunArray :: Int -> (Int -> a) -> ST s (STArray s a);
-newFunArray k f = Data.Array.ST.newListArray (0, k) (map f [0..k-1]);
-
-lengthArray :: STArray s a -> ST s Int;
-lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
-
-readArray :: STArray s a -> Int -> ST s a;
-readArray = Data.Array.ST.readArray;
-
-writeArray :: STArray s a -> Int -> a -> ST s ();
-writeArray = Data.Array.ST.writeArray;*}
-
-code_reserved Haskell Heap
-
-text {* Monad *}
-
-code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _")
-code_monad bind Haskell
-code_const return (Haskell "return")
-code_const Heap_Monad.raise' (Haskell "error")
-
 hide_const (open) Heap heap guard raise' fold_map
 
 end
diff -r ff1c9cb6dc5d -r 336dae59af03 src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Fri Jul 16 13:57:46 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Fri Jul 16 13:58:37 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