src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 37964 0a1ae22df1f1
parent 37947 844977c7abeb
child 38057 5ac79735cfef
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Sat Jul 24 18:08:43 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jul 26 11:09:44 2010 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* A monad with a polymorphic heap and primitive reasoning infrastructure *}
     1.5  
     1.6  theory Heap_Monad
     1.7 -imports Heap Monad_Syntax
     1.8 +imports Heap Monad_Syntax Code_Natural
     1.9  begin
    1.10  
    1.11  subsection {* The monad *}
    1.12 @@ -430,31 +430,33 @@
    1.13  import qualified Data.STRef;
    1.14  import qualified Data.Array.ST;
    1.15  
    1.16 +import Natural;
    1.17 +
    1.18  type RealWorld = Control.Monad.ST.RealWorld;
    1.19  type ST s a = Control.Monad.ST.ST s a;
    1.20  type STRef s a = Data.STRef.STRef s a;
    1.21 -type STArray s a = Data.Array.ST.STArray s Integer a;
    1.22 +type STArray s a = Data.Array.ST.STArray s Natural a;
    1.23  
    1.24  newSTRef = Data.STRef.newSTRef;
    1.25  readSTRef = Data.STRef.readSTRef;
    1.26  writeSTRef = Data.STRef.writeSTRef;
    1.27  
    1.28 -newArray :: Integer -> a -> ST s (STArray s a);
    1.29 +newArray :: Natural -> a -> ST s (STArray s a);
    1.30  newArray k = Data.Array.ST.newArray (0, k);
    1.31  
    1.32  newListArray :: [a] -> ST s (STArray s a);
    1.33 -newListArray xs = Data.Array.ST.newListArray (0, toInteger (length xs)) xs;
    1.34 +newListArray xs = Data.Array.ST.newListArray (0, (fromInteger . toInteger . length) xs) xs;
    1.35  
    1.36 -newFunArray :: Integer -> (Integer -> a) -> ST s (STArray s a);
    1.37 +newFunArray :: Natural -> (Natural -> a) -> ST s (STArray s a);
    1.38  newFunArray k f = Data.Array.ST.newListArray (0, k) (map f [0..k-1]);
    1.39  
    1.40 -lengthArray :: STArray s a -> ST s Integer;
    1.41 +lengthArray :: STArray s a -> ST s Natural;
    1.42  lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
    1.43  
    1.44 -readArray :: STArray s a -> Integer -> ST s a;
    1.45 +readArray :: STArray s a -> Natural -> ST s a;
    1.46  readArray = Data.Array.ST.readArray;
    1.47  
    1.48 -writeArray :: STArray s a -> Integer -> a -> ST s ();
    1.49 +writeArray :: STArray s a -> Natural -> a -> ST s ();
    1.50  writeArray = Data.Array.ST.writeArray;*}
    1.51  
    1.52  code_reserved Haskell Heap
    1.53 @@ -470,7 +472,10 @@
    1.54  subsubsection {* Scala *}
    1.55  
    1.56  code_include Scala "Heap"
    1.57 -{*def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
    1.58 +{*import collection.mutable.ArraySeq
    1.59 +import Natural._
    1.60 +
    1.61 +def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
    1.62  
    1.63  class Ref[A](x: A) {
    1.64    var value = x
    1.65 @@ -478,13 +483,20 @@
    1.66  
    1.67  object Ref {
    1.68    def apply[A](x: A): Ref[A] = new Ref[A](x)
    1.69 +  def lookup[A](r: Ref[A]): A = r.value
    1.70 +  def update[A](r: Ref[A], x: A): Unit = { r.value = x }
    1.71  }
    1.72  
    1.73 -def lookup[A](r: Ref[A]): A = r.value
    1.74 +object Array {
    1.75 +  def alloc[A](n: Natural)(x: A): ArraySeq[A] = ArraySeq.fill(n.as_Int)(x)
    1.76 +  def make[A](n: Natural)(f: Natural => A): ArraySeq[A] = ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural(k)))
    1.77 +  def len[A](a: ArraySeq[A]): Natural = Natural(a.length)
    1.78 +  def nth[A](a: ArraySeq[A], n: Natural): A = a(n.as_Int)
    1.79 +  def upd[A](a: ArraySeq[A], n: Natural, x: A): Unit = a.update(n.as_Int, x)
    1.80 +  def freeze[A](a: ArraySeq[A]): List[A] = a.toList
    1.81 +}*}
    1.82  
    1.83 -def update[A](r: Ref[A], x: A): Unit = { r.value = x }*}
    1.84 -
    1.85 -code_reserved Scala Heap
    1.86 +code_reserved Scala bind Ref Array
    1.87  
    1.88  code_type Heap (Scala "Unit/ =>/ _")
    1.89  code_const bind (Scala "bind")