src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 37947 844977c7abeb
parent 37878 d016aaead7a2
child 37964 0a1ae22df1f1
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 23 10:25:00 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 23 10:58:13 2010 +0200
     1.3 @@ -433,28 +433,28 @@
     1.4  type RealWorld = Control.Monad.ST.RealWorld;
     1.5  type ST s a = Control.Monad.ST.ST s a;
     1.6  type STRef s a = Data.STRef.STRef s a;
     1.7 -type STArray s a = Data.Array.ST.STArray s Int a;
     1.8 +type STArray s a = Data.Array.ST.STArray s Integer a;
     1.9  
    1.10  newSTRef = Data.STRef.newSTRef;
    1.11  readSTRef = Data.STRef.readSTRef;
    1.12  writeSTRef = Data.STRef.writeSTRef;
    1.13  
    1.14 -newArray :: Int -> a -> ST s (STArray s a);
    1.15 +newArray :: Integer -> a -> ST s (STArray s a);
    1.16  newArray k = Data.Array.ST.newArray (0, k);
    1.17  
    1.18  newListArray :: [a] -> ST s (STArray s a);
    1.19 -newListArray xs = Data.Array.ST.newListArray (0, length xs) xs;
    1.20 +newListArray xs = Data.Array.ST.newListArray (0, toInteger (length xs)) xs;
    1.21  
    1.22 -newFunArray :: Int -> (Int -> a) -> ST s (STArray s a);
    1.23 +newFunArray :: Integer -> (Integer -> a) -> ST s (STArray s a);
    1.24  newFunArray k f = Data.Array.ST.newListArray (0, k) (map f [0..k-1]);
    1.25  
    1.26 -lengthArray :: STArray s a -> ST s Int;
    1.27 +lengthArray :: STArray s a -> ST s Integer;
    1.28  lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
    1.29  
    1.30 -readArray :: STArray s a -> Int -> ST s a;
    1.31 +readArray :: STArray s a -> Integer -> ST s a;
    1.32  readArray = Data.Array.ST.readArray;
    1.33  
    1.34 -writeArray :: STArray s a -> Int -> a -> ST s ();
    1.35 +writeArray :: STArray s a -> Integer -> a -> ST s ();
    1.36  writeArray = Data.Array.ST.writeArray;*}
    1.37  
    1.38  code_reserved Haskell Heap