--- a/src/HOL/Imperative_HOL/Array.thy Tue Feb 03 16:54:31 2009 +0100
+++ b/src/HOL/Imperative_HOL/Array.thy Tue Feb 03 19:37:00 2009 +0100
@@ -198,12 +198,12 @@
subsubsection {* Haskell *}
-code_type array (Haskell "STArray/ RealWorld/ _")
+code_type array (Haskell "Heap.STArray/ Heap.RealWorld/ _")
code_const Array (Haskell "error/ \"bare Array\"")
-code_const Array.new' (Haskell "newArray/ (0,/ _)")
-code_const Array.of_list' (Haskell "newListArray/ (0,/ _)")
-code_const Array.length' (Haskell "lengthArray")
-code_const Array.nth' (Haskell "readArray")
-code_const Array.upd' (Haskell "writeArray")
+code_const Array.new' (Haskell "Heap.newArray/ (0,/ _)")
+code_const Array.of_list' (Haskell "Heap.newListArray/ (0,/ _)")
+code_const Array.length' (Haskell "Heap.lengthArray")
+code_const Array.nth' (Haskell "Heap.readArray")
+code_const Array.upd' (Haskell "Heap.writeArray")
end
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Feb 03 16:54:31 2009 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Feb 03 19:37:00 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Library/Heap_Monad.thy
- ID: $Id$
Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
*)
@@ -375,7 +374,7 @@
text {* Adaption layer *}
-code_include Haskell "STMonad"
+code_include Haskell "Heap"
{*import qualified Control.Monad;
import qualified Control.Monad.ST;
import qualified Data.STRef;
@@ -386,9 +385,6 @@
type STRef s a = Data.STRef.STRef s a;
type STArray s a = Data.Array.ST.STArray s Int a;
-runST :: (forall s. ST s a) -> a;
-runST s = Control.Monad.ST.runST s;
-
newSTRef = Data.STRef.newSTRef;
readSTRef = Data.STRef.readSTRef;
writeSTRef = Data.STRef.writeSTRef;
@@ -408,14 +404,11 @@
writeArray :: STArray s a -> Int -> a -> ST s ();
writeArray = Data.Array.ST.writeArray;*}
-code_reserved Haskell RealWorld ST STRef Array
- runST
- newSTRef reasSTRef writeSTRef
- newArray newListArray lengthArray readArray writeArray
+code_reserved Haskell Heap
text {* Monad *}
-code_type Heap (Haskell "ST/ RealWorld/ _")
+code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _")
code_const Heap (Haskell "error/ \"bare Heap\"")
code_monad "op \<guillemotright>=" Haskell
code_const return (Haskell "return")
--- a/src/HOL/Imperative_HOL/Ref.thy Tue Feb 03 16:54:31 2009 +0100
+++ b/src/HOL/Imperative_HOL/Ref.thy Tue Feb 03 19:37:00 2009 +0100
@@ -82,10 +82,10 @@
subsubsection {* Haskell *}
-code_type ref (Haskell "STRef/ RealWorld/ _")
+code_type ref (Haskell "Heap.STRef/ Heap.RealWorld/ _")
code_const Ref (Haskell "error/ \"bare Ref\"")
-code_const Ref.new (Haskell "newSTRef")
-code_const Ref.lookup (Haskell "readSTRef")
-code_const Ref.update (Haskell "writeSTRef")
+code_const Ref.new (Haskell "Heap.newSTRef")
+code_const Ref.lookup (Haskell "Heap.readSTRef")
+code_const Ref.update (Haskell "Heap.writeSTRef")
end
\ No newline at end of file
--- a/src/HOL/Library/Efficient_Nat.thy Tue Feb 03 16:54:31 2009 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy Tue Feb 03 19:37:00 2009 +0100
@@ -308,7 +308,7 @@
code_reserved Haskell Nat
code_type nat
- (Haskell "Nat")
+ (Haskell "Nat.Nat")
code_instance nat :: eq
(Haskell -)
--- a/src/HOL/ex/ImperativeQuicksort.thy Tue Feb 03 16:54:31 2009 +0100
+++ b/src/HOL/ex/ImperativeQuicksort.thy Tue Feb 03 19:37:00 2009 +0100
@@ -629,9 +629,9 @@
ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
-export_code qsort in SML_imp module_name Arr
-export_code qsort in OCaml module_name Arr file -
-export_code qsort in OCaml_imp module_name Arr file -
-export_code qsort in Haskell module_name Arr file -
+export_code qsort in SML_imp module_name QSort
+export_code qsort in OCaml module_name QSort file -
+export_code qsort in OCaml_imp module_name QSort file -
+export_code qsort in Haskell module_name QSort file -
end
\ No newline at end of file