src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 51143 0a2371e7ced3
parent 48073 1b609a7837ef
child 51485 637aa1649ac7
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Feb 15 08:31:30 2013 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -8,7 +8,6 @@
     1.4  imports
     1.5    Heap
     1.6    "~~/src/HOL/Library/Monad_Syntax"
     1.7 -  "~~/src/HOL/Library/Code_Natural"
     1.8  begin
     1.9  
    1.10  subsection {* The monad *}
    1.11 @@ -529,33 +528,31 @@
    1.12  import qualified Data.STRef;
    1.13  import qualified Data.Array.ST;
    1.14  
    1.15 -import Natural;
    1.16 -
    1.17  type RealWorld = Control.Monad.ST.RealWorld;
    1.18  type ST s a = Control.Monad.ST.ST s a;
    1.19  type STRef s a = Data.STRef.STRef s a;
    1.20 -type STArray s a = Data.Array.ST.STArray s Natural a;
    1.21 +type STArray s a = Data.Array.ST.STArray s Integer a;
    1.22  
    1.23  newSTRef = Data.STRef.newSTRef;
    1.24  readSTRef = Data.STRef.readSTRef;
    1.25  writeSTRef = Data.STRef.writeSTRef;
    1.26  
    1.27 -newArray :: Natural -> a -> ST s (STArray s a);
    1.28 +newArray :: Integer -> a -> ST s (STArray s a);
    1.29  newArray k = Data.Array.ST.newArray (0, k);
    1.30  
    1.31  newListArray :: [a] -> ST s (STArray s a);
    1.32  newListArray xs = Data.Array.ST.newListArray (0, (fromInteger . toInteger . length) xs) xs;
    1.33  
    1.34 -newFunArray :: Natural -> (Natural -> a) -> ST s (STArray s a);
    1.35 +newFunArray :: Integer -> (Integer -> a) -> ST s (STArray s a);
    1.36  newFunArray k f = Data.Array.ST.newListArray (0, k) (map f [0..k-1]);
    1.37  
    1.38 -lengthArray :: STArray s a -> ST s Natural;
    1.39 +lengthArray :: STArray s a -> ST s Integer;
    1.40  lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
    1.41  
    1.42 -readArray :: STArray s a -> Natural -> ST s a;
    1.43 +readArray :: STArray s a -> Integer -> ST s a;
    1.44  readArray = Data.Array.ST.readArray;
    1.45  
    1.46 -writeArray :: STArray s a -> Natural -> a -> ST s ();
    1.47 +writeArray :: STArray s a -> Integer -> a -> ST s ();
    1.48  writeArray = Data.Array.ST.writeArray;*}
    1.49  
    1.50  code_reserved Haskell Heap
    1.51 @@ -590,16 +587,16 @@
    1.52  
    1.53  object Array {
    1.54    import collection.mutable.ArraySeq
    1.55 -  def alloc[A](n: Natural)(x: A): ArraySeq[A] =
    1.56 -    ArraySeq.fill(n.as_Int)(x)
    1.57 -  def make[A](n: Natural)(f: Natural => A): ArraySeq[A] =
    1.58 -    ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural(k)))
    1.59 -  def len[A](a: ArraySeq[A]): Natural =
    1.60 -    Natural(a.length)
    1.61 -  def nth[A](a: ArraySeq[A], n: Natural): A =
    1.62 -    a(n.as_Int)
    1.63 -  def upd[A](a: ArraySeq[A], n: Natural, x: A): Unit =
    1.64 -    a.update(n.as_Int, x)
    1.65 +  def alloc[A](n: BigInt)(x: A): ArraySeq[A] =
    1.66 +    ArraySeq.fill(n.toInt)(x)
    1.67 +  def make[A](n: BigInt)(f: BigInt => A): ArraySeq[A] =
    1.68 +    ArraySeq.tabulate(n.toInt)((k: Int) => f(BigInt(k)))
    1.69 +  def len[A](a: ArraySeq[A]): BigInt =
    1.70 +    BigInt(a.length)
    1.71 +  def nth[A](a: ArraySeq[A], n: BigInt): A =
    1.72 +    a(n.toInt)
    1.73 +  def upd[A](a: ArraySeq[A], n: BigInt, x: A): Unit =
    1.74 +    a.update(n.toInt, x)
    1.75    def freeze[A](a: ArraySeq[A]): List[A] =
    1.76      a.toList
    1.77  }