# HG changeset patch
# User haftmann
# Date 1280135384 -7200
# Node ID 0a1ae22df1f1042ed467878a10cf3bba90e3500f
# Parent  6fe5fa827f188860af59d1793e8bad7b013082a6
use Natural as index type for Haskell and Scala

diff -r 6fe5fa827f18 -r 0a1ae22df1f1 src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Sat Jul 24 18:08:43 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Mon Jul 26 11:09:44 2010 +0200
@@ -484,13 +484,11 @@
 
 code_type array (Scala "!collection.mutable.ArraySeq[_]")
 code_const Array (Scala "!error(\"bare Array\")")
-code_const Array.new' (Scala "('_: Unit)/ => / collection.mutable.ArraySeq.fill((_))((_))")
-code_const Array.make' (Scala "('_: Unit)/ =>/ collection.mutable.ArraySeq.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
+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
diff -r 6fe5fa827f18 -r 0a1ae22df1f1 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Sat Jul 24 18:08:43 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jul 26 11:09:44 2010 +0200
@@ -5,7 +5,7 @@
 header {* A monad with a polymorphic heap and primitive reasoning infrastructure *}
 
 theory Heap_Monad
-imports Heap Monad_Syntax
+imports Heap Monad_Syntax Code_Natural
 begin
 
 subsection {* The monad *}
@@ -430,31 +430,33 @@
 import qualified Data.STRef;
 import qualified Data.Array.ST;
 
+import Natural;
+
 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 Integer a;
+type STArray s a = Data.Array.ST.STArray s Natural a;
 
 newSTRef = Data.STRef.newSTRef;
 readSTRef = Data.STRef.readSTRef;
 writeSTRef = Data.STRef.writeSTRef;
 
-newArray :: Integer -> a -> ST s (STArray s a);
+newArray :: Natural -> 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, toInteger (length xs)) xs;
+newListArray xs = Data.Array.ST.newListArray (0, (fromInteger . toInteger . length) xs) xs;
 
-newFunArray :: Integer -> (Integer -> a) -> ST s (STArray s a);
+newFunArray :: Natural -> (Natural -> 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 Integer;
+lengthArray :: STArray s a -> ST s Natural;
 lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
 
-readArray :: STArray s a -> Integer -> ST s a;
+readArray :: STArray s a -> Natural -> ST s a;
 readArray = Data.Array.ST.readArray;
 
-writeArray :: STArray s a -> Integer -> a -> ST s ();
+writeArray :: STArray s a -> Natural -> a -> ST s ();
 writeArray = Data.Array.ST.writeArray;*}
 
 code_reserved Haskell Heap
@@ -470,7 +472,10 @@
 subsubsection {* Scala *}
 
 code_include Scala "Heap"
-{*def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
+{*import collection.mutable.ArraySeq
+import Natural._
+
+def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
 
 class Ref[A](x: A) {
   var value = x
@@ -478,13 +483,20 @@
 
 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 }
 }
 
-def lookup[A](r: Ref[A]): A = r.value
+object Array {
+  def alloc[A](n: Natural)(x: A): ArraySeq[A] = ArraySeq.fill(n.as_Int)(x)
+  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, x: A): Unit = a.update(n.as_Int, x)
+  def freeze[A](a: ArraySeq[A]): List[A] = a.toList
+}*}
 
-def update[A](r: Ref[A], x: A): Unit = { r.value = x }*}
-
-code_reserved Scala Heap
+code_reserved Scala bind Ref Array
 
 code_type Heap (Scala "Unit/ =>/ _")
 code_const bind (Scala "bind")