src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 37838 28848d338261
parent 37835 d8fdbcbde4b6
child 37842 27e7047d9ae6
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Jul 15 10:16:17 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 16 10:23:21 2010 +0200
     1.3 @@ -419,6 +419,69 @@
     1.4  code_const return (OCaml "!(fun/ ()/ ->/ _)")
     1.5  code_const Heap_Monad.raise' (OCaml "failwith")
     1.6  
     1.7 +
     1.8 +subsubsection {* Haskell *}
     1.9 +
    1.10 +text {* Adaption layer *}
    1.11 +
    1.12 +code_include Haskell "Heap"
    1.13 +{*import qualified Control.Monad;
    1.14 +import qualified Control.Monad.ST;
    1.15 +import qualified Data.STRef;
    1.16 +import qualified Data.Array.ST;
    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 Int 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 :: Int -> a -> ST s (STArray s a);
    1.28 +newArray k = Data.Array.ST.newArray (0, k);
    1.29 +
    1.30 +newListArray :: [a] -> ST s (STArray s a);
    1.31 +newListArray xs = Data.Array.ST.newListArray (0, length xs) xs;
    1.32 +
    1.33 +newFunArray :: Int -> (Int -> a) -> ST s (STArray s a);
    1.34 +newFunArray k f = Data.Array.ST.newListArray (0, k) (map f [0..k-1]);
    1.35 +
    1.36 +lengthArray :: STArray s a -> ST s Int;
    1.37 +lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
    1.38 +
    1.39 +readArray :: STArray s a -> Int -> ST s a;
    1.40 +readArray = Data.Array.ST.readArray;
    1.41 +
    1.42 +writeArray :: STArray s a -> Int -> a -> ST s ();
    1.43 +writeArray = Data.Array.ST.writeArray;*}
    1.44 +
    1.45 +code_reserved Haskell Heap
    1.46 +
    1.47 +text {* Monad *}
    1.48 +
    1.49 +code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _")
    1.50 +code_monad bind Haskell
    1.51 +code_const return (Haskell "return")
    1.52 +code_const Heap_Monad.raise' (Haskell "error")
    1.53 +
    1.54 +
    1.55 +subsubsection {* Scala *}
    1.56 +
    1.57 +code_include Haskell "Heap"
    1.58 +{*def bind[A, B](f: Unit => A, g: A => Unit => B, u: Unit): B = g (f ()) ()*}
    1.59 +
    1.60 +code_reserved Scala Heap
    1.61 +
    1.62 +code_type Heap (Scala "Unit/ =>/ _")
    1.63 +code_const bind (Scala "Heap.bind")
    1.64 +code_const return (Scala "!(()/ =>/ _)")
    1.65 +code_const Heap_Monad.raise' (Scala "!error(_)")
    1.66 +
    1.67 +
    1.68 +subsubsection {* Target variants with less units *}
    1.69 +
    1.70  setup {*
    1.71  
    1.72  let
    1.73 @@ -483,58 +546,13 @@
    1.74  
    1.75  Code_Target.extend_target ("SML_imp", ("SML", imp_program))
    1.76  #> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program))
    1.77 +#> Code_Target.extend_target ("Scala_imp", ("Scala", imp_program))
    1.78  
    1.79  end
    1.80  
    1.81  *}
    1.82  
    1.83  
    1.84 -subsubsection {* Haskell *}
    1.85 -
    1.86 -text {* Adaption layer *}
    1.87 -
    1.88 -code_include Haskell "Heap"
    1.89 -{*import qualified Control.Monad;
    1.90 -import qualified Control.Monad.ST;
    1.91 -import qualified Data.STRef;
    1.92 -import qualified Data.Array.ST;
    1.93 -
    1.94 -type RealWorld = Control.Monad.ST.RealWorld;
    1.95 -type ST s a = Control.Monad.ST.ST s a;
    1.96 -type STRef s a = Data.STRef.STRef s a;
    1.97 -type STArray s a = Data.Array.ST.STArray s Int a;
    1.98 -
    1.99 -newSTRef = Data.STRef.newSTRef;
   1.100 -readSTRef = Data.STRef.readSTRef;
   1.101 -writeSTRef = Data.STRef.writeSTRef;
   1.102 -
   1.103 -newArray :: Int -> a -> ST s (STArray s a);
   1.104 -newArray k = Data.Array.ST.newArray (0, k);
   1.105 -
   1.106 -newListArray :: [a] -> ST s (STArray s a);
   1.107 -newListArray xs = Data.Array.ST.newListArray (0, length xs) xs;
   1.108 -
   1.109 -newFunArray :: Int -> (Int -> a) -> ST s (STArray s a);
   1.110 -newFunArray k f = Data.Array.ST.newListArray (0, k) (map f [0..k-1]);
   1.111 -
   1.112 -lengthArray :: STArray s a -> ST s Int;
   1.113 -lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
   1.114 -
   1.115 -readArray :: STArray s a -> Int -> ST s a;
   1.116 -readArray = Data.Array.ST.readArray;
   1.117 -
   1.118 -writeArray :: STArray s a -> Int -> a -> ST s ();
   1.119 -writeArray = Data.Array.ST.writeArray;*}
   1.120 -
   1.121 -code_reserved Haskell Heap
   1.122 -
   1.123 -text {* Monad *}
   1.124 -
   1.125 -code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _")
   1.126 -code_monad bind Haskell
   1.127 -code_const return (Haskell "return")
   1.128 -code_const Heap_Monad.raise' (Haskell "error")
   1.129 -
   1.130  hide_const (open) Heap heap guard raise' fold_map
   1.131  
   1.132  end